Physical mild equation of the real complete Sobolev fixed point

The real physical trajectory of a complete H²ᵏ fixed point solves the regularized L² mild equation on the same local interval.

theorem CKN.Leray.regularisedBesselLocalRealFixedPoint_isTrajectory (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (b₀ : ↥RealVectorL2) (hb : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) b = complexifyVectorL2 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)) : IsRegularizedMildTrajectory ρ ε hε b₀ (regularisedBesselLocalLifespan ρ ε hε k b) (regularisedBesselRealPartPath k (regularisedBesselLocalLifespan ρ ε hε k b) u)

A real complete Sobolev local fixed point is a physical L² mild trajectory with the same initial datum.