Stability Finite Sum Integral

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_tendsto_integral_finsetSum {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Finset ι) (F : ℕ → ι → α → ℝ) (G : ι → α → ℝ) (hF : ∀ (n : ℕ), ∀ i ∈ s, MeasureTheory.Integrable (F n i) μ) (hG : ∀ i ∈ s, MeasureTheory.Integrable (G i) μ) (hconv : ∀ i ∈ s, Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), F n i x ∂μ) Filter.atTop (nhds (∫ (x : α), G i x ∂μ))) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), ∑ i ∈ s, F n i x ∂μ) Filter.atTop (nhds (∫ (x : α), ∑ i ∈ s, G i x ∂μ))

A finite sum of integrable scalar pairings preserves convergence of its integrals.