Algorithmic Game Theory

Motivation

A correlated equilibrium (Aumann 1974) is a joint distribution over the players' strategy profiles such that no player gains by deviating from the strategy the distribution recommends to them. It is the equilibrium notion that learning dynamics in repeated games most naturally reach, and a basic question in learning in games is which simple rules, played repeatedly, drive the empirical distribution of play to the set of correlated equilibria.

Foster and Vohra (1997) answer this with a hypothesis on forecasts instead of a particular algorithm. Each player forecasts the other's next move and best-responds to the forecast. They only require the forecasts to be calibrated in the sense of Dawid (1982): among the rounds in which a player forecast a given probability vector, the empirical frequencies of the opponent's moves must approach that vector. Their Theorem 1 says that this already forces the empirical joint distribution of play to approach the set of correlated equilibria. The paper uses this to argue that Bayesian players under a common prior, whose forecasts are calibrated by Dawid's theorem, end up playing a correlated equilibrium. That is an alternative to Aumann's (1987) derivation of correlated equilibrium from common priors and rationality.

Timeline:

• Aumann (1974, 1987) introduces correlated equilibrium and derives it from Bayesian rationality.
• Dawid (1982) proposes calibration as a minimal requirement on probability forecasts.
• Foster and Vohra (1997) prove Theorem 1 (this mission) and show that calibrated forecasts exist once the forecaster may randomize.
• Hart and Mas-Colell (2000) give regret matching, an adaptive procedure with the same limit set.

Setting

A finite two-player game $G$ has strategy sets $S(1) = \{0, \dots, m-1\}$ and $S(2) = \{0, \dots, n-1\}$ and payoff matrices $u_1, u_2 : S(1) \times S(2) \to \mathbb{R}$, which the players maximize. A joint distribution $D$ is a nonnegative $m \times n$ matrix with entries summing to $1$. It is a correlated equilibrium if

$$\sum_{x,y} D(x,y)\, u_1(\Phi(x), y) \le \sum_{x,y} D(x,y)\, u_1(x,y) \quad \text{for all } \Phi : S(1) \to S(1),$$

and symmetrically for player 2. The set of correlated equilibria is $\pi(G)$.

The game is played in rounds $s = 0, 1, 2, \dots$. In round $s$ player 1 issues a forecast $f_1(s)$, a probability vector over $S(2)$, and player 2 issues a forecast $f_2(s)$ over $S(1)$. Each player then plays a best response to its forecast, $x(s) = R_1(f_1(s))$ and $y(s) = R_2(f_2(s))$. Here $R_1$ and $R_2$ are best-reply functions: $R_1(p)$ maximizes $\sum_y p_y u_1(\cdot, y)$ for every probability vector $p$, and $R_1$ is a fixed function of the forecast alone. This is the paper's standing assumption of a stationary, deterministic tie-breaking rule.

For a forecast sequence $f$ and the opponent's plays $z$, $N(p,t)$ counts the rounds among the first $t$ in which $f$ forecast $p$. $\rho(p,j,t)$ is the fraction of those rounds in which the opponent played $j$, and $0$ if there are none. The forecast is calibrated with respect to $z$ if for every $j$

$$\sum_p |\rho(p,j,t) - p_j|\, \frac{N(p,t)}{t} \longrightarrow 0 \qquad (t \to \infty).$$

The empirical joint distribution $D_t(x,y)$ is the fraction of the first $t$ rounds in which player 1 played $x$ and player 2 played $y$.

Formalization targets

Goal: Theorem 1

If $f_1$ is calibrated with respect to $y$ and $f_2$ is calibrated with respect to $x$, then

$$\min_{D \in \pi(G)} \ \max_{x \in S(1),\, y \in S(2)} |D_t(x,y) - D(x,y)| \longrightarrow 0 \qquad (t \to \infty).$$

The goal fixes no rate and no particular forecasting method: it asserts only convergence of $D_t$ to the set $\pi(G)$, for every calibrated forecast.

Milestones: the steps of the proof (pp. 44–45)

1. $D_t$ lies in the simplex for $t \ge 1$.
2. For each $x \in S(1)$, the set $M_b(x)$ of mixtures to which $x$ is a best response is closed and convex.
3. The mixtures $M_p(x)$ at which player 1 actually plays $x$ satisfy $M_p(x) \subseteq M_b(x)$.
4. The identity writing $D_t(x,y)$ as a forecast-weighted term plus a calibration error.
5. Calibration makes the error term vanish.
6. The weighted average of the forecasts at which player 1 plays $x$ lies in $M_b(x)$.
7. For a convergent subsequence $D_{t_i} \to D$, every row of $D$ with positive mass, normalized, lies in $M_b(x)$.
8. Every subsequential limit of $D_t$ is a correlated equilibrium.

Further result: matching pennies (p. 46)

With the constant forecast $(1/2, 1/2)$ and the non-stationary tie-break "heads on even rounds, tails on odd rounds", both forecasts are calibrated and every play is a best reply, yet $D_t$ does not approach $\pi(G)$. The stationarity assumption cannot be dropped.

Significance

The result. Theorem 1 separates what learning needs from how it is achieved. Any forecasting procedure that is calibrated, combined with myopic best responses, yields correlated equilibrium behaviour in the long run. The paper's Theorem 3 constructs a randomized calibrated forecaster, so the theorem gives an uncoupled learning procedure for correlated equilibrium, one that needs no knowledge of the opponent's payoffs. The converse direction, that every correlated equilibrium arises this way for almost every game, is the paper's Theorem 2 (a separate mission of this series).

Formalizing it. The theorem is proved in the paper and has no machine-checked proof on Prove2Me or, to the knowledge of this mission, elsewhere. The platform's existing correlated-equilibrium results (the Algorithmic Game Theory swap-regret development, AGT.swap_regret_correlated_equilibrium) reach correlated equilibrium through swap regret of mixed strategies, a different hypothesis and a different object. This mission adds a formal notion of calibration and the convergence argument, both reusable for the paper's Theorems 2 and 3 and for later work on calibration and learning.

Difficulty

The obvious reading of calibration is that each player's forecast converges to the opponent's empirical distribution; if that held, best responses to it would give convergence. It does not hold. Calibration constrains the opponent's frequencies only conditionally on the forecast issued, and the forecasts need not converge at all. What must be shown is a statement about the conditional distributions of the joint play given each strategy of player 1, while the set of forecasts issued keeps growing. Rows of the limit with zero mass carry no conditional distribution. The "min → 0" form also asks for more than a property of limit points: it is a uniform statement about all large $t$.

Formalization scope

• Strategies are Fin m and Fin n; payoffs are real matrices; forecasts are real vectors required to be probability vectors in every round.
• A correlated equilibrium is the joint-distribution form of p. 44 (the correlated strategy on a finite probability space is represented by its law). It is the $\varepsilon = 0$, two-player, payoff (not cost) instance of the published AGT.IsCorrelatedEquilibrium, restated rather than imported.
• The stationary deterministic tie-break is modelled by arbitrary best-reply functions $R_i$ of the forecast. They do not depend on the round, and the statements quantify over all of them, which includes the lowest-index rule.
• Forecasts are sequences $f_i : \mathbb{N} \to \mathbb{R}^k$. The theorem uses only the realized forecasts, and every sequence is realized by a rule reading the round number from the history.
• Rounds are indexed from $0$: "the first $t$ rounds" are $0, \dots, t-1$. $D_0 = 0$ by Lean's division convention; only $t \ge 1$ and limits are used.
• The calibration sum runs over the forecasts issued in the first $t$ rounds, which is the paper's sum over all $p$ with its zero terms removed. $\rho(p,j,t) = 0$ when $N(p,t) = 0$, as on the page.
• "min … → 0" is stated as: for every $\varepsilon > 0$, eventually some $D \in \pi(G)$ is within $\varepsilon$ of $D_t$ in every coordinate. The two forms are equivalent because $\pi(G)$ is compact and nonempty. The formalization avoids an infimum over $\pi(G)$, which Lean would evaluate to $0$ on an empty set.
• A statement that drops the best-reply property, the probability-vector condition on forecasts, or the stationarity of $R_i$ is not Theorem 1: the matching pennies example shows the last one is essential. Swapping the calibration hypotheses (player 1's forecast calibrated against player 1's own plays) type-checks when $m = n$ and is not the theorem.
• Only the two-player case is claimed. The paper says the results "generalize easily to the $n$-person case" without proof.

Proofs of any milestone, and reusable lemmas about calibration scores and compactness of the simplex of joint distributions, are welcome.

Selected references

• D. P. Foster, R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997) 40–55. https://doi.org/10.1006/game.1997.0595
• R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1 (1974) 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• R. J. Aumann, Correlated equilibrium as an expression of Bayesian rationality, Econometrica 55 (1987) 1–18. https://doi.org/10.2307/1911154
• A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77 (1982) 605–610. https://doi.org/10.1080/01621459.1982.10477856
• S. Hart, A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000) 1127–1150. https://doi.org/10.1111/1468-0262.00153

Motivation

A buyer and a seller negotiate over a single indivisible good. Each knows how much the good is worth to them, but not how much it is worth to the other side. Whether the two will trade, and at what price, then depends on how each party shades its offer to exploit the other's uncertainty. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this situation as a one-shot game in which both parties submit sealed offers simultaneously, and characterised its Bayesian equilibria.

The model became the standard reference point for bilateral trade with two-sided private information. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) showed that no mechanism can guarantee efficient trade in this setting, and that the equilibrium of the Chatterjee–Samuelson game with $k = 1/2$ and uniform values attains the second-best efficiency bound. Later work on the $k$-double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) studies the continuum of equilibria of exactly this game. The object of the present mission, a pair of linked differential equations, is the tool these papers use to construct and classify equilibria.

Setting

A seller has reservation price $v_s \in [\underline v_s, \bar v_s]$ and a buyer has reservation price $v_b \in [\underline v_b, \bar v_b]$. Each knows their own value. The buyer's belief about $v_s$ is a probability measure $\mu_b$ with distribution function $F_b$; the seller's belief about $v_b$ is $\mu_s$ with distribution function $F_s$. The subscript names the player who holds the belief, not the variable. Each belief is regular: $F(\underline v) = 0$, $F(\bar v) = 1$, and $F$ is strictly increasing and differentiable on the value interval, with density $f_b$ (respectively $f_s$).

Under the Bargaining Rule, the seller asks $s$ and the buyer offers $b$ simultaneously. If $b \ge s$ the good is sold at $P = kb + (1-k)s$ for a fixed $k \in [0, 1]$; otherwise nothing happens. Profits are $P - v_s$ for the seller and $v_b - P$ for the buyer on trade, and zero otherwise.

An offer strategy is a function $S$ (for the seller) or $B$ (for the buyer) from values to offers. Against $S$, a buyer with value $v$ offering $b$ earns in expectation

$$\pi_b(b, v) = \int \mathbf 1\{S(v_s) \le b\}\,\bigl(v - kb - (1-k)S(v_s)\bigr)\,d\mu_b(v_s),$$

and symmetrically $\pi_s(s, v) = \int \mathbf 1\{s \le B(v_b)\}\,(kB(v_b) + (1-k)s - v)\,d\mu_s(v_b)$. The pair $(S, B)$ is an equilibrium if $B(v)$ maximises $\pi_b(\cdot, v)$ over all real offers for every buyer value $v$, and $S(v)$ maximises $\pi_s(\cdot, v)$ for every seller value $v$.

A strategy is of class $A$ if its offers are bounded, it is nondecreasing, it is strictly increasing except where it sits at its lowest offer $m$ or its highest offer $M$, and it is differentiable wherever its offer lies strictly between $m$ and $M$. A class $A$ equilibrium is an equilibrium in which both strategies are of class $A$.

Formalization targets

Goal: Theorem 2, the linked differential equations

In a class $A$ equilibrium, wherever the seller's strategy is strictly increasing around $y$ and the buyer value $x$ offers $B(x) = S(y)$,

$$k F_b(y) S'(y) + f_b(y) S(y) = x\, f_b(y), \tag{3a}$$

and wherever the buyer's strategy is strictly increasing around $x$ and the seller value $y$ asks $S(y) = B(x)$,

$$(1-k)\bigl(1 - F_s(x)\bigr) B'(x) - f_s(x) B(x) = -\,y\, f_s(x). \tag{3b}$$

The paper writes $x = B^{-1}(S(y))$ in (3a) and $y = S^{-1}(B(x))$ in (3b).

Milestones: the displays of the proof

1. $G_b(S(y)) = F_b(y)$: the buyer's probability that the seller asks at most $S(y)$ equals $F_b(y)$.
2. The buyer's first-order condition: $\partial \pi_b / \partial b = (v - b) g_b(b) - k G_b(b)$ at $b = S(y)$, with offer density $g_b(S(y)) = f_b(y)/S'(y)$, and it vanishes at an equilibrium offer.
3. The seller's first-order condition: $\partial \pi_s / \partial s = (v - s) g_s(s) + (1-k)(1 - G_s(s))$ at $s = B(x)$, and it vanishes at an equilibrium ask.

The milestones assume $S'(y) > 0$ (respectively $B'(x) > 0$), which the paper's formula for the offer density needs. The goal does not assume it.

Significance

Theorem 2 reduces the search for equilibria to the analysis of a pair of ordinary differential equations. Every explicit equilibrium in the paper and in the later $k$-double-auction literature is found as a solution of (3a)–(3b) with suitable boundary conditions: the linear equilibrium for uniform beliefs (the paper's Example 1), the one-parameter families of Satterthwaite–Williams, and the non-linear equilibria of Leininger–Linhart–Radner. The equations also expose how the split parameter $k$ distributes bargaining power: at $k = 1$ equation (3b) forces the seller to ask their own value, and at $k = 0$ equation (3a) forces the buyer to bid theirs.

The result is proved in the paper. To the best of a search of the platform, no formalization of it or of the bargaining model exists. This mission produces a machine-checked version of the necessary conditions. Its definitions of beliefs, expected profits, equilibrium and class $A$ are also the basis for companion missions on the uniform linear equilibrium and its trade probability.

Difficulty

The paper's proof is four lines: differentiate the expected profit, set the derivative to zero, substitute. Three steps of that argument do not survive a careful reading.

First, the paper differentiates under an offer density $g_b$ that exists only if $S$ is strictly increasing and has a positive derivative. Class $A$ allows $S$ to be flat at its bounds, to jump between them, and to have zero derivative. The formal goal assumes none of this. It must handle the case $S'(y) = 0$, where the offer distribution has an infinite density at $S(y)$ and the first-order condition becomes a one-sided argument.

Second, identifying $G_b(S(y))$ with $F_b(y)$ requires that no seller value outside a neighbourhood of $y$ makes the same offer. That is a global statement about $S$, and it is where monotonicity on the whole interval and the "flat only at the bounds" clause of class $A$ enter.

Third, the first-order condition needs the equilibrium offer $S(y)$ to be an interior maximiser of a function of $b$ that is differentiable there. The profit $\pi_b$ is an integral over the belief, and its differentiability at $S(y)$ must be derived from the differentiability of $S$ at the single point $y$ and of $F_b$. Neither $S$ nor $\pi_b$ is assumed continuous elsewhere.

Formalization scope

Values, offers and $k$ are real numbers. Beliefs are probability measures on $\mathbb R$, with distribution function Mathlib's ProbabilityTheory.cdf. Expected profits are Bochner integrals over the opponent's value, not over an offer density. The two agree whenever the density exists, and the integral form needs none. Integrability is not assumed: for a class $A$ strategy and a regular belief supported on the value interval, the integrand is bounded and almost everywhere measurable. Ties ($b = s$) trade. Deviations range over all real offers. Strategies are arbitrary functions $\mathbb R \to \mathbb R$ whose values outside the value interval play no role.

The derivative $S'(y)$ is deriv S y. The paper's inverses $B^{-1}$ and $S^{-1}$ are not introduced as functions. The matching value is a universally quantified variable $x$ with $B(x) = S(y)$, so no junk value of an inverse can make an equation true or false. The equations are asserted only at values $y$ interior to an open subinterval on which $S$ is strictly increasing. A formalization that assumed the first-order condition, or restricted to strategies with $S' > 0$ everywhere, would be a different and weaker theorem.

A complete development needs: differentiation of parametric integrals of indicator type (the derivative of $b \mapsto \int \mathbf 1\{S \le b\}\,h\,d\mu$), the change of variables from values to offers under a strictly increasing strategy, and Fermat's rule (IsLocalMax.hasDerivAt_eq_zero). The first two are reusable for auctions and other Bayesian games with monotone strategies. Proofs of the milestones, alternative proofs of the goal, and general lemmas about monotone strategies are welcome.

Selected references

• K. Chatterjee and W. Samuelson, Bargaining under Incomplete Information, Operations Research 31(5):835–851, 1983. https://doi.org/10.1287/opre.31.5.835
• R. B. Myerson and M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory 29(2):265–281, 1983. https://doi.org/10.1016/0022-0531(83)90048-0
• M. A. Satterthwaite and S. R. Williams, Bilateral Trade with the Sealed Bid k-Double Auction: Existence and Efficiency, Journal of Economic Theory 48(1):107–133, 1989. https://doi.org/10.1016/0022-0531(89)90120-8
• W. Leininger, P. B. Linhart and R. Radner, Equilibria of the Sealed-Bid Mechanism for Bargaining with Incomplete Information, Journal of Economic Theory 48(1):63–106, 1989. https://doi.org/10.1016/0022-0531(89)90121-X

Motivation

Classical non-cooperative game theory randomizes with objective, independent devices: each player spins a private wheel whose odds everyone agrees on. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) asks what changes when the randomizing events are ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. The paper introduced correlated equilibrium, and it also separates two effects that the classical model fuses: subjectivity (players disagree about probabilities) and correlation (players peg their choices on common or dependent events).

This mission formalizes the paper's result on subjectivity without correlation. Example 2.3 of the paper exhibits a three-person game in which strategies pegged on subjective but mutually secret events form an equilibrium that every player prefers to every classical mixed equilibrium. Proposition 5.1 shows that this cannot happen with two players.

Setting

A game has a finite set $N=\{1,\dots,n\}$ of players, a finite set $S_i$ of pure strategies for each player, a finite set $X$ of outcomes and an outcome function $g$ from $S=\times_{i\in N}S_i$ onto $X$. Player $i$ has a utility $u_i:X\to\mathbb R$; write $h_i(a)=u_i(g(a))$ for $a\in S$.

A randomizing structure consists of a set $\Omega$ of states of the world with a $\sigma$-field $\mathcal B$ of events, a sub-$\sigma$-field $\mathcal J_i\subseteq\mathcal B$ for each player (the events $i$ is informed about), and a probability measure $p_i$ on $\mathcal B$ for each player (the subjective probability of $i$). A strategy of $i$ is a map $s_i:\Omega\to S_i$ whose level sets $\{s_i=a\}$ lie in $\mathcal J_i$. For a profile $s=(s_1,\dots,s_n)$ of strategies the payoff of $i$ is

$$H_i(s)=\int_\Omega h_i\big(s(\omega)\big)\,dp_i(\omega),$$

computed under player $i$'s own beliefs. An equilibrium point is a profile $s$ with $H_i(s)\ge H_i(s_1,\dots,t_i,\dots,s_n)$ for every player $i$ and every strategy $t_i$ of $i$.

An event $A$ is $i$-secret if $A\in\mathcal J_i$ and every other player $j$ regards $A$ as independent of every event in the $\sigma$-field generated by the $\mathcal J_k$, $k\ne i$: $p_j(A\cap B)=p_j(A)p_j(B)$. A strategy is mixed if its level sets are $i$-secret, and objective if each level set has the same probability under every $p_j$. A measure is non-atomic on a $\sigma$-field $\mathcal R$ if every event of $\mathcal R$ of positive measure contains an event of $\mathcal R$ of strictly smaller positive measure; a roulette is a sub-$\sigma$-field of $\mathcal B$ on which every $p_j$ is non-atomic. Throughout, Assumption II holds: every player $i$ has a $\sigma$-field $\mathcal R_i$ of $i$-secret events on which every $p_j$ is non-atomic.

For distributions $\sigma_i$ on $S_i$ the classical payoff is $F_i(\sigma)=\sum_{a\in S}h_i(a)\prod_j\sigma_j(a_j)$, and $\sigma$ is a Nash equilibrium point if no player gains by switching to another distribution.

Formalization targets

Goal: Proposition 5.1 (p. 78)

Let $n=2$ and assume

$$p_1(B)=0\iff p_2(B)=0\qquad\text{for every }B\in\mathcal B.\tag{5.2}$$

Then for every equilibrium point $s$ in mixed strategies there is an equilibrium point $t$ in objective mixed strategies with

$$H(s)=H(t).$$

The game need not be zero-sum.

Milestones

1. Lemma 7.1 (p. 81): in a roulette $\mathcal R$, for events $B^1,\dots,B^l$ and $\alpha\in[0,1]$, there is an objective $A\in\mathcal R$ with $p_i(A)=\alpha$ and $p_i(A\cap B^k)=p_i(A)p_i(B^k)$ for all $i,k$.
2. Lemma 4.1 (p. 77): every distribution $\sigma_i$ on $S_i$ is realised by an objective mixed strategy $s_i$ with $p\{s_i=a\}=\sigma_i(a)$.
3. Lemma 7.3 (p. 82): if every $s_j$, $j\ne i$, is mixed, then $p_i\{s=a\}=p_i\{s_i=a_i\}\,p_i\{s_j=a_j\ \forall j\ne i\}=\prod_j p_i\{s_j=a_j\}$.
4. Corollary 7.4 (p. 83): mixed strategies are independent under every $p_k$.
5. Proposition 4.3 (p. 77): $\{F(\sigma):\sigma\text{ Nash}\}=\{H(s): s\text{ an equilibrium point in objective mixed strategies}\}$.

Significance

The result. Proposition 5.1 isolates correlation as the source of the new equilibrium payoffs of the subjective model in two-person games: disagreement about probabilities alone, with strategies pegged on secret events, reproduces only payoffs already achievable by classical mixed strategies (by Proposition 4.3, only Nash equilibrium payoffs). The paper uses it to explain Example 2.9, where two zero-sum players both expect more than the value, as an effect of subjectivity combined with correlation. Proposition 4.3 is the bridge that embeds classical Nash theory in the subjective model; with Nash's theorem it gives existence of equilibrium points in every game.

Formalizing it. The results are proved in the paper; to our knowledge none of them has been machine-checked. The mission produces a reusable measure-theoretic model of randomized strategies with private information and subjective beliefs (secret events, mixed and objective strategies, roulettes), a non-atomicity notion relative to a sub-$\sigma$-field, and the Lyapunov-type construction of Lemma 7.1, none of which exists in Mathlib at the pinned revision.

Difficulty

The equilibrium conditions quantify over all strategies of the deviator, i.e. all $\mathcal J_i$-measurable maps, and the deviator may know events on which the opponent's mixed strategy is pegged. The obvious computation of $H_1(t_1,s_2)$ as a sum of products of marginal probabilities is valid only because the opponent's strategy is pegged on secret events, which is the content of Lemma 7.3; for correlated strategies it fails, and Example 2.9 shows the proposition then fails. A second obstacle is that the replacement $t_1$ must reproduce player 2's beliefs about $s_1$, while player 1's own equilibrium condition is stated under $p_1$; condition (5.2) is what transfers "$a$ is played with positive probability" from one player's beliefs to the other's. Constructing objective strategies with prescribed probabilities (Lemmas 7.1 and 4.1) needs the convexity of the range of a non-atomic vector measure (Lyapunov's theorem), which is not in Mathlib.

Formalization scope

Players are a finite type (Fin 2 in the goal, players $1,2\mapsto 0,1$); the $S_i$ and $X$ are finite types, and $g$ is surjective. The $\sigma$-field $\mathcal B$ is an explicit parameter mΩ of the structure RandomizingStructure ι Ω mΩ, which carries the $\mathcal J_i$ and the probability measures $p_i$. Probabilities are $[0,\infty]$-valued Mathlib measures. Utilities and $p_i$ are data (Assumption I is used only to compare lotteries by expected utility; the uniqueness of $p_i$ is not encoded). $H_i$ is a Bochner integral; for strategy profiles the integrand has finitely many values and is measurable, hence integrable. Non-atomicity on a sub-$\sigma$-field is defined directly; Mathlib's NoAtoms (singletons are null) would trivialize Assumption II and is not used. "Mixed" means pegged on the family of all $i$-secret events, not on the $\sigma$-field $\mathcal R_i$ of Assumption II. Classical distributions, $F_i$ and Nash equilibrium points are AGT.IsLottery, AGT.expectedPayoff and AGT.IsMixedNash from the published definition agt_games.

A formalization that restricted deviations to mixed or objective strategies, or dropped "mixed" from the hypothesis on $s$, would state a different theorem and is ruled out.

Useful contributions: Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures (or the special case needed for Lemma 7.1), the factorization of Lemma 7.3, and the payoff identities used in the proof of Proposition 4.3. The model definitions are shared in meaning with the companion mission on two-person zero-sum games.

Selected references

• R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974) 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• J. Nash, Non-Cooperative Games, Annals of Mathematics 54 (1951) 286–295. https://doi.org/10.2307/1969529
• A. Liapounoff, Sur les fonctions-vecteurs complètement additives, Izv. Akad. Nauk SSSR Ser. Mat. 4 (1940) 465–478.
• L. J. Savage, The Foundations of Statistics, Wiley, 1954.

Motivation

Howard's finite Markovian decision process (MDP) models a controller who, at each instant, observes the state of a system, chooses a decision, collects a reward and moves to a random next state with known transition probabilities. Howard's policy-iteration algorithm computes an optimal policy, and the model has been applied to inventory control, equipment replacement, quality control and marketing. Its weak point is the requirement that every transition probability be known exactly: in applications these numbers are estimated and are hard to measure.

Satia and Lave (Operations Research 21(3), 1973) relax this requirement. In their game-theoretic formulation, the controller knows only a set of admissible probability rows for every state–decision pair, and nature chooses the rows adversarially. This is the model now called a robust MDP with (s,a)-rectangular uncertainty, studied later by Iyengar (Math. Oper. Res. 2005) and Nilim and El Ghaoui (Oper. Res. 2005), who reprove and extend the dynamic-programming results for it. The paper gives a policy-iteration algorithm for the max-min criterion and proves that it terminates at an optimal policy. This mission formalizes that part of the paper (pp. 728–732).

Timeline:

• 1953: Shapley introduces stochastic games (PNAS 39).
• 1960: Howard, Dynamic Programming and Markov Processes, policy iteration for known transitions.
• 1973: Satia and Lave, max-min and max-max policy iteration for uncertain transitions (dynamic-programming equations and optimality of pure stationary policies cited from Satia's 1968 Stanford thesis).
• 2005: Iyengar; Nilim and El Ghaoui, robust dynamic programming under rectangular uncertainty.

Setting

There are finitely many states $i$ and, in state $i$, a finite nonempty set $D_i$ of decisions $k$. A transition $i\to j$ under decision $k$ earns reward $r^k_{ij}$; rewards are discounted by $\beta$ with $0\le\beta<1$. For every pair $(i,k)$ there is a nonempty, closed, convex set $S_i^k$ of probability rows $p=(p_1,\dots,p_N)$, $p_j\ge0$, $\sum_j p_j=1$. Nature's choice is a matrix $P\in S$: one row $p_i^k\in S_i^k$ for every pair.

A pure stationary policy $A=(A_1,\dots,A_N)$ selects $A_i\in D_i$. Under $P$ its present value $v^A(P)$ is the unique solution of equations (5),

$$v_i^A=\sum_j p^{A_i}_{ij}\big(r^{A_i}_{ij}+\beta v_j^A\big).$$

Nature's minimum is $\underline v_i(A)=\inf_{P\in S}v_i^A(P)$, and the max-min return of criterion (2) is $\bar v_i=\max_A\underline v_i(A)$. A policy is max-min optimal if $\underline v(A)=\bar v$ in every state.

The algorithm alternates two routines. Phase 1 (nature's policy evaluation) fixes $A$, computes $v^A$ from the current rows, replaces each row at $A_i$ by a minimizer of $\sum_j p_j(r^{A_i}_{ij}+\beta v^A_j)$ over $S_i^{A_i}$ (6), and stops when the minima reproduce $v^A$. Phase 2 (policy improvement) chooses in each state a decision $B_i$ maximizing the test quantity (7),

$$t_i^k(v)=\min_{p\in S_i^k}\sum_j p_j\big(r^k_{ij}+\beta v_j\big),$$

at $v=\underline v(A)$, keeping $A_i$ on ties; if $B=A$ the algorithm terminates.

Formalization targets

Goal: Proposition 5 with Proposition 3

Along every run $A^0,A^1,\dots$ of Phase 2 steps,

$$\underline v(A^n)\le\underline v(A^{n+1})\ \ \forall n,\qquad \exists\,n<\#\{\text{policies}\}:\ A^{n+1}=A^n,\ \ \underline v(A^n)=\bar v,$$

and the terminal policy attains the solution of the equations (4) and is $\varepsilon$-optimal for every $\varepsilon>0$.

Milestones

• Eq. (5): the present-value equations have a unique solution.
• $[I-\beta P]^{-1}$ is nonnegative with diagonal at least 1 for stochastic $P$ (proof of Proposition 5).
• Proposition 1: equations (4), with randomized decisions and mixed choices of nature, have a unique solution, and it is the max-min return.
• Proposition 2: a pure stationary policy attains it.
• A non-final Phase 1 iteration lowers nature's value weakly everywhere and strictly somewhere (proof of Proposition 4).
• Proposition 4: Phase 1 comes within $\varepsilon$ of nature's optimum after finitely many iterations.
• Proposition 3: at termination no pure stationary policy is better.
• Each policy change strictly improves the max-min return (proof of Proposition 5).

Significance

The goal certifies a complete algorithm for the max-min problem: it computes a policy that is optimal against the worst admissible transition probabilities, in all states at once, in finitely many improvement steps. Propositions 1 and 2 show that the dynamic-programming equations (4) characterize the max-min value and that neither side gains from randomization. The known-transition case (every $S_i^k$ a single row) recovers Howard's policy iteration.

On the platform, Howard-type policy iteration for known transitions has been formalized (the Bertsekas Dynamic Programming and Optimal Control missions); nothing with uncertain transitions exists. The results of this paper are proved in the literature (Satia's thesis, and in greater generality by Iyengar and by Nilim and El Ghaoui); none has a machine-checked proof. This mission produces the first formal robust-MDP model and robust policy-iteration theorem on the platform.

Difficulty

The obvious argument copies Howard's improvement lemma. It fails at two points. First, the value of a policy is itself the result of an inner optimization by nature, so comparing two policies requires comparing two different worst-case transition matrices; the matrix $P^{*B}$ minimizing against $B$ is not the one minimizing against $A$. Second, the proof of Proposition 4 as printed shows only that nature's values decrease and converge; that the limit is nature's optimum, over a continuum of admissible rows, needs a separate argument. Finally, Proposition 1 involves randomized strategies and probability measures on the uncertainty sets, and reducing them to pure strategies is the content of Propositions 1 and 2, not a definitional convenience.

Formalization scope

States are a finite type S (nonemptiness is not needed: every statement is unchanged in meaning at $N=1$ and trivially true at $N=0$), decisions a family D : S → Type* of finite nonempty types. The model fixes these conventions and readings:

• $0\le\beta<1$ (not printed; every return is an infinite discounted sum) and nonempty $S_i^k$ (not printed; Phase 1 presupposes a feasible row) are added standing hypotheses; closedness and convexity are the paper's.
• The present value is $[I-\beta P^A]^{-1}$ applied to the one-step rewards; the Eq. (5) milestone proves it is the unique solution of (5).
• "min over $p_i^k\in S_i^k$" in (2) is an infimum over the nonempty type of admissible choices $P\in S$, bounded below; "max over all policies" is a maximum over pure stationary policies, with randomization handled in (4).
• In (4), $\tau$ ranges over probability vectors on $D_j$ and $\alpha$ over probability measures on row vectors with $\alpha(S_j^k)=1$; the missing integral sign and unmatched brace of the printed display are corrected.
• "Optimal" = equal to the max-min return in every state; "$\varepsilon$-optimal" = within $\pm\varepsilon$ in every state (p. 731); "$\varepsilon$-optimal for nature" = within $\varepsilon$ of nature's minimum.
• "Terminates" = Phase 2 returns the same policy; "a finite number of iterations" is stated with the explicit bound "fewer than the number of policies".
• Phase 1 is taken exact in Phase 2 (the proofs of Propositions 3 and 5 use exact minimizers); the Phase 1 stopping test is printed without $\Sigma$ and the sum is formalized.
• Retention rule: Phase 2 keeps $A_i$ when it is already a maximizer. It is not printed, but it is Howard's rule and Proposition 5 is false without it.
• Proposition 5's "$\varepsilon$-optimal … in a finite number of iterations" is formalized as exact termination at an optimal policy, which implies the printed claim for every $\varepsilon$.

Equation (4) must not be collapsed to $\max_k\min_{p\in S_j^k}$ in its definition: that would make Proposition 2 true by definition. Similarly, the Phase 2 relation always has a successor and algorithm runs exist from every policy, so the goal is not vacuous.

Needed infrastructure: Neumann series for $I-\beta P$ with stochastic $P$, monotonicity of policy evaluation, existence of minimizers of linear functions on compact subsets of the simplex, and the contraction argument for the robust Bellman operator. These are reusable for any robust or known-transition MDP development. Proofs of any milestone, alternative arguments for Propositions 1 and 2, and extensions to the max-max criterion are welcome.

Selected references

• J. K. Satia and R. E. Lave, Jr., Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3), 728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• L. S. Shapley, Stochastic Games, PNAS 39(10), 1095–1100, 1953. https://doi.org/10.1073/pnas.39.10.1095
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2), 257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• A. Nilim and L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5), 780–798, 2005. https://doi.org/10.1287/opre.1050.0216

Motivation

Existence of equilibrium is the first question any model of strategic interaction must answer, and the classical answer — Nash's theorem via Kakutani's fixed point theorem — asks for a convex, compact strategy space and continuous payoffs. Many of the models economists actually use do not have that: a firm's technology set can be discrete or irregular, and a payoff need only be upper semicontinuous, not continuous. Topkis [1979] showed that when a game's structure is instead order-theoretic — each player's strategies form a lattice, and the players' incentives reinforce each other in a precise sense — an equilibrium exists without any convexity or continuity assumption at all, and the proof method delivers something Kakutani's theorem cannot: a greatest and a least equilibrium point, with the whole equilibrium set forming a complete lattice. Zhou [1994] later showed the completeness of the equilibrium lattice in full generality; this mission formalizes the resulting theorem (Topkis's Theorem 4.2.1) together with its parametric extension (Theorem 4.2.2, established independently by Milgrom and Roberts [1990a] and Sobel [1988]), which shows how the greatest and least equilibria move as a parameter of the game — its technology, its cost structure — changes. This machinery underlies monotone comparative statics for games throughout economics: oligopoly models with strategic complements, coordination games, and search and matching models with increasing returns.

Setting

A noncooperative game $(N, S, \{f_i : i \in N\})$ consists of a finite player set $N$, a set $S \subseteq \mathbb{R}^m$ of feasible joint strategies $x = (x_i)_{i \in N}$ (allowing the set of strategies feasible for one player to depend on the others' choices, so $S$ need not be a product set), and a payoff function $f_i$ for each player $i$. Write $x_{-i}$ for the strategies of every player but $i$, $S_i(x_{-i})$ for the section of $S$ at $x_{-i}$ — player $i$'s feasible strategies given the others' choice — and $Y_i(x_{-i}) = \operatorname{argmax}_{y_i \in S_i(x_{-i})} f_i(y_i, x_{-i})$ for player $i$'s best-response set. The best joint response correspondence is $Y(x) = \prod_{i \in N} Y_i(x_{-i})$. A feasible $x'$ is an equilibrium point if $f_i(y_i, x'_{-i}) \le f_i(x')$ for every player $i$ and every feasible deviation $y_i \in S_i(x'_{-i})$ — no player can unilaterally improve.

A lattice is a partially ordered set in which every pair of elements has a join $\vee$ and a meet $\wedge$. A function $g$ is supermodular on a subset if $g(x) + g(y) \le g(x \vee y) + g(x \wedge y)$ for all $x, y$ in it, and has increasing differences in two of its arguments $(y,t)$ if $y \mapsto g(y, t'') - g(y, t')$ is monotone whenever $t' \prec t''$. A game $(N, S, \{f_i\})$ is a supermodular game if $S$ is a sublattice, $f_i(y_i, x_{-i})$ is supermodular in $y_i$ for every fixed $x_{-i}$ and every $i$, and $f_i(y_i, x_{-i})$ has increasing differences in $(y_i, x_{-i})$ for every $i$ — jointly, the conditions under which each player's own strategy components are complements and complementary to the other players' strategies (Theorem 2.6.1 of chunk 01-lattices/02-monotonicity's book).

Formalization targets

Goal — Theorem 4.2.1

If $(N, S, \{f_i\})$ is a supermodular game, $S$ is nonempty and compact, and each $f_i(y_i, x_{-i})$ is upper semicontinuous in $y_i$ on $S_i(x_{-i})$ for every $x_{-i}$ and every $i$, then

$$\{\text{equilibrium points of } (N, S, \{f_i\})\}$$

is nonempty, has a greatest and a least element, and, under the order it inherits from $\mathbb{R}^m$, is itself a nonempty complete lattice.

Theorem 4.2.2 (the parametric extension)

Let $T$ be a partially ordered set and, for each $t \in T$, $(N, S^t, \{f_i^t\})$ a supermodular game with $S^t$ nonempty, compact, and increasing in $t$; suppose each $f_i^t(y_i, x_{-i})$ is upper semicontinuous in $y_i$ and has increasing differences in $(y_i, t)$. Then for every $t$ there exist a greatest and a least equilibrium point of game $t$, and both are increasing functions of $t$ on $T$ — the equilibrium set moves monotonically as the parameter increases.

Two supporting results are formalized as milestones because Theorem 4.2.1's own proof uses them directly: Lemma 4.2.1 (equilibrium points are exactly the fixed points of the best joint response correspondence) and Lemma 4.2.2, parts (b) and (f) (the best joint response set is a nonempty compact sublattice for every feasible $x$, and the correspondence is increasing in $x$).

Significance

The result itself. Theorem 4.2.1 is the lattice-theoretic alternative to Nash/Kakutani existence: it needs no convexity of $S$ and no continuity of $f_i$ (upper semicontinuity suffices), and in exchange it delivers a greatest and a least equilibrium — with an explicit order-theoretic characterization via Theorem 2.5.1 of chunk 01-lattices — and the guarantee that the entire equilibrium set is a complete lattice, not merely nonempty. Theorem 4.2.2 gives this existence result teeth for applied comparative statics: it says that if a firm's cost structure, a market's demand parameter, or any other feature of the game increases (in the sense of the induced set order on $S^t$ and increasing differences in the payoffs), the extremal equilibria increase too — the qualitative content behind results such as "more competition leads to lower prices" in supermodular oligopoly models.

Formalizing it. The platform's existing Nash-equilibrium theorem (AGT.nash_existence, Theorem 1.8 of Algorithmic Game Theory) is a Brouwer/Kakutani argument for finite games with mixed strategies: it needs finiteness of every player's strategy set (so that mixed strategies form a compact convex simplex) and gives no lattice structure on the equilibrium set at all. Theorem 4.2.1 is a different technique entirely — it needs no finiteness, no mixing, and no convexity, and its conclusion (a complete lattice of equilibria) is exactly the content Brouwer/Kakutani cannot give. This mission is therefore not a restatement of Nash's theorem in different notation, but a second, independent existence technique with a strictly different structural payoff, formalized here for the first time on the platform. It builds directly on chunk 01-lattices's Theorem 2.5.1 (Zhou's fixed point theorem for increasing correspondences) and chunk 02-monotonicity's supermodularity/increasing differences definitions, both formalized earlier in this series.

Difficulty

The natural first idea for existence — "the best joint response correspondence has a fixed point by some general fixed-point theorem for correspondences" — needs the correspondence to be convex-valued and upper hemicontinuous for a Kakutani argument, neither of which supermodularity or upper semicontinuity alone supply: a best-response set under only upper semicontinuity can be a disconnected, non-convex set (e.g. the maximizers of a supermodular but non-quasiconcave function). The actual route goes through order instead of topology: Lemma 4.2.2 shows the best joint response set is a compact sublattice (hence subcomplete, by Theorem 2.3.1) and that the correspondence is increasing under the induced set order, which is exactly the hypothesis Theorem 2.5.1's non-constructive supremum/infimum construction needs — no convexity anywhere. A second subtlety, which the mission is careful not to elide: the equilibrium set of a supermodular game need be neither compact nor a sublattice of $\mathbb{R}^m$ when there are more than one player (Topkis's Examples 4.2.1 and 4.2.2 exhibit both failures); only the weaker claim — a complete lattice under the inherited order — is true in general, and that is what Theorem 2.5.1(b) supplies.

Formalization scope

A joint strategy is represented as a dependent function ∀ i, Fin (m i) → ℝ over a finite player type ι, with a player's own strategy accessed and overwritten via Function.update, so that $x_{-i}$ is never reified as a separate object — every statement about $f_i(y_i, x_{-i})$ or membership in $S_i(x_{-i})$ substitutes y for x's own i-th coordinate directly. IsSupermodularGame reuses chunk 02-monotonicity's SupermodularOn and IncreasingDifferencesOn verbatim, applied to each player's own payoff, rather than restating the supermodularity/increasing- differences conditions from scratch — a formalization that inlined a weaker, ad hoc notion here (e.g. supermodularity of the joint payoff vector rather than each player's own payoff in their own strategy) would trivialize the connection to chunk 02-monotonicity's theorems that the book's own proof relies on. Theorem 4.2.1's "nonempty complete lattice" conclusion is formalized, as in chunk 01-lattices, via IsLUB/IsGLB on the subtype of equilibrium points — never as membership of the ambient $\mathbb{R}^m$ supremum/infimum in the equilibrium set, which the book's own Examples 4.2.1–4.2.2 refute; a solution that instead proved the equilibrium set compact or a sublattice of $\mathbb{R}^m$ would be proving a strictly stronger and false claim. Only parts (b) and (f) of Lemma 4.2.2 are formalized, since those are the only two of its eight parts the proof of Theorem 4.2.1 uses; a complete development still needs chunk 01-lattices's Theorem 2.3.1 (subcomplete iff compact) and Theorem 2.5.1/2.5.2, and chunk 02-monotonicity's Theorem 2.8.1 and Corollary 2.7.1, none of which are restated here.

Selected references

• Topkis, D. M., Equilibrium points in nonzero-sum n-person submodular games, SIAM Journal on Control and Optimization 17(6), 1979, pp. 773–787. https://doi.org/10.1137/0317054
• Zhou, L., The set of Nash equilibria of a supermodular game is a complete lattice, Games and Economic Behavior 7(2), 1994, pp. 295–300. https://doi.org/10.1006/game.1994.1051
• Milgrom, P. and Roberts, J., Rationalizability, learning, and equilibrium in games with strategic complementarities, Econometrica 58(6), 1990, pp. 1255–1277. https://doi.org/10.2307/2938316
• Sobel, M. J., Isotone comparative statics for supermodular games, unpublished manuscript, 1988 (cited by Topkis [2011], Theorem 4.2.2).
• Topkis, D. M., Supermodularity and Complementarity, Princeton University Press, 2011 (DOI 10.1515/9781400822539), Chapter 4, §4.1–4.2.

Motivation

Two-player zero-sum games and linear programming are, on their surface, unrelated pieces of 20th-century mathematics: von Neumann's minimax theorem for games (1928) was proved with tools from topology, and linear programming duality (Dantzig, 1940s) with convexity and geometry. Yet the two are formally equivalent — Dantzig recounts von Neumann conjecturing the equivalence outright, on first hearing a description of linear programming, because he had "just recently completed a book with Oscar Morgenstern on the theory of games" [Albers, Alexanderson, and Reid, More Mathematical People, 1990]. Freund and Schapire (1999) later showed that both concepts reduce, in one uniform way, to online regret minimization: a decades-old topological existence proof and a decades-old LP-duality argument both become corollaries of a single fact about no-regret learning. This mission formalizes the algorithmic content of that reduction — Hazan's Lemma 8.4, which is not merely an existence statement but a concrete, efficient algorithm with an explicit convergence rate.

Setting

A two-player zero-sum game in normal form is a real matrix $A \in \mathbb{R}^{n \times m}$ (Hazan restricts entries to $[-1,1]$ for interpretability as losses/rewards, a convention this mission's theorems drop as inessential — the argument is invariant to scaling and shifting). The row player picks a mixed strategy $x$ in the probability simplex $\Delta_n = \{x \in \mathbb{R}^n : x_i \ge 0, \sum_i x_i = 1\}$; the column player picks $y \in \Delta_m$. The row player's expected loss, and simultaneously the column player's expected reward, is the bilinear form $x^{\mathsf T} A y$.

The row player's guaranteed loss is $\lambda_R = \min_{x \in \Delta_n} \max_{y \in \Delta_m} x^{\mathsf T} A y$: the smallest loss she can secure no matter what the column player does. Symmetrically, the column player's guaranteed reward is $\lambda_C = \max_{y \in \Delta_m} \min_{x \in \Delta_n} x^{\mathsf T} A y$. Always $\lambda_R \ge \lambda_C$ ("weak duality" — an elementary max-min/min-max inequality, Direction 1 of Section 8.3). Von Neumann's minimax theorem (Theorem 8.3) is the nontrivial converse: $\lambda_R = \lambda_C$, a common value $\lambda^\star$ called the value of the game, whose optimal strategies form a Nash equilibrium — already on the platform as AGT.zero_sum_minimax.

Algorithm 28 ("Simple LP", p. 147) computes an approximate equilibrium constructively. The row player runs a multiplicative-weights / Exponentiated Gradient update against the sequence of best-response losses the column player generates in a repeated $T$-round play of the game: starting from the uniform strategy $x_1 = (1/n, \dots, 1/n)$, at each round $t$ the column player best-responds with $y_t \in \arg\max_{y \in \Delta_m} x_t^{\mathsf T} A y$, and the row player updates $x_{t+1}(i) \propto x_t(i)\, e^{-\eta (A y_t)_i}$. The algorithm returns the time-averaged strategy $\bar{x} = \frac{1}{T}\sum_{t=1}^T x_t$.

Formalization targets

Goal — Lemma 8.4

$$\max_{y' \in \Delta_m} \bar{x}^{\mathsf T} A y' \;\le\; \lambda_R(A) + \frac{\sqrt{2 \log n}}{\sqrt{T}}$$

for the vector $\bar{x}$ returned by Algorithm 28 after $T$ rounds with learning rate $\eta = \sqrt{2 \log n / T}$. The book calls $\bar{x}$ a "$\sqrt{2 \log n}/\sqrt{T}$-approximate solution" to the zero-sum game — and, via Section 8.2.1's equivalence, to the linear program the game encodes — in exactly this sense. The goal is stated against $\lambda_R$, the quantity the algorithm's own analysis produces; Theorem 8.3 identifies it with $\lambda_C$ and with the book's $\lambda^\star$, so nothing about the bound is lost by this choice of rendering.

Supporting milestone — Eq. (8.1)

$$\sum_{t=0}^{T-1} x_t^{\mathsf T} A y_t \;\le\; \min_{x' \in \Delta_n} \sum_{t=0}^{T-1} (x')^{\mathsf T} A y_t \;+\; \sqrt{2T \log n}$$

the external-regret bound the row player's multiplicative-weights update achieves against the adaptively-chosen linear loss sequence $f_t(\cdot) = (\cdot)^{\mathsf T} A y_t$ — the single analytical fact the goal's proof needs.

Significance

The result itself. Lemma 8.4 gives a genuinely efficient algorithm: $O(\log n / \varepsilon^2)$ rounds of a trivial multiplicative update to reach an $\varepsilon$-approximate value and equilibrium of an $n \times m$ zero-sum game, and — through the equivalence with LP duality — an approximation algorithm for a broad class of linear programs, predating and prefiguring the multiplicative-weights-based approximation schemes surveyed by Arora, Hazan, and Kale (2012). It is also the constructive engine behind Theorem 8.3: unlike the classical topological proof of the minimax theorem, this one produces the equilibrium, not just its existence.

Formalizing it. The equilibrium-existence half of this story, Theorem 8.3, is already a published, proved-format Prove2Me theorem (AGT.zero_sum_minimax, from the Algorithmic Game Theory series) and is reused here as a reference item rather than redrafted. What that theorem does not capture — and what makes this mission non-trivial rather than a restatement — is the quantitative, algorithmic content: that one specific, simple, Hedge-type update, run for a specific number of rounds, provably gets within a specific, explicit distance of the value, using only the existence of some sublinear-regret online algorithm as a black box.

Difficulty

The tempting shortcut is to formalize only "no-regret learning dynamics converge to an equilibrium" as a qualitative statement, discharging it by citing AGT.zero_sum_minimax (equilibria exist) plus a generic regret bound. That collapses Lemma 8.4 into a restatement of Theorem 8.3 and drops exactly what is new here: the explicit rate $\sqrt{2\log n}/\sqrt{T}$, tied to one concrete update rule (Algorithm 28) rather than an arbitrary sublinear-regret black box. The real content is in chaining three quantitative facts — Eq. (8.1)'s specific regret bound for the multiplicative-weights update, the column player's best-response equality (Eq. (8.2)), and the definitional unfolding of $\lambda_R$ — with none of the slack that a purely qualitative "an algorithm with sublinear regret exists" argument would tolerate.

Formalization scope

Matrices are Matrix (Fin n) (Fin m) ℝ with n, m ≥ 1 (empty strategy sets are excluded throughout, matching this mission's reference item AGT.zero_sum_minimax); mixed strategies use Mathlib's stdSimplex ℝ (Fin n). lambdaR/lambdaC are rendered with iInf/iSup over simplex membership, the same convention Introduction to Online Convex Optimization III fixed for RegretT earlier in this series. Algorithm 28's run is packaged as a Prop-valued structure (IsSimpleLPRun) rather than a computable function, in the style of this series' other algorithm-run definitions (IsHedgeRun, IsOnlineGradientDescent): initial uniform strategy, a best-response condition on the column player at every round, and the multiplicative-weights recursion on the row player, with the learning rate η left free and fixed to √(2 log n / T) only at the point the theorems need the book's specific constant.

The trivializing risk here is stating only that some sublinear-regret algorithm secures the bound (already implied, vacuously, by AGT.zero_sum_minimax plus any regret bound); this mission rules that out by fixing the exact update rule of Algorithm 28 in IsSimpleLPRun and proving the bound for that rule specifically, with the book's exact constant √(2 log n)/√T, not an unspecified O(·).

Chapter 5's Corollary 5.7 (the general RFTL/Exponentiated-Gradient regret bound) belongs to a different mission of this series and is not imported; eg_regret_bound restates, locally and self-containedly, exactly the instance of it this chapter's proof needs. A later mission for Chapter 5, once published, could supersede this local restatement by specializing its general bound — a natural contribution for a solver with that mission's Lean available.

Selected references

• J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen, 1928.
• Y. Freund and R. E. Schapire, "Adaptive Game Playing Using Multiplicative Weights", Games and Economic Behavior, 1999. https://doi.org/10.1006/game.1999.0738
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., 2022. arXiv:1909.05207v3
• N. Nisan, T. Roughgarden, E. Tardos, and V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007. https://doi.org/10.1017/CBO9780511800481
• S. Arora, E. Hazan, and S. Kale, "The Multiplicative Weights Update Method: a Meta-Algorithm and Applications", Theory of Computing, 2012. https://doi.org/10.4086/toc.2012.v008a006

Motivation

The strategic-form game is the basic object of noncooperative game theory, and the Nash equilibrium — a profile of randomized strategies from which no player benefits by deviating unilaterally — is its central solution concept. Nash proved in 1951 that every game with finitely many players and finite strategy sets has such an equilibrium (Nash, Non-cooperative games, Ann. Math. 54 (1951)); this single existence theorem is the reason the concept organizes the rest of the field, from the computational complexity of finding equilibria to the price of anarchy. The theorem is stated as Theorem 1.8 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), the source text of this mission series, whose first chapter (Tardos–Vazirani) also treats the two special cases that admit direct algorithmic proofs: two-person zero-sum games, where equilibria are exactly the optimal solutions of a dual pair of linear programs (von Neumann 1928; Theorem 1.11), and a simple linear market, where equilibrium prices are computed by an ascending tight-set algorithm (Theorem 1.17).

A timeline of the existence theorem: von Neumann (1928) proved the minimax theorem for two-person zero-sum games; Nash (1950, 1951) extended existence to arbitrary finite games, first via Kakutani's fixed-point theorem and then via Brouwer's. All known proofs of the general theorem pass through a fixed-point principle, and this is not an artifact: computing a Nash equilibrium is PPAD-complete (Daskalakis–Goldberg–Papadimitriou 2009; Chen–Deng–Teng 2009), and PPAD is precisely the complexity class of the fixed-point arguments.

Setting

A finite strategic-form game consists of a finite set $\iota$ of players, for each player $i$ a finite nonempty set $S_i$ of pure strategies, and for each player a payoff function $u_i : \prod_j S_j \to \mathbb{R}$; all players are utility maximizers. A mixed strategy for player $i$ is a probability distribution on $S_i$, represented as a weight function $\sigma_i : S_i \to \mathbb{R}$ with $\sigma_i \ge 0$ and $\sum_{s} \sigma_i(s) = 1$ (a lottery). Players randomize independently, so a mixed profile $\sigma = (\sigma_i)_{i}$ induces the product distribution on pure strategy vectors, and player $i$'s expected payoff is

$$U_i(\sigma) \;=\; \sum_{s \in \prod_j S_j} \Big(\prod_j \sigma_j(s_j)\Big)\, u_i(s).$$

A mixed profile $\sigma$ is a (mixed) Nash equilibrium if for every player $i$ and every lottery $\tau$ on $S_i$, replacing $\sigma_i$ by $\tau$ does not increase $U_i$.

A two-person zero-sum game is given by a matrix $A \in \mathbb{R}^{m \times n}$: the row player picks a row distribution $p$, the column player a column distribution $q$, and the column player pays the row player $p^{\mathsf T} A q$ in expectation.

The market of §1.8.1 of the source has finitely many divisible goods, good $a$ in $s_a$ units, and finitely many buyers, buyer $j$ bringing budget $m_j > 0$ and interested in a nonempty set of goods; utilities are linear 0/1, so a buyer wants any goods from her interest set and none other. Market-clearing prices are positive prices under which each buyer can spend her whole budget on cheapest goods in her interest set while every good sells out exactly.

Formalization targets

Goal (capstone) — Theorem 1.8

$$\text{Every finite strategic-form game has a mixed Nash equilibrium.}$$

Stated for an arbitrary finite family of finite nonempty strategy types; no bound on the number of players, no genericity assumptions.

Supporting — Brouwer fixed-point theorem

$$K \subseteq E \text{ nonempty compact convex},\ E \text{ finite-dimensional},\ f : K \to K \text{ continuous} \implies \exists x,\ f(x) = x.$$

Mathlib currently has no form of Brouwer's theorem; every known proof of Theorem 1.8 needs it (or an equivalent), so it enters the mission as an explicit milestone rather than an assumed library fact.

Theorem 1.11 — zero-sum games

$$\exists\, p^\ast, q^\ast:\quad \forall p,\ p^{\mathsf T} A q^\ast \le {p^\ast}^{\mathsf T} A q^\ast, \quad \forall q,\ {p^\ast}^{\mathsf T} A q^\ast \le {p^\ast}^{\mathsf T} A q, \quad\text{and}\quad (p^\ast, q^\ast) \text{ is a mixed Nash equilibrium}$$

of the explicit two-player game with payoffs $A_{xy}$ to the row player and $-A_{xy}$ to the column player. The source states the result as: optimal solutions of a dual pair of LPs form a Nash equilibrium of the zero-sum game; the first two conjuncts are the saddle point that LP optimality amounts to, and the third states the Nash-equilibrium clause against the mission's own game vocabulary, so "zero-sum" is formal (the two payoffs sum to zero) rather than implicit in the shape of the statement.

Theorem 1.17 (existence form)

$$\text{The 0/1-utilities linear market admits market-clearing prices and allocations.}$$

The source proves this by an ascending-price algorithm and also bounds its running time; the complexity half has no formal counterpart in this mission.

Significance

The capstone is the foundation of the whole mission series: correlated equilibria, price-of-anarchy bounds, and mechanism-design characterizations in later missions all quantify over or compare against Nash equilibria, and the series inherits its game vocabulary (IsLottery, IsMixedProfile, expectedPayoff, IsMixedNash) from this mission.

Formalizing it produces the first Brouwer fixed-point theorem in this environment — a well-known gap in mathlib with reuse value far beyond game theory (every degree-theoretic and equilibrium-existence argument needs it). The zero-sum milestone yields the minimax theorem, reusable for the learning-dynamics mission that follows. All results here are classical and proved on paper; the work requested is machine-checked proof, not new mathematics.

Difficulty

The central difficulty is Brouwer. The standard routes are (i) Sperner's lemma plus a limit argument, which needs a formal theory of simplicial subdivisions that does not exist in mathlib; (ii) algebraic topology (no retraction of the ball onto the sphere), for which mathlib has singular homology but not yet the homology of spheres in usable form; (iii) analytic proofs (Milnor–Rogers). None is short; the milestone is deliberately stated for a general nonempty compact convex set in a finite-dimensional normed space so that any route serves, and so the lemma lands in reusable generality.

Given Brouwer, Theorem 1.8 still requires Nash's gain-function construction on the product of simplices and the verification that fixed points are equilibria — bookkeeping-heavy but standard. Theorem 1.11 does not need Brouwer: mathlib's Sion minimax theorem (Mathlib.Topology.Sion) applies to the bilinear payoff on the product of standard simplices, or one can argue by LP duality directly. Theorem 1.17 needs the tight-set/max-flow argument of Lemmas 1.15–1.16 or any direct construction of the equilibrium.

Formalization scope

Games are presented concretely: players form a finite index type, strategies a finite type per player, payoffs are functions into $\mathbb{R}$; mixed strategies are weight functions with a IsLottery predicate, not measure-theoretic distributions. Deviations in the equilibrium definition range over all lotteries (not only pure strategies): the pure-deviation reduction is a lemma a solver may prove, not part of the definition. Strategy sets are assumed nonempty in the capstone; the player set need not be. In the zero-sum milestone both dimensions are positive (Fin (m+1), Fin (n+1)), payoffs flow from the column player to the row player, stdSimplex plays the role of the mixed-strategy space, and the Nash-equilibrium conjunct is stated for the Boolean-indexed two-player game built by matrixGameStrat/zeroSumPayoff/matrixGameProfile from the definitions bundle. In the market milestone all supplies and budgets are positive, every buyer's interest set is nonempty, and every good has an interested buyer, matching the standing assumptions of §1.8.1; allocations are recorded as money spent, so the clearing condition is $\sum_j x_{ja} = p_a s_a$ with no division anywhere.

Trivializing readings are ruled out: the empty simplex has no lotteries, so nonemptiness hypotheses appear exactly where their absence would make an existence claim false (Brouwer on the empty set, games with an empty strategy set, zero-dimensional matrix games).

Selected references

• J. F. Nash, Non-cooperative games, Annals of Mathematics 54 (1951), 286–295. DOI
• J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100 (1928), 295–320. DOI
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 1. DOI
• C. Daskalakis, P. W. Goldberg, C. H. Papadimitriou, The complexity of computing a Nash equilibrium, SIAM J. Computing 39 (2009), 195–259. DOI

Why acquihiring matters

Technology firms often buy small startups mainly to obtain their staff, a practice known as acquihiring; Chatterji and Patro (2014) identify 98 such deals between 2009 and 2013. Bar-Isaac, Johnson and Nocke (CRC TR 224 Discussion Paper No. 500, 2024, www.crctr224.de; published in Management Science, 2025, doi:10.1287/mnsc.2024.04604) study the labour-market side instead. A firm that wants a startup's essential employee can compete for her in wages, or it can buy her employer and so remove the only rival bidder for her services. Their baseline model, the subject of this mission, isolates that choice. It shows that whenever the acquirer hires the employee, it does so by buying the startup, and that the employee is always worse off as a result.

This mission is the first of a series of three on the paper. The second formalizes the extension with Nash bargaining over the price and possible poaching after a failed bid (Proposition 2). The third formalizes the version in which the employee's private benefit is private information (Proposition 5).

Setting

There are three players: a startup $s$, an employee $e$, and a potential acquirer $a$. The employee generates value $v_s$ when working at the startup and $v_a$ when working at the acquirer. At either firm she is paid a wage of at least the floor $\underline{w}$ (written wl in Lean), and at the startup she also enjoys a private benefit $b$. Throughout the paper,

$$b > 0, \qquad \min\{v_a, v_s\} > b + \underline{w}.$$

In Lean these four numbers form the structure Params (fields va, vs, b, wl), and the displayed assumption is the predicate Params.Standing.

The acquirer first chooses a mode.

• Direct hiring. The acquirer and the startup simultaneously offer wages $w_a, w_s \ge \underline{w}$. The employee then joins the acquirer (payoff $w_a$) or stays at the startup (payoff $w_s + b$). The acquirer earns $v_a - w_a$ if she joins it, and the startup earns $v_s - w_s$ if she stays; the firm that loses her earns $0$.
• Acquihiring. The acquirer bids a price $p$ for the startup. If the startup accepts, the acquirer makes the employee a wage offer $w_a \ge \underline{w}$ and earns $v_a - w_a - p$, while the startup receives $p$. If the startup declines, it makes a wage offer $w_s \ge \underline{w}$ and earns $v_s - w_s$. The employee has no alternative offer at that stage.

The paper restricts attention to equilibria in undominated strategies: no firm offers or bids more than its willingness to pay (footnote 13). A continuation equilibrium of each mode is a profile (offers, bid, and the accept/decline rules of the employee and of the startup at every possible offer) in which every player best-responds, both on and off the path of play. The total surplus of an outcome is $v_a$ if the employee ends up at the acquirer and $v_s + b$ if she stays; wages and the price are transfers. An outcome is efficient when its surplus equals $\max\{v_a, v_s + b\}$.

Formalization targets

Goal: Proposition 1

For every continuation equilibrium of the direct-hiring subgame and every continuation equilibrium of the acquihiring subgame:

$$v_a > v_s \;\Longrightarrow\; \text{the bid is accepted and } \pi_a^{\mathrm{AH}} > \pi_a^{\mathrm{DH}}, \qquad v_a < v_s \;\Longrightarrow\; \text{no hiring under either mode},$$ $$u_e^{\mathrm{AH}} < u_e^{\mathrm{DH}} \quad\text{for all admissible parameters},$$

where $\pi_a$ denotes the acquirer's payoff and $u_e$ the employee's payoff under each mode. The goal also states that continuation equilibria exist away from the knife edges $v_a = v_s + b$ (direct hiring) and $v_a = v_s$ (acquihiring), so that the universal statements are not vacuous. In words: if the acquirer hires the employee, which happens exactly when $v_a > v_s$, then it does so through acquihiring, and the employee always prefers direct hiring.

Milestones

1. Lemma 1 (p. 5). Under direct hiring, the acquirer hires the employee at wage $v_s + b$ if $v_a > v_s + b$; the startup retains her at wage $v_a - b$ if $v_a < v_s + b$; and the outcome is efficient.
2. Lemma 2 (pp. 5–6). Under acquihiring, if $v_a > v_s$ the bid $p = v_s - \underline{w}$ is accepted and the employee is paid $\underline{w}$; if $v_a < v_s$ the bid (for instance $p = v_a - \underline{w}$) is declined and the startup pays $\underline{w}$. The outcome is efficient if $v_a \ge v_s + b$ or $v_a < v_s$, and inefficient if $v_s < v_a < v_s + b$.
3. The acquirer's direct-hiring payoff (proof of Proposition 1, p. 6): $\max\{0, v_a - v_s - b\}$.
4. The employee's direct-hiring payoff (proof of Proposition 1, p. 6): $v_s + b$ if $v_a \ge v_s + b$, and $v_a$ otherwise.

Significance

The proposition carries the paper's main message in its simplest form. Buying the startup removes wage competition: the acquirer pays the startup its retention profit $v_s - \underline{w}$ and then pays the employee only the floor $\underline{w}$. It never compensates her for the private benefit she loses. As a result, acquihiring occurs whenever $v_a > v_s$, including the range $v_s < v_a < v_s + b$ in which it destroys surplus, and the employee loses relative to direct hiring in every case. Formalization adds a fully explicit version of the equilibrium analysis. The paper calls Lemmas 1 and 2 "immediate" and does not spell out the employee's tie-breaking or the off-path behaviour that the equilibrium concept requires. Here each subgame is an explicit predicate on strategy profiles, so a complete proof also has to show that the stated outcomes are the only ones. The results are proved in the paper. No machine-checked proof of them is known, and the platform currently has no formalization of acquisitions or of wage competition between firms.

Difficulty

The algebra is elementary; the work lies in the uniqueness half of Lemma 1. Exhibiting one equilibrium is routine. Showing that every equilibrium has the stated outcome requires ruling out each alternative: a winning offer above the rival's reservation level can be undercut, and a losing firm with surplus left can overbid. Each deviation has to be shown both feasible (at least $\underline{w}$, which is where the standing assumption enters) and profitable against the employee's rule. A naive treatment that fixes the employee's choice only on the equilibrium path fails, because a firm's deviation could then be "punished" by an employee who chooses the worse offer. A treatment with strict tie-breaking fails too: when $v_a > v_s + b$ the acquirer would want the unattained infimum $v_s + b$, and no equilibrium would exist. Lemma 2 needs the same care with the startup's acceptance rule. There, the bid is not unique when $v_a < v_s$.

Formalization scope

All quantities are real numbers. The direct-hiring profile DHProfile consists of the two offers and a Bool-valued acceptance rule acceptA x y defined at every pair of offers $(x, y)$. The predicate IsDHEquilibrium requires:

• feasible, undominated offers: $\underline{w} \le w_a \le v_a$ and $\underline{w} \le w_s \le v_s$;
• an employee who is sequentially rational at every pair of offers, with the tie hers to break;
• offers that are best responses among all feasible offers.

The acquihiring profile AHProfile consists of the bid, the startup's acceptance rule at every bid, and the two post-bid wages. The predicate IsAHEquilibrium requires:

• cost-minimizing wages at the monopsony stage, which forces both wages to equal $\underline{w}$, as the page states in words;
• an optimal accept/decline decision at every bid;
• the undominated-bid cap $p \le v_a - w_a$;
• an optimal bid.

The standing assumption ($b > 0$ and $\min\{v_a, v_s\} > b + \underline{w}$) is a hypothesis of every theorem. Footnote 13 enters only through these caps. The other hypotheses added relative to the page are:

• the existence clauses that give "the continuation equilibrium" a meaning;
• in Lemma 2, the existence (rather than uniqueness) of the bid $v_a - \underline{w}$ when $v_a < v_s$.

The knife edges $v_a = v_s$ and $v_a = v_s + b$ are not covered by the page's case distinctions, and the corresponding clauses stay conditional on strict inequalities. Milestones 3–4 and the employee's preference hold at the knife edges as well and are stated without exclusions.

The payoffs are never defined by their closed forms ($\max\{0, v_a - v_s - b\}$ or $v_a - v_s$ as definitions would turn Proposition 1 into arithmetic), the standing assumption and the employee-preference clause are never dropped, and the declined bid $v_a - \underline{w}$ is never claimed unique.

All definitions live in AcquihiringMonopsony.Baseline.Model. The direct-hiring wage game, an asymmetric Bertrand contest for a single worker with a private benefit at one firm, is reusable for the other missions of this series. Contributions are welcome at every level: proofs of the two lemmas, of the payoff identities, and of the goal from them.

Selected references

• H. Bar-Isaac, J. P. Johnson, V. Nocke, Acquihiring for Monopsony Power, CRC TR 224 Discussion Paper No. 500, January 2024. https://www.crctr224.de (Discussion Papers)
• H. Bar-Isaac, J. P. Johnson, V. Nocke, Acquihiring for Monopsony Power, Management Science, 2025. https://doi.org/10.1287/mnsc.2024.04604
• A. K. Chatterji, A. Patro, Dynamic Capabilities and Managing Human Capital, Academy of Management Perspectives 28(4), 2014, 395–408.