Chapter 2: Conditional Expectation and Projection

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

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

T2.1 Simple Law of Iterated Expectations1 endpoint

\int \mathbb{E}[Y \mid \mathcal{G}] \, d\mu = \int Y \, d\mu

theorem HansenEconometrics.simple_law_iterated_expectation

Theorem 2.1, specialized to Mathlib notation: simple law of iterated expectations.

Formal statement

∀ {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → Real}
  (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  Eq (MeasureTheory.integral μ fun ω => MeasureTheory.condExp m μ Y ω) (MeasureTheory.integral μ fun ω => Y ω)

HansenEconometrics/Chapter2CondExp.lean:18

T2.2 Tower Property2 endpoints

\mathbb{E}[\mathbb{E}[Y \mid \mathcal{G}_2] \mid \mathcal{G}_1] = \mathbb{E}[Y \mid \mathcal{G}_1]

theorem HansenEconometrics.tower_property

Theorem 2.2: tower property for nested sigma-algebras.

Formal statement

∀ {Ω : Type u_1} {m₁ m₂ m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → Real},
  MeasurableSpace.instLE.le m₁ m₂ →
    ∀ (hm₂₀ : MeasurableSpace.instLE.le m₂ m₀) [MeasureTheory.SigmaFinite (μ.trim hm₂₀)],
      (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m₁ μ (MeasureTheory.condExp m₂ μ Y))
        (MeasureTheory.condExp m₁ μ Y)

HansenEconometrics/Chapter2CondExp.lean:26

theorem HansenEconometrics.tower_property_X1_X2

Theorem 2.2 written as E[E[Y | X₁, X₂] | X₁] = E[Y | X₁].

Formal statement

∀ {Ω : Type u_1} {β : Type u_2} {γ : Type u_3} {m₀ : MeasurableSpace Ω} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure Ω} {Y : Ω → Real} {X1 : Ω → β} {X2 : Ω → γ} (hX1 : Measurable X1)
  (hX2 : Measurable X2) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
  (MeasureTheory.ae μ).EventuallyEq
    (MeasureTheory.condExp (MeasurableSpace.comap X1 mβ) μ
      (MeasureTheory.condExp (SemilatticeSup.toMax.max (MeasurableSpace.comap X1 mβ) (MeasurableSpace.comap X2 mγ)) μ
        Y))
    (MeasureTheory.condExp (MeasurableSpace.comap X1 mβ) μ Y)

HansenEconometrics/Chapter2CondExp.lean:37

T2.3 Conditioning Theorem1 endpoint

\int gY \, d\mu = \int g \, \mathbb{E}[Y \mid X] \, d\mu

theorem HansenEconometrics.conditioning_theorem_ae

Theorem 2.3, a.e. version: pull out an m-measurable factor from conditional expectation.

Formal statement

∀ {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {g Y : Ω → Real},
  MeasureTheory.AEStronglyMeasurable g μ →
    MeasureTheory.Integrable (fun ω => instHMul.hMul (g ω) (Y ω)) μ →
      MeasureTheory.Integrable Y μ →
        (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ fun ω => instHMul.hMul (g ω) (Y ω)) fun ω =>
          instHMul.hMul (g ω) (MeasureTheory.condExp m μ Y ω)

HansenEconometrics/Chapter2CondExp.lean:54

T2.4 Properties of the CEF Error1 endpoint

\int g(X) e \, d\mu = 0

theorem HansenEconometrics.condExp_cefError_zero

Theorem 2.4.1: the CEF error has conditional mean zero.

Formal statement

∀ {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → Real}
  (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasureTheory.Integrable Y μ →
    (MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ (HansenEconometrics.cefError μ Y m)) 0

Direct statement dependencies (1)

• HansenEconometrics.cefError

HansenEconometrics/Chapter2CondExp.lean:78

T2.5 Finite Regression-error Variance1 endpoint

\mathbb{E}[Y^2] \lt \infty \Longrightarrow \mathbb{E}[e^2] \lt \infty

theorem HansenEconometrics.memLp_cefError

Hansen Theorem 2.5: if Y has a finite second moment (MemLp Y 2 μ), then the CEF error e = Y - E[Y|m] also has a finite second moment, i.e., the regression-error variance σ² < ∞.

Formal statement

∀ {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → Real},
  MeasureTheory.MemLp Y 2 μ → MeasureTheory.MemLp (HansenEconometrics.cefError μ Y m) 2 μ

Direct statement dependencies (1)

• HansenEconometrics.cefError

HansenEconometrics/Chapter2Variance.lean:26

T2.6 More Information Weakly Reduces Residual Variance1 endpoint

\operatorname{Var}(Y - \mathbb{E}[Y \mid \mathcal{G}_2]) \le \operatorname{Var}(Y - \mathbb{E}[Y \mid \mathcal{G}_1])

theorem HansenEconometrics.variance_cefError_antitone

Hansen Theorem 2.6: monotonic decrease of residual variance under larger conditioning sets. If m₁ ≤ m₂ ≤ m₀, then Var[Y - E[Y|m₂]] ≤ Var[Y - E[Y|m₁]], i.e., conditioning on more information (weakly) reduces the variance of the regression error.

Formal statement

∀ {Ω : Type u_1} {m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {m₁ m₂ : MeasurableSpace Ω} {Y : Ω → Real},
  MeasurableSpace.instLE.le m₁ m₂ →
    MeasurableSpace.instLE.le m₂ m₀ →
      ∀ [MeasureTheory.IsProbabilityMeasure μ],
        MeasureTheory.MemLp Y 2 μ →
          Real.instLE.le (ProbabilityTheory.variance (HansenEconometrics.cefError μ Y m₂) μ)
            (ProbabilityTheory.variance (HansenEconometrics.cefError μ Y m₁) μ)

Direct statement dependencies (1)

• HansenEconometrics.cefError

HansenEconometrics/Chapter2Variance.lean:74

T2.7 Conditional Expectation as Best Predictor1 endpoint

\mathbb{E}[(Y - g(X))^2] \ge \mathbb{E}[(Y - \mathbb{E}[Y \mid X])^2]

theorem HansenEconometrics.integral_sq_sub_condExp_le_integral_sq_sub

Hansen Theorem 2.7 in sigma-algebra form: the conditional mean minimizes mean squared prediction error among m-measurable square-integrable predictors.

Formal statement

∀ {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y g : Ω → Real}
  (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp Y 2 μ →
    MeasureTheory.MemLp g 2 μ →
      MeasureTheory.AEStronglyMeasurable g μ →
        Real.instLE.le
          (MeasureTheory.integral μ fun ω => instHPow.hPow (instHSub.hSub (Y ω) (MeasureTheory.condExp m μ Y ω)) 2)
          (MeasureTheory.integral μ fun ω => instHPow.hPow (instHSub.hSub (Y ω) (g ω)) 2)

HansenEconometrics/Chapter2CondExp.lean:175

T2.8 Law of Total Variance1 endpoint

\operatorname{Var}(Y) = \mathbb{E}[\operatorname{Var}(Y \mid X)] + \operatorname{Var}(\mathbb{E}[Y \mid X])

theorem HansenEconometrics.law_total_variance

Hansen Theorem 2.8 / law of total variance in Mathlib form.

Formal statement

∀ {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → Real},
  MeasurableSpace.instLE.le m m₀ →
    ∀ [MeasureTheory.IsProbabilityMeasure μ],
      MeasureTheory.MemLp Y 2 μ →
        Eq
          (instHAdd.hAdd (MeasureTheory.integral μ fun x => ProbabilityTheory.condVar m Y μ x)
            (ProbabilityTheory.variance (MeasureTheory.condExp m μ Y) μ))
          (ProbabilityTheory.variance Y μ)

HansenEconometrics/Chapter2Variance.lean:33

T2.9 Linear Projection Model6 of 7 linked endpoints

If EXX = E[XX'], EXY = E[XY], and EY2 = E[Y^2], then S(\beta) \le S(b)

theorem HansenEconometrics.linearProjectionBeta_minimizes_MSE

Hansen Definition 2.5 / Theorem 2.9: the projection coefficient minimizes the population linear-prediction mean squared error.

Formal statement

∀ {k : Type u_1} [inst : Fintype k] [inst_1 : DecidableEq k] (QXX : Matrix k k Real) (QXY : k → Real) (QYY : Real)
  [inst_2 : Invertible QXX],
  Eq QXX.transpose QXX →
    (∀ (v : k → Real), Real.instLE.le 0 (dotProduct v (QXX.mulVec v))) →
      ∀ (b : k → Real),
        Real.instLE.le
          (HansenEconometrics.linearProjectionMSE QXX QXY QYY (HansenEconometrics.linearProjectionBeta QXX QXY))
          (HansenEconometrics.linearProjectionMSE QXX QXY QYY b)

Direct statement dependencies (2)

• HansenEconometrics.linearProjectionBeta
• HansenEconometrics.linearProjectionMSE

HansenEconometrics/Chapter2LinearProjection.lean:95

theorem HansenEconometrics.linearProjectionBeta_normal_equations

Hansen Theorem 2.9: the projection coefficient satisfies the population normal equations.

Formal statement

∀ {k : Type u_1} [inst : Fintype k] [inst_1 : DecidableEq k] (QXX : Matrix k k Real) (QXY : k → Real)
  [inst_2 : Invertible QXX], Eq (QXX.mulVec (HansenEconometrics.linearProjectionBeta QXX QXY)) QXY

Direct statement dependencies (1)

• HansenEconometrics.linearProjectionBeta

HansenEconometrics/Chapter2LinearProjection.lean:24

theorem HansenEconometrics.linearProjectionBeta_orthogonal_moment

Hansen Theorem 2.9: population projection residuals are orthogonal to the regressors.

Formal statement

∀ {k : Type u_1} [inst : Fintype k] [inst_1 : DecidableEq k] (QXX : Matrix k k Real) (QXY : k → Real)
  [inst_2 : Invertible QXX], Eq (instHSub.hSub QXY (QXX.mulVec (HansenEconometrics.linearProjectionBeta QXX QXY))) 0

Direct statement dependencies (1)

• HansenEconometrics.linearProjectionBeta

HansenEconometrics/Chapter2LinearProjection.lean:33

theorem HansenEconometrics.linearProjectionBeta_minimizes_MSE_of_moments

Hansen Theorem 2.9 in textbook moment notation: if EXX = E[XXᵀ], EXY = E[XY], and EY2 = E[Y²], then β = (EXX)⁻¹ EXY minimizes the population linear-prediction criterion.

Formal statement

∀ {k : Type u_1} [inst : Fintype k] [inst_1 : DecidableEq k] (EXX : Matrix k k Real) (EXY : k → Real) (EY2 : Real)
  [inst_2 : Invertible EXX],
  Eq EXX.transpose EXX →
    (∀ (v : k → Real), Real.instLE.le 0 (dotProduct v (EXX.mulVec v))) →
      ∀ (b : k → Real),
        Real.instLE.le
          (HansenEconometrics.linearProjectionMSE EXX EXY EY2 (HansenEconometrics.linearProjectionBeta EXX EXY))
          (HansenEconometrics.linearProjectionMSE EXX EXY EY2 b)

Direct statement dependencies (2)

• HansenEconometrics.linearProjectionBeta
• HansenEconometrics.linearProjectionMSE

HansenEconometrics/Chapter2LinearProjection.lean:107

theorem HansenEconometrics.linearProjectionMSE_at_beta

At the projection coefficient, the quadratic criterion simplifies to E[Y²] - β’QXY.

Formal statement

∀ {k : Type u_1} [inst : Fintype k] [inst_1 : DecidableEq k] (QXX : Matrix k k Real) (QXY : k → Real) (QYY : Real)
  [inst_2 : Invertible QXX],
  Eq (HansenEconometrics.linearProjectionMSE QXX QXY QYY (HansenEconometrics.linearProjectionBeta QXX QXY))
    (instHSub.hSub QYY (dotProduct (HansenEconometrics.linearProjectionBeta QXX QXY) QXY))

Direct statement dependencies (2)

• HansenEconometrics.linearProjectionBeta
• HansenEconometrics.linearProjectionMSE

HansenEconometrics/Chapter2LinearProjection.lean:51

theorem HansenEconometrics.linearProjectionBeta_eq_of_MSE_eq

Under strict positive definiteness of the quadratic form, the projection coefficient is the unique minimizer of the population linear-prediction criterion.

Formal statement

∀ {k : Type u_1} [inst : Fintype k] [inst_1 : DecidableEq k] (QXX : Matrix k k Real) (QXY : k → Real) (QYY : Real)
  (b : k → Real) [inst_2 : Invertible QXX],
  Eq QXX.transpose QXX →
    (∀ (v : k → Real), Ne v 0 → Real.instLT.lt 0 (dotProduct v (QXX.mulVec v))) →
      Eq (HansenEconometrics.linearProjectionMSE QXX QXY QYY b)
          (HansenEconometrics.linearProjectionMSE QXX QXY QYY (HansenEconometrics.linearProjectionBeta QXX QXY)) →
        Eq b (HansenEconometrics.linearProjectionBeta QXX QXY)

Direct statement dependencies (2)

• HansenEconometrics.linearProjectionBeta
• HansenEconometrics.linearProjectionMSE

HansenEconometrics/Chapter2LinearProjection.lean:118

T2.10 Regression Coefficients2 endpoints

\beta = \operatorname{var}[X]^{-1} \operatorname{cov}(X, Y)

theorem HansenEconometrics.linearProjectionIntercept_eq_mean_sub_dotProduct

Hansen Theorem 2.10 intercept formula in the linear projection model.

Formal statement

∀ {k : Type u_1} [inst : Fintype k] {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → k → Real) (Y e : Ω → Real) (α : Real) (β : k → Real),
  (∀ (i : k), MeasureTheory.MemLp (fun ω => X ω i) 2 μ) →
    MeasureTheory.MemLp e 2 μ →
      (Eq Y fun ω => instHAdd.hAdd (instHAdd.hAdd α (dotProduct (X ω) β)) (e ω)) →
        Eq (MeasureTheory.integral μ fun ω => e ω) 0 →
          Eq α (instHSub.hSub (MeasureTheory.integral μ fun ω => Y ω) (dotProduct (HansenEconometrics.meanVec μ X) β))

Direct statement dependencies (1)

• HansenEconometrics.meanVec

HansenEconometrics/Chapter2LinearProjection.lean:158

theorem HansenEconometrics.linearProjectionBeta_eq_covMat_inv_covVec

Hansen Theorem 2.10 slope formula in the linear projection model.

Formal statement

∀ {k : Type u_1} [inst : Fintype k] [inst_1 : DecidableEq k] {Ω : Type u_2} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → k → Real) (Y e : Ω → Real) (α : Real)
  (β : k → Real) [inst_3 : Invertible (HansenEconometrics.covMat μ X)],
  (∀ (i : k), MeasureTheory.MemLp (fun ω => X ω i) 2 μ) →
    MeasureTheory.MemLp e 2 μ →
      (Eq Y fun ω => instHAdd.hAdd (instHAdd.hAdd α (dotProduct (X ω) β)) (e ω)) →
        Eq (HansenEconometrics.covVec μ X e) 0 →
          Eq β
            (HansenEconometrics.linearProjectionBeta (HansenEconometrics.covMat μ X) (HansenEconometrics.covVec μ X Y))

Direct statement dependencies (3)

• HansenEconometrics.covMat
• HansenEconometrics.covVec
• HansenEconometrics.linearProjectionBeta

HansenEconometrics/Chapter2LinearProjection.lean:187

T2.12 Conditional Average Causal Effects6 of 27 linked endpoints

Under CIA, CATE conditioned on treatment and covariates equals CATE conditioned on covariates

theorem HansenEconometrics.integral_condVar_eq_integral_cefError_sq

Hansen Chapter 2.12: the expected conditional variance equals the expected squared CEF error. This is the regression-error variance identity following Definitions 2.1-2.2.

Formal statement

∀ {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → Real}
  (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasureTheory.Integrable (instHPow.hPow (instHSub.hSub Y (MeasureTheory.condExp m μ Y)) 2) μ →
    Eq (MeasureTheory.integral μ fun ω => ProbabilityTheory.condVar m Y μ ω)
      (MeasureTheory.integral μ fun ω => instHPow.hPow (HansenEconometrics.cefError μ Y m ω) 2)

Direct statement dependencies (1)

• HansenEconometrics.cefError

HansenEconometrics/Chapter2Variance.lean:14

theorem HansenEconometrics.condExp_apply

Coordinate projection commutes with conditional expectation for finite-dimensional real-valued random vectors.

Formal statement

∀ {Ω : Type u_3} {ι : Type u_4} {E : Type u_6} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace Real E] [inst_3 : CompleteSpace E]
  {f : Ω → ι → E},
  MeasureTheory.Integrable f μ →
    ∀ (i : ι),
      (MeasureTheory.ae μ).EventuallyEq (fun ω => MeasureTheory.condExp m μ f ω i)
        (MeasureTheory.condExp m μ fun ω => f ω i)

HansenEconometrics/ProbabilityUtils.lean:326

theorem HansenEconometrics.integral_apply

Coordinate projection commutes with integration for finite-dimensional real-valued random vectors.

Formal statement

∀ {Ω : Type u_3} {ι : Type u_4} {E : Type u_6} {m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : Fintype ι]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace Real E] [CompleteSpace E] {f : Ω → ι → E},
  MeasureTheory.Integrable f μ →
    ∀ (i : ι), Eq (MeasureTheory.integral μ (fun ω => f ω) i) (MeasureTheory.integral μ fun ω => f ω i)

HansenEconometrics/ProbabilityUtils.lean:349

theorem HansenEconometrics.condExpL2_minimal

Conditional expectation in L² is the orthogonal projection onto the space of m-measurable square-integrable functions, hence it minimizes L² distance.

Formal statement

∀ {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y g : Ω → Real}
  (hm : MeasurableSpace.instLE.le m m₀) [MeasureTheory.IsFiniteMeasure μ] (hY : MeasureTheory.MemLp Y 2 μ)
  (hg : MeasureTheory.MemLp g 2 μ),
  MeasureTheory.AEStronglyMeasurable g μ →
    Real.instLE.le
      (MeasureTheory.Lp.instNorm.norm
        (instHSub.hSub (MeasureTheory.MemLp.toLp Y hY)
          (ContinuousLinearMap.funLike.coe (MeasureTheory.condExpL2 Real Real hm) (MeasureTheory.MemLp.toLp Y hY)).val))
      (MeasureTheory.Lp.instNorm.norm (instHSub.hSub (MeasureTheory.MemLp.toLp Y hY) (MeasureTheory.MemLp.toLp g hg)))

HansenEconometrics/Chapter2CondExp.lean:137

theorem HansenEconometrics.covVec_affineModel

Covariances in an affine linear model decompose into the fitted part and the residual part.

Formal statement

∀ {Ω : Type u_3} {k : Type u_4} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : Fintype k]
  [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → k → Real) (e : Ω → Real) (α : Real) (β : k → Real),
  (∀ (i : k), MeasureTheory.MemLp (fun ω => X ω i) 2 μ) →
    MeasureTheory.MemLp e 2 μ →
      Eq (HansenEconometrics.covVec μ X fun ω => instHAdd.hAdd (instHAdd.hAdd α (dotProduct (X ω) β)) (e ω))
        (instHAdd.hAdd ((HansenEconometrics.covMat μ X).mulVec β) (HansenEconometrics.covVec μ X e))

Direct statement dependencies (2)

• HansenEconometrics.covMat
• HansenEconometrics.covVec

HansenEconometrics/ProbabilityUtils.lean:717

theorem HansenEconometrics.condExp_apply_apply

Applying two coordinate projections in succession commutes with conditional expectation for finite-dimensional real-valued arrays.

Formal statement

∀ {Ω : Type u_3} {ι : Type u_4} {κ : Type u_5} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : Fintype ι] [inst_1 : Fintype κ] {f : Ω → ι → κ → Real},
  MeasureTheory.Integrable f μ →
    ∀ (i : ι) (j : κ),
      (MeasureTheory.ae μ).EventuallyEq (fun ω => MeasureTheory.condExp m μ f ω i j)
        (MeasureTheory.condExp m μ fun ω => f ω i j)

HansenEconometrics/ProbabilityUtils.lean:336