proposition: Lemma RiemannInt_P11 : forall (f:R -> R) (a b l:R) (un:nat -> posreal) (phi1 phi2 psi1 psi2:nat -> StepFun a b), Un_cv un 0 -> (forall n:nat, (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - phi1 n t) <= psi1 n t) /\ Rabs (RiemannInt_SF (psi1 n)) < un n) -> (forall n:nat, (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - phi2 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < un n) -> Un_cv (fun N:nat => RiemannInt_SF (phi1 N)) l -> Un_cv (fun N:nat => RiemannInt_SF (phi2 N)) l.
proof: Proof. unfold Un_cv; intro f; intros; intros. case (Rle_dec a b); intro Hyp. - assert (H4 : 0 < eps / 3) by lra. elim (H _ H4); clear H; intros N0 H. elim (H2 _ H4); clear H2; intros N1 H2. set (N := max N0 N1); exists N; intros; unfold Rdist. apply Rle_lt_trans with (Rabs (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n)) + Rabs (RiemannInt_SF (phi1 n) - l)). { replace (RiemannInt_SF (phi2 n) - l) with (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n) + (RiemannInt_SF (phi1 n) - l)); [ apply Rabs_triang | ring ]. } replace eps with (2 * (eps / 3) + eps / 3) by lra. apply Rplus_lt_compat. 2:{ unfold Rdist in H2; apply H2; unfold ge; apply Nat.le_trans with N; try assumption; unfold N; apply Nat.le_max_r. } replace (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n)) with (RiemannInt_SF (phi2 n) + -1 * RiemannInt_SF (phi1 n)); [ idtac | ring ]. rewrite <- StepFun_P30. apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 (-1) (phi2 n) (phi1 n)))))). { apply StepFun_P34; assumption. } apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P28 1 (psi1 n) (psi2 n)))). { apply StepFun_P37; try assumption; intros; simpl; rewrite Rmult_1_l. apply Rle_trans with (Rabs (phi2 n x - f x) + Rabs (f x - phi1 n x)). { replace (phi2 n x + -1 * phi1 n x) with (phi2 n x - f x + (f x - phi1 n x)); [ apply Rabs_triang | ring ]. } rewrite (Rplus_comm (psi1 n x)); apply Rplus_le_compat. { rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; elim (H1 n); intros; apply H7. assert (H10 : Rmin a b = a). { unfold Rmin; decide (Rle_dec a b) with Hyp; reflexivity. } assert (H11 : Rmax a b = b). { unfold Rmax; decide (Rle_dec a b) with Hyp; reflexivity. } rewrite H10; rewrite H11; elim H6; intros; split; left; assumption. } elim (H0 n); intros; apply H7; assert (H10 : Rmin a b = a). { unfold Rmin; decide (Rle_dec a b) with Hyp; reflexivity. } assert (H11 : Rmax a b = b). { unfold Rmax; decide (Rle_dec a b) with Hyp; reflexivity. } rewrite H10; rewrite H11; elim H6; intros; split; left; assumption. } rewrite StepFun_P30; rewrite Rmult_1_l; rewrite <-Rplus_diag; apply Rplus_lt_compat. { apply Rlt_trans with (pos (un n)). { elim (H0 n); intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi1 n))). { apply RRle_abs. } assumption. } replace (pos (un n)) with (Rdist (un n) 0). { apply H; unfold ge; apply Nat.le_trans with N; try assumption. unfold N; apply Nat.le_max_l. } unfold Rdist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right. apply Rle_ge; left; apply (cond_pos (un n)). } apply Rlt_trans with (pos (un n)). { elim (H1 n); intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi2 n))). { apply RRle_abs; assumption. } assumption. } replace (pos (un n)) with (Rdist (un n) 0). { apply H; unfold ge; apply Nat.le_trans with N; try assumption; unfold N; apply Nat.le_max_l. } unfold Rdist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge; left; apply (cond_pos (un n)). - assert (H4 : 0 < eps / 3) by lra. elim (H _ H4); clear H; intros N0 H. elim (H2 _ H4); clear H2; intros N1 H2. set (N := max N0 N1); exists N; intros; unfold Rdist. apply Rle_lt_trans with (Rabs (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n)) + Rabs (RiemannInt_SF (phi1 n) - l)). { replace (RiemannInt_SF (phi2 n) - l) with (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n) + (RiemannInt_SF (phi1 n) - l)); [ apply Rabs_triang | ring ]. } assert (Hyp_b : b <= a). { auto with real. } replace eps with (2 * (eps / 3) + eps / 3) by lra. apply Rplus_lt_compat. 2:{ unfold Rdist in H2; apply H2; unfold ge; apply Nat.le_trans with N; try assumption; unfold N; apply Nat.le_max_r. } replace (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n)) with (RiemannInt_SF (phi2 n) + -1 * RiemannInt_SF (phi1 n)); [ idtac | ring ]. rewrite <- StepFun_P30. rewrite StepFun_P39. rewrite Rabs_Ropp. apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P6 (pre (mkStepFun (StepFun_P28 (-1) (phi2 n) (phi1 n))))))))). { apply StepFun_P34; try assumption. } apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P6 (pre (mkStepFun (StepFun_P28 1 (psi1 n) (psi2 n))))))). { apply StepFun_P37; try assumption. intros; simpl; rewrite Rmult_1_l. apply Rle_trans with (Rabs (phi2 n x - f x) + Rabs (f x - phi1 n x)). { replace (phi2 n x + -1 * phi1 n x) with (phi2 n x - f x + (f x - phi1 n x)); [ apply Rabs_triang | ring ]. } rewrite (Rplus_comm (psi1 n x)); apply Rplus_le_compat. { rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; elim (H1 n); intros; apply H7. assert (H10 : Rmin a b = b). { unfold Rmin; case (Rle_dec a b); intro; [ elim Hyp; assumption | reflexivity ]. } assert (H11 : Rmax a b = a). { unfold Rmax; case (Rle_dec a b); intro; [ elim Hyp; assumption | reflexivity ]. } rewrite H10; rewrite H11; elim H6; intros; split; left; assumption. } elim (H0 n); intros; apply H7; assert (H10 : Rmin a b = b). { unfold Rmin; case (Rle_dec a b); intro; [ elim Hyp; assumption | reflexivity ]. } assert (H11 : Rmax a b = a). { unfold Rmax; case (Rle_dec a b); intro; [ elim Hyp; assumption | reflexivity ]. } rewrite H10; rewrite H11; elim H6; intros; split; left; assumption. } rewrite <- (Ropp_involutive (RiemannInt_SF (mkStepFun (StepFun_P6 (pre (mkStepFun (StepFun_P28 1 (psi1 n) (psi2 n)))))))). rewrite <- StepFun_P39. rewrite StepFun_P30. rewrite Rmult_1_l; rewrite <-Rplus_diag. rewrite Ropp_plus_distr; apply Rplus_lt_compat. { apply Rlt_trans with (pos (un n)). { elim (H0 n); intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi1 n))). { rewrite <- Rabs_Ropp; apply RRle_abs. } assumption. } replace (pos (un n)) with (Rdist (un n) 0). { apply H; unfold ge; apply Nat.le_trans with N; try assumption. unfold N; apply Nat.le_max_l. } unfold Rdist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right. apply Rle_ge; left; apply (cond_pos (un n)). } apply Rlt_trans with (pos (un n)). { elim (H1 n); intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi2 n))). { rewrite <- Rabs_Ropp; apply RRle_abs; assumption. } assumption. } replace (pos (un n)) with (Rdist (un n) 0). { apply H; unfold ge; apply Nat.le_trans with N; try assumption; unfold N; apply Nat.le_max_l. } unfold Rdist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge; left; apply (cond_pos (un n)). Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra