Proof of the Laplace Integral Identity (Bessel K_{1/2})

This file proves the integral identity: ∫₀^∞ s^{-1/2} exp(-a/s - b*s) ds = √(π/b) exp(-2√(ab))

This is a special case of the modified Bessel function K_{1/2} identity.

Proof Strategy

1. Substitution s = t²: Transforms s^{-1/2} ds to 2 dt
2. Complete the square: a/t² + bt² = (√a/t - √b·t)² + 2√(ab)
3. Factor out exp(-2√(ab))
4. Substitution u = √b·t: Reduces to ∫ exp(-(c/u - u)²) du where c = √(ab)
5. Glasser/Cauchy-Schlömilch: Show ∫₀^∞ exp(-(c/u - u)²) du = √π/2
6. Combine: Get the final result

References

• Gradshteyn & Ryzhik, Table of Integrals, Entry 3.471.9
• DLMF §10.32.10 (Modified Bessel functions)
• Glasser, M.L. "A remarkable property of definite integrals" (1983)

Part 2: The Glasser/Cauchy-Schlömilch Identity

The key identity is: for c > 0, ∫₀^∞ exp(-(c/u - u)²) du = √π / 2

Note: we use (c/u - u) not (u - c/u) to match the form after our substitutions. Since (c/u - u)² = (u - c/u)², these are equivalent.

theorem LaplaceIntegral.glasser_sq_symm (c u : ℝ) : (c / u - u) ^ 2 = (u - c / u) ^ 2

The Glasser quadratic form is symmetric: (c/u - u)² = (u - c/u)²

theorem LaplaceIntegral.glasser_expand (c u : ℝ) (hu : u ≠ 0) : (c / u - u) ^ 2 = c ^ 2 / u ^ 2 - 2 * c + u ^ 2

Expansion: (c/u - u)² = c²/u² - 2c + u²

theorem LaplaceIntegral.glasser_lower_bound (c u : ℝ) (hu : u ≠ 0) : (c / u - u) ^ 2 ≥ u ^ 2 - 2 * c

Lower bound: (c/u - u)² ≥ u² - 2c

theorem LaplaceIntegral.hasDerivAt_glasser_map (c u : ℝ) (hu : u ≠ 0) : HasDerivAt (fun (x : ℝ) => c / x - x) (-c / u ^ 2 - 1) u

The derivative of u ↦ c/u - u is -c/u² - 1

Part 3: The core Glasser integral

This is the key technical result. The proof uses the remarkable fact that the substitution v = c/u, combined with appropriate symmetry arguments, reduces the integral to a Gaussian.

Proof idea: Let I = ∫₀^∞ exp(-(c/u - u)²) du.

Substitute v = c/u in I:

• When u → 0⁺, v → ∞; when u → ∞, v → 0⁺
• du = -c/v² dv
• c/u - u = c/(c/v) - c/v = v - c/v = -(c/v - v)

So I = ∫_∞^0 exp(-(-(c/v - v))²) (-c/v²) dv = ∫_0^∞ exp(-(c/v - v)²) (c/v²) dv

Adding these: 2I = ∫_0^∞ exp(-(c/u - u)²) (1 + c/u²) du

Note that d/du(c/u - u) = -c/u² - 1 = -(1 + c/u²), so |d/du(c/u - u)| = 1 + c/u².

Thus 2I = ∫_0^∞ exp(-(c/u - u)²) |d/du(c/u - u)| du

Substituting w = c/u - u (which maps (0,∞) → ℝ bijectively): 2I = ∫_{-∞}^{+∞} exp(-w²) dw = √π

Therefore I = √π/2.

theorem LaplaceIntegral.glasser_integral_substitution_identity (c : ℝ) (hc : 0 < c) : ∫ (u : ℝ) in Set.Ioi 0, Real.exp (-(c / u - u) ^ 2) = ∫ (u : ℝ) in Set.Ioi 0, c / u ^ 2 * Real.exp (-(c / u - u) ^ 2)

The substitution u ↦ c/u shows that the Glasser integral is invariant under multiplication by c/u². This is the key identity that enables the proof.

theorem LaplaceIntegral.glasser_integrable (c : ℝ) (_hc : 0 < c) : MeasureTheory.IntegrableOn (fun (u : ℝ) => Real.exp (-(c / u - u) ^ 2)) (Set.Ioi 0) MeasureTheory.volume

The Glasser integrand is integrable on (0, ∞). Proof: On (0, 1], bounded by 1 on finite measure set. On (1, ∞), dominated by e^{2c} · e^{-u²} which is Gaussian-integrable.

theorem LaplaceIntegral.glasser_weighted_integrable (c : ℝ) (hc : 0 < c) : MeasureTheory.IntegrableOn (fun (u : ℝ) => c / u ^ 2 * Real.exp (-(c / u - u) ^ 2)) (Set.Ioi 0) MeasureTheory.volume

The weighted Glasser integrand is integrable on (0, ∞). Proof: Use change of variables v = c/u which maps (0,1] → [c,∞) and (1,∞) → (0,c]. On each piece, the weighted integrand transforms to the unweighted one on a subset of (0,∞).

theorem LaplaceIntegral.glasser_integral_double (c : ℝ) (hc : 0 < c) : 2 * ∫ (u : ℝ) in Set.Ioi 0, Real.exp (-(c / u - u) ^ 2) = ∫ (u : ℝ) in Set.Ioi 0, (1 + c / u ^ 2) * Real.exp (-(c / u - u) ^ 2)

theorem LaplaceIntegral.glasser_tendsto_atTop_at_zero (c : ℝ) (hc : 0 < c) : Filter.Tendsto (fun (u : ℝ) => c / u - u) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

The Glasser map w = c/u - u tends to +∞ as u → 0⁺.

theorem LaplaceIntegral.glasser_tendsto_atBot_at_top (c : ℝ) (_hc : 0 < c) : Filter.Tendsto (fun (u : ℝ) => c / u - u) Filter.atTop Filter.atBot

The Glasser map w = c/u - u tends to -∞ as u → +∞.

theorem LaplaceIntegral.glasser_continuousOn (c : ℝ) : ContinuousOn (fun (u : ℝ) => c / u - u) (Set.Ioi 0)

The Glasser map is continuous on (0, ∞).

theorem LaplaceIntegral.glasser_strictAntiOn (c : ℝ) (hc : 0 < c) : StrictAntiOn (fun (u : ℝ) => c / u - u) (Set.Ioi 0)

The Glasser map is strictly decreasing on (0, ∞).

theorem LaplaceIntegral.glasser_injOn (c : ℝ) (hc : 0 < c) : Set.InjOn (fun (u : ℝ) => c / u - u) (Set.Ioi 0)

The Glasser map is injective on (0, ∞).

theorem LaplaceIntegral.glasser_hasDerivWithinAt (c u : ℝ) (hu : 0 < u) : HasDerivWithinAt (fun (x : ℝ) => c / x - x) (-c / u ^ 2 - 1) (Set.Ioi 0) u

The Glasser map has the stated derivative on (0, ∞).

theorem LaplaceIntegral.glasser_image_eq_univ (c : ℝ) (hc : 0 < c) : (fun (u : ℝ) => c / u - u) '' Set.Ioi 0 = Set.univ

The image of (0, ∞) under the Glasser map is all of ℝ.

theorem LaplaceIntegral.glasser_deriv_abs (c : ℝ) (hc : 0 < c) (u : ℝ) (hu : u ∈ Set.Ioi 0) : |-c / u ^ 2 - 1| = 1 + c / u ^ 2

The absolute value of the Glasser map derivative is 1 + c/u².

theorem LaplaceIntegral.weighted_glasser_integral_eq_gaussian (c : ℝ) (hc : 0 < c) : ∫ (u : ℝ) in Set.Ioi 0, (1 + c / u ^ 2) * Real.exp (-(c / u - u) ^ 2) = √Real.pi

The weighted integral equals √π via change of variables w = c/u - u. This is the core analytical step.

theorem LaplaceIntegral.glasser_gaussian_integral (c : ℝ) (hc : 0 < c) : ∫ (u : ℝ) in Set.Ioi 0, Real.exp (-(c / u - u) ^ 2) = √Real.pi / 2

Part 4: Completing the square

theorem LaplaceIntegral.complete_square (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (t : ℝ) (ht : 0 < t) : a / t ^ 2 + b * t ^ 2 = (√a / t - √b * t) ^ 2 + 2 * √(a * b)

Completing the square: a/t² + b·t² = (√a/t - √b·t)² + 2√(ab)

Part 5: The main substitutions

theorem LaplaceIntegral.laplace_integral_subst_sq (a b : ℝ) (_ha : 0 < a) (_hb : 0 < b) : ∫ (s : ℝ) in Set.Ioi 0, s ^ (-(1 / 2)) * Real.exp (-a / s - b * s) = 2 * ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-a / t ^ 2 - b * t ^ 2)

First substitution: s = t² transforms s^{-1/2} ds to 2 dt

theorem LaplaceIntegral.laplace_integral_factor (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-a / t ^ 2 - b * t ^ 2) = Real.exp (-2 * √(a * b)) * ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-(√a / t - √b * t) ^ 2)

After completing the square, factor out exp(-2√(ab))

theorem LaplaceIntegral.laplace_integral_subst_scale (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-(√a / t - √b * t) ^ 2) = 1 / √b * ∫ (u : ℝ) in Set.Ioi 0, Real.exp (-(√(a * b) / u - u) ^ 2)

Second substitution: u = √b · t, so √a/t - √b·t = √(ab)/u - u

Part 6: The main theorem

theorem LaplaceIntegral.laplace_integral_half_power (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : ∫ (s : ℝ) in Set.Ioi 0, s ^ (-(1 / 2)) * Real.exp (-a / s - b * s) = √(Real.pi / b) * Real.exp (-2 * √(a * b))

Main Theorem: The Laplace integral identity (Bessel K_{1/2}).

∫₀^∞ s^{-1/2} exp(-a/s - b*s) ds = √(π/b) exp(-2√(ab))

This is Gradshteyn & Ryzhik 3.471.9 with ν = 1/2.

theorem LaplaceIntegral.laplace_integral_half_power_nonneg (a b : ℝ) (ha : 0 ≤ a) (hb : 0 < b) : ∫ (s : ℝ) in Set.Ioi 0, s ^ (-(1 / 2)) * Real.exp (-a / s - b * s) = √(Real.pi / b) * Real.exp (-2 * √(a * b))

Extension: The Laplace integral identity for a ≥ 0 (extends to include a = 0).

When a = 0, the integral reduces to the Gamma function: ∫₀^∞ s^{-1/2} exp(-b·s) ds = Γ(1/2) / √b = √(π/b)

which matches √(π/b) · exp(-2√(0·b)) = √(π/b) · 1 = √(π/b).