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₁, E₂, and F be real or complex Banach spaces. Let f : E₁ × E₂ → F be a function that
is $C^n$ at a point (u₁, u₂) : E₁ × E₂, where n ≥ 1. Let f' be the derivative of f at
(u₁, u₂). If the map y ↦ f' (0, y) is a Banach space isomorphism, then there exists a function
ψ : E₁ → E₂ such that ψ u₁ = u₂, and f (x, ψ x) = f (u₁, u₂) holds for all x in a
neighbourhood of u₁. Furthermore, ψ is $C^n$ at u₁.
Tags #
implicit function, inverse function
theorem
ImplicitFunctionData.contDiffAt_implicitFunction
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[CompleteSpace E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[CompleteSpace E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{φ : ImplicitFunctionData 𝕜 E₁ E₂ F}
{n : WithTop ℕ∞}
(hl : ContDiffAt 𝕜 n φ.leftFun φ.pt)
(hr : ContDiffAt 𝕜 n φ.rightFun φ.pt)
(pn : n ≠ 0)
:
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.
noncomputable def
ContDiffAt.implicitFunction
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[CompleteSpace E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[CompleteSpace E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{u : E₁ × E₂}
{f : E₁ × E₂ → F}
{n : WithTop ℕ∞}
(cdf : ContDiffAt 𝕜 n f u)
(pn : n ≠ 0)
(if₂ : ((fderiv 𝕜 f u).comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
E₁ → E₂
Implicit function ψ defined by f (x, ψ x) = f u.
Equations
- cdf.implicitFunction pn if₂ = ⋯.implicitFunctionOfProdDomain if₂
Instances For
theorem
ContDiffAt.implicitFunction_def
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[CompleteSpace E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[CompleteSpace E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{u : E₁ × E₂}
{f : E₁ × E₂ → F}
{n : WithTop ℕ∞}
(cdf : ContDiffAt 𝕜 n f u)
(pn : n ≠ 0)
(if₂ : ((fderiv 𝕜 f u).comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
theorem
ContDiffAt.implicitFunction_apply_self
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[CompleteSpace E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[CompleteSpace E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{u : E₁ × E₂}
{f : E₁ × E₂ → F}
{n : WithTop ℕ∞}
(cdf : ContDiffAt 𝕜 n f u)
(pn : n ≠ 0)
(if₂ : ((fderiv 𝕜 f u).comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
At the base point u.1, the implicit function evaluates to u.2.
theorem
ContDiffAt.eventually_apply_implicitFunction
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[CompleteSpace E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[CompleteSpace E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{u : E₁ × E₂}
{f : E₁ × E₂ → F}
{n : WithTop ℕ∞}
(cdf : ContDiffAt 𝕜 n f u)
(pn : n ≠ 0)
(if₂ : ((fderiv 𝕜 f u).comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
implicitFunction is indeed the (local) implicit function defined by f.
theorem
ContDiffAt.eventually_apply_eq_iff_implicitFunction
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[CompleteSpace E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[CompleteSpace E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{u : E₁ × E₂}
{f : E₁ × E₂ → F}
{n : WithTop ℕ∞}
(cdf : ContDiffAt 𝕜 n f u)
(pn : n ≠ 0)
(if₂ : ((fderiv 𝕜 f u).comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
theorem
ContDiffAt.hasStrictFDerivAt_implicitFunction
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[CompleteSpace E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[CompleteSpace E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{u : E₁ × E₂}
{f : E₁ × E₂ → F}
{n : WithTop ℕ∞}
(cdf : ContDiffAt 𝕜 n f u)
(pn : n ≠ 0)
(if₂ : ((fderiv 𝕜 f u).comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
HasStrictFDerivAt (cdf.implicitFunction pn if₂)
(-((fderiv 𝕜 f u).comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).inverse.comp
((fderiv 𝕜 f u).comp (ContinuousLinearMap.inl 𝕜 E₁ E₂)))
u.1
theorem
ContDiffAt.contDiffAt_implicitFunction
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[CompleteSpace E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[CompleteSpace E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{u : E₁ × E₂}
{f : E₁ × E₂ → F}
{n : WithTop ℕ∞}
(cdf : ContDiffAt 𝕜 n f u)
(pn : n ≠ 0)
(if₂ : ((fderiv 𝕜 f u).comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
ContDiffAt 𝕜 n (cdf.implicitFunction pn if₂) u.1
If the implicit equation f is $C^n$ at (u₁, u₂), then its implicit function ψ around u₁
is also $C^n$ at u₁.
@[deprecated "ContDiffAt.implicitFunction does not require this" (since := "2026-01-27")]
structure
IsContDiffImplicitAt
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(n : WithTop ℕ∞)
(f : E₁ × E₂ → F)
(f' : E₁ × E₂ →L[𝕜] F)
(u : E₁ × E₂)
:
A predicate stating the sufficient conditions on an implicit equation f : E₁ × E₂ → F that
will lead to a $C^n$ implicit function ψ : E₁ → E₂.
- hasFDerivAt : HasFDerivAt f f' u
- contDiffAt : ContDiffAt 𝕜 n f u
- bijective : Function.Bijective ⇑(f'.comp (ContinuousLinearMap.inr 𝕜 E₁ E₂))
Instances For
@[deprecated ContDiffAt.implicitFunction (since := "2026-01-27")]
def
IsContDiffImplicitAt.implicitFunction
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[CompleteSpace E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[CompleteSpace E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{u : E₁ × E₂}
{f : E₁ × E₂ → F}
{n : WithTop ℕ∞}
(cdf : ContDiffAt 𝕜 n f u)
(pn : n ≠ 0)
(if₂ : ((fderiv 𝕜 f u).comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
E₁ → E₂
Alias of ContDiffAt.implicitFunction.
Implicit function ψ defined by f (x, ψ x) = f u.
Instances For
@[deprecated ContDiffAt.implicitFunction_def (since := "2026-01-27")]
theorem
IsContDiffImplicitAt.implicitFunction_def
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[CompleteSpace E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[CompleteSpace E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{u : E₁ × E₂}
{f : E₁ × E₂ → F}
{n : WithTop ℕ∞}
(cdf : ContDiffAt 𝕜 n f u)
(pn : n ≠ 0)
(if₂ : ((fderiv 𝕜 f u).comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
Alias of ContDiffAt.implicitFunction_def.
@[deprecated ContDiffAt.eventually_apply_implicitFunction (since := "2026-01-27")]
theorem
IsContDiffImplicitAt.apply_implicitFunction
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[CompleteSpace E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[CompleteSpace E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{u : E₁ × E₂}
{f : E₁ × E₂ → F}
{n : WithTop ℕ∞}
(cdf : ContDiffAt 𝕜 n f u)
(pn : n ≠ 0)
(if₂ : ((fderiv 𝕜 f u).comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
Alias of ContDiffAt.eventually_apply_implicitFunction.
implicitFunction is indeed the (local) implicit function defined by f.
@[deprecated ContDiffAt.eventually_apply_eq_iff_implicitFunction (since := "2026-01-27")]
theorem
IsContDiffImplicitAt.eventually_implicitFunction_apply_eq
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[CompleteSpace E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[CompleteSpace E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{u : E₁ × E₂}
{f : E₁ × E₂ → F}
{n : WithTop ℕ∞}
(cdf : ContDiffAt 𝕜 n f u)
(pn : n ≠ 0)
(if₂ : ((fderiv 𝕜 f u).comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
Alias of ContDiffAt.eventually_apply_eq_iff_implicitFunction.
@[deprecated ContDiffAt.contDiffAt_implicitFunction (since := "2026-01-27")]
theorem
IsContDiffImplicitAt.contDiffAt_implicitFunction
{𝕜 : Type u_1}
[RCLike 𝕜]
{E₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[CompleteSpace E₁]
{E₂ : Type u_3}
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[CompleteSpace E₂]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{u : E₁ × E₂}
{f : E₁ × E₂ → F}
{n : WithTop ℕ∞}
(cdf : ContDiffAt 𝕜 n f u)
(pn : n ≠ 0)
(if₂ : ((fderiv 𝕜 f u).comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
ContDiffAt 𝕜 n (cdf.implicitFunction pn if₂) u.1
Alias of ContDiffAt.contDiffAt_implicitFunction.
If the implicit equation f is $C^n$ at (u₁, u₂), then its implicit function ψ around u₁
is also $C^n$ at u₁.