The OLS t-statistic is Student’s t.

This is a machine-checked proof that the usual t-test in linear regression follows a t distribution.

t_{j} = \frac{{β̂}_{j} - β_{j}}{s \sqrt{{[{(X^{'} X)}^{- 1}]}_{j j}}} \sim t_{n - p}

with $s^{2}$ the residual mean square on $n - p$ degrees of freedom.

Applied work uses the result constantly. A complete proof is rare. The nodes below are green only when Lean compiled them.

1 proved · 0 stated · 24 remaining of 25

build 7cc7ba7 · mathlib 8f9d9cf · sorry 0 · 2026-08-12