Mechanism Design

Motivation

Myerson's optimal auction (Myerson 1981) maximizes a seller's expected revenue when buyers have independent private values, but it is a sealed-bid mechanism: every buyer reports a value, and the allocation and payments are computed from all reports at once. Real sellers more often post prices: buyers arrive, each sees a take-it-or-leave-it price, and buys or leaves. Chawla, Hartline, Malec and Sivan (arXiv:0907.2435) ask how much revenue such simple mechanisms lose. Their strongest notion is the order-oblivious posted-price mechanism (OPM): the prices are fixed in advance, and the guarantee must hold whatever order the buyers arrive in, even an adversarial one.

The tool behind the guarantee for sellers of $k$ identical units is a prophet inequality. In the single-choice version, a gambler inspects independent random rewards one at a time and must accept or reject each on the spot; Krengel and Sucheston, and Samuel-Cahn (Ann. Probab. 1984), showed that a single fixed threshold earns at least half of what a prophet who sees all rewards earns. The paper extends Samuel-Cahn's threshold rule to $k$ choices (Appendix D.2) and turns it into a revenue guarantee (Theorem 10).

Setting

There are $n$ agents $[n]$. Agent $i$'s value $v_i$ for being served is drawn independently from a distribution $F_i$ with density $f_i$; the virtual valuation is $\phi_i(v) = v - (1 - F_i(v))/f_i(v)$ (Definition 1), and $F_i$ is regular if $\phi_i$ is non-decreasing (Definition 2). The seller may serve any set of agents in a downward-closed set system $\mathcal J$; this mission uses the $k$-uniform matroid, where a set is feasible exactly when it has at most $k$ members.

A mechanism $M$ maps reported values $\mathbf v$ to an allocation $M(\mathbf v) \in \mathcal J$ and payments $\pi_i(\mathbf v)$. It is truthful if reporting the true value is a dominant strategy and no agent ever gets negative utility. Its expected revenue is $\mathcal R^M = \mathbb E_{\mathbf v}[\sum_i \pi_i(\mathbf v)]$, and $\mathcal R^{\mathcal M}$ denotes the revenue of Myerson's mechanism, the largest over truthful mechanisms (Theorem 19).

Given prices $\mathbf p$ and values $\mathbf v$, agent $i$ desires service if $v_i \ge p_i$. Let $\mathcal S_{\mathbf v}$ be the class of maximal feasible sets of desiring agents. When agents arrive in an arbitrary order and each buys if it desires service and can still be feasibly served, the set of buyers lies in $\mathcal S_{\mathbf v}$. The paper's pessimistic revenue estimate is

$$\mathcal R^{\mathrm{obl}}_{\mathbf p} = \mathbb E_{\mathbf v \sim \mathbf F}\ \min_{S \in \mathcal S_{\mathbf v}} \sum_{i \in S} p_i .$$

For the prophet inequality, $X_1, \dots, X_n$ are independent nonnegative random variables with order statistics $X_{(1)} \ge \dots \ge X_{(n)}$, and $(x)^+ = \max(0, x)$. The threshold rule with threshold $c$ picks indices $t_1(c), \dots, t_k(c)$, where $t_i(c)$ is the lesser of $n-k+i$ and the $i$-th smallest index $j$ with $X_j \ge c$ (or $n - k + i$ if there is none). The numbers $a^*$ and $b^*$ are the unique solutions of

$$a = \sum_{i=1}^k \mathbb E\big(X_{(i)} - a/k\big)^+, \qquad b = \sum_{i=1}^n \mathbb E\big(X_i - b/k\big)^+ .$$

Formalization targets

Goal: Theorem 10 (p. 9)

$$\exists\, \mathbf p\ \ \forall M \text{ truthful}:\qquad \mathcal R^M \le 2\, \mathcal R^{\mathrm{obl}}_{\mathbf p}$$

for every instance with regular distributions and a $k$-uniform matroid constraint. The prices are chosen once, before the mechanism it is compared with; this is the paper's "$\mathcal R^{\mathrm{obl}}_{\mathbf p}$ 2-approximates $\mathcal R^{\mathcal M}$".

Milestones

1. Proposition 1 (p. 5): under regularity, the expected revenue of a truthful mechanism equals its expected virtual surplus $\mathbb E[\sum_{i \in M(\mathbf v)} \phi_i(v_i)]$ (with the lowest type receiving zero utility).
2. $a^*$ and $b^*$ exist and are unique (App. D.2, p. 18).
3. The claim $a^* \le b^*$ (App. D.2, p. 18).
4. Theorem 24 (p. 18), the $k$-choice prophet inequality: for $a^* \le k c \le b^*$,

$$\sum_{i=1}^k \mathbb E\big[X_{(i)}\big] \le 2 \sum_{i=1}^k \mathbb E\big[X_{t_i(c)}\big].$$

Significance

The theorem says that a seller of $k$ identical units can fix one price per buyer, ignore the arrival order entirely, and still collect half of the optimal revenue. The factor 2 is tight: Appendix D.2 gives a single-item example with two buyers where no order-oblivious pricing does better. Corollary 11 extends the result to partition matroids, and Theorem 24 is reused for the graphical-matroid result (Theorem 12, App. D.3). Theorem 24 is a statement in optimal stopping independent of mechanism design, and $k$-choice prophet inequalities are now a standard tool for online allocation.

The results are proved in the paper (preprint arXiv:0907.2435v2; a conference version appeared at STOC 2010). To our knowledge none of them, nor any prophet inequality, has a machine-checked proof; Mathlib has independence of random variables but no order statistics, stopping-rule prophet inequalities, or Myerson's revenue characterization in this multi-agent dominant-strategy form. A related single-unit, Bayesian-incentive-compatible form of Proposition 1 exists on the platform (MechanismDesign.Auctions.revenue_eq_virtual_surplus), in a different model.

Difficulty

The threshold rule picks the first values above $c$, not the largest, and its picks are dependent random indices; the expectation $\mathbb E[X_{t_i(c)}]$ does not factor. The obvious comparison of the gambler with the prophet term by term fails, because the gambler can exhaust its $k$ picks on early, small values. The bound has to balance two events: either at least $k$ values reach $c$, or a value is picked whenever it exceeds $c$; independence enters exactly in the second. The rule also has forced picks at the end of the sequence, which must be handled as stated.

On the mechanism side, $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ is a minimum over an adversarially chosen family, not the revenue of one run, so it cannot be read off from a single sequential mechanism. Proposition 1 needs the full revenue-equivalence argument: monotone allocations, the payment identity, and an integration by parts against the density.

Formalization scope

• Distributions: each $F_i$ has a bounded support $[\underline v_i, \overline v_i]$ with $0 \le \underline v_i$, and a measurable density positive on it (a pinned convention; the paper says only "with density $f_i$"). Regularity is required on the support. The prior is the product of the marginals.
• Mechanisms: deterministic, dominant-strategy incentive compatible and ex-post individually rational on the type space, with measurable allocation events and measurable, integrable payments. Payments of unserved agents are not forced to be zero.
• $\mathcal R^{\mathcal M}$ is not constructed. The goal is stated against every truthful mechanism, which by Theorem 19 is equivalent. Quantifier order matters: "for every mechanism there are prices" is a weaker statement and is not the goal.
• Proposition 1 carries the normalization that an agent of the lowest type gets zero utility, which the paper presupposes on p. 12.
• $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ is a genuine minimum over the finite, nonempty family $\mathcal S_{\mathbf v}$; maximality is essential, since without it the empty set makes the estimate $0$ and the goal false. Prices are arbitrary reals.
• $a^*$ and $b^*$ are characterised by their equations as hypotheses, not defined by an infimum. Order statistics count multiplicity. Lean indices are 0-based. The threshold rule includes the page's forced picks $t_i(c) = n - k + i$; it is not replaced by a pure threshold rule. Theorem 24 and the claims about $a^*, b^*$ assume $1 \le k \le n$; the goal assumes nothing about $k$.
• Out of scope: non-regular distributions (ironing), Corollary 11, and the p. 19 identity rewriting $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ as a sum of virtual values (a proof step, not a milestone).

Useful reusable infrastructure: order statistics and their measurability, Samuel-Cahn-type threshold rules, and Myerson's payment identity for dominant-strategy mechanisms. Proofs of any milestone, and supporting lemmas on these objects, are welcome.

Selected references

• S. Chawla, J. D. Hartline, D. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, arXiv:0907.2435v2, 2010 (STOC 2010). https://arxiv.org/abs/0907.2435
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• E. Samuel-Cahn, Comparison of Threshold Stop Rules and Maximum for Independent Nonnegative Random Variables, Annals of Probability 12(4), 1984. https://doi.org/10.1214/aop/1176993150

Motivation

A seller who knows the distributions of buyers' values can maximise expected revenue with Myerson's optimal mechanism (Myerson 1981): collect bids, compute virtual values, serve a feasible set of maximum virtual surplus, and charge threshold payments. Real sellers seldom run such auctions. They post prices: a buyer is offered a take-it-or-leave-it price and either accepts or walks away. Posted prices need no bidding, involve no competition between buyers, and are trivially truthful. The question is how much revenue they give up.

Chawla, Hartline, Malec and Sivan (arXiv:0907.2435, STOC 2010) answer this for a range of feasibility constraints with a single construction, the sequential posted-price mechanism (SPM) $\mathcal S$. For general matroids it loses at most a factor $2$ (Theorem 5). For uniform and partition matroids, that is, multi-unit sales and unions of multi-unit sales, it loses at most a factor $e/(e-1)\approx1.58$ (Theorem 6), and the paper shows this factor is tight for its mechanism. This mission targets Theorem 6.

Timeline. Myerson (1981) characterised the optimal single-parameter mechanism. Blumrosen and Holenstein (2008) showed that the best single-unit SPM can be a factor $\sqrt{\pi/2}$ below Myerson's revenue even with i.i.d. buyers. Chawla, Hartline and Kleinberg (EC 2007) used posted prices to approximate multi-parameter unit-demand pricing. Chawla, Hartline, Malec and Sivan (2010) gave the matroid, partition-matroid and matroid-intersection bounds. Yan (SODA 2011) explained the $e/(e-1)$ factor through the correlation gap of submodular functions and sharpened it for $k$ units to $1-k^ke^{-k}/k!$.

Setting

There are $n$ agents. Agent $i$ has a private value $v_i$ for being served, drawn independently from a distribution $F_i$ with density $f_i$. The virtual value is $\varphi_i(v)=v-\frac{1-F_i(v)}{f_i(v)}$, and $F_i$ is regular if $\varphi_i$ is non-decreasing. The seller may serve any set in a downward-closed family $\mathcal J\subseteq2^{[n]}$.

A partition matroid assigns each agent $i$ to a part $\mathrm{part}(i)$ and each part $b$ a capacity $\mathrm{cap}(b)\in\mathbb N$. A set is feasible iff it contains at most $\mathrm{cap}(b)$ agents of every part $b$. With one part of capacity $k$ this is the $k$-uniform matroid: at most $k$ agents are served.

A truthful mechanism $M$ maps a value vector $\mathbf v$ to a feasible set $M(\mathbf v)$ and payments $\pi_i(\mathbf v)$. It is dominant-strategy incentive compatible and individually rational. Its expected revenue is $\mathcal R^M=\mathbb E[\sum_i\pi_i(\mathbf v)]$, and $q^M_i=\Pr[i\in M(\mathbf v)]$ is its service probability for agent $i$.

The sequential posted-price mechanism $\mathcal S$ built from $M$ sets the price $p_i=F_i^{-1}(1-q^M_i)$ for agent $i$, so that agent $i$ accepts with probability exactly $q^M_i$. It approaches the agents one at a time in decreasing order of price ($\sigma$ is the ordering). It offers agent $i$ the price $p_i$ if adding $i$ to the agents already served keeps the set feasible. The agent accepts iff $p_i\le v_i$. Its expected revenue is $\mathcal R^\sigma_{\mathbf p}$.

Formalization targets

Goal: Theorem 6, partition matroids

For every partition matroid, every truthful $M$, and $\mathcal S$ built from $M$ as above,

$$\mathcal R^M\le\frac{e}{e-1}\,\mathcal R^\sigma_{\mathbf p}.$$

Taking $M$ to be Myerson's mechanism gives the paper's statement.

Milestones

1. Lemma 2 (regular case): $\mathcal R^M\le\sum_ip^M_iq^M_i$ with $p^M_i=F_i^{-1}(1-q^M_i)$.
2. Rank bound (§4): $\sum_{i\in S}q^M_i\le\operatorname{rank}(S)$ for every set $S$; for a part $b$ this reads $\sum_{\mathrm{part}(i)=b}q^M_i\le\mathrm{cap}(b)$.
3. Single-unit revenue formula (App. C.2): $\mathcal R^{\mathcal S}=\sum_kc_kp_kq_k$ with $c_k=\prod_{j<k}(1-q_j)$, positions in offer order.
4. Lemma 20: with $p$ defined by $\sum_kp_kq_k=p\sum_kq_k$ (equation (2)) and prices decreasing, $p\sum_kc_kq_k\le\sum_kc_kp_kq_k$.
5. Display (3): if $\sum_kq_k=s\le1$, then $p\sum_kc_kq_k=p(1-\prod_k(1-q_k))\ge p(1-(1-s/n)^n)\ge(1-1/e)ps$.
6. Theorem 21: the goal for the $1$-uniform matroid.
7. Theorem 22: the goal for the $k$-uniform matroid, every $k$.

Significance

The theorem shows that a mechanism with no bidding loses at most about $37\%$ of the optimal revenue when the constraint is a union of multi-unit supplies. That covers selling several kinds of goods, each in limited stock, to single-minded buyers. The prices are computed once from the distributions. The order is fixed before any value is seen. No agent's payment depends on another agent's report. The factor is tight for this mechanism (App. C.2), and the same template (prices from service probabilities, decreasing order) gives factor $2$ for all matroids and $m+1$ for intersections of $m$ matroids.

On the formal side, the paper's results are proved but none is machine-checked as far as we know. The platform has Myerson-type results for a single unit with Bayesian incentive compatibility and a common support (Börgers), and for i.i.d. buyers with a fixed number of units (Talluri and van Ryzin). Neither covers independent, non-identical buyers under a set-system constraint with dominant-strategy truthfulness. A complete development would include the ex-ante revenue bound of Lemma 2 for regular distributions, which is reusable for any posted-price or prophet-inequality argument, and the $1-1/e$ correlation-gap inequality.

Difficulty

The obvious argument compares $\mathcal S$ with Myerson's mechanism one agent at a time. That fails, because $\mathcal S$ may stop offering to an agent once the units of its part are gone, and the agents blocked this way can be the ones Myerson's mechanism serves. The loss has to be bounded in aggregate, using only the ex-ante constraint $\sum_{\mathrm{part}(i)=b}q_i\le\mathrm{cap}(b)$. The single-unit case reduces to an inequality about products $\prod(1-q_j)$. For $k$ units, the printed proof (pp. 15–16) is an induction that compares the run with a hypothetical single-unit instance with probabilities $q_i/k$. Its second case is informal, so a formal proof needs its own argument for the $k$-unit bound. Passing from uniform to partition matroids needs the observation that with a global order the run inside each part depends only on that part's agents. Lemma 2 needs the revenue-curve concavity that regularity gives, stated through densities rather than derivatives.

Formalization scope

• Values. Each $F_i$ has a density that is measurable and strictly positive on a bounded interval $[\underline v_i,\bar v_i]$ with $0\le\underline v_i$, integrates to $1$ there, and has no mass outside. The paper says only "with density $f_i$". This pin rules out point masses, so the randomised-price variant of $\mathcal S$ never arises. The prior is the product of these laws.
• Regularity is $\varphi_i$ non-decreasing on the support, assumed for every agent in the goal, as in the paper's §4 analyses. The non-regular extension (second paragraph of Lemma 2, Appendix E) is out of scope.
• Truthful means deterministic, dominant-strategy incentive compatible over the support, ex-post individually rational, feasible, with measurable allocations and integrable payments.
• Prices are arguments tied to $M$ by $p_i\in[\underline v_i,\bar v_i]$ and $F_i(p_i)=1-q^M_i$. No inverse distribution function is defined.
• Order. The order $\sigma$ is a permutation with $\sigma(0)$ first, decreasing in price, and ties are arbitrary. It is global across parts. Parts of capacity $0$ are allowed.
• Constant. The constant is exactly $e/(e-1)$.
• No free prices. The theorem is not stated with free or existentially chosen prices. Prices are pinned to $M$'s service probabilities, and $\mathcal S$ uses the same constraint as $M$. A statement in which the prices could be chosen after the fact, or in which $M$ were not required to be individually rational, would be a different or false theorem.
• Every truthful $M$. The comparison is with every truthful $M$, not with a constructed Myerson mechanism. This form is at least as strong as the paper's, and it is what the paper's proof shows.

Welcome contributions: proofs of the algebraic milestones (Lemma 20, display (3)), the revenue formula, Lemma 2 (reusable payment-identity infrastructure for dominant-strategy mechanisms), and a correlation-gap argument for $k$ units.

Selected references

• S. Chawla, J. D. Hartline, D. L. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, STOC 2010; arXiv:0907.2435v2, 2010. https://arxiv.org/abs/0907.2435
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• L. Blumrosen, T. Holenstein, Posted Prices vs. Negotiations: An Asymptotic Analysis, ACM EC 2008.
• Q. Yan, Mechanism Design via Correlation Gap, ACM-SIAM SODA 2011.

Why posted prices

A seller who must decide whom to serve among several buyers with private values can, in principle, run Myerson's revenue-optimal mechanism: collect bids, compute virtual values, serve the feasible set of largest virtual surplus, and charge threshold payments (Myerson 1981). In practice sellers rarely do this. Retail, ticketing and online platforms mostly use posted prices: each buyer is offered a take-it-or-leave-it price and accepts if and only if the price does not exceed the buyer's value. Posted prices are simple to explain, are trivially truthful, and do not require buyers to reveal their values.

Chawla, Hartline, Malec and Sivan (arXiv:0907.2435, STOC 2010) asked how much revenue is lost by this simplification, and showed that for a wide range of feasibility constraints a sequential posted-price mechanism recovers a constant fraction of the optimal revenue. The matroid case, a factor of 2, is the first and most widely cited of their results. It is a revenue analogue of the prophet inequality and was one of the starting points of the literature on "simple versus optimal" mechanisms.

Setting

There are $n$ single-parameter agents, indexed by $[n]$, and one seller. Agent $i$ has a private value $v_i$ for being served, drawn independently from a distribution $F_i$ with density $f_i$. The virtual valuation of agent $i$ is

$$\phi_i(v_i) = v_i - \frac{1 - F_i(v_i)}{f_i(v_i)},$$

and $F_i$ is regular if $\phi_i$ is non-decreasing.

The seller faces a feasibility constraint: a downward-closed family $\mathcal J$ of subsets of $[n]$, the sets of agents that can be served together. The rank of a set $S$ is $\operatorname{rank}(S) = \max_{S' \subseteq S,\, S' \in \mathcal J} |S'|$. The constraint is a matroid if it satisfies the augmentation axiom: whenever $A, B \in \mathcal J$ and $|A| > |B|$, some $e \in A \setminus B$ has $B \cup \{e\} \in \mathcal J$. Examples are $k$ identical units ($k$-uniform matroids) and disjoint markets with separate capacities (partition matroids).

A mechanism $M$ maps reported values $\mathbf v$ to a feasible set $M(\mathbf v) \in \mathcal J$ of served agents and a payment $\pi_i(\mathbf v)$ for each agent. 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[\sum_i \pi_i(\mathbf v)]$, and $q^M_i = \Pr[i \in M(\mathbf v)]$ is the probability that it serves agent $i$.

A sequential posted-price mechanism (SPM) with ordering $\sigma$ and prices $\mathbf p$ approaches the agents in the order $\sigma$. When agent $i$'s turn comes, if adding $i$ to the set $A$ of agents served so far keeps $A$ feasible, $i$ is offered price $p_i$ and is served (and pays $p_i$) if $p_i \le v_i$; otherwise $i$ is blocked. Its expected revenue is $\mathcal R^\sigma_{\mathbf p}$.

The mechanism $\mathcal S$ of the paper sets $p_i = F_i^{-1}(1 - q^M_i)$, so that agent $i$ accepts an offer with probability exactly $q^M_i$, and approaches the agents in decreasing order of price.

Formalization targets

Goal: Theorem 5

For regular, independent values and a matroid constraint, for every truthful mechanism $M$ and the SPM $\mathcal S$ built from its service probabilities,

$$\mathcal R^M \le 2\, \mathcal R^\sigma_{\mathbf p}.$$

Taking $M$ to be Myerson's optimal mechanism gives the paper's statement that $\mathcal S$ 2-approximates the optimal revenue.

Milestones

1. Proposition 1 (p. 5): the expected revenue of a truthful mechanism equals its expected virtual surplus $\mathbb E[\sum_{i \in M(\mathbf v)} \phi_i(v_i)]$.
2. Lemma 2 (p. 5): $\mathcal R^M \le \sum_i p^M_i q^M_i$ with $p^M_i = F_i^{-1}(1 - q^M_i)$.
3. Revenue of an SPM (§2.2, p. 4): $\mathcal R^\sigma_{\mathbf p} = \sum_i c_i q_i p_i$, where $c_i$ is the probability that agent $i$ is offered service and $q_i = 1 - F_i(p_i)$.
4. Rank bound (§4, p. 6): $\sum_{i \in S} q^M_i \le \operatorname{rank}(S)$ for every set $S$.
5. Lost revenue (proof of Theorem 5, p. 7): in any run under a matroid, with prices in decreasing order and weights $q$ satisfying the rank bound, $\sum_{i \text{ blocked}} p_i q_i \le \sum_{i \text{ served}} p_i$.
6. Half of the benchmark (p. 7): under the same conditions, $\sum_i p_i q_i \le 2 \mathcal R^\sigma_{\mathbf p}$.

Significance

The theorem shows that under a matroid constraint the optimal mechanism's advantage over a single round of posted prices is at most a factor of 2, uniformly over all regular distributions. Prices, rather than an auction, then suffice up to a constant, which justifies posted pricing in settings where an auction is impractical. The same argument, with the matroid replaced by an intersection of $m$ matroids, gives the paper's Theorems 7 and 8, and the bound underlies the analysis of VCG with reserve prices (Theorem 32). Lemma 2's benchmark $\sum_i p^M_i q^M_i$ became a standard tool for "ex ante relaxation" arguments.

The results are proved in the paper; none of them has a machine-checked proof. Formalizing them requires Myerson's revenue characterization in a multi-agent, dominant-strategy setting with a general feasibility constraint, which Lean's libraries do not have, and a probabilistic analysis of a sequential process over a product measure. Related formalizations exist for narrower models: the single-unit, Bayesian incentive compatible revenue identity MechanismDesign.Auctions.revenue_eq_virtual_surplus (Börgers' textbook, common support) and the i.i.d. multi-unit RevenueManagement.revenue_equivalence. Neither covers per-agent supports, set-system constraints or dominant-strategy truthfulness.

Difficulty

The obvious argument compares the SPM with the hypothetical mechanism that ignores the feasibility constraint, whose revenue is exactly $\sum_i p_i q_i$. The SPM loses the revenue of agents who would have accepted but are blocked. The difficulty is that blocking is correlated with the values of earlier agents, and the lost revenue must be bounded by revenue actually collected. A naive per-agent charge fails in a general matroid, because one served agent can block many others; the bound has to use the matroid's rank structure together with the decreasing price order.

On the mechanism side, Lemma 2 needs the full Myerson theory: monotonicity of truthful allocations, the payment identity, and an optimization over interim allocation rules with a fixed service probability, where regularity is used.

Formalization scope

All objects live in the namespace CHMSPricing.SpmMatroid. Agents are Fin n. The following conventions are fixed.

• Distributions. Each $F_i$ is given by a measurable density, strictly positive on a bounded interval $[\underline v_i, \overline v_i]$ with $0 \le \underline v_i < \overline v_i$, integrating to $1$ there, with no mass outside. There are no point masses, so the randomized variant of $\mathcal S$ in §4 does not arise. The prior is the product measure.
• Regularity. Monotone non-decreasing virtual values on the support (Definition 2). All goals assume regular distributions, as the body's analyses do; the non-regular case (the second paragraph of Lemma 2, Appendix E) uses randomized prices and is out of scope.
• Truthfulness. Deterministic mechanisms, dominant-strategy incentive compatible with deviations within the support, ex-post individually rational, feasible on the type space, with measurable allocation events and measurable integrable payments. Payments of unserved agents are not forced to zero.
• Benchmark. The goal is stated for every truthful $M$, with $\mathcal S$ built from $M$'s own service probabilities; this is stronger than comparing with Myerson's mechanism alone and avoids constructing it.
• Prices. $p_i = F_i^{-1}(1 - q_i)$ is passed as an argument with the hypotheses $p_i \in [\underline v_i, \overline v_i]$ and $F_i(p_i) = 1 - q_i$, rather than through a generalized inverse.
• SPM. Positions are $0$-based; the price belongs to the agent; acceptance is $p_i \le v_i$; ties in the decreasing price order are arbitrary, and the goal holds for every such order.
• Proposition 1 additionally assumes the normalization that an agent with value $\underline v_i$ has zero utility, which is how the paper's payments are pinned down.

The goal cannot be trivialized by a free choice of prices: the prices are tied to the mechanism's service probabilities, and the SPM uses the same matroid as the mechanism. Individual rationality is essential, since without it a "truthful" mechanism can extract unbounded revenue.

A complete development needs Myerson's lemma for dominant-strategy single-parameter mechanisms, a quantile/revenue-curve argument under regularity, matroid span and rank facts for the paper's finite set systems, and independence arguments for a sequential process on a product measure. The rank bound and the deterministic lost-revenue inequality are independent of the probabilistic parts and are good first contributions; the Myerson-side lemmas are reusable for the other missions of this series.

Selected references

• S. Chawla, J. D. Hartline, D. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, arXiv:0907.2435v2, 2010; STOC 2010. https://arxiv.org/abs/0907.2435
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1):58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• J. Bulow, J. Roberts, The Simple Economics of Optimal Auctions, Journal of Political Economy 97(5):1060–1090, 1989. https://doi.org/10.1086/261643
• R. Kleinberg, S. M. Weinberg, Matroid Prophet Inequalities, STOC 2012. https://arxiv.org/abs/1201.4764

Motivation

In data-driven algorithm design, an algorithm or mechanism comes with a vector of tunable parameters $\rho$, and the parameters are chosen by optimizing average performance over sample instances drawn from an unknown distribution. How many samples suffice for the empirical optimum to be near-optimal in expectation is governed by the pseudo-dimension of the class $\mathcal U=\{u_\rho\}$ of performance functions, where $u_\rho(x)$ is the performance of the parameter $\rho$ on instance $x$. Balcan, DeBlasio, Dick, Kingsford, Sandholm and Vitercik (arXiv:1908.02894v4, 2021) give a general upper bound on $\mathrm{Pdim}(\mathcal U)$ for classes whose dual functions are piecewise structured (their Theorem 3.3, the subject of mission 1 of this series), and apply it across integer programming, computational biology, clustering and mechanism design.

A general upper bound raises the question of whether it can be improved. Section 5 of the paper answers it for one application: neutral affine maximizers (NAMs), a family of voting mechanisms studied by Roberts (1979), Mishra and Sen (2012) and Nath and Sandholm (2019). For NAMs with $n$ agents and $m$ alternatives the general theorem gives $\mathrm{Pdim}(\mathcal U)=O(n\ln m)$, and Theorem 5.2 shows a lower bound linear in $n$. So the sample complexity of tuning a NAM by sampling cannot be reduced below order $n$ by a sharper analysis, and the general bound is tight up to logarithmic factors.

Setting

There are $n$ agents and $m$ alternatives. Agent $i$ has a value $v_i(j)\in\mathbb R$ for each alternative $j\in[m]$; a valuation profile is $v=(v_1,\dots,v_n)\in\mathbb R^{nm}$.

A NAM is specified by a weight vector $\rho=(\rho[1],\dots,\rho[n])\in\mathbb R^n_{\ge0}$ in which at least one agent has weight zero; an agent with $\rho[i]=0$ is a sink agent. The NAM's outcome on a profile $v$ is an alternative maximizing the weighted value,

$$\psi_\rho(v)\in\operatorname*{argmax}_{j\in[m]}\ \sum_{i=1}^n\rho[i]\,v_i(j).$$

Its utility is the social welfare of that outcome,

$$u_\rho(v)=\sum_{i=1}^n v_i\bigl(\psi_\rho(v)\bigr),$$

and the class studied is $\mathcal U=\{u_\rho \mid \rho\in\mathbb R^n_{\ge0},\ \{i\mid\rho[i]=0\}\ne\emptyset\}$. NAMs also charge VCG-style payments that are redistributed to the sink agents; these do not enter $u_\rho$.

A class $\mathcal H$ of real-valued functions on a set $Y$ shatters points $y_1,\dots,y_N$ if there are thresholds $z_1,\dots,z_N\in\mathbb R$ such that every pattern $b\in\{0,1\}^N$ is realized by some $h\in\mathcal H$, in the sense that $h(y_\ell)>z_\ell$ exactly when $b_\ell=1$. The pseudo-dimension $\mathrm{Pdim}(\mathcal H)$ is the largest $N$ for which some $N$ points are shattered. In Lean: a profile is v : Fin n → Fin m → ℝ, the outcome rule is ψ, the utility is welfare ψ ρ, the class is namClass ψ, and shattering is the published FoundationsML.Regression.Shatters.

Formalization targets

Goal: Theorem 5.2, corrected

For every $n\ge1$, every $m\ge2$ and every tie-breaking rule,

$$\mathrm{Pdim}(\mathcal U)\ \ge\ \Bigl\lfloor\frac n2\Bigr\rfloor .$$

The printed statement reads $\mathrm{Pdim}(\mathcal U)\ge n/2$; see Formalization scope for why the floor is needed.

Milestones: the two claims of the proof (p. 24)

The proof fixes $N=\lfloor n/2\rfloor$ explicit profiles $v^{(1)},\dots,v^{(N)}$ and, for each bit vector $b\in\{0,1\}^N$, an explicit weight vector $\rho\in\{0,1\}^n$ (both are definitions of this mission). The two milestones are the claims the proof makes about them: for every $\ell\in[N]$ and $\varepsilon\in(0,\tfrac12)$,

$$b_\ell=0\ \Longrightarrow\ u_\rho\bigl(v^{(\ell)}\bigr)=\varepsilon,\qquad b_\ell=1\ \Longrightarrow\ u_\rho\bigl(v^{(\ell)}\bigr)=1 .$$

Significance

The result. Theorem 5.2 is the paper's evidence that its main upper bound cannot be improved in general by more than logarithmic factors: for NAMs the upper bound is $O(n\ln m)$ and the lower bound is of order $n$. Through the standard link between pseudo-dimension and uniform convergence, it also means that any learner choosing NAM weights from samples needs a number of samples growing with the number of agents, whatever tie-breaking rule the mechanism uses.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any pseudo-dimension lower bound for a mechanism class, was found on Prove2Me. This mission produces a Lean model of NAM outcomes and welfare that does not fix a tie-breaking rule, an explicit lower-bound construction stated as definitions, and a pseudo-dimension lower bound in the vocabulary of the published FoundationsML pseudo-dimension items. It complements mission 1, which formalizes the matching upper-bound machinery.

Difficulty

The mathematical content is a single explicit construction, and the work lies in stating and verifying it at full generality rather than in a deep argument. Three points make the naive transcription wrong. First, the printed bound $n/2$ is false at $n=1$ and is not what the proof establishes for odd $n$; the even-$n$ reduction must be replaced by a statement in $\lfloor n/2\rfloor$. Second, the outcome $\psi_\rho(v)$ is defined by an argmax with unspecified tie-breaking, so the claims must hold for every maximizer; this requires showing the relevant maximizers are unique on the constructed profiles, not reading off a convenient one. Third, the construction embeds $\lfloor n/2\rfloor$ indices into the $n$ agents twice (as $\ell$ and $\lfloor n/2\rfloor+\ell$), and the printed index condition for the second alternative is a typo; an off-by-one in this embedding silently breaks both claims. Finally, every constructed $\rho$ must be admissible: it needs a sink agent, which holds only because $N\ge1$ or because $n$ is odd and the last agent keeps weight $0$.

Formalization scope

Representation. Agents are Fin n, alternatives Fin m, profiles Fin n → Fin m → ℝ, all 0-based: the paper's agent $i$ is i - 1, and its first and second alternatives are 0 and 1. Bits are Bool with true for $1$. An outcome rule is any ψ : (Fin n → ℝ) → (Fin n → Fin m → ℝ) → Fin m with IsArgmaxSelector ψ, which requires ψ ρ v to maximize ∑ i, ρ i * v i j for every ρ and v; the theorem and both claims are stated for every such ψ. "$\mathrm{Pdim}(\mathcal U)\ge N$" is the existence of an $N$-tuple of profiles shattered by namClass ψ in the sense of FoundationsML.Regression.Shatters, whose strict threshold t i < g (z i) shatters the same tuples as the paper's sign convention.

Corrections and readings of the printed text.

1. The bound is $\lfloor n/2\rfloor$ (natural-number division n / 2) instead of $n/2$. The proof assumes $n$ even; at $n=1$ the only admissible $\rho$ is $0$, so $\mathcal U$ is a single function and $\mathrm{Pdim}(\mathcal U)=0<\tfrac12$.
2. The hypotheses $n\ge1$ and $m\ge2$ are explicit. For $n=0$ no weight vector has a zero coordinate and $\mathcal U=\emptyset$; for $m=1$ the class is a single function. The proof takes $m=2$; the statement is for every $m\ge2$, with value $0$ on every further alternative in the constructed profiles.
3. The set-builder "$\{\rho[i]\mid i=0\}\ne\emptyset$" in Theorem 5.2 is read as $\{i\mid\rho[i]=0\}\ne\emptyset$, as written in Lemma 5.1.
4. The construction's condition "$\ell=n/2+i$" for $v_i^{(\ell)}(2)=\varepsilon$ is read as $i=n/2+\ell$, as the paper's own $n=6$ example shows. The milestone texts are verbatim and keep the printed "$v^{(\ell)}_{n/2+\ell}(1)$", which should read "$(2)$".

Ruled-out trivializations. Fixing one tie-breaking rule would state a special case and is excluded by quantifying over all argmax selectors. Dropping the sink-agent condition, or allowing $n=0$ or $m=1$, would change the class or make the statement vacuous or false; the conventions above exclude all three.

Infrastructure. Only Mathlib finite sums over Fin and the published Shatters definition are needed. The NAM model (IsNAMParam, IsArgmaxSelector, welfare, namClass) is reusable for any further statement about learning NAM parameters, including the matching $O(n\ln m)$ upper bound once mission 1's general theorem is available. Proofs of the two claims, of the admissibility of the constructed weight vectors, and of the goal are all welcome.

Selected references

• M.-F. Balcan, D. DeBlasio, T. Dick, C. Kingsford, T. Sandholm, E. Vitercik, How Much Data Is Sufficient to Learn High-Performing Algorithms? Generalization Guarantees for Data-Driven Algorithm Design, arXiv:1908.02894v4, 2021. https://arxiv.org/abs/1908.02894v4
• K. Roberts, The characterization of implementable social choice rules, in J.-J. Laffont (ed.), Aggregation and Revelation of Preferences, North-Holland, 1979 (reference [86] of the paper).
• D. Mishra, A. Sen, Roberts' theorem with neutrality: a social welfare ordering approach, Games and Economic Behavior 75(1):283–298, 2012 (reference [74] of the paper).
• S. Nath, T. Sandholm, Efficiency and budget balance in general quasi-linear domains, Games and Economic Behavior 113:673–693, 2019 (reference [78] of the paper).
• D. Pollard, Convergence of Stochastic Processes, Springer, 1984 (pseudo-dimension; reference [83] of the paper).

Motivation

Algorithmic mechanism design, introduced by Nisan and Ronen (Games Econ. Behav. 35, 2001), studies optimization problems whose input is held by self-interested agents. Each agent reports its private data to a protocol, and the protocol must choose an output and payments so that reporting the truth is in every agent's interest while the chosen output is close to optimal.

The paper's test case is task scheduling on unrelated machines: $k$ tasks must be assigned to $n$ agents, agent $i$ needs time $t^i_j$ for task $j$, and the goal is to minimize the make-span. For deterministic mechanisms the paper shows that truthfulness is costly: the MinWork mechanism achieves ratio $n$, and no mechanism achieves a ratio below $2$ (Theorem 4.6). Section 4.4 asks whether randomization helps and answers yes for two agents: a randomized mechanism, truthful for every outcome of its coins, achieves expected ratio $7/4 < 2$.

Timeline.

• 1979: Roberts characterizes weighted (affine) maximizers; the weighted Vickrey–Groves–Clarke (VGC) mechanisms are truthful.
• 1999: Lehmann supplies the case analysis that improves the authors' original bound of $1.823$ to $7/4$ (acknowledged on p. 182).
• 2001: Nisan and Ronen publish the randomly biased min work mechanism and Theorem 4.16.

Setting

There are two agents, $1$ and $2$, and $k$ tasks. A type vector $t = (t^1, t^2)$ gives, for each agent $i$ and task $j$, the positive time $t^i_j$ agent $i$ needs for task $j$. An allocation $x$ assigns each task to one agent; $x^i$ is the set of tasks of agent $i$. The make-span of $x$ is

$$g(x, t) = \max_{i \in \{1,2\}} \sum_{j \in x^i} t^i_j .$$

A direct mechanism receives declared types $d$ and returns an allocation $x(d)$ and payments $p^i(d)$ handed to the agents. Agent $i$ with true type $t^i$ gets utility $p^i(d) - \sum_{j \in x^i(d)} t^i_j$. The mechanism is truthful if declaring the true type maximizes an agent's utility whatever the other agent declares, and strongly truthful if in addition every false declaration is strictly worse for some declaration of the other agent.

A randomized mechanism is a probability distribution over deterministic mechanisms; its objective is the expected make-span. It is universally truthful if every mechanism in its support is truthful, and universally strongly truthful if moreover truth-telling is the only strategy dominant in every mechanism of the support.

The biased min work mechanism with parameters $\beta \ge 1$ and $s \in \{1,2\}^k$ treats each task $j$ separately. With $i = s_j$ the favoured agent and $i' = 3 - i$ the other: if $t^i_j \le \beta \cdot t^{i'}_j$, task $j$ goes to $i$, who is paid $\beta \cdot t^{i'}_j$; otherwise it goes to $i'$, who is paid $\beta^{-1} \cdot t^i_j$. The randomly biased min work mechanism draws $s$ uniformly from $\{1,2\}^k$ and uses $\beta = 4/3$. Its expected make-span is

$$\mathbb{E}_s\, g(x_s(t), t) = \frac{1}{2^k} \sum_{s \in \{1,2\}^k} g(x_s(t), t).$$

Formalization targets

Goal: Theorem 4.16

For every $k$: the randomly biased min work mechanism is universally strongly truthful, and for every positive type vector $t$ and every allocation $y$,

$$\frac{1}{2^k} \sum_{s \in \{1,2\}^k} g(x_s(t), t) \le \frac74\, g(y, t).$$

Milestones

• Theorem 3.2 (Roberts): for positive weights $\beta^i$, a mechanism whose output maximizes $\sum_i \beta^i v^i(t^i, o)$ and whose payments are $p^i = \frac{1}{\beta^i}\sum_{j \ne i}\beta^j v^j(t^j, o) + h^i(t^{-i})$ is truthful.
• Lemma 4.15: for every $\beta \ge 1$ and every $s$, the biased min work mechanism is strongly truthful.
• Lemma 4.17: the randomly biased min work mechanism is universally strongly truthful.
• Claim 4.19, part 5: allocating two tasks independently at random gives an expected make-span no larger than allocating their merge at random.
• Reduced case (Fig. 2, Cases 1–3): for $a, b, c, d \ge 0$ with $a + c = \frac43 b + d$,

$$\tfrac14\Big(\max(a+b+c+\tfrac43 d, 0) + \max(a+b+c, d) + \max(a+b+\tfrac43 d, \tfrac43 c) + \max(a+b, \tfrac43 c + d)\Big) \le \tfrac74 (a+c).$$

• Lemma 4.18: the $7/4$ bound on the expected make-span.

Significance

The result. Theorem 4.16 separates randomized from deterministic truthful mechanisms for scheduling two unrelated machines: $7/4$ against the deterministic lower bound of $2$. The notion of truthfulness it uses is the strong one, dominance for every coin outcome, so the separation does not rest on agents being risk-neutral or knowing the distribution. Later work on truthful randomized scheduling, and on the gap between deterministic and randomized truthful mechanisms, starts from this construction.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it is known. A formalization produces a checked definition of universal truthfulness for randomized mechanisms, a checked weighted VGC theorem usable for any affine-maximizer mechanism, and a checked version of the reduction argument (Claim 4.19), which the paper states in five informal instance transformations, one of them a limiting argument.

Difficulty

Truthfulness reduces to one task at a time, where the mechanism is a weighted VGC mechanism; the difficulty lies in the approximation bound. A naive task-by-task comparison with the optimum fails: the bound is on a maximum of two loads averaged over $2^k$ coin vectors, and the maximum does not decompose over tasks. The paper reduces an arbitrary instance to four tasks through transformations that each move the ratio in one direction, and the reduced instance still needs a three-way case analysis. Making the reduction rigorous is the main work: part 1 of Claim 4.19 replaces a ratio "arbitrarily close to $\beta$" by $\beta$, and under the mechanism's tie rule a task with ratio exactly $\beta$ is allocated by the coin rather than to the efficient agent.

Formalization scope

• Agents are Fin 2 (agent $1$ is 0, agent $2$ is 1); the other agent is other i = 1 - i. Tasks are Fin k; allocations are functions Fin k → Fin 2. The statements hold for every $k$, including $k = 0$.
• Types are positive: every truthfulness quantifier ranges over positive declarations, true types and misreports, and the approximation bound is stated on positive type vectors. The reduced-case and merging milestones are pure real inequalities with nonnegative times, since the paper represents missing tasks by zero times.
• Payments are handed to the agent; utility is quasi-linear.
• The make-span is a finite maximum (Finset.sup') over the two agents. The expected make-span is the average over all $2^k$ vectors $s$, which is exactly the expectation of Definition 15 for the uniform distribution; no measure theory is used.
• Universal (strong) truthfulness quantifies over all $s \in \{1,2\}^k$, the support of the uniform distribution. Truthfulness in expectation over $s$ is weaker and is not the notion stated.
• The tie rule of Fig. 1 ($\le$: ties go to the favoured agent) is kept.
• The goal fixes $\beta = 4/3$; only Lemma 4.15 is stated for every $\beta \ge 1$. The ratio is compared with every allocation $y$, not with one fixed allocation, and the average is over all $s$, not the best $s$.
• Roberts' theorem is stated for arbitrary output sets, type sets and valuations, with positive weights.
• "Polynomial time computable" in Theorem 4.16 is not formalized; running time is out of scope.
• Claim 4.19 (the reduction to the four-task case) is not a separate item beyond its part 5, because its parts are instance transformations with a limiting step, not a single statement; a solver may formalize the reduction in any form that proves Lemma 4.18.

Contributions welcome: proofs of the milestones, and reusable lemmas on averages of maxima over product coin spaces.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• K. Roberts, The characterization of implementable choice rules, in J.-J. Laffont (ed.), Aggregation and Revelation of Preferences, North-Holland, 1979, pp. 321–349.
• T. Groves, Incentives in teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 2, the linked differential equations

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

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

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

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

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

Milestones: the displays of the proof

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

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

Significance

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

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

Difficulty

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

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

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

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

Formalization scope

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

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

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

Selected references

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

Motivation

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