The backward carrier and the time windows that can contribute to it

The one-sided pressure-gradient estimate of prop:bootstrap measures the selected gradient only through the indicator of the backward cylinder parabolicCylinder 0 0 R₁. Every cell of that indicator therefore sees the gradient only on the intersection of the cell with that cylinder, and the time factor of the intersection is contained in (-R₁ ^ 2, 0], whatever the cell centre and radius are.

This module records that geometry. The product decomposition of the intersection separates the spatial and temporal factors; the window inclusion says that the contributing times of a cell always lie in the time factor (-1, 0] of the unit cylinder, so a cell bound stated for the intersection never refers to times outside the region controlled by the data hypothesis of thm:A. The last theorem is the composition with the one-sided Morrey transfer: cell bounds for the gradient restricted to the backward carrier give the Morrey cell output the estimate consumes.

theorem CKN.Core.Step4.parabolicCylinder_origin_eq_prod (R : ℝ) : Foundation.Parabolic.parabolicCylinder 0 0 R = Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioc (-R ^ 2) 0

The backward cylinder at the origin as a space-time product.

theorem CKN.Core.Step4.parabolicCylinder_inter_origin_eq_prod (x : Foundation.Parabolic.Vec3) (t r R : ℝ) : Foundation.Parabolic.parabolicCylinder x t r ∩ Foundation.Parabolic.parabolicCylinder 0 0 R = (Foundation.Parabolic.vec3Ball x r ∩ Foundation.Parabolic.vec3Ball 0 R) ×ˢ (Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R ^ 2) 0)

A cell meets the backward carrier in the product of the intersected spatial balls with the intersected time windows.

theorem CKN.Core.Step4.originClauseWindow_subset_unitTime {R : ℝ} (hR0 : 0 ≤ R) (hR : R ≤ 1) (t r : ℝ) : Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R ^ 2) 0 ⊆ Set.Ioc (-1) 0

Whatever the cell centre and radius, the times of the cell that can contribute to the backward carrier lie in the time factor of the unit cylinder. No restriction on R beyond R ≤ 1 is needed, and in particular none beyond the range 0 < R₁ < R₀ < 3/4 of prop:bootstrap.

theorem CKN.Core.Step4.originClauseWindow_subset_of_unitTime {I : Set ℝ} {R : ℝ} (hR0 : 0 ≤ R) (hR : R ≤ 1) (hI : Set.Icc (-1) 0 ⊆ I) (t r : ℝ) : Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R ^ 2) 0 ⊆ I

Under the domain hypothesis of thm:A the contributing times of every cell lie in the solution interval.

theorem CKN.Core.Step4.cylinderPowerIntegral_carrier_eq {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 a function cut off outside a measurable set is the power integral of the function over the intersection.

theorem CKN.Core.Step4.measurableSet_parabolicCylinder_origin (R : ℝ) : MeasurableSet (Foundation.Parabolic.parabolicCylinder 0 0 R)

The backward carrier is measurable.

theorem CKN.Core.Step4.originCellOutput_of_carrier_cell_bounds {R₁ κ : ℝ} {A B : ENNReal} {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hR₁ : 0 < R₁) (hR₁34 : R₁ < 3 / 4) (hκ : 6 / 5 ≤ κ) (hsmall : ∀ (i : Fin 3), ∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4), ∀ (r : ℝ), 0 < r → r ≤ R₁ → ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r ∩ Foundation.Parabolic.parabolicCylinder 0 0 R₁, ENNReal.ofReal |Dp w i| ^ (6 / 5) ≤ A * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / κ)))) (hglobal : ∀ (i : Fin 3), ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 R₁, ENNReal.ofReal |Dp w i| ^ (6 / 5) ≤ B) : oneSidedPressureGradientOriginCellOutput R₁ κ (Endgame.oneSidedMorreyBound (6 / 5) κ R₁ A B) Dp

Cell bounds for the gradient restricted to the backward carrier, at admissible centres and radii, together with the total integral on the carrier, give the Morrey cell output of prop:bootstrap. This is the one-sided transfer morreyNorm_one_sided_indicator_le_on_cylinder applied to the cut-off field, so it needs no hypothesis about the gradient at times outside (-R₁ ^ 2, 0].