Fixed pressure split estimates

The whole-space pressure slice estimate, harmonicity, and interior estimate give the fixed decomposition used in lem:pressure-split.

theorem ESS.pressureSplit_remainder_harmonic_interior_bound {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) : have p₁ := pressureSplitRieszPressure (CKN.pressureSplitTensor u) ⋯; have p₂ := pressureSplitRemainder p p₁; MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p₂ (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict pressureSplitTime, CKN.Foundation.Heat.WeaklyHarmonicOn pressureSplitBall fun (x : CKN.Foundation.Parabolic.Vec3) => p₂ (x, t)) ∧ ∃ C < ⊤, ∫⁻ (t : ℝ) in pressureSplitTime, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => p₂ (x, t)) ⊤ (MeasureTheory.volume.restrict (CKN.euclideanBall 0 (3 / 4))) ^ (3 / 2) ≤ C * MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p₂ (z.1, z.2)) (3 / 2) ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict pressureSplitTime)) ^ (3 / 2)

The harmonic part of the fixed pressure split has an integrable interior spatial supremum, bounded by its local space-time L^(3/2) mass.