mathlib documentation

analysis.calculus.inverse

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:

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:

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

def approximates_linear_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] (f : E → F) (f' : E →L[𝕜] F) (s : set E) (c : nnreal) :
Prop

We say that f approximates a continuous linear map f' on s with constant c, if ∥f x - f y - f' (x - y)∥ ≤ c * ∥x - y∥ whenever x, y ∈ s.

This predicate is defined to facilitate the splitting of the inverse function theorem into small lemmas. Some of these lemmas can be useful, e.g., to prove that the inverse function is defined on a specific set.

Equations
@[simp]
theorem approximates_linear_on_empty {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] (f : E → F) (f' : E →L[𝕜] F) (c : nnreal) :

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

theorem approximates_linear_on.mono_num {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c c' : nnreal} (hc : c c') (hf : approximates_linear_on f f' s c) :
theorem approximates_linear_on.mono_set {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s t : set E} {c : nnreal} (hst : s t) (hf : approximates_linear_on f f' t c) :
theorem approximates_linear_on.approximates_linear_on_iff_lipschitz_on_with {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c : nnreal} :
theorem lipschitz_on_with.approximates_linear_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c : nnreal} :

Alias of the reverse direction of approximates_linear_on.approximates_linear_on_iff_lipschitz_on_with.

theorem approximates_linear_on.lipschitz_on_with {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c : nnreal} :

Alias of the forward direction of approximates_linear_on.approximates_linear_on_iff_lipschitz_on_with.

theorem approximates_linear_on.lipschitz_sub {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) :
lipschitz_with c (λ (x : s), f x - f' x)
@[protected]
theorem approximates_linear_on.lipschitz {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) :
@[protected]
theorem approximates_linear_on.continuous {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) :
@[protected]
theorem approximates_linear_on.continuous_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) :

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.

theorem approximates_linear_on.surj_on_closed_ball_of_nonlinear_right_inverse {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {s : set E} {c : nnreal} {f' : E →L[𝕜] F} (hf : approximates_linear_on f f' s c) (f'symm : f'.nonlinear_right_inverse) {ε : } {b : E} (ε0 : 0 ε) (hε : metric.closed_ball b ε s) :

If a function is linearly approximated by a continuous linear map with a (possibly nonlinear) right inverse, then it is locally onto: a ball of an explicit radius is included in the image of the map.

theorem approximates_linear_on.open_image {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {s : set E} {c : nnreal} {f' : E →L[𝕜] F} (hf : approximates_linear_on f f' s c) (f'symm : f'.nonlinear_right_inverse) (hs : is_open s) (hc : subsingleton F c < (f'symm.nnnorm)⁻¹) :
is_open (f '' s)
theorem approximates_linear_on.image_mem_nhds {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {s : set E} {c : nnreal} {f' : E →L[𝕜] F} (hf : approximates_linear_on f f' s c) (f'symm : f'.nonlinear_right_inverse) {x : E} (hs : s nhds x) (hc : subsingleton F c < (f'symm.nnnorm)⁻¹) :
f '' s nhds (f x)
theorem approximates_linear_on.map_nhds_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {s : set E} {c : nnreal} {f' : E →L[𝕜] F} (hf : approximates_linear_on f f' s c) (f'symm : f'.nonlinear_right_inverse) {x : E} (hs : s nhds x) (hc : subsingleton F c < (f'symm.nnnorm)⁻¹) :
filter.map f (nhds x) = nhds (f x)

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

@[protected]
theorem approximates_linear_on.antilipschitz {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (f'.symm)∥₊⁻¹) :
@[protected]
theorem approximates_linear_on.injective {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (f'.symm)∥₊⁻¹) :
@[protected]
theorem approximates_linear_on.inj_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (f'.symm)∥₊⁻¹) :
@[protected]
theorem approximates_linear_on.surjective {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {c : nnreal} [complete_space E] (hf : approximates_linear_on f f' set.univ c) (hc : subsingleton E c < (f'.symm)∥₊⁻¹) :
noncomputable def approximates_linear_on.to_local_equiv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (f'.symm)∥₊⁻¹) :

A map approximating a linear equivalence on a set defines a local equivalence on this set. Should not be used outside of this file, because it is superseded by to_local_homeomorph below.

This is a first step towards the inverse function.

Equations
theorem approximates_linear_on.inverse_continuous_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (f'.symm)∥₊⁻¹) :

The inverse function is continuous on f '' s. Use properties of local_homeomorph instead.

theorem approximates_linear_on.to_inv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (f'.symm)∥₊⁻¹) :

The inverse function is approximated linearly on f '' s by f'.symm.

noncomputable def approximates_linear_on.to_local_homeomorph {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] (f : E → F) {f' : E ≃L[𝕜] F} (s : set E) {c : nnreal} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (f'.symm)∥₊⁻¹) (hs : is_open s) :

Given a function f that approximates a linear equivalence on an open set s, returns a local homeomorph with to_fun = f and source = s.

Equations
noncomputable def approximates_linear_on.to_homeomorph {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] (f : E → F) {f' : E ≃L[𝕜] F} {c : nnreal} (hf : approximates_linear_on f f' set.univ c) (hc : subsingleton E c < (f'.symm)∥₊⁻¹) :
E ≃ₜ F

A function f that approximates a linear equivalence on the whole space is a homeomorphism.

Equations

In a real vector space, a function f that approximates a linear equivalence on a subset s can be extended to a homeomorphism of the whole space.

@[simp]
theorem approximates_linear_on.to_local_homeomorph_coe {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (f'.symm)∥₊⁻¹) (hs : is_open s) :
@[simp]
theorem approximates_linear_on.to_local_homeomorph_source {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (f'.symm)∥₊⁻¹) (hs : is_open s) :
@[simp]
theorem approximates_linear_on.to_local_homeomorph_target {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (f'.symm)∥₊⁻¹) (hs : is_open s) :
theorem approximates_linear_on.closed_ball_subset_target {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {ε : } [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : nnreal} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (f'.symm)∥₊⁻¹) (hs : is_open s) {b : E} (ε0 : 0 ε) (hε : metric.closed_ball b ε s) :

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.

theorem has_strict_fderiv_at.approximates_deriv_on_nhds {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) {c : nnreal} (hc : subsingleton E 0 < c) :
∃ (s : set E) (H : s nhds a), approximates_linear_on 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 has_strict_fderiv_at.map_nhds_eq_of_surj {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [complete_space E] [complete_space F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (h : f'.range = ) :
filter.map f (nhds a) = nhds (f a)
theorem has_strict_fderiv_at.approximates_deriv_on_open_nhds {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :
∃ (s : set E) (hs : a s is_open s), approximates_linear_on f f' s ((f'.symm)∥₊⁻¹ / 2)
noncomputable def has_strict_fderiv_at.to_local_homeomorph {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] (f : E → F) {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :

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

Equations
@[simp]
theorem has_strict_fderiv_at.to_local_homeomorph_coe {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :
theorem has_strict_fderiv_at.mem_to_local_homeomorph_source {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :
theorem has_strict_fderiv_at.image_mem_to_local_homeomorph_target {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :
theorem has_strict_fderiv_at.map_nhds_eq_of_equiv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :
filter.map f (nhds a) = nhds (f a)
noncomputable def has_strict_fderiv_at.local_inverse {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] (f : E → F) (f' : E ≃L[𝕜] F) (a : E) (hf : has_strict_fderiv_at f f' a) :
F → E

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

Equations
theorem has_strict_fderiv_at.local_inverse_def {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :
theorem has_strict_fderiv_at.eventually_left_inverse {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :
∀ᶠ (x : E) in nhds a, has_strict_fderiv_at.local_inverse f f' a hf (f x) = x
@[simp]
theorem has_strict_fderiv_at.local_inverse_apply_image {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :
theorem has_strict_fderiv_at.eventually_right_inverse {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :
∀ᶠ (y : F) in nhds (f a), f (has_strict_fderiv_at.local_inverse f f' a hf y) = y
theorem has_strict_fderiv_at.local_inverse_continuous_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :
theorem has_strict_fderiv_at.local_inverse_tendsto {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :
theorem has_strict_fderiv_at.local_inverse_unique {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) {g : F → E} (hg : ∀ᶠ (x : E) in nhds a, g (f x) = x) :
∀ᶠ (y : F) in nhds (f a), g y = has_strict_fderiv_at.local_inverse f f' a hf y
theorem has_strict_fderiv_at.to_local_inverse {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :

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

theorem has_strict_fderiv_at.to_local_left_inverse {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) {g : F → E} (hg : ∀ᶠ (x : E) in nhds a, g (f x) = x) :

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 [complete_space E] see of_local_left_inverse.

theorem open_map_of_strict_fderiv_equiv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [complete_space E] {f : E → F} {f' : E → (E ≃L[𝕜] F)} (hf : ∀ (x : E), has_strict_fderiv_at f (f' x) x) :

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

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.

@[reducible]
noncomputable def has_strict_deriv_at.local_inverse {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] [cs : complete_space 𝕜] (f : 𝕜 → 𝕜) (f' a : 𝕜) (hf : has_strict_deriv_at f f' a) (hf' : f' 0) :
𝕜 → 𝕜

A function that is inverse to f near a.

Equations
theorem has_strict_deriv_at.map_nhds_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] [cs : complete_space 𝕜] {f : 𝕜 → 𝕜} {f' a : 𝕜} (hf : has_strict_deriv_at f f' a) (hf' : f' 0) :
filter.map f (nhds a) = nhds (f a)
theorem has_strict_deriv_at.to_local_inverse {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] [cs : complete_space 𝕜] {f : 𝕜 → 𝕜} {f' a : 𝕜} (hf : has_strict_deriv_at f f' a) (hf' : f' 0) :
theorem has_strict_deriv_at.to_local_left_inverse {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] [cs : complete_space 𝕜] {f : 𝕜 → 𝕜} {f' a : 𝕜} (hf : has_strict_deriv_at f f' a) (hf' : f' 0) {g : 𝕜 → 𝕜} (hg : ∀ᶠ (x : 𝕜) in nhds a, g (f x) = x) :
theorem open_map_of_strict_deriv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] [complete_space 𝕜] {f f' : 𝕜 → 𝕜} (hf : ∀ (x : 𝕜), has_strict_deriv_at f (f' x) x) (h0 : ∀ (x : 𝕜), f' x 0) :

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

Inverse function theorem, smooth case #

noncomputable def cont_diff_at.to_local_homeomorph {𝕂 : Type u_6} [is_R_or_C 𝕂] {E' : Type u_7} [normed_add_comm_group E'] [normed_space 𝕂 E'] {F' : Type u_8} [normed_add_comm_group F'] [normed_space 𝕂 F'] [complete_space E'] (f : E' → F') {f' : E' ≃L[𝕂] F'} {a : E'} {n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f f' a) (hn : 1 n) :

Given a cont_diff function over 𝕂 (which is or ) with an invertible derivative at a, returns a local_homeomorph with to_fun = f and a ∈ source.

Equations
@[simp]
theorem cont_diff_at.to_local_homeomorph_coe {𝕂 : Type u_6} [is_R_or_C 𝕂] {E' : Type u_7} [normed_add_comm_group E'] [normed_space 𝕂 E'] {F' : Type u_8} [normed_add_comm_group F'] [normed_space 𝕂 F'] [complete_space E'] {f : E' → F'} {f' : E' ≃L[𝕂] F'} {a : E'} {n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f f' a) (hn : 1 n) :
theorem cont_diff_at.mem_to_local_homeomorph_source {𝕂 : Type u_6} [is_R_or_C 𝕂] {E' : Type u_7} [normed_add_comm_group E'] [normed_space 𝕂 E'] {F' : Type u_8} [normed_add_comm_group F'] [normed_space 𝕂 F'] [complete_space E'] {f : E' → F'} {f' : E' ≃L[𝕂] F'} {a : E'} {n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f f' a) (hn : 1 n) :
theorem cont_diff_at.image_mem_to_local_homeomorph_target {𝕂 : Type u_6} [is_R_or_C 𝕂] {E' : Type u_7} [normed_add_comm_group E'] [normed_space 𝕂 E'] {F' : Type u_8} [normed_add_comm_group F'] [normed_space 𝕂 F'] [complete_space E'] {f : E' → F'} {f' : E' ≃L[𝕂] F'} {a : E'} {n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f f' a) (hn : 1 n) :
noncomputable def cont_diff_at.local_inverse {𝕂 : Type u_6} [is_R_or_C 𝕂] {E' : Type u_7} [normed_add_comm_group E'] [normed_space 𝕂 E'] {F' : Type u_8} [normed_add_comm_group F'] [normed_space 𝕂 F'] [complete_space E'] {f : E' → F'} {f' : E' ≃L[𝕂] F'} {a : E'} {n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f f' a) (hn : 1 n) :
F' → E'

Given a cont_diff function over 𝕂 (which is or ) with an invertible derivative at a, returns a function that is locally inverse to f.

Equations
theorem cont_diff_at.local_inverse_apply_image {𝕂 : Type u_6} [is_R_or_C 𝕂] {E' : Type u_7} [normed_add_comm_group E'] [normed_space 𝕂 E'] {F' : Type u_8} [normed_add_comm_group F'] [normed_space 𝕂 F'] [complete_space E'] {f : E' → F'} {f' : E' ≃L[𝕂] F'} {a : E'} {n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f f' a) (hn : 1 n) :
hf.local_inverse hf' hn (f a) = a
theorem cont_diff_at.to_local_inverse {𝕂 : Type u_6} [is_R_or_C 𝕂] {E' : Type u_7} [normed_add_comm_group E'] [normed_space 𝕂 E'] {F' : Type u_8} [normed_add_comm_group F'] [normed_space 𝕂 F'] [complete_space E'] {f : E' → F'} {f' : E' ≃L[𝕂] F'} {a : E'} {n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f f' a) (hn : 1 n) :
cont_diff_at 𝕂 n (hf.local_inverse hf' hn) (f a)

Given a cont_diff function over 𝕂 (which is or ) with an invertible derivative at a, the inverse function (produced by cont_diff.to_local_homeomorph) is also cont_diff.