proposition: Lemma RiemannInt_derivable_pt_lim : forall (f:R -> R) (a x:R) (pr:forall x y:R, Riemann_integrable f x y) (Hcont:continuity_pt f x), derivable_pt_lim (fun t1 => @RiemannInt f a t1 (pr a t1)) x (f x).
proof: Proof. intros. unfold derivable_pt_lim. intros. assert (H4:0 < eps / 2) by lra. destruct (Hcont _ H4) as [x1 [Hcont1 Hcont2]]. exists (mkposreal _ Hcont1). intros. rewrite <- (RiemannInt_Chasles f a x (x+h) (pr a x) (pr x (x + h)) (pr a (x + h))). ring_simplify ((RiemannInt (pr a x) + RiemannInt (pr x (x + h)) - RiemannInt (pr a x))). replace (f x) with (RiemannInt (Riemann_integrable_constant x (x + h) (f x)) / h) by (rewrite RiemannInt_constant; field; assumption). replace (RiemannInt (pr x (x + h)) / h - RiemannInt (Riemann_integrable_constant x (x + h) (f x)) / h) with ((RiemannInt (pr x (x + h)) + (-1) * RiemannInt (Riemann_integrable_constant x (x + h) (f x))) / h) by (unfold Rdiv ; ring). rewrite RiemannInt_linear_1. unfold Rdiv in |- *; rewrite Rabs_mult; case (Rle_dec x (x + h)); intro. apply Rle_lt_trans with (RiemannInt (Riemann_integrable_Rabs _ _ _ (Riemann_integrable_linear _ _ _ _ (-1) (pr x (x + h)) (Riemann_integrable_constant x (x + h) (f x)))) * Rabs (/ h)). do 2 rewrite <- (Rmult_comm (Rabs (/ h))); apply Rmult_le_compat_l. apply Rabs_pos. apply RiemannInt_le_Rabs. assumption. apply Rle_lt_trans with (RiemannInt (Riemann_integrable_constant x (x + h) (eps / 2)) * Rabs (/ h)). do 2 rewrite <- (Rmult_comm (Rabs (/ h))); apply Rmult_le_compat_l. apply Rabs_pos. apply RiemannInt_P19; try assumption. intros; replace (f x0 + -1 * fct_cte (f x) x0) with (f x0 - f x) by (intros ; unfold fct_cte ; simpl ; ring). unfold fct_cte. assert (x <> x0) by (intro ; subst ; destruct H2 ; lra). left. simpl in *. unfold R_dist in *. apply Hcont2. unfold D_x, no_cond. repeat split. assumption. eapply Rlt_trans ; [|apply H1]. assert (0 < x0 - x < h) by (intuition ; lra). rewrite Rabs_pos_eq. rewrite Rabs_pos_eq. intuition. apply Rle_trans with (x0 - x) ; intuition. intuition. rewrite RiemannInt_constant. rewrite Rmult_assoc; replace ((x + h - x) * Rabs (/ h)) with 1. ring_simplify. lra. rewrite Rabs_right. replace (x + h - x) with h; [ idtac | ring ]. apply Rinv_r_sym. assumption. apply Rle_ge; left; apply Rinv_0_lt_compat. elim r; intro. apply Rplus_lt_reg_r with x; rewrite Rplus_comm, Rplus_0_r, Rplus_comm. assumption. elim H0; symmetry in |- *; apply Rplus_eq_reg_l with x; rewrite Rplus_0_r; assumption. apply Rle_lt_trans with (RiemannInt (Riemann_integrable_Rabs _ _ _ (Riemann_integrable_opp_bound _ _ _ (Riemann_integrable_linear f (fct_cte (f x)) x (x + h) (-1) (pr x (x + h)) (Riemann_integrable_constant x (x + h) (f x))))) * Rabs (/ h)). do 2 rewrite <- (Rmult_comm (Rabs (/ h))); apply Rmult_le_compat_l. apply Rabs_pos. rewrite RiemannInt_bound_exchange_1. rewrite Rabs_Ropp. apply RiemannInt_le_Rabs. left. intuition. apply Rle_lt_trans with (RiemannInt (Riemann_integrable_constant (x + h) x (eps / 2)) * Rabs (/ h)). do 2 rewrite <- (Rmult_comm (Rabs (/ h))); apply Rmult_le_compat_l. apply Rabs_pos. apply RiemannInt_le_ext. auto with real. intros. unfold fct_cte in *. ring_simplify (-1 * f x). intros; replace (f x0 + -1 * fct_cte (f x) x0) with (f x0 - f x). unfold fct_cte in |- *; case (Req_dec x x0); intro. rewrite H3. ring_simplify (f x0 + - f x0). rewrite Rabs_R0; left; assumption. left; simpl in Hcont2 ; ring_simplify (f x0 + -1 * f x) ; apply Hcont2. repeat split. assumption. unfold R_dist. rewrite Rabs_left. apply Rplus_lt_reg_r with (x0 - x1); replace (x0 - x1 + x1) with x0 by ring. replace (- (x0 - x) + (x0 - x1)) with (x - x1) by ring. apply Rle_lt_trans with (x + h). unfold Rminus in |- *; apply Rplus_le_compat_l; apply Ropp_le_cancel. rewrite Ropp_involutive; apply Rle_trans with (Rabs h). rewrite <- Rabs_Ropp; apply RRle_abs. apply Rle_trans with x1; [ left; assumption | idtac ]. right. reflexivity. ring_simplify. now intuition. apply Rplus_lt_reg_r with x. ring_simplify. now intuition. unfold fct_cte in |- *; ring. rewrite RiemannInt_P15. rewrite Rmult_assoc; replace ((x - (x + h)) * Rabs (/ h)) with 1. rewrite Rmult_1_r; unfold Rdiv in |- *; apply Rmult_lt_reg_l with 2; [ prove_sup0 | rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; pattern eps at 1 in |- *; rewrite <- Rplus_0_r; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. rewrite Rabs_left. replace (x - (x + h)) with (- h); [ idtac | ring ]. rewrite Ropp_mult_distr_l_reverse; rewrite Ropp_mult_distr_r_reverse; rewrite Ropp_involutive; apply Rinv_r_sym. assumption. apply Rinv_lt_0_compat. assert (H8 : x + h < x). auto with real. apply Rplus_lt_reg_r with x. ring_simplify. rewrite Rplus_comm; assumption. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality