Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:218

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file