Sections / Section 8: Applied Economics -- Elasticity, Demand, Trade / iv_undefined_without_relevance

Iv Undefined Without Relevance

theoremprovedFoundations

Documentation

Lean 4 Proof

theorem iv_undefined_without_relevance (covZY : ℝ) :
    ivEstimator covZY 0 = 0 := by
  simp [ivEstimator, div_zero]

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:268

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file

fisherInfoRho cramerRaoBound logRatio olsSlope simultaneityBias olsPlim ivRelevance ivExclusion ivEstimator withinTransform panelShareIdentity fisherInfoRho_eq_escortVariance fisherInfoRho_zero_at_symmetry cramerRao_diverges_at_symmetry logRatio_antisymmetric logRatio_zero_at_symmetry shares_are_expectations_not_sufficient ols_consistent_when_exogenous ols_upward_bias ols_downward_bias