Stability Component Convergence

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_tendsto_eLpNorm_component_three {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {ι : Type u_2} [Fintype ι] (F : ℕ → α → ι → ℝ) (G : α → ι → ℝ) (hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) 3 μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) 3 μ) Filter.atTop (nhds 0)) (i : ι) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => F n x i - G x i) 3 μ) Filter.atTop (nhds 0)

Strong L³ convergence of a finite vector field passes to each component (thm:stability).