Contraction of the local complete Sobolev mild map

The translated Abel integral makes the complete H²ᵏ mild map a strict contraction on the chosen closed trajectory ball.

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

On the chosen complete H²ᵏ trajectory ball, the local mild map contracts differences by a factor of one half.