Smoothness of regularized L² fields

Convolution by the fixed smooth compactly supported mollifier maps every spatial L² field into a smooth coordinate field. The input need not be divergence free when it is a difference in the local Lipschitz estimate.

theorem CKN.Leray.regUniformMollifiedInitial_contDiff_of_memLp (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : ContDiff ℝ (↑⊤) (regUniformMollifiedInitial ρ ε hε a)

Mollification of an arbitrary coordinate L² field is spatially smooth.