proposition: Lemma is_derive_RInt_param_bound_comp_aux1 : forall (f : R -> R -> R) (a : R -> R) (x : R), (exists eps:posreal, locally x (fun y : R => ex_RInt (fun t => f y t) (a x - eps) (a x + eps))) -> (exists eps:posreal, locally x (fun x0 : R => forall t : R, a x-eps <= t <= a x+eps -> ex_derive (fun u : R => f u t) x0)) -> (locally_2d (fun x' t => continuity_2d_pt (fun u v : R => Derive (fun z : R => f z v) u) x' t) x (a x)) -> continuity_2d_pt (fun u v : R => Derive (fun z : R => RInt (fun t : R => f z t) v (a x)) u) x (a x).
proof: Proof. intros f a x (d1,(d2,Ia)) (d3,(d4,Df)) Cdf e. assert (J1:(continuity_2d_pt (fun u v : R => Derive (fun z : R => f z v) u) x (a x))) by now apply locally_2d_singleton in Cdf. destruct Cdf as (d5,Cdf). destruct (J1 (mkposreal _ Rlt_0_1)) as (d6,Df1); simpl in Df1. assert (J2: 0 < e / (Rabs (Derive (fun z : R => f z (a x)) x)+1)). apply Rdiv_lt_0_compat. apply cond_pos. apply Rlt_le_trans with (0+1). rewrite Rplus_0_l; apply Rlt_0_1. apply Rplus_le_compat_r; apply Rabs_pos. exists (mkposreal _ (Rmin_stable_in_posreal (mkposreal _ (Rmin_stable_in_posreal d1 (mkposreal _ (Rmin_stable_in_posreal (pos_div_2 d2) d3)))) (mkposreal _ (Rmin_stable_in_posreal (mkposreal _ (Rmin_stable_in_posreal (pos_div_2 d4) d5)) (mkposreal _ (Rmin_stable_in_posreal d6 (mkposreal _ J2))))))). simpl; intros u v Hu Hv. rewrite (Derive_ext (fun z : R => RInt (fun t : R => f z t) (a x) (a x)) (fun z => 0)). 2: intros t; exact: RInt_point. replace (Derive (fun _ : R => 0) x) with 0%R. 2: apply sym_eq, Derive_const. rewrite Rminus_0_r. replace (Derive (fun z : R => RInt (fun t : R => f z t) v (a x)) u) with (RInt (fun z => Derive (fun u => f u z) u) v (a x)). apply Rle_lt_trans with (Rabs (a x -v) * (Rabs (Derive (fun z : R => f z (a x)) x) +1)). apply (norm_RInt_le_const_abs (fun z : R => Derive (fun u0 : R => f u0 z) u) v (a x)). intros t Ht. apply Rplus_le_reg_r with (-Rabs (Derive (fun z : R => f z (a x)) x)). apply Rle_trans with (1:=Rabs_triang_inv _ _). ring_simplify. left; apply Df1. apply Rlt_le_trans with (1:=Hu). apply Rle_trans with (1:=Rmin_r _ _). apply Rle_trans with (1:=Rmin_r _ _). apply Rmin_l. apply Rle_lt_trans with (Rabs (v - a x)). now apply Rabs_le_between_min_max. apply Rlt_le_trans with (1:=Hv). apply Rle_trans with (1:=Rmin_r _ _). apply Rle_trans with (1:=Rmin_r _ _). apply Rmin_l. apply: RInt_correct. apply: ex_RInt_continuous. intros y Hy ; apply continuity_pt_filterlim. intros eps Heps. assert (Y1:(Rabs (u - x) < d5)). apply Rlt_le_trans with (1:=Hu). apply Rle_trans with (1:=Rmin_r _ _). apply Rle_trans with (1:=Rmin_l _ _). apply Rmin_r. assert (Y2:(Rabs (y - a x) < d5)). apply Rle_lt_trans with (Rabs (v-a x)). now apply Rabs_le_between_min_max. apply Rlt_le_trans with (1:=Hv). apply Rle_trans with (1:=Rmin_r _ _). apply Rle_trans with (1:=Rmin_l _ _). apply Rmin_r. destruct (Cdf u y Y1 Y2 (mkposreal eps Heps)) as (d,Hd); simpl in Hd. exists d; split. apply cond_pos. unfold dist; simpl; unfold R_dist. intros z (_,Hz). apply Hd. rewrite /Rminus Rplus_opp_r Rabs_R0. apply cond_pos. exact Hz. replace (a x -v) with (-(v - a x)) by ring; rewrite Rabs_Ropp. apply Rlt_le_trans with ((e / (Rabs (Derive (fun z : R => f z (a x)) x) + 1)) * (Rabs (Derive (fun z : R => f z (a x)) x) + 1)). apply Rmult_lt_compat_r. apply Rlt_le_trans with (0+1). rewrite Rplus_0_l; apply Rlt_0_1. apply Rplus_le_compat_r; apply Rabs_pos. apply Rlt_le_trans with (1:=Hv). apply Rle_trans with (1:=Rmin_r _ _). apply Rle_trans with (1:=Rmin_r _ _). apply Rmin_r. right; field. apply sym_not_eq, Rlt_not_eq. apply Rlt_le_trans with (0+1). rewrite Rplus_0_l; apply Rlt_0_1. apply Rplus_le_compat_r; apply Rabs_pos. apply sym_eq, is_derive_unique. apply is_derive_RInt_param. exists (pos_div_2 d4). intros y Hy t Ht. apply Df. rewrite (double_var d4). apply ball_triangle with u. apply Rlt_le_trans with (1:=Hu). apply Rle_trans with (1:=Rmin_r _ _). apply Rle_trans with (1:=Rmin_l _ _). apply Rmin_l. by apply Hy. apply (proj1 (Rabs_le_between' t (a x) d3)). apply Rle_trans with (Rabs (v - a x)). now apply Rabs_le_between_min_max. left; apply Rlt_le_trans with (1:=Hv). apply Rle_trans with (1:=Rmin_l _ _). apply Rle_trans with (1:=Rmin_r _ _). apply Rmin_r. intros t Ht. apply Cdf. apply Rlt_le_trans with (1:=Hu). apply Rle_trans with (1:=Rmin_r _ _). apply Rle_trans with (1:=Rmin_l _ _). apply Rmin_r. apply Rle_lt_trans with (Rabs (v - a x)). now apply Rabs_le_between_min_max. apply Rlt_le_trans with (1:=Hv). apply Rle_trans with (1:=Rmin_r _ _). apply Rle_trans with (1:=Rmin_l _ _). apply Rmin_r. exists (pos_div_2 d2). intros y Hy. apply (ex_RInt_inside (f y)) with (a x) d1. apply Ia. rewrite (double_var d2). apply ball_triangle with u. apply Rlt_le_trans with (1:=Hu). apply Rle_trans with (1:=Rmin_l _ _). apply Rle_trans with (1:=Rmin_r _ _). apply Rmin_l. apply Hy. left; apply Rlt_le_trans with (1:=Hv). apply Rle_trans with (1:=Rmin_l _ _). apply Rmin_l. rewrite /Rminus Rplus_opp_r Rabs_R0. left; apply cond_pos. 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