Implicit function theorem — curried bivariate #
This specialization of the implicit function theorem applies to a curried bivariate function
f : E₁ → E₂ → F and assumes continuity of both its partial derivatives at u : E₁ × E₂ as well as
invertibility of f₂ u.1 u.2 : 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.1 v.2 = f u.1 u.2 ↔ ψ v.1 = v.2. This is implicitFunctionOfBivariate. A formula for its
first derivative follows.
A similar specialization is made to an uncurried bivariate function by
HasStrictFDerivAt.implicitFunctionOfProdDomain in a sister file.
Tags #
implicit function
noncomputable def
implicitFunctionOfBivariate
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[IsRCLikeNormedField 𝕜]
{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₁ : E₁ → E₂ → E₁ →L[𝕜] F}
{f₂ : E₁ → E₂ → E₂ →L[𝕜] F}
(df₁ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₁) => f x v.2) (f₁ v.1 v.2) v.1)
(df₂ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₂) => f v.1 x) (f₂ v.1 v.2) v.2)
(cf₁ : ContinuousAt (↿f₁) u)
(cf₂ : ContinuousAt (↿f₂) u)
(if₂u : (f₂ u.1 u.2).IsInvertible)
:
E₁ → E₂
Implicit function ψ : E₁ → E₂ associated with the (curried) bivariate function
f : E₁ → E₂ → F at u : E₁ × E₂.
Equations
- implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u = ⋯.implicitFunctionOfProdDomain ⋯
Instances For
theorem
implicitFunctionOfBivariate_def
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[IsRCLikeNormedField 𝕜]
{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₁ : E₁ → E₂ → E₁ →L[𝕜] F}
{f₂ : E₁ → E₂ → E₂ →L[𝕜] F}
(df₁ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₁) => f x v.2) (f₁ v.1 v.2) v.1)
(df₂ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₂) => f v.1 x) (f₂ v.1 v.2) v.2)
(cf₁ : ContinuousAt (↿f₁) u)
(cf₂ : ContinuousAt (↿f₂) u)
(if₂u : (f₂ u.1 u.2).IsInvertible)
:
theorem
tendsto_implicitFunctionOfBivariate
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[IsRCLikeNormedField 𝕜]
{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₁ : E₁ → E₂ → E₁ →L[𝕜] F}
{f₂ : E₁ → E₂ → E₂ →L[𝕜] F}
(df₁ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₁) => f x v.2) (f₁ v.1 v.2) v.1)
(df₂ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₂) => f v.1 x) (f₂ v.1 v.2) v.2)
(cf₁ : ContinuousAt (↿f₁) u)
(cf₂ : ContinuousAt (↿f₂) u)
(if₂u : (f₂ u.1 u.2).IsInvertible)
:
Filter.Tendsto (implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u) (nhds u.1) (nhds u.2)
theorem
eventually_apply_implicitFunctionOfBivariate
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[IsRCLikeNormedField 𝕜]
{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₁ : E₁ → E₂ → E₁ →L[𝕜] F}
{f₂ : E₁ → E₂ → E₂ →L[𝕜] F}
(df₁ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₁) => f x v.2) (f₁ v.1 v.2) v.1)
(df₂ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₂) => f v.1 x) (f₂ v.1 v.2) v.2)
(cf₁ : ContinuousAt (↿f₁) u)
(cf₂ : ContinuousAt (↿f₂) u)
(if₂u : (f₂ u.1 u.2).IsInvertible)
:
theorem
eventually_apply_eq_iff_implicitFunctionOfBivariate
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[IsRCLikeNormedField 𝕜]
{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₁ : E₁ → E₂ → E₁ →L[𝕜] F}
{f₂ : E₁ → E₂ → E₂ →L[𝕜] F}
(df₁ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₁) => f x v.2) (f₁ v.1 v.2) v.1)
(df₂ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₂) => f v.1 x) (f₂ v.1 v.2) v.2)
(cf₁ : ContinuousAt (↿f₁) u)
(cf₂ : ContinuousAt (↿f₂) u)
(if₂u : (f₂ u.1 u.2).IsInvertible)
:
theorem
hasStrictFDerivAt_implicitFunctionOfBivariate
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[IsRCLikeNormedField 𝕜]
{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₁ : E₁ → E₂ → E₁ →L[𝕜] F}
{f₂ : E₁ → E₂ → E₂ →L[𝕜] F}
(df₁ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₁) => f x v.2) (f₁ v.1 v.2) v.1)
(df₂ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₂) => f v.1 x) (f₂ v.1 v.2) v.2)
(cf₁ : ContinuousAt (↿f₁) u)
(cf₂ : ContinuousAt (↿f₂) u)
(if₂u : (f₂ u.1 u.2).IsInvertible)
:
HasStrictFDerivAt (implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u) (-(f₂ u.1 u.2).inverse.comp (f₁ u.1 u.2)) u.1