Moments of Student's t law

This file proves the mean, variance, polynomial moment thresholds and exponential moment domain of the Student t distribution defined in TauCeti/Probability/Distributions/StudentT/Basic.lean. The cumulative distribution function is computed in TauCeti/Probability/Distributions/StudentT/Cdf.lean. The density is even, and on the positive half-line the substitution w = x ^ 2 / ν turns every weighted integral into Euler's second beta integral ∫ w ^ (a - 1) * (1 + w) ^ (-(a + b)) = Β(a, b), so the weighted density is integrable there exactly for -1 < q < ν; the exponential-moment statements read off that sharp threshold.

Main results

• integrable_pow_studentTMeasure_iff — within the nondegenerate family, a natural power is integrable exactly when its degree is less than the degrees of freedom;
• integrable_id_studentTMeasure_iff and integral_id_studentTMeasure — within the nondegenerate family the mean exists exactly when 1 < ν, while its Bochner integral is zero for every parameter;
• integrable_sq_studentTMeasure_iff, integral_sq_studentTMeasure and variance_id_studentTMeasure — the second moment exists exactly when 2 < ν, and then both it and the variance equal ν / (ν - 2);
• integrable_exp_mul_id_studentTMeasure_iff — exp (t · x) is integrable exactly at t = 0;
• integrableExpSet_id_studentTMeasure — the exponential-moment domain is the singleton {0}, together with the matching non-integrability statement for every nonzero rate.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 2, 2nd ed., Wiley (1995), ch. 28.

Polynomial moments

@[simp]

theorem TauCeti.Probability.integrable_pow_studentTMeasure_iff {ν : ℝ} (hν : 0 < ν) (q : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ q) (studentTMeasure ν) ↔ ↑q < ν

A natural power is integrable under a nondegenerate Student t law exactly when its degree is less than the degrees of freedom.

@[simp]

theorem TauCeti.Probability.integrable_id_studentTMeasure_iff {ν : ℝ} (hν : 0 < ν) : MeasureTheory.Integrable id (studentTMeasure ν) ↔ 1 < ν

The identity is integrable under a nondegenerate Student t law exactly when the number of degrees of freedom exceeds one.

@[simp]

theorem TauCeti.Probability.integral_id_studentTMeasure (ν : ℝ) : ∫ (x : ℝ), x ∂studentTMeasure ν = 0

The Bochner integral of the identity under a Student t measure is zero for every parameter, including by convention when the identity is not integrable.

@[simp]

theorem TauCeti.Probability.integral_sq_studentTMeasure {ν : ℝ} (hν : 2 < ν) : ∫ (x : ℝ), x ^ 2 ∂studentTMeasure ν = ν / (ν - 2)

The second raw moment of a Student t law is ν / (ν - 2) when 2 < ν.

theorem TauCeti.Probability.integrable_sq_studentTMeasure_iff {ν : ℝ} (hν : 0 < ν) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ 2) (studentTMeasure ν) ↔ 2 < ν

Squaring is integrable under a nondegenerate Student t law exactly when the number of degrees of freedom exceeds two.

theorem TauCeti.Probability.not_integrable_sq_studentTMeasure {ν : ℝ} (hν : 0 < ν) (hν2 : ν ≤ 2) : ¬MeasureTheory.Integrable (fun (x : ℝ) => x ^ 2) (studentTMeasure ν)

At or below two degrees of freedom, the second raw moment of a nondegenerate Student t law diverges.

@[simp]

theorem TauCeti.Probability.variance_id_studentTMeasure {ν : ℝ} (hν : 2 < ν) : ProbabilityTheory.variance id (studentTMeasure ν) = ν / (ν - 2)

The variance of a Student t law is ν / (ν - 2) when 2 < ν.

Exponential moments

theorem TauCeti.Probability.not_integrable_exp_mul_id_studentTMeasure {ν : ℝ} (hν : 0 < ν) {t : ℝ} (ht : t ≠ 0) : ¬MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (studentTMeasure ν)

The exponential of a nonzero multiple of the identity is not integrable under a Student t law: if exp (t * x) and exp (-t * x) were both integrable, then every moment would be finite, contradicting the sharp moment threshold q < ν.

@[simp]

theorem TauCeti.Probability.integrable_exp_mul_id_studentTMeasure_iff {ν : ℝ} (hν : 0 < ν) (t : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (studentTMeasure ν) ↔ t = 0

The exponential integrand of a Student t law is integrable exactly at rate zero.

@[simp]

theorem TauCeti.Probability.integrableExpSet_id_studentTMeasure {ν : ℝ} (hν : 0 < ν) : ProbabilityTheory.integrableExpSet id (studentTMeasure ν) = {0}

The exponential-integrability domain of the identity under a Student t law is the singleton {0}: every nonzero exponential moment diverges in the polynomial tails.