Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.game-equilibria

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/game_equilibria.clj5 definitions, 4 theorems

Kochenderfer 'Algorithms for Decision Making' Ch.24-27 multi-agent equilibrium cores as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog. FLAGSHIP (a genuine OR theorem, not a worked instance): D25.5 Markov-game / zero-sum Nash : the 2x2 MINIMAX INEQUALITY max_row min_col V <= min_col max_row V (the saddle-point / weak-duality direction of von Neumann's minimax theorem), assembled purely from the min/max lattice (min-lower, max-upper, at-most-min, at-most-max, transitivity). Plus the shared no-profitable-deviation property of the other equilibrium solvers: D26.3 POMG Nash (conditional plans) : equilibrium value >= any deviation D27.3 Dec-POMDP iterated best resp. : joint best-response value >= any deviation D24.9 level-k / hierarchical softmax : level-k value >= the response it improves on Native and axiom-free; chains nnrat-minmax on d63.

Depends onmath.rational.nnrat.minmax

game/maximin :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

game/minimax :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

game/pomg-value :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

game/dec-ibr-value :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

game/levelk-value :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

game/minimax-inequality :
  (v00 v01 v10 v11 : ℚ≥0)
  → game/maximin v00 v01 v10 v11 ≤ game/minimax v00 v01 v10 v11

game/pomg-no-deviation :
  (r0 r1 : ℚ≥0)
  → r0 ≤ game/pomg-value r0 r1

game/dec-ibr-no-deviation :
  (r0 r1 : ℚ≥0)
  → r0 ≤ game/pomg-value r0 r1

game/levelk-no-deviation :
  (r0 r1 : ℚ≥0)
  → r0 ≤ game/pomg-value r0 r1