mathlib3 documentation

analysis.calculus.implicit

Implicit function theorem #

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

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) [nontrivially_normed_field 𝕜] (E : Type u_2) [normed_add_comm_group E] [normed_space 𝕜 E] [complete_space E] (F : Type u_3) [normed_add_comm_group F] [normed_space 𝕜 F] [complete_space F] (G : Type u_4) [normed_add_comm_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.
Instances for implicit_function_data
  • implicit_function_data.has_sizeof_inst

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

Equations
@[simp]

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

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

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]

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

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

Equations
noncomputable def has_strict_fderiv_at.implicit_function_of_complemented {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_add_comm_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' : linear_map.range f' = ) (hker : (linear_map.ker f').closed_complemented) :

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

Equations

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

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

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 φ.

noncomputable def has_strict_fderiv_at.implicit_to_local_homeomorph {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_add_comm_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' : linear_map.range f' = ) :

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
noncomputable def has_strict_fderiv_at.implicit_function {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_add_comm_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' : linear_map.range f' = ) :

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} [nontrivially_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_add_comm_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' : linear_map.range f' = ) (x : E) :
@[simp]
@[simp]
theorem has_strict_fderiv_at.tendsto_implicit_function {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_add_comm_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' : linear_map.range f' = ) {α : Type u_4} {l : filter α} {g₁ : α F} {g₂ : α (linear_map.ker f')} (h₁ : filter.tendsto g₁ l (nhds (f a))) (h₂ : filter.tendsto g₂ l (nhds 0)) :
filter.tendsto (λ (t : α), has_strict_fderiv_at.implicit_function f f' hf hf' (g₁ t) (g₂ t)) l (nhds a)
theorem filter.tendsto.implicit_function {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_add_comm_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' : linear_map.range f' = ) {α : Type u_4} {l : filter α} {g₁ : α F} {g₂ : α (linear_map.ker f')} (h₁ : filter.tendsto g₁ l (nhds (f a))) (h₂ : filter.tendsto g₂ l (nhds 0)) :
filter.tendsto (λ (t : α), has_strict_fderiv_at.implicit_function f f' hf hf' (g₁ t) (g₂ t)) l (nhds a)

Alias of has_strict_fderiv_at.tendsto_implicit_function.

theorem has_strict_fderiv_at.map_implicit_function_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_add_comm_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' : linear_map.range f' = ) :

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

@[simp]
theorem has_strict_fderiv_at.implicit_function_apply_image {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] [complete_space 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] [complete_space E] {F : Type u_3} [normed_add_comm_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' : linear_map.range f' = ) :

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