proposition: Lemma RiemannInt_P27 : 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; clear H; intros; assert (H1 : continuity_pt f x). { apply C0; split; left; assumption. } unfold derivable_pt_lim; intros; assert (Hyp : 0 < eps / 2). { unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. } elim (H1 _ Hyp); unfold dist, D_x, no_cond; simpl; unfold Rdist; intros; set (del := Rmin x0 (Rmin (b - x) (x - a))); assert (H4 : 0 < del). { unfold del; unfold Rmin; case (Rle_dec (b - x) (x - a)); intro. { destruct (Rle_dec x0 (b - x)) as [Hle|Hnle]; [ elim H3; intros; assumption | apply Rlt_0_minus; assumption ]. } destruct (Rle_dec x0 (x - a)) as [Hle'|Hnle']; [ elim H3; intros; assumption | apply Rlt_0_minus; assumption ]. } split with (mkposreal _ H4); intros; assert (H7 : Riemann_integrable f x (x + h0)). { destruct (Rle_dec x (x + h0)) as [Hle''|Hnle'']. { apply continuity_implies_RiemannInt; try assumption. intros; apply C0; elim H7; intros; split. { apply Rle_trans with x; [ left; assumption | assumption ]. } apply Rle_trans with (x + h0). { assumption. } left; apply Rlt_le_trans with (x + del). { apply Rplus_lt_compat_l; apply Rle_lt_trans with (Rabs h0); [ apply RRle_abs | apply H6 ]. } unfold del; apply Rle_trans with (x + Rmin (b - x) (x - a)). { apply Rplus_le_compat_l; apply Rmin_r. } pattern b at 2; replace b with (x + (b - x)); [ apply Rplus_le_compat_l; apply Rmin_l | ring ]. } apply RiemannInt_P1; apply continuity_implies_RiemannInt; auto with real. intros; apply C0; elim H7; intros; split. { apply Rle_trans with (x + h0). { left; apply Rle_lt_trans with (x - del). { unfold del; apply Rle_trans with (x - Rmin (b - x) (x - a)). { pattern a at 1; replace a with (x + (a - x)); [ idtac | ring ]. unfold Rminus; apply Rplus_le_compat_l; apply Ropp_le_cancel. rewrite Ropp_involutive; rewrite Ropp_plus_distr; rewrite Ropp_involutive; rewrite (Rplus_comm x); apply Rmin_r. } unfold Rminus; apply Rplus_le_compat_l; apply Ropp_le_cancel. do 2 rewrite Ropp_involutive; apply Rmin_r. } 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 H6 ]. } assumption. } apply Rle_trans with x; [ assumption | left; assumption ]. } replace (primitive h (FTC_P1 h C0) (x + h0) - primitive h (FTC_P1 h C0) x) with (RiemannInt H7). 2:{ cut (a <= x + h0). { cut (x + h0 <= b). { intros; unfold primitive. assert (H10: a <= x) by (left; assumption). assert (H11: x <= b) by (left; assumption). decide (Rle_dec a (x + h0)) with H9; decide (Rle_dec (x + h0) b) with H8; decide (Rle_dec a x) with H10; decide (Rle_dec x b) with H11. rewrite <- (RiemannInt_P26 (FTC_P1 h C0 H10 H11) H7 (FTC_P1 h C0 H9 H8)); ring. } apply Rplus_le_reg_l with (- x); replace (- x + (x + h0)) with h0; [ idtac | ring ]. rewrite Rplus_comm; apply Rle_trans with (Rabs h0). { apply RRle_abs. } apply Rle_trans with del; [ left; assumption | unfold del; apply Rle_trans with (Rmin (b - x) (x - a)); [ apply Rmin_r | apply Rmin_l ] ]. } apply Ropp_le_cancel; apply Rplus_le_reg_l with x; replace (x + - (x + h0)) with (- h0) by ring. apply Rle_trans with (Rabs h0). { rewrite <- Rabs_Ropp; apply RRle_abs. } apply Rle_trans with del. { left; assumption. } unfold del; apply Rle_trans with (Rmin (b - x) (x - a)); apply Rmin_r. } replace (f x) with (RiemannInt (RiemannInt_P14 x (x + h0) (f x)) / h0). 2:{ rewrite RiemannInt_P15; apply Rmult_eq_reg_l with h0; [ unfold Rdiv; rewrite (Rmult_comm h0); repeat rewrite Rmult_assoc; rewrite Rinv_l; [ ring | assumption ] | assumption ]. } replace (RiemannInt H7 / h0 - RiemannInt (RiemannInt_P14 x (x + h0) (f x)) / h0) with ((RiemannInt H7 - RiemannInt (RiemannInt_P14 x (x + h0) (f x))) / h0). 2:{ unfold Rdiv, Rminus; rewrite Rmult_plus_distr_r; ring. } replace (RiemannInt H7 - RiemannInt (RiemannInt_P14 x (x + h0) (f x))) with (RiemannInt (RiemannInt_P10 (-1) H7 (RiemannInt_P14 x (x + h0) (f x)))). 2:{ rewrite (RiemannInt_P13 H7 (RiemannInt_P14 x (x + h0) (f x)) (RiemannInt_P10 (-1) H7 (RiemannInt_P14 x (x + h0) (f x)))). ring. } unfold Rdiv; rewrite Rabs_mult; destruct (Rle_dec x (x + h0)) as [Hle|Hnle]. - apply Rle_lt_trans with (RiemannInt (RiemannInt_P16 (RiemannInt_P10 (-1) H7 (RiemannInt_P14 x (x + h0) (f x)))) * Rabs (/ h0)). { do 2 rewrite <- (Rmult_comm (Rabs (/ h0))); apply Rmult_le_compat_l. { apply Rabs_pos. } apply (RiemannInt_P17 (RiemannInt_P10 (-1) H7 (RiemannInt_P14 x (x + h0) (f x))) (RiemannInt_P16 (RiemannInt_P10 (-1) H7 (RiemannInt_P14 x (x + h0) (f x))))); assumption. } apply Rle_lt_trans with (RiemannInt (RiemannInt_P14 x (x + h0) (eps / 2)) * Rabs (/ h0)). { do 2 rewrite <- (Rmult_comm (Rabs (/ h0))); apply Rmult_le_compat_l. { apply Rabs_pos. } apply RiemannInt_P19; try assumption. intros; replace (f x1 + -1 * fct_cte (f x) x1) with (f x1 - f x). { unfold fct_cte; destruct (Req_dec x x1) as [H9|H9]. { rewrite H9; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; left; assumption. } elim H3; intros; left; apply H11. repeat split. { assumption. } rewrite Rabs_right. { apply Rplus_lt_reg_l with x; replace (x + (x1 - x)) with x1; [ idtac | ring ]. apply Rlt_le_trans with (x + h0). { elim H8; intros; assumption. } apply Rplus_le_compat_l; apply Rle_trans with del. { left; apply Rle_lt_trans with (Rabs h0); [ apply RRle_abs | assumption ]. } unfold del; apply Rmin_l. } apply Rge_minus; apply Rle_ge; left; elim H8; intros; assumption. } unfold fct_cte; ring. } rewrite RiemannInt_P15. rewrite Rmult_assoc; replace ((x + h0 - x) * Rabs (/ h0)) with 1. { rewrite Rmult_1_r; unfold Rdiv; apply Rmult_lt_reg_l with 2; [ prove_sup0 | rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r; [ rewrite Rmult_1_l; pattern eps at 1; rewrite <- Rplus_0_r; rewrite <-Rplus_diag; apply Rplus_lt_compat_l; assumption | discrR ] ]. } rewrite Rabs_right. { replace (x + h0 - x) with h0; [ idtac | ring ]. symmetry; apply Rinv_r. assumption. } apply Rle_ge; left; apply Rinv_0_lt_compat. elim Hle; intro. { apply Rplus_lt_reg_l with x; rewrite Rplus_0_r; assumption. } elim H5; symmetry ; apply Rplus_eq_reg_l with x; rewrite Rplus_0_r; assumption. - apply Rle_lt_trans with (RiemannInt (RiemannInt_P16 (RiemannInt_P1 (RiemannInt_P10 (-1) H7 (RiemannInt_P14 x (x + h0) (f x))))) * Rabs (/ h0)). { do 2 rewrite <- (Rmult_comm (Rabs (/ h0))); apply Rmult_le_compat_l. { apply Rabs_pos. } replace (RiemannInt (RiemannInt_P10 (-1) H7 (RiemannInt_P14 x (x + h0) (f x)))) with (- RiemannInt (RiemannInt_P1 (RiemannInt_P10 (-1) H7 (RiemannInt_P14 x (x + h0) (f x))))). { rewrite Rabs_Ropp; apply (RiemannInt_P17 (RiemannInt_P1 (RiemannInt_P10 (-1) H7 (RiemannInt_P14 x (x + h0) (f x)))) (RiemannInt_P16 (RiemannInt_P1 (RiemannInt_P10 (-1) H7 (RiemannInt_P14 x (x + h0) (f x)))))); auto with real. } symmetry ; apply RiemannInt_P8. } apply Rle_lt_trans with (RiemannInt (RiemannInt_P14 (x + h0) x (eps / 2)) * Rabs (/ h0)). { do 2 rewrite <- (Rmult_comm (Rabs (/ h0))); apply Rmult_le_compat_l. { apply Rabs_pos. } apply RiemannInt_P19. { auto with real. } intros; replace (f x1 + -1 * fct_cte (f x) x1) with (f x1 - f x). { unfold fct_cte; case (Req_dec x x1); intro. { rewrite H9; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; left; assumption. } elim H3; intros; left; apply H11. repeat split. { assumption. } rewrite Rabs_left. { apply Rplus_lt_reg_l with (x1 - x0); replace (x1 - x0 + x0) with x1 by ring. replace (x1 - x0 + - (x1 - x)) with (x - x0) by ring. apply Rle_lt_trans with (x + h0). { unfold Rminus; apply Rplus_le_compat_l; apply Ropp_le_cancel. rewrite Ropp_involutive; apply Rle_trans with (Rabs h0). { rewrite <- Rabs_Ropp; apply RRle_abs. } apply Rle_trans with del; [ left; assumption | unfold del; apply Rmin_l ]. } elim H8; intros; assumption. } lra. } unfold fct_cte; ring. } rewrite RiemannInt_P15. rewrite Rmult_assoc; replace ((x - (x + h0)) * Rabs (/ h0)) with 1. { lra. } rewrite Rabs_left. { field. lra. } apply Rinv_lt_0_compat. assert (H8 : x + h0 < x). { auto with real. } apply Rplus_lt_reg_l with x; rewrite Rplus_0_r; assumption. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra