Real local fixed point in the complete Sobolev space

The complete H²ᵏ mild map has a fixed point whose physical L² trajectory is real, on the same positive interval as its complex fixed point.

theorem CKN.Leray.regularisedBesselLocalRealFixedPoint (ρ : 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)), regularisedBesselLocalMap ρ ε hε k b (regularisedBesselLocalLifespan ρ ε hε k b) ⋯ u = u ∧ u ∈ regularisedBesselLocalRealBall k (regularisedBesselLocalLifespan ρ ε hε k b) (regularisedBesselLocalRadius k b)

A real physical complete H²ᵏ mild solution exists on the explicit positive local lifespan.