Documentation

Lean 4 Proof

theorem iv_consistent {ρ covZX : ℝ} (hrel : ivRelevance covZX) :
    ivEstimator (ρ * covZX) covZX = ρ := by
  simp only [ivEstimator, ivRelevance] at *
  exact mul_div_cancel_of_imp (fun h => absurd h hrel)

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CESEstimation.lean:261

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file