Chapter 4: Least Squares Regression

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

This page is generated from the canonical Chapter 4 inventory and the compiled Lean environment. It contains 21 textbook result groups and 38 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.

Equation (4.6) OLS decomposition1 endpoint

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

theorem HansenEconometrics.olsBeta_linear_decomposition

Hansen equation (4.6): OLS equals the true coefficient plus the projected 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)
  (β : k → Real) (e : n → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.olsBeta X (instHAdd.hAdd (X.mulVec β) e))
    (instHAdd.hAdd β
      ((inst_3.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)).mulVec (X.transpose.mulVec e)))

Direct statement dependencies (1)

• HansenEconometrics.olsBeta

HansenEconometrics/Chapter4LeastSquaresRegression.lean:17

Orthogonal-error specialization1 endpoint

X' e = 0 \Longrightarrow \hat{\beta} = \beta

theorem HansenEconometrics.olsBeta_eq_of_regressors_orthogonal_error

If the model error is orthogonal to the regressors, the closed-form OLS coefficient is β.

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)
  (β : k → Real) (e : n → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (X.transpose.mulVec e) 0 → Eq (HansenEconometrics.olsBeta X (instHAdd.hAdd (X.mulVec β) e)) β

Direct statement dependencies (1)

• HansenEconometrics.olsBeta

HansenEconometrics/Chapter4LeastSquaresRegression.lean:30

Fitted values in the linear model1 endpoint

\hat{Y} = X \beta + P e

theorem HansenEconometrics.fitted_linear_model

In the finite-sample linear model, fitted values equal signal plus projected 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)
  (β : k → Real) (e : n → Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.fitted X (instHAdd.hAdd (X.mulVec β) e))
    (instHAdd.hAdd (X.mulVec β) ((HansenEconometrics.hatMatrix X).mulVec e))

Direct statement dependencies (2)

• HansenEconometrics.fitted
• HansenEconometrics.hatMatrix

HansenEconometrics/Chapter4LeastSquaresRegression.lean:38

Residuals in the linear model1 endpoint

\hat{e} = M e

theorem HansenEconometrics.residual_linear_model

In the finite-sample linear model, OLS residuals are the annihilator applied to the 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)
  (β : k → Real) (e : n → Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.residual X (instHAdd.hAdd (X.mulVec β) e)) ((HansenEconometrics.annihilatorMatrix X).mulVec e)

Direct statement dependencies (2)

• HansenEconometrics.annihilatorMatrix
• HansenEconometrics.residual

HansenEconometrics/Chapter4LeastSquaresRegression.lean:47

Theorem 4.1 conditional unbiasedness1 endpoint

\mathbb{E}[\hat{\beta} \mid X] = \beta

theorem HansenEconometrics.ols_condExp_eq_beta

Vector-valued conditional unbiasedness of OLS.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {Ω : Type u_3}
  {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real)
  [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [MeasureTheory.IsProbabilityMeasure μ] (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  (∀ (i : n), MeasureTheory.Integrable (fun ω => e ω i) μ) →
    (∀ (i : n), (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => e ω i) 0) →
      (MeasureTheory.ae μ).EventuallyEq
        (MeasureTheory.condExp m μ fun ω => HansenEconometrics.olsBeta X (instHAdd.hAdd (X.mulVec β) (e ω))) fun x => β

Direct statement dependencies (1)

• HansenEconometrics.olsBeta

HansenEconometrics/Chapter4LeastSquaresRegression.lean:2902

Theorem 4.1 unconditional unbiasedness1 endpoint

\mathbb{E}[\hat{\beta}] = \beta

theorem HansenEconometrics.ols_integral_eq_beta

Vector-valued unconditional unbiasedness of OLS.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {Ω : Type u_3}
  {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real)
  [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [MeasureTheory.IsProbabilityMeasure μ] (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  (∀ (i : n), MeasureTheory.Integrable (fun ω => e ω i) μ) →
    (∀ (i : n), (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => e ω i) 0) →
      Eq (MeasureTheory.integral μ fun ω => HansenEconometrics.olsBeta X (instHAdd.hAdd (X.mulVec β) (e ω))) β

Direct statement dependencies (1)

• HansenEconometrics.olsBeta

HansenEconometrics/Chapter4LeastSquaresRegression.lean:2947

Theorem 4.2 conditional covariance formula2 endpoints

\operatorname{Var}(\hat{\beta} \mid X) = (X'X)^{-1} X' D X (X'X)^{-1}

def HansenEconometrics.olsConditionalVarianceMatrix

Hansen Theorem 4.2 matrix core: conditional covariance formula for OLS.

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) →
            Matrix n n Real →
              [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] → Matrix k k Real

HansenEconometrics/Chapter4LeastSquaresRegression.lean:57

theorem HansenEconometrics.ols_condExp_centered_mul_eq_variance_matrix

Matrix-valued conditional covariance bridge for OLS.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {Ω : Type u_3}
  {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real)
  (D : Matrix n n Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [MeasureTheory.IsProbabilityMeasure μ] (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  (∀ (i r : n), MeasureTheory.Integrable (fun ω => instHMul.hMul (e ω i) (e ω r)) μ) →
    (∀ (i r : n),
        (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => instHMul.hMul (e ω i) (e ω r)) fun x =>
          D i r) →
      (MeasureTheory.ae μ).EventuallyEq
        (MeasureTheory.condExp m μ fun ω j l =>
          instHMul.hMul (instHSub.hSub (HansenEconometrics.olsBeta X (instHAdd.hAdd (X.mulVec β) (e ω)) j) (β j))
            (instHSub.hSub (HansenEconometrics.olsBeta X (instHAdd.hAdd (X.mulVec β) (e ω)) l) (β l)))
        fun x => HansenEconometrics.olsConditionalVarianceMatrix X D

Direct statement dependencies (2)

• HansenEconometrics.olsBeta
• HansenEconometrics.olsConditionalVarianceMatrix

HansenEconometrics/Chapter4LeastSquaresRegression.lean:3206

Theorem 4.2 unconditional covariance identity1 endpoint

\mathbb{E}[(\hat{\beta} - \beta)(\hat{\beta} - \beta)'] = \mathbb{E}[\operatorname{Var}(\hat{\beta} \mid X)]

theorem HansenEconometrics.ols_integral_centered_mul_eq_variance_matrix

Matrix-valued unconditional covariance bridge for OLS.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {Ω : Type u_3}
  {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real)
  (D : Matrix n n Real) [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [MeasureTheory.IsProbabilityMeasure μ] (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  (∀ (i r : n), MeasureTheory.Integrable (fun ω => instHMul.hMul (e ω i) (e ω r)) μ) →
    (∀ (i r : n),
        (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => instHMul.hMul (e ω i) (e ω r)) fun x =>
          D i r) →
      Eq
        (MeasureTheory.integral μ fun ω j l =>
          instHMul.hMul (instHSub.hSub (HansenEconometrics.olsBeta X (instHAdd.hAdd (X.mulVec β) (e ω)) j) (β j))
            (instHSub.hSub (HansenEconometrics.olsBeta X (instHAdd.hAdd (X.mulVec β) (e ω)) l) (β l)))
        (HansenEconometrics.olsConditionalVarianceMatrix X D)

Direct statement dependencies (2)

• HansenEconometrics.olsBeta
• HansenEconometrics.olsConditionalVarianceMatrix

HansenEconometrics/Chapter4LeastSquaresRegression.lean:3379

Theorem 4.2 homoskedastic simplification1 endpoint

\operatorname{Var}(\hat{\beta} \mid X) = \sigma^2 (X'X)^{-1}

theorem HansenEconometrics.olsConditionalVarianceMatrix_homoskedastic

Hansen Theorem 4.2 homoskedastic simplification: D = σ² 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)
  (σ2 : Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.olsConditionalVarianceMatrix X (instHSMul.hSMul σ2 1))
    (instHSMul.hSMul σ2 (inst_4.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)))

Direct statement dependencies (1)

• HansenEconometrics.olsConditionalVarianceMatrix

HansenEconometrics/Chapter4LeastSquaresRegression.lean:102

Gauss-Markov lower bound1 endpoint

\operatorname{Var}(\tilde{\beta} \mid X) - \operatorname{Var}(\hat{\beta} \mid X) \succeq 0

theorem HansenEconometrics.gaussMarkov_variance_gap_posSemidef

Deterministic core of the Gauss-Markov theorem: the variance-gap matrix is positive semidefinite.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X A : Matrix n k Real)
  [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul A.transpose X) 1 →
    (instHSub.hSub (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul A.transpose A)
        (inst_3.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X))).PosSemidef

HansenEconometrics/Chapter4LeastSquaresRegression.lean:1443

GLS coefficient1 endpoint

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

def HansenEconometrics.glsBeta

Generalized least squares estimator with weight 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) →
            (Ω : Matrix n n Real) →
              (n → Real) →
                [inst_3 : DecidableEq n] →
                  [inst_4 : Invertible Ω] →
                    [Invertible
                          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose (inst_4.invOf Ω)) X)] →
                      k → Real

HansenEconometrics/Chapter4LeastSquaresRegression.lean:3444

GLS decomposition1 endpoint

\hat{\beta}_{GLS} = \beta + (X' \Omega^{-1} X)^{-1} X' \Omega^{-1} e

theorem HansenEconometrics.glsBeta_linear_decomposition

GLS equals the true coefficient plus the weighted projected 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)
  (Ω : Matrix n n Real) (β : k → Real) (e : n → Real) [inst_3 : DecidableEq n] [inst_4 : Invertible Ω]
  [inst_5 :
    Invertible
      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose (inst_4.invOf Ω)) X)],
  Eq (HansenEconometrics.glsBeta X Ω (instHAdd.hAdd (X.mulVec β) e))
    (instHAdd.hAdd β
      ((inst_5.invOf
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose (inst_4.invOf Ω)) X)).mulVec
        (X.transpose.mulVec ((inst_4.invOf Ω).mulVec e))))

Direct statement dependencies (1)

• HansenEconometrics.glsBeta

HansenEconometrics/Chapter4LeastSquaresRegression.lean:3450

Generalized Gauss-Markov lower bound1 endpoint

weighted variance gap is positive semidefinite

theorem HansenEconometrics.generalizedGaussMarkov_variance_gap_posSemidef

Deterministic core of the generalized Gauss-Markov theorem: the weighted variance gap is positive semidefinite.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X A : Matrix n k Real)
  (Ω : Matrix n n Real) [inst_3 : DecidableEq n] [inst_4 : Invertible Ω]
  [inst_5 :
    Invertible
      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose (inst_4.invOf Ω)) X)],
  Ω.PosSemidef →
    Eq (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul A.transpose X) 1 →
      (instHSub.hSub
          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul A.transpose Ω) A)
          (inst_5.invOf
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose (inst_4.invOf Ω)) X))).PosSemidef

HansenEconometrics/Chapter4LeastSquaresRegression.lean:3475

White HC0 covariance estimator1 endpoint

\hat{V}_{HC0} = (X'X)^{-1} X' \operatorname{diag}(\hat{e}_i^2) X (X'X)^{-1}

def HansenEconometrics.olsHuberWhiteVarianceEstimator

White’s HC0 heteroskedasticity-robust covariance estimator.

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) →
              [DecidableEq n] →
                [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] → Matrix k k Real

HansenEconometrics/Chapter4LeastSquaresRegression.lean:68

HC1 covariance estimator1 endpoint

\hat{V}_{HC1} = \frac{n}{n-k} \hat{V}_{HC0}

def HansenEconometrics.olsHuberWhiteHC1VarianceEstimator

HC1 degrees-of-freedom adjustment to the Huber-White covariance estimator.

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) →
              [DecidableEq n] →
                [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] → Matrix k k Real

HansenEconometrics/Chapter4LeastSquaresRegression.lean:73

Method-of-moments residual variance σ̂²3 endpoints

\hat{\sigma}^2 = n^{-1}\sum_i \hat e_i^2 and, under diagonal heteroskedastic conditional second moments, \mathbb{E}[\hat{\sigma}^2 \mid X] = n^{-1}\operatorname{tr}(MD)

def HansenEconometrics.olsSigmaSqHat

Hansen’s method-of-moments residual variance estimator σ̂² = 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) →
            (n → Real) →
              [DecidableEq n] → [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] → Real

HansenEconometrics/Chapter4LeastSquaresRegression.lean:1356

theorem HansenEconometrics.olsSigmaSqHat_linear_model_quadratic_form

Under the linear model, Hansen’s σ̂² = n⁻¹∑ᵢ êᵢ² is the annihilator quadratic form scaled by 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)
  (β : k → Real) (e : n → Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.olsSigmaSqHat X (instHAdd.hAdd (X.mulVec β) e))
    (instHMul.hMul (Real.instInv.inv (Fintype.card n).cast)
      (dotProduct e ((HansenEconometrics.annihilatorMatrix X).mulVec e)))

Direct statement dependencies (2)

• HansenEconometrics.annihilatorMatrix
• HansenEconometrics.olsSigmaSqHat

HansenEconometrics/Chapter4LeastSquaresRegression.lean:1420

theorem HansenEconometrics.ols_condExp_sigmaSqHat_eq_inv_card_trace_diagonal

Hansen equation (4.25): under diagonal heteroskedastic conditional second moments, E[σ̂² | X] = n⁻¹ tr(MD) where M is the annihilator matrix and D is the diagonal matrix of conditional error variances.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {Ω : Type u_3}
  {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real)
  (σ2 : n → Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [MeasureTheory.IsProbabilityMeasure μ] (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  (∀ (i j : n), MeasureTheory.Integrable (fun ω => instHMul.hMul (e ω i) (e ω j)) μ) →
    (∀ (i j : n),
        (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => instHMul.hMul (e ω i) (e ω j)) fun x =>
          Matrix.diagonal σ2 i j) →
      (MeasureTheory.ae μ).EventuallyEq
        (MeasureTheory.condExp m μ fun ω => HansenEconometrics.olsSigmaSqHat X (instHAdd.hAdd (X.mulVec β) (e ω)))
        fun x =>
        instHMul.hMul (Real.instInv.inv (Fintype.card n).cast)
          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.annihilatorMatrix X)
              (Matrix.diagonal σ2)).trace

Direct statement dependencies (2)

• HansenEconometrics.annihilatorMatrix
• HansenEconometrics.olsSigmaSqHat

HansenEconometrics/Chapter4LeastSquaresRegression.lean:2703

Residual variance estimator s²3 endpoints

s^2 = (n-k)^{-1}\sum_i \hat e_i^2

def HansenEconometrics.olsResidualVarianceEstimator

Finite-sample residual variance estimator in the homoskedastic linear regression model.

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) →
              [DecidableEq n] → [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] → Real

HansenEconometrics/Chapter4LeastSquaresRegression.lean:1362

def HansenEconometrics.olsResidualSumSquares

The OLS residual sum of squares RSS = ê’ê. This is the likelihood-scale quadratic form that appears in Hansen’s Chapter 5 likelihood-ratio / F-test derivation.

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) →
              [DecidableEq n] → [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] → Real

HansenEconometrics/Chapter4LeastSquaresRegression.lean:1369

theorem HansenEconometrics.olsResidualVarianceEstimator_linear_model_quadratic_form

Under the linear model, the residual variance estimator is the annihilator quadratic form divided by n-k. This is the deterministic identity underlying the chi-square step.

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)
  (β : k → Real) (e : n → Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.olsResidualVarianceEstimator X (instHAdd.hAdd (X.mulVec β) e))
    (instHDiv.hDiv (dotProduct e ((HansenEconometrics.annihilatorMatrix X).mulVec e))
      (instHSub.hSub (Fintype.card n).cast (Fintype.card k).cast))

Direct statement dependencies (2)

• HansenEconometrics.annihilatorMatrix
• HansenEconometrics.olsResidualVarianceEstimator

HansenEconometrics/Chapter4LeastSquaresRegression.lean:1432

s² conditional and unconditional unbiasedness2 endpoints

\mathbb{E}[s^2 \mid X] = \sigma^2 and \mathbb{E}[s^2] = \sigma^2 under homoskedastic conditional second moments

theorem HansenEconometrics.ols_condExp_residualVarianceEstimator_eq_sigmaSq

Hansen equation (4.26): under a homoskedastic conditional second-moment assumption, E[s² | X] = σ². The hypothesis hee_homo is a second-moment condition on E[eᵢeⱼ | m]; with conditional mean zero it specializes to the usual conditional variance/covariance statement.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {Ω : Type u_3}
  {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real)
  (σ2 : Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [MeasureTheory.IsProbabilityMeasure μ] (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  (∀ (i j : n), MeasureTheory.Integrable (fun ω => instHMul.hMul (e ω i) (e ω j)) μ) →
    (∀ (i j : n),
        (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => instHMul.hMul (e ω i) (e ω j)) fun x =>
          instHMul.hMul σ2 (1 i j)) →
      Ne (instHSub.hSub (Fintype.card n).cast (Fintype.card k).cast) 0 →
        (MeasureTheory.ae μ).EventuallyEq
          (MeasureTheory.condExp m μ fun ω =>
            HansenEconometrics.olsResidualVarianceEstimator X (instHAdd.hAdd (X.mulVec β) (e ω)))
          fun x => σ2

Direct statement dependencies (1)

• HansenEconometrics.olsResidualVarianceEstimator

HansenEconometrics/Chapter4LeastSquaresRegression.lean:2737

theorem HansenEconometrics.ols_integral_residualVarianceEstimator_eq_sigmaSq

Unconditional unbiasedness of s² obtained by integrating the conditional statement.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {Ω : Type u_3}
  {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real)
  (σ2 : Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [MeasureTheory.IsProbabilityMeasure μ] (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  (∀ (i j : n), MeasureTheory.Integrable (fun ω => instHMul.hMul (e ω i) (e ω j)) μ) →
    (∀ (i j : n),
        (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => instHMul.hMul (e ω i) (e ω j)) fun x =>
          instHMul.hMul σ2 (1 i j)) →
      Ne (instHSub.hSub (Fintype.card n).cast (Fintype.card k).cast) 0 →
        MeasureTheory.Integrable
            (fun ω => HansenEconometrics.olsResidualVarianceEstimator X (instHAdd.hAdd (X.mulVec β) (e ω))) μ →
          Eq
            (MeasureTheory.integral μ fun ω =>
              HansenEconometrics.olsResidualVarianceEstimator X (instHAdd.hAdd (X.mulVec β) (e ω)))
            σ2

Direct statement dependencies (1)

• HansenEconometrics.olsResidualVarianceEstimator

HansenEconometrics/Chapter4LeastSquaresRegression.lean:2787

HC2 covariance estimator4 endpoints

\hat V_{HC2} = (X'X)^{-1} X'\operatorname{diag}((1-h_{ii})^{-1}\hat e_i^2)X(X'X)^{-1}

def HansenEconometrics.olsHuberWhiteHC2VarianceEstimator

HC2 covariance estimator: leverage-adjusted by (1 - hᵢᵢ)⁻¹. Lean totalizes (1 - hᵢᵢ)⁻¹ to 0 at saturated observations (hᵢᵢ = 1); textbook agreement requires hᵢᵢ < 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) →
            (n → Real) →
              [DecidableEq n] →
                [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] → Matrix k k Real

HansenEconometrics/Chapter4LeastSquaresRegression.lean:130

theorem HansenEconometrics.olsHuberWhiteHC2VarianceEstimator_linear_model

In the linear model, HC2 uses annihilator-transformed errors.

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)
  (β : k → Real) (e : n → Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.olsHuberWhiteHC2VarianceEstimator X (instHAdd.hAdd (X.mulVec β) e))
    (HansenEconometrics.olsConditionalVarianceMatrix X
      (Matrix.diagonal fun i =>
        instHMul.hMul (Real.instInv.inv (instHSub.hSub 1 (HansenEconometrics.hatMatrix X i i)))
          (instHPow.hPow ((HansenEconometrics.annihilatorMatrix X).mulVec e i) 2)))

Direct statement dependencies (4)

• HansenEconometrics.annihilatorMatrix
• HansenEconometrics.hatMatrix
• HansenEconometrics.olsConditionalVarianceMatrix
• HansenEconometrics.olsHuberWhiteHC2VarianceEstimator

HansenEconometrics/Chapter4LeastSquaresRegression.lean:1242

theorem HansenEconometrics.condExp_olsHuberWhiteHC2VarianceEstimator_eq_homoskedastic

Matrix-valued conditional expectation of HC2 under homoskedastic second moments.

The rowwise leverage adjustment exactly removes the homoskedastic residual shrinkage, so the conditional expectation is the usual homoskedastic covariance matrix.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {Ω : Type u_3}
  {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real)
  (σ2 : Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [MeasureTheory.IsProbabilityMeasure μ] (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  (∀ (r s : n), MeasureTheory.Integrable (fun ω => instHMul.hMul (e ω r) (e ω s)) μ) →
    (∀ (r s : n),
        (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => instHMul.hMul (e ω r) (e ω s)) fun x =>
          instHMul.hMul σ2 (1 r s)) →
      (∀ (i : n), Ne (instHSub.hSub 1 (HansenEconometrics.hatMatrix X i i)) 0) →
        (∀ (i : n),
            MeasureTheory.Integrable
              (fun ω =>
                instHMul.hMul (Real.instInv.inv (instHSub.hSub 1 (HansenEconometrics.hatMatrix X i i)))
                  (instHPow.hPow ((HansenEconometrics.annihilatorMatrix X).mulVec (e ω) i) 2))
              μ) →
          (MeasureTheory.ae μ).EventuallyEq
            (MeasureTheory.condExp m μ fun ω a b =>
              HansenEconometrics.olsHuberWhiteHC2VarianceEstimator X (instHAdd.hAdd (X.mulVec β) (e ω)) a b)
            fun x a b => HansenEconometrics.olsConditionalVarianceMatrix X (instHSMul.hSMul σ2 1) a b

Direct statement dependencies (4)

• HansenEconometrics.annihilatorMatrix
• HansenEconometrics.hatMatrix
• HansenEconometrics.olsConditionalVarianceMatrix
• HansenEconometrics.olsHuberWhiteHC2VarianceEstimator

HansenEconometrics/Chapter4LeastSquaresRegression.lean:2538

theorem HansenEconometrics.condExp_olsHuberWhiteHC2VarianceEstimator_eq_diagonal

Matrix-valued conditional expectation of HC2 under diagonal heteroskedastic second moments.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {Ω : Type u_3}
  {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real)
  (σ2 : n → Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [MeasureTheory.IsProbabilityMeasure μ] (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  (∀ (r s : n), MeasureTheory.Integrable (fun ω => instHMul.hMul (e ω r) (e ω s)) μ) →
    (∀ (r s : n),
        (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => instHMul.hMul (e ω r) (e ω s)) fun x =>
          Matrix.diagonal σ2 r s) →
      (∀ (i : n),
          MeasureTheory.Integrable
            (fun ω =>
              instHMul.hMul (Real.instInv.inv (instHSub.hSub 1 (HansenEconometrics.hatMatrix X i i)))
                (instHPow.hPow ((HansenEconometrics.annihilatorMatrix X).mulVec (e ω) i) 2))
            μ) →
        (MeasureTheory.ae μ).EventuallyEq
          (MeasureTheory.condExp m μ fun ω a b =>
            HansenEconometrics.olsHuberWhiteHC2VarianceEstimator X (instHAdd.hAdd (X.mulVec β) (e ω)) a b)
          fun x a b =>
          HansenEconometrics.olsConditionalVarianceMatrix X
            (Matrix.diagonal fun i =>
              instHMul.hMul (Real.instInv.inv (instHSub.hSub 1 (HansenEconometrics.hatMatrix X i i)))
                (Finset.univ.sum fun r =>
                  instHMul.hMul
                    (instHMul.hMul (HansenEconometrics.annihilatorMatrix X i r)
                      (HansenEconometrics.annihilatorMatrix X i r))
                    (σ2 r)))
            a b

Direct statement dependencies (4)

• HansenEconometrics.annihilatorMatrix
• HansenEconometrics.hatMatrix
• HansenEconometrics.olsConditionalVarianceMatrix
• HansenEconometrics.olsHuberWhiteHC2VarianceEstimator

HansenEconometrics/Chapter4LeastSquaresRegression.lean:2603

HC3 covariance estimator4 endpoints

\hat V_{HC3} = (X'X)^{-1} X'\operatorname{diag}((1-h_{ii})^{-2}\hat e_i^2)X(X'X)^{-1}

def HansenEconometrics.olsHuberWhiteHC3VarianceEstimator

HC3 covariance estimator: leverage-adjusted by (1 - hᵢᵢ)⁻². Same totalization caveat as HC2 (zero at hᵢᵢ = 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) →
            (n → Real) →
              [DecidableEq n] →
                [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] → Matrix k k Real

HansenEconometrics/Chapter4LeastSquaresRegression.lean:138

theorem HansenEconometrics.olsHuberWhiteHC3VarianceEstimator_linear_model

In the linear model, HC3 uses annihilator-transformed errors.

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)
  (β : k → Real) (e : n → Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.olsHuberWhiteHC3VarianceEstimator X (instHAdd.hAdd (X.mulVec β) e))
    (HansenEconometrics.olsConditionalVarianceMatrix X
      (Matrix.diagonal fun i =>
        instHMul.hMul (instHPow.hPow (Real.instInv.inv (instHSub.hSub 1 (HansenEconometrics.hatMatrix X i i))) 2)
          (instHPow.hPow ((HansenEconometrics.annihilatorMatrix X).mulVec e i) 2)))

Direct statement dependencies (4)

• HansenEconometrics.annihilatorMatrix
• HansenEconometrics.hatMatrix
• HansenEconometrics.olsConditionalVarianceMatrix
• HansenEconometrics.olsHuberWhiteHC3VarianceEstimator

HansenEconometrics/Chapter4LeastSquaresRegression.lean:1252

theorem HansenEconometrics.condExp_olsHuberWhiteHC3VarianceEstimator_eq_homoskedastic_inflated

Matrix-valued conditional expectation of HC3 under homoskedastic second moments.

Relative to HC2, HC3 retains one extra inverse-leverage factor in each diagonal entry.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {Ω : Type u_3}
  {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real)
  (σ2 : Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [MeasureTheory.IsProbabilityMeasure μ] (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  (∀ (r s : n), MeasureTheory.Integrable (fun ω => instHMul.hMul (e ω r) (e ω s)) μ) →
    (∀ (r s : n),
        (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => instHMul.hMul (e ω r) (e ω s)) fun x =>
          instHMul.hMul σ2 (1 r s)) →
      (∀ (i : n), Ne (instHSub.hSub 1 (HansenEconometrics.hatMatrix X i i)) 0) →
        (∀ (i : n),
            MeasureTheory.Integrable
              (fun ω =>
                instHMul.hMul
                  (instHPow.hPow (Real.instInv.inv (instHSub.hSub 1 (HansenEconometrics.hatMatrix X i i))) 2)
                  (instHPow.hPow ((HansenEconometrics.annihilatorMatrix X).mulVec (e ω) i) 2))
              μ) →
          (MeasureTheory.ae μ).EventuallyEq
            (MeasureTheory.condExp m μ fun ω a b =>
              HansenEconometrics.olsHuberWhiteHC3VarianceEstimator X (instHAdd.hAdd (X.mulVec β) (e ω)) a b)
            fun x a b =>
            HansenEconometrics.olsConditionalVarianceMatrix X
              (Matrix.diagonal fun i =>
                instHMul.hMul σ2 (Real.instInv.inv (instHSub.hSub 1 (HansenEconometrics.hatMatrix X i i))))
              a b

Direct statement dependencies (4)

• HansenEconometrics.annihilatorMatrix
• HansenEconometrics.hatMatrix
• HansenEconometrics.olsConditionalVarianceMatrix
• HansenEconometrics.olsHuberWhiteHC3VarianceEstimator

HansenEconometrics/Chapter4LeastSquaresRegression.lean:2571

theorem HansenEconometrics.condExp_olsHuberWhiteHC3VarianceEstimator_eq_diagonal

Matrix-valued conditional expectation of HC3 under diagonal heteroskedastic second moments.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {Ω : Type u_3}
  {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real)
  (σ2 : n → Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [MeasureTheory.IsProbabilityMeasure μ] (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  (∀ (r s : n), MeasureTheory.Integrable (fun ω => instHMul.hMul (e ω r) (e ω s)) μ) →
    (∀ (r s : n),
        (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => instHMul.hMul (e ω r) (e ω s)) fun x =>
          Matrix.diagonal σ2 r s) →
      (∀ (i : n),
          MeasureTheory.Integrable
            (fun ω =>
              instHMul.hMul (instHPow.hPow (Real.instInv.inv (instHSub.hSub 1 (HansenEconometrics.hatMatrix X i i))) 2)
                (instHPow.hPow ((HansenEconometrics.annihilatorMatrix X).mulVec (e ω) i) 2))
            μ) →
        (MeasureTheory.ae μ).EventuallyEq
          (MeasureTheory.condExp m μ fun ω a b =>
            HansenEconometrics.olsHuberWhiteHC3VarianceEstimator X (instHAdd.hAdd (X.mulVec β) (e ω)) a b)
          fun x a b =>
          HansenEconometrics.olsConditionalVarianceMatrix X
            (Matrix.diagonal fun i =>
              instHMul.hMul (instHPow.hPow (Real.instInv.inv (instHSub.hSub 1 (HansenEconometrics.hatMatrix X i i))) 2)
                (Finset.univ.sum fun r =>
                  instHMul.hMul
                    (instHMul.hMul (HansenEconometrics.annihilatorMatrix X i r)
                      (HansenEconometrics.annihilatorMatrix X i r))
                    (σ2 r)))
            a b

Direct statement dependencies (4)

• HansenEconometrics.annihilatorMatrix
• HansenEconometrics.hatMatrix
• HansenEconometrics.olsConditionalVarianceMatrix
• HansenEconometrics.olsHuberWhiteHC3VarianceEstimator

HansenEconometrics/Chapter4LeastSquaresRegression.lean:2637

Clustered covariance estimator6 of 36 linked endpoints

cluster-level score sandwich, Hansen finite-sample adjustment, singleton-cluster simplifications, finite block decompositions, cluster covariance middle/sandwich formulas, and CR3-style leave-cluster-out estimator

theorem HansenEconometrics.olsClusteredCR3VarianceEstimator_posSemidef

The CR3-style clustered covariance estimator is positive semidefinite.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {G : Type u_3}
  [inst_3 : Fintype G] [inst_4 : DecidableEq G] (X : Matrix n k Real) (y : n → Real) (cluster : n → G)
  [inst_5 : DecidableEq n] [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  (hInv : (g : G) → Invertible (HansenEconometrics.clusterLeaveOutAdjustmentMatrix X cluster g)),
  (HansenEconometrics.olsClusteredCR3VarianceEstimator X y cluster hInv).PosSemidef

Direct statement dependencies (3)

• HansenEconometrics.ClusterIndex
• HansenEconometrics.clusterLeaveOutAdjustmentMatrix
• HansenEconometrics.olsClusteredCR3VarianceEstimator

HansenEconometrics/Chapter4LeastSquaresRegression.lean:1159

theorem HansenEconometrics.olsClusteredVarianceEstimatorAdjusted_posSemidef

The finite-sample adjusted clustered covariance estimator is positive semidefinite whenever the adjustment factor is nonnegative.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {G : Type u_3}
  [inst_3 : Fintype G] [inst_4 : DecidableEq G] (X : Matrix n k Real) (y : n → Real) (cluster : n → G)
  [inst_5 : DecidableEq n] [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Real.instLE.le 0 (HansenEconometrics.clusterFiniteSampleAdjustment n k G) →
    (HansenEconometrics.olsClusteredVarianceEstimatorAdjusted X y cluster).PosSemidef

Direct statement dependencies (2)

• HansenEconometrics.clusterFiniteSampleAdjustment
• HansenEconometrics.olsClusteredVarianceEstimatorAdjusted

HansenEconometrics/Chapter4LeastSquaresRegression.lean:360

theorem HansenEconometrics.olsClusteredVarianceEstimatorAdjusted_posSemidef_of_card

The finite-sample adjusted clustered covariance estimator is positive semidefinite on the standard cardinality range k < n and 1 < G.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {G : Type u_3}
  [inst_3 : Fintype G] [inst_4 : DecidableEq G] (X : Matrix n k Real) (y : n → Real) (cluster : n → G)
  [inst_5 : DecidableEq n] [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  instLTNat.lt (Fintype.card k) (Fintype.card n) →
    instLTNat.lt 1 (Fintype.card G) → (HansenEconometrics.olsClusteredVarianceEstimatorAdjusted X y cluster).PosSemidef

Direct statement dependencies (1)

• HansenEconometrics.olsClusteredVarianceEstimatorAdjusted

HansenEconometrics/Chapter4LeastSquaresRegression.lean:371

theorem HansenEconometrics.olsBeta_linear_decomposition_clusterScores

Hansen clustered OLS decomposition: β_hat - β = (X’X)^{-1} ∑_g X_g’e_g.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {G : Type u_3}
  [inst_3 : Fintype G] [inst_4 : DecidableEq G] (X : Matrix n k Real) (β : k → Real) (e : n → Real) (cluster : n → G)
  [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (HansenEconometrics.olsBeta X (instHAdd.hAdd (X.mulVec β) e))
    (instHAdd.hAdd β
      ((inst_5.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)).mulVec
        (Finset.univ.sum fun g => HansenEconometrics.clusterErrorScore X e cluster g)))

Direct statement dependencies (2)

• HansenEconometrics.clusterErrorScore
• HansenEconometrics.olsBeta

HansenEconometrics/Chapter4LeastSquaresRegression.lean:727

theorem HansenEconometrics.clusterLeaveOutBeta_eq_olsBeta_sub_invGram_mulVec_cr3Residual

Hansen equation (4.53), reduced-Gram form.

The cluster-deleted coefficient equals the full-sample coefficient minus the cluster leverage correction based on the CR3-style prediction errors.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {G : Type u_3}
  [inst_3 : DecidableEq G] (X : Matrix n k Real) (y : n → Real) (cluster : n → G) (g : G) [inst_4 : DecidableEq n]
  [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_6 : Invertible (HansenEconometrics.clusterLeaveOutAdjustmentMatrix X cluster g)]
  [inst_7 : Invertible (HansenEconometrics.clusterLeaveOutGram X cluster g)],
  Eq (HansenEconometrics.clusterLeaveOutBeta X y cluster g)
    (instHSub.hSub (HansenEconometrics.olsBeta X y)
      ((inst_5.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)).mulVec
        ((HansenEconometrics.clusterDesign X cluster g).transpose.mulVec
          (HansenEconometrics.clusterCR3Residual X y cluster g))))

Direct statement dependencies (7)

• HansenEconometrics.ClusterIndex
• HansenEconometrics.clusterCR3Residual
• HansenEconometrics.clusterDesign
• HansenEconometrics.clusterLeaveOutAdjustmentMatrix
• HansenEconometrics.clusterLeaveOutBeta
• HansenEconometrics.clusterLeaveOutGram
• HansenEconometrics.olsBeta

HansenEconometrics/Chapter4LeastSquaresRegression.lean:953

theorem HansenEconometrics.olsClusteredCR3VarianceEstimator_eq_clusterCovarianceMiddle_cr3Outer

Hansen equation (4.54) with the CR3 residual block outer-product expression for the clustered middle matrix.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] {G : Type u_3}
  [inst_3 : Fintype G] [inst_4 : DecidableEq G] (X : Matrix n k Real) (y : n → Real) (cluster : n → G)
  [inst_5 : DecidableEq n] [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  (hInv : (g : G) → Invertible (HansenEconometrics.clusterLeaveOutAdjustmentMatrix X cluster g)),
  Eq (HansenEconometrics.olsClusteredCR3VarianceEstimator X y cluster hInv)
    (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
        (inst_6.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X))
        (HansenEconometrics.clusterCovarianceMiddle X cluster fun g =>
          Matrix.vecMulVec (HansenEconometrics.clusterCR3Residual X y cluster g)
            (HansenEconometrics.clusterCR3Residual X y cluster g)))
      (inst_6.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)))

Direct statement dependencies (5)

• HansenEconometrics.ClusterIndex
• HansenEconometrics.clusterCR3Residual
• HansenEconometrics.clusterCovarianceMiddle
• HansenEconometrics.clusterLeaveOutAdjustmentMatrix
• HansenEconometrics.olsClusteredCR3VarianceEstimator

HansenEconometrics/Chapter4LeastSquaresRegression.lean:1116