Documentation

Lean 4 Proof

theorem convex_distiller_expensive {p_0 β Q target : ℝ}
    (_hp : 0 < p_0) (_hβ : 0 < β) (_hQ : 0 < Q)
    (hlarge : 2 * target / (p_0 * β) < Q) :
    target < convexAvgCost p_0 β Q := by
  unfold convexAvgCost
  have hpβ : 0 < p_0 * β := mul_pos _hp _hβ
  rw [div_lt_iff₀ hpβ] at hlarge; nlinarith

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:261

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file