Chapter 13: Generalized Method of Moments
Foldable textbook-to-Lean result crosswalk for Chapter 13.
This page is generated from the canonical Chapter 13 inventory and the compiled Lean environment. It contains 18 textbook result groups and 52 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 13.15 endpoints
With positive weight W, \hat\beta_{\mathrm{GMM}}=(X'ZWZ'X)^{-1}X'ZWZ'Y minimizes J(\beta)=(Z'(Y-X\beta))'W(Z'(Y-X\beta)).
def HansenEconometrics.gmmBeta
Hansen equation (13.6): the base one-step linear GMM estimator.
Formal statement
{n : Type u_1} →
{k : Type u_2} →
{l : Type u_3} →
[inst : Fintype n] →
[inst_1 : Fintype k] →
[inst_2 : Fintype l] →
[inst_3 : DecidableEq k] →
(X : Matrix n k Real) →
(Z : Matrix n l Real) →
(n → Real) → (W : Matrix l l Real) → [Invertible (HansenEconometrics.gmmGram X Z W)] → k → RealDirect statement dependencies (1)
-
HansenEconometrics.gmmGram
theorem HansenEconometrics.gmmCriterion_gmmBeta_le
Hansen Theorem 13.1 (existence). The one-step GMM estimator minimizes the GMM criterion.
Formal statement
∀ {n : Type u_1} {k : Type u_2} {l : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype l]
[inst_3 : DecidableEq k] (X : Matrix n k Real) (Z : Matrix n l Real) (y : n → Real) (W : Matrix l l Real)
(b : k → Real) [inst_4 : Invertible (HansenEconometrics.gmmGram X Z W)],
W.PosSemidef →
Real.instLE.le (HansenEconometrics.gmmCriterion X Z y W (HansenEconometrics.gmmBeta X Z y W))
(HansenEconometrics.gmmCriterion X Z y W b)Direct statement dependencies (3)
-
HansenEconometrics.gmmBeta -
HansenEconometrics.gmmCriterion -
HansenEconometrics.gmmGram
theorem HansenEconometrics.gmmBeta_isMinOn
Hansen Theorem 13.1 (existence), packaged as IsMinOn.
Formal statement
∀ {n : Type u_1} {k : Type u_2} {l : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype l]
[inst_3 : DecidableEq k] (X : Matrix n k Real) (Z : Matrix n l Real) (y : n → Real) (W : Matrix l l Real)
[inst_4 : Invertible (HansenEconometrics.gmmGram X Z W)],
W.PosSemidef → IsMinOn (HansenEconometrics.gmmCriterion X Z y W) Set.univ (HansenEconometrics.gmmBeta X Z y W)Direct statement dependencies (3)
-
HansenEconometrics.gmmBeta -
HansenEconometrics.gmmCriterion -
HansenEconometrics.gmmGram
theorem HansenEconometrics.gmmBeta_eq_of_minimizer
Hansen Theorem 13.1 (uniqueness). A coefficient that attains the minimum equals the one-step GMM estimator.
Formal statement
∀ {n : Type u_1} {k : Type u_2} {l : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype l]
[inst_3 : DecidableEq k] (X : Matrix n k Real) (Z : Matrix n l Real) (y : n → Real) (W : Matrix l l Real)
(b : k → Real) [inst_4 : Invertible (HansenEconometrics.gmmGram X Z W)],
W.PosSemidef →
Eq (HansenEconometrics.gmmCriterion X Z y W b)
(HansenEconometrics.gmmCriterion X Z y W (HansenEconometrics.gmmBeta X Z y W)) →
Eq b (HansenEconometrics.gmmBeta X Z y W)Direct statement dependencies (3)
-
HansenEconometrics.gmmBeta -
HansenEconometrics.gmmCriterion -
HansenEconometrics.gmmGram
def HansenEconometrics.gmmCriterion
Hansen’s linear GMM criterion, without its positive scalar factor n.
Formal statement
{n : Type u_1} →
{k : Type u_2} →
{l : Type u_3} →
[Fintype n] →
[Fintype k] → [Fintype l] → Matrix n k Real → Matrix n l Real → (n → Real) → Matrix l l Real → (k → Real) → RealTheorem 13.24 endpoints
If W=(Z'Z)^{-1}, then \hat\beta_{\mathrm{GMM}}=\hat\beta_{\mathrm{2SLS}}; if k=\ell, then \hat\beta_{\mathrm{GMM}}=\hat\beta_{\mathrm{IV}}.
theorem HansenEconometrics.gmmBetaStar_eq_twoSLSBetaStar
Hansen Theorem 13.2 (2SLS, Star form). GMM with weight (Z’Z)⁻¹ equals 2SLS.
Formal statement
∀ {n : Type u_1} {k : Type u_2} {l : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype l]
[inst_3 : DecidableEq k] [inst_4 : DecidableEq l] (X : Matrix n k Real) (Z : Matrix n l Real) (y : n → Real),
Eq
(HansenEconometrics.gmmBetaStar X Z y
(Matrix.inv.inv (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul Z.transpose Z)))
(HansenEconometrics.twoSLSBetaStar Z X y)Direct statement dependencies (2)
-
HansenEconometrics.gmmBetaStar -
HansenEconometrics.twoSLSBetaStar
theorem HansenEconometrics.gmmBetaOrZero_eq_twoSLSBetaOrZero
Hansen Theorem 13.2 (2SLS, textbook-facing form). Totalized GMM with weight (Z’Z)⁻¹ equals totalized 2SLS, including singular designs.
Formal statement
∀ {n : Type u_1} {k : Type u_2} {l : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype l]
[inst_3 : DecidableEq k] [inst_4 : DecidableEq l] (X : Matrix n k Real) (Z : Matrix n l Real) (y : n → Real),
Eq
(HansenEconometrics.gmmBetaOrZero X Z y
(Matrix.inv.inv (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul Z.transpose Z)))
(HansenEconometrics.twoSLSBetaOrZero Z X y)Direct statement dependencies (2)
-
HansenEconometrics.gmmBetaOrZero -
HansenEconometrics.twoSLSBetaOrZero
theorem HansenEconometrics.gmmBetaOrZero_eq_twoSLSBeta
Hansen Theorem 13.2 (2SLS, nonsingular form). With the ordinary inverse weight, textbook-facing GMM equals the ordinary 2SLS estimator.
Formal statement
∀ {n : Type u_1} {k : Type u_2} {l : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype l]
[inst_3 : DecidableEq k] [inst_4 : DecidableEq l] (X : Matrix n k Real) (Z : Matrix n l Real) (y : n → Real)
[inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul Z.transpose Z)]
[inst_6 : Invertible (HansenEconometrics.twoSLSMomentMatrix Z X)],
Eq
(HansenEconometrics.gmmBetaOrZero X Z y
(inst_5.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul Z.transpose Z)))
(HansenEconometrics.twoSLSBeta Z X y)Direct statement dependencies (3)
-
HansenEconometrics.gmmBetaOrZero -
HansenEconometrics.twoSLSBeta -
HansenEconometrics.twoSLSMomentMatrix
theorem HansenEconometrics.gmmBetaOrZero_eq_ivBeta_of_justIdentified
Hansen Theorem 13.2 (just-identified form). If the moment map is square and nonsingular, GMM equals IV for every invertible weight.
Formal statement
∀ {n : Type u_1} {k : Type u_2} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : DecidableEq k] (X Z : Matrix n k Real)
(y : n → Real) (W : Matrix k k Real)
[inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul Z.transpose X)] [Invertible W],
Eq (HansenEconometrics.gmmBetaOrZero X Z y W) (HansenEconometrics.ivBeta Z X y)Direct statement dependencies (2)
-
HansenEconometrics.gmmBetaOrZero -
HansenEconometrics.ivBeta
Theorem 13.35 endpoints
If \hat W\xrightarrow{p}W\succ0, then \sqrt n(\hat\beta_{\mathrm{GMM}}-\beta)\xrightarrow{d}N(0,V_\beta) with V_\beta=(Q'WQ)^{-1}(Q'W\Omega WQ)(Q'WQ)^{-1}.
def HansenEconometrics.gmmAsymptoticVariance
Hansen equation (13.7), the linear GMM sandwich covariance.
Formal statement
{k : Type u_2} →
{l : Type u_3} →
[inst : Fintype k] →
[inst_1 : Fintype l] →
[inst_2 : DecidableEq k] →
(Q : Matrix l k Real) →
(W : Matrix l l Real) →
Matrix l l Real → [Invertible (HansenEconometrics.gmmPopulationGram Q W)] → Matrix k k RealDirect statement dependencies (1)
-
HansenEconometrics.gmmPopulationGram
theorem HansenEconometrics.gmmAsymptoticVariance_eq_formula
Hansen equation (13.7) in its displayed symmetric-weight form.
Formal statement
∀ {k : Type u_2} {l : Type u_3} [inst : Fintype k] [inst_1 : Fintype l] [inst_2 : DecidableEq k] (Q : Matrix l k Real)
(W Omega : Matrix l l Real) [inst_3 : Invertible (HansenEconometrics.gmmPopulationGram Q W)],
W.PosSemidef →
Eq (HansenEconometrics.gmmAsymptoticVariance Q W Omega)
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(inst_3.invOf (HansenEconometrics.gmmPopulationGram Q W)) Q.transpose)
W)
Omega)
W)
Q)
(inst_3.invOf (HansenEconometrics.gmmPopulationGram Q W)))Direct statement dependencies (2)
-
HansenEconometrics.gmmAsymptoticVariance -
HansenEconometrics.gmmPopulationGram
theorem HansenEconometrics.gmmLinearizedScore_tendstoInDistribution
The random GMM influence matrix applied to the scaled instrument score has the sandwich Gaussian limit in Hansen equation (13.7).
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {l : Type u_3} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : DecidableEq k] [inst_5 : DecidableEq l] {Qhat : Nat → OmegaSpace → Matrix l k Real}
{What : Nat → OmegaSpace → Matrix l l Real} {Z : Nat → OmegaSpace → l → Real} {e : Nat → OmegaSpace → Real}
{Q : Matrix l k Real} {W : Matrix l l Real},
HansenEconometrics.GMMMomentCLTConditions mu Qhat What Z e Q W →
MeasureTheory.TendstoInDistribution
(fun n omega =>
(HansenEconometrics.gmmLinearizationMatrixStar (Qhat n omega) (What n omega)).mulVec
(instHSMul.hSMul n.cast.sqrt
(HansenEconometrics.sampleCrossMoment (HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackErrors e n omega))))
Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.gmmAsymptoticVarianceStar Q W (HansenEconometrics.scoreCovMat mu Z e)))Direct statement dependencies (7)
-
HansenEconometrics.GMMMomentCLTConditions -
HansenEconometrics.gmmAsymptoticVarianceStar -
HansenEconometrics.gmmLinearizationMatrixStar -
HansenEconometrics.sampleCrossMoment -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackErrors -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.gmmBetaStar_tendstoInDistribution
Hansen Theorem 13.3 (Star form). Under convergence of the sample derivative and weight matrix, the linear GMM estimator is asymptotically normal with the sandwich covariance in equation (13.8).
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {l : Type u_3} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : DecidableEq k] [inst_5 : DecidableEq l] {What : Nat → OmegaSpace → Matrix l l Real}
{Z : Nat → OmegaSpace → l → Real} {X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real}
{Q : Matrix l k Real} {W : Matrix l l Real},
HansenEconometrics.GMMMomentCLTConditions mu
(fun n omega =>
HansenEconometrics.sampleQZX (HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackRegressors X n omega))
What Z e Q W →
∀ (b : k → Real),
(∀ (i : Nat) (omega : OmegaSpace), Eq (Y i omega) (instHAdd.hAdd (dotProduct (X i omega) b) (e i omega))) →
(∀ (n : Nat),
AEMeasurable
(fun omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmBetaStar (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega) (HansenEconometrics.stackOutcomes Y n omega)
(What n omega))
b))
mu) →
MeasureTheory.TendstoInDistribution
(fun n omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmBetaStar (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega) (HansenEconometrics.stackOutcomes Y n omega)
(What n omega))
b))
Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.gmmAsymptoticVarianceStar Q W (HansenEconometrics.scoreCovMat mu Z e)))Direct statement dependencies (7)
-
HansenEconometrics.GMMMomentCLTConditions -
HansenEconometrics.gmmAsymptoticVarianceStar -
HansenEconometrics.gmmBetaStar -
HansenEconometrics.sampleQZX -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.gmmBetaOrZero_tendstoInDistribution_of_assumption12_2
Hansen Theorem 13.3 under Assumption 12.2. A convergent positive-definite weight sequence gives the standard GMM sandwich limit.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {l : Type u_3} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : DecidableEq k] [inst_5 : DecidableEq l] {What : Nat → OmegaSpace → Matrix l l Real}
{Z : Nat → OmegaSpace → l → Real} {X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real},
HansenEconometrics.TwoSLSGramScoreCLTPositiveCovarianceConditions mu Z X e →
∀ (W : Matrix l l Real),
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (What n) mu) →
(MeasureTheory.TendstoInMeasure mu What Filter.atTop fun x => W) →
W.PosDef →
∀ (b : k → Real),
(∀ (i : Nat) (omega : OmegaSpace),
Eq (Y i omega) (instHAdd.hAdd (dotProduct (X i omega) b) (e i omega))) →
(∀ (n : Nat),
AEMeasurable
(fun omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmBetaOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackOutcomes Y n omega) (What n omega))
b))
mu) →
MeasureTheory.TendstoInDistribution
(fun n omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmBetaOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega) (HansenEconometrics.stackOutcomes Y n omega)
(What n omega))
b))
Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.gmmAsymptoticVarianceStar
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X)))
W (HansenEconometrics.scoreCovMat mu Z e)))Direct statement dependencies (9)
-
HansenEconometrics.TwoSLSGramScoreCLTPositiveCovarianceConditions -
HansenEconometrics.gmmAsymptoticVarianceStar -
HansenEconometrics.gmmBetaOrZero -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedRegressors
Theorem 13.42 endpoints
With efficient weight W=\Omega^{-1}, \sqrt n(\hat\beta_{\mathrm{GMM}}-\beta)\xrightarrow{d}N(0,(Q'\Omega^{-1}Q)^{-1}).
theorem HansenEconometrics.gmmAsymptoticVarianceStar_efficient
Hansen Theorem 13.4 (Star covariance formula). With a positive-definite moment covariance and a full-rank derivative, efficient GMM has covariance (Q’Omega⁻¹Q)⁻¹.
Formal statement
∀ {k : Type u_2} {l : Type u_3} [inst : Fintype k] [inst_1 : Fintype l] [inst_2 : DecidableEq k] (Q : Matrix l k Real)
(Omega : Matrix l l Real) [inst_3 : DecidableEq l],
Omega.PosDef →
Function.Injective Q.mulVec →
Eq (HansenEconometrics.gmmAsymptoticVarianceStar Q (Matrix.inv.inv Omega) Omega)
(Matrix.inv.inv (HansenEconometrics.gmmPopulationGram Q (Matrix.inv.inv Omega)))Direct statement dependencies (2)
-
HansenEconometrics.gmmAsymptoticVarianceStar -
HansenEconometrics.gmmPopulationGram
theorem HansenEconometrics.gmmBetaOrZero_tendstoInDistribution_efficient_of_assumption12_2
Hansen Theorem 13.4. If the GMM weight converges to the inverse score covariance, the coefficient limit has covariance (Q’Omega⁻¹Q)⁻¹.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {l : Type u_3} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : DecidableEq k] [inst_5 : DecidableEq l] {What : Nat → OmegaSpace → Matrix l l Real}
{Z : Nat → OmegaSpace → l → Real} {X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real},
HansenEconometrics.TwoSLSGramScoreCLTPositiveCovarianceConditions mu Z X e →
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (What n) mu) →
(MeasureTheory.TendstoInMeasure mu What Filter.atTop fun x =>
Matrix.inv.inv (HansenEconometrics.scoreCovMat mu Z e)) →
∀ (b : k → Real),
(∀ (i : Nat) (omega : OmegaSpace), Eq (Y i omega) (instHAdd.hAdd (dotProduct (X i omega) b) (e i omega))) →
(∀ (n : Nat),
AEMeasurable
(fun omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmBetaOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega) (HansenEconometrics.stackOutcomes Y n omega)
(What n omega))
b))
mu) →
MeasureTheory.TendstoInDistribution
(fun n omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmBetaOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega) (HansenEconometrics.stackOutcomes Y n omega)
(What n omega))
b))
Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0
(Matrix.inv.inv
(HansenEconometrics.gmmPopulationGram
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(Matrix.inv.inv (HansenEconometrics.scoreCovMat mu Z e)))))Direct statement dependencies (9)
-
HansenEconometrics.TwoSLSGramScoreCLTPositiveCovarianceConditions -
HansenEconometrics.gmmBetaOrZero -
HansenEconometrics.gmmPopulationGram -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedRegressors
Theorem 13.51 endpoint
For every W\succ0, V_\beta(W)-(Q'\Omega^{-1}Q)^{-1}\succeq0; efficient GMM has weakly smaller asymptotic covariance.
theorem HansenEconometrics.gmmAsymptoticVariance_sub_efficient_posSemidef
Hansen Theorem 13.5. The covariance of any identified linear GMM estimator dominates the efficient GMM covariance in Loewner order.
Formal statement
∀ {k : Type u_2} {l : Type u_3} [inst : Fintype k] [inst_1 : Fintype l] [inst_2 : DecidableEq k] (Q : Matrix l k Real)
(W Omega : Matrix l l Real) [inst_3 : DecidableEq l] [inst_4 : Invertible Omega]
[inst_5 : Invertible (HansenEconometrics.gmmPopulationGram Q (inst_4.invOf Omega))]
[inst_6 : Invertible (HansenEconometrics.gmmPopulationGram Q W)],
Omega.PosSemidef →
(instHSub.hSub (HansenEconometrics.gmmAsymptoticVariance Q W Omega)
(HansenEconometrics.gmmAsymptoticVariance Q (inst_4.invOf Omega) Omega)).PosSemidefDirect statement dependencies (2)
-
HansenEconometrics.gmmAsymptoticVariance -
HansenEconometrics.gmmPopulationGram
Theorem 13.62 endpoints
If \mathbb E[e^2\mid Z]=\sigma^2, then \Omega=\sigma^2Q_{ZZ} and the 2SLS weight Q_{ZZ}^{-1} is efficient.
theorem HansenEconometrics.twoSLSWeight_is_efficientGMM_of_assumption12_2_observedRows_homoskedastic
Hansen Theorem 13.6, observed-row form. Literal observed-row Assumption 12.2 and conditional homoskedasticity imply that the population 2SLS weight attains the efficient GMM covariance.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {l : Type u_3} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : DecidableEq k] [inst_5 : DecidableEq l] [Nonempty l] {Z : Nat → OmegaSpace → l → Real}
{X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real} {b : k → Real},
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions mu Z X e Y b →
∀ (hZ0 : Measurable (Z 0)) [MeasureTheory.SigmaFinite (mu.trim ⋯)],
HansenEconometrics.HomoskedasticErrorVariance mu Z e →
Eq
(HansenEconometrics.gmmAsymptoticVarianceStar
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(Matrix.inv.inv
(HansenEconometrics.twoSLSCombinedQZZ
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X))))
(HansenEconometrics.scoreCovMat mu Z e))
(Matrix.inv.inv
(HansenEconometrics.gmmPopulationGram
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(Matrix.inv.inv (HansenEconometrics.scoreCovMat mu Z e))))Direct statement dependencies (11)
-
HansenEconometrics.HomoskedasticErrorVariance -
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.conditioningSpace -
HansenEconometrics.conditioningSpace_le -
HansenEconometrics.gmmAsymptoticVarianceStar -
HansenEconometrics.gmmPopulationGram -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedQZZ -
HansenEconometrics.twoSLSCombinedRegressors
theorem HansenEconometrics.twoSLSWeight_is_efficientGMM_of_assumption12_2_homoskedastic
Hansen Theorem 13.6. Under Assumption 12.2 and conditional homoskedasticity, the population 2SLS weight attains the efficient GMM covariance.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {l : Type u_3} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : DecidableEq k] [inst_5 : DecidableEq l] [Nonempty l] {Z : Nat → OmegaSpace → l → Real}
{X : Nat → OmegaSpace → k → Real} {e : Nat → OmegaSpace → Real},
HansenEconometrics.TwoSLSResidualJointIidMixedMomentPositiveCovarianceConditions mu Z X e →
∀ (hZ0 : Measurable (Z 0)) [MeasureTheory.SigmaFinite (mu.trim ⋯)],
HansenEconometrics.HomoskedasticErrorVariance mu Z e →
Eq
(HansenEconometrics.gmmAsymptoticVarianceStar
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(Matrix.inv.inv
(HansenEconometrics.twoSLSCombinedQZZ
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X))))
(HansenEconometrics.scoreCovMat mu Z e))
(Matrix.inv.inv
(HansenEconometrics.gmmPopulationGram
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(Matrix.inv.inv (HansenEconometrics.scoreCovMat mu Z e))))Direct statement dependencies (11)
-
HansenEconometrics.HomoskedasticErrorVariance -
HansenEconometrics.TwoSLSResidualJointIidMixedMomentPositiveCovarianceConditions -
HansenEconometrics.conditioningSpace -
HansenEconometrics.conditioningSpace_le -
HansenEconometrics.gmmAsymptoticVarianceStar -
HansenEconometrics.gmmPopulationGram -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedQZZ -
HansenEconometrics.twoSLSCombinedRegressors
Theorem 13.76 endpoints
If \Omega\succ0, both two-step weights satisfy \hat W_{\mathrm{unc}},\hat W_{\mathrm{cen}}\xrightarrow{p}\Omega^{-1} and give the efficient Gaussian limit.
theorem HansenEconometrics.gmmBetaOrZero_uncenteredTwoStep_tendstoInDistribution_observedRows
Hansen Theorem 13.7, observed-row uncentered form. The two-step GMM estimator using equation (13.8) has the efficient Gaussian limit under the literal observed-row Assumption 12.2 package.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {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 → OmegaSpace → l → Real}
{X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real} {b : k → Real},
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions mu Z X e Y b →
MeasureTheory.TendstoInDistribution
(fun n omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmBetaOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega) (HansenEconometrics.stackOutcomes Y n omega)
(HansenEconometrics.gmmUncenteredTwoStepWeightStar (HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackRegressors X n omega) (HansenEconometrics.stackOutcomes Y n omega)))
b))
Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0
(Matrix.inv.inv
(HansenEconometrics.gmmPopulationGram
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(Matrix.inv.inv (HansenEconometrics.scoreCovMat mu Z e)))))Direct statement dependencies (10)
-
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.gmmBetaOrZero -
HansenEconometrics.gmmPopulationGram -
HansenEconometrics.gmmUncenteredTwoStepWeightStar -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedRegressors
theorem HansenEconometrics.gmmBetaOrZero_centeredTwoStep_tendstoInDistribution_observedRows
Hansen Theorem 13.7, observed-row centered form. The two-step GMM estimator using equation (13.9) has the efficient Gaussian limit under the literal observed-row Assumption 12.2 package.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {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 → OmegaSpace → l → Real}
{X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real} {b : k → Real},
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions mu Z X e Y b →
MeasureTheory.TendstoInDistribution
(fun n omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmBetaOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega) (HansenEconometrics.stackOutcomes Y n omega)
(HansenEconometrics.gmmCenteredTwoStepWeightStar (HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackRegressors X n omega) (HansenEconometrics.stackOutcomes Y n omega)))
b))
Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0
(Matrix.inv.inv
(HansenEconometrics.gmmPopulationGram
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(Matrix.inv.inv (HansenEconometrics.scoreCovMat mu Z e)))))Direct statement dependencies (10)
-
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.gmmBetaOrZero -
HansenEconometrics.gmmCenteredTwoStepWeightStar -
HansenEconometrics.gmmPopulationGram -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedRegressors
theorem HansenEconometrics.gmmBetaOrZero_uncenteredTwoStep_tendstoInDistribution
Hansen Theorem 13.7, uncentered form. The two-step GMM estimator based on equation (13.8) has the efficient Gaussian limit.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {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 → OmegaSpace → l → Real}
{X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real},
HansenEconometrics.TwoSLSResidualJointIidMixedMomentPositiveCovarianceConditions mu Z X e →
∀ (b : k → Real),
(∀ (i : Nat) (omega : OmegaSpace), Eq (Y i omega) (instHAdd.hAdd (dotProduct (X i omega) b) (e i omega))) →
MeasureTheory.TendstoInDistribution
(fun n omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmBetaOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega) (HansenEconometrics.stackOutcomes Y n omega)
(HansenEconometrics.gmmUncenteredTwoStepWeightStar (HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackRegressors X n omega) (HansenEconometrics.stackOutcomes Y n omega)))
b))
Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0
(Matrix.inv.inv
(HansenEconometrics.gmmPopulationGram
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(Matrix.inv.inv (HansenEconometrics.scoreCovMat mu Z e)))))Direct statement dependencies (10)
-
HansenEconometrics.TwoSLSResidualJointIidMixedMomentPositiveCovarianceConditions -
HansenEconometrics.gmmBetaOrZero -
HansenEconometrics.gmmPopulationGram -
HansenEconometrics.gmmUncenteredTwoStepWeightStar -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedRegressors
theorem HansenEconometrics.gmmBetaOrZero_centeredTwoStep_tendstoInDistribution
Hansen Theorem 13.7, centered form. The two-step GMM estimator based on equation (13.9) has the efficient Gaussian limit.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {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 → OmegaSpace → l → Real}
{X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real},
HansenEconometrics.TwoSLSResidualJointIidMixedMomentPositiveCovarianceConditions mu Z X e →
∀ (b : k → Real),
(∀ (i : Nat) (omega : OmegaSpace), Eq (Y i omega) (instHAdd.hAdd (dotProduct (X i omega) b) (e i omega))) →
MeasureTheory.TendstoInDistribution
(fun n omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmBetaOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega) (HansenEconometrics.stackOutcomes Y n omega)
(HansenEconometrics.gmmCenteredTwoStepWeightStar (HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackRegressors X n omega) (HansenEconometrics.stackOutcomes Y n omega)))
b))
Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0
(Matrix.inv.inv
(HansenEconometrics.gmmPopulationGram
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X)))
(Matrix.inv.inv (HansenEconometrics.scoreCovMat mu Z e)))))Direct statement dependencies (10)
-
HansenEconometrics.TwoSLSResidualJointIidMixedMomentPositiveCovarianceConditions -
HansenEconometrics.gmmBetaOrZero -
HansenEconometrics.gmmCenteredTwoStepWeightStar -
HansenEconometrics.gmmPopulationGram -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedRegressors
theorem HansenEconometrics.gmmUncenteredTwoStepWeightStar_tendstoInMeasure
The uncentered two-step weight converges to the efficient weight under the Chapter 12 robust-middle consistency package.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {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 → OmegaSpace → l → Real}
{X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real},
HansenEconometrics.TwoSLSResidualJointIidMixedMomentPositiveCovarianceConditions mu Z X e →
∀ (b : k → Real),
(∀ (i : Nat) (omega : OmegaSpace), Eq (Y i omega) (instHAdd.hAdd (dotProduct (X i omega) b) (e i omega))) →
MeasureTheory.TendstoInMeasure mu
(fun n omega =>
HansenEconometrics.gmmUncenteredTwoStepWeightStar (HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackRegressors X n omega) (HansenEconometrics.stackOutcomes Y n omega))
Filter.atTop fun x => Matrix.inv.inv (HansenEconometrics.scoreCovMat mu Z e)Direct statement dependencies (5)
-
HansenEconometrics.TwoSLSResidualJointIidMixedMomentPositiveCovarianceConditions -
HansenEconometrics.gmmUncenteredTwoStepWeightStar -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.gmmCenteredTwoStepWeightStar_tendstoInMeasure
Hansen’s centered two-step weight converges to the efficient population weight.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {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 → OmegaSpace → l → Real}
{X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real},
HansenEconometrics.TwoSLSResidualJointIidMixedMomentPositiveCovarianceConditions mu Z X e →
∀ (b : k → Real),
(∀ (i : Nat) (omega : OmegaSpace), Eq (Y i omega) (instHAdd.hAdd (dotProduct (X i omega) b) (e i omega))) →
MeasureTheory.TendstoInMeasure mu
(fun n omega =>
HansenEconometrics.gmmCenteredTwoStepWeightStar (HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackRegressors X n omega) (HansenEconometrics.stackOutcomes Y n omega))
Filter.atTop fun x => Matrix.inv.inv (HansenEconometrics.scoreCovMat mu Z e)Direct statement dependencies (5)
-
HansenEconometrics.TwoSLSResidualJointIidMixedMomentPositiveCovarianceConditions -
HansenEconometrics.gmmCenteredTwoStepWeightStar -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 13.82 endpoints
Under the null, the GMM Wald statistic satisfies W(\theta)\xrightarrow{d}\chi_q^2, so its calibrated upper-tail test has asymptotic size \alpha.
theorem HansenEconometrics.gmmWaldStatOrZero_tendstoInDistribution_of_assumption12_2
Hansen Theorem 13.8. Under Assumption 12.2, the Assumption 7.3 restriction linearization, and the null, the GMM Wald statistic converges to chiSquared r.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {l : Type u_3} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : DecidableEq k] [inst_5 : DecidableEq l] {r : Nat} [inst_6 : Fact (instLTNat.lt 0 r)]
{What : Nat → OmegaSpace → Matrix l l Real} {Z : Nat → OmegaSpace → l → Real} {X : Nat → OmegaSpace → k → Real}
{e Y : Nat → OmegaSpace → Real},
HansenEconometrics.TwoSLSGramScoreCLTPositiveCovarianceConditions mu Z X e →
∀ (W : Matrix l l Real),
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (What n) mu) →
(MeasureTheory.TendstoInMeasure mu What Filter.atTop fun x => W) →
W.PosDef →
∀ (b : k → Real),
(∀ (i : Nat) (omega : OmegaSpace),
Eq (Y i omega) (instHAdd.hAdd (dotProduct (X i omega) b) (e i omega))) →
∀ (rfun : (k → Real) → Fin r → Real) (theta0 : Fin r → Real) (Rderiv : Matrix k (Fin r) Real),
Eq (rfun b) theta0 →
(∀ (n : Nat),
AEMeasurable
(fun omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmBetaOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackOutcomes Y n omega) (What n omega))
b))
mu) →
(∀ (n : Nat),
AEMeasurable
(fun omega =>
{
ofLp :=
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(rfun
(HansenEconometrics.gmmBetaOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackOutcomes Y n omega) (What n omega)))
(rfun b)) })
mu) →
(MeasureTheory.TendstoInMeasure mu
(fun n omega =>
instHSub.hSub
{
ofLp :=
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(rfun
(HansenEconometrics.gmmBetaOrZero
(HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackOutcomes Y n omega) (What n omega)))
(rfun b)) }
(ContinuousLinearMap.funLike.coe
(HansenEconometrics.matrixContinuousLinearMap Rderiv.transpose)
{
ofLp :=
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmBetaOrZero
(HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackOutcomes Y n omega) (What n omega))
b) }))
Filter.atTop fun x => 0) →
∀ {VthetaHat : Nat → OmegaSpace → Matrix (Fin r) (Fin r) Real},
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (VthetaHat n) mu) →
(MeasureTheory.TendstoInMeasure mu VthetaHat Filter.atTop fun x =>
Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul Rderiv.transpose
(HansenEconometrics.gmmAsymptoticVarianceStar
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu
(HansenEconometrics.twoSLSCombinedRegressors Z X)))
W (HansenEconometrics.scoreCovMat mu Z e)))
Rderiv) →
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul Rderiv.transpose
(HansenEconometrics.gmmAsymptoticVarianceStar
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu
(HansenEconometrics.twoSLSCombinedRegressors Z X)))
W (HansenEconometrics.scoreCovMat mu Z e)))
Rderiv).PosDef →
MeasureTheory.TendstoInDistribution
(fun n omega =>
HansenEconometrics.gmmWaldStatOrZero
(instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(rfun
(HansenEconometrics.gmmBetaOrZero
(HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackOutcomes Y n omega) (What n omega)))
theta0))
(VthetaHat n omega))
Filter.atTop (fun x => x) (fun x => mu) (HansenEconometrics.chiSquared r)Direct statement dependencies (13)
-
HansenEconometrics.TwoSLSGramScoreCLTPositiveCovarianceConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.gmmAsymptoticVarianceStar -
HansenEconometrics.gmmBetaOrZero -
HansenEconometrics.gmmWaldStatOrZero -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.matrixContinuousLinearMap -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedRegressors
theorem HansenEconometrics.gmmWaldTest_rejectionProb_tendsto_alpha
Size form of Hansen Theorem 13.8. A chi-square critical value with upper tail mass alpha gives asymptotic rejection probability alpha.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {r : Nat} [inst_2 : Fact (instLTNat.lt 0 r)]
{Wald : Nat → OmegaSpace → Real} {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared r) (Set.Ioi crit)) alpha →
MeasureTheory.TendstoInDistribution Wald Filter.atTop (fun x => x) (fun x => mu) (HansenEconometrics.chiSquared r) →
Filter.Tendsto
(fun n => MeasureTheory.Measure.instFunLike.coe mu (setOf fun omega => Real.instLT.lt crit (Wald n omega)))
Filter.atTop (nhds alpha)Direct statement dependencies (2)
-
HansenEconometrics.chiSquared -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat
Theorem 13.92 endpoints
The linearly constrained estimator satisfies \sqrt n(\hat\beta_{\mathrm{CGMM}}-\beta)\xrightarrow{d}N(0,V_{\mathrm{CGMM}}) with covariance (13.18).
theorem HansenEconometrics.gmmConstrainedAsymptoticVariance_eq_hansen_1318
Hansen equation (13.18), expanded into its four textbook terms.
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 q] (Q : Matrix l k Real) (W Omega : Matrix l l Real)
(R : Matrix k q Real),
Eq (HansenEconometrics.gmmPopulationGram Q W).transpose (HansenEconometrics.gmmPopulationGram Q W) →
Eq (HansenEconometrics.gmmConstrainedAsymptoticVariance Q W Omega R)
(instHAdd.hAdd
(instHSub.hSub
(instHSub.hSub (HansenEconometrics.gmmAsymptoticVarianceStar Q W Omega)
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.inv.inv (HansenEconometrics.gmmPopulationGram Q W)) R)
(Matrix.inv.inv
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose
(Matrix.inv.inv (HansenEconometrics.gmmPopulationGram Q W)))
R)))
R.transpose)
(HansenEconometrics.gmmAsymptoticVarianceStar Q W Omega)))
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(HansenEconometrics.gmmAsymptoticVarianceStar Q W Omega) R)
(Matrix.inv.inv
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose
(Matrix.inv.inv (HansenEconometrics.gmmPopulationGram Q W)))
R)))
R.transpose)
(Matrix.inv.inv (HansenEconometrics.gmmPopulationGram Q W))))
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.inv.inv (HansenEconometrics.gmmPopulationGram Q W)) R)
(Matrix.inv.inv
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose
(Matrix.inv.inv (HansenEconometrics.gmmPopulationGram Q W)))
R)))
R.transpose)
(HansenEconometrics.gmmAsymptoticVarianceStar Q W Omega))
R)
(Matrix.inv.inv
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose
(Matrix.inv.inv (HansenEconometrics.gmmPopulationGram Q W)))
R)))
R.transpose)
(Matrix.inv.inv (HansenEconometrics.gmmPopulationGram Q W))))Direct statement dependencies (3)
-
HansenEconometrics.gmmAsymptoticVarianceStar -
HansenEconometrics.gmmConstrainedAsymptoticVariance -
HansenEconometrics.gmmPopulationGram
theorem HansenEconometrics.gmmConstrainedBetaStar_tendstoInDistribution_of_assumption12_2
Hansen Theorem 13.9. Under Assumption 12.2, a linear constrained GMM estimator has the minimum-distance Gaussian limit in equation (13.18).
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {l : Type u_3} {q : Type u_4} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : Fintype q] [inst_5 : DecidableEq k] [inst_6 : DecidableEq l] [inst_7 : DecidableEq q]
{What : Nat → OmegaSpace → Matrix l l Real} {Z : Nat → OmegaSpace → l → Real} {X : Nat → OmegaSpace → k → Real}
{e Y : Nat → OmegaSpace → Real},
HansenEconometrics.TwoSLSGramScoreCLTPositiveCovarianceConditions mu Z X e →
∀ (W : Matrix l l Real),
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (What n) mu) →
(MeasureTheory.TendstoInMeasure mu What Filter.atTop fun x => W) →
W.PosDef →
∀ (R : Matrix k q Real) (c : q → Real),
Function.Injective R.mulVec →
∀ (b : k → Real),
Eq (R.transpose.mulVec b) c →
(∀ (i : Nat) (omega : OmegaSpace),
Eq (Y i omega) (instHAdd.hAdd (dotProduct (X i omega) b) (e i omega))) →
(∀ (n : Nat),
AEMeasurable
(fun omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmBetaOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackOutcomes Y n omega) (What n omega))
b))
mu) →
MeasureTheory.TendstoInDistribution
(fun n omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmConstrainedBetaStar
(HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackOutcomes Y n omega) (What n omega) R c)
b))
Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.gmmConstrainedAsymptoticVariance
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X)))
W (HansenEconometrics.scoreCovMat mu Z e) R))Direct statement dependencies (10)
-
HansenEconometrics.TwoSLSGramScoreCLTPositiveCovarianceConditions -
HansenEconometrics.gmmBetaOrZero -
HansenEconometrics.gmmConstrainedAsymptoticVariance -
HansenEconometrics.gmmConstrainedBetaStar -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedRegressors
Theorem 13.102 endpoints
Efficient constrained GMM satisfies \sqrt n(\hat\beta_{\mathrm{ECGMM}}-\beta)\xrightarrow{d}N(0,V_{\mathrm{ECGMM}}) with covariance (13.20).
theorem HansenEconometrics.gmmEfficientConstrainedAsymptoticVariance_eq_hansen_1320
Hansen equation (13.20), in its displayed covariance form.
Formal statement
∀ {k : Type u_2} {q : Type u_4} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq q] (R : Matrix k q Real)
(V : Matrix k k Real),
Eq (HansenEconometrics.gmmEfficientConstrainedAsymptoticVariance R V)
(instHSub.hSub V
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul V R)
(Matrix.inv.inv
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose V) R)))
R.transpose)
V))Direct statement dependencies (1)
-
HansenEconometrics.gmmEfficientConstrainedAsymptoticVariance
theorem HansenEconometrics.gmmEfficientConstrainedBetaStar_tendstoInDistribution
Hansen Theorem 13.10. A consistent estimate of the unrestricted efficient-GMM covariance gives the efficient constrained Gaussian limit.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {q : Type u_4} [inst_2 : Fintype k]
[inst_3 : Fintype q] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] (root : Nat → Real)
(bhat : Nat → OmegaSpace → k → Real) (Vhat : Nat → OmegaSpace → Matrix k k Real) (V : Matrix k k Real)
(R : Matrix k q Real) (c : q → Real) (b : k → Real),
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (Vhat n) mu) →
(MeasureTheory.TendstoInMeasure mu Vhat Filter.atTop fun x => V) →
V.PosDef →
Function.Injective R.mulVec →
Eq (R.transpose.mulVec b) c →
MeasureTheory.TendstoInDistribution
(fun n omega => instHSMul.hSMul (root n) (instHSub.hSub (bhat n omega) b)) Filter.atTop
(fun z => z.ofLp) (fun x => mu) (ProbabilityTheory.multivariateGaussian 0 V) →
MeasureTheory.TendstoInDistribution
(fun n omega =>
instHSMul.hSMul (root n)
(instHSub.hSub
(HansenEconometrics.gmmEfficientConstrainedBetaStar R c (Vhat n omega) (bhat n omega)) b))
Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.gmmEfficientConstrainedAsymptoticVariance R V))Direct statement dependencies (2)
-
HansenEconometrics.gmmEfficientConstrainedAsymptoticVariance -
HansenEconometrics.gmmEfficientConstrainedBetaStar
Theorem 13.112 endpoints
For smooth restrictions r(\beta)=0, nonlinear constrained GMM has the Chapter 8 Gaussian limit, with efficient covariance when W=\Omega^{-1}.
theorem HansenEconometrics.gmmNonlinearConstrainedBeta_tendstoInDistribution
Hansen Theorem 13.11. A nonlinear constrained GMM estimator has the same first-order minimum-distance limit once Assumption 8.3 supplies its linearization.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {q : Type u_4} [inst_2 : Fintype k]
[inst_3 : Fintype q] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] (root : Nat → Real)
(btilde : Nat → OmegaSpace → k → Real) (b : k → Real) (G : Matrix k k Real) (Rderiv : Matrix k q Real)
(T : Nat → OmegaSpace → k → Real) (V : Matrix k k Real),
V.PosSemidef →
MeasureTheory.TendstoInDistribution T Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0 V) →
HansenEconometrics.ConstrainedEstimatorLinearization mu root btilde b G Rderiv T →
MeasureTheory.TendstoInDistribution (HansenEconometrics.constrainedScaledError root btilde b) Filter.atTop
(fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.mdAsymptoticVariance G Rderiv V))Direct statement dependencies (3)
-
HansenEconometrics.ConstrainedEstimatorLinearization -
HansenEconometrics.constrainedScaledError -
HansenEconometrics.mdAsymptoticVariance
theorem HansenEconometrics.gmmNonlinearEfficientConstrainedBeta_tendstoInDistribution
Efficient specialization of Hansen Theorem 13.11, with covariance V - V R (R’ V R)⁻¹ R’ V.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {q : Type u_4} [inst_2 : Fintype k]
[inst_3 : Fintype q] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] (root : Nat → Real)
(btilde : Nat → OmegaSpace → k → Real) (b : k → Real) (Rderiv : Matrix k q Real) (T : Nat → OmegaSpace → k → Real)
(V : Matrix k k Real),
V.PosDef →
Function.Injective Rderiv.mulVec →
MeasureTheory.TendstoInDistribution T Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0 V) →
HansenEconometrics.ConstrainedEstimatorLinearization mu root btilde b (Matrix.inv.inv V) Rderiv T →
MeasureTheory.TendstoInDistribution (HansenEconometrics.constrainedScaledError root btilde b) Filter.atTop
(fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0
(HansenEconometrics.gmmEfficientConstrainedAsymptoticVariance Rderiv V))Direct statement dependencies (3)
-
HansenEconometrics.ConstrainedEstimatorLinearization -
HansenEconometrics.constrainedScaledError -
HansenEconometrics.gmmEfficientConstrainedAsymptoticVariance
Theorem 13.123 endpoints
Under the null, the efficient criterion distance satisfies D=J(\tilde\beta)-J(\hat\beta)\xrightarrow{d}\chi_q^2, and its calibrated test has asymptotic size \alpha.
theorem HansenEconometrics.gmmUncenteredTwoStepLinearDistanceStatOrZero_tendstoInDistribution_observedRows
Hansen Theorem 13.12, exact linear-restriction observed-row form. Under Assumption 12.2 and the null R’ b = c, the actual common-efficient- weight restricted-minus-unrestricted GMM criterion converges to chi-square with the number of restrictions as degrees of freedom.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {l : Type u_3} {q : Type u_4} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : Fintype q] [inst_5 : DecidableEq k] [inst_6 : DecidableEq l] [inst_7 : DecidableEq q]
[inst_8 : Fact (instLTNat.lt 0 (Fintype.card q))] {Z : Nat → OmegaSpace → l → Real} {X : Nat → OmegaSpace → k → Real}
{e Y : Nat → OmegaSpace → Real} {b : k → Real},
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions mu Z X e Y b →
∀ (R : Matrix k q Real) (c : q → Real),
Function.Injective R.mulVec →
Eq (R.transpose.mulVec b) c →
MeasureTheory.TendstoInDistribution
(fun n omega =>
HansenEconometrics.gmmUncenteredTwoStepLinearDistanceStatOrZero
(HansenEconometrics.stackRegressors X n omega) (HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackOutcomes Y n omega) R c)
Filter.atTop (fun x => x) (fun x => mu) (HansenEconometrics.chiSquared (Fintype.card q))Direct statement dependencies (6)
-
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.gmmUncenteredTwoStepLinearDistanceStatOrZero -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.gmmUncenteredTwoStepLinearDistanceTest_rejectionProb_tendsto_alpha_observedRows
Asymptotic-size conclusion for the exact linear-restriction form of Hansen Theorem 13.12.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {l : Type u_3} {q : Type u_4} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : Fintype q] [inst_5 : DecidableEq k] [inst_6 : DecidableEq l] [inst_7 : DecidableEq q]
[Fact (instLTNat.lt 0 (Fintype.card q))] {Z : Nat → OmegaSpace → l → Real} {X : Nat → OmegaSpace → k → Real}
{e Y : Nat → OmegaSpace → Real} {b : k → Real} {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared (Fintype.card q)) (Set.Ioi crit)) alpha →
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions mu Z X e Y b →
∀ (R : Matrix k q Real) (c : q → Real),
Function.Injective R.mulVec →
Eq (R.transpose.mulVec b) c →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe mu
(setOf fun omega =>
Real.instLT.lt crit
(HansenEconometrics.gmmUncenteredTwoStepLinearDistanceStatOrZero
(HansenEconometrics.stackRegressors X n omega) (HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackOutcomes Y n omega) R c)))
Filter.atTop (nhds alpha)Direct statement dependencies (5)
-
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.gmmUncenteredTwoStepLinearDistanceStatOrZero -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.gmmUncenteredTwoStepDistanceStatOrZero_tendstoInDistribution_observedRows_of_linearization
Conditional nonlinear observed-row endpoint toward Hansen Theorem 13.12.
h73 is Hansen Assumption 7.3, while hlinear is an additional optimizer regularity premise: it records the first-order expansion of the supplied nonlinear constrained GMM estimator and is not implied by Assumption 7.3 alone. The exact linear-restriction endpoint below derives this expansion from the concrete constrained estimator.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {l : Type u_3} {q : Type u_4} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : Fintype q] [inst_5 : DecidableEq k] [inst_6 : DecidableEq l] [inst_7 : DecidableEq q]
[inst_8 : Fact (instLTNat.lt 0 (Fintype.card q))] {Z : Nat → OmegaSpace → l → Real} {X : Nat → OmegaSpace → k → Real}
{e Y : Nat → OmegaSpace → Real} {b : k → Real},
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions mu Z X e Y b →
∀ (rfun : (k → Real) → q → Real) (theta0 : q → Real) (Rderiv : Matrix k q Real)
(btilde : Nat → OmegaSpace → k → Real) (h73 : HansenEconometrics.SmoothFunctionCondition rfun b Rderiv),
Eq (rfun b) theta0 →
(∀ (n : Nat) (omega : OmegaSpace), Eq (rfun (btilde n omega)) theta0) →
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (btilde n) mu) →
(have Q :=
HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Z X));
have G := HansenEconometrics.gmmPopulationGram Q (Matrix.inv.inv (HansenEconometrics.scoreCovMat mu Z e));
HansenEconometrics.ConstrainedEstimatorLinearization mu (fun n => n.cast.sqrt) btilde b G Rderiv
fun n omega =>
instHSMul.hSMul n.cast.sqrt
(instHSub.hSub
(HansenEconometrics.gmmUncenteredTwoStepBetaOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega) (HansenEconometrics.stackOutcomes Y n omega))
b)) →
MeasureTheory.TendstoInDistribution
(fun n omega =>
HansenEconometrics.gmmUncenteredTwoStepDistanceStatOrZero
(HansenEconometrics.stackRegressors X n omega) (HansenEconometrics.stackRegressors Z n omega)
(HansenEconometrics.stackOutcomes Y n omega) (btilde n omega))
Filter.atTop (fun x => x) (fun x => mu) (HansenEconometrics.chiSquared (Fintype.card q))Direct statement dependencies (14)
-
HansenEconometrics.ConstrainedEstimatorLinearization -
HansenEconometrics.SmoothFunctionCondition -
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.gmmPopulationGram -
HansenEconometrics.gmmUncenteredTwoStepBetaOrZero -
HansenEconometrics.gmmUncenteredTwoStepDistanceStatOrZero -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.popGram -
HansenEconometrics.scoreCovMat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedRegressors
Theorem 13.132 endpoints
With a common weight, D\ge0; for linear restrictions and the efficient common weight, D=W.
theorem HansenEconometrics.gmmDistanceStat_nonneg_of_commonWeight
Hansen Theorem 13.13, first clause. With a common weight matrix, the constrained criterion cannot be below the unrestricted GMM minimum.
Formal statement
∀ {n : Type u_1} {k : Type u_2} {l : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype l] [Nonempty n]
[inst_4 : DecidableEq k] (X : Matrix n k Real) (Z : Matrix n l Real) (y : n → Real) (W : Matrix l l Real)
(btilde : k → Real) [Invertible (HansenEconometrics.gmmNormalizedGram X Z W)],
W.PosSemidef →
Real.instLE.le 0 (HansenEconometrics.gmmDistanceStat X Z y W btilde (HansenEconometrics.gmmBetaOrZero X Z y W))Direct statement dependencies (3)
-
HansenEconometrics.gmmBetaOrZero -
HansenEconometrics.gmmDistanceStat -
HansenEconometrics.gmmNormalizedGram
theorem HansenEconometrics.gmmDistanceStat_eq_wald_of_linear_commonWeight
Hansen Theorem 13.13, second clause. With a common efficient weight and a linear restriction, the GMM distance statistic equals the Wald statistic exactly.
Formal statement
∀ {n : Type u_1} {k : Type u_2} {l : Type u_3} {r : Nat} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype l]
[Nonempty n] [inst_4 : DecidableEq k] (X : Matrix n k Real) (Z : Matrix n l Real) (y : n → Real) (W : Matrix l l Real)
(R : Matrix k (Fin r) Real) (c : Fin r → Real),
W.PosSemidef →
(HansenEconometrics.gmmNormalizedGram X Z W).PosDef →
Function.Injective R.mulVec →
Eq
(HansenEconometrics.gmmDistanceStat X Z y W (HansenEconometrics.gmmConstrainedBetaStar X Z y W R c)
(HansenEconometrics.gmmBetaOrZero X Z y W))
(HansenEconometrics.restrictionWaldStatOrZero
(instHSMul.hSMul (Fintype.card n).cast.sqrt
(instHSub.hSub (R.transpose.mulVec (HansenEconometrics.gmmBetaOrZero X Z y W)) c))
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose
(Matrix.inv.inv (HansenEconometrics.gmmNormalizedGram X Z W)))
R))Direct statement dependencies (5)
-
HansenEconometrics.gmmBetaOrZero -
HansenEconometrics.gmmConstrainedBetaStar -
HansenEconometrics.gmmDistanceStat -
HansenEconometrics.gmmNormalizedGram -
HansenEconometrics.restrictionWaldStatOrZero
Theorem 13.143 endpoints
The efficient two-step overidentification statistic satisfies J(\hat\beta)\xrightarrow{d}\chi^2_{\ell-k}, and its calibrated test has asymptotic size \alpha.
theorem HansenEconometrics.gmmUncenteredTwoStepJStatOrZero_tendstoInDistribution_observedRows
Hansen Theorem 13.14, observed-row form. Under the literal observed-row Assumption 12.2 package, the efficient two-step GMM criterion at the GMM estimator converges to chiSquared (card l - card k).
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {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 → OmegaSpace → l → Real}
{X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real} {b : k → Real}
[inst_6 : Fact (instLTNat.lt 0 (instHSub.hSub (Fintype.card l) (Fintype.card k)))],
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions mu Z X e Y b →
MeasureTheory.TendstoInDistribution
(fun n omega =>
HansenEconometrics.gmmUncenteredTwoStepJStatOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega) (HansenEconometrics.stackOutcomes Y n omega))
Filter.atTop (fun x => x) (fun x => mu)
(HansenEconometrics.chiSquared (instHSub.hSub (Fintype.card l) (Fintype.card k)))Direct statement dependencies (6)
-
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.gmmUncenteredTwoStepJStatOrZero -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.gmmUncenteredTwoStepJTest_rejectionProb_tendsto_alpha_observedRows
Asymptotic-size conclusion in Hansen Theorem 13.14 for the actual efficient two-step GMM overidentification criterion.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {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 → OmegaSpace → l → Real}
{X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real} {b : k → Real}
[Fact (instLTNat.lt 0 (instHSub.hSub (Fintype.card l) (Fintype.card k)))] {crit : Real} {alpha : ENNReal},
Eq
(MeasureTheory.Measure.instFunLike.coe
(HansenEconometrics.chiSquared (instHSub.hSub (Fintype.card l) (Fintype.card k))) (Set.Ioi crit))
alpha →
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions mu Z X e Y b →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe mu
(setOf fun omega =>
Real.instLT.lt crit
(HansenEconometrics.gmmUncenteredTwoStepJStatOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Z n omega) (HansenEconometrics.stackOutcomes Y n omega))))
Filter.atTop (nhds alpha)Direct statement dependencies (5)
-
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.gmmUncenteredTwoStepJStatOrZero -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.gmmJStatOrZero_tendstoInDistribution_chiSquared_of_factorSymmIdem
Generic Gaussian factor/symmetric-idempotent specialization of the feasible-quadratic transfer engine used by Hansen Theorem 13.14.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {l : Type u_2} [inst_2 : Fintype l] [inst_3 : DecidableEq l]
{df : Nat} [inst_4 : Fact (instLTNat.lt 0 df)] {T : Nat → OmegaSpace → l → Real}
{OmegaHat : Nat → OmegaSpace → Matrix l l Real} {Omega B : Matrix l l Real},
MeasureTheory.TendstoInDistribution T Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0 (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul B B.transpose)) →
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (OmegaHat n) mu) →
(MeasureTheory.TendstoInMeasure mu OmegaHat Filter.atTop fun x => Omega) →
Omega.PosDef →
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul B.transpose (Matrix.inv.inv Omega)) B).IsHermitian →
IsIdempotentElem
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul B.transpose (Matrix.inv.inv Omega)) B) →
Eq
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul B.transpose (Matrix.inv.inv Omega)) B).rank
df →
MeasureTheory.TendstoInDistribution
(fun n omega => HansenEconometrics.gmmJStatOrZero (T n omega) (OmegaHat n omega)) Filter.atTop
(fun x => x) (fun x => mu) (HansenEconometrics.chiSquared df)Direct statement dependencies (3)
-
HansenEconometrics.chiSquared -
HansenEconometrics.gmmJStatOrZero -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat
Theorem 13.153 endpoints
For Z=(Z_a,Z_b), the subset statistic C=\hat J-\tilde J\xrightarrow{d}\chi^2_{\ell_b} under full rank of \mathbb E[Z_aX'].
def HansenEconometrics.gmmUncenteredTwoStepSubsetJStatOrZero
Hansen’s subset overidentification statistic formed from the efficient two-step GMM criteria for the full and maintained instrument sets.
Formal statement
{n : Type u_1} →
{k : Type u_2} →
{la : Type u_3} →
{lb : Type u_4} →
[Fintype n] →
[Fintype k] →
[Fintype la] →
[Fintype lb] →
[DecidableEq k] →
[DecidableEq la] →
[DecidableEq lb] → Matrix n k Real → Matrix n la Real → Matrix n lb Real → (n → Real) → Real
theorem HansenEconometrics.gmmUncenteredTwoStepSubsetJStatOrZero_tendstoInDistribution_observedRows
Hansen Theorem 13.15, observed-row form. Under Assumption 12.2 for the full instrument vector and full rank of the maintained moment derivative, the full-minus-maintained efficient-GMM criterion converges to chi-square with degrees of freedom equal to the number of tested moments. This result is slightly more general than Hansen’s displayed context because it also covers an exactly identified maintained model.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {la : Type u_3} {lb : Type u_4} [inst_2 : Fintype k]
[inst_3 : Fintype la] [inst_4 : Fintype lb] [inst_5 : DecidableEq k] [inst_6 : DecidableEq la]
[inst_7 : DecidableEq lb] {Za : Nat → OmegaSpace → la → Real} {Zb : Nat → OmegaSpace → lb → Real}
{X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real} {b : k → Real}
[inst_8 : Fact (instLTNat.lt 0 (Fintype.card lb))],
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions mu
(fun i omega => Sum.elim (Za i omega) (Zb i omega)) X e Y b →
Function.Injective
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Za X))).mulVec →
MeasureTheory.TendstoInDistribution
(fun n omega =>
HansenEconometrics.gmmUncenteredTwoStepSubsetJStatOrZero (HansenEconometrics.stackRegressors X n omega)
(HansenEconometrics.stackRegressors Za n omega) (HansenEconometrics.stackRegressors Zb n omega)
(HansenEconometrics.stackOutcomes Y n omega))
Filter.atTop (fun x => x) (fun x => mu) (HansenEconometrics.chiSquared (Fintype.card lb))Direct statement dependencies (9)
-
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.gmmUncenteredTwoStepSubsetJStatOrZero -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.popGram -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedRegressors
theorem HansenEconometrics.gmmUncenteredTwoStepSubsetJTest_rejectionProb_tendsto_alpha_observedRows
Asymptotic-size conclusion in Hansen Theorem 13.15 for the actual full-minus-maintained efficient two-step GMM criterion.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {la : Type u_3} {lb : Type u_4} [inst_2 : Fintype k]
[inst_3 : Fintype la] [inst_4 : Fintype lb] [inst_5 : DecidableEq k] [inst_6 : DecidableEq la]
[inst_7 : DecidableEq lb] {Za : Nat → OmegaSpace → la → Real} {Zb : Nat → OmegaSpace → lb → Real}
{X : Nat → OmegaSpace → k → Real} {e Y : Nat → OmegaSpace → Real} {b : k → Real}
[Fact (instLTNat.lt 0 (Fintype.card lb))] {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared (Fintype.card lb)) (Set.Ioi crit)) alpha →
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions mu
(fun i omega => Sum.elim (Za i omega) (Zb i omega)) X e Y b →
Function.Injective
(HansenEconometrics.twoSLSCombinedQZX
(HansenEconometrics.popGram mu (HansenEconometrics.twoSLSCombinedRegressors Za X))).mulVec →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe mu
(setOf fun omega =>
Real.instLT.lt crit
(HansenEconometrics.gmmUncenteredTwoStepSubsetJStatOrZero
(HansenEconometrics.stackRegressors X n omega) (HansenEconometrics.stackRegressors Za n omega)
(HansenEconometrics.stackRegressors Zb n omega) (HansenEconometrics.stackOutcomes Y n omega))))
Filter.atTop (nhds alpha)Direct statement dependencies (8)
-
HansenEconometrics.TwoSLSObservedIidFourthMomentPositiveCovarianceConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.gmmUncenteredTwoStepSubsetJStatOrZero -
HansenEconometrics.popGram -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors -
HansenEconometrics.twoSLSCombinedQZX -
HansenEconometrics.twoSLSCombinedRegressors
Theorem 13.163 endpoints
In Y=Z_1'\beta_1+Y_2'\beta_2+e, the endogeneity statistic comparing instruments (Z_1,Z_2,Y_2) and (Z_1,Z_2) satisfies C\xrightarrow{d}\chi^2_{k_2}.
def HansenEconometrics.gmmEndogeneityTwoStepStatOrZero
Hansen’s Theorem 13.16 criterion difference: efficient two-step GMM with instruments (Z₁,Z₂,Y₂) minus efficient two-step GMM with (Z₁,Z₂), both using regressors (Z₁,Y₂).
Formal statement
{n : Type u_1} →
{k1 : Type u_2} →
{k2 : Type u_3} →
{l2 : Type u_4} →
[Fintype n] →
[Fintype k1] →
[Fintype k2] →
[Fintype l2] →
[DecidableEq k1] →
[DecidableEq k2] →
[DecidableEq l2] → Matrix n k1 Real → Matrix n k2 Real → Matrix n l2 Real → (n → Real) → Real
theorem HansenEconometrics.gmmEndogeneityTwoStepStatOrZero_tendstoInDistribution_observedRows
Hansen Theorem 13.16, observed-row form. The actual full-minus- maintained two-step GMM criterion for testing exogeneity of Y₂ converges to chi-square with k₂ degrees of freedom.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k1 : Type u_2} {k2 : Type u_3} {l2 : Type u_4} [inst_2 : Fintype k1]
[inst_3 : Fintype k2] [inst_4 : Fintype l2] [inst_5 : DecidableEq k1] [inst_6 : DecidableEq k2]
[inst_7 : DecidableEq l2] {Z1 : Nat → OmegaSpace → k1 → Real} {Z2 : Nat → OmegaSpace → l2 → Real}
{Y2 : Nat → OmegaSpace → k2 → Real} {e Y : Nat → OmegaSpace → Real} {b : Sum k1 k2 → Real}
[inst_8 : Fact (instLTNat.lt 0 (Fintype.card k2))],
HansenEconometrics.GMMEndogeneityObservedRowsConditions mu Z1 Z2 Y2 e Y b →
MeasureTheory.TendstoInDistribution
(fun n omega =>
HansenEconometrics.gmmEndogeneityTwoStepStatOrZero (HansenEconometrics.stackRegressors Z1 n omega)
(HansenEconometrics.stackRegressors Y2 n omega) (HansenEconometrics.stackRegressors Z2 n omega)
(HansenEconometrics.stackOutcomes Y n omega))
Filter.atTop (fun x => x) (fun x => mu) (HansenEconometrics.chiSquared (Fintype.card k2))Direct statement dependencies (6)
-
HansenEconometrics.GMMEndogeneityObservedRowsConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.gmmEndogeneityTwoStepStatOrZero -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.gmmEndogeneityTwoStepTest_rejectionProb_tendsto_alpha_observedRows
Asymptotic-size conclusion in Hansen Theorem 13.16 for the concrete observed-row endogeneity statistic.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k1 : Type u_2} {k2 : Type u_3} {l2 : Type u_4} [inst_2 : Fintype k1]
[inst_3 : Fintype k2] [inst_4 : Fintype l2] [inst_5 : DecidableEq k1] [inst_6 : DecidableEq k2]
[inst_7 : DecidableEq l2] {Z1 : Nat → OmegaSpace → k1 → Real} {Z2 : Nat → OmegaSpace → l2 → Real}
{Y2 : Nat → OmegaSpace → k2 → Real} {e Y : Nat → OmegaSpace → Real} {b : Sum k1 k2 → Real}
[Fact (instLTNat.lt 0 (Fintype.card k2))] {crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared (Fintype.card k2)) (Set.Ioi crit)) alpha →
HansenEconometrics.GMMEndogeneityObservedRowsConditions mu Z1 Z2 Y2 e Y b →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe mu
(setOf fun omega =>
Real.instLT.lt crit
(HansenEconometrics.gmmEndogeneityTwoStepStatOrZero (HansenEconometrics.stackRegressors Z1 n omega)
(HansenEconometrics.stackRegressors Y2 n omega) (HansenEconometrics.stackRegressors Z2 n omega)
(HansenEconometrics.stackOutcomes Y n omega))))
Filter.atTop (nhds alpha)Direct statement dependencies (5)
-
HansenEconometrics.GMMEndogeneityObservedRowsConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.gmmEndogeneityTwoStepStatOrZero -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Theorem 13.173 endpoints
In Y=Z_1'\beta_1+Y_2'\beta_2+Y_3'\beta_3+e, the subset test for Y_2 satisfies C\xrightarrow{d}\chi^2_{k_2}.
def HansenEconometrics.gmmSubsetEndogeneityTwoStepStatOrZero
Hansen’s Theorem 13.17 criterion difference: efficient two-step GMM with instruments (Z₁,Z₂,Y₂) minus efficient two-step GMM with (Z₁,Z₂), both using regressors (Z₁,Y₂,Y₃).
Formal statement
{n : Type u_1} →
{k1 : Type u_2} →
{k2 : Type u_3} →
{k3 : Type u_4} →
{l2 : Type u_5} →
[Fintype n] →
[Fintype k1] →
[Fintype k2] →
[Fintype k3] →
[Fintype l2] →
[DecidableEq k1] →
[DecidableEq k2] →
[DecidableEq k3] →
[DecidableEq l2] →
Matrix n k1 Real →
Matrix n k2 Real → Matrix n k3 Real → Matrix n l2 Real → (n → Real) → Real
theorem HansenEconometrics.gmmSubsetEndogeneityTwoStepStatOrZero_tendstoInDistribution_observedRows
Hansen Theorem 13.17, observed-row form. The actual full-minus- maintained two-step GMM criterion for testing the Y₂ block while retaining endogenous block Y₃ converges to chi-square with k₂ degrees of freedom.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k1 : Type u_2} {k2 : Type u_3} {k3 : Type u_4} {l2 : Type u_5}
[inst_2 : Fintype k1] [inst_3 : Fintype k2] [inst_4 : Fintype k3] [inst_5 : Fintype l2] [inst_6 : DecidableEq k1]
[inst_7 : DecidableEq k2] [inst_8 : DecidableEq k3] [inst_9 : DecidableEq l2] {Z1 : Nat → OmegaSpace → k1 → Real}
{Z2 : Nat → OmegaSpace → l2 → Real} {Y2 : Nat → OmegaSpace → k2 → Real} {Y3 : Nat → OmegaSpace → k3 → Real}
{e Y : Nat → OmegaSpace → Real} {b : Sum k1 (Sum k2 k3) → Real} [inst_10 : Fact (instLTNat.lt 0 (Fintype.card k2))],
HansenEconometrics.GMMSubsetEndogeneityObservedRowsConditions mu Z1 Z2 Y2 Y3 e Y b →
MeasureTheory.TendstoInDistribution
(fun n omega =>
HansenEconometrics.gmmSubsetEndogeneityTwoStepStatOrZero (HansenEconometrics.stackRegressors Z1 n omega)
(HansenEconometrics.stackRegressors Y2 n omega) (HansenEconometrics.stackRegressors Y3 n omega)
(HansenEconometrics.stackRegressors Z2 n omega) (HansenEconometrics.stackOutcomes Y n omega))
Filter.atTop (fun x => x) (fun x => mu) (HansenEconometrics.chiSquared (Fintype.card k2))Direct statement dependencies (6)
-
HansenEconometrics.GMMSubsetEndogeneityObservedRowsConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.gmmSubsetEndogeneityTwoStepStatOrZero -
HansenEconometrics.instIsProbabilityMeasureRealChiSquaredOfFactLtNatOfNat -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
theorem HansenEconometrics.gmmSubsetEndogeneityTwoStepTest_rejectionProb_tendsto_alpha_observedRows
Asymptotic-size conclusion in Hansen Theorem 13.17 for the concrete observed-row subset-endogeneity statistic.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k1 : Type u_2} {k2 : Type u_3} {k3 : Type u_4} {l2 : Type u_5}
[inst_2 : Fintype k1] [inst_3 : Fintype k2] [inst_4 : Fintype k3] [inst_5 : Fintype l2] [inst_6 : DecidableEq k1]
[inst_7 : DecidableEq k2] [inst_8 : DecidableEq k3] [inst_9 : DecidableEq l2] {Z1 : Nat → OmegaSpace → k1 → Real}
{Z2 : Nat → OmegaSpace → l2 → Real} {Y2 : Nat → OmegaSpace → k2 → Real} {Y3 : Nat → OmegaSpace → k3 → Real}
{e Y : Nat → OmegaSpace → Real} {b : Sum k1 (Sum k2 k3) → Real} [Fact (instLTNat.lt 0 (Fintype.card k2))]
{crit : Real} {alpha : ENNReal},
Eq (MeasureTheory.Measure.instFunLike.coe (HansenEconometrics.chiSquared (Fintype.card k2)) (Set.Ioi crit)) alpha →
HansenEconometrics.GMMSubsetEndogeneityObservedRowsConditions mu Z1 Z2 Y2 Y3 e Y b →
Filter.Tendsto
(fun n =>
MeasureTheory.Measure.instFunLike.coe mu
(setOf fun omega =>
Real.instLT.lt crit
(HansenEconometrics.gmmSubsetEndogeneityTwoStepStatOrZero
(HansenEconometrics.stackRegressors Z1 n omega) (HansenEconometrics.stackRegressors Y2 n omega)
(HansenEconometrics.stackRegressors Y3 n omega) (HansenEconometrics.stackRegressors Z2 n omega)
(HansenEconometrics.stackOutcomes Y n omega))))
Filter.atTop (nhds alpha)Direct statement dependencies (5)
-
HansenEconometrics.GMMSubsetEndogeneityObservedRowsConditions -
HansenEconometrics.chiSquared -
HansenEconometrics.gmmSubsetEndogeneityTwoStepStatOrZero -
HansenEconometrics.stackOutcomes -
HansenEconometrics.stackRegressors
Proposition 13.12 endpoints
A nonlinear GMM estimator satisfies \sqrt n(\hat\beta-\beta)\xrightarrow{d}N(0,V) with sandwich covariance; efficient weighting gives V=(Q'\Omega^{-1}Q)^{-1}.
theorem HansenEconometrics.nonlinearGMMBeta_tendstoInDistribution
Hansen Proposition 13.1. A nonlinear GMM estimator with the standard first-order expansion has the sandwich Gaussian limit.
Here Q is the derivative of the population moment. Therefore, the linearization uses the negative GMM influence matrix. Its sign cancels from the covariance.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {l : Type u_3} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : DecidableEq k] [inst_5 : DecidableEq l] (bhat : Nat → OmegaSpace → k → Real)
(b : k → Real) (score : Nat → OmegaSpace → l → Real) (Q : Matrix l k Real) (W Omega : Matrix l l Real),
Omega.PosSemidef →
MeasureTheory.TendstoInDistribution score Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0 Omega) →
(∀ (n : Nat),
AEMeasurable (fun omega => { ofLp := instHSMul.hSMul n.cast.sqrt (instHSub.hSub (bhat n omega) b) }) mu) →
(MeasureTheory.TendstoInMeasure mu
(fun n omega =>
instHSub.hSub { ofLp := instHSMul.hSMul n.cast.sqrt (instHSub.hSub (bhat n omega) b) }
(ContinuousLinearMap.funLike.coe
(HansenEconometrics.matrixContinuousLinearMap
(Matrix.neg.neg (HansenEconometrics.LinearGMM.influenceMatrixStar Q W)))
{ ofLp := score n omega }))
Filter.atTop fun x => 0) →
MeasureTheory.TendstoInDistribution
(fun n omega => instHSMul.hSMul n.cast.sqrt (instHSub.hSub (bhat n omega) b)) Filter.atTop (fun z => z.ofLp)
(fun x => mu)
(ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.gmmAsymptoticVarianceStar Q W Omega))Direct statement dependencies (3)
-
HansenEconometrics.LinearGMM.influenceMatrixStar -
HansenEconometrics.gmmAsymptoticVarianceStar -
HansenEconometrics.matrixContinuousLinearMap
theorem HansenEconometrics.nonlinearGMMBeta_tendstoInDistribution_efficient
Efficient-weight form of Hansen Proposition 13.1. With a positive-definite moment covariance and a full-rank derivative, the sandwich covariance reduces to (Q’ Omega⁻¹ Q)⁻¹.
Formal statement
∀ {OmegaSpace : Type u_1} [inst : MeasurableSpace OmegaSpace] {mu : MeasureTheory.Measure OmegaSpace}
[inst_1 : MeasureTheory.IsProbabilityMeasure mu] {k : Type u_2} {l : Type u_3} [inst_2 : Fintype k]
[inst_3 : Fintype l] [inst_4 : DecidableEq k] [inst_5 : DecidableEq l] (bhat : Nat → OmegaSpace → k → Real)
(b : k → Real) (score : Nat → OmegaSpace → l → Real) (Q : Matrix l k Real) (Omega : Matrix l l Real),
Omega.PosDef →
Function.Injective Q.mulVec →
MeasureTheory.TendstoInDistribution score Filter.atTop (fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0 Omega) →
(∀ (n : Nat),
AEMeasurable (fun omega => { ofLp := instHSMul.hSMul n.cast.sqrt (instHSub.hSub (bhat n omega) b) }) mu) →
(MeasureTheory.TendstoInMeasure mu
(fun n omega =>
instHSub.hSub { ofLp := instHSMul.hSMul n.cast.sqrt (instHSub.hSub (bhat n omega) b) }
(ContinuousLinearMap.funLike.coe
(HansenEconometrics.matrixContinuousLinearMap
(Matrix.neg.neg (HansenEconometrics.LinearGMM.influenceMatrixStar Q (Matrix.inv.inv Omega))))
{ ofLp := score n omega }))
Filter.atTop fun x => 0) →
MeasureTheory.TendstoInDistribution
(fun n omega => instHSMul.hSMul n.cast.sqrt (instHSub.hSub (bhat n omega) b)) Filter.atTop
(fun z => z.ofLp) (fun x => mu)
(ProbabilityTheory.multivariateGaussian 0
(Matrix.inv.inv (HansenEconometrics.gmmPopulationGram Q (Matrix.inv.inv Omega))))Direct statement dependencies (3)
-
HansenEconometrics.LinearGMM.influenceMatrixStar -
HansenEconometrics.gmmPopulationGram -
HansenEconometrics.matrixContinuousLinearMap