Gaussian variance mixtures: Student-t marginals and excess kurtosis

Marginalizing a centered Gaussian of precision β against a Gamma(a, b) law on β gives the Student-t density, normalized by b^a. For any variance mixture X = √V · Z with Z standard normal and independent of V ≥ 0, the kurtosis is 3 E[V²] / E[V]², so the excess kurtosis 3 Var(V) / E[V]² is nonnegative.

Main results

• Superstatistics.gaussian_gamma_mixture_studentt: the Gaussian–Gamma mixture integral.
• Superstatistics.std_normal_second_moment, Superstatistics.std_normal_fourth_moment: E[Z²] = 1 and E[Z⁴] = 3, from the moment generating function.
• Superstatistics.sq_expectation_le_expectation_sq: E[V]² ≤ E[V²].
• Superstatistics.variance_mixture_kurtosis_identity: the kurtosis identity, given the moment factorization.
• Superstatistics.variance_mixture_kurtosis_identity': the same on the product space μV.prod (gaussianReal 0 1), with the factorization derived from integral_prod_mul.

References

• C. Beck, E. G. D. Cohen, Superstatistics, Physica A 322 (2003) 267–275.
• D. F. Andrews, C. L. Mallows, Scale mixtures of normal distributions, J. Roy. Statist. Soc. Ser. B 36 (1974) 99–102.

T1 — Gaussian/Gamma scale-mixture = Student-t (pure analytic / integral form)

Marginalising a zero-mean Gaussian of precision β against a Gamma(a,b) prior on β yields the (unnormalised) Student-t density. In Mathlib pieces: Real.Gamma, ProbabilityTheory.gaussianPDFReal, ProbabilityTheory.gammaPDFReal exist, but no MIXTURE / compound / subordination identity does. Setting a = ν/2, b = ν σ²/2 recovers Student-t_ν(scale σ) ∝ (1 + x²/(νσ²))^(−(ν+1)/2). Proof: substitute u = β (b + x²/2), pull constants, recognise Real.Gamma (a+1/2) via Real.Gamma_eq_integral / integral_rpow_mul_exp_neg_mul_Ioi-style Gamma integrals.

The right-hand side carries the Gamma normalization b^a; with a=ν/2, b=νσ²/2 this is the properly normalised Student-t_ν density (b^a·(b+x²/2)^(-(a+1/2)) collapses to the standard (1+x²/(νσ²))^(-(ν+1)/2) shape times the σ/normalisation constants).

theorem Superstatistics.gaussian_gamma_mixture_studentt (a b x : ℝ) (ha : 0 < a) (hb : 0 < b) : ∫ (β : ℝ) in Set.Ioi 0, √(β / (2 * Real.pi)) * Real.exp (-(β * x ^ 2) / 2) * (b ^ a / Real.Gamma a) * β ^ (a - 1) * Real.exp (-(b * β)) = b ^ a * Real.Gamma (a + 1 / 2) / (Real.Gamma a * √(2 * Real.pi)) * (b + x ^ 2 / 2) ^ (-(a + 1 / 2))

T2 — Gaussian variance-mixture is leptokurtic (excess kurtosis ≥ 0)

If X = √V · Z with Z ~ N(0,1) ⟂ V ≥ 0, then kurtosis(X) = 3 · E[V²]/E[V]² ≥ 3, equality iff V a.s. constant; excess kurtosis = 3 · Var(V)/E[V]². Mathlib DEFINES no kurtosis, so the whole claim reduces to the Jensen core E[V]² ≤ E[V²], which is exactly variance_nonneg unfolded via variance_eq_sub (Var V = E[V²] − E[V]²). This lemma IS the leptokurtic engine.

theorem Superstatistics.sq_expectation_le_expectation_sq {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (V : Ω → ℝ) (hV : MeasureTheory.MemLp V 2 μ) : (∫ (ω : Ω), V ω ∂μ) ^ 2 ≤ ∫ (ω : Ω), (V ^ 2) ω ∂μ

theorem Superstatistics.variance_mixture_excess_kurtosis_nonneg {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (V : Ω → ℝ) : 0 ≤ ProbabilityTheory.variance V μ

Explicit leptokurtic form: excess kurtosis = 3·Var(V)/E[V]² ≥ 0. Stated as the nonnegativity of Var(V)/E[V]² (the 3· and the √V·Z kurtosis identity are downstream). Leans on variance_nonneg.

Standard-normal moments E[Z²]=1, E[Z⁴]=3 (the leptokurtic inputs)

Computed via the moment-generating function: with Z ~ N(0,1) the mgf is t ↦ exp(t²/2), and E[Z^n] = (d/dt)^n mgf |₀ (iteratedDeriv_mgf_zero). Differentiating exp(t²/2) four times gives the polynomial-times-Gaussian tower t·e, (1+t²)·e, (3t+t³)·e, (3+6t²+t⁴)·e; evaluating at 0 yields 1 and 3.

theorem Superstatistics.std_normal_second_moment : ∫ (z : ℝ), z ^ 2 ∂ProbabilityTheory.gaussianReal 0 1 = 1

Standard-normal second moment: E[Z²] = 1.

theorem Superstatistics.std_normal_fourth_moment : ∫ (z : ℝ), z ^ 4 ∂ProbabilityTheory.gaussianReal 0 1 = 3

Standard-normal fourth moment: E[Z⁴] = 3.

theorem Superstatistics.variance_mixture_kurtosis_identity (eX2 eX4 eV eV2 varV : ℝ) (hX2 : eX2 = eV) (hX4 : eX4 = 3 * eV2) (hvar : varV = eV2 - eV ^ 2) (heV : 0 < eV) (hJ : eV ^ 2 ≤ eV2) : eX4 / eX2 ^ 2 = 3 * eV2 / eV ^ 2 ∧ eX4 / eX2 ^ 2 - 3 = 3 * varV / eV ^ 2 ∧ 3 ≤ eX4 / eX2 ^ 2

Leptokurtic identity for a variance-mixture Gaussian. Writing X = √V·Z with Z ~ N(0,1) ⟂ V ≥ 0, the independence factorisation gives E[X²] = E[V]·E[Z²] = E[V] and E[X⁴] = E[V²]·E[Z⁴] = 3·E[V²], the standard-normal moments E[Z²]=1, E[Z⁴]=3 being std_normal_second_moment and std_normal_fourth_moment. Given those two moment facts (as hX2, hX4) and E[V] > 0, the kurtosis is E[X⁴]/E[X²]² = 3·E[V²]/E[V]², the EXCESS kurtosis equals 3·Var(V)/E[V]², and (since Var(V) ≥ 0) the kurtosis is ≥ 3: the mixture is leptokurtic.

The independence-factorisation step E[V·Z²] = E[V]·E[Z²], E[V²·Z⁴] = E[V²]·E[Z⁴] (which produces hX2, hX4 from X = √V·Z) is taken as a hypothesis here; variance_mixture_kurtosis_identity' derives it on a concrete product space.

Self-contained version: the factorisation DERIVED from a product space

variance_mixture_kurtosis_identity above took the independence factorisation E[X²]=E[V], E[X⁴]=3·E[V²] as hypotheses (hX2, hX4). Here we DISCHARGE them: we build the concrete independent product space μ := μV.prod (gaussianReal 0 1) on ℝ × ℝ, set V ω = ω.1, Z ω = ω.2, X ω = √(ω.1)·ω.2, and derive both moment identities from Mathlib's Fubini factorisation integral_prod_mul (∫ f(z.1)·g(z.2) ∂(μ.prod ν) = (∫f ∂μ)·(∫g ∂ν), unconditional) together with the standard-normal moments std_normal_second_moment/std_normal_fourth_moment.

The ONLY remaining hypotheses are legitimate ones on the mixing law μV: its second L²-integrability (MemLp (·) 2 μV, needed for the Jensen step E[V]²≤E[V²]), V ≥ 0 a.e. (hVnn, so (√V)²=V), and E[V] > 0 (heV). No factorisation hypothesis remains — it is now a THEOREM (via integral_prod_mul).

theorem Superstatistics.variance_mixture_kurtosis_identity' (μV : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μV] (hV2 : MeasureTheory.MemLp (fun (v : ℝ) => v) 2 μV) (hVnn : ∀ᵐ (v : ℝ) ∂μV, 0 ≤ v) (heV : 0 < ∫ (v : ℝ), v ∂μV) : (∫ (ω : ℝ × ℝ), (√ω.1 * ω.2) ^ 4 ∂μV.prod (ProbabilityTheory.gaussianReal 0 1)) / (∫ (ω : ℝ × ℝ), (√ω.1 * ω.2) ^ 2 ∂μV.prod (ProbabilityTheory.gaussianReal 0 1)) ^ 2 = (3 * ∫ (v : ℝ), v ^ 2 ∂μV) / (∫ (v : ℝ), v ∂μV) ^ 2 ∧ (∫ (ω : ℝ × ℝ), (√ω.1 * ω.2) ^ 4 ∂μV.prod (ProbabilityTheory.gaussianReal 0 1)) / (∫ (ω : ℝ × ℝ), (√ω.1 * ω.2) ^ 2 ∂μV.prod (ProbabilityTheory.gaussianReal 0 1)) ^ 2 - 3 = 3 * (∫ (v : ℝ), v ^ 2 ∂μV - (∫ (v : ℝ), v ∂μV) ^ 2) / (∫ (v : ℝ), v ∂μV) ^ 2 ∧ 3 ≤ (∫ (ω : ℝ × ℝ), (√ω.1 * ω.2) ^ 4 ∂μV.prod (ProbabilityTheory.gaussianReal 0 1)) / (∫ (ω : ℝ × ℝ), (√ω.1 * ω.2) ^ 2 ∂μV.prod (ProbabilityTheory.gaussianReal 0 1)) ^ 2