Stability Divergence Sum

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_divergence_sum_integral_eq {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (hbox : localBox Ω I Ω' J) (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (hψ : ψ ∈ spaceTimeTestFunction Ω I) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : MeasureTheory.MemLp f 3 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ∑ i : Fin 3, f z i * spatialPartial ψ i z = ∑ i : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, spatialPartial ψ i z * f z i

The divergence pairing on a local box is the finite sum of its coordinate pairings when the velocity is locally L³.