Transport from a power integral to the Lp seminorm #
The scalar conversion requires measurability of only the two actual functions. A finite input seminorm then gives a finite output seminorm.
theorem
CKN.Core.Endgame.eLpNorm_bound_of_absE_power_bound
{f g : Foundation.Parabolic.Vec3 → ℝ}
{C p : ℝ}
(hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
(hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume)
(hp : 0 < p)
(hbound :
∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE g x ^ p ≤ ENNReal.ofReal C * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x ^ p)
:
A power-integral estimate gives the corresponding scalar Lp seminorm estimate for two actual a.e. strongly measurable functions.
theorem
CKN.Core.Endgame.memLp_of_absE_power_bound
{f g : Foundation.Parabolic.Vec3 → ℝ}
{C p : ℝ}
(hf : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume)
(hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume)
(hp : 0 < p)
(hbound :
∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE g x ^ p ≤ ENNReal.ofReal C * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x ^ p)
:
A power-integral estimate transports finite Lp membership to its actual output function.