Student's t distribution

Student's t law with ν degrees of freedom is the symmetric law on the line with density proportional to (1 + x ^ 2 / ν) ^ (-(ν + 1) / 2). This file defines it, proves that it is a probability measure for 0 < ν, identifies it as a MeasureTheory.HasPDF law with that density, records its reflection symmetry, and identifies the one degree of freedom member of the family with the standard Cauchy law. Polynomial and exponential moment results live in TauCeti/Probability/Distributions/StudentT/Moments.lean.

Boundary. The number of degrees of freedom must be positive for the density to normalize, so both studentTPDFReal and studentTMeasure are defined to vanish for ν ≤ 0 (studentTMeasure_of_nonpos); every formula describing the probability law carries 0 < ν as a hypothesis.

Main definitions

• TauCeti.Probability.studentTPDFReal — the real-valued density;
• TauCeti.Probability.studentTPDF — its ℝ≥0∞-valued companion;
• TauCeti.Probability.studentTMeasure — the law;
• TauCeti.Probability.studentTMeasure_def — its withDensity presentation.

Main results

• isProbabilityMeasure_studentTMeasure — it is a probability measure when 0 < ν;
• hasPDF_of_hasLaw_studentTMeasure, pdf_eq_studentTPDF_of_hasLaw_studentTMeasure and rnDeriv_studentTMeasure — the HasPDF bridge, the density, and the Radon–Nikodym derivative;
• studentTMeasure_map_neg — the law is invariant under reflection in the origin;
• studentTMeasure_one — one degree of freedom gives the standard Cauchy law ProbabilityTheory.cauchyMeasure 0 1;
• measurable_studentTMeasure — the family is measurable in its parameter, so it can be used as a kernel.

Implementation

The whole analytic content is the normalization. Scaling by √ν with MeasureTheory.integral_comp_mul_left reduces the total mass of (1 + x ^ 2 / ν) ^ (-(ν + 1) / 2) to that of the Cauchy-type kernel (1 + x ^ 2) ^ (-(ν + 1) / 2), which is TauCeti.integral_one_add_sq_rpow: the value Β(1 / 2, ν / 2) of Euler's second beta integral. Writing that value as a quotient of Gamma values cancels the normalizing constant exactly. The moment modules reuse the same normalization and symmetry facts.

References

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

The density

noncomputable def TauCeti.Probability.studentTPDFReal (ν x : ℝ) : ℝ

The density of Student's t law with ν degrees of freedom, as a real-valued function.

For ν ≤ 0 there is no such law and the density is 0.

Equations

• TauCeti.Probability.studentTPDFReal ν x = if 0 < ν then Real.Gamma ((ν + 1) / 2) / (√(ν * Real.pi) * Real.Gamma (ν / 2)) * (1 + x ^ 2 / ν) ^ (-((ν + 1) / 2)) else 0

noncomputable def TauCeti.Probability.studentTPDF (ν x : ℝ) : ENNReal

The density of Student's t law, as a function valued in ℝ≥0∞.

Equations

• TauCeti.Probability.studentTPDF ν x = ENNReal.ofReal (TauCeti.Probability.studentTPDFReal ν x)

@[simp]

theorem TauCeti.Probability.studentTPDFReal_of_nonpos {ν : ℝ} (hν : ν ≤ 0) (x : ℝ) : studentTPDFReal ν x = 0

Outside the valid parameter range the density vanishes.

@[simp]

theorem TauCeti.Probability.studentTPDFReal_of_pos {ν : ℝ} (hν : 0 < ν) (x : ℝ) : studentTPDFReal ν x = Real.Gamma ((ν + 1) / 2) / (√(ν * Real.pi) * Real.Gamma (ν / 2)) * (1 + x ^ 2 / ν) ^ (-((ν + 1) / 2))

For a positive number of degrees of freedom the density is the Student t formula.

@[simp]

theorem TauCeti.Probability.studentTPDF_of_pos {ν : ℝ} (hν : 0 < ν) (x : ℝ) : studentTPDF ν x = ENNReal.ofReal (Real.Gamma ((ν + 1) / 2) / (√(ν * Real.pi) * Real.Gamma (ν / 2)) * (1 + x ^ 2 / ν) ^ (-((ν + 1) / 2)))

For a positive number of degrees of freedom the ℝ≥0∞-valued density is the Student t formula.

@[simp]

theorem TauCeti.Probability.studentTPDF_of_nonpos {ν : ℝ} (hν : ν ≤ 0) (x : ℝ) : studentTPDF ν x = 0

Outside the valid parameter range the ℝ≥0∞-valued density vanishes.

theorem TauCeti.Probability.studentT_const_pos {ν : ℝ} (hν : 0 < ν) : 0 < Real.Gamma ((ν + 1) / 2) / (√(ν * Real.pi) * Real.Gamma (ν / 2))

The normalizing constant of Student's t law is positive.

theorem TauCeti.Probability.studentTPDFReal_pos {ν : ℝ} (hν : 0 < ν) (x : ℝ) : 0 < studentTPDFReal ν x

For a positive number of degrees of freedom the density is strictly positive everywhere: the Student t law has no vanishing tail.

theorem TauCeti.Probability.studentTPDFReal_nonneg (ν x : ℝ) : 0 ≤ studentTPDFReal ν x

The Student t density is nonnegative at every parameter, valid or not.

@[simp]

theorem TauCeti.Probability.toReal_studentTPDF (ν x : ℝ) : (studentTPDF ν x).toReal = studentTPDFReal ν x

The two Student t densities agree under ENNReal.toReal; the density is never infinite.

theorem TauCeti.Probability.studentTPDF_lt_top (ν x : ℝ) : studentTPDF ν x < ⊤

The ℝ≥0∞-valued Student t density is finite.

@[simp]

theorem TauCeti.Probability.studentTPDFReal_neg (ν x : ℝ) : studentTPDFReal ν (-x) = studentTPDFReal ν x

The Student t density is even in the sample point.

@[simp]

theorem TauCeti.Probability.studentTPDF_neg (ν x : ℝ) : studentTPDF ν (-x) = studentTPDF ν x

The ℝ≥0∞-valued Student t density is even in the sample point.

theorem TauCeti.Probability.measurable_studentTPDFReal (ν : ℝ) : Measurable (studentTPDFReal ν)

The real-valued Student t density is measurable.

theorem TauCeti.Probability.measurable_studentTPDF (ν : ℝ) : Measurable (studentTPDF ν)

The ℝ≥0∞-valued Student t density is measurable.

The measure and its total mass

noncomputable def TauCeti.Probability.studentTMeasure (ν : ℝ) : MeasureTheory.Measure ℝ

Student's t probability measure with ν degrees of freedom.

For ν ≤ 0 this is the zero measure, not a probability measure; see studentTMeasure_of_nonpos.

This is presented as Lebesgue measure with density studentTPDF ν; use studentTMeasure_def when a proof needs the withDensity representation.

Equations

• TauCeti.Probability.studentTMeasure ν = MeasureTheory.volume.withDensity (TauCeti.Probability.studentTPDF ν)

theorem TauCeti.Probability.studentTMeasure_def (ν : ℝ) : studentTMeasure ν = MeasureTheory.volume.withDensity (studentTPDF ν)

The defining withDensity presentation of Student's t measure.

@[simp]

theorem TauCeti.Probability.studentTMeasure_of_nonpos {ν : ℝ} (hν : ν ≤ 0) : studentTMeasure ν = 0

Outside the valid parameter range Student's t law is the zero measure.

theorem TauCeti.Probability.integrable_studentTPDFReal (ν : ℝ) : MeasureTheory.Integrable (studentTPDFReal ν) MeasureTheory.volume

The Student t density is integrable on the whole line for every parameter.

theorem TauCeti.Probability.integral_studentTPDFReal {ν : ℝ} (hν : 0 < ν) : ∫ (x : ℝ), studentTPDFReal ν x = 1

The Student t density integrates to 1.

theorem TauCeti.Probability.lintegral_studentTPDF_eq_one {ν : ℝ} (hν : 0 < ν) : ∫⁻ (x : ℝ), studentTPDF ν x = 1

The ℝ≥0∞-valued Student t density has total mass 1.

theorem TauCeti.Probability.isProbabilityMeasure_studentTMeasure {ν : ℝ} (hν : 0 < ν) : MeasureTheory.IsProbabilityMeasure (studentTMeasure ν)

For a positive number of degrees of freedom Student's t law is a probability measure.

Absolute continuity

theorem TauCeti.Probability.hasPDF_of_hasLaw_studentTMeasure {ν : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (studentTMeasure ν) P) : MeasureTheory.HasPDF X P MeasureTheory.volume

A random variable with a Student t law has a density.

theorem TauCeti.Probability.pdf_eq_studentTPDF_of_hasLaw_studentTMeasure {ν : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (studentTMeasure ν) P) : MeasureTheory.pdf X P MeasureTheory.volume =ᵐ[MeasureTheory.volume] studentTPDF ν

The density of a Student t law is studentTPDF.

theorem TauCeti.Probability.rnDeriv_studentTMeasure (ν : ℝ) : (studentTMeasure ν).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] studentTPDF ν

The Radon–Nikodym derivative of a Student t law against Lebesgue measure is studentTPDF.

theorem TauCeti.Probability.studentTMeasure_absolutelyContinuous (ν : ℝ) : (studentTMeasure ν).AbsolutelyContinuous MeasureTheory.volume

Student's t measure is absolutely continuous with respect to Lebesgue measure.

theorem TauCeti.Probability.integrable_studentTMeasure_iff {ν : ℝ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} : MeasureTheory.Integrable f (studentTMeasure ν) ↔ MeasureTheory.Integrable (fun (x : ℝ) => studentTPDFReal ν x • f x) MeasureTheory.volume

A Student t law presented through its real-valued density.

theorem TauCeti.Probability.measureReal_studentTMeasure {ν : ℝ} {s : Set ℝ} (hs : MeasurableSet s) : (studentTMeasure ν).real s = ∫ (z : ℝ) in s, studentTPDFReal ν z

The real mass of a measurable set under a Student t law is the integral of its real-valued density.

Symmetry

theorem TauCeti.Probability.studentTMeasure_map_neg (ν : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => -x) (studentTMeasure ν) = studentTMeasure ν

Student's t law is invariant under reflection in the origin: its density is even and Lebesgue measure is reflection invariant.

One degree of freedom

theorem TauCeti.Probability.studentTPDFReal_one (x : ℝ) : studentTPDFReal 1 x = ProbabilityTheory.cauchyPDFReal 0 1 x

With one degree of freedom the Student t density is the standard Cauchy density.

theorem TauCeti.Probability.studentTMeasure_one : studentTMeasure 1 = ProbabilityTheory.cauchyMeasure 0 1

Student's t law with one degree of freedom is the standard Cauchy law.

Parameter measurability

theorem TauCeti.Probability.measurable_uncurry_studentTPDF : Measurable fun (q : ℝ × ℝ) => studentTPDF q.1 q.2

The Student t density is jointly measurable in the degrees of freedom and the sample point.

theorem TauCeti.Probability.measurable_studentTMeasure : Measurable fun (ν : ℝ) => studentTMeasure ν

The Student t family is measurable in its degrees of freedom.