Algorithmic Game Theory

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.

Why streaming revenue is a cooperative-game question

Music streaming platforms collect a subscription fee from each user and have to pass the revenue on to the artists whose content was played. The two rules used in practice are pro-rata (each artist is paid in proportion to their total number of streams, over all users) and user-centric (each user's fee is split among the artists that user played, in proportion to that user's streams). Which rule is fair has been debated by platforms, rights holders and regulators. Bergantiños and Moreno-Ternero (arXiv:2310.11861, Management Science, 2025) study the problem axiomatically, and in their §4 also through cooperative game theory: they associate a transferable-utility game with every streaming problem and ask which revenue allocations no coalition of artists could object to.

This mission formalizes their Theorem 2. It gives an explicit description of the core of that game.

Setting

There are $n$ artists $N=\{1,\dots,n\}$ and a finite set $M$ of users, each of whom pays $1$, so $m=|M|$ is to be shared. A streaming problem records the number $t_{ij}\in\mathbb N$ of times user $j$ played artist $i$. Every user in $M$ is assumed to have played at least one artist.

• The list of user $j$ is $L^j=\{i\in N:t_{ij}>0\}$, the artists that user played.
• The streaming game gives a coalition $S\subseteq N$ of artists the fees of the users who played only artists in $S$:

$$v(S)=\bigl|\{j\in M: L^j\subseteq S\}\bigr|.$$

This is a pessimistic estimate of what a group of artists could earn by leaving to found its own platform. Because every list is nonempty, $v(\emptyset)=0$.

• The core of $v$ is the set of payoff vectors $x\in\mathbb R^N$ that distribute exactly $v(N)=m$ and give every coalition at least its worth:

$$C(N,v)=\Bigl\{x:\ \sum_{i\in N}x_i=v(N),\ \sum_{i\in S}x_i\ge v(S)\ \text{for all } S\subseteq N\Bigr\}.$$

• The allocation set $A(N,M,t)$ consists of the vectors $x=\sum_{j\in M}x^j$, where each $x^j\in\mathbb R^N$ is nonnegative, vanishes outside $L^j$, and sums to $1$. Each user's fee is split in any way among the artists that user played, and the shares are added up.

The proof goes through two classical objects of cooperative game theory. The Harsanyi dividends are $\Delta_v(R)=\sum_{S\subseteq R}(-1)^{|R|-|S|}v(S)$. A sharing system $p=(p^R)_{\emptyset\ne R\subseteq N}$ assigns to each nonempty coalition $R$ a probability vector $p^R$ supported on $R$. The Harsanyi set $H(N,v)$ is the set of allocations $y^p_i=\sum_{R\ni i}\Delta_v(R)\,p^R_i$ that a sharing system induces. The unanimity game $u_R$ has $u_R(S)=1$ if $R\subseteq S$ and $0$ otherwise.

Formalization targets

Goal: Theorem 2 (p. 14)

$$C(N,v)=A(N,M,t)\qquad\text{for every streaming problem }(N,M,t).$$

Milestones (the proof in the paper's appendix, pp. 22–23)

1. Harsanyi (1959). For every TU game, $v=\sum_{\emptyset\ne R\subseteq N}\Delta_v(R)\,u_R$, and these weights are unique.
2. Vasil'ev (1981). If $\Delta_v(R)\ge 0$ for every nonempty $R$, then $C(N,v)=H(N,v)$.
3. The streaming game decomposes as $v=\sum_{\emptyset\ne R\subseteq N}|\{j\in M:L^j=R\}|\,u_R$.
4. Its dividends are $\Delta_v(R)=|\{j\in M:L^j=R\}|\ge 0$.
5. $H(N,v)\subseteq A(N,M,t)$.
6. $A(N,M,t)\subseteq H(N,v)$.
7. Companion (§4, p. 13): $v$ is a convex (supermodular) game.

Significance

Theorem 2 says that the core-stable allocations of streaming revenue are exactly those that split each user's fee among the artists that user played. The user-centric rule is such a split, so its rewards always lie in the core. The pro-rata rule can fall outside the core: in the paper's Example 1 a coalition of one artist receives less than the fee of the user who played only that artist. This observation underlies the paper's Theorem 3, where core selection together with homogeneity and additivity characterizes the user-centric index. Beyond streaming, the theorem gives an explicit core for a class of games built from users' lists. The museum-pass games of Ginsburg and Zang have the same structure.

The paper's proof combines two cited classical theorems (Harsanyi's unanimity decomposition and Vasil'ev's identification of core and Harsanyi set for games with nonnegative dividends) with bookkeeping specific to streaming. None of these is formalized on the platform except the bare existence of a unanimity decomposition (Young 1985's exists_unanimity_expansion, Proved, referenced here). The mission therefore produces reusable statements of Harsanyi dividends, the Harsanyi set and Vasil'ev's theorem for arbitrary finite TU games, as well as the streaming result itself.

Difficulty

Most of the mission is finite bookkeeping: Möbius inversion over the subset lattice and regrouping sums by users' lists. The central difficulty is the inclusion $C(N,v)\subseteq H(N,v)$ in Vasil'ev's theorem. One has to show that every core vector can be generated by splitting each dividend among the members of its coalition. This is a feasibility statement for a transportation problem whose supplies are the dividends and whose demands are the core payoffs, with each coalition allowed to ship only to its own members. The core inequalities have to be turned into such a shipment plan, and neither of the obvious candidates does that. Splitting each dividend equally among a coalition's members gives the Shapley value, a single point. Taking extreme points of the core gives the marginal vectors, and writing an arbitrary core point through them is the same feasibility question again. The paper cites the result without proof.

Formalization scope

• Artists and users. Artists are Fin n, numbered from $0$. Users are named by natural numbers. A problem is a finitely supported map t : ℕ →₀ (Fin n → ℕ) with t j i $=t_{ij}$; the user set $M$ is its support. Every user in $M$ therefore has a nonempty list, which is the paper's standing assumption $L^j\ne\emptyset$ (recalled on p. 19). Streams are natural numbers. The empty problem is allowed; there both sides of Theorem 2 are $\{0\}$.
• Inclusions. The paper's $\subset$ is read as $\subseteq$ throughout: $R=N$ is a coalition, and $S=\emptyset$ and $S=N$ are core constraints.
• Vectors. Payoff vectors are Fin n → ℝ. The core is the published Supermodularity.Cooperative.Core Finset.univ. Convexity is the published Supermodularity.Cooperative.IsConvexGame. The unanimity game is the published MonotonicSolutions.StrongMono.unanimity.
• Dividends. The paper defines the dividends implicitly, as the unique weights of the unanimity decomposition. The formalization uses the explicit formula $\Delta_v(R)=\sum_{S\subseteq R}(-1)^{|R|-|S|}v(S)$, and milestone 1 states that it gives those unique weights. A sharing system is a function on all coalitions whose value at $\emptyset$ is never read.
• No trivialization. The allocation set is the set of sums of user-indexed probability vectors supported on the users' lists. It is not the larger set "$x\ge 0$, $\sum_i x_i=m$", which would make Theorem 2 false. Theorem 2 is stated directly as a set equality between the core and the allocation set, not through the Harsanyi set. Vasil'ev's theorem is stated for every TU game with nonnegative dividends, as cited.
• Reusable parts. The Harsanyi dividend, sharing systems, the Harsanyi set, Harsanyi's uniqueness theorem and Vasil'ev's theorem apply to any finite TU game. Proofs of these, especially of Vasil'ev's inclusion $C\subseteq H$, are the most valuable contributions. The streaming steps (milestones 3 to 6) are welcome as independent footholds.
• The same streaming objects are restated in the sibling missions Revenue Sharing at Music Streaming Platforms I and III.

Selected references

• G. Bergantiños, J. D. Moreno-Ternero, Revenue sharing at music streaming platforms, Management Science, 2025; preprint arXiv:2310.11861v1, 2023. https://arxiv.org/abs/2310.11861
• J. C. Harsanyi, A bargaining model for the cooperative n-person game, in Contributions to the Theory of Games IV, Annals of Mathematics Studies 40, Princeton University Press, 1959.
• V. A. Vasil'ev, On a class of imputations in cooperative games, Soviet Mathematics Doklady 23 (1981), 53–57.
• R. van den Brink, G. van der Laan, V. Vasil'ev, Constrained core solutions for totally positive games with ordered players, International Journal of Game Theory, 2014 (the presentation of the Harsanyi set the paper follows, footnote 22).
• H. P. Young, Monotonic solutions of cooperative games, International Journal of Game Theory 14 (1985), 65–72. https://doi.org/10.1007/BF01769885

Motivation

Learning dynamics in games describe how players who repeatedly interact adjust their strategies from observed payoffs. A central question is whether such dynamics lead to Nash equilibrium. For the replicator dynamics, the canonical model of evolutionary game theory, the answer is negative in general: in Matching Pennies and in generic zero-sum games with a unique interior equilibrium, replicator trajectories cycle forever. A classical positive result survives: if a replicator trajectory of a 2-player game stays a bounded distance away from the boundary of the strategy space, its time average converges to the Nash set (Hofbauer and Sigmund, 1998, Ch. 7).

Mertikopoulos and Sandholm (arXiv:1407.6267v2; Math. Oper. Res. 41(4), 2016) study a broad family of continuous-time learning dynamics, regularized reinforcement learning: each player aggregates payoffs into scores and plays the mixed strategy that maximizes score minus a strongly convex penalty function. The family contains the replicator dynamics (entropic penalty) and the projection dynamics (quadratic penalty). For non-steep penalties, trajectories can enter and leave the boundary of the strategy space infinitely often, so the classical "stay away from the boundary" criterion is no longer natural. Section 6 of the paper replaces it with a condition on scores and derives convergence of time averages in zero-sum games with an interior equilibrium.

Setting

A 2-player finite game $\mathcal G$ has players $k = 1, 2$, finite pure strategy sets $\mathcal A_k$, and payoff functions $u_k$ on pure profiles. A mixed strategy $x_k$ is a probability vector on $\mathcal A_k$; $\mathcal X$ is the set of mixed profiles $x = (x_1, x_2)$ and $u_k(x)$ the expected payoff (2.1). The payoff vector of player $k$ is $v_{k\alpha}(x) = u_k(\alpha; x_{-k})$, the payoff of the pure strategy $\alpha$ against the opponent's mixed strategy (2.2). A profile $x^*$ is a Nash equilibrium if no player gains by a unilateral deviation to another mixed strategy; it is interior if $x^*_{k\alpha} > 0$ for every $k$ and $\alpha$. The game is zero-sum if $u_1 = -u_2$.

On the simplex $\Delta$ of a finite set, a penalty function $h$ (Definition 2.1) is continuous on $\Delta$, smooth on the relative interior of every face, and $K$-strongly convex for some $K > 0$:

$$h(tx_1 + (1-t)x_2) \le t h(x_1) + (1-t) h(x_2) - \tfrac12 K t(1-t)\|x_1 - x_2\|^2 .$$

No steepness is required. The choice map is $Q(y) = \arg\max_{x\in\Delta}\{\langle y|x\rangle - h(x)\}$ (Definition 2.2), the convex conjugate is $h^*(y) = \max_{x\in\Delta}\{\langle y|x\rangle - h(x)\}$ (C.1), and the Fenchel coupling is $F_h(p, y) = h(p) + h^*(y) - \langle y|p\rangle$ (C.10).

Each player $k$ has its own penalty function $h_k$. An orbit of (RL) is a pair of trajectories $(y(t), x(t))$, $t \ge 0$, of score vectors and mixed profiles with

$$\dot y_k(t) = v_k(x(t)), \qquad x_k(t) = Q_k(y_k(t)) .$$

The time average of the orbit is $\bar x(t) = t^{-1}\int_0^t x(s)\,ds$.

Formalization targets

Goal: Proposition 6.2 (p. 26)

If $\mathcal G$ is a 2-player zero-sum game with an interior Nash equilibrium, then for every orbit of (RL),

$$\operatorname{dist}\big(\bar x(t), \mathrm{NE}(\mathcal G)\big) \xrightarrow[t\to\infty]{} 0 .$$

The statement fixes no rate and no particular penalty function: it holds for every choice of $h_1, h_2$.

Milestones

1. Proposition C.1 (p. 33): $Q$ is Lipschitz and $Q = dh^*$.
2. Lemma C.6 (p. 36): along (RL), $\frac{d}{dt}F_{h_k}(p_k, y_k(t)) = \langle v_k(x(t)) | x_k(t) - p_k\rangle$.
3. (6.5) (p. 26): in the goal's setting, $F_h(x^*, y(t)) = \sum_k F_{h_k}(x_k^*, y_k(t))$ is constant.
4. Proposition A.1(iii) (p. 31): $Q_\alpha(y) \to 0$ when $y_\alpha - y_\beta \to -\infty$.
5. Proposition C.5 (pp. 35–36): for interior $p$, bounded $F_h(p, y_j)$ forces bounded score differences.
6. Theorem 6.1 (p. 25): in any 2-player game, bounded score differences imply convergence of $\bar x(t)$ to the Nash set.

Significance

The result. Proposition 6.2 shows that the time-average convergence known for the replicator dynamics in zero-sum games is a property of the whole class of regularized reinforcement learning schemes, including those whose trajectories hit the boundary of the strategy space infinitely often, such as the projection dynamics. Time-averaged play of no-regret-type dynamics in zero-sum games is the continuous-time counterpart of the standard argument that averaged learning computes minimax strategies. Theorem 6.1 isolates the mechanism for general 2-player games: bounded score differences suffice, with no zero-sum assumption.

Formalizing it. The results are proved in the paper; none has a machine-checked proof. A complete formalization produces reusable components: differentiability of the conjugate of a strongly convex function on the simplex (a Danskin-type statement), the Fenchel-coupling identity along the dynamics, and a conservation law for zero-sum games. These are the building blocks of many analyses of mirror-descent and follow-the-regularized-leader dynamics.

Difficulty

The first idea, comparing $x(t)$ itself with the equilibrium, fails: $x(t)$ need not converge, and for non-steep penalties it does not stay in the interior, so the Kullback–Leibler argument used for the replicator dynamics is unavailable. The conserved quantity is a function of the scores $y(t)$, not of $x(t)$, and turning its boundedness into control of score differences requires the asymptotic behaviour of the choice map when some scores diverge. The second difficulty is analytic: $h$ is not differentiable at the boundary of $\Delta$, yet $h^*$ must be differentiable everywhere on the score space, with derivative $Q$, for the chain rule along (RL) to apply. Finally, the passage from score differences to the time average uses that $v_k$ is linear in the single opponent's strategy, which is specific to two players.

Formalization scope

• Game. Players are Fin 2, strategy types A k are finite, payoffs are real functions on pure profiles; mixed profiles, expected payoffs and mixed Nash equilibria come from the published agt_games vocabulary (AGT.IsMixedNash). Zero-sum is $u_0(s) + u_1(s) = 0$ for every pure profile; interiority is $x^*_{k\alpha} > 0$.
• Penalty functions. IsPenalty h K is Definition 2.1 with strong convexity in the Euclidean norm; since $K$ is existential the class does not depend on the norm. Steepness is not assumed. Each player has its own $h_k$.
• Choice map and orbits. $x = Q(y)$ is the predicate IsChoice h y x (maximizer of $\langle y|x\rangle - h(x)$ over $\Delta$), never a chosen argmax. An orbit is IsRLOrbit u h y x: for $t \ge 0$, $x_k(t) = Q_k(y_k(t))$ and $\dot y_{k\alpha}(t) = v_{k\alpha}(x(t))$, a right derivative at $t = 0$. This differential form is equivalent to the integral form (RL) because $x$ is continuous along an orbit.
• Time average and convergence. $\bar x(t)$ is defined coordinatewise with the interval integral; only $t \to \infty$ is used. Convergence to the Nash set is Metric.infDist $\to 0$ in the sup metric on profiles. For Theorem 6.1, which has no equilibrium among its hypotheses, the conclusion also asserts that the Nash set is nonempty, because the distance to the empty set is $0$ in Lean.
• Ruled out. A chosen argmax for $Q$, orbits that are vacuous, steepness added to the penalty, convergence of a subsequence or a liminf in place of the limit, and a Nash set that may be empty are all excluded by the encoding. A sorry-free check exhibits a game, penalty functions and an orbit satisfying all hypotheses of the goal, and verifies that Matching Pennies has the interior equilibrium $((\tfrac12,\tfrac12),(\tfrac12,\tfrac12))$.
• Not included. Theorem 6.3 (chain transitivity under the best-response dynamics) depends on the theory of perturbed solutions of differential inclusions, which is not available. Proposition 6.4 is omitted (see the mission notes).

Contributions are welcome on any milestone; Proposition C.1 and Proposition A.1(iii) are self-contained convex-analysis statements about a single penalty function.

Selected references

• P. Mertikopoulos and W. H. Sandholm, Learning in games via reinforcement and regularization, Mathematics of Operations Research 41(4), 2016. Preprint arXiv:1407.6267v2 (cited version). https://arxiv.org/abs/1407.6267
• J. Hofbauer and K. Sigmund, Evolutionary Games and Population Dynamics, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9781139173179
• J. Hofbauer, S. Sorin and Y. Viossat, Time average replicator and best-reply dynamics, Mathematics of Operations Research 34(2), 2009. https://doi.org/10.1287/moor.1080.0359
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

A basic test of any model of learning in games is whether it respects strict dominance: a strategy that does worse than another against every behaviour of the opponents should eventually be abandoned, and, after it is gone, so should every strategy that becomes dominated in what remains. For the replicator dynamics of evolutionary game theory this is classical: elimination of dominated and iteratively dominated strategies goes back to Akin (1980), Nachbar (1990) and Samuelson and Zhang (1992), whose notion of extinction of a mixed strategy is the one used here; Weibull (1995) gives the textbook account, including a conditional result for weakly dominated strategies.

The replicator dynamics are the continuous-time limit of exponential weights (the logit choice rule), one member of a large family of learning schemes in which every player accumulates the payoffs of their strategies into a score and turns scores into mixed strategies by a regularized best response. Different regularizers give different dynamics: the Gibbs entropy gives the replicator dynamics, the Euclidean square gives the projection dynamics, and many others are used in online optimization. Mertikopoulos and Sandholm (arXiv:1407.6267, Mathematics of Operations Research 41(4), 2016) analyse this whole family in a single framework. In particular they do not assume that the regularizer is steep, so play can reach the boundary of the simplex in finite time and the induced dynamics on the simplex can fail to be well-posed. Their first rationality result is that every iteratively dominated strategy becomes extinct under every scheme of the family.

Setting

A finite game has a finite set of players $\mathcal N$, a finite set $\mathcal A_k$ of pure strategies for each player $k$, and payoffs $u_k:\prod_\ell\mathcal A_\ell\to\mathbb R$. A mixed strategy of player $k$ is a point $x_k$ of the simplex $\mathcal X_k=\Delta(\mathcal A_k)$, and $u_k(x)$ is the expected payoff (2.1) at a mixed profile $x=(x_k)_k$. The payoff vector of player $k$ is $v_k(x)=(v_{k\alpha}(x))_{\alpha\in\mathcal A_k}$, where $v_{k\alpha}(x)=u_k(\alpha;x_{-k})$ is the payoff of the pure strategy $\alpha$ against $x_{-k}$.

A penalty function on a simplex $\Delta$ (Definition 2.1) is a function $h:\Delta\to\mathbb R$ that is continuous, smooth on the relative interior of every face of $\Delta$, and strongly convex with some constant $K>0$:

$$h(tx_1+(1-t)x_2)\le t\,h(x_1)+(1-t)\,h(x_2)-\tfrac12K\,t(1-t)\,\|x_1-x_2\|^2 .$$

Its choice map is $Q(y)=\arg\max_{x\in\Delta}\{\langle y|x\rangle-h(x)\}$ (Definition 2.2). Each player $k$ has a penalty function $h_k$ and choice map $Q_k$. The reinforcement learning dynamics are

$$\dot y_k=v_k(x),\qquad x_k=Q_k(y_k),\qquad\text{(RL)}$$

so that $y_k(t)$ is the cumulative payoff of player $k$'s pure strategies and $x(t)=Q(y(t))$ is the resulting play. Strategy $p_k$ is dominated by $p'_k$, written $p_k\prec p'_k$, if $u_k(p_k;x_{-k})<u_k(p'_k;x_{-k})$ for all $x$ (4.1). Removing dominated strategies and repeating gives the iteratively dominated strategies. A mixed strategy $p_k$ becomes extinct along $x(t)$ if $\min\{x_{k\alpha}(t):\alpha\in\operatorname{supp}(p_k)\}\to0$.

The analysis runs through the Fenchel coupling $F_h(p,y)=h(p)+h^*(y)-\langle y|p\rangle$, where $h^*(y)=\max_{x\in\Delta}\{\langle y|x\rangle-h(x)\}$, and the Bregman divergence $D_h(p,x)=h(p)-h(x)-h'(x;p-x)$, defined with the one-sided directional derivative so that it makes sense at boundary points where $h$ has no gradient.

Formalization targets

Goal: Theorem 4.1

For every orbit $x(t)=Q(y(t))$ of (RL), every player $k$, and every mixed strategy $p_k$ that is dominated, possibly only after some rounds of elimination,

$$\lim_{t\to\infty}\ \min\{x_{k\alpha}(t):\alpha\in\operatorname{supp}(p_k)\}=0 .$$

The penalty functions are arbitrary in the sense of Definition 2.1, including non-steep ones, and may differ across players.

Milestones

1. Proposition C.3: $F_h(p,y)\ge\tfrac12K\|Q(y)-p\|^2$, hence $F_h\ge0$, and $F_h(p,y_j)\to0$ iff $Q(y_j)\to p$.
2. (4.6)–(4.8): if $p_k\prec p'_k$ with payoff gap at least $\delta$, then $F_k(p_k,y_k(t))\ge V_k(y_k(0))+\delta t$.
3. Proposition C.2 (i)–(iii): $D_h(p,\cdot)$ is finite, at least $\tfrac12K\|x-p\|^2$, and continuous on $\Delta_p=\{x\in\Delta:x_\alpha>0\text{ whenever }p_\alpha>0\}$.
4. (C.11): $F_h(p,y)=D_h(p,Q(y))$ whenever $Q(y)\in\Delta_p$.
5. Proposition C.4: if $F_h(p,y_j)\to+\infty$, then $Q(y_j)$ has no limit point in $\Delta_p$.
6. Theorem 4.1 for strategies dominated in the original game.

Two companion statements extend the goal: Proposition 4.2, the rate $x_{k\alpha}(t)\le\varphi_k(c_k-\gamma_k\delta_kt)$ under the rescaled dynamics (RLγ) with decomposable penalties, which gives extinction in finite time when the kernel is not steep at $0$; and Proposition 4.3, a conditional extinction result for weakly dominated strategies.

Significance

The theorem shows that elimination of iteratively dominated strategies is a property of the whole class of regularized reinforcement learning schemes, not only of exponential weights. It is also unilateral: a player who follows (RL) stops playing dominated strategies whatever the other players do (Remark 4.2). The proof does not use the dynamics induced on the simplex, which need not be well-posed for non-steep regularizers; it works with the scores in the dual space. Proposition 4.2 then shows that the regularizer sets the speed of elimination: exponential for the entropy, finite time for the Euclidean square.

The result is proved in the paper; nothing here is open. No part of it is formalized. The mission produces the paper's convex-analytic toolkit for penalty functions on a simplex (Fenchel coupling, the one-sided Bregman divergence, their comparison with the Euclidean distance) and a machine-checked proof of the elimination theorem on top of it. The same toolkit is used by the paper's results on strict equilibria and zero-sum games.

Difficulty

The familiar argument for the replicator dynamics shows that the Kullback–Leibler divergence $D_{KL}(p_k,x_k(t))$ diverges. For a general penalty function the analogous Bregman divergence uses $dh(x)$, which does not exist at boundary points, and non-steep dynamics spend time on the boundary. The proof therefore tracks the Fenchel coupling $F_k(p_k,y_k(t))$, whose growth is easy to bound, and must convert its divergence into extinction. That conversion (Propositions C.2–C.4) needs continuity of the one-sided Bregman divergence on $\Delta_p$, including at points of lower-dimensional faces, and a compactness argument that turns "no limit point in $\Delta_p$" into a statement about every time sequence. The iterated case adds an induction in which the payoff gap is only positive on the surviving profiles, so the trajectory's distance to those profiles must be controlled.

Formalization scope

Lean conventions:

• Players form a Fintype ι; strategies are Fintype (A k); payoffs are u : ι → (∀ k, A k) → ℝ. Mixed strategies, mixed profiles and expected payoffs are those of the published agt_games definition.
• A penalty function is IsPenalty h K: continuity on the simplex, $C^\infty$ along smooth curves in the relative interior of a face (footnote 5), and (2.5) with the Euclidean norm. Steepness is not assumed.
• The choice map is the predicate IsChoice h y x ($x$ maximizes $\langle y|\cdot\rangle-h$ on the simplex), never a chosen maximizer.
• An orbit of (RL) is a pair of trajectories $(y,x)$ with $x_k(t)=Q_k(y_k(t))$ and $\dot y_{k\alpha}(t)=v_{k\alpha}(x(t))$ for $t\ge0$ (right derivative at $0$). This is the differential form of the paper's integral equation and is equivalent to it along continuous orbits.
• Iterated dominance eliminates pure strategies round by round, each time removing those strictly dominated by a mixed strategy supported on the survivors, against profiles supported on the survivors. A mixed strategy is iteratively dominated when it is dominated in this sense at some round.
• Extinction is stated as a limit: for every $\varepsilon>0$ there is $T$ such that for every $t\ge T$ some $\alpha\in\operatorname{supp}(p_k)$ has $x_{k\alpha}(t)<\varepsilon$.
• The one-sided Bregman divergence is handled through a predicate asserting that the one-sided derivative is a given real number. The value $+\infty$ is never encoded as a real number.

Trivializing formalizations are ruled out. Orbits are not vacuous: a sorry-free check exhibits an explicit orbit of a game with a strictly dominated action, under the quadratic penalty. The choice map is not a junk argmax. Steepness, which would keep play interior, is not added. Extinction is not weakened to a $\liminf$.

Needed infrastructure: properties of strongly convex functions on a simplex, the conjugate and its maximizers, one-sided derivatives of convex functions along segments, and compactness of the product of simplices. Most of this is reusable beyond the mission. Contributions are welcome on the Appendix-C lemmas, which are independent of the game, as well as on the goal.

Selected references

• P. Mertikopoulos and W. H. Sandholm, Learning in games via reinforcement and regularization, Mathematics of Operations Research 41(4), 2016; preprint arXiv:1407.6267v2. https://arxiv.org/abs/1407.6267
• E. Akin, Domination or equilibrium, Mathematical Biosciences 50, 239–250, 1980.
• J. H. Nachbar, Evolutionary selection dynamics in games, International Journal of Game Theory 19, 59–89, 1990.
• L. Samuelson and J. Zhang, Evolutionary stability in asymmetric games, Journal of Economic Theory 57, 363–391, 1992.
• J. W. Weibull, Evolutionary Game Theory, MIT Press, 1995.
• K. C. Kiwiel, Free-steering relaxation methods for problems with strictly convex costs and linear constraints, Mathematics of Operations Research 22(2), 326–349, 1997.