Chapter 11: Multivariate Regression

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

This page is generated from the canonical Chapter 11 inventory and the compiled Lean environment. It contains 12 textbook result groups and 14 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 11.12 endpoints

Under Assumption 7.2, system least squares satisfies \sqrt n(\hat\beta_{\mathrm{SLS}}-\beta)\xrightarrow{d}N(0,V_{\mathrm{SLS}}).

theorem HansenEconometrics.SystemLeastSquaresTheorem11_1.orZeroObs_of_equation_blocks

Hansen Theorem 11.1 with the displayed equation-specific block design.

This thin wrapper permits equation-specific regressor dimensions, identifies Q = E[Xᵢ’Xᵢ] with the block-diagonal matrix whose jth block is E[X_{ji}X_{ji}’], and reuses the observed-row system CLT above.

Formal statement

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsProbabilityMeasure μ] {m : Type u_4} [inst_2 : Fintype m] [inst_3 : DecidableEq m]
  {κ : m → Type u_5} [inst_4 : (j : m) → Fintype (κ j)] [inst_5 : (j : m) → DecidableEq (κ j)]
  {x : Nat → Ω → (j : m) → κ j → Real} {e Y : Nat → Ω → m → Real} {β : Sigma κ → Real},
  HansenEconometrics.SystemObservedResponseFourthMomentConditions μ
      (fun i ω => HansenEconometrics.systemEquationBlockDesign (x i ω)) e Y β →
    MeasureTheory.TendstoInDistribution
      (fun t ω =>
        instHSMul.hSMul t.cast.sqrt
          (instHSub.hSub
            (HansenEconometrics.systemLeastSquaresBetaOrZeroObs
              (fun i => HansenEconometrics.systemEquationBlockDesign (x i.val ω)) fun i => Y i.val ω)
            β))
      Filter.atTop (fun z => z.ofLp) (fun x => μ)
      (ProbabilityTheory.multivariateGaussian 0
        (HansenEconometrics.systemAsymptoticVariance (HansenEconometrics.systemEquationBlockPopulationGram μ x)
          (HansenEconometrics.systemPopulationScoreCovariance μ
            (fun i ω => HansenEconometrics.systemEquationBlockDesign (x i ω)) e)))

Direct statement dependencies (6)

• HansenEconometrics.SystemObservedResponseFourthMomentConditions
• HansenEconometrics.systemAsymptoticVariance
• HansenEconometrics.systemEquationBlockDesign
• HansenEconometrics.systemEquationBlockPopulationGram
• HansenEconometrics.systemLeastSquaresBetaOrZeroObs
• HansenEconometrics.systemPopulationScoreCovariance

HansenEconometrics/Chapter11MultivariateRegression/Asymptotics.lean:2270

theorem HansenEconometrics.SystemLeastSquaresTheorem11_1.orZeroObs_of_observed_assumption72

Hansen Theorem 11.1 from literal observed-row Assumption 7.2.

The residual-row iid, Gram WLLN, score CLT, and population nonsingularity inputs are derived from observed (Xᵢ,Yᵢ) iid rows, Hansen’s fourth moments, orthogonality, and positive definiteness of Q.

Formal statement

∀ {Ω : Type u_1} {k : Type u_2} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsProbabilityMeasure μ] [inst_2 : Fintype k] [inst_3 : DecidableEq k] {m : Type u_4}
  [inst_4 : Fintype m] {X : Nat → Ω → Matrix m k Real} {e Y : Nat → Ω → m → Real} {β : k → Real},
  HansenEconometrics.SystemObservedResponseFourthMomentConditions μ X e Y β →
    MeasureTheory.TendstoInDistribution
      (fun t ω =>
        instHSMul.hSMul t.cast.sqrt
          (instHSub.hSub (HansenEconometrics.systemLeastSquaresBetaOrZeroObs (fun i => X i.val ω) fun i => Y i.val ω)
            β))
      Filter.atTop (fun z => z.ofLp) (fun x => μ)
      (ProbabilityTheory.multivariateGaussian 0
        (HansenEconometrics.systemAsymptoticVariance (HansenEconometrics.systemPopulationGram μ X)
          (HansenEconometrics.systemPopulationScoreCovariance μ X e)))

Direct statement dependencies (5)

• HansenEconometrics.SystemObservedResponseFourthMomentConditions
• HansenEconometrics.systemAsymptoticVariance
• HansenEconometrics.systemLeastSquaresBetaOrZeroObs
• HansenEconometrics.systemPopulationGram
• HansenEconometrics.systemPopulationScoreCovariance

HansenEconometrics/Chapter11MultivariateRegression/Asymptotics.lean:2248

Theorem 11.22 endpoints

For a smooth map h, \sqrt n(h(\hat\beta_{\mathrm{SLS}})-h(\beta))\xrightarrow{d}N(0,H'V_{\mathrm{SLS}}H).

theorem HansenEconometrics.SystemDelta.orZeroObs_of_observed_rows_contDiffAt

Hansen Theorem 11.2 from literal observed-row Assumption 7.2 and the literal ContDiffAt Assumption 7.3 surface.

Formal statement

∀ {Ω : Type u_1} {k : Type u_2} {q : Type u_3} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsProbabilityMeasure μ] [inst_2 : Fintype k] [inst_3 : Fintype q] [inst_4 : DecidableEq k]
  [inst_5 : DecidableEq q] {m : Type u_4} [inst_6 : Fintype m] {X : Nat → Ω → Matrix m k Real}
  {e Y : Nat → Ω → m → Real} {r : (k → Real) → q → Real} {β : k → Real} {R : Matrix k q Real},
  HansenEconometrics.SystemObservedResponseFourthMomentConditions μ X e Y β →
    ∀ (h73 : HansenEconometrics.SystemDeltaContDiffAtConditions r β R),
      MeasureTheory.TendstoInDistribution
        (fun t ω =>
          instHSMul.hSMul t.cast.sqrt
            (instHSub.hSub
              (r (HansenEconometrics.systemLeastSquaresBetaOrZeroObs (fun i => X i.val ω) fun i => Y i.val ω)) (r β)))
        Filter.atTop (fun z => z.ofLp) (fun x => μ)
        (ProbabilityTheory.multivariateGaussian 0
          (HansenEconometrics.systemDeltaVariance
            (HansenEconometrics.systemAsymptoticVariance (HansenEconometrics.systemPopulationGram μ X)
              (HansenEconometrics.systemPopulationScoreCovariance μ X e))
            R))

Direct statement dependencies (7)

• HansenEconometrics.SystemDeltaContDiffAtConditions
• HansenEconometrics.SystemObservedResponseFourthMomentConditions
• HansenEconometrics.systemAsymptoticVariance
• HansenEconometrics.systemDeltaVariance
• HansenEconometrics.systemLeastSquaresBetaOrZeroObs
• HansenEconometrics.systemPopulationGram
• HansenEconometrics.systemPopulationScoreCovariance

HansenEconometrics/Chapter11MultivariateRegression/Asymptotics.lean:2473

theorem HansenEconometrics.SystemDelta.betaOrZeroObs_of_primitive_rows

Hansen Theorem 11.2 from the literal row-iid Assumption 7.2 surface and the generic Chapter 7 smooth-function Assumption 7.3 package, with transform measurability stated separately.

Formal statement

∀ {Ω : Type u_1} {k : Type u_2} {q : Type u_3} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsProbabilityMeasure μ] [inst_2 : Fintype k] [inst_3 : Fintype q] [inst_4 : DecidableEq k]
  [inst_5 : DecidableEq q] {m : Type u_4} [inst_6 : Fintype m] {X : Nat → Ω → Matrix m k Real}
  {e Y : Nat → Ω → m → Real} {r : (k → Real) → q → Real} {β : k → Real} {R : Matrix k q Real},
  HansenEconometrics.SystemPrimitiveRowRegressionMomentConditions μ X e →
    Measurable r →
      ∀ (h73 : HansenEconometrics.SmoothFunctionCondition r β R),
        (∀ (i : Nat) (ω : Ω) (j : m), Eq (Y i ω j) (instHAdd.hAdd (dotProduct (X i ω j) β) (e i ω j))) →
          MeasureTheory.TendstoInDistribution
            (fun t ω =>
              instHSMul.hSMul t.cast.sqrt
                (instHSub.hSub
                  (r (HansenEconometrics.systemLeastSquaresBetaOrZeroObs (fun i => X i.val ω) fun i => Y i.val ω))
                  (r β)))
            Filter.atTop (fun z => z.ofLp) (fun x => μ)
            (ProbabilityTheory.multivariateGaussian 0
              (HansenEconometrics.systemDeltaVariance
                (HansenEconometrics.systemAsymptoticVariance (HansenEconometrics.systemPopulationGram μ X)
                  (HansenEconometrics.systemPopulationScoreCovariance μ X e))
                R))

Direct statement dependencies (7)

• HansenEconometrics.SmoothFunctionCondition
• HansenEconometrics.SystemPrimitiveRowRegressionMomentConditions
• HansenEconometrics.systemAsymptoticVariance
• HansenEconometrics.systemDeltaVariance
• HansenEconometrics.systemLeastSquaresBetaOrZeroObs
• HansenEconometrics.systemPopulationGram
• HansenEconometrics.systemPopulationScoreCovariance

HansenEconometrics/Chapter11MultivariateRegression/Asymptotics.lean:2420

Theorem 11.31 endpoint

The robust and homoskedastic system covariance estimators are consistent: \hat V_{\mathrm{SLS}}\xrightarrow{p}V_{\mathrm{SLS}} and \hat V^0_{\mathrm{SLS}}\xrightarrow{p}V^0_{\mathrm{SLS}}.

theorem HansenEconometrics.SystemCovarianceTheorem11_3.of_observed_assumption72

Hansen Theorem 11.3 from literal observed-row Assumption 7.2.

The observed-row fourth moments derive all residual-substitution moments in the compact covariance package. Measurability of both displayed feasible middle matrices is derived from the observed rows and the Star estimator.

Formal statement

∀ {Ω : Type u_1} {k : Type u_2} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsProbabilityMeasure μ] [inst_2 : Fintype k] [inst_3 : DecidableEq k] {m : Type u_4}
  [inst_4 : Fintype m] {X : Nat → Ω → Matrix m k Real} {e Y : Nat → Ω → m → Real} {β : k → Real},
  HansenEconometrics.SystemObservedResponseFourthMomentConditions μ X e Y β →
    And
      (MeasureTheory.TendstoInMeasure μ
        (fun n ω => HansenEconometrics.systemRobustCovarianceStarObs (fun i => X i.val ω) fun i => Y i.val ω)
        Filter.atTop fun x =>
        HansenEconometrics.systemAsymptoticVariance (HansenEconometrics.systemPopulationGram μ X)
          (HansenEconometrics.systemPopulationScoreCovariance μ X e))
      (MeasureTheory.TendstoInMeasure μ
        (fun n ω => HansenEconometrics.systemHomoskedasticCovarianceStarObs (fun i => X i.val ω) fun i => Y i.val ω)
        Filter.atTop fun x =>
        HansenEconometrics.systemAsymptoticVariance (HansenEconometrics.systemPopulationGram μ X)
          (MeasureTheory.integral μ fun x =>
            (fun ω =>
                HansenEconometrics.systemMiddleTerm (X 0 ω)
                  (MeasureTheory.integral μ fun x => (fun ω => Matrix.vecMulVec (e 0 ω) (e 0 ω)) x))
              x))

Direct statement dependencies (7)

• HansenEconometrics.SystemObservedResponseFourthMomentConditions
• HansenEconometrics.systemAsymptoticVariance
• HansenEconometrics.systemHomoskedasticCovarianceStarObs
• HansenEconometrics.systemMiddleTerm
• HansenEconometrics.systemPopulationGram
• HansenEconometrics.systemPopulationScoreCovariance
• HansenEconometrics.systemRobustCovarianceStarObs

HansenEconometrics/Chapter11MultivariateRegression/Asymptotics.lean:5515

Theorem 11.41 endpoint

Under conditional homoskedasticity, feasible SUR satisfies \sqrt n(\hat\beta_{\mathrm{SUR}}-\beta)\xrightarrow{d}N(0,V_{\mathrm{SUR}}).

theorem HansenEconometrics.SURTheorem11_4.orZeroObs_of_observed_rows

Hansen Theorem 11.4 from the literal observed-row Assumption 7.2 surface, conditional mean zero, and the matrix conditional-homoskedasticity condition (11.8).

Formal statement

∀ {Ω : Type u_1} {k : Type u_2} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsProbabilityMeasure μ] [inst_2 : Fintype k] [inst_3 : DecidableEq k] {m : Type u_4}
  [inst_4 : Fintype m] [inst_5 : DecidableEq m] {ζ : Type u_5} [inst_6 : MeasurableSpace ζ] {Z : Ω → ζ}
  {X : Nat → Ω → Matrix m k Real} {e Y : Nat → Ω → m → Real} {Sigma : Matrix m m Real} {β : k → Real},
  HansenEconometrics.SystemObservedResponseFourthMomentConditions μ X e Y β →
    HansenEconometrics.MatrixSystemConditionalHomoskedasticity μ Z X e Sigma →
      HansenEconometrics.SystemConditionalMeanZero μ Z X e →
        Sigma.PosDef →
          MeasureTheory.TendstoInDistribution
            (fun t ω =>
              instHSMul.hSMul t.cast.sqrt
                (instHSub.hSub (HansenEconometrics.surBetaEstimatorOrZeroObs (fun i => X i.val ω) fun i => Y i.val ω)
                  β))
            Filter.atTop (fun z => z.ofLp) (fun x => μ)
            (ProbabilityTheory.multivariateGaussian 0
              (HansenEconometrics.surAsymptoticVariance
                (MeasureTheory.integral μ fun x =>
                  (fun ω => HansenEconometrics.systemMiddleTerm (X 0 ω) (Matrix.inv.inv Sigma)) x)))

Direct statement dependencies (6)

• HansenEconometrics.MatrixSystemConditionalHomoskedasticity
• HansenEconometrics.SystemConditionalMeanZero
• HansenEconometrics.SystemObservedResponseFourthMomentConditions
• HansenEconometrics.surAsymptoticVariance
• HansenEconometrics.surBetaEstimatorOrZeroObs
• HansenEconometrics.systemMiddleTerm

HansenEconometrics/Chapter11MultivariateRegression/SUR.lean:7416

Theorem 11.51 endpoint

SUR is asymptotically at least as efficient as system least squares: V_{\mathrm{SLS}}-V_{\mathrm{SUR}}\succeq0.

theorem HansenEconometrics.SURTheorem11_5.efficiency_of_observed_rows

Hansen Theorem 11.5 from the literal observed-row Assumption 7.2 surface and matrix conditional homoskedasticity (11.8).

The proof is a thin wrapper around the population Gauss-Markov comparison; the observed-row package supplies the primitive Assumption 7.2 facts and positive-definite Sigma supplies the inverse used by Hansen’s display.

Formal statement

∀ {Ω : Type u_1} {k : Type u_2} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsProbabilityMeasure μ] [inst_2 : Fintype k] [inst_3 : DecidableEq k] {m : Type u_4}
  [inst_4 : Fintype m] [inst_5 : DecidableEq m] {ζ : Type u_5} [inst_6 : MeasurableSpace ζ] {Z : Ω → ζ}
  {X : Nat → Ω → Matrix m k Real} {e Y : Nat → Ω → m → Real} {Sigma : Matrix m m Real} {β : k → Real},
  HansenEconometrics.SystemObservedResponseFourthMomentConditions μ X e Y β →
    HansenEconometrics.MatrixSystemConditionalHomoskedasticity μ Z X e Sigma →
      Sigma.PosDef →
        (instHSub.hSub
            (HansenEconometrics.systemAsymptoticVariance (HansenEconometrics.systemPopulationGram μ X)
              (HansenEconometrics.systemPopulationMiddle μ (fun ω => X 0 ω) Sigma))
            (HansenEconometrics.surAsymptoticVariance
              (MeasureTheory.integral μ fun x =>
                (fun ω => HansenEconometrics.systemMiddleTerm (X 0 ω) (Matrix.inv.inv Sigma)) x))).PosSemidef

Direct statement dependencies (7)

• HansenEconometrics.MatrixSystemConditionalHomoskedasticity
• HansenEconometrics.SystemObservedResponseFourthMomentConditions
• HansenEconometrics.surAsymptoticVariance
• HansenEconometrics.systemAsymptoticVariance
• HansenEconometrics.systemMiddleTerm
• HansenEconometrics.systemPopulationGram
• HansenEconometrics.systemPopulationMiddle

HansenEconometrics/Chapter11MultivariateRegression/SUR.lean:6558

Theorem 11.60 endpoints

Corrected target: the normalized feasible-SUR covariance converges to V_\beta^*=(\mathbb E[X_i'\Sigma^{-1}X_i])^{-1}, not to the OLS variance V_\beta in general.

The canonical crosswalk does not name a compiled Lean endpoint. See the chapter inventory for the current qualification.

Theorem 11.71 endpoint

The reduced-rank Gaussian estimator solves (\hat\Gamma,\hat B,\hat\Sigma)\in\operatorname*{arg\,max}_{\Gamma,B,\Sigma}\ell(\Gamma,B,\Sigma) and is recovered from the ordered residualized generalized eigenvectors.

theorem HansenEconometrics.reducedRankHansenTheorem11_7GaussianMLE_residualized_exists

Hansen Theorem 11.7 for residualized multivariate regression, including existence of the jointly selected primal and dual spectral blocks and the actual global Gaussian MLE conclusion.

The construction is tie-safe: no separation is assumed between the last selected root and the first omitted root. The selected-rank premise is the finite-sample condition ensuring that the positive exact-rank parameter space has a maximizer rather than only a lower-rank boundary supremum. Positive definiteness of the unrestricted residual Gram is required only for positive rank; the rank-zero case is handled directly from the residualized outcome Gram.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {r : Type u_3} {m : Type u_4} {ell : Type u_5} [inst : Fintype n] [inst_1 : Fintype k]
  [inst_2 : Fintype r] [inst_3 : Fintype m] [inst_4 : Fintype ell] [inst_5 : DecidableEq n] [inst_6 : DecidableEq k]
  [inst_7 : DecidableEq r] [inst_8 : DecidableEq m] [inst_9 : DecidableEq ell] (Z : Matrix n ell Real)
  (X : Matrix n k Real) (Y : Matrix n m Real)
  [inst_10 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul Z.transpose Z)]
  [inst_11 : Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (X.fromCols Z).transpose (X.fromCols Z))]
  [Invertible (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Y.fromCols Z).transpose (Y.fromCols Z))],
  instLTNat.lt 0 (Fintype.card n) →
    Or
        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.reducedRankTildeE X Z Y).transpose
            (HansenEconometrics.reducedRankTildeE X Z Y)).PosDef
        (IsEmpty r) →
      instLTNat.lt (Fintype.card r) (instMinNat.min (Fintype.card k) (Fintype.card m)) →
        instLENat.le (Fintype.card r)
            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (HansenEconometrics.reducedRankTildeX Z X).transpose
                (HansenEconometrics.reducedRankTildeY Z Y)).rank →
          Exists fun G =>
            Exists fun lambda =>
              Exists fun Aperp =>
                Exists fun eta =>
                  HansenEconometrics.ReducedRankHansenTheorem11_7GaussianMLE Z X
                    (HansenEconometrics.reducedRankTildeX Z X) Y (HansenEconometrics.reducedRankTildeY Z Y)
                    (HansenEconometrics.reducedRankTildeE X Z Y) G
                    (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                        (HansenEconometrics.reducedRankTildeY Z Y).transpose (HansenEconometrics.reducedRankTildeX Z X))
                      G)
                    (HansenEconometrics.reducedRankChat Z X Y G
                      (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                          (HansenEconometrics.reducedRankTildeY Z Y).transpose
                          (HansenEconometrics.reducedRankTildeX Z X))
                        G))
                    (instHSMul.hSMul (Real.instInv.inv (Fintype.card n).cast)
                      (instHSub.hSub
                        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                          (HansenEconometrics.reducedRankTildeY Z Y).transpose
                          (HansenEconometrics.reducedRankTildeY Z Y))
                        (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                            (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                              (HansenEconometrics.reducedRankTildeY Z Y).transpose
                              (HansenEconometrics.reducedRankTildeX Z X))
                            G)
                          (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                              (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul
                                (HansenEconometrics.reducedRankTildeY Z Y).transpose
                                (HansenEconometrics.reducedRankTildeX Z X))
                              G).transpose)))
                    Aperp lambda eta
                    (HansenEconometrics.reducedRankMaximizedLogLikelihood (HansenEconometrics.reducedRankTildeY Z Y)
                      lambda)

Direct statement dependencies (7)

• HansenEconometrics.ReducedRankHansenTheorem11_7GaussianMLE
• HansenEconometrics.reducedRankAperpIndex
• HansenEconometrics.reducedRankChat
• HansenEconometrics.reducedRankMaximizedLogLikelihood
• HansenEconometrics.reducedRankTildeE
• HansenEconometrics.reducedRankTildeX
• HansenEconometrics.reducedRankTildeY

HansenEconometrics/Chapter11MultivariateRegression/ReducedRankLikelihood.lean:2014

Theorem 11.82 endpoints

The jth principal component solves \max_{\lVert h\rVert=1,\,h\perp h_1,\ldots,h_{j-1}}\operatorname{Var}(h'Y)=\lambda_j, and the score covariance is diagonal.

theorem HansenEconometrics.ordered_covMat_principalComponents_theorem11_8

Hansen Theorem 11.8, bundled ordered-covariance endpoint for the full principal-component vector U = H’X.

Formal statement

∀ {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k] {Ω : Type u_3} [inst_2 : MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_3 : MeasureTheory.IsProbabilityMeasure μ] (X : Ω → k → Real),
  (∀ (i : k), MeasureTheory.MemLp (fun ω => X ω i) 2 μ) →
    HansenEconometrics.OrderedCovMatPrincipalComponentsTheorem11_8 μ X

Direct statement dependencies (1)

• HansenEconometrics.OrderedCovMatPrincipalComponentsTheorem11_8

HansenEconometrics/Chapter11MultivariateRegression/PCA.lean:992

theorem HansenEconometrics.ordered_covMat_maximizes_variance_feasibleBefore_iff_eigenvector

Hansen Theorem 11.8, optimizer/eigenspace characterization.

For the sequential feasible set, maximizing Var[h’X] is equivalent to lying in the eigenspace of the jth ordered covariance eigenvalue. The eigenspace form is the correct statement in the presence of repeated eigenvalues.

Formal statement

∀ {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k] {Ω : Type u_3} [inst_2 : MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → k → Real),
  (∀ (i : k), MeasureTheory.MemLp (fun ω => X ω i) 2 μ) →
    ∀ (j : Fin (Fintype.card k)) (h : k → Real),
      Iff
        (And (HansenEconometrics.pcaFeasibleBefore (HansenEconometrics.orderedPCEigenvector ⋯) j h)
          (∀ (g : k → Real),
            HansenEconometrics.pcaFeasibleBefore (HansenEconometrics.orderedPCEigenvector ⋯) j g →
              Real.instLE.le (ProbabilityTheory.variance (HansenEconometrics.principalComponent g X) μ)
                (ProbabilityTheory.variance (HansenEconometrics.principalComponent h X) μ)))
        (And (HansenEconometrics.pcaFeasibleBefore (HansenEconometrics.orderedPCEigenvector ⋯) j h)
          (Eq ((HansenEconometrics.covMat μ X).mulVec h)
            (instHSMul.hSMul (HansenEconometrics.orderedPCEigenvalue ⋯ j) h)))

Direct statement dependencies (6)

• HansenEconometrics.covMat
• HansenEconometrics.covMat_isHermitian
• HansenEconometrics.orderedPCEigenvalue
• HansenEconometrics.orderedPCEigenvector
• HansenEconometrics.pcaFeasibleBefore
• HansenEconometrics.principalComponent

HansenEconometrics/Chapter11MultivariateRegression/PCA.lean:625

Theorem 11.91 endpoint

Under score normalization, the least-squares factor estimator is the leading PCA solution, \hat F=YH_mD_m^{-1/2}, with the corresponding joint least-squares minimum.

theorem HansenEconometrics.factorPCTheorem11_9_with_jointLSMinimizer_of_sampleCovariance_rank_ge

Citeable Hansen Theorem 11.9 surface from the sharp selected sample-covariance rank condition: the PCA formula certificate and the literal normalized joint least-squares minimizer hold together.

Formal statement

∀ {n : Type u_1} {k : Type u_2} {r : Type u_3} [inst : Fintype n] [inst_1 : Fintype k] [inst_2 : Fintype r]
  [inst_3 : DecidableEq k] [inst_4 : DecidableEq r] [Nonempty n]
  (hcard : instLENat.le (Fintype.card r) (Fintype.card k)) (X : n → k → Real),
  instLENat.le (Fintype.card r) (HansenEconometrics.factorSampleCovariance X).rank →
    And
      (HansenEconometrics.FactorPCTheorem11_9 (HansenEconometrics.factorSampleCovariance X)
        (HansenEconometrics.factorLeadingPCEigenvectors ⋯ hcard)
        (Matrix.diagonal (HansenEconometrics.factorLeadingPCEigenvalues ⋯ hcard))
        (HansenEconometrics.factorPCDiagonalSqrtD (HansenEconometrics.factorLeadingPCEigenvalues ⋯ hcard))
        (HansenEconometrics.factorPCDiagonalInvSqrtD (HansenEconometrics.factorLeadingPCEigenvalues ⋯ hcard))
        (HansenEconometrics.factorLoadingEstimator (HansenEconometrics.factorLeadingPCEigenvectors ⋯ hcard)
          (HansenEconometrics.factorPCDiagonalSqrtD (HansenEconometrics.factorLeadingPCEigenvalues ⋯ hcard)))
        X fun i =>
        HansenEconometrics.factorScoreEstimator (HansenEconometrics.factorLeadingPCEigenvectors ⋯ hcard)
          (HansenEconometrics.factorPCDiagonalInvSqrtD (HansenEconometrics.factorLeadingPCEigenvalues ⋯ hcard)) (X i))
      (HansenEconometrics.FactorLeastSquaresNormalizedMinimizer X
        (HansenEconometrics.factorLoadingEstimator (HansenEconometrics.factorLeadingPCEigenvectors ⋯ hcard)
          (HansenEconometrics.factorPCDiagonalSqrtD (HansenEconometrics.factorLeadingPCEigenvalues ⋯ hcard)))
        fun i =>
        HansenEconometrics.factorScoreEstimator (HansenEconometrics.factorLeadingPCEigenvectors ⋯ hcard)
          (HansenEconometrics.factorPCDiagonalInvSqrtD (HansenEconometrics.factorLeadingPCEigenvalues ⋯ hcard)) (X i))

Direct statement dependencies (10)

• HansenEconometrics.FactorLeastSquaresNormalizedMinimizer
• HansenEconometrics.FactorPCTheorem11_9
• HansenEconometrics.factorLeadingPCEigenvalues
• HansenEconometrics.factorLeadingPCEigenvectors
• HansenEconometrics.factorLoadingEstimator
• HansenEconometrics.factorPCDiagonalInvSqrtD
• HansenEconometrics.factorPCDiagonalSqrtD
• HansenEconometrics.factorSampleCovariance
• HansenEconometrics.factorSampleCovariance_isHermitian
• HansenEconometrics.factorScoreEstimator

HansenEconometrics/Chapter11MultivariateRegression/FactorModels.lean:4427

Theorem 11.101 endpoint

If Y_i\sim N(\mu,\Sigma) independently, then \hat\Sigma\sim W_m(n-1,\Sigma/(n-1)).

theorem HansenEconometrics.sampleCovarianceMatrix_hasLaw_theorem11_10_wishart

Hansen Theorem 11.10 in the textbook’s literal Wishart notation.

The canonical sample-covariance proof above yields a scaled push-forward law; scaledWishartLaw_eq_wishartLaw_smul identifies it with W_m(n-1, (n-1)⁻¹Σ) exactly as displayed by Hansen.

Formal statement

∀ {Ω : Type u_1} {n : Type u_2} {m : Type u_3} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : Fintype n] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : DecidableEq m]
  [MeasureTheory.IsProbabilityMeasure μ] [Nonempty n] (Y : Ω → Matrix n m Real) (mean : m → Real)
  {Sigma : Matrix m m Real},
  Sigma.PosSemidef →
    (∀ (i : n), ProbabilityTheory.HasLaw (fun ω => Y ω i) (HansenEconometrics.rowGaussianLaw mean Sigma) μ) →
      ProbabilityTheory.iIndepFun (fun i ω => Y ω i) μ →
        ProbabilityTheory.HasLaw (fun ω => HansenEconometrics.sampleCovarianceMatrix (Y ω))
          (HansenEconometrics.wishartLaw
            (instHSMul.hSMul (Real.instInv.inv (instHSub.hSub (Fintype.card n).cast 1)) Sigma))
          μ

Direct statement dependencies (5)

• HansenEconometrics.rowGaussianLaw
• HansenEconometrics.sampleCenteringMatrix
• HansenEconometrics.sampleCenteringMatrix_isHermitian
• HansenEconometrics.sampleCovarianceMatrix
• HansenEconometrics.wishartLaw

HansenEconometrics/Chapter11MultivariateRegression/MatrixNormal.lean:2491

Theorem 11.111 endpoint

If W\sim W_m(n,\Sigma), then (\alpha'W^{-1}\alpha)^{-1}\sim\chi^2_{n-m+1}/(\alpha'\Sigma^{-1}\alpha).

theorem HansenEconometrics.inverseWishartLinearForm_hasLaw_theorem11_11_raw_of_posDef_card_le

Hansen Theorem 11.11, raw inverse-Wishart scalar endpoint.

This is the theorem-facing fixed-direction statement: if W ∼ Wishart_n(Σ), Σ is positive definite, α ≠ 0, and the Wishart degrees of freedom dominate the dimension, then (α’W⁻¹α)⁻¹ has Hansen’s scaled chi-square law. The proof reuses the standard-coordinate Schur-complement theorem, canonical rectangular Gaussian Gram nonsingularity, and deterministic square-root whitening/alignment.

Formal statement

∀ {Ω : Type u_1} {m : Type u_3} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [inst_1 : Fintype m]
  [inst_2 : DecidableEq m] {dfidx : Type u_4} [inst_3 : Fintype dfidx] (W : Ω → Matrix m m Real)
  (Sigma : Matrix m m Real) (α : m → Real),
  Sigma.PosDef →
    Ne α 0 →
      ProbabilityTheory.HasLaw W (HansenEconometrics.wishartLaw Sigma) μ →
        instLENat.le (Fintype.card m) (Fintype.card dfidx) →
          ProbabilityTheory.HasLaw (fun ω => HansenEconometrics.inverseWishartLinearForm α (W ω))
            (MeasureTheory.Measure.map
              (fun x => instHMul.hMul (Real.instInv.inv (dotProduct α ((Matrix.inv.inv Sigma).mulVec α))) x)
              (HansenEconometrics.chiSquared (instHAdd.hAdd (instHSub.hSub (Fintype.card dfidx) (Fintype.card m)) 1)))
            μ

Direct statement dependencies (3)

• HansenEconometrics.chiSquared
• HansenEconometrics.inverseWishartLinearForm
• HansenEconometrics.wishartLaw

HansenEconometrics/Chapter11MultivariateRegression/MatrixNormal.lean:7022

Theorem 11.121 endpoint

Hotelling’s statistic has the scaled law T^2\sim\frac{m(n-1)}{n-m}F_{m,n-m}.

theorem HansenEconometrics.hotellingT2HansenFStatistic_hasLaw_theorem11_12_of_iid_normal_rows_posDef

Hansen Theorem 11.12, normalized Hotelling F endpoint.

This is Hansen’s normalized form: under iid normal rows with positive-definite covariance, (n-m)/(m(n-1)) T² has the classical F_{m,n-m} law.

Formal statement

∀ {Ω : Type u_1} {n : Type u_2} {m : Type u_3} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : Fintype n] [inst_2 : Fintype m] [inst_3 : DecidableEq m] [MeasureTheory.IsProbabilityMeasure μ]
  (Y : Ω → Matrix n m Real) (μ0 : m → Real) {Sigma : Matrix m m Real},
  Sigma.PosDef →
    instLTNat.lt 0 (Fintype.card m) →
      instLTNat.lt 0 (instHSub.hSub (Fintype.card n) (Fintype.card m)) →
        (∀ (i : n), ProbabilityTheory.HasLaw (fun ω => Y ω i) (HansenEconometrics.rowGaussianLaw μ0 Sigma) μ) →
          ProbabilityTheory.iIndepFun (fun i ω => Y ω i) μ →
            ProbabilityTheory.HasLaw (fun ω => HansenEconometrics.hotellingT2HansenFStatistic (Y ω) μ0)
              (HansenEconometrics.classicalFDist (Fintype.card m) (instHSub.hSub (Fintype.card n) (Fintype.card m))) μ

Direct statement dependencies (3)

• HansenEconometrics.classicalFDist
• HansenEconometrics.hotellingT2HansenFStatistic
• HansenEconometrics.rowGaussianLaw

HansenEconometrics/Chapter11MultivariateRegression/MatrixNormal.lean:9406