proposition: Lemma RiemannInt_P25 : forall (f:R -> R) (a b c:R) (pr1:Riemann_integrable f a b) (pr2:Riemann_integrable f b c) (pr3:Riemann_integrable f a c), a <= b -> b <= c -> RiemannInt pr1 + RiemannInt pr2 = RiemannInt pr3.
proof: Proof. intros f a b c pr1 pr2 pr3 Hyp1 Hyp2; unfold RiemannInt; case (RiemannInt_exists pr1 RinvN RinvN_cv) as (x1,HUn_cv1); case (RiemannInt_exists pr2 RinvN RinvN_cv) as (x0,HUn_cv0); case (RiemannInt_exists pr3 RinvN RinvN_cv) as (x,HUn_cv); symmetry ; eapply UL_sequence. { apply HUn_cv. } unfold Un_cv; intros; assert (H0 : 0 < eps / 3). { unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. } destruct (HUn_cv1 _ H0) as (N1,H1); clear HUn_cv1; destruct (HUn_cv0 _ H0) as (N2,H2); clear HUn_cv0; cut (Un_cv (fun n:nat => RiemannInt_SF (phi_sequence RinvN pr3 n) - (RiemannInt_SF (phi_sequence RinvN pr1 n) + RiemannInt_SF (phi_sequence RinvN pr2 n))) 0). { intro; elim (H3 _ H0); clear H3; intros N3 H3; set (N0 := max (max N1 N2) N3); exists N0; intros; unfold Rdist; apply Rle_lt_trans with (Rabs (RiemannInt_SF (phi_sequence RinvN pr3 n) - (RiemannInt_SF (phi_sequence RinvN pr1 n) + RiemannInt_SF (phi_sequence RinvN pr2 n))) + Rabs (RiemannInt_SF (phi_sequence RinvN pr1 n) + RiemannInt_SF (phi_sequence RinvN pr2 n) - (x1 + x0))). { replace (RiemannInt_SF (phi_sequence RinvN pr3 n) - (x1 + x0)) with (RiemannInt_SF (phi_sequence RinvN pr3 n) - (RiemannInt_SF (phi_sequence RinvN pr1 n) + RiemannInt_SF (phi_sequence RinvN pr2 n)) + (RiemannInt_SF (phi_sequence RinvN pr1 n) + RiemannInt_SF (phi_sequence RinvN pr2 n) - (x1 + x0))); [ apply Rabs_triang | ring ]. } replace eps with (eps / 3 + eps / 3 + eps / 3) by lra. rewrite Rplus_assoc; apply Rplus_lt_compat. { unfold Rdist in H3; cut (n >= N3)%nat. { intro; assert (H6 := H3 _ H5); unfold Rminus in H6; rewrite Ropp_0 in H6; rewrite Rplus_0_r in H6; apply H6. } unfold ge; apply Nat.le_trans with N0; [ unfold N0; apply Nat.le_max_r | assumption ]. } apply Rle_lt_trans with (Rabs (RiemannInt_SF (phi_sequence RinvN pr1 n) - x1) + Rabs (RiemannInt_SF (phi_sequence RinvN pr2 n) - x0)). { replace (RiemannInt_SF (phi_sequence RinvN pr1 n) + RiemannInt_SF (phi_sequence RinvN pr2 n) - (x1 + x0)) with (RiemannInt_SF (phi_sequence RinvN pr1 n) - x1 + (RiemannInt_SF (phi_sequence RinvN pr2 n) - x0)); [ apply Rabs_triang | ring ]. } apply Rplus_lt_compat. { unfold Rdist in H1; apply H1. unfold ge; apply Nat.le_trans with N0; [ apply Nat.le_trans with (max N1 N2); [ apply Nat.le_max_l | unfold N0; apply Nat.le_max_l ] | assumption ]. } unfold Rdist in H2; apply H2. unfold ge; apply Nat.le_trans with N0; [ apply Nat.le_trans with (max N1 N2); [ apply Nat.le_max_r | unfold N0; apply Nat.le_max_l ] | assumption ]. } clear x HUn_cv x0 x1 eps H H0 N1 H1 N2 H2; assert (H1 : exists psi1 : nat -> StepFun a b, (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi_sequence RinvN pr1 n t) <= psi1 n t) /\ Rabs (RiemannInt_SF (psi1 n)) < RinvN n)). { split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro; apply (proj2_sig (phi_sequence_prop RinvN pr1 n)). } assert (H2 : exists psi2 : nat -> StepFun b c, (forall n:nat, (forall t:R, Rmin b c <= t /\ t <= Rmax b c -> Rabs (f t - phi_sequence RinvN pr2 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < RinvN n)). { split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr2 n)); intro; apply (proj2_sig (phi_sequence_prop RinvN pr2 n)). } assert (H3 : exists psi3 : nat -> StepFun a c, (forall n:nat, (forall t:R, Rmin a c <= t /\ t <= Rmax a c -> Rabs (f t - phi_sequence RinvN pr3 n t) <= psi3 n t) /\ Rabs (RiemannInt_SF (psi3 n)) < RinvN n)). { split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr3 n)); intro; apply (proj2_sig (phi_sequence_prop RinvN pr3 n)). } elim H1; clear H1; intros psi1 H1; elim H2; clear H2; intros psi2 H2; elim H3; clear H3; intros psi3 H3; assert (H := RinvN_cv); unfold Un_cv; intros; assert (H4 : 0 < eps / 3). { unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. } elim (H _ H4); clear H; intros N0 H; assert (H5 : forall n:nat, (n >= N0)%nat -> RinvN n < eps / 3). { intros; replace (pos (RinvN n)) with (Rdist (mkposreal (/ (INR n + 1)) (RinvN_pos n)) 0). { apply H; assumption. } unfold Rdist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge; left; apply (cond_pos (RinvN n)). } exists N0; intros; elim (H1 n); elim (H2 n); elim (H3 n); clear H1 H2 H3; intros; unfold Rdist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; set (phi1 := phi_sequence RinvN pr1 n) in H8 |- *; set (phi2 := phi_sequence RinvN pr2 n) in H3 |- *; set (phi3 := phi_sequence RinvN pr3 n) in H1 |- *; assert (H10 : IsStepFun phi3 a b). { apply StepFun_P44 with c. { apply (pre phi3). } split; assumption. } assert (H11 : IsStepFun (psi3 n) a b). { apply StepFun_P44 with c. { apply (pre (psi3 n)). } split; assumption. } assert (H12 : IsStepFun phi3 b c). { apply StepFun_P45 with a. { apply (pre phi3). } split; assumption. } assert (H13 : IsStepFun (psi3 n) b c). { apply StepFun_P45 with a. { apply (pre (psi3 n)). } split; assumption. } replace (RiemannInt_SF phi3) with (RiemannInt_SF (mkStepFun H10) + RiemannInt_SF (mkStepFun H12)). { apply Rle_lt_trans with (Rabs (RiemannInt_SF (mkStepFun H10) - RiemannInt_SF phi1) + Rabs (RiemannInt_SF (mkStepFun H12) - RiemannInt_SF phi2)). { replace (RiemannInt_SF (mkStepFun H10) + RiemannInt_SF (mkStepFun H12) + - (RiemannInt_SF phi1 + RiemannInt_SF phi2)) with (RiemannInt_SF (mkStepFun H10) - RiemannInt_SF phi1 + (RiemannInt_SF (mkStepFun H12) - RiemannInt_SF phi2)) by ring; apply Rabs_triang. } replace (RiemannInt_SF (mkStepFun H10) - RiemannInt_SF phi1) with (RiemannInt_SF (mkStepFun (StepFun_P28 (-1) (mkStepFun H10) phi1))) by (rewrite StepFun_P30; ring). replace (RiemannInt_SF (mkStepFun H12) - RiemannInt_SF phi2) with (RiemannInt_SF (mkStepFun (StepFun_P28 (-1) (mkStepFun H12) phi2))) by (rewrite StepFun_P30; ring). apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 (-1) (mkStepFun H10) phi1)))) + RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 (-1) (mkStepFun H12) phi2))))). { apply Rle_trans with (Rabs (RiemannInt_SF (mkStepFun (StepFun_P28 (-1) (mkStepFun H10) phi1))) + RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 (-1) (mkStepFun H12) phi2))))). { apply Rplus_le_compat_l. apply StepFun_P34; try assumption. } do 2 rewrite <- (Rplus_comm (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 (-1) (mkStepFun H12) phi2)))))) ; apply Rplus_le_compat_l; apply StepFun_P34; try assumption. } apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P28 1 (mkStepFun H11) (psi1 n))) + RiemannInt_SF (mkStepFun (StepFun_P28 1 (mkStepFun H13) (psi2 n)))). { apply Rle_trans with (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 (-1) (mkStepFun H10) phi1)))) + RiemannInt_SF (mkStepFun (StepFun_P28 1 (mkStepFun H13) (psi2 n)))). { apply Rplus_le_compat_l; apply StepFun_P37; try assumption. intros; simpl; rewrite Rmult_1_l; apply Rle_trans with (Rabs (f x - phi3 x) + Rabs (f x - phi2 x)). { rewrite <- (Rabs_Ropp (f x - phi3 x)); rewrite Ropp_minus_distr; replace (phi3 x + -1 * phi2 x) with (phi3 x - f x + (f x - phi2 x)); [ apply Rabs_triang | ring ]. } apply Rplus_le_compat. { apply H1. elim H14; intros; split. { rewrite Rmin_left; eauto using Rle_trans. apply Rle_trans with b; try assumption. left; assumption. } rewrite Rmax_right; eauto using Rle_trans. left; assumption. } apply H3. elim H14; intros; split. { rewrite Rmin_left; eauto using Rle_trans. left; assumption. } rewrite Rmax_right; eauto using Rle_trans. left; assumption. } do 2 rewrite <- (Rplus_comm (RiemannInt_SF (mkStepFun (StepFun_P28 1 (mkStepFun H13) (psi2 n))))) ; apply Rplus_le_compat_l; apply StepFun_P37; try assumption. intros; simpl; rewrite Rmult_1_l; apply Rle_trans with (Rabs (f x - phi3 x) + Rabs (f x - phi1 x)). { rewrite <- (Rabs_Ropp (f x - phi3 x)); rewrite Ropp_minus_distr; replace (phi3 x + -1 * phi1 x) with (phi3 x - f x + (f x - phi1 x)); [ apply Rabs_triang | ring ]. } apply Rplus_le_compat. { apply H1. elim H14; intros; split. { rewrite Rmin_left; eauto using Rle_trans. left; assumption. } rewrite Rmax_right; eauto using Rle_trans. apply Rle_trans with b. { left; assumption. } assumption. } apply H8. elim H14; intros; split. { rewrite Rmin_left; trivial. left; assumption. } rewrite Rmax_right; trivial. left; assumption. } do 2 rewrite StepFun_P30. do 2 rewrite Rmult_1_l; replace (RiemannInt_SF (mkStepFun H11) + RiemannInt_SF (psi1 n) + (RiemannInt_SF (mkStepFun H13) + RiemannInt_SF (psi2 n))) with (RiemannInt_SF (psi3 n) + RiemannInt_SF (psi1 n) + RiemannInt_SF (psi2 n)). { replace eps with (eps / 3 + eps / 3 + eps / 3) by lra. repeat rewrite Rplus_assoc; apply Rplus_lt_compat. { apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi3 n))). { apply RRle_abs. } apply Rlt_trans with (pos (RinvN n)). { assumption. } apply H5; assumption. } apply Rplus_lt_compat. { apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi1 n))). { apply RRle_abs. } apply Rlt_trans with (pos (RinvN n)). { assumption. } apply H5; assumption. } apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi2 n))). { apply RRle_abs. } apply Rlt_trans with (pos (RinvN n)). { assumption. } apply H5; assumption. } replace (RiemannInt_SF (psi3 n)) with (RiemannInt_SF (mkStepFun (pre (psi3 n)))). { rewrite <- (StepFun_P43 H11 H13 (pre (psi3 n))); ring. } reflexivity. } apply (StepFun_P43 H10 H12 (pre phi3)). Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra