mathlib documentation

analysis.calculus.implicit

Implicit function theorem

We prove three versions of the implicit function theorem. First we define a structure implicit_function_data that holds arguments for the most general version of the implicit function theorem, see implicit_function_data.implicit_function and implicit_function_data.to_implicit_function. This version allows a user to choose a specific implicit function but provides only a little convenience over the inverse function theorem.

Then we define implicit_function_of_complemented: implicit function defined by f (g z y) = z, where f : E → F is a function strictly differentiable at a such that its derivative f' is surjective and has a complemented kernel.

Finally, if the codomain of f is a finite dimensional space, then we can automatically prove that the kernel of f' is complemented, hence the only assumptions are has_strict_fderiv_at and f'.range = ⊤. This version is named implicit_function.

TODO

Tags

implicit function, inverse function

General version

Consider two functions f : E → F and g : E → G and a point a such that

Note that the map x ↦ (f x, g x) has a bijective derivative, hence it is a local homeomorphism between E and F × G. We use this fact to define a function φ : F → G → E (see implicit_function_data.implicit_function) such that for (y, z) close enough to (f a, g a) we have f (φ y z) = y and g (φ y z) = z.

We also prove a formula for $$\frac{\partial\varphi}{\partial z}.$$

Though this statement is almost symmetric with respect to F, G, we interpret it in the following way. Consider a family of surfaces {x | f x = y}, y ∈ 𝓝 (f a). Each of these surfaces is parametrized by φ y.

There are many ways to choose a (differentiable) function φ such that f (φ y z) = y but the extra condition g (φ y z) = z allows a user to select one of these functions. If we imagine that the level surfaces f = const form a local horizontal foliation, then the choice of g fixes a transverse foliation g = const, and φ is the inverse function of the projection of {x | f x = y} along this transverse foliation.

This version of the theorem is used to prove the other versions and can be used if a user needs to have a complete control over the choice of the implicit function.

@[nolint]
structure implicit_function_data (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (E : Type u_2) [normed_group E] [normed_space 𝕜 E] [complete_space E] (F : Type u_3) [normed_group F] [normed_space 𝕜 F] [complete_space F] (G : Type u_4) [normed_group G] [normed_space 𝕜 G] [complete_space G] :
Type (max u_2 u_3 u_4)

Data for the general version of the implicit function theorem. It holds two functions f : E → F and g : E → G (named left_fun and right_fun) and a point a (named pt) such that

  • both functions are strictly differentiable at a;
  • the derivatives are surjective;
  • the kernels of the derivatives are complementary subspaces of E.
def implicit_function_data.prod_fun {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {G : Type u_4} [normed_group G] [normed_space 𝕜 G] [complete_space G] :
implicit_function_data 𝕜 E F GE → F × G

The function given by x ↦ (left_fun x, right_fun x).

Equations
@[simp]
theorem implicit_function_data.prod_fun_apply {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {G : Type u_4} [normed_group G] [normed_space 𝕜 G] [complete_space G] (φ : implicit_function_data 𝕜 E F G) (x : E) :
φ.prod_fun x = (φ.left_fun x, φ.right_fun x)

def implicit_function_data.to_local_homeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {G : Type u_4} [normed_group G] [normed_space 𝕜 G] [complete_space G] :

Implicit function theorem. If f : E → F and g : E → G are two maps strictly differentiable at a, their derivatives f', g' are surjective, and the kernels of these derivatives are complementary subspaces of E, then x ↦ (f x, g x) defines a local homeomorphism between E and F × G. In particular, {x | f x = f a} is locally homeomorphic to G.

Equations
def implicit_function_data.implicit_function {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {G : Type u_4} [normed_group G] [normed_space 𝕜 G] [complete_space G] :
implicit_function_data 𝕜 E F GF → G → E

Implicit function theorem. If f : E → F and g : E → G are two maps strictly differentiable at a, their derivatives f', g' are surjective, and the kernels of these derivatives are complementary subspaces of E, then implicit_function_of_is_compl_ker is the unique (germ of a) map φ : F → G → E such that f (φ y z) = y and g (φ y z) = z.

Equations
@[simp]
theorem implicit_function_data.to_local_homeomorph_coe {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {G : Type u_4} [normed_group G] [normed_space 𝕜 G] [complete_space G] (φ : implicit_function_data 𝕜 E F G) :

theorem implicit_function_data.to_local_homeomorph_apply {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {G : Type u_4} [normed_group G] [normed_space 𝕜 G] [complete_space G] (φ : implicit_function_data 𝕜 E F G) (x : E) :

theorem implicit_function_data.prod_map_implicit_function {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {G : Type u_4} [normed_group G] [normed_space 𝕜 G] [complete_space G] (φ : implicit_function_data 𝕜 E F G) :
∀ᶠ (p : F × G) in 𝓝 (φ.prod_fun φ.pt), φ.prod_fun (φ.implicit_function p.fst p.snd) = p

theorem implicit_function_data.left_map_implicit_function {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {G : Type u_4} [normed_group G] [normed_space 𝕜 G] [complete_space G] (φ : implicit_function_data 𝕜 E F G) :
∀ᶠ (p : F × G) in 𝓝 (φ.prod_fun φ.pt), φ.left_fun (φ.implicit_function p.fst p.snd) = p.fst

theorem implicit_function_data.right_map_implicit_function {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {G : Type u_4} [normed_group G] [normed_space 𝕜 G] [complete_space G] (φ : implicit_function_data 𝕜 E F G) :
∀ᶠ (p : F × G) in 𝓝 (φ.prod_fun φ.pt), φ.right_fun (φ.implicit_function p.fst p.snd) = p.snd

theorem implicit_function_data.implicit_function_apply_image {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {G : Type u_4} [normed_group G] [normed_space 𝕜 G] [complete_space G] (φ : implicit_function_data 𝕜 E F G) :
∀ᶠ (x : E) in 𝓝 φ.pt, φ.implicit_function (φ.left_fun x) (φ.right_fun x) = x

theorem implicit_function_data.implicit_function_has_strict_fderiv_at {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {G : Type u_4} [normed_group G] [normed_space 𝕜 G] [complete_space G] (φ : implicit_function_data 𝕜 E F G) (g'inv : G →L[𝕜] E) :

Case of a complemented kernel

In this section we prove the following version of the implicit function theorem. Consider a map f : E → F and a point a : E such that f is strictly differentiable at a, its derivative f' is surjective and the kernel of f' is a complemented subspace of E (i.e., it has a closed complementary subspace). Then there exists a function φ : F → ker f' → E such that for (y, z) close to (f a, 0) we have f (φ y z) = y and the derivative of φ (f a) at zero is the embedding ker f' → E.

Note that a map with these properties is not unique. E.g., different choices of a subspace complementary to ker f' lead to different maps φ.

@[simp]
def has_strict_fderiv_at.implicit_function_data_of_complemented {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] (f : E → F) (f' : E →L[𝕜] F) {a : E} :

Data used to apply the generic implicit function theorem to the case of a strictly differentiable map such that its derivative is surjective and has a complemented kernel.

Equations
def has_strict_fderiv_at.implicit_to_local_homeomorph_of_complemented {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] (f : E → F) (f' : E →L[𝕜] F) {a : E} :

A local homeomorphism between E and F × f'.ker sending level surfaces of f to vertical subspaces.

Equations
def has_strict_fderiv_at.implicit_function_of_complemented {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] (f : E → F) (f' : E →L[𝕜] F) {a : E} :
has_strict_fderiv_at f f' af'.range = f'.ker.closed_complementedF → (f'.ker) → E

Implicit function g defined by f (g z y) = z.

Equations
@[simp]
theorem has_strict_fderiv_at.implicit_to_local_homeomorph_of_complemented_fst {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) (x : E) :

theorem has_strict_fderiv_at.implicit_to_local_homeomorph_of_complemented_apply {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) (y : E) :

@[simp]
theorem has_strict_fderiv_at.implicit_to_local_homeomorph_of_complemented_apply_ker {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) (y : (f'.ker)) :

@[simp]
theorem has_strict_fderiv_at.implicit_to_local_homeomorph_of_complemented_self {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) :

theorem has_strict_fderiv_at.mem_implicit_to_local_homeomorph_of_complemented_target {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) :

theorem has_strict_fderiv_at.map_implicit_function_of_complemented_eq {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) :
∀ᶠ (p : F × (f'.ker)) in 𝓝 (f a, 0), f (has_strict_fderiv_at.implicit_function_of_complemented f f' hf hf' hker p.fst p.snd) = p.fst

implicit_function_of_complemented sends (z, y) to a point in f ⁻¹' z.

theorem has_strict_fderiv_at.eq_implicit_function_of_complemented {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) :

Any point in some neighborhood of a can be represented as implicit_function of some point.

theorem has_strict_fderiv_at.to_implicit_function_of_complemented {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) :

Finite dimensional case

In this section we prove the following version of the implicit function theorem. Consider a map f : E → F from a Banach normed space to a finite dimensional space. Take a point a : E such that f is strictly differentiable at a and its derivative f' is surjective. Then there exists a function φ : F → ker f' → E such that for (y, z) close to (f a, 0) we have f (φ y z) = y and the derivative of φ (f a) at zero is the embedding ker f' → E.

This version deduces that ker f' is a complemented subspace from the fact that F is a finite dimensional space, then applies the previous version.

Note that a map with these properties is not unique. E.g., different choices of a subspace complementary to ker f' lead to different maps φ.

def has_strict_fderiv_at.implicit_to_local_homeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [finite_dimensional 𝕜 F] (f : E → F) (f' : E →L[𝕜] F) {a : E} :

Given a map f : E → F to a finite dimensional space with a surjective derivative f', returns a local homeomorphism between E and F × ker f'.

Equations
def has_strict_fderiv_at.implicit_function {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [finite_dimensional 𝕜 F] (f : E → F) (f' : E →L[𝕜] F) {a : E} :
has_strict_fderiv_at f f' af'.range = F → (f'.ker) → E

Implicit function g defined by f (g z y) = z.

Equations
@[simp]
theorem has_strict_fderiv_at.implicit_to_local_homeomorph_fst {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [finite_dimensional 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) (x : E) :

@[simp]
theorem has_strict_fderiv_at.implicit_to_local_homeomorph_apply_ker {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [finite_dimensional 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) (y : (f'.ker)) :

@[simp]
theorem has_strict_fderiv_at.implicit_to_local_homeomorph_self {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [finite_dimensional 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) :

theorem has_strict_fderiv_at.mem_implicit_to_local_homeomorph_source {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [finite_dimensional 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) :

theorem has_strict_fderiv_at.mem_implicit_to_local_homeomorph_target {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [finite_dimensional 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) :

theorem has_strict_fderiv_at.map_implicit_function_eq {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [finite_dimensional 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) :
∀ᶠ (p : F × (f'.ker)) in 𝓝 (f a, 0), f (has_strict_fderiv_at.implicit_function f f' hf hf' p.fst p.snd) = p.fst

implicit_function sends (z, y) to a point in f ⁻¹' z.

theorem has_strict_fderiv_at.eq_implicit_function {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [finite_dimensional 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) :

Any point in some neighborhood of a can be represented as implicit_function of some point.

theorem has_strict_fderiv_at.to_implicit_function {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [finite_dimensional 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ) :