Cell estimates for spatially bounded pressure remainders

A spatial supremum controlled in L^{3/2} in time gives the cell-radius power needed for the harmonic part of the pressure gradient. The temporal Hölder factor is retained explicitly before the Morrey normalization.

theorem CKN.Core.Step4.pressure_remainder_time_power_bound {H : ℝ → ENNReal} (hH : AEMeasurable H MeasureTheory.volume) {t r : ℝ} (hr : 0 < r) : ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, H s ^ (6 / 5) ≤ (∫⁻ (s : ℝ), H s ^ (3 / 2)) ^ (4 / 5) * ENNReal.ofReal r ^ (2 / 5)

Temporal Hölder on a cell window produces the factor r^{2/5} for the 6/5 power integral of a function controlled in L^{3/2} in time.

theorem CKN.Core.Step4.pressure_remainder_cylinder_power_bound {F : Foundation.Parabolic.ParabolicPoint → ℝ} {H : ℝ → ENNReal} (hF : AEMeasurable F MeasureTheory.volume) (hH : AEMeasurable H MeasureTheory.volume) (hbound : ∀ᵐ (s : ℝ), ∀ (x : Foundation.Parabolic.Vec3), ‖F (x, s)‖ₑ ≤ H s) {x : Foundation.Parabolic.Vec3} {t r : ℝ} (hr : 0 < r) : Foundation.Parabolic.Morrey.cylinderPowerIntegral (6 / 5) F (x, t) r ≤ MeasureTheory.volume (Foundation.Parabolic.vec3Ball x r) * (∫⁻ (s : ℝ), H s ^ (3 / 2)) ^ (4 / 5) * ENNReal.ofReal r ^ (2 / 5)

A spatial bound on almost every time slice gives a power-integral estimate on every cylinder, with its full spatial volume factor.

theorem CKN.Core.Step4.pressure_remainder_morreyCell_bound {κ : ℝ} {F : Foundation.Parabolic.ParabolicPoint → ℝ} {H : ℝ → ENNReal} (hF : AEMeasurable F MeasureTheory.volume) (hH : AEMeasurable H MeasureTheory.volume) (hbound : ∀ᵐ (s : ℝ), ∀ (x : Foundation.Parabolic.Vec3), ‖F (x, s)‖ₑ ≤ H s) {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) : Foundation.Parabolic.Morrey.morreyCell (6 / 5) κ F z r ≤ ENNReal.ofReal (Real.pi * 4 / 3) ^ (5 / 6) * (∫⁻ (s : ℝ), H s ^ (3 / 2)) ^ (2 / 3) * ENNReal.ofReal r ^ (5 / κ - 4 / 3)

The normalized cell estimate for a spatially bounded remainder. Its radius exponent is positive throughout the pressure-gradient bootstrap range.