Invariance of the real complete Sobolev trajectory ball

The complete mild map preserves real physical realizations when its initial datum is real in physical L².

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

The local complete Sobolev mild map preserves the closed real ball.