Leray Limit Tightness

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayLimit_eLpNorm_tendsto_of_local_and_uniform_tails {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} (F : ℕ → α → E) (G : α → E) (K : ℕ → Set α) (hK : ∀ (m : ℕ), MeasurableSet (K m)) (hlocal : ∀ (m : ℕ), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) 2 (μ.restrict (K m))) Filter.atTop (nhds 0)) (hFtail : ∀ (ε : ENNReal), 0 < ε → ∀ᶠ (m : ℕ) in Filter.atTop, ∀ (n : ℕ), MeasureTheory.eLpNorm ((K m)ᶜ.indicator (F n)) 2 μ ≤ ε) (hGtail : ∀ (ε : ENNReal), 0 < ε → ∀ᶠ (m : ℕ) in Filter.atTop, MeasureTheory.eLpNorm ((K m)ᶜ.indicator G) 2 μ ≤ ε) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) 2 μ) Filter.atTop (nhds 0)

Local L² convergence becomes global when the discarded part is uniformly small for the sequence and its limit.