Time-integrated harmonic pressure bound

CKN's interior estimate on each harmonic slice gives a uniform estimate after integration in time (lem:pressure-split).

theorem ESS.blowupHarmonicSlices_time_bound : ∃ C < ⊤, ∀ (h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (J : Set ℝ), (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)) ∧ CKN.Foundation.Heat.WeaklyHarmonicOn (CKN.euclideanBall 0 1) fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)) → ∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)) ⊤ (MeasureTheory.volume.restrict (CKN.euclideanBall 0 (3 / 4))) ^ (3 / 2) ≤ C * ∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)) ^ (3 / 2)

The interior L∞ norm of almost every harmonic slice has a time-integral bound with an absolute constant.