Documentation

Lean 4 Proof

theorem frontLoaded_one {R_0 γ : ℝ} (hγ : 0 < γ) :
    frontLoadedRevenue R_0 γ 1 = 0 := by
  unfold frontLoadedRevenue
  simp [zero_rpow (by linarith : (1 : ℝ) + γ ≠ 0)]

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:211

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file