Classical divergence of the mollified transport field

The smooth convolution of a weakly divergence-free velocity is pointwise divergence free. This supplies the cancellation in the differentiated energy estimate.

theorem CKN.Leray.regUniformMollifiedVelocity_divergence_eq_zero (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (t : ℝ) (hJ : IsInJ fun (x : Foundation.Parabolic.Vec3) => u (x, t)) (x : Foundation.Parabolic.Vec3) : ∑ i : Fin 3, (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε u (y, t) i) x) (basisVec i) = 0

The mollified velocity from a Leray-space slice has zero classical divergence at every spatial point.