Inverse function theorem #

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

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

Then we define has_strict_fderiv_at.local_inverse to be the inv_fun of this local_homeomorph, and prove two versions of the inverse function theorem:

• has_strict_fderiv_at.to_local_inverse: if f has an invertible derivative f' at a in the strict sense (hf), then hf.local_inverse f f' a has derivative f'.symm at f a in the strict sense;

• has_strict_fderiv_at.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 has_strict_deriv_at and f'⁻¹.

We also reformulate the theorems in terms of cont_diff, 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 is_R_or_C 𝕂.

Some related theorems, providing the derivative and higher regularity assuming that we already know the inverse function, are formulated in fderiv.lean, deriv.lean, and cont_diff.lean.

Notations #

In the section about approximates_linear_on 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 approximates_linear_on.to_local_homeomorph to be a local_homeomorph with to_fun = 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 approximates_linear_on.to_local_homeomorph 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.

First we prove some properties of a function that approximates_linear_on a (not necessarily invertible) continuous linear map.

We prove that a function which is linearly approximated by a continuous linear map with a nonlinear right inverse is locally onto. This will apply to the case where the approximating map is a linear equivalence, for the local inverse theorem, but also whenever the approximating map is onto, by Banach's open mapping theorem.

From now on we assume that f approximates an invertible continuous linear map f : E ≃L[𝕜] F.

We also assume that either E = {0}, or c < ‖f'⁻¹‖⁻¹. We use N as an abbreviation for ‖f'⁻¹‖.

Inverse function theorem #

Now we prove the 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 approximates_linear_on on an open neighborhood of a, and we can apply approximates_linear_on.to_local_homeomorph to construct the inverse function.

Inverse function theorem, 1D case #

In this case we prove a version of the inverse function theorem for maps f : 𝕜 → 𝕜. We use continuous_linear_equiv.units_equiv_aut to translate has_strict_deriv_at f f' a and f' ≠ 0 into has_strict_fderiv_at f (_ : 𝕜 ≃L[𝕜] 𝕜) a.

Inverse function theorem, smooth case #