Chapter 8: Restricted Estimation

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

This page is generated from the canonical Chapter 8 inventory and the compiled Lean environment. It contains 18 textbook result groups and 94 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 8.16 of 9 linked endpoints

For R'\beta=c, constrained least squares has R'\tilde\beta_{\mathrm{CLS}}=c and \tilde e=(I-P+XAX')e; the residual maker is symmetric and idempotent with rank n-k+q.

theorem HansenEconometrics.clsBeta_linear_model

Hansen Theorem 8.1 coefficient decomposition in the linear model.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq k] [inst_4 : DecidableEq q] (X : Matrix n k Real) (β : k → Real) (e : n → Real)
  (R : Matrix k q Real) (c : q → Real)
  [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_6 : Invertible (HansenEconometrics.clsConstraintGram X R)],
  Eq (R.transpose.mulVec β) c →
    Eq (HansenEconometrics.clsBeta X (instHAdd.hAdd (X.mulVec β) e) R c)
      (instHAdd.hAdd β
        ((instHSub.hSub
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                (inst_5.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)) X.transpose)
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.clsCorrectionMatrix X R)
                X.transpose)).mulVec
          e))

Direct statement dependencies (3)

HansenEconometrics.clsBeta
HansenEconometrics.clsConstraintGram
HansenEconometrics.clsCorrectionMatrix

HansenEconometrics/Chapter8RestrictedEstimation.lean:100

theorem HansenEconometrics.clsResidual_linear_model

Hansen Theorem 8.1 residual decomposition in the linear model.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] (X : Matrix n k Real) (β : k → Real)
  (e : n → Real) (R : Matrix k q Real) (c : q → Real)
  [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_7 : Invertible (HansenEconometrics.clsConstraintGram X R)],
  Eq (R.transpose.mulVec β) c →
    Eq (HansenEconometrics.clsResidual X (instHAdd.hAdd (X.mulVec β) e) R c)
      ((HansenEconometrics.clsProjectionMatrix X R).mulVec e)

Direct statement dependencies (3)

HansenEconometrics.clsConstraintGram
HansenEconometrics.clsProjectionMatrix
HansenEconometrics.clsResidual

HansenEconometrics/Chapter8RestrictedEstimation.lean:113

theorem HansenEconometrics.clsProjectionMatrix_rank

Hansen Theorem 8.1: the rank of the CLS residual-maker is n - k + q.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] (X : Matrix n k Real) (R : Matrix k q Real)
  [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_7 : Invertible (HansenEconometrics.clsConstraintGram X R)],
  Eq (HansenEconometrics.clsProjectionMatrix X R).rank
    (instHAdd.hAdd (instHSub.hSub (Fintype.card n) (Fintype.card k)) (Fintype.card q))

Direct statement dependencies (2)

HansenEconometrics.clsConstraintGram
HansenEconometrics.clsProjectionMatrix

HansenEconometrics/Chapter8RestrictedEstimation.lean:273

theorem HansenEconometrics.clsProjectionMatrix_trace

Hansen Theorem 8.1: trace of the CLS residual-maker matrix.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] (X : Matrix n k Real) (R : Matrix k q Real)
  [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_7 : Invertible (HansenEconometrics.clsConstraintGram X R)],
  Eq (HansenEconometrics.clsProjectionMatrix X R).trace
    (instHAdd.hAdd (instHSub.hSub (Fintype.card n).cast (Fintype.card k).cast) (Fintype.card q).cast)

Direct statement dependencies (2)

HansenEconometrics.clsConstraintGram
HansenEconometrics.clsProjectionMatrix

HansenEconometrics/Chapter8RestrictedEstimation.lean:231

theorem HansenEconometrics.clsProjectionMatrix_transpose

Hansen Theorem 8.1: symmetry of the CLS residual-maker matrix.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] (X : Matrix n k Real) (R : Matrix k q Real)
  [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_7 : Invertible (HansenEconometrics.clsConstraintGram X R)],
  Eq (HansenEconometrics.clsProjectionMatrix X R).transpose (HansenEconometrics.clsProjectionMatrix X R)

Direct statement dependencies (2)

HansenEconometrics.clsConstraintGram
HansenEconometrics.clsProjectionMatrix

HansenEconometrics/Chapter8RestrictedEstimation.lean:184

theorem HansenEconometrics.clsProjectionMatrix_idempotent

Hansen Theorem 8.1: the CLS residual-maker matrix is idempotent.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] (X : Matrix n k Real) (R : Matrix k q Real)
  [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_7 : Invertible (HansenEconometrics.clsConstraintGram X R)],
  Eq
    (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.clsProjectionMatrix X R)
      (HansenEconometrics.clsProjectionMatrix X R))
    (HansenEconometrics.clsProjectionMatrix X R)

Direct statement dependencies (2)

HansenEconometrics.clsConstraintGram
HansenEconometrics.clsProjectionMatrix

HansenEconometrics/Chapter8RestrictedEstimation.lean:201

Theorem 8.22 endpoints

Under conditional mean zero, \mathbb E[\tilde\beta_{\mathrm{CLS}}\mid X]=\beta.

theorem HansenEconometrics.cls_condExp_unbiased

Hansen Theorem 8.2 conditional-unbiasedness bridge for CLS.

The stochastic input is the conditional mean of the linear CLS error term, while the theorem rewrites the estimator itself using clsBeta_linear_model.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq k] [inst_4 : DecidableEq q] {Ω : Type u_4} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real) (R : Matrix k q Real) (c : q → Real)
  [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_6 : Invertible (HansenEconometrics.clsConstraintGram X R)],
  Eq (R.transpose.mulVec β) c →
    ((MeasureTheory.ae μ).EventuallyEq
        (MeasureTheory.condExp m μ fun ω =>
          instHAdd.hAdd β
            ((instHSub.hSub
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                    (inst_5.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)) X.transpose)
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.clsCorrectionMatrix X R)
                    X.transpose)).mulVec
              (e ω)))
        fun x => β) →
      (MeasureTheory.ae μ).EventuallyEq
        (MeasureTheory.condExp m μ fun ω => HansenEconometrics.clsBeta X (instHAdd.hAdd (X.mulVec β) (e ω)) R c)
        fun x => β

Direct statement dependencies (3)

HansenEconometrics.clsBeta
HansenEconometrics.clsConstraintGram
HansenEconometrics.clsCorrectionMatrix

HansenEconometrics/Chapter8RestrictedEstimation.lean:290

theorem HansenEconometrics.cls_condExp_unbiased_of_error_zero

Hansen Theorem 8.2 conditional unbiasedness from coordinatewise mean-zero errors.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq k] [inst_4 : DecidableEq q] {Ω : Type u_4} {m m₀ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real) (R : Matrix k q Real)
  (c : q → Real) [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_6 : Invertible (HansenEconometrics.clsConstraintGram X R)] [MeasureTheory.IsProbabilityMeasure μ],
  Eq (R.transpose.mulVec β) c →
    ∀ (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
      (∀ (i : n), MeasureTheory.Integrable (fun ω => e ω i) μ) →
        (∀ (i : n), (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => e ω i) fun x => 0) →
          (MeasureTheory.ae μ).EventuallyEq
            (MeasureTheory.condExp m μ fun ω => HansenEconometrics.clsBeta X (instHAdd.hAdd (X.mulVec β) (e ω)) R c)
            fun x => β

Direct statement dependencies (2)

HansenEconometrics.clsBeta
HansenEconometrics.clsConstraintGram

HansenEconometrics/Chapter8RestrictedEstimation.lean:308

Theorem 8.33 endpoints

Under \mathbb E[e^2\mid X]=\sigma^2, \operatorname{Var}(\tilde\beta_{\mathrm{CLS}}\mid X)=V^0_{\tilde\beta}.

theorem HansenEconometrics.cls_conditionalVariance_homoskedastic

Hansen Theorem 8.3 homoskedastic covariance bridge from the deterministic sandwich core.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] (X : Matrix n k Real) (R : Matrix k q Real)
  (σ2 : Real) [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_7 : Invertible (HansenEconometrics.clsConstraintGram X R)],
  Eq
      (have B :=
        instHSub.hSub
          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
            (inst_6.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)) X.transpose)
          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.clsCorrectionMatrix X R) X.transpose);
      Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul B B.transpose)
      (instHSub.hSub (inst_6.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X))
        (HansenEconometrics.clsCorrectionMatrix X R)) →
    Eq (HansenEconometrics.clsConditionalVarianceMatrix X R (instHSMul.hSMul σ2 1))
      (HansenEconometrics.clsHomoskedasticVarianceMatrix X R σ2)

Direct statement dependencies (4)

HansenEconometrics.clsConditionalVarianceMatrix
HansenEconometrics.clsConstraintGram
HansenEconometrics.clsCorrectionMatrix
HansenEconometrics.clsHomoskedasticVarianceMatrix

HansenEconometrics/Chapter8RestrictedEstimation.lean:445

theorem HansenEconometrics.cls_conditionalVariance_homoskedastic_composed

Hansen Theorem 8.3: composed homoskedastic CLS covariance formula.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] (X : Matrix n k Real) (R : Matrix k q Real)
  (σ2 : Real) [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_7 : Invertible (HansenEconometrics.clsConstraintGram X R)],
  Eq (HansenEconometrics.clsConditionalVarianceMatrix X R (instHSMul.hSMul σ2 1))
    (HansenEconometrics.clsHomoskedasticVarianceMatrix X R σ2)

Direct statement dependencies (3)

HansenEconometrics.clsConditionalVarianceMatrix
HansenEconometrics.clsConstraintGram
HansenEconometrics.clsHomoskedasticVarianceMatrix

HansenEconometrics/Chapter8RestrictedEstimation.lean:462

theorem HansenEconometrics.cls_sandwichCore_eq

Lean-only deterministic bridge for Hansen Theorem 8.3’s homoskedastic sandwich core.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq k] [inst_4 : DecidableEq q] (X : Matrix n k Real) (R : Matrix k q Real)
  [inst_5 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_6 : Invertible (HansenEconometrics.clsConstraintGram X R)],
  Eq
    (have B :=
      instHSub.hSub
        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
          (inst_5.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)) X.transpose)
        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.clsCorrectionMatrix X R) X.transpose);
    Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul B B.transpose)
    (instHSub.hSub (inst_5.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X))
      (HansenEconometrics.clsCorrectionMatrix X R))

Direct statement dependencies (2)

HansenEconometrics.clsConstraintGram
HansenEconometrics.clsCorrectionMatrix

HansenEconometrics/Chapter8RestrictedEstimation.lean:401

Theorem 8.42 endpoints

Under conditional homoskedasticity, \mathbb E[s^2_{\mathrm{CLS}}\mid X]=\sigma^2 and \mathbb E[\hat V^0_{\tilde\beta}\mid X]=V^0_{\tilde\beta}.

theorem HansenEconometrics.cls_residualVariance_condExp_eq_sigmaSq

Hansen Theorem 8.4 residual-variance conditional expectation bridge.

The stochastic input is stated for the quadratic form of the structural error after applying the CLS residual-maker.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] {Ω : Type u_4} {m : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real) (R : Matrix k q Real)
  (c : q → Real) (σ2 : Real) [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_7 : Invertible (HansenEconometrics.clsConstraintGram X R)],
  Eq (R.transpose.mulVec β) c →
    ((MeasureTheory.ae μ).EventuallyEq
        (MeasureTheory.condExp m μ fun ω =>
          instHMul.hMul
            (Real.instInv.inv
              (instHAdd.hAdd (instHSub.hSub (Fintype.card n).cast (Fintype.card k).cast) (Fintype.card q).cast))
            (dotProduct ((HansenEconometrics.clsProjectionMatrix X R).mulVec (e ω))
              ((HansenEconometrics.clsProjectionMatrix X R).mulVec (e ω))))
        fun x => σ2) →
      (MeasureTheory.ae μ).EventuallyEq
        (MeasureTheory.condExp m μ fun ω =>
          HansenEconometrics.clsResidualVariance X (instHAdd.hAdd (X.mulVec β) (e ω)) R c)
        fun x => σ2

Direct statement dependencies (3)

HansenEconometrics.clsConstraintGram
HansenEconometrics.clsProjectionMatrix
HansenEconometrics.clsResidualVariance

HansenEconometrics/Chapter8RestrictedEstimation.lean:473

theorem HansenEconometrics.cls_residualVariance_condExp_eq_sigmaSq_of_homoskedastic

Hansen Theorem 8.4 residual-variance conditional expectation from homoskedastic second moments. The explicit degrees-of-freedom nonzero assumption is needed because clsResidualVariance uses a totalized inverse.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] {Ω : Type u_4} {m m₀ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (e : Ω → n → Real) (R : Matrix k q Real)
  (c : q → Real) (σ2 : Real) [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_7 : Invertible (HansenEconometrics.clsConstraintGram X R)] [MeasureTheory.IsProbabilityMeasure μ],
  Eq (R.transpose.mulVec β) c →
    ∀ (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
      (∀ (i j : n), MeasureTheory.Integrable (fun ω => instHMul.hMul (e ω i) (e ω j)) μ) →
        (∀ (i j : n),
            (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => instHMul.hMul (e ω i) (e ω j))
              fun x => instHMul.hMul σ2 (1 i j)) →
          Ne (instHAdd.hAdd (instHSub.hSub (Fintype.card n).cast (Fintype.card k).cast) (Fintype.card q).cast) 0 →
            (MeasureTheory.ae μ).EventuallyEq
              (MeasureTheory.condExp m μ fun ω =>
                HansenEconometrics.clsResidualVariance X (instHAdd.hAdd (X.mulVec β) (e ω)) R c)
              fun x => σ2

Direct statement dependencies (2)

HansenEconometrics.clsConstraintGram
HansenEconometrics.clsResidualVariance

HansenEconometrics/Chapter8RestrictedEstimation.lean:495

Theorem 8.56 endpoints

In the constrained normal model, \tilde\beta_{\mathrm{CLS}}\sim N(\beta,V^0_{\tilde\beta}), (n-k+q)s^2_{\mathrm{CLS}}/\sigma^2\sim\chi^2_{n-k+q}, and T\sim t_{n-k+q}.

theorem HansenEconometrics.clsNormalRegressionFiniteSampleLaws

Hansen Theorem 8.5: exact finite-sample Gaussian, chi-square, and Student-t laws for CLS.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] {Ω : Type u_4} [inst_6 : MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) {σ2 : Real},
  Real.instLT.lt 0 σ2 →
    ∀ (R : Matrix k q Real) (c : q → Real)
      [inst_7 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
      [inst_8 : Invertible (HansenEconometrics.clsConstraintGram X R)],
      Eq (R.transpose.mulVec β) c →
        instLTNat.lt (Fintype.card k) (instHAdd.hAdd (Fintype.card n) (Fintype.card q)) →
          ∀ (ε : Ω → EuclideanSpace Real n),
            ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
              ProbabilityTheory.HasGaussianLaw (Function.comp WithLp.ofLp ε) μ →
                ∀ (Z : Ω → Real),
                  ProbabilityTheory.HasLaw Z (ProbabilityTheory.gaussianReal 0 1) μ →
                    ProbabilityTheory.IndepFun Z
                        (HansenEconometrics.scaledClsResidualVarianceStatistic X β σ2 R c (Function.comp WithLp.ofLp ε))
                        μ →
                      HansenEconometrics.ClsNormalRegressionFiniteSampleLaws μ X β σ2 R c ε Z

Direct statement dependencies (3)

HansenEconometrics.ClsNormalRegressionFiniteSampleLaws
HansenEconometrics.clsConstraintGram
HansenEconometrics.scaledClsResidualVarianceStatistic

HansenEconometrics/Chapter8RestrictedEstimation.lean:815

theorem HansenEconometrics.clsBeta_hasGaussianLaw_of_gaussian_error

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

Formal statement

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

Direct statement dependencies (2)

HansenEconometrics.clsBeta
HansenEconometrics.clsConstraintGram

HansenEconometrics/Chapter8RestrictedEstimation.lean:587

theorem HansenEconometrics.scaledClsResVarStat_eq_sum_sq_eigenvector_coords

The scaled CLS residual statistic is the sum of squared standardized Gaussian coordinates on the 1-eigenspace of the CLS residual-maker. This is the deterministic bridge for Hansen Theorem 8.5.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] {Ω : Type u_4} [MeasurableSpace Ω]
  (X : Matrix n k Real) (β : k → Real) {σ2 : Real},
  Real.instLT.lt 0 σ2 →
    ∀ (R : Matrix k q Real) (c : q → Real)
      [inst_7 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
      [inst_8 : Invertible (HansenEconometrics.clsConstraintGram X R)],
      Eq (R.transpose.mulVec β) c →
        instLTNat.lt (Fintype.card k) (instHAdd.hAdd (Fintype.card n) (Fintype.card q)) →
          ∀ (ε : Ω → EuclideanSpace Real n),
            let P := HansenEconometrics.clsProjectionMatrix X R;
            have hP := ⋯;
            have b := hP.eigenvectorBasis;
            Eq (HansenEconometrics.scaledClsResidualVarianceStatistic X β σ2 R c (Function.comp WithLp.ofLp ε))
              (HansenEconometrics.sumSquaresRV
                (HansenEconometrics.restrictedStandardizedCoords b (fun i => i.val) σ2 ε))

Direct statement dependencies (6)

HansenEconometrics.clsConstraintGram
HansenEconometrics.clsProjectionMatrix
HansenEconometrics.clsProjectionMatrix_isHermitian
HansenEconometrics.restrictedStandardizedCoords
HansenEconometrics.scaledClsResidualVarianceStatistic
HansenEconometrics.sumSquaresRV

HansenEconometrics/Chapter8RestrictedEstimation.lean:630

theorem HansenEconometrics.scaledClsResidualVarianceStatistic_hasLaw_chiSquared

Hansen Theorem 8.5, chi-square component: under homoskedastic Gaussian structural errors, the scaled CLS residual variance statistic has a chi-square law with n - k + q degrees of freedom.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] {Ω : Type u_4} [inst_6 : MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) {σ2 : Real},
  Real.instLT.lt 0 σ2 →
    ∀ (R : Matrix k q Real) (c : q → Real)
      [inst_7 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
      [inst_8 : Invertible (HansenEconometrics.clsConstraintGram X R)],
      Eq (R.transpose.mulVec β) c →
        instLTNat.lt (Fintype.card k) (instHAdd.hAdd (Fintype.card n) (Fintype.card q)) →
          ∀ (ε : Ω → EuclideanSpace Real n),
            ProbabilityTheory.HasLaw ε (ProbabilityTheory.multivariateGaussian 0 (instHSMul.hSMul σ2 1)) μ →
              ProbabilityTheory.HasLaw
                (HansenEconometrics.scaledClsResidualVarianceStatistic X β σ2 R c (Function.comp WithLp.ofLp ε))
                (HansenEconometrics.chiSquared
                  (instHAdd.hAdd (instHSub.hSub (Fintype.card n) (Fintype.card k)) (Fintype.card q)))
                μ

Direct statement dependencies (3)

HansenEconometrics.chiSquared
HansenEconometrics.clsConstraintGram
HansenEconometrics.scaledClsResidualVarianceStatistic

HansenEconometrics/Chapter8RestrictedEstimation.lean:699

theorem HansenEconometrics.scaledClsResidualVarianceStatistic_hasChiSquareLaw

Hansen Theorem 8.5 chi-square law bridge for the scaled CLS residual statistic.

The law input is stated for the residual-maker quadratic form of the structural error; the theorem transfers it to the named CLS residual-variance statistic using clsResidual_linear_model.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {q : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype q]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq k] [inst_5 : DecidableEq q] {Ω : Type u_4} [inst_6 : MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} (X : Matrix n k Real) (β : k → Real) (σ2 : Real) (R : Matrix k q Real) (c : q → Real)
  [inst_7 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_8 : Invertible (HansenEconometrics.clsConstraintGram X R)] (e : Ω → n → Real) (ν : Nat),
  Eq (R.transpose.mulVec β) c →
    ProbabilityTheory.HasLaw
        (fun ω =>
          instHDiv.hDiv
            (instHMul.hMul
              (instHAdd.hAdd (instHSub.hSub (Fintype.card n).cast (Fintype.card k).cast) (Fintype.card q).cast)
              (instHMul.hMul
                (Real.instInv.inv
                  (instHAdd.hAdd (instHSub.hSub (Fintype.card n).cast (Fintype.card k).cast) (Fintype.card q).cast))
                (dotProduct ((HansenEconometrics.clsProjectionMatrix X R).mulVec (e ω))
                  ((HansenEconometrics.clsProjectionMatrix X R).mulVec (e ω)))))
            σ2)
        (HansenEconometrics.chiSquared ν) μ →
      ProbabilityTheory.HasLaw (HansenEconometrics.scaledClsResidualVarianceStatistic X β σ2 R c e)
        (HansenEconometrics.chiSquared ν) μ

Direct statement dependencies (4)

HansenEconometrics.chiSquared
HansenEconometrics.clsConstraintGram
HansenEconometrics.clsProjectionMatrix
HansenEconometrics.scaledClsResidualVarianceStatistic

HansenEconometrics/Chapter8RestrictedEstimation.lean:751

theorem HansenEconometrics.clsTStat_hasStudentTLaw

Hansen Theorem 8.5 Student-t bridge from the standard-normal numerator, chi-square studentizer, and independence inputs.

Formal statement

∀ {Ω : Type u_4} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (Z Q : Ω → Real) (ν : Nat),
  instLTNat.lt 0 ν →
    ProbabilityTheory.HasLaw Z (ProbabilityTheory.gaussianReal 0 1) μ →
      ProbabilityTheory.HasLaw Q (HansenEconometrics.chiSquared ν) μ →
        ProbabilityTheory.IndepFun Z Q μ →
          ProbabilityTheory.HasLaw (fun ω => HansenEconometrics.clsTStatFromComponents (Z ω) (Q ω) ν)
            (HansenEconometrics.studentT ν) μ

Direct statement dependencies (3)

HansenEconometrics.chiSquared
HansenEconometrics.clsTStatFromComponents
HansenEconometrics.studentT

HansenEconometrics/Chapter8RestrictedEstimation.lean:782

Theorem 8.66 of 9 linked endpoints

Under Assumptions 7.1, 8.1, and 8.2, \tilde\beta_{\mathrm{MD}}\xrightarrow{p}\beta.

theorem HansenEconometrics.mdBeta_tendstoInMeasure_beta

Hansen Theorem 8.6 MD consistency from explicit continuity and convergence inputs.

The assumptions are convergence of the unrestricted estimator and the weight matrix plus continuity of the MD map at the limiting values.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] (bhat : Nat → Ω → k → Real) (What : Nat → Ω → Matrix k k Real) (W : Matrix k k Real)
  (R : Matrix k q Real) (c : q → Real) (β : k → Real),
  (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (bhat n) μ) →
    (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (What n) μ) →
      (∀ (n : Nat),
          MeasureTheory.AEStronglyMeasurable (fun ω => HansenEconometrics.mdBetaStar (What n ω) R c (bhat n ω)) μ) →
        (MeasureTheory.TendstoInMeasure μ bhat Filter.atTop fun x => β) →
          (MeasureTheory.TendstoInMeasure μ What Filter.atTop fun x => W) →
            ContinuousAt (fun p => HansenEconometrics.mdBetaStar p.snd R c p.fst) { fst := β, snd := W } →
              Eq (R.transpose.mulVec β) c →
                MeasureTheory.TendstoInMeasure μ (fun n ω => HansenEconometrics.mdBetaStar (What n ω) R c (bhat n ω))
                  Filter.atTop fun x => β

Direct statement dependencies (1)

HansenEconometrics.mdBetaStar

HansenEconometrics/Chapter8Asymptotics.lean:2148

theorem HansenEconometrics.mdBeta_tendstoInMeasure_beta_of_nonsingular

Hansen Theorem 8.6 consistency wrapper with the MD-map continuity and measurability side conditions discharged from nonsingularity of the population weight and restriction Gram.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] (bhat : Nat → Ω → k → Real) (What : Nat → Ω → Matrix k k Real) (W : Matrix k k Real)
  (R : Matrix k q Real) (c : q → Real) (β : k → Real),
  (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (bhat n) μ) →
    (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (What n) μ) →
      (MeasureTheory.TendstoInMeasure μ bhat Filter.atTop fun x => β) →
        (MeasureTheory.TendstoInMeasure μ What Filter.atTop fun x => W) →
          IsUnit W.det →
            IsUnit
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                    (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv W)) R).det →
              Eq (R.transpose.mulVec β) c →
                MeasureTheory.TendstoInMeasure μ (fun n ω => HansenEconometrics.mdBetaStar (What n ω) R c (bhat n ω))
                  Filter.atTop fun x => β

Direct statement dependencies (1)

HansenEconometrics.mdBetaStar

HansenEconometrics/Chapter8Asymptotics.lean:2177

theorem HansenEconometrics.mdBeta_tendstoInMeasure_beta_of_consistency

Hansen Theorem 8.6 from the stable minimum-distance consistency interface.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] (bhat : Nat → Ω → k → Real) (What : Nat → Ω → Matrix k k Real) (W : Matrix k k Real)
  (R : Matrix k q Real) (c : q → Real) (β : k → Real),
  HansenEconometrics.MinimumDistanceConsistencyConditions μ bhat What W R c β →
    MeasureTheory.TendstoInMeasure μ (fun n ω => HansenEconometrics.mdBetaStar (What n ω) R c (bhat n ω)) Filter.atTop
      fun x => β

Direct statement dependencies (2)

HansenEconometrics.MinimumDistanceConsistencyConditions
HansenEconometrics.mdBetaStar

HansenEconometrics/Chapter8Asymptotics.lean:2197

theorem HansenEconometrics.mdBeta_restrict

The closed-form minimum-distance estimator satisfies the imposed linear restriction.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (W : Matrix k k Real) (R : Matrix k q Real) (c : q → Real) (bhat : k → Real)
  [inst_4 : Invertible W]
  [inst_5 :
    Invertible
      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (inst_4.invOf W)) R)],
  Eq (R.transpose.mulVec (HansenEconometrics.mdBeta W R c bhat)) c

Direct statement dependencies (1)

HansenEconometrics.mdBeta

HansenEconometrics/Chapter8Asymptotics.lean:36

theorem HansenEconometrics.minimumDistanceConsistencyConditions_of_weight_posDef

Positive-definite limiting weights and full-column-rank restrictions construct the stable minimum-distance consistency interface.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (bhat : Nat → Ω → k → Real) (What : Nat → Ω → Matrix k k Real) (W : Matrix k k Real) (R : Matrix k q Real)
  (c : q → Real) (β : k → Real),
  (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (bhat n) μ) →
    (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (What n) μ) →
      (MeasureTheory.TendstoInMeasure μ bhat Filter.atTop fun x => β) →
        (MeasureTheory.TendstoInMeasure μ What Filter.atTop fun x => W) →
          W.PosDef →
            Function.Injective R.mulVec →
              Eq (R.transpose.mulVec β) c → HansenEconometrics.MinimumDistanceConsistencyConditions μ bhat What W R c β

Direct statement dependencies (1)

HansenEconometrics.MinimumDistanceConsistencyConditions

HansenEconometrics/Chapter8Asymptotics.lean:2065

theorem HansenEconometrics.mdBeta_eq_mdBetaStar

On nonsingular inputs, the totalized Star MD estimator agrees with the base estimator.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (W : Matrix k k Real) (R : Matrix k q Real) (c : q → Real) (bhat : k → Real)
  [inst_4 : Invertible W]
  [inst_5 :
    Invertible
      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (inst_4.invOf W)) R)],
  Eq (HansenEconometrics.mdBeta W R c bhat) (HansenEconometrics.mdBetaStar W R c bhat)

Direct statement dependencies (2)

HansenEconometrics.mdBeta
HansenEconometrics.mdBetaStar

HansenEconometrics/Chapter8Asymptotics.lean:53

Theorem 8.76 of 31 linked endpoints

Under Assumptions 7.2, 8.1, and 8.2, \sqrt n(\tilde\beta_{\mathrm{MD}}-\beta)\xrightarrow{d}N(0,V_\beta(W)).

theorem HansenEconometrics.mdBeta_tendstoInDistribution_gaussian

Hansen Theorem 8.7 current-assumption MD asymptotic-normality/Slutsky wrapper.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} {Ω' : Type u_4} [inst_4 : MeasurableSpace Ω] [inst_5 : MeasurableSpace Ω']
  {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [inst_6 : MeasureTheory.IsProbabilityMeasure μ]
  [inst_7 : MeasureTheory.IsProbabilityMeasure ν] (root : Nat → Real) (bhat : Nat → Ω → k → Real)
  (What : Nat → Ω → Matrix k k Real) (W : Matrix k k Real) (R : Matrix k q Real) (c : q → Real) (β : k → Real)
  (T : Nat → Ω → k → Real) (Z : Ω' → k → Real),
  MeasureTheory.TendstoInDistribution (fun n ω => (HansenEconometrics.mdLinearMap W R).mulVec (T n ω)) Filter.atTop Z
      (fun x => μ) ν →
    (MeasureTheory.TendstoInMeasure μ
        (instHSub.hSub (HansenEconometrics.mdScaledError root bhat What R c β) fun n ω =>
          (HansenEconometrics.mdLinearMap W R).mulVec (T n ω))
        Filter.atTop fun x => 0) →
      (∀ (n : Nat), AEMeasurable (HansenEconometrics.mdScaledError root bhat What R c β n) μ) →
        MeasureTheory.TendstoInDistribution (HansenEconometrics.mdScaledError root bhat What R c β) Filter.atTop Z
          (fun x => μ) ν

Direct statement dependencies (2)

HansenEconometrics.mdLinearMap
HansenEconometrics.mdScaledError

HansenEconometrics/Chapter8Asymptotics.lean:3140

theorem HansenEconometrics.mdAsymptoticVariance_eq_hansen_expanded

Hansen Theorem 8.7, equation (8.24): the compact MD sandwich variance expands to the four-term textbook formula when the weight matrix is symmetric.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (W : Matrix k k Real) (R : Matrix k q Real) (V : Matrix k k Real),
  Eq W.transpose W →
    Eq (HansenEconometrics.mdAsymptoticVariance W R V)
      (instHAdd.hAdd
        (instHSub.hSub
          (instHSub.hSub V
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.inv.inv W) R)
                  (Matrix.inv.inv
                    (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv W)) R)))
                R.transpose)
              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 (Matrix.inv.inv W)) R)))
              R.transpose)
            (Matrix.inv.inv 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 W) R)
                      (Matrix.inv.inv
                        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv W)) R)))
                    R.transpose)
                  V)
                R)
              (Matrix.inv.inv
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv W)) R)))
            R.transpose)
          (Matrix.inv.inv W)))

Direct statement dependencies (1)

HansenEconometrics.mdAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:294

theorem HansenEconometrics.mdBeta_tendstoInDistribution_multivariateGaussian

Hansen Theorem 8.7 with the fixed-linear Gaussian limit and scaled-error measurability discharged from explicit inputs. The stable-interface version mdBeta_tendstoInDistribution_multivariateGaussian_of_linearization packages the same linearization capability as AsymptoticallyLinearEstimator.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_5 : MeasureTheory.IsProbabilityMeasure μ] (root : Nat → Real) (bhat : Nat → Ω → k → Real)
  (What : Nat → Ω → Matrix k k Real) (W : Matrix k k Real) (R : Matrix k q Real) (c : q → Real) (β : k → Real)
  (S : Matrix k k Real) (T : Nat → Ω → k → Real),
  S.PosSemidef →
    (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (bhat n) μ) →
      (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (What n) μ) →
        MeasureTheory.TendstoInDistribution T Filter.atTop (fun z => z.ofLp) (fun x => μ)
            (ProbabilityTheory.multivariateGaussian 0 S) →
          (MeasureTheory.TendstoInMeasure μ
              (instHSub.hSub (HansenEconometrics.mdScaledError root bhat What R c β) fun n ω =>
                (HansenEconometrics.mdLinearMap W R).mulVec (T n ω))
              Filter.atTop fun x => 0) →
            MeasureTheory.TendstoInDistribution (HansenEconometrics.mdScaledError root bhat What R c β) Filter.atTop
              (fun z => z.ofLp) (fun x => μ)
              (ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.mdAsymptoticVariance W R S))

Direct statement dependencies (3)

HansenEconometrics.mdAsymptoticVariance
HansenEconometrics.mdLinearMap
HansenEconometrics.mdScaledError

HansenEconometrics/Chapter8Asymptotics.lean:3180

theorem HansenEconometrics.mdBeta_tendstoInDistribution_gaussian_of_measurable

Hansen Theorem 8.7 with scaled-error measurability discharged from measurability of the unrestricted estimator and weight process.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} {Ω' : Type u_4} [inst_4 : MeasurableSpace Ω] [inst_5 : MeasurableSpace Ω']
  {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [inst_6 : MeasureTheory.IsProbabilityMeasure μ]
  [inst_7 : MeasureTheory.IsProbabilityMeasure ν] (root : Nat → Real) (bhat : Nat → Ω → k → Real)
  (What : Nat → Ω → Matrix k k Real) (W : Matrix k k Real) (R : Matrix k q Real) (c : q → Real) (β : k → Real)
  (T : Nat → Ω → k → Real) (Z : Ω' → k → Real),
  (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (bhat n) μ) →
    (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (What n) μ) →
      MeasureTheory.TendstoInDistribution (fun n ω => (HansenEconometrics.mdLinearMap W R).mulVec (T n ω)) Filter.atTop
          Z (fun x => μ) ν →
        (MeasureTheory.TendstoInMeasure μ
            (instHSub.hSub (HansenEconometrics.mdScaledError root bhat What R c β) fun n ω =>
              (HansenEconometrics.mdLinearMap W R).mulVec (T n ω))
            Filter.atTop fun x => 0) →
          MeasureTheory.TendstoInDistribution (HansenEconometrics.mdScaledError root bhat What R c β) Filter.atTop Z
            (fun x => μ) ν

Direct statement dependencies (2)

HansenEconometrics.mdLinearMap
HansenEconometrics.mdScaledError

HansenEconometrics/Chapter8Asymptotics.lean:3159

theorem HansenEconometrics.mdBeta_fixedWeight_tendstoInDistribution_multivariateGaussian

Hansen Theorem 8.7 in the fixed-weight MD case: the exact fixed-weight linearization discharges the remainder side condition.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_5 : MeasureTheory.IsProbabilityMeasure μ] (root : Nat → Real) (bhat : Nat → Ω → k → Real) (W : Matrix k k Real)
  (R : Matrix k q Real) (c : q → Real) (β : k → Real) (S : Matrix k k Real),
  S.PosSemidef →
    (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (bhat n) μ) →
      Eq (R.transpose.mulVec β) c →
        MeasureTheory.TendstoInDistribution (fun n ω => instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) β))
            Filter.atTop (fun z => z.ofLp) (fun x => μ) (ProbabilityTheory.multivariateGaussian 0 S) →
          MeasureTheory.TendstoInDistribution (HansenEconometrics.mdScaledError root bhat (fun x x_1 => W) R c β)
            Filter.atTop (fun z => z.ofLp) (fun x => μ)
            (ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.mdAsymptoticVariance W R S))

Direct statement dependencies (2)

HansenEconometrics.mdAsymptoticVariance
HansenEconometrics.mdScaledError

HansenEconometrics/Chapter8Asymptotics.lean:3238

theorem HansenEconometrics.mdBeta_randomWeight_tendstoInDistribution_multivariateGaussian

Hansen Theorem 8.7 random-weight MD case. Assumption 8.2 supplies What →ₚ W; continuity of the MD linear map and the random matrix Slutsky wrapper discharge the linearization step.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_5 : MeasureTheory.IsProbabilityMeasure μ] (root : Nat → Real) (bhat : Nat → Ω → k → Real)
  (What : Nat → Ω → Matrix k k Real) (W : Matrix k k Real) (R : Matrix k q Real) (c : q → Real) (β : k → Real)
  (S : Matrix k k Real),
  S.PosSemidef →
    (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (What n) μ) →
      (MeasureTheory.TendstoInMeasure μ What Filter.atTop fun x => W) →
        IsUnit W.det →
          IsUnit
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv W)) R).det →
            Eq (R.transpose.mulVec β) c →
              MeasureTheory.TendstoInDistribution (fun n ω => instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) β))
                  Filter.atTop (fun z => z.ofLp) (fun x => μ) (ProbabilityTheory.multivariateGaussian 0 S) →
                MeasureTheory.TendstoInDistribution (HansenEconometrics.mdScaledError root bhat What R c β) Filter.atTop
                  (fun z => z.ofLp) (fun x => μ)
                  (ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.mdAsymptoticVariance W R S))

Direct statement dependencies (2)

HansenEconometrics.mdAsymptoticVariance
HansenEconometrics.mdScaledError

HansenEconometrics/Chapter8Asymptotics.lean:3259

Theorem 8.86 of 14 linked endpoints

Under Assumptions 7.2 and 8.1, \sqrt n(\tilde\beta_{\mathrm{CLS}}-\beta)\xrightarrow{d}N(0,V_{\mathrm{CLS}}).

theorem HansenEconometrics.clsBeta_tendstoInDistribution_gaussian

Hansen Theorem 8.8 CLS asymptotic-normality wrapper as the MD specialization.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} {Ω' : Type u_4} [inst_4 : MeasurableSpace Ω] [inst_5 : MeasurableSpace Ω']
  {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [inst_6 : MeasureTheory.IsProbabilityMeasure μ]
  [inst_7 : MeasureTheory.IsProbabilityMeasure ν] (root : Nat → Real) (bhat : Nat → Ω → k → Real)
  (Qhat : Nat → Ω → Matrix k k Real) (Q : Matrix k k Real) (R : Matrix k q Real) (c : q → Real) (β : k → Real)
  (T : Nat → Ω → k → Real) (Z : Ω' → k → Real),
  MeasureTheory.TendstoInDistribution (fun n ω => (HansenEconometrics.mdLinearMap Q R).mulVec (T n ω)) Filter.atTop Z
      (fun x => μ) ν →
    (MeasureTheory.TendstoInMeasure μ
        (instHSub.hSub (HansenEconometrics.clsMDScaledError root bhat Qhat R c β) fun n ω =>
          (HansenEconometrics.mdLinearMap Q R).mulVec (T n ω))
        Filter.atTop fun x => 0) →
      (∀ (n : Nat), AEMeasurable (HansenEconometrics.clsMDScaledError root bhat Qhat R c β n) μ) →
        MeasureTheory.TendstoInDistribution (HansenEconometrics.clsMDScaledError root bhat Qhat R c β) Filter.atTop Z
          (fun x => μ) ν

Direct statement dependencies (2)

HansenEconometrics.clsMDScaledError
HansenEconometrics.mdLinearMap

HansenEconometrics/Chapter8Asymptotics.lean:3306

theorem HansenEconometrics.clsAsymptoticVariance_eq_hansen_expanded

Hansen Theorem 8.8: the CLS asymptotic variance is the Theorem 8.7 four-term minimum-distance formula with the population Gram weight.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (Q : Matrix k k Real) (R : Matrix k q Real) (V : Matrix k k Real),
  Eq Q.transpose Q →
    Eq (HansenEconometrics.clsAsymptoticVariance Q R V)
      (instHAdd.hAdd
        (instHSub.hSub
          (instHSub.hSub V
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.inv.inv Q) R)
                  (Matrix.inv.inv
                    (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv Q)) R)))
                R.transpose)
              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 (Matrix.inv.inv Q)) R)))
              R.transpose)
            (Matrix.inv.inv Q)))
        (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 Q) R)
                      (Matrix.inv.inv
                        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv Q)) R)))
                    R.transpose)
                  V)
                R)
              (Matrix.inv.inv
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv Q)) R)))
            R.transpose)
          (Matrix.inv.inv Q)))

Direct statement dependencies (1)

HansenEconometrics.clsAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:335

theorem HansenEconometrics.clsBeta_tendstoInDistribution_multivariateGaussian

Hansen Theorem 8.8 with the fixed-linear Gaussian limit and scaled-error measurability discharged from explicit inputs. The stable-interface version clsBeta_tendstoInDistribution_multivariateGaussian_of_linearization packages the same CLS-as-MD linearization capability as AsymptoticallyLinearEstimator.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_5 : MeasureTheory.IsProbabilityMeasure μ] (root : Nat → Real) (bhat : Nat → Ω → k → Real)
  (Qhat : Nat → Ω → Matrix k k Real) (Q : Matrix k k Real) (R : Matrix k q Real) (c : q → Real) (β : k → Real)
  (S : Matrix k k Real) (T : Nat → Ω → k → Real),
  S.PosSemidef →
    (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (bhat n) μ) →
      (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (Qhat n) μ) →
        MeasureTheory.TendstoInDistribution T Filter.atTop (fun z => z.ofLp) (fun x => μ)
            (ProbabilityTheory.multivariateGaussian 0 S) →
          (MeasureTheory.TendstoInMeasure μ
              (instHSub.hSub (HansenEconometrics.clsMDScaledError root bhat Qhat R c β) fun n ω =>
                (HansenEconometrics.mdLinearMap Q R).mulVec (T n ω))
              Filter.atTop fun x => 0) →
            MeasureTheory.TendstoInDistribution (HansenEconometrics.clsMDScaledError root bhat Qhat R c β) Filter.atTop
              (fun z => z.ofLp) (fun x => μ)
              (ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.clsAsymptoticVariance Q R S))

Direct statement dependencies (3)

HansenEconometrics.clsAsymptoticVariance
HansenEconometrics.clsMDScaledError
HansenEconometrics.mdLinearMap

HansenEconometrics/Chapter8Asymptotics.lean:3344

theorem HansenEconometrics.clsBeta_tendstoInDistribution_gaussian_of_measurable

Hansen Theorem 8.8 with scaled CLS error measurability discharged from estimator and sample-Gram measurability.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} {Ω' : Type u_4} [inst_4 : MeasurableSpace Ω] [inst_5 : MeasurableSpace Ω']
  {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [inst_6 : MeasureTheory.IsProbabilityMeasure μ]
  [inst_7 : MeasureTheory.IsProbabilityMeasure ν] (root : Nat → Real) (bhat : Nat → Ω → k → Real)
  (Qhat : Nat → Ω → Matrix k k Real) (Q : Matrix k k Real) (R : Matrix k q Real) (c : q → Real) (β : k → Real)
  (T : Nat → Ω → k → Real) (Z : Ω' → k → Real),
  (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (bhat n) μ) →
    (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (Qhat n) μ) →
      MeasureTheory.TendstoInDistribution (fun n ω => (HansenEconometrics.mdLinearMap Q R).mulVec (T n ω)) Filter.atTop
          Z (fun x => μ) ν →
        (MeasureTheory.TendstoInMeasure μ
            (instHSub.hSub (HansenEconometrics.clsMDScaledError root bhat Qhat R c β) fun n ω =>
              (HansenEconometrics.mdLinearMap Q R).mulVec (T n ω))
            Filter.atTop fun x => 0) →
          MeasureTheory.TendstoInDistribution (HansenEconometrics.clsMDScaledError root bhat Qhat R c β) Filter.atTop Z
            (fun x => μ) ν

Direct statement dependencies (2)

HansenEconometrics.clsMDScaledError
HansenEconometrics.mdLinearMap

HansenEconometrics/Chapter8Asymptotics.lean:3323

theorem HansenEconometrics.clsBeta_randomWeight_tendstoInDistribution_multivariateGaussian

Hansen Theorem 8.8 random-weight CLS-as-MD case. Convergence of the sample Gram weight discharges the CLS-as-MD linearization through the random-weight MD theorem.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_5 : MeasureTheory.IsProbabilityMeasure μ] (root : Nat → Real) (bhat : Nat → Ω → k → Real)
  (Qhat : Nat → Ω → Matrix k k Real) (Q : Matrix k k Real) (R : Matrix k q Real) (c : q → Real) (β : k → Real)
  (S : Matrix k k Real),
  S.PosSemidef →
    (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (Qhat n) μ) →
      (MeasureTheory.TendstoInMeasure μ Qhat Filter.atTop fun x => Q) →
        IsUnit Q.det →
          IsUnit
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv Q)) R).det →
            Eq (R.transpose.mulVec β) c →
              MeasureTheory.TendstoInDistribution (fun n ω => instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) β))
                  Filter.atTop (fun z => z.ofLp) (fun x => μ) (ProbabilityTheory.multivariateGaussian 0 S) →
                MeasureTheory.TendstoInDistribution (HansenEconometrics.clsMDScaledError root bhat Qhat R c β)
                  Filter.atTop (fun z => z.ofLp) (fun x => μ)
                  (ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.clsAsymptoticVariance Q R S))

Direct statement dependencies (2)

HansenEconometrics.clsAsymptoticVariance
HansenEconometrics.clsMDScaledError

HansenEconometrics/Chapter8Asymptotics.lean:3403

theorem HansenEconometrics.clsBeta_tendstoInDistribution_multivariateGaussian_of_linearization

Hansen Theorem 8.8 from the stable asymptotically linear estimator interface.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_5 : MeasureTheory.IsProbabilityMeasure μ] (root : Nat → Real) (bhat : Nat → Ω → k → Real)
  (Qhat : Nat → Ω → Matrix k k Real) (Q : Matrix k k Real) (R : Matrix k q Real) (c : q → Real) (β : k → Real)
  (S : Matrix k k Real) (T : Nat → Ω → k → Real),
  S.PosSemidef →
    HansenEconometrics.AsymptoticallyLinearEstimator μ (HansenEconometrics.clsMDScaledError root bhat Qhat R c β)
        (HansenEconometrics.mdLinearMap Q R) T →
      MeasureTheory.TendstoInDistribution T Filter.atTop (fun z => z.ofLp) (fun x => μ)
          (ProbabilityTheory.multivariateGaussian 0 S) →
        MeasureTheory.TendstoInDistribution (HansenEconometrics.clsMDScaledError root bhat Qhat R c β) Filter.atTop
          (fun z => z.ofLp) (fun x => μ)
          (ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.clsAsymptoticVariance Q R S))

Direct statement dependencies (4)

HansenEconometrics.AsymptoticallyLinearEstimator
HansenEconometrics.clsAsymptoticVariance
HansenEconometrics.clsMDScaledError
HansenEconometrics.mdLinearMap

HansenEconometrics/Chapter8Asymptotics.lean:3369

Section 8.76 of 13 linked endpoints

If \hat V\xrightarrow{p}V, then \sqrt{a'\hat Va}\xrightarrow{p}\sqrt{a'Va} and the corresponding studentized statistic has its stated limit.

theorem HansenEconometrics.covarianceStdErrorScale_aemeasurable

A fixed-linear-combination standard-error scale is a.e. measurable whenever the covariance estimator is.

Formal statement

∀ {k : Type u_1} [inst : Fintype k] {Ω : Type u_3} [inst_1 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (h : k → Real) {Vhat : Ω → Matrix k k Real},
  MeasureTheory.AEStronglyMeasurable Vhat μ →
    AEMeasurable (fun ω => HansenEconometrics.covarianceStdErrorScale h (Vhat ω)) μ

Direct statement dependencies (1)

HansenEconometrics.covarianceStdErrorScale

HansenEconometrics/Chapter8Asymptotics.lean:486

theorem HansenEconometrics.mdAsymptoticVariance_aestronglyMeasurable

The MD asymptotic-variance plug-in map is a.e. strongly measurable whenever its weight and unrestricted covariance inputs are.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (Wseq Vseq : Ω → Matrix k k Real) (R : Matrix k q Real),
  MeasureTheory.AEStronglyMeasurable Wseq μ →
    MeasureTheory.AEStronglyMeasurable Vseq μ →
      MeasureTheory.AEStronglyMeasurable (fun ω => HansenEconometrics.mdAsymptoticVariance (Wseq ω) R (Vseq ω)) μ

Direct statement dependencies (1)

HansenEconometrics.mdAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:586

theorem HansenEconometrics.mdCovarianceEstimatorConsistent_of_consistency

Stable-interface constructor for consistency of the MD asymptotic-variance plug-in estimator.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {What Vhat : Nat → Ω → Matrix k k Real} {W V : Matrix k k Real}
  (R : Matrix k q Real),
  HansenEconometrics.CovarianceEstimatorConsistent μ What W →
    HansenEconometrics.CovarianceEstimatorConsistent μ Vhat V →
      IsUnit W.det →
        IsUnit
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv W)) R).det →
          HansenEconometrics.CovarianceEstimatorConsistent μ
            (fun n ω => HansenEconometrics.mdAsymptoticVariance (What n ω) R (Vhat n ω))
            (HansenEconometrics.mdAsymptoticVariance W R V)

Direct statement dependencies (2)

HansenEconometrics.CovarianceEstimatorConsistent
HansenEconometrics.mdAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:661

theorem HansenEconometrics.clsCovarianceEstimatorConsistent_of_consistency

CLS covariance-estimator consistency is the MD plug-in consistency theorem with the Gram matrix as the weight.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {Qhat Vhat : Nat → Ω → Matrix k k Real} {Q V : Matrix k k Real}
  (R : Matrix k q Real),
  HansenEconometrics.CovarianceEstimatorConsistent μ Qhat Q →
    HansenEconometrics.CovarianceEstimatorConsistent μ Vhat V →
      IsUnit Q.det →
        IsUnit
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv Q)) R).det →
          HansenEconometrics.CovarianceEstimatorConsistent μ
            (fun n ω => HansenEconometrics.clsAsymptoticVariance (Qhat n ω) R (Vhat n ω))
            (HansenEconometrics.clsAsymptoticVariance Q R V)

Direct statement dependencies (2)

HansenEconometrics.CovarianceEstimatorConsistent
HansenEconometrics.clsAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:681

theorem HansenEconometrics.mdAsymptoticVariance_continuousAt_of_nonsingular

The MD asymptotic-variance plug-in map is continuous at nonsingular limiting weights whose restriction Gram is nonsingular.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (W : Matrix k k Real) (R : Matrix k q Real) (V : Matrix k k Real),
  IsUnit W.det →
    IsUnit
        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv W)) R).det →
      ContinuousAt (fun p => HansenEconometrics.mdAsymptoticVariance p.fst R p.snd) { fst := W, snd := V }

Direct statement dependencies (1)

HansenEconometrics.mdAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:607

theorem HansenEconometrics.feasibleStandardErrorConsistent_of_tendstoInMeasure

Constructor for the feasible-standard-error interface from explicit measurability and convergence fields.

Formal statement

∀ {Ω : Type u_3} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (sehat : Nat → Ω → Real) (se : Real),
  (∀ (n : Nat), AEMeasurable (sehat n) μ) →
    (MeasureTheory.TendstoInMeasure μ sehat Filter.atTop fun x => se) →
      HansenEconometrics.FeasibleStandardErrorConsistent μ sehat se

Direct statement dependencies (1)

HansenEconometrics.FeasibleStandardErrorConsistent

HansenEconometrics/Chapter8Asymptotics.lean:526

Theorem 8.96 of 24 linked endpoints

Efficient MD uses W=V_\beta^{-1} and has \sqrt n(\tilde\beta_{\mathrm{EMD}}-\beta)\xrightarrow{d}N(0,V_{\beta,\mathrm{EMD}}), where V_{\beta,\mathrm{EMD}}=V_\beta-V_\beta R(R'V_\beta R)^{-1}R'V_\beta\preceq V_\beta(W).

theorem HansenEconometrics.mdAsymptoticVariance_sub_emd_factor

Hansen Theorem 8.9, equation (8.28): concrete factorization of the arbitrary-weight minimum-distance variance gap relative to the efficient-MD variance.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (W : Matrix k k Real) (R : Matrix k q Real) (V : Matrix k k Real),
  Eq W.transpose W →
    Eq V.transpose V →
      IsUnit
          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose V) R).det →
        Eq
          (instHSub.hSub (HansenEconometrics.mdAsymptoticVariance W R V) (HansenEconometrics.emdAsymptoticVariance R V))
          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
              (instHSub.hSub
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.inv.inv W) R)
                  (Matrix.inv.inv
                    (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv W)) R)))
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul V R)
                  (Matrix.inv.inv
                    (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose V) R))))
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose V) R))
            (instHSub.hSub
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.inv.inv W) R)
                  (Matrix.inv.inv
                    (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv W)) R)))
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul V R)
                  (Matrix.inv.inv
                    (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose V) R)))).transpose)

Direct statement dependencies (2)

HansenEconometrics.emdAsymptoticVariance
HansenEconometrics.mdAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:3907

theorem HansenEconometrics.emdAsymptoticVariance_le_md_concrete

Hansen Theorem 8.9, equation (8.28): efficient MD weakly lowers asymptotic variance relative to any symmetric minimum-distance weight at this abstraction layer.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (W : Matrix k k Real) (R : Matrix k q Real) (V : Matrix k k Real),
  Eq W.transpose W →
    Eq V.transpose V →
      IsUnit
          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose V) R).det →
        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose V) R).PosSemidef →
          (instHSub.hSub (HansenEconometrics.mdAsymptoticVariance W R V)
              (HansenEconometrics.emdAsymptoticVariance R V)).PosSemidef

Direct statement dependencies (2)

HansenEconometrics.emdAsymptoticVariance
HansenEconometrics.mdAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:3961

theorem HansenEconometrics.emdBeta_tendstoInDistribution_gaussian

Hansen Theorem 8.9 efficient-MD distribution wrapper.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} {Ω' : Type u_4} [inst_4 : MeasurableSpace Ω] [inst_5 : MeasurableSpace Ω']
  {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [inst_6 : MeasureTheory.IsProbabilityMeasure μ]
  [inst_7 : MeasureTheory.IsProbabilityMeasure ν] (root : Nat → Real) (bhat : Nat → Ω → k → Real) (R : Matrix k q Real)
  (c : q → Real) (V : Matrix k k Real) (β : k → Real) (T : Nat → Ω → k → Real) (Z : Ω' → k → Real),
  MeasureTheory.TendstoInDistribution (fun n ω => (HansenEconometrics.mdLinearMap (Matrix.inv.inv V) R).mulVec (T n ω))
      Filter.atTop Z (fun x => μ) ν →
    (MeasureTheory.TendstoInMeasure μ
        (instHSub.hSub (HansenEconometrics.emdScaledError root bhat R c V β) fun n ω =>
          (HansenEconometrics.mdLinearMap (Matrix.inv.inv V) R).mulVec (T n ω))
        Filter.atTop fun x => 0) →
      (∀ (n : Nat), AEMeasurable (HansenEconometrics.emdScaledError root bhat R c V β n) μ) →
        MeasureTheory.TendstoInDistribution (HansenEconometrics.emdScaledError root bhat R c V β) Filter.atTop Z
          (fun x => μ) ν

Direct statement dependencies (2)

HansenEconometrics.emdScaledError
HansenEconometrics.mdLinearMap

HansenEconometrics/Chapter8Asymptotics.lean:3632

theorem HansenEconometrics.mdAsymptoticVariance_efficientWeight_eq_emd

Hansen Theorem 8.9: the MD asymptotic variance at the efficient weight V⁻¹ equals the efficient-MD asymptotic variance.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (R : Matrix k q Real) (V : Matrix k k Real),
  IsUnit V.det →
    Eq V.transpose V →
      IsUnit
          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose V) R).det →
        Eq (HansenEconometrics.mdAsymptoticVariance (Matrix.inv.inv V) R V)
          (HansenEconometrics.emdAsymptoticVariance R V)

Direct statement dependencies (2)

HansenEconometrics.emdAsymptoticVariance
HansenEconometrics.mdAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:3717

theorem HansenEconometrics.emdBeta_tendstoInDistribution_multivariateGaussian

Hansen Theorem 8.9 efficient-MD distribution with the final covariance written as emdAsymptoticVariance, from explicit linearization inputs. The stable-interface version emdBeta_tendstoInDistribution_multivariateGaussian_of_linearization packages the same EMD linearization capability as AsymptoticallyLinearEstimator.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_5 : MeasureTheory.IsProbabilityMeasure μ] (root : Nat → Real) (bhat : Nat → Ω → k → Real) (R : Matrix k q Real)
  (c : q → Real) (V : Matrix k k Real) (β : k → Real) (T : Nat → Ω → k → Real),
  V.PosSemidef →
    IsUnit V.det →
      Eq V.transpose V →
        IsUnit
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose V) R).det →
          (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (bhat n) μ) →
            MeasureTheory.TendstoInDistribution T Filter.atTop (fun z => z.ofLp) (fun x => μ)
                (ProbabilityTheory.multivariateGaussian 0 V) →
              (MeasureTheory.TendstoInMeasure μ
                  (instHSub.hSub (HansenEconometrics.emdScaledError root bhat R c V β) fun n ω =>
                    (HansenEconometrics.mdLinearMap (Matrix.inv.inv V) R).mulVec (T n ω))
                  Filter.atTop fun x => 0) →
                MeasureTheory.TendstoInDistribution (HansenEconometrics.emdScaledError root bhat R c V β) Filter.atTop
                  (fun z => z.ofLp) (fun x => μ)
                  (ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.emdAsymptoticVariance R V))

Direct statement dependencies (3)

HansenEconometrics.emdAsymptoticVariance
HansenEconometrics.emdScaledError
HansenEconometrics.mdLinearMap

HansenEconometrics/Chapter8Asymptotics.lean:3761

theorem HansenEconometrics.emdBeta_tendstoInDistribution_gaussian_of_measurable

Hansen Theorem 8.9 efficient-MD distribution wrapper with scaled-error measurability discharged from unrestricted-estimator measurability.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} {Ω' : Type u_4} [inst_4 : MeasurableSpace Ω] [inst_5 : MeasurableSpace Ω']
  {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [inst_6 : MeasureTheory.IsProbabilityMeasure μ]
  [inst_7 : MeasureTheory.IsProbabilityMeasure ν] (root : Nat → Real) (bhat : Nat → Ω → k → Real) (R : Matrix k q Real)
  (c : q → Real) (V : Matrix k k Real) (β : k → Real) (T : Nat → Ω → k → Real) (Z : Ω' → k → Real),
  (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (bhat n) μ) →
    MeasureTheory.TendstoInDistribution
        (fun n ω => (HansenEconometrics.mdLinearMap (Matrix.inv.inv V) R).mulVec (T n ω)) Filter.atTop Z (fun x => μ)
        ν →
      (MeasureTheory.TendstoInMeasure μ
          (instHSub.hSub (HansenEconometrics.emdScaledError root bhat R c V β) fun n ω =>
            (HansenEconometrics.mdLinearMap (Matrix.inv.inv V) R).mulVec (T n ω))
          Filter.atTop fun x => 0) →
        MeasureTheory.TendstoInDistribution (HansenEconometrics.emdScaledError root bhat R c V β) Filter.atTop Z
          (fun x => μ) ν

Direct statement dependencies (2)

HansenEconometrics.emdScaledError
HansenEconometrics.mdLinearMap

HansenEconometrics/Chapter8Asymptotics.lean:3650

Section 8.96 of 9 linked endpoints

For the exclusion restriction \beta_2=0, the long, short/CLS, and efficient restricted estimators have the displayed asymptotic variances; under heteroskedasticity, V_{\mathrm{EMD}}\preceq V_{\mathrm{long}} while V_{\mathrm{short}} can be larger.

theorem HansenEconometrics.scalarSchurVariance_heteroskedasticExample

Hansen Section 8.9 heteroskedastic example: Q₁₁·₂ = 3/4.

Formal statement

Eq (HansenEconometrics.scalarSchurVariance 1 (1 / 2) (1 / 2) 1) (3 / 4)

Direct statement dependencies (1)

HansenEconometrics.scalarSchurVariance

HansenEconometrics/Chapter8Asymptotics.lean:372

theorem HansenEconometrics.scalarLongRegressionAsymptoticVariance_heteroskedasticExample

Hansen equation (8.32) in the Section 8.9 heteroskedastic example.

Formal statement

Eq (HansenEconometrics.scalarLongRegressionAsymptoticVariance 1 (1 / 2) (1 / 2) 1 1 (7 / 8) (7 / 8) 1) (2 / 3)

Direct statement dependencies (1)

HansenEconometrics.scalarLongRegressionAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:377

theorem HansenEconometrics.scalarShortRegressionAsymptoticVariance_heteroskedasticExample

Hansen equation (8.33) in the Section 8.9 heteroskedastic example.

Formal statement

Eq (HansenEconometrics.scalarShortRegressionAsymptoticVariance 1 1) 1

Direct statement dependencies (1)

HansenEconometrics.scalarShortRegressionAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:383

theorem HansenEconometrics.scalarExclusionRestriction_heteroskedasticExample_variance_order

Hansen Section 8.9 heteroskedastic example: efficient MD has the smallest variance, while the short-regression CLS variance exceeds the unrestricted long-regression variance.

Formal statement

And
  (Real.instLT.lt (HansenEconometrics.scalarEfficientRestrictedAsymptoticVariance (2 / 3) (1 / 6) (1 / 6) (2 / 3))
    (HansenEconometrics.scalarLongRegressionAsymptoticVariance 1 (1 / 2) (1 / 2) 1 1 (7 / 8) (7 / 8) 1))
  (Real.instLT.lt (HansenEconometrics.scalarLongRegressionAsymptoticVariance 1 (1 / 2) (1 / 2) 1 1 (7 / 8) (7 / 8) 1)
    (HansenEconometrics.scalarShortRegressionAsymptoticVariance 1 1))

Direct statement dependencies (3)

HansenEconometrics.scalarEfficientRestrictedAsymptoticVariance
HansenEconometrics.scalarLongRegressionAsymptoticVariance
HansenEconometrics.scalarShortRegressionAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:395

theorem HansenEconometrics.scalarEfficientRestrictedAsymptoticVariance_heteroskedasticExample

Hansen equation (8.34) in the Section 8.9 heteroskedastic example.

Formal statement

Eq (HansenEconometrics.scalarEfficientRestrictedAsymptoticVariance (2 / 3) (1 / 6) (1 / 6) (2 / 3)) (5 / 8)

Direct statement dependencies (1)

HansenEconometrics.scalarEfficientRestrictedAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:388

def HansenEconometrics.scalarSchurVariance

Scalar Schur-complement variance Q₁₁·₂ used in Hansen Section 8.9.

Formal statement

Real → Real → Real → Real → Real

HansenEconometrics/Chapter8Asymptotics.lean:347

Section 8.106 of 20 linked endpoints

The plug-in covariance and standard error satisfy \hat V_{\mathrm{EMD}}\xrightarrow{p}V_{\mathrm{EMD}} and \widehat{\operatorname{se}}(a'\tilde\beta)=n^{-1/2}\sqrt{a'\hat V_{\mathrm{EMD}}a}.

theorem HansenEconometrics.emdCovarianceEstimator_eq_hansen

Hansen equation (8.35) written in expanded matrix form.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq q] (R : Matrix k q Real)
  (Vhat : Matrix k k Real),
  Eq (HansenEconometrics.emdCovarianceEstimator R Vhat)
    (instHSub.hSub Vhat
      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul Vhat R)
            (Matrix.inv.inv
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose Vhat) R)))
          R.transpose)
        Vhat))

Direct statement dependencies (1)

HansenEconometrics.emdCovarianceEstimator

HansenEconometrics/Chapter8Asymptotics.lean:708

def HansenEconometrics.emdStdError

Hansen equation (8.36) specialized to the efficient-MD plug-in covariance estimator.

Formal statement

{k : Type u_1} →
  {q : Type u_2} →
    [Fintype k] → [Fintype q] → [DecidableEq q] → Real → (k → Real) → Matrix k q Real → Matrix k k Real → Real

HansenEconometrics/Chapter8Asymptotics.lean:715

def HansenEconometrics.covarianceStdError

Hansen equation (8.36): finite-sample standard error for h’β̂, written as the asymptotic covariance scale divided by the square-root normalization.

Formal statement

{k : Type u_1} → [Fintype k] → Real → (k → Real) → Matrix k k Real → Real

HansenEconometrics/Chapter8Asymptotics.lean:454

def HansenEconometrics.emdCovarianceEstimator

Hansen equation (8.35): efficient-MD plug-in covariance estimator from an unrestricted covariance estimator.

Formal statement

{k : Type u_1} →
  {q : Type u_2} → [Fintype k] → [Fintype q] → [DecidableEq q] → Matrix k q Real → Matrix k k Real → Matrix k k Real

HansenEconometrics/Chapter8Asymptotics.lean:702

theorem HansenEconometrics.emdStdError_eq_hansen

Expanded form of the efficient-MD standard error for h’β.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq q] (root : Real)
  (h : k → Real) (R : Matrix k q Real) (Vhat : Matrix k k Real),
  Eq (HansenEconometrics.emdStdError root h R Vhat)
    (instHDiv.hDiv (dotProduct h ((HansenEconometrics.emdCovarianceEstimator R Vhat).mulVec h)).sqrt root)

Direct statement dependencies (2)

HansenEconometrics.emdCovarianceEstimator
HansenEconometrics.emdStdError

HansenEconometrics/Chapter8Asymptotics.lean:721

theorem HansenEconometrics.covarianceStdError_eq_inv_mul_scale

The finite-sample standard error in (8.36) is the same as root⁻¹ times the asymptotic standard-error scale.

Formal statement

∀ {k : Type u_1} [inst : Fintype k] (root : Real) (h : k → Real) (V : Matrix k k Real),
  Eq (HansenEconometrics.covarianceStdError root h V)
    (instHMul.hMul (Real.instInv.inv root) (HansenEconometrics.covarianceStdErrorScale h V))

Direct statement dependencies (2)

HansenEconometrics.covarianceStdError
HansenEconometrics.covarianceStdErrorScale

HansenEconometrics/Chapter8Asymptotics.lean:466

Section 8.116 of 8 linked endpoints

Under the restriction, \operatorname{Avar}(\hat\beta-\tilde\beta_{\mathrm{EMD}})=V_\beta-V_{\beta,\mathrm{EMD}}.

theorem HansenEconometrics.emdDifferenceAsymptoticVariance_eq_gap

Hansen Section 8.11, equation (8.37): the asymptotic variance of the Hausman difference equals the unrestricted asymptotic variance minus the efficient restricted asymptotic variance.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq q] (R : Matrix k q Real)
  (V : Matrix k k Real),
  Eq V.transpose V →
    IsUnit
        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose V) R).det →
      Eq (HansenEconometrics.emdDifferenceAsymptoticVariance R V)
        (instHSub.hSub V (HansenEconometrics.emdAsymptoticVariance R V))

Direct statement dependencies (2)

HansenEconometrics.emdAsymptoticVariance
HansenEconometrics.emdDifferenceAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:4035

theorem HansenEconometrics.emdDifference_tendstoInDistribution_multivariateGaussian

Hansen Section 8.11: Gaussian limit for the Hausman difference between the unrestricted estimator and the efficient minimum-distance estimator.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_5 : MeasureTheory.IsProbabilityMeasure μ] (root : Nat → Real) (bhat : Nat → Ω → k → Real) (R : Matrix k q Real)
  (c : q → Real) (V : Matrix k k Real) (β : k → Real),
  V.PosSemidef →
    IsUnit V.det →
      Eq (R.transpose.mulVec β) c →
        MeasureTheory.TendstoInDistribution (fun n ω => instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) β))
            Filter.atTop (fun z => z.ofLp) (fun x => μ) (ProbabilityTheory.multivariateGaussian 0 V) →
          MeasureTheory.TendstoInDistribution (HansenEconometrics.emdDifferenceScaledError root bhat R c V) Filter.atTop
            (fun z => z.ofLp) (fun x => μ)
            (ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.emdDifferenceAsymptoticVariance R V))

Direct statement dependencies (2)

HansenEconometrics.emdDifferenceAsymptoticVariance
HansenEconometrics.emdDifferenceScaledError

HansenEconometrics/Chapter8Asymptotics.lean:4092

theorem HansenEconometrics.emdDifference_tendstoInDistribution_multivariateGaussian_gap

Hansen Section 8.11: the Hausman-difference Gaussian covariance can be written as V - V*, the difference between the unrestricted and efficient restricted asymptotic variances.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_5 : MeasureTheory.IsProbabilityMeasure μ] (root : Nat → Real) (bhat : Nat → Ω → k → Real) (R : Matrix k q Real)
  (c : q → Real) (V : Matrix k k Real) (β : k → Real),
  V.PosSemidef →
    IsUnit V.det →
      Eq V.transpose V →
        IsUnit
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose V) R).det →
          Eq (R.transpose.mulVec β) c →
            MeasureTheory.TendstoInDistribution (fun n ω => instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) β))
                Filter.atTop (fun z => z.ofLp) (fun x => μ) (ProbabilityTheory.multivariateGaussian 0 V) →
              MeasureTheory.TendstoInDistribution (HansenEconometrics.emdDifferenceScaledError root bhat R c V)
                Filter.atTop (fun z => z.ofLp) (fun x => μ)
                (ProbabilityTheory.multivariateGaussian 0
                  (instHSub.hSub V (HansenEconometrics.emdAsymptoticVariance R V)))

Direct statement dependencies (2)

HansenEconometrics.emdAsymptoticVariance
HansenEconometrics.emdDifferenceScaledError

HansenEconometrics/Chapter8Asymptotics.lean:4119

theorem HansenEconometrics.emdDifferenceScaledError_eq_linearMap

The scaled Hausman difference is exactly the fixed Hausman linear map applied to the unrestricted scaled error.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} (root : Nat → Real) (bhat : Nat → Ω → k → Real) (R : Matrix k q Real)
  (c : q → Real) (V : Matrix k k Real) (β : k → Real),
  IsUnit V.det →
    Eq (R.transpose.mulVec β) c →
      Eq (HansenEconometrics.emdDifferenceScaledError root bhat R c V) fun n ω =>
        (HansenEconometrics.emdDifferenceLinearMap R V).mulVec (instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) β))

Direct statement dependencies (2)

HansenEconometrics.emdDifferenceLinearMap
HansenEconometrics.emdDifferenceScaledError

HansenEconometrics/Chapter8Asymptotics.lean:4079

theorem HansenEconometrics.emdBetaStar_difference_eq_linearMap

Efficient-MD pointwise Hausman-difference algebra under the maintained restriction.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (R : Matrix k q Real) (c : q → Real) (V : Matrix k k Real) (β bhat : k → Real),
  IsUnit V.det →
    Eq (R.transpose.mulVec β) c →
      Eq (instHSub.hSub bhat (HansenEconometrics.emdBetaStar R c V bhat))
        ((HansenEconometrics.emdDifferenceLinearMap R V).mulVec (instHSub.hSub bhat β))

Direct statement dependencies (2)

HansenEconometrics.emdBetaStar
HansenEconometrics.emdDifferenceLinearMap

HansenEconometrics/Chapter8Asymptotics.lean:4059

def HansenEconometrics.emdDifferenceLinearMap

Linear map for the Hausman difference between the unrestricted estimator and the efficient minimum-distance estimator.

Formal statement

{k : Type u_1} →
  {q : Type u_2} → [Fintype k] → [Fintype q] → [DecidableEq q] → Matrix k q Real → Matrix k k Real → Matrix k k Real

HansenEconometrics/Chapter8Asymptotics.lean:4003

Section 8.136 of 19 linked endpoints

Under misspecification, MD converges to its weighted pseudo-true projection; under n^{-1/2} local alternatives, \sqrt n(\tilde\beta_{\mathrm{MD}}-\beta_n) has the stated shifted Gaussian limit.

theorem HansenEconometrics.mdMisspecified_tendstoInDistribution_multivariateGaussian

Hansen Section 8.13, equation (8.40): misspecified MD has the same centered Gaussian variance when centered at the sample pseudo-true value.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_5 : MeasureTheory.IsProbabilityMeasure μ] (root : Nat → Real) (bhat : Nat → Ω → k → Real)
  (What : Nat → Ω → Matrix k k Real) (W : Matrix k k Real) (R : Matrix k q Real) (cStar c : q → Real) (β : k → Real)
  (S : Matrix k k Real),
  S.PosSemidef →
    (∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (What n) μ) →
      (MeasureTheory.TendstoInMeasure μ What Filter.atTop fun x => W) →
        IsUnit W.det →
          IsUnit
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv W)) R).det →
            Eq (R.transpose.mulVec β) cStar →
              MeasureTheory.TendstoInDistribution (fun n ω => instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) β))
                  Filter.atTop (fun z => z.ofLp) (fun x => μ) (ProbabilityTheory.multivariateGaussian 0 S) →
                MeasureTheory.TendstoInDistribution
                  (HansenEconometrics.mdMisspecifiedScaledError root bhat What R cStar c β) Filter.atTop
                  (fun z => z.ofLp) (fun x => μ)
                  (ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.mdAsymptoticVariance W R S))

Direct statement dependencies (2)

HansenEconometrics.mdAsymptoticVariance
HansenEconometrics.mdMisspecifiedScaledError

HansenEconometrics/Chapter8Asymptotics.lean:3086

theorem HansenEconometrics.mdLocalAlternative_fixedWeight_tendstoInDistribution_multivariateGaussian

Hansen Section 8.13, equations (8.41)–(8.43), fixed-weight local-alternative MD limit. Under the local restriction root n • (Rᵀ β_n - c) = δ, the centered estimator has the usual MD covariance and a fixed local-alternative mean shift.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_5 : MeasureTheory.IsProbabilityMeasure μ] (root : Nat → Real) (bhat : Nat → Ω → k → Real) (W : Matrix k k Real)
  (R : Matrix k q Real) (c : q → Real) (βseq : Nat → k → Real) (δ : q → Real) (S : Matrix k k Real),
  S.PosSemidef →
    HansenEconometrics.LocalAlternativeRestriction root R c βseq δ →
      MeasureTheory.TendstoInDistribution (fun n ω => instHSMul.hSMul (root n) (instHSub.hSub (bhat n ω) (βseq n)))
          Filter.atTop (fun z => z.ofLp) (fun x => μ) (ProbabilityTheory.multivariateGaussian 0 S) →
        MeasureTheory.TendstoInDistribution (HansenEconometrics.mdLocalAlternativeScaledError root bhat W R c βseq)
          Filter.atTop (fun z => z.ofLp) (fun x => μ)
          (ProbabilityTheory.multivariateGaussian { ofLp := HansenEconometrics.mdLocalAlternativeBias W R δ }
            (HansenEconometrics.mdAsymptoticVariance W R S))

Direct statement dependencies (4)

HansenEconometrics.LocalAlternativeRestriction
HansenEconometrics.mdAsymptoticVariance
HansenEconometrics.mdLocalAlternativeBias
HansenEconometrics.mdLocalAlternativeScaledError

HansenEconometrics/Chapter8Asymptotics.lean:2830

def HansenEconometrics.mdPseudoTrueValue

Hansen Section 8.13, equation (8.38): the pseudo-true MD projection value when the population restriction is Rᵀ β = cStar, but the imposed restriction is c.

Formal statement

{k : Type u_1} →
  {q : Type u_2} →
    [Fintype k] →
      [Fintype q] →
        [DecidableEq k] →
          [DecidableEq q] → Matrix k k Real → Matrix k q Real → (q → Real) → (q → Real) → (k → Real) → k → Real

HansenEconometrics/Chapter8Asymptotics.lean:2265

def HansenEconometrics.mdSamplePseudoTrueValue

Hansen Section 8.13, equation (8.39): the sample pseudo-true value obtained by replacing the limiting weight in (8.38) with the sample weight.

Formal statement

{k : Type u_1} →
  {q : Type u_2} →
    [Fintype k] →
      [Fintype q] →
        [DecidableEq k] →
          [DecidableEq q] →
            {Ω : Type u_3} →
              (Nat → Ω → Matrix k k Real) → Matrix k q Real → (q → Real) → (q → Real) → (k → Real) → Nat → Ω → k → Real

HansenEconometrics/Chapter8Asymptotics.lean:2428

def HansenEconometrics.localUnrestrictedScaledError

Hansen Section 8.13, equation (8.42): unrestricted scaled error under a local parameter sequence.

Formal statement

{k : Type u_1} → {Ω : Type u_3} → (Nat → Real) → (Nat → Ω → k → Real) → (Nat → k → Real) → Nat → Ω → k → Real

HansenEconometrics/Chapter8Asymptotics.lean:2318

theorem HansenEconometrics.mdPseudoTrueValue_restrict

The pseudo-true value satisfies the imposed restriction when the restriction Gram is nonsingular.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (W : Matrix k k Real) (R : Matrix k q Real) (cStar c : q → Real) (β : k → Real),
  Eq (R.transpose.mulVec β) cStar →
    IsUnit
        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv W)) R).det →
      Eq (R.transpose.mulVec (HansenEconometrics.mdPseudoTrueValue W R cStar c β)) c

Direct statement dependencies (1)

HansenEconometrics.mdPseudoTrueValue

HansenEconometrics/Chapter8Asymptotics.lean:2272

Theorem 8.106 of 54 linked endpoints

For smooth nonlinear restrictions r(\beta)=c, both nonlinear MD and nonlinear CLS satisfy \sqrt n(\tilde\beta-\beta)\xrightarrow{d}N(0,V_{\mathrm{constrained}}).

theorem HansenEconometrics.nonlinearMdBeta_tendstoInDistribution_gaussian

Hansen Theorem 8.10 for nonlinear minimum distance at the stable-interface layer.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} {Ω' : Type u_4} [inst_4 : MeasurableSpace Ω] [inst_5 : MeasurableSpace Ω']
  {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [inst_6 : MeasureTheory.IsProbabilityMeasure μ]
  [inst_7 : MeasureTheory.IsProbabilityMeasure ν] (root : Nat → Real) (btilde : Nat → Ω → k → Real) (β : k → Real)
  (W : Matrix k k Real) (Rderiv : Matrix k q Real) (T : Nat → Ω → k → Real) (Z : Ω' → k → Real),
  MeasureTheory.TendstoInDistribution (fun n ω => (HansenEconometrics.mdLinearMap W Rderiv).mulVec (T n ω)) Filter.atTop
      Z (fun x => μ) ν →
    HansenEconometrics.ConstrainedEstimatorLinearization μ root btilde β W Rderiv T →
      MeasureTheory.TendstoInDistribution (HansenEconometrics.constrainedScaledError root btilde β) Filter.atTop Z
        (fun x => μ) ν

Direct statement dependencies (3)

HansenEconometrics.ConstrainedEstimatorLinearization
HansenEconometrics.constrainedScaledError
HansenEconometrics.mdLinearMap

HansenEconometrics/Chapter8Asymptotics.lean:4545

theorem HansenEconometrics.nonlinearClsBeta_tendstoInDistribution_gaussian

Hansen Theorem 8.10 for nonlinear constrained least squares at the stable-interface layer.

The CLS specialization uses the population Gram weight in the linearized MD map, matching the linear restriction specialization in Theorem 8.8.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} {Ω' : Type u_4} [inst_4 : MeasurableSpace Ω] [inst_5 : MeasurableSpace Ω']
  {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [inst_6 : MeasureTheory.IsProbabilityMeasure μ]
  [inst_7 : MeasureTheory.IsProbabilityMeasure ν] (root : Nat → Real) (btilde : Nat → Ω → k → Real) (β : k → Real)
  (Q : Matrix k k Real) (Rderiv : Matrix k q Real) (T : Nat → Ω → k → Real) (Z : Ω' → k → Real),
  MeasureTheory.TendstoInDistribution (fun n ω => (HansenEconometrics.mdLinearMap Q Rderiv).mulVec (T n ω)) Filter.atTop
      Z (fun x => μ) ν →
    HansenEconometrics.ConstrainedEstimatorLinearization μ root btilde β Q Rderiv T →
      MeasureTheory.TendstoInDistribution (HansenEconometrics.constrainedScaledError root btilde β) Filter.atTop Z
        (fun x => μ) ν

Direct statement dependencies (3)

HansenEconometrics.ConstrainedEstimatorLinearization
HansenEconometrics.constrainedScaledError
HansenEconometrics.mdLinearMap

HansenEconometrics/Chapter8Asymptotics.lean:4594

theorem HansenEconometrics.nonlinearFirstOrder_lagrangeMultiplier_eq_hansen

Hansen’s solved multiplier formula in the proof of Theorem 8.10. This is the line between the linearized constraint (8.53) and the substitution producing (8.54).

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (W : Matrix k k Real) (Rhat Rstar : Matrix k q Real) (β bhat btilde : k → Real)
  (lam : q → Real),
  Eq (instHSub.hSub bhat btilde)
      ((Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.inv.inv W) Rhat).mulVec lam) →
    Eq (Rstar.transpose.mulVec (instHSub.hSub btilde β)) 0 →
      IsUnit
          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul Rstar.transpose (Matrix.inv.inv W)) Rhat).det →
        Eq lam
          ((Matrix.inv.inv
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                  (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul Rstar.transpose (Matrix.inv.inv W)) Rhat)).mulVec
            (Rstar.transpose.mulVec (instHSub.hSub bhat β)))

HansenEconometrics/Chapter8Asymptotics.lean:1562

theorem HansenEconometrics.nonlinearMdBeta_tendstoInDistribution_multivariateGaussian

Hansen Theorem 8.10 for nonlinear minimum distance with the Gaussian image limit derived from the unrestricted estimator CLT.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_5 : MeasureTheory.IsProbabilityMeasure μ] (root : Nat → Real) (btilde : Nat → Ω → k → Real) (β : k → Real)
  (W : Matrix k k Real) (Rderiv : Matrix k q Real) (T : Nat → Ω → k → Real) (S : Matrix k k Real),
  S.PosSemidef →
    MeasureTheory.TendstoInDistribution T Filter.atTop (fun z => z.ofLp) (fun x => μ)
        (ProbabilityTheory.multivariateGaussian 0 S) →
      HansenEconometrics.ConstrainedEstimatorLinearization μ root btilde β W Rderiv T →
        MeasureTheory.TendstoInDistribution (HansenEconometrics.constrainedScaledError root btilde β) Filter.atTop
          (fun z => z.ofLp) (fun x => μ)
          (ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.mdAsymptoticVariance W Rderiv S))

Direct statement dependencies (3)

HansenEconometrics.ConstrainedEstimatorLinearization
HansenEconometrics.constrainedScaledError
HansenEconometrics.mdAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:4560

theorem HansenEconometrics.nonlinearClsBeta_tendstoInDistribution_multivariateGaussian

Hansen Theorem 8.10 for nonlinear constrained least squares with the Gaussian image limit derived from the unrestricted estimator CLT.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} [inst_4 : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_5 : MeasureTheory.IsProbabilityMeasure μ] (root : Nat → Real) (btilde : Nat → Ω → k → Real) (β : k → Real)
  (Q : Matrix k k Real) (Rderiv : Matrix k q Real) (T : Nat → Ω → k → Real) (S : Matrix k k Real),
  S.PosSemidef →
    MeasureTheory.TendstoInDistribution T Filter.atTop (fun z => z.ofLp) (fun x => μ)
        (ProbabilityTheory.multivariateGaussian 0 S) →
      HansenEconometrics.ConstrainedEstimatorLinearization μ root btilde β Q Rderiv T →
        MeasureTheory.TendstoInDistribution (HansenEconometrics.constrainedScaledError root btilde β) Filter.atTop
          (fun z => z.ofLp) (fun x => μ)
          (ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.clsAsymptoticVariance Q Rderiv S))

Direct statement dependencies (3)

HansenEconometrics.ConstrainedEstimatorLinearization
HansenEconometrics.clsAsymptoticVariance
HansenEconometrics.constrainedScaledError

HansenEconometrics/Chapter8Asymptotics.lean:4609

theorem HansenEconometrics.nonlinearConstrainedEstimator_tendstoInDistribution_gaussian

Hansen Theorem 8.10, interface-level nonlinear constrained-estimator limit.

The estimator-specific work is isolated in ConstrainedEstimatorLinearization: consistency of the constrained optimizer, differentiability of the restriction map, and first-order conditions should be used to construct that interface. This theorem performs the stable Slutsky step from the linearized representation to the asymptotic distribution.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {Ω : Type u_3} {Ω' : Type u_4} [inst_4 : MeasurableSpace Ω] [inst_5 : MeasurableSpace Ω']
  {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [inst_6 : MeasureTheory.IsProbabilityMeasure μ]
  [inst_7 : MeasureTheory.IsProbabilityMeasure ν] (root : Nat → Real) (btilde : Nat → Ω → k → Real) (β : k → Real)
  (W : Matrix k k Real) (Rderiv : Matrix k q Real) (T : Nat → Ω → k → Real) (Z : Ω' → k → Real),
  MeasureTheory.TendstoInDistribution (fun n ω => (HansenEconometrics.mdLinearMap W Rderiv).mulVec (T n ω)) Filter.atTop
      Z (fun x => μ) ν →
    HansenEconometrics.ConstrainedEstimatorLinearization μ root btilde β W Rderiv T →
      MeasureTheory.TendstoInDistribution (HansenEconometrics.constrainedScaledError root btilde β) Filter.atTop Z
        (fun x => μ) ν

Direct statement dependencies (3)

HansenEconometrics.ConstrainedEstimatorLinearization
HansenEconometrics.constrainedScaledError
HansenEconometrics.mdLinearMap

HansenEconometrics/Chapter8Asymptotics.lean:4493

Section 8.156 of 10 linked endpoints

For the restriction \beta\ge0, the constraint is asymptotically inactive when \beta\gt 0; at the boundary, \sqrt n\,\tilde\beta\xrightarrow{d}\max\{Z,0\}.

theorem HansenEconometrics.nonnegativeInterior_tendstoInDistribution

Hansen Section 8.15 interior case for a scalar nonnegativity restriction: if the constraint is asymptotically inactive, the constrained estimator has the same limit as the unrestricted estimator.

Formal statement

∀ {Ω : Type u_3} {Ω' : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω}
  {ν : MeasureTheory.Measure Ω'} [inst_2 : MeasureTheory.IsProbabilityMeasure μ]
  [inst_3 : MeasureTheory.IsProbabilityMeasure ν] (root : Nat → Real) (bhat : Nat → Ω → Real) (β : Real)
  (Z : Ω' → Real),
  (∀ (n : Nat), AEMeasurable (HansenEconometrics.nonnegativeConstrainedScalarScaledError root bhat β n) μ) →
    Real.instLT.lt 0 β →
      (MeasureTheory.TendstoInMeasure μ bhat Filter.atTop fun x => β) →
        MeasureTheory.TendstoInDistribution (HansenEconometrics.scalarScaledError root bhat β) Filter.atTop Z
            (fun x => μ) ν →
          MeasureTheory.TendstoInDistribution (HansenEconometrics.nonnegativeConstrainedScalarScaledError root bhat β)
            Filter.atTop Z (fun x => μ) ν

Direct statement dependencies (2)

HansenEconometrics.nonnegativeConstrainedScalarScaledError
HansenEconometrics.scalarScaledError

HansenEconometrics/Chapter8Asymptotics.lean:2985

theorem HansenEconometrics.nonnegativeInterior_asymptoticallyInactiveConstraint

Hansen Section 8.15 interior case: consistency for a strictly positive parameter makes the scalar nonnegativity constraint asymptotically inactive.

Formal statement

∀ {Ω : Type u_3} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ]
  (root : Nat → Real) (bhat : Nat → Ω → Real) (β : Real),
  (∀ (n : Nat), AEMeasurable (HansenEconometrics.nonnegativeConstrainedScalarScaledError root bhat β n) μ) →
    Real.instLT.lt 0 β →
      (MeasureTheory.TendstoInMeasure μ bhat Filter.atTop fun x => β) →
        HansenEconometrics.ScalarAsymptoticallyInactiveConstraint μ (HansenEconometrics.scalarScaledError root bhat β)
          (HansenEconometrics.nonnegativeConstrainedScalarScaledError root bhat β)

Direct statement dependencies (3)

HansenEconometrics.ScalarAsymptoticallyInactiveConstraint
HansenEconometrics.nonnegativeConstrainedScalarScaledError
HansenEconometrics.scalarScaledError

HansenEconometrics/Chapter8Asymptotics.lean:2951

theorem HansenEconometrics.nonnegativeBoundaryScaledError_tendstoInDistribution

Hansen Section 8.15 boundary case for a scalar nonnegativity restriction: if the unconstrained boundary statistic converges, the constrained statistic converges to the continuous image max Z 0.

Formal statement

∀ {Ω : Type u_3} {Ω' : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω}
  {ν : MeasureTheory.Measure Ω'} [inst_2 : MeasureTheory.IsProbabilityMeasure μ]
  [inst_3 : MeasureTheory.IsProbabilityMeasure ν] (root : Nat → Real) (bhat : Nat → Ω → Real) (Z : Ω' → Real),
  (∀ (n : Nat), Real.instLE.le 0 (root n)) →
    MeasureTheory.TendstoInDistribution (fun n ω => instHMul.hMul (root n) (bhat n ω)) Filter.atTop Z (fun x => μ) ν →
      MeasureTheory.TendstoInDistribution (HansenEconometrics.nonnegativeBoundaryScaledError root bhat) Filter.atTop
        (fun ω => Real.instMax.max (Z ω) 0) (fun x => μ) ν

Direct statement dependencies (1)

HansenEconometrics.nonnegativeBoundaryScaledError

HansenEconometrics/Chapter8Asymptotics.lean:3022

theorem HansenEconometrics.nonnegativeBoundaryScaledError_eq_max_scaled

With a nonnegative scaling sequence, scaling commutes with the one-dimensional nonnegativity projection at the boundary.

Formal statement

∀ {Ω : Type u_3} (root : Nat → Real) (bhat : Nat → Ω → Real),
  (∀ (n : Nat), Real.instLE.le 0 (root n)) →
    Eq (HansenEconometrics.nonnegativeBoundaryScaledError root bhat) fun n ω =>
      Real.instMax.max (instHMul.hMul (root n) (bhat n ω)) 0

Direct statement dependencies (1)

HansenEconometrics.nonnegativeBoundaryScaledError

HansenEconometrics/Chapter8Asymptotics.lean:3009

theorem HansenEconometrics.scalarAsymptoticallyInactiveConstraint_of_eventuallyEq

Constructor for the scalar inactive-constraint interface from eventual almost-sure equality of the scaled constrained and unrestricted statistics.

Formal statement

∀ {Ω : Type u_3} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ]
  (unrestricted constrained : Nat → Ω → Real),
  (∀ (n : Nat), AEMeasurable (constrained n) μ) →
    Filter.Eventually (fun n => (MeasureTheory.ae μ).EventuallyEq (constrained n) (unrestricted n)) Filter.atTop →
      HansenEconometrics.ScalarAsymptoticallyInactiveConstraint μ unrestricted constrained

Direct statement dependencies (1)

HansenEconometrics.ScalarAsymptoticallyInactiveConstraint

HansenEconometrics/Chapter8Asymptotics.lean:2915

theorem HansenEconometrics.scalarAsymptoticallyInactiveConstraint_tendstoInDistribution

If a scalar inequality constraint is asymptotically inactive, the constrained statistic has the same distributional limit as the unrestricted statistic.

Formal statement

∀ {Ω : Type u_3} {Ω' : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω}
  {ν : MeasureTheory.Measure Ω'} [inst_2 : MeasureTheory.IsProbabilityMeasure μ]
  [inst_3 : MeasureTheory.IsProbabilityMeasure ν] (unrestricted constrained : Nat → Ω → Real) (Z : Ω' → Real),
  HansenEconometrics.ScalarAsymptoticallyInactiveConstraint μ unrestricted constrained →
    MeasureTheory.TendstoInDistribution unrestricted Filter.atTop Z (fun x => μ) ν →
      MeasureTheory.TendstoInDistribution constrained Filter.atTop Z (fun x => μ) ν

Direct statement dependencies (1)

HansenEconometrics.ScalarAsymptoticallyInactiveConstraint

HansenEconometrics/Chapter8Asymptotics.lean:2902

Exercise 8.106 endpoints

Equations (8.22)–(8.23) give the MD multiplier and estimator; with W=Q_{XX}, \tilde\beta_{\mathrm{MD}}=\tilde\beta_{\mathrm{CLS}}.

def HansenEconometrics.mdLagrangeMultiplier

Hansen equation (8.22), the solved minimum-distance Lagrange multiplier.

Formal statement

{k : Type u_1} →
  {q : Type u_2} →
    [Fintype k] →
      [Fintype q] →
        [DecidableEq k] →
          [DecidableEq q] → Real → Matrix k k Real → Matrix k q Real → (q → Real) → (k → Real) → q → Real

HansenEconometrics/Chapter8Asymptotics.lean:76

theorem HansenEconometrics.mdLagrangeMultiplier_eq_hansen_822

Displayed formula for Hansen equation (8.22).

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (sampleSize : Real) (W : Matrix k k Real) (R : Matrix k q Real) (c : q → Real)
  (bhat : k → Real),
  Eq (HansenEconometrics.mdLagrangeMultiplier sampleSize W R c bhat)
    (instHSMul.hSMul sampleSize
      ((Matrix.inv.inv
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv W)) R)).mulVec
        (instHSub.hSub (R.transpose.mulVec bhat) c)))

Direct statement dependencies (1)

HansenEconometrics.mdLagrangeMultiplier

HansenEconometrics/Chapter8Asymptotics.lean:82

theorem HansenEconometrics.mdBetaStar_eq_hansen_823

Displayed formula for Hansen equation (8.23).

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (W : Matrix k k Real) (R : Matrix k q Real) (c : q → Real) (bhat : k → Real),
  Eq (HansenEconometrics.mdBetaStar W R c bhat)
    (instHSub.hSub bhat
      ((Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.inv.inv W) R)
            (Matrix.inv.inv
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose (Matrix.inv.inv W)) R))).mulVec
        (instHSub.hSub (R.transpose.mulVec bhat) c)))

Direct statement dependencies (1)

HansenEconometrics.mdBetaStar

HansenEconometrics/Chapter8Asymptotics.lean:89

theorem HansenEconometrics.sampleGram_nonsingInv_eq_card_smul_invOf

On nonsingular designs, the inverse of the sample Gram is the sample size times the typeclass inverse of the unnormalized Gram.

Formal statement

∀ {k : Type u_1} [inst : Fintype k] [inst_1 : DecidableEq k] {n : Type u_3} [inst_2 : Fintype n] (X : Matrix n k Real)
  [inst_3 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)],
  Eq (Matrix.inv.inv (HansenEconometrics.sampleGram X))
    (instHSMul.hSMul (Fintype.card n).cast
      (inst_3.invOf (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)))

Direct statement dependencies (1)

HansenEconometrics.sampleGram

HansenEconometrics/Chapter8Asymptotics.lean:96

theorem HansenEconometrics.mdBetaStar_sampleGram_olsBetaStar_eq_clsBetaStar

Exercise 8.10 bridge: MD with the sample-Gram weight is the Star CLS estimator.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {n : Type u_3} [inst_4 : Fintype n] (X : Matrix n k Real) (y : n → Real)
  (R : Matrix k q Real) (c : q → Real),
  Eq (HansenEconometrics.mdBetaStar (HansenEconometrics.sampleGram X) R c (HansenEconometrics.olsBetaStar X y))
    (HansenEconometrics.clsBetaStar X y R c)

Direct statement dependencies (4)

HansenEconometrics.clsBetaStar
HansenEconometrics.mdBetaStar
HansenEconometrics.olsBetaStar
HansenEconometrics.sampleGram

HansenEconometrics/Chapter8Asymptotics.lean:104

theorem HansenEconometrics.clsBetaStar_eq_clsBeta

Exercise 8.10 bridge: under the usual nonsingularity hypotheses, the sample-Gram minimum-distance specialization agrees with the finite-sample CLS estimator.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] {n : Type u_3} [inst_4 : Fintype n] [Nonempty n] (X : Matrix n k Real) (y : n → Real)
  (R : Matrix k q Real) (c : q → Real)
  [inst_6 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul X.transpose X)]
  [inst_7 : Invertible (HansenEconometrics.clsConstraintGram X R)],
  Eq (HansenEconometrics.clsBetaStar X y R c) (HansenEconometrics.clsBeta X y R c)

Direct statement dependencies (3)

HansenEconometrics.clsBeta
HansenEconometrics.clsBetaStar
HansenEconometrics.clsConstraintGram

HansenEconometrics/Chapter8Asymptotics.lean:111

Exercises 8.14-8.153 endpoints

With W=V_\beta^{-1}, the MD covariance is V_{\beta,\mathrm{EMD}}=V_\beta-V_\beta R(R'V_\beta R)^{-1}R'V_\beta\preceq V_\beta.

theorem HansenEconometrics.emdAsymptoticVariance_eq_hansen_826

Hansen equation (8.26), the displayed efficient-MD asymptotic variance formula.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq q] (R : Matrix k q Real)
  (V : Matrix k k Real),
  Eq (HansenEconometrics.emdAsymptoticVariance 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.emdAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:3890

theorem HansenEconometrics.mdAsymptoticVariance_efficientWeight_eq_hansen_826

Exercise 8.14: Hansen equation (8.26) is the generic MD variance at efficient weight W = V⁻¹.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq k]
  [inst_3 : DecidableEq q] (R : Matrix k q Real) (V : Matrix k k Real),
  IsUnit V.det →
    Eq V.transpose V →
      IsUnit
          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose V) R).det →
        Eq (HansenEconometrics.mdAsymptoticVariance (Matrix.inv.inv V) 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.mdAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:3897

theorem HansenEconometrics.emdAsymptoticVariance_le_unrestricted_hansen_827

Exercise 8.15, Hansen equation (8.27): efficient MD weakly lowers asymptotic variance relative to the unrestricted estimator.

Formal statement

∀ {k : Type u_1} {q : Type u_2} [inst : Fintype k] [inst_1 : Fintype q] [inst_2 : DecidableEq q] (R : Matrix k q Real)
  (V : Matrix k k Real),
  Eq V.transpose V →
    (Matrix.inv.inv
          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R.transpose V) R)).PosSemidef →
      (instHSub.hSub V (HansenEconometrics.emdAsymptoticVariance R V)).PosSemidef

Direct statement dependencies (1)

HansenEconometrics.emdAsymptoticVariance

HansenEconometrics/Chapter8Asymptotics.lean:3994