Weighted Abel kernel in elapsed time

The exponentially weighted Stokes kernel has a bound independent of the length of the time interval.

theorem CKN.Leray.regularisedAbelElapsedExpIntegral_le {lam T : ℝ} (hlam : 0 < lam) : ∫ (τ : ℝ) in Set.Ioc 0 T, τ ^ (-(1 / 2)) * Real.exp (-lam * τ) ≤ lam ^ (-(1 / 2)) * Real.Gamma (1 / 2)

The elapsed-time Abel kernel has an exponentially weighted integral bounded by the complete Gamma integral.