Stability Fixed Multiplier

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_tendsto_integral_mul_test_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 μ) (hφ : MeasureTheory.MemLp φ ⊤ μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) 3 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), φ x • F n x ∂μ) Filter.atTop (nhds (∫ (x : α), φ x • G x ∂μ))

A fixed essentially bounded scalar test preserves convergence of the integrals of a strongly L³-convergent sequence (thm:stability).