Leray Limit Slices

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayLimit_globalWeakLp_of_compactSupport {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [PseudoMetricSpace α] [BorelSpace α] [R1Space α] [WeaklyLocallyCompactSpace α] {μ : MeasureTheory.Measure α} [μ.Regular] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (F : ℕ → α → E) (G : α → E) (hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) 2 μ) (hG : MeasureTheory.MemLp G 2 μ) (C : ℝ) (hC : 0 ≤ C) (hFbound : ∀ (n : ℕ), ‖MeasureTheory.MemLp.toLp (F n) ⋯‖ ≤ C) (hGbound : ‖MeasureTheory.MemLp.toLp G hG‖ ≤ C) (hlocal : ∀ (v : α → E), HasCompactSupport v → Continuous v → ∀ (hv : MeasureTheory.MemLp v 2 μ), Filter.Tendsto (fun (n : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (F n) ⋯) (MeasureTheory.MemLp.toLp v hv)) Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp G hG) (MeasureTheory.MemLp.toLp v hv)))) (w : α → E) (hw : MeasureTheory.MemLp w 2 μ) : Filter.Tendsto (fun (n : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (F n) ⋯) (MeasureTheory.MemLp.toLp w hw)) Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp G hG) (MeasureTheory.MemLp.toLp w hw)))

Weak convergence against compactly supported tests extends to all global L² tests when the sequence and limit have a common global norm bound.