Regularised Mild Initial Data

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.regUniformMollifiedInitial_mildJData (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) : RegularizedMildJData (realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯)

The mollified initial datum in the real L² carrier belongs to the closed solenoidal subspace used by lem:reg-local-mild.

theorem CKN.Leray.regUniformMollifiedInitial_contDiff (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) : ContDiff ℝ (↑⊤) (regUniformMollifiedInitial ρ ε hε a)

The mollified initial velocity is smooth in space, as used in thm:regularised.