Stability S1Local Core

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_s1_local_integrability {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} {q : ℝ} (u : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : ℕ → Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : ℕ → Foundation.Parabolic.ParabolicPoint → ℝ) (v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Dv : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (r : Foundation.Parabolic.ParabolicPoint → ℝ) (hsol : ∀ (n : ℕ), IsSuitableWeakSolution Ω I q (u n) (Du n) (p n) 0) (hbox : localBox Ω I Ω' J) (huConv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (u n - v) 3 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) Filter.atTop (nhds 0)) (hDv : MeasureTheory.MemLp Dv 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hpConv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (p n - r) (3 / 2) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) Filter.atTop (nhds 0)) (M : ENNReal) (hM : M < ⊤) (hbound : ∀ (n : ℕ), essSup (fun (t : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3) in Ω', ‖u n (x, t)‖ₑ ^ 2) (MeasureTheory.volume.restrict J) ≤ M) : MeasureTheory.AEStronglyMeasurable v (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)) ∧ MeasureTheory.AEStronglyMeasurable Dv (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)) ∧ MeasureTheory.AEStronglyMeasurable r (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)) ∧ essSup (fun (t : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3) in Ω', ‖v (x, t)‖ₑ ^ 2) (MeasureTheory.volume.restrict J) < ⊤ ∧ ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 < ⊤ ∧ MeasureTheory.MemLp r (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

Strong velocity and pressure convergence, weak-gradient L² membership, and the uniform slice bound provide the local integrability clauses of (S1) in thm:stability.