Theorem 7.3 — Asymptotic normality of OLS (scalar projection)

Open the canonical result card

Textbook statement

Under i.i.d. sampling and the moment conditions of Theorem 7.2 (CLT for the score X_i e_i), the OLS estimator is asymptotically normal:

\sqrt{n}\,(\hat\beta_n - \beta) \xrightarrow{d} N\!\left(0,\; Q^{-1} \Omega Q^{-1}\right),

where

Q = \mathbb{E}[X_i X_i^\top], \qquad \Omega = \mathbb{E}[e_i^2 X_i X_i^\top]

is the score covariance. The asymptotic variance V := Q^{-1} \Omega Q^{-1} is the sandwich matrix; under homoskedasticity (\Omega = \sigma^2 Q) it collapses to \sigma^2 Q^{-1}.

The Lean formalization works through the scalar (Cramér–Wold) face: for every fixed direction a \in \mathbb{R}^k,

\sqrt{n}\, a^\top (\hat\beta_n - \beta) \xrightarrow{d} N(0,\, a^\top V a).

Assumptions

Hansen Theorem 7.3 requires:

  • Linear model: y_i = X_i^\top \beta + e_i.
  • i.i.d. sampling under measure \mu.
  • Population Gram matrix invertibility: Q := \mathbb{E}[X_i X_i^\top] is invertible.
  • Score moment finiteness: \Omega := \mathbb{E}[e_i^2 X_i X_i^\top] is finite (entries integrable). This is what powers Theorem 7.2’s CLT.
  • Mean-zero score: \mathbb{E}[X_i e_i] = 0 (which is automatic when \beta is the projection coefficient and e_i is the projection error).

In Lean, these are bundled into SampleCLTAssumption72 μ X e, which extends SampleMomentAssumption71.

Lean statement

The headline theorem in HansenEconometrics/Chapter7Asymptotics.lean:

theorem scoreProjection_olsBetaStar_tendstoInDistribution_gaussian_covariance
    {μ : Measure Ω} [IsProbabilityMeasure μ]
    {ν : Measure Ω'} [IsProbabilityMeasure ν]
    {X : ℕ → Ω → (k → ℝ)} {e : ℕ → Ω → ℝ} {y : ℕ → Ω → ℝ}
    (h : SampleCLTAssumption72 μ X e) (β a : k → ℝ)
    (hmodel : ∀ i ω, y i ω = (X i ω) ⬝ᵥ β + e i ω)
    {Z : Ω' → ℝ}
    (hZ : HasLaw Z
      (gaussianReal 0 (olsProjectionAsymptoticVariance μ X e a).toNNReal) ν) :
    TendstoInDistribution
      (fun (n : ℕ) ω =>
        (Real.sqrt (n : ℝ) •
          (olsBetaStar (stackRegressors X n ω) (stackOutcomes y n ω) - β)) ⬝ᵥ a)
      atTop Z (fun _ => μ) ν

Reading the statement

In English: given an i.i.d. sample (X_i, e_i) on probability space (\Omega, \mu) satisfying the score-CLT moment assumptions of Theorem 7.2, a true coefficient \beta, a fixed projection direction a, the linear model y_i = X_i^\top \beta + e_i, and a random variable Z on an auxiliary probability space (\Omega', \nu) with the named Gaussian law, the scalar projection \sqrt{n}\, a^\top (\hat\beta_n^\ast - \beta) converges in distribution (under sample measure \mu) to Z.

Lean Math What it gives us
{μ : Measure Ω} [IsProbabilityMeasure μ] (\Omega, \mu) Given: the sample probability space. The sequence (X_i, e_i) lives here. Curly braces mark μ as implicit (inferred from later arguments).
{ν : Measure Ω'} [IsProbabilityMeasure ν] (\Omega', \nu) Given: an auxiliary probability space hosting the limiting Gaussian. This is the Lean idiom for “convergence in distribution to a random variable defined elsewhere” — the limit Z lives on (\Omega', \nu), not on the sample space.
{X : ℕ → Ω → (k → ℝ)} (X_i)_{i \in \mathbb{N}} Given: the regressor sequence. X i ω : k → ℝ is observation i’s regressor vector, indexed by the regressor coordinate type k.
{e : ℕ → Ω → ℝ} (e_i)_{i \in \mathbb{N}} Given: the error / disturbance sequence.
{y : ℕ → Ω → ℝ} (y_i)_{i \in \mathbb{N}} Given: the response sequence.
(h : SampleCLTAssumption72 μ X e) Hansen Assumption 7.2 Given (hypothesis): the bundled package — i.i.d. sampling, identical distributions, \mathbb{E}[X_i e_i] = 0, L^2 moments on the score X_i e_i, and the score covariance is finite. This is everything Theorem 7.2 needs. It extends SampleMomentAssumption71, so Theorem 7.1’s WLLN inputs come along for free.
(β a : k → ℝ) \beta, a \in \mathbb{R}^k Given: the true coefficient \beta (so the OLS error is \hat\beta_n^\ast - \beta) and the projection direction a (so we read a^\top (\hat\beta_n^\ast - \beta)).
(hmodel : ∀ i ω, y i ω = (X i ω) ⬝ᵥ β + e i ω) y_i = X_i^\top \beta + e_i Given (hypothesis): the linear model, asserted pointwise on every i and every \omega. ⬝ᵥ is Matrix.dotProduct.
{Z : Ω' → ℝ} Z : \Omega' \to \mathbb{R} Given: the random variable that will play the role of the Gaussian limit, on the auxiliary space.
(hZ : HasLaw Z (gaussianReal 0 (olsProjectionAsymptoticVariance μ X e a).toNNReal) ν) Z \sim N(0, V_a) Given (hypothesis): the law of Z on (\Omega', \nu) is exactly N(0, V_a), where V_a = a^\top Q^{-1} \Omega Q^{-1} a is the named asymptotic variance. The .toNNReal is the variance argument’s nonnegative coercion (Mathlib’s gaussianReal takes a nonnegative variance).
TendstoInDistribution (fun n ω => (Real.sqrt (n : ℝ) • (olsBetaStar … - β)) ⬝ᵥ a) atTop Z (fun _ => μ) ν \sqrt{n}\, a^\top (\hat\beta_n^\ast - \beta) \xrightarrow{d} Z Conclusion: scalar convergence in distribution. The sample statistic, indexed by n, lives under measure \mu (the constant family fun _ => μ); Z lives under \nu. Real.sqrt (n : ℝ) • (… - β) is the scaled error vector; ⬝ᵥ a projects onto direction a. olsBetaStar is the totalized OLS estimator (returns 0 when the sample Gram is singular), so the statement is meaningful even on the measure-zero singular set.

(The ambient typeclasses [Fintype k] [DecidableEq k] and the measurable structures on Ω, Ω' are in the file’s variable block.)

Companion / related theorems:

Translation notes

  • Hansen writes the theorem as a multivariate convergence \sqrt{n}\, (\hat\beta - \beta) \Rightarrow N(0, V). Lean works through the Cramér–Wold face: every scalar projection converges to a normal limit. The aggregator scoreProjection_olsBetaStar_tendstoInDistribution_gaussian_covariance_all combines all directions.
  • The auxiliary measure space (\Omega', \nu) hosts the limiting random variable Z. This is a Lean idiom: rather than asserting a measure equals a Gaussian, the theorem says “for any Z defined on any auxiliary space with the right law, the sample statistics converge in distribution to Z.”
  • The named asymptotic variance olsProjectionAsymptoticVarianceμ X e a unfolds to ((Q^{-1})^\top a)^\top \Omega ((Q^{-1})^\top a). By the symmetry of Q, (Q^{-1})^\top = Q^{-1}, so this is exactly a^\top Q^{-1} \Omega Q^{-1} a = a^\top V a.
  • The score variance equality a^\top V a = \mathrm{Var}[e_0 \cdot (X_0 \cdot Q^{-1} a)] is exposed as scoreProjection_variance_eq_quadraticScoreCovariance and is used to bridge between the variance form Lean works with and the textbook sandwich form.

Proof sketch

The standard textbook proof in three steps:

  1. OLS error decomposition. From the closed form,

    \sqrt{n}(\hat\beta_n - \beta) = \hat Q_n^{-1} \cdot \sqrt{n}\, \hat g_n, \qquad \hat g_n := \frac{1}{n} \sum_i X_i e_i.

  2. Score CLT (Theorem 7.2). For every fixed c \in \mathbb{R}^k,

    \sqrt{n}\, c^\top \hat g_n \xrightarrow{d} N(0, c^\top \Omega c)

    by the multivariate CLT applied to X_i e_i in direction c.

  3. Slutsky. Since \hat Q_n^{-1} \xrightarrow{p} Q^{-1} (Theorem 7.1’s WLLN + continuous-mapping), the product \hat Q_n^{-1} \cdot \sqrt{n}\, \hat g_n \xrightarrow{d} Q^{-1} \cdot Z where Z \sim N(0, \Omega), so the limit is N(0, Q^{-1} \Omega Q^{-1}).

For the scalar projection face: project everything onto direction a first (i.e., apply a^\top), apply the score CLT in direction Q^{-1} a, then put it back together via Slutsky.

Lean proof structure

The Lean proof has serious moving parts. Trace the chain:

  1. scoreProjection_sum_tendstoInDistribution_gaussian at HansenEconometrics/Chapter7Asymptotics.lean:4773 — Theorem 7.2 scalar CLT for \sqrt{n}\, c^\top \hat g_n.
  2. Slutsky bridges via the inverse-Gram convergence and the fixed-score decomposition. The key algebraic identity is scoreProjection_sqrt_smul_olsBetaStar_sub_eq_residual_add_fixedScore_add_inverseGap at HansenEconometrics/Chapter7Asymptotics.lean:1491 — this is the algebraic decomposition of \sqrt{n}\, a^\top (\hat\beta^\ast_n - \beta) into a fixed score, an inverse-gap term, and a residual; the latter two are o_p(1).
  3. inverseGapProjection_tendstoInMeasure_zero_of_coord at HansenEconometrics/Chapter7Asymptotics.lean:1415 — the inverse-gap residual goes to 0 in probability.
  4. scoreProjection_olsBetaStar_tendstoInDistribution_gaussian_of_finalMeas at HansenEconometrics/Chapter7Asymptotics.lean:5277 — packages the chain modulo a measurability hypothesis.
  5. scoreProjection_olsBetaStar_tendstoInDistribution_gaussian at HansenEconometrics/Chapter7Asymptotics.lean:5307 — discharges the measurability via scoreProjection_sqrt_smul_olsBetaStar_sub_aemeasurable.
  6. scoreProjection_olsBetaStar_tendstoInDistribution_gaussian_covariance at HansenEconometrics/Chapter7Asymptotics.lean:5332 — restates the result using the named asymptotic variance, via scoreProjection_variance_eq_quadraticScoreCovariance.

The chain is heavy because the Lean version handles olsBetaStar (the totalized estimator) and has to manage the singular-sample contribution explicitly — an issue Hansen sidesteps by working “modulo events of probability tending to zero.”

Tactic-by-tactic walkthrough

The headline theorem at line 5332 has a short body: it hypothesis-massages the Gaussian variance into the named-asymptotic-variance form, then defers to the variance-form sibling.

theorem scoreProjection_olsBetaStar_tendstoInDistribution_gaussian_covariance
    {μ : Measure Ω} [IsProbabilityMeasure μ]
    {ν : Measure Ω'} [IsProbabilityMeasure ν]
    {X : ℕ → Ω → (k → ℝ)} {e : ℕ → Ω → ℝ} {y : ℕ → Ω → ℝ}
    (h : SampleCLTAssumption72 μ X e) (β a : k → ℝ)
    (hmodel : ∀ i ω, y i ω = (X i ω) ⬝ᵥ β + e i ω)
    {Z : Ω' → ℝ}
    (hZ : HasLaw Z
      (gaussianReal 0 (olsProjectionAsymptoticVariance μ X e a).toNNReal) ν) :
    TendstoInDistribution
      (fun (n : ℕ) ω =>
        (Real.sqrt (n : ℝ) •
          (olsBetaStar (stackRegressors X n ω) (stackOutcomes y n ω) - β)) ⬝ᵥ a)
      atTop Z (fun _ => μ) ν := by
  have hZ' : HasLaw Z
      (gaussianReal 0
        (Var[fun ω => (e 0 ω • X 0 ω) ⬝ᵥ ((popGram μ X)⁻¹)ᵀ *ᵥ a; μ]).toNNReal)
      ν := by
    rw [scoreProjection_variance_eq_quadraticScoreCovariance
      (μ := μ) (X := X) (e := e) h (((popGram μ X)⁻¹)ᵀ *ᵥ a)]
    simpa [olsProjectionAsymptoticVariance] using hZ
  exact scoreProjection_olsBetaStar_tendstoInDistribution_gaussian
    (μ := μ) (ν := ν) (X := X) (e := e) (y := y) h β a hmodel hZ'

What each step is doing:

  • have hZ' : … := by … — re-state the Gaussian-law hypothesis on Z using the variance-form parameter, so we can hand it to the sibling scoreProjection_olsBetaStar_tendstoInDistribution_gaussian. The two variances are equal but have different syntactic shapes: \mathrm{Var}[(e_0 X_0) \cdot ((Q^{-1})^\top a); \mu] on the variance-form side and olsProjectionAsymptoticVariance μ X e a (the named matrix-form ((Q^{-1})^\top a)^\top \Omega ((Q^{-1})^\top a)) on the covariance-form side.
  • rw [scoreProjection_variance_eq_quadraticScoreCovariance …] — apply Theorem 7.2’s covariance-matrix face (line 2503) in direction ((Q^{-1})^\top a). This rewrites the variance of the score projection as the quadratic form ((Q^{-1})^\top a)^\top \Omega ((Q^{-1})^\top a).
  • simpa [olsProjectionAsymptoticVariance] using hZ — unfold the named asymptotic variance on the goal side; the resulting expression matches the hypothesis hZ directly.
  • exact scoreProjection_olsBetaStar_tendstoInDistribution_gaussian … — hand off to the variance-form headline at line 5307 with the rewritten Gaussian hypothesis hZ'.

So the line-5332 wrapper is essentially a one-line bridge: the real work sits in the variance-form chain it composes. Walking that chain top-down:

  • scoreProjection_olsBetaStar_tendstoInDistribution_gaussian (line 5307) — same Theorem 7.3 statement but with the Gaussian variance in variance-form. Its body discharges the measurability premise of the _of_finalMeas variant by applying scoreProjection_sqrt_smul_olsBetaStar_sub_aemeasurable.
  • scoreProjection_olsBetaStar_tendstoInDistribution_gaussian_of_finalMeas (line 5277) — same statement with an explicit AEMeasurable premise. Its body discharges the score-bounded premise of an even more upstream variant from scoreCoordinate_sampleCrossMoment_boundedInProbability, passing through a chain that eventually reduces the goal to a Slutsky combination of a CLT term and an o_p(1) inverse-gap term.
  • scoreProjection_sum_tendstoInDistribution_gaussian (line 4773) — the score CLT (Theorem 7.2 face). Supplies the Gaussian limit for (\sqrt{n})^{-1} \sum_i (e_i X_i) \cdot c in any fixed direction c. Used in direction c = (Q^{-1})^\top a.
  • scoreProjection_sqrt_smul_olsBetaStar_sub_eq_residual_add_fixedScore_add_inverseGap (line 1491) — the algebraic decomposition: at every n and \omega, \sqrt{n}\, a^\top (\hat\beta_n^\ast - \beta) equals the sum of (i) a scaled singular-sample residual, (ii) the fixed-Q^{-1} score projection (which gets the CLT), and (iii) the random-inverse-gap projection (which needs Slutsky).
  • inverseGapProjection_tendstoInMeasure_zero_of_coord (line 1415) — the Slutsky o_p(1) control: the random-inverse-gap term ((\hat Q_n^{-1} - Q^{-1}) \sqrt{n}\, \hat g_n) \cdot a goes to zero in measure, because each coordinate weight goes to 0 in probability (continuous mapping on \hat Q_n^{-1} \to Q^{-1}) and the score coordinates are bounded in probability.
  • scoreProjection_variance_eq_quadraticScoreCovariance (line 2503) — the variance bridge invoked by the line-5332 wrapper: rewrites \mathrm{Var}[(e_0 X_0) \cdot c; \mu] = c^\top \Omega c, so the variance-form Gaussian and the named-covariance Gaussian agree.

Putting it together: line 5332 reformulates the limit Gaussian’s variance, line 5307 discharges measurability, line 5277 packages a Slutsky combination, line 4773 supplies the CLT term, line 1491 says what the OLS scalar projection is algebraically, and line 1415 says the only remaining piece is o_p(1).

Downstream uses