Documentation

Lean 4 Proof

def theilIndex (J : ℕ) (s : Fin J → ℝ) : ℝ :=
  ∑ j : Fin J, s j * Real.log (↑J * s j)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Inequality.lean:211

Module Section

## CES Inequality Measures

In the same file