Theorem 3.5 — Frisch–Waugh–Lovell

Open the coefficient result card Open the residual result card

Textbook statement

Partition the regressors X = [X_1, X_2] with k_1 and k_2 columns respectively, and consider the full regression

y = X_1 \hat\beta_1 + X_2 \hat\beta_2 + \hat e.

Let M_1 = I - X_1(X_1^\top X_1)^{-1} X_1^\top be the annihilator for X_1, and define the residualized quantities \tilde y = M_1 y and \tilde X_2 = M_1 X_2.

The Frisch–Waugh–Lovell theorem states:

  1. Coefficient part. The second-block coefficient \hat\beta_2 from the full regression equals the coefficient from the auxiliary OLS of \tilde y on \tilde X_2: \hat\beta_2 = (\tilde X_2^\top \tilde X_2)^{-1} \tilde X_2^\top \tilde y.
  2. Residual part. The residuals from the auxiliary regression equal the residuals from the full regression: \tilde y - \tilde X_2 \hat\beta_2 = \hat e.

So you can recover the partial effect \hat\beta_2 — and the same residuals — by first partialling out X_1 from both y and X_2, then running OLS on the residualized variables.

Assumptions

  • Partitioned design X = [X_1, X_2] with X_1 \in \mathbb{R}^{n\times k_1}, X_2 \in \mathbb{R}^{n\times k_2}.
  • X_1^\top X_1 is invertible (the first block has full column rank).
  • The full Gram matrix [X_1, X_2]^\top [X_1, X_2] is invertible (the joint design has full column rank).
  • The residualized Gram matrix \tilde X_2^\top \tilde X_2 = (M_1 X_2)^\top (M_1 X_2) is invertible.
  • No distributional assumption — FWL is a purely algebraic identity.

Lean statement

All in HansenEconometrics/Chapter3FWL.lean:

The two headline theorems:

theorem fromColsRightBeta_eq_fwlBeta
    (X₁ : Matrix n k₁ ℝ) (X₂ : Matrix n k₂ ℝ) (y : n → ℝ)
    [DecidableEq n] [Fintype k₁] [DecidableEq k₁] [Fintype k₂] [DecidableEq k₂]
    [Invertible (X₁ᵀ * X₁)]
    [Invertible ((Matrix.fromCols X₁ X₂)ᵀ * Matrix.fromCols X₁ X₂)]
    [Invertible ((residualizedRegressors X₁ X₂)ᵀ * residualizedRegressors X₁ X₂)] :
    fromColsRightBeta X₁ X₂ y = fwlBeta X₁ X₂ y

theorem fwl_residual_eq_full_residual
    (X₁ : Matrix n k₁ ℝ) (X₂ : Matrix n k₂ ℝ) (y : n → ℝ)
    [DecidableEq n] [Fintype k₁] [DecidableEq k₁] [Fintype k₂] [DecidableEq k₂]
    [Invertible (X₁ᵀ * X₁)]
    [Invertible ((Matrix.fromCols X₁ X₂)ᵀ * Matrix.fromCols X₁ X₂)]
    [Invertible ((residualizedRegressors X₁ X₂)ᵀ * residualizedRegressors X₁ X₂)] :
    residual (residualizedRegressors X₁ X₂) (annihilatorMatrix X₁ *ᵥ y) =
      residual (Matrix.fromCols X₁ X₂) y

Reading the statement

In English (coefficient part): given a partitioned design [X_1, X_2], a response vector y, and witnesses that X_1^\top X_1, the full Gram matrix, and the residualized Gram matrix are all invertible, the second-block coefficient from the full regression equals the OLS coefficient from regressing M_1 y on M_1 X_2.

Lean Math What it gives us
(X₁ : Matrix n k₁ ℝ) X_1 \in \mathbb{R}^{n\times k_1} Given: first block of regressors. The index types n, k₁, k₂ come from the file’s variable block.
(X₂ : Matrix n k₂ ℝ) X_2 \in \mathbb{R}^{n\times k_2} Given: second block of regressors. Same row index n so the two blocks can be column-glued.
(y : n → ℝ) y \in \mathbb{R}^n Given: response vector, modeled as a function n → ℝ.
[DecidableEq n] (decidable equality on \{1,\ldots,n\}) Mathlib bookkeeping: Lean needs to decide row equality to define the annihilator M_1 = I - X_1(X_1^\top X_1)^{-1}X_1^\top (the identity matrix is built using if i = j).
[Fintype k₁] [Fintype k₂] k_1, k_2 finite Mathlib bookkeeping: column index types are finite, so matrix sums and products are well-defined.
[DecidableEq k₁] [DecidableEq k₂] (decidable equality on column indices) Mathlib bookkeeping: needed for identity matrices on the column spaces and for fromCols-style index manipulation.
[Invertible (X₁ᵀ * X₁)] X_1^\top X_1 invertible Given (hypothesis): first block has full column rank — needed so M_1 is well-defined.
[Invertible ((Matrix.fromCols X₁ X₂)ᵀ * Matrix.fromCols X₁ X₂)] [X_1,X_2]^\top[X_1,X_2] invertible Given (hypothesis): the joint design has full column rank — needed so the full-regression coefficient olsBeta (fromCols X₁ X₂) y exists.
[Invertible ((residualizedRegressors X₁ X₂)ᵀ * residualizedRegressors X₁ X₂)] \tilde X_2^\top \tilde X_2 invertible Given (hypothesis): the residualized regressors have full column rank — needed so fwlBeta, the auxiliary OLS coefficient, exists.
fromColsRightBeta X₁ X₂ y \hat\beta_2 from the full regression LHS of the conclusion. Defined as fun j => olsBeta (fromCols X₁ X₂) y (Sum.inr j) — projecting the full coefficient vector to its X_2 block via Sum.inr.
= fwlBeta X₁ X₂ y = (\tilde X_2^\top\tilde X_2)^{-1}\tilde X_2^\top\tilde y Conclusion: equality of the two k₂ → ℝ vectors. fwlBeta is defined as olsBeta (M₁ X₂) (M₁ y).

(Square brackets mark instance arguments — they are filled in by Lean’s typeclass resolution rather than supplied positionally. The three Invertible instances are the substantive economic/algebraic hypotheses; the DecidableEq/Fintype instances are Mathlib boilerplate that lets the machinery run.)

Supporting / helper theorems used internally:

Translation notes

  • Hansen states FWL with \hat\beta_2 from regressing \tilde y on \tilde X_2; Lean defines fwlBeta := olsBeta (M_1 X_2) (M_1 y). Identical.
  • Lean uses Matrix.fromCols X₁ X₂ for the column-partitioned [X_1, X_2]. The full-regression coefficients are projected to their two blocks via Sum.inl / Sum.inr (the index type is k₁ ⊕ k₂).
  • The residual part of FWL is stated using the auxiliary regression’s residual; the textbook commonly states “\tilde y - \tilde X_2 \hat\beta_2 = \hat e” with \hat\beta_2 from the full regression. Lean’s fwl_residual_eq_full_residual is the corresponding equality in the formalization.
  • Three invertibility instances are required for the coefficient theorem: X_1^\top X_1, [X_1, X_2]^\top [X_1, X_2], and \tilde X_2^\top \tilde X_2. The third is genuinely needed — without it, fwlBeta is undefined.

Proof sketch

The argument has two halves.

Coefficient part. Show that the full-regression coefficient \hat\beta_2 satisfies the auxiliary normal equations

\tilde X_2^\top (\tilde y - \tilde X_2 \hat\beta_2) = 0,

then invoke uniqueness of the OLS solution.

To verify the auxiliary normal equations, decompose \tilde y - \tilde X_2 \hat\beta_2. Substitute \tilde y = M_1 y and \tilde X_2 = M_1 X_2, and use \hat e = y - X_1 \hat\beta_1 - X_2 \hat\beta_2 from the full regression. After algebra,

\tilde y - \tilde X_2 \hat\beta_2 = M_1 \hat e.

Now use X_1^\top \hat e = 0 (normal equations for the X_1 block of the full regression) to get M_1 \hat e = \hat e, so \tilde y - \tilde X_2 \hat\beta_2 = \hat e. Premultiplying by \tilde X_2^\top = X_2^\top M_1 and using X_2^\top \hat e = 0 (the other block’s normal equations) gives the auxiliary normal equations. Uniqueness then implies \hat\beta_2 is the auxiliary regression’s coefficient.

Residual part. The chain above already showed \tilde y - \tilde X_2 \hat\beta_2 = \hat e, which is exactly the residual identity once you observe that the auxiliary regression’s residual at the FWL coefficient is \tilde y - \tilde X_2 \hat\beta_2^{\text{FWL}} and \hat\beta_2^{\text{FWL}} = \hat\beta_2 by the coefficient part.

Lean proof structure

The proof in Lean follows the sketch closely:

  1. fwl_auxiliary_residual_eq_annihilator_full_residual (line 106) shows \tilde y - \tilde X_2 \cdot \hat\beta_2^{\text{full}} = M_1 \hat e_{\text{full}}. It unfolds residual and fitted, splits the full fit via fromCols_full_fitted_eq (line 83), and uses Matrix.mulVec_mulVec plus annihilator_mul_X to drop the X_1 contribution.
  2. fwl_fromColsRightBeta_normal_equations (line 123) takes that bridge and applies X_1^\top \hat e = 0 to collapse M_1 \hat e = \hat e via annihilator_mulVec_eq_self_of_regressors_orthogonal. Then it premultiplies by \tilde X_2^\top and uses normal_equations_fromCols_right to finish.
  3. fromColsRightBeta_eq_fwlBeta (line 147) is the symmetric closure: from the auxiliary normal equations, olsBeta_eq_of_normal_equations (Chapter3LeastSquaresAlgebra.lean:67) yields fwlBeta = fromColsRightBeta.
  4. fwl_residual_eq_full_residual (line 163) reuses the same bridge and the orthogonal-fixed-point lemma to conclude.

The orthogonality “infrastructure” underpinning the proof is regressors_transpose_mul_annihilator (line 37, X^\top M = 0) and residualizedRegressors_orthogonal_left (line 94, X_1^\top \tilde X_2 = 0). Every collapse of M_1-products in the proof above ultimately reduces to one of these.

Tactic-by-tactic walkthrough

The headline theorem itself is short — it just packages uniqueness of OLS:

theorem fromColsRightBeta_eq_fwlBeta
    (X₁ : Matrix n k₁ ℝ) (X₂ : Matrix n k₂ ℝ) (y : n → ℝ)
    [DecidableEq n] [Fintype k₁] [DecidableEq k₁] [Fintype k₂] [DecidableEq k₂]
    [Invertible (X₁ᵀ * X₁)]
    [Invertible ((Matrix.fromCols X₁ X₂)ᵀ * Matrix.fromCols X₁ X₂)]
    [Invertible ((residualizedRegressors X₁ X₂)ᵀ * residualizedRegressors X₁ X₂)] :
    fromColsRightBeta X₁ X₂ y = fwlBeta X₁ X₂ y := by
  symm
  unfold fwlBeta
  exact olsBeta_eq_of_normal_equations
    (residualizedRegressors X₁ X₂)
    (annihilatorMatrix X₁ *ᵥ y)
    (fromColsRightBeta X₁ X₂ y)
    (fwl_fromColsRightBeta_normal_equations X₁ X₂ y)

Line by line:

  • symm — flip the goal from fromColsRightBeta X₁ X₂ y = fwlBeta X₁ X₂ y to fwlBeta X₁ X₂ y = fromColsRightBeta X₁ X₂ y. This sets things up so the = reads “the auxiliary OLS coefficient equals this candidate vector,” which is the shape olsBeta_eq_of_normal_equations produces.
  • unfold fwlBeta — replace fwlBeta X₁ X₂ y by its definition, olsBeta (residualizedRegressors X₁ X₂) (annihilatorMatrix X₁ *ᵥ y). The goal becomes olsBeta (M₁ X₂) (M₁ y) = fromColsRightBeta X₁ X₂ y.
  • exact olsBeta_eq_of_normal_equations … — apply the OLS uniqueness lemma (olsBeta_eq_of_normal_equations) with design matrix \tilde X_2, response \tilde y = M_1 y, candidate coefficient $_2 = $ fromColsRightBeta X₁ X₂ y, and the proof that this candidate satisfies the auxiliary normal equations. That last argument is fwl_fromColsRightBeta_normal_equations X₁ X₂ y, which is where the actual FWL algebra happens.

The substantive work lives in fwl_fromColsRightBeta_normal_equations (line 123). Its proof body:

theorem fwl_fromColsRightBeta_normal_equations
    (X₁ : Matrix n k₁ ℝ) (X₂ : Matrix n k₂ ℝ) (y : n → ℝ)
    [DecidableEq n] [Fintype k₁] [DecidableEq k₁] [Fintype k₂] [DecidableEq k₂]
    [Invertible (X₁ᵀ * X₁)]
    [Invertible ((Matrix.fromCols X₁ X₂)ᵀ * Matrix.fromCols X₁ X₂)] :
    (residualizedRegressors X₁ X₂)ᵀ *ᵥ
        (annihilatorMatrix X₁ *ᵥ y -
          residualizedRegressors X₁ X₂ *ᵥ fromColsRightBeta X₁ X₂ y) = 0 := by
  rw [fwl_auxiliary_residual_eq_annihilator_full_residual]
  have hM :
      annihilatorMatrix X₁ *ᵥ residual (Matrix.fromCols X₁ X₂) y =
        residual (Matrix.fromCols X₁ X₂) y :=
    annihilator_mulVec_eq_self_of_regressors_orthogonal X₁
      (residual (Matrix.fromCols X₁ X₂) y)
      (normal_equations_fromCols_left X₁ X₂ y)
  rw [hM]
  unfold residualizedRegressors
  rw [Matrix.transpose_mul, annihilatorMatrix_transpose]
  rw [← Matrix.mulVec_mulVec (residual (Matrix.fromCols X₁ X₂) y) X₂ᵀ
    (annihilatorMatrix X₁)]
  rw [hM]
  exact normal_equations_fromCols_right X₁ X₂ y

Line by line:

  • rw [fwl_auxiliary_residual_eq_annihilator_full_residual] — rewrite the inner subtraction \tilde y - \tilde X_2 \hat\beta_2 as M_1 \hat e_{\text{full}} using the bridge lemma at line 106. The goal becomes \tilde X_2^\top \cdot (M_1 \hat e_{\text{full}}) = 0.
  • have hM := … — record the fact that M_1 acts as the identity on the full residual: M_1 \hat e_{\text{full}} = \hat e_{\text{full}}. This uses annihilator_mulVec_eq_self_of_regressors_orthogonal applied to the first-block normal equations normal_equations_fromCols_left X₁ X₂ y (which says X_1^\top \hat e_{\text{full}} = 0).
  • rw [hM] — apply that identity. The goal is now \tilde X_2^\top \cdot \hat e_{\text{full}} = 0.
  • unfold residualizedRegressors — replace \tilde X_2 by M_1 X_2 on the left of the matrix-vector product. Goal: (M_1 X_2)^\top \cdot \hat e_{\text{full}} = 0.
  • rw [Matrix.transpose_mul, annihilatorMatrix_transpose] — distribute the transpose: (M_1 X_2)^\top = X_2^\top M_1^\top = X_2^\top M_1 (the annihilator is symmetric). Goal: (X_2^\top M_1) \cdot \hat e_{\text{full}} = 0.
  • rw [← Matrix.mulVec_mulVec …] — rewrite the matrix product (X_2^\top M_1) \cdot v as the iterated matrix-vector application X_2^\top \cdot (M_1 \cdot v), applied backwards (the ← direction). Goal: X_2^\top \cdot (M_1 \hat e_{\text{full}}) = 0.
  • rw [hM] — collapse M_1 \hat e_{\text{full}} to \hat e_{\text{full}} again. Goal: X_2^\top \cdot \hat e_{\text{full}} = 0.
  • exact normal_equations_fromCols_right X₁ X₂ y — discharge the goal: this is exactly the second-block normal equations for the full regression (X_2^\top \hat e_{\text{full}} = 0, line 26).

The shape of the proof is “rewrite using the bridge, kill the M_1 on both sides using X_1^\top \hat e = 0, then finish with X_2^\top \hat e = 0” — exactly the algebraic sketch above, broken into seven rw/exact steps.

Downstream uses

  • fwl_normal_equations (line 181) — straightforward consequence, packaged as the auxiliary regression’s normal equations.
  • fwl_residual_maker_mul_fromCols (line 195) — the sequential residual-maker M_{\tilde X_2} M_1 kills both X_1 and X_2, used in projection-geometry arguments downstream.
  • (Future) Chapter 4 / 7 partial-effect arguments will likely consume FWL — not yet wired up at the time of writing.