Implicit function theorem — domain a product space #
This specialization of the implicit function theorem applies to an uncurried bivariate function
f : E₁ × E₂ → F and assumes strict differentiability of f at u : E₁ × E₂ as well as
invertibility of f₂u : E₂ →L[𝕜] F its partial derivative with respect to the second argument.
It proves the existence of ψ : E₁ → E₂ such that for v in a neighbourhood of u we have
f v = f u ↔ ψ v.1 = v.2. This is HasStrictFDerivAt.implicitFunctionOfProdDomain. A formula for
its first derivative follows.
Tags #
implicit function
def
HasStrictFDerivAt.implicitFunctionDataOfProdDomain
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{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}
{f'u : E₁ × E₂ →L[𝕜] F}
(dfu : HasStrictFDerivAt f f'u u)
(if₂u : (f'u.comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁
Given f : E₁ × E₂ → F strictly differentiable at u with invertible partial derivative
f₂u : E₂ →L[𝕜] F, we may construct an ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ with f as its
leftFun and Prod.fst : E₁ × E₂ → E₁ as its rightFun by proving that the kernels of the
associated leftDeriv and rightDeriv are complementary.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
HasStrictFDerivAt.pt_implicitFunctionDataOfProdDomain
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{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}
{f'u : E₁ × E₂ →L[𝕜] F}
(dfu : HasStrictFDerivAt f f'u u)
(if₂u : (f'u.comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
@[simp]
theorem
HasStrictFDerivAt.leftFun_implicitFunctionDataOfProdDomain
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{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}
{f'u : E₁ × E₂ →L[𝕜] F}
(dfu : HasStrictFDerivAt f f'u u)
(if₂u : (f'u.comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
@[simp]
theorem
HasStrictFDerivAt.rightFun_implicitFunctionDataOfProdDomain
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{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}
{f'u : E₁ × E₂ →L[𝕜] F}
(dfu : HasStrictFDerivAt f f'u u)
(if₂u : (f'u.comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
noncomputable def
HasStrictFDerivAt.implicitFunctionOfProdDomain
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{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}
{f'u : E₁ × E₂ →L[𝕜] F}
(dfu : HasStrictFDerivAt f f'u u)
(if₂u : (f'u.comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
E₁ → E₂
Implicit function ψ : E₁ → E₂ associated with the (uncurried) bivariate function
f : E₁ × E₂ → F at u : E₁ × E₂.
Equations
- dfu.implicitFunctionOfProdDomain if₂u x = ((dfu.implicitFunctionDataOfProdDomain if₂u).implicitFunction (f u) x).2
Instances For
theorem
HasStrictFDerivAt.implicitFunctionOfProdDomain_def
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{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}
{f'u : E₁ × E₂ →L[𝕜] F}
{dfu : HasStrictFDerivAt f f'u u}
{if₂u : (f'u.comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible}
:
dfu.implicitFunctionOfProdDomain if₂u = fun (x : E₁) =>
((dfu.implicitFunctionDataOfProdDomain if₂u).implicitFunction (f u) x).2
theorem
HasStrictFDerivAt.eventually_apply_eq_iff_implicitFunctionOfProdDomain
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{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}
{f'u : E₁ × E₂ →L[𝕜] F}
(dfu : HasStrictFDerivAt f f'u u)
(if₂u : (f'u.comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
theorem
HasStrictFDerivAt.hasStrictFDerivAt_implicitFunctionOfProdDomain
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{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}
{f'u : E₁ × E₂ →L[𝕜] F}
(dfu : HasStrictFDerivAt f f'u u)
(if₂u : (f'u.comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
HasStrictFDerivAt (dfu.implicitFunctionOfProdDomain if₂u)
(-(f'u.comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).inverse.comp (f'u.comp (ContinuousLinearMap.inl 𝕜 E₁ E₂))) u.1
theorem
HasStrictFDerivAt.tendsto_implicitFunctionOfProdDomain
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{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}
{f'u : E₁ × E₂ →L[𝕜] F}
(dfu : HasStrictFDerivAt f f'u u)
(if₂u : (f'u.comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
:
Filter.Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (nhds u.1) (nhds u.2)
theorem
HasStrictFDerivAt.eventually_apply_implicitFunctionOfProdDomain
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{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}
{f'u : E₁ × E₂ →L[𝕜] F}
(dfu : HasStrictFDerivAt f f'u u)
(if₂u : (f'u.comp (ContinuousLinearMap.inr 𝕜 E₁ E₂)).IsInvertible)
: