Stability Energy Decompose

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_energy_rhs_decompose_localBox {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} {q : ℝ} {v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Dv : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {r : Foundation.Parabolic.ParabolicPoint → ℝ} (hdata : IsSuitableWeakSolutionData Ω I q v Dv r 0) (hbox : localBox Ω I Ω' J) (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (hψ : ψ ∈ spaceTimeTestFunction Ω I) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, 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 = ((∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ∑ i : Fin 3, v z i * v z i * (timePartial ψ z + ∑ j : Fin 3, spatialSecondPartial ψ j j z)) + ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ∑ i : Fin 3, ∑ j : Fin 3, v z i * v z i * v z j * spatialPartial ψ j z) + 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ∑ j : Fin 3, r z * v z j * spatialPartial ψ j z

On a local box, the zero-force right side of (S4) is the sum of its quadratic, cubic, and pressure terms.