Global contraction of the linear complete Sobolev mild map

With a fixed bounded physical L² coefficient, the complete Sobolev mild map contracts on the entire trajectory Banach space over the uniform time step.

theorem CKN.Leray.regularisedBesselLinearLocalMap_contraction (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (B : ℝ) (hB : 0 ≤ B) (g : C(↑(RegularizedMildTimeInterval (regularisedBesselUniformEnergyStep ρ ε hε k B)), ↥ComplexVectorL2)) (hg : ∀ (q : ↑(RegularizedMildTimeInterval (regularisedBesselUniformEnergyStep ρ ε hε k B))), ‖g q‖ ≤ B) (v w : C(↑(RegularizedMildTimeInterval (regularisedBesselUniformEnergyStep ρ ε hε k B)), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) : ‖regularisedBesselLinearLocalMap ρ ε hε k b (regularisedBesselUniformEnergyStep ρ ε hε k B) ⋯ g B hB hg v - regularisedBesselLinearLocalMap ρ ε hε k b (regularisedBesselUniformEnergyStep ρ ε hε k B) ⋯ g B hB hg w‖ ≤ 1 / 2 * ‖v - w‖

The linear complete Sobolev mild map is a one-half contraction on the uniform energy time step, without a Sobolev norm ball.