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 HasStrictDerivAt.toLocalHomeomorph that repacks a function f with a hf : HasStrictFDerivAt f f' a, f' : E ≃L[𝕜] F, into a LocalHomeomorph. The toFun of this LocalHomeomorph is defeq to f, so one can apply theorems about LocalHomeomorph to hf.toLocalHomeomorph f, and get statements about f.

Then we define HasStrictFDerivAt.localInverse to be the invFun of this LocalHomeomorph, 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.

In the one-dimensional case we reformulate these theorems in terms of HasStrictDerivAt and f'⁻¹.

We also reformulate the theorems in terms of ContDiff, to give that C^k (respectively, smooth) inputs give C^k (smooth) inverses. These versions require that continuous differentiability implies strict differentiability; this is false over a general field, true over ℝ or ℂ and implemented here assuming IsROrC 𝕂.

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.

Notations #

In the section about ApproximatesLinearOn we introduce some local notation to make formulas shorter:

by N we denote ‖f'⁻¹‖;
by g we denote the auxiliary contracting map x ↦ x + f'.symm (y - f x) used to prove that {x | f x = y} is nonempty.

Tags #

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

Non-linear maps close to affine maps #

In this section we study a map f such that ‖f x - f y - f' (x - y)‖ ≤ c * ‖x - y‖ on an open set s, where f' : E →L[𝕜] F is a continuous linear map and c is suitably small. Maps of this type behave like f a + f' (x - a) near each a ∈ s.

When f' is onto, we show that f is locally onto.

When f' is a continuous linear equiv, we show that f is a homeomorphism between s and f '' s. More precisely, we define ApproximatesLinearOn.toLocalHomeomorph to be a LocalHomeomorph with toFun = f, source = s, and target = f '' s.

Maps of this type naturally appear in the proof of the inverse function theorem (see next section), and ApproximatesLinearOn.toLocalHomeomorph will imply that the locally inverse function exists.

We define this auxiliary notion to split the proof of the inverse function theorem into small lemmas. This approach makes it possible

to prove a lower estimate on the size of the domain of the inverse function;
to reuse parts of the proofs in the case if a function is not strictly differentiable. E.g., for a function f : E × F → G with estimates on f x y₁ - f x y₂ but not on f x₁ y - f x₂ y.

Inverse function theorem #

Notations #

Tags #

Non-linear maps close to affine maps #

Inverse function theorem #

Inverse function theorem, 1D case #

Inverse function theorem, smooth case #