Stability Energy Pressure

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_energy_pressureTerm_tendsto {Ω Ω' : 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) (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)) (hpConv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (p n - r) (3 / 2) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) Filter.atTop (nhds 0)) (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (hψ : ψ ∈ spaceTimeTestFunction Ω I) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ∑ j : Fin 3, p n z * u n z j * spatialPartial ψ j z) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ∑ j : Fin 3, r z * v z j * spatialPartial ψ j z))

The pressure flux in (S4) converges under strong local convergence of the pressure and velocity.