Stability Weak Set Integral #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.stability_tendsto_setIntegral_mul_test_of_weak_Ltwo
{α : Type u_1}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(F : ℕ → α → ℝ)
(G φ : α → ℝ)
(S : Set α)
(hφ : MeasureTheory.MemLp φ ⊤ μ)
(hS : MeasurableSet S)
(hweak :
∀ (w : α → ℝ),
MeasureTheory.MemLp w 2 μ →
Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), F n x * w x ∂μ) Filter.atTop (nhds (∫ (x : α), G x * w x ∂μ)))
:
Weak L² convergence passes a bounded linear pairing through every
measurable restriction of a finite-measure domain.