Smooth spatial slices of the regularized velocity

The all-order Bessel lifts give integrable Fourier moments of every finite degree. Fourier inversion therefore makes every regularized velocity slice smooth in space.

theorem ESS.lps_regR12FreqCurve_moment_integrable (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (t : ℝ) (ht : 0 ≤ t) (r : ℕ) : MeasureTheory.Integrable (fun (ξ : CKN.Foundation.Parabolic.L2Vec3) => ‖ξ‖ ^ r * ‖↑↑(CKN.Leray.regR12FreqCurve ρ ε hε a ha t) ξ‖) MeasureTheory.volume

Every polynomial moment of the Fourier transform of a nonnegative-time regularized velocity slice is integrable (prop:lps-smoothing).

theorem ESS.lps_regR12Velocity_slice_contDiff (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (t : ℝ) (ht : 0 ≤ t) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε a ha (x, t) i

Every nonnegative-time spatial slice of the actual regularized velocity is smooth to all orders (prop:lps-smoothing).