The implicit function theorem with a moving level

Let f : E₁ × E₂ → F be strictly differentiable at u with invertible partial derivative ∂₂f(u) : E₂ →L[𝕜] F. Mathlib's HasStrictFDerivAt.implicitFunctionOfProdDomain solves f (z, v) = f u for v as a function of z, at the fixed level f u. Here the level w varies as well: the joint implicit function ψ (z, w) solves f (z, ψ (z, w)) = w for (z, w) near (u.1, f u). For each z it is a local inverse of v ↦ f (z, v), and it depends jointly on the parameter z and the value w.

The construction applies Mathlib's ImplicitFunctionData for f and Prod.fst (HasStrictFDerivAt.implicitFunctionDataOfProdDomain), that is, the local inverse of (z, v) ↦ (f (z, v), z), and reads off the second coordinate. So ψ inherits the joint regularity of that local inverse: it is strictly differentiable, C^n when f is (over ℝ or ℂ), and analytic when f is. Over ℂ in finite dimensions this gives the holomorphic implicit map of a holomorphic equation, see TauCeti.Analysis.Complex.ImplicitFunction.

Main results

• HasStrictFDerivAt.jointImplicitFunctionOfProdDomain: the joint implicit function ψ.
• HasStrictFDerivAt.jointImplicitFunctionOfProdDomain_apply_self: ψ (u.1, f u) = u.2.
• HasStrictFDerivAt.eventually_apply_jointImplicitFunctionOfProdDomain: near (u.1, f u), f (z, ψ (z, w)) = w.
• HasStrictFDerivAt.eventually_jointImplicitFunctionOfProdDomain_apply: near u, ψ (z, f (z, v)) = v.
• HasStrictFDerivAt.eventually_apply_eq_iff_jointImplicitFunctionOfProdDomain: near (u, f u), f (z, v) = w ↔ ψ (z, w) = v.
• HasStrictFDerivAt.eventuallyEq_jointImplicitFunctionOfProdDomain and HasStrictFDerivAt.eventuallyEq_jointImplicitFunctionOfProdDomain_of_continuousAt: local uniqueness of ψ, from a left-inverse identity, or from a right-inverse identity together with continuity and the value at the base point.
• HasStrictFDerivAt.hasStrictFDerivAt_jointImplicitFunctionOfProdDomain: the derivative of ψ at (u.1, f u) is (z, w) ↦ ∂₂f(u)⁻¹ (w - ∂₁f(u) z).
• HasStrictFDerivAt.contDiffAt_jointImplicitFunctionOfProdDomain and HasStrictFDerivAt.analyticAt_jointImplicitFunctionOfProdDomain: ψ is as regular as f.

References

• R. C. Gunning, H. Rossi, Analytic Functions of Several Complex Variables, Prentice-Hall (1965), Chapter I (the holomorphic inverse and implicit function theorems).

noncomputable def HasStrictFDerivAt.jointImplicitFunctionOfProdDomain {𝕜 : 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 ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible) : E₁ × F → E₂

The joint implicit function ψ : E₁ × F → E₂ of f : E₁ × E₂ → F at u, defined near (u.1, f u) by f (z, ψ (z, w)) = w. It is the second coordinate of the local inverse of (z, v) ↦ (f (z, v), z) given by HasStrictFDerivAt.implicitFunctionDataOfProdDomain.

theorem HasStrictFDerivAt.jointImplicitFunctionOfProdDomain_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 ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible} : dfu.jointImplicitFunctionOfProdDomain if₂u = fun (p : E₁ × F) => ((dfu.implicitFunctionDataOfProdDomain if₂u).implicitFunction p.2 p.1).2

theorem HasStrictFDerivAt.implicitFunctionOfProdDomain_eq_jointImplicitFunctionOfProdDomain {𝕜 : 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 ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible) : dfu.implicitFunctionOfProdDomain if₂u = fun (z : E₁) => dfu.jointImplicitFunctionOfProdDomain if₂u (z, f u)

At the fixed level f u, the joint implicit function is Mathlib's implicit function.

theorem HasStrictFDerivAt.eventually_apply_jointImplicitFunctionOfProdDomain {𝕜 : 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 ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible) : ∀ᶠ (p : E₁ × F) in nhds (u.1, f u), f (p.1, dfu.jointImplicitFunctionOfProdDomain if₂u p) = p.2

Near (u.1, f u), the joint implicit function solves f (z, ψ (z, w)) = w.

theorem HasStrictFDerivAt.eventually_jointImplicitFunctionOfProdDomain_apply {𝕜 : 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 ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible) : ∀ᶠ (v : E₁ × E₂) in nhds u, dfu.jointImplicitFunctionOfProdDomain if₂u (v.1, f v) = v.2

Near u, the joint implicit function inverts v ↦ f (z, v): ψ (z, f (z, v)) = v.

@[simp]

theorem HasStrictFDerivAt.jointImplicitFunctionOfProdDomain_apply_self {𝕜 : 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 ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible) : dfu.jointImplicitFunctionOfProdDomain if₂u (u.1, f u) = u.2

The joint implicit function takes the value u.2 at (u.1, f u).

theorem HasStrictFDerivAt.eventually_apply_eq_iff_jointImplicitFunctionOfProdDomain {𝕜 : 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 ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible) : ∀ᶠ (q : (E₁ × E₂) × F) in nhds (u, f u), f q.1 = q.2 ↔ dfu.jointImplicitFunctionOfProdDomain if₂u (q.1.1, q.2) = q.1.2

Local uniqueness of solutions. For (z, v) near u and w near f u, the equation f (z, v) = w holds exactly when v = ψ (z, w).

theorem HasStrictFDerivAt.eventuallyEq_jointImplicitFunctionOfProdDomain {𝕜 : 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 ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible) {φ : E₁ × F → E₂} (hφ : ∀ᶠ (v : E₁ × E₂) in nhds u, φ (v.1, f v) = v.2) : φ =ᶠ[nhds (u.1, f u)] dfu.jointImplicitFunctionOfProdDomain if₂u

Local uniqueness of the joint implicit function, left-inverse form: a function φ with φ (z, f (z, v)) = v for (z, v) near u agrees with ψ near (u.1, f u).

theorem HasStrictFDerivAt.eventuallyEq_jointImplicitFunctionOfProdDomain_of_continuousAt {𝕜 : 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 ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible) {φ : E₁ × F → E₂} (hφc : ContinuousAt φ (u.1, f u)) (hφu : φ (u.1, f u) = u.2) (hφ : ∀ᶠ (p : E₁ × F) in nhds (u.1, f u), f (p.1, φ p) = p.2) : φ =ᶠ[nhds (u.1, f u)] dfu.jointImplicitFunctionOfProdDomain if₂u

Local uniqueness of the joint implicit function, right-inverse form: a function φ, continuous at (u.1, f u) with value u.2 there and with f (z, φ (z, w)) = w near (u.1, f u), agrees with ψ near (u.1, f u).

theorem HasStrictFDerivAt.hasStrictFDerivAt_jointImplicitFunctionOfProdDomain {𝕜 : 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 ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible) : HasStrictFDerivAt (dfu.jointImplicitFunctionOfProdDomain if₂u) ((f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL (ContinuousLinearMap.snd 𝕜 E₁ F - f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂ ∘SL ContinuousLinearMap.fst 𝕜 E₁ F)) (u.1, f u)

The joint implicit function is strictly differentiable at (u.1, f u), with derivative (z, w) ↦ ∂₂f(u)⁻¹ (w - ∂₁f(u) z).

theorem HasStrictFDerivAt.analyticAt_jointImplicitFunctionOfProdDomain {𝕜 : 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 ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible) (hf : AnalyticAt 𝕜 f u) : AnalyticAt 𝕜 (dfu.jointImplicitFunctionOfProdDomain if₂u) (u.1, f u)

The joint implicit function of an analytic equation is analytic.

theorem HasStrictFDerivAt.contDiffAt_jointImplicitFunctionOfProdDomain {𝕜 : 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} {f'u : E₁ × E₂ →L[𝕜] F} (dfu : HasStrictFDerivAt f f'u u) (if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible) {n : WithTop ℕ∞} (hf : ContDiffAt 𝕜 n f u) : ContDiffAt 𝕜 n (dfu.jointImplicitFunctionOfProdDomain if₂u) (u.1, f u)

The joint implicit function of a C^n equation is C^n.