Time integrability on fixed pressure carriers #
The 3/2 power of a spatial norm, integrated in time over a fixed local box,
is the space-time power integral on that box: Tonelli exchanges the two. The
finiteness that identity delivers is stable under a finite fixed coefficient
and under extending the time window by zero. The coefficients below are fixed
before the time integral; no shrinking-cell growth is asserted.
theorem
CKN.Core.Step4.glued_slice_norm_power_integral
{B : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{a : ℝ}
(ha : 0 < a)
(hF : MeasureTheory.AEStronglyMeasurable F ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict J)))
:
AEMeasurable
(fun (t : ℝ) =>
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) (ENNReal.ofReal a)
(MeasureTheory.volume.restrict B))
(MeasureTheory.volume.restrict J) ∧ ∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) (ENNReal.ofReal a)
(MeasureTheory.volume.restrict B) ^ a = ∫⁻ (z : Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ J, ‖F z‖ₑ ^ a
Tonelli identifies the time integral of spatial norm powers with the space-time power integral on the same product box.
theorem
CKN.Core.Step4.glued_time_indicator_power
{J : Set ℝ}
{K : ℝ → ENNReal}
(hJ : MeasurableSet J)
(hm : AEMeasurable K (MeasureTheory.volume.restrict J))
(hp : ∫⁻ (t : ℝ) in J, K t ^ (3 / 2) < ⊤)
:
Zero extension in time gives precisely a global measurable majorant
with finite 3/2 time power integral.