Local complete Sobolev representation of the global mild curve

For every real complete Sobolev initial state, the global regularized mild solution is represented by a complete Sobolev mild curve on a positive interval.

theorem CKN.Leray.regularisedBesselLocalGlobalRepresentation (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (b₀ : ↥RealVectorL2) (hb : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) b = complexifyVectorL2 b₀) (hbJ : RegularizedMildJData b₀) : ∃ (u : C(↑(RegularizedMildTimeInterval (regularisedBesselLocalLifespan ρ ε hε k b)), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)), regularisedBesselLocalMap ρ ε hε k b (regularisedBesselLocalLifespan ρ ε hε k b) ⋯ u = u ∧ ‖u‖ ≤ regularisedBesselLocalRadius k b ∧ ∀ (t : ↑(RegularizedMildTimeInterval (regularisedBesselLocalLifespan ρ ε hε k b))), (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (u t) = complexifyVectorL2 (regularizedGlobalMildCurve ρ ε hε b₀ hbJ ↑t)

The global regularized mild curve has a real complete H²ᵏ representation on the explicit local lifespan.