Stability Set Integral Convergence

Supporting estimates for the Navier–Stokes development.

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

Strong local L³ convergence passes to a bounded linear pairing on every measurable subset of a finite-measure domain.