Large-cell normalization for pressure gradients

For the Morrey quantities in prop:bootstrap, a cell of radius r ≥ r₀ > 0 has normalization at most r₀ ^ (-(5 * (1 - p / q) / p)) when 0 < p ≤ q. Its power integral is bounded by the whole-carrier integral. For p = 6/5, the resulting factor is r₀ ^ (5 / q - 25 / 6) and the integral has power 5/6. The constant is one; the carrier radius enters only through its domain.

The indicator versions hold for every cell centre, including cells crossing the carrier boundary. Both the origin past cylinder and the symmetric parabolic metric ball are treated without any small-cell estimate.

theorem CKN.Core.Step4.morreyCell_indicator_le_carrier_integral_of_large_radius {p q r₀ r : ℝ} {f : Foundation.Parabolic.ParabolicPoint → ℝ} {S : Set Foundation.Parabolic.ParabolicPoint} (hS : MeasurableSet S) (hp : 0 < p) (hpq : p ≤ q) (hr₀ : 0 < r₀) (hr : r₀ ≤ r) (z : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.Morrey.morreyCell p q (S.indicator f) z r ≤ ENNReal.ofReal (r₀ ^ (-(5 * (1 - p / q) / p))) * (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in S, ENNReal.ofReal |f w| ^ p) ^ (1 / p)

Restricting a field to a measurable carrier controls every large cell, including cells that intersect its boundary, as used in prop:bootstrap.

theorem CKN.Core.Step4.morreyCell_origin_cylinder_le_of_large_radius {p q r₀ r R : ℝ} {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hp : 0 < p) (hpq : p ≤ q) (hr₀ : 0 < r₀) (hr : r₀ ≤ r) (z : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.Morrey.morreyCell p q ((Foundation.Parabolic.parabolicCylinder 0 0 R).indicator f) z r ≤ ENNReal.ofReal (r₀ ^ (-(5 * (1 - p / q) / p))) * (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 R, ENNReal.ofReal |f w| ^ p) ^ (1 / p)

The origin past-cylinder carrier in prop:bootstrap has the large-cell bound with constant one and explicit cutoff scale r₀.

theorem CKN.Core.Step4.morreyCell_ball_le_of_large_radius {p q r₀ r R : ℝ} {f : Foundation.Parabolic.ParabolicPoint → ℝ} (z₀ : Foundation.Parabolic.ParabolicPoint) (hp : 0 < p) (hpq : p ≤ q) (hr₀ : 0 < r₀) (hr : r₀ ≤ r) (z : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.Morrey.morreyCell p q ((Metric.ball z₀ R).indicator f) z r ≤ ENNReal.ofReal (r₀ ^ (-(5 * (1 - p / q) / p))) * (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Metric.ball z₀ R, ENNReal.ofReal |f w| ^ p) ^ (1 / p)

The symmetric parabolic-ball carrier in prop:bootstrap has the same large-cell normalization, independently of the carrier centre.

theorem CKN.Core.Step4.pressure_gradient_origin_cylinder_large_cell_le {κ r₀ r R : ℝ} {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hκ : 6 / 5 ≤ κ) (hr₀ : 0 < r₀) (hr : r₀ ≤ r) (z : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.Morrey.morreyCell (6 / 5) κ ((Foundation.Parabolic.parabolicCylinder 0 0 R).indicator f) z r ≤ ENNReal.ofReal (r₀ ^ (5 / κ - 25 / 6)) * (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 R, ENNReal.ofReal |f w| ^ (6 / 5)) ^ (5 / 6)

At pressure-gradient exponent 6/5 in prop:bootstrap, the origin past-cylinder bound has scale power 5/κ - 25/6 and integral power 5/6.

theorem CKN.Core.Step4.pressure_gradient_ball_large_cell_le {κ r₀ r R : ℝ} {f : Foundation.Parabolic.ParabolicPoint → ℝ} (z₀ : Foundation.Parabolic.ParabolicPoint) (hκ : 6 / 5 ≤ κ) (hr₀ : 0 < r₀) (hr : r₀ ≤ r) (z : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.Morrey.morreyCell (6 / 5) κ ((Metric.ball z₀ R).indicator f) z r ≤ ENNReal.ofReal (r₀ ^ (5 / κ - 25 / 6)) * (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Metric.ball z₀ R, ENNReal.ofReal |f w| ^ (6 / 5)) ^ (5 / 6)

At pressure-gradient exponent 6/5 in prop:bootstrap, the symmetric ball bound has scale power 5/κ - 25/6 and integral power 5/6.