Revision #2228 → #2901 · back to history
modifiedExistence for finite gamesaa02158bb8c9
| Field | From #2228 | To #2901 |
|---|
| note | 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. | 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). |
addedBest response dynamics8ab5ac7c8690
addedk-resilient Nash equilibrium598a9b117840
modifiedNash existence theorem18b7648df46b
| Field | From #2228 | To #2901 |
|---|
| note | The Nash existence theorem is not formalized; Mathlib also lacks the Brouwer and 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 (Brouwer/Kakutani hits in Mathlib are Brouwer/Heyting algebras and the Riesz–Markov–Kakutani representation theorem). |
modifiedExistence proof via Brouwer fixed-point theorem0dc268b0663b
| Field | From #2228 | To #2901 |
|---|
| note | 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. | 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; the Mathlib hits for `Brouwer` are Brouwer/Heyting algebras), so this Nash existence proof is not formalized. |