Stability Quadratic Integral

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_tendsto_integral_quadratic_test {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (F G : ℕ → α → ℝ) (f g φ : α → ℝ) (hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) 3 μ) (hG : ∀ (n : ℕ), MeasureTheory.MemLp (G n) 3 μ) (hf : MeasureTheory.MemLp f 3 μ) (hg : MeasureTheory.MemLp g 3 μ) (hφ : MeasureTheory.MemLp φ ⊤ μ) (hFconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - f) 3 μ) Filter.atTop (nhds 0)) (hGconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (G n - g) 3 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), F n x * G n x * φ x ∂μ) Filter.atTop (nhds (∫ (x : α), f x * g x * φ x ∂μ))

Quadratic velocity pairings against a bounded test converge under strong local L³ convergence.