Global complete Sobolev paths of the regularized mild solution

Uniform Sobolev restarts and the physical L² energy bound give a continuous complete Sobolev realization on every finite interval.

theorem CKN.Leray.regularisedBesselGlobalFinitePath (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b₀ : ↥RealVectorL2) (hbJ : RegularizedMildJData b₀) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (hb : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) b = complexifyVectorL2 b₀) (T : ℝ) (hT : 0 ≤ T) : ∃ (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)), ∀ (t : ↑(RegularizedMildTimeInterval T)), (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (v t) = complexifyVectorL2 (regularizedGlobalMildCurve ρ ε hε b₀ hbJ ↑t)

An initial H²ᵏ realization of the regularized mild curve extends as a continuous H²ᵏ representative on every finite time interval.

theorem CKN.Leray.regUniformMollifiedInitial_global_bessel_path (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (k : ℕ) (T : ℝ) (hT : 0 ≤ T) : let b₀ := realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯; ∃ (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)), ∀ (t : ↑(RegularizedMildTimeInterval T)), (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (v t) = complexifyVectorL2 (regularizedGlobalMildCurve ρ ε hε b₀ ⋯ ↑t)

The global regularized mild curve from mollified Leray data has a continuous H²ᵏ realization on every finite interval.