Documentation

Lean 4 Proof

theorem healthy_eq_zero_profit {R c_min : ℝ}
    (_hc : 0 < c_min) (hR : c_min < R) :
    producerProfit R (healthyEquilibrium R c_min) c_min = 0 := by
  unfold producerProfit healthyEquilibrium
  rw [div_div_cancel₀ (ne_of_gt (by linarith : 0 < R))]; ring

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:142

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file