Chapter 12: Instrumental Variables
Foldable textbook-to-Lean result crosswalk for Chapter 12.
This page is generated from the canonical Chapter 12 inventory and the compiled Lean environment. It contains 19 textbook result groups and 21 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 12.11 endpoint
Under Assumption 12.1, the 2SLS estimator is consistent: \hat\beta_{\mathrm{2SLS}} \xrightarrow{p} \beta.
theorem HansenEconometrics.twoSLSBetaOrZero_tendstoInMeasure_beta_of_textbook12_1_joint_iid_second
Textbook-facing OrZero version of Hansen Theorem 12.1 from the literal observed-row iid finite-second-moment surface.
Formal statement
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
[inst_1 : MeasureTheory.IsProbabilityMeasure μ] {k : Type u_2} {l : Type u_3} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : DecidableEq k] [inst_5 : DecidableEq l] {Z : Nat → Ω → l → Real}
{X : Nat → Ω → k → Real} {e Y : Nat → Ω → Real} {β0 : k → Real},
HansenEconometrics.TwoSLSObservedIidSecondMomentRankConditions μ Z X e Y β0 →
MeasureTheory.TendstoInMeasure μ
(fun t ω => HansenEconometrics.twoSLSBetaOrZero (fun i => Z i.val ω) (fun i => X i.val ω) fun i => Y i.val ω)
Filter.atTop fun x => β0Direct statement dependencies (2)
-
HansenEconometrics.TwoSLSObservedIidSecondMomentRankConditions -
HansenEconometrics.twoSLSBetaOrZero
Theorem 12.21 endpoint
Under Assumption 12.2, \sqrt n(\hat\beta_{\mathrm{2SLS}}-\beta) \xrightarrow{d} N(0,V_\beta), where V_\beta=Q^{-1}Q_{XZ}Q_{ZZ}^{-1}\Omega Q_{ZZ}^{-1}Q_{ZX}Q^{-1} and Q=Q_{XZ}Q_{ZZ}^{-1}Q_{ZX}.
theorem HansenEconometrics.twoSLSBetaOrZero_tendstoInDistribution_formula_of_textbook12_2_observed_iid_fourth
Textbook-facing OrZero endpoint for Hansen Theorem 12.2 from the literal observed-row finite-fourth-moment version of Assumption 12.2.
Formal statement
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
[inst_1 : MeasureTheory.IsProbabilityMeasure μ] {k : Type u_2} {l : Type u_3} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : DecidableEq k] [inst_5 : DecidableEq l] {Z : Nat → Ω → l → Real}
{X : Nat → Ω → k → Real} {e Y : Nat → Ω → Real} {β0 : k → Real},
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions μ Z X e Y β0 →
MeasureTheory.TendstoInDistribution
(fun t ω =>
instHSMul.hSMul t.cast.sqrt
(instHSub.hSub
(HansenEconometrics.twoSLSBetaOrZero (fun i => Z i.val ω) (fun i => X i.val ω) fun i => Y i.val ω) β0))
Filter.atTop (fun z => z.ofLp) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.twoSLSAsymptoticVariance
(HansenEconometrics.twoSLSCombinedQXZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.twoSLSCombinedQZZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.scoreCovMat μ Z e)
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))))Direct statement dependencies (9)
-
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.twoSLSAsymptoticVariance -
HansenEconometrics.twoSLSBetaOrZero -
HansenEconometrics.twoSLSCombinedQXZ -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedQZZ -
HansenEconometrics.twoSLSCombinedRegressors
Theorem 12.31 endpoint
Under Assumption 12.2, the robust and homoskedastic covariance estimators are consistent: \hat V_\beta\xrightarrow{p}V_\beta and \hat V_\beta^{0}\xrightarrow{p}V_\beta^{0}.
theorem HansenEconometrics.twoSLSCovariances_tendstoInMeasure_formula_of_textbook12_2_observed_iid_fourth
Hansen Theorem 12.3 formula-facing endpoint from the literal observed-row finite-fourth-moment version of Assumption 12.2.
Formal statement
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
[inst_1 : MeasureTheory.IsProbabilityMeasure μ] {k : Type u_2} {l : Type u_3} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : DecidableEq k] [inst_5 : DecidableEq l] {Z : Nat → Ω → l → Real}
{X : Nat → Ω → k → Real} {e Y : Nat → Ω → Real} {β0 : k → Real},
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions μ Z X e Y β0 →
And
(MeasureTheory.TendstoInMeasure μ
(fun n ω => HansenEconometrics.twoSLSVHatStar (fun i => Z i.val ω) (fun i => X i.val ω) fun i => Y i.val ω)
Filter.atTop fun x =>
HansenEconometrics.twoSLSAsymptoticVariance
(HansenEconometrics.twoSLSCombinedQXZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.twoSLSCombinedQZZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.scoreCovMat μ Z e)
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X))))
(MeasureTheory.TendstoInMeasure μ
(fun n ω =>
HansenEconometrics.twoSLSHomoskedasticVHatStar (fun i => Z i.val ω) (fun i => X i.val ω) fun i => Y i.val ω)
Filter.atTop fun x =>
HansenEconometrics.twoSLSHomoskedasticAsymptoticVariance
(HansenEconometrics.twoSLSCombinedQXZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.twoSLSCombinedQZZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.errorVariance μ e))Direct statement dependencies (12)
-
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.errorVariance -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.twoSLSAsymptoticVariance -
HansenEconometrics.twoSLSCombinedQXZ -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedQZZ -
HansenEconometrics.twoSLSCombinedRegressors -
HansenEconometrics.twoSLSHomoskedasticAsymptoticVariance -
HansenEconometrics.twoSLSHomoskedasticVHatStar -
HansenEconometrics.twoSLSVHatStar
Theorem 12.41 endpoint
If \theta=h(\beta) satisfies Assumption 7.3, then \hat\theta_{\mathrm{2SLS}}=h(\hat\beta_{\mathrm{2SLS}})\xrightarrow{p}\theta.
theorem HansenEconometrics.twoSLSFunctionEstimatorOrZero_tendstoInMeasure_of_textbook12_1_joint_iid_second_73
Hansen Theorem 12.4 OrZero endpoint from the literal observed-row finite second-moment Assumption 12.1 package and Assumption 7.3 smoothness.
This is the canonical textbook-facing endpoint and has no assumptions beyond the two Hansen packages.
Formal statement
∀ {k : Type u_2} {l : Type u_3} {q : Type u_4} [inst : Fintype k] [inst_1 : Fintype l] [inst_2 : Fintype q]
[inst_3 : DecidableEq k] [inst_4 : DecidableEq l] {Ω : Type u_5} [inst_5 : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω} [inst_6 : MeasureTheory.IsProbabilityMeasure μ] {rfun : (k → Real) → q → Real}
{Z : Nat → Ω → l → Real} {X : Nat → Ω → k → Real} {e Y : Nat → Ω → Real} {β0 : k → Real} {R : Matrix k q Real},
HansenEconometrics.TwoSLSObservedIidSecondMomentRankConditions μ Z X e Y β0 →
∀ (h73 : HansenEconometrics.SmoothFunctionCondition rfun β0 R),
MeasureTheory.TendstoInMeasure μ
(fun t ω =>
HansenEconometrics.twoSLSFunctionEstimatorOrZero rfun (fun i => Z i.val ω) (fun i => X i.val ω) fun i =>
Y i.val ω)
Filter.atTop fun x => rfun β0Direct statement dependencies (3)
-
HansenEconometrics.SmoothFunctionCondition -
HansenEconometrics.TwoSLSObservedIidSecondMomentRankConditions -
HansenEconometrics.twoSLSFunctionEstimatorOrZero
Theorem 12.51 endpoint
Under Assumptions 12.2 and 7.3, \sqrt n(\hat\theta_{\mathrm{2SLS}}-\theta)\xrightarrow{d}N(0,V_\theta), and the plug-in estimator satisfies \hat V_\theta\xrightarrow{p}V_\theta.
theorem HansenEconometrics.twoSLSFunction_theorem12_5_of_textbook12_2_observed_iid_73_derivativePlugIn
Hansen Theorem 12.5, literal observed-row iid Assumption 12.2 plus Assumption 7.3 with Hansen’s plug-in derivative estimator.
Formal statement
∀ {k : Type u_2} {l : Type u_3} {q : Type u_4} [inst : Fintype k] [inst_1 : Fintype l] [inst_2 : Fintype q]
[inst_3 : DecidableEq k] [inst_4 : DecidableEq l] {Ω : Type u_5} [inst_5 : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω} [inst_6 : MeasureTheory.IsProbabilityMeasure μ] [inst_7 : DecidableEq q]
{rfun : (k → Real) → q → Real} {Z : Nat → Ω → l → Real} {X : Nat → Ω → k → Real} {e Y : Nat → Ω → Real}
{β0 : k → Real} {R : Matrix k q Real} {Rfun : (k → Real) → Matrix k q Real},
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions μ Z X e Y β0 →
∀ (h73 : HansenEconometrics.SmoothFunctionPlugInDerivativeConditions rfun β0 R Rfun),
And
(MeasureTheory.TendstoInDistribution
(fun t ω =>
{
ofLp :=
instHSMul.hSMul t.cast.sqrt
(instHSub.hSub
(HansenEconometrics.twoSLSFunctionEstimatorOrZero rfun (fun i => Z i.val ω) (fun i => X i.val ω)
fun i => Y i.val ω)
(rfun β0)) })
Filter.atTop (fun z => z) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.twoSLSFunctionVariance
(HansenEconometrics.twoSLSAsymptoticVariance
(HansenEconometrics.twoSLSCombinedQXZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.twoSLSCombinedQZZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.scoreCovMat μ Z e)
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X))))
R)))
(MeasureTheory.TendstoInMeasure μ
(fun t ω =>
HansenEconometrics.twoSLSFunctionVHat
(HansenEconometrics.twoSLSVHatStar (fun i => Z i.val ω) (fun i => X i.val ω) fun i => Y i.val ω)
(Rfun (HansenEconometrics.twoSLSBetaOrZero (fun i => Z i.val ω) (fun i => X i.val ω) fun i => Y i.val ω)))
Filter.atTop fun x =>
HansenEconometrics.twoSLSFunctionVariance
(HansenEconometrics.twoSLSAsymptoticVariance
(HansenEconometrics.twoSLSCombinedQXZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.twoSLSCombinedQZZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.scoreCovMat μ Z e)
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X))))
R)Direct statement dependencies (14)
-
HansenEconometrics.SmoothFunctionPlugInDerivativeConditions -
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.twoSLSAsymptoticVariance -
HansenEconometrics.twoSLSBetaOrZero -
HansenEconometrics.twoSLSCombinedQXZ -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedQZZ -
HansenEconometrics.twoSLSCombinedRegressors -
HansenEconometrics.twoSLSFunctionEstimatorOrZero -
HansenEconometrics.twoSLSFunctionVHat -
HansenEconometrics.twoSLSFunctionVariance -
HansenEconometrics.twoSLSVHatStar
Theorem 12.61 endpoint
Under the null and Assumptions 12.2 and 7.3, the Wald statistic satisfies W(\theta)\xrightarrow{d}\chi_q^2.
theorem HansenEconometrics.twoSLSFunctionWald_theorem12_6_of_textbook12_2_observed_iid_73_derivativePlugIn
Hansen Theorem 12.6, literal observed-row iid Assumption 12.2 plus Assumption 7.3 with Hansen’s plug-in derivative estimator.
Formal statement
∀ {k : Type u_2} {l : Type u_3} [inst : Fintype k] [inst_1 : Fintype l] [inst_2 : DecidableEq k]
[inst_3 : DecidableEq l] {Ω : Type u_5} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
[inst_5 : MeasureTheory.IsProbabilityMeasure μ] {r : Nat} [inst_6 : Fact (instLTNat.lt 0 r)]
{rfun : (k → Real) → Fin r → Real} {θ0 : Fin r → Real} {Z : Nat → Ω → l → Real} {X : Nat → Ω → k → Real}
{e Y : Nat → Ω → Real} {β0 : k → Real} {R : Matrix k (Fin r) Real} {Rfun : (k → Real) → Matrix k (Fin r) Real},
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions μ Z X e Y β0 →
∀ (h73 : HansenEconometrics.SmoothFunctionPlugInDerivativeConditions rfun β0 R Rfun),
Eq (rfun β0) θ0 →
∀ {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared r) (Set.Ioi crit)) alpha →
And
(MeasureTheory.TendstoInDistribution
(fun t ω =>
HansenEconometrics.twoSLSFunctionWaldStatOrZero rfun θ0
(Rfun
(HansenEconometrics.twoSLSBetaOrZero (fun i => Z i.val ω) (fun i => X i.val ω) fun i =>
Y i.val ω))
(HansenEconometrics.twoSLSVHatStar (fun i => Z i.val ω) (fun i => X i.val ω) fun i => Y i.val ω)
(fun i => Z i.val ω) (fun i => X i.val ω) (fun i => Y i.val ω) t.cast.sqrt)
Filter.atTop (fun x => x) (fun x => μ) (HansenEconometrics.chiSquared r))
(Filter.Tendsto
(fun t =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.twoSLSFunctionWaldStatOrZero rfun θ0
(Rfun
(HansenEconometrics.twoSLSBetaOrZero (fun i => Z i.val ω) (fun i => X i.val ω) fun i =>
Y i.val ω))
(HansenEconometrics.twoSLSVHatStar (fun i => Z i.val ω) (fun i => X i.val ω) fun i =>
Y i.val ω)
(fun i => Z i.val ω) (fun i => X i.val ω) (fun i => Y i.val ω) t.cast.sqrt)))
Filter.atTop (nhds alpha))Direct statement dependencies (7)
-
HansenEconometrics.SmoothFunctionPlugInDerivativeConditions -
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.twoSLSBetaOrZero -
HansenEconometrics.twoSLSFunctionWaldStatOrZero -
HansenEconometrics.twoSLSVHatStar
Theorem 12.71 endpoint
Corrected Kinal statement: under the stated central-Wishart, Gaussian-direction, independence, and rank conditions, \mathbb E\lVert\hat\beta_{\mathrm{2SLS},2}\rVert^r\lt \infty \Longleftrightarrow r\lt \ell_2-k_2+1. Hansen’s printed joint-normal hypothesis alone is insufficient.
theorem HansenEconometrics.KinalSupport.twoSLSKinal_theorem12_7_of_centralWishart_normalizedGaussianVector_of_rank_ae
Strongest vector-valued central-Wishart Kinal threshold.
Only one normalized-direction coordinate must have positive variance. The remaining zero-variance coordinates are constants and hence have every finite moment. The residualized fitted-endogenous rank event is derived from the central-Wishart law; the remaining rank events and instrument-count inequality are the deterministic premises used by the proof.
Formal statement
∀ {n : Type u_1} {k₁ : Type u_2} {k₂ : Type u_3} {l₂ : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n]
[inst_2 : Fintype k₁] [inst_3 : DecidableEq k₁] [inst_4 : Fintype k₂] [inst_5 : DecidableEq k₂] [inst_6 : Fintype l₂]
[inst_7 : DecidableEq l₂] {Ω : Type u_5} [inst_8 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
{X₁ : Ω → Matrix n k₁ Real} {Y₂ : Ω → Matrix n k₂ Real} {Z₂ : Ω → Matrix n l₂ Real} {Y₁ : Ω → n → Real}
{β₂ : k₂ → Real} {Sigma : Matrix k₂ k₂ Real} {directionVar : k₂ → NNReal},
instLENat.le (Fintype.card k₂) (Fintype.card l₂) →
Filter.Eventually
(fun ω =>
IsUnit
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul ((X₁ ω).fromCols (Z₂ ω)).transpose
((X₁ ω).fromCols (Z₂ ω))).det)
(MeasureTheory.ae μ) →
Filter.Eventually
(fun ω =>
IsUnit
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
((HansenEconometrics.KinalSupport.twoSLSFittedIncludedRegressorsStar (X₁ ω) (Y₂ ω) (Z₂ ω)).fromCols
(HansenEconometrics.KinalSupport.twoSLSFittedEndogenousRegressorsStar (X₁ ω) (Y₂ ω)
(Z₂ ω))).transpose
((HansenEconometrics.KinalSupport.twoSLSFittedIncludedRegressorsStar (X₁ ω) (Y₂ ω) (Z₂ ω)).fromCols
(HansenEconometrics.KinalSupport.twoSLSFittedEndogenousRegressorsStar (X₁ ω) (Y₂ ω) (Z₂ ω)))).det)
(MeasureTheory.ae μ) →
Filter.Eventually
(fun ω =>
IsUnit
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(HansenEconometrics.KinalSupport.twoSLSFittedIncludedRegressorsStar (X₁ ω) (Y₂ ω) (Z₂ ω)).transpose
(HansenEconometrics.KinalSupport.twoSLSFittedIncludedRegressorsStar (X₁ ω) (Y₂ ω) (Z₂ ω))).det)
(MeasureTheory.ae μ) →
(Exists fun j => NNReal.instPartialOrder.lt 0 (directionVar j)) →
HansenEconometrics.KinalSupport.TwoSLSKinalNormalizedCoefficientGaussianVectorInputs μ X₁ Y₂ Z₂ Y₁ β₂ Sigma
directionVar →
∀ (r : NNReal),
Iff
(MeasureTheory.MemLp
(fun ω => HansenEconometrics.twoSLSEndogenousBetaOrZero (X₁ ω) (Y₂ ω) (Z₂ ω) (Y₁ ω))
(ENNReal.ofNNReal r) μ)
(Real.instLT.lt r.toReal
(instHAdd.hAdd (instHSub.hSub (Fintype.card l₂).cast (Fintype.card k₂).cast) 1))Direct statement dependencies (4)
-
HansenEconometrics.KinalSupport.TwoSLSKinalNormalizedCoefficientGaussianVectorInputs -
HansenEconometrics.KinalSupport.twoSLSFittedEndogenousRegressorsStar -
HansenEconometrics.KinalSupport.twoSLSFittedIncludedRegressorsStar -
HansenEconometrics.twoSLSEndogenousBetaOrZero
Theorem 12.81 endpoint
Under Assumption 12.2, the pairs bootstrap reproduces the coefficient law and the robust studentized law: \sqrt n(\hat\beta^{*}_{\mathrm{2SLS}}-\hat\beta_{\mathrm{2SLS}})\xrightarrow{d^{*}}N(0,V_\beta) and T^{*}\xrightarrow{d^{*}}N(0,1).
theorem HansenEconometrics.TwoSLSBootstrapTheorem12_8.distribution_of_observed_textbook_fourth
Hansen-facing Theorem 12.8 distribution result from observed textbook Assumption 12.2 and a nonzero one-row restriction.
Both the bootstrap coefficient limit and the studentized robust one-row limit are conclusions; coefficient linearization and robust covariance resampling are derived internally from the observed fourth-moment assumptions.
Formal statement
∀ {Ω : Type u_1} {k : Type u_2} {l : Type u_3} [inst : Fintype k] [inst_1 : Fintype l] [inst_2 : DecidableEq k]
[inst_3 : DecidableEq l] [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
[inst_5 : MeasureTheory.IsProbabilityMeasure μ] {Z : Nat → Ω → l → Real} {X : Nat → Ω → k → Real}
{e Y : Nat → Ω → Real} {R : Matrix Unit k Real} {β : k → Real},
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions μ Z X e Y β →
(Exists fun j => Ne (R Unit.unit j) 0) →
And
(HansenEconometrics.TendstoInBootstrapDistributionIndexed μ
HansenEconometrics.twoSLSBootstrapUniformPstarFinSucc
(fun n ω ωs => HansenEconometrics.twoSLSBootstrapBetaGapFinSucc Z X Y n ω ωs)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.twoSLSAsymptoticVariance
(HansenEconometrics.twoSLSCombinedQXZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.twoSLSCombinedQZZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.scoreCovMat μ Z e)
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))))
fun z => z.ofLp)
(HansenEconometrics.TendstoInBootstrapDistributionIndexed μ
HansenEconometrics.twoSLSBootstrapUniformPstarFinSucc
(fun n ω ωs x => HansenEconometrics.twoSLSBootstrapRobustLinearTStatFinSucc R Z X Y n ω ωs)
(ProbabilityTheory.gaussianReal 0 1) fun z x => z)Direct statement dependencies (12)
-
HansenEconometrics.TendstoInBootstrapDistributionIndexed -
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.twoSLSAsymptoticVariance -
HansenEconometrics.twoSLSBootstrapBetaGapFinSucc -
HansenEconometrics.twoSLSBootstrapRobustLinearTStatFinSucc -
HansenEconometrics.twoSLSBootstrapUniformPstarFinSucc -
HansenEconometrics.twoSLSCombinedQXZ -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedQZZ -
HansenEconometrics.twoSLSCombinedRegressors
Theorem 12.91 endpoint
Corrected generated-regressor result: \sqrt n(\hat\beta-\beta)\xrightarrow{d}N(0,V), \hat V_{\mathrm{HC0}}\xrightarrow{p}V, and the tested-block Wald statistic converges to \chi_q^2 with calibrated asymptotic size.
theorem HansenEconometrics.GeneratedRegressorObservedIidConditions.theorem12_9_corrected_normal_covariance_wald_size
Corrected Hansen Theorem 12.9, full endpoint.
The literal observed-iid fourth moments derive the generated-design empirical third/fourth weight bounds and hence feasible HC0 consistency. The minimal extension supplies only tested-block covariance nondegeneracy before assembling coefficient normality, the chi-square Wald limit, and calibrated asymptotic size.
Formal statement
∀ {l : Type u_3} {k₁ : Type u_4} [inst : Fintype l] [inst_1 : Fintype k₁] [inst_2 : DecidableEq k₁] {Ω : Type u_6}
[inst_3 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [inst_4 : MeasureTheory.IsProbabilityMeasure μ] {r : Nat}
[inst_5 : Fact (instLTNat.lt 0 r)] {Z : Nat → Ω → l → Real} {v Y : Nat → Ω → Real}
{Ahat : Nat → Ω → Matrix l (Sum k₁ (Fin r)) Real} {A : Matrix l (Sum k₁ (Fin r)) Real} {β : Sum k₁ (Fin r) → Real},
HansenEconometrics.GeneratedRegressorObservedIidHC0Conditions μ Z v Y Ahat A β →
∀ {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared r) (Set.Ioi crit)) alpha →
And
(MeasureTheory.TendstoInDistribution
(fun m ω =>
instHSMul.hSMul m.cast.sqrt
(instHSub.hSub
(HansenEconometrics.generatedRegressorBetaStar (HansenEconometrics.stackRegressors Z m ω) (Ahat m ω)
(HansenEconometrics.stackOutcomes Y m ω))
β))
Filter.atTop (fun z => z.ofLp) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.generatedRegressorAsymptoticVariance A (HansenEconometrics.popGram μ Z)
(HansenEconometrics.scoreSecondMomMat μ Z v))))
(And
(MeasureTheory.TendstoInMeasure μ
(fun m ω =>
HansenEconometrics.generatedRegressorVHatStar (HansenEconometrics.stackRegressors Z m ω) (Ahat m ω)
(HansenEconometrics.stackOutcomes Y m ω))
Filter.atTop fun x =>
HansenEconometrics.generatedRegressorAsymptoticVariance A (HansenEconometrics.popGram μ Z)
(HansenEconometrics.scoreSecondMomMat μ Z v))
(And
(MeasureTheory.TendstoInDistribution
(fun m ω =>
HansenEconometrics.generatedRegressorBlockWaldStatOrZero
(HansenEconometrics.generatedRegressorBetaStar (HansenEconometrics.stackRegressors Z m ω) (Ahat m ω)
(HansenEconometrics.stackOutcomes Y m ω))
(HansenEconometrics.generatedRegressorVHatStar (HansenEconometrics.stackRegressors Z m ω) (Ahat m ω)
(HansenEconometrics.stackOutcomes Y m ω))
m.cast.sqrt)
Filter.atTop (fun x => x) (fun x => μ) (HansenEconometrics.chiSquared r))
(Filter.Tendsto
(fun m =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.generatedRegressorBlockWaldStatOrZero
(HansenEconometrics.generatedRegressorBetaStar (HansenEconometrics.stackRegressors Z m ω)
(Ahat m ω) (HansenEconometrics.stackOutcomes Y m ω))
(HansenEconometrics.generatedRegressorVHatStar (HansenEconometrics.stackRegressors Z m ω)
(Ahat m ω) (HansenEconometrics.stackOutcomes Y m ω))
m.cast.sqrt)))
Filter.atTop (nhds alpha))))Direct statement dependencies (11)
-
HansenEconometrics.GeneratedRegressorObservedIidHC0Conditions -
HansenEconometrics.chiSquared -
HansenEconometrics.generatedRegressorAsymptoticVariance -
HansenEconometrics.generatedRegressorBetaStar -
HansenEconometrics.generatedRegressorBlockWaldStatOrZero -
HansenEconometrics.generatedRegressorVHatStar -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.popGram -
HansenEconometrics.scoreSecondMomMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 12.103 endpoints
Under the corrected fixed-design Gaussian conditions, the known-variance pivot is N(0,1), the residual-variance pivot is t_{n-k}, and W^0/q\sim F_{q,n-k}.
theorem HansenEconometrics.generatedRegressorBeta2KnownSigmaPivotOrZero_hasLaw_standardNormal
Corrected scalar-pivot face of Hansen Theorem 12.10: with the population variance in the denominator, the totalized generated-block coefficient pivot is exactly standard normal on a full-rank realized design.
Formal statement
∀ {n : Type u_1} {k₁ : Type u_4} {k₂ : Type u_5} [inst : Fintype n] [inst_1 : Fintype k₁] [inst_2 : Fintype k₂]
[inst_3 : DecidableEq n] [inst_4 : DecidableEq k₁] [inst_5 : DecidableEq k₂] {Ω : Type u_6}
[inst_6 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (W₁ : Matrix n k₁ Real) (W₂hat : Matrix n k₂ Real)
(β₁ : k₁ → Real) {σ2 : Real} (j : k₂),
Real.instLT.lt 0 σ2 →
∀ (v : Ω → EuclideanSpace Real n)
[Invertible
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (W₁.fromCols W₂hat).transpose (W₁.fromCols W₂hat))],
ProbabilityTheory.HasLaw v (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
ProbabilityTheory.HasLaw
(fun ω =>
HansenEconometrics.generatedRegressorBeta2KnownSigmaPivotOrZero W₁ W₂hat
(instHAdd.hAdd (W₁.mulVec β₁) (v ω).ofLp) σ2 j)
(ProbabilityTheory.gaussianReal 0 1) μDirect statement dependencies (1)
-
HansenEconometrics.generatedRegressorBeta2KnownSigmaPivotOrZero
theorem HansenEconometrics.generatedRegressorBeta2TStatOrZero_hasLaw_classicalStudentT_card_sub
Corrected conventional-pivot face of Hansen Theorem 12.10: replacing the population variance by the OLS residual variance gives Student-t, not the standard-normal law printed in the theorem.
Formal statement
∀ {n : Type u_1} {k₁ : Type u_4} {k₂ : Type u_5} [inst : Fintype n] [inst_1 : Fintype k₁] [inst_2 : Fintype k₂]
[inst_3 : DecidableEq n] [inst_4 : DecidableEq k₁] [inst_5 : DecidableEq k₂] {Ω : Type u_6}
[inst_6 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (W₁ : Matrix n k₁ Real) (W₂hat : Matrix n k₂ Real)
(β₁ : k₁ → Real) {σ2 : Real} (j : k₂),
Real.instLT.lt 0 σ2 →
instLTNat.lt (instHAdd.hAdd (Fintype.card k₁) (Fintype.card k₂)) (Fintype.card n) →
∀ (v : Ω → EuclideanSpace Real n)
[Invertible
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (W₁.fromCols W₂hat).transpose (W₁.fromCols W₂hat))],
ProbabilityTheory.HasLaw v (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
ProbabilityTheory.HasLaw
(fun ω =>
HansenEconometrics.generatedRegressorBeta2TStatOrZero W₁ W₂hat (instHAdd.hAdd (W₁.mulVec β₁) (v ω).ofLp)
j)
(HansenEconometrics.classicalStudentT
(instHSub.hSub (instHSub.hSub (Fintype.card n) (Fintype.card k₁)) (Fintype.card k₂)))
μDirect statement dependencies (2)
-
HansenEconometrics.classicalStudentT -
HansenEconometrics.generatedRegressorBeta2TStatOrZero
theorem HansenEconometrics.generatedRegressorHomoskedasticFStatOrZero_hasLaw_classicalFDist
Hansen Theorem 12.10 exact homoskedastic F law for the canonical covariance-based statistic.
Formal statement
∀ {n : Type u_1} {k₁ : Type u_4} [inst : Fintype n] [inst_1 : Fintype k₁] [inst_2 : DecidableEq n]
[inst_3 : DecidableEq k₁] {Ω : Type u_6} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {r : Nat}
(W₁ : Matrix n k₁ Real) (W₂hat : Matrix n (Fin r) Real) (β₁ : k₁ → Real) {σ2 : Real},
Real.instLT.lt 0 σ2 →
instLTNat.lt 0 r →
instLTNat.lt (Fintype.card (Sum k₁ (Fin r))) (Fintype.card n) →
∀ (v : Ω → EuclideanSpace Real n)
[Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul W₁.transpose W₁)]
[Invertible
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (W₁.fromCols W₂hat).transpose (W₁.fromCols W₂hat))],
ProbabilityTheory.HasLaw v (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
ProbabilityTheory.HasLaw
(fun ω =>
HansenEconometrics.generatedRegressorHomoskedasticFStatOrZero W₁ W₂hat
(instHAdd.hAdd (W₁.mulVec β₁) (v ω).ofLp))
(HansenEconometrics.classicalFDist r (instHSub.hSub (Fintype.card n) (Fintype.card (Sum k₁ (Fin r))))) μDirect statement dependencies (2)
-
HansenEconometrics.classicalFDist -
HansenEconometrics.generatedRegressorHomoskedasticFStatOrZero
Theorem 12.111 endpoint
Under the corrected generated-regressor regularity conditions, \sqrt n(\hat\beta-\beta)\xrightarrow{d}N(0,V) and the structural-residual covariance estimator in (12.57) satisfies \hat V\xrightarrow{p}V.
theorem HansenEconometrics.generatedRegressorLS_theorem12_11_of_corrected_regularities
Corrected raw-model endpoint for Hansen Theorem 12.11.
The conclusion is exactly the generated-regressor coefficient CLT with Hansen’s covariance (12.56) and consistency of the structural-residual HC0 estimator (12.57). The two extra regularity assumptions needed to repair the printed theorem are isolated in GeneratedRegressorLSObservedIidRegularityConditions.
Formal statement
∀ {k : Type u_2} {l : Type u_3} [inst : Fintype k] [inst_1 : Fintype l] [inst_2 : DecidableEq k]
[inst_3 : DecidableEq l] {Ω : Type u_6} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
[inst_5 : MeasureTheory.IsProbabilityMeasure μ] {Z : Nat → Ω → l → Real} {X u : Nat → Ω → k → Real}
{v Y : Nat → Ω → Real} {A : Matrix l k Real} {β : k → Real},
HansenEconometrics.GeneratedRegressorLSObservedIidRegularityConditions μ Z X u v Y A β →
And
(MeasureTheory.TendstoInDistribution
(fun m ω =>
instHSMul.hSMul m.cast.sqrt
(instHSub.hSub
(HansenEconometrics.generatedRegressorBetaStar (HansenEconometrics.stackRegressors Z m ω)
(HansenEconometrics.generatedRegressorLSFirstStageCoefStar (HansenEconometrics.stackRegressors Z m ω)
(HansenEconometrics.stackRegressors X m ω))
(HansenEconometrics.stackOutcomes Y m ω))
β))
Filter.atTop (fun z => z.ofLp) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.generatedRegressorAsymptoticVariance A
(HansenEconometrics.twoSLSCombinedQZZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.scoreCovMat μ Z (HansenEconometrics.expectationErrorStructuralError X Y β)))))
(MeasureTheory.TendstoInMeasure μ
(fun m ω =>
HansenEconometrics.generatedRegressorLSVHatStar (HansenEconometrics.stackRegressors Z m ω)
(HansenEconometrics.stackRegressors X m ω) (HansenEconometrics.stackOutcomes Y m ω))
Filter.atTop fun x =>
HansenEconometrics.generatedRegressorAsymptoticVariance A
(HansenEconometrics.twoSLSCombinedQZZ
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(HansenEconometrics.scoreCovMat μ Z (HansenEconometrics.expectationErrorStructuralError X Y β)))Direct statement dependencies (12)
-
HansenEconometrics.GeneratedRegressorLSObservedIidRegularityConditions -
HansenEconometrics.expectationErrorStructuralError -
HansenEconometrics.generatedRegressorAsymptoticVariance -
HansenEconometrics.generatedRegressorBetaStar -
HansenEconometrics.generatedRegressorLSFirstStageCoefStar -
HansenEconometrics.generatedRegressorLSVHatStar -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSCombinedQZZ -
HansenEconometrics.twoSLSCombinedRegressors
Theorem 12.121 endpoint
Under the corrected expectation-error model, the joint estimator satisfies \sqrt n((\hat\beta,\hat\alpha)-(\beta,\alpha))\xrightarrow{d}N(0,V), and the three-block estimator satisfies \hat V\xrightarrow{p}V.
theorem HansenEconometrics.ExpectationErrorHansenObservedIidConditions.expectationError_theorem12_12_multivariateGaussian_and_canonicalVHat_of_observed_iid
Corrected Hansen Theorem 12.12, complete observed-iid endpoint.
The joint estimator has Hansen’s displayed Gaussian limit and the literal three-block estimator following Theorem 12.12 is consistent for the same covariance matrix.
Formal statement
∀ {k : Type u_2} {l : Type u_3} [inst : Fintype k] [inst_1 : Fintype l] [inst_2 : DecidableEq k]
[inst_3 : DecidableEq l] {Ω : Type u_6} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
[inst_5 : MeasureTheory.IsProbabilityMeasure μ] {Z : Nat → Ω → l → Real} {X u : Nat → Ω → k → Real}
{νe Y : Nat → Ω → Real} {A : Matrix l k Real} {β α : k → Real},
HansenEconometrics.ExpectationErrorHansenObservedIidConditions μ Z X u νe Y A β α →
And
(MeasureTheory.TendstoInDistribution
(fun m ω =>
instHSMul.hSMul m.cast.sqrt
(instHSub.hSub
(HansenEconometrics.expectationErrorBetaAlphaStar (HansenEconometrics.stackRegressors Z m ω)
(HansenEconometrics.stackRegressors X m ω) (HansenEconometrics.stackOutcomes Y m ω))
(Sum.elim β α)))
Filter.atTop (fun z => z.ofLp) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.expectationErrorAsymptoticVariance A (HansenEconometrics.popGram μ Z)
(HansenEconometrics.popGram μ u)
(HansenEconometrics.scoreCovMat μ Z (HansenEconometrics.expectationErrorStructuralError X Y β))
(HansenEconometrics.expectationErrorOmegaUZeNu μ u Z
(HansenEconometrics.expectationErrorStructuralError X Y β) νe)
(HansenEconometrics.scoreCovMat μ u νe))))
(MeasureTheory.TendstoInMeasure μ
(fun m ω =>
HansenEconometrics.expectationErrorVHatStar (HansenEconometrics.stackRegressors Z m ω)
(HansenEconometrics.stackRegressors X m ω) (HansenEconometrics.stackOutcomes Y m ω))
Filter.atTop fun x =>
HansenEconometrics.expectationErrorAsymptoticVariance A (HansenEconometrics.popGram μ Z)
(HansenEconometrics.popGram μ u)
(HansenEconometrics.scoreCovMat μ Z (HansenEconometrics.expectationErrorStructuralError X Y β))
(HansenEconometrics.expectationErrorOmegaUZeNu μ u Z
(HansenEconometrics.expectationErrorStructuralError X Y β) νe)
(HansenEconometrics.scoreCovMat μ u νe))Direct statement dependencies (10)
-
HansenEconometrics.ExpectationErrorHansenObservedIidConditions -
HansenEconometrics.expectationErrorAsymptoticVariance -
HansenEconometrics.expectationErrorBetaAlphaStar -
HansenEconometrics.expectationErrorOmegaUZeNu -
HansenEconometrics.expectationErrorStructuralError -
HansenEconometrics.expectationErrorVHatStar -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 12.131 endpoint
For the corrected control-function model, \sqrt n(\hat\alpha-\alpha)\xrightarrow{d}N(0,V_{22}+V_{\gamma\gamma}-V_{\gamma2}-V_{\gamma2}^{\prime}), and the correctly normalized robust covariance estimator is consistent.
theorem HansenEconometrics.ControlFunctionHansenObservedIidConditions.controlFunction_theorem12_13_multivariateGaussian_and_canonicalVHat_of_observed_iid
Corrected Hansen Theorem 12.13, complete observed-iid endpoint.
The actual control-function endogeneity estimator has Hansen’s displayed Gaussian limit, and the correctly normalized robust covariance estimator is consistent for the same alpha covariance. This corrects the 1/n prefactors printed on the raw-matrix Vhat22 and Vhatgamma2 sandwiches in (12.62). All finite-sample rank failures are discharged in probability from the observed-iid assumptions.
Formal statement
∀ {l : Type u_3} {k₁ : Type u_4} {k₂ : Type u_5} [inst : Fintype l] [inst_1 : Fintype k₁] [inst_2 : Fintype k₂]
[inst_3 : DecidableEq l] [inst_4 : DecidableEq k₁] [inst_5 : DecidableEq k₂] {Ω : Type u_6}
[inst_6 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [inst_7 : MeasureTheory.IsProbabilityMeasure μ]
{X₁ : Nat → Ω → k₁ → Real} {X₂ u₂ : Nat → Ω → k₂ → Real} {Z : Nat → Ω → l → Real} {Y e νe : Nat → Ω → Real}
{A₁ : Matrix l k₁ Real} {Γ : Matrix l k₂ Real} {β : Sum k₁ k₂ → Real} {α : k₂ → Real},
HansenEconometrics.ControlFunctionHansenObservedIidConditions μ X₁ X₂ u₂ Z Y e νe A₁ Γ β α →
And
(MeasureTheory.TendstoInDistribution
(fun m ω =>
instHSMul.hSMul m.cast.sqrt
(instHSub.hSub
(HansenEconometrics.controlFunctionAlphaHatStar (HansenEconometrics.stackRegressors X₁ m ω)
(HansenEconometrics.stackRegressors X₂ m ω) (HansenEconometrics.stackRegressors Z m ω)
(HansenEconometrics.stackOutcomes Y m ω))
α))
Filter.atTop (fun z => z.ofLp) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.controlFunctionAlphaAsymptoticVariance
(HansenEconometrics.controlFunctionFirstStageLoading A₁ Γ) (HansenEconometrics.popGram μ Z)
(HansenEconometrics.popGram μ u₂) (HansenEconometrics.scoreCovMat μ Z e)
(HansenEconometrics.expectationErrorOmegaUZeNu μ u₂ Z e νe) (HansenEconometrics.scoreCovMat μ u₂ νe))))
(MeasureTheory.TendstoInMeasure μ
(fun m ω =>
HansenEconometrics.controlFunctionAlphaVHatStar (HansenEconometrics.stackRegressors X₁ m ω)
(HansenEconometrics.stackRegressors X₂ m ω) (HansenEconometrics.stackRegressors Z m ω)
(HansenEconometrics.stackOutcomes Y m ω))
Filter.atTop fun x =>
HansenEconometrics.controlFunctionAlphaAsymptoticVariance
(HansenEconometrics.controlFunctionFirstStageLoading A₁ Γ) (HansenEconometrics.popGram μ Z)
(HansenEconometrics.popGram μ u₂) (HansenEconometrics.scoreCovMat μ Z e)
(HansenEconometrics.expectationErrorOmegaUZeNu μ u₂ Z e νe) (HansenEconometrics.scoreCovMat μ u₂ νe))Direct statement dependencies (10)
-
HansenEconometrics.ControlFunctionHansenObservedIidConditions -
HansenEconometrics.controlFunctionAlphaAsymptoticVariance -
HansenEconometrics.controlFunctionAlphaHatStar -
HansenEconometrics.controlFunctionAlphaVHatStar -
HansenEconometrics.controlFunctionFirstStageLoading -
HansenEconometrics.expectationErrorOmegaUZeNu -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 12.141 endpoint
Under the exogeneity null H_0:\alpha=0, the robust control-function Wald statistic satisfies W\xrightarrow{d}\chi_{k_2}^2, so its calibrated upper-tail test has asymptotic size \alpha_0.
theorem HansenEconometrics.ControlFunctionHansenObservedIidConditions.controlFunctionEndogeneityWald_theorem12_14_of_observed_iid_lowerTail
Corrected Hansen Theorem 12.14, complete observed-iid endpoint.
Under Hansen’s primitive exogeneity null, the robust control-function Wald statistic converges to chiSquared r; a lower-tail calibrated critical value therefore gives the stated asymptotic rejection probability. The displayed alpha covariance is assumed positive definite because Hansen’s remaining conditions allow degenerate errors.
Formal statement
∀ {l : Type u_3} {k₁ : Type u_4} [inst : Fintype l] [inst_1 : Fintype k₁] [inst_2 : DecidableEq l]
[inst_3 : DecidableEq k₁] {Ω : Type u_6} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
[inst_5 : MeasureTheory.IsProbabilityMeasure μ] {r : Nat} [inst_6 : Fact (instLTNat.lt 0 r)]
{X₁ : Nat → Ω → k₁ → Real} {X₂ u₂ : Nat → Ω → Fin r → Real} {Z : Nat → Ω → l → Real} {Y e νe : Nat → Ω → Real}
{A₁ : Matrix l k₁ Real} {Γ : Matrix l (Fin r) Real} {β : Sum k₁ (Fin r) → Real} {α : Fin r → Real},
HansenEconometrics.ControlFunctionHansenObservedIidConditions μ X₁ X₂ u₂ Z Y e νe A₁ Γ β α →
HansenEconometrics.controlFunctionPrimitiveEndogeneityNull μ X₂ e →
(HansenEconometrics.controlFunctionAlphaAsymptoticVariance
(HansenEconometrics.controlFunctionFirstStageLoading A₁ Γ) (HansenEconometrics.popGram μ Z)
(HansenEconometrics.popGram μ u₂) (HansenEconometrics.scoreCovMat μ Z e)
(HansenEconometrics.expectationErrorOmegaUZeNu μ u₂ Z e νe)
(HansenEconometrics.scoreCovMat μ u₂ νe)).PosDef →
∀ {crit : Real} {alphaTail : ENNReal},
ENNReal.instPartialOrder.le alphaTail 1 →
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared r) (Set.Iic crit))
(instHSub.hSub 1 alphaTail) →
And
(MeasureTheory.TendstoInDistribution
(fun m ω =>
HansenEconometrics.controlFunctionEndogeneityWaldStatOrZero
(HansenEconometrics.stackRegressors X₁ m ω) (HansenEconometrics.stackRegressors X₂ m ω)
(HansenEconometrics.stackRegressors Z m ω) (HansenEconometrics.stackOutcomes Y m ω) m.cast.sqrt)
Filter.atTop (fun x => x) (fun x => μ) (HansenEconometrics.chiSquared r))
(Filter.Tendsto
(fun m =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.controlFunctionEndogeneityWaldStatOrZero
(HansenEconometrics.stackRegressors X₁ m ω) (HansenEconometrics.stackRegressors X₂ m ω)
(HansenEconometrics.stackRegressors Z m ω) (HansenEconometrics.stackOutcomes Y m ω)
m.cast.sqrt)))
Filter.atTop (nhds alphaTail))Direct statement dependencies (12)
-
HansenEconometrics.ControlFunctionHansenObservedIidConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.controlFunctionAlphaAsymptoticVariance -
HansenEconometrics.controlFunctionEndogeneityWaldStatOrZero -
HansenEconometrics.controlFunctionFirstStageLoading -
HansenEconometrics.controlFunctionPrimitiveEndogeneityNull -
HansenEconometrics.expectationErrorOmegaUZeNu -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 12.151 endpoint
Under the corrected conditional-Gaussian and full-rank conditions, the control-function statistic has the exact law F\sim F_{k_2,n-k}.
theorem HansenEconometrics.controlFunctionEndogeneityHomoskedasticFStatOrZero_hasLaw_classicalFDist
Hansen Theorem 12.15 exact F law for the canonical covariance-based control-function statistic.
Formal statement
∀ {n : Type u_1} {l : Type u_3} {k₁ : Type u_4} [inst : Fintype n] [inst_1 : Fintype l] [inst_2 : Fintype k₁]
[inst_3 : DecidableEq n] [inst_4 : DecidableEq l] [inst_5 : DecidableEq k₁] {Ω : Type u_6}
[inst_6 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {r : Nat} (X₁ : Matrix n k₁ Real)
(X₂ : Matrix n (Fin r) Real) (Z : Matrix n l Real) (β : Sum k₁ (Fin r) → Real) {σ2 : Real},
Real.instLT.lt 0 σ2 →
instLTNat.lt 0 r →
instLTNat.lt (Fintype.card (Sum (Sum k₁ (Fin r)) (Fin r))) (Fintype.card n) →
∀ (ε : Ω → EuclideanSpace Real n)
[Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (X₁.fromCols X₂).transpose (X₁.fromCols X₂))]
[Invertible
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
((X₁.fromCols X₂).fromCols (HansenEconometrics.controlFunctionResidualStar Z X₂)).transpose
((X₁.fromCols X₂).fromCols (HansenEconometrics.controlFunctionResidualStar Z X₂)))],
ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
ProbabilityTheory.HasLaw
(fun ω =>
HansenEconometrics.controlFunctionEndogeneityHomoskedasticFStatOrZero X₁ X₂ Z
(instHAdd.hAdd ((X₁.fromCols X₂).mulVec β) (ε ω).ofLp))
(HansenEconometrics.classicalFDist r
(instHSub.hSub (Fintype.card n) (Fintype.card (Sum (Sum k₁ (Fin r)) (Fin r)))))
μDirect statement dependencies (3)
-
HansenEconometrics.classicalFDist -
HansenEconometrics.controlFunctionEndogeneityHomoskedasticFStatOrZero -
HansenEconometrics.controlFunctionResidualStar
Theorem 12.161 endpoint
Under Assumption 12.2 and conditional homoskedasticity, the Sargan statistic satisfies J\xrightarrow{d}\chi_{\ell-k}^2, and its calibrated upper-tail test has asymptotic size \alpha.
theorem HansenEconometrics.Theorem12_16.observed
Hansen Theorem 12.16 from the literal observed-row finite-fourth-moment Assumption 12.2 package and conditional homoskedasticity, with the scalar variance positivity derived from Ω > 0 rather than assumed separately.
Formal statement
∀ {k : Type u_2} {l : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k] [inst_2 : Fintype l]
[inst_3 : DecidableEq l] {Ω : Type u_6} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
[inst_5 : MeasureTheory.IsProbabilityMeasure μ] {Z : Nat → Ω → l → Real} {X : Nat → Ω → k → Real}
{e Y : Nat → Ω → Real} {β : k → Real}
[inst_6 : Fact (instLTNat.lt 0 (instHSub.hSub (Fintype.card l) (Fintype.card k)))],
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions μ Z X e Y β →
∀ (hZ0 : Measurable (Z 0)) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
HansenEconometrics.HomoskedasticErrorVariance μ Z e →
∀ {crit : Real} {alpha : ENNReal},
Eq
(MeasureTheory.Measure.instFunLike.coe
(HansenEconometrics.chiSquared (instHSub.hSub (Fintype.card l) (Fintype.card k))) (Set.Ioi crit))
alpha →
And
(MeasureTheory.TendstoInDistribution
(fun m ω =>
HansenEconometrics.twoSLSSarganStatOrZero (HansenEconometrics.stackRegressors Z m ω)
(HansenEconometrics.stackRegressors X m ω) (HansenEconometrics.stackOutcomes Y m ω))
Filter.atTop (fun x => x) (fun x => μ)
(HansenEconometrics.chiSquared (instHSub.hSub (Fintype.card l) (Fintype.card k))))
(Filter.Tendsto
(fun m =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.twoSLSSarganStatOrZero (HansenEconometrics.stackRegressors Z m ω)
(HansenEconometrics.stackRegressors X m ω) (HansenEconometrics.stackOutcomes Y m ω))))
Filter.atTop (nhds alpha))Direct statement dependencies (9)
-
HansenEconometrics.HomoskedasticErrorVariance -
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.conditioningSpace -
HansenEconometrics.conditioningSpace_le -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSSarganStatOrZero
Theorem 12.171 endpoint
Corrected subset-overidentification result: N=C^{*} on the full-rank sample events, N-C\xrightarrow{p}0, and N,C\xrightarrow{d}\chi_{\ell_b}^2. The maintained instrument block must also be relevant.
def HansenEconometrics.Theorem12_17.corrected
Corrected observed-row endpoint for Hansen Theorem 12.17.
The printed theorem’s full-instrument relevance condition does not imply relevance of the maintained instruments. This endpoint therefore adds exactly injectivity of E[Z_a X’]; the projection bridge derives the remaining maintained observed-iid, moment, orthogonality, QZZ, and Omega fields.
Formal statement
∀ {k : Type u_2} {la : Type u_4} {lb : Type u_5} [inst : Fintype k] [inst_1 : DecidableEq k] [inst_2 : Fintype la]
[inst_3 : DecidableEq la] [inst_4 : Fintype lb] [inst_5 : DecidableEq lb] {Ω : Type u_6} [inst_6 : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω} [inst_7 : MeasureTheory.IsProbabilityMeasure μ] {Za : Nat → Ω → la → Real}
{Zb : Nat → Ω → lb → Real} {X : Nat → Ω → k → Real} {e Y : Nat → Ω → Real} {df : Nat}
[inst_8 : Fact (instLTNat.lt 0 df)] {β : k → Real},
instLTNat.lt (Fintype.card k) (Fintype.card la) →
Eq df (Fintype.card lb) →
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions μ
(fun i ω => Sum.elim (Za i ω) (Zb i ω)) X e Y β →
Function.Injective
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram μ (HansenEconometrics.twoSLSCombinedRegressors Za X))).mulVec →
∀ (hZa0 : Measurable (Za 0)) [MeasureTheory.SigmaFinite (μ.trim ⋯)]
(hZfull0 : Measurable fun ω => Sum.elim (Za 0 ω) (Zb 0 ω)) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
HansenEconometrics.HomoskedasticErrorVariance μ (fun i ω => Sum.elim (Za i ω) (Zb i ω)) e →
∀ {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared df) (Set.Ioi crit)) alpha →
And
(Filter.Tendsto
(fun m =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Ne
(HansenEconometrics.twoSLSSubsetNeweyStatOrZero
(HansenEconometrics.stackRegressors Za m ω) (HansenEconometrics.stackRegressors Zb m ω)
(HansenEconometrics.stackRegressors X m ω) (HansenEconometrics.stackOutcomes Y m ω))
(HansenEconometrics.twoSLSSubsetSarganDiffCommonSigmaStatOrZero
(HansenEconometrics.stackRegressors Za m ω) (HansenEconometrics.stackRegressors Zb m ω)
(HansenEconometrics.stackRegressors X m ω) (HansenEconometrics.stackOutcomes Y m ω))))
Filter.atTop (nhds 0))
(And
(MeasureTheory.TendstoInDistribution
(fun m ω =>
HansenEconometrics.twoSLSSubsetNeweyStatOrZero (HansenEconometrics.stackRegressors Za m ω)
(HansenEconometrics.stackRegressors Zb m ω) (HansenEconometrics.stackRegressors X m ω)
(HansenEconometrics.stackOutcomes Y m ω))
Filter.atTop (fun x => x) (fun x => μ) (HansenEconometrics.chiSquared df))
(And
(MeasureTheory.TendstoInDistribution
(fun m ω =>
HansenEconometrics.twoSLSSubsetSarganDiffStatOrZero
(HansenEconometrics.stackRegressors Za m ω) (HansenEconometrics.stackRegressors Zb m ω)
(HansenEconometrics.stackRegressors X m ω) (HansenEconometrics.stackOutcomes Y m ω))
Filter.atTop (fun x => x) (fun x => μ) (HansenEconometrics.chiSquared df))
(And
(MeasureTheory.TendstoInMeasure μ
(fun m ω =>
instHSub.hSub
(HansenEconometrics.twoSLSSubsetNeweyStatOrZero
(HansenEconometrics.stackRegressors Za m ω)
(HansenEconometrics.stackRegressors Zb m ω) (HansenEconometrics.stackRegressors X m ω)
(HansenEconometrics.stackOutcomes Y m ω))
(HansenEconometrics.twoSLSSubsetSarganDiffStatOrZero
(HansenEconometrics.stackRegressors Za m ω)
(HansenEconometrics.stackRegressors Zb m ω) (HansenEconometrics.stackRegressors X m ω)
(HansenEconometrics.stackOutcomes Y m ω)))
Filter.atTop fun x => 0)
(And
(Filter.Tendsto
(fun m =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.twoSLSSubsetNeweyStatOrZero
(HansenEconometrics.stackRegressors Za m ω)
(HansenEconometrics.stackRegressors Zb m ω)
(HansenEconometrics.stackRegressors X m ω)
(HansenEconometrics.stackOutcomes Y m ω))))
Filter.atTop (nhds alpha))
(Filter.Tendsto
(fun m =>
MeasureTheory.Measure.instFunLike.coe μ
(setOf fun ω =>
Real.instLT.lt crit
(HansenEconometrics.twoSLSSubsetSarganDiffStatOrZero
(HansenEconometrics.stackRegressors Za m ω)
(HansenEconometrics.stackRegressors Zb m ω)
(HansenEconometrics.stackRegressors X m ω)
(HansenEconometrics.stackOutcomes Y m ω))))
Filter.atTop (nhds alpha))))))Direct statement dependencies (14)
-
HansenEconometrics.HomoskedasticErrorVariance -
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.conditioningSpace -
HansenEconometrics.conditioningSpace_le -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.popGram -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedRegressors -
HansenEconometrics.twoSLSSubsetNeweyStatOrZero -
HansenEconometrics.twoSLSSubsetSarganDiffCommonSigmaStatOrZero -
HansenEconometrics.twoSLSSubsetSarganDiffStatOrZero
Theorem 12.181 endpoint
Under the corrected weak-instrument triangular-array conditions, \hat\beta_{\mathrm{OLS}}-\beta\xrightarrow{p}\Sigma_{22}^{-1}\Sigma_{2e}, while \hat\beta_{\mathrm{2SLS}}-\beta and \hat\beta_{\mathrm{LIML}}-\beta have Hansen’s non-Gaussian random-matrix limits.
theorem HansenEconometrics.weakIV_theorem12_18_triangular_estimators_of_raw_moments
Hansen Theorem 12.18 directly from raw iid moments and the concrete smallest generalized-Rayleigh root. No selector convergence, estimator convergence, or Rayleigh minimizer is assumed. The remaining premises are the population rank conditions needed by the totalized inverse maps.
Formal statement
∀ {k : Type u_1} {l : Type u_2} [inst : Fintype k] [inst_1 : Fintype l] [inst_2 : DecidableEq k]
[inst_3 : DecidableEq l] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
[inst_5 : MeasureTheory.IsProbabilityMeasure μ] {Z : Nat → Ω → l → Real} {u : Nat → Ω → Sum Unit k → Real}
{C : Matrix l k Real} {beta : k → Real},
HansenEconometrics.WeakIVRawJointMomentConditions μ Z u →
IsUnit (HansenEconometrics.popGram μ Z).det →
(HansenEconometrics.popGram μ u).PosDef →
Eq
(MeasureTheory.Measure.instFunLike.coe
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.covMat μ (HansenEconometrics.weakIVRawReducedFormScoreRow Z u 0)))
(setOf fun z =>
Not
(IsUnit
(HansenEconometrics.weakIV2SLSLimitBread (HansenEconometrics.popGram μ Z) C
(HansenEconometrics.weakIVRawGaussianFirstStage
(HansenEconometrics.weakIVRawGaussianMatrix z))).det)))
0 →
Eq
(MeasureTheory.Measure.instFunLike.coe
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.covMat μ (HansenEconometrics.weakIVRawReducedFormScoreRow Z u 0)))
(setOf fun z =>
Not
(IsUnit
(HansenEconometrics.weakIVLIMLLimitBread (HansenEconometrics.popGram μ Z) C
(HansenEconometrics.weakIVRawGaussianFirstStage
(HansenEconometrics.weakIVRawGaussianMatrix z))
(HansenEconometrics.weakIVRawLIMLSmallestRoot μ Z u C beta z)
(HansenEconometrics.weakIVRawSigma22 (HansenEconometrics.popGram μ u))).det)))
0 →
And
(MeasureTheory.TendstoInMeasure μ
(fun m omega => instHSub.hSub (HansenEconometrics.weakIVLocalOLSBetaStar Z u C beta m omega) beta)
Filter.atTop fun x =>
HansenEconometrics.weakIVOLSBias (HansenEconometrics.weakIVRawSigma22 (HansenEconometrics.popGram μ u))
(HansenEconometrics.weakIVRawSigma2e (HansenEconometrics.popGram μ u) beta))
(And
(MeasureTheory.TendstoInDistribution
(fun m omega => instHSub.hSub (HansenEconometrics.weakIVLocal2SLSBetaStar Z u C beta m omega) beta)
Filter.atTop
(fun z =>
HansenEconometrics.weakIV2SLSBias (HansenEconometrics.popGram μ Z) C
(HansenEconometrics.weakIVRawGaussianFirstStage (HansenEconometrics.weakIVRawGaussianMatrix z))
(HansenEconometrics.weakIVRawGaussianStructuralScore
(HansenEconometrics.weakIVRawGaussianMatrix z) beta))
(fun x => μ)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.covMat μ (HansenEconometrics.weakIVRawReducedFormScoreRow Z u 0))))
(And
(MeasureTheory.TendstoInDistribution
(fun m omega =>
instHSub.hSub
(HansenEconometrics.weakIVLocalLIMLBetaStar Z u C beta
(HansenEconometrics.weakIVLocalLIMLSmallestRoot Z u C beta) m omega)
beta)
Filter.atTop
(fun z =>
HansenEconometrics.weakIVLIMLBias (HansenEconometrics.popGram μ Z) C
(HansenEconometrics.weakIVRawGaussianFirstStage (HansenEconometrics.weakIVRawGaussianMatrix z))
(HansenEconometrics.weakIVRawGaussianStructuralScore
(HansenEconometrics.weakIVRawGaussianMatrix z) beta)
(HansenEconometrics.weakIVRawLIMLSmallestRoot μ Z u C beta z)
(HansenEconometrics.weakIVRawSigma22 (HansenEconometrics.popGram μ u))
(HansenEconometrics.weakIVRawSigma2e (HansenEconometrics.popGram μ u) beta))
(fun x => μ)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.covMat μ (HansenEconometrics.weakIVRawReducedFormScoreRow Z u 0))))
(∀ (z : EuclideanSpace Real (Prod l (Sum Unit k))),
have p := HansenEconometrics.weakIVRawLIMLGeneralizedEigenvalueLimitPair μ Z u C beta z;
HansenEconometrics.LIMLRayleighMinimizer p.fst p.snd
(HansenEconometrics.weakIVRawLIMLSmallestRoot μ Z u C beta z))))Direct statement dependencies (21)
-
HansenEconometrics.LIMLRayleighMinimizer -
HansenEconometrics.WeakIVRawJointMomentConditions -
HansenEconometrics.covMat -
HansenEconometrics.popGram -
HansenEconometrics.weakIV2SLSBias -
HansenEconometrics.weakIV2SLSLimitBread -
HansenEconometrics.weakIVLIMLBias -
HansenEconometrics.weakIVLIMLLimitBread -
HansenEconometrics.weakIVLocal2SLSBetaStar -
HansenEconometrics.weakIVLocalLIMLBetaStar -
HansenEconometrics.weakIVLocalLIMLSmallestRoot -
HansenEconometrics.weakIVLocalOLSBetaStar -
HansenEconometrics.weakIVOLSBias -
HansenEconometrics.weakIVRawGaussianFirstStage -
HansenEconometrics.weakIVRawGaussianMatrix -
HansenEconometrics.weakIVRawGaussianStructuralScore -
HansenEconometrics.weakIVRawLIMLGeneralizedEigenvalueLimitPair -
HansenEconometrics.weakIVRawLIMLSmallestRoot -
HansenEconometrics.weakIVRawReducedFormScoreRow -
HansenEconometrics.weakIVRawSigma22 -
HansenEconometrics.weakIVRawSigma2e
Theorem 12.191 endpoint
Under the corrected many-instrument model with \ell_n/n\to\alpha, \hat\beta_{\mathrm{OLS}}\xrightarrow{p}\beta+(H+\Sigma_{22})^{-1}\Sigma_{2e}, \hat\beta_{\mathrm{2SLS}}\xrightarrow{p}\beta+(H+\alpha\Sigma_{22})^{-1}\alpha\Sigma_{2e}, and \hat\beta_{\mathrm{LIML}}\xrightarrow{p}\beta.
theorem HansenEconometrics.manyInstruments_estimators_theorem12_19_of_hansenRawModel_smallestRoot
Corrected Hansen-facing Theorem 12.19 endpoint. The full OLS assembly, projected quadratic concentration (12.81), and concrete LIML selector are derived from the primitive [u₁,u₂] conditional model.
Formal statement
∀ {k : Type u_1} [inst : Fintype k] [inst_1 : DecidableEq k] {ι : Nat → Type u_2} [inst_2 : (m : Nat) → Fintype (ι m)]
[inst_3 : (m : Nat) → DecidableEq (ι m)] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
[inst_5 : MeasureTheory.IsProbabilityMeasure μ] [inst_6 : StandardBorelSpace Ω]
{Z : (m : Nat) → Ω → Matrix (Fin m) (ι m) Real} {X : (m : Nat) → Ω → Matrix (Fin m) k Real}
{Y : (m : Nat) → Ω → Fin m → Real} {Gamma : (m : Nat) → Matrix (ι m) k Real} {u1 : (m : Nat) → Ω → Fin m → Real}
{u2 : (m : Nat) → Ω → Matrix (Fin m) k Real} {β : k → Real} {H : Matrix k k Real}
{Sigma : Matrix (Sum Unit k) (Sum Unit k) Real} {alpha B : Real},
HansenEconometrics.ManyInstrumentsPrimitiveErrorRawModelConditions μ Z X Y Gamma u1 u2 β H Sigma alpha B →
And
(MeasureTheory.TendstoInMeasure μ (fun m ω => HansenEconometrics.olsBetaStar (X m ω) (Y m ω)) Filter.atTop
fun x =>
instHAdd.hAdd β
(HansenEconometrics.manyInstrumentsOLSBias H (HansenEconometrics.manyInstrumentsSigma22 Sigma)
(HansenEconometrics.manyInstrumentsHansenSigma2e β Sigma)))
(And
(MeasureTheory.TendstoInMeasure μ (fun m ω => HansenEconometrics.twoSLSBetaStar (Z m ω) (X m ω) (Y m ω))
Filter.atTop fun x =>
instHAdd.hAdd β
(HansenEconometrics.manyInstrumentsTwoSLSBias H (HansenEconometrics.manyInstrumentsSigma22 Sigma)
(HansenEconometrics.manyInstrumentsHansenSigma2e β Sigma) alpha))
(MeasureTheory.TendstoInMeasure μ
(fun m ω =>
HansenEconometrics.limlBetaStar (Z m ω) (X m ω) (Y m ω)
(HansenEconometrics.manyInstrumentsLIMLSmallestRoot Z X Y m ω))
Filter.atTop fun x => β))Direct statement dependencies (9)
-
HansenEconometrics.ManyInstrumentsPrimitiveErrorRawModelConditions -
HansenEconometrics.limlBetaStar -
HansenEconometrics.manyInstrumentsHansenSigma2e -
HansenEconometrics.manyInstrumentsLIMLSmallestRoot -
HansenEconometrics.manyInstrumentsOLSBias -
HansenEconometrics.manyInstrumentsSigma22 -
HansenEconometrics.manyInstrumentsTwoSLSBias -
HansenEconometrics.olsBetaStar -
HansenEconometrics.twoSLSBetaStar