Local partial differential relations and their formal solutions

This file defines RelLoc E F, the type of first order partial differential relations for maps between two real normed spaces E and F.

To any R : RelLoc E F we associate the type sol R of maps f : E → F of solutions of R, and its formal counterpart FormalSol R. (FIXME(grunweg): sol is never mentioned; is this docstring outdated?)

The h-principle question is whether we can deform any formal solution into a solution. The type of deformations is HtpyJetSet E F (homotopies of 1-jet sections).

@[reducible, inline]

abbrev RelLoc (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] : Type (max u_2 u_1)

A first order relation for maps between real vector spaces.

Equations

• RelLoc E F = Set (OneJet E F)

instance instMembershipProdContinuousLinearMapRealIdRelLoc (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] : Membership (E × F × (E →L[ℝ] F)) (RelLoc E F)

Equations

• instMembershipProdContinuousLinearMapRealIdRelLoc E F = id inferInstance

def JetSec.IsFormalSol {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 : JetSec E F) (R : RelLoc E F) : Prop

A predicate stating that a 1-jet section is a formal solution to a first order relation for maps between vector spaces.

Equations

• 𝓕.IsFormalSol R = ∀ (x : E), (x, 𝓕.f x, 𝓕.φ x) ∈ R

structure RelLoc.FormalSol {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (R : RelLoc E F) extends JetSec E F : Type (max u_1 u_2)

A formal solution to a local relation R.

• f : E → F
• f_diff : 𝒞 (↑⊤) (↑self).f
• φ : E → E →L[ℝ] F
• φ_diff : 𝒞 (↑⊤) (↑self).φ
• is_sol (x : E) : (x, (↑self).f x, (↑self).φ x) ∈ R

theorem RelLoc.FormalSol.ext {E : Type u_1} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {F : Type u_2} {inst✝² : NormedAddCommGroup F} {inst✝³ : NormedSpace ℝ F} {R : RelLoc E F} {x y : R.FormalSol} (f : (↑x).f = (↑y).f) (φ : (↑x).φ = (↑y).φ) : x = y

instance RelLoc.instCoeOutFormalSolJetSec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (R : RelLoc E F) : CoeOut R.FormalSol (JetSec E F)

Equations

• R.instCoeOutFormalSolJetSec = { coe := RelLoc.FormalSol.toJetSec }

@[simp]

theorem RelLoc.FormalSol.toJetSec_eq_coe {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} (𝓕 : R.FormalSol) : ↑𝓕 = ↑𝓕

@[simp]

theorem RelLoc.FormalSol.coeIsFormalSol {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} (𝓕 : R.FormalSol) : (↑𝓕).IsFormalSol R

def JetSec.IsFormalSol.formalSol {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝓕 : JetSec E F} {R : RelLoc E F} (h : 𝓕.IsFormalSol R) : R.FormalSol

Bundling a formal solution from a 1-jet section that is a formal solution.

Equations

• h.formalSol = { toJetSec := 𝓕, is_sol := h }

instance RelLoc.instFunLikeFormalSolProdContinuousLinearMapRealId {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (R : RelLoc E F) : FunLike R.FormalSol E (F × (E →L[ℝ] F))

Equations

• R.instFunLikeFormalSolProdContinuousLinearMapRealId = { coe := fun (𝓕 : R.FormalSol) (x : E) => ((↑𝓕).f x, (↑𝓕).φ x), coe_injective' := ⋯ }

@[simp]

theorem RelLoc.FormalSol.coe_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} (𝓕 : R.FormalSol) (x : E) : ↑𝓕 x = 𝓕 x

theorem RelLoc.FormalSol.eq_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} {𝓕 𝓕' : R.FormalSol} {x : E} : 𝓕 x = 𝓕' x ↔ (↑𝓕).f x = (↑𝓕').f x ∧ (↑𝓕).φ x = (↑𝓕').φ x

def RelLoc.FormalSol.IsHolonomicAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} (𝓕 : R.FormalSol) (x : E) : Prop

A formal solution (f, φ) is holonomic at x if the differential of f at x is φ x.

Equations

• 𝓕.IsHolonomicAt x = (D (↑𝓕).f x = (↑𝓕).φ x)

theorem RelLoc.FormalSol.isHolonomicAt_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} (𝓕 𝓕' : R.FormalSol) {s : Set E} (h : ∀ᶠ (x : E) in nhdsSet s, 𝓕 x = 𝓕' x) : ∀ᶠ (x : E) in nhdsSet s, 𝓕.IsHolonomicAt x ↔ 𝓕'.IsHolonomicAt x

structure RelLoc.FamilyFormalSol {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (P : Type u_3) [NormedAddCommGroup P] [NormedSpace ℝ P] (R : RelLoc E F) extends FamilyJetSec E F P : Type (max (max u_1 u_2) u_3)

A family of formal solutions is a 1-parameter family of formal solutions.

• f : P → E → F
• f_diff : 𝒞 ↑⊤ ↿self.f
• φ : P → E → E →L[ℝ] F
• φ_diff : 𝒞 ↑⊤ ↿self.φ
• is_sol (t : P) (x : E) : (x, self.f t x, self.φ t x) ∈ R

theorem RelLoc.FamilyFormalSol.ext {E : Type u_1} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {F : Type u_2} {inst✝² : NormedAddCommGroup F} {inst✝³ : NormedSpace ℝ F} {P : Type u_3} {inst✝⁴ : NormedAddCommGroup P} {inst✝⁵ : NormedSpace ℝ P} {R : RelLoc E F} {x y : FamilyFormalSol P R} (f : x.f = y.f) (φ : x.φ = y.φ) : x = y

@[reducible]

def RelLoc.HtpyFormalSol {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (R : RelLoc E F) : Type (max (max u_1 u_2) 0)

A homotopy of formal solutions is a 1-parameter family of formal solutions.

Equations

• R.HtpyFormalSol = RelLoc.FamilyFormalSol ℝ R

def RelLoc.HtpyFormalSol.toHtpyJetSec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} (𝓕 : R.HtpyFormalSol) : HtpyJetSec E F

Equations

• 𝓕.toHtpyJetSec = 𝓕.toFamilyJetSec

instance RelLoc.instFunLikeFamilyFormalSolJetSec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (P : Type u_3) [NormedAddCommGroup P] [NormedSpace ℝ P] (R : RelLoc E F) : FunLike (FamilyFormalSol P R) P (JetSec E F)

Equations

• RelLoc.instFunLikeFamilyFormalSolJetSec P R = { coe := fun (S : RelLoc.FamilyFormalSol P R) => ⇑S.toFamilyJetSec, coe_injective' := ⋯ }