Stability S4

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_suitable_energy {Ω : Set Foundation.Parabolic.Vec3} {I : 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) (hdata : IsSuitableWeakSolutionData Ω I q v Dv r 0) (huConv : ∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I Ω' J → Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (u n - v) 3 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) Filter.atTop (nhds 0)) (hDv : ∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I Ω' J → MeasureTheory.MemLp Dv 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hDuWeak : ∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I Ω' J → ∀ (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)))) (hpConv : ∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I Ω' J → Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (p n - r) (3 / 2) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) Filter.atTop (nhds 0)) (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) : ψ ∈ spaceTimeTestFunction Ω I → (∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ ψ z) → 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, spatialGradientSq v Dv z * ψ z ≤ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + (Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + 2 * r z) * ∑ i : Fin 3, v z i * spatialPartial ψ i z + (2 * ∑ i : Fin 3, 0 z i * v z i) * ψ z

The local energy inequality (S4) passes to the limit through strong velocity and pressure convergence and weak gradient convergence.