Stability Integral Convergence

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_tendsto_integral_of_Lthree {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (F : ℕ → α → E) (G : α → E) (hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) 3 μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) 3 μ) 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³ convergence implies convergence of Bochner integrals. This is the linear limit step in (S2) and (S3) of thm:stability.