One-sided transfer with carrier-centred cells

The cells that the one-sided transfer actually consumes are the ones centred in the carrier cylinder itself: each small cylinder meeting the carrier has a truncated centre that already lies in the carrier, so the growth input can be, and here is, restricted to the carrier's own centres rather than to a larger fixed cylinder. The transfer still covers every cell, because cells whose centre is not met by the carrier contribute nothing, and cells at or above the fixed scale are handled by the total integral on the carrier.

theorem CKN.Core.Step4.exists_one_sided_covering_cylinder_on_carrier {a : ℝ} {w : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hmeet : (Foundation.Parabolic.parabolicCylinder w.1 w.2 ρ ∩ Foundation.Parabolic.parabolicCylinder 0 0 a).Nonempty) : ∃ c ∈ Foundation.Parabolic.parabolicCylinder 0 0 a, Foundation.Parabolic.parabolicCylinder w.1 w.2 ρ ∩ {z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0} ⊆ Foundation.Parabolic.parabolicCylinder c.1 c.2 (2 * ρ)

Any cylinder meeting the carrier cylinder has a truncated centre inside the carrier whose doubled-radius cylinder covers the cylinder's whole portion below time zero.

theorem CKN.Core.Step4.cylinderPowerIntegral_indicator_inter {P : ℝ} (hP : 0 < P) {S : Set Foundation.Parabolic.ParabolicPoint} (hS : MeasurableSet S) (g : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : Foundation.Parabolic.Morrey.cylinderPowerIntegral P (S.indicator g) z r = ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r ∩ S, ENNReal.ofReal |g w| ^ P

The power integral of an indicator is the integral of the power of the function over the cylinder intersected with the underlying set.

theorem CKN.Core.Step4.morreyNorm_one_sided_indicator_le_of_carrier_cells (a P τ ρ₀ : ℝ) (A B : ENNReal) (hP : 1 ≤ P) (hPτ : P ≤ τ) (hρ₀ : 0 < ρ₀) (g : Foundation.Parabolic.ParabolicPoint → ℝ) (hsmall : ∀ c ∈ Foundation.Parabolic.parabolicCylinder 0 0 a, ∀ (r : ℝ), 0 < r → r ≤ ρ₀ → Foundation.Parabolic.Morrey.cylinderPowerIntegral P g c r ≤ A * ENNReal.ofReal (r ^ (5 * (1 - P / τ)))) (hglobal : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 a, ENNReal.ofReal |g w| ^ P ≤ B) : Foundation.Parabolic.Morrey.morreyNorm P τ ((Foundation.Parabolic.parabolicCylinder 0 0 a).indicator g) ≤ Endgame.oneSidedMorreyBound P τ ρ₀ A B

Small-scale cylinder estimates at carrier centres and a total integral bound on the carrier imply an explicit Morrey estimate for the one-sided indicator of the carrier, with no upper bound on the carrier radius.