The source cylinder for the fixed pressure decomposition in lem:pressure-split.

def ESS.pressureSplitBall : Set CKN.Foundation.Parabolic.Vec3

The unit spatial ball used in the fixed pressure decomposition.

Equations

• ESS.pressureSplitBall = CKN.Foundation.Parabolic.vec3Ball 0 1

def ESS.pressureSplitTime : Set ℝ

The source time interval used in the fixed pressure decomposition.

Equations

• ESS.pressureSplitTime = Set.Ioo (-1) 0

def ESS.pressureSplitDomain : Set CKN.Foundation.Parabolic.ParabolicPoint

The parabolic source cylinder for the fixed pressure decomposition.

Equations

• ESS.pressureSplitDomain = CKN.spaceTimeSet ESS.pressureSplitBall ESS.pressureSplitTime

def ESS.pressureSplitProductDomain : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)

The product-coordinate source cylinder for the fixed pressure decomposition.

Equations

• ESS.pressureSplitProductDomain = ESS.pressureSplitBall ×ˢ ESS.pressureSplitTime

theorem ESS.pressureSplit_viscousTerm_zero_product {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict pressureSplitDomain)) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict pressureSplitDomain)) (henergy : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in pressureSplitDomain, ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤) (hgrad : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict pressureSplitTime, ∀ (i : Fin 3), CKN.HasWeakGradientOn pressureSplitBall (fun (x : CKN.Vec 3) => u (x, t) i) fun (x : CKN.Vec 3) => Du (x, t) i) (hdiv : ∀ χ ∈ CKN.spaceTimeTestFunction pressureSplitBall pressureSplitTime, ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in pressureSplitDomain, ∑ i : Fin 3, u z i * CKN.spatialPartial χ i z = 0) {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψB : tsupport ψ ⊆ pressureSplitBall) {θ : ℝ → ℝ} (hθ : ContDiff ℝ (↑⊤) θ) (hθc : HasCompactSupport θ) (hθI : tsupport θ ⊆ pressureSplitTime) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in pressureSplitProductDomain, ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * (θ z.2 * CKN.mixedSecond ψ j i z.1) = 0

The viscous contribution vanishes when the momentum equation is tested against a separated spatial gradient in lem:pressure-split.