Theorem 7.1 — Consistency of OLS

Open the canonical result card

Textbook statement

Suppose we observe an i.i.d. sample (X_i, e_i) drawn from the population (X, e) on a probability space (\Omega, \mu), and form the response y_i = X_i^\top \beta + e_i. Stack the first n observations into a regressor matrix X_{(n)} and outcome vector y_{(n)}. Under the moment assumptions that \mathbb{E}[X_i X_i^\top] is invertible, \mathbb{E}\|X_i\|^2 < \infty, and \mathbb{E}\|X_i e_i\| < \infty, the OLS estimator from the stacked sample converges in probability to \beta:

\hat\beta_{(n)} \xrightarrow{p} \beta \qquad \text{as } n \to \infty.

This is “consistency”: OLS recovers the true parameter \beta in the large-sample limit.

Assumptions

Hansen Theorem 7.1 requires:

  • Linear model with stable parameter: y_i = X_i^\top \beta + e_i for all i, with \beta \in \mathbb{R}^k fixed.
  • i.i.d. sampling under measure \mu.
  • Population Gram matrix invertibility: \mathbb{E}[X_i X_i^\top] = Q is invertible (full-rank regressors in population).
  • Finite second moment of regressors: \mathbb{E}\|X_i\|^2 < \infty — needed for the WLLN of the sample Gram.
  • Finite first moment of cross-product: \mathbb{E}\|X_i e_i\| < \infty — needed for the WLLN of the sample cross-moment.

In Lean, these are bundled into a single typeclass SampleMomentAssumption71 μ X e.

Lean statement

The textbook-facing theorem lives in HansenEconometrics/Chapter7Asymptotics.lean:

theorem olsBetaOrZero_stack_tendstoInMeasure_beta
    {μ : Measure Ω} [IsFiniteMeasure μ]
    {X : ℕ → Ω → (k → ℝ)} {e : ℕ → Ω → ℝ} {y : ℕ → Ω → ℝ} (β : k → ℝ)
    (h : SampleMomentAssumption71 μ X e)
    (hmodel : ∀ i ω, y i ω = (X i ω) ⬝ᵥ β + e i ω) :
    TendstoInMeasure μ
      (fun n ω => olsBetaOrZero (stackRegressors X n ω) (stackOutcomes y n ω))
      atTop (fun _ => β)

Reading the statement

In English: given a probability space (\Omega, \mu), an i.i.d. sequence of regressor rows X_i and errors e_i satisfying the moment assumptions, and a true coefficient \beta that links outcomes to regressors via y_i = X_i^\top \beta + e_i, the OLS estimator built from the first n stacked observations converges in probability to \beta as n \to \infty.

Lean Math What it gives us
{μ : Measure Ω} \mu on \Omega Given: the underlying measure on the sample space. Implicit ({...}), inferred from later arguments.
[IsFiniteMeasure μ] \mu(\Omega) < \infty Given (hypothesis): finite total mass — so probability statements like TendstoInMeasure are well-typed. Square brackets mark this as a typeclass instance.
{X : ℕ → Ω → (k → ℝ)} X_i : \Omega \to \mathbb{R}^k Given: the i.i.d. sequence of regressor row processes — observation i at sample point \omega is the row vector X_i(\omega).
{e : ℕ → Ω → ℝ} e_i : \Omega \to \mathbb{R} Given: the i.i.d. sequence of scalar error processes.
{y : ℕ → Ω → ℝ} y_i : \Omega \to \mathbb{R} Given: the i.i.d. sequence of scalar outcomes. Logically determined by X, e, and β via hmodel.
(β : k → ℝ) \beta \in \mathbb{R}^k Given: the true (population) coefficient vector — a fixed parameter, not random.
(h : SampleMomentAssumption71 μ X e) i.i.d. + moment + invertibility bundle Given (hypothesis): the bundled Theorem 7.1 assumptions: i.i.d. structure, integrability of X_i, X_i X_i^\top and X_i e_i, plus invertibility of the population Gram \mathbb{E}[X_i X_i^\top]. Each face is exposed as a separate field on h.
(hmodel : ∀ i ω, y i ω = (X i ω) ⬝ᵥ β + e i ω) y_i = X_i^\top \beta + e_i Given (hypothesis): the linear model holds pointwise at every observation i and every sample point \omega. ⬝ᵥ is Matrix.dotProduct (vector inner product).
TendstoInMeasure μ … atTop (fun _ => β) \hat\beta_n \xrightarrow{p} \beta Conclusion: convergence in probability under \mu as n \to \infty. The constant target fun _ => β is the fixed limit.
fun n ω => olsBetaOrZero (stackRegressors X n ω) (stackOutcomes y n ω) \hat\beta_{(n)}(\omega) The sample OLS estimator: stackRegressors X n ω builds the n \times k design from the first n rows at \omega, stackOutcomes y n ω stacks the first n outcomes, and olsBetaOrZero returns the closed-form OLS coefficient (or 0 on the singular set).

(The ambient typeclasses [Fintype k] [DecidableEq k] for the regressor index type, and the universe Ω : Type*, are hoisted into a variable block at the top of the file’s section.)

The Lean development uses a totalized estimator olsBetaStar (defined for every design and returning 0 when X^\top X is singular) together with a wrapper olsBetaOrZero that agrees with ordinary olsBeta whenever the sample Gram is nonsingular and equals olsBetaStar unconditionally. The asymptotic statement uses olsBetaOrZero because measurability is cleaner — singular samples have measure zero in the limit, so the wrapper’s behavior on those samples doesn’t matter.

The substantive work is done by the totalized companion theorem:

The wrapper version reduces to it via olsBetaOrZero_eq_olsBetaStar.

Translation notes

  • Hansen writes \hat\beta_n \to_p \beta. Lean writes TendstoInMeasure μ (fun n ω => olsBetaOrZero …) atTop (fun _ => β). These are the same notion: convergence in probability under measure \mu.
  • The SampleMomentAssumption71 typeclass packages: IsFiniteMeasure μ, i.i.d. structure, integrability of X_i, integrability of X_i \cdot X_i and X_i e_i, plus invertibility of \mathbb{E}[X X^\top]. Each face is exposed as a separate lemma so that downstream proofs can pick out exactly the moment hypothesis they need.
  • The Lean form uses stackRegressors X n and stackOutcomes y n to build the sample design matrix and outcome vector from the i.i.d. processes X : ℕ → Ω → (k → ℝ) and y : ℕ → Ω → ℝ. This exposes the stacking as a measurable function rather than a hand-waved “first n observations.”
  • The theorem is stated for olsBetaOrZero, not olsBeta, because the latter requires [Invertible (Xᵀ * X)] as a typeclass — which we cannot guarantee on every \omega. olsBetaOrZero returns 0 outside the nonsingular set; on the asymptotic limit set, it agrees with ordinary OLS.

Proof sketch

The standard textbook argument:

  1. Sample-moment WLLN. By the i.i.d. WLLN applied to X_i X_i^\top and X_i e_i: \hat Q_n := \frac{1}{n}\sum_{i=1}^n X_i X_i^\top \xrightarrow{p} Q, \qquad \hat g_n := \frac{1}{n}\sum_{i=1}^n X_i e_i \xrightarrow{p} \mathbb{E}[X_i e_i].
  2. Cross moment is zero in the linear model. Under the linear-model hypothesis the cross-moment limit reduces to 0 (the Lean development states this directly as a tendsto-to-zero claim, sidestepping the intermediate orthogonality identity).
  3. Continuous mapping. Since Q is invertible and inversion is continuous on the open set of invertible matrices, \hat Q_n^{-1} \xrightarrow{p} Q^{-1} on the limit set.
  4. OLS error decomposition. \hat\beta_n - \beta = \hat Q_n^{-1} \hat g_n, so by Slutsky’s theorem \hat\beta_n - \beta \xrightarrow{p} Q^{-1} \cdot 0 = 0.

Lean proof structure

The Lean proof breaks into many supporting lemmas; the headline theorem is short because it composes pieces.

The deterministic algebraic engine:

The sample-moment WLLN faces:

The Slutsky / continuous-mapping bridge that combines them:

The totalized consistency theorem packages all of this:

The ordinary-wrapper version on line 1822 is then a one-liner:

simpa [olsBetaOrZero_eq_olsBetaStar] using
  olsBetaStar_stack_tendstoInMeasure_beta
    (μ := μ) (X := X) (e := e) (y := y) β h hmodel

Tactic-by-tactic walkthrough

The headline wrapper (line 1822). The full proof body of olsBetaOrZero_stack_tendstoInMeasure_beta is two lines:

theorem olsBetaOrZero_stack_tendstoInMeasure_beta … := by
  simpa [olsBetaOrZero_eq_olsBetaStar] using
    olsBetaStar_stack_tendstoInMeasure_beta
      (μ := μ) (X := X) (e := e) (y := y) β h hmodel

There is essentially nothing to walk through here — the wrapper version reduces immediately to the totalized version. The olsBetaOrZero_eq_olsBetaStar rewrite (line 265) replaces olsBetaOrZero by olsBetaStar pointwise, and simpa applies that rewrite to both sides of the totalized statement to produce the wrapper statement verbatim.

The totalized version (line 1600). The substantive proof is olsBetaStar_stack_tendstoInMeasure_beta. It is too long to walk line by line; instead, here is the role each composed lemma plays in the high-level structure (the proof is built around the identity \hat\beta_n - \beta = R'_n + \hat Q_n^{-1}\,\hat g_n, where R'_n is a “residual” term that vanishes on the nonsingular event):

  • Pointwise residual identity — olsBetaStar_sub_identity (line 714) gives, for every \omega, the algebraic decomposition \hat\beta_n - \beta - \hat Q_n^{-1}\,\hat g_n = (\hat Q_n^{-1}\hat Q_n - 1)\,\beta. The right-hand side is exactly R'_n — it equals 0 on \{\hat Q_n \text{ invertible}\} and -\beta off it.
  • Algebraic engine on nonsingular samples — olsBeta_sub_eq_sampleGram_inv_mulVec_sampleCrossMoment (line 512) is the deterministic Hansen §7.2 identity \hat\beta_n - \beta = \hat Q_n^{-1}\,\hat g_n on the invertible event. olsBetaStar_sub_identity is its olsBetaStar-on-all-of-\Omega extension.
  • Residual vanishes in probability — residual_tendstoInMeasure_zero (line 1144) shows R'_n \xrightarrow{p} 0. Inside, it uses measure_sampleGram_singular_tendsto_zero (the singular set has vanishing measure) plus the fact that R'_n \equiv 0 on the nonsingular event. This is loaded as hF6 and immediately re-shaped via the residual identity to give the “R'_n” tendsto piece.
  • Sample Gram WLLN — sampleGram_stackRegressors_tendstoInMeasure_popGram (line 838) gives \hat Q_n \xrightarrow{p} Q via the i.i.d. WLLN applied to X_i X_i^\top (uses the second-moment hypothesis from h).
  • Inversion-continuity — sampleGramInv_stackRegressors_tendstoInMeasure_popGramInv (line 875) lifts the Gram WLLN through matrix inversion: since matrix inversion is continuous at any nonsingular point and h.Q_nonsing guarantees Q is invertible, \hat Q_n^{-1} \xrightarrow{p} Q^{-1} on the limit set.
  • Cross-moment WLLN — sampleCrossMoment_stackRegressors_stackErrors_tendstoInMeasure_zero (line 892) gives \hat g_n \xrightarrow{p} 0. The cross-product X_i \cdot e_i has mean 0 in the linear-model setup (Hansen’s orthogonality axiom) and finite first moment, so the WLLN delivers a zero limit.
  • Slutsky combination — sampleGramInv_mulVec_sampleCrossMoment_e_tendstoInMeasure_zero (line 1042) combines the inverted-Gram tendsto with the cross-moment tendsto via tendstoInMeasure_mulVec to conclude \hat Q_n^{-1}\,\hat g_n \xrightarrow{p} Q^{-1} \cdot 0 = 0. This is loaded as hCore.
  • Add the two convergences — the proof then uses tendstoInMeasure_add to combine R'_n \xrightarrow{p} 0 (hR') and \hat Q_n^{-1}\,\hat g_n \xrightarrow{p} 0 (hCore), giving R'_n + \hat Q_n^{-1}\,\hat g_n \xrightarrow{p} 0. A second tendstoInMeasure_add against the constant tendsto for \beta shifts the limit to \beta.
  • Congr back to olsBetaStar — finally, hSumPlus.congr_left rewrites the sample function R'_n + \hat Q_n^{-1}\hat g_n + \beta back to \hat\beta_n^* using olsBetaStar_sub_identity once more, closing the goal.

(The intervening hGram_meas, hCrossE_meas, hInv_meas, hCoreMV_meas, hR'_meas blocks at lines 1608-1656 are all measurability boilerplate — they expand each sample function into a (1/n) • ∑ … form and chain AEStronglyMeasurable through the algebra. They feed the tendstoInMeasure_add and tendstoInMeasure_mulVec calls but contribute nothing mathematically beyond “everything in sight is measurable.”)

Downstream uses

  • Theorem 7.8 (continuous mapping for OLS): if \phi is continuous at \beta, then \phi(\hat\beta_n) \xrightarrow{p} \phi(\beta). Lean: continuousAt_function_olsBetaOrZero_tendstoInMeasure at HansenEconometrics/Chapter7Asymptotics.lean:1854.
  • Theorem 7.4 (variance estimator consistency): builds on \hat\beta \to_p \beta to show \hat\sigma^2 \to_p \sigma^2.
  • Theorem 7.3 (asymptotic normality): consistency is a precondition for the CLT-style result.