Mixed norm convergence under spatial mollification

Spatial mollification converges in finite mixed Lebesgue norms on a finite time slab. The spatial and temporal exponents may differ.

theorem ESS.lps_mollify_mixed_norm_tendsto {T p q : ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hp : 1 ≤ p) (hq : 1 ≤ q) (hf : MeasureTheory.AEStronglyMeasurable f (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 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 < ⊤) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => serrinSM f n (x, t) - f (x, t)) (ENNReal.ofReal q) MeasureTheory.volume ^ p) Filter.atTop (nhds 0)

Slice-wise spatial mollification converges in the mixed norm L^p_t L^q_x when both exponents are finite and at least one.