proposition: Lemma RiemannInt_P21 : forall (f:R -> R) (a b c:R), a <= b -> b <= c -> Riemann_integrable f a b -> Riemann_integrable f b c -> Riemann_integrable f a c.
proof: Proof. unfold Riemann_integrable; intros f a b c Hyp1 Hyp2 X X0 eps. assert (H : 0 < eps / 2). { unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos eps) | apply Rinv_0_lt_compat; prove_sup0 ]. } elim (X (mkposreal _ H)); clear X; intros phi1 [psi1 H1]; elim (X0 (mkposreal _ H)); clear X0; intros phi2 [psi2 H2]. set (phi3 := fun x:R => match Rle_dec a x with | left _ => match Rle_dec x b with | left _ => phi1 x | right _ => phi2 x end | right _ => 0 end). set (psi3 := fun x:R => match Rle_dec a x with | left _ => match Rle_dec x b with | left _ => psi1 x | right _ => psi2 x end | right _ => 0 end). cut (IsStepFun phi3 a c). 1:intro; cut (IsStepFun psi3 a b). 1:intro; cut (IsStepFun psi3 b c). 1:intro; assert (IsStepFun psi3 a c) by (apply StepFun_P46 with b; assumption). - split with (mkStepFun X); split with (mkStepFun X2); simpl; split. + intros; unfold phi3, psi3; case (Rle_dec t b) as [|Hnle]; case (Rle_dec a t) as [|Hnle']. * elim H1; intros; apply H3. replace (Rmin a b) with a. { replace (Rmax a b) with b. { split; assumption. } unfold Rmax; decide (Rle_dec a b) with Hyp1; reflexivity. } unfold Rmin; decide (Rle_dec a b) with Hyp1; reflexivity. * elim Hnle'; replace a with (Rmin a c). { elim H0; intros; assumption. } unfold Rmin; case (Rle_dec a c) as [|[]]; [ reflexivity | apply Rle_trans with b; assumption ]. * elim H2; intros; apply H3. replace (Rmax b c) with (Rmax a c). { elim H0; intros; split; try assumption. replace (Rmin b c) with b. { auto with real. } unfold Rmin; decide (Rle_dec b c) with Hyp2; reflexivity. } unfold Rmax; decide (Rle_dec b c) with Hyp2; case (Rle_dec a c) as [|[]]; [ reflexivity | apply Rle_trans with b; assumption ]. * elim Hnle'; replace a with (Rmin a c). { elim H0; intros; assumption. } unfold Rmin; case (Rle_dec a c) as [|[]]; [ reflexivity | apply Rle_trans with b; assumption ]. + rewrite <- (StepFun_P43 X0 X1 X2). apply Rle_lt_trans with (Rabs (RiemannInt_SF (mkStepFun X0)) + Rabs (RiemannInt_SF (mkStepFun X1))). { apply Rabs_triang. } rewrite <-(Rplus_half_diag eps); replace (RiemannInt_SF (mkStepFun X0)) with (RiemannInt_SF psi1). { replace (RiemannInt_SF (mkStepFun X1)) with (RiemannInt_SF psi2). { apply Rplus_lt_compat. { elim H1; intros; assumption. } elim H2; intros; assumption. } apply Rle_antisym. { apply StepFun_P37; try assumption. simpl; intros; unfold psi3; elim H0; clear H0; intros; destruct (Rle_dec a x) as [Hle|Hnle]; destruct (Rle_dec x b) as [Hle'|Hnle']; [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H0)) | right; reflexivity | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] ]. } apply StepFun_P37; try assumption. simpl; intros; unfold psi3; elim H0; clear H0; intros; destruct (Rle_dec a x) as [Hle|Hnle]; destruct (Rle_dec x b) as [Hle'|Hnle']; [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H0)) | right; reflexivity | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] ]. } apply Rle_antisym. { apply StepFun_P37; try assumption. simpl; intros; unfold psi3; elim H0; clear H0; intros; destruct (Rle_dec a x) as [Hle|Hnle]; destruct (Rle_dec x b) as [Hle'|Hnle']; [ right; reflexivity | elim Hnle'; left; assumption | elim Hnle; left; assumption | elim Hnle; left; assumption ]. } apply StepFun_P37; try assumption. simpl; intros; unfold psi3; elim H0; clear H0; intros; destruct (Rle_dec a x) as [Hle|Hnle]; destruct (Rle_dec x b) as [Hle'|Hnle']; [ right; reflexivity | elim Hnle'; left; assumption | elim Hnle; left; assumption | elim Hnle; left; assumption ]. - assert (H3 := pre psi2); unfold IsStepFun in H3; unfold is_subdivision in H3; elim H3; clear H3; intros l1 [lf1 H3]; split with l1; split with lf1; unfold adapted_couple in H3; decompose [and] H3; clear H3; unfold adapted_couple; repeat split; try assumption. intros; assert (H9 := H8 i H3); unfold constant_D_eq, open_interval; unfold constant_D_eq, open_interval in H9; intros; rewrite <- (H9 x H7); unfold psi3; assert (H10 : b < x). { apply Rle_lt_trans with (pos_Rl l1 i). { replace b with (Rmin b c). { rewrite <- H5; elim (RList_P6 l1); intros; apply H10; try assumption. { apply Nat.le_0_l. } apply Nat.lt_trans with (pred (length l1)); try assumption; apply Nat.lt_pred_l; red; intro; rewrite H12 in H6; discriminate. } unfold Rmin; decide (Rle_dec b c) with Hyp2; reflexivity. } elim H7; intros; assumption. } destruct (Rle_dec a x) as [Hle|Hnle]; destruct (Rle_dec x b) as [Hle'|Hnle']; [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H10)) | reflexivity | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] ]. - assert (H3 := pre psi1); unfold IsStepFun in H3; unfold is_subdivision in H3; elim H3; clear H3; intros l1 [lf1 H3]; split with l1; split with lf1; unfold adapted_couple in H3; decompose [and] H3; clear H3; unfold adapted_couple; repeat split; try assumption. intros; assert (H9 := H8 i H3); unfold constant_D_eq, open_interval; unfold constant_D_eq, open_interval in H9; intros; rewrite <- (H9 x H7); unfold psi3; assert (H10 : x <= b). { apply Rle_trans with (pos_Rl l1 (S i)). { elim H7; intros; left; assumption. } replace b with (Rmax a b). { rewrite <- H4; elim (RList_P6 l1); intros; apply H10; try assumption. apply Nat.lt_pred_l; red; intro; rewrite H12 in H6; discriminate. } unfold Rmax; decide (Rle_dec a b) with Hyp1; reflexivity. } assert (H11 : a <= x). { apply Rle_trans with (pos_Rl l1 i). { replace a with (Rmin a b). { rewrite <- H5; elim (RList_P6 l1); intros; apply H11; try assumption. { apply Nat.le_0_l. } apply Nat.lt_trans with (pred (length l1)); try assumption; apply Nat.lt_pred_l; red; intro; rewrite H13 in H6; discriminate. } unfold Rmin; decide (Rle_dec a b) with Hyp1; reflexivity. } left; elim H7; intros; assumption. } decide (Rle_dec a x) with H11; decide (Rle_dec x b) with H10; reflexivity. - apply StepFun_P46 with b. { assert (H3 := pre phi1); unfold IsStepFun in H3; unfold is_subdivision in H3; elim H3; clear H3; intros l1 [lf1 H3]; split with l1; split with lf1; unfold adapted_couple in H3; decompose [and] H3; clear H3; unfold adapted_couple; repeat split; try assumption. intros; assert (H9 := H8 i H3); unfold constant_D_eq, open_interval; unfold constant_D_eq, open_interval in H9; intros; rewrite <- (H9 x H7); unfold psi3; assert (H10 : x <= b). { apply Rle_trans with (pos_Rl l1 (S i)). { elim H7; intros; left; assumption. } replace b with (Rmax a b). { rewrite <- H4; elim (RList_P6 l1); intros; apply H10; try assumption. apply Nat.lt_pred_l; red; intro; rewrite H12 in H6; discriminate. } unfold Rmax; decide (Rle_dec a b) with Hyp1; reflexivity. } assert (H11 : a <= x). { apply Rle_trans with (pos_Rl l1 i). { replace a with (Rmin a b). { rewrite <- H5; elim (RList_P6 l1); intros; apply H11; try assumption. { apply Nat.le_0_l. } apply Nat.lt_trans with (pred (length l1)); try assumption; apply Nat.lt_pred_l; red; intro; rewrite H13 in H6; discriminate. } unfold Rmin; decide (Rle_dec a b) with Hyp1; reflexivity. } left; elim H7; intros; assumption. } unfold phi3; decide (Rle_dec a x) with H11; decide (Rle_dec x b) with H10; reflexivity || elim n; assumption. } assert (H3 := pre phi2); unfold IsStepFun in H3; unfold is_subdivision in H3; elim H3; clear H3; intros l1 [lf1 H3]; split with l1; split with lf1; unfold adapted_couple in H3; decompose [and] H3; clear H3; unfold adapted_couple; repeat split; try assumption. intros; assert (H9 := H8 i H3); unfold constant_D_eq, open_interval; unfold constant_D_eq, open_interval in H9; intros; rewrite <- (H9 x H7); unfold psi3; assert (H10 : b < x). { apply Rle_lt_trans with (pos_Rl l1 i). { replace b with (Rmin b c). { rewrite <- H5; elim (RList_P6 l1); intros; apply H10; try assumption. { apply Nat.le_0_l. } apply Nat.lt_trans with (pred (length l1)); try assumption; apply Nat.lt_pred_l; red; intro; rewrite H12 in H6; discriminate. } unfold Rmin; decide (Rle_dec b c) with Hyp2; reflexivity. } elim H7; intros; assumption. } unfold phi3; destruct (Rle_dec a x) as [Hle|Hnle]; destruct (Rle_dec x b) as [Hle'|Hnle']; intros; [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H10)) | reflexivity | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra