Documentation

Lean 4 Proof

theorem gini_zero_at_equality (hJ : 0 < J) :
    giniIndex J (fun _ : Fin J => (1 / ↑J : ℝ)) = 0 := by
  simp only [giniIndex, sub_self, abs_zero, Finset.sum_const_zero, mul_zero]

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:300

Module Section

## CES Inequality Measures

In the same file