Products in finite mixed norms #
Spatial Hölder followed by time Hölder puts products of two mixed-norm fields in the mixed space with the reciprocal-sum exponents.
theorem
ESS.lps_mixed_two_moment_of_memLp_two
{T : ℝ}
{f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
:
(∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume) ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume ^ 2 < ⊤
A spacetime L² scalar field has a finite L²_t L²_x moment on the
finite time slab.
theorem
ESS.lps_vector_component_mixed_moment
{T p q : ℝ}
{F : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hp : 0 ≤ p)
(hSlice :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t)) (ENNReal.ofReal q) MeasureTheory.volume)
(hMoment :
∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t)) (ENNReal.ofReal q)
MeasureTheory.volume ^ p < ⊤)
(i : Fin 3)
:
(∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t) i) (ENNReal.ofReal q)
MeasureTheory.volume) ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t) i) (ENNReal.ofReal q)
MeasureTheory.volume ^ p < ⊤
A vector-valued mixed moment controls the corresponding mixed moments of all coordinate functions.
theorem
ESS.lps_vector_mixed_moment_of_raw
{T p q : ℝ}
{F : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hq : 0 < q)
(hSlice :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t)) (ENNReal.ofReal q) MeasureTheory.volume)
(hRaw : ∫⁻ (t : ℝ) in Set.Ioo 0 T, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖F (x, t)‖ₑ ^ q) ^ (p / q) < ⊤)
:
∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t)) (ENNReal.ofReal q)
MeasureTheory.volume ^ p < ⊤
A raw vector-valued mixed moment is the corresponding moment of the
spatial eLpNorm on almost every slice.
theorem
ESS.lps_vector_mixed_slice_memLp_of_raw
{T p q : ℝ}
{F : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hp : 0 < p)
(hq : 0 < q)
(hF : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hRaw : ∫⁻ (t : ℝ) in Set.Ioo 0 T, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖F (x, t)‖ₑ ^ q) ^ (p / q) < ⊤)
:
∀ᵐ (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 raw mixed moment gives almost every vector slice membership in
the corresponding spatial L^q space.
theorem
ESS.lps_mixed_product_moment
{T px qx rx pt qt rt : ℝ}
(hpx : 1 ≤ px)
(hqx : 1 ≤ qx)
(hrx : 1 ≤ rx)
(hpt : 1 ≤ pt)
(hqt : 1 ≤ qt)
(hrt : 1 ≤ rt)
(hSpace : px⁻¹ + qx⁻¹ = rx⁻¹)
(hTime : pt⁻¹ + qt⁻¹ = rt⁻¹)
{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 < ⊤)
:
(∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t) * g (x, t)) (ENNReal.ofReal rx)
MeasureTheory.volume) ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t) * g (x, t)) (ENNReal.ofReal rx)
MeasureTheory.volume ^ rt < ⊤
Two finite mixed norms multiply into the mixed norm whose spatial and time reciprocal exponents are the corresponding sums.