Mixed-norm scaling of the harmonic pressure remainder

The interior slice supremum scales with degree two in space, and the time change of variables leaves the critical factor R.

theorem ESS.blowupPressureRemainder_mixed_sup_scale_bound (p₂ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₂ : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p₂ (z.1, z.2)) (3 / 2) ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)))) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) {Ω : Set CKN.Foundation.Parabolic.Vec3} (hΩ : MeasurableSet Ω) (himage : ∀ x ∈ Ω, CKN.scalingSpace r x₀ x ∈ CKN.euclideanBall 0 (3 / 4)) : ∫⁻ (t : ℝ), MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => parabolicRescalePressure x₀ t₀ r (goodPointDomain.indicator p₂) (x, t)) ⊤ (MeasureTheory.volume.restrict Ω) ^ (3 / 2) ≤ ENNReal.ofReal r * ∫⁻ (s : ℝ), blowupHarmonicSupExtended p₂ s ^ (3 / 2)

The zero-extended rescaled harmonic remainder has a mixed spatial L∞ time L^(3/2) bound with the critical linear scale factor.