Abel bound for the shifted complete Sobolev Stokes integral

The complete Sobolev Stokes integral has the same square-root time factor as its physical L² counterpart.

theorem CKN.Leray.regularisedBesselShiftedStokesIntegral_norm_le (k : ℕ) (F : ℝ → BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2) (C : ℝ) (hFC : ∀ (s : ℝ), ‖F s‖ ≤ C) (hC : 0 ≤ C) (T t : ℝ) (hT : 0 ≤ T) : ‖∫ (τ : ℝ) in 0..T, regularisedBesselShiftedStokesIntegrand k F t τ‖ ≤ 2 * (C / √(2 * Real.exp 1)) * √T

A uniform complete tensor bound gives a square-root bound for the shifted complete Sobolev Stokes integral.