The cumulative distribution function of Student's t law

This file computes the cumulative distribution function of the Student t distribution defined in TauCeti/Probability/Distributions/StudentT/Basic.lean. On the positive half-line the substitution w = x ^ 2 / ν turns the tail integral into Euler's second beta integral, and the substitution u = w / (1 + w) then turns it into the regularized incomplete beta function.

Main results

• cdf_studentTMeasure_eq — writing z = ν / (ν + x ^ 2), the cdf is regularizedIncompleteBeta (ν / 2) (1 / 2) z / 2 for x < 0 and 1 - regularizedIncompleteBeta (ν / 2) (1 / 2) z / 2 for 0 ≤ x.

References

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

The cumulative distribution function

@[simp]

theorem TauCeti.Probability.cdf_studentTMeasure_eq {ν : ℝ} (hν : 0 < ν) (x : ℝ) : ↑(ProbabilityTheory.cdf (studentTMeasure ν)) x = if x < 0 then regularizedIncompleteBeta (ν / 2) (1 / 2) (ν / (ν + x ^ 2)) / 2 else 1 - regularizedIncompleteBeta (ν / 2) (1 / 2) (ν / (ν + x ^ 2)) / 2

The cumulative distribution function of a Student t law. Writing z = ν / (ν + x ^ 2), it is regularizedIncompleteBeta (ν / 2) (1 / 2) z / 2 for x < 0 and 1 - regularizedIncompleteBeta (ν / 2) (1 / 2) z / 2 for 0 ≤ x.