proposition: Lemma is_derive_inverse (f g : R -> R) l x : {near x, cancel f g} -> {near x, continuous f} -> is_derive x 1 f l -> l != 0 -> is_derive (f x) 1 g l^-1.
proof: Proof. move=> fgK fC fD lNZ. have /is_derive1_caratheodory [h [fE hC hxE]] := fD. have gfxE : g (f x) = x by have [d Hd]:= nbhs_ex fgK; apply: Hd. pose g1 y := if y == f x then (h (g y))^-1 else (g y - g (f x)) / (y - f x). apply/is_derive1_caratheodory. exists g1; split; first 2 last. - by rewrite /g1 eqxx gfxE hxE. - move=> z; rewrite /g1; case: eqP => [->|/eqP]; first by rewrite !subrr mulr0. by rewrite -subr_eq0 => /divfK. have F1 : (h (g x))^-1 @[x --> f x] --> g1 (f x). rewrite /g1 eqxx; apply: continuousV; first by rewrite /= gfxE hxE. apply: continuous_comp; last by rewrite gfxE. by apply: nbhs_singleton (near_can_continuous _ _). apply: cvg_sub0 F1. apply/cvgrPdist_lt => eps eps_gt0 /=; rewrite !near_simpl /=. near=> y; rewrite sub0r normrN !fctE. have fgyE : f (g y) = y by near: y; apply: near_continuous_can_sym. rewrite /g1; case: eqP => [_|/eqP x1Dfx]; first by rewrite subrr normr0. have -> : y - f x = h (g y) * (g y - x) by rewrite -fE fgyE. rewrite gfxE invfM mulrC divfK ?subrr ?normr0 // subr_eq0. by apply: contra x1Dfx => /eqP<-; apply/eqP. 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)