Restricting suitable solutions

Open restrictions of suitable solutions retain the same test identities, as in lem:sws-restrict of the CKN manuscript.

def ESS.parabolicScalarTest (g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : CKN.Foundation.Parabolic.ParabolicPoint → ℝ

A scalar product-spacetime test viewed on parabolic spacetime.

Equations

• ESS.parabolicScalarTest g z = g (CKN.Foundation.Parabolic.parabolicHomeomorph z)

def ESS.parabolicVectorTest (g : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

A vector product-spacetime test viewed on parabolic spacetime.

Equations

• ESS.parabolicVectorTest g z = g (CKN.Foundation.Parabolic.parabolicHomeomorph z)

theorem ESS.isSuitableWeakSolution_restrict {Ω Ω₁ : Set CKN.Foundation.Parabolic.Vec3} {I I₁ : Set ℝ} {q : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hSuitable : CKN.IsSuitableWeakSolution Ω I q u Du p f) (hΩ₁open : IsOpen Ω₁) (hI₁open : IsOpen I₁) (hI₁ord : I₁.OrdConnected) (hΩ₁ : Ω₁ ⊆ Ω) (hI₁ : I₁ ⊆ I) : CKN.IsSuitableWeakSolution Ω₁ I₁ q u Du p f

Suitable weak solutions restrict to open subdomains and open time intervals.