Documentation

Lean 4 Proof

def shareVariance (J : ℕ) (s : Fin J → ℝ) : ℝ :=
  ∑ j : Fin J, (s j - 1 / ↑J) ^ 2

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Inequality.lean:220

Module Section

## CES Inequality Measures

In the same file