Chapter 7: Asymptotic Theory for Least Squares
This page is generated from the canonical Chapter 7 inventory and the compiled Lean environment. It contains 19 textbook result groups and 75 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.
Assumption 7.1 iid sample with finite second moments and nonsingular population Gram1 endpoint
(Y_i, X_i) i.i.d., \mathbb{E}[Y^2] \lt \infty, \mathbb{E}\lVert X\rVert^2 \lt \infty, Q_{XX} = \mathbb{E}[X X'] \succ 0
def HansenEconometrics.SampleMomentAssumption71
Compatibility name for the moment-level proof bundle behind LeastSquaresConsistencyConditions.
Formal statement
{Ω : Type u_1} →
{mΩ : MeasurableSpace Ω} →
{k : Type u_3} →
[Fintype k] →
[DecidableEq k] →
(μ : MeasureTheory.Measure Ω) →
[MeasureTheory.IsFiniteMeasure μ] → (Nat → Ω → k → Real) → (Nat → Ω → Real) → PropTheorem 7.1 consistency of least squares3 endpoints
Under Assumption 7.1, \hat{\beta} \xrightarrow{p} \beta as n \to \infty
theorem HansenEconometrics.olsBetaStar_stack_tendstoInMeasure_beta
Consistency of the totalized least-squares estimator. Under the moment-level assumptions above and the linear model yᵢ = Xᵢ·β + eᵢ, the total OLS estimator β̂*ₙ := (Xᵀ X)⁺ Xᵀ y (using Matrix.nonsingInv) converges in probability to β.
Proof chain: * F2: β̂ₙ = Q̂ₙ⁻¹ ᵥ ĝₙ(y) pointwise. * F3: ĝₙ(y) = Q̂ₙ β + ĝₙ(e) under the linear model. * F6: residual β̂ₙ − β − Q̂ₙ⁻¹ ᵥ ĝₙ(e) →ₚ 0 (it vanishes on the invertibility event, whose complement has measure → 0 by F4). * Task 11: Q̂ₙ⁻¹ ᵥ ĝₙ(e) →ₚ 0. F5 (twice): residual + error term + β →ₚ 0 + 0 + β = β. * Pointwise algebra: the sum equals β̂*ₙ.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsFiniteMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} (β : k → Real),
HansenEconometrics.LeastSquaresConsistencyConditions μ X e →
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsBetaStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => βDirect statement dependencies (4)
-
HansenEconometrics.LeastSquaresConsistencyConditions -
HansenEconometrics.olsBetaStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsBetaOrZero_stack_tendstoInMeasure_beta
Theorem 7.1 ordinary-OLS-on-nonsingular-samples consistency.
The textbook-facing wrapper olsBetaOrZero equals ordinary olsBeta whenever the sample Gram is nonsingular and equals olsBetaStar unconditionally, so the totalized consistency theorem transfers directly.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsFiniteMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} (β : k → Real),
HansenEconometrics.LeastSquaresConsistencyConditions μ X e →
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => βDirect statement dependencies (4)
-
HansenEconometrics.LeastSquaresConsistencyConditions -
HansenEconometrics.olsBetaOrZero -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsBeta_stack_tendstoInMeasure_beta_of_invertible
Theorem 7.1 for literal ordinary OLS under sample-Gram invertibility.
When every realized stacked sample Gram is invertible, the textbook olsBeta estimator is available pointwise and agrees with olsBetaOrZero, so the ordinary-wrapper consistency theorem transfers to the dependent ordinary-OLS surface.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsFiniteMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} (β : k → Real)
(hInv :
(n : Nat) →
(ω : Ω) →
Invertible
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.stackRegressors X n ω).transpose
(HansenEconometrics.stackRegressors X n ω))),
HansenEconometrics.LeastSquaresConsistencyConditions μ X e →
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsBeta (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => βDirect statement dependencies (4)
-
HansenEconometrics.LeastSquaresConsistencyConditions -
HansenEconometrics.olsBeta -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Assumption 7.2 / score CLT setup1 endpoint
The score has sufficient moments for \Omega=\mathbb E[e_i^2X_iX_i']\lt \infty and a central limit theorem.
def HansenEconometrics.SampleCLTAssumption72
Compatibility name for the CLT proof bundle behind ScoreCLTConditions.
Formal statement
{Ω : Type u_1} →
{mΩ : MeasurableSpace Ω} →
{k : Type u_4} →
[Fintype k] →
[DecidableEq k] →
(μ : MeasureTheory.Measure Ω) →
[MeasureTheory.IsProbabilityMeasure μ] → (Nat → Ω → k → Real) → (Nat → Ω → Real) → PropTheorem 7.2 score CLT bridge6 endpoints
Assumption 7.2 implies \Omega\lt \infty and n^{-1/2}\sum_{i=1}^n X_i e_i\xrightarrow{d}N(0,\Omega).
theorem HansenEconometrics.scoreProj_sampleCrossMoment_tendstoInDistribution_gaussian_cov_all
Hansen Theorem 7.2, all scalar projections with Ω.
This packages the scalar projection family used by the vector-valued Cramér-Wold theorem below: for every fixed direction a, the scalar projection of √n · ĝₙ(e) has Gaussian limit with variance a’ Ω a.
Formal statement
∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {k : Type u_3} [inst : Fintype k]
[inst_1 : DecidableEq k] {μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ]
{ν : MeasureTheory.Measure Ω'} [inst_3 : MeasureTheory.IsProbabilityMeasure ν] {X : Nat → Ω → k → Real}
{e : Nat → Ω → Real},
HansenEconometrics.SampleCLTAssumption72 μ X e →
∀ {Z : (k → Real) → Ω' → Real},
(∀ (a : k → Real),
ProbabilityTheory.HasLaw (Z a)
(ProbabilityTheory.gaussianReal 0 (dotProduct a ((HansenEconometrics.scoreCovMat μ X e).mulVec a)).toNNReal)
ν) →
∀ (a : k → Real),
MeasureTheory.TendstoInDistribution
(fun n ω =>
dotProduct
(instHSMul.hSMul n.cast.sqrt
(HansenEconometrics.sampleCrossMoment (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackErrors e n ω)))
a)
Filter.atTop (Z a) (fun x => μ) νDirect statement dependencies (5)
-
HansenEconometrics.SampleCLTAssumption72 -
HansenEconometrics.sampleCrossMoment -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackErrors -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.scoreVector_sampleCrossMoment_tendstoInDistribution_multivariateGaussian
Hansen Theorem 7.2, vector score CLT in Chapter 7 function-vector notation.
This is the public Chapter 7 score CLT: √n · ĝₙ(e) converges to the multivariate Gaussian score vector. The limit random variable is the coordinate view of the Gaussian on EuclideanSpace ℝ k, matching the rest of the chapter’s k → ℝ vector notation.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e : Nat → Ω → Real},
HansenEconometrics.ScoreCLTConditions μ X e →
MeasureTheory.TendstoInDistribution
(fun n ω =>
instHSMul.hSMul n.cast.sqrt
(HansenEconometrics.sampleCrossMoment (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackErrors e n ω)))
Filter.atTop (fun z => z.ofLp) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.scoreCovMat μ X e))Direct statement dependencies (5)
-
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.sampleCrossMoment -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackErrors -
HansenEconometrics.stackRegressors
def HansenEconometrics.scoreCovMat
Hansen’s score covariance matrix Ω := Var(e₀X₀). Under the population orthogonality condition this agrees entrywise with E[e₀² X₀ X₀’].
Formal statement
{Ω : Type u_1} →
{mΩ : MeasurableSpace Ω} →
{k : Type u_4} → MeasureTheory.Measure Ω → (Nat → Ω → k → Real) → (Nat → Ω → Real) → Matrix k k Real
theorem HansenEconometrics.scoreSecondMoment_integrable
Theorem 7.2 finite second-moment face.
Every entry of the score second-moment matrix E[(e₀X₀)_j (e₀X₀)_ℓ] is finite. This is the Lean-facing version of the textbook statement that the asymptotic covariance matrix Ω has finite entries under Assumption 7.2.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e : Nat → Ω → Real},
HansenEconometrics.SampleCLTAssumption72 μ X e →
∀ (j l : k),
MeasureTheory.Integrable
(fun ω => instHMul.hMul (instHSMul.hSMul (e 0 ω) (X 0 ω) j) (instHSMul.hSMul (e 0 ω) (X 0 ω) l)) μDirect statement dependencies (1)
-
HansenEconometrics.SampleCLTAssumption72
theorem HansenEconometrics.scoreCovMat_posSemidef
Hansen’s score covariance matrix Ω is positive semidefinite.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e : Nat → Ω → Real},
HansenEconometrics.SampleCLTAssumption72 μ X e → (HansenEconometrics.scoreCovMat μ X e).PosSemidefDirect statement dependencies (2)
-
HansenEconometrics.SampleCLTAssumption72 -
HansenEconometrics.scoreCovMat
theorem HansenEconometrics.scoreProj_variance_eq_quadraticScoreCovariance
Theorem 7.2 covariance-matrix face.
The variance of every scalar projection of the score vector is the quadratic form of Hansen’s score covariance matrix Ω. This is the matrix-language version of the scalar variance appearing in the one-dimensional CLT below.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e : Nat → Ω → Real},
HansenEconometrics.SampleCLTAssumption72 μ X e →
∀ (a : k → Real),
Eq (ProbabilityTheory.variance (fun ω => dotProduct (instHSMul.hSMul (e 0 ω) (X 0 ω)) a) μ)
(dotProduct a ((HansenEconometrics.scoreCovMat μ X e).mulVec a))Direct statement dependencies (2)
-
HansenEconometrics.SampleCLTAssumption72 -
HansenEconometrics.scoreCovMat
Theorem 7.36 endpoints
Under Assumption 7.2, \sqrt n(\hat\beta-\beta)\xrightarrow{d}N(0,Q_{XX}^{-1}\Omega Q_{XX}^{-1}).
theorem HansenEconometrics.scoreProj_olsBetaStar_tendstoInDistribution_gaussian_cov_all
Hansen Theorem 7.3, all scalar projections for totalized OLS with Ω.
For every fixed direction a, the scaled totalized OLS error has Gaussian limit with asymptotic variance ((Q⁻¹)‘a)’ Ω ((Q⁻¹)’a). This is the complete projection-family form currently available before the vector/Cramér-Wold wrapper is formalized.
Formal statement
∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {k : Type u_3} [inst : Fintype k]
[inst_1 : DecidableEq k] {μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ]
{ν : MeasureTheory.Measure Ω'} [inst_3 : MeasureTheory.IsProbabilityMeasure ν] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.ScoreCLTConditions μ X e →
∀ (β : k → Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
∀ {Z : (k → Real) → Ω' → Real},
(∀ (a : k → Real),
ProbabilityTheory.HasLaw (Z a)
(ProbabilityTheory.gaussianReal 0 (HansenEconometrics.olsProjectionAsymVar μ X e a).toNNReal) ν) →
∀ (a : k → Real),
MeasureTheory.TendstoInDistribution
(fun n ω =>
dotProduct
(instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.olsBetaStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
β))
a)
Filter.atTop (Z a) (fun x => μ) νDirect statement dependencies (5)
-
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.olsBetaStar -
HansenEconometrics.olsProjectionAsymVar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.scoreProj_olsBetaOrZero_tendstoInDistribution_gaussian_cov_all
Hansen Theorem 7.3, all scalar projections for ordinary OLS on nonsingular samples.
This is the textbook-facing projection-family form for olsBetaOrZero: for every fixed direction a, ordinary OLS on the nonsingular sample-Gram event has the same scalar Gaussian limit as the totalized estimator.
Formal statement
∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {k : Type u_3} [inst : Fintype k]
[inst_1 : DecidableEq k] {μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ]
{ν : MeasureTheory.Measure Ω'} [inst_3 : MeasureTheory.IsProbabilityMeasure ν] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.ScoreCLTConditions μ X e →
∀ (β : k → Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
∀ {Z : (k → Real) → Ω' → Real},
(∀ (a : k → Real),
ProbabilityTheory.HasLaw (Z a)
(ProbabilityTheory.gaussianReal 0 (HansenEconometrics.olsProjectionAsymVar μ X e a).toNNReal) ν) →
∀ (a : k → Real),
MeasureTheory.TendstoInDistribution
(fun n ω =>
dotProduct
(instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
β))
a)
Filter.atTop (Z a) (fun x => μ) νDirect statement dependencies (5)
-
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.olsBetaOrZero -
HansenEconometrics.olsProjectionAsymVar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsBetaStar_vector_tendstoInDistribution_multivariateGaussian
Hansen Theorem 7.3, vector asymptotic normality for totalized OLS.
Under the Chapter 7.2 scalar-projection CLT assumptions, the scaled totalized OLS estimator converges to the population-inverse transform of the Gaussian score vector. This theorem discharges the vector score CLT using the Cramér-Wold score theorem above.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.ScoreCLTConditions μ X e →
∀ (β : k → Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
MeasureTheory.TendstoInDistribution
(fun n ω =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.olsBetaStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
β))
Filter.atTop (fun z => (Matrix.inv.inv (HansenEconometrics.popGram μ X)).mulVec z.ofLp) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.scoreCovMat μ X e))Direct statement dependencies (6)
-
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.olsBetaStar -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsBetaOrZero_vector_tendstoInDistribution_multivariateGaussian
Hansen Theorem 7.3, ordinary-wrapper vector asymptotic normality.
The same non-conditional vector CLT for the textbook-facing olsBetaOrZero wrapper, using the pointwise equality with olsBetaStar.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.ScoreCLTConditions μ X e →
∀ (β : k → Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
MeasureTheory.TendstoInDistribution
(fun n ω =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
β))
Filter.atTop (fun z => (Matrix.inv.inv (HansenEconometrics.popGram μ X)).mulVec z.ofLp) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.scoreCovMat μ X e))Direct statement dependencies (6)
-
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.olsBetaOrZero -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.scoreProj_olsBeta_tendstoInDistribution_gaussian_cov_all_of_invertible
Hansen Theorem 7.3, all scalar projections for literal ordinary OLS under sample-Gram invertibility.
Formal statement
∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {k : Type u_3} [inst : Fintype k]
[inst_1 : DecidableEq k] {μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ]
{ν : MeasureTheory.Measure Ω'} [inst_3 : MeasureTheory.IsProbabilityMeasure ν] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.ScoreCLTConditions μ X e →
∀ (β : k → Real)
(hInv :
(n : Nat) →
(ω : Ω) →
Invertible
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.stackRegressors X n ω).transpose
(HansenEconometrics.stackRegressors X n ω))),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
∀ {Z : (k → Real) → Ω' → Real},
(∀ (a : k → Real),
ProbabilityTheory.HasLaw (Z a)
(ProbabilityTheory.gaussianReal 0 (HansenEconometrics.olsProjectionAsymVar μ X e a).toNNReal) ν) →
∀ (a : k → Real),
MeasureTheory.TendstoInDistribution
(fun n ω =>
dotProduct
(instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.olsBeta (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
β))
a)
Filter.atTop (Z a) (fun x => μ) νDirect statement dependencies (5)
-
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.olsBeta -
HansenEconometrics.olsProjectionAsymVar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsBeta_vector_tendstoInDistribution_multivariateGaussian_of_invertible
Hansen Theorem 7.3 for literal ordinary OLS under sample-Gram invertibility.
When every realized stacked sample Gram is invertible, the textbook olsBeta estimator is available pointwise and agrees with olsBetaOrZero, so the ordinary-wrapper vector asymptotic-normality theorem transfers to the dependent ordinary-OLS surface.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.ScoreCLTConditions μ X e →
∀ (β : k → Real)
(hInv :
(n : Nat) →
(ω : Ω) →
Invertible
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.stackRegressors X n ω).transpose
(HansenEconometrics.stackRegressors X n ω))),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
MeasureTheory.TendstoInDistribution
(fun n ω =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.olsBeta (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
β))
Filter.atTop (fun z => (Matrix.inv.inv (HansenEconometrics.popGram μ X)).mulVec z.ofLp) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.scoreCovMat μ X e))Direct statement dependencies (6)
-
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.olsBeta -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 7.45 endpoints
Under Assumption 7.1, \hat\sigma^2\xrightarrow{p}\sigma^2 and s^2\xrightarrow{p}\sigma^2.
theorem HansenEconometrics.olsSigmaSqHatStar_tendstoInMeasure_errorVariance
Theorem 7.4 residual-variance consistency.
Under the squared-error WLLN assumptions and the linear model, the totalized OLS residual average σ̂²ₙ converges in probability to σ² = E[e₀²].
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsFiniteMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.ErrorVarianceConsistencyConditions μ X e →
∀ (β : k → Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsSigmaSqHatStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.errorVariance μ eDirect statement dependencies (5)
-
HansenEconometrics.ErrorVarianceConsistencyConditions -
HansenEconometrics.errorVariance -
HansenEconometrics.olsSigmaSqHatStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsS2Star_tendstoInMeasure_errorVariance
Theorem 7.4 degrees-of-freedom variance consistency.
Under the squared-error WLLN assumptions and the linear model, the degrees-of-freedom adjusted totalized residual variance s²ₙ converges in probability to σ² = E[e₀²].
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsFiniteMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.ErrorVarianceConsistencyConditions μ X e →
∀ (β : k → Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsS2Star (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.errorVariance μ eDirect statement dependencies (5)
-
HansenEconometrics.ErrorVarianceConsistencyConditions -
HansenEconometrics.errorVariance -
HansenEconometrics.olsS2Star -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsSigmaSqHatStar_tendstoInMeasure_errorVariance_of_iidRobustFeasibleHCMomentConditions
IID joint-observation residual-variance consistency for σ̂².
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} (β : k → Real),
HansenEconometrics.IidRobustFeasibleHCMomentConditions μ X e y β →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsSigmaSqHatStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.errorVariance μ eDirect statement dependencies (5)
-
HansenEconometrics.IidRobustFeasibleHCMomentConditions -
HansenEconometrics.errorVariance -
HansenEconometrics.olsSigmaSqHatStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsS2Star_tendstoInMeasure_errorVariance_of_iidRobustFeasibleHCMomentConditions
IID joint-observation residual-variance consistency for s².
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} (β : k → Real),
HansenEconometrics.IidRobustFeasibleHCMomentConditions μ X e y β →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsS2Star (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.errorVariance μ eDirect statement dependencies (5)
-
HansenEconometrics.IidRobustFeasibleHCMomentConditions -
HansenEconometrics.errorVariance -
HansenEconometrics.olsS2Star -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
def HansenEconometrics.SampleVarianceAssumption74
Compatibility name for the variance proof bundle behind ErrorVarianceConsistencyConditions.
Formal statement
{Ω : Type u_1} →
{mΩ : MeasurableSpace Ω} →
{k : Type u_3} →
[Fintype k] →
[DecidableEq k] →
(μ : MeasureTheory.Measure Ω) →
[MeasureTheory.IsFiniteMeasure μ] → (Nat → Ω → k → Real) → (Nat → Ω → Real) → PropTheorem 7.52 endpoints
Under Assumption 7.1, the homoskedastic covariance estimator is consistent: \hat V_\beta^0\xrightarrow{p}V_\beta^0.
theorem HansenEconometrics.olsHomoCovStar_tendstoInMeasure
Hansen Theorem 7.5, totalized homoskedastic covariance consistency.
Under the variance-estimator assumptions and the linear model, the plug-in homoskedastic covariance estimator V̂⁰_β = s² Q̂⁻¹ converges in probability to V⁰_β = σ² Q⁻¹.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsFiniteMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.ErrorVarianceConsistencyConditions μ X e →
∀ (β : k → Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsHomoCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.homoAsymCov μ X eDirect statement dependencies (5)
-
HansenEconometrics.ErrorVarianceConsistencyConditions -
HansenEconometrics.homoAsymCov -
HansenEconometrics.olsHomoCovStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsHomoCovStar_tendstoInMeasure_of_iidRobustFeasibleHCMomentConditions
IID joint-observation homoskedastic covariance consistency.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} (β : k → Real),
HansenEconometrics.IidRobustFeasibleHCMomentConditions μ X e y β →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsHomoCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.homoAsymCov μ X eDirect statement dependencies (5)
-
HansenEconometrics.IidRobustFeasibleHCMomentConditions -
HansenEconometrics.homoAsymCov -
HansenEconometrics.olsHomoCovStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 7.64 endpoints
Under Assumption 7.2, \hat\Omega\xrightarrow{p}\Omega and the HC0 covariance estimator satisfies \hat V_\beta\xrightarrow{p}V_\beta.
theorem HansenEconometrics.olsHetCovStar_tendstoInMeasure_of_bddWts_components
Hansen Theorem 7.6, feasible HC0 sandwich under component measurability.
This version derives the residual HC0 middle-matrix measurability premise from component measurability of the regressors and errors, leaving only the empirical third/fourth bounded-weight hypotheses as explicit stochastic remainder controls.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.SampleHC0Assumption76 μ X e →
∀ (β : k → Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
(∀ (i : Nat), MeasureTheory.AEStronglyMeasurable (X i) μ) →
(∀ (i : Nat), MeasureTheory.AEStronglyMeasurable (e i) μ) →
(∀ (a b l : k),
HansenEconometrics.BoundedInProbability μ fun n ω =>
HansenEconometrics.sampleScoreCovCrossWeight (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackErrors e n ω) a b l) →
(∀ (a b l m : k),
HansenEconometrics.BoundedInProbability μ fun n ω =>
HansenEconometrics.sampleScoreCovQuadraticWeight (HansenEconometrics.stackRegressors X n ω) a b l
m) →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsHetCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.heteroAsymCov μ X eDirect statement dependencies (9)
-
HansenEconometrics.BoundedInProbability -
HansenEconometrics.SampleHC0Assumption76 -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.olsHetCovStar -
HansenEconometrics.sampleScoreCovCrossWeight -
HansenEconometrics.sampleScoreCovQuadraticWeight -
HansenEconometrics.stackErrors -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsHetCovStar_tendstoInMeasure_of_feasibleHCRemainderConditions
Hansen Theorem 7.6, feasible HC0 sandwich under packaged remainder conditions.
This is the chapter-facing packaged version of olsHetCovStar_tendstoInMeasure_of_bddWts_components: the linear model, component measurability, and bounded-weight residual-remainder controls are carried by FeasibleHCRemainderConditions.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.SampleHC0Assumption76 μ X e →
∀ (β : k → Real),
HansenEconometrics.FeasibleHCRemainderConditions μ X e y β →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsHetCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.heteroAsymCov μ X eDirect statement dependencies (6)
-
HansenEconometrics.FeasibleHCRemainderConditions -
HansenEconometrics.SampleHC0Assumption76 -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.olsHetCovStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsHetCovStar_tendstoInMeasure_of_robustFeasibleHCMomentConditions
Hansen Theorem 7.6, feasible HC0 sandwich under compact robust moments.
This endpoint uses the combined robust feasible-HC moment package, discharging both the robust covariance assumptions and the feasible HC0 remainder package.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} (β : k → Real),
HansenEconometrics.RobustFeasibleHCMomentConditions μ X e y β →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsHetCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.heteroAsymCov μ X eDirect statement dependencies (5)
-
HansenEconometrics.RobustFeasibleHCMomentConditions -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.olsHetCovStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.IidRobustFeasibleHCMomentConditions.toRobustFeasibleHCMomentConditions
The iid joint-observation package discharges the combined robust feasible-HC moment package used by the compact HC0–HC3 covariance and inference endpoints.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {β : k → Real},
HansenEconometrics.IidRobustFeasibleHCMomentConditions μ X e y β →
HansenEconometrics.RobustFeasibleHCMomentConditions μ X e y βDirect statement dependencies (2)
-
HansenEconometrics.IidRobustFeasibleHCMomentConditions -
HansenEconometrics.RobustFeasibleHCMomentConditions
Theorem 7.76 of 7 linked endpoints
Under Assumption 7.2, the HC1, HC2, and HC3 middle matrices and covariance estimators converge to \Omega and V_\beta.
theorem HansenEconometrics.olsHetCovHC1Star_tendstoInMeasure_of_bddWts_components
Hansen Theorem 7.7, HC1 sandwich under component measurability.
This is the HC1 analogue of olsHetCovStar_tendstoInMeasure_of_bddWts_components: component measurability supplies the feasible HC0 middle-matrix measurability needed by the HC1 assembly theorem.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.SampleHC0Assumption76 μ X e →
∀ (β : k → Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
(∀ (i : Nat), MeasureTheory.AEStronglyMeasurable (X i) μ) →
(∀ (i : Nat), MeasureTheory.AEStronglyMeasurable (e i) μ) →
(∀ (a b l : k),
HansenEconometrics.BoundedInProbability μ fun n ω =>
HansenEconometrics.sampleScoreCovCrossWeight (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackErrors e n ω) a b l) →
(∀ (a b l m : k),
HansenEconometrics.BoundedInProbability μ fun n ω =>
HansenEconometrics.sampleScoreCovQuadraticWeight (HansenEconometrics.stackRegressors X n ω) a b l
m) →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsHetCovHC1Star (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.heteroAsymCov μ X eDirect statement dependencies (9)
-
HansenEconometrics.BoundedInProbability -
HansenEconometrics.SampleHC0Assumption76 -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.olsHetCovHC1Star -
HansenEconometrics.sampleScoreCovCrossWeight -
HansenEconometrics.sampleScoreCovQuadraticWeight -
HansenEconometrics.stackErrors -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsHetCovHC2Star_tendstoInMeasure_of_feasibleHCLeverageConditions
Hansen Theorem 7.7, HC2 sandwich under packaged leverage conditions.
This is the packaged HC2 wrapper: the feasible HC0 remainder controls are bundled together with maximal leverage oₚ(1).
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.RobustCovarianceConsistencyConditions μ X e →
∀ (β : k → Real),
HansenEconometrics.FeasibleHCLeverageConditions μ X e y β →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsHetCovHC2Star (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.heteroAsymCov μ X eDirect statement dependencies (6)
-
HansenEconometrics.FeasibleHCLeverageConditions -
HansenEconometrics.RobustCovarianceConsistencyConditions -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.olsHetCovHC2Star -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsHetCovHC3Star_tendstoInMeasure_of_feasibleHCLeverageConditions
Hansen Theorem 7.7, HC3 sandwich under packaged leverage conditions.
This is the packaged HC3 wrapper: the feasible HC0 remainder controls are bundled together with maximal leverage oₚ(1).
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.RobustCovarianceConsistencyConditions μ X e →
∀ (β : k → Real),
HansenEconometrics.FeasibleHCLeverageConditions μ X e y β →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsHetCovHC3Star (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.heteroAsymCov μ X eDirect statement dependencies (6)
-
HansenEconometrics.FeasibleHCLeverageConditions -
HansenEconometrics.RobustCovarianceConsistencyConditions -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.olsHetCovHC3Star -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsHetCovHC1Star_tendstoInMeasure_of_feasibleHCRemainderConditions
Hansen Theorem 7.7, HC1 sandwich under packaged remainder conditions.
HC1 has the same probability limit as HC0 under the packaged feasible remainder conditions.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.SampleHC0Assumption76 μ X e →
∀ (β : k → Real),
HansenEconometrics.FeasibleHCRemainderConditions μ X e y β →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsHetCovHC1Star (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.heteroAsymCov μ X eDirect statement dependencies (6)
-
HansenEconometrics.FeasibleHCRemainderConditions -
HansenEconometrics.SampleHC0Assumption76 -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.olsHetCovHC1Star -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsHetCovHC1Star_tendstoInMeasure_of_robustFeasibleHCMomentConditions
Hansen Theorem 7.7, HC1 sandwich under compact robust moments.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} (β : k → Real),
HansenEconometrics.RobustFeasibleHCMomentConditions μ X e y β →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.olsHetCovHC1Star (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
Filter.atTop fun x => HansenEconometrics.heteroAsymCov μ X eDirect statement dependencies (5)
-
HansenEconometrics.RobustFeasibleHCMomentConditions -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.olsHetCovHC1Star -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.hc1FiniteSampleScale_tendsto_one
The HC1 finite-sample degrees-of-freedom multiplier n / (n - k) tends to 1.
Formal statement
∀ (k : Type u_5) [inst : Fintype k],
Filter.Tendsto (fun n => instHDiv.hDiv n.cast (instHSub.hSub n.cast (Fintype.card k).cast)) Filter.atTop (nhds 1)Theorem 7.82 endpoints
If r is continuous at \beta, then r(\hat\beta)\xrightarrow{p}r(\beta).
def HansenEconometrics.olsBetaStar
Star primitive: totalized OLS coefficient that is defined on every design matrix.
Uses Matrix.nonsingInv in place of the typeclass inverse ⅟(Xᵀ * X), so it is a genuine function with no typeclass precondition. On singular designs (Xᵀ * X)⁻¹ = 0 by definition, so olsBetaStar X y = 0; on nonsingular designs it agrees with olsBeta (see olsBetaStar_eq_olsBeta).
Role in the project architecture: - Chapters 3–5 use olsBeta (typeclass inverse) for finite-sample algebra. - Chapter 7+ use olsBetaStar as the proof engine for asymptotic results, where nonsingularity holds only a.s. and cannot be supplied as a global typeclass. - Textbook-facing statements that a reader would want to cite use olsBetaOrZero (Chapter 7), which is provably equal to olsBetaStar (see olsBetaOrZero_eq_olsBetaStar).
Formal statement
{n : Type u_1} → {k : Type u_2} → [Fintype n] → [Fintype k] → [DecidableEq k] → Matrix n k Real → (n → Real) → k → Real
def HansenEconometrics.olsBetaOrZero
OrZero primitive: textbook-facing totalization of ordinary OLS.
Branches explicitly on IsUnit (Xᵀ * X).det: - nonsingular: returns the ordinary olsBeta X y (typeclass inverse); - singular: returns 0.
This makes olsBetaOrZero suitable for textbook-facing statements that a reader would want to cite directly (e.g., consistency, asymptotic normality headlines), because the formula matches ordinary OLS on the high-probability nonsingularity event.
For proofs, the equivalent olsBetaStar (a Star primitive using Matrix.nonsingInv) is typically more convenient; the bridge olsBetaOrZero_eq_olsBetaStar (private @[simp]) connects the two. See the Star / OrZero totalization convention in AGENTS.md for the full architecture.
Formal statement
{n : Type u_1} → {k : Type u_2} → [Fintype n] → [Fintype k] → [DecidableEq k] → Matrix n k Real → (n → Real) → k → RealTheorem 7.94 endpoints
If r is differentiable at \beta with derivative R, then \sqrt n(r(\hat\beta)-r(\beta))\xrightarrow{d}N(0,R'V_\beta R).
theorem HansenEconometrics.nonlinearFunction_olsBetaStar_delta_tendstoInDistribution_gaussian
Hansen Theorem 7.9, nonlinear Delta-method wrapper for totalized OLS.
This is the Chapter 7-facing nonlinear packaging now that the Chapter 6 Delta-method/law-relabeling layer is available. If Yₙ is the scaled nonlinear statistic and it differs from the derivative image of √n(β̂*ₙ - β) by oₚ(1), then Yₙ has the named Gaussian law of that derivative image. Concrete transforms r(β̂ₙ) discharge hrem from the usual Fréchet-derivative remainder.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {q : Type u_4} [inst_3 : Fintype q] [inst_4 : DecidableEq q],
HansenEconometrics.ScoreCLTConditions μ X e →
∀ (β : k → Real) (R : Matrix q k Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
∀ {Y : Nat → Ω → EuclideanSpace Real q},
(∀ (n : Nat), AEMeasurable (Y n) μ) →
(MeasureTheory.TendstoInMeasure μ
(fun n ω =>
instHSub.hSub (Y n ω)
(ContinuousLinearMap.funLike.coe (HansenEconometrics.matrixContinuousLinearMap R)
{
ofLp :=
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.olsBetaStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
β) }))
Filter.atTop fun x => 0) →
ProbabilityTheory.HasLaw
(fun z =>
ContinuousLinearMap.funLike.coe (HansenEconometrics.matrixContinuousLinearMap R)
{ ofLp := (Matrix.inv.inv (HansenEconometrics.popGram μ X)).mulVec z.ofLp })
(ProbabilityTheory.multivariateGaussian 0
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R (HansenEconometrics.heteroAsymCov μ X e))
R.transpose))
(ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.scoreCovMat μ X e)) →
MeasureTheory.TendstoInDistribution Y Filter.atTop (fun z => z) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R (HansenEconometrics.heteroAsymCov μ X e))
R.transpose))Direct statement dependencies (8)
-
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.matrixContinuousLinearMap -
HansenEconometrics.olsBetaStar -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.nonlinearFunction_olsBetaOrZero_delta_tendstoInDistribution_gaussian
Hansen Theorem 7.9, nonlinear Delta-method wrapper for ordinary OLS.
Ordinary-wrapper version of nonlinearFunction_olsBetaStar_delta_tendstoInDistribution_gaussian.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {q : Type u_4} [inst_3 : Fintype q] [inst_4 : DecidableEq q],
HansenEconometrics.ScoreCLTConditions μ X e →
∀ (β : k → Real) (R : Matrix q k Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
∀ {Y : Nat → Ω → EuclideanSpace Real q},
(∀ (n : Nat), AEMeasurable (Y n) μ) →
(MeasureTheory.TendstoInMeasure μ
(fun n ω =>
instHSub.hSub (Y n ω)
(ContinuousLinearMap.funLike.coe (HansenEconometrics.matrixContinuousLinearMap R)
{
ofLp :=
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
β) }))
Filter.atTop fun x => 0) →
ProbabilityTheory.HasLaw
(fun z =>
ContinuousLinearMap.funLike.coe (HansenEconometrics.matrixContinuousLinearMap R)
{ ofLp := (Matrix.inv.inv (HansenEconometrics.popGram μ X)).mulVec z.ofLp })
(ProbabilityTheory.multivariateGaussian 0
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R (HansenEconometrics.heteroAsymCov μ X e))
R.transpose))
(ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.scoreCovMat μ X e)) →
MeasureTheory.TendstoInDistribution Y Filter.atTop (fun z => z) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R (HansenEconometrics.heteroAsymCov μ X e))
R.transpose))Direct statement dependencies (8)
-
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.matrixContinuousLinearMap -
HansenEconometrics.olsBetaOrZero -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
def HansenEconometrics.olsBetaStar
Star primitive: totalized OLS coefficient that is defined on every design matrix.
Uses Matrix.nonsingInv in place of the typeclass inverse ⅟(Xᵀ * X), so it is a genuine function with no typeclass precondition. On singular designs (Xᵀ * X)⁻¹ = 0 by definition, so olsBetaStar X y = 0; on nonsingular designs it agrees with olsBeta (see olsBetaStar_eq_olsBeta).
Role in the project architecture: - Chapters 3–5 use olsBeta (typeclass inverse) for finite-sample algebra. - Chapter 7+ use olsBetaStar as the proof engine for asymptotic results, where nonsingularity holds only a.s. and cannot be supplied as a global typeclass. - Textbook-facing statements that a reader would want to cite use olsBetaOrZero (Chapter 7), which is provably equal to olsBetaStar (see olsBetaOrZero_eq_olsBetaStar).
Formal statement
{n : Type u_1} → {k : Type u_2} → [Fintype n] → [Fintype k] → [DecidableEq k] → Matrix n k Real → (n → Real) → k → Real
def HansenEconometrics.olsBetaOrZero
OrZero primitive: textbook-facing totalization of ordinary OLS.
Branches explicitly on IsUnit (Xᵀ * X).det: - nonsingular: returns the ordinary olsBeta X y (typeclass inverse); - singular: returns 0.
This makes olsBetaOrZero suitable for textbook-facing statements that a reader would want to cite directly (e.g., consistency, asymptotic normality headlines), because the formula matches ordinary OLS on the high-probability nonsingularity event.
For proofs, the equivalent olsBetaStar (a Star primitive using Matrix.nonsingInv) is typically more convenient; the bridge olsBetaOrZero_eq_olsBetaStar (private @[simp]) connects the two. See the Star / OrZero totalization convention in AGENTS.md for the full architecture.
Formal statement
{n : Type u_1} → {k : Type u_2} → [Fintype n] → [Fintype k] → [DecidableEq k] → Matrix n k Real → (n → Real) → k → RealTheorem 7.100 endpoints
Under Assumptions 7.2 and 7.3, \hat V_\theta\xrightarrow{p}V_\theta=R'V_\beta R.
The canonical crosswalk does not name a compiled Lean endpoint. See the chapter inventory for the current qualification.
Theorem 7.116 endpoints
Under Assumptions 7.2–7.4, T(\theta)=(\hat\theta-\theta)/\operatorname{se}(\hat\theta)\xrightarrow{d}N(0,1).
theorem HansenEconometrics.studentizedLimit_tendstoInDistribution
Generic studentization bridge for scalar linear inference.
If a numerator has a distributional limit and the standard error converges in probability to a positive constant, then the studentized statistic has the corresponding ratio limit.
Formal statement
∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω}
[inst : MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure Ω'}
[inst_1 : MeasureTheory.IsProbabilityMeasure ν] {num se : Nat → Ω → Real} {Z : Ω' → Real} {c : Real},
Real.instLT.lt 0 c →
MeasureTheory.TendstoInDistribution num Filter.atTop Z (fun x => μ) ν →
(MeasureTheory.TendstoInMeasure μ se Filter.atTop fun x => c) →
(∀ (n : Nat), AEMeasurable (se n) μ) →
MeasureTheory.TendstoInDistribution (fun n ω => instHDiv.hDiv (num n ω) (se n ω)) Filter.atTop
(fun ω => instHDiv.hDiv (Z ω) c) (fun x => μ) ν
theorem HansenEconometrics.nonlinearScalarTStat_tendstoInDistribution
Hansen Theorem 7.11, generic nonlinear scalar t-statistic.
If the scaled scalar plug-in error has a distributional limit and the nonlinear standard error converges in probability to a positive constant, then the studentized nonlinear scalar statistic converges to the corresponding ratio limit.
Formal statement
∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω}
[inst : MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure Ω'}
[inst_1 : MeasureTheory.IsProbabilityMeasure ν] {θ : Real} {θhat se : Nat → Ω → Real} {root : Nat → Real}
{Z : Ω' → Real} {c : Real},
Real.instLT.lt 0 c →
MeasureTheory.TendstoInDistribution (fun n ω => instHMul.hMul (root n) (instHSub.hSub (θhat n ω) θ)) Filter.atTop Z
(fun x => μ) ν →
(MeasureTheory.TendstoInMeasure μ se Filter.atTop fun x => c) →
(∀ (n : Nat), AEMeasurable (se n) μ) →
MeasureTheory.TendstoInDistribution
(fun n ω => HansenEconometrics.scalarFunctionTStat (θhat n ω) θ (se n ω) (root n)) Filter.atTop
(fun ω => instHDiv.hDiv (Z ω) c) (fun x => μ) νDirect statement dependencies (1)
-
HansenEconometrics.scalarFunctionTStat
def HansenEconometrics.linearRestrictionStdError
Standard error induced by a covariance estimator for a fixed one-row restriction.
Formal statement
{k : Type u_3} → [Fintype k] → Matrix Unit k Real → Matrix k k Real → Real
def HansenEconometrics.scalarFunctionTStat
Scalar t-statistic for a generic nonlinear scalar parameter transform.
Formal statement
Real → Real → Real → Real → Real
def HansenEconometrics.olsLinearTStatStar
Scalar t-statistic for totalized OLS and an arbitrary covariance estimator.
Formal statement
{k : Type u_3} →
[Fintype k] →
[DecidableEq k] →
{n : Type u_4} →
[Fintype n] → Matrix Unit k Real → Matrix k k Real → Matrix n k Real → (n → Real) → (k → Real) → Real → Real
def HansenEconometrics.olsLinearTStatOrZero
Scalar t-statistic for ordinary-on-nonsingular OLS and an arbitrary covariance estimator.
Formal statement
{k : Type u_3} →
[Fintype k] →
[DecidableEq k] →
{n : Type u_4} →
[Fintype n] → Matrix Unit k Real → Matrix k k Real → Matrix n k Real → (n → Real) → (k → Real) → Real → RealTheorem 7.124 endpoints
For \hat C=[\hat\theta-c\,\operatorname{se}(\hat\theta),\hat\theta+c\,\operatorname{se}(\hat\theta)], \Pr(\theta\in\hat C)\to\Pr(\lvert Z\rvert\le c) with Z\sim N(0,1).
theorem HansenEconometrics.symmetricCI_coverage_of_abs_tstat_nonpos_tendsto_zero
Hansen Theorem 7.12, probabilistic symmetric confidence-interval coverage bridge.
This version removes the pointwise eventual standard-error positivity shortcut: it is enough that the nonpositive-standard-error event has probability tending to zero. The interval event and the absolute-t-statistic event can then differ only on a negligible bad set.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ]
{θ crit : Real} {θhat se : Nat → Ω → Real} {root : Nat → Real},
Filter.Eventually (fun n => Real.instLT.lt 0 (root n)) Filter.atTop →
Filter.Tendsto (fun n => MeasureTheory.Measure.instFunLike.coe μ (setOf fun ω => Real.instLE.le (se n ω) 0))
Filter.atTop (nhds 0) →
MeasureTheory.TendstoInDistribution
(fun n ω => abs (instHDiv.hDiv (instHMul.hMul (root n) (instHSub.hSub (θhat n ω) θ)) (se n ω))) Filter.atTop
(fun x => abs x) (fun x => μ) (ProbabilityTheory.gaussianReal 0 1) →
Eq
(MeasureTheory.Measure.instFunLike.coe
(MeasureTheory.Measure.map (fun x => abs x) (ProbabilityTheory.gaussianReal 0 1))
(frontier (Set.Iic crit)))
0 →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Set.instMembership.mem
(Set.Icc (instHSub.hSub (θhat n ω) (instHDiv.hDiv (instHMul.hMul crit (se n ω)) (root n)))
(instHAdd.hAdd (θhat n ω) (instHDiv.hDiv (instHMul.hMul crit (se n ω)) (root n))))
θ))
Filter.atTop
(nhds
(MeasureTheory.Measure.instFunLike.coe
(MeasureTheory.Measure.map (fun x => abs x) (ProbabilityTheory.gaussianReal 0 1)) (Set.Iic crit)))
theorem HansenEconometrics.symmetricCI_coverage_of_abs_tstat_standardNormal_se_tendsto_pos
Standard-normal confidence-interval coverage from convergence in probability of the standard error to a positive constant.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ]
{θ crit c : Real} {θhat se : Nat → Ω → Real} {root : Nat → Real},
Filter.Eventually (fun n => Real.instLT.lt 0 (root n)) Filter.atTop →
Real.instLT.lt 0 c →
(MeasureTheory.TendstoInMeasure μ se Filter.atTop fun x => c) →
MeasureTheory.TendstoInDistribution
(fun n ω => abs (instHDiv.hDiv (instHMul.hMul (root n) (instHSub.hSub (θhat n ω) θ)) (se n ω))) Filter.atTop
(fun x => abs x) (fun x => μ) (ProbabilityTheory.gaussianReal 0 1) →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Set.instMembership.mem
(Set.Icc (instHSub.hSub (θhat n ω) (instHDiv.hDiv (instHMul.hMul crit (se n ω)) (root n)))
(instHAdd.hAdd (θhat n ω) (instHDiv.hDiv (instHMul.hMul crit (se n ω)) (root n))))
θ))
Filter.atTop
(nhds
(MeasureTheory.Measure.instFunLike.coe
(MeasureTheory.Measure.map (fun x => abs x) (ProbabilityTheory.gaussianReal 0 1)) (Set.Iic crit)))
theorem HansenEconometrics.nonlinearScalarCI_coverage_of_tstat_standardNormal_se_tendsto_pos
Hansen Theorem 7.12, nonlinear scalar CI coverage from a signed t limit.
If a nonlinear scalar t-statistic has the standard-normal limit and its standard error converges to a positive constant, then the usual symmetric confidence interval has standard-normal asymptotic coverage.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ]
{θ crit c : Real} {θhat se : Nat → Ω → Real} {root : Nat → Real},
Filter.Eventually (fun n => Real.instLT.lt 0 (root n)) Filter.atTop →
Real.instLT.lt 0 c →
(MeasureTheory.TendstoInMeasure μ se Filter.atTop fun x => c) →
MeasureTheory.TendstoInDistribution
(fun n ω => HansenEconometrics.scalarFunctionTStat (θhat n ω) θ (se n ω) (root n)) Filter.atTop (fun x => x)
(fun x => μ) (ProbabilityTheory.gaussianReal 0 1) →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω => HansenEconometrics.scalarFunctionCIEvent (θhat n ω) θ (se n ω) (root n) crit))
Filter.atTop
(nhds
(MeasureTheory.Measure.instFunLike.coe
(MeasureTheory.Measure.map (fun x => abs x) (ProbabilityTheory.gaussianReal 0 1)) (Set.Iic crit)))Direct statement dependencies (2)
-
HansenEconometrics.scalarFunctionCIEvent -
HansenEconometrics.scalarFunctionTStat
def HansenEconometrics.olsLinearCIEventOrZero
Symmetric confidence-interval membership for a scalar ordinary-OLS restriction.
Formal statement
{k : Type u_3} →
[Fintype k] →
[DecidableEq k] →
{n : Type u_4} →
[Fintype n] →
Matrix Unit k Real → Matrix k k Real → Matrix n k Real → (n → Real) → (k → Real) → Real → Real → PropTheorem 7.133 endpoints
Under Assumptions 7.2–7.4, the Wald statistic satisfies W(\theta)\xrightarrow{d}\chi_r^2.
theorem HansenEconometrics.hasLaw_stdGaussian_normSq_chiSquared
The squared Euclidean norm of a Fin n-dimensional standard Gaussian vector has a χ²(n) law. This is the full-rank special case of hasLaw_quadForm_symmIdem_chiSquared with the identity quadratic form.
Formal statement
∀ {n : Nat},
instLTNat.lt 0 n →
∀ {Ω : Type u_1} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure inst.volume]
{Z : Ω → EuclideanSpace Real (Fin n)},
ProbabilityTheory.HasLaw Z (ProbabilityTheory.stdGaussian (EuclideanSpace Real (Fin n))) inst.volume →
ProbabilityTheory.HasLaw (fun ω => dotProduct (Z ω).ofLp (Z ω).ofLp) (HansenEconometrics.chiSquared n)
inst.volumeDirect statement dependencies (1)
-
HansenEconometrics.chiSquared
theorem HansenEconometrics.hasLaw_gaussian_mahalanobis_chiSquared
Random-variable form of hasLaw_multivariateGaussian_zero_mahalanobis_chiSquared.
Formal statement
∀ {n : Nat},
instLTNat.lt 0 n →
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Z : Ω → EuclideanSpace Real (Fin n)}
{V : Matrix (Fin n) (Fin n) Real},
V.PosDef →
ProbabilityTheory.HasLaw Z (ProbabilityTheory.multivariateGaussian 0 V) μ →
ProbabilityTheory.HasLaw (fun ω => dotProduct (Z ω).ofLp ((Matrix.inv.inv V).mulVec (Z ω).ofLp))
(HansenEconometrics.chiSquared n) μDirect statement dependencies (1)
-
HansenEconometrics.chiSquared
theorem HansenEconometrics.hasLaw_multivariateGaussian_zero_linearMap
A fixed matrix image of a centered multivariate Gaussian is a centered multivariate Gaussian with covariance R S Rᵀ.
Formal statement
∀ {n : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] {q : Type u_4} [inst_2 : Fintype q]
[inst_3 : DecidableEq q] {S : Matrix n n Real},
S.PosSemidef →
∀ (R : Matrix q n Real),
ProbabilityTheory.HasLaw (fun z => { ofLp := R.mulVec z.ofLp })
(ProbabilityTheory.multivariateGaussian 0
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R S)
R.transpose))
(ProbabilityTheory.multivariateGaussian 0 S)Theorem 7.146 endpoints
Under homoskedasticity, the homoskedastic Wald statistic satisfies W^0(\theta)\xrightarrow{d}\chi_r^2.
def HansenEconometrics.HomoskedasticErrorVariance
Variable-facing homoskedasticity assumption for Chapter 7.
The squared structural error has constant conditional expectation given the regressor vector: E[e₀² | X₀] = E[e₀²].
Formal statement
{Ω : Type u_1} →
{mΩ : MeasurableSpace Ω} → {k : Type u_4} → MeasureTheory.Measure Ω → (Nat → Ω → k → Real) → (Nat → Ω → Real) → Prop
theorem HansenEconometrics.scoreCovMat_eq_errorVariance_smul_popGram_homo
Homoskedasticity implies Hansen’s score-covariance identity Ω = σ²Q.
This is the variable-facing bridge used to replace public assumptions of the already-finished covariance identity.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e : Nat → Ω → Real},
HansenEconometrics.SampleCLTAssumption72 μ X e →
HansenEconometrics.SampleVarianceAssumption74 μ X e →
∀ (hX0 : Measurable (X 0)) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
HansenEconometrics.HomoskedasticErrorVariance μ X e →
Eq (HansenEconometrics.scoreCovMat μ X e)
(instHSMul.hSMul (HansenEconometrics.errorVariance μ e) (HansenEconometrics.popGram μ X))Direct statement dependencies (8)
-
HansenEconometrics.HomoskedasticErrorVariance -
HansenEconometrics.SampleCLTAssumption72 -
HansenEconometrics.SampleVarianceAssumption74 -
HansenEconometrics.conditioningSpace -
HansenEconometrics.conditioningSpace_le -
HansenEconometrics.errorVariance -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat
theorem HansenEconometrics.olsHomoLinWaldStatOrZero_tendstoInDistribution_chiSquared_one_homo
Hansen Theorem 7.14, scalar homoskedastic Wald statistic from homoskedasticity.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.ScoreCLTConditions μ X e →
HansenEconometrics.ErrorVarianceConsistencyConditions μ X e →
∀ (β : k → Real) (R : Matrix Unit k Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
(∀ (i : Nat), MeasureTheory.AEStronglyMeasurable (X i) μ) →
(∀ (i : Nat), MeasureTheory.AEStronglyMeasurable (e i) μ) →
∀ (hX0 : Measurable (X 0)) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
HansenEconometrics.HomoskedasticErrorVariance μ X e →
Real.instLT.lt 0
(HansenEconometrics.linearRestrictionStdError R (HansenEconometrics.homoAsymCov μ X e)) →
MeasureTheory.TendstoInDistribution
(fun n ω =>
HansenEconometrics.olsLinearWaldStatOrZero R
(HansenEconometrics.olsHomoCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
(HansenEconometrics.stackRegressors X n ω) (HansenEconometrics.stackOutcomes y n ω) β
n.cast.sqrt)
Filter.atTop (fun x => x) (fun x => μ) (HansenEconometrics.chiSquared 1)Direct statement dependencies (13)
-
HansenEconometrics.ErrorVarianceConsistencyConditions -
HansenEconometrics.HomoskedasticErrorVariance -
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.conditioningSpace -
HansenEconometrics.conditioningSpace_le -
HansenEconometrics.homoAsymCov -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.linearRestrictionStdError -
HansenEconometrics.olsHomoCovStar -
HansenEconometrics.olsLinearWaldStatOrZero -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.linMap_olsHomoWaldStatOrZero_tendstoInDistribution_chiSquared_homo
Hansen Theorem 7.14, multivariate homoskedastic Wald statistic from homoskedasticity.
This variable-facing wrapper derives Ω = σ²Q from constant conditional error variance given X₀, then applies the covariance-identity bridge.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {r : Nat} [inst_3 : Fact (instLTNat.lt 0 r)],
HansenEconometrics.ScoreCLTConditions μ X e →
HansenEconometrics.ErrorVarianceConsistencyConditions μ X e →
∀ (β : k → Real) (R : Matrix (Fin r) k Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
(∀ (i : Nat), MeasureTheory.AEStronglyMeasurable (X i) μ) →
(∀ (i : Nat), MeasureTheory.AEStronglyMeasurable (e i) μ) →
∀ (hX0 : Measurable (X 0)) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
HansenEconometrics.HomoskedasticErrorVariance μ X e →
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R (HansenEconometrics.homoAsymCov μ X e))
R.transpose).PosDef →
MeasureTheory.TendstoInDistribution
(fun n ω =>
dotProduct
(R.mulVec
(instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
β)))
((Matrix.inv.inv
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R
(HansenEconometrics.olsHomoCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω)))
R.transpose)).mulVec
(R.mulVec
(instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
β)))))
Filter.atTop (fun x => x) (fun x => μ) (HansenEconometrics.chiSquared r)Direct statement dependencies (12)
-
HansenEconometrics.ErrorVarianceConsistencyConditions -
HansenEconometrics.HomoskedasticErrorVariance -
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.conditioningSpace -
HansenEconometrics.conditioningSpace_le -
HansenEconometrics.homoAsymCov -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.olsBetaOrZero -
HansenEconometrics.olsHomoCovStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsHomoLinWaldStatOrZero_tendstoInDistribution_chiSquared_one_of_iidRobustFeasibleHC
IID joint-observation scalar homoskedastic Wald statistic from homoskedasticity.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} (β : k → Real) (R : Matrix Unit k Real),
HansenEconometrics.IidRobustFeasibleHCMomentConditions μ X e y β →
∀ (hX0 : Measurable (X 0)) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
HansenEconometrics.HomoskedasticErrorVariance μ X e →
Real.instLT.lt 0 (HansenEconometrics.linearRestrictionStdError R (HansenEconometrics.homoAsymCov μ X e)) →
MeasureTheory.TendstoInDistribution
(fun n ω =>
HansenEconometrics.olsLinearWaldStatOrZero R
(HansenEconometrics.olsHomoCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
(HansenEconometrics.stackRegressors X n ω) (HansenEconometrics.stackOutcomes y n ω) β n.cast.sqrt)
Filter.atTop (fun x => x) (fun x => μ) (HansenEconometrics.chiSquared 1)Direct statement dependencies (12)
-
HansenEconometrics.HomoskedasticErrorVariance -
HansenEconometrics.IidRobustFeasibleHCMomentConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.conditioningSpace -
HansenEconometrics.conditioningSpace_le -
HansenEconometrics.homoAsymCov -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.linearRestrictionStdError -
HansenEconometrics.olsHomoCovStar -
HansenEconometrics.olsLinearWaldStatOrZero -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.linMap_olsHomoWaldStatOrZero_tendstoInDistribution_chiSquared_of_iidRobustFeasibleHC
IID joint-observation multivariate homoskedastic Wald statistic from homoskedasticity.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {r : Nat} [inst_3 : Fact (instLTNat.lt 0 r)] (β : k → Real) (R : Matrix (Fin r) k Real),
HansenEconometrics.IidRobustFeasibleHCMomentConditions μ X e y β →
∀ (hX0 : Measurable (X 0)) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
HansenEconometrics.HomoskedasticErrorVariance μ X e →
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R (HansenEconometrics.homoAsymCov μ X e))
R.transpose).PosDef →
MeasureTheory.TendstoInDistribution
(fun n ω =>
dotProduct
(R.mulVec
(instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
β)))
((Matrix.inv.inv
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R
(HansenEconometrics.olsHomoCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω)))
R.transpose)).mulVec
(R.mulVec
(instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
β)))))
Filter.atTop (fun x => x) (fun x => μ) (HansenEconometrics.chiSquared r)Direct statement dependencies (11)
-
HansenEconometrics.HomoskedasticErrorVariance -
HansenEconometrics.IidRobustFeasibleHCMomentConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.conditioningSpace -
HansenEconometrics.conditioningSpace_le -
HansenEconometrics.homoAsymCov -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.olsBetaOrZero -
HansenEconometrics.olsHomoCovStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 7.156 of 8 linked endpoints
Under the stated high-moment conditions, \Pr(T\le x)=\Phi(x)+n^{-1/2}p_1(x)\phi(x)+n^{-1}p_2(x)\phi(x)+o(n^{-1}); the n^{-1/2} term cancels for symmetric intervals.
theorem HansenEconometrics.SecondOrderEdgeworthExpansion.symmetric_interval_scaled_remainder_tendsto_zero
Symmetric two-sided Edgeworth expansion consequence.
For a symmetric interval, the n^{-1/2} correction cancels when p₁ is even and the density is even, while the odd p₂ term contributes twice its positive cutoff value. This is the formal version of Hansen’s explanation after Theorem 7.15 that two-sided intervals remove the first-order Edgeworth coverage error.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ]
{T : Nat → Ω → Real} {baseCDF density p1 p2 : Real → Real},
HansenEconometrics.SecondOrderEdgeworthExpansion μ T baseCDF density p1 p2 →
∀ (c : Real),
Eq (p1 (Real.instNeg.neg c)) (p1 c) →
Eq (p2 (Real.instNeg.neg c)) (Real.instNeg.neg (p2 c)) →
Eq (density (Real.instNeg.neg c)) (density c) →
Filter.Tendsto
(fun n =>
instHMul.hMul n.cast
(instHSub.hSub
(instHSub.hSub
(instHSub.hSub (HansenEconometrics.statisticCDFReal μ T n c)
(HansenEconometrics.statisticCDFReal μ T n (Real.instNeg.neg c)))
(instHSub.hSub (baseCDF c) (baseCDF (Real.instNeg.neg c))))
(instHMul.hMul (Real.instInv.inv n.cast) (instHMul.hMul 2 (instHMul.hMul (p2 c) (density c))))))
Filter.atTop (nhds 0)Direct statement dependencies (2)
-
HansenEconometrics.SecondOrderEdgeworthExpansion -
HansenEconometrics.statisticCDFReal
def HansenEconometrics.edgeworthP1Polynomial
The even quadratic polynomial shape appearing as p₁ in Hansen’s Theorem 7.15 Edgeworth expansion. The concrete coefficients are cumulant functions of the regression moments; this definition records the textbook polynomial order and parity.
Formal statement
Real → Real → Real → Real
def HansenEconometrics.edgeworthP2Polynomial
The odd degree-five polynomial shape appearing as p₂ in Hansen’s Theorem 7.15 Edgeworth expansion.
Formal statement
Real → Real → Real → Real → Real
theorem HansenEconometrics.FirstOrderEdgeworthExpansion.scaled_remainder_tendsto_zero
First-order Edgeworth expansion, written as a vanishing scaled remainder.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ]
{T : Nat → Ω → Real} {baseCDF correction : Real → Real},
HansenEconometrics.FirstOrderEdgeworthExpansion μ T baseCDF correction →
∀ (x : Real),
Filter.Tendsto
(fun n =>
instHMul.hMul n.cast.sqrt
(instHSub.hSub (instHSub.hSub (HansenEconometrics.statisticCDFReal μ T n x) (baseCDF x))
(instHMul.hMul (Real.instInv.inv n.cast.sqrt) (correction x))))
Filter.atTop (nhds 0)Direct statement dependencies (2)
-
HansenEconometrics.FirstOrderEdgeworthExpansion -
HansenEconometrics.statisticCDFReal
theorem HansenEconometrics.SecondOrderEdgeworthExpansion.toFirstOrderEdgeworthExpansion
A second-order Edgeworth expansion implies the first-order Edgeworth interface, with correction p1(x) * density(x).
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ]
{T : Nat → Ω → Real} {baseCDF density p1 p2 : Real → Real},
HansenEconometrics.SecondOrderEdgeworthExpansion μ T baseCDF density p1 p2 →
HansenEconometrics.FirstOrderEdgeworthExpansion μ T baseCDF fun x => instHMul.hMul (p1 x) (density x)Direct statement dependencies (2)
-
HansenEconometrics.FirstOrderEdgeworthExpansion -
HansenEconometrics.SecondOrderEdgeworthExpansion
theorem HansenEconometrics.SecondOrderEdgeworthExpansion.pointwise_remainder_tendsto_zero
The unscaled second-order Edgeworth approximation error vanishes at each cutoff.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ]
{T : Nat → Ω → Real} {baseCDF density p1 p2 : Real → Real},
HansenEconometrics.SecondOrderEdgeworthExpansion μ T baseCDF density p1 p2 →
∀ (x : Real),
Filter.Tendsto
(fun n =>
instHSub.hSub
(instHSub.hSub (instHSub.hSub (HansenEconometrics.statisticCDFReal μ T n x) (baseCDF x))
(instHMul.hMul (Real.instInv.inv n.cast.sqrt) (instHMul.hMul (p1 x) (density x))))
(instHMul.hMul (Real.instInv.inv n.cast) (instHMul.hMul (p2 x) (density x))))
Filter.atTop (nhds 0)Direct statement dependencies (2)
-
HansenEconometrics.SecondOrderEdgeworthExpansion -
HansenEconometrics.statisticCDFReal
Theorem 7.166 endpoints
If \mathbb E\lVert X\rVert^r\lt \infty, then \max_{1\le i\le n}\lvert\hat e_i-e_i\rvert=o_p(n^{-1/2+1/r}).
theorem HansenEconometrics.scaledMaxResidualErrorStar_tendstoInMeasure_zero_of_scaled_product
Hansen Theorem 7.16, max residual rate packaging.
If a deterministic rate scaling sends the product of the maximal row norm and the totalized coefficient error to zero in probability, then the scaled maximum residual error is also oₚ(1). The remaining textbook-specific work is to combine this wrapper with the Chapter 6 maximum bound for the regressor row norm and the Chapter 7 OLS rate.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Nat → Ω → k → Real} {e : Nat → Ω → Real}
(β : k → Real) (scale : Nat → Real),
(∀ (n : Nat), Real.instLE.le 0 (scale n)) →
(MeasureTheory.TendstoInMeasure μ
(fun n ω =>
instHMul.hMul (scale n)
(instHMul.hMul
(instHMul.hMul (Fintype.card k).cast
(HansenEconometrics.maxRowNorm (HansenEconometrics.stackRegressors X n ω)))
(Pi.normedRing.norm
(instHSub.hSub
(HansenEconometrics.olsBetaStar (HansenEconometrics.stackRegressors X n ω)
(instHAdd.hAdd ((HansenEconometrics.stackRegressors X n ω).mulVec β)
(HansenEconometrics.stackErrors e n ω)))
β))))
Filter.atTop fun x => 0) →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
instHMul.hMul (scale n)
(HansenEconometrics.maxResidualErrorStar (HansenEconometrics.stackRegressors X n ω) β
(HansenEconometrics.stackErrors e n ω)))
Filter.atTop fun x => 0Direct statement dependencies (5)
-
HansenEconometrics.maxResidualErrorStar -
HansenEconometrics.maxRowNorm -
HansenEconometrics.olsBetaStar -
HansenEconometrics.stackErrors -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.sqrt_smul_olsBetaStar_sub_boundedInProbabilityNorm
Hansen Theorem 7.16/7.3 bridge, totalized estimator.
The vector OLS CLT implies the scaled coefficient error √n(β̂*ₙ - β) is bounded in probability. This is the coefficient-error factor needed by the max-residual product-rate proof.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.ScoreCLTConditions μ X e →
∀ (β : k → Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
HansenEconometrics.BoundedInProbabilityNorm μ fun n ω =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.olsBetaStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
β)Direct statement dependencies (5)
-
HansenEconometrics.BoundedInProbabilityNorm -
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.olsBetaStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.sqrt_scaledMaxRowNorm_sq_tendstoInMeasure_zero_of_uniformIntegrable_norm_sq
Hansen Theorem 7.16/7.17, root row-rate discharge.
Uniform integrability of squared row norms implies the root-form sqrt(n⁻¹ max_i ‖X_i‖²) = oₚ(1), the row-norm factor used in the residual uniformity rate and the unscaled leverage consequence.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] {μ : MeasureTheory.Measure Ω}
{X : Nat → Ω → k → Real},
MeasureTheory.UniformIntegrable (fun i ω => instHPow.hPow (Pi.normedRing.norm (X i ω)) 2) 1 μ →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
(instHMul.hMul (Real.instInv.inv (Fintype.card (Fin n)).cast)
(instHPow.hPow (HansenEconometrics.maxRowNorm (HansenEconometrics.stackRegressors X n ω)) 2)).sqrt)
Filter.atTop fun x => 0Direct statement dependencies (2)
-
HansenEconometrics.maxRowNorm -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.maxResidualErrorStar_tendstoInMeasure_zero_of_uniformIntegrable_rowNorm_sq
Hansen Theorem 7.16, residual uniformity rate.
Under the score CLT conditions, a correctly specified linear model, and uniform integrability of squared regressor row norms, the maximum totalized residual error is oₚ(1). The proof combines the Chapter 6 root row-norm rate with the OLS CLT’s √n(β̂*ₙ - β)=Oₚ(1) factor and the deterministic residual bound.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.ScoreCLTConditions μ X e →
∀ (β : k → Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
MeasureTheory.UniformIntegrable (fun i ω => instHPow.hPow (Pi.normedRing.norm (X i ω)) 2) 1 μ →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.maxResidualErrorStar (HansenEconometrics.stackRegressors X n ω) β
(HansenEconometrics.stackErrors e n ω))
Filter.atTop fun x => 0Direct statement dependencies (4)
-
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.maxResidualErrorStar -
HansenEconometrics.stackErrors -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.maxResidualErrorStar_tendstoInMeasure_zero_of_identDistrib_memLp_rowNorm_sq
Hansen Theorem 7.16, iid finite-row-moment residual uniformity rate.
If the squared regressor row norms are identically distributed and the first row has finite second moment, then the Chapter 6 iid UI bridge discharges the row uniform-integrability assumption in the max-residual rate theorem.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real},
HansenEconometrics.ScoreCLTConditions μ X e →
∀ (β : k → Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
MeasureTheory.MemLp (fun ω => instHPow.hPow (Pi.normedRing.norm (X 0 ω)) 2) 1 μ →
(∀ (i : Nat),
ProbabilityTheory.IdentDistrib (fun ω => instHPow.hPow (Pi.normedRing.norm (X i ω)) 2)
(fun ω => instHPow.hPow (Pi.normedRing.norm (X 0 ω)) 2) μ μ) →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.maxResidualErrorStar (HansenEconometrics.stackRegressors X n ω) β
(HansenEconometrics.stackErrors e n ω))
Filter.atTop fun x => 0Direct statement dependencies (4)
-
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.maxResidualErrorStar -
HansenEconometrics.stackErrors -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.maxResidualErrorStar_tendstoInMeasure_zero_of_iidRobustFeasibleHCMomentConditions
Hansen Theorem 7.16, iid feasible-HC package endpoint.
The unified iid robust feasible-HC package directly discharges residual uniformity through its score-CLT, model, fourth-row-moment, and row-norm identical-distribution fields.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {β : k → Real},
HansenEconometrics.IidRobustFeasibleHCMomentConditions μ X e y β →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.maxResidualErrorStar (HansenEconometrics.stackRegressors X n ω) β
(HansenEconometrics.stackErrors e n ω))
Filter.atTop fun x => 0Direct statement dependencies (4)
-
HansenEconometrics.IidRobustFeasibleHCMomentConditions -
HansenEconometrics.maxResidualErrorStar -
HansenEconometrics.stackErrors -
HansenEconometrics.stackRegressors
Theorem 7.174 endpoints
If X_i is i.i.d., Q_{XX}\succ0, and \mathbb E\lVert X\rVert^r\lt \infty for r\ge2, then \max_{1\le i\le n}h_{ii}=o_p(n^{2/r-1}).
theorem HansenEconometrics.scaledMaxLeverageStar_tendstoInMeasure_zero_of_scaled_maxRowNorm_sq
Hansen Theorem 7.17, max-leverage rate packaging.
Once the Chapter 6 maximum-row-norm rate supplies aₙ n⁻¹ max_i ‖X_i‖² = oₚ(1), sample-Gram consistency makes the inverse sample-Gram norm Oₚ(1), so aₙ max_i hᵢᵢ = oₚ(1). This is the theorem-shaped bridge from the already formalized maximum-bound layer to HC2/HC3’s maximal leverage hypothesis.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsFiniteMeasure μ] {X : Nat → Ω → k → Real}
{e : Nat → Ω → Real},
HansenEconometrics.SampleMomentAssumption71 μ X e →
∀ (scale : Nat → Real),
(∀ (n : Nat), Real.instLE.le 0 (scale n)) →
(MeasureTheory.TendstoInMeasure μ
(fun n ω =>
instHMul.hMul (scale n)
(instHMul.hMul (Real.instInv.inv (Fintype.card (Fin n)).cast)
(instHPow.hPow (HansenEconometrics.maxRowNorm (HansenEconometrics.stackRegressors X n ω)) 2)))
Filter.atTop fun x => 0) →
MeasureTheory.TendstoInMeasure μ
(fun n ω =>
instHMul.hMul (scale n) (HansenEconometrics.maxLeverageStar (HansenEconometrics.stackRegressors X n ω)))
Filter.atTop fun x => 0Direct statement dependencies (4)
-
HansenEconometrics.SampleMomentAssumption71 -
HansenEconometrics.maxLeverageStar -
HansenEconometrics.maxRowNorm -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.maxLeverageStar_tendstoInMeasure_zero_of_uniformIntegrable_rowNorm_sq
Hansen Theorem 7.17, primitive max-leverage rate.
Uniform integrability of the squared row norms gives the unscaled max_i hᵢᵢ = oₚ(1) leverage rate through the Chapter 6 maximum theorem and the sample-Gram consistency package.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsFiniteMeasure μ] {X : Nat → Ω → k → Real}
{e : Nat → Ω → Real},
HansenEconometrics.SampleMomentAssumption71 μ X e →
MeasureTheory.UniformIntegrable (fun i ω => instHPow.hPow (Pi.normedRing.norm (X i ω)) 2) 1 μ →
MeasureTheory.TendstoInMeasure μ
(fun n ω => HansenEconometrics.maxLeverageStar (HansenEconometrics.stackRegressors X n ω)) Filter.atTop fun x =>
0Direct statement dependencies (3)
-
HansenEconometrics.SampleMomentAssumption71 -
HansenEconometrics.maxLeverageStar -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.maxLeverageStar_tendstoInMeasure_zero_of_identDistrib_memLp_rowNorm_sq
Hansen Theorem 7.17, iid finite-row-moment max-leverage rate.
If the squared regressor row norms are identically distributed and the first row has finite second moment, then the uniform-integrability hypothesis in the primitive max-leverage wrapper is discharged by the Chapter 6 iid UI bridge.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsFiniteMeasure μ] {X : Nat → Ω → k → Real}
{e : Nat → Ω → Real},
HansenEconometrics.SampleMomentAssumption71 μ X e →
MeasureTheory.MemLp (fun ω => instHPow.hPow (Pi.normedRing.norm (X 0 ω)) 2) 1 μ →
(∀ (i : Nat),
ProbabilityTheory.IdentDistrib (fun ω => instHPow.hPow (Pi.normedRing.norm (X i ω)) 2)
(fun ω => instHPow.hPow (Pi.normedRing.norm (X 0 ω)) 2) μ μ) →
MeasureTheory.TendstoInMeasure μ
(fun n ω => HansenEconometrics.maxLeverageStar (HansenEconometrics.stackRegressors X n ω)) Filter.atTop
fun x => 0Direct statement dependencies (3)
-
HansenEconometrics.SampleMomentAssumption71 -
HansenEconometrics.maxLeverageStar -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.IidRobustFeasibleHCMomentConditions.maxLeverageStar_tendstoInMeasure_zero_of_iidRobustFeasibleHCMomentConditions
Hansen Theorem 7.17, iid feasible-HC package endpoint.
The unified iid robust feasible-HC package directly discharges the max-leverage rate through its fourth-row-moment field and the row-norm identical-distribution bridge above.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_4} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {β : k → Real},
HansenEconometrics.IidRobustFeasibleHCMomentConditions μ X e y β →
MeasureTheory.TendstoInMeasure μ
(fun n ω => HansenEconometrics.maxLeverageStar (HansenEconometrics.stackRegressors X n ω)) Filter.atTop fun x => 0Direct statement dependencies (3)
-
HansenEconometrics.IidRobustFeasibleHCMomentConditions -
HansenEconometrics.maxLeverageStar -
HansenEconometrics.stackRegressors