← Mathematical handbook

The Laplace radial integral is a modified Bessel function

K₀(z)=∫₀^∞ exp(-z cosh s) ds (the standard integral representation, z>0). For q>0 the substitution t=√(q/2)·e^s turns ∫₀^∞ t⁻¹ exp(-t-q/(2t)) dt into ∫_ℝ exp(-√(2q) cosh s) ds = 2K₀(√(2q)). Hence the Laplace joint density (2π√(1-r²))⁻¹ · laplaceRadialDensity(Q) equals the printed K₀(√(2Q))/(π√(1-r²)).

noncomputable def Verification.besselK0 (z : ℝ) : ENNReal

The modified Bessel function of the second kind of order zero, in its integral form.

Equations

• Verification.besselK0 z = ∫⁻ (s : ℝ) in Set.Ioi 0, ENNReal.ofReal (Real.exp (-z * Real.cosh s))

theorem Verification.lintegral_Iio_eq_Ioi (f : ℝ → ENNReal) : ∫⁻ (s : ℝ) in Set.Iio 0, f s = ∫⁻ (s : ℝ) in Set.Ioi 0, f (-s)

theorem Verification.lintegral_even (f : ℝ → ENNReal) (hf : ∀ (s : ℝ), f (-s) = f s) : ∫⁻ (s : ℝ), f s = 2 * ∫⁻ (s : ℝ) in Set.Ioi 0, f s

theorem Verification.laplaceRadialDensity_eq_besselK0 {q : ℝ} (hq : 0 < q) : laplaceRadialDensity q = 2 * besselK0 √(2 * q)