# mathlib3documentation

analysis.calculus.deriv.inverse

# Inverse function theorem - the easy half #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 has_strict_deriv_at.has_strict_fderiv_at_equiv {𝕜 : Type u} {f : 𝕜 𝕜} {f' x : 𝕜} (hf : x) (hf' : f' 0) :
(units.mk0 f' hf')) x
theorem has_deriv_at.has_fderiv_at_equiv {𝕜 : Type u} {f : 𝕜 𝕜} {f' x : 𝕜} (hf : f' x) (hf' : f' 0) :
(units.mk0 f' hf')) x
theorem has_strict_deriv_at.of_local_left_inverse {𝕜 : Type u} {f g : 𝕜 𝕜} {f' a : 𝕜} (hg : a) (hf : (g a)) (hf' : f' 0) (hfg : ∀ᶠ (y : 𝕜) in nhds a, f (g y) = y) :
a

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 local_homeomorph.has_strict_deriv_at_symm {𝕜 : Type u} (f : 𝕜) {a f' : 𝕜} (ha : a f.to_local_equiv.target) (hf' : f' 0) (htff' : ((f.symm) a)) :
f'⁻¹ a

If f is a local 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 has_deriv_at.of_local_left_inverse {𝕜 : Type u} {f g : 𝕜 𝕜} {f' a : 𝕜} (hg : a) (hf : f' (g a)) (hf' : f' 0) (hfg : ∀ᶠ (y : 𝕜) in nhds a, f (g y) = y) :
f'⁻¹ a

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 local_homeomorph.has_deriv_at_symm {𝕜 : Type u} (f : 𝕜) {a f' : 𝕜} (ha : a f.to_local_equiv.target) (hf' : f' 0) (htff' : f' ((f.symm) a)) :
f'⁻¹ a

If f is a local homeomorphism defined on a neighbourhood of f.symm a, and f has an 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 has_deriv_at.eventually_ne {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} (h : f' x) (hf' : f' 0) :
∀ᶠ (z : 𝕜) in {x}, f z f x
theorem has_deriv_at.tendsto_punctured_nhds {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} (h : f' x) (hf' : f' 0) :
{x}) (nhds_within (f x) {f x})
theorem not_differentiable_within_at_of_local_left_inverse_has_deriv_within_at_zero {𝕜 : Type u} {f g : 𝕜 𝕜} {a : 𝕜} {s t : set 𝕜} (ha : a s) (hsu : a) (hf : t (g a)) (hst : s t) (hfg : f g =ᶠ[ s] id) :
¬ a
theorem not_differentiable_at_of_local_left_inverse_has_deriv_at_zero {𝕜 : Type u} {f g : 𝕜 𝕜} {a : 𝕜} (hf : 0 (g a)) (hfg : f g =ᶠ[nhds a] id) :
¬ a