proposition: Lemma derivable_pt_in_continuity_pt_in : forall f D x, derivable_pt_in f D x -> continuity_pt_in f D x.
proof: Proof. intros D f x [l Hl] Dx eps eps_pos. pose (eps' := Rmin eps (eps / (eps + Rabs l))). assert (eps'_pos: 0 < eps'). apply Rmin_pos_lt, Rlt_mult_inv_pos, Rplus_lt_le_0_compat ; [| | | apply Rabs_pos] ; assumption. destruct (Hl _ eps'_pos) as [alp [alp_pos Halp]] ; exists (Rmin alp eps') ; split ; [apply Rmin_pos_lt ; assumption |]. intros y [Dy y_bd] ; destruct (Req_dec y x) as [Heq | Hneq]. subst ; rewrite R_dist_eq ; assumption. transitivity ((eps + Rabs l) * Rabs (y - x)). apply Rle_lt_trans with (Rabs (growth_rate f x y) * Rabs (y - x)). right ; simpl ; unfold R_dist, growth_rate ; rewrite <- Rabs_mult ; apply Rabs_eq_compat ; field ; apply Rminus_eq_contra ; assumption. apply Rle_lt_trans with ((dist R_met (growth_rate f x y) l + Rabs l) * Rabs (y - x)). apply Rmult_le_compat_r ; [apply Rabs_pos |]. apply Rle_trans with (Rabs (growth_rate f x y - l + l)) ; [right ; apply Rabs_eq_compat ; ring | apply Rabs_triang]. apply Rmult_lt_compat_r ; [apply Rabs_pos_lt, Rminus_eq_contra ; assumption |]. apply Rplus_lt_compat_r, Rlt_le_trans with eps'. apply Halp ; repeat split ; [assumption | symmetry ; assumption |]. apply Rlt_le_trans with (Rmin alp eps'), Rmin_l ; assumption. apply Rmin_l. apply Rlt_le_trans with ((eps + Rabs l) * eps'). apply Rmult_lt_compat_l. apply Rplus_lt_le_0_compat ; [assumption | apply Rabs_pos]. apply Rlt_le_trans with (Rmin alp eps') ; [apply y_bd | apply Rmin_r]. transitivity ((eps + Rabs l) * (eps / (eps + Rabs l))). apply Rmult_le_compat_l, Rmin_r ; apply Rplus_le_le_0_compat ; [left ; assumption | apply Rabs_pos]. right ; field ; apply Rgt_not_eq, Rplus_lt_le_0_compat, Rabs_pos ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics