{"id":"palomar/PALOMAR-2026-09-08-000001","url":"https://github.com/Arthur742Ramos/correlated-equilibrium-lean/tree/67f1dc1f2fcb6e75ea62de92f9c67bd92191fd6e","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-08-000001-v1.json","repo":"https://github.com/Arthur742Ramos/correlated-equilibrium-lean","tags":["cs.GT","msc:91A10","msc:91A26","game-theory","correlated-equilibrium","regret-bounds","formalization"],"score":0,"title":"Finite correlated equilibria and regret certificates","trust":"high","domain":"cs.GT","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy Jose Guerra Barretto de Queiroz"],"reviews":0,"subject":"cs.GT","summary":"For finite games with player-specific action types, a valid independent product distribution is a correlated equilibrium exactly when its mixed profile is Nash. The correlated-equilibrium set is nonempty, compact, and convex when every player's action type is nonempty. For every positive finite horizon, cumulative external-regret and swap-regret bounds give corresponding approximate coarse-correlated and correlated equilibria of the empirical distribution. The development also proves equivalence with conditional obedience inequalities, arbitrary mixed-deviation sufficiency, and…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-09-08","reactions":{},"formalized":true,"formalizes":[{"title":"Subjectivity and correlation in randomized strategies","identifier":"https://doi.org/10.1016/0304-4068(74)90037-8","relationship":"formalizes"},{"title":"Algorithmic Game Theory lecture notes, lectures 17 and 18","identifier":"https://timroughgarden.org/f13/l/f13.pdf","relationship":"formalizes"},{"title":"Dependent finite mixed Nash equilibria in Lean","identifier":"https://github.com/Arthur742Ramos/dependent-nash-equilibrium-lean/tree/2f65710af26a24a26660dd1e92d09adf1697a527","relationship":"adapts"}]}