Mixed norm pairings on shorter time slabs #
Finite mixed norm mollification limits restrict from a full time slab to every shorter slab. This is the pairing limit used in cross-testing at an almost every terminal time.
theorem
ESS.lps_mixed_cutoff_pairing_limit_slab
{T t px qx pt qt : ℝ}
(ht : t ≤ T)
(hpx1 : 1 ≤ px)
(hqx1 : 1 ≤ qx)
(hpt1 : 1 ≤ pt)
(hqt1 : 1 ≤ 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 :
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, τ)) (ENNReal.ofReal px) MeasureTheory.volume)
(hgSlice :
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, τ)) (ENNReal.ofReal qx) MeasureTheory.volume)
(hfMoment :
∫⁻ (τ : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, τ)) (ENNReal.ofReal px)
MeasureTheory.volume ^ pt < ⊤)
(hgMoment :
∫⁻ (τ : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, τ)) (ENNReal.ofReal qx)
MeasureTheory.volume ^ qt < ⊤)
:
(∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
serrinCutoff n (CKN.Foundation.Parabolic.parabolicHomeomorph z).1 * serrinSM f n z * serrinSM g n z)
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) ∧ Filter.Tendsto
(fun (n : ℕ) =>
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), serrinCutoff n (CKN.Foundation.Parabolic.parabolicHomeomorph z).1 * serrinSM f n z * serrinSM g n z)
Filter.atTop
(nhds (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), f z * g z))
The cutoff-weighted pairing of two spatial mollifications converges on every shorter slab when the factors have conjugate finite mixed norms.