Time integrals on clipped origin cells

The time integrals in prop:bootstrap use the spatial intersection of a cell with the origin carrier and the corresponding intersection of backward time windows. Tonelli identifies these integrals with the carrier-restricted space-time mass without extending any data outside the carrier.

theorem CKN.Core.Step4.origin_time_slice_norm_power_eq {P : ℝ} (hP : 0 < P) {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {E : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hg : AEMeasurable g (MeasureTheory.volume.restrict (E ×ˢ J))) : ∫⁻ (s : ℝ) in J, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => g (y, s)) (ENNReal.ofReal P) (MeasureTheory.volume.restrict E) ^ P = ∫⁻ (w : Foundation.Parabolic.Vec3 × ℝ) in E ×ˢ J, ENNReal.ofReal |g w| ^ P

The time integral of the powers of spatial slice norms equals the space-time power integral on an arbitrary product box.

theorem CKN.Core.Step4.origin_time_slice_norm_aemeasurable {P : ℝ} (hP : 0 < P) {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {E : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hg : AEMeasurable g (MeasureTheory.volume.restrict (E ×ˢ J))) : AEMeasurable (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => g (y, s)) (ENNReal.ofReal P) (MeasureTheory.volume.restrict E)) (MeasureTheory.volume.restrict J)

Spatial slice norms are measurable on the chosen time window whenever the scalar field is measurable on the product box.

theorem CKN.Core.Step4.origin_clipped_slice_norm_power_eq {P : ℝ} (hP : 0 < P) {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (R : ℝ) (hg : AEMeasurable g (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 R))) (x : Foundation.Parabolic.Vec3) (t r : ℝ) : ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => g (y, s)) (ENNReal.ofReal P) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r ∩ Foundation.Parabolic.vec3Ball 0 R)) ^ P = Foundation.Parabolic.Morrey.cylinderPowerIntegral P ((Foundation.Parabolic.parabolicCylinder 0 0 R).indicator g) (x, t) r

Clipped time and spatial slice norms have exactly the power integral of the origin-carrier indicator, for every cell centre and radius.

theorem CKN.Core.Step4.origin_clipped_slice_norm_time_bound {P κ R : ℝ} {K : ENNReal} {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hP : 0 < P) (hg : AEMeasurable g (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 R))) (hK : Foundation.Parabolic.Morrey.morreyNorm P κ ((Foundation.Parabolic.parabolicCylinder 0 0 R).indicator g) ≤ K) (x : Foundation.Parabolic.Vec3) (t : ℝ) {r : ℝ} (hr : 0 < r) : ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => g (y, s)) (ENNReal.ofReal P) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r ∩ Foundation.Parabolic.vec3Ball 0 R)) ^ P ≤ K ^ P * ENNReal.ofReal (r ^ (5 * (1 - P / κ)))

A source Morrey bound gives the exact clipped time-power growth used by the origin data clause. The constant is independent of the cell.