Motivation

Almost every model in queueing theory is analysed through a Markov chain. The number of customers in an M/M/c queue is a continuous-time birth–death chain; the number left behind by departing customers of an M/G/1 queue is a discrete-parameter chain on $\{0,1,2,\dots\}$ (the imbedded Markov chain); networks of queues are chains on vectors of queue lengths. Before any steady-state formula (Erlang's formulas, the Pollaczek–Khintchine formula, product forms) can be used, one has to know that the chain has a steady state at all: that it is positive recurrent, so that a stationary distribution exists and equals the limiting distribution.

Chapter 1 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), collects the two ingredients the rest of the book stands on: the Poisson process with its exponential interarrival times (§§1.7–1.8), and the classification theory of discrete-parameter Markov chains (§1.9), ending with Foster's criterion (Theorem 1.2), a sufficient condition for positive recurrence in terms of a drift inequality. The criterion goes back to F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24 (1953) (DOI 10.1214/aoms/1177728976), and is the ancestor of the Foster–Lyapunov method used for stability of queueing networks and stochastic systems.

This mission is the first of a series formalizing the book chapter by chapter.

Setting

A homogeneous discrete-parameter Markov chain on $\{0,1,2,\dots\}$ is given by a transition matrix $P=\{p_{ij}\}$ with $p_{ij}\ge0$ and $\sum_j p_{ij}=1$ for every $i$. The $m$-step transition probabilities $p_{ij}^{(m)}$ are the entries of $P^m$.

The first-passage probability $f_{ij}^{(n)}$ is the probability that the chain started in $i$ enters $j$ for the first time at step $n\ge1$; for $i=j$ it is the probability of first return at step $n$. The return probability is $f_{jj}=\sum_{n\ge1}f_{jj}^{(n)}$ and the mean recurrence time is $m_{jj}=\sum_{n\ge1}n f_{jj}^{(n)}\in[0,\infty]$. A state is positive recurrent if $f_{jj}=1$ and $m_{jj}<\infty$; the chain is positive recurrent if every state is.

The chain is irreducible if for every pair of states $(i,j)$ some $p_{ij}^{(n)}$ is positive, and aperiodic if for every state $k$ the greatest common divisor of $\{n\ge1:p_{kk}^{(n)}>0\}$ is $1$. A stationary distribution is a probability vector $\pi$ with $\pi=\pi P$, i.e. $\pi_j=\sum_i\pi_i p_{ij}$ for every $j$.

For the Poisson part, $T_0,T_1,\dots$ are independent interarrival times, each exponentially distributed with rate $\lambda>0$; the arrival epochs are $S_n=T_0+\dots+T_{n-1}$, and $N(t)=\#\{n\ge1:S_n\le t\}$ counts the arrivals in $[0,t]$.

Formalization targets

Goal: Theorem 1.2 (Foster's criterion)

An irreducible, aperiodic chain is positive recurrent if there exist $x_j\ge0$ with

$$\sum_{j=0}^\infty p_{ij}x_j\le x_i-1\quad(i\ne0),\qquad\sum_{j=0}^\infty p_{0j}x_j<\infty .$$

Milestones: the Markov chain theorems

• Theorem 1.1(a). In an irreducible, positive recurrent chain, $\pi_j=1/m_{jj}$ is a stationary distribution, and it is the only one.
• Theorem 1.1(c). If moreover the chain is aperiodic and all moments of $\pi$ are finite, then $\lim_{m\to\infty}p_{ij}^{(m)}=\pi_j$ for all $i,j$.

Milestones: the Poisson process and the exponential distribution

• Eqs. (1.11)–(1.14). The unique solution of $p_0'=-\lambda p_0$, $p_n'=-\lambda p_n+\lambda p_{n-1}$ with $p_0(0)=1$, $p_n(0)=0$ is $p_n(t)=(\lambda t)^n e^{-\lambda t}/n!$.
• Eq. (1.15). With exponential interarrival times,

$$\Pr\{N(t)\le n\}=\int_t^\infty\frac{\lambda(\lambda x)^n}{n!}e^{-\lambda x}dx=\sum_{i=0}^n\frac{(\lambda t)^ie^{-\lambda t}}{i!}.$$

• Eq. (1.16). Given $N(L)=k$, the arrival epochs have density $k!/L^k$ on $\{0<t_1<\dots<t_k<L\}$.
• Eq. (1.17) and its converse (p.21). The exponential law satisfies $\Pr\{T\le t_1\mid T\ge t_0\}=\Pr\{0\le T\le t_1-t_0\}$, and it is the only continuous distribution on $[0,\infty)$ that does.
• Nonhomogeneous Poisson law (p.22). With a continuous rate $\lambda(t)$ the forward equations have the unique solution $p_n(t)=e^{-m(t)}m(t)^n/n!$, $m(t)=\int_0^t\lambda(s)\,ds$.

Significance

Foster's criterion reduces positive recurrence, a statement about return times, to exhibiting one test function $x$ with negative drift outside a single state. In the book it is the tool that establishes the existence of steady state for imbedded chains of the M/G/1 and G/M/1 queues (Chapter 5); its generalizations are the standard stability proofs for queueing networks. Theorem 1.1 then supplies what positive recurrence buys: the stationary distribution exists, is unique, equals $1/m_{jj}$, and is the limit of the transition probabilities. The Poisson results justify the "Markovian" arrivals and services of Chapters 2–4.

All of these results are classical and proved in the literature; the book states Theorems 1.1 and 1.2 without proof. The Prove2Me platform already holds machine-checked versions of related Markov chain theorems in other missions (Levin–Peres–Wilmer's and Durrett's countable-chain convergence theorems), stated with different definitions and hypotheses. What this mission adds is a formal development in the book's own terms — first-passage probabilities $f_{jj}^{(n)}$, mean recurrence times $m_{jj}$, gcd periodicity — on which the later missions of the series (imbedded chains, birth–death processes) can build, together with a formal proof of Foster's criterion, which is not on the platform.

Difficulty

For Foster's criterion the natural first step, taking expectations of the drift inequality along the chain, only shows that the expected value of $x$ decreases while the chain stays away from $0$. Turning that into a bound on the expected return time to $0$ requires an optional-stopping or telescoping argument over a random time, with the value $x$ possibly unbounded, and a separate argument that positive recurrence of state $0$ propagates to all states of an irreducible chain. The book's hypotheses include aperiodicity, which the argument does not use.

For Theorem 1.1, identifying the stationary distribution with $1/m_{jj}$ requires relating the matrix powers $P^n$ to the first-passage probabilities (a renewal decomposition), and uniqueness over countably many states needs care with infinite sums. For the Poisson results, the difficulty is measure-theoretic: the distribution of the sum of $n+1$ exponential variables, and conditioning on the event $\{N(L)=k\}$ for the order-statistics property.

Formalization scope

States are natural numbers; the transition matrix is a real function $p:\mathbb N\times\mathbb N\to\mathbb R$ with nonnegative entries and rows summing to one (as a convergent series). The return probability and the mean recurrence time are valued in $[0,\infty]$, so null recurrence ($m_{jj}=\infty$) is representable. Irreducibility is the per-pair notion. Stationary equations are stated componentwise with convergent series.

In Foster's criterion the series $\sum_j p_{ij}x_j$ are required to converge for every $i$, which is the book's condition $\sum_j p_{0j}x_j<\infty$ together with the finiteness implicit in the inequalities for $i\ne0$; $x$ is real-valued and nonnegative. Dropping the convergence requirement would let a divergent row series (whose Lean sum is $0$) satisfy the inequality vacuously; allowing $x_j=\infty$ would make the hypothesis trivially satisfiable. Neither is permitted.

The closed forms stated explicitly are: $\pi_j=1/m_{jj}$ (Theorem 1.1(a), with both existence and uniqueness), the Poisson probabilities $(\lambda t)^ne^{-\lambda t}/n!$ (1.14), the Erlang tail integral and the Poisson CDF (1.15), the density $k!/L^k$ (1.16), and $e^{-m(t)}m(t)^n/n!$ for the nonhomogeneous law. Equations (1.14) and the nonhomogeneous law are stated as "solves the equations with the initial conditions if and only if equals the closed form", so both existence and uniqueness are asserted.

The Poisson results use random variables on a probability space, with Mathlib's expMeasure for the exponential law and cond for conditional probability. The derivation of the forward equations from the $o(\Delta t)$ axioms of §1.7 is not formalized; the Poisson law is reached from the equations and, separately, from exponential interarrival times.

Not formalized: Theorem 1.1(b) and the word "ergodic" in 1.1(c), which rest on the book's informal notion of ergodicity; Theorem 1.3, whose phrase "for Theorem 1.1 to be valid" for a continuous-time chain is not pinned down.

The Markov chain definitions are reusable by every later mission that studies an imbedded chain. Contributions welcome: proofs of the milestones, and supporting lemmas (Chapman–Kolmogorov, renewal decomposition of $p_{jj}^{(n)}$, class properties of recurrence).

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953), 355–360. https://doi.org/10.1214/aoms/1177728976

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

Bayesian mechanism design asks which collective decisions and payments a designer can implement when every agent holds private information, the type, drawn from a commonly known prior. Most of the classical theory (Myerson's optimal auction, the Myerson–Satterthwaite impossibility, the public goods results) assumes that types are independent. Once types are correlated, as they are when bidders' values share a common component, the theory changes in a way that is best read as a paradox: Crémer and McLean (Econometrica 1988) showed that a designer can then extract the entire surplus, leaving agents no information rents. This mission formalizes Chapter 6 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press 2015), which sets up Bayesian mechanism design in general, treats independent types, and proves the Crémer–McLean theorem, together with the one numbered result of Chapter 9, the impossibility theorem of Jehiel and Moldovanu for interdependent values.

Timeline of the results formalized here:

• Rochet (1987) characterized implementable decision rules by cyclical monotonicity; Proposition 6.1 is its interim version for independent types.
• Crémer and McLean (1988): under their condition on the prior, every direct mechanism can be made Bayesian incentive-compatible without changing its decision rule or interim payments (Proposition 6.4).
• Krishna and Maenner (2001): revenue equivalence for convex type sets and convex utilities (Proposition 6.2).
• Jehiel and Moldovanu (2001): with interdependent values, efficient decisions are generically not Bayesian implementable (Proposition 9.1).
• Kosenok and Severinov (2008): an identifiability condition added to Crémer–McLean gives ex post budget balance as well (Proposition 6.6).

Setting

There are finitely many agents $i \in I$ and a set $A$ of alternatives. Agent $i$ has a type $\theta_i \in \Theta_i$ and utility $u_i(a,\theta_i) - t_i$ from alternative $a$ and payment $t_i$. Types $\theta = (\theta_1,\dots,\theta_N) \in \Theta = \prod_i \Theta_i$ are drawn from a common prior $\mu$; $\mu(\cdot\mid\theta_i)$ is the conditional distribution of the others' types $\theta_{-i}$ given $\theta_i$. Types are independent if $\mu(\cdot\mid\theta_i)$ does not depend on $\theta_i$.

A direct mechanism $(q, t_1,\dots,t_N)$ is a decision rule $q:\Theta\to A$ and payment rules $t_i:\Theta\to\mathbb R$. It is Bayesian incentive-compatible (BIC) if for every $i$ and all $\theta_i,\theta_i'$,

$$\int_{\Theta_{-i}} u_i(q(\theta_i,\theta_{-i}),\theta_i) - t_i(\theta_i,\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i) \ \ge\ \int_{\Theta_{-i}} u_i(q(\theta_i',\theta_{-i}),\theta_i) - t_i(\theta_i',\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i).$$

The interim decision rule $Q_i(\theta_i)$ is the distribution of $q(\theta_i,\theta_{-i})$ given $\theta_i$, and the interim expected payment is $T_i(\theta_i) = \int t_i(\theta_i,\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i)$. A mechanism is ex post budget balanced if $\sum_i t_i(\theta) = 0$ for every $\theta$, and ex ante budget balanced if $\int_\Theta \sum_i t_i\,d\mu = 0$.

In §6.4 every $\Theta_i$ is finite and $\mu(\theta) > 0$ for every $\theta$. The prior satisfies the Crémer–McLean condition if for no agent $i$ and type $\theta_i$ there are weights $\lambda \ge 0$ on $\Theta_i\setminus\{\theta_i\}$ with

$$\mu(\theta_{-i}\mid\theta_i) = \sum_{\theta_i'\ne\theta_i}\lambda(\theta_i')\,\mu(\theta_{-i}\mid\theta_i')\quad\text{for all }\theta_{-i}.$$

Identifiability requires that for every full-support distribution $\nu\ne\mu$ some agent's type $\theta_i$ has a belief $\nu(\cdot\mid\theta_i)$ that is not a nonnegative combination of the beliefs $\mu(\cdot\mid\theta_i')$.

Formalization targets

Goal: Crémer–McLean (Proposition 6.4)

If $\mu$ satisfies the Crémer–McLean condition, then for every direct mechanism $(q,t)$ there is a BIC direct mechanism $(q,t')$ with

$$\sum_{\theta_{-i}} t_i(\theta_i,\theta_{-i})\,\mu(\theta_{-i}\mid\theta_i) = \sum_{\theta_{-i}} t_i'(\theta_i,\theta_{-i})\,\mu(\theta_{-i}\mid\theta_i)\quad\text{for all } i,\theta_i.$$

Milestones

1. Proposition 6.1 (independent types): $q$ is part of a BIC mechanism iff it is interim cyclically monotone, $\sum_{\kappa=1}^{k-1}\big(\int_A u_i(a,\theta_i^{\kappa+1})\,dQ_i(\theta_i^\kappa) - \int_A u_i(a,\theta_i^\kappa)\,dQ_i(\theta_i^\kappa)\big)\le 0$ for every cycle $\theta_i^k = \theta_i^1$.
2. Proposition 6.2 (independent types, convex type sets, convex utilities): two BIC mechanisms with $Q_i' = Q_i$ have $T_i' = T_i + \tau_i$.
3. Proposition 6.3 (independent types): every ex ante budget balanced mechanism has an equivalent ex post budget balanced one.
4. Proposition 6.5 (Farkas's alternative), already proved on the platform as Polyhedral.farkas_lemma.
5. Proposition 6.6 (Kosenok–Severinov): under Crémer–McLean and identifiability, every ex ante budget balanced mechanism has an equivalent BIC and ex post budget balanced one.
6. Proposition 9.1 (Jehiel–Moldovanu): in the linear interdependent-values model, under a regularity condition on first best rules and the weight condition $\alpha^i_{ai}/\alpha^i_{bi}\ne\sum_j\alpha^i_{aj}/\sum_j\alpha^i_{bj}$ for some $i,a,b$, no first best direct mechanism is BIC. It uses its own model (§9.3) and is not on the goal's proof path.

Significance

The Crémer–McLean theorem says that, with correlated finite types, incentive compatibility imposes essentially no constraint: every decision rule and every interim payment rule can be implemented. In a single-unit auction this gives full surplus extraction. The result is the benchmark against which the literature on risk aversion, limited liability, collusion and the genericity of priors (Robert 1991, Laffont–Martimort 2000, Heifetz–Neeman 2006) measures its departures, and Proposition 6.6 extends it to budget-balanced mechanisms, which is what bilateral trade and public goods applications need. Propositions 6.1–6.3 are the independent-types counterpart that the correlated case breaks: they show why revenue equivalence and the ex ante/ex post budget-balance equivalence hold there and fail here. Proposition 9.1 shows the opposite failure, for interdependent values, where efficient decisions cannot be implemented even without participation or budget constraints.

All results are proved in the literature (Kosenok–Severinov's proof is omitted in the book). Apart from Farkas's alternative (Proposition 6.5), which is proved on the platform, none of them is formalized in Mathlib or on the platform; the platform's other mechanism design results (dominant-strategy results in a valuation model, revenue equivalence for symmetric independent auctions) do not cover correlated types.

Difficulty

For the goal the difficulty is the uniformity of the construction: a single payment adjustment must make truth-telling optimal against every possible deviation of every type of every agent, while leaving each type's expected payment unchanged. The obvious scoring-rule adjustment, charging $-\ln\mu(\theta_{-i}\mid\theta_i')$, changes interim payments, and removing that change is where the Crémer–McLean condition enters. For Proposition 6.2 the envelope argument must handle convex type sets that are not open and utilities that are only convex, not differentiable. For Proposition 9.1 the obvious argument differentiates interim utility twice; the proposition does not assume that interim utility is twice differentiable, so that regularity has to be derived from the hypotheses on the interim probabilities.

Formalization scope

Three definition files carry the three models. Independent types (§6.2–6.3): type sets are arbitrary measurable spaces, the prior is the product of probability measures $\rho_i$, and interim quantities are integrals against it. Finite correlated types (§6.4): finite type sets, a prior $\mu:\Theta\to\mathbb R$ with $\mu(\theta)>0$ and $\sum_\theta\mu(\theta)=1$, and conditional beliefs $\mu(\theta_{-i}\mid\theta_i) = \mu(\theta)/\mu(\theta_i)$; the alternative set $A$ is arbitrary. Interdependent values (§9.3): finite $A$, signals in $[0,1]^A$ with positive densities, independent across agents, linear utilities with nonzero weights $\alpha^j_{ai}$.

Committed conventions and explicit formulas:

• The Crémer–McLean condition uses nonnegative weights without a sum-to-one constraint, as Definition 6.7 prints it.
• "Equivalent" in Propositions 6.4 and 6.6 means the same decision rule and the same interim expected payments at truthful reports, as Proposition 6.4 states; in Proposition 6.3 it is the report-by-report notion, which under independence is equality of the interim payment rules $T_i$.
• Proposition 6.2 adds continuity of $u_i(a,\cdot)$ on $\Theta_i$, and Proposition 6.3 adds at least two agents; without them the printed statements are false.
• Measurability, which the book omits throughout, is made explicit: decision rules are measurable, and the payment sections and utilities are integrable against the relevant interim distributions.
• In Proposition 9.1 the partial derivatives are derivatives within the closed cube $[0,1]^K$, and the weight condition is the displayed ratio inequality.

A trivializing formalization of the goal, one that proves it only for mechanisms that are already incentive compatible, or with a payment rule that is not a function of the reported type profile, or with "equivalent" weakened to "some BIC mechanism exists", is ruled out: the statement quantifies over every direct mechanism and fixes both the decision rule and every interim payment.

Reusable infrastructure: finite conditional expectations under a full-support prior, the Crémer–McLean and identifiability conditions, and the interim model with product priors. Proofs of any milestone and of the goal, including via the Farkas reference, are welcome.

Selected references

• 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
• J. Crémer and R. P. McLean, "Full extraction of the surplus in Bayesian and dominant strategy auctions", Econometrica 56(6), 1988. https://doi.org/10.2307/1913096
• G. Kosenok and S. Severinov, "Individually rational, budget-balanced mechanisms and allocation of surplus", Journal of Economic Theory 140(1), 2008.
• P. Jehiel and B. Moldovanu, "Efficient design with interdependent valuations", Econometrica 69(5), 2001. https://doi.org/10.1111/1468-0262.00237
• V. Krishna and E. Maenner, "Convex potentials with an application to mechanism design", Econometrica 69(4), 2001. https://doi.org/10.1111/1468-0262.00225
• J.-C. Rochet, "A necessary and sufficient condition for rationalizability in a quasi-linear context", Journal of Mathematical Economics 16(2), 1987. https://doi.org/10.1016/0304-4068(87)90007-3

Motivation

Revenue management decides how much of a fixed, perishable capacity (airline seats, hotel rooms) to sell, and at what price. Classical single-leg models assume a known demand distribution for each fare class and maximise expected revenue. Many carriers instead use bid-price controls: a request is accepted when its fare is at least a threshold ("bid price") that rises as capacity is sold. Fares then need not fall into a few predefined classes; a fare may be any number in an interval.

Ball and Queyranne (Oper. Res. 57(4), 2009) study booking with competitive analysis from the theory of online algorithms. A policy is judged by the worst case, over all request sequences, of the ratio between its revenue and the revenue of a seller who knows the whole sequence in advance; no distribution is assumed. For two fare classes the best ratio is $1/(2 - r)$; for $m$ classes it is $1/\Delta$. For fares ranging over a whole interval $[f_{\min}, f_{\max}]$ with $r = f_{\min}/f_{\max}$, the paper shows that the best ratio is $1/(1 - \ln r)$ and that an explicit bid-price policy attains it. This mission formalizes that result (§2.2 of the paper). The constant $1/(1 - \ln r)$ is the same as in the threat-based one-way trading algorithm of El-Yaniv, Fiat, Karp and Turpin (2001), which works in a different model.

Setting

A seller holds capacity $n > 0$, a real number. In the continuous problem demands and accepted quantities are nonnegative reals and orders may be partially accepted. Fix fares $0 < f_{\min} < f_{\max}$ and the maximum discount ratio $r = f_{\min}/f_{\max} \in (0,1)$. A request has a fare $O \in [f_{\min}, f_{\max}]$ and a quantity $d > 0$. An instance $I$ is a finite sequence of requests, revealed one at a time. On each arrival the seller irrevocably accepts some $a \in [0, \min(d, \text{remaining capacity})]$, and its revenue $v'(I)$ is $\sum O\,a$. The optimal offline revenue $v^*(I)$ is the maximum of $\sum_i O_i x_i$ over $0 \le x_i \le d_i$, $\sum_i x_i \le n$.

A deterministic online policy chooses each accepted quantity from the earlier requests and the current one only. Its competitive ratio is

$$\mathrm{CR}(A) = \inf_{I \,:\, v^*(I) > 0} \frac{v'_A(I)}{v^*(I)}.$$

A randomized policy is a random choice $A(\omega)$ of a deterministic policy, and its ratio uses the expected revenue $\mathbb{E}[v'_{A(\omega)}(I)]$.

Bid-price policies are built from protection levels $\theta(f)$, nonincreasing in $f$. The paper's choice is Eq. (15):

$$\theta(f) = \frac{\ln f_{\max} - \ln f}{\ln f_{\max} - \ln f_{\min}}\Big(1 - \frac{1}{1 - \ln r}\Big)n, \qquad f_{\min} \le f \le f_{\max}.$$

The protection-level control function is $Q(f) = n - \theta(f)$, and the order quantity control function is $P(q) = \min\{f \in [f_{\min}, f_{\max}] : Q(f) \ge q\}$ for $0 \le q \le n$. Let $\hat q$ be the quantity accepted so far and $\hat q(f)$ the part of it accepted at fares $\le f$. The protection-level control policy $A_\theta$ accepts from a request with fare $O$ the largest $\alpha \le d$ with $\alpha + \hat q(f) \le Q(f)$ for every $f \in [O, f_{\max}]$. The order quantity control policy $A'_\theta$ rejects the request if $O < P(\hat q)$, and otherwise accepts the largest $\alpha \le d$ with $P(\alpha + \hat q) \le O$. Finally $\rho = 1/(1 - \ln r)$ and $V(q) = \int_0^q P(s)\,ds$.

Formalization targets

Goal: Theorem 7 (p. 959)

$$v'_{A_\theta}(I) \ \ge\ \frac{1}{1 - \ln r}\, v^*(I) \quad\text{and}\quad v'_{A'_\theta}(I) \ \ge\ \frac{1}{1 - \ln r}\, v^*(I)$$

for every instance $I$ with all fares in $[f_{\min}, f_{\max}]$, with $\theta$ given by Eq. (15). Both bid-price policies achieve competitive ratio at least $1/(1 - \ln r)$. The paper claims "at least", and so does the goal.

Milestones

• Eq. (5) (p. 956): $P(Q(f)) \le f$ for $f_{\min} \le f \le f_{\max}$.
• Lemma 2 (p. 959): closed forms (16) and (17). $P(q) = f_{\min}$ and $V(q) = q f_{\min}$ for $q < n\rho$; $P(q) = f_{\max} r^{(n-q)/(n(1-\rho))}$ and $V(q) = nP(q)/(1 - \ln r)$ for $n\rho \le q \le n$.
• Proof of Theorem 6, first display (p. 959): on the geometric fares $f_i^{(m)} = f_{\max} r^{(i-1)/(m-1)}$ of Eq. (13), $m \ge 2$, no policy has competitive ratio above $c^{(m)} = 1/(m - (m-1) r^{1/(m-1)})$.
• Theorem 6 (p. 959): no policy, deterministic or randomized, has competitive ratio larger than $1/(1 - \ln r)$.

Significance

The result. Theorems 6 and 7 together give the exact optimal competitive ratio of online booking when fares range over an interval: $1/(1 - \ln r)$, attained by bid-price policies whose protection levels are linear in $\ln f$. The guarantee holds for every demand sequence with no forecast. It decreases slowly as the fare spread grows: it is about $0.59$ at $r = 1/2$ and about $0.42$ at $r = 1/4$. It is the limit of the $m$-fare ratios $1/\Delta$ as the fare grid becomes dense. The paper derives its discrete bid-price policy (§2.3) from this continuous one.

Formalizing it. The results are proved in the paper; none is known to be machine-checked. The proof of Theorem 7 for the protection-level policy is only sketched in the paper, as an interval-rearrangement argument around Figure 7, and Lemma 2 is proved only in the online companion. A formal proof closes both gaps. The mission also produces a reusable model of online booking with real-valued fares, sized requests, an offline optimum, deterministic and randomized nonanticipative policies, and competitive ratios restricted to a fare set.

Difficulty

The lower bound must hold for every admissible instance, including sequences where fares go up and down and the offline optimum is not a closed form. Both policies are defined by suprema over constraints: for $A'_\theta$ through the minimum defining $P$, and for $A_\theta$ through protection constraints on nested cumulative sums over a continuum of fares. The accepted orders of $A_\theta$ need not form consecutive blocks of capacity, so the analysis of one policy does not transfer to the other. The paper sketches the protection-level case only informally, around a figure. Theorem 6 is a bound against randomized policies, which may hedge between accepting and rejecting cheap requests. No single hard instance defeats them, and the bound must connect the finite-grid bounds $c^{(m)}$, which involve real powers $r^{1/(m-1)}$, to the constant $1/(1-\ln r)$. Lemma 2 needs the minimum defining $P$ to be computed exactly and then integrated.

Formalization scope

• Capacity $n$ is real with $n > 0$; fares are reals with $0 < f_{\min} < f_{\max}$, and $r$ is f_min / f_max; $\ln$ is Real.log and real powers are Real.rpow.
• Requests are sized (a real fare and a quantity qty > 0); the paper's unit orders with fractional acceptance are qty = 1. Instances are lists, and the admissibility hypothesis that every fare lies in $[f_{\min}, f_{\max}]$ is explicit. Theorems 6 and 7 are false without it.
• A deterministic policy is any function from the history (earlier requests with their accepted quantities) and the current request to a proposed quantity; the run clips proposals to $[0, \min(d, n - \hat q)]$. A randomized policy is an arbitrary probability space with a measurable revenue for each admissible instance. The revenue is bounded by $n f_{\max}$, so the Bochner integral is a genuine expectation.
• $v^*$ is the sSup of offline revenues (nonempty, bounded, attained). Competitive ratios are sInfs over admissible instances with positive optimum (nonempty, bounded below by $0$). "At least $c$" in Theorem 7 is stated per instance as $c\,v^* \le v'$.
• $P$ is defined from $Q$ by an sInf over $\{f \in [f_{\min}, f_{\max}] : Q(f) \ge q\}$, not by the closed form (16). $V$ is an interval integral. $A_\theta$ checks its constraint over the whole continuum $[O, f_{\max}]$, and $A'_\theta$ also requires $\alpha + \hat q \le n$ so that $P$ is evaluated on its domain.
• A trivializing formalization — defining $P$ or $V$ by the closed forms of Lemma 2, replacing the policies' sup rules or the protection levels (15), checking protection constraints on a finite grid of fares, dropping the fare interval, or letting the offline optimum be a formula — is ruled out by the definitions above.
• Useful infrastructure: monotonicity of $Q$ and $P$, invariants of the policies' runs (the protection constraints hold after every step), a description of the offline optimum as a greedy fill by fare, and averaging over a distribution of instances. General lemmas about online policies and offline optima are reusable in the two-fare and multifare missions.

Selected references

• M. O. Ball, M. Queyranne, Toward Robust Revenue Management: Competitive Analysis of Online Booking, Operations Research 57(4):950–963, 2009. https://doi.org/10.1287/opre.1080.0654
• R. El-Yaniv, A. Fiat, R. M. Karp, G. Turpin, Optimal Search and One-Way Trading Online Algorithms, Algorithmica 30(1):101–139, 2001. https://doi.org/10.1007/s00453-001-0003-0
• A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

Motivation

Airlines, hotels and rental firms sell a fixed stock of capacity to customers who arrive over time and pay different prices for the same unit. Classical revenue management, from Littlewood's two-fare rule (1972) to the dynamic programs of Brumelle and McGill (1993), decides how much capacity to hold back for high-fare customers from a demand forecast. When demand is new, volatile or unknown, no reliable forecast is available.

Ball and Queyranne (Oper. Res. 57(4), 2009) study the problem as an online algorithm instead, with no distributional assumption at all. A policy is judged by its competitive ratio: the worst case, over every demand sequence, of the revenue it earns divided by the revenue of a clairvoyant seller who knew the whole sequence in advance. For $m$ fare classes they compute the best achievable ratio exactly and show that it is attained by the nested protection-level policies that practitioners already use. This mission formalizes that $m$-fare result.

Setting

A seller holds $n > 0$ units of capacity. There are $m \ge 2$ fare classes with fares $f_1 > f_2 > \dots > f_m > 0$. A request names a class and a quantity $d > 0$; an instance $I$ is a finite sequence of requests, of any classes in any order. Quantities are real numbers and requests may be partly accepted (the continuous problem).

A deterministic online policy decides how much of each request to accept when it arrives. It knows the earlier requests and what it accepted from them, but not what comes later. Its decision is clipped to the request's size and the remaining capacity. Its revenue $R(A, I)$ is the sum of fare times accepted quantity. The offline optimum $v^*(I)$ is the largest revenue of any feasible acceptance vector $0 \le x_k \le d_k$, $\sum_k x_k \le n$. The competitive ratio of $A$ is

$$c(A) = \inf_{I:\ v^*(I) > 0} \frac{R(A, I)}{v^*(I)}.$$

A randomized policy draws a deterministic policy $A(\omega)$ at random, $\omega \sim \mu$ for a probability measure $\mu$. Its ratio $c(\mu, A)$ uses the expected revenue $\mathbb{E}_\mu[R(A(\omega), I)]$ in place of $R(A, I)$.

The paper's constants are

$$\Delta = m - \sum_{i=2}^{m} \frac{f_i}{f_{i-1}}, \qquad \theta_i = \frac{n}{\Delta}\Bigl(i - \sum_{j=1}^{i} \frac{f_{j+1}}{f_j}\Bigr)\ (1 \le i \le m-1), \quad \theta_m = n,$$

and the protection-level controls $Q_i = n - \theta_{i-1}$ for $1 \le i \le m+1$, with $Q_1 = n$ and $Q_{m+1} = 0$. The control $Q_i$ caps the total quantity sold to classes $i, \dots, m$. The order quantity control function is $P(q) = f_i$ for $Q_{i+1} < q \le Q_i$, with $P(0) = 0$; it gives the lowest fare still accepted once $q$ units are sold.

Two policies use these controls. Write $\hat q$ for the quantity sold so far and $\hat q(f_j)$ for the quantity sold so far at fares $\le f_j$.

• The protection-level policy $A_\theta$ gives a class-$c$ request of size $d$ the amount $\sup\{\alpha \in [0, d] : \alpha + \hat q(f_j) \le Q_j \text{ for all } j \le c\}$.
• The order quantity policy $A'_\theta$ gives it $0$ if $f_c < P(\hat q)$, and otherwise $\sup\{\alpha \in [0, d] : \alpha + \hat q \le n,\ P(\alpha + \hat q) \le f_c\}$.

Formalization targets

Goal — Theorem 5 (p. 958)

For every $m \ge 2$, all fares $f_1 > \dots > f_m > 0$ and every $n > 0$,

$$c(A_\theta) = c(A'_\theta) = \frac{1}{\Delta}.$$

Both directions are part of the claim: each policy guarantees a $1/\Delta$ fraction of the offline optimum on every instance, and some instances bring it down to exactly that fraction.

Milestone — Lemma 1 (p. 957)

The controls satisfy

$$f_i(Q_i - Q_{i+1}) = \tfrac{n}{\Delta}(f_i - f_{i+1})\ (1 \le i \le m-1), \qquad f_m(Q_m - Q_{m+1}) = \tfrac{f_m n}{\Delta},$$ $$\sum_{i=i'}^{m} f_i(Q_i - Q_{i+1}) = f_{i'} \tfrac{n}{\Delta} \quad (1 \le i' \le m).$$

Milestone — Theorem 4 (p. 957)

No policy does better. For every deterministic policy $B$, and every randomized policy $(\mu, A)$ whose revenue on each instance is measurable in $\omega$,

$$c(B) \le \frac{1}{\Delta}, \qquad c(\mu, A) \le \frac{1}{\Delta}.$$

Significance

Theorems 4 and 5 together settle the robust $m$-fare problem in the continuous setting. The best worst-case guarantee, over all deterministic and randomized online policies, is $1/\Delta$. The protection levels of Eq. (7) achieve it, with either implementation, protection-level control or order-quantity control. Nested booking therefore needs no forecast to be optimal in this sense, and $1/\Delta$ is an explicit guarantee a practitioner can compute from the fares alone. For $m = 2$ and $f_2/f_1 = r$ it is the two-fare ratio $1/(2 - r)$. As the fares get denser, the paper's §2.2 obtains the bid-price bound $1/(1 - \ln r)$ as a limit, reusing Theorem 4.

The paper proves Theorem 4 and Theorem 5 in the text; Lemma 1's proof is in the online companion. None of these results has a machine-checked proof. A formal development pins down what the paper leaves informal (partial orders at the thresholds, the $\sup$ in the policy definitions) and yields a reusable library of online booking policies, offline optima and competitive ratios.

Difficulty

The upper bound (Theorem 4) needs a lower bound on every policy, randomized ones included. Exhibiting one hard instance for each deterministic policy does not bound a randomized policy, whose expected revenue averages over its choices, and the bound must hold uniformly over an arbitrary probability space of such choices.

The lower bound in Theorem 5 needs a guarantee on every instance: arbitrary interleavings of classes, arbitrary sizes, and partial acceptances at the control thresholds. It is not enough to check the extreme instances that fix the protection levels. The order-quantity policy is harder than the protection-level policy, because it cuts off lower fares based on the total sold rather than per class, so the revenue collected before and after the critical threshold must be accounted for separately. The offline optimum is a supremum over a linear program and has to be bounded from above on arbitrary instances.

Formalization scope

• Fares are a function f : ℕ → ℝ read 1-based. The hypotheses are StrictAntiOn f (Set.Icc 1 m) and 0 < f m, with 2 ≤ m. The paper's §2.1 says $m \ge 3$; every statement here is claimed for $m \ge 2$, a strengthening, and $m = 2$ is the paper's two-fare case.
• Capacity is a real n with 0 < n. A request is a class cls : ℕ with a real qty. An instance is a List of requests with $1 \le$ cls $\le m$ and qty $> 0$. The paper's unit orders with fractional acceptance are the case qty = 1.
• A deterministic policy is any function from the booking record so far (requests and accepted quantities) and the current request to a proposed quantity; the run clips it to $[0, \min(d, n - \text{sold})]$. Seeing its own past acceptances gives a policy no information beyond the past requests, since those acceptances are determined by them.
• Randomized policies live on an arbitrary probability space; expected revenue is a Bochner integral, and the revenue on each instance is required to be measurable in $\omega$. It is bounded, so it is then integrable.
• $v^*$ is a real sSup of a nonempty set that is bounded above. Competitive ratios are real sInfs over instances with $v^*(I) > 0$, a nonempty set bounded below by $0$.
• $Q$ is defined from Eqs. (8)–(9), $Q_i = n - \theta_{i-1}$. The paper's text also writes $Q(f) = n - \theta(f)$ with $\theta_i = \theta(f_i)$, which is off by one index. $P$ picks the largest index $i \le m$ with $q \le Q_i$. The policies use it only on $[0, n]$, and $A'_\theta$ carries the constraint $\alpha + \hat q \le n$ explicitly.
• The sup in $A_\theta$ ranges over the fares $f_j \ge f_c$, i.e. the classes $j \le c$.

Theorem 5 is an equality. A statement of only $c \ge 1/\Delta$, or one restricted to the extreme instances $I_1, \dots, I_m$ or to low-before-high arrival orders, would be a different and weaker theorem. So would treating $v^*(I_i) = f_i n$ as a definition instead of a consequence of the offline optimum.

A complete development needs finite sums over Lists and Fin, sSup/sInf on ℝ, the Bochner integral, and facts about the offline optimum of a single-resource allocation. The booking model and offline-optimum lemmas are reusable for the two-fare and bid-price results of the same paper; general lemmas about the offline optimum are welcome contributions.

Selected references

• M. O. Ball, M. Queyranne, Toward Robust Revenue Management: Competitive Analysis of Online Booking, Operations Research 57(4):950–963, 2009. https://doi.org/10.1287/opre.1080.0654
• K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4(2):111–123, 2005. https://doi.org/10.1057/palgrave.rpm.5170134
• S. L. Brumelle, J. I. McGill, Airline seat allocation with multiple nested fare classes, Operations Research 41(1):127–137, 1993. https://doi.org/10.1287/opre.41.1.127
• A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9780511546563
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2005. https://doi.org/10.1007/b139000