The Set of Correlated Equilibrium Payoffs for a Fixed Information Structure Need Not Be Closed
Michael Greinecker, Patrick Lahr, Christoph Schwerdtfeger
econ.TH
Aug 2, 2026 · v1
cs.GT math.PR
TL;DR
Main results and supporting lemmas on nonclosed correlated-equilibrium payoff sets are formalized in the Lean proof assistant, with an appendix recording coverage.
Abstract
Aumann (1974) showed that an atomless public randomization device makes the feasible- and equilibrium-payoff sets of a game with a fixed information structure convex, and asked whether they are closed. We show that, in every case the question leaves open, they need not be. One information structure drives all the examples: two sequences of fair signs whose coordinate correlations increase to a ceiling $ρ<1$ that no pair of separately measurable square-integrable rules attains. For every $0<ρ<1$ it yields a three-player game with a public randomization device whose equilibrium-payoff set is exactly the open interval $\{(0,0,t):-ρ<t<ρ\}$; a two-player game with a public randomization device whose equilibrium-payoff set is convex, full dimensional, and not closed; and, without any public device, nonclosed feasible- and equilibrium-payoff sets, the latter along equilibria with unique best replies modulo null events whose payoffs approach a vector that is not even feasible. With distinct but mutually absolutely continuous subjective priors, even the feasible-payoff set can fail to be closed in the presence of an objective public randomization device, together with every $\varepsilon$-equilibrium payoff set and the set of induced law tuples. Our construction also allows us to resolve a conjecture of Stinchcombe (2011). The main results and the lemmas supporting them are formalized in the Lean proof assistant; an appendix records the exact coverage of each statement, including the clauses for which only a paper proof is given.
Problem
Aumann (1974) asked whether the feasible- and equilibrium-payoff sets of a game with a fixed information structure are closed, with or without a public randomization device. The question remained open in several cases.
Approach
A single information structure is constructed from two sequences of fair signs whose coordinate correlations increase to a ceiling rho<1 that no pair of separately measurable square-integrable rules attains. This source drives three- and two-player game examples showing nonclosedness, and extends to subjective mutually absolutely continuous priors. The main theorems and supporting lemmas are formalized in the Lean proof assistant, with an appendix documenting exact formalization coverage of each statement.
Results
In every open case, the payoff sets need not be closed: with a public device the equilibrium-payoff set can be exactly an open interval, and without one both feasible- and equilibrium-payoff sets can fail to be closed. Distinct subjective priors do not restore closedness, and a conjecture of Stinchcombe (2011) is resolved.
| public device | no public device |
|---|
| feasible payoffs | closed (Aumann 1974) | not closed (Thm C) |
| equilibrium payoffs | not closed (Thms A, B) | not closed (Thm D) |
Closedness of payoff sets with and without a public randomization device (objective priors)