Abel estimates for the local regularized mild map

The translated Stokes integral has the square-root time bound used in lem:reg-local-mild.

theorem CKN.Leray.mildShiftedStokesIntegral_norm_le (F : ℝ → ↥RealTensorL2) (C : ℝ) (hFC : ∀ (s : ℝ), ‖F s‖ ≤ C) (hC : 0 ≤ C) (T t : ℝ) (hT : 0 ≤ T) : ‖∫ (τ : ℝ) in 0..T, mildShiftedStokesIntegrand F t τ‖ ≤ 2 * (C / √(2 * Real.exp 1)) * √T

The translated Stokes term is bounded by the Abel integral of a uniform tensor bound.