Harmonicity of the fixed pressure remainder #
The whole-space Riesz pressure and the pressure from the weak momentum equation have the same spatial Laplacian on the source cylinder.
noncomputable def
ESS.pressureSplitRieszPressure
(F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume)
:
The fixed whole-space pressure of the zero-extended local velocity tensor, written in parabolic coordinates.
Equations
Instances For
The pressure remainder on the original source cylinder, extended by zero.
Equations
- ESS.pressureSplitRemainder p p₁ = ESS.goodPointDomain.indicator fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => p z - p₁ z
Instances For
theorem
ESS.pressureSplit_remainder_memLp_product
{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 → ℝ}
(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 < ⊤)
(hp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict pressureSplitDomain))
(hL3 :
essSup
(fun (t : ℝ) =>
∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in pressureSplitBall, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3)
(MeasureTheory.volume.restrict pressureSplitTime) < ⊤)
(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)
:
theorem
ESS.pressureSplit_remainder_pairing_zero
{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 → ℝ}
(hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict pressureSplitDomain))
(hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict pressureSplitDomain))
(hpmeas : MeasureTheory.AEStronglyMeasurable p (MeasureTheory.volume.restrict pressureSplitDomain))
(hL2 :
essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in pressureSplitBall, ‖u (x, t)‖ₑ ^ 2)
(MeasureTheory.volume.restrict pressureSplitTime) < ⊤)
(henergy : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in pressureSplitDomain, ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤)
(hp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict pressureSplitDomain))
(hL3 :
essSup
(fun (t : ℝ) =>
∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in pressureSplitBall, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3)
(MeasureTheory.volume.restrict pressureSplitTime) < ⊤)
(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)
(hMomentum :
∀ φ ∈ CKN.spaceTimeTestFunction pressureSplitBall pressureSplitTime,
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in pressureSplitDomain, -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3,
∑ j : Fin 3,
u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3,
∑ j : Fin 3,
Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, 0 z i * φ z i = 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 × ℝ), pressureSplitRemainder p (pressureSplitRieszPressure (CKN.pressureSplitTensor u) ⋯)
(CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) * (θ z.2 * CKN.spatialLaplacian ψ z.1) = 0