Agreement of the complete local trajectory with the global mild curve

The real physical realization of the complete H²ᵏ fixed point is the existing global regularized mild curve throughout its local lifespan.

theorem CKN.Leray.regularisedBesselLocalRealFixedPoint_eq_global (ρ : 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)) (hfix : regularisedBesselLocalMap ρ ε hε k b (regularisedBesselLocalLifespan ρ ε hε k b) ⋯ u = u) (hu : u ∈ regularisedBesselLocalRealBall k (regularisedBesselLocalLifespan ρ ε hε k b) (regularisedBesselLocalRadius k b)) (t : ↑(RegularizedMildTimeInterval (regularisedBesselLocalLifespan ρ ε hε k b))) : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (u t) = complexifyVectorL2 (regularizedGlobalMildCurve ρ ε hε b₀ hbJ ↑t)

The physical L² path of any real complete Sobolev local fixed point agrees with the unique global regularized mild solution.