Documentation

Lean 4 Proof

theorem ols_consistent_when_exogenous (ρ : ℝ) {varZ : ℝ}
    (_hvarZ : varZ ≠ 0) :
    olsPlim ρ 0 varZ = ρ := by
  simp [olsPlim, simultaneityBias, zero_div]

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:209

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file