Chapter 9: Hypothesis Testing
This page is generated from the canonical Chapter 9 inventory and the compiled Lean environment. It contains 11 textbook result groups and 24 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 9.13 endpoints
Under H_0:\theta=\theta_0, T(\theta_0)\xrightarrow{d}N(0,1) and \Pr(\lvert T\rvert\gt c)\to2(1-\Phi(c)).
theorem HansenEconometrics.olsHC0LinTTest_rejectionProb_tendsto
Hansen Theorem 9.1, asymptotic-size half, for the ordinary-OLS HC0 t-test.
The two-sided HC0 t-test “reject if |T| > c” has asymptotic rejection probability equal to the absolute-standard-normal mass of (c, ∞) — that is, P[|Z| > c] = 2(1 - Φ(c)) for Z ∼ N(0, 1).
Scope and faithfulness notes: * This formalizes only claim (b) of Hansen Theorem 9.1 (the rejection-probability limit). Claim (a), T(θ₀) →d N(0, 1), is Hansen Theorem 7.11 and is reused via olsHC0LinTStatOrZero_tendstoInDistribution_standardNormal. Claim (c), “the test has asymptotic size α”, is the calibrated wrapper olsHC0LinTTest_rejectionProb_tendsto_alpha. * The hypotheses are RobustCovarianceConsistencyConditions plus the score-weight bounded-in-probability conditions. That package is documented as stronger than Hansen’s bare Assumption 7.2 (it adds iid-type conditions on the score outer products); it is the standard Chapter 7 robust-inference hypothesis stack, not a literal rendering of Assumptions 7.2/7.3. * The t-statistic is evaluated at the true coefficient vector β, so the null H₀ : θ = θ₀ holds by construction (θ₀ = R’β). The statement is therefore Theorem 9.1’s conclusion under H₀; it is not a decision rule that discriminates H₀ from an alternative.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [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) (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) μ) →
(∀ (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) →
Real.instLT.lt 0
(HansenEconometrics.linearRestrictionStdError R (HansenEconometrics.heteroAsymCov μ X e)) →
∀ (crit : Real),
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(abs
(HansenEconometrics.olsLinearTStatOrZero R
(HansenEconometrics.olsHetCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
(HansenEconometrics.stackRegressors X n ω) (HansenEconometrics.stackOutcomes y n ω) β
n.cast.sqrt))))
Filter.atTop
(nhds
(MeasureTheory.Measure.instFunLike.coe
(MeasureTheory.Measure.map (fun x => abs x) (ProbabilityTheory.gaussianReal 0 1))
(Set.Ioi crit)))Direct statement dependencies (11)
-
HansenEconometrics.BoundedInProbability -
HansenEconometrics.RobustCovarianceConsistencyConditions -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.linearRestrictionStdError -
HansenEconometrics.olsHetCovStar -
HansenEconometrics.olsLinearTStatOrZero -
HansenEconometrics.sampleScoreCovCrossWeight -
HansenEconometrics.sampleScoreCovQuadraticWeight -
HansenEconometrics.stackErrors -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsHC0LinTTest_rejectionProb_tendsto_alpha
Hansen Theorem 9.1, explicit asymptotic-size α wrapper, for the ordinary-OLS HC0 t-test.
This is the same rejection-probability conclusion as olsHC0LinTTest_rejectionProb_tendsto, with the critical value calibrated so that the absolute-standard-normal upper-tail mass is α.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [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) (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) μ) →
(∀ (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) →
Real.instLT.lt 0
(HansenEconometrics.linearRestrictionStdError R (HansenEconometrics.heteroAsymCov μ X e)) →
∀ {crit : Real} {alpha : ENNReal},
Eq
(MeasureTheory.Measure.instFunLike.coe
(MeasureTheory.Measure.map (fun x => abs x) (ProbabilityTheory.gaussianReal 0 1))
(Set.Ioi crit))
alpha →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(abs
(HansenEconometrics.olsLinearTStatOrZero R
(HansenEconometrics.olsHetCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
(HansenEconometrics.stackRegressors X n ω) (HansenEconometrics.stackOutcomes y n ω)
β n.cast.sqrt))))
Filter.atTop (nhds alpha)Direct statement dependencies (11)
-
HansenEconometrics.BoundedInProbability -
HansenEconometrics.RobustCovarianceConsistencyConditions -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.linearRestrictionStdError -
HansenEconometrics.olsHetCovStar -
HansenEconometrics.olsLinearTStatOrZero -
HansenEconometrics.sampleScoreCovCrossWeight -
HansenEconometrics.sampleScoreCovQuadraticWeight -
HansenEconometrics.stackErrors -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.olsHC0LinTStatOrZero_tendstoInDistribution_standardNormal
Hansen Theorem 7.11 for ordinary OLS, HC0 standard-normal face.
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.RobustCovarianceConsistencyConditions μ 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) μ) →
(∀ (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) →
Real.instLT.lt 0
(HansenEconometrics.linearRestrictionStdError R (HansenEconometrics.heteroAsymCov μ X e)) →
MeasureTheory.TendstoInDistribution
(fun n ω =>
HansenEconometrics.olsLinearTStatOrZero R
(HansenEconometrics.olsHetCovStar (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 => μ) (ProbabilityTheory.gaussianReal 0 1)Direct statement dependencies (11)
-
HansenEconometrics.BoundedInProbability -
HansenEconometrics.RobustCovarianceConsistencyConditions -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.linearRestrictionStdError -
HansenEconometrics.olsHetCovStar -
HansenEconometrics.olsLinearTStatOrZero -
HansenEconometrics.sampleScoreCovCrossWeight -
HansenEconometrics.sampleScoreCovQuadraticWeight -
HansenEconometrics.stackErrors -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 9.22 endpoints
Under the multivariate null, W\xrightarrow{d}\chi_q^2; a calibrated upper-tail critical value gives asymptotic size \alpha.
theorem HansenEconometrics.nonlinearOlsWaldTest_rejectionProb_tendsto_alpha_of_chapter7
Hansen Theorem 9.2, nonlinear OLS Wald test from Chapter 7.
This is the theorem-facing robust nonlinear Wald wrapper. The restriction-gap Gaussian limit is supplied by Chapter 7’s nonlinear Delta-method wrapper, and the plug-in restriction covariance is supplied by Chapter 7’s transposed nonlinear derivative covariance wrapper. The differentiability/Taylor remainder and Gaussian image-law premises are the corresponding Chapter 7 inputs, not new Chapter 9 CLT assumptions.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {r : Nat} [Fact (instLTNat.lt 0 r)],
HansenEconometrics.ScoreCLTConditions μ X e →
∀ (β : k → Real) (rfun : (k → Real) → Fin r → Real) (θ0 : Fin r → Real) (Rfun : (k → Real) → Matrix k (Fin r) Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
(∀ (n : Nat),
AEMeasurable
(fun ω =>
{
ofLp :=
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(rfun
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω)))
θ0) })
μ) →
(MeasureTheory.TendstoInMeasure μ
(fun n ω =>
instHSub.hSub
{
ofLp :=
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(rfun
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω)))
θ0) }
(ContinuousLinearMap.funLike.coe (HansenEconometrics.matrixContinuousLinearMap (Rfun β).transpose)
{
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 (Rfun β).transpose)
{ ofLp := (Matrix.inv.inv (HansenEconometrics.popGram μ X)).mulVec z.ofLp })
(ProbabilityTheory.multivariateGaussian 0
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Rfun β).transpose
(HansenEconometrics.heteroAsymCov μ X e))
(Rfun β)))
(ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.scoreCovMat μ X e)) →
ContinuousAt Rfun β →
(∀ (n : Nat),
MeasureTheory.AEStronglyMeasurable
(fun ω =>
Rfun
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω)))
μ) →
∀ {Vhat : Nat → Ω → Matrix k k Real},
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (Vhat n) μ) →
(MeasureTheory.TendstoInMeasure μ Vhat Filter.atTop fun x =>
HansenEconometrics.heteroAsymCov μ X e) →
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Rfun β).transpose
(HansenEconometrics.heteroAsymCov μ X e))
(Rfun β)).PosDef →
∀ {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared r) (Set.Ioi crit))
alpha →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.nonlinearOlsWaldStatOrZero rfun θ0
(Rfun
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω)))
(Vhat n ω) (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω) n.cast.sqrt)))
Filter.atTop (nhds alpha)Direct statement dependencies (10)
-
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.matrixContinuousLinearMap -
HansenEconometrics.nonlinearOlsWaldStatOrZero -
HansenEconometrics.olsBetaOrZero -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.linMap_olsHC0WaldTest_rejectionProb_tendsto_alpha
Hansen Theorem 9.2, robust multivariate Wald test, asymptotic-size α form.
For a linear hypothesis encoded by R, the ordinary-OLS HC0 Wald rule “reject if W > c” has rejection probability tending to α when the critical value has χ²(r) upper-tail mass α. The null is encoded by centering at the true coefficient vector β; the hypotheses reuse Chapter 7’s robust feasible HC moment package, which is stronger than Hansen’s bare Assumptions 7.2–7.4.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {r : Nat} [Fact (instLTNat.lt 0 r)] (β : k → Real) (R : Matrix (Fin r) k Real),
HansenEconometrics.RobustFeasibleHCMomentConditions μ X e y β →
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R (HansenEconometrics.heteroAsymCov μ X e))
R.transpose).PosDef →
∀ {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared r) (Set.Ioi crit)) alpha →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.linMapOlsWaldStatOrZero R
(HansenEconometrics.olsHetCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
(HansenEconometrics.stackRegressors X n ω) (HansenEconometrics.stackOutcomes y n ω) β
n.cast.sqrt)))
Filter.atTop (nhds alpha)Direct statement dependencies (7)
-
HansenEconometrics.RobustFeasibleHCMomentConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.linMapOlsWaldStatOrZero -
HansenEconometrics.olsHetCovStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 9.32 endpoints
Under homoskedasticity and the null, W^0\xrightarrow{d}\chi_q^2.
theorem HansenEconometrics.nonlinearOlsHomoWaldTest_rejectionProb_tendsto_alpha_of_chapter7
Hansen Theorem 9.3, nonlinear homoskedastic OLS Wald test from Chapter 7.
The homoskedastic statistic uses the same Chapter 7 nonlinear Delta-method limit together with Chapter 7’s homoskedastic-to-sandwich covariance bridge. The equality premise is normally provided by homoAsymCov_eq_heteroAsymCov or one of its Chapter 7 homoskedastic wrappers.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {r : Nat} [Fact (instLTNat.lt 0 r)],
HansenEconometrics.ScoreCLTConditions μ X e →
∀ (β : k → Real) (rfun : (k → Real) → Fin r → Real) (θ0 : Fin r → Real) (Rfun : (k → Real) → Matrix k (Fin r) Real),
(∀ (i : Nat) (ω : Ω), Eq (y i ω) (instHAdd.hAdd (dotProduct (X i ω) β) (e i ω))) →
(∀ (n : Nat),
AEMeasurable
(fun ω =>
{
ofLp :=
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(rfun
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω)))
θ0) })
μ) →
(MeasureTheory.TendstoInMeasure μ
(fun n ω =>
instHSub.hSub
{
ofLp :=
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(rfun
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω)))
θ0) }
(ContinuousLinearMap.funLike.coe (HansenEconometrics.matrixContinuousLinearMap (Rfun β).transpose)
{
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 (Rfun β).transpose)
{ ofLp := (Matrix.inv.inv (HansenEconometrics.popGram μ X)).mulVec z.ofLp })
(ProbabilityTheory.multivariateGaussian 0
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Rfun β).transpose
(HansenEconometrics.heteroAsymCov μ X e))
(Rfun β)))
(ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.scoreCovMat μ X e)) →
ContinuousAt Rfun β →
(∀ (n : Nat),
MeasureTheory.AEStronglyMeasurable
(fun ω =>
Rfun
(HansenEconometrics.olsBetaOrZero (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω)))
μ) →
∀ {Vhat : Nat → Ω → Matrix k k Real},
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (Vhat n) μ) →
(MeasureTheory.TendstoInMeasure μ Vhat Filter.atTop fun x =>
HansenEconometrics.homoAsymCov μ X e) →
Eq (HansenEconometrics.homoAsymCov μ X e) (HansenEconometrics.heteroAsymCov μ X e) →
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Rfun β).transpose
(HansenEconometrics.homoAsymCov μ X e))
(Rfun β)).PosDef →
∀ {crit : Real} {alpha : ENNReal},
Eq
(MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared r)
(Set.Ioi crit))
alpha →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.nonlinearOlsWaldStatOrZero rfun θ0
(Rfun
(HansenEconometrics.olsBetaOrZero
(HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω)))
(Vhat n ω) (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω) n.cast.sqrt)))
Filter.atTop (nhds alpha)Direct statement dependencies (11)
-
HansenEconometrics.ScoreCLTConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.homoAsymCov -
HansenEconometrics.matrixContinuousLinearMap -
HansenEconometrics.nonlinearOlsWaldStatOrZero -
HansenEconometrics.olsBetaOrZero -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.linMap_olsHomoWaldTest_rejectionProb_tendsto_alpha
Hansen Theorem 9.3, homoskedastic multivariate Wald test, asymptotic-size α form.
For a linear hypothesis encoded by R, the ordinary-OLS homoskedastic Wald rule “reject if W⁰ > c” has rejection probability tending to α when the critical value has χ²(r) upper-tail mass α. The statement reuses Chapter 7’s homoskedastic Wald limit and the iid robust feasible HC package used there.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {r : Nat} [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 →
∀ {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared r) (Set.Ioi crit)) alpha →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.linMapOlsWaldStatOrZero R
(HansenEconometrics.olsHomoCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
(HansenEconometrics.stackRegressors X n ω) (HansenEconometrics.stackOutcomes y n ω) β
n.cast.sqrt)))
Filter.atTop (nhds alpha)Direct statement dependencies (10)
-
HansenEconometrics.HomoskedasticErrorVariance -
HansenEconometrics.IidRobustFeasibleHCMomentConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.conditioningSpace -
HansenEconometrics.conditioningSpace_le -
HansenEconometrics.homoAsymCov -
HansenEconometrics.linMapOlsWaldStatOrZero -
HansenEconometrics.olsHomoCovStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 9.42 endpoints
Under the null, the efficient minimum-distance statistic satisfies J^*\xrightarrow{d}\chi_q^2.
theorem HansenEconometrics.emdJTest_rejectionProb_tendsto_alpha_of_chapter8
Hansen Theorem 9.4, efficient-MD nonlinear criterion test from Chapter 8.
This theorem-facing wrapper obtains the scaled unrestricted-minus-constrained estimator limit and the limiting criterion quadratic law from Chapter 8, then applies the reusable Chapter 9 criterion-test bridge.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {q : Type u_3} [inst_3 : Fintype q]
[inst_4 : DecidableEq q] [Fact (instLTNat.lt 0 (Fintype.card q))] {bhat btilde : Nat → Ω → k → Real}
{root : Nat → Real} (β : k → Real) (R : Matrix k q Real) (V : Matrix k k Real) {Vhat : Nat → Ω → Matrix k k Real},
(HansenEconometrics.ConstrainedEstimatorLinearization μ root btilde β (Matrix.inv.inv V) R fun n ω =>
instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) β)) →
HansenEconometrics.GaussianLimit μ (fun n ω => instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) β)) V →
V.PosDef →
Function.Injective R.mulVec →
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (Vhat n) μ) →
(MeasureTheory.TendstoInMeasure μ Vhat Filter.atTop fun x => V) →
∀ {crit : Real} {alpha : ENNReal},
Eq
(MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared (Fintype.card q))
(Set.Ioi crit))
alpha →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.emdJStatOrZero (Vhat n ω) (bhat n ω) (btilde n ω) (root n))))
Filter.atTop (nhds alpha)Direct statement dependencies (4)
-
HansenEconometrics.ConstrainedEstimatorLinearization -
HansenEconometrics.GaussianLimit -
HansenEconometrics.chiSquared -
HansenEconometrics.emdJStatOrZero
theorem HansenEconometrics.emdLinearJTest_rejectionProb_tendsto_alpha
Hansen Theorem 9.4, linear efficient minimum-distance test, asymptotic-size α form.
This is the linear-hypothesis slice of the efficient minimum-distance test: Hansen’s deterministic identity J* = W reduces the rejection-probability claim to the robust Wald wrapper. The general nonlinear criterion-statistic wrapper is emdJTest_rejectionProb_tendsto_alpha_of_limitLaw.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {r : Nat} [Fact (instLTNat.lt 0 r)] (β : k → Real) (R : Matrix (Fin r) k Real),
HansenEconometrics.RobustFeasibleHCMomentConditions μ X e y β →
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R (HansenEconometrics.heteroAsymCov μ X e))
R.transpose).PosDef →
∀ {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared r) (Set.Ioi crit)) alpha →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.emdLinearJStatOrZero R
(HansenEconometrics.olsHetCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
(HansenEconometrics.stackRegressors X n ω) (HansenEconometrics.stackOutcomes y n ω) β
n.cast.sqrt)))
Filter.atTop (nhds alpha)Direct statement dependencies (7)
-
HansenEconometrics.RobustFeasibleHCMomentConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.emdLinearJStatOrZero -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.olsHetCovStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 9.52 endpoints
Under homoskedasticity and the null, the homoskedastic minimum-distance statistic satisfies J^0\xrightarrow{d}\chi_q^2.
theorem HansenEconometrics.clsJTest_rejectionProb_tendsto_alpha_of_chapter8
Hansen Theorem 9.5, CLS nonlinear criterion test from Chapter 8.
This has the same formal shape as the EMD wrapper, but is named separately for Hansen’s CLS criterion surface. The constrained-estimator difference limit and criterion quadratic law are composed from Chapter 8 rather than assumed directly in Chapter 9.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {q : Type u_3} [inst_3 : Fintype q]
[inst_4 : DecidableEq q] [Fact (instLTNat.lt 0 (Fintype.card q))] {bhat btilde : Nat → Ω → k → Real}
{root : Nat → Real} (β : k → Real) (R : Matrix k q Real) (V : Matrix k k Real) {Vhat : Nat → Ω → Matrix k k Real},
(HansenEconometrics.ConstrainedEstimatorLinearization μ root btilde β (Matrix.inv.inv V) R fun n ω =>
instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) β)) →
HansenEconometrics.GaussianLimit μ (fun n ω => instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) β)) V →
V.PosDef →
Function.Injective R.mulVec →
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (Vhat n) μ) →
(MeasureTheory.TendstoInMeasure μ Vhat Filter.atTop fun x => V) →
∀ {crit : Real} {alpha : ENNReal},
Eq
(MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared (Fintype.card q))
(Set.Ioi crit))
alpha →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.clsJStatOrZero (Vhat n ω) (bhat n ω) (btilde n ω) (root n))))
Filter.atTop (nhds alpha)Direct statement dependencies (4)
-
HansenEconometrics.ConstrainedEstimatorLinearization -
HansenEconometrics.GaussianLimit -
HansenEconometrics.chiSquared -
HansenEconometrics.clsJStatOrZero
theorem HansenEconometrics.clsLinearJTest_rejectionProb_tendsto_alpha
Hansen Theorem 9.5, linear homoskedastic minimum-distance test, asymptotic-size α form.
This is the linear-hypothesis slice of the homoskedastic minimum-distance test: Hansen’s deterministic identity with the homoskedastic Wald statistic reduces the rejection-probability claim to the homoskedastic Wald wrapper. The general nonlinear criterion-statistic wrapper is clsJTest_rejectionProb_tendsto_alpha_of_limitLaw.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {r : Nat} [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 →
∀ {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared r) (Set.Ioi crit)) alpha →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.clsLinearJStatOrZero R
(HansenEconometrics.olsHomoCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
(HansenEconometrics.stackRegressors X n ω) (HansenEconometrics.stackOutcomes y n ω) β
n.cast.sqrt)))
Filter.atTop (nhds alpha)Direct statement dependencies (10)
-
HansenEconometrics.HomoskedasticErrorVariance -
HansenEconometrics.IidRobustFeasibleHCMomentConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.clsLinearJStatOrZero -
HansenEconometrics.conditioningSpace -
HansenEconometrics.conditioningSpace_le -
HansenEconometrics.homoAsymCov -
HansenEconometrics.olsHomoCovStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 9.63 endpoints
For H_0:R'\beta=\theta_0, F=W^0/q and F\xrightarrow{d}\chi_q^2/q.
theorem HansenEconometrics.linMap_olsHomoFStatOrZero_tendstoInDistribution_chiSquaredDivDegrees
Hansen Theorem 9.6, linear F statistic, asymptotic χ²(q) / q law.
For a linear hypothesis encoded by R, the homoskedastic F statistic is the homoskedastic Wald statistic divided by the number of restrictions. Therefore the Chapter 7 homoskedastic Wald limit implies the scaled chi-square limit χ²(r) / r. The hypotheses reuse Chapter 7’s iid robust feasible HC package plus homoskedasticity, which is stronger than Hansen’s bare asymptotic assumption stack.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [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 ω =>
HansenEconometrics.linMapOlsFStatOrZero 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.chiSquaredDivDegrees r)Direct statement dependencies (11)
-
HansenEconometrics.HomoskedasticErrorVariance -
HansenEconometrics.IidRobustFeasibleHCMomentConditions -
HansenEconometrics.chiSquaredDivDegrees -
HansenEconometrics.conditioningSpace -
HansenEconometrics.conditioningSpace_le -
HansenEconometrics.homoAsymCov -
HansenEconometrics.instIsProbabilityMeasureChiSquaredDivDegrees -
HansenEconometrics.linMapOlsFStatOrZero -
HansenEconometrics.olsHomoCovStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.linMap_olsHomoFTest_rejectionProb_tendsto_alpha
Hansen Theorem 9.6, linear F test, asymptotic-size α form.
If the F critical value is calibrated against the χ²(r) / r upper-tail law, then the homoskedastic OLS F-test rejection probability tends to α.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {r : Nat} [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 →
∀ {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquaredDivDegrees r) (Set.Ioi crit))
alpha →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.linMapOlsFStatOrZero R
(HansenEconometrics.olsHomoCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
(HansenEconometrics.stackRegressors X n ω) (HansenEconometrics.stackOutcomes y n ω) β
n.cast.sqrt)))
Filter.atTop (nhds alpha)Direct statement dependencies (10)
-
HansenEconometrics.HomoskedasticErrorVariance -
HansenEconometrics.IidRobustFeasibleHCMomentConditions -
HansenEconometrics.chiSquaredDivDegrees -
HansenEconometrics.conditioningSpace -
HansenEconometrics.conditioningSpace_le -
HansenEconometrics.homoAsymCov -
HansenEconometrics.linMapOlsFStatOrZero -
HansenEconometrics.olsHomoCovStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.linMapOlsFStatOrZero_eq_wald_div
Hansen’s linear-hypothesis identity F = W⁰ / q in statistic form.
Formal statement
∀ {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k] {r : Nat} {n : Type u_3} [inst_2 : Fintype n]
(R : Matrix (Fin r) k Real) (Vhat : Matrix k k Real) (X : Matrix n k Real) (y : n → Real) (β : k → Real)
(root : Real),
Eq (HansenEconometrics.linMapOlsFStatOrZero R Vhat X y β root)
(instHDiv.hDiv (HansenEconometrics.linMapOlsWaldStatOrZero R Vhat X y β root) r.cast)Direct statement dependencies (2)
-
HansenEconometrics.linMapOlsFStatOrZero -
HansenEconometrics.linMapOlsWaldStatOrZero
Theorem 9.73 endpoints
The Hausman statistic has the null limit H\xrightarrow{d}\chi_q^2; for linear restrictions, H=W.
theorem HansenEconometrics.nonlinearHausmanTest_rejectionProb_tendsto_alpha_of_chapter8
Hansen Theorem 9.7, nonlinear Hausman test from Chapter 8.
The estimator-difference limit is obtained from Chapter 8’s constrained estimator theorem; the Hausman plug-in matrix limit and limiting quadratic law are also supplied by Chapter 8. Chapter 9 only assembles the statistic and rejection-probability bridge.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {r : Nat} [Fact (instLTNat.lt 0 r)]
{bhat btilde : Nat → Ω → k → Real} {root : Nat → Real} (β : k → Real) (R : Matrix k (Fin r) Real)
(V : Matrix k k Real) {Rhat : Nat → Ω → Matrix k (Fin r) Real} {Vhat : Nat → Ω → Matrix k k Real},
(HansenEconometrics.ConstrainedEstimatorLinearization μ root btilde β (Matrix.inv.inv V) R fun n ω =>
instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) β)) →
HansenEconometrics.GaussianLimit μ (fun n ω => instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) β)) V →
V.PosDef →
Function.Injective R.mulVec →
HansenEconometrics.MatrixEstimatorConsistent μ Rhat R →
HansenEconometrics.CovarianceEstimatorConsistent μ Vhat V →
∀ {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared r) (Set.Ioi crit)) alpha →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.nonlinearHausmanStatOrZero (Rhat n ω) (Vhat n ω) (bhat n ω) (btilde n ω)
(root n))))
Filter.atTop (nhds alpha)Direct statement dependencies (6)
-
HansenEconometrics.ConstrainedEstimatorLinearization -
HansenEconometrics.CovarianceEstimatorConsistent -
HansenEconometrics.GaussianLimit -
HansenEconometrics.MatrixEstimatorConsistent -
HansenEconometrics.chiSquared -
HansenEconometrics.nonlinearHausmanStatOrZero
theorem HansenEconometrics.linMapOlsHausmanStatOrZero_eq_wald
Hansen’s linear-hypothesis Hausman/Wald identity.
Formal statement
∀ {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k] {r : Nat} {n : Type u_3} [inst_2 : Fintype n]
(R : Matrix (Fin r) k Real) (Vhat : Matrix k k Real) (X : Matrix n k Real) (y : n → Real) (β : k → Real)
(root : Real),
Eq (HansenEconometrics.linMapOlsHausmanStatOrZero R Vhat X y β root)
(HansenEconometrics.linMapOlsWaldStatOrZero R Vhat X y β root)Direct statement dependencies (2)
-
HansenEconometrics.linMapOlsHausmanStatOrZero -
HansenEconometrics.linMapOlsWaldStatOrZero
theorem HansenEconometrics.linMap_olsHC0HausmanTest_rejectionProb_tendsto_alpha
Hansen Theorem 9.7, linear Hausman/Wald equivalence slice, asymptotic-size α form.
For linear hypotheses the Hausman statistic reduces to the robust Wald statistic. This theorem records the corresponding rejection-probability conclusion. The general nonlinear statistic-level wrapper is nonlinearHausmanTest_rejectionProb_tendsto_alpha_of_matrixLimit.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {X : Nat → Ω → k → Real}
{e y : Nat → Ω → Real} {r : Nat} [Fact (instLTNat.lt 0 r)] (β : k → Real) (R : Matrix (Fin r) k Real),
HansenEconometrics.RobustFeasibleHCMomentConditions μ X e y β →
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R (HansenEconometrics.heteroAsymCov μ X e))
R.transpose).PosDef →
∀ {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared r) (Set.Ioi crit)) alpha →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.linMapOlsHausmanStatOrZero R
(HansenEconometrics.olsHetCovStar (HansenEconometrics.stackRegressors X n ω)
(HansenEconometrics.stackOutcomes y n ω))
(HansenEconometrics.stackRegressors X n ω) (HansenEconometrics.stackOutcomes y n ω) β
n.cast.sqrt)))
Filter.atTop (nhds alpha)Direct statement dependencies (7)
-
HansenEconometrics.RobustFeasibleHCMomentConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.heteroAsymCov -
HansenEconometrics.linMapOlsHausmanStatOrZero -
HansenEconometrics.olsHetCovStar -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 9.81 endpoint
Under a fixed alternative, \lvert T\rvert\xrightarrow{p}\infty, so every fixed-threshold two-sided t test is consistent.
theorem HansenEconometrics.tTest_consistent_of_abs_tstat_tendstoInProbabilityAtTop
Reusable consistency bridge for two-sided t tests.
Once the absolute t statistic diverges to +∞ in probability under a fixed alternative, every fixed two-sided rejection threshold is crossed with probability tending to one. The model-specific proof of |Tₙ| →p +∞ remains a separate premise.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
{T : Nat → Ω → Real} {crit : Real},
(∀ (n : Nat), MeasureTheory.NullMeasurableSet (setOf fun ω => Real.instLE.le (abs (T n ω)) crit) μ) →
(HansenEconometrics.TendstoInProbabilityAtTop μ fun n ω => abs (T n ω)) →
Filter.Tendsto
(fun n => MeasureTheory.Measure.instFunLike.coe μ (setOf fun ω => Real.instLT.lt crit (abs (T n ω))))
Filter.atTop (nhds 1)Direct statement dependencies (1)
-
HansenEconometrics.TendstoInProbabilityAtTop
Theorem 9.91 endpoint
Under a fixed alternative \theta=r(\beta)\ne\theta_0, W\xrightarrow{p}\infty, so every fixed-threshold Wald test is consistent.
theorem HansenEconometrics.waldTest_consistent_of_stat_tendstoInProbabilityAtTop
Reusable consistency bridge for Wald tests.
Once a Wald statistic diverges to +∞ in probability under a fixed alternative, every fixed upper-tail rejection threshold is crossed with probability tending to one. The model-specific proof of Wₙ →p +∞ remains a separate premise.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
{W : Nat → Ω → Real} {crit : Real},
(∀ (n : Nat), MeasureTheory.NullMeasurableSet (setOf fun ω => Real.instLE.le (W n ω) crit) μ) →
HansenEconometrics.TendstoInProbabilityAtTop μ W →
Filter.Tendsto (fun n => MeasureTheory.Measure.instFunLike.coe μ (setOf fun ω => Real.instLT.lt crit (W n ω)))
Filter.atTop (nhds 1)Direct statement dependencies (1)
-
HansenEconometrics.TendstoInProbabilityAtTop
Theorem 9.102 endpoints
Under \theta_n=\theta_0+n^{-1/2}h, the t statistic has a shifted-normal limit T_n\xrightarrow{d}N(h/\sigma_\theta,1).
theorem HansenEconometrics.tTest_localPower_tendsto_of_tstat_shiftedNormal
Reusable local-power bridge from a shifted-normal t limit.
If the t statistic converges to N(δ, 1) under a local alternative, then the two-sided rejection probability converges to P(|N(δ,1)| > c). In Hansen’s notation, the shift δ is the local-alternative drift determined by h and the asymptotic variance.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ]
{T : Nat → Ω → Real} {crit delta : Real},
MeasureTheory.TendstoInDistribution T Filter.atTop (fun x => x) (fun x => μ)
(ProbabilityTheory.gaussianReal delta 1) →
Filter.Tendsto (fun n => MeasureTheory.Measure.instFunLike.coe μ (setOf fun ω => Real.instLT.lt crit (abs (T n ω))))
Filter.atTop
(nhds
(MeasureTheory.Measure.instFunLike.coe
(MeasureTheory.Measure.map (fun x => abs x) (ProbabilityTheory.gaussianReal delta 1)) (Set.Ioi crit)))
theorem HansenEconometrics.tTest_oneSidedLocalPower_tendsto_of_tstat_shiftedNormal
Reusable one-sided local-power bridge from a shifted-normal t limit.
If the t statistic converges to N(δ, 1) under a local alternative, then the one-sided rejection probability for {Tₙ > c} converges to the shifted-normal upper-tail probability.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ]
{T : Nat → Ω → Real} {crit delta : Real},
MeasureTheory.TendstoInDistribution T Filter.atTop (fun x => x) (fun x => μ)
(ProbabilityTheory.gaussianReal delta 1) →
Filter.Tendsto (fun n => MeasureTheory.Measure.instFunLike.coe μ (setOf fun ω => Real.instLT.lt crit (T n ω)))
Filter.atTop
(nhds (MeasureTheory.Measure.instFunLike.coe (ProbabilityTheory.gaussianReal delta 1) (Set.Ioi crit)))Theorem 9.113 endpoints
Under \theta_n=\theta_0+n^{-1/2}h, the Wald statistic has a noncentral chi-square limit W_n\xrightarrow{d}\chi_q^2(\lambda) with \lambda=h'V_\theta^{-1}h.
theorem HansenEconometrics.restrictionWaldStatOrZero_tendstoInDistribution_noncentralChiSquared
Local-alternative Wald statistic theorem with a named noncentral chi-square limit.
If the scaled restriction gap converges to N(mean, Vtheta) and the plug-in restriction covariance consistently estimates Vtheta, then Hansen’s Wald quadratic form converges to the noncentral chi-square law with noncentrality mean’ Vtheta⁻¹ mean.
Formal statement
∀ {Ω : Type u_3} {Ω' : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω}
[inst_2 : MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure Ω'}
[inst_3 : MeasureTheory.IsProbabilityMeasure ν] {r : Nat} {T : Nat → Ω → Fin r → Real}
{Z : Ω' → EuclideanSpace Real (Fin r)} {VthetaHat : Nat → Ω → Matrix (Fin r) (Fin r) Real}
{Vtheta : Matrix (Fin r) (Fin r) Real} {mean : Fin r → Real},
MeasureTheory.TendstoInDistribution T Filter.atTop (fun ω i => (Z ω).ofLp i) (fun x => μ) ν →
ProbabilityTheory.HasLaw Z (ProbabilityTheory.multivariateGaussian { ofLp := mean } Vtheta) ν →
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (VthetaHat n) μ) →
(MeasureTheory.TendstoInMeasure μ VthetaHat Filter.atTop fun x => Vtheta) →
IsUnit Vtheta.det →
MeasureTheory.TendstoInDistribution
(fun n ω => HansenEconometrics.restrictionWaldStatOrZero (T n ω) (VthetaHat n ω)) Filter.atTop
(fun x => x) (fun x => μ) (HansenEconometrics.noncentralChiSquared r mean Vtheta)Direct statement dependencies (3)
-
HansenEconometrics.instIsProbabilityMeasureNoncentralChiSquared -
HansenEconometrics.noncentralChiSquared -
HansenEconometrics.restrictionWaldStatOrZero
theorem HansenEconometrics.waldTest_localPower_tendsto_noncentralChiSquared
Reusable local-power bridge for the named noncentral chi-square law.
Once the local-alternative Wald statistic has the noncentral chi-square limit given by restrictionWaldStatOrZero_tendstoInDistribution_noncentralChiSquared, the upper-tail rejection probability converges to the corresponding noncentral chi-square tail probability. The frontier-null premise is the only analytic regularity fact needed to apply the portmanteau rejection-set bridge.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ]
{W : Nat → Ω → Real} {r : Nat} {mean : Fin r → Real} {V : Matrix (Fin r) (Fin r) Real} {crit : Real},
Eq
(MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.noncentralChiSquared r mean V)
(frontier (Set.Ioi crit)))
0 →
MeasureTheory.TendstoInDistribution W Filter.atTop (fun x => x) (fun x => μ)
(HansenEconometrics.noncentralChiSquared r mean V) →
Filter.Tendsto (fun n => MeasureTheory.Measure.instFunLike.coe μ (setOf fun ω => Real.instLT.lt crit (W n ω)))
Filter.atTop
(nhds (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.noncentralChiSquared r mean V) (Set.Ioi crit)))Direct statement dependencies (2)
-
HansenEconometrics.instIsProbabilityMeasureNoncentralChiSquared -
HansenEconometrics.noncentralChiSquared
def HansenEconometrics.noncentralChiSquared
Noncentral chi-square law induced by a shifted Gaussian Wald quadratic form.
For Hansen’s local Wald theorem this is the law of Z’ V⁻¹ Z when Z ∼ N(mean, V). Its noncentrality parameter is mean’ V⁻¹ mean, exposed separately by noncentralityParam.
Formal statement
(q : Nat) → (Fin q → Real) → Matrix (Fin q) (Fin q) Real → MeasureTheory.Measure Real