Stability Flux Product

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_flux_product_tendsto {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (F G : ℕ → α → ℝ) (f g φ : α → ℝ) (hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) (3 / 2) μ) (hG : ∀ (n : ℕ), MeasureTheory.MemLp (G n) 3 μ) (hf : MeasureTheory.MemLp f (3 / 2) μ) (hg : MeasureTheory.MemLp g 3 μ) (hφ : MeasureTheory.MemLp φ ⊤ μ) (hFconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - f) (3 / 2) μ) 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 ∂μ))

Strong local convergence of an L^{3/2} field and an L³ field passes their product against a bounded scalar test to the integral limit.