Revision #1760 → #2228 · back to history
modifiedNash equilibriumc24b2b534694
| Field | From #1760 | To #2228 |
|---|
| note | Mathlib has no game-theory library and no definition of Nash equilibrium. | Mathlib has no game-theory library and no definition of Nash equilibrium (grep for `Nash` returns only unrelated hits like Cartan, NashAdd, etc.). |
modifiedExistence for finite gamesaa02158bb8c9
| Field | From #1760 | To #2228 |
|---|
| note | The Nash existence theorem for finite games is not in Mathlib (no Brouwer/Kakutani fixed-point theorem either). | The Nash existence theorem for finite games is not in Mathlib, and neither Brouwer's nor Kakutani's fixed-point theorem (only Banach contraction and 1D IVT-fixed-point) is available. |
addedMixed strategydf7955b3ee64
modifiedMixed-strategy existence for zero-sum games (von Neumann)b4fd9948cc20
| Field | From #1760 | To #2228 |
|---|
| note | Mathlib proves Sion's generalization of the von Neumann minimax theorem (saddle-point existence on compact convex sets), but the finite-action mixed-strategy zero-sum game case is not spelled out. | Mathlib proves Sion's generalization of the von Neumann minimax theorem (saddle-point existence on compact convex sets) in `Mathlib.Topology.Sion`, but the finite-action mixed-strategy zero-sum game case is not spelled out as a corollary. |
modifiedStrong Nash is weakly Pareto efficienta2a9d3947b72
| Field | From #1760 | To #2228 |
|---|
| note | Neither strong Nash equilibrium nor Pareto efficiency is formalized (Mathlib's only Pareto is the probability distribution). | Neither strong Nash equilibrium nor Pareto efficiency of allocations is formalized in Mathlib. |
modifiedNash existence theorem18b7648df46b
| Field | From #1760 | To #2228 |
|---|
| note | The Nash existence theorem is not formalized; Mathlib lacks the Brouwer/Kakutani fixed-point theorems it relies on. | The Nash existence theorem is not formalized; Mathlib also lacks the Brouwer and Kakutani fixed-point theorems it relies on. |
modifiedNash equilibrium need not be Pareto optimal58483f4096f2
| Field | From #1760 | To #2228 |
|---|
| note | Neither Nash equilibrium nor Pareto optimality is formalized in Mathlib. | Neither Nash equilibrium nor Pareto optimality of allocations is formalized in Mathlib. |
modifiedExistence proof via Kakutani fixed-point theoremd5fccfe30cbe
| Field | From #1760 | To #2228 |
|---|
| note | The Kakutani fixed-point theorem is not in Mathlib (only the Riesz–Markov–Kakutani representation theorem). | The Kakutani set-valued fixed-point theorem is not in Mathlib (the `Kakutani` hits are the Riesz–Markov–Kakutani representation theorem, a different result), so this proof is not formalized. |
modifiedExistence proof via Brouwer fixed-point theorem0dc268b0663b
| Field | From #1760 | To #2228 |
|---|
| note | The Brouwer fixed-point theorem itself is not in Mathlib, so this proof is not formalized. | Even the Brouwer fixed-point theorem itself is not in Mathlib (only Banach contraction and the 1D IVT-fixed-point variants like `exists_mem_Icc_isFixedPt` appear), so this Nash existence proof is not formalized. |
| provenance | ai | ai-moderated |