From margin cells to all cells in the origin A slot of prop:bootstrap

The clipped cell estimate of prop:bootstrap for the spatial pressure gradient is proved directly only on margin cells: cells whose centre lies in the closure of the origin carrier of radius R₁ and whose radius is at most (1 - R₁)/4. This file removes both restrictions, at the cost of one absolute factor on the Calderón–Zygmund constant.

The clipped time integral of the 6/5 power of the spatial L^{6/5} slice norm is the space-time mass of |∂ᵢp|^{6/5} over the cell clipped to the carrier, so it is monotone in the cell. Two comparisons then suffice.

• A cell of radius at most (1 - R₁)/8 clipped to the carrier is contained in a margin cell of twice the radius centred in the carrier. Doubling the radius costs the factor 2^θ ≤ 8, since the growth exponent θ of prop:bootstrap is at most 71/25.
• A cell of radius larger than (1 - R₁)/8 is bounded by the whole clipped carrier mass, and the carrier is covered by 197³ · 4611 margin cells of radius exactly (1 - R₁)/8, each of which is smaller than the given radius, so the growth factor only improves.

Both costs are absolute, and the affine slot originKPAffineASlot is superhomogeneous in |C_CZ| + 1, so both are absorbed by requiring C_CZ ≥ originASlotLargeCellThreshold Cbase. Nothing else is assumed: the centre of the given cell is arbitrary and its radius is arbitrary.

def CKN.Core.Step4.originASlotLargeCellThreshold (Cbase : ℝ) : ℝ

The Calderón–Zygmund threshold at which every clipped cell of the origin carrier inherits the margin-cell A slot: the number of margin cells used to cover the carrier, times the constant of the margin-cell estimate.

Equations

• CKN.Core.Step4.originASlotLargeCellThreshold Cbase = 35252814903 * (|Cbase| + 1)

theorem CKN.Core.Step4.originKPAffineASlot_cover_count_mul_le {q ε Cbase C_CZ : ℝ} {KU KD : ENNReal} (hthreshold : originASlotLargeCellThreshold Cbase ≤ C_CZ) : 35252814903 * originKPAffineASlot q Cbase ε KU KD ≤ originKPAffineASlot q C_CZ ε KU KD

The threshold multiplies the affine slot by the cover count.

theorem CKN.Core.Step4.originASlot_clipped_cell_of_margin_cells {q τ R₁ ε Cbase C_CZ : ℝ} {KU KD : ENNReal} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (hτhi : τ ≤ 25) (hR₁ : 0 < R₁) (hR₁lt : R₁ < 3 / 4) (hthreshold : originASlotLargeCellThreshold Cbase ≤ C_CZ) {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hDp : Measurable Dp) (i : Fin 3) (hmargin : ∀ w ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁), ∀ (ρ : ℝ), 0 < ρ → ρ ≤ (1 - R₁) / 4 → ∫⁻ (s : ℝ) in Set.Ioc (w.2 - ρ ^ 2) w.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball w.1 ρ ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ originKPAffineASlot q Cbase ε KU KD * ENNReal.ofReal (ρ ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 < r) : ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))

Margin cells control every cell. Given the clipped A-slot estimate of prop:bootstrap on margin cells at the constant Cbase, every clipped cell — any centre, any positive radius — obeys the same estimate at any constant above originASlotLargeCellThreshold Cbase.

theorem CKN.Core.Step4.theoremA_aSlot_integral_of_margin_cells (Cbase : ℝ) (hCbase : 0 ≤ Cbase) (hmargin : ∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal), 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → 0 ≤ C_CZ → Cbase ≤ C_CZ → 0 < R₁ → R₁ < R₀ → R₀ < 3 / 4 → 0 ≤ ε → KU < ⊤ → KD < ⊤ → ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → (∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) → (∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε → ∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), Measurable Dp → (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) → ∀ (i : Fin 3), ∀ z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁), ∀ (r : ℝ), 0 < r → r ≤ (1 - R₁) / 4 → ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))) (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal) : 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → 0 ≤ C_CZ → originASlotLargeCellThreshold Cbase ≤ C_CZ → 0 < R₁ → R₁ < R₀ → R₀ < 3 / 4 → 0 ≤ ε → KU < ⊤ → KD < ⊤ → ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → (∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) → (∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε → ∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), Measurable Dp → (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) → ∀ (i : Fin 3), ∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4), ∀ (r : ℝ), 0 < r → r ≤ R₁ → ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))

The A slot of prop:bootstrap above the threshold. The clipped component-cell estimate for every centre in Q(3/4) and every radius 0 < r ≤ R₁ follows from its margin-cell restriction — centres in the closure of the carrier, radii at most (1 - R₁)/4 — once the Calderón–Zygmund constant is at least originASlotLargeCellThreshold Cbase. No hypothesis on the solution beyond those of the margin-cell estimate is used.