Frisch–Waugh–Lovell theorem

TheoremFrisch–Waugh–Lovell#✓fully proved

Frisch–Waugh–Lovell for weighted least squares with a symmetric weight matrix W: if (b, t) solves the normal equations of the regression of y on [A | z] and z⊥ = z - A u is the weighted residual of z on A (Aᵀ W z⊥ = 0), then t ⟪z⊥, z⊥⟫_W = ⟪z⊥, y⟫_W, where ⟪x, y⟫_W = x ⬝ᵥ W y.

theorem frischWaughLovell {W : Matrix m m ℝ} (hW : Wᵀ = W) {A : Matrix m κ ℝ}
    {y z : m → ℝ} {b u : κ → ℝ} {t : ℝ}
    (hA : Aᵀ *ᵥ (W *ᵥ (y - A *ᵥ b - t • z)) = 0)
    (hz : z ⬝ᵥ (W *ᵥ (y - A *ᵥ b - t • z)) = 0)
    (hu : Aᵀ *ᵥ (W *ᵥ (z - A *ᵥ u)) = 0) :
    t * ((z - A *ᵥ u) ⬝ᵥ (W *ᵥ (z - A *ᵥ u))) = (z - A *ᵥ u) ⬝ᵥ (W *ᵥ y)

Used by 1

Used byFrisch–Waugh–Lovell, residualized form

TheoremFrisch–Waugh–Lovell, residualized form#✓fully proved

Under the hypotheses of frischWaughLovell, if also y⊥ = y - A v is the weighted residual of y on A (Aᵀ W y⊥ = 0), then t ⟪z⊥, z⊥⟫_W = ⟪z⊥, y⊥⟫_W: the coefficient of z in the full regression is the coefficient of the regression of the residualized response on the residualized regressor.

theorem frischWaughLovell_residual {W : Matrix m m ℝ} (hW : Wᵀ = W) {A : Matrix m κ ℝ}
    {y z : m → ℝ} {b u v : κ → ℝ} {t : ℝ}
    (hA : Aᵀ *ᵥ (W *ᵥ (y - A *ᵥ b - t • z)) = 0)
    (hz : z ⬝ᵥ (W *ᵥ (y - A *ᵥ b - t • z)) = 0)
    (hu : Aᵀ *ᵥ (W *ᵥ (z - A *ᵥ u)) = 0) :
    t * ((z - A *ᵥ u) ⬝ᵥ (W *ᵥ (z - A *ᵥ u))) = (z - A *ᵥ u) ⬝ᵥ (W *ᵥ (y - A *ᵥ v))

Uses 1 · Used by 1

Proof usesFrisch–Waugh–Lovell

Used byFrisch–Waugh–Lovell, solved form

TheoremFrisch–Waugh–Lovell, solved form#✓fully proved

Under the hypotheses of frischWaughLovell_residual, if ⟪z⊥, z⊥⟫_W ≠ 0 then t = ⟪z⊥, y⊥⟫_W / ⟪z⊥, z⊥⟫_W.

theorem frischWaughLovell_eq_div {W : Matrix m m ℝ} (hW : Wᵀ = W) {A : Matrix m κ ℝ}
    {y z : m → ℝ} {b u v : κ → ℝ} {t : ℝ}
    (hA : Aᵀ *ᵥ (W *ᵥ (y - A *ᵥ b - t • z)) = 0)
    (hz : z ⬝ᵥ (W *ᵥ (y - A *ᵥ b - t • z)) = 0)
    (hu : Aᵀ *ᵥ (W *ᵥ (z - A *ᵥ u)) = 0)
    (hne : (z - A *ᵥ u) ⬝ᵥ (W *ᵥ (z - A *ᵥ u)) ≠ 0) :
    t = (z - A *ᵥ u) ⬝ᵥ (W *ᵥ (y - A *ᵥ v)) / ((z - A *ᵥ u) ⬝ᵥ (W *ᵥ (z - A *ᵥ u)))

Uses 1

Proof usesFrisch–Waugh–Lovell, residualized form

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.