Inverse function theorem

In this file we prove the inverse function theorem. It says that if a map f : E → F has an invertible strict derivative f' at a, then it is locally invertible, and the inverse function has derivative f' ⁻¹.

We define HasStrictFDerivAt.toPartialHomeomorph that repacks a function f with a hf : HasStrictFDerivAt f f' a, f' : E ≃L[𝕜] F, into a PartialHomeomorph. The toFun of this PartialHomeomorph is defeq to f, so one can apply theorems about PartialHomeomorph to hf.toPartialHomeomorph f, and get statements about f.

Then we define HasStrictFDerivAt.localInverse to be the invFun of this PartialHomeomorph, and prove two versions of the inverse function theorem:

• HasStrictFDerivAt.to_localInverse: if f has an invertible derivative f' at a in the strict sense (hf), then hf.localInverse f f' a has derivative f'.symm at f a in the strict sense;

• HasStrictFDerivAt.to_local_left_inverse: if f has an invertible derivative f' at a in the strict sense and g is locally left inverse to f near a, then g has derivative f'.symm at f a in the strict sense.

Some related theorems, providing the derivative and higher regularity assuming that we already know the inverse function, are formulated in the Analysis/Calculus/FDeriv and Analysis/Calculus/Deriv folders, and in ContDiff.lean.

Tags

derivative, strictly differentiable, continuously differentiable, smooth, inverse function

Inverse function theorem

Let f : E → F be a map defined on a complete vector space E. Assume that f has an invertible derivative f' : E ≃L[𝕜] F at a : E in the strict sense. Then f approximates f' in the sense of ApproximatesLinearOn on an open neighborhood of a, and we can apply ApproximatesLinearOn.toPartialHomeomorph to construct the inverse function.

theorem HasStrictFDerivAt.approximates_deriv_on_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) {c : NNReal} (hc : Subsingleton E ∨ 0 < c) : ∃ s ∈ nhds a, ApproximatesLinearOn f f' s c

If f has derivative f' at a in the strict sense and c > 0, then f approximates f' with constant c on some neighborhood of a.

theorem HasStrictFDerivAt.map_nhds_eq_of_surj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (h : LinearMap.range f' = ⊤) : Filter.map f (nhds a) = nhds (f a)

theorem HasStrictFDerivAt.approximates_deriv_on_open_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) : ∃ (s : Set E), a ∈ s ∧ IsOpen s ∧ ApproximatesLinearOn f (↑f') s (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ / 2)

def HasStrictFDerivAt.toPartialHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] (f : E → F) {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) : PartialHomeomorph E F

Given a function with an invertible strict derivative at a, returns a PartialHomeomorph with to_fun = f and a ∈ source. This is a part of the inverse function theorem. The other part HasStrictFDerivAt.to_localInverse states that the inverse function of this PartialHomeomorph has derivative f'.symm.

Equations

• HasStrictFDerivAt.toPartialHomeomorph f hf = ApproximatesLinearOn.toPartialHomeomorph f (Classical.choose ⋯) ⋯ ⋯ ⋯

@[simp]

theorem HasStrictFDerivAt.toPartialHomeomorph_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) : ↑(HasStrictFDerivAt.toPartialHomeomorph f hf) = f

theorem HasStrictFDerivAt.mem_toPartialHomeomorph_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) : a ∈ (HasStrictFDerivAt.toPartialHomeomorph f hf).source

theorem HasStrictFDerivAt.image_mem_toPartialHomeomorph_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) : f a ∈ (HasStrictFDerivAt.toPartialHomeomorph f hf).target

theorem HasStrictFDerivAt.map_nhds_eq_of_equiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) : Filter.map f (nhds a) = nhds (f a)

def HasStrictFDerivAt.localInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] (f : E → F) (f' : E ≃L[𝕜] F) (a : E) (hf : HasStrictFDerivAt f (↑f') a) : F → E

Given a function f with an invertible derivative, returns a function that is locally inverse to f.

Equations

• HasStrictFDerivAt.localInverse f f' a hf = ↑(PartialHomeomorph.symm (HasStrictFDerivAt.toPartialHomeomorph f hf))

theorem HasStrictFDerivAt.localInverse_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) : HasStrictFDerivAt.localInverse f f' a hf = ↑(PartialHomeomorph.symm (HasStrictFDerivAt.toPartialHomeomorph f hf))

theorem HasStrictFDerivAt.eventually_left_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) : ∀ᶠ (x : E) in nhds a, HasStrictFDerivAt.localInverse f f' a hf (f x) = x

@[simp]

theorem HasStrictFDerivAt.localInverse_apply_image {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) : HasStrictFDerivAt.localInverse f f' a hf (f a) = a

theorem HasStrictFDerivAt.eventually_right_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) : ∀ᶠ (y : F) in nhds (f a), f (HasStrictFDerivAt.localInverse f f' a hf y) = y

theorem HasStrictFDerivAt.localInverse_continuousAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) : ContinuousAt (HasStrictFDerivAt.localInverse f f' a hf) (f a)

theorem HasStrictFDerivAt.localInverse_tendsto {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) : Filter.Tendsto (HasStrictFDerivAt.localInverse f f' a hf) (nhds (f a)) (nhds a)

theorem HasStrictFDerivAt.localInverse_unique {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) {g : F → E} (hg : ∀ᶠ (x : E) in nhds a, g (f x) = x) : ∀ᶠ (y : F) in nhds (f a), g y = HasStrictFDerivAt.localInverse f f' a hf y

theorem HasStrictFDerivAt.to_localInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) : HasStrictFDerivAt (HasStrictFDerivAt.localInverse f f' a hf) (↑(ContinuousLinearEquiv.symm f')) (f a)

If f has an invertible derivative f' at a in the sense of strict differentiability (hf), then the inverse function hf.localInverse f has derivative f'.symm at f a.

theorem HasStrictFDerivAt.to_local_left_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑f') a) {g : F → E} (hg : ∀ᶠ (x : E) in nhds a, g (f x) = x) : HasStrictFDerivAt g (↑(ContinuousLinearEquiv.symm f')) (f a)

If f : E → F has an invertible derivative f' at a in the sense of strict differentiability and g (f x) = x in a neighborhood of a, then g has derivative f'.symm at f a.

For a version assuming f (g y) = y and continuity of g at f a but not [CompleteSpace E] see of_local_left_inverse.

theorem isOpenMap_of_hasStrictFDerivAt_equiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E → E ≃L[𝕜] F} (hf : ∀ (x : E), HasStrictFDerivAt f (↑(f' x)) x) : IsOpenMap f

If a function has an invertible strict derivative at all points, then it is an open map.

@[deprecated isOpenMap_of_hasStrictFDerivAt_equiv]

theorem open_map_of_strict_fderiv_equiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E → E ≃L[𝕜] F} (hf : ∀ (x : E), HasStrictFDerivAt f (↑(f' x)) x) : IsOpenMap f

Alias of isOpenMap_of_hasStrictFDerivAt_equiv.

---

If a function has an invertible strict derivative at all points, then it is an open map.