Stability Momentum Decompose

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_momentum_integral_decompose_localBox {Ω Ω' : 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 → ℝ} (hdata : IsSuitableWeakSolutionData Ω I q u Du p 0) (hbox : localBox Ω I Ω' J) (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hφ : φ ∈ spaceTimeTestFunction Ω I) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, -∑ i : Fin 3, u z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z - p z * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z - ∑ i : Fin 3, 0 z i * φ z i = (((-∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ∑ i : Fin 3, u z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z) - ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z) + ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z) - ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, p z * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z

The four nonzero pieces of the zero-force momentum pairing may be integrated separately on a local box.