Documentation

Lean 4 Proof

theorem convex_consumer_approx {p_0 β Q : ℝ}
    (hp : 0 < p_0) (hβ : 0 < β) (_hQ : 0 < Q) (hsmall : Q ≤ 1) :
    convexAvgCost p_0 β Q ≤ p_0 * (1 + β / 2) := by
  unfold convexAvgCost
  apply mul_le_mul_of_nonneg_left _ (le_of_lt hp)
  linarith [mul_le_mul_of_nonneg_left hsmall (le_of_lt hβ)]

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:250

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file