proposition: Lemma RiemannInt_P28 : forall (f:R -> R) (a b x:R) (h:a <= b) (C0:forall x:R, a <= x <= b -> continuity_pt f x), a <= x <= b -> derivable_pt_lim (primitive h (FTC_P1 h C0)) x (f x).
proof: Proof. intro f; intros; elim h; intro. 1:elim H; clear H; intros; elim H; intro. - elim H1; intro. { apply RiemannInt_P27; split; assumption. } set (f_b := fun x:R => f b * (x - b) + RiemannInt (FTC_P1 h C0 h (Rle_refl b))); rewrite H3. assert (H4 : derivable_pt_lim f_b b (f b)). { unfold f_b; pattern (f b) at 2; replace (f b) with (f b + 0) by ring. change (derivable_pt_lim ((fct_cte (f b) * (id - fct_cte b))%F + fct_cte (RiemannInt (FTC_P1 h C0 h (Rle_refl b)))) b ( f b + 0)). apply derivable_pt_lim_plus. { pattern (f b) at 2; replace (f b) with (0 * (id - fct_cte b)%F b + fct_cte (f b) b * 1) by (unfold fct_cte;ring). apply derivable_pt_lim_mult. { apply derivable_pt_lim_const. } replace 1 with (1 - 0); [ idtac | ring ]. apply derivable_pt_lim_minus. { apply derivable_pt_lim_id. } apply derivable_pt_lim_const. } apply derivable_pt_lim_const. } unfold derivable_pt_lim; intros; elim (H4 _ H5); intros; assert (H7 : continuity_pt f b). { apply C0; split; [ left; assumption | right; reflexivity ]. } assert (H8 : 0 < eps / 2). { unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. } elim (H7 _ H8); unfold D_x, no_cond, dist; simpl; unfold Rdist; intros; set (del := Rmin x0 (Rmin x1 (b - a))); assert (H10 : 0 < del). { unfold del; unfold Rmin; case (Rle_dec x1 (b - a)); intros. { destruct (Rle_dec x0 x1) as [Hle|Hnle]; [ apply (cond_pos x0) | elim H9; intros; assumption ]. } destruct (Rle_dec x0 (b - a)) as [Hle'|Hnle']; [ apply (cond_pos x0) | apply Rlt_0_minus; assumption ]. } split with (mkposreal _ H10); intros; destruct (Rcase_abs h0) as [Hle|Hnle]. + assert (H14 : b + h0 < b). { pattern b at 2; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; assumption. } assert (H13 : Riemann_integrable f (b + h0) b). { apply continuity_implies_RiemannInt. { left; assumption. } intros; apply C0; elim H13; intros; split; try assumption. apply Rle_trans with (b + h0); try assumption. apply Rplus_le_reg_l with (- a - h0). replace (- a - h0 + a) with (- h0); [ idtac | ring ]. replace (- a - h0 + (b + h0)) with (b - a); [ idtac | ring ]. apply Rle_trans with del. { apply Rle_trans with (Rabs h0). { rewrite <- Rabs_Ropp; apply RRle_abs. } left; assumption. } unfold del; apply Rle_trans with (Rmin x1 (b - a)); apply Rmin_r. } replace (primitive h (FTC_P1 h C0) (b + h0) - primitive h (FTC_P1 h C0) b) with (- RiemannInt H13). { replace (f b) with (- RiemannInt (RiemannInt_P14 (b + h0) b (f b)) / h0). 2:{ rewrite RiemannInt_P15. rewrite <- Ropp_mult_distr_l_reverse; apply Rmult_eq_reg_l with h0; [ repeat rewrite (Rmult_comm h0); unfold Rdiv; repeat rewrite Rmult_assoc; rewrite Rinv_l; [ ring | assumption ] | assumption ]. } rewrite <- Rabs_Ropp; unfold Rminus; unfold Rdiv; rewrite Ropp_mult_distr_l_reverse; rewrite Ropp_plus_distr; repeat rewrite Ropp_involutive; replace (RiemannInt H13 * / h0 + - RiemannInt (RiemannInt_P14 (b + h0) b (f b)) * / h0) with ((RiemannInt H13 - RiemannInt (RiemannInt_P14 (b + h0) b (f b))) / h0). 2:{ unfold Rdiv, Rminus; rewrite Rmult_plus_distr_r; ring. } replace (RiemannInt H13 - RiemannInt (RiemannInt_P14 (b + h0) b (f b))) with (RiemannInt (RiemannInt_P10 (-1) H13 (RiemannInt_P14 (b + h0) b (f b)))). 2:{ rewrite (RiemannInt_P13 H13 (RiemannInt_P14 (b + h0) b (f b)) (RiemannInt_P10 (-1) H13 (RiemannInt_P14 (b + h0) b (f b)))) ; ring. } unfold Rdiv; rewrite Rabs_mult; apply Rle_lt_trans with (RiemannInt (RiemannInt_P16 (RiemannInt_P10 (-1) H13 (RiemannInt_P14 (b + h0) b (f b)))) * Rabs (/ h0)). { do 2 rewrite <- (Rmult_comm (Rabs (/ h0))); apply Rmult_le_compat_l. { apply Rabs_pos. } apply (RiemannInt_P17 (RiemannInt_P10 (-1) H13 (RiemannInt_P14 (b + h0) b (f b))) (RiemannInt_P16 (RiemannInt_P10 (-1) H13 (RiemannInt_P14 (b + h0) b (f b))))); left; assumption. } apply Rle_lt_trans with (RiemannInt (RiemannInt_P14 (b + h0) b (eps / 2)) * Rabs (/ h0)). { do 2 rewrite <- (Rmult_comm (Rabs (/ h0))); apply Rmult_le_compat_l. { apply Rabs_pos. } apply RiemannInt_P19. { left; assumption. } intros; replace (f x2 + -1 * fct_cte (f b) x2) with (f x2 - f b) by (unfold fct_cte; ring). unfold fct_cte; case (Req_dec b x2); intro. { rewrite H16; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; left; assumption. } elim H9; intros; left; apply H18. repeat split. { assumption. } rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; rewrite Rabs_right. 2:{ apply Rle_ge; left; apply Rlt_0_minus; elim H15; intros; assumption. } apply Rplus_lt_reg_l with (x2 - x1); replace (x2 - x1 + (b - x2)) with (b - x1); [ idtac | ring ]. replace (x2 - x1 + x1) with x2; [ idtac | ring ]. apply Rlt_le_trans with (b + h0). 2: elim H15; intros; left; assumption. unfold Rminus; apply Rplus_lt_compat_l; apply Ropp_lt_cancel; rewrite Ropp_involutive; apply Rle_lt_trans with (Rabs h0). { rewrite <- Rabs_Ropp; apply RRle_abs. } apply Rlt_le_trans with del; [ assumption | unfold del; apply Rle_trans with (Rmin x1 (b - a)); [ apply Rmin_r | apply Rmin_l ] ]. } rewrite RiemannInt_P15. rewrite Rmult_assoc; replace ((b - (b + h0)) * Rabs (/ h0)) with 1. { lra. } rewrite Rabs_left. { apply Rmult_eq_reg_l with h0; [ do 2 rewrite (Rmult_comm h0); rewrite Rmult_assoc; rewrite Ropp_mult_distr_l_reverse; rewrite Rinv_l; [ ring | assumption ] | assumption ]. } apply Rinv_lt_0_compat; assumption. } cut (a <= b + h0). { cut (b + h0 <= b). 2:{ left; assumption. } intros; unfold primitive; destruct (Rle_dec a (b + h0)) as [Hle'|Hnle']; destruct (Rle_dec (b + h0) b) as [Hle''|[]]; destruct (Rle_dec a b) as [Hleab|[]]; destruct (Rle_dec b b) as [Hlebb|[]]; assumption || (right; reflexivity) || (try (left; assumption)). { rewrite <- (RiemannInt_P26 (FTC_P1 h C0 Hle' Hle'') H13 (FTC_P1 h C0 Hleab Hlebb)); ring. } elim Hnle'; assumption. } apply Rplus_le_reg_l with (- a - h0). replace (- a - h0 + a) with (- h0); [ idtac | ring ]. replace (- a - h0 + (b + h0)) with (b - a); [ idtac | ring ]. apply Rle_trans with del. { apply Rle_trans with (Rabs h0). { rewrite <- Rabs_Ropp; apply RRle_abs. } left; assumption. } unfold del; apply Rle_trans with (Rmin x1 (b - a)); apply Rmin_r. + cut (primitive h (FTC_P1 h C0) b = f_b b). { intro; cut (primitive h (FTC_P1 h C0) (b + h0) = f_b (b + h0)). { intro; rewrite H13; rewrite H14; apply H6. { assumption. } apply Rlt_le_trans with del; [ assumption | unfold del; apply Rmin_l ]. } assert (H14 : b < b + h0). { pattern b at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l. assert (H14 := Rge_le _ _ Hnle); elim H14; intro. { assumption. } elim H11; symmetry ; assumption. } unfold primitive; destruct (Rle_dec a (b + h0)) as [Hle|[]]; destruct (Rle_dec (b + h0) b) as [Hle'|Hnle']; [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H14)) | unfold f_b; reflexivity | left; apply Rlt_trans with b; assumption | left; apply Rlt_trans with b; assumption ]. } unfold f_b; unfold Rminus; rewrite Rplus_opp_r; rewrite Rmult_0_r; rewrite Rplus_0_l; unfold primitive; destruct (Rle_dec a b) as [Hle'|Hnle']; destruct (Rle_dec b b) as [Hle''|[]]; [ apply RiemannInt_P5 | right; reflexivity | elim Hnle'; left; assumption | right; reflexivity ]. - set (f_a := fun x:R => f a * (x - a)); rewrite <- H2; assert (H3 : derivable_pt_lim f_a a (f a)). { unfold f_a; change (derivable_pt_lim (fct_cte (f a) * (id - fct_cte a)%F) a (f a)) ; pattern (f a) at 2; replace (f a) with (0 * (id - fct_cte a)%F a + fct_cte (f a) a * 1). { apply derivable_pt_lim_mult. { apply derivable_pt_lim_const. } replace 1 with (1 - 0); [ idtac | ring ]. apply derivable_pt_lim_minus. { apply derivable_pt_lim_id. } apply derivable_pt_lim_const. } unfold fct_cte; ring. } unfold derivable_pt_lim; intros; elim (H3 _ H4); intros. assert (H6 : continuity_pt f a). { apply C0; split; [ right; reflexivity | left; assumption ]. } assert (H7 : 0 < eps / 2). { unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. } elim (H6 _ H7); unfold D_x, no_cond, dist; simpl; unfold Rdist; intros. set (del := Rmin x0 (Rmin x1 (b - a))). assert (H9 : 0 < del). { unfold del; unfold Rmin. case (Rle_dec x1 (b - a)); intros. { case (Rle_dec x0 x1); intro. { apply (cond_pos x0). } elim H8; intros; assumption. } case (Rle_dec x0 (b - a)); intro. { apply (cond_pos x0). } apply Rlt_0_minus; assumption. } split with (mkposreal _ H9). intros; destruct (Rcase_abs h0) as [Hle|Hnle]. + assert (H12 : a + h0 < a). { pattern a at 2; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; assumption. } unfold primitive. destruct (Rle_dec a (a + h0)) as [Hle'|Hnle']; destruct (Rle_dec (a + h0) b) as [Hle''|Hnle'']; destruct (Rle_dec a a) as [Hleaa|[]]; destruct (Rle_dec a b) as [Hleab|[]]; try (left; assumption) || (right; reflexivity). * elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H12)). * elim Hnle''; left; apply Rlt_trans with a; assumption. * rewrite RiemannInt_P9; replace 0 with (f_a a). { replace (f a * (a + h0 - a)) with (f_a (a + h0)). { apply H5; try assumption. apply Rlt_le_trans with del; [ assumption | unfold del; apply Rmin_l ]. } unfold f_a; ring. } unfold f_a; ring. * elim Hnle''; left; apply Rlt_trans with a; assumption. + assert (H12 : a < a + h0). { pattern a at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l. assert (H12 := Rge_le _ _ Hnle); elim H12; intro. { assumption. } elim H10; symmetry ; assumption. } assert (H13 : Riemann_integrable f a (a + h0)). { apply continuity_implies_RiemannInt. { left; assumption. } intros; apply C0; elim H13; intros; split; try assumption. apply Rle_trans with (a + h0); try assumption. apply Rplus_le_reg_l with (- b - h0). replace (- b - h0 + b) with (- h0); [ idtac | ring ]. replace (- b - h0 + (a + h0)) with (a - b); [ idtac | ring ]. apply Ropp_le_cancel; rewrite Ropp_involutive; rewrite Ropp_minus_distr; apply Rle_trans with del. { apply Rle_trans with (Rabs h0); [ apply RRle_abs | left; assumption ]. } unfold del; apply Rle_trans with (Rmin x1 (b - a)); apply Rmin_r. } replace (primitive h (FTC_P1 h C0) (a + h0) - primitive h (FTC_P1 h C0) a) with (RiemannInt H13). { replace (f a) with (RiemannInt (RiemannInt_P14 a (a + h0) (f a)) / h0). 2:{ rewrite RiemannInt_P15. rewrite Rplus_comm; unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; unfold Rdiv; rewrite Rmult_assoc; rewrite Rinv_r; [ ring | assumption ]. } replace (RiemannInt H13 / h0 - RiemannInt (RiemannInt_P14 a (a + h0) (f a)) / h0) with ((RiemannInt H13 - RiemannInt (RiemannInt_P14 a (a + h0) (f a))) / h0). 2:{ unfold Rdiv, Rminus; rewrite Rmult_plus_distr_r; ring. } replace (RiemannInt H13 - RiemannInt (RiemannInt_P14 a (a + h0) (f a))) with (RiemannInt (RiemannInt_P10 (-1) H13 (RiemannInt_P14 a (a + h0) (f a)))). 2:{ rewrite (RiemannInt_P13 H13 (RiemannInt_P14 a (a + h0) (f a)) (RiemannInt_P10 (-1) H13 (RiemannInt_P14 a (a + h0) (f a)))) ; ring. } unfold Rdiv; rewrite Rabs_mult; apply Rle_lt_trans with (RiemannInt (RiemannInt_P16 (RiemannInt_P10 (-1) H13 (RiemannInt_P14 a (a + h0) (f a)))) * Rabs (/ h0)). { do 2 rewrite <- (Rmult_comm (Rabs (/ h0))); apply Rmult_le_compat_l. { apply Rabs_pos. } apply (RiemannInt_P17 (RiemannInt_P10 (-1) H13 (RiemannInt_P14 a (a + h0) (f a))) (RiemannInt_P16 (RiemannInt_P10 (-1) H13 (RiemannInt_P14 a (a + h0) (f a))))); left; assumption. } apply Rle_lt_trans with (RiemannInt (RiemannInt_P14 a (a + h0) (eps / 2)) * Rabs (/ h0)). { do 2 rewrite <- (Rmult_comm (Rabs (/ h0))); apply Rmult_le_compat_l. { apply Rabs_pos. } apply RiemannInt_P19. { left; assumption. } intros; replace (f x2 + -1 * fct_cte (f a) x2) with (f x2 - f a). 2:{ unfold fct_cte; ring. } unfold fct_cte; case (Req_dec a x2); intro. { rewrite H15; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; left; assumption. } elim H8; intros; left; apply H17; repeat split. { assumption. } rewrite Rabs_right. { apply Rplus_lt_reg_l with a; replace (a + (x2 - a)) with x2; [ idtac | ring ]. apply Rlt_le_trans with (a + h0). { elim H14; intros; assumption. } apply Rplus_le_compat_l; left; apply Rle_lt_trans with (Rabs h0). { apply RRle_abs. } apply Rlt_le_trans with del; [ assumption | unfold del; apply Rle_trans with (Rmin x1 (b - a)); [ apply Rmin_r | apply Rmin_l ] ]. } apply Rle_ge; left; apply Rlt_0_minus; elim H14; intros; assumption. } rewrite RiemannInt_P15. rewrite Rmult_assoc; replace ((a + h0 - a) * Rabs (/ h0)) with 1. { lra. } rewrite Rabs_right. { rewrite Rplus_comm; unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; rewrite Rinv_r; [ reflexivity | assumption ]. } apply Rle_ge; left; apply Rinv_0_lt_compat; assert (H14 := Rge_le _ _ Hnle); elim H14; intro. { assumption. } elim H10; symmetry ; assumption. } cut (a <= a + h0). 2:left;assumption. cut (a + h0 <= b). { intros; unfold primitive. decide (Rle_dec (a+h0) b) with H14. decide (Rle_dec a a) with (Rle_refl a). decide (Rle_dec a (a+h0)) with H15. decide (Rle_dec a b) with h. rewrite RiemannInt_P9; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply RiemannInt_P5. } apply Rplus_le_reg_l with (- a); replace (- a + (a + h0)) with h0; [ idtac | ring ]. rewrite Rplus_comm; apply Rle_trans with del; [ apply Rle_trans with (Rabs h0); [ apply RRle_abs | left; assumption ] | unfold del; apply Rle_trans with (Rmin x1 (b - a)); apply Rmin_r ]. - assert (H1 : x = a). { rewrite <- H0 in H; elim H; intros; apply Rle_antisym; assumption. } set (f_a := fun x:R => f a * (x - a)). assert (H2 : derivable_pt_lim f_a a (f a)). { unfold f_a; change (derivable_pt_lim (fct_cte (f a) * (id - fct_cte a)%F) a (f a)) ; pattern (f a) at 2; replace (f a) with (0 * (id - fct_cte a)%F a + fct_cte (f a) a * 1). { apply derivable_pt_lim_mult. { apply derivable_pt_lim_const. } replace 1 with (1 - 0); [ idtac | ring ]. apply derivable_pt_lim_minus. { apply derivable_pt_lim_id. } apply derivable_pt_lim_const. } unfold fct_cte; ring. } set (f_b := fun x:R => f b * (x - b) + RiemannInt (FTC_P1 h C0 h (Rle_refl b))). assert (H3 : derivable_pt_lim f_b b (f b)). { unfold f_b; pattern (f b) at 2; replace (f b) with (f b + 0). { change (derivable_pt_lim ((fct_cte (f b) * (id - fct_cte b))%F + fct_cte (RiemannInt (FTC_P1 h C0 h (Rle_refl b)))) b ( f b + 0)). apply derivable_pt_lim_plus. { pattern (f b) at 2; replace (f b) with (0 * (id - fct_cte b)%F b + fct_cte (f b) b * 1). { apply derivable_pt_lim_mult. { apply derivable_pt_lim_const. } replace 1 with (1 - 0); [ idtac | ring ]. apply derivable_pt_lim_minus. { apply derivable_pt_lim_id. } apply derivable_pt_lim_const. } unfold fct_cte; ring. } apply derivable_pt_lim_const. } ring. } unfold derivable_pt_lim; intros; elim (H2 _ H4); intros; elim (H3 _ H4); intros; set (del := Rmin x0 x1). assert (H7 : 0 < del). { unfold del; unfold Rmin; destruct (Rle_dec x0 x1) as [Hle|Hnle]. { apply (cond_pos x0). } apply (cond_pos x1). } split with (mkposreal _ H7); intros; destruct (Rcase_abs h0) as [Hle|Hnle]. { assert (H10 : a + h0 < a). { pattern a at 2; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; assumption. } rewrite H1; unfold primitive. apply (decide_left (Rle_dec a b) h); intro h'. assert (H11:~ a<=a+h0) by auto using Rlt_not_le. decide (Rle_dec a (a+h0)) with H11. decide (Rle_dec a a) with (Rle_refl a). rewrite RiemannInt_P9; replace 0 with (f_a a). { replace (f a * (a + h0 - a)) with (f_a (a + h0)). { apply H5; try assumption. apply Rlt_le_trans with del; try assumption. unfold del; apply Rmin_l. } unfold f_a; ring. } unfold f_a; ring. } assert (H10 : a < a + h0). { pattern a at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l. assert (H10 := Rge_le _ _ Hnle); elim H10; intro. { assumption. } elim H8; symmetry ; assumption. } rewrite H0 in H1; rewrite H1; unfold primitive. decide (Rle_dec a b) with h. decide (Rle_dec b b) with (Rle_refl b). assert (H12 : a<=b+h0) by (eauto using Rlt_le_trans with real). decide (Rle_dec a (b+h0)) with H12. rewrite H0 in H10. assert (H13 : ~b+h0<=b) by (auto using Rlt_not_le). decide (Rle_dec (b+h0) b) with H13. replace (RiemannInt (FTC_P1 h C0 hbis H11)) with (f_b b). { fold (f_b (b + h0)). apply H6; try assumption. apply Rlt_le_trans with del; try assumption. unfold del; apply Rmin_r. } unfold f_b; unfold Rminus; rewrite Rplus_opp_r; rewrite Rmult_0_r; rewrite Rplus_0_l; apply RiemannInt_P5. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra