  31theorem nash_equilibrium : Jcost 1 = 0 := Jcost_unit0
  32
  33/-- Off-equilibrium deviation: J > 0. -/
  34theorem off_equilibrium {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  35    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  36
  37structure GameTheoryCert where
  38  five_types : Fintype.card GameType = 5
  39  nash_eq : Jcost 1 = 0
  40  off_eq : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  41
  42def gameTheoryCert : GameTheoryCert where
  43  five_types := gameTypeCount
  44  nash_eq := nash_equilibrium
  45  off_eq := off_equilibrium
  46
  47end IndisputableMonolith.Economics.GameTheoryFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.