Documentation

Lean 4 Proof

theorem rhoDiversity_at_two_eq_one_minus_hhi
    (s : Fin J → ℝ) :
    rhoDiversity J 2 s = 1 - herfindahlIndex J s := by
  unfold rhoDiversity tsallisEntropy herfindahlIndex
  simp only [show (2 : ℝ) ≠ 1 from by norm_num, ite_false]
  norm_num

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:556

Module Section

### The rho-Diversity Index

In the same file