Whole-space convergence in the Leray limit

Uniform spatial tightness upgrades the local compactness limit to a global space-time limit, after which the energy-space bound gives the subcritical Lebesgue convergence in prop:leray-limit.

theorem CKN.Leray.lerayLimit_spaceTime_strongLp_of_local_compactness_and_tails (T : ℝ) (F : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (u : 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) (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)

Local compactness and uniform tails yield the whole-space subcritical convergence on a finite time slab, as in prop:leray-limit.

theorem CKN.Leray.lerayLimit_strongLp_of_contraction_and_fixed_limit {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} (F : ℕ → α → E) (u : α → E) (J : ℕ → (α → E) → α → E) (hF : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - u) 3 μ) Filter.atTop (nhds 0)) (hJu : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (J n u - u) 3 μ) Filter.atTop (nhds 0)) (hcontract : ∀ (n : ℕ), MeasureTheory.eLpNorm (J n (F n) - J n u) 3 μ ≤ MeasureTheory.eLpNorm (F n - u) 3 μ) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (J n (F n) - u) 3 μ) Filter.atTop (nhds 0)

Strong convergence of mollified fields follows from contraction and the approximate-identity limit for the fixed field. This is the final estimate in the L³ assertion of prop:leray-limit.