Documentation

Lean 4 Proof

theorem totalRevenue_between {R_ad R_mp φ : ℝ}
    (_hφ0 : 0 ≤ φ) (_hφ1 : φ ≤ 1) (_hR : R_ad ≤ R_mp) :
    R_ad ≤ totalRevenue R_ad R_mp φ := by
  unfold totalRevenue; nlinarith

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:114

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file