Documentation

Lean 4 Proof

theorem above_healthy_repels {R J c_min : ℝ}
    (hc : 0 < c_min) (hJ : 0 < J)
    (habove : healthyEquilibrium R c_min < J) :
    producerProfit R J c_min < 0 := by
  unfold producerProfit healthyEquilibrium at *
  rw [div_lt_iff₀ hc] at habove
  rw [sub_neg, div_lt_iff₀ hJ]; linarith

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:166

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file