Stability Momentum Support

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_momentum_integral_eq_localBox {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hφ : φ ∈ spaceTimeTestFunction Ω I) (hKbox : tsupport (have this := φ; this) ⊆ spaceTimeSet Ω' J) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, -∑ 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 - ∑ 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

A weak momentum test has the same pairing on the whole carrier and on any local box containing its compact support.