proposition: Lemma is_derive_RInt_param_aux : forall (f : R -> R -> R) (a b x : R), locally x (fun x : R => forall t, Rmin a b <= t <= Rmax a b -> ex_derive (fun u : R => f u t) x) -> (forall t, Rmin a b <= t <= Rmax a b -> continuity_2d_pt (fun u v => Derive (fun z => f z v) u) x t) -> locally x (fun y : R => ex_RInt (fun t => f y t) a b) -> ex_RInt (fun t => Derive (fun u => f u t) x) a b -> is_derive (fun x : R => RInt (fun t => f x t) a b) x (RInt (fun t => Derive (fun u => f u t) x) a b).
proof: Proof. intros f a b x. wlog: a b / a < b => H. destruct (total_order_T a b) as [[Hab|Hab]|Hab]. now apply H. intros _ _ _ _. rewrite Hab. rewrite RInt_point. apply is_derive_ext with (fun _ => 0). simpl => t. apply sym_eq. apply: RInt_point. apply: is_derive_const. simpl => H1 H2 H3 H4. apply is_derive_ext_loc with (fun u => - RInt (fun t => f u t) b a). apply: filter_imp H3 => t Ht. apply: opp_RInt_swap. exact: ex_RInt_swap. eapply filterdiff_ext_lin. apply @filterdiff_opp_fct ; try by apply locally_filter. apply H. exact Hab. now rewrite Rmin_comm Rmax_comm. now rewrite Rmin_comm Rmax_comm. move: H3 ; apply filter_imp => y H3. now apply ex_RInt_swap. now apply ex_RInt_swap. rewrite -opp_RInt_swap //=. intros y. by rewrite -scal_opp_r opp_opp. rewrite Rmin_left. 2: now apply Rlt_le. rewrite Rmax_right. 2: now apply Rlt_le. intros Df Cdf If IDf. split => [ | y Hy]. by apply @is_linear_scal_l. rewrite -(is_filter_lim_locally_unique _ _ Hy) => {y Hy}. assert (Cdf'' : forall t : R, a <= t <= b -> continuity_2d_pt (fun u v : R => Derive (fun z : R => f z u) v) t x). intros t Ht eps. specialize (Cdf t Ht eps). simpl in Cdf. destruct Cdf as (d,Cdf). exists d. intros v u Hv Hu. now apply Cdf. assert (Cdf' := uniform_continuity_2d_1d (fun u v => Derive (fun z => f z u) v) a b x Cdf''). intros eps. try clearbody Cdf'. clear Cdf. assert (H': 0 < eps / Rabs (b - a)). apply Rmult_lt_0_compat. apply cond_pos. apply Rinv_0_lt_compat. apply Rabs_pos_lt. apply Rgt_not_eq. now apply Rgt_minus. move: (Cdf' (mkposreal _ H')) => {Cdf'} [d1 Cdf]. generalize (filter_and _ _ Df If). move => {Df If} [d2 DIf]. exists (mkposreal _ (Rmin_stable_in_posreal d1 (pos_div_2 d2))) => /= y Hy. assert (D1: ex_RInt (fun t => f y t) a b). apply DIf. apply Rlt_le_trans with (1 := Hy). apply Rle_trans with (1 := Rmin_r _ _). apply Rlt_le. apply Rlt_eps2_eps. apply cond_pos. assert (D2: ex_RInt (fun t => f x t) a b). apply DIf. apply ball_center. rewrite -RInt_minus // -RInt_scal //. assert (D3: ex_RInt (fun t => f y t - f x t) a b). apply @ex_RInt_minus. by apply D1. by apply D2. assert (D4: ex_RInt (fun t => (y - x) * Derive (fun u => f u t) x) a b) by now apply @ex_RInt_scal. rewrite -RInt_minus //. assert (D5: ex_RInt (fun t => f y t - f x t - (y - x) * Derive (fun u => f u t) x) a b) by now apply @ex_RInt_minus. rewrite (RInt_Reals _ _ _ (ex_RInt_Reals_0 _ _ _ D5)). assert (D6: ex_RInt (fun t => Rabs (f y t - f x t - (y - x) * Derive (fun u => f u t) x)) a b) by now apply ex_RInt_norm. apply Rle_trans with (1 := RiemannInt_P17 _ (ex_RInt_Reals_0 _ _ _ D6) (Rlt_le _ _ H)). refine (Rle_trans _ _ _ (RiemannInt_P19 _ (RiemannInt_P14 a b (eps / Rabs (b - a) * Rabs (y - x))) (Rlt_le _ _ H) _) _). intros u Hu. destruct (MVT_cor4 (fun t => f t u) (Derive (fun t => f t u)) x) with (eps := pos_div_2 d2) (b := y) as (z,Hz). intros z Hz. apply Derive_correct, DIf. apply Rle_lt_trans with (1 := Hz). apply: Rlt_eps2_eps. apply cond_pos. split ; now apply Rlt_le. apply Rlt_le. apply Rlt_le_trans with (1 := Hy). apply Rmin_r. rewrite (proj1 Hz). rewrite Rmult_comm. rewrite -Rmult_minus_distr_l Rabs_mult. rewrite Rmult_comm. apply Rmult_le_compat_r. apply Rabs_pos. apply Rlt_le. apply Cdf. split ; now apply Rlt_le. apply Rabs_le_between'. rewrite /Rminus Rplus_opp_r Rabs_R0. apply Rlt_le. apply cond_pos. split ; now apply Rlt_le. apply Rabs_le_between'. apply Rle_trans with (1 := proj2 Hz). apply Rlt_le. apply Rlt_le_trans with (1 := Hy). apply Rmin_l. rewrite /Rminus Rplus_opp_r Rabs_R0. apply cond_pos. rewrite RiemannInt_P15. rewrite Rabs_pos_eq. right. change (norm (minus y x)) with (Rabs (y - x)). field. apply Rgt_not_eq. now apply Rgt_minus. apply Rge_le. apply Rge_minus. now apply Rgt_ge. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(eqtype seq) Markov Rcomplements Rbar Lub Lim_seq Derive SF_seq Continuity Hierarchy Seq_fct RInt PSeries