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} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {f' x : 𝕜} (hf : HasStrictDerivAt f f' x) (hf' : f' ≠ 0) : HasStrictFDerivAt f (↑((ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 f' hf'))) x

theorem HasDerivAt.hasFDerivAt_equiv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {f' x : 𝕜} (hf : HasDerivAt f f' x) (hf' : f' ≠ 0) : HasFDerivAt f (↑((ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 f' hf'))) x

theorem HasStrictDerivAt.of_local_left_inverse {𝕜 : Type u} [NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {f' a : 𝕜} (hg : ContinuousAt g a) (hf : HasStrictDerivAt f f' (g a)) (hf' : f' ≠ 0) (hfg : ∀ᶠ (y : 𝕜) in nhds a, f (g y) = y) : HasStrictDerivAt g 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 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} [NontriviallyNormedField 𝕜] (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} [NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {f' a : 𝕜} (hg : ContinuousAt g a) (hf : HasDerivAt f f' (g a)) (hf' : f' ≠ 0) (hfg : ∀ᶠ (y : 𝕜) in nhds a, f (g y) = y) : HasDerivAt g 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 PartialHomeomorph.hasDerivAt_symm {𝕜 : Type u} [NontriviallyNormedField 𝕜] (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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (h : HasDerivAt f f' x) (hf' : f' ≠ 0) : Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhdsWithin (f x) {f x}ᶜ)

theorem not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {a : 𝕜} {s 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 =ᶠ[nhdsWithin a s] id) : ¬DifferentiableWithinAt 𝕜 g s a

theorem not_differentiableAt_of_local_left_inverse_hasDerivAt_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {a : 𝕜} (hf : HasDerivAt f 0 (g a)) (hfg : f ∘ g =ᶠ[nhds a] id) : ¬DifferentiableAt 𝕜 g a