Algorithmic Game Theory

Motivation

The classical secretary problem asks how to select one valuable candidate when candidates arrive in random order and a decision must be made when each candidate appears. Many allocation settings have several goods of unequal quality instead of a single position. An employer may have roles of different desirability, or a seller may have placements with different visibility. In the weighted secretary problem, an agent's value is multiplied by the weight of the good assigned to that agent. The algorithm must decide irrevocably as agents arrive, while the benchmark sees every value before assigning goods. Babaioff, Dinitz, Gupta, Immorlica and Talwar study this model with arbitrary fixed agent values and a uniformly random arrival order, and give a constant competitive ratio independent of the number of agents and goods (authors' version, §§2–3).

The paper also studies time discounts and matroid constraints. This mission concerns its weighted-goods result, Theorem 3.4. The result combines an online allocation rule for several comparably valuable agents with the familiar one-choice secretary rule for an unusually valuable agent. These are distinct ways in which the sorted offline assignment can earn value; both are present even when the weights are fixed in advance. The weighted model matters because matching a valuable agent to an unsuitable good can lose value despite accepting the right agent.

Setting

There are $n$ agents $e\in U$, each with a nonnegative value $v(e)$, and $K$ goods indexed in decreasing order of nonnegative weight:

An assignment $s$ gives each good to at most one agent, and each agent receives at most one good. A good may remain unassigned, represented by $\bot$ with $v(\bot)=0$. Its value is $\sum_{k=1}^K v(s(k))w(k)$. Agent values are arbitrary, not drawn independently from a distribution. The uncertainty is the arrival order $\pi$, chosen uniformly from all permutations; an agent's value becomes visible on arrival, and an allocation decision cannot be revised.

The offline optimum, $\mathrm{OPT}$, assigns the heaviest good to the highest-valued agent, the next good to the next agent, and so on. If $K>n$, the extra goods remain unassigned. A consistent tie break makes the ordering unique without changing the numerical value. This sorted assignment is defined directly; the mission does not replace it with an unconstrained variable said to be optimal.

The reservation algorithm draws a sample size $\tau\sim\mathrm{Binom}(n,1/2)$, observes the first $\tau$ agents without allocation, and retains the best $\min(K,\tau)$ sampled agents. Positive values are grouped into value classes $[2^{i-1},2^i)$ for integer $i$. A sampled agent in class $i$ reserves one good in that class's contiguous block, with higher classes receiving heavier blocks. A later agent receives the heaviest unassigned good reserved for its class when one is available. The classical secretary rule instead observes the first $\lfloor n/e\rfloor$ agents, then selects the first later arrival better than every predecessor; its winner receives good $1$.

Formalization targets

The mission's goal is the exact guarantee of Theorem 3.4 for Algorithm $A$, which runs the reservation algorithm with probability $8/(3e+8)$ and the classical rule with probability $3e/(3e+8)$:

Here the expectation covers the uniform arrival permutation, the independent binomial sample size used by the reservation branch, and the mixing coin. The multiplicative inequality expresses competitiveness even when an expected payoff is zero. It uses the explicit constant in the paper's proof rather than an instance-dependent or unspecified constant.

Four source results form the milestones. The classical secretary rule selects the maximum with probability at least $1/e$. Lemma 3.2 compares the starting indices $b_i$ and $o_i$ of class-$i$ blocks in the reservation and optimum assignments. Lemma 3.1 says that if the optimum assigns at least two agents from class $i$, the reservation rule assigns at least $u_i/4$ agents from that class in expectation. Lemma 3.3 converts this to expected value at least $\mathrm{OPT}_i/8$. The target retains the paper's class condition and both numerical fractions (authors' version, pp. 4–5).

Significance

Theorem 3.4 supplies a constant factor guarantee for irrevocable allocation when goods have different weights and agents arrive in random order. The factor does not grow with $n$ or $K$. It separates the effects of uncertain arrivals from the offline matching of high values to high weights, and it supplies a benchmark for later variants with more complicated feasibility constraints. The paper extends the reservation idea to additional combinatorial settings, including partition-matroid variants in Appendix C (authors' version, Appendix C).

The theorem is proved in the source paper, while the Lean statements in this mission are proof obligations. Formalizing them requires checking that the random-order model, sample distribution, tie convention and assignments jointly express the same algorithm. A complete development will also establish reusable finite-average facts for random permutations and binomial samples, and structural facts about sorted assignments and reserved blocks. Those pieces can support other secretary problems in the series; the mission's specific promise remains the weighted algorithm's exact bound.

Difficulty

A count of how many agents a class receives does not by itself control the weighted value of those goods. Goods have unequal weights, and the value of assigning the next good changes with its position in a block. A class whose offline optimum receives several agents can also lose all its sampled members from the allocation phase. Thus a direct comparison of expected class counts with expected class values is insufficient. The paper's separate count, block-position and value statements identify the claims a solver must establish; the final theorem must also account for classes represented only once in the offline assignment (authors' version, p. 5).

Formalization scope

Agents and goods are Fin n and Fin K; their indices start at zero in Lean, so paper time $t$ corresponds to Lean index $t-1$. An arrival permutation maps time to agent. Values and weights are real and explicitly nonnegative, and weights are antitone in the good index. The finite sums defining expectations are normalized by $n!$ for permutations and by $\binom n\tau/2^n$ for sample sizes. No measurability or integration convention is needed. For the goal, $K\ge1$ makes the heaviest good available; $K>n$ is allowed.

Equal values are ordered by smaller original agent index throughout the sorted optimum, the sample's top agents and the classical rule. The classical rule observes exactly $\lfloor n/e\rfloor$ arrivals, and zero-valued agents reserve no value-class goods. Positive values below one use negative integer class indices. The paper says only that class $i$ holds the values “between” $2^{i-1}$ and $2^i$ (p. 4, and again in Appendix C, p. 12); the mission fixes the half-open interval $[2^{i-1},2^i)$, so that the classes partition the positive reals (authors' version, pp. 4, 12). A reservation assignment is built from each post-sample agent's rank within its class, so a good is offered to at most one such agent. The theorem is about this concrete algorithm and the concrete sorted offline assignment; an arbitrary favorable policy or an optimum supplied as a hypothesis would not express the source result.

The development needs a finite assignment interface, a tie-aware rank order, value classes, the two online rules, and normalized finite expectations. The assignment and finite-average definitions are reusable. Contributions that prove the structural validity of the reservation assignment, the classical success guarantee, Lemmas 3.1–3.3, or the final combination all advance the stated target.

Selected references

• Moshe Babaioff, Michael Dinitz, Anupam Gupta, Nicole Immorlica and Kunal Talwar, Secretary Problems: Weights and Discounts, Proceedings of SODA 2009; authors' full version, proceedings DOI.

Motivation

Blackwell approachability is the vector-payoff analogue of von Neumann's minimax theorem. In a repeated game where each round's outcome is a vector $u(x_t, y_t) \in \mathbb R^d$, a player wants the running average of these vectors to converge to a target set $S$, whatever the opponent does. Blackwell (1956) showed when this is possible, and approachability has since become a standard tool for calibrated forecasting, regret minimization with respect to general benchmarks, and learning in games.

Online linear optimization (OLO) is the problem of choosing points $\theta_t$ in a fixed decision set $\mathcal K$ against a sequence of linear losses $\langle f_t, \cdot\rangle$, with performance measured by regret against the best fixed point in hindsight. Algorithms with regret $o(T)$ — "no-regret" algorithms such as online gradient descent (Zinkevich, 2003) — are among the most studied objects of machine learning.

Abernethy, Bartlett and Hazan (COLT 2011) showed that the two problems are algorithmically equivalent: each can be converted into the other with explicit control of the rates. This mission covers the direction from OLO to approachability.

Timeline:

• 1956: Blackwell proves the approachability theorem for convex sets, via a geometric projection strategy.
• 2003: Zinkevich introduces online gradient descent, a no-regret algorithm for any bounded convex decision set.
• 2009: Even-Dar, Kleinberg, Mannor and Mansour state approachability in the response-satisfiability form (as cited on p. 32 of the 2011 paper).
• 2011: Abernethy, Bartlett and Hazan give the two reductions, with explicit rates, and apply them to efficient calibration.

Setting

A Blackwell instance $(\mathcal X, \mathcal Y, u, S)$ consists of compact convex sets $\mathcal X \subseteq \mathbb R^n$, $\mathcal Y \subseteq \mathbb R^m$, a payoff $u : \mathcal X \times \mathcal Y \to \mathbb R^d$ that is affine in each argument (biaffine), and a closed convex target set $S \subseteq \mathbb R^d$. Write $\mathtt{dist}(z, U) = \inf_{w \in U}\|z - w\|$ for the Euclidean distance to a set, and $B_2(r)$ for the closed Euclidean ball of radius $r$.

A halfspace oracle takes a halfspace $H = \{z : \langle a, z\rangle \le c\}$ and returns a point $\mathcal O(H) \in \mathcal X$; it is valid if for every halfspace $H \supseteq S$, $u(\mathcal O(H), y) \in H$ for all $y \in \mathcal Y$.

A set $X \subseteq \mathbb R^d$ is a cone if $\alpha z \in X$ for all $z \in X$, $\alpha \ge 0$. For $K \subseteq \mathbb R^d$, $\mathtt{cone}(K) = \{\alpha x : \alpha \ge 0, x \in K\}$, and the polar cone of $C$ is $C^0 = \{\theta : \langle \theta, x\rangle \le 0 \ \forall x \in C\}$.

An OLO algorithm $\mathcal L$ maps past loss vectors $(f_1, \dots, f_{t-1})$ to a point $\theta_t \in \mathcal K$, and its regret is

Algorithm 2 runs $\mathcal L$ on $\mathcal K = S^0 \cap B_2(1)$ when $S$ is a cone: at round $t$ it sets $\theta_t = \mathcal L(f_1, \dots, f_{t-1})$, plays $x_t = \mathcal O(\{z : \langle \theta_t, z\rangle \le 0\})$, observes $y_t \in \mathcal Y$, and feeds $f_t = -u(x_t, y_t)$ back to $\mathcal L$.

When $S$ is compact but not a cone, it is lifted: with $\kappa = \max_{s\in S}\|s\|$ and $\kappa \oplus z \in \mathbb R^{d+1}$ the concatenation, put $u'(x, y) = \kappa \oplus u(x, y)$ and $S' = \mathtt{cone}(\{\kappa\} \times S)$, and run Algorithm 2 on $(\mathcal X, \mathcal Y, u', S')$.

Formalization targets

Goal: Corollary 18 (p. 39)

For a Blackwell instance with $S$ nonempty and compact, any valid halfspace oracle for the lifted instance, any OLO algorithm with values in $\mathcal K' = (S')^0 \cap B_2(1)$, any $T \ge 1$ and any $y_1, \dots, y_T \in \mathcal Y$, the run of Algorithm 2 on the lifted instance satisfies

The bound holds for every $T$ and every adversary, with no rate assumed for $\mathcal L$; a no-regret $\mathcal L$ then gives approachability.

Milestones

1. Lemma 13 (p. 35): for a nonempty convex cone $C$, $\mathtt{dist}(x, C) = \max_{\theta \in C^0 \cap B_2(1)} \langle \theta, x\rangle$.
2. Theorem 17 (p. 38): if $S$ is a cone, Algorithm 2 achieves $\mathtt{dist}\big(\frac1T\sum_t u(x_t,y_t), S\big) \le \mathrm{Regret}(\mathcal L_{\mathcal K}; f_{1:T})/T$.
3. Lemma 14 (p. 35): for nonempty compact convex $\mathcal K$, $\kappa = \max_{\mathcal K}\|\cdot\|$ and $x \notin \mathcal K$, $\mathtt{dist}(\kappa\oplus x, \mathtt{cone}(\{\kappa\}\times\mathcal K)) \le \mathtt{dist}(x, \mathcal K) \le 2\,\mathtt{dist}(\kappa\oplus x, \mathtt{cone}(\{\kappa\}\times\mathcal K))$.

Significance

The result. Corollary 18 turns any no-regret algorithm into an approachability strategy for a compact convex target, provided a valid halfspace oracle is available, with rate $2\,\mathrm{Regret}_T/T$. Combined with online gradient descent it gives an $O(1/\sqrt T)$ approachability rate, and through the choice of OLO algorithm it lets approachability inherit the computational efficiency of online learning. The paper uses this route to build an efficient calibrated forecaster (Section 5). Together with the converse reduction (Theorem 16), it shows that the two problems are equivalent.

Formalizing it. The results are proved in the paper; none of them has been machine-checked. Formalizing them requires the conic duality formula for distances (Lemma 13), a quantitative lifting lemma (Lemma 14) and the bookkeeping of an interactive protocol. The proof of Lemma 14 on the page is a sketch: it refers to an undefined point and uses a triangle-similarity argument, so a complete proof is new work.

Difficulty

The reduction's core is Lemma 13: the distance to a cone is a maximum of a linear function over the polar cone's unit ball. Lemma 13 needs projection onto a cone in Euclidean space; for a non-closed cone the projection may not exist, and the argument must go through the closure. The lifting Lemma 14 is a geometric statement whose page proof relies on a picture and an undefined point, so the factor 2 has no complete written argument. Finally, connecting the average lifted payoff to the lift of the average payoff, and the halfspace guarantee $\langle\theta_t, f_t\rangle \ge 0$ to the regret, requires keeping the round indexing and the oracle's validity domain exactly aligned.

Formalization scope

All spaces are EuclideanSpace ℝ (Fin d). The concatenation $\kappa\oplus z$ lives in EuclideanSpace ℝ (Fin (d+1)) with coordinate 0 equal to $\kappa$, so $\|\kappa\oplus z\|^2 = \kappa^2 + \|z\|^2$; a product type with the sup norm would change every distance and is ruled out. Distances are Metric.infDist. The polar cone uses the paper's sign ($\le 0$), the negative of Mathlib's innerDual. A halfspace is the pair $(a, c)$; a valid oracle must answer every halfspace containing $S$, including $a = 0$, not only the halfspaces the algorithm happens to query. The OLO algorithm is a map from histories Fin t → ℝᴰ with values in $S^0 \cap B_2(1)$ at every history. Rounds are $t = 1, \dots, T$, and the run of Algorithm 2 is given as hypotheses on sequences $\theta, x, f$, which exist and are unique by recursion. The minimum in the regret and $\kappa$ are written as sInf/sSup of images over nonempty compact sets, where they are attained.

Hypotheses added relative to the page: $S \neq \emptyset$ and $T \ge 1$ in the goal; $C \ne \emptyset$ in Lemma 13 (the empty set is a cone under Definition 11 and the identity fails for it); $\mathcal K \ne \emptyset$ in Lemma 14. Corrected misprints, each disclosed in the item's note: "$\mathrm{Regret}_T(\mathcal A)$" in Corollary 18 and (9) denotes the regret of the OLO algorithm $\mathcal L$ on the lifted losses; Lemma 14's "$\mathcal K \subseteq \mathcal H$" has a stray $\mathcal H$; $\kappa$ is the maximal norm of the set, not its diameter. The oracle in the goal is a valid oracle for the lifted instance, which is what applying Algorithm 2 to $(\mathcal X, \mathcal Y, u', S')$ requires.

A formalization in which the oracle is valid only at the run's own queries, the OLO algorithm is unconstrained, the regret's minimum ranges over all of $\mathbb R^{d+1}$, or the middle term of the goal is dropped, is a different statement and is ruled out.

The development needs: the dual formula for the distance to a convex cone, nearest-point projection onto closed convex sets (in Mathlib), compactness of polar-cone slices, and finite sums of biaffine payoffs. The cone layer (Lemma 13) is reusable for the converse direction of the paper and for conic duality generally. Proofs of any milestone, and of the bridge from an oracle for the original instance to one for the lifted instance, are welcome.

Selected references

• J. Abernethy, P. L. Bartlett, E. Hazan, Blackwell Approachability and No-Regret Learning are Equivalent, JMLR W&CP 19 (COLT 2011), pp. 27–46. https://proceedings.mlr.press/v19/abernethy11b.html
• D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6(1), 1956, pp. 1–8. https://doi.org/10.2140/pjm.1956.6.1
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf

Motivation

A correlated equilibrium is the equilibrium notion that arises when the players of a game take their actions on the advice of a common randomizing device, each player seeing only his own recommendation. It was introduced by Aumann in 1974 (Aumann 1974). Aumann's 1987 paper (Aumann 1987) gives the simple, finite form of the definition used today (Definition 2.1) and shows that the notion is what Bayesian rationality with a common prior predicts. On the way it records, as Proposition 2.3, the fact that makes correlated equilibrium tractable in practice: for a finite two-person game, the distributions over action pairs that come from correlated equilibria are exactly the solutions of an explicit finite system of linear inequalities.

That characterization is the starting point of the computational theory of correlated equilibria. Because the set is a polyhedron, an optimal correlated equilibrium can be found by linear programming, and no-swap-regret learning dynamics converge to this set (Foster and Vohra 1997; Hart and Mas-Colell 2000). In each of these works the linear-inequality description is taken as the definition; the paper's Proposition 2.3 is the bridge back to the strategic definition.

Setting

Player 1 has a finite set $S^1$ of actions and player 2 a finite set $S^2$. For $j \in S^1$ and $k \in S^2$, $h^1_{jk}$ and $h^2_{jk}$ are the two players' payoffs at the action pair $(j,k)$.

A correlated strategy pair is a pair of functions $f^1 : \Gamma \to S^1$, $f^2 : \Gamma \to S^2$ on a finite probability space $(\Gamma, \mu)$: a finite set $\Gamma$ with nonnegative weights $\mu(\gamma)$ summing to $1$. Chance draws $\gamma$ and suggests the action $f^i(\gamma)$ to player $i$. The pair is a correlated equilibrium (Definition 2.1, condition (2.2)) if no player gains by a deviation that depends only on his own suggestion: for every $\varphi : S^1 \to S^1$,

and the analogous inequality holds for player 2 and every $\psi : S^2 \to S^2$.

A distribution is a family $(p_{jk})_{j \in S^1, k \in S^2}$ with $p_{jk} \ge 0$ and $\sum_j \sum_k p_{jk} = 1$. The distribution of a correlated strategy pair assigns to $(j,k)$ the probability $\mu\{f^1 = j,\ f^2 = k\}$. A correlated equilibrium distribution (c.e.d.) is the distribution of some correlated equilibrium on some finite probability space.

In the Lean development these are IsDistribution p, IsProbVec μ, IsCE h₁ h₂ μ f₁ f₂, distr μ f₁ f₂ and IsCED h₁ h₂ p, with h₁ j k $= h^1_{jk}$ and p j k $= p_{jk}$.

Formalization targets

Goal: Proposition 2.3

For every distribution $(p_{jk})$: $(p_{jk})$ is a correlated equilibrium distribution if and only if

Milestones

1. Identification with distributions (Sect. 2, p. 4). A correlated strategy pair is a correlated equilibrium if and only if its distribution $p$ satisfies $\sum_j\sum_k p_{jk} h^1_{\varphi(j)k} \le \sum_j\sum_k p_{jk} h^1_{jk}$ for all $\varphi$, and the analogous condition for player 2.
2. Conditioning on possible suggestions (proof of Prop. 2.3, p. 6). For a distribution, player 1's condition holds if and only if $H^1(q \mid j) \le H^1(j \mid j)$ for every suggestion $j$ of positive probability and every $q$, where $H^1(q\mid j) = \sum_k h^1_{qk} p_{jk} / \sum_k p_{jk}$; likewise for player 2.
3. Player 1 gives (2.4): player 1's condition on $p$ is equivalent to (2.4).
4. Player 2 gives (2.5): player 2's condition on $p$ is equivalent to (2.5).

A further statement, not a milestone, records the paper's example on p. 5: in the game of chicken (Figure 4) the distribution of Figure 5 is a c.e.d. with expected payoff $(5,5)$.

Significance

The result. Proposition 2.3 turns an existential statement — there is some probability space and some correlated strategy pair that is an equilibrium and has distribution $p$ — into finitely many linear inequalities on $p$ alone. Consequently the set of c.e.d.'s is a compact convex polyhedron, membership is decidable by evaluating $|S^1|^2 + |S^2|^2$ linear forms, and optimizing a linear objective over it is a linear program. The paper states the two-person case and remarks that "the principle, however, is no different in the general case".

Formalizing it. The proposition is classical and its proof is short; to our knowledge it has no machine-checked proof. The platform already has the linear-inequality (swap) form of correlated equilibrium for two-player games on Fin m × Fin n (Foster–Vohra 1997 missions) and Aumann's 1974 randomizing-structure model, but no statement that connects the strategic definition over arbitrary finite probability spaces with the linear system. This mission supplies that connection, so that results proved about the polyhedron apply to equilibria in Aumann's sense and conversely.

Difficulty

The mathematics is elementary; the care is in the statement. Two points need attention. First, the direction from the inequalities to a c.e.d. requires constructing a probability space and a correlated strategy pair whose distribution is the given $p$; the c.e.d. notion quantifies over probability spaces, not over distributions. Second, the paper's argument divides by the probability $\sum_k p_{jk}$ of a suggestion, which may be zero; the conditional formulation (milestone 2) holds only over possible suggestions, while (2.4) and (2.5) quantify over all actions and hold trivially at impossible ones. Deviations must be functions of the player's own suggestion: restricting to constant deviations gives coarse correlated equilibrium, which (2.4)–(2.5) do not characterize, and allowing arbitrary functions of $\gamma$ gives a stronger notion.

Formalization scope

Two players with finite action types S₁ S₂ : Type* (Fintype, DecidableEq); payoffs h₁ h₂ : S₁ → S₂ → ℝ; distributions p : S₁ → S₂ → ℝ with the sign and sum conditions as an explicit hypothesis of every statement about distributions. Finite probability spaces are finite types Γ : Type with a probability vector μ : Γ → ℝ; deviations are compositions φ ∘ f₁ with φ : S₁ → S₁. The conditional payoffs $H^1$, $H^2$ use Lean's x / 0 = 0 and are only ever used at possible suggestions. Empty action sets admit no distribution, so the statements are then vacuous, exactly as in the paper.

A trivializing formalization is ruled out: "c.e.d." is the existential notion over finite probability spaces with a genuine probability vector and an equilibrium in the sense of Definition 2.1, not the inequalities themselves or the swap form on $p$.

No infrastructure beyond finite sums and Finset.filter is needed. Contributions welcome: proofs of the milestones, and the $n$-player generalization the paper alludes to.

Selected references

• R. J. Aumann, Correlated Equilibrium as an Expression of Bayesian Rationality, Econometrica 55 (1987), 1–18. https://doi.org/10.2307/1911154
• 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
• D. P. Foster and R. V. Vohra, Calibrated Learning and Correlated Equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
• S. Hart and 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

Online decision makers often have to choose an action before seeing the cost assigned to it. A no-regret algorithm performs almost as well, in total, as the best single action that could have been chosen after the costs were known. In a related repeated-game problem, Blackwell approachability asks a player to keep the average of vector payoffs close to a desired set despite an adversary's choices. These two performance criteria look different: one compares scalar costs to a fixed benchmark, while the other measures a geometric distance. Abernethy, Bartlett, and Hazan establish algorithmic reductions between them, with explicit finite-horizon bounds in their COLT 2011 paper. This mission isolates the direction that turns an approachability algorithm into an online linear optimization algorithm.

The bound matters even when the input algorithm has no known rate. It relates the regret of the resulting online algorithm to the actual distance attained on the corresponding sequence. Any subsequent guarantee on that distance then yields a regret guarantee through the same reduction. The paper also gives the reverse reduction and an application to calibrated forecasting; those are separate missions in this series.

Setting

Fix a dimension $d$ and a nonempty compact convex decision set $K\subseteq\mathbb R^d$. On round $t$, an algorithm selects $x_t\in K$ using only the preceding cost vectors $f_1,\ldots,f_{t-1}$. The adversary then reveals $f_t$ in the Euclidean unit ball $B_2(1)$. The incurred linear cost is $\langle f_t,x_t\rangle$. For a horizon $T$, regret compares these costs with the cost of the best single point of $K$ evaluated on all $T$ rounds:

The minimum exists because $K$ is nonempty and compact. No probabilistic model for the cost sequence is assumed. The round index begins at one, and $x_t$ cannot depend on $f_t$.

The reduction uses $\kappa=\max_{x\in K}\|x\|$, the maximum norm of a decision. Write $a\oplus x$ for Euclidean concatenation of a scalar and a vector, an element of $\mathbb R^{d+1}$. The generated cone of a set $M$ consists of its nonnegative scalar multiples, $\operatorname{cone}(M)=\{\alpha m:\alpha\ge0,\ m\in M\}$. For a set $C$, its polar cone is $C^0=\{\theta:\langle\theta,z\rangle\le0\text{ for every }z\in C\}$. This negative-sign convention is fixed throughout the mission.

Algorithm 1 of the paper constructs a vector-payoff game. Its player actions are $K$, its adversary actions are $B_2(1)$, its payoff and target are

A Blackwell approachability algorithm for this game chooses each $x_t$ from the preceding adversary moves. Its finite-horizon approachability rate on a given sequence is $D_T(A)=\operatorname{dist}(T^{-1}\sum_{t=1}^T u(x_t,f_t),S)$, where distance means the Euclidean distance from a point to a set. The online algorithm created by Algorithm 1 uses precisely the same choices $x_t$.

Formalization targets

The goal is Theorem 16 of the paper. For every admissible history-based algorithm, every sequence of unit-ball costs, and every $T\ge1$, it asserts

This is a statement about the rate actually obtained on the chosen cost sequence. It assumes no upper bound on $D_T(A)$ and does not require an oracle call in the statement. Thus it also covers algorithms whose behavior is specified directly rather than through an implementation of the oracle.

The milestone targets are the distance formula of Lemma 13, the conic distance identity in display (8) of Theorem 16's proof, and the existence of a valid halfspace oracle in Lemma 15. Lemma 13 says distance to a nonempty convex cone equals the attained maximum of a linear functional over the polar cone's unit ball. Display (8) specializes this geometry to Algorithm 1's lifted target. Lemma 15 says that every halfspace containing that target admits a player action whose payoff remains in the halfspace against every permitted adversary move. Together these statements specify the geometry and the oracle needed by the reduction.

Significance

Theorem 16 gives a numerical transfer rule: a bound on approachability distance for Algorithm 1's game immediately bounds average regret for the same sequence. Its factor depends only on the size $\kappa$ of the decision set. This permits comparison of algorithms in a common finite-horizon language, without replacing the online cost sequence by a distribution or an asymptotic limit. The source paper uses this direction as one half of its equivalence between approachability and no-regret learning Abernethy, Bartlett, and Hazan, 2011.

The mathematical results are established in that paper; the goal here is a machine-checked Lean development of their statements and eventually their proofs. The mission also supplies reusable definitions of generated and polar cones, a Euclidean lift, a finite-history online algorithm, and regret over a compact decision set. Lemma 13 is useful outside this reduction whenever distance to a cone is compared with linear functionals on its polar. The proposed theorem items currently carry open proofs, while their statements and definition files are checked for elaboration in the pinned Lean environment.

Difficulty

The main obstacle is the change of viewpoint from a scalar regret comparison to distance from a set of lifted vector payoffs. A direct comparison of individual round costs does not describe that distance. The target is a polar cone in one additional Euclidean dimension, so a faithful account must keep the lift's geometry, the cone's sign convention, and the normalization by $\kappa$ aligned. The distance formula also asserts that its maximum is attained. An encoding that merely writes an infimum or supremum with default values can silently make an edge case look valid without representing the paper's claim.

The oracle milestone has a separate quantifier demand. One selected action must work against every adversary move for each halfspace containing the target. It cannot be replaced by a possibly different action for each move, or by a claim only about tangent halfspaces. The theorem includes halfspaces with arbitrary offsets and zero normals because the source oracle accepts any containing halfspace.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d), and $a\oplus x$ lives in EuclideanSpace ℝ (Fin (d+1)) with the Euclidean norm. The generated cone uses exactly one nonnegative multiple of a point of the generating set, as in Definition 11. The polar uses $\langle\theta,z\rangle\le0$, the opposite sign from a positive dual-cone convention. Distances are Euclidean point-to-set distances. All arithmetic is over exact real numbers, and the regret minimum ranges over the image of the nonempty compact set $K$.

The statements require $\kappa>0$ because the source payoff divides by $\kappa$. This excludes the degenerate case $K=\{0\}$, in which the source instance is undefined. They require $T\ge1$ wherever an average is formed. Admissible histories consist of unit-ball adversary moves, and each round's decision belongs to $K$. The dimension may be zero syntactically, but the positive-$\kappa$ hypothesis excludes that case in results using Algorithm 1. These conditions keep the bound from being satisfied through Lean's default values for division by zero, distance to an empty set, or infima over empty sets.

The paper's display (8) writes $\operatorname{cone}(\kappa\oplus K)$ and labels its unit ball with dimension $d$; the formalization uses the cone of $\{\kappa\}\times K$ in $\mathbb R^{d+1}$, matching Algorithm 1. Lemma 12's printed bipolar claim omits closedness; this mission does not use that uncorrected sentence as a milestone. The oracle statement covers all containing halfspaces. Contributions are welcome for the distance identity, the oracle existence result, and the final regret inequality, as well as geometric lemmas supporting those proofs.

Selected references

• Jacob Abernethy, Peter L. Bartlett, and Elad Hazan, Blackwell Approachability and No-Regret Learning are Equivalent, Proceedings of the 24th Annual Conference on Learning Theory, JMLR Workshop and Conference Proceedings 19, 2011, pp. 27–46. Published paper.

Why zero-sum games belong in a linear programming course

A two-player zero-sum game models any situation in which one party's gain is exactly the other party's loss: a military allocation in the spirit of Colonel Blotto, a sealed-bid contest, rock–paper–scissors. The central question is what each player should do when the opponent is also reasoning about them. John von Neumann answered it in 1928 with the minimax theorem (von Neumann 1928): each player has a strategy guaranteeing the same number, the value of the game, whatever the opponent does. The theorem underlies modern game theory, robust decision making, and the analysis of online learning algorithms, where regret bounds are routinely derived from it.

Section 8.1 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) presents the theorem as an application of linear programming duality. This mission is the sixth of a series formalizing the capstone results of the book.

Setting

Alice has $m \ge 1$ pure strategies and Bob has $n \ge 1$. A real $m \times n$ payoff matrix $M = (m_{ij})$ records Alice's gain, and Bob's loss, when Alice plays her $i$th and Bob his $j$th pure strategy. A mixed strategy of Alice is a probability vector $\mathbf x \in \mathbb R^m$, $\sum_i x_i = 1$, $\mathbf x \ge \mathbf 0$; a mixed strategy of Bob is a probability vector $\mathbf y \in \mathbb R^n$. When the players randomize independently, Alice's expected payoff is

The worst-case payoffs are

over mixed strategies. A mixed strategy of Bob is a best response against $\mathbf x$ if it minimizes $\mathbf x^T M\mathbf y$; a mixed strategy of Alice is a best response against $\mathbf y$ if it maximizes it. A pair $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium (Definition 8.1.1) if each is a best response against the other. Alice's $\tilde{\mathbf x}$ is worst-case optimal if $\beta(\tilde{\mathbf x}) = \max_{\mathbf x} \beta(\mathbf x)$; Bob's $\tilde{\mathbf y}$ is worst-case optimal if $\alpha(\tilde{\mathbf y}) = \min_{\mathbf y}\alpha(\mathbf y)$.

The proof in the book passes through three linear programs: the dual of (8.1), which for a fixed $\mathbf x$ maximizes $x_0$ subject to $M^T \mathbf x - \mathbf 1 x_0 \ge \mathbf 0$; program (8.2), the same with $\mathbf x$ as variables subject to $\sum_i x_i = 1$, $\mathbf x \ge \mathbf 0$; and program (8.4), which minimizes $y_0$ subject to $M \mathbf y - \mathbf 1 y_0 \le \mathbf 0$, $\sum_j y_j = 1$, $\mathbf y \ge \mathbf 0$.

Formalization targets

Goal: Theorem 8.1.3 (minimax theorem for zero-sum games)

For every $m \times n$ payoff matrix with $m, n \ge 1$: worst-case optimal mixed strategies exist for both players; for any worst-case optimal $\tilde{\mathbf x}$ of Alice and $\tilde{\mathbf y}$ of Bob, the pair $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium; and there is a single number $v$, the value of the game, with

for every such pair. The third clause is what distinguishes the theorem from the existence of some saddle point.

Milestones

1. $\beta$ and $\alpha$ are attained minima and maxima (p. 135).
2. Lemma 8.1.2(i): $\beta(\mathbf x) \le \mathbf x^T M \mathbf y \le \alpha(\mathbf y)$ for all mixed $\mathbf x, \mathbf y$, hence $\max_{\mathbf x}\beta \le \min_{\mathbf y}\alpha$.
3. Lemma 8.1.2(ii): both strategies of a mixed Nash equilibrium are worst-case optimal.
4. Lemma 8.1.2(iii): $\beta(\tilde{\mathbf x}) = \alpha(\tilde{\mathbf y})$ implies that $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium.
5. The dual of (8.1) has optimal value $\beta(\mathbf x)$ (p. 137).
6. Eq. (8.3): an optimal solution $(\tilde x_0, \tilde{\mathbf x})$ of (8.2) satisfies $\tilde x_0 = \beta(\tilde{\mathbf x}) = \max_{\mathbf x}\beta(\mathbf x)$.
7. Eq. (8.5): an optimal solution $(\tilde y_0, \tilde{\mathbf y})$ of (8.4) satisfies $\tilde y_0 = \alpha(\tilde{\mathbf y}) = \min_{\mathbf y}\alpha(\mathbf y)$.
8. Programs (8.2) and (8.4) both have optimal solutions, and their optimum values coincide (p. 138).
9. The minimax equality (p. 137):

Significance

The theorem gives a complete prescription for zero-sum play: a worst-case optimal strategy secures at least the value against any opponent, and a worst-case optimal opponent holds the player to at most the value, so both players can announce their strategies in advance without loss. With Lemma 8.1.2(ii) it yields a characterization: a pair of mixed strategies is a Nash equilibrium if and only if both are worst-case optimal. The minimax equality is used downstream in online learning (regret-to-value arguments), in robust optimization, and in Yao's principle for randomized algorithms.

The mathematics is classical and proved; what this mission adds is a machine-checked version in the book's own formulation. The platform already has AGT.zero_sum_minimax (Algorithmic Game Theory I), which proves the existence of a saddle point, and the general FamousTheorems.sion_minimax_theorem. Neither states that every pair of worst-case optimal strategies is an equilibrium with a common value, and neither exhibits the LP route: the dual of (8.1), the programs (8.2) and (8.4), and their duality. The mission records that route statement by statement, so that it can be reused as a worked instance of LP duality.

Difficulty

Lemma 8.1.2 is routine; the entire content is the reverse inequality $\max_{\mathbf x}\beta(\mathbf x) \ge \min_{\mathbf y}\alpha(\mathbf y)$. The obvious attack, maximizing $\beta$ directly, fails because $\beta$ is a minimum of linear functions and hence not linear, so its maximization is not a linear program as written. The obstacle is removed only by an appeal to LP duality in the proof, together with the facts that the simplices are nonempty and compact, and that the relevant programs are feasible and bounded so that optima exist. None of this is supplied by the pure-strategy structure of the game: pure Nash equilibria need not exist (rock–paper–scissors has none).

Formalization scope

Pure strategies are indexed by Fin m and Fin n, with the book's standing assumption $m, n \ge 1$ carried as hypotheses 1 ≤ m, 1 ≤ n by every theorem; the book's indices $1,\dots,m$ become $0,\dots,m-1$. Mixed strategies are Mathlib's stdSimplex ℝ (Fin m), the payoff is x ⬝ᵥ (M *ᵥ y). $\beta(\mathbf x)$ is the real sInf and $\alpha(\mathbf y)$ the real sSup of the payoffs over the opponent's simplex; milestone 1 states that these are attained. A mixed Nash equilibrium is defined in the verbal form of Definition 8.1.1 (mutual best responses). Worst-case optimality is defined against all mixed strategies, never as a saddle-point condition, so the goal is not circular with Lemma 8.1.2(iii). LP optimality is stated as "feasible and at least as good as every feasible point", so no supremum over a possibly empty or unbounded feasible set is used.

The book's clause that worst-case optimal strategies "can be efficiently computed by linear programming" is algorithmic and is not part of the formal statement; there is no complexity model. A goal asserting only the existence of worst-case optimal strategies, or only the existence of some equilibrium, would drop the theorem's third clause and is ruled out: the common value $v$ is quantified before all pairs of worst-case optimal strategies.

A complete development needs compactness of the standard simplex, continuity of the bilinear payoff, and a strong duality theorem for linear programs in the form of the programs (8.2)/(8.4); the latter is reusable across the whole series. Proofs by other routes (Sion's theorem, a separating hyperplane argument, fixed points) are welcome for the goal; the LP milestones stand on their own as statements about the programs.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.1, pp. 131–142. https://doi.org/10.1007/978-3-540-30717-4
• J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847
• M. Sion, "On general minimax theorems", Pacific Journal of Mathematics 8 (1958), 171–176. https://doi.org/10.2140/pjm.1958.8.171

Motivation

Classical Bayesian mechanism design assumes that the designer knows the agents' beliefs about each other: typically a commonly known prior over independent private values. Wilson's critique (1987) observed that mechanisms tuned to such a prior can depend on details that no designer knows, and a literature on robust mechanism design replaced the fixed prior by a large family of possible beliefs. Chapter 10 of Börgers, An Introduction to the Theory of Mechanism Design (OUP 2015), develops this programme in the framework of Bergemann and Morris (2001, 2005): agents' information is described by a type space, the designer is uncertain which beliefs agents hold, and mechanisms are compared across all type profiles at once.

Timeline of the results formalized here:

• 1980: Hylland shows that strategy-proof random mechanisms satisfying unanimity conditions are random dictatorships; Dutta, Peters and Sen (2007, 2008) give and correct the cardinal version used in the chapter.
• 1985: Mertens and Zamir construct the universal type space of belief hierarchies; the space of finite types is emphasized by Dekel, Fudenberg and Morris (2006).
• 1988: Crémer and McLean show that with correlated types satisfying a spanning condition, beliefs can be elicited at no cost (Proposition 6.4 of the book).
• 2001–2005: Bergemann and Morris introduce payoff and belief types and prove that on finite type spaces only incentive constraints between types with the same beliefs matter (their Proposition 4.5, the goal of this mission).
• 2010–2014: Smith, Börgers and Smith study the ranking of mechanisms without a common prior; random dictatorship with compromise comes from Börgers and Smith (2012, 2014).

Setting

There are finitely many agents $i \in I$, and agent $i$ has a set $\Theta_i$ of payoff types. An outcome $x$ gives agent $i$ the utility $u_i(x,\theta)$, which may depend on all payoff types. A type space $\mathcal T = (T_i,\hat\theta_i,\hat\beta_i)_{i\in I}$ consists of nonempty sets $T_i$ of types, a payoff type map $\hat\theta_i : T_i \to \Theta_i$ and a belief map $\hat\beta_i : T_i \to \Delta(T_{-i})$, where $T_{-i} = \prod_{j\ne i}T_j$. Different types may share a payoff type and differ only in their beliefs, and vice versa. A common prior is a distribution $\mu$ on $T$ from which every type's belief is obtained by conditioning. A type space has a large variety of certainties if for every $\theta_i$ and $\theta_{-i}$ some type with payoff type $\theta_i$ is certain that the others' payoff types are $\theta_{-i}$. The space of finite types $\mathcal T^+$ collects every infinite hierarchy of beliefs ("I believe that you believe that …") that is generated by a type of some finite type space.

A mechanism $(S_1,\dots,S_N,g)$ has strategy sets $S_i$ and an outcome rule $g : S \to \Delta(X)$. Strategies $\sigma_i : T_i \to \Delta(S_i)$ form a Bayesian equilibrium if each type maximizes expected utility under its own belief; it is belief-independent if types with equal payoff types play alike, and ex post if each type's choice stays optimal when it becomes certain of the others' types. A direct mechanism asks agents for their types, a reduced direct mechanism only for their payoff types. In the quasi-linear case outcomes are $(a,t_1,\dots,t_N)$ and $u_i = v_i(a,\theta) - t_i$, with $t_i$ paid by agent $i$; a direct mechanism is $(q,t)$.

Formalization targets

Goal: belief revelation on finite type spaces (Proposition 10.6)

On a finite type space with quasi-linear utilities, suppose that for every agent no belief in $\{\hat\beta_i(\tau_i) : \tau_i\in T_i\}$ is a convex combination of the others, and that in the direct mechanism $(q,t)$ no type wants to imitate another type with the same belief. Then there is a direct mechanism $(\tilde q,\tilde t)$ in which truth telling is a Bayesian equilibrium, with

The goal fixes neither the transfers $\tilde t$ nor any bound on them; it asserts the existence of a truthful mechanism with the same alternatives and the same interim payments.

Milestones

The other fourteen numbered results of the chapter: conditional independence of payoff types under a full-support common prior (10.1); three revelation principles (10.2–10.4); existence of Bayesian equilibria of finite mechanisms on $\mathcal T^+$ (10.5); betting between agents with inconsistent beliefs (10.7); ex post implementation of unique equilibrium outcomes and alternatives (10.8, 10.9); emptiness of the set of undominated auctions under interim Pareto welfare and under ex post revenue (10.10, 10.11); Hylland's characterization of random dictatorship (10.12); and three comparisons of random dictatorship with random dictatorship with compromise (10.13–10.15).

Significance

Proposition 10.6 reduces the design problem on a finite type space to incentive constraints among types with the same beliefs: belief types can always be elicited by side payments that leave interim utilities unchanged. With a common prior and Proposition 10.1 this yields optimal mechanisms by solving an independent-types problem for each profile of belief types (§10.8; Farinha Luz 2013 carries this out for auctions). Proposition 10.7 and its consequences 10.10–10.11 show why the same construction cannot be used without a common prior: inconsistent beliefs allow unbounded bets, so interim or revenue criteria admit no undominated mechanism. Propositions 10.12–10.15 show that relaxing belief independence escapes Hylland's impossibility result in the voting problem.

None of these results is formalized elsewhere to our knowledge. The book proves only some of them (10.1, 10.5, 10.8, 10.9, 10.13–10.15 are proved or outlined; 10.6 is sketched; the proofs of 10.2–10.4 are omitted as standard; 10.7 and 10.10–10.12 are stated without proof), so formalization also produces complete proofs of results the book leaves informal. Two printed statements are corrected (see Formalization scope).

Difficulty

The obvious approach to Proposition 10.6 applies the Crémer–McLean construction type by type. This fails because several types may share a belief: a side payment that depends on the reported belief cannot separate them, and the convex-independence condition concerns the set of distinct beliefs rather than the indexed family of types.

For the results on $\mathcal T^+$, a type is an infinite belief hierarchy, and a strategy must be one function on all finite types simultaneously. Existence (10.5) cannot be obtained by applying Nash's theorem to a single finite type space, because a type belongs to many finite type spaces and must play the same strategy in all of them. Hylland's theorem (10.12) requires a full characterization of strategy-proof random rules on a cardinal preference domain.

Formalization scope

• Distributions $\Delta(X)$ are countably supported (PMF X); expected utilities are sums. The book leaves the measure structure of type spaces unspecified (p.179, note 3); finite type spaces, $\mathcal T^+$ and point beliefs are covered exactly. A Bayesian equilibrium requires every type's expected utility to exist (absolute summability) under every mixed strategy.
• A type's belief is a distribution on $\prod_{j\ne i}T_j$. Beliefs in Proposition 10.6 are vectors in $\mathbb R^{T_{-i}}$, and condition (i) is stated with the convex hull of the other distinct beliefs.
• Quasi-linear direct mechanisms are deterministic, $q : T\to A$, $t_i : T\to\mathbb R$. Mixed misreports are allowed in every equilibrium notion.
• $\mathcal T^+$ is built from belief hierarchies encoded level by level ($L_0 = \Theta_i$, $L_{n+1} = \Theta_i\times\Delta(\prod_{j\ne i}L_{n,j})$) and the finite type spaces generating them. The universal type space (Definition 10.5) is not needed and not formalized.
• §10.11: two agents Fin 2, candidates $\{a,b,c\}$, strict private vNM utilities with every strict utility attained; mechanisms map to lotteries over candidates; rankings are bijections C ≃ Fin 3.
• Corrections of the page: in Proposition 10.7 the signs of the transfers in (v) are reversed on the page relative to the bet described on p.186 and are stated as described; Proposition 10.9 is false under a large variety of certainties alone and is stated under the common-certainty condition that its proof uses, on type spaces whose beliefs have finite support (with countably supported beliefs the reduced mechanism's expected utilities need not exist). Both are explained in the item notes.
• The goal is not trivialized by taking $(\tilde q,\tilde t) = (q,t)$: condition (ii) constrains only types with the same belief, so the original mechanism is in general not incentive-compatible, and the conclusion demands full Bayesian incentive compatibility.

Welcome contributions: a finite Farkas/separation lemma in the form needed for 10.6 (the platform has Polyhedral.farkas_lemma), basic API for PMF-valued type spaces (products of mixed strategies, conditioning), and the hierarchy map of finite type spaces, which all $\mathcal T^+$ milestones share.

Selected references

• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Ch. 10. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• D. Bergemann, S. Morris, Robust Mechanism Design, Cowles Foundation Discussion Paper 1421, 2001; Econometrica 73 (2005) 1771–1813. https://doi.org/10.1111/j.1468-0262.2005.00638.x
• J. Crémer, R. McLean, Full Extraction of the Surplus in Bayesian and Dominant Strategy Auctions, Econometrica 56 (1988) 1247–1257. https://doi.org/10.2307/1913096
• J.-F. Mertens, S. Zamir, Formulation of Bayesian Analysis for Games with Incomplete Information, International Journal of Game Theory 14 (1985) 1–29. https://doi.org/10.1007/BF01770224
• B. Dutta, H. Peters, A. Sen, Strategy-Proof Cardinal Decision Schemes, Social Choice and Welfare 28 (2007) 163–179. https://doi.org/10.1007/s00355-006-0152-4
• T. Börgers, D. Smith, Robust Mechanism Design and Dominant Strategy Voting Rules, Theoretical Economics 9 (2014) 339–360. https://doi.org/10.3982/TE1100

Motivation

Voting rules, committee procedures and any other method that turns individual rankings into one collective choice face the same question: can the rule be designed so that no participant ever gains by misreporting their ranking? The Gibbard–Satterthwaite theorem (Gibbard, 1973; Satterthwaite, 1975) answers no. When at least three alternatives can be chosen and all strict rankings are admissible, the only rules immune to manipulation are dictatorships. The result is the starting point of mechanism design without money. It explains why the positive results of the transferable-utility chapters of the book (Groves, VCG, posted prices) depend on quasi-linear preferences, and why research on voting turned to restricted preference domains and weaker solution concepts.

This mission formalizes Chapter 8 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), §§8.2–8.3. The book's route to the theorem follows Reny (2001). Strategy-proofness implies Maskin monotonicity, and every monotone rule with full range over at least three alternatives is dictatorial. The second step is the Muller–Satterthwaite theorem (Muller and Satterthwaite, 1977), which is stronger than Gibbard–Satterthwaite because monotonicity is weaker than strategy-proofness. The chapter closes with the classical escape route: on single-peaked preferences (Moulin, 1980) the median voting rule is strategy-proof and not dictatorial.

Timeline. Arrow (1951/1963) proved the impossibility of non-dictatorial preference aggregation under independence of irrelevant alternatives. Gibbard (1973) and Satterthwaite (1975) proved the manipulation version independently, and Satterthwaite showed the two theorems are equivalent. Muller and Satterthwaite (1977) showed that on the full domain strategy-proofness is equivalent to a monotonicity condition (strong positive association). Moulin (1980) characterized strategy-proof rules on single-peaked domains that depend only on reported peaks. Reny (2001) gave the short common proof of Arrow's and the Muller–Satterthwaite theorems that the book follows.

Setting

There is a finite set $I=\{1,\dots,N\}$ of agents and a finite set $A$ of alternatives. Each agent $i$ has a preference relation $R_i$ over $A$; $a\,R_i\,b$ reads "$a$ is weakly preferred to $b$". Every $R_i$ is a linear order: complete, transitive, and the only indifference is among identical alternatives. Its strict part is $P_i$. The set of all linear orders over $A$ is $\mathcal R$, and a profile is $R=(R_1,\dots,R_N)\in\mathcal R^N$. $(R_i',R_{-i})$ is the profile obtained from $R$ by replacing agent $i$'s preference with $R_i'$.

A direct mechanism is a function $f:\mathcal R^N\to A$ (Definition 8.1). It is

• dominant strategy incentive-compatible (DSIC) if $f(R_i,R_{-i})\,R_i\,f(R_i',R_{-i})$ for all $i$, $R$, $R_i'$ (Definition 8.2);
• dictatorial if some agent $i$ satisfies $f(R)\,R_i\,a$ for all profiles $R$ and all $a\in A$ (Definition 8.3);
• monotone if $f(R)=a$ and, for every $i$, $a\,R_i\,b\Rightarrow a\,R_i'\,b$ for all $b$, together imply $f(R')=a$ (Definition 8.4);
• set-monotone if $f(R)\in B$ and, for every $i$, $R_i'$ differs from $R_i$ only in the ranking of elements of $B$, together imply $f(R')\in B$ (Definition 8.5);
• unanimity-respecting if $f(R)=a$ whenever every agent ranks $a$ at the top (Definition 8.6).