proposition: Lemma Dfn_CVU_implies_Df_exists : forall (fn fn' : nat -> R -> R) f g x lb ub (pr : lb < ub), open_interval lb ub x -> (forall n x, open_interval lb ub x -> derivable_pt_lim_in (open_interval lb ub) (fn n) x (fn' n x)) -> (forall x, open_interval lb ub x -> Rseq_cv (fun n => fn n x) (f x)) -> (CVU fn' g (middle lb ub) (mkposreal (interval_size lb ub) (interval_size_pos _ _ pr))) -> (continuity_in (open_interval lb ub) g) -> derivable_pt_lim f x (g x).
proof: Proof. intros fn fn' f g x lb ub pr x_in Dfn_eq_fn' fn_CV_f fn'_CVU_g g_cont eps eps_pos. assert (eps_6_pos : 0 < (eps / 3) / 2). apply Rlt_mult_inv_pos ; [apply Rlt_mult_inv_pos |] ; lra. destruct (g_cont _ x_in _ eps_6_pos) as [d1 [d1_pos Hd1]]. pose (delta := Rmin (interval_dist lb ub x) d1) ; assert (delta_pos : 0 < delta). apply Rmin_pos_lt ; [apply open_interval_dist_pos |] ; assumption. exists (mkposreal _ delta_pos) ; intros h h_neq h_bd. pose (eps1 := Rabs h * eps / 3) ; assert (eps1_pos : 0 < eps1). unfold eps1 ; repeat apply Rmult_lt_0_compat ; [apply Rabs_pos_lt ; assumption | |] ; lra. destruct (fn_CV_f x x_in _ eps1_pos) as [N1 HN1]. assert (xh_in : open_interval lb ub (x + h)). apply open_interval_dist_bound. apply open_interval_interval ; assumption. eapply Rlt_le_trans ; [eassumption | apply Rmin_l]. destruct (fn_CV_f (x + h) xh_in _ eps1_pos) as [N2 HN2]. destruct (fn'_CVU_g _ eps_6_pos) as [N3 HN3]. pose (N := max (max N1 N2) N3). apply Rle_lt_trans with (Rabs ((f (x + h) - f x) - h * g x) * Rabs (/ h)). right ; rewrite <- Rabs_mult ; apply Rabs_eq_compat ; field ; assumption. apply Rlt_le_trans with (Rabs h * eps * Rabs (/ h)). apply Rmult_lt_compat_r ; [apply Rabs_pos_lt, Rinv_neq_0_compat ; assumption |]. apply Rle_lt_trans with (Rabs (f (x + h) - fn N (x + h) + - (f x - fn N x) + ((fn N (x + h) - fn N x) - h * g x))). right ; apply Rabs_eq_compat ; ring. eapply Rle_lt_trans ; [eapply Rabs_triang |]. eapply Rle_lt_trans ; [eapply Rplus_le_compat_r, Rabs_triang |]. rewrite Rabs_Ropp. destruct (Rneq_lt_gt_dec _ _ h_neq) as [h_neg | h_pos]. assert (c_deduc : forall c, interval (x + h) x c -> open_interval lb ub c). intros ; eapply interval_open_restriction ; [| | eassumption]. apply open_interval_dist_bound ; [apply open_interval_interval | eapply Rlt_le_trans, Rmin_l] ; eassumption. assumption. assert (pr1 : forall c : R, x + h < c < x -> derivable_pt (fn N) c). intros c c_encad ; exists (fn' N c) ; apply derivable_pt_lim_open_interval_pt_lim with lb ub, Dfn_eq_fn' ; apply c_deduc ; apply open_interval_interval ; assumption. assert (pr2 : forall c : R, x + h < c < x -> derivable_pt id c). intros ; apply derivable_pt_id. destruct (MVT (fn N) id (x + h) x pr1 pr2) as [c [c_in H]]. lra. intros c c_encad ; apply derivable_continuous_pt ; exists (fn' N c) ; apply derivable_pt_lim_open_interval_pt_lim with lb ub, Dfn_eq_fn' ; apply c_deduc ; assumption. intros ; apply derivable_continuous, derivable_id. unfold id in H ; rewrite (derive_pt_eq_0 _ _ _ _ (derivable_pt_lim_id c)), Rmult_1_r in H ; ring_simplify in H. assert (Hc : fn N (x + h) - fn N x = h * derive_pt (fn N) c (pr1 c c_in)). apply Rmult_eq_reg_l with (-1) ; [| apply Ropp_neq_0_compat, R1_neq_R0] ; unfold Rminus in H ; ring_simplify ; rewrite H ; apply Rplus_comm. rewrite Hc ; clear Hc H. replace (derive_pt (fn N) c (pr1 c c_in)) with (fn' N c). replace (h * fn' N c - h * g x) with (h * (fn' N c - g x)) by ring. rewrite Rabs_mult. transitivity (eps1 + Rabs (f x - fn N x) + Rabs h * Rabs (fn' N c - g x)). do 2 apply Rplus_lt_compat_r ; rewrite Rabs_minus_sym ; apply HN2. apply Nat.le_trans with (max N1 N2) ; [apply Nat.le_max_r | apply Nat.le_max_l]. transitivity (eps1 + eps1 + Rabs h * Rabs (fn' N c - g x)). apply Rplus_lt_compat_r, Rplus_lt_compat_l ; unfold R_dist in HN1 ; rewrite Rabs_minus_sym ; apply HN1, Nat.le_trans with (max N1 N2) ; apply Nat.le_max_l. replace (fn' N c - g x) with ((fn' N c - g c) + (g c - g x)) by ring. apply Rle_lt_trans with (eps1 + eps1 + Rabs h * Rabs (fn' N c - g c) + Rabs h * Rabs (g c - g x)). do 3 rewrite Rplus_assoc ; do 2 apply Rplus_le_compat_l ; rewrite <- Rmult_plus_distr_l ; apply Rmult_le_compat_l ; [apply Rabs_pos | apply Rabs_triang]. apply Rlt_trans with (eps1 + eps1 + Rabs h * ((eps / 3) / 2) + Rabs h * Rabs (g c - g x)). apply Rplus_lt_compat_r, Rplus_lt_compat_l, Rmult_lt_compat_l. apply Rabs_pos_lt ; assumption. rewrite Rabs_minus_sym ; apply HN3 ; [apply Nat.le_max_r |]. apply interval_size_Boule_middle, c_deduc, open_interval_interval ; assumption. apply Rlt_le_trans with (eps1 + eps1 + Rabs h * (eps / 3 / 2) + Rabs h * (eps / 3 / 2)) ; [| right ; unfold eps1 ; field] ; repeat rewrite Rplus_assoc ; do 3 apply Rplus_lt_compat_l ; apply Rmult_lt_compat_l ; [apply Rabs_pos_lt ; assumption |]. simpl in Hd1 ; apply Hd1 ; split. apply c_deduc, open_interval_interval ; assumption. transitivity (Rabs h) ; [| apply Rlt_le_trans with delta ; [apply h_bd | apply Rmin_r]]. rewrite Rabs_left ; [| assumption] ; apply Rabs_def1 ; clear -c_in h_neg ; destruct c_in ; [transitivity 0 |] ; lra. destruct (pr1 c c_in) as [l Hl] ; eapply uniqueness_limite ; eauto. eapply derivable_pt_lim_open_interval_pt_lim, Dfn_eq_fn' ; apply c_deduc, open_interval_interval ; assumption. assert (c_deduc : forall c, interval x (x + h) c -> open_interval lb ub c). intros ; eapply interval_open_restriction ; [| | eassumption]. assumption. apply open_interval_dist_bound ; [apply open_interval_interval | eapply Rlt_le_trans, Rmin_l] ; eassumption. assert (pr1 : forall c : R, x < c < x + h -> derivable_pt (fn N) c). intros c c_encad ; exists (fn' N c) ; apply derivable_pt_lim_open_interval_pt_lim with lb ub, Dfn_eq_fn' ; apply c_deduc ; apply open_interval_interval ; assumption. assert (pr2 : forall c : R, x < c < x + h -> derivable_pt id c). intros ; apply derivable_pt_id. destruct (MVT (fn N) id x (x + h) pr1 pr2) as [c [c_in Hc]]. lra. intros c c_encad ; apply derivable_continuous_pt ; exists (fn' N c) ; apply derivable_pt_lim_open_interval_pt_lim with lb ub, Dfn_eq_fn' ; apply c_deduc ; assumption. intros ; apply derivable_continuous, derivable_id. unfold id in Hc ; rewrite (derive_pt_eq_0 _ _ _ _ (derivable_pt_lim_id c)), Rmult_1_r in Hc ; ring_simplify in Hc. rewrite <- Hc ; clear Hc. replace (derive_pt (fn N) c (pr1 c c_in)) with (fn' N c). replace (h * fn' N c - h * g x) with (h * (fn' N c - g x)) by ring. rewrite Rabs_mult. transitivity (eps1 + Rabs (f x - fn N x) + Rabs h * Rabs (fn' N c - g x)). do 2 apply Rplus_lt_compat_r ; rewrite Rabs_minus_sym ; apply HN2. apply Nat.le_trans with (max N1 N2) ; [apply Nat.le_max_r | apply Nat.le_max_l]. transitivity (eps1 + eps1 + Rabs h * Rabs (fn' N c - g x)). apply Rplus_lt_compat_r, Rplus_lt_compat_l ; unfold R_dist in HN1 ; rewrite Rabs_minus_sym ; apply HN1, Nat.le_trans with (max N1 N2) ; apply Nat.le_max_l. replace (fn' N c - g x) with ((fn' N c - g c) + (g c - g x)) by ring. apply Rle_lt_trans with (eps1 + eps1 + Rabs h * Rabs (fn' N c - g c) + Rabs h * Rabs (g c - g x)). do 3 rewrite Rplus_assoc ; do 2 apply Rplus_le_compat_l ; rewrite <- Rmult_plus_distr_l ; apply Rmult_le_compat_l ; [apply Rabs_pos | apply Rabs_triang]. apply Rlt_trans with (eps1 + eps1 + Rabs h * ((eps / 3) / 2) + Rabs h * Rabs (g c - g x)). apply Rplus_lt_compat_r, Rplus_lt_compat_l, Rmult_lt_compat_l. apply Rabs_pos_lt ; assumption. rewrite Rabs_minus_sym ; apply HN3 ; [apply Nat.le_max_r |]. apply interval_size_Boule_middle, c_deduc, open_interval_interval ; assumption. apply Rlt_le_trans with (eps1 + eps1 + Rabs h * (eps / 3 / 2) + Rabs h * (eps / 3 / 2)) ; [| right ; unfold eps1 ; field] ; repeat rewrite Rplus_assoc ; do 3 apply Rplus_lt_compat_l ; apply Rmult_lt_compat_l ; [apply Rabs_pos_lt ; assumption |]. simpl in Hd1 ; apply Hd1 ; split. apply c_deduc, open_interval_interval ; assumption. transitivity (Rabs h) ; [| apply Rlt_le_trans with delta ; [apply h_bd | apply Rmin_r]]. rewrite Rabs_right ; [| left ; assumption] ; apply Rabs_def1 ; clear -c_in h_pos ; destruct c_in ; [| transitivity 0] ; lra. destruct (pr1 c c_in) as [l Hl] ; eapply uniqueness_limite ; eauto. eapply derivable_pt_lim_open_interval_pt_lim, Dfn_eq_fn' ; apply c_deduc, open_interval_interval ; assumption. right ; rewrite (Rabs_Rinv _ h_neq) ; field ; apply Rabs_no_R0 ; assumption. Qed.
imports: Rbase Ranalysis Rfunctions Rfunction_def Rseries_def Lra RiemannInt SeqProp PeanoNat RIneq MyRIneq Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rinterval RIVT Rsequence_def