The Gaussian–exponential scale mixture is Laplace

A centered Gaussian whose variance v is exponentially distributed with rate λ has a Laplace marginal with rate √(2λ):

∫_{v > 0} (2πv)^{-1/2} e^{-x²/(2v)} · λ e^{-λv} dv = (√(2λ)/2) e^{-√(2λ)|x|}.

The proof reduces the integral to the Glasser (modified Bessel K_{1/2}) integral ∫_{v > 0} v^{-1/2} e^{-a/v - bv} dv = √(π/b) e^{-2√(ab)}, which is proved through the substitution v = √(a/b) s² and Schlömilch's change of variables u = s - 1/s.

Main definitions

• Superstatistics.laplacePDFReal rate x: the Laplace density (rate/2) e^{-rate |x|}.

Main results

• Superstatistics.laplacePDFReal_integral_eq_one: the density integrates to 1.
• Superstatistics.combined: ∫_{s > 0} (1 + s⁻²) e^{-c (s - s⁻¹)²} ds = √(π/c).
• Superstatistics.glasser_integral: the Glasser integral.
• Superstatistics.gaussian_exponential_mixture_laplace: the scale-mixture identity.

References

• D. F. Andrews, C. L. Mallows, Scale mixtures of normal distributions, J. Roy. Statist. Soc. Ser. B 36 (1974) 99–102.
• M. L. Glasser, A remarkable property of definite integrals, Math. Comp. 40 (1983) 561.

The Laplace density (Mathlib defines none)

laplacePDFReal rate x = (rate/2)·exp(−rate·|x|) is the pdf of the centred Laplace (double-exponential) law with the given rate.

noncomputable def Superstatistics.laplacePDFReal (rate x : ℝ) : ℝ

Equations

• Superstatistics.laplacePDFReal rate x = rate / 2 * Real.exp (-(rate * |x|))

theorem Superstatistics.laplacePDFReal_pos {rate : ℝ} (x : ℝ) (h : 0 < rate) : 0 < laplacePDFReal rate x

The Laplace density is strictly positive for a positive rate.

theorem Superstatistics.laplace_rate_eq (lam : ℝ) : √(2 * lam) / 2 = √(lam / 2)

Rate identification: the mixture output constant √(2λ)/2 equals the density-normalisation constant √(λ/2) = √(λ/2); i.e. the marginal density reads √(λ/2)·exp(−√(2λ)·|x|), a Laplace of rate √(2λ).

theorem Superstatistics.rhs_eq_laplacePDF (lam x : ℝ) : √(2 * lam) / 2 * Real.exp (-(√(2 * lam) * |x|)) = laplacePDFReal (√(2 * lam)) x

The claimed mixture RHS is exactly the Laplace pdf of rate √(2λ).

Normalisation (the RHS is a genuine probability density)

theorem Superstatistics.integral_exp_neg_mul_Ioi_zero {b : ℝ} (hb : 0 < b) : ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-(b * x)) = 1 / b

Scaled exponential tail integral ∫_{Ioi 0} exp(−b x) dx = 1/b (b>0).

theorem Superstatistics.laplacePDFReal_integral_eq_one {b : ℝ} (hb : 0 < b) : ∫ (x : ℝ), laplacePDFReal b x = 1

The Laplace density integrates to 1 (rate > 0): it is a probability density.

T1′ — the Gaussian/Exponential scale-mixture = Laplace (integral form)

Marginalising X | V ~ N(0, V) against V ~ Exponential(λ) yields the Laplace law of rate √(2λ). In pure integral form (over the variance v):

∫_{Ioi 0} (√(2πv))⁻¹ · exp(−x²/(2v)) · (λ·exp(−λ v)) dv = (√(2λ)/2) · exp(−√(2λ)·|x|).

The Gaussian kernel is gaussianPDFReal 0 v x; the prior weight λ·exp(−λ v) is exponentialPDFReal λ v on v > 0.

Proof: Pull the constant λ·(2π)^(−1/2) out; the remaining integral is the Glasser / modified-Bessel-K_{1/2} integral (glasser_integral below) ∫_{Ioi 0} v^(−1/2) · exp(−a/v − b v) dv = √(π/b) · exp(−2√(a b)) (a≥0,b>0) with a = x²/2, b = λ. Evaluating: √(π/λ)·exp(−2√(x²λ/2)) = √(π/λ)·exp(−√(2λ)·|x|), and λ·(2π)^(−1/2)·√(π/λ) = √(λ/2) = √(2λ)/2 (this last step is laplace_rate_eq). glasser_integral is proved via the substitution v = √(a/b)·s² and the Schlömilch change of variables u = s − 1/s : Ioi 0 → ℝ (combined), both realised with the one-variable Jacobian lemma integral_image_eq_integral_abs_deriv_smul.

Schlömilch / Glasser kernel — the analytic core (now fully formalised)

The whole chain rests on the reflection s ↦ 1/s and the change of variables u = s − 1/s : Ioi 0 → univ, both handled by the one-variable Jacobian lemma integral_image_eq_integral_abs_deriv_smul. No modified Bessel K is needed.

theorem Superstatistics.combined (c : ℝ) : ∫ (x : ℝ) in Set.Ioi 0, (1 + (x ^ 2)⁻¹) * Real.exp (-c * (x - x⁻¹) ^ 2) = √(Real.pi / c)

Key step (Schlömilch). ∫_{Ioi 0} (1 + 1/x²)·exp(−c(x−1/x)²) dx = √(π/c), via the change of variables u = x − 1/x (a C¹ bijection Ioi 0 → ℝ, jacobian 1 + 1/x²) reducing to the Gaussian integral ∫_ℝ exp(−c u²) = √(π/c).

theorem Superstatistics.hderiv_inv (x : ℝ) : x ∈ Set.Ioi 0 → HasDerivWithinAt (fun (s : ℝ) => s⁻¹) (-(x ^ 2)⁻¹) (Set.Ioi 0) x

Derivative of x ↦ x⁻¹ on Ioi 0 (used for the reflection).

theorem Superstatistics.hinj_inv : Set.InjOn (fun (s : ℝ) => s⁻¹) (Set.Ioi 0)

theorem Superstatistics.himg_inv : (fun (s : ℝ) => s⁻¹) '' Set.Ioi 0 = Set.Ioi 0

theorem Superstatistics.refl_int (g : ℝ → ℝ) : ∫ (x : ℝ) in Set.Ioi 0, g x = ∫ (x : ℝ) in Set.Ioi 0, (x ^ 2)⁻¹ * g x⁻¹

Reflection x ↦ 1/x on Ioi 0 (jacobian 1/x²).

theorem Superstatistics.refl_integ (g : ℝ → ℝ) (hg : MeasureTheory.IntegrableOn g (Set.Ioi 0) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : ℝ) => (x ^ 2)⁻¹ * g x⁻¹) (Set.Ioi 0) MeasureTheory.volume

theorem Superstatistics.value_sq (c : ℝ) (hc : 0 < c) : ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-c * (x ^ 2 + (x ^ 2)⁻¹)) = 1 / 2 * (Real.exp (-2 * c) * √(Real.pi / c))

∫_{Ioi 0} exp(−c(x²+1/x²)) dx = (1/2)·exp(−2c)·√(π/c) for c > 0 (reflection halves the (1 + 1/x²)-weighted combined integral).

theorem Superstatistics.glasser_integral {a b : ℝ} (ha : 0 ≤ a) (hb : 0 < b) : ∫ (v : ℝ) in Set.Ioi 0, v ^ (-1 / 2) * Real.exp (-a / v - b * v) = √(Real.pi / b) * Real.exp (-(2 * √(a * b)))

Glasser / modified-Bessel-K_{1/2} integral (the analytic kernel). For a ≥ 0, b > 0, ∫_{Ioi 0} v^(−1/2)·exp(−a/v − b·v) dv = √(π/b)·exp(−2·√(a·b)). a = 0: Gamma integral (integral_rpow_mul_exp_neg_mul_Ioi, Real.Gamma_one_half_eq). a > 0: the substitution v = √(a/b)·s² (one-variable Jacobian CoV) reduces it to 2·√(√(a/b))·value_sq(√(ab)); value_sq in turn rests on combined (the Schlömilch u = s − 1/s change of variables).

theorem Superstatistics.gaussian_exponential_mixture_laplace (lam x : ℝ) (hlam : 0 < lam) : ∫ (v : ℝ) in Set.Ioi 0, (√(2 * Real.pi * v))⁻¹ * Real.exp (-x ^ 2 / (2 * v)) * (lam * Real.exp (-(lam * v))) = √(2 * lam) / 2 * Real.exp (-(√(2 * lam) * |x|))