Documentation

Lean 4 Proof

theorem sybil_still_superlinear {p_0 β Q : ℝ} {K : ℕ}
    (hp : 0 < p_0) (hβ : 0 < β) (hQ : 0 < Q) (_hK : 1 ≤ K) :
    p_0 * Q < sybilTotalCost p_0 β Q K := by
  unfold sybilTotalCost
  nlinarith [sq_nonneg Q, mul_pos hβ (sq_pos_of_pos hQ),
             div_pos (mul_pos hβ (sq_pos_of_pos hQ))
               (by positivity : (0:ℝ) < 2 * (↑K : ℝ))]

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:278

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file