# Inverse function theorem - the easy half #

In this file we prove that g' (f x) = (f' x)โปยน provided that f is strictly differentiable at x, f' x โ  0, and g is a local left inverse of f that is continuous at f x. This is the easy half of the inverse function theorem: the harder half states that g exists.

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of Analysis/Calculus/Deriv/Basic.

## Keywords #

derivative, inverse function

theorem HasStrictDerivAt.hasStrictFDerivAt_equiv {๐ : Type u} [] {f : ๐ โ ๐} {f' : ๐} {x : ๐} (hf : HasStrictDerivAt f f' x) (hf' : f' โ  0) :
HasStrictFDerivAt f (โ( (Units.mk0 f' hf'))) x
theorem HasDerivAt.hasFDerivAt_equiv {๐ : Type u} [] {f : ๐ โ ๐} {f' : ๐} {x : ๐} (hf : HasDerivAt f f' x) (hf' : f' โ  0) :
HasFDerivAt f (โ( (Units.mk0 f' hf'))) x
theorem HasStrictDerivAt.of_local_left_inverse {๐ : Type u} [] {f : ๐ โ ๐} {g : ๐ โ ๐} {f' : ๐} {a : ๐} (hg : ) (hf : HasStrictDerivAt f f' (g a)) (hf' : f' โ  0) (hfg : โแถ  (y : ๐) in nhds a, f (g y) = y) :

If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an invertible derivative f' at g a in the strict sense, then g has the derivative f'โปยน at a in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem PartialHomeomorph.hasStrictDerivAt_symm {๐ : Type u} [] (f : PartialHomeomorph ๐ ๐) {a : ๐} {f' : ๐} (ha : a โ f.target) (hf' : f' โ  0) (htff' : HasStrictDerivAt (โf) f' (โf.symm a)) :
HasStrictDerivAt (โf.symm) f'โปยน a

If f is a partial homeomorphism defined on a neighbourhood of f.symm a, and f has a nonzero derivative f' at f.symm a in the strict sense, then f.symm has the derivative f'โปยน at a in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem HasDerivAt.of_local_left_inverse {๐ : Type u} [] {f : ๐ โ ๐} {g : ๐ โ ๐} {f' : ๐} {a : ๐} (hg : ) (hf : HasDerivAt f f' (g a)) (hf' : f' โ  0) (hfg : โแถ  (y : ๐) in nhds a, f (g y) = y) :

If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an invertible derivative f' at g a, then g has the derivative f'โปยน at a.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem PartialHomeomorph.hasDerivAt_symm {๐ : Type u} [] (f : PartialHomeomorph ๐ ๐) {a : ๐} {f' : ๐} (ha : a โ f.target) (hf' : f' โ  0) (htff' : HasDerivAt (โf) f' (โf.symm a)) :
HasDerivAt (โf.symm) f'โปยน a

If f is a partial homeomorphism defined on a neighbourhood of f.symm a, and f has a nonzero derivative f' at f.symm a, then f.symm has the derivative f'โปยน at a.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem HasDerivAt.eventually_ne {๐ : Type u} [] {F : Type v} [NormedSpace ๐ F] {f : ๐ โ F} {f' : F} {x : ๐} (h : HasDerivAt f f' x) (hf' : f' โ  0) :
โแถ  (z : ๐) in nhdsWithin x {x}แถ, f z โ  f x
theorem HasDerivAt.tendsto_punctured_nhds {๐ : Type u} [] {F : Type v} [NormedSpace ๐ F] {f : ๐ โ F} {f' : F} {x : ๐} (h : HasDerivAt f f' x) (hf' : f' โ  0) :
theorem not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero {๐ : Type u} [] {f : ๐ โ ๐} {g : ๐ โ ๐} {a : ๐} {s : Set ๐} {t : Set ๐} (ha : a โ s) (hsu : UniqueDiffWithinAt ๐ s a) (hf : HasDerivWithinAt f 0 t (g a)) (hst : Set.MapsTo g s t) (hfg : f โ g =แถ [] id) :
theorem not_differentiableAt_of_local_left_inverse_hasDerivAt_zero {๐ : Type u} [] {f : ๐ โ ๐} {g : ๐ โ ๐} {a : ๐} (hf : HasDerivAt f 0 (g a)) (hfg : f โ g =แถ [nhds a] id) :