proposition: Fact der_inv f (x v : V) : f x != 0 -> derivable f x v -> (fun h => h^-1 *: (((fun y => (f y)^-1) \o shift x) (h *: v) - (f x)^-1)) @ (0 : R)^' --> - (f x) ^-2 *: 'D_v f x.
proof: Proof. move=> fxn0 df. have /derivable1P/derivable1_diffP/differentiable_continuous := df. move=> /continuous_withinNx; rewrite scale0r add0r => fc. have fn0 : (0 : R)^' [set h | f (h *: v + x) != 0]. apply: (fc [set x | x != 0]); exists `|f x|; first by rewrite /= normr_gt0. move=> y; rewrite /= => yltfx. by apply/eqP => y0; move: yltfx; rewrite y0 subr0 ltxx. have : (fun h => - ((f x)^-1 * (f (h *: v + x))^-1) *: (h^-1 *: (f (h *: v + x) - f x))) @ (0 : R)^' --> - (f x) ^- 2 *: 'D_v f x. by apply: cvgM => //; apply: cvgN; rewrite expr2 invfM; apply: cvgM; [exact: cvg_cst| exact: cvgV]. apply: cvg_trans => A [_/posnumP[e] /= Ae]. move: fn0; apply: filter_app; near=> h => /= fhvxn0. have he : ball 0 e%:num (h : R) by near: h; exists e%:num => /=. have hn0 : h != 0 by near: h; exists e%:num => /=. suff <- : - ((f x)^-1 * (f (h *: v + x))^-1) *: (h^-1 *: (f (h *: v + x) - f x)) = h^-1 *: ((f (h *: v + x))^-1 - (f x)^-1) by exact: Ae. rewrite scalerA mulrC -scalerA; congr (_ *: _). apply/eqP; rewrite scaleNr eqr_oppLR opprB scalerBr. rewrite -scalerA [_ *: f _]mulVf // [_%:A]mulr1. by rewrite mulrC -scalerA [_ *: f _]mulVf // [_%:A]mulr1. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms