proposition: Lemma derivable_pt_lim_CVU (fn fn':nat -> R -> R) (f g:R->R) (x:R) : forall c r, Boule c r x -> (forall y n, Boule c r y -> derivable_pt_lim (fn n) y (fn' n y)) -> (forall y, Boule c r y -> Un_cv (fun n => fn n y) (f y)) -> (CVU fn' g c r) -> (forall y, Boule c r y -> continuity_pt g y) -> derivable_pt_lim f x (g x).
proof: Proof. intros c' r xinb Dfn_eq_fn' fn_CV_f fn'_CVU_g g_cont eps eps_pos. assert (eps_8_pos : 0 < eps / 8) by lra. elim (g_cont x xinb _ eps_8_pos) ; clear g_cont ; intros delta1 (delta1_pos, g_cont). destruct (Ball_in_inter _ _ _ _ _ xinb (Boule_center x (mkposreal _ delta1_pos))) as [delta Pdelta]. exists delta; intros h hpos hinbdelta. assert (eps'_pos : 0 < (Rabs h) * eps / 4). { unfold Rdiv ; rewrite Rmult_assoc ; apply Rmult_lt_0_compat. { apply Rabs_pos_lt ; assumption. } lra. } destruct (fn_CV_f x xinb ((Rabs h) * eps / 4) eps'_pos) as [N2 fnx_CV_fx]. assert (xhinbxdelta : Boule x delta (x + h)). { clear -hinbdelta; apply Rabs_def2 in hinbdelta; unfold Boule; simpl. destruct hinbdelta; apply Rabs_def1; lra. } assert (t : Boule c' r (x + h)). { apply Pdelta in xhinbxdelta; tauto. } destruct (fn_CV_f (x+h) t ((Rabs h) * eps / 4) eps'_pos) as [N1 fnxh_CV_fxh]. clear fn_CV_f t. destruct (fn'_CVU_g (eps/8) eps_8_pos) as [N3 fn'c_CVU_gc]. pose (N := ((N1 + N2) + N3)%nat). assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn N x - h * (g x))) < (Rabs h)*eps). 2:{ replace ((f (x + h) - f x) / h - g x) with ((/h) * ((f (x + h) - f x) - h * g x)) by (field;assumption). rewrite Rabs_mult ; rewrite Rabs_inv. replace eps with (/ Rabs h * (Rabs h * eps)). { apply Rmult_lt_compat_l. { apply Rinv_0_lt_compat ; apply Rabs_pos_lt ; assumption. } replace (f (x + h) - f x - h * g x) with (f (x + h) - fn N (x + h) - (f x - fn N x) + (fn N (x + h) - fn N x - h * g x)) by field. assumption. } field ; apply Rgt_not_eq ; apply Rabs_pos_lt ; assumption. } apply Rle_lt_trans with (Rabs (f (x + h) - fn N (x + h) - (f x - fn N x)) + Rabs ((fn N (x + h) - fn N x - h * g x))). { solve[apply Rabs_triang]. } apply Rle_lt_trans with (Rabs (f (x + h) - fn N (x + h)) + Rabs (- (f x - fn N x)) + Rabs (fn N (x + h) - fn N x - h * g x)). { solve[apply Rplus_le_compat_r ; apply Rabs_triang]. } rewrite Rabs_Ropp. case (Rlt_le_dec h 0) ; intro sgn_h. { assert (pr1 : forall c : R, x + h < c < x -> derivable_pt (fn N) c). { intros c c_encad ; unfold derivable_pt. exists (fn' N c) ; apply Dfn_eq_fn'. assert (t : Boule x delta c). { apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta; destruct c_encad. apply Rabs_def2 in xinb; apply Rabs_def1; lra. } apply Pdelta in t; tauto. } assert (pr2 : forall c : R, x + h < c < x -> derivable_pt id c). { solve[intros; apply derivable_id]. } assert (xh_x : x+h < x) by lra. assert (pr3 : forall c : R, x + h <= c <= x -> continuity_pt (fn N) c). { intros c c_encad ; apply derivable_continuous_pt. exists (fn' N c) ; apply Dfn_eq_fn' ; intuition. assert (t : Boule x delta c). { apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. apply Rabs_def2 in xinb; apply Rabs_def1; lra. } apply Pdelta in t; tauto. } assert (pr4 : forall c : R, x + h <= c <= x -> continuity_pt id c). { solve[intros; apply derivable_continuous ; apply derivable_id]. } destruct (MVT (fn N) id (x+h) x pr1 pr2 xh_x pr3 pr4) as [c [P Hc]]. assert (Hc' : h * derive_pt (fn N) c (pr1 c P) = (fn N (x+h) - fn N x)). { apply Rmult_eq_reg_l with (-1). { replace (-1 * (h * derive_pt (fn N) c (pr1 c P))) with (-h * derive_pt (fn N) c (pr1 c P)) by field. replace (-1 * (fn N (x + h) - fn N x)) with (- (fn N (x + h) - fn N x)) by field. replace (-h) with (id x - id (x + h)) by (unfold id; field). rewrite <- Rmult_1_r ; replace 1 with (derive_pt id c (pr2 c P)) by reg. replace (- (fn N (x + h) - fn N x)) with (fn N x - fn N (x + h)) by field. assumption. } now apply Rlt_not_eq, IZR_lt. } rewrite <- Hc'; clear Hc Hc'. replace (derive_pt (fn N) c (pr1 c P)) with (fn' N c). 2:{ assert (H := pr1 c P) ; elim H ; clear H ; intros l Hl. assert (Temp : l = fn' N c). { assert (bc'rc : Boule c' r c). { assert (t : Boule x delta c). { clear - xhinbxdelta P. destruct P; apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. apply Rabs_def1; lra. } apply Pdelta in t; tauto. } assert (Hl' := Dfn_eq_fn' c N bc'rc). unfold derivable_pt_abs in Hl; clear -Hl Hl'. apply uniqueness_limite with (f:= fn N) (x:=c) ; assumption. } rewrite <- Temp. assert (Hl' : derivable_pt (fn N) c). { exists l ; apply Hl. } rewrite pr_nu_var with (g:= fn N) (pr2:=Hl'). { elim Hl' ; clear Hl' ; intros l' Hl'. assert (Main : l = l'). { apply uniqueness_limite with (f:= fn N) (x:=c) ; assumption. } rewrite Main ; reflexivity. } reflexivity. } replace (h * fn' N c - h * g x) with (h * (fn' N c - g x)) by field. rewrite Rabs_mult. apply Rlt_trans with (Rabs h * eps / 4 + Rabs (f x - fn N x) + Rabs h * Rabs (fn' N c - g x)). { apply Rplus_lt_compat_r ; apply Rplus_lt_compat_r ; unfold Rdist in fnxh_CV_fxh ; rewrite Rabs_minus_sym ; apply fnxh_CV_fxh. unfold N; lia. } apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g x)). { apply Rplus_lt_compat_r ; apply Rplus_lt_compat_l. unfold Rdist in fnx_CV_fx ; rewrite Rabs_minus_sym ; apply fnx_CV_fx. unfold N ; lia. } replace (fn' N c - g x) with ((fn' N c - g c) + (g c - g x)) by field. apply Rle_lt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g c) + Rabs h * Rabs (g c - g x)). { rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite Rplus_assoc ; apply Rplus_le_compat_l ; apply Rplus_le_compat_l ; rewrite <- Rmult_plus_distr_l ; apply Rmult_le_compat_l. { solve[apply Rabs_pos]. } solve[apply Rabs_triang]. } apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) + Rabs h * Rabs (g c - g x)). { apply Rplus_lt_compat_r; apply Rplus_lt_compat_l; apply Rmult_lt_compat_l. { apply Rabs_pos_lt ; assumption. } rewrite Rabs_minus_sym ; apply fn'c_CVU_gc. { unfold N ; lia. } assert (t : Boule x delta c). { destruct P. apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. apply Rabs_def2 in xinb; apply Rabs_def1; lra. } apply Pdelta in t; tauto. } apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) + Rabs h * (eps / 8)). { rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite Rplus_assoc ; apply Rplus_lt_compat_l ; apply Rplus_lt_compat_l ; rewrite <- Rmult_plus_distr_l ; rewrite <- Rmult_plus_distr_l ; apply Rmult_lt_compat_l. { apply Rabs_pos_lt ; assumption. } apply Rplus_lt_compat_l ; simpl in g_cont ; apply g_cont ; split ; [unfold D_x ; split |]. - solve[unfold no_cond ; intuition]. - apply Rgt_not_eq ; exact (proj2 P). - apply Rlt_trans with (Rabs h). { apply Rabs_def1. { apply Rlt_trans with 0. { destruct P; lra. } apply Rabs_pos_lt ; assumption. } rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_involutive;[ | lra]. destruct P; lra. } clear -Pdelta xhinbxdelta. apply Pdelta in xhinbxdelta; destruct xhinbxdelta as [_ P']. apply Rabs_def2 in P'; simpl in P'; destruct P'; apply Rabs_def1; lra. } rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite <- Rmult_plus_distr_l. replace (Rabs h * eps / 4 + (Rabs h * eps / 4 + Rabs h * (eps / 8 + eps / 8))) with (Rabs h * (eps / 4 + eps / 4 + eps / 8 + eps / 8)) by field. apply Rmult_lt_compat_l. { apply Rabs_pos_lt ; assumption. } lra. } assert (h_pos : h > 0). { case sgn_h ; intro Hyp. { assumption. } apply False_ind ; apply hpos ; symmetry ; assumption. } clear sgn_h. assert (pr1 : forall c : R, x < c < x + h -> derivable_pt (fn N) c). { intros c c_encad ; unfold derivable_pt. exists (fn' N c) ; apply Dfn_eq_fn'. assert (t : Boule x delta c). { apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta; destruct c_encad. apply Rabs_def2 in xinb; apply Rabs_def1; lra. } apply Pdelta in t; tauto. } assert (pr2 : forall c : R, x < c < x + h -> derivable_pt id c). { solve[intros; apply derivable_id]. } assert (xh_x : x < x + h) by lra. assert (pr3 : forall c : R, x <= c <= x + h -> continuity_pt (fn N) c). { intros c c_encad ; apply derivable_continuous_pt. exists (fn' N c) ; apply Dfn_eq_fn' ; intuition. assert (t : Boule x delta c). { apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. apply Rabs_def2 in xinb; apply Rabs_def1; lra. } apply Pdelta in t; tauto. } assert (pr4 : forall c : R, x <= c <= x + h -> continuity_pt id c). { solve[intros; apply derivable_continuous ; apply derivable_id]. } destruct (MVT (fn N) id x (x+h) pr1 pr2 xh_x pr3 pr4) as [c [P Hc]]. assert (Hc' : h * derive_pt (fn N) c (pr1 c P) = fn N (x+h) - fn N x). { pattern h at 1; replace h with (id (x + h) - id x) by (unfold id; field). rewrite <- Rmult_1_r ; replace 1 with (derive_pt id c (pr2 c P)) by reg. assumption. } rewrite <- Hc'; clear Hc Hc'. replace (derive_pt (fn N) c (pr1 c P)) with (fn' N c). { replace (h * fn' N c - h * g x) with (h * (fn' N c - g x)) by field. rewrite Rabs_mult. apply Rlt_trans with (Rabs h * eps / 4 + Rabs (f x - fn N x) + Rabs h * Rabs (fn' N c - g x)). { apply Rplus_lt_compat_r ; apply Rplus_lt_compat_r ; unfold Rdist in fnxh_CV_fxh ; rewrite Rabs_minus_sym ; apply fnxh_CV_fxh. unfold N; lia. } apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g x)). { apply Rplus_lt_compat_r ; apply Rplus_lt_compat_l. unfold Rdist in fnx_CV_fx ; rewrite Rabs_minus_sym ; apply fnx_CV_fx. unfold N ; lia. } replace (fn' N c - g x) with ((fn' N c - g c) + (g c - g x)) by field. apply Rle_lt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g c) + Rabs h * Rabs (g c - g x)). { rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite Rplus_assoc ; apply Rplus_le_compat_l ; apply Rplus_le_compat_l ; rewrite <- Rmult_plus_distr_l ; apply Rmult_le_compat_l. { solve[apply Rabs_pos]. } solve[apply Rabs_triang]. } apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) + Rabs h * Rabs (g c - g x)). { apply Rplus_lt_compat_r; apply Rplus_lt_compat_l; apply Rmult_lt_compat_l. { apply Rabs_pos_lt ; assumption. } rewrite Rabs_minus_sym ; apply fn'c_CVU_gc. { unfold N ; lia. } assert (t : Boule x delta c). { destruct P. apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. apply Rabs_def2 in xinb; apply Rabs_def1; lra. } apply Pdelta in t; tauto. } apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) + Rabs h * (eps / 8)). { rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite Rplus_assoc ; apply Rplus_lt_compat_l ; apply Rplus_lt_compat_l ; rewrite <- Rmult_plus_distr_l ; rewrite <- Rmult_plus_distr_l ; apply Rmult_lt_compat_l. { apply Rabs_pos_lt ; assumption. } apply Rplus_lt_compat_l ; simpl in g_cont ; apply g_cont ; split ; [unfold D_x ; split |]. - solve[unfold no_cond ; intuition]. - apply Rlt_not_eq ; exact (proj1 P). - apply Rlt_trans with (Rabs h). { apply Rabs_def1. { destruct P; rewrite Rabs_pos_eq;lra. } apply Rle_lt_trans with 0. { assert (t := Rabs_pos h); clear -t; lra. } clear -P; destruct P; lra. } clear -Pdelta xhinbxdelta. apply Pdelta in xhinbxdelta; destruct xhinbxdelta as [_ P']. apply Rabs_def2 in P'; simpl in P'; destruct P'; apply Rabs_def1; lra. } rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite <- Rmult_plus_distr_l. replace (Rabs h * eps / 4 + (Rabs h * eps / 4 + Rabs h * (eps / 8 + eps / 8))) with (Rabs h * (eps / 4 + eps / 4 + eps / 8 + eps / 8)) by field. apply Rmult_lt_compat_l. { apply Rabs_pos_lt ; assumption. } lra. } assert (H := pr1 c P) ; elim H ; clear H ; intros l Hl. assert (Temp : l = fn' N c). { assert (bc'rc : Boule c' r c). { assert (t : Boule x delta c). { clear - xhinbxdelta P. destruct P; apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. apply Rabs_def1; lra. } apply Pdelta in t; tauto. } assert (Hl' := Dfn_eq_fn' c N bc'rc). unfold derivable_pt_abs in Hl; clear -Hl Hl'. apply uniqueness_limite with (f:= fn N) (x:=c) ; assumption. } rewrite <- Temp. assert (Hl' : derivable_pt (fn N) c). { exists l ; apply Hl. } rewrite pr_nu_var with (g:= fn N) (pr2:=Hl'). { elim Hl' ; clear Hl' ; intros l' Hl'. assert (Main : l = l'). { apply uniqueness_limite with (f:= fn N) (x:=c) ; assumption. } rewrite Main ; reflexivity. } reflexivity. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra