proposition: Lemma is_derive1_caratheodory (f : R -> R) (x a : R) : is_derive x 1 f a <-> exists g, [/\ forall z, f z - f x = g z * (z - x), {for x, continuous g} & g x = a].
proof: Proof. split => [Hd|[g [fxE Cg gxE]]]. exists (fun z => if z == x then a else (f(z) - f(x)) / (z - x)); split. - move=> z; case: eqP => [->|/eqP]; first by rewrite !subrr mulr0. by rewrite -subr_eq0 => /divfK->. - apply/continuous_withinNshiftx; rewrite eqxx /=. pose g1 h := (h^-1 *: ((f \o shift x) h%:A - f x)). have F1 : g1 @ 0^' --> a by case: Hd => H1 <-. apply: cvg_trans F1; apply: near_eq_cvg; rewrite /g1 !fctE. near=> i. rewrite ifN; first by rewrite addrK mulrC /= [_%:A]mulr1. rewrite -subr_eq0 addrK. by near: i; rewrite near_withinE /= near_simpl; near=> x1. by rewrite eqxx. suff Hf : h^-1 *: ((f \o shift x) h%:A - f x) @[h --> 0^'] --> a. have F1 : 'D_1 f x = a by apply: cvg_lim. rewrite -F1 in Hf. by constructor. have F1 : (g \o shift x) y @[y --> 0^'] --> a. by rewrite -gxE; apply/continuous_withinNshiftx. apply: cvg_trans F1; apply: near_eq_cvg. near=> y. rewrite /= fxE /= addrK [_%:A]mulr1. suff yNZ : y != 0 by rewrite [RHS]mulrC mulfK. by near: y; rewrite near_withinE /= near_simpl; near=> x1. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)