Quantitative inequalities for the complete Sobolev lifespan

The chosen lifespan makes the Abel contribution fit the fixed-point ball and gives a strict contraction factor.

theorem CKN.Leray.regularisedBesselLocalLifespan_ball_bound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) : ‖b‖ + 2 * (regularisedBesselTensorConstant ρ ε hε k / √(2 * Real.exp 1)) * regularisedBesselLocalRadius k b ^ 2 * √(regularisedBesselLocalLifespan ρ ε hε k b) ≤ regularisedBesselLocalRadius k b

The Abel bound of the local map fits inside the chosen H²ᵏ ball.

theorem CKN.Leray.regularisedBesselLocalLifespan_contraction_bound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) : 2 * (regularisedBesselTensorConstant ρ ε hε k / √(2 * Real.exp 1)) * (2 * regularisedBesselLocalRadius k b) * √(regularisedBesselLocalLifespan ρ ε hε k b) ≤ 1 / 2

The Abel difference bound gives contraction factor at most one half.