Stability Pressure Integral Convergence

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_tendsto_integral_of_LthreeHalves {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (F : ℕ → α → ℝ) (G : α → ℝ) (hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) (3 / 2) μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) (3 / 2) μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), F n x ∂μ) Filter.atTop (nhds (∫ (x : α), G x ∂μ))

On a finite-measure set, strong L^{3/2} convergence passes to scalar integrals.