Space-time pressure mass estimates for the fixed split #
The uniform spatial pressure estimate also controls the local space-time mass of the whole-space part.
theorem
ESS.pressureSplitRieszPressure_source_mass_bound
{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 < ⊤)
(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)
:
∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in pressureSplitProductDomain, ENNReal.ofReal
|pressureSplitRieszPressure (CKN.pressureSplitTensor u) ⋯
(CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)| ^ (3 / 2) ≤ ENNReal.ofReal
(CKN.Leray.rieszPressureOperatorBound (3 / 2) pressureSplitRieszPressure_source_mass_bound._proof_1 * (9 * pressureSplitVelocityLpBound u ^ 2)) ^ (3 / 2)
Integrating the fixed-slice pressure estimate bounds the local space-time
L^(3/2) mass of the whole-space pressure by its uniform slice bound.