Continuous scalar Sobolev trajectories of the regularized velocity

The global Bessel realization gives a continuous spatial L² path for every ordered classical derivative on a finite interval.

theorem ESS.lps_regR12Velocity_wordDeriv_continuous_L2 (ρ : 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)) : ∃ (F : ℝ → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)), Continuous F ∧ ∀ t ∈ Set.Icc 0 T, ↑↑(F t) =ᵐ[MeasureTheory.volume] CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε a ha (x, t) i

Every ordered spatial derivative of the physical regularized velocity has a continuous scalar L² realization on a finite closed interval (prop:lps-smoothing).

theorem ESS.lps_regR12Velocity_all_word_memLp_slab (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (δ T : ℝ) (hδ : 0 ≤ δ) (hδT : δ < T) (i : Fin 3) (α : List (Fin 3)) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.wordDeriv α (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε a ha (x, z.2) i) z.1) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo δ T)))

Every ordered spatial derivative of the regularized velocity belongs to L² on a positive finite space-time slab (prop:lps-smoothing).