Regularised Equation Interval Component

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.regularisedInterval_scalarWeakMomentum_of_vector (T : ℝ) (u J : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → ℝ) (P : Foundation.Parabolic.ParabolicPoint → ℝ) (hWeak : ∀ φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ k : Fin 3, u z k * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y k) z - ∑ k : Fin 3, ∑ j : Fin 3, J z j * u z k * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y k) j z + ∑ k : Fin 3, ∑ j : Fin 3, D z k j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y k) j z - P z * ∑ k : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y k) k z = 0) (i : Fin 3) (ψ : Foundation.Parabolic.ParabolicPoint → ℝ) (hψ : ψ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), -(u z i * timePartial ψ z) - ∑ j : Fin 3, J z j * u z i * spatialPartial ψ j z + ∑ j : Fin 3, D z i j * spatialPartial ψ j z - P z * spatialPartial ψ i z = 0

Testing the vector weak momentum identity against a single-coordinate field gives the corresponding scalar weak identity.