← Mathematical handbook

theorem Verification.laplace_radial_integrand_bound {q t : ℝ} (hq : 0 < q) (ht : 0 < t) : t⁻¹ * Real.exp (-t - q / (2 * t)) ≤ 2 / q * Real.exp (-t)

theorem Verification.laplaceRadialDensity_ne_top {q : ℝ} (hq : 0 < q) : laplaceRadialDensity q ≠ ⊤

theorem Verification.laplaceRadialDensity_zero : laplaceRadialDensity 0 = ⊤

theorem Verification.laplaceRadialDensity_tendsto_zero : Filter.Tendsto laplaceRadialDensity (nhds 0) (nhds ⊤)

theorem Verification.laplaceRadialDensity_continuousAt {q : ℝ} (hq : 0 < q) : ContinuousAt laplaceRadialDensity q