Invariance of the complete Sobolev mild ball

The complete H²ᵏ mild map sends the explicit closed trajectory ball into itself on its positive local lifespan.

theorem CKN.Leray.regularisedBesselLocalMap_ball (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (u : C(↑(RegularizedMildTimeInterval (regularisedBesselLocalLifespan ρ ε hε k b)), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) (hu : ‖u‖ ≤ regularisedBesselLocalRadius k b) : ‖regularisedBesselLocalMap ρ ε hε k b (regularisedBesselLocalLifespan ρ ε hε k b) ⋯ u‖ ≤ regularisedBesselLocalRadius k b

The chosen complete H²ᵏ trajectory ball is invariant under the local regularized mild map.