Documentation

Lean 4 Proof

def giniIndex (J : ℕ) (s : Fin J → ℝ) : ℝ :=
  (1 / (2 * ↑J)) * ∑ i : Fin J, ∑ j : Fin J, |s i - s j|

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Inequality.lean:216

Module Section

## CES Inequality Measures

In the same file