proposition: Lemma differentiable_continuous_along_axis : forall f (x v : C), differentiable_pt f x v -> continuity_along_axis_pt f v x.
proof: Proof. intros f x v f_diff. destruct (Ceq_dec v C0) as [v_eq | v_neq] ; intros eps eps_pos. exists (mkposreal R1 Rlt_0_1) ; intros h h_ub ; simpl ; unfold C_dist, Cminus ; rewrite v_eq, Cmult_0_r, Cadd_0_r, Cadd_opp_r, Cnorm_C0 ; assumption. destruct f_diff as (l, f_diff) ; destruct (Ceq_dec l C0) as [l_eq | l_neq]. assert (eps_2_pos : eps / 2 > 0) by lra ; destruct (f_diff v_neq (eps / 2)%R eps_2_pos) as ([alpha alpha_pos], Halpha). assert (delta_pos : 0 < Rmin (/ (2 * Cnorm v)) alpha). apply Rmin_pos. rewrite Rinv_mult. apply Rlt_mult_inv_pos ; [lra | apply Cnorm_pos_lt ; assumption]. assumption. exists (mkposreal (Rmin (/(2 * Cnorm v)) alpha) delta_pos). intros h h_ub ; simpl ; unfold C_dist ; destruct (Ceq_dec h 0) as [h_eq | h_neq]. rewrite h_eq, Cmult_0_l, Cadd_0_r, Cminus_diag_eq ; [| reflexivity] ; rewrite Cnorm_C0 ; assumption. apply Rlt_trans with (Cnorm (h * v) *eps)%R. apply Rle_lt_trans with (Cnorm (f (x + h * v)%C - f x) * (/ Cnorm (h * v) * Cnorm (h * v)))%R. right ; field ; apply Rgt_not_eq ; apply Cnorm_pos_lt ; apply Cmult_integral_contrapositive_currified ; assumption. unfold Rdiv ; rewrite <- Rmult_assoc ; rewrite <- Cnorm_inv, <- Cnorm_Cmult. rewrite Rmult_comm ; apply Rmult_lt_compat_l. apply Cnorm_pos_lt ; apply Cmult_integral_contrapositive_currified ; assumption. replace ((f (x + h * v) - f x) * / (h * v)) with ((f (x + h * v) - f x) / (h *v) - l). apply Rlt_trans with (eps / 2)%R. apply Halpha. intro Hf ; apply h_neq ; rewrite Hf ; intuition. subst ; apply Rlt_le_trans with (Rmin (/(2* Cnorm v)) alpha) ; [apply h_ub | apply Rmin_r]. lra. rewrite l_eq ; field ; split ; assumption. apply Cmult_integral_contrapositive_currified ; assumption. rewrite Cnorm_Cmult. apply Rlt_trans with ((Rmin (/(2 * Cnorm v)) alpha) * Cnorm v * eps)%R. repeat apply Rmult_lt_compat_r ; [| apply Cnorm_pos_lt | rewrite Cnorm_IRC_Rabs] ; assumption. apply Rle_lt_trans with (eps / 2)%R. unfold Rdiv ; rewrite Rmult_comm ; apply Rmult_le_compat_l ; intuition (auto with real) ; apply Rle_trans with (/(2*Cnorm v) * Cnorm v)%R. apply Rmult_le_compat_r ; [apply Cnorm_pos | apply Rmin_l]. right ; field. apply Rgt_not_eq ; apply Cnorm_pos_lt ; assumption. lra. assert (eps_2_pos : eps / 2 > 0) by lra ; destruct (f_diff v_neq (eps / 2)%R eps_2_pos) as ([alpha alpha_pos], Halpha). pose (delta1 := Rmin (eps / (2 * Cnorm l)) (Rmin (1/2) alpha)). assert (delta1_pos : 0 < delta1). unfold delta1 ; repeat apply Rmin_pos. apply Rlt_mult_inv_pos ; [| apply Rmult_lt_0_compat] ; [| lra | apply Cnorm_pos_lt] ; assumption. lra. assumption. pose (delta := Rmin (delta1 / Cnorm v)%R delta1). assert (delta_pos : 0 < delta). unfold delta ; apply Rmin_pos. unfold Rdiv ; apply Rlt_mult_inv_pos ; [| apply Cnorm_pos_lt] ; assumption. assumption. exists (mkposreal delta delta_pos) ; intros h h_ub ; simpl ; unfold C_dist, Cminus. destruct (Ceq_dec h 0) as [h_eq | h_neq]. rewrite h_eq, Cmult_0_l, Cadd_0_r, Cadd_opp_r, Cnorm_C0 ; assumption. apply Rlt_trans with (Cnorm (h * v) * eps + Cnorm (h * v) * Cnorm l )%R. apply Rle_lt_trans with (Cnorm (f (x + h * v)%C - f x) * (/ Cnorm (h * v) * Cnorm (h * v)))%R. right ; rewrite Rinv_l, Rmult_1_r ; [reflexivity |]. apply Cnorm_no_R0 ; apply Cmult_integral_contrapositive_currified ; assumption. unfold Rdiv ; rewrite <- Rmult_assoc ; rewrite <- Cnorm_inv, <- Cnorm_Cmult. apply Rle_lt_trans with ((Cnorm ((f (x + h * v)%C - f x) * / (h * v)) + (- Cnorm l + Cnorm l)) * Cnorm (h*v))%R. right ; field. repeat rewrite Rmult_plus_distr_r. replace (Cnorm l * Cnorm (h * v))%R with (Cnorm (h *v) * Cnorm l)%R by (apply Rmult_comm). rewrite <- Rplus_assoc ; apply Rplus_lt_compat_r. apply Rle_lt_trans with (Cnorm ((f (x +h * v)%C - f x) / (h * v) - l)* Cnorm (h * v))%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 ; apply Cmult_integral_contrapositive_currified ; assumption. apply Rlt_trans with (eps /2)%R ; [apply Halpha | lra]. intro Hf ; apply h_neq ; rewrite Hf ; intuition. apply Rlt_le_trans with delta ; [apply h_ub |]. apply Rle_trans with delta1 ; [apply Rmin_r |]. apply Rle_trans with (Rmin (1/2) alpha) ; apply Rmin_r. apply Cmult_integral_contrapositive_currified ; assumption. apply Rlt_trans with (eps / 2 + Cnorm (h*v) * Cnorm l)%R. apply Rplus_lt_compat_r. unfold Rdiv ; rewrite Rmult_comm ; apply Rmult_lt_compat_l ; [assumption |]. apply Rlt_le_trans with delta1. unfold delta1. apply Rlt_le_trans with (delta * Cnorm v)%R. rewrite Cnorm_Cmult ; apply Rmult_lt_compat_r ; [apply Cnorm_pos_lt ; assumption |] ; rewrite Cnorm_IRC_Rabs ; assumption. apply Rle_trans with (delta1 / Cnorm v * Cnorm v)%R. apply Rmult_le_compat_r ; [apply Cnorm_pos | apply Rmin_l]. unfold Rdiv ; rewrite Rmult_assoc, Rinv_l, Rmult_1_r. right ; reflexivity. apply Cnorm_no_R0 ; 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. apply Rlt_le_trans with (Rmin (eps / (2 * Cnorm l)) (Rmin (1 / 2) alpha)). apply Rlt_le_trans with (delta * Cnorm v)%R. rewrite Cnorm_Cmult ; apply Rmult_lt_compat_r ; [apply Cnorm_pos_lt ; assumption |] ; rewrite Cnorm_IRC_Rabs ; assumption. apply Rle_trans with (delta1 / Cnorm v * Cnorm v)%R. apply Rmult_le_compat_r ; [apply Cnorm_pos | apply Rmin_l]. unfold Rdiv ; rewrite Rmult_assoc, Rinv_l, Rmult_1_r. right ; reflexivity. apply Cnorm_no_R0 ; assumption. apply Rmin_l. Qed.
imports: Cprop_base Cnorm Ctacfield Canalysis_def