Documentation

Lean 4 Proof

theorem iv_identifies_complier_rho
    {ρ_complier covZX_complier : ℝ}
    (hrel : ivRelevance covZX_complier) :
    ivEstimator (ρ_complier * covZX_complier) covZX_complier = ρ_complier :=
  iv_consistent hrel

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:405

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file