Documentation

Lean 4 Proof

theorem cooperation_easier_with_higher_punishment
    {g p₁ p₂ : ℝ} (hg : 0 < g) (_hp1 : 0 < p₁)
    (_hp2 : 0 < p₂) (hlt : p₁ < p₂) :
    g / (g + p₂) < g / (g + p₁) := by
  apply div_lt_div_of_pos_left hg (by linarith) (by linarith)

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:323

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file