proposition: Theorem fully_differentiable_pt_not_derivable_pt : (forall f x, fully_differentiable_pt f x -> derivable_pt f x) -> False.
proof: Proof. intro H. assert (Main : forall (x y : R), differentiable_pt_abs (fun z1 => (Cre z1 * Cre z1 + Cim z1 * Cim z1)%R) 1 (x +i y) (2 * x / (x +i y))). intros x y v_neq eps eps_pos. pose (delta := (eps / Cnorm (x +i y))%R) ; assert (delta_pos : 0 < delta). unfold Rdiv ; apply Rlt_mult_inv_pos ; [| apply Cnorm_pos_lt] ; assumption. exists (mkposreal delta delta_pos) ; intros h h_neq h_bd ; simpl. repeat rewrite Rmult_0_l ; repeat rewrite Rminus_0_r ; repeat rewrite Rplus_0_r ; repeat rewrite Rplus_0_l. apply Rle_lt_trans with (Cnorm (h * (h * (x ^ 2) + h * (y ^ 2) + 2 * x)%R / (h * (x, y)) - 2 * x / (x, y))). right ; apply Cnorm_eq_compat. unfold Cminus ; apply Cadd_eq_compat_r ; apply Cmult_eq_compat_r. rewrite Rmult_plus_distr_l ; repeat rewrite Rmult_plus_distr_r. repeat rewrite Rmult_1_r ; repeat rewrite Rmult_1_l. apply (proj1 (Ceq _ _)) ; split ; simpl ; ring. apply Rle_lt_trans with (Cnorm ((h * x ^ 2 + h * y ^ 2 + 2 * x)%R / (x, y) - 2 * x / (x, y))). right ; apply Cnorm_eq_compat. apply Cadd_eq_compat_r. rewrite Cmult_comm ; unfold Cdiv ; repeat rewrite Cmult_assoc ; apply Cmult_eq_compat_l ; field ; split ; [| apply IRC_neq_compat] ; assumption. apply Rle_lt_trans with (Cnorm ((h * x ^ 2 + h * y ^ 2)%R / (x, y))). right ; apply Cnorm_eq_compat ; apply (proj1 (Ceq _ _)) ; split ; simpl ; ring. rewrite <- Rmult_plus_distr_l ; unfold Cdiv ; rewrite Cmult_IRC_Rmult ; repeat rewrite Cnorm_Cmult. apply Rlt_le_trans with (eps * Cnorm_sqr (x, y) * (/ Cnorm (x, y)) ^ 2)%R. simpl ; repeat rewrite Rmult_1_r ; rewrite <- Rmult_assoc, Cnorm_inv. apply Rmult_lt_compat_r. apply Rinv_0_lt_compat ; apply Cnorm_pos_lt ; assumption. replace (Cnorm_sqr (x, y))%R with (Cnorm (x * x + y * y)%R). apply Rlt_le_trans with (eps * / Cnorm (x, y)* Cnorm (x * x + y * y)%R)%R. apply Rmult_lt_compat_r. apply Cnorm_pos_lt ; intro Hf ; apply v_neq. apply HC0_norm_R0. unfold Cnorm_sqr ; simpl. destruct (proj2 (Ceq _ _) Hf) as [Hf' _] ; apply Hf'. rewrite Cnorm_IRC_Rabs ; apply h_bd. right ; field. apply Cnorm_no_R0 ; assumption. unfold Cnorm_sqr ; rewrite Cnorm_IRC_Rabs, Rabs_right ; [reflexivity |]. apply Rle_ge ; apply Cnorm_sqr_pos. assumption. right ; rewrite <- Rmult_1_r, Rmult_assoc ; apply Rmult_eq_compat_l. unfold Cnorm, Cnorm_sqr. simpl. rewrite Rmult_1_r, <- Rinv_mult_distr, sqrt_sqrt, Rinv_r. reflexivity. apply Rgt_not_eq. apply Cnorm_sqr_pos_lt ; assumption. apply Cnorm_sqr_pos. apply Rgt_not_eq ; apply sqrt_lt_R0 ; apply Cnorm_sqr_pos_lt ; assumption. apply Rgt_not_eq ; apply sqrt_lt_R0 ; apply Cnorm_sqr_pos_lt ; assumption. assert (Main2 : fully_differentiable_pt Cnorm_sqr 1). intros v ; unfold Cnorm_sqr ; destruct v as [x y] ; exists (2 * x / (x, y)) ; apply Main. assert (Main3 : derivable_pt Cnorm_sqr C1 -> False). intros [l Hl]. assert (H1 := derivable_differentiable_pt_abs Cnorm_sqr 1 l Hl (0,1)%R). assert (H1' := Main R0 R1). assert (H2 := derivable_differentiable_pt_abs Cnorm_sqr 1 l Hl (1,0)%R). assert (H2' := Main R1 R0). unfold differentiable_pt_abs in *. assert (H1_neq : (R0, R1) <> C0). apply HintC0_neq_R0_neq ; right ; simpl ; apply Rgt_not_eq ; apply Rlt_0_1. assert (H2_neq : (R1, R0) <> C0). apply HintC0_neq_R0_neq ; left ; simpl ; apply Rgt_not_eq ; apply Rlt_0_1. assert (Hf1 := Canalysis_diff.uniqueness_limite _ _ _ _ _ H1_neq H1 H1'). assert (Hf2 := Canalysis_diff.uniqueness_limite _ _ _ _ _ H2_neq H2 H2'). subst. unfold Cdiv in Hf2 ; repeat rewrite Cmult_assoc in Hf2. assert (Hneq : IRC 2 <> IRC 0) by (apply IRC_neq_compat ; apply Rgt_not_eq ; lra) ; assert (T := Cmult_eq_reg_l _ _ _ Hneq Hf2). clear -T H1_neq H2_neq. do 2 rewrite Cinv_rew in T. destruct (proj2 (Ceq _ _) T) as [H _] ; clear T. simpl in H ; ring_simplify in H. repeat rewrite Rmult_0_l in H ; repeat rewrite Rmult_1_l in H ; rewrite Rplus_0_r, Rinv_1 in H. lra. assumption. assumption. assumption. apply Main3 ; apply H ; apply Main2. 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