Product-box power integrals and their spatial slices

This module records the product-box form of the slice decomposition of a power integral. For a nonnegative function on Vec3 × ℝ and arbitrary sets E of space points and F of times, the integral of the power |g| ^ P over the box E ×ˢ F equals the integral over F of the spatial power integrals of the slices y ↦ g (y, s).

The second result turns an almost-everywhere bound on the L^P norm of the spatial slices into a bound on the power integral over the whole box. Both are stated for an arbitrary spatial set and an arbitrary time set; no geometry of a ball or a backward time window is used.

theorem CKN.Core.Step4.prodPowerIntegral_eq_lintegral_slices {P : ℝ} {g : Foundation.Parabolic.ParabolicPoint → ℝ} {E : Set Foundation.Parabolic.Vec3} {F : Set ℝ} (hmeas : AEMeasurable g (MeasureTheory.volume.restrict (E ×ˢ F))) : ∫⁻ (w : Foundation.Parabolic.Vec3 × ℝ) in E ×ˢ F, ENNReal.ofReal |g w| ^ P = ∫⁻ (s : ℝ) in F, ∫⁻ (y : Foundation.Parabolic.Vec3) in E, ENNReal.ofReal |g (y, s)| ^ P

The power integral over a product box is the time integral of its spatial slices. No positivity hypothesis is needed on the exponent P.

theorem CKN.Core.Step4.prodPowerIntegral_le_of_slice_eLpNorm {P : ℝ} (hP : 0 < P) {g : Foundation.Parabolic.ParabolicPoint → ℝ} {E : Set Foundation.Parabolic.Vec3} {F : Set ℝ} {M : ℝ → ENNReal} (hmeas : AEMeasurable g (MeasureTheory.volume.restrict (E ×ˢ F))) (hslice : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict F, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => g (y, s)) (ENNReal.ofReal P) (MeasureTheory.volume.restrict E) ≤ M s) : ∫⁻ (w : Foundation.Parabolic.Vec3 × ℝ) in E ×ˢ F, ENNReal.ofReal |g w| ^ P ≤ ∫⁻ (s : ℝ) in F, M s ^ P

An almost-everywhere bound on the spatial L^P norms of the slices bounds the power integral over the whole product box by the time integral of the P-th powers of the bounds.