Stability S1Weak Gradient

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_s1_weak_gradient_on_localBox {Ω Ω' : 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) (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))) (hDuWeak : ∀ (i j : Fin 3) (w : Foundation.Parabolic.Vec3 × ℝ → ℝ), MeasureTheory.MemLp w 2 ((MeasureTheory.volume.restrict Ω').prod (MeasureTheory.volume.restrict J)) → Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.Vec3 × ℝ), Du n (z.1, z.2) i j * w z ∂(MeasureTheory.volume.restrict Ω').prod (MeasureTheory.volume.restrict J)) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.Vec3 × ℝ), Dv (z.1, z.2) i j * w z ∂(MeasureTheory.volume.restrict Ω').prod (MeasureTheory.volume.restrict J)))) (i : Fin 3) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, HasWeakGradientOn Ω' (fun (x : Vec 3) => v (x, t) i) fun (x : Vec 3) => Dv (x, t) i

The weak-gradient clause of (S1) is preserved by the convergences in thm:stability; it need not be assumed for the limit.