The Leray and Stokes ranges in the initial-data space

The physical weak-divergence conclusions for the Fourier multipliers imply membership in the closure space J used in lem:reg-local-mild.

theorem CKN.Leray.realStokesOperator_isInJ {t : ℝ} (ht : 0 < t) (F : ↥RealTensorL2) : IsInJ (realVectorL2Representative (realStokesOperator ht F))

The real heat-regularized Leray-Stokes operator takes values in J, as needed for the time integral in eq:reg-mild.