proposition: Theorem derivable_continuous_pt : forall f x, derivable_pt f x -> continuity_pt f x.
proof: Proof. intros f x Hf_deriv eps eps_pos ; destruct Hf_deriv as (l, Hl). case (Ceq_or_neq_C0 l) ; intro Hl_0. assert (eps_2_pos : eps / 2 > 0) by lra ; destruct (Hl (eps / 2)%R eps_2_pos) as ([alpha alpha_pos], Halpha) ; exists (Rmin (1/2) alpha) ; split ; [apply Rmin_pos ; lra|] ; intros x' [_ x'_bd] ; simpl ; simpl in Halpha ; unfold C_dist in *. pose (h := x' - x) ; replace x' with (x + h) by (unfold h ; intuition). case (Ceq_or_neq_C0 h) ; intro Hh_0. rewrite Hh_0, Cadd_0_r, Cminus_diag_eq ; [| reflexivity] ; rewrite Cnorm_C0 ; assumption. apply Rlt_trans with (Cnorm h*eps)%R. apply Rle_lt_trans with (Cnorm (f (x + h)%C - f x) * (/ Cnorm h * Cnorm h))%R. right ; field ; apply Rgt_not_eq ; apply Cnorm_pos_lt ; assumption. unfold Rdiv ; rewrite <- Rmult_assoc ; rewrite <- Cnorm_inv, <- Cnorm_Cmult. rewrite Rmult_comm ; apply Rmult_lt_compat_l. apply Cnorm_pos_lt ; assumption. replace ((f (x + h) - f x) * / h) with ((f (x + h) - f x) / h - l). apply Rlt_trans with (eps / 2)%R ; [apply Halpha ; intuition | lra]. subst ; apply Rlt_le_trans with (Rmin (1/2) alpha) ; [apply x'_bd | apply Rmin_r]. rewrite Hl_0. rewrite Cminus_0_r. auto. assumption. apply Rlt_trans with ((Rmin (1/2) alpha) * eps)%R. apply Rmult_lt_compat_r ; assumption. apply Rle_lt_trans with (eps / 2)%R. unfold Rdiv ; rewrite Rmult_comm ; apply Rmult_le_compat_l ; intuition ; apply Rle_trans with (1 * /2)%R ; [apply Rmin_l | right ; field]. lra. assert (eps_2_pos : eps / 2 > 0) by lra ; destruct (Hl (eps / 2)%R eps_2_pos) as ([alpha alpha_pos], Halpha). exists (Rmin (eps / (2 * Cnorm l)) (Rmin (1/2) alpha)) ; split ; [apply Rmin_pos |]. unfold Rdiv ; rewrite Rinv_mult_distr ; repeat apply Rmult_lt_0_compat. assumption. lra. apply Rinv_0_lt_compat ; apply Cnorm_pos_lt ; assumption. apply Rgt_not_eq ; lra. apply Rgt_not_eq ; apply Cnorm_pos_lt ; assumption. apply Rmin_pos ; lra. intros x' [_ x'_bd] ; simpl ; unfold C_dist. pose (h := x' - x) ; replace x' with (x+h) by (unfold h ; intuition) ; case (Ceq_or_neq_C0 h) ; intro Hh_0. rewrite Hh_0, Cadd_0_r, Cminus_diag_eq ; [| reflexivity] ; rewrite Cnorm_C0 ; assumption. apply Rlt_trans with (Cnorm h * eps + Cnorm h * Cnorm l )%R. apply Rle_lt_trans with (Cnorm (f (x + h)%C - f x) * (/ Cnorm h * Cnorm h))%R. right ; field ; apply Rgt_not_eq ; apply Cnorm_pos_lt ; assumption. unfold Rdiv ; rewrite <- Rmult_assoc ; rewrite <- Cnorm_inv, <- Cnorm_Cmult. apply Rle_lt_trans with ((Cnorm ((f (x + h)%C - f x) * / h) + (- Cnorm l + Cnorm l)) * Cnorm h)%R. right ; field. repeat rewrite Rmult_plus_distr_r. replace (Cnorm l * Cnorm h)%R with (Cnorm h * Cnorm l)%R by (apply Rmult_comm). rewrite <- Rplus_assoc ; apply Rplus_lt_compat_r. apply Rle_lt_trans with (Cnorm ((f (x +h)%C - f x) / h - l)* Cnorm h)%R. rewrite <- Rmult_plus_distr_r ; apply Rmult_le_compat_r ; [apply Cnorm_pos | apply Cnorm_triang_rev_l]. rewrite Rmult_comm ; apply Rmult_lt_compat_l. apply Cnorm_pos_lt ; assumption. apply Rlt_trans with (eps /2)%R ; [apply Halpha | lra]. assumption. unfold h ; apply Rlt_le_trans with (Rmin (eps / (2 * Cnorm l)) (Rmin (1/2) alpha)) ; [apply x'_bd |]. apply Rle_trans with (Rmin (1/2) alpha) ; apply Rmin_r. assumption. apply Rlt_trans with (eps / 2 + Cnorm h * Cnorm l)%R. apply Rplus_lt_compat_r ; unfold h. unfold Rdiv ; rewrite Rmult_comm ; apply Rmult_lt_compat_l ; [assumption |]. apply Rlt_le_trans with (Rmin (eps / (2 * Cnorm l)) (Rmin (1 / 2) alpha)). assumption. apply Rle_trans with (Rmin (1/2) alpha) ; [apply Rmin_r | apply Rle_trans with (1/2)%R ; [apply Rmin_l | right ; field]]. apply Rlt_le_trans with (eps / 2 + eps / 2)%R ; [apply Rplus_lt_compat_l | right ; field]. replace (eps / 2)%R with ((eps / (2 * Cnorm l)) * Cnorm l)%R by (field ; apply Cnorm_no_R0 ; assumption). apply Rmult_lt_compat_r. apply Cnorm_pos_lt ; assumption. unfold h ; apply Rlt_le_trans with (Rmin (eps / (2 * Cnorm l)) (Rmin (1 / 2) alpha)). apply x'_bd. apply Rmin_l. Qed.
imports: MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_usual Ranalysis_facts Ranalysis_MVT Canalysis_diff Cprop_base Cnorm Ctacfield Cmet Canalysis_def Cderiv