Documentation

Lean 4 Proof

theorem diversity_exponent_superlinear {rho : ℝ} (hrho_neg : rho < 0) :
    (1 - rho) / rho < -1 := by
  rw [div_lt_iff_of_neg hrho_neg]; linarith

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:82

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file