Documentation

Lean 4 Proof

theorem gini_nonneg (hJ : 0 < J) (s : Fin J → ℝ) :
    0 ≤ giniIndex J s := by
  simp only [giniIndex]
  apply mul_nonneg
  · apply div_nonneg one_pos.le
    exact mul_nonneg (by norm_num) (by exact_mod_cast le_of_lt hJ)
  · apply Finset.sum_nonneg; intro i _
    apply Finset.sum_nonneg; intro j _
    exact abs_nonneg _

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:305

Module Section

## CES Inequality Measures

In the same file