Chapter 5: Normal Regression

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

This page is generated from the canonical Chapter 5 inventory and the compiled Lean environment. It contains 16 textbook result groups and 32 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 5.1 standard normal moments3 endpoints

If Z \sim N(0,1), then all integer moments are finite, odd moments vanish, \mathbb{E}[Z^{2m}] = (2m-1)!!, and for r \gt 0, \mathbb{E}[|Z|^r] = 2^{r/2} \pi^{-1/2} \Gamma\!\left(\frac{r+1}{2}\right)

theorem HansenEconometrics.standardNormal_memLp

Standard normal random variables have finite moments of every finite nonnegative order. This is the Mathlib-backed finite-moment face of Hansen Theorem 5.1.

Formal statement

∀ (p : NNReal), MeasureTheory.MemLp id (ENNReal.ofNNReal p) (ProbabilityTheory.gaussianReal 0 1)

HansenEconometrics/MultivariateNormal.lean:23

theorem HansenEconometrics.standardNormal_mean

The standard normal has mean zero.

Formal statement

Eq (MeasureTheory.integral (ProbabilityTheory.gaussianReal 0 1) fun z => z) 0

HansenEconometrics/MultivariateNormal.lean:28

theorem HansenEconometrics.standardNormal_variance

The standard normal has variance one.

Formal statement

Eq (ProbabilityTheory.variance id (ProbabilityTheory.gaussianReal 0 1)) 1

HansenEconometrics/MultivariateNormal.lean:33

Theorem 5.2 affine image of a multivariate normal2 endpoints

If X \sim N(\mu,\Sigma) and Y = a + B X, then Y \sim N(a + B\mu, B \Sigma B')

theorem HansenEconometrics.map_affine_multivariateGaussian

Hansen Theorem 5.2. If X ∼ N(μ, Σ), then a + B X has law N(a + B μ, B Σ B’).

Formal statement

∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] {μ : EuclideanSpace Real n} {S : Matrix n n Real},
  S.PosSemidef →
    ∀ (a : EuclideanSpace Real m) (B : Matrix m n Real),
      Eq
        (MeasureTheory.Measure.map
          (fun x =>
            instHAdd.hAdd a (ContinuousLinearMap.funLike.coe (HansenEconometrics.matrixContinuousLinearMap B) x))
          (ProbabilityTheory.multivariateGaussian μ S))
        (ProbabilityTheory.multivariateGaussian
          (instHAdd.hAdd a (ContinuousLinearMap.funLike.coe (HansenEconometrics.matrixContinuousLinearMap B) μ))
          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul B S)
            B.conjTranspose))

Direct statement dependencies (1)

• HansenEconometrics.matrixContinuousLinearMap

HansenEconometrics/MultivariateNormal.lean:111

theorem HansenEconometrics.hasLaw_affine_multivariateGaussian

Random-variable version of Hansen Theorem 5.2.

Formal statement

∀ {Ω : Type u_1} {m : Type u_2} {n : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] {P : MeasureTheory.Measure Ω} {X : Ω → EuclideanSpace Real n}
  {μ : EuclideanSpace Real n} {S : Matrix n n Real},
  S.PosSemidef →
    ProbabilityTheory.HasLaw X (ProbabilityTheory.multivariateGaussian μ S) P →
      ∀ (a : EuclideanSpace Real m) (B : Matrix m n Real),
        ProbabilityTheory.HasLaw
          (fun ω =>
            instHAdd.hAdd a (ContinuousLinearMap.funLike.coe (HansenEconometrics.matrixContinuousLinearMap B) (X ω)))
          (ProbabilityTheory.multivariateGaussian
            (instHAdd.hAdd a (ContinuousLinearMap.funLike.coe (HansenEconometrics.matrixContinuousLinearMap B) μ))
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul B S)
              B.conjTranspose))
          P

Direct statement dependencies (1)

• HansenEconometrics.matrixContinuousLinearMap

HansenEconometrics/MultivariateNormal.lean:129

Theorem 5.3 properties of the multivariate normal5 endpoints

For X \sim N(\mu,\Sigma): \mathbb{E}[X] = \mu, \operatorname{Var}(X) = \Sigma, uncorrelated subvectors are independent, affine images are normal, and the standard quadratic-form laws give \chi^2, non-central \chi^2, and t/F consequences

theorem HansenEconometrics.multivariateGaussian_mean

The mean vector of N(μ, Σ) is μ.

Formal statement

∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {μ : EuclideanSpace Real n} {S : Matrix n n Real},
  Eq (MeasureTheory.integral (ProbabilityTheory.multivariateGaussian μ S) fun x => x) μ

HansenEconometrics/MultivariateNormal.lean:151

theorem HansenEconometrics.multivariateGaussian_covarianceBilin

The covariance bilinear form of N(μ, Σ) is represented by Σ.

Formal statement

∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {μ : EuclideanSpace Real n} {S : Matrix n n Real},
  S.PosSemidef →
    ∀ (u v : EuclideanSpace Real n),
      Eq
        (ContinuousLinearMap.funLike.coe
          (ContinuousLinearMap.funLike.coe
            (ProbabilityTheory.covarianceBilin (ProbabilityTheory.multivariateGaussian μ S)) u)
          v)
        (dotProduct u.ofLp (S.mulVec v.ofLp))

HansenEconometrics/MultivariateNormal.lean:158

theorem HansenEconometrics.multivariateGaussian_eval_hasLaw

A coordinate projection of a multivariate normal is univariate normal.

Formal statement

∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {μ : EuclideanSpace Real n} {S : Matrix n n Real},
  S.PosSemidef →
    ∀ (i : n),
      ProbabilityTheory.HasLaw (fun x => x.ofLp i) (ProbabilityTheory.gaussianReal (μ.ofLp i) (S i i).toNNReal)
        (ProbabilityTheory.multivariateGaussian μ S)

HansenEconometrics/MultivariateNormal.lean:182

theorem HansenEconometrics.multivariateGaussian_restrict₂_hasLaw

A coordinate subvector of a multivariate normal is multivariate normal with the corresponding subvector mean and covariance submatrix.

Formal statement

∀ {ι : Type u_1} [inst : DecidableEq ι] {I J : Finset ι}
  {μ : EuclideanSpace Real (Subtype fun x => SetLike.instMembership.mem I x)}
  {S : Matrix (Subtype fun x => SetLike.instMembership.mem I x) (Subtype fun x => SetLike.instMembership.mem I x) Real},
  S.PosSemidef →
    ∀ (hJI : Finset.instHasSubset.Subset J I),
      ProbabilityTheory.HasLaw (ContinuousLinearMap.funLike.coe (EuclideanSpace.restrict₂ hJI))
        (ProbabilityTheory.multivariateGaussian (ContinuousLinearMap.funLike.coe (EuclideanSpace.restrict₂ hJI) μ)
          (S.submatrix (fun i => ⟨i.val, ⋯⟩) fun i => ⟨i.val, ⋯⟩))
        (ProbabilityTheory.multivariateGaussian μ S)

HansenEconometrics/MultivariateNormal.lean:192

theorem HansenEconometrics.jointGaussian_indepFun_iff_cov_eq_zero

For scalar jointly Gaussian variables, independence is equivalent to zero covariance. This is the scalar Hansen-facing form of the uncorrelated-subvector property in Theorem 5.3.

Formal statement

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X Y : Ω → Real},
  ProbabilityTheory.HasGaussianLaw (fun ω => { fst := X ω, snd := Y ω }) P →
    Iff (ProbabilityTheory.IndepFun X Y P) (Eq (ProbabilityTheory.covariance X Y P) 0)

HansenEconometrics/MultivariateNormal.lean:204

Theorem 5.4 conditional law of the OLS coefficient vector2 endpoints

\hat{\beta} \mid X \sim N\!\left(\beta, \sigma^2 (X'X)^{-1}\right)

theorem HansenEconometrics.olsBeta_hasGaussianLaw_of_error

If the error vector has a Gaussian law, then the OLS coefficient vector is Gaussian as an affine image of the error vector.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [DecidableEq n] [inst_3 : DecidableEq k]
  {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real)
  (e : Ω → n → Real) [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  ProbabilityTheory.HasGaussianLaw e μ →
    ProbabilityTheory.HasGaussianLaw (fun ω => HansenEconometrics.olsBeta X (instHAdd.hAdd (X.mulVec β) (e ω))) μ

Direct statement dependencies (1)

• HansenEconometrics.olsBeta

HansenEconometrics/Chapter5NormalRegression.lean:37

theorem HansenEconometrics.olsBeta_memLp_of_error_gaussian

Fixed-design normal-regression coefficient vectors have finite moments of every finite order. This is the fixed-X finite-moment face behind the normal coefficient law; the random-design Kinal threshold is a separate tail statement about the inverse random Gram 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}
  [inst_3 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real)
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] (p : ENNReal),
  Ne p instTopENNReal.top →
    ProbabilityTheory.HasGaussianLaw e μ →
      MeasureTheory.MemLp (fun ω => HansenEconometrics.olsBeta X (instHAdd.hAdd (X.mulVec β) (e ω))) p μ

Direct statement dependencies (1)

• HansenEconometrics.olsBeta

HansenEconometrics/Chapter5NormalRegression.lean:68

Theorem 5.5 Kinal (1980) moment existence1 endpoint

If (Y,X) are jointly normal, then \mathbb{E}\|\hat{\beta}\|^r \lt \infty if and only if r \lt n-k+1

theorem HansenEconometrics.olsBeta_memLp_of_error_gaussian

Fixed-design normal-regression coefficient vectors have finite moments of every finite order. This is the fixed-X finite-moment face behind the normal coefficient law; the random-design Kinal threshold is a separate tail statement about the inverse random Gram 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}
  [inst_3 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real)
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)] (p : ENNReal),
  Ne p instTopENNReal.top →
    ProbabilityTheory.HasGaussianLaw e μ →
      MeasureTheory.MemLp (fun ω => HansenEconometrics.olsBeta X (instHAdd.hAdd (X.mulVec β) (e ω))) p μ

Direct statement dependencies (1)

• HansenEconometrics.olsBeta

HansenEconometrics/Chapter5NormalRegression.lean:68

Theorem 5.6 conditional law of the OLS residual vector1 endpoint

\hat{e} \mid X \sim N(0,\sigma^2 M) and \hat{e} is independent of \hat{\beta}

theorem HansenEconometrics.residual_hasGaussianLaw_of_error

If the error vector has a Gaussian law, then the OLS residual vector is Gaussian as a linear image of the error vector.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [DecidableEq n] [inst_3 : DecidableEq k]
  {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real)
  (e : Ω → n → Real) [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  ProbabilityTheory.HasGaussianLaw e μ →
    ProbabilityTheory.HasGaussianLaw (fun ω => HansenEconometrics.residual X (instHAdd.hAdd (X.mulVec β) (e ω))) μ

Direct statement dependencies (1)

• HansenEconometrics.residual

HansenEconometrics/Chapter5NormalRegression.lean:79

Residual variance estimator1 endpoint

s^2 = \hat{e}' \hat{e} / (n-k)

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

Residual variance under the linear model1 endpoint

s^2 = (M e)' (M e) / (n-k)

theorem HansenEconometrics.olsResidualVarianceEstimator_linear_model

Under the linear model, the residual variance estimator is the residual quadratic form divided by n-k, expressed directly in terms of the model 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.olsResidualVarianceEstimator X (instHAdd.hAdd (X.mulVec β) e))
    (instHDiv.hDiv
      (dotProduct ((HansenEconometrics.annihilatorMatrix X).mulVec 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:1375

Residual quadratic form identity1 endpoint

\hat{e}' \hat{e} = e' M e

theorem HansenEconometrics.residual_quadratic_form_of_linear_model

The residual sum of squares in the linear model is the annihilator quadratic form e’Me.

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)
  (e : n → Real) [inst_3 : DecidableEq n]
  [inst_4 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq
    (dotProduct ((HansenEconometrics.annihilatorMatrix X).mulVec e) ((HansenEconometrics.annihilatorMatrix X).mulVec e))
    (dotProduct e ((HansenEconometrics.annihilatorMatrix X).mulVec e))

Direct statement dependencies (1)

• HansenEconometrics.annihilatorMatrix

HansenEconometrics/Chapter4LeastSquaresRegression.lean:1387

Theorem 5.7 residual variance estimator distribution2 endpoints

\dfrac{(n-k)s^2}{\sigma^2} \sim \chi^2_{n-k} and s^2 is independent of \hat{\beta}

theorem HansenEconometrics.scaledOlsResidualVarianceStatistic_hasLaw_chiSquared

Hansen Theorem 5.7, chi-square component: in the homoskedastic normal regression model, (n-k) s² / σ² has a chi-square distribution with n-k degrees of freedom.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq k] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) {σ2 : Real},
  Real.instLT.lt 0 σ2 →
    instLTNat.lt (Fintype.card k) (Fintype.card n) →
      ∀ (ε : Ω → EuclideanSpace Real n)
        [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
        ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
          ProbabilityTheory.HasLaw (HansenEconometrics.scaledOlsResidualVarianceStatistic X β σ2 ε)
            (HansenEconometrics.chiSquared (instHSub.hSub (Fintype.card n) (Fintype.card k))) μ

Direct statement dependencies (2)

• HansenEconometrics.chiSquared
• HansenEconometrics.scaledOlsResidualVarianceStatistic

HansenEconometrics/Chapter5NormalRegression.lean:216

theorem HansenEconometrics.olsBeta_indep_scaledOlsResidualVarianceStatistic

No plain-language docstring is available.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq k] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) {σ2 : Real},
  Real.instLT.lt 0 σ2 →
    instLTNat.lt (Fintype.card k) (Fintype.card n) →
      ∀ (ε : Ω → EuclideanSpace Real n)
        [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
        ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
          ProbabilityTheory.IndepFun (fun ω => HansenEconometrics.olsBeta X (instHAdd.hAdd (X.mulVec β) (ε ω).ofLp))
            (HansenEconometrics.scaledOlsResidualVarianceStatistic X β σ2 ε) μ

Direct statement dependencies (2)

• HansenEconometrics.olsBeta
• HansenEconometrics.scaledOlsResidualVarianceStatistic

HansenEconometrics/Chapter5NormalRegression.lean:305

Theorem 5.8 exact t statistic law1 endpoint

T = \dfrac{\hat{\beta}_j - \beta_j}{\sqrt{s^2[(X'X)^{-1}]_{jj}}} \sim t_{n-k}

theorem HansenEconometrics.olsTStat_hasLaw_classicalStudentT

Hansen Theorem 5.8 in classical form: the OLS t-statistic has the standalone density-backed Student-t law with n-k degrees of freedom.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq k] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) {σ2 : Real} (j : k),
  Real.instLT.lt 0 σ2 →
    instLTNat.lt (Fintype.card k) (Fintype.card n) →
      ∀ (ε : Ω → EuclideanSpace Real n)
        [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
        ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
          ProbabilityTheory.HasLaw (HansenEconometrics.olsTStat X β σ2 j ε)
            (HansenEconometrics.classicalStudentT (instHSub.hSub (Fintype.card n) (Fintype.card k))) μ

Direct statement dependencies (2)

• HansenEconometrics.classicalStudentT
• HansenEconometrics.olsTStat

HansenEconometrics/Chapter5NormalRegression.lean:607

Theorem 5.9 regression-coefficient confidence interval3 endpoints

\hat{C} = [\hat{\beta} - c\, s(\hat{\beta}), \hat{\beta} + c\, s(\hat{\beta})] with c = F^{-1}(1-\alpha/2) satisfies \mathbb{P}[\beta \in \hat{C}] = 1 - \alpha

theorem HansenEconometrics.olsConfidenceInterval_coverage_eq_classicalStudentT_interval

Classical version of the exact coverage theorem for Hansen’s Chapter 5 coefficient confidence interval for an arbitrary critical value c.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq k] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) {σ2 : Real} (j : k) (c : Real),
  Real.instLT.lt 0 σ2 →
    instLTNat.lt (Fintype.card k) (Fintype.card n) →
      ∀ (ε : Ω → EuclideanSpace Real n)
        [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
        ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
          Eq
            (μ.real
              (setOf fun ω =>
                Set.instMembership.mem
                  (HansenEconometrics.olsConfidenceInterval X j c (instHAdd.hAdd (X.mulVec β) (ε ω).ofLp)) (β j)))
            ((HansenEconometrics.classicalStudentT (instHSub.hSub (Fintype.card n) (Fintype.card k))).real
              (Set.Icc (Real.instNeg.neg c) c))

Direct statement dependencies (2)

• HansenEconometrics.classicalStudentT
• HansenEconometrics.olsConfidenceInterval

HansenEconometrics/Chapter5NormalRegression.lean:833

theorem HansenEconometrics.olsConfidenceInterval_coverage_eq_classicalStudentT_cdf

Classical CDF version of the exact coverage theorem for Hansen’s Chapter 5 coefficient confidence interval.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq k] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) {σ2 : Real} (j : k) (c : Real),
  Real.instLE.le 0 c →
    Real.instLT.lt 0 σ2 →
      instLTNat.lt (Fintype.card k) (Fintype.card n) →
        ∀ (ε : Ω → EuclideanSpace Real n)
          [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
          ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
            Eq
              (μ.real
                (setOf fun ω =>
                  Set.instMembership.mem
                    (HansenEconometrics.olsConfidenceInterval X j c (instHAdd.hAdd (X.mulVec β) (ε ω).ofLp)) (β j)))
              (instHSub.hSub
                ((ProbabilityTheory.cdf
                      (HansenEconometrics.classicalStudentT (instHSub.hSub (Fintype.card n) (Fintype.card k)))).toFun
                  c)
                (Function.leftLim
                  (ProbabilityTheory.cdf
                      (HansenEconometrics.classicalStudentT (instHSub.hSub (Fintype.card n) (Fintype.card k)))).toFun
                  (Real.instNeg.neg c)))

Direct statement dependencies (2)

• HansenEconometrics.classicalStudentT
• HansenEconometrics.olsConfidenceInterval

HansenEconometrics/Chapter5NormalRegression.lean:903

theorem HansenEconometrics.olsConfidenceInterval_coverage_eq_one_sub_classical

Classical confidence-interval version of Hansen Theorem 5.9: if the critical value c matches the desired tail probabilities for the standalone density-backed Student-t law, then the classical OLS interval has exact coverage 1 - α.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq k] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) {σ2 α : Real} (j : k) (c : Real),
  Real.instLE.le 0 c →
    Eq
        ((ProbabilityTheory.cdf
              (HansenEconometrics.classicalStudentT (instHSub.hSub (Fintype.card n) (Fintype.card k)))).toFun
          c)
        (instHSub.hSub 1 (instHDiv.hDiv α 2)) →
      Eq
          (Function.leftLim
            (ProbabilityTheory.cdf
                (HansenEconometrics.classicalStudentT (instHSub.hSub (Fintype.card n) (Fintype.card k)))).toFun
            (Real.instNeg.neg c))
          (instHDiv.hDiv α 2) →
        Real.instLT.lt 0 σ2 →
          instLTNat.lt (Fintype.card k) (Fintype.card n) →
            ∀ (ε : Ω → EuclideanSpace Real n)
              [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
              ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
                Eq
                  (μ.real
                    (setOf fun ω =>
                      Set.instMembership.mem
                        (HansenEconometrics.olsConfidenceInterval X j c (instHAdd.hAdd (X.mulVec β) (ε ω).ofLp)) (β j)))
                  (instHSub.hSub 1 α)

Direct statement dependencies (2)

• HansenEconometrics.classicalStudentT
• HansenEconometrics.olsConfidenceInterval

HansenEconometrics/Chapter5NormalRegression.lean:977

Theorem 5.10 rule-of-thumb 95\% interval1 endpoint

If n-k \ge 61, then \hat{C} = [\hat{\beta} - 2 s(\hat{\beta}), \hat{\beta} + 2 s(\hat{\beta})] has coverage probability at least 0.95

theorem HansenEconometrics.olsConfidenceInterval_two_se_coverage_ge_nineteen_twentieths

Hansen Theorem 5.10: if the residual degrees of freedom satisfy n - k ≥ 61, then the two-standard-error OLS coefficient confidence interval has at least 95% coverage.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq k] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) {σ2 : Real} (j : k),
  Real.instLT.lt 0 σ2 →
    instLENat.le 61 (instHSub.hSub (Fintype.card n) (Fintype.card k)) →
      ∀ (ε : Ω → EuclideanSpace Real n)
        [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
        ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
          Real.instLE.le (19 / 20)
            (μ.real
              (setOf fun ω =>
                Set.instMembership.mem
                  (HansenEconometrics.olsConfidenceInterval X j 2 (instHAdd.hAdd (X.mulVec β) (ε ω).ofLp)) (β j)))

Direct statement dependencies (1)

• HansenEconometrics.olsConfidenceInterval

HansenEconometrics/Chapter5NormalRegression.lean:995

Theorem 5.11 error-variance confidence interval3 endpoints

\hat{C} = \left[\dfrac{(n-k)s^2}{c_2}, \dfrac{(n-k)s^2}{c_1}\right] with c_1 = F^{-1}(\alpha/2) and c_2 = F^{-1}(1-\alpha/2) satisfies \mathbb{P}[\sigma^2 \in \hat{C}] = 1 - \alpha

theorem HansenEconometrics.olsVarianceCI_coverage_eq_chiSquared_interval

Exact interval-probability statement underlying Hansen Theorem 5.11.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq k] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) {σ2 : Real} (c₁ c₂ : Real),
  Real.instLT.lt 0 σ2 →
    instLTNat.lt (Fintype.card k) (Fintype.card n) →
      Real.instLT.lt 0 c₁ →
        Real.instLE.le c₁ c₂ →
          ∀ (ε : Ω → EuclideanSpace Real n)
            [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
            ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
              Eq
                (μ.real
                  (setOf fun ω =>
                    Set.instMembership.mem (HansenEconometrics.olsVarianceConfidenceInterval X β c₁ c₂ ε ω) σ2))
                ((HansenEconometrics.chiSquared (instHSub.hSub (Fintype.card n) (Fintype.card k))).real (Set.Icc c₁ c₂))

Direct statement dependencies (2)

• HansenEconometrics.chiSquared
• HansenEconometrics.olsVarianceConfidenceInterval

HansenEconometrics/Chapter5NormalRegression.lean:1059

theorem HansenEconometrics.olsVarianceConfidenceInterval_coverage_eq_chiSquared_cdf

CDF version of the exact variance-interval coverage identity from Hansen Theorem 5.11.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq k] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) {σ2 : Real} (c₁ c₂ : Real),
  Real.instLT.lt 0 σ2 →
    instLTNat.lt (Fintype.card k) (Fintype.card n) →
      Real.instLT.lt 0 c₁ →
        Real.instLE.le c₁ c₂ →
          ∀ (ε : Ω → EuclideanSpace Real n)
            [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
            ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
              Eq
                (μ.real
                  (setOf fun ω =>
                    Set.instMembership.mem (HansenEconometrics.olsVarianceConfidenceInterval X β c₁ c₂ ε ω) σ2))
                (instHSub.hSub
                  ((ProbabilityTheory.cdf
                        (HansenEconometrics.chiSquared (instHSub.hSub (Fintype.card n) (Fintype.card k)))).toFun
                    c₂)
                  ((ProbabilityTheory.cdf
                        (HansenEconometrics.chiSquared (instHSub.hSub (Fintype.card n) (Fintype.card k)))).toFun
                    c₁))

Direct statement dependencies (2)

• HansenEconometrics.chiSquared
• HansenEconometrics.olsVarianceConfidenceInterval

HansenEconometrics/Chapter5NormalRegression.lean:1082

theorem HansenEconometrics.olsVarianceConfidenceInterval_coverage_eq_one_sub

Critical-value wrapper for Hansen Theorem 5.11: if the chi-square interval endpoints match the desired α/2 and 1 - α/2 cdf values, then the variance interval has exact coverage 1 - α.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq k] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) {σ2 α : Real} (c₁ c₂ : Real),
  Eq
      ((ProbabilityTheory.cdf (HansenEconometrics.chiSquared (instHSub.hSub (Fintype.card n) (Fintype.card k)))).toFun
        c₁)
      (instHDiv.hDiv α 2) →
    Eq
        ((ProbabilityTheory.cdf (HansenEconometrics.chiSquared (instHSub.hSub (Fintype.card n) (Fintype.card k)))).toFun
          c₂)
        (instHSub.hSub 1 (instHDiv.hDiv α 2)) →
      Real.instLT.lt 0 σ2 →
        instLTNat.lt (Fintype.card k) (Fintype.card n) →
          Real.instLT.lt 0 c₁ →
            Real.instLE.le c₁ c₂ →
              ∀ (ε : Ω → EuclideanSpace Real n)
                [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
                ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
                  Eq
                    (μ.real
                      (setOf fun ω =>
                        Set.instMembership.mem (HansenEconometrics.olsVarianceConfidenceInterval X β c₁ c₂ ε ω) σ2))
                    (instHSub.hSub 1 α)

Direct statement dependencies (2)

• HansenEconometrics.chiSquared
• HansenEconometrics.olsVarianceConfidenceInterval

HansenEconometrics/Chapter5NormalRegression.lean:1111

Theorem 5.12 classical t test3 endpoints

Under H_0 : \beta = \beta_0, if T = \dfrac{\hat{\beta} - \beta_0}{s(\hat{\beta})} and c satisfies \mathbb{P}(|t_{n-k}| \ge c) = \alpha, then the test “reject H_0 if |T| \gt c” has significance level \alpha

theorem HansenEconometrics.olsNullTStat_hasLaw_classicalStudentT

Hansen Theorem 5.12 null-law wrapper: under the null hypothesis H₀ : β_j = β₀, the literal null-centered t-statistic has the classical Student-t law with n-k degrees of freedom.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq k] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) {σ2 : Real} (j : k) (β0 : Real),
  Eq (β j) β0 →
    Real.instLT.lt 0 σ2 →
      instLTNat.lt (Fintype.card k) (Fintype.card n) →
        ∀ (ε : Ω → EuclideanSpace Real n)
          [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
          ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
            ProbabilityTheory.HasLaw
              (fun ω => HansenEconometrics.olsNullTStat X j β0 (instHAdd.hAdd (X.mulVec β) (ε ω).ofLp))
              (HansenEconometrics.classicalStudentT (instHSub.hSub (Fintype.card n) (Fintype.card k))) μ

Direct statement dependencies (2)

• HansenEconometrics.classicalStudentT
• HansenEconometrics.olsNullTStat

HansenEconometrics/Chapter5NormalRegression.lean:732

theorem HansenEconometrics.olsTStat_rejection_probability_eq_alpha_classical

Hansen Theorem 5.12 in classical form: if the critical value c is calibrated against the standalone density-backed Student-t law, then the two-sided rejection rule c < |T| has exact size α under the null.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq k] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) {σ2 α : Real} (j : k) (c : Real),
  Real.instLE.le 0 c →
    Eq
        ((ProbabilityTheory.cdf
              (HansenEconometrics.classicalStudentT (instHSub.hSub (Fintype.card n) (Fintype.card k)))).toFun
          c)
        (instHSub.hSub 1 (instHDiv.hDiv α 2)) →
      Eq
          (Function.leftLim
            (ProbabilityTheory.cdf
                (HansenEconometrics.classicalStudentT (instHSub.hSub (Fintype.card n) (Fintype.card k)))).toFun
            (Real.instNeg.neg c))
          (instHDiv.hDiv α 2) →
        Real.instLT.lt 0 σ2 →
          instLTNat.lt (Fintype.card k) (Fintype.card n) →
            ∀ (ε : Ω → EuclideanSpace Real n)
              [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
              ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
                Eq (μ.real (setOf fun ω => Real.instLT.lt c (abs (HansenEconometrics.olsTStat X β σ2 j ε ω)))) α

Direct statement dependencies (2)

• HansenEconometrics.classicalStudentT
• HansenEconometrics.olsTStat

HansenEconometrics/Chapter5NormalRegression.lean:1197

theorem HansenEconometrics.olsTTest_rejection_probability_eq_alpha

Hansen Theorem 5.12 in explicit testing language: under the null hypothesis H₀ : β_j = β₀, if the critical value c is calibrated against the classical Student-t law, then the two-sided test that rejects when |T_j(β₀)| > c has exact size α.

Formal statement

∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq n]
  [inst_3 : DecidableEq k] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) {σ2 α : Real} (j : k) (β0 c : Real),
  Eq (β j) β0 →
    Real.instLE.le 0 c →
      Eq
          ((ProbabilityTheory.cdf
                (HansenEconometrics.classicalStudentT (instHSub.hSub (Fintype.card n) (Fintype.card k)))).toFun
            c)
          (instHSub.hSub 1 (instHDiv.hDiv α 2)) →
        Eq
            (Function.leftLim
              (ProbabilityTheory.cdf
                  (HansenEconometrics.classicalStudentT (instHSub.hSub (Fintype.card n) (Fintype.card k)))).toFun
              (Real.instNeg.neg c))
            (instHDiv.hDiv α 2) →
          Real.instLT.lt 0 σ2 →
            instLTNat.lt (Fintype.card k) (Fintype.card n) →
              ∀ (ε : Ω → EuclideanSpace Real n)
                [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
                ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
                  Eq
                    (μ.real
                      (setOf fun ω =>
                        HansenEconometrics.olsTTestRejects X j β0 c (instHAdd.hAdd (X.mulVec β) (ε ω).ofLp)))
                    α

Direct statement dependencies (2)

• HansenEconometrics.classicalStudentT
• HansenEconometrics.olsTTestRejects

HansenEconometrics/Chapter5NormalRegression.lean:1221

Theorem 5.13 likelihood-ratio / F-test layer2 endpoints

Under H_0 : \beta_2 = 0, if F = \dfrac{(\tilde{\sigma}^2 - \hat{\sigma}^2)/q}{\hat{\sigma}^2/(n-k)}, then F \sim F_{q,n-k} and the test “reject H_0 if F \gt c” has significance level \alpha when \mathbb{P}(F_{q,n-k} \ge c) = \alpha

theorem HansenEconometrics.olsFStatistic_hasLaw_classicalFDist

Hansen Theorem 5.13 in classical form: the block F statistic has the classical Fisher-Snedecor distribution under the null. This is a thin wrapper over the ratio-law result using the standalone fDist = classicalFDist bridge in FDist.lean.

Formal statement

∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {k₁ : Type u_3} {k₂ : Type u_4} [inst_2 : Fintype k₁]
  [inst_3 : DecidableEq k₁] [inst_4 : Fintype k₂] [inst_5 : DecidableEq k₂] {Ω : Type u_5} [inst_6 : MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} (X₁ : Matrix n k₁ Real) (X₂ : Matrix n k₂ Real) (β₁ : k₁ → Real) {σ2 : Real},
  Real.instLT.lt 0 σ2 →
    instLTNat.lt 0 (Fintype.card k₂) →
      instLTNat.lt (Fintype.card (Sum k₁ k₂)) (Fintype.card n) →
        ∀ (ε : Ω → EuclideanSpace Real n)
          [inst_7 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X₁.transpose X₁)]
          [inst_8 :
            Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (X₁.fromCols X₂).transpose (X₁.fromCols X₂))],
          ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
            ProbabilityTheory.HasLaw
              (fun ω => HansenEconometrics.olsFStatistic X₁ X₂ (instHAdd.hAdd (X₁.mulVec β₁) (ε ω).ofLp))
              (HansenEconometrics.classicalFDist (Fintype.card k₂)
                (instHSub.hSub (Fintype.card n) (Fintype.card (Sum k₁ k₂))))
              μ

Direct statement dependencies (2)

• HansenEconometrics.classicalFDist
• HansenEconometrics.olsFStatistic

HansenEconometrics/Chapter5LikelihoodRatioTest.lean:472

theorem HansenEconometrics.olsFStatistic_rejection_probability_eq_alpha_classical

Hansen Theorem 5.13 rejection statement in classical form.

Formal statement

∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {k₁ : Type u_3} {k₂ : Type u_4} [inst_2 : Fintype k₁]
  [inst_3 : DecidableEq k₁] [inst_4 : Fintype k₂] [inst_5 : DecidableEq k₂] {Ω : Type u_5} [inst_6 : MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} (X₁ : Matrix n k₁ Real) (X₂ : Matrix n k₂ Real) (β₁ : k₁ → Real) {σ2 α : Real}
  (c : Real),
  Eq
      ((HansenEconometrics.classicalFDist (Fintype.card k₂)
            (instHSub.hSub (Fintype.card n) (Fintype.card (Sum k₁ k₂)))).real
        (Set.Ioi c))
      α →
    Real.instLT.lt 0 σ2 →
      instLTNat.lt 0 (Fintype.card k₂) →
        instLTNat.lt (Fintype.card (Sum k₁ k₂)) (Fintype.card n) →
          ∀ (ε : Ω → EuclideanSpace Real n)
            [inst_7 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X₁.transpose X₁)]
            [inst_8 :
              Invertible
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (X₁.fromCols X₂).transpose (X₁.fromCols X₂))],
            ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
              Eq
                (μ.real
                  (setOf fun ω =>
                    Real.instLT.lt c
                      (HansenEconometrics.olsFStatistic X₁ X₂ (instHAdd.hAdd (X₁.mulVec β₁) (ε ω).ofLp))))
                α

Direct statement dependencies (2)

• HansenEconometrics.classicalFDist
• HansenEconometrics.olsFStatistic

HansenEconometrics/Chapter5LikelihoodRatioTest.lean:513