Leray Limit Convergence

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayLimit_spaceTime_outputs (T : ℝ) (F : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (J : ℕ → (Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (K : ℕ → Set Foundation.Parabolic.ParabolicPoint) (hK : ∀ (m : ℕ), MeasurableSet (K m)) (hlocal : ∀ (m : ℕ), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - u) 2 ((MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))).restrict (K m))) Filter.atTop (nhds 0)) (hFtail : ∀ (ε : ENNReal), 0 < ε → ∀ᶠ (m : ℕ) in Filter.atTop, ∀ (n : ℕ), MeasureTheory.eLpNorm ((K m)ᶜ.indicator (F n)) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ≤ ε) (huTail : ∀ (ε : ENNReal), 0 < ε → ∀ᶠ (m : ℕ) in Filter.atTop, MeasureTheory.eLpNorm ((K m)ᶜ.indicator u) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ≤ ε) (hEnergy : ∀ (n : ℕ), MeasureTheory.MemLp (F n) (ENNReal.ofReal 2) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hTenThirds : ∃ B < ⊤, ∀ (n : ℕ), MeasureTheory.eLpNorm (F n) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ≤ B) (hFthree : ∀ (n : ℕ), MeasureTheory.MemLp (F n) (ENNReal.ofReal 3) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hJthree : ∀ (n : ℕ), MeasureTheory.MemLp (J n (F n)) (ENNReal.ofReal 3) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hJu : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (J n u - u) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0)) (hcontract : ∀ (n : ℕ), MeasureTheory.eLpNorm (J n (F n) - J n u) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ≤ MeasureTheory.eLpNorm (F n - u) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) : (∀ (q : ℝ), 2 ≤ q → q < 10 / 3 → Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - u) (ENNReal.ofReal q) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0)) ∧ MeasureTheory.MemLp u (ENNReal.ofReal 3) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ (∀ (n : ℕ), MeasureTheory.MemLp (J n (F n)) (ENNReal.ofReal 3) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (J n (F n) - u) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0)

Whole-space tails and the uniform energy-space bound yield all subcritical strong convergences, including strong convergence of the regularized transport fields in L³.