# mathlibdocumentation

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 #

• Add a version for a function f : E × F → G such that $$\frac{\partial f}{\partial y}$$ is invertible.
• Add a version for f : 𝕜 × 𝕜 → 𝕜 proving has_strict_deriv_at and deriv φ = ....
• Prove that in a real vector space the implicit function has the same smoothness as the original one.
• If the original function is differentiable in a neighborhood, then the implicit function is differentiable in a neighborhood as well. Current setup only proves differentiability at one point for the implicit function constructed in this file (as opposed to an unspecified implicit function). One of the ways to overcome this difficulty is to use uniqueness of the implicit function in the general version of the theorem. Another way is to prove that any implicit function satisfying some predicate is strictly differentiable.

## Tags #

implicit function, inverse function

### General version #

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

• both functions are strictly differentiable at a;
• the derivatives are surjective;
• the kernels of the derivatives are complementary subspaces of E.

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) (E : Type u_2) [normed_group E] [ E] (F : Type u_3) [normed_group F] [ F] (G : Type u_4) [normed_group G] [ G]  :
Type (max u_2 u_3 u_4)
• left_fun : E → F
• left_deriv : E →L[𝕜] F
• right_fun : E → G
• right_deriv : E →L[𝕜] G
• pt : E
• left_has_deriv :
• right_has_deriv :
• left_range :
• right_range :
• is_compl_ker :

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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : G) (x : E) :
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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : G) (x : E) :
φ.prod_fun x = (φ.left_fun x, φ.right_fun x)
theorem implicit_function_data.has_strict_fderiv_at {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : G) :
def implicit_function_data.to_local_homeomorph {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : G) :
(F × 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : G) :
F → 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : G) :
theorem implicit_function_data.to_local_homeomorph_apply {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : G) (x : E) :
theorem implicit_function_data.pt_mem_to_local_homeomorph_source {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : G) :
theorem implicit_function_data.map_pt_mem_to_local_homeomorph_target {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : G) :
theorem implicit_function_data.prod_map_implicit_function {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : G) :
∀ᶠ (x : E) in 𝓝 φ.pt, φ.implicit_function (φ.left_fun x) (φ.right_fun x) = x
theorem implicit_function_data.map_nhds_eq {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : G) :
(𝓝 φ.pt) = 𝓝 (φ.left_fun φ.pt)
theorem implicit_function_data.implicit_function_has_strict_fderiv_at {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (φ : G) (g'inv : G →L[𝕜] E) (hg'inv : φ.right_deriv.comp g'inv = ) (hg'invf : φ.left_deriv.comp g'inv = 0) :

### 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E → F) (f' : E →L[𝕜] F) {a : E} (hf : a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) :
(f'.ker)

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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E → F) (f' : E →L[𝕜] F) {a : E} (hf : a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) :
(F × (f'.ker))

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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E → F) (f' : E →L[𝕜] F) {a : E} (hf : a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) :
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_of_complemented_fst {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) (x : E) :
( hker) x).fst = f x
theorem has_strict_fderiv_at.implicit_to_local_homeomorph_of_complemented_apply {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) (y : E) :
hker) y = (f y, (classical.some hker) (y - a))
@[simp]
theorem has_strict_fderiv_at.implicit_to_local_homeomorph_of_complemented_apply_ker {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) (y : (f'.ker)) :
hker) (y + a) = (f (y + a), y)
@[simp]
theorem has_strict_fderiv_at.implicit_to_local_homeomorph_of_complemented_self {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) :
hker) a = (f a, 0)
theorem has_strict_fderiv_at.mem_implicit_to_local_homeomorph_of_complemented_source {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) :
a
theorem has_strict_fderiv_at.mem_implicit_to_local_homeomorph_of_complemented_target {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) :
(f a, 0)
theorem has_strict_fderiv_at.map_implicit_function_of_complemented_eq {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) :
∀ᶠ (p : F × (f'.ker)) in 𝓝 (f a, 0), f 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) (hker : f'.ker.closed_complemented) :
∀ᶠ (x : E) in 𝓝 a, hker (f x) ( hker) x).snd = x

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

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

### 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] [ F] (f : E → F) (f' : E →L[𝕜] F) {a : E} (hf : a) (hf' : f'.range = ) :
(F × (f'.ker))

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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] [ F] (f : E → F) (f' : E →L[𝕜] F) {a : E} (hf : a) (hf' : f'.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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) (x : E) :
( hf') x).fst = f x
@[simp]
theorem has_strict_fderiv_at.implicit_to_local_homeomorph_apply_ker {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) (y : (f'.ker)) :
hf') (y + a) = (f (y + a), y)
@[simp]
theorem has_strict_fderiv_at.implicit_to_local_homeomorph_self {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) :
hf') a = (f a, 0)
theorem has_strict_fderiv_at.mem_implicit_to_local_homeomorph_source {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) :
theorem has_strict_fderiv_at.mem_implicit_to_local_homeomorph_target {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) :
(f a, 0)
theorem has_strict_fderiv_at.tendsto_implicit_function {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) {α : Type u_4} {l : filter α} {g₁ : α → F} {g₂ : α → (f'.ker)} (h₁ : l (𝓝 (f a))) (h₂ : l (𝓝 0)) :
filter.tendsto (λ (t : α), hf' (g₁ t) (g₂ t)) l (𝓝 a)
theorem filter.tendsto.implicit_function {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) {α : Type u_4} {l : filter α} {g₁ : α → F} {g₂ : α → (f'.ker)} (h₁ : l (𝓝 (f a))) (h₂ : l (𝓝 0)) :
filter.tendsto (λ (t : α), hf' (g₁ t) (g₂ t)) l (𝓝 a)

Alias of tendsto_implicit_function.

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

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

@[simp]
theorem has_strict_fderiv_at.implicit_function_apply_image {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) :
hf' (f a) 0 = a
theorem has_strict_fderiv_at.eq_implicit_function {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) :
∀ᶠ (x : E) in 𝓝 a, hf' (f x) ( hf') x).snd = x

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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] [ F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : a) (hf' : f'.range = ) :