Physical agreement after a complete Sobolev restart

The complete Sobolev solution of the equation linearized around the global physical trajectory realizes that same global trajectory on its interval.

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

A fixed point of the complete Sobolev linear equation after any nonnegative restart time represents the global complex physical mild curve.