Implicit function theorem #
In this file, we apply the generalised implicit function theorem to the more familiar case and show that the implicit function preserves the smoothness class of the implicit equation.
Let E, F, and G be real or complex Banach spaces. Let f : E × F → G be a function that is
$C^n$ at a point (a, b) : E × F, where n ≥ 1. Let f' be the derivative of f at (a, b). If
the map y ↦ f' (0, y) is a Banach space isomorphism, then there exists a function φ : E → F such
that φ a = b, and f x (φ x) = f a b holds for all x in a neighbourhood of a. Furthermore,
φ is $C^n$ at a.
TODO #
- Local uniqueness of the implicit function
- Derivative of the implicit function
Tags #
implicit function, inverse function
theorem
ImplicitFunctionData.contDiff_implicitFunction
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace G]
{φ : ImplicitFunctionData 𝕜 E F G}
{n : WithTop ℕ∞}
(hl : ContDiffAt 𝕜 n φ.leftFun φ.pt)
(hr : ContDiffAt 𝕜 n φ.rightFun φ.pt)
(hn : 1 ≤ n)
:
ContDiffAt 𝕜 n (Function.uncurry φ.implicitFunction) (φ.prodFun φ.pt)
The implicit function defined by a $C^n$ implicit equation is $C^n$. This applies to the general form of the implicit function theorem.
structure
IsContDiffImplicitAt
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(n : WithTop ℕ∞)
(f : E × F → G)
(f' : E × F →L[𝕜] G)
(a : E × F)
:
A predicate stating the sufficient conditions on an implicit equation f : E × F → G that will
lead to a $C^n$ implicit function φ : E → F.
- hasFDerivAt : HasFDerivAt f f' a
- contDiffAt : ContDiffAt 𝕜 n f a
- bijective : Function.Bijective ⇑(f'.comp (ContinuousLinearMap.inr 𝕜 E F))
Instances For
def
IsContDiffImplicitAt.implicitFunctionData
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace G]
{n : WithTop ℕ∞}
{f : E × F → G}
{f' : E × F →L[𝕜] G}
{a : E × F}
(h : IsContDiffImplicitAt n f f' a)
:
ImplicitFunctionData 𝕜 (E × F) E G
We record the parameters of our specific case in order to apply the general implicit function theorem.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
IsContDiffImplicitAt.implicitFunctionData_leftFun_pt
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace G]
{n : WithTop ℕ∞}
{f : E × F → G}
{f' : E × F →L[𝕜] G}
{a : E × F}
(h : IsContDiffImplicitAt n f f' a)
:
@[simp]
theorem
IsContDiffImplicitAt.implicitFunctionData_rightFun_pt
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace G]
{n : WithTop ℕ∞}
{f : E × F → G}
{f' : E × F →L[𝕜] G}
{a : E × F}
(h : IsContDiffImplicitAt n f f' a)
:
noncomputable def
IsContDiffImplicitAt.implicitFunctionAux
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace G]
{n : WithTop ℕ∞}
{f : E × F → G}
{f' : E × F →L[𝕜] G}
{a : E × F}
(h : IsContDiffImplicitAt n f f' a)
:
E → G → E × F
The implicit function provided by the general theorem, from which we construct the more useful
form IsContDiffImplicitAt.implicitFunction.
Equations
Instances For
theorem
IsContDiffImplicitAt.implicitFunctionAux_fst
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace G]
{n : WithTop ℕ∞}
{f : E × F → G}
{f' : E × F →L[𝕜] G}
{a : E × F}
(h : IsContDiffImplicitAt n f f' a)
:
theorem
IsContDiffImplicitAt.comp_implicitFunctionAux_eq_snd
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace G]
{n : WithTop ℕ∞}
{f : E × F → G}
{f' : E × F →L[𝕜] G}
{a : E × F}
(h : IsContDiffImplicitAt n f f' a)
:
noncomputable def
IsContDiffImplicitAt.implicitFunction
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace G]
{n : WithTop ℕ∞}
{f : E × F → G}
{f' : E × F →L[𝕜] G}
{a : E × F}
(h : IsContDiffImplicitAt n f f' a)
:
E → F
Implicit function φ defined by f (x, φ x) = f a.
Equations
- h.implicitFunction x = (h.implicitFunctionAux x (f a)).2
Instances For
theorem
IsContDiffImplicitAt.implicitFunction_def
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace G]
{n : WithTop ℕ∞}
{f : E × F → G}
{f' : E × F →L[𝕜] G}
{a : E × F}
(h : IsContDiffImplicitAt n f f' a)
:
h.implicitFunction = fun (x : E) => (Function.uncurry h.implicitFunctionData.implicitFunction (x, f a)).2
theorem
IsContDiffImplicitAt.apply_implicitFunction
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace G]
{n : WithTop ℕ∞}
{f : E × F → G}
{f' : E × F →L[𝕜] G}
{a : E × F}
(h : IsContDiffImplicitAt n f f' a)
:
implicitFunction is indeed the (local) implicit function defined by f.
theorem
IsContDiffImplicitAt.contDiffAt_implicitFunction
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace G]
{n : WithTop ℕ∞}
{f : E × F → G}
{f' : E × F →L[𝕜] G}
{a : E × F}
(h : IsContDiffImplicitAt n f f' a)
:
ContDiffAt 𝕜 n h.implicitFunction a.1
If the implicit equation f is $C^n$ at (x, y), then its implicit function φ around x is
also $C^n$ at x.