Documentation

Lean 4 Proof

def innerDiversityMultiplier (J : ℕ) (ρ : ℝ) : ℝ :=
  (↑J : ℝ) ^ ((1 - ρ) / ρ)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:308

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file