Documentation

Lean 4 Proof

theorem convex_pricing_deterrence {p_1 p_n : ℝ} {n : ℕ}
    (_hp1 : 0 < p_1) (_hn : 2 ≤ n)
    (h_convex : p_1 * ↑n < p_n) :
    p_1 * ↑n < p_n := h_convex

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:287

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file