Motivation

A hotel sells rooms of several types, in limited numbers, to guests who each want one room. The revenue-optimal way to sell is known only in special cases: for buyers with several private values, optimal mechanisms can be randomized, involve lotteries, and lack a closed form (Manelli–Vincent 2007; Chawla, Hartline, Kleinberg 2007). In practice sellers post prices. The question is how much revenue posting prices gives up.

Chawla, Hartline, Malec and Sivan (arXiv:0907.2435v2, STOC 2010) answer it for a broad class of single- and multi-parameter problems. For unit-demand buyers of multiple copies of multiple items they show that a menu of posted prices, offered to the buyers in whatever order they arrive, earns at least $1/6.75$ of the revenue of any deterministic truthful mechanism (Theorem 14). This mission formalizes that result together with the two steps it is built from: a reduction from the multi-parameter problem to a single-parameter one with "copies" of each buyer (Lemma 3, Theorem 4), and an order-oblivious pricing for the intersection of two partition matroids (Theorem 13).

Setting

Single-parameter problem (BSMD). Finitely many agents $i$ have independent private values $v_i \sim F_i$, each with a density on a bounded interval. A seller may serve any set in a downward-closed set system $\mathcal J$. A deterministic mechanism $M$ maps reported values $v$ to a served set $M(v) \in \mathcal J$ and payments $\pi_i(v)$; it is truthful if reporting the true value is a dominant strategy and no agent ends with negative utility. Its expected revenue is $\mathcal R^M = \mathbb E_v[\sum_i \pi_i(v)]$. For prices $p$, agent $i$ desires service if $p_i \le v_i$, and $\mathcal S_v$ is the class of maximal feasible sets of desiring agents. The order-oblivious revenue is

$$\mathcal R^{\mathrm{obl}}_{\mathbf p} = \mathbb E_{v}\Big[\min_{S \in \mathcal S_v} \sum_{i \in S} p_i\Big],$$

a lower bound on the revenue of posting the prices $p$ to the agents in an adversarial order.

Multi-parameter unit-demand problem (BMUMD). There are $m$ buyers and a finite set $J$ of services, partitioned into the groups $J_i$ of services targeted at buyer $i$. Buyer $i$ has value $v_j$ for each $j \in J_i$, all values independent with $v_j \sim F_j$, and the set system $\mathcal J \subseteq 2^J$ is unit-demand: $|S \cap J_i| \le 1$ for feasible $S$. A mechanism $\mathcal A$ is truthful if no buyer gains by misreporting its whole vector $(v_j)_{j \in J_i}$, and individually rational if a buyer receiving $j$ pays at most $v_j$ and a buyer receiving nothing pays $0$.

Copies. The instance $\mathcal I^{\mathrm{copies}}$ replaces each buyer $i$ by $|J_i|$ single-parameter agents, one per service $j \in J_i$ with value $v_j$, under the same $\mathcal J$.

Price menus. Given prices $(p_j)$ and an arrival order $\sigma$, the price-menu mechanism approaches the buyers in order; buyer $i$ is offered the services of $J_i$ that can still be feasibly allocated, at prices $p_j$, and buys a utility-maximizing one if some has $p_j \le v_j$.

Multiple copies of items. With items $K$ and $\mathrm{cap}(k)$ copies of item $k$, services are pairs $(i,k)$ and a set of services is feasible if it gives each buyer at most one item and uses at most $\mathrm{cap}(k)$ copies of $k$: the intersection of two partition matroids.

Formalization targets

Goal: Theorem 14

For regular distributions there are prices $p$ such that, for every arrival order $\sigma$, the price-menu mechanism $\mathcal P_\sigma$ is truthful and

$$\mathcal R^{\mathcal A} \le \tfrac{27}{4}\,\mathcal R^{\mathcal P_\sigma}$$

for every individually rational, truthful deterministic mechanism $\mathcal A$.

Milestones

• Truthful BMUMD mechanisms are weakly monotone (p. 13), and the allocation of $\mathcal A^{\mathrm{copies}}$ is monotone in each $v_j$ (p. 13).
• Lemma 3: $\mathcal R^{\mathcal A} \le \mathcal R^{\mathcal A'}$ for some truthful $\mathcal A'$ on $\mathcal I^{\mathrm{copies}}$.
• The price-menu mechanism allocates a maximal feasible set of services (p. 14).
• Theorem 4: if $\mathcal R^{M'} \le \alpha\,\mathcal R^{\mathrm{obl}}_{\mathbf p}$ for every truthful $M'$ on $\mathcal I^{\mathrm{copies}}$, then $\mathcal R^{\mathcal A} \le \alpha\,\mathcal R^{\mathcal P_\sigma}$ for every $\sigma$ and every truthful IR $\mathcal A$.
• Lemma 2 (regular part): $\mathcal R^M \le \sum_i p^M_i q^M_i$, with $q^M_i$ the probability that $M$ serves $i$ and $F_i(p^M_i) = 1 - q^M_i$.
• Theorem 19 (existence form): a revenue-optimal truthful mechanism exists.
• The claim $c_i \ge 4/9$ of App. D.4: under $\sum_{i' \in P} q_{i'} \le \mathrm{cap}(P)/3$ in every part, with probability at least $4/9$ neither part of $i$ is full without $i$.
• Theorem 13: for two partition matroids there are prices with $\mathcal R^M \le \tfrac{27}{4}\,\mathcal R^{\mathrm{obl}}_{\mathbf p}$ for every truthful $M$.

Significance

The result shows that for unit-demand buyers, a seller loses at most a constant factor by replacing the optimal, possibly opaque, truthful mechanism with a menu of prices that does not depend on the order in which buyers arrive. The reduction of Theorem 4 is generic: any order-oblivious pricing for the single-parameter instance with copies, under any unit-demand constraint, transfers to the multi-parameter instance with the same factor. Theorem 13 supplies one such pricing for the intersection of two partition matroids, which is exactly the shape of the multi-unit, multi-item constraint.

All results here are proved in the paper and none is formalized elsewhere; the platform has Myerson's single-unit optimal auction and weak monotonicity in an abstract quasilinear model (Börgers), but no posted-price approximation, no copies reduction, and no order-oblivious revenue. The formal development adds a machine-checked account of the reduction (in particular that the price-menu mechanism is truthful and allocates a maximal feasible set for every order), a precise version of the probabilistic claim behind the constant $6.75$, and reusable definitions of order-oblivious revenue and of multi-parameter truthfulness with the paper's individual rationality.

Difficulty

Lemma 3 needs more than the observation that the copies instance has more competition: one must build a truthful single-parameter mechanism with at least the same revenue. The allocation is copied, but the payments must be threshold payments of the copies mechanism, and showing they dominate the original payments uses both weak monotonicity and the paper's individual rationality, through the taxation principle.

Theorem 13 compares order-oblivious revenue with Myerson's revenue through the bound of Lemma 2, at prices built from Myerson's service probabilities scaled by $1/3$. The step that is easy to get wrong is the probability that an agent is considered: the events "part $P_1$ is not full" and "part $P_2$ is not full" depend on overlapping agents, so the product bound $(2/3)(2/3)$ does not follow from Markov's inequality alone; it holds because both events are decreasing in the set of desiring agents (Harris' inequality). The comparison must also be uniform: one set of prices must serve against every truthful mechanism, which requires an optimal mechanism to exist.

Formalization scope

• Distributions (P1): each $F_j$ has a measurable density, strictly positive on a bounded interval $[\underline v_j, \overline v_j] \subseteq [0, \infty)$, with no mass outside. Values are independent (product prior).
• Regularity (P2): the virtual value $\phi(v) = v - (1 - F(v))/f(v)$ is non-decreasing on the support. It is assumed in Lemma 2, Theorem 19, Theorem 13 and the goal. Theorem 14 does not state it, but its proof goes through Theorem 13, which the paper proves for regular distributions; the non-regular extension (App. E, randomized prices) is out of scope, as is the second paragraph of Lemma 2.
• Mechanisms (P3): deterministic; dominant-strategy truthful with misreports in the support (a buyer misreports all coordinates of $J_i$ at once); single-parameter IR is ex-post nonnegative utility; multi-parameter IR is the paper's ($\pi_i \le v_j$ if served $j$, $\pi_i = 0$ if unserved); allocation events and payments measurable, payments integrable.
• Benchmarks (P4): Myerson's mechanism is not constructed. "Approximates $\mathcal R^{\mathcal M}$" is stated against every truthful mechanism, and Lemma 3 and Theorem 19 in existence form.
• Price menus: ties between utility-maximizing services are broken by a fixed enumeration of $J$; a service of utility $0$ is bought. Theorem 4 assumes $\alpha \ge 0$.
• Dropped: the last sentence of Theorem 14 (polynomial-time computability of the prices) has no cost model here.
• Constant: $6.75$ is written $27/4$ everywhere.
• Not trivializable: the prices in Theorem 13 and the goal are chosen before the mechanism, and the benchmark includes every truthful mechanism, so a degenerate price vector cannot meet the bound; $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ is a genuine minimum over a nonempty finite class.

Needed infrastructure, reusable beyond this mission: Myerson's characterization of truthful single-parameter mechanisms and the revenue–virtual-surplus identity for densities on intervals, Harris' inequality for product measures, and the taxation principle for deterministic multi-parameter mechanisms. Contributions on any of these are welcome.

Selected references

• S. Chawla, J. D. Hartline, D. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, STOC 2010; arXiv:0907.2435v2, 2010. https://arxiv.org/abs/0907.2435
• R. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• S. Chawla, J. D. Hartline, R. Kleinberg, Algorithmic Pricing via Virtual Valuations, EC 2007. https://arxiv.org/abs/0711.3203
• A. M. Manelli, D. R. Vincent, Multidimensional mechanism design: Revenue maximization and the multiple-good monopoly, Journal of Economic Theory 137(1), 2007. https://doi.org/10.1016/j.jet.2006.12.007
• T. E. Harris, A lower bound for the critical probability in a certain percolation process, Proc. Cambridge Philos. Soc. 56, 1960. https://doi.org/10.1017/S0305004100034241

Motivation

Many sales are contracted before the buyer knows what the good is worth to her. An airline sells a ticket months before the trip, a hotel sells a refundable or non-refundable room before the traveller's plans are settled, and a supplier signs a capacity contract before demand is realised. At the time of contracting the buyer holds some private information about her future valuation (how likely she is to travel), and after contracting she learns more (whether she actually travels). Sequential screening is the mechanism design problem of a seller facing such a buyer.

The chapter formalized here, Daniel Krähmer and Roland Strausz's Dynamic Mechanism Design (Chapter 11 of Börgers' textbook), develops the problem along two lines. The first is dynamic private information: one sale, two rounds of private information. The second is dynamic allocations: repeated sales, one fixed valuation.

Timeline:

• Baron and Besanko (1984) show that dynamic allocations with static information produce no real dynamics in the optimal mechanism.
• Courty and Li (2000, Review of Economic Studies) solve the sequential screening problem and show that the optimal mechanism is a menu of option contracts.
• Esö and Szentes (2007) decompose the buyer's information into initial and additional information, show that the seller can extract the additional information at no cost, and derive the optimal multi-buyer mechanism, the handicap auction.
• Krähmer and Strausz (2011, 2014), cited in the chapter's problems (notes 2–3, p.237), show that the conclusions depend on the model's assumptions; with discrete ex ante types the privacy of the additional information can cost the seller (Problem 11.5(c), p.233).

Setting

A seller sells one indivisible good. Before contracting, the buyer privately observes her ex ante type $\tau\in[\underline\tau,\bar\tau]$, with distribution function $G$ and density $g>0$. After accepting the mechanism she privately observes her ex post type $\theta\in[\underline\theta,\bar\theta]$, $0\le\underline\theta<\bar\theta$, which is her valuation. Conditionally on $\tau$ it has distribution function $F(\theta\mid\tau)$ and density $f(\theta\mid\tau)>0$. Both $F$ and $f$ are continuously differentiable in $\tau$, $|\partial F/\partial\tau|<K$, and higher $\tau$ is good news in the sense of first-order stochastic dominance: $\partial F(\theta\mid\tau)/\partial\tau<0$ for $\theta\in(\underline\theta,\bar\theta)$.

A direct mechanism is a pair $q(\tau,\theta)\in[0,1]$, $t(\tau,\theta)\in\mathbb R$. The buyer first reports $\tau$, then $\theta$. Write $u(\tau,\theta)=\theta q(\tau,\theta)-t(\tau,\theta)$, $\hat U(\tau'\mid\tau)=\int u(\tau',\hat\theta)f(\hat\theta\mid\tau)\,d\hat\theta$ and $U(\tau)=\hat U(\tau\mid\tau)$. The mechanism is incentive-compatible if truth about $\theta$ is optimal after every report of $\tau$, and truth about $\tau$ is optimal against every subsequent reporting function $\theta_r$. It is individually rational if $U(\tau)\ge0$ for all $\tau$. The seller maximizes expected revenue $\int\!\!\int t\,f\,g$. The virtual valuation is

$$\psi(\tau,\theta)=\theta+\frac{1-G(\tau)}{g(\tau)}\,\frac{\partial F(\theta\mid\tau)/\partial\tau}{f(\theta\mid\tau)} ,$$

and Assumption 11.1 requires $\psi$ to be increasing in $\tau$ and $\theta$. The exercise price is $p(\tau)=\min\{\hat\theta\mid\psi(\tau,\hat\theta)\ge0\}$.

Formalization targets

Goal: Proposition 11.8 (optimal sequential screening)

Under Assumption 11.1 the optimal mechanism is

$$q^*(\tau,\theta)=\mathbf 1[\theta\ge p(\tau)],\qquad t^*(\tau,\theta)=t_0(\tau)+p(\tau)\,\mathbf 1[\theta\ge p(\tau)],$$

where $t_0$ is the expression of Proposition 11.5 for $q^*$, and the lowest type pays

$$t(\underline\tau,\underline\theta)=\int_{p(\underline\tau)}^{\bar\theta}\hat\theta f(\hat\theta\mid\underline\tau)\,d\hat\theta-p(\underline\tau)\bigl[1-F(p(\underline\tau)\mid\underline\tau)\bigr]+\underline\theta q^*(\underline\tau,\underline\theta).$$

The goal asserts that this mechanism is incentive-compatible, individually rational and optimal. It also characterizes all optimal mechanisms: an incentive-compatible, individually rational mechanism is optimal if and only if $q=q^*$ almost everywhere off $\{\psi=0\}$ and $U(\underline\tau)=0$. When $\{\psi=0\}$ is null, this becomes $q=q^*$ and $t=t^*$ almost everywhere.

Milestones

The path to the goal, in the book's order:

• the dynamic revelation principle (Proposition 11.1);
• the reduction of incentive compatibility to two families of inequalities (Proposition 11.2);
• the ex post characterization (Proposition 11.3);
• monotonicity and absolute continuity of $U$ (Lemma 11.1);
• the envelope formula $U'(\tau)=-\int q(\tau,\hat\theta)\,\partial F(\hat\theta\mid\tau)/\partial\tau\,d\hat\theta$ (Proposition 11.4);
• the transfer formula (Proposition 11.5);
• sufficiency of monotone allocation rules (Proposition 11.6);
• individual rationality at $\underline\tau$ (Proposition 11.7).

Three extensions follow. Propositions 11.9 and 11.10 show that the privacy of the additional information $\gamma=F(\theta\mid\tau)$ costs the seller nothing. Proposition 11.11 gives the optimal mechanism with several buyers. Proposition 11.12 shows that with dynamic allocations and a fixed valuation, repeating the static posted price is optimal.

Significance

The result gives a practical rule: sell an option. Ex ante type $\tau$ pays a fee $t_0(\tau)$ for the right to buy later at the exercise price $p(\tau)$, and $p$ decreases in $\tau$. This explains refund and cancellation menus in advance-purchase markets. Proposition 11.10 adds that information the buyer receives after contracting generates no rents under Assumption 11.1. A seller therefore gains from contracting early and from disclosing information after contracting. Proposition 11.12 shows that, under full commitment, a monopolist gains nothing from responding to past purchases.

On the formal side, the results are proved in the literature and in the book, but none of them is machine-checked. The mission produces a verified envelope theorem in a two-dimensional type space where incentive compatibility does not imply monotonicity. It also produces a verified revenue-equivalence formula for sequential mechanisms, and the first verified optimal-mechanism results with dynamic information.

Difficulty

The static argument of Chapter 2 does not carry over directly. Incentive compatibility with respect to $\tau$ does not make $q$ increasing in $\tau$. The buyer's first-period utility is an expectation over a whole schedule $q(\tau',\cdot)$, so single crossing has no bite. The characterization therefore splits into necessary conditions (the envelope formula in $\tau$, which needs Lipschitz continuity of $U$ from the bound $K$) and a sufficient condition (monotonicity in both arguments, via first-order stochastic dominance), and the two meet only under Assumption 11.1.

Definition 11.2(ii) quantifies over all off-path reporting functions. The revelation principle does not remove them, so Proposition 11.2 is needed before any envelope argument applies.

Pointwise maximization of the virtual surplus pins down $q$ only where $\psi\ne0$ and only almost everywhere. The optimal mechanism is therefore not unique in the pointwise sense the page states.

Formalization scope

• Representation. $F(\theta\mid\tau)$ is F θ τ and $q(\tau,\theta)$ is q τ θ. Functions are total on $\mathbb R$ or $\mathbb R^2$, and conditions quantify over the type intervals only. $\partial F/\partial\tau$ and $\partial f/\partial\tau$ are fields pinned by HasDerivWithinAt on $[\underline\tau,\bar\tau]$.
• Measurability. The book omits all measurability. Here the densities are jointly measurable, mechanisms are admissible (measurable on the type rectangle, $q\in[0,1]$), and reporting functions are measurable. In the observable-$\gamma$ model each $\tilde t(\tau,\cdot)$ is integrable on $[0,1]$, and in the several-buyer model each payment $t_i$ is integrable against the distribution of the type profile, so that expected utilities and expected revenue are genuine integrals.
• Revenue and a.e. Revenue is the integral of $t$ against the joint law with density $g(\tau)f(\theta\mid\tau)$, and "almost everywhere" refers to that law.
• Corrected necessity. The page's pointwise "if and only if" in Propositions 11.8 and 11.11 is corrected. The explicit optimal mechanism is kept, with the formulas (11.10), (11.11), (11.12) and $t_0$ of Proposition 11.5. Necessity is stated almost everywhere and off $\{\psi=0\}$, and, for several buyers, off ties between virtual valuations.
• Regularity. Propositions 11.9 and 11.10 assume $f$ and $\partial F/\partial\tau$ continuous in $(\tau,\theta)$, the regularity the book invokes on p.217 to differentiate $F^{-1}(\gamma\mid\tau)$.
• Exercise price. $p(\tau)$ is the infimum of $\{\hat\theta\mid\psi(\tau,\hat\theta)\ge0\}$.

Ruled out. Stating only that the cutoff mechanism is incentive-compatible and individually rational, or only that it beats posted prices, would trivialize the goal. The goal asserts optimality among all admissible incentive-compatible, individually rational sequential mechanisms with randomized allocations, together with the explicit fee $t_0$ and (11.12).

Infrastructure. A complete development needs envelope theorems for suprema of equi-differentiable families, integration by parts with absolutely continuous functions, differentiation under the integral sign, and change of variables $\gamma=F(\theta\mid\tau)$. The single-buyer lemmas (Propositions 11.2–11.7) are reusable for the multi-buyer case through the interim mechanism $(Q_i,T_i)$. Proofs of any milestone, and sorry-free lemmas on the definitions, are welcome.

Selected references

• D. Krähmer and R. Strausz, Dynamic Mechanism Design, Chapter 11 in T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• P. Courty and H. Li, Sequential Screening, Review of Economic Studies 67 (2000) 697–717. https://doi.org/10.1111/1467-937X.00150
• P. Eső and B. Szentes, Optimal Information Disclosure in Auctions and the Handicap Auction, Review of Economic Studies 74 (2007) 705–731. https://doi.org/10.1111/j.1467-937X.2007.00438.x
• D. P. Baron and D. Besanko, Regulation and Information in a Continuing Relationship, Information Economics and Policy 1 (1984) 267–302.

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

$$\tilde q(\tau) = q(\tau)\ \ \forall \tau\in T,\qquad \sum_{\tau_{-i}}\hat\beta_i(\tau_i)(\tau_{-i})\,\tilde t_i(\tau) = \sum_{\tau_{-i}}\hat\beta_i(\tau_i)(\tau_{-i})\, t_i(\tau)\ \ \forall i,\tau_i.$$

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).

"The range of $f$ is $A$" means that every alternative is chosen at some profile.

For §8.3 the alternatives are labelled $1,\dots,K$. A preference is single-peaked if it has a top alternative $k(i)$ and declines monotonically to the right and to the left of it. $\hat{\mathcal R}$ is the set of single-peaked preferences, and on the restricted domain $\hat{\mathcal R}^N$ DSIC and dictatorship are read with all profiles and deviations taken from $\hat{\mathcal R}$.

Formalization targets

Goal: Proposition 8.5 (Muller–Satterthwaite)

$$|A|\ge 3,\quad f(\mathcal R^N)=A,\quad f\ \text{monotone}\ \Longrightarrow\ \exists\, i\in I\ \ \forall R\in\mathcal R^N\ \forall a\in A:\ f(R)\,R_i\,a.$$

This is the book's own capstone ("the core of the proof", p.144). No constant needs to be fixed, and the statement is strictly stronger than the necessity half of Gibbard–Satterthwaite.

Milestones

• Proposition 8.2: DSIC $\Rightarrow$ monotone.
• Proposition 8.3: monotone $\Rightarrow$ set-monotone.
• Proposition 8.4: monotone and full range $\Rightarrow$ respects unanimity.
• Proposition 8.1 (Gibbard–Satterthwaite): for $|A|\ge3$ and full range, $f$ is DSIC $\iff$ $f$ is dictatorial.
• Proposition 8.6: for $|A|\ge3$ and at least two agents, there is a mechanism on $\hat{\mathcal R}^N$ with range $A$ that is DSIC on $\hat{\mathcal R}^N$ and not dictatorial on $\hat{\mathcal R}^N$.

Significance

The result itself. Proposition 8.5 turns an incentive question into a purely ordinal one: any full-range rule that is Maskin monotone is a dictatorship once three alternatives are available. With Proposition 8.2 it gives Gibbard–Satterthwaite. Proposition 8.6 marks the boundary of the impossibility: with a one-dimensional ordering of alternatives and single-peaked preferences, the median voter rule escapes it.

Formalizing it. All results are classical and proved. The platform already has a proved Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite, Algorithmic Game Theory III), derived from Arrow's theorem in the alternative Mathlib environment c5ea0035…. It uses strict-order profiles and a one-agent-deviation monotonicity. This mission adds Maskin monotonicity, the Muller–Satterthwaite theorem, Reny's direct proof route, and the single-peaked possibility result, none of which is on the platform, all in the default environment.

Difficulty

Propositions 8.2–8.4 are short. The difficulty is in Proposition 8.5. Its proof moves one alternative up or down agents' rankings one agent at a time, and it has to keep the chosen alternative pinned at every step using only monotonicity, set-monotonicity and unanimity. It needs a pivotal agent, whose identity depends on the pair of alternatives, and then an argument that the pivots for different alternatives coincide. The argument uses a third alternative $c$ in an essential way. With two alternatives the conclusion is false (majority rule), so any argument that never uses $|A|\ge3$ cannot succeed. Formally, each "move $b$ just below $a$ in agent $j$'s ranking" is an explicit construction of a new linear order, together with a check that the monotonicity hypothesis applies. The figures on pp.146–149 describe these orders only partially ("the other alternatives in arbitrary order"). For Proposition 8.6, the obstacle is that DSIC must be checked against every single-peaked misreport, not only misreports of the peak.

Formalization scope

• A linear order is the structure LinPref A (relation rel, completeness, transitivity, antisymmetry). A profile is ι → LinPref A for a finite agent type ι, and a direct mechanism is (ι → LinPref A) → A. $A$ is a Fintype. "The range of $f$ is $A$" is Function.Surjective f, and $|A|\ge3$ is 3 ≤ Fintype.card A.
• Monotonicity is the book's Definition 8.4 for arbitrary pairs of profiles, with the lower-contour condition required for each agent separately. Dictatorship is ∃ i, ∀ R a, f R ≥_{R_i} a, with the agent chosen before the profile. A weaker monotonicity (one-agent deviations only) or a weaker dictatorship ("some agent's top is chosen at some profile") would trivialize the goal and is ruled out.
• §8.3: the labelling is lab : A ≃ Fin K (labels $0,\dots,K-1$). The restricted domain is a predicate on LinPref A, and DSIC, dictatorship and full range are relativized to profiles in the domain (IsDSICOn, IsDictatorialOn, HasFullRangeOn). Values of the mechanism off the domain are never consulted.
• Two corrections of the page. The left-hand clause of single-peakedness is printed as $(\ell-1)\,R_i\,\ell$ and is used as $\ell\,R_i\,(\ell-1)$ (the book's words "decline monotonically to the left"). Proposition 8.6 carries the added hypothesis $N\ge2$, since with one agent every onto strategy-proof rule is dictatorial.
• Proposition 8.6 is an existence statement. The median voting mechanism is the book's witness, but the statement does not fix it.
• Reusable beyond this mission: the linear-order profile model, Maskin monotonicity and the restricted-domain notions, which apply to Arrow-type results, implementation theory and Moulin's characterization. Proofs of any milestone, or an independent formal proof of Proposition 8.5, are welcome.

Selected references

• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Ch. 8. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• A. Gibbard, "Manipulation of voting schemes: a general result", Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083
• M. A. Satterthwaite, "Strategy-proofness and Arrow's conditions", Journal of Economic Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
• E. Muller and M. A. Satterthwaite, "The equivalence of strong positive association and strategy-proofness", Journal of Economic Theory 14 (1977) 412–418. https://doi.org/10.1016/0022-0531(77)90140-5
• P. J. Reny, "Arrow's theorem and the Gibbard–Satterthwaite theorem: a unified approach", Economics Letters 70 (2001) 99–105. https://doi.org/10.1016/S0165-1765(00)00332-3
• H. Moulin, "On strategy-proofness and single peakedness", Public Choice 35 (1980) 437–455. https://doi.org/10.1007/BF00128122
• S. Barberà, "An introduction to strategy-proof social choice functions", Social Choice and Welfare 18 (2001) 619–653. https://doi.org/10.1007/s003550100151

Motivation

A group of agents must choose one alternative from a set $A$ (whether to build a public project, who receives an object, which of several policies to adopt). Each agent privately knows how much each alternative is worth to them, and money can be transferred. A designer who wants the welfare-maximizing alternative must ask the agents for their valuations, and must set payments so that no agent gains by misreporting, whatever the others report. This requirement, dominant strategy incentive compatibility, does not depend on what agents believe about one another, which is why it is the standard robustness benchmark in public economics, auction design and algorithmic game theory.

The Vickrey–Clarke–Groves (VCG) mechanisms solve this problem for every efficient decision rule. The central question of Chapter 7 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), is whether they are the only solution, and what can be implemented in dominant strategies at all.

Timeline:

• 1961–1973: Vickrey (1961), Clarke (1971) and Groves (1973) introduce the payments that make efficient decisions dominant-strategy incentive-compatible.
• 1977: Green and Laffont (Econometrica 45) show that, when valuations range over a sufficiently rich connected domain, every efficient dominant-strategy mechanism has the Groves form.
• 1979: Holmström (Econometrica 47) extends the uniqueness result to smoothly connected domains. Roberts (1979) characterizes decision rules with positive association of differences on unrestricted domains as weighted welfare maximizers.
• 1987: Rochet (J. Math. Econ. 16) characterizes implementable decision rules by cyclical monotonicity, with no structure on alternatives or types.
• 2001: Krishna and Maenner (Econometrica 69) prove payoff equivalence for convex type sets and utilities convex in the type.
• 2009: Lavi, Mu'alem and Nisan (Soc. Choice Welf. 32) give two short proofs of Roberts' theorem.

Setting

There is a finite set $I$ of agents and a set $A$ of alternatives. Agent $i$ has a type $\theta_i$ from an abstract set $\Theta_i$. If alternative $a$ is chosen and agent $i$ pays $t_i$, agent $i$'s utility is $u_i(a,\theta_i) - t_i$. A type vector is $\theta \in \Theta = \prod_i \Theta_i$; $\theta_{-i} \in \Theta_{-i} = \prod_{j \ne i}\Theta_j$ omits agent $i$, and $(\theta_i', \theta_{-i})$ replaces agent $i$'s type by $\theta_i'$.

A direct mechanism $(q, t_1, \dots, t_N)$ consists of a decision rule $q : \Theta \to A$ and transfer rules $t_i : \Theta \to \mathbb R$. It is dominant strategy incentive-compatible (DSIC) if for all $\theta$, $i$ and $\theta_i'$,

$$u_i(q(\theta),\theta_i) - t_i(\theta) \ \ge\ u_i(q(\theta_i',\theta_{-i}),\theta_i) - t_i(\theta_i',\theta_{-i}).$$

A decision rule is efficient if $q(\theta)$ maximizes $\sum_i u_i(a,\theta_i)$ over $a \in A$ at every $\theta$. A mechanism is VCG if $q$ is efficient and every agent's transfer has the form

$$t_i(\theta) = -\sum_{j \ne i} u_j(q(\theta),\theta_j) + \tau_i(\theta_{-i})$$

for some function $\tau_i$ of the other agents' types. The chapter also uses positive association of differences (PAD: if $q(\theta) = a$ and every agent's utility advantage of $a$ over every other alternative strictly increases from $\theta$ to $\theta'$, then $q(\theta') = a$), flexibility (the range $q(\Theta)$ has at least three elements), ex post individual rationality and ex post budget balance ($\sum_i t_i(\theta) = 0$).

Formalization targets

Goal: uniqueness of VCG (Corollary 7.1, Green–Laffont–Holmström)

If every $\Theta_i$ is a convex subset of a Euclidean space $\mathbb R^{d_i}$ and every $u_i(a,\cdot)$ is convex and continuous on $\Theta_i$, then every DSIC mechanism $(q,t)$ with an efficient $q$ is a VCG mechanism: for each $i$ there is $\tau_i : \Theta_{-i} \to \mathbb R$ with

$$t_i(\theta) = -\sum_{j \ne i} u_j(q(\theta),\theta_j) + \tau_i(\theta_{-i}) \qquad \text{for all } \theta.$$

The goal leaves $A$, the number of agents and the dimensions $d_i$ free; it asserts only the form of the transfers.

Milestones

Every numbered result of Chapter 7 except Proposition 7.6 (see Formalization scope):

1. Proposition 7.1: implementability iff cyclical monotonicity in each agent's type (Rochet).
2. Proposition 7.2: on bounded, one-dimensional type sets, implementability iff monotonicity.
3. Proposition 7.3: under the goal's convexity hypotheses, the transfers implementing a given $q$ are unique up to $\tau_i(\theta_{-i})$.
4. Proposition 7.4: VCG mechanisms are DSIC.
5. Proposition 7.5: weak monotonicity in every $\theta_i$ implies PAD.
6. Proposition 7.7 (Roberts): on unrestricted domains with finite $A$, a flexible $q$ with range $q(\Theta) = A$ satisfies PAD iff there are $k_i \ge 0$, not all zero, and $F : A \to \mathbb R$ with $\sum_i k_i u_i(q(\theta),\theta_i) + F(q(\theta)) \ge \sum_i k_i u_i(a,\theta_i) + F(a)$ for all $a \in A$.
7. Proposition 7.8: affine maximizers with all $k_i > 0$ are implementable.
8. Proposition 7.9: ex post individual rationality holds iff it holds at the lowest type $\underline\theta_i$ with outside option $\underline a_i$.
9. Proposition 7.10: with $N \ge 2$, a budget-balanced VCG mechanism for efficient $q$ exists iff $\sum_i u_i(q(\theta),\theta_i) = \sum_i f_i(\theta_{-i})$ for some $f_i : \Theta_{-i} \to \mathbb R$.

Significance

Corollary 7.1 turns the VCG construction from one solution into the complete answer. Any question about efficient dominant-strategy mechanisms (revenue, budget balance, individual rationality) reduces to a question about the functions $\tau_i$. With Proposition 7.10 it gives a necessary and sufficient condition for efficient, budget-balanced dominant-strategy implementation. That condition fails in bilateral trade, and the failure does not use individual rationality. Roberts' theorem plays the same role for inefficient rules: on unrestricted domains, weighted welfare maximization is essentially all that can be implemented.

All of these results are proved in the literature, and none is formalized. The platform has VCG incentive compatibility and weak monotonicity for valuation-based types (the Algorithmic Game Theory IV mission). It has no uniqueness theorem, no revenue equivalence for multidimensional convex types, no Rochet theorem and no Roberts theorem. The book proves Corollary 7.1 from Proposition 7.3, but proves 7.3 itself only by reference to Krishna and Maenner. It states Roberts' theorem without proof.

Difficulty

The uniqueness claim does not follow from incentive compatibility alone. With finitely many types it is false, because any transfers inside the gaps left by the incentive constraints work (Börgers §5.8). The work lies in showing that, along every segment in the convex type set, an agent's equilibrium utility is pinned down by the decision rule. The equilibrium utility is a pointwise supremum of convex functions, one for each report, and the chosen alternative can change at uncountably many points of the segment. A differentiable envelope argument is therefore not directly available. At the boundary of the type set, convexity alone does not prevent upward jumps, which is why continuity is part of the hypotheses. Roberts' theorem needs a separate, combinatorial analysis of the sets of utility differences at which each alternative is chosen, and flexibility is essential there.

Formalization scope

Agents form a finite type ι with decidable equality. Types are arbitrary types Θ i, and utilities are u : ∀ i, A → Θ i → ℝ. The profile $(\theta_i',\theta_{-i})$ is Function.update θ i θ'. $\Theta_{-i}$ is the product Others Θ i over j ≠ i, so each $\tau_i$ and $f_i$ is a function of the others' types only; a constant or a function of the full profile would change the theorem. In the goal and Proposition 7.3, $\Theta_i$ is a convex set S i in EuclideanSpace ℝ (Fin (d i)).

Deviations from the page, each forced by a counterexample recorded in the item's natural-language statement:

• Corollary 7.1 and Proposition 7.3 add continuity of $u_i(a,\cdot)$ on $\Theta_i$. With convexity alone, a utility with a jump at the endpoint of $[0,1]$ admits a non-VCG DSIC mechanism.
• Proposition 7.7 is stated with $k_i \ge 0$, not all zero, instead of $k_i > 0$, and with the added hypothesis that $q$ is onto $A$ (the conclusion still ranges over all $a \in A$, as on the page). Dictatorships and affine maximizers over a proper subset of $A$ are counterexamples to the printed version.
• Proposition 7.6 (flexible PAD rules on unrestricted domains are implementable) is false as printed. It is not a milestone; the reason is in the mission's hard list.
• Proposition 7.10 adds $N \ge 2$, since its proof divides by $N-1$.

The trivializing formalization to avoid is proving Proposition 7.4 (VCG $\Rightarrow$ DSIC) in place of the goal (DSIC $+$ efficient $\Rightarrow$ VCG). A development that proves the goal needs reusable infrastructure: convex functions restricted to segments, absolute continuity of continuous convex functions on compact intervals, and an envelope theorem for suprema of convex functions. Proofs of Rochet's and Roberts' theorems in this abstract setting are also welcome.

Selected references

• T. Börgers (with D. Krähmer and R. Strausz), An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 7. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16, 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• E. H. Clarke, Multipart Pricing of Public Goods, Public Choice 11, 1971. https://doi.org/10.1007/BF01726210
• T. Groves, Incentives in Teams, Econometrica 41, 1973. https://doi.org/10.2307/1914085
• J. Green and J.-J. Laffont, Characterization of Satisfactory Mechanisms for the Revelation of Preferences for Public Goods, Econometrica 45, 1977. https://doi.org/10.2307/1911219
• B. Holmström, Groves' Scheme on Restricted Domains, Econometrica 47, 1979. https://www.jstor.org/stable/1911954
• K. Roberts, The Characterization of Implementable Choice Rules, in J.-J. Laffont (ed.), Aggregation and Revelation of Preferences, North-Holland, 1979, pp. 321–348.
• J.-C. Rochet, A Necessary and Sufficient Condition for Rationalizability in a Quasi-Linear Context, Journal of Mathematical Economics 16, 1987. https://doi.org/10.1016/0304-4068(87)90007-3
• V. Krishna and E. Maenner, Convex Potentials with an Application to Mechanism Design, Econometrica 69, 2001. https://doi.org/10.1111/1468-0262.00233
• R. Lavi, A. Mu'alem and N. Nisan, Two Simplified Proofs for Roberts' Theorem, Social Choice and Welfare 32, 2009. https://doi.org/10.1007/s00355-008-0333-3
• P. Milgrom, Putting Auction Theory to Work, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511813825