Implicit function theorem #
We prove three versions of the implicit function theorem. First we define a structure
ImplicitFunctionData that holds arguments for the most general version of the implicit function
theorem, see ImplicitFunctionData.implicitFunction and
ImplicitFunctionData.implicitFunction_hasStrictFDerivAt. 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 HasStrictFDerivAt.implicitFunctionDataOfComplemented: 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 HasStrictFDerivAt
and f'.range = ⊤. This version is named HasStrictFDerivAt.implicitFunction.
TODO #
- Add a version for a function
f : E × F → Gsuch that - Add a version for
f : 𝕜 × 𝕜 → 𝕜provingHasStrictDerivAtandderiv φ = .... - 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 partial homeomorphism
between E and F × G. We use this fact to define a function φ : F → G → E
(see ImplicitFunctionData.implicitFunction) 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
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.
Data for the general version of the implicit function theorem. It holds two functions
f : E → F and g : E → G (named leftFun and rightFun) 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.
- leftFun : E → F
Left function
Derivative of the left function
- rightFun : E → G
Right function
Derivative of the right function
- pt : E
- left_has_deriv : HasStrictFDerivAt self.leftFun self.leftDeriv self.pt
- right_has_deriv : HasStrictFDerivAt self.rightFun self.rightDeriv self.pt
- isCompl_ker : IsCompl (LinearMap.ker self.leftDeriv) (LinearMap.ker self.rightDeriv)
The function given by x ↦ (leftFun x, rightFun x).
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 partial 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 implicitFunction 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 φ.
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
- One or more equations did not get rendered due to their size.
A partial homeomorphism between E and F × f'.ker sending level surfaces of f
to vertical subspaces.
Equations
- HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented f f' hf hf' hker = (HasStrictFDerivAt.implicitFunctionDataOfComplemented f f' hf hf' hker).toPartialHomeomorph
Implicit function g defined by f (g z y) = z.
Equations
- HasStrictFDerivAt.implicitFunctionOfComplemented f f' hf hf' hker = (HasStrictFDerivAt.implicitFunctionDataOfComplemented f f' hf hf' hker).implicitFunction
HasStrictFDerivAt.implicitFunctionOfComplemented sends (z, y) to a point in f ⁻¹' z.
Any point in some neighborhood of a can be represented as
HasStrictFDerivAt.implicitFunctionOfComplemented 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 φ.
Given a map f : E → F to a finite dimensional space with a surjective derivative f',
returns a partial homeomorphism between E and F × ker f'.
Equations
- HasStrictFDerivAt.implicitToPartialHomeomorph f f' hf hf' = HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented f f' hf hf' ⋯
Implicit function g defined by f (g z y) = z.
Equations
- HasStrictFDerivAt.implicitFunction f f' hf hf' = Function.curry ↑(HasStrictFDerivAt.implicitToPartialHomeomorph f f' hf hf').symm
HasStrictFDerivAt.implicitFunction sends (z, y) to a point in f ⁻¹' z.
Any point in some neighborhood of a can be represented as HasStrictFDerivAt.implicitFunction
of some point.