Stability Energy Support

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_energy_gradient_integral_eq_localBox {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (hψ : ψ ∈ spaceTimeTestFunction Ω I) (hKbox : tsupport (have this := ψ; this) ⊆ spaceTimeSet Ω' J) (v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Dv : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, spatialGradientSq v Dv z * ψ z = ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, spatialGradientSq v Dv z * ψ z

The weighted gradient term has the same integral on the carrier and on a local box containing the test support.

theorem CKN.stability_energy_rhs_integral_eq_localBox {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (hψ : ψ ∈ spaceTimeTestFunction Ω I) (hKbox : tsupport (have this := ψ; this) ⊆ spaceTimeSet Ω' J) (v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (r : Foundation.Parabolic.ParabolicPoint → ℝ) : ∫ (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 = ∫ (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

The right side of the zero-force local energy inequality is supported where its test is supported.