Documentation

Lean 4 Proof

theorem diversity_exponent_negative {rho : ℝ} (hrho_neg : rho < 0) :
    (1 - rho) / rho < 0 :=
  div_neg_of_pos_of_neg (by linarith) hrho_neg

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:87

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file