Stability Divergence Support

Supporting estimates for the Navier–Stokes development.

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

A compactly supported divergence pairing has the same integral on the whole carrier and on any local box containing the test support.