Fixed pressure slice bound

The tensor slices inherit the quadratic bound from the velocity slices, and the spatial Riesz operator gives the corresponding pressure estimate.

theorem ESS.pressureSplitRieszPressure_slice_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) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict pressureSplitTime, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => pressureSplitRieszPressure (CKN.pressureSplitTensor u) ⋯ (x, t)) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => pressureSplitRieszPressure (CKN.pressureSplitTensor u) ⋯ (x, t)) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ ENNReal.ofReal (CKN.Leray.rieszPressureOperatorBound (3 / 2) pressureSplitRieszPressure_slice_bound._proof_1 * (9 * pressureSplitVelocityLpBound u ^ 2))

The fixed whole-space pressure has an essentially uniform spatial L^(3/2) bound on the source time interval.