Documentation

Lean 4 Proof

def sybilTotalCost (p_0 β Q : ℝ) (K : ℕ) : ℝ :=
  p_0 * (Q + β * Q ^ 2 / (2 * ↑K))

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:272

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file