proposition: Lemma RiemannInt_P4 : forall (f:R -> R) (a b l:R) (pr1 pr2:Riemann_integrable f a b) (un vn:nat -> posreal), Un_cv un 0 -> Un_cv vn 0 -> Un_cv (fun N:nat => RiemannInt_SF (phi_sequence un pr1 N)) l -> Un_cv (fun N:nat => RiemannInt_SF (phi_sequence vn pr2 N)) l.
proof: Proof. unfold Un_cv; unfold Rdist; intros f; intros; assert (H3 : 0 < eps / 3). { unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. } elim (H _ H3); clear H; intros N0 H; elim (H0 _ H3); clear H0; intros N1 H0; elim (H1 _ H3); clear H1; intros N2 H1; set (N := max (max N0 N1) N2); exists N; intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF (phi_sequence vn pr2 n) - RiemannInt_SF (phi_sequence un pr1 n)) + Rabs (RiemannInt_SF (phi_sequence un pr1 n) - l)). { replace (RiemannInt_SF (phi_sequence vn pr2 n) - l) with (RiemannInt_SF (phi_sequence vn pr2 n) - RiemannInt_SF (phi_sequence un pr1 n) + (RiemannInt_SF (phi_sequence un pr1 n) - l)); [ apply Rabs_triang | ring ]. } replace eps with (2 * (eps / 3) + eps / 3) by lra. apply Rplus_lt_compat. 2:{ apply H1; unfold ge; apply Nat.le_trans with N; try assumption; unfold N; apply Nat.le_max_r. } elim (phi_sequence_prop vn pr2 n); intros psi_vn H5; elim (phi_sequence_prop un pr1 n); intros psi_un H6; replace (RiemannInt_SF (phi_sequence vn pr2 n) - RiemannInt_SF (phi_sequence un pr1 n)) with (RiemannInt_SF (phi_sequence vn pr2 n) + -1 * RiemannInt_SF (phi_sequence un pr1 n)); [ idtac | ring ]; rewrite <- StepFun_P30. destruct (Rle_dec a b) as [Hle|Hnle]. - apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 (-1) (phi_sequence vn pr2 n) (phi_sequence un pr1 n)))))). { apply StepFun_P34; assumption. } apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P28 1 psi_un psi_vn))). { apply StepFun_P37; try assumption; intros; simpl; rewrite Rmult_1_l; apply Rle_trans with (Rabs (phi_sequence vn pr2 n x - f x) + Rabs (f x - phi_sequence un pr1 n x)). { replace (phi_sequence vn pr2 n x + -1 * phi_sequence un pr1 n x) with (phi_sequence vn pr2 n x - f x + (f x - phi_sequence un pr1 n x)); [ apply Rabs_triang | ring ]. } assert (H10 : Rmin a b = a). { unfold Rmin; decide (Rle_dec a b) with Hle; reflexivity. } assert (H11 : Rmax a b = b). { unfold Rmax; decide (Rle_dec a b) with Hle; reflexivity. } rewrite (Rplus_comm (psi_un x)); apply Rplus_le_compat. { rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; destruct H5 as (H8,H9); apply H8. rewrite H10; rewrite H11; elim H7; intros; split; left; assumption. } elim H6; intros; apply H8. rewrite H10; rewrite H11; elim H7; 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 H6; intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF psi_un)). { apply RRle_abs. } assumption. } replace (pos (un n)) with (Rabs (un n - 0)); [ apply H; unfold ge; apply Nat.le_trans with N; try assumption; unfold N; apply Nat.le_trans with (max N0 N1); apply Nat.le_max_l | 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 (vn n)). { elim H5; intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF psi_vn)). { apply RRle_abs; assumption. } assumption. } replace (pos (vn n)) with (Rabs (vn n - 0)); [ apply H0; unfold ge; apply Nat.le_trans with N; try assumption; unfold N; apply Nat.le_trans with (max N0 N1); [ apply Nat.le_max_r | apply Nat.le_max_l ] | unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge; left; apply (cond_pos (vn n)) ]. - rewrite StepFun_P39; rewrite Rabs_Ropp; apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P6 (pre (mkStepFun (StepFun_P28 (-1) (phi_sequence vn pr2 n) (phi_sequence un pr1 n))))))))). { apply StepFun_P34; try auto with real. } apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P6 (pre (mkStepFun (StepFun_P28 1 psi_vn psi_un)))))). { apply StepFun_P37. { auto with real. } intros; simpl; rewrite Rmult_1_l; apply Rle_trans with (Rabs (phi_sequence vn pr2 n x - f x) + Rabs (f x - phi_sequence un pr1 n x)). { replace (phi_sequence vn pr2 n x + -1 * phi_sequence un pr1 n x) with (phi_sequence vn pr2 n x - f x + (f x - phi_sequence un pr1 n x)); [ apply Rabs_triang | ring ]. } assert (H10 : Rmin a b = b). { unfold Rmin; decide (Rle_dec a b) with Hnle; reflexivity. } assert (H11 : Rmax a b = a). { unfold Rmax; decide (Rle_dec a b) with Hnle; reflexivity. } apply Rplus_le_compat. { rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; elim H5; intros; apply H8. rewrite H10; rewrite H11; elim H7; intros; split; left; assumption. } elim H6; intros; apply H8. rewrite H10; rewrite H11; elim H7; intros; split; left; assumption. } rewrite <- (Ropp_involutive (RiemannInt_SF (mkStepFun (StepFun_P6 (pre (mkStepFun (StepFun_P28 1 psi_vn psi_un))))))) ; 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 (vn n)). { elim H5; intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF psi_vn)). { rewrite <- Rabs_Ropp; apply RRle_abs. } assumption. } replace (pos (vn n)) with (Rabs (vn n - 0)); [ apply H0; unfold ge; apply Nat.le_trans with N; try assumption; unfold N; apply Nat.le_trans with (max N0 N1); [ apply Nat.le_max_r | 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 (vn n)) ]. } apply Rlt_trans with (pos (un n)). { elim H6; intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF psi_un)). { rewrite <- Rabs_Ropp; apply RRle_abs; assumption. } assumption. } replace (pos (un n)) with (Rabs (un n - 0)); [ apply H; unfold ge; apply Nat.le_trans with N; try assumption; unfold N; apply Nat.le_trans with (max N0 N1); apply Nat.le_max_l | 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