Cutoff pairings for finite mixed norms

Spatial mollification converges in conjugate finite mixed norms. The cutoff pairing then converges by mixed Hölder and dominated convergence.

theorem ESS.lps_mixed_cutoff_pairing_limit {T px qx pt qt : ℝ} (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 : ∀ᵐ (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 < ⊤) : (∀ᶠ (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 when the factors have conjugate finite mixed norms.