proposition: Theorem MVT_Cre : forall (f : C -> C) (z h : C) (f_deriv : forall (t : R), interval 0 1 t -> derivable_pt f (z + t*h)), h <> 0 -> exists u : R, exists u_in_I : interval 0 1 u, Cre ((f (z + h) - f z) / h) = Cre (derive_pt f (z + u * h) (f_deriv u u_in_I)).
proof: Proof. intros f z h f_deriv h_neq. pose (H := fun (t : R) => Cre ((f (z + t*h) - f z) / h)). assert (H0_0 : (H 0 = 0)%R). unfold H ; unfold Cminus, Cdiv ; rewrite Cmult_0_l, Cadd_0_r, Cadd_opp_r, Cmult_0_l ; reflexivity. assert (H1_d : H R1 = Cre ((f (z + h) - f z) / h)). unfold H ; rewrite Cmult_1_l ; reflexivity. assert (H_deriv : forall (t:R) (t_in : interval 0 1 t), Ranalysis_def.derivable_pt_lim_in (interval 0 1) H t (Cre (derive_pt f (z + t * h) (f_deriv t t_in)))). { intros t t_in ; destruct (f_deriv t t_in) as [f' Hf'] ; intros eps eps_pos ; destruct (Hf' _ eps_pos) as [delta Hdelta]. pose (delta' := (delta / Cnorm h)%R) ; assert (delta'_pos : 0 < delta'). unfold delta', Rdiv ; apply Rlt_mult_inv_pos ; [destruct delta | apply Cnorm_pos_lt] ; assumption. exists delta' ; split ; [assumption |]. simpl ; intros u [[u_in ut_neq] u_bd] ; replace (Ranalysis_def.growth_rate H t u) with (Cre (growth_rate f (z + t * h) (z + u * h))). + unfold R_dist ; rewrite Cre_minus_compat ; eapply Rle_lt_trans. - eapply Cre_le_Cnorm. - unfold growth_rate. replace (z + IRC u * h - (z + IRC t * h)) with (IRC (u - t) * h). replace (IRC u * h) with (IRC t * h + IRC (u - t) * h). rewrite <- Cadd_assoc ; apply Hdelta. * apply Cmult_integral_contrapositive_currified. apply IRC_neq_compat, Rminus_eq_contra ; symmetry ; assumption. assumption. * rewrite Cnorm_Cmult, Cnorm_IRC_Rabs ; apply Rlt_le_trans with (delta' * Cnorm h)%R. apply Rmult_lt_compat_r ; [apply Cnorm_pos_lt |] ; assumption. unfold delta', Rdiv ; rewrite Rmult_assoc, Rinv_l, Rmult_1_r. reflexivity. apply Rgt_not_eq, Cnorm_pos_lt ; assumption. * rewrite <- IRC_minus_compat ; ring. * rewrite <- IRC_minus_compat ; ring. + unfold growth_rate, Ranalysis_def.growth_rate, H. rewrite Cre_minus_compat, <- Cre_div_compat. rewrite <- IRC_minus_compat ; apply Cre_eq_compat ; field ; repeat split. assumption. rewrite IRC_minus_compat ; apply IRC_neq_compat, Rminus_eq_contra ; symmetry ; assumption. ring_simplify (z + IRC u * h - (z + IRC t * h)) ; rewrite Cmult_comm, <- Cmult_minus_distr_l. apply Cmult_integral_contrapositive_currified. assumption. rewrite IRC_minus_compat ; apply IRC_neq_compat, Rminus_eq_contra ; symmetry ; assumption. apply Rminus_eq_contra ; symmetry ; assumption. } assert (H_deriv2 : derivable_open_interval 0 1 H). intros a a_in ; exists (Cre (derive_pt f (z + a * h) (f_deriv a (open_interval_interval _ _ _ a_in)))). eapply derivable_pt_lim_in_contravariant, H_deriv. unfold included ; apply open_interval_interval ; assumption. assert (id_deriv : derivable_open_interval 0 1 Ranalysis1.id). apply derivable_in_id. assert (H_cont : Ranalysis_def.continuity_interval 0 1 H). apply derivable_in_continuity_in ; intros x x_in ; eexists ; apply (H_deriv _ x_in). assert (id_cont : Ranalysis_def.continuity_interval 0 1 Ranalysis1.id). apply derivable_in_continuity_in, derivable_in_id. destruct (Ranalysis_MVT.MVT H (Ranalysis1.id) 0 1 H_deriv2 id_deriv Rlt_0_1 H_cont id_cont) as [c [c_in Hc]] ; exists c ; exists (open_interval_interval _ _ _ c_in). assert (Hrew := Rminus_0_r (H R1)) ; rewrite <- H0_0 in Hrew. rewrite <- H1_d, <- Hrew ; clear Hrew. unfold Ranalysis1.id in Hc ; rewrite Rminus_0_r, Rmult_1_l in Hc. rewrite derive_open_interval_unfold with (f := fun x => x) (c_in := c_in) in Hc. rewrite derive_pt_open_interval_id, Rmult_1_r in Hc ; [| assumption]. rewrite derive_open_interval_unfold with (f := H) (c_in := c_in) in Hc. erewrite derivable_pt_lim_derive_pt_open_interval in Hc. change R0 with (IZR 0). change R1 with (IZR 1). rewrite <- Hc. reflexivity. assumption. apply derivable_pt_lim_in_contravariant with (interval 0 1), H_deriv. apply included_open_interval_interval. 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