Uniform Sobolev realization after a global restart

Every complete Sobolev state of the global mild curve extends as a complete Sobolev path over a time step fixed by the initial physical energy bound.

theorem CKN.Leray.regularisedBesselShiftedGlobalRepresentation (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b₀ : ↥RealVectorL2) (hbJ : RegularizedMildJData b₀) (a : ℝ) (ha : 0 ≤ a) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (hb : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) b = complexifyVectorL2 (regularizedGlobalMildCurve ρ ε hε b₀ hbJ a)) : let δ := regularisedBesselUniformEnergyStep ρ ε hε k ‖b₀‖; ∃ (v : C(↑(RegularizedMildTimeInterval δ), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)), v ⟨0, ⋯⟩ = b ∧ ‖v‖ ≤ 2 * ‖b‖ ∧ ∀ (t : ↑(RegularizedMildTimeInterval δ)), (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (v t) = complexifyVectorL2 (regularizedGlobalMildCurve ρ ε hε b₀ hbJ (a + ↑t))

Starting from any nonnegative time where the global mild curve has an H²ᵏ realization, the same curve has an H²ᵏ path over the uniform step.