Revision #2901 → #3364 · back to history
modifiedNash equilibriumc24b2b534694
| Field | From #2901 | To #3364 |
|---|
| note | Mathlib has no game-theory library and no definition of Nash equilibrium (grep for `Nash` returns only unrelated hits like Cartan, NashAdd, etc.). | Mathlib has no game-theory library and no definition of Nash equilibrium (all `Nash` hits are the author name Oliver Nash). |
modifiedExistence for finite gamesaa02158bb8c9
| Field | From #2901 | To #3364 |
|---|
| note | The Nash existence theorem for finite games is not in Mathlib, and neither Brouwer's nor Kakutani's set-valued fixed-point theorem is available (only Banach contraction and 1D IVT-fixed-point). | The Nash existence theorem for finite games is not in Mathlib, and neither Brouwer's nor Kakutani's set-valued fixed-point theorem is available. |
addedKakutani fixed-point theorem (used by Nash 1950)62da699735c1
addedBrouwer fixed-point theorem (used by Nash 1951)be12e372327b
addedSubgame perfect equilibrium (Selten)d21a0a12629d
modifiedStrong Nash is weakly Pareto efficienta2a9d3947b72
| Field | From #2901 | To #3364 |
|---|
| note | Neither strong Nash equilibrium nor Pareto efficiency of allocations is formalized in Mathlib. | Neither strong Nash equilibrium nor Pareto efficiency of allocations is formalized in Mathlib (only the Pareto probability distribution appears). |
addedBerge's maximum theorem97894c795c66