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 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'⁻¹. Some other versions of the theorem assuming that we already know the inverse function are formulated in fderiv.lean and deriv.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, inverse function

Non-linear maps approximating 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 equivalence and c < ∥f'⁻¹∥. Maps of this type behave like f a + f' (x - a) near each a ∈ s.

If E is a complete space, we prove that the image f '' s is open, and 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.

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'⁻¹∥.

Now we prove that f '' s is an open set. This follows from the fact that the restriction of f on s is an open map. More precisely, we show that the image of a closed ball $$\bar B(a, ε) ⊆ s$$ under f includes the closed ball $$\bar B\left(f(a), frac{ε}{∥{f'}⁻¹∥⁻¹-c}\right)$$.

In order to do this, we introduce an auxiliary map $$g_y(x) = x + {f'}⁻¹ (y - f x)$$. Provided that $$∥y - f a∥ ≤ frac{ε}{∥{f'}⁻¹∥⁻¹-c}$$, we prove that $$g_y$$ contracts in $$\bar B(a, ε)$$ and f sends the fixed point of $$g_y$$ to y.

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.