Uniform energy bound for the linear complete Sobolev solution

The fixed physical L² coefficient makes the complete Sobolev mild estimate linear, so the uniform energy time step controls its fixed point.

theorem CKN.Leray.regularisedBesselLinearLocalFixedPoint_norm_le_twice (ρ : 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 : C(↑(RegularizedMildTimeInterval (regularisedBesselUniformEnergyStep ρ ε hε k B)), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) (hfix : regularisedBesselLinearLocalMap ρ ε hε k b (regularisedBesselUniformEnergyStep ρ ε hε k B) ⋯ g B hB hg v = v) : ‖v‖ ≤ 2 * ‖b‖

A fixed point of the linear complete Sobolev mild map on the uniform energy interval has norm at most twice its initial norm.