Documentation

Lean 4 Proof

theorem iv_biased_without_exclusion {ρ covZX covZε : ℝ}
    (hrel : ivRelevance covZX) (hcov : covZε ≠ 0) :
    ivEstimator (ρ * covZX + covZε) covZX ≠ ρ := by
  simp only [ivEstimator, ivRelevance] at *
  rw [add_div, mul_div_cancel_of_imp (fun h => absurd h hrel)]
  intro h
  have : covZε / covZX = 0 := by linarith
  exact hcov ((div_eq_zero_iff.mp this).resolve_right hrel)

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:275

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file