The small-cell regime: the slice estimate at twice the cell radius

The slice estimate of display eq:pressure-gradient-morrey produces, on a backward cylinder of radius ρ whose closure lies in the space-time domain, a weak spatial derivative of the pressure slice on the half ball of radius ρ / 2. To control a cell of radius r it must therefore be applied at ρ = 2 * r, and this is possible exactly when the doubled cylinder still lies in the region the hypotheses control.

That is the margin-safe regime. For the origin carrier the controlled region is the closed unit cylinder, so the governing condition is r ≤ (1 - R₁) / 4, with a top time in the backward window of the cylinder of admissible centres; for the symmetric carrier of the uniform route it is 3 * r ≤ R. A cell that misses the carrier contributes nothing, because the selected field vanishes there, so only cells meeting the carrier have to be considered, and for those the margin condition is what makes the doubled ball fit.

Cells above the margin scale are not reached by this argument; they belong to the other regime and are bounded by the whole-carrier integral.

theorem CKN.Core.Step4.ae_slice_bound_on_cell_ball_of_double_radius {p : Foundation.Parabolic.ParabolicPoint → ℝ} {i : Fin 3} {x : Foundation.Parabolic.Vec3} {t r : ℝ} {N : ℝ → ENNReal} (hr : 0 < r) (hslice : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - (2 * r) ^ 2) t), ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g (euclideanBall x (2 * r / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (euclideanBall x (2 * r / 2)) i (fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall x (2 * r / 2))) ≤ N s) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t), ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g (Foundation.Parabolic.vec3Ball x r) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball x r) i (fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)) ≤ N s

The slice estimate read at twice the cell radius gives the cell's own ball: the carrier euclideanBall x ((2 * r) / 2) of the estimate is vec3Ball x r, and the cell's time window is contained in the estimate's.

theorem CKN.Core.Step4.cylinderPowerIntegral_le_of_double_radius_slice_bounds {B : Set Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {i : Fin 3} {x : Foundation.Parabolic.Vec3} {t r : ℝ} {N : ℝ → ENNReal} (hr : 0 < r) (hball : Foundation.Parabolic.vec3Ball x r ⊆ B) (hmeas : AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x t r))) (hfield : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) B MeasureTheory.volume ∧ HasWeakPartialDerivOn B i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) (hslice : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - (2 * r) ^ 2) t), ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g (euclideanBall x (2 * r / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (euclideanBall x (2 * r / 2)) i (fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall x (2 * r / 2))) ≤ N s) : Foundation.Parabolic.Morrey.cylinderPowerIntegral (6 / 5) (fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) (x, t) r ≤ ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, N s ^ (6 / 5)

The cell power integral of the selected field at a margin-safe cell, from the slice estimate applied at twice the cell radius. The field is fixed first; almost-everywhere uniqueness of weak partial derivatives transports the estimate's bound to it, and Tonelli integrates the slice bounds over the cell's window.

theorem CKN.Core.Step4.origin_margin_double_radius_slice {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {R₁ : ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {i : Fin 3} {x : Foundation.Parabolic.Vec3} {t r : ℝ} {N : Foundation.Parabolic.Vec3 → ℝ → ℝ → ℝ → ENNReal} (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hR₁ : 0 < R₁) (hR₁unit : R₁ < 1) (hr : 0 < r) (hmargin : r ≤ (1 - R₁) / 4) (hx : Foundation.Parabolic.vec3EuclideanNorm (x - 0) < R₁ + r) (ht : t ∈ Set.Ioc (-(9 / 16)) 0) (hslice : ∀ (c : Foundation.Parabolic.Vec3) (t₀ ρ : ℝ), 0 < ρ → closure (Foundation.Parabolic.parabolicCylinder c t₀ ρ) ⊆ spaceTimeSet Ω I → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀), ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g (euclideanBall c (ρ / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (euclideanBall c (ρ / 2)) i (fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall c (ρ / 2))) ≤ N c t₀ ρ s) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - (2 * r) ^ 2) t), ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g (euclideanBall x (2 * r / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (euclideanBall x (2 * r / 2)) i (fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall x (2 * r / 2))) ≤ N x t (2 * r) s

The doubled cylinder of a margin-safe cell of the origin carrier is admissible for the slice estimate, so the estimate applies at twice the cell radius. The margin is measured against the unit ball, which is the region the domain hypothesis controls, so the scale (1 - R₁) / 4 is bounded below by 1/16 on the admissible range and does not degenerate.

theorem CKN.Core.Step4.symmetric_margin_double_radius_slice {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {z₀ : Foundation.Parabolic.ParabolicPoint} {R : ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {i : Fin 3} {x : Foundation.Parabolic.Vec3} {t r : ℝ} {N : Foundation.Parabolic.Vec3 → ℝ → ℝ → ℝ → ENNReal} (hdom : Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I) (hR : 0 < R) (hr : 0 < r) (hmargin : 3 * r ≤ R) (hmeet : (Foundation.Parabolic.parabolicCylinder x t r ∩ Metric.ball z₀ (R / 2)).Nonempty) (hslice : ∀ (c : Foundation.Parabolic.Vec3) (t₀ ρ : ℝ), 0 < ρ → closure (Foundation.Parabolic.parabolicCylinder c t₀ ρ) ⊆ spaceTimeSet Ω I → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀), ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g (euclideanBall c (ρ / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (euclideanBall c (ρ / 2)) i (fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall c (ρ / 2))) ≤ N c t₀ ρ s) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - (2 * r) ^ 2) t), ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g (euclideanBall x (2 * r / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (euclideanBall x (2 * r / 2)) i (fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall x (2 * r / 2))) ≤ N x t (2 * r) s

The doubled cylinder of a margin-safe cell of the symmetric carrier is admissible for the slice estimate, so the estimate applies at twice the cell radius.

theorem CKN.Core.Step4.origin_margin_cylinderPowerIntegral_le {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {R₁ : ℝ} {Bf : Set Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {i : Fin 3} {x : Foundation.Parabolic.Vec3} {t r : ℝ} {N : Foundation.Parabolic.Vec3 → ℝ → ℝ → ℝ → ENNReal} (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hR₁ : 0 < R₁) (hR₁unit : R₁ < 1) (hr : 0 < r) (hmargin : r ≤ (1 - R₁) / 4) (hmeet : (Foundation.Parabolic.vec3Ball x r ∩ Foundation.Parabolic.vec3Ball 0 R₁).Nonempty) (ht : t ∈ Set.Ioc (-(9 / 16)) 0) (hball : Foundation.Parabolic.vec3Ball x r ⊆ Bf) (hmeas : AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x t r))) (hfield : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) Bf MeasureTheory.volume ∧ HasWeakPartialDerivOn Bf i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) (hslice : ∀ (c : Foundation.Parabolic.Vec3) (t₀ ρ : ℝ), 0 < ρ → closure (Foundation.Parabolic.parabolicCylinder c t₀ ρ) ⊆ spaceTimeSet Ω I → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀), ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g (euclideanBall c (ρ / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (euclideanBall c (ρ / 2)) i (fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall c (ρ / 2))) ≤ N c t₀ ρ s) : Foundation.Parabolic.Morrey.cylinderPowerIntegral (6 / 5) (fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) (x, t) r ≤ ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, N x t (2 * r) s ^ (6 / 5)

The small-cell regime of the origin carrier. A cell that meets the carrier ball, at a radius at most a quarter of the margin 1 - R₁ between the carrier and the unit ball and with a top time in the backward window of the cylinder of admissible centres, has its power integral bounded by the time integral of the slice majorant taken at twice the cell radius.

theorem CKN.Core.Step4.symmetric_margin_indicator_cylinderPowerIntegral_le {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {z₀ : Foundation.Parabolic.ParabolicPoint} {R : ℝ} {B : Set Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {i : Fin 3} {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} {N : Foundation.Parabolic.Vec3 → ℝ → ℝ → ℝ → ENNReal} (hdom : Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I) (hR : 0 < R) (hr : 0 < r) (hmargin : 3 * r ≤ R) (hball : Foundation.Parabolic.vec3Ball z.1 r ⊆ B) (hmeas : AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 r))) (hfield : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - r ^ 2) z.2), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) B MeasureTheory.volume ∧ HasWeakPartialDerivOn B i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) (hslice : ∀ (c : Foundation.Parabolic.Vec3) (t₀ ρ : ℝ), 0 < ρ → closure (Foundation.Parabolic.parabolicCylinder c t₀ ρ) ⊆ spaceTimeSet Ω I → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀), ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g (euclideanBall c (ρ / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (euclideanBall c (ρ / 2)) i (fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall c (ρ / 2))) ≤ N c t₀ ρ s) : Foundation.Parabolic.Morrey.cylinderPowerIntegral (6 / 5) ((Metric.ball z₀ (R / 2)).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) z r ≤ ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2, N z.1 z.2 (2 * r) s ^ (6 / 5)

The small-cell regime of the symmetric carrier. A cell of radius at most a third of R has the power integral of the field restricted to the inner ball bounded by the time integral of the slice majorant taken at twice the cell radius. A cell disjoint from the inner ball carries no mass at all, so no geometric hypothesis is needed for it.