Documentation

Lean 4 Proof

theorem marketplace_rescue {R_mp c_min φ : ℝ}
    (hR : 0 < R_mp) (_hcR : c_min < R_mp)
    (hφ : c_min / R_mp < φ) :
    c_min < totalRevenue 0 R_mp φ := by
  unfold totalRevenue; simp only [mul_zero, zero_add]
  rwa [div_lt_iff₀ hR] at hφ

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:126

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file