Documentation

Lean 4 Proof

def fisherCESMetricDiag (ρ : ℝ) (s_i : ℝ) : ℝ :=
  (1 / bridgeRatio ρ) * (1 / s_i - 1)

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:315

Module Section

### The Cramer-Rao Bound for Market Mechanisms

In the same file