Slice decomposition of the power integral on a parabolic cylinder #
The power integral over a backward parabolic cylinder is the time integral of
the power integrals of its spatial slices. Consequently a bound on the L^P
norm of almost every spatial slice controls the full cylinder power integral.
theorem
CKN.Core.Step4.cylinderPowerIntegral_eq_lintegral_slices
{P : ℝ}
(hP : 0 < P)
{g : Foundation.Parabolic.ParabolicPoint → ℝ}
{x : Foundation.Parabolic.Vec3}
{t r : ℝ}
(hmeas : AEMeasurable g (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x t r)))
:
The power integral of a parabolic cylinder is the time integral of its spatial slices.
theorem
CKN.Core.Step4.cylinderPowerIntegral_le_of_slice_eLpNorm
{P : ℝ}
(hP : 0 < P)
{g : Foundation.Parabolic.ParabolicPoint → ℝ}
{x : Foundation.Parabolic.Vec3}
{t r : ℝ}
{M : ℝ → ENNReal}
(hmeas : AEMeasurable g (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x t r)))
(hslice :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t), MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => g (y, s)) (ENNReal.ofReal P)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)) ≤ M s)
:
Slicewise L^P bounds integrate to a bound on the cylinder power
integral.