Divergence form of the regularized momentum equation

The actual transport field is a smooth mollification of a J slice. Its pointwise zero divergence converts the regularized transport term to the tensor divergence used in the high-order energy identity.

theorem ESS.lps_regR12TimeRHS_divergence (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (t : ℝ) (hJ : CKN.IsInJ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) (hu : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) (x : CKN.Foundation.Parabolic.Vec3) (i : Fin 3) : CKN.Leray.regR12TimeRHS ρ ε hε u p (x, t) i = ∑ j : Fin 3, CKN.spatialDeriv (CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) i) j) j x - ∑ j : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regUniformMollifiedVelocity ρ ε hε u (y, t) j * u (y, t) i) j x - CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => p (y, t)) i x

The right-hand side of the regularized momentum equation equals the heat operator minus tensor divergence and pressure gradient (eq:lps-regularized-Hm-identity).