Space-time L¹ limits from fixed-time domination

A family of space-time functions converges in L¹ of the slab once the spatial L¹ distances to the limit are dominated by a fixed integrable time profile and tend to zero at almost every time. This is the dominated-convergence step of the endpoint density passage in lem:lps-comparison.

theorem ESS.lps_slab_integral_tendsto_of_slice_domination {T : ℝ} {F : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {G : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {D : ℝ → ENNReal} (hF : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hG : MeasureTheory.Integrable G (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hD : ∫⁻ (t : ℝ) in Set.Ioo 0 T, D t ≠ ⊤) (hbound : ∀ (n : ℕ), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖F n (x, t) - G (x, t)‖ₑ ≤ D t) (hlim : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖F n (x, t) - G (x, t)‖ₑ) Filter.atTop (nhds 0)) : (∀ (n : ℕ), MeasureTheory.Integrable (F n) (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), F n z) Filter.atTop (nhds (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), G z))

Slice-wise domination and slice-wise convergence of the spatial L¹ distances give integrability and convergence of the space-time integrals.