Chapter 3: The Algebra of Least Squares

Foldable textbook-to-Lean result crosswalk for Chapter 3.

This page is generated from the canonical Chapter 3 inventory and the compiled Lean environment. It contains 27 textbook result groups and 47 selected Lean endpoints. When an inventory row links a large proof surface, this page shows at most six theorem-facing endpoints. The inventory remains the source of truth for all supporting links, qualifications, and open gaps.

Theorem 3.1 objective-level argmin statement3 endpoints

\hat{\beta} = \arg\min_b (Y - X b)'(Y - X b)

theorem HansenEconometrics.sumSquaredErrors_olsBeta_le

Hansen Theorem 3.1 (existence half): olsBeta X y attains the minimum of the sum of squared errors. For any coefficient vector b, SSE(olsBeta X y) ≤ SSE(b).

Uniqueness — b = olsBeta X y whenever SSE(b) = SSE(olsBeta X y) — requires strict positive-definiteness of Xᵀ * X and is left to a follow-up.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) (b : k → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Real.instLE.le (HansenEconometrics.sumSquaredErrors X y (HansenEconometrics.olsBeta X y))
    (HansenEconometrics.sumSquaredErrors X y b)

Direct statement dependencies (2)

• HansenEconometrics.olsBeta
• HansenEconometrics.sumSquaredErrors

HansenEconometrics/Chapter3LeastSquaresAlgebra.lean:149

theorem HansenEconometrics.olsBeta_isMinOn

Hansen Theorem 3.1 (existence half), packaged as IsMinOn: olsBeta X y is a global minimizer of sumSquaredErrors X y over all of k → ℝ.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  IsMinOn (HansenEconometrics.sumSquaredErrors X y) Set.univ (HansenEconometrics.olsBeta X y)

Direct statement dependencies (2)

• HansenEconometrics.olsBeta
• HansenEconometrics.sumSquaredErrors

HansenEconometrics/Chapter3LeastSquaresAlgebra.lean:160

theorem HansenEconometrics.olsBeta_eq_of_minimizer

Hansen Theorem 3.1 (uniqueness half): if b attains the minimum of the SSE, then b = olsBeta X y. Combined with sumSquaredErrors_olsBeta_le and olsBeta_isMinOn, this completes Hansen’s Theorem 3.1: olsBeta X y is the unique minimizer of sumSquaredErrors X y over k → ℝ whenever Xᵀ * X is invertible.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) (b : k → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.sumSquaredErrors X y b)
      (HansenEconometrics.sumSquaredErrors X y (HansenEconometrics.olsBeta X y)) →
    Eq b (HansenEconometrics.olsBeta X y)

Direct statement dependencies (2)

• HansenEconometrics.olsBeta
• HansenEconometrics.sumSquaredErrors

HansenEconometrics/Chapter3LeastSquaresAlgebra.lean:170

Definition 3.1 sum of squared errors1 endpoint

S(b) = (Y - X b)'(Y - X b)

def HansenEconometrics.sumSquaredErrors

Hansen Definition 3.1: sum of squared errors, written in matrix notation.

Formal statement

{n : Type u_1} → {k : Type u_2} → [Fintype n] → [Fintype k] → Matrix n k Real → (n → Real) → (k → Real) → Real

HansenEconometrics/Chapter3LeastSquaresAlgebra.lean:14

Theorem 3.2 closed-form OLS coefficient1 endpoint

\hat{\beta} = (X'X)^{-1} X' Y

def HansenEconometrics.olsBeta

Hansen Theorem 3.2: closed-form OLS coefficient under invertibility of Xᵀ X.

Formal statement

{n : Type u_1} →
  {k : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : Fintype k] →
        [inst_2 : DecidableEq k] →
          (X : Matrix n k Real) →
            (n → Real) → [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] → k → Real

HansenEconometrics/Chapter3LeastSquaresAlgebra.lean:18

Theorem 3.2 normal equations1 endpoint

X' \hat{e} = 0

theorem HansenEconometrics.normal_equations

Hansen Theorem 3.2: normal equations in closed-form OLS notation.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (X.transpose.mulVec (HansenEconometrics.residual X y)) 0

Direct statement dependencies (1)

• HansenEconometrics.residual

HansenEconometrics/Chapter3LeastSquaresAlgebra.lean:53

Equation (3.17) residuals sum to zero with an intercept1 endpoint

\iota \in \operatorname{col}(X) \Longrightarrow \sum_i \hat{e}_i = 0

theorem HansenEconometrics.residual_sum_zero_of_one_mem_colspan

Hansen equation (3.17): if the regressor matrix contains a constant column, residuals sum to zero.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] {c : k → Real},
  Eq (X.mulVec c) 1 → Eq (Finset.univ.sum fun i => HansenEconometrics.residual X y i) 0

Direct statement dependencies (1)

• HansenEconometrics.residual

HansenEconometrics/Chapter3LeastSquaresAlgebra.lean:105

Section 3.11 hat matrix1 endpoint

P = X (X'X)^{-1} X'

def HansenEconometrics.hatMatrix

Hansen Section 3.11: the OLS projection / hat matrix P = X (Xᵀ X)⁻¹ Xᵀ.

Formal statement

{n : Type u_1} →
  {k : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : Fintype k] →
        [inst_2 : DecidableEq k] →
          (X : Matrix n k Real) →
            [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] → Matrix n n Real

HansenEconometrics/Chapter3Projections.lean:16

Section 3.12 annihilator matrix1 endpoint

M = I - P

def HansenEconometrics.annihilatorMatrix

Hansen Section 3.12: the annihilator matrix M = I - P.

Formal statement

{n : Type u_1} →
  {k : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : Fintype k] →
        [inst_2 : DecidableEq k] →
          (X : Matrix n k Real) →
            [DecidableEq n] →
              [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] → Matrix n n Real

HansenEconometrics/Chapter3Projections.lean:20

Theorem 3.3.1 hat-matrix symmetry1 endpoint

P' = P

theorem HansenEconometrics.hatMatrix_transpose

Hansen Theorem 3.3.1: the hat matrix is symmetric.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.hatMatrix X).transpose (HansenEconometrics.hatMatrix X)

Direct statement dependencies (1)

• HansenEconometrics.hatMatrix

HansenEconometrics/Chapter3Projections.lean:25

Theorem 3.3.2 hat-matrix idempotence1 endpoint

P^2 = P

theorem HansenEconometrics.hatMatrix_idempotent

Hansen Theorem 3.3.2: the hat matrix is idempotent.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq
    (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.hatMatrix X)
      (HansenEconometrics.hatMatrix X))
    (HansenEconometrics.hatMatrix X)

Direct statement dependencies (1)

• HansenEconometrics.hatMatrix

HansenEconometrics/Chapter3Projections.lean:89

Theorem 3.3.3 trace of the hat matrix1 endpoint

\operatorname{tr}(P) = k

theorem HansenEconometrics.hatMatrix_trace

Hansen Theorem 3.3.3: the trace of the hat matrix is the number of regressors.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.hatMatrix X).trace (Fintype.card k).cast

Direct statement dependencies (1)

• HansenEconometrics.hatMatrix

HansenEconometrics/Chapter3Projections.lean:98

Theorem 3.6 leverage values6 endpoints

h_{ii}=X_i'(X'X)^{-1}X_i, 0\le h_{ii}\le 1, h_{ii}\ge 1/n with an intercept, and \sum_i h_{ii}=k

def HansenEconometrics.leverageValue

Hansen equation (3.40): the ith leverage value is the ith diagonal entry of the hat matrix.

Formal statement

{n : Type u_1} →
  {k : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : Fintype k] →
        [inst_2 : DecidableEq k] →
          (X : Matrix n k Real) →
            [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] → n → Real

HansenEconometrics/Chapter3Projections.lean:113

theorem HansenEconometrics.leverageValue_eq_row_invGram_row

Hansen equation (3.40): leverage as the row quadratic form xᵢ’(X’X)⁻¹xᵢ.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] (i : n),
  Eq (HansenEconometrics.leverageValue X i)
    (dotProduct (X i) ((inst_3.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)).mulVec (X i)))

Direct statement dependencies (1)

• HansenEconometrics.leverageValue

HansenEconometrics/Chapter3Projections.lean:119

theorem HansenEconometrics.leverageValue_nonneg

Hansen Theorem 3.6.1: leverage values are nonnegative.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] (i : n),
  Real.instLE.le 0 (HansenEconometrics.leverageValue X i)

Direct statement dependencies (1)

• HansenEconometrics.leverageValue

HansenEconometrics/Chapter3Projections.lean:127

theorem HansenEconometrics.leverageValue_le_one

Hansen Theorem 3.6.1: leverage values are bounded above by one.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] (i : n),
  Real.instLE.le (HansenEconometrics.leverageValue X i) 1

Direct statement dependencies (1)

• HansenEconometrics.leverageValue

HansenEconometrics/Chapter3Projections.lean:201

theorem HansenEconometrics.inv_card_le_leverageValue_of_intercept

Hansen Theorem 3.6.2: if X contains an intercept, every leverage value is at least 1 / n.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] {c : k → Real},
  Eq (X.mulVec c) 1 →
    ∀ (i : n), Real.instLE.le (Real.instInv.inv (Fintype.card n).cast) (HansenEconometrics.leverageValue X i)

Direct statement dependencies (1)

• HansenEconometrics.leverageValue

HansenEconometrics/Chapter3Projections.lean:176

theorem HansenEconometrics.sum_leverageValue_eq_card

Hansen Theorem 3.6.3: the leverage values sum to the number of regressors.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (Finset.univ.sum fun i => HansenEconometrics.leverageValue X i) (Fintype.card k).cast

Direct statement dependencies (1)

• HansenEconometrics.leverageValue

HansenEconometrics/Chapter3Projections.lean:135

Theorem 3.7 leave-one-out regression6 of 9 linked endpoints

\hat{\beta}_{(-i)}=\hat{\beta}-(X'X)^{-1}X_i\tilde e_i and \tilde e_i=(1-h_{ii})^{-1}\hat e_i

theorem HansenEconometrics.leaveOneOutBeta_eq_olsBeta_sub_invGram_mulVec

Hansen Theorem 3.7 / equation (3.43): leave-one-out coefficients can be computed from the full-sample coefficient and prediction error.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) (i : n) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_4 : Invertible (HansenEconometrics.leaveOneOutGram X i)],
  Eq (HansenEconometrics.leaveOneOutBeta X y i)
    (instHSub.hSub (HansenEconometrics.olsBeta X y)
      (instHSMul.hSMul (HansenEconometrics.leaveOneOutResidual X y i)
        ((inst_3.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)).mulVec (X i))))

Direct statement dependencies (4)

• HansenEconometrics.leaveOneOutBeta
• HansenEconometrics.leaveOneOutGram
• HansenEconometrics.leaveOneOutResidual
• HansenEconometrics.olsBeta

HansenEconometrics/Chapter3Projections.lean:308

theorem HansenEconometrics.one_sub_leverage_mul_leaveOneOutResidual_eq_residual

Hansen Theorem 3.7 / equation (3.44), multiplication form: (1 - hᵢᵢ) ẽᵢ = êᵢ.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) (i : n) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_4 : Invertible (HansenEconometrics.leaveOneOutGram X i)],
  Eq
    (instHMul.hMul (instHSub.hSub 1 (HansenEconometrics.leverageValue X i))
      (HansenEconometrics.leaveOneOutResidual X y i))
    (HansenEconometrics.residual X y i)

Direct statement dependencies (4)

• HansenEconometrics.leaveOneOutGram
• HansenEconometrics.leaveOneOutResidual
• HansenEconometrics.leverageValue
• HansenEconometrics.residual

HansenEconometrics/Chapter3Projections.lean:340

theorem HansenEconometrics.leaveOneOutResidual_eq_inv_one_sub_leverage_mul_residual

Hansen Theorem 3.7 / equation (3.44): leave-one-out prediction errors are full-sample residuals scaled by (1 - hᵢᵢ)⁻¹.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) (i : n) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_4 : Invertible (HansenEconometrics.leaveOneOutGram X i)],
  Ne (instHSub.hSub 1 (HansenEconometrics.leverageValue X i)) 0 →
    Eq (HansenEconometrics.leaveOneOutResidual X y i)
      (instHMul.hMul (Real.instInv.inv (instHSub.hSub 1 (HansenEconometrics.leverageValue X i)))
        (HansenEconometrics.residual X y i))

Direct statement dependencies (4)

• HansenEconometrics.leaveOneOutGram
• HansenEconometrics.leaveOneOutResidual
• HansenEconometrics.leverageValue
• HansenEconometrics.residual

HansenEconometrics/Chapter3Projections.lean:364

theorem HansenEconometrics.leaveOneOutBetaDeleted_eq_leaveOneOutBeta

The literal row-deleted OLS coefficient agrees with the reduced-Gram leave-one-out coefficient used in Hansen Theorem 3.7.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) (i : n) [inst_3 : DecidableEq n] [inst_4 : Invertible (HansenEconometrics.leaveOneOutGram X i)],
  Eq (HansenEconometrics.leaveOneOutBetaDeleted X y i) (HansenEconometrics.leaveOneOutBeta X y i)

Direct statement dependencies (3)

• HansenEconometrics.leaveOneOutBeta
• HansenEconometrics.leaveOneOutBetaDeleted
• HansenEconometrics.leaveOneOutGram

HansenEconometrics/Chapter3Projections.lean:281

def HansenEconometrics.leaveOneOutGram

Hansen equation (3.42): the leave-one-out Gram matrix X’X - Xᵢ Xᵢ’.

Formal statement

{n : Type u_1} → {k : Type u_2} → [Fintype n] → Matrix n k Real → n → Matrix k k Real

HansenEconometrics/Chapter3Projections.lean:216

def HansenEconometrics.leaveOneOutBeta

Hansen equation (3.42): leave-one-out coefficient written with the reduced Gram matrix.

Formal statement

{n : Type u_1} →
  {k : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : Fintype k] →
        [inst_2 : DecidableEq k] →
          (X : Matrix n k Real) →
            (n → Real) → (i : n) → [Invertible (HansenEconometrics.leaveOneOutGram X i)] → k → Real

Direct statement dependencies (1)

• HansenEconometrics.leaveOneOutGram

HansenEconometrics/Chapter3Projections.lean:265

Section 3.21 influential observations4 endpoints

\hat{\beta}-\hat{\beta}_{(-i)}=(X'X)^{-1}X_i\tilde e_i, \hat Y_i-\tilde Y_i=h_{ii}\tilde e_i, and \max_i|\hat Y_i-\tilde Y_i|=\max_i|h_{ii}\tilde e_i|

theorem HansenEconometrics.olsBeta_sub_leaveOneOutBeta_eq_invGram_mulVec

Hansen equation (3.48): the change in coefficient estimates after dropping observation i.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) (i : n) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_4 : Invertible (HansenEconometrics.leaveOneOutGram X i)],
  Eq (instHSub.hSub (HansenEconometrics.olsBeta X y) (HansenEconometrics.leaveOneOutBeta X y i))
    (instHSMul.hSMul (HansenEconometrics.leaveOneOutResidual X y i)
      ((inst_3.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)).mulVec (X i)))

Direct statement dependencies (4)

• HansenEconometrics.leaveOneOutBeta
• HansenEconometrics.leaveOneOutGram
• HansenEconometrics.leaveOneOutResidual
• HansenEconometrics.olsBeta

HansenEconometrics/Chapter3Projections.lean:375

theorem HansenEconometrics.fitted_sub_leaveOneOutPrediction_eq_leverage_mul_residual

Hansen Section 3.21: the full-sample fitted value minus the leave-one-out predicted value is hᵢᵢ ẽᵢ.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) (i : n) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_4 : Invertible (HansenEconometrics.leaveOneOutGram X i)],
  Eq (instHSub.hSub (HansenEconometrics.fitted X y i) (HansenEconometrics.leaveOneOutPrediction X y i))
    (instHMul.hMul (HansenEconometrics.leverageValue X i) (HansenEconometrics.leaveOneOutResidual X y i))

Direct statement dependencies (5)

• HansenEconometrics.fitted
• HansenEconometrics.leaveOneOutGram
• HansenEconometrics.leaveOneOutPrediction
• HansenEconometrics.leaveOneOutResidual
• HansenEconometrics.leverageValue

HansenEconometrics/Chapter3Projections.lean:388

theorem HansenEconometrics.predictionInfluence_eq_abs_leverage_mul_leaveOneOutResidual

Hansen Section 3.21: the prediction-change diagnostic is |hᵢᵢ ẽᵢ|.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) (i : n) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_4 : Invertible (HansenEconometrics.leaveOneOutGram X i)],
  Eq (HansenEconometrics.predictionInfluence X y i)
    (abs (instHMul.hMul (HansenEconometrics.leverageValue X i) (HansenEconometrics.leaveOneOutResidual X y i)))

Direct statement dependencies (4)

• HansenEconometrics.leaveOneOutGram
• HansenEconometrics.leaveOneOutResidual
• HansenEconometrics.leverageValue
• HansenEconometrics.predictionInfluence

HansenEconometrics/Chapter3Projections.lean:417

theorem HansenEconometrics.maxPredictionInfluence_eq_maxLeveragePredictionErrorInfluence

Hansen Section 3.21: the maximum prediction-change diagnostic equals max_i |hᵢᵢ ẽᵢ|.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  (hloo : (i : n) → Invertible (HansenEconometrics.leaveOneOutGram X i)) [inst_4 : Nonempty n],
  Eq (HansenEconometrics.maxPredictionInfluence X y hloo)
    (HansenEconometrics.maxLeveragePredictionErrorInfluence X y hloo)

Direct statement dependencies (3)

• HansenEconometrics.leaveOneOutGram
• HansenEconometrics.maxLeveragePredictionErrorInfluence
• HansenEconometrics.maxPredictionInfluence

HansenEconometrics/Chapter3Projections.lean:444

Theorem 3.3.4 hat-matrix eigenvalues2 endpoints

\lambda_i(P) \in \{0,1\}, with k eigenvalues equal to 1

theorem HansenEconometrics.hatMatrix_eigenvalues_zero_or_one

Hansen Theorem 3.3.4: every eigenvalue of the hat matrix is 0 or 1.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : DecidableEq n] [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  (i : n), Or (Eq (⋯.eigenvalues i) 0) (Eq (⋯.eigenvalues i) 1)

Direct statement dependencies (2)

• HansenEconometrics.hatMatrix
• HansenEconometrics.hatMatrix_isHermitian

HansenEconometrics/Chapter3Projections.lean:512

theorem HansenEconometrics.hatMatrix_card_eigenvalues_eq_one

Hansen Theorem 3.3.4: exactly k hat-matrix eigenvalues are equal to 1.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : DecidableEq n] [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (Fintype.card (Subtype fun i => Eq (⋯.eigenvalues i) 1)) (Fintype.card k)

Direct statement dependencies (2)

• HansenEconometrics.hatMatrix
• HansenEconometrics.hatMatrix_isHermitian

HansenEconometrics/Chapter3Projections.lean:521

Theorem 3.3.5 rank of the hat matrix1 endpoint

\operatorname{rank}(P) = k

theorem HansenEconometrics.rank_hatMatrix

The rank of the hat matrix equals the number of regressors.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.hatMatrix X).rank (Fintype.card k)

Direct statement dependencies (1)

• HansenEconometrics.hatMatrix

HansenEconometrics/Chapter3Projections.lean:503

Equation (3.21) annihilator kills the regressors1 endpoint

M X = 0

theorem HansenEconometrics.annihilator_mul_X

Hansen equation (3.21): the annihilator matrix kills the regressor matrix, M X = 0.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : DecidableEq n] [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.annihilatorMatrix X) X) 0

Direct statement dependencies (1)

• HansenEconometrics.annihilatorMatrix

HansenEconometrics/Chapter3Projections.lean:75

Equation (3.22) trace of the annihilator1 endpoint

\operatorname{tr}(M) = n - k

theorem HansenEconometrics.annihilatorMatrix_trace

Hansen equation (3.22): the trace of the annihilator matrix is n - k.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : DecidableEq n] [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.annihilatorMatrix X).trace (instHSub.hSub (Fintype.card n).cast (Fintype.card k).cast)

Direct statement dependencies (1)

• HansenEconometrics.annihilatorMatrix

HansenEconometrics/Chapter3Projections.lean:468

Section 3.12 annihilator eigenvalues and rank2 endpoints

\lambda_i(M) \in \{0,1\}, \operatorname{rank}(M)=n-k

theorem HansenEconometrics.annihilatorMatrix_eigenvalues_zero_or_one

Hansen Section 3.12: every eigenvalue of the annihilator matrix is 0 or 1.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : DecidableEq n] [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  (i : n), Or (Eq (⋯.eigenvalues i) 0) (Eq (⋯.eigenvalues i) 1)

Direct statement dependencies (2)

• HansenEconometrics.annihilatorMatrix
• HansenEconometrics.annihilatorMatrix_isHermitian

HansenEconometrics/Chapter3Projections.lean:531

theorem HansenEconometrics.rank_annihilatorMatrix

Hansen Section 3.12: the rank of the annihilator matrix is n - k.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  [inst_3 : DecidableEq n] [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.annihilatorMatrix X).rank (instHSub.hSub (Fintype.card n) (Fintype.card k))

Direct statement dependencies (1)

• HansenEconometrics.annihilatorMatrix

HansenEconometrics/Chapter3Projections.lean:497

Equation (3.23) residual representation1 endpoint

\hat{e} = M Y

theorem HansenEconometrics.residual_eq_annihilator_mul_y

Hansen equation (3.23): residuals are the annihilator matrix applied to the data vector.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.residual X y) ((HansenEconometrics.annihilatorMatrix X).mulVec y)

Direct statement dependencies (2)

• HansenEconometrics.annihilatorMatrix
• HansenEconometrics.residual

HansenEconometrics/Chapter3Projections.lean:577

Section 3.14 fitted values and residuals are orthogonal1 endpoint

\hat{Y}' \hat{e} = 0

theorem HansenEconometrics.fitted_dot_residual

Hansen Section 3.14: fitted values and residuals are orthogonal.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (dotProduct (HansenEconometrics.fitted X y) (HansenEconometrics.residual X y)) 0

Direct statement dependencies (2)

• HansenEconometrics.fitted
• HansenEconometrics.residual

HansenEconometrics/Chapter3Projections.lean:584

Section 3.14 Pythagorean decomposition1 endpoint

Y'Y = \hat{Y}'\hat{Y} + \hat{e}'\hat{e}

theorem HansenEconometrics.fitted_residual_pythagorean

Hansen Section 3.14: finite-sample Pythagorean decomposition for fitted values and residuals.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (dotProduct y y)
    (instHAdd.hAdd (dotProduct (HansenEconometrics.fitted X y) (HansenEconometrics.fitted X y))
      (dotProduct (HansenEconometrics.residual X y) (HansenEconometrics.residual X y)))

Direct statement dependencies (2)

• HansenEconometrics.fitted
• HansenEconometrics.residual

HansenEconometrics/Chapter3Projections.lean:594

Section 3.14 centered fitted/residual orthogonality1 endpoint

(\hat{Y}-\bar{Y}\iota)'\hat{e}=0 when X contains an intercept

theorem HansenEconometrics.centered_fitted_dot_residual

Hansen Section 3.14: with an intercept, centered fitted values are orthogonal to residuals.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] {c : k → Real},
  Eq (X.mulVec c) 1 →
    Eq
      (dotProduct (HansenEconometrics.centeredAtSampleMean y (HansenEconometrics.fitted X y))
        (HansenEconometrics.residual X y))
      0

Direct statement dependencies (3)

• HansenEconometrics.centeredAtSampleMean
• HansenEconometrics.fitted
• HansenEconometrics.residual

HansenEconometrics/Chapter3Projections.lean:642

Section 3.14 analysis-of-variance formula1 endpoint

\sum_i(Y_i-\bar{Y})^2=\sum_i(\hat{Y}_i-\bar{Y})^2+\sum_i\hat{e}_i^2

theorem HansenEconometrics.centered_anova_decomposition

Hansen Section 3.14: centered analysis-of-variance decomposition for OLS with an intercept.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] {c : k → Real},
  Eq (X.mulVec c) 1 →
    Eq (HansenEconometrics.totalSumSquares y)
      (instHAdd.hAdd (HansenEconometrics.explainedSumSquares X y) (HansenEconometrics.residualSumSquares X y))

Direct statement dependencies (3)

• HansenEconometrics.explainedSumSquares
• HansenEconometrics.residualSumSquares
• HansenEconometrics.totalSumSquares

HansenEconometrics/Chapter3Projections.lean:668

Section 3.14 coefficient of determination2 endpoints

R^2=\mathrm{ESS}/\mathrm{TSS}=1-\mathrm{RSS}/\mathrm{TSS}

def HansenEconometrics.rSquared

Hansen Section 3.14: coefficient of determination.

Formal statement

{n : Type u_1} →
  {k : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : Fintype k] →
        [inst_2 : DecidableEq k] →
          (X : Matrix n k Real) →
            (n → Real) → [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] → Real

HansenEconometrics/Chapter3Projections.lean:629

theorem HansenEconometrics.rSquared_eq_one_sub_residualSumSquares_div_totalSumSquares

Hansen Section 3.14: R² can be written as one minus the residual share of TSS.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X : Matrix n k Real)
  (y : n → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] {c : k → Real},
  Eq (X.mulVec c) 1 →
    Ne (HansenEconometrics.totalSumSquares y) 0 →
      Eq (HansenEconometrics.rSquared X y)
        (instHSub.hSub 1
          (instHDiv.hDiv (HansenEconometrics.residualSumSquares X y) (HansenEconometrics.totalSumSquares y)))

Direct statement dependencies (3)

• HansenEconometrics.rSquared
• HansenEconometrics.residualSumSquares
• HansenEconometrics.totalSumSquares

HansenEconometrics/Chapter3Projections.lean:679

Theorem 3.4 partitioned coefficient formulae3 endpoints

\hat{\beta}_1=(X_1' M_2 X_1)^{-1} X_1' M_2Y, \hat{\beta}_2=(X_2' M_1 X_2)^{-1} X_2' M_1Y

def HansenEconometrics.partitionedLeftBetaFormula

Hansen equation (3.37): the left-block partitioned-regression formula.

Formal statement

{n : Type u_1} →
  {k₁ : Type u_3} →
    {k₂ : Type u_4} →
      [inst : Fintype n] →
        Matrix n k₁ Real →
          (X₂ : Matrix n k₂ Real) →
            (n → Real) →
              [DecidableEq n] →
                [Fintype k₁] →
                  [DecidableEq k₁] →
                    [inst_4 : Fintype k₂] →
                      [inst_5 : DecidableEq k₂] →
                        [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X₂.transpose X₂)] → k₁ → Real

HansenEconometrics/Chapter3FWL.lean:83

def HansenEconometrics.partitionedRightBetaFormula

Hansen equation (3.38): the right-block partitioned-regression formula.

Formal statement

{n : Type u_1} →
  {k₁ : Type u_3} →
    {k₂ : Type u_4} →
      [inst : Fintype n] →
        (X₁ : Matrix n k₁ Real) →
          Matrix n k₂ Real →
            (n → Real) →
              [DecidableEq n] →
                [inst_2 : Fintype k₁] →
                  [inst_3 : DecidableEq k₁] →
                    [Fintype k₂] →
                      [DecidableEq k₂] →
                        [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X₁.transpose X₁)] → k₂ → Real

HansenEconometrics/Chapter3FWL.lean:75

theorem HansenEconometrics.fromColsBeta_eq_partitionedBetaFormulas

Hansen Theorem 3.4: both partitioned-regression coefficients in formula form.

Formal statement

∀ {n : Type u_1} {k₁ : Type u_3} {k₂ : Type u_4} [inst : Fintype n] (X₁ : Matrix n k₁ Real) (X₂ : Matrix n k₂ Real)
  (y : n → Real) [inst_1 : DecidableEq n] [inst_2 : Fintype k₁] [inst_3 : DecidableEq k₁] [inst_4 : Fintype k₂]
  [inst_5 : DecidableEq k₂] [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X₁.transpose X₁)]
  [inst_7 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X₂.transpose X₂)]
  [inst_8 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (X₁.fromCols X₂).transpose (X₁.fromCols X₂))]
  [Invertible
      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.residualizedRegressors X₁ X₂).transpose
        (HansenEconometrics.residualizedRegressors X₁ X₂))]
  [Invertible
      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.residualizedRegressors X₂ X₁).transpose
        (HansenEconometrics.residualizedRegressors X₂ X₁))],
  And (Eq (HansenEconometrics.fromColsLeftBeta X₁ X₂ y) (HansenEconometrics.partitionedLeftBetaFormula X₁ X₂ y))
    (Eq (HansenEconometrics.fromColsRightBeta X₁ X₂ y) (HansenEconometrics.partitionedRightBetaFormula X₁ X₂ y))

Direct statement dependencies (5)

• HansenEconometrics.fromColsLeftBeta
• HansenEconometrics.fromColsRightBeta
• HansenEconometrics.partitionedLeftBetaFormula
• HansenEconometrics.partitionedRightBetaFormula
• HansenEconometrics.residualizedRegressors

HansenEconometrics/Chapter3FWL.lean:328

Theorem 3.5 coefficient equivalence1 endpoint

\hat{\beta}_2 = (X_2' M_1 X_2)^{-1} X_2' M_1 Y

theorem HansenEconometrics.fromColsRightBeta_eq_fwlBeta

Hansen Theorem 3.5, coefficient part: the second full-regression block equals FWL.

Formal statement

∀ {n : Type u_1} {k₁ : Type u_3} {k₂ : Type u_4} [inst : Fintype n] (X₁ : Matrix n k₁ Real) (X₂ : Matrix n k₂ Real)
  (y : n → Real) [inst_1 : DecidableEq n] [inst_2 : Fintype k₁] [inst_3 : DecidableEq k₁] [inst_4 : Fintype k₂]
  [inst_5 : DecidableEq k₂] [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X₁.transpose X₁)]
  [inst_7 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (X₁.fromCols X₂).transpose (X₁.fromCols X₂))]
  [inst_8 :
    Invertible
      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.residualizedRegressors X₁ X₂).transpose
        (HansenEconometrics.residualizedRegressors X₁ X₂))],
  Eq (HansenEconometrics.fromColsRightBeta X₁ X₂ y) (HansenEconometrics.fwlBeta X₁ X₂ y)

Direct statement dependencies (3)

• HansenEconometrics.fromColsRightBeta
• HansenEconometrics.fwlBeta
• HansenEconometrics.residualizedRegressors

HansenEconometrics/Chapter3FWL.lean:209

Theorem 3.5 residual equivalence1 endpoint

\hat{e}_{\text{full}} = M_{M_1 X_2} M_1 Y

theorem HansenEconometrics.fwl_residual_eq_full_residual

Hansen Theorem 3.5, residual part: FWL and full OLS produce the same residual.

Formal statement

∀ {n : Type u_1} {k₁ : Type u_3} {k₂ : Type u_4} [inst : Fintype n] (X₁ : Matrix n k₁ Real) (X₂ : Matrix n k₂ Real)
  (y : n → Real) [inst_1 : DecidableEq n] [inst_2 : Fintype k₁] [inst_3 : DecidableEq k₁] [inst_4 : Fintype k₂]
  [inst_5 : DecidableEq k₂] [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X₁.transpose X₁)]
  [inst_7 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (X₁.fromCols X₂).transpose (X₁.fromCols X₂))]
  [inst_8 :
    Invertible
      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.residualizedRegressors X₁ X₂).transpose
        (HansenEconometrics.residualizedRegressors X₁ X₂))],
  Eq
    (HansenEconometrics.residual (HansenEconometrics.residualizedRegressors X₁ X₂)
      ((HansenEconometrics.annihilatorMatrix X₁).mulVec y))
    (HansenEconometrics.residual (X₁.fromCols X₂) y)

Direct statement dependencies (3)

• HansenEconometrics.annihilatorMatrix
• HansenEconometrics.residual
• HansenEconometrics.residualizedRegressors

HansenEconometrics/Chapter3FWL.lean:341