Documentation

Lean 4 Proof

theorem ols_downward_bias {ρ covZε varZ : ℝ}
    (hcov : covZε < 0) (hvar : 0 < varZ) :
    olsPlim ρ covZε varZ < ρ := by
  simp only [olsPlim, simultaneityBias]
  linarith [div_neg_of_neg_of_pos hcov hvar]

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:232

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file