theorem
proved
gameTypeCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Economics.GameTheoryFromRS on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25 | zeroSum | cooperative | nonCooperative | symmetric | repeated
26 deriving DecidableEq, Repr, BEq, Fintype
27
28theorem gameTypeCount : Fintype.card GameType = 5 := by decide
29
30/-- Nash equilibrium: J = 0. -/
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