Pressure Split Data

The decomposition of pressure into local Poisson and harmonic parts.

theorem ESS.pressureSplit_localData {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)) (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) : CKN.IsSuitableWeakSolutionData pressureSplitBall pressureSplitTime 3 u Du p fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0

Local integrability data on compact subcylinders follows from the data in thm:ess-local; it is used when testing the momentum equation in lem:pressure-split.