Products in mixed Lebesgue spaces #
Spatial and temporal Hölder inequalities show that conjugate mixed norms control the space-time integral of a product.
theorem
ESS.lps_mixed_eLpNorm_formula
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
{q : ℝ}
(hq : 0 < q)
(hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
:
MeasureTheory.eLpNorm f (ENNReal.ofReal q) MeasureTheory.volume = (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖f x‖ₑ ^ q) ^ (1 / q)
The Lq norm of a scalar function through the lower integral of its q-th power.
theorem
ESS.lps_mixed_slice_memLp_ae
{T p q : ℝ}
{f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hp : 0 < p)
(hq : 0 < q)
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hMoment :
∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) (ENNReal.ofReal q)
MeasureTheory.volume ^ p < ⊤)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) (ENNReal.ofReal q) MeasureTheory.volume
A finite mixed-norm moment gives almost-everywhere finite spatial slices.
theorem
ESS.lps_mixed_product_integrable
{T px qx pt qt : ℝ}
(hpx : 0 < px)
(hqx : 0 < qx)
(hpt : 0 < pt)
(hqt : 0 < qt)
(hSpace : px.HolderConjugate qx)
(hTime : pt.HolderConjugate qt)
{f g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hfSlice :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) (ENNReal.ofReal px) MeasureTheory.volume)
(hgSlice :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t)) (ENNReal.ofReal qx) MeasureTheory.volume)
(hfMoment :
∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) (ENNReal.ofReal px)
MeasureTheory.volume ^ pt < ⊤)
(hgMoment :
∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t)) (ENNReal.ofReal qx)
MeasureTheory.volume ^ qt < ⊤)
:
MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => f z * g z)
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ‖f z * g z‖ₑ ≤ (∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) (ENNReal.ofReal px)
MeasureTheory.volume ^ pt) ^ (1 / pt) * (∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t)) (ENNReal.ofReal qx)
MeasureTheory.volume ^ qt) ^ (1 / qt)
Conjugate finite mixed norms make a product integrable on the space-time slab, with its integral controlled by the product of the time mixed norms.