Leray Limit Interpolation

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayLimit_strongLp_of_strongL2_and_uniform_high {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {F : ℕ → α → E} {G : α → E} (hFlow : ∀ (n : ℕ), MeasureTheory.MemLp (F n) (ENNReal.ofReal 2) μ) (hbound : ∃ B < ⊤, ∀ (n : ℕ), MeasureTheory.eLpNorm (F n) (ENNReal.ofReal (10 / 3)) μ ≤ B) (h2 : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) (ENNReal.ofReal 2) μ) Filter.atTop (nhds 0)) (q : ℝ) : 2 ≤ q → q < 10 / 3 → Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) (ENNReal.ofReal q) μ) Filter.atTop (nhds 0)

A strong global L² limit and a uniform global L^(10/3) bound give strong convergence in each intermediate exponent on an arbitrary measure space.