The actual regularized momentum right-hand side in spatial L²

At positive times the regularized velocity and canonical pressure are spatially smooth, with all their classical ordered derivatives in L². The complete regularized momentum right-hand side has the same property.

theorem ESS.lps_regR12Velocity_slice_isInJ (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (t : ℝ) (ht : 0 ≤ t) : CKN.IsInJ fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε a ha (x, t)

The physical regularized velocity is in the solenoidal L² space on every nonnegative-time slice.

theorem ESS.lps_regR12TimeRHS_all_word_memLp_actual (ρ : 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) (α : List (Fin 3)) : MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12TimeRHS ρ ε hε (CKN.Leray.regR12Velocity ρ ε hε a ha) (CKN.Leray.forcedQuadPressure ρ ε hε (CKN.Leray.regR12Curve ρ ε hε a ha)) (x, t) i) 2 MeasureTheory.volume

Every ordered spatial derivative of the actual regularized momentum right-hand side is in L² on a positive-time slice (prop:lps-smoothing).