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 OpenPartialHomeomorph.hasStrictDerivAt_symm {𝕜 : Type u} [NontriviallyNormedField 𝕜] (f : OpenPartialHomeomorph 𝕜 𝕜) {a f' : 𝕜} (ha : a ∈ f.target) (hf' : f' ≠ 0) (htff' : HasStrictDerivAt (↑f) f' (↑f.symm a)) : HasStrictDerivAt (↑f.symm) f'⁻¹ a

If f is an open 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 OpenPartialHomeomorph.hasDerivAt_symm {𝕜 : Type u} [NontriviallyNormedField 𝕜] (f : OpenPartialHomeomorph 𝕜 𝕜) {a f' : 𝕜} (ha : a ∈ f.target) (hf' : f' ≠ 0) (htff' : HasDerivAt (↑f) f' (↑f.symm a)) : HasDerivAt (↑f.symm) f'⁻¹ a

If f is an open 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 HasDerivWithinAt.tendsto_nhdsWithin_nhdsNE {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {s : Set 𝕜} {x : 𝕜} (h : HasDerivWithinAt f f' s x) (hf' : f' ≠ 0) : Filter.Tendsto f (nhdsWithin x (s \ {x})) (nhdsWithin (f x) {f x}ᶜ)

theorem HasDerivWithinAt.eventually_ne {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {s : Set 𝕜} {x : 𝕜} {c : F} (h : HasDerivWithinAt f f' s x) (hf' : f' ≠ 0) : ∀ᶠ (z : 𝕜) in nhdsWithin x (s \ {x}), f z ≠ c

theorem HasDerivWithinAt.eventually_notMem {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {s : Set 𝕜} {x : 𝕜} (h : HasDerivWithinAt f f' s x) (hf' : f' ≠ 0) (t : Set F) (ht : ¬AccPt (f x) (Filter.principal t)) : ∀ᶠ (z : 𝕜) in nhdsWithin x (s \ {x}), f z ∉ t

theorem HasDerivAt.tendsto_nhdsNE {𝕜 : 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 HasDerivAt.eventually_ne {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {c : F} (h : HasDerivAt f f' x) (hf' : f' ≠ 0) : ∀ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z ≠ c

theorem HasDerivAt.eventually_notMem {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (h : HasDerivAt f f' x) (hf' : f' ≠ 0) (t : Set F) (ht : ¬AccPt (f x) (Filter.principal t)) : ∀ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z ∉ t

theorem derivWithin_zero_of_frequently_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} {c : F} (h : ∃ᶠ (y : 𝕜) in nhdsWithin x (s \ {x}), f y = c) : derivWithin f s x = 0

If a function is equal to a constant at a set of points that accumulates to x in s, then its derivative within s at x equals zero, either because it has derivative zero or because it isn't differentiable at this point.

theorem derivWithin_zero_of_frequently_mem {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} (t : Set F) (ht : ¬AccPt (f x) (Filter.principal t)) (h : ∃ᶠ (y : 𝕜) in nhdsWithin x (s \ {x}), f y ∈ t) : derivWithin f s x = 0

If a function frequently (in 𝓝[s ∖ {x}] x) takes values in a set t that does not accumulate at f x, then its derivative within s at x equals zero, either because it has derivative zero or because it isn't differentiable at this point.

theorem deriv_zero_of_frequently_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {c : F} (h : ∃ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, f y = c) : deriv f x = 0

If a function is equal to a constant at a set of points that accumulates to x, then its derivative at x equals zero, either because it has derivative zero or because it isn't differentiable at this point.

theorem deriv_zero_of_frequently_mem {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} (t : Set F) (ht : ¬AccPt (f x) (Filter.principal t)) (h : ∃ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, f y ∈ t) : deriv f x = 0

If a function frequently (in 𝓝[≠] x) takes values in a set t that does not accumulate at f x, then its derivative at x equals zero, either because it has derivative zero or because it isn't differentiable at this point.

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