Stability Pressure Fixed Multiplier

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_tendsto_integral_mul_test_of_LthreeHalves {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (F : ℕ → α → ℝ) (G φ : α → ℝ) (hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) (3 / 2) μ) (hφ : MeasureTheory.MemLp φ ⊤ μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) (3 / 2) μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), φ x * F n x ∂μ) Filter.atTop (nhds (∫ (x : α), φ x * G x ∂μ))

A bounded scalar test preserves convergence of pressure integrals under strong local L^{3/2} convergence.