Mechanism Design

Motivation

Retailers that run predictable promotions teach their customers to wait for them. A customer who knows that a discount will come next week has no reason to buy at the list price today. Firms therefore lose margin on exactly the customers who would have paid in full. One response, documented in practice by Moon, Bimpikis and Mendelson (2017), is to randomize promotions: commit to a distribution of prices, draw a fresh price every period, and let customers know only the distribution. A customer cannot time a discount that arrives at random. Whether waiting is worthwhile then depends on how patient the customer is.

The classical deterministic answer to strategic waiting is cyclic pricing: Conlisk, Gerstner and Sobel (1984) showed that a durable-goods monopolist facing a stream of arriving customers lowers its price periodically. Besbes and Lobel (2015) characterized optimal deterministic policies when customers differ in valuation and patience. Randomized prices as a model of sales go back to Varian (1980) in a competitive setting. Chen, Hu and Wu (SSRN 3223844, published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1194) ask the monopoly question directly: which price distribution should a seller commit to when two customer segments differ in both valuation and waiting cost? This mission formalizes their answer for the two-segment base model.

Setting

A monopolist sells one product over an infinite horizon. A fraction $\alpha\in(0,1)$ of arriving customers are low-valuation customers, who value the product at $v_L$ and pay a waiting cost $c_L$ per period; the remaining $1-\alpha$ are high-valuation customers, with valuation $v_H>v_L$ and waiting cost $c_H$. Assumption (S) of the paper is $0<c_L<v_L$ and $0<c_H<v_H$.

The firm announces a price distribution: a random price $P$ with finitely many possible values $p$ and probabilities $f(p)\ge0$ summing to one. Each period an independent price is drawn from it. Write $F(x)=\sum_{p\le x}f(p)$ for the distribution function, $\mathbb E[P\mid P\le x]$ for the mean price conditional on $P\le x$, and $\mathbb E[(v-P)^+]=\sum_p f(p)\max(v-p,0)$ for the expected one-period surplus of a customer with valuation $v$. The purchase threshold of a customer with waiting cost $c$ is

$$\underline p=\max\{v'\mid \mathbb E[(v'-P)^+]\le c\}.$$

A customer whose valuation exceeds her threshold waits and buys at the first price not above it.

The paper reduces the firm's choice to the regime where low-valuation customers wait and high-valuation customers buy on arrival. The firm's long-run profit per arriving customer is then the objective of problem (2):

$$\max_{F}\ \alpha\,\mathbb E[P\mid P\le \underline p^L]+(1-\alpha)F(v_H)\,\mathbb E[P\mid P\le v_H]\quad\text{s.t.}\quad \mathbb E[(v_L-P)^+]>c_L,\ \ \mathbb E[(v_H-P)^+]\le c_H,$$

where $\underline p^L$ is the low type's threshold. Replacing $\underline p^L$ by $v_L$ in the objective gives the relaxation, problem (3). The key constants are

$$\Delta_R=\sqrt{\frac{\alpha c_L}{(1-\alpha)(v_H-v_L)}},\qquad U_1=\alpha v_L+(1-\alpha)v_H-(1-\alpha)c_L-2(1-\alpha)(v_H-v_L)\Delta_R,$$ $$U_2=\alpha v_L+(1-\alpha)v_H-(1-\alpha)c_H-\alpha c_L\frac{v_H-v_L}{c_H-c_L}.$$

In Lean the parameters are vL vH cL cH α, a law is w : ℝ →₀ ℝ with IsPriceDist w, and the objects above are cdf, condExp, gain, thresh, Feas, obj2, obj3, ΔR, bnd $=(c_H-c_L)/(v_H-v_L)$, U1, U2. Here $\underline p^L$ is written p^L in milestone text.

Formalization targets

Goal: Proposition 3 (p. 16)

Assume $c_L<c_H$ and $\Delta_R<1$, and let $U=U_1$ if $\Delta_R<\frac{c_H-c_L}{v_H-v_L}$ and $U=U_2$ otherwise. Then every price distribution feasible for (2) earns at most $U$ in (2), and there is $\eta$ with $\eta(\delta)\to0$ as $\delta\searrow0$ such that the two-point law

$$f(p)=\begin{cases}\beta^* & p=\underline p^*,\\ 1-\beta^* & p=v_H,\end{cases}\qquad \beta^*=\min\Big\{\Delta_R,\frac{c_H-c_L}{v_H-v_L}-\delta\Big\},\quad \underline p^*=v_L-\frac{c_L}{\beta^*}-\eta(\delta),$$

is feasible for (2) for all small $\delta>0$ and its profit tends to $U$. This is the $\epsilon$-optimality of the paper's Definition 1.

Milestones

1. §3.2.2: for every law feasible for (2), $\mathbb E[P\mid P\le\underline p^L]\le\mathbb E[P\mid P\le v_L]$, so (3) relaxes (2).
2. §3.2.2: every feasible law has $F(v_L)<\frac{c_H-c_L}{v_H-v_L}$.
3. Lemma 5, in the form its proof establishes: moving all mass above $v_L$ to $v_H$ preserves feasibility and does not lower the objective of (3).
4. Lemma 6(ii)(a) and (b): every feasible law earns at most $U_1$, respectively $U_2$, in (3).
5. Lemma 6(i), the complementary regime $\Delta_R\ge1$: no feasible law beats the static profit $\max\{v_L,(1-\alpha)v_H\}$.

Significance

The result says that, in this model, the optimal randomized promotion is the simplest one. The firm posts the regular price $v_H$ most of the time and runs a promotion at $\underline p^*$ with probability $\beta^*$. High-valuation customers buy on arrival; low-valuation customers wait for the promotion. The discount below $v_L$, of size $c_L/\beta^*$, is the price of keeping low types in the market. The closed forms $U_1,U_2$ quantify the profit lost relative to perfect discrimination $\alpha v_L+(1-\alpha)v_H$. The paper uses them to compare randomized with static and cyclic pricing (Propositions 4 and 8) and generalizes the structure to myopic customers and to $n$ segments.

The result is proved on paper; no machine-checked version exists. The mission produces a formal statement of the firm's problem over all finitely supported price laws on $\mathbb R$, a verified upper bound on its value, and a verified family that attains it in the limit. It also records three points the printed statements leave implicit (below).

Difficulty

The decision variable is an entire distribution, and the objective of (2) depends on it through the threshold $\underline p^L$, itself defined by a maximization over the distribution. The obvious approach, guessing the two-point law and checking first-order conditions, gives no upper bound over all laws. The upper bound has to hold for laws with arbitrarily many support points, of either sign and above $v_H$, and both incentive constraints enter it. Problem (3) has a strict constraint and no maximizer, so every statement about "the optimal profit" has to be read as a supremum. The attainment half then needs the threshold of the two-point law, computed from its definition, to sit exactly $\eta(\delta)$ below $v_L$.

Formalization scope

• Distributions. A price law is w : ℝ →₀ ℝ with nonnegative masses summing to one (finite support, as the paper assumes on p. 9). Prices range over all of $\mathbb R$: $\underline p^*$ can be negative under the hypotheses, and with prices restricted to $[0,\infty)$ Proposition 3 is false for some admissible parameters.
• Standing assumptions, hypotheses of every theorem: Assumption (S), $v_L<v_H$ (printed on p. 9), and $0<\alpha<1$ (added; $\Delta_R$ divides by $1-\alpha$).
• Added hypothesis of the goal: $c_L<c_H$. Without it $\beta^*<0$ and the two-point law is not a distribution.
• Conventions. $\mathbb E[P\mid P\le x]$ is a quotient that Lean sets to $0$ when $F(x)=0$; this never happens for feasible laws. $\underline p^L$ is the real supremum of $\{v'\mid\mathbb E[(v'-P)^+]\le c_L\}$, which is a maximum for every price law. "The optimal expected profit is no more than $U$" is read as a bound on every feasible law. "Optimal" in Proposition 3 is $\epsilon$-optimality for (2), stated as the upper bound plus the approaching family, with $\eta$ existential.
• Lemma 5 as printed quantifies over optimal solutions of (3), which do not exist; the milestone states the dominance that its proof (Online Supplement p. 8) establishes.
• Ruled out. The profit and the threshold of the two-point law are not given in closed form: they are the general obj2 and thresh applied to it. The upper bound ranges over all feasible laws, not two-point laws or laws on $[0,v_H]$. "Optimal" is not read as "beats static pricing" (that is Proposition 4) or as an attained maximum, and $\eta$ may not depend on the competing law.
• Not in the mission. The customer's optimal-stopping model (Lemma 1, Proposition 1, Lemma 2) is the paper's justification of the objective of (2); the mission states problem (2) as printed. Cyclic and Markovian pricing, myopic customers and $n$ segments are not posed.
• Needed infrastructure. Finite sums over Finsupp supports, monotonicity and continuity of $v\mapsto\mathbb E[(v-P)^+]$, and the elementary concavity argument for $\beta\mapsto U(\beta)$. A general library of finitely supported real price laws (distribution function, partial expectations, expected surplus) would be reusable for other pricing papers. Proofs of any milestone are welcome.

Selected references

• H. Chen, M. Hu, J. Wu, Intertemporal Price Discrimination via Randomized Promotions, SSRN preprint 3223844 (revision of 2022-11-16); Manufacturing & Service Operations Management, 2023. https://ssrn.com/abstract=3223844, https://doi.org/10.1287/msom.2023.1194
• J. Conlisk, E. Gerstner, J. Sobel, Cyclic pricing by a durable goods monopolist, Quarterly Journal of Economics 99(3), 1984. https://doi.org/10.2307/1885961
• O. Besbes, I. Lobel, Intertemporal price discrimination: Structure and computation of optimal policies, Management Science 61(1), 2015. https://doi.org/10.1287/mnsc.2014.2049
• H. Varian, A model of sales, American Economic Review 70(4), 1980. https://www.jstor.org/stable/1803562
• X. Su, Intertemporal pricing with strategic customer behavior, Management Science 53(5), 2007. https://doi.org/10.1287/mnsc.1060.0628
• K. Moon, K. Bimpikis, H. Mendelson, Randomized markdowns and online monitoring, Management Science, 2017.

Motivation

Fair division asks how to share a resource among $n$ agents with different preferences so that each agent can be promised a minimum level of welfare, whatever the preferences of the others. Classical cake cutting treats a good cake, valued additively or at least monotonically. Many real problems mix goods and bads: a plot of land with both fertile and polluted parts, a set of chores some of which are welcome, a workload whose value first rises and then falls with its size. Bogomolnaia and Moulin (arXiv:1911.10009, Mathematics of Operations Research 2023) study the most general non-atomic model, in which a utility is only required to be continuous and bounded, and ask which utility levels can be guaranteed simultaneously to all agents.

Their first main result is that Kuhn's $n$-person Divide & Choose rule (Kuhn 1967) guarantees each agent her minMax utility, in this full generality. The key ingredient is an equipartition theorem of Avvakumov and Karasev ([4]), which lets the current divider cut any piece into equally valued parts even when the utility is neither monotone nor of constant sign.

Setting

The manna $\Omega$ is a bounded Lebesgue-measurable subset of $\mathbb R^d$, $d\ge1$, with $|\Omega|>0$; $|\cdot|$ is Lebesgue measure. A share is a measurable subset $S\subseteq\Omega$, possibly empty. For a share $S$, an $n$-partition $\Pi=(S_i)_{i=1}^n\in\mathcal P_n(S)$ is an $n$-tuple of shares with $\bigcup_i S_i=S$ and $|S_i\cap S_j|=0$ for $i\ne j$. The pseudo-metric on shares is $\delta(S,T)=|S\otimes T|$, the measure of the symmetric difference.

A utility $u$ assigns a real number to each share, with $u(\emptyset)=0$, and is bounded and continuous for $\delta$. The set of utilities is $\mathcal D(\Omega)$. Nothing else is assumed: $u$ may increase or decrease with the share and may take both signs.

An $n$-equipartition of a share $S$ for $u$ is a partition $\Pi^e\in\mathcal P_n(S)$ whose parts all have the same utility $u(\Pi^e)$; their set is $\mathcal{EP}_n(S;u)$. The two benchmarks are

$$\mathrm{minMax}(u;n)=\inf_{\Pi\in\mathcal P_n(\Omega)}\max_i u(S_i),\qquad \mathrm{Maxmin}(u;n)=\sup_{\Pi\in\mathcal P_n(\Omega)}\min_i u(S_i).$$

minMax is what an agent gets choosing first from the worst partition for her; Maxmin is what she gets choosing last from the best one.

In the D&C$_n$ rule the agents are ordered $1,\dots,n$. At each step the first remaining agent, the Divider, proposes an $m$-partition of the remaining manna $S$ among the $m$ remaining agents. Every other remaining agent reports which shares she likes (at least one); the Divider likes all of them. A set of agents is properly matched to a set of shares when they are matched one-to-one to liked shares and no other remaining agent likes any of those shares. The largest properly matchable set of agents is served; the other shares return to the manna, and the rule continues with the unserved agents.

Formalization targets

Goal: Theorem 1 i)

An agent $i$ with utility $u\in\mathcal D(\Omega)$ follows the minMax strategy when, as Divider, she proposes an equipartition $\Pi^e\in\mathcal{EP}_m(S;u)$, and, as chooser, she likes exactly the shares $T$ with $u(T)\ge\mathrm{minMax}(u;n)$, the level of the initial problem. Then, whatever the other agents do,

1. the Divider move is always available (an equipartition exists);
2. the chooser move is always available (some offered share is worth at least $\mathrm{minMax}(u;n)$);
3. in every complete play,

$$u(S_i)\ \ge\ \mathrm{minMax}(u;n).$$

Milestones

The equipartition theorem of [4] on $[0,1]$; Lemma 1, $\mathcal{EP}_n(S;u)\ne\emptyset$ for every share and every $u\in\mathcal D(\Omega)$; Lemma 2, existence of a largest properly matchable set containing the Divider; and the three steps of the proof of Theorem 1 i): the invariant that previously assigned shares are worth less than minMax to an unserved agent, the chooser step and the Divider step.

Companions

Proposition 1 iii), $\mathrm{minMax}(u;n)\le u(\Pi^e)\le\mathrm{Maxmin}(u;n)$ for every $\Pi^e\in\mathcal{EP}_n(\Omega;u)$, and the statement that $\mathrm{minMax}(\cdot;n)$ is a Fair Guarantee in $\mathcal D(\Omega)$: every profile $(u_i)\in\mathcal D(\Omega)^n$ admits $\Pi\in\mathcal P_n(\Omega)$ with $u_i(S_i)\ge\mathrm{minMax}(u_i;n)$ for all $i$ (Definition 3).

Significance

Maxmin is an upper bound on any Fair Guarantee, and in the mixed-manna domain it is not itself a Fair Guarantee. Theorem 1 establishes minMax as a guarantee that holds on the whole domain, is implemented by a simple decentralised protocol, and requires no knowledge of the other agents' preferences. Together with the companion results it brackets what can be promised to every agent in non-atomic division with arbitrary continuous preferences.

The result is proved in the paper; nothing in this mission is open mathematics. None of it is machine-checked. The formalization adds a non-atomic fair-division layer (shares up to null sets, $\delta$-continuous utilities, equipartitions, minMax and Maxmin) and a precise model of a sequential division protocol in which the other agents' behaviour is quantified over, rather than fixed. The goal also makes explicit the step the informal proof passes over quickly: the minMax strategy is always a legal move.

Difficulty

Once the protocol is modelled, the guarantee is an invariant argument over the steps of a play. The difficulty is Lemma 1. For an additive utility, Lyapunov's theorem gives equipartitions; for a utility of constant sign, the Knaster–Kuratowski–Mazurkiewicz lemma does (Remark 1). A utility that takes both signs defeats both arguments, and an obvious intermediate-value argument handles only $n=2$. The paper reduces Lemma 1, through a moving knife, to the interval theorem of Avvakumov and Karasev, whose proof is topological (mapping degree). Mathlib has neither that theorem nor the degree theory it uses. Lemma 2 needs the Gallai–Edmonds decomposition of a bipartite graph, which Mathlib does not have either; Hall's theorem is available.

Formalization scope

The space is EuclideanSpace ℝ (Fin d) with volume, and every statement that needs non-atomicity assumes $d\ge1$ (on $\mathbb R^0$, a point of measure $1$, Lemma 1 fails). A utility is a function on all subsets, but every condition is imposed on shares only. Partitions are indexed by Fin n, have union exactly the share and null pairwise overlaps; disjointness is not required. minMax and Maxmin are real sInf/sSup; every statement using them assumes $n\ge1$, which makes the defining sets nonempty and bounded. Agents are Fin n, the Divider is the least remaining agent, and a play is a list of steps, each recording the remaining agents and manna, the proposed partition, all reports and the assignment. A step is admissible exactly as Definition 4 requires, including that the served set is the largest properly matchable one.

The following formalizations would trivialize the goal and are ruled out: fixing the other agents' behaviour; accepting against the minMax of the remaining manna instead of the initial one; assuming the utility monotone, additive or of constant sign; defining minMax as a minimum over a possibly empty set; and omitting the availability parts 1–2, which would make Lemma 1 irrelevant.

A complete development needs the interval equipartition theorem (a topological result of independent interest), moving knives through a measurable set, a Gallai–Edmonds-type argument for bipartite graphs, and the invariant over plays. The non-atomic model and the equipartition lemmas are reusable for the Moving Knife and Bid & Choose rules of the companion mission. Proofs of any milestone, alternative proofs of Lemma 1 for special classes of utilities, and the run-level lemmas are all welcome.

Selected references

• A. Bogomolnaia, H. Moulin, Guarantees in Fair Division: General or Monotone Preferences, Mathematics of Operations Research, 2023; arXiv:1911.10009v3. https://arxiv.org/abs/1911.10009
• S. Avvakumov, R. Karasev, Equipartition of an interval, cited in the paper as [4] (2020, in preparation).
• H. W. Kuhn, On games of fair division, in Essays in Mathematical Economics in Honour of Oskar Morgenstern, Princeton University Press, 1967, pp. 29–37.
• L. Lovász, M. D. Plummer, Matching Theory, Annals of Discrete Mathematics 29, North-Holland, 1986 (Gallai–Edmonds decomposition, Chapter 3).

Motivation

Classical mechanism design assumes that agents optimize exactly: a buyer facing a menu picks the option that maximizes his utility, however small the advantage over the next-best option. In many settings this is implausible. Agents may face cognitive or computational costs, or the designer may only be able to certify incentives approximately, as in algorithmic mechanism design where exact incentive compatibility is replaced by ε-incentive compatibility: no deviation gains more than $\varepsilon$.

Balseiro, Besbes and Castro (arXiv:2103.03403v2; Operations Research, 2024) ask how much a revenue-maximizing seller can gain when the buyer is only an $\varepsilon$-optimizer, in the most basic setting: one seller, one item, one buyer. Without the relaxation the answer is classical: by Myerson (1981) and Riley–Zeckhauser (1983) the optimal mechanism is a posted price. The rounding argument usually attributed to Nisan shows that the gain from the relaxation is $O(\varepsilon^{1/2})$ for every distribution. This mission formalizes the paper's first main theorem, which shows that for regular instances the gain is much smaller and is determined by the local curvature of the revenue curve at the optimal price.

Setting

The buyer's value $v$ has a density $f$ on $S=[0,\bar v]$, with $\bar v>0$, $f\ge 0$, $f=0$ off $S$ and $\int_0^{\bar v}f=1$. Assumption 1 requires in addition that $f$ has bounded variation on $S$. Write $F(v)=\int_0^v f$, $\bar F=1-F$, the revenue function $R(v)=v\bar F(v)$ (the revenue of a posted price $v$), and $\dot R(v)=\bar F(v)-vf(v)$.

A mechanism $m=(x,t)$ assigns to every report $v\in S$ an allocation probability $x(v)\in[0,1]$ and a payment $t(v)\in\mathbb R$. It is individually rational (IR) if $v x(v)-t(v)\ge 0$ for all $v\in S$, and ε-incentive compatible (IC$_\varepsilon$) if

$$v\,x(v)-t(v)\ \ge\ v\,x(v')-t(v')-\varepsilon\qquad\forall v,v'\in S .$$

$\mathcal M(\varepsilon)$ is the set of such mechanisms, $\Pi(m)=\int_0^{\bar v}t(v)f(v)\,dv$ the expected revenue, and $\Pi^\star(\mathcal M(\varepsilon))=\sup_{m\in\mathcal M(\varepsilon)}\Pi(m)$.

Definition 1 (local α-power envelopes). $R$ has a unique maximizer $p^\star\in(0,\bar v)$ on $S$, and there are $\alpha>1$, $\kappa_L,\kappa_U>0$ and a neighborhood $\mathcal N_\ell=(p^\star-\ell,p^\star+\ell)\subset(0,\bar v)$ with

$$\kappa_L\alpha|v-p^\star|^\alpha\le(p^\star-v)\dot R(v)\le\kappa_U\alpha|v-p^\star|^\alpha\qquad\forall v\in\mathcal N_\ell .$$

For the uniform distribution on $[0,1]$, $p^\star=1/2$ and $\alpha=2$.

Formalization targets

Goal: Theorem 1 (p. 16)

Under Assumption 1, local $\alpha$-power envelopes at $p^\star$ and $\inf_{p\in S\setminus\mathcal N_\ell}|\dot R(p)|>0$,

$$\Pi^\star(\mathcal M(\varepsilon))-\Pi^\star(\mathcal M(0))=\tilde O\big(\varepsilon^{\alpha/(2\alpha-1)}\big),$$

where $\tilde O$ allows a factor $\log(1/\varepsilon)$ and the constants depend on the instance but not on $\varepsilon$.

Milestones

The paper's argument passes through the following stated results, in attack order:

1. $\mathcal M(\varepsilon)\subseteq\mathcal M_{\text{path}}(\varepsilon)$ for the relaxation that keeps IR on $[0,\mu]$ and IC only along a path $v\mapsto v^\star(v)$ (p. 17);
2. Lemma 1 (weak duality): $\Pi(m)\le\Phi_1(\lambda)+\Phi_2(\lambda)$ for every $m\in\mathcal M_{\text{path}}(\varepsilon)$ and every dual-feasible $\lambda$;
3. Lemma 2: an explicit dual solution $\lambda^\star(v)=\frac{d}{dv}\sum_{j\le k}F(w^j(v))$ on the $k$-th step, where $w$ inverts $v^\star$;
4. Lemma 3: $\Phi_1(\lambda^\star)\le C\varepsilon K$, $K$ the number of steps;
5. Lemma 4: $\int_x^{\bar v}\Delta\le R(x)+2(w(x)-x)$ when the dual virtual value $\Delta$ is nonnegative on $[x,\nu_0]$;
6. Proposition 2: for the piecewise-linear path of eq. (9), $K=O(\log(1/\varepsilon)/\varepsilon^\beta)$;
7. the sandwich $vf-\bar F-C_L\varepsilon^\beta\le\Delta\le vf-\bar F+C_U\varepsilon^\beta$ a.e. on $[p^\star,\nu_0]$ (p. 48);
8. $\Delta\le-\dot R+C\varepsilon^\beta$ a.e. on $[0,p^\star]$ (pp. 51–52).

Significance

Theorem 1 is an instance-dependent impossibility result: no $\varepsilon$-IC mechanism can extract more than $\tilde O(\varepsilon^{\alpha/(2\alpha-1)})$ beyond the optimal posted price. Since $\alpha/(2\alpha-1)>1/2$ for every $\alpha>1$, it strictly improves the universal $O(\varepsilon^{1/2})$ bound for these distributions; for $\alpha=2$ (a revenue curve with nonzero second derivative at $p^\star$) the rate is $\varepsilon^{2/3}$. Together with Theorem 3 of the same paper, a matching $\Omega(\varepsilon^{\alpha/(2\alpha-1)})$ lower bound by a randomized mechanism, it identifies the exact rate up to the logarithm. The authors conjecture that the logarithmic factor can be removed.

The result is proved in the paper; no machine-checked proof of it or of any of its lemmas exists. A formalization would check an appendix argument of several pages of explicit estimates, and would produce reusable components: a weak duality theorem for a mechanism-design program over a path of incentive constraints, an explicit solution of the functional equation $\lambda(v)=f(v)+\dot w(v)\lambda(w(v))$ by iterates of $w$, and estimates of iterated piecewise-linear maps.

Difficulty

The obvious approach is to bound the gain by perturbing the optimal posted price, which yields only the $\varepsilon^{1/2}$ rate of the rounding argument. Getting the exponent $\alpha/(2\alpha-1)$ requires an upper bound that is tight to first order, i.e. a nearly optimal dual certificate for an infinite-dimensional program. The dual depends on the choice of path: the paper's analysis shows that a parallel shift $w(x)=x+\delta$ cannot beat $\varepsilon^{1/2}$, so the path must approach the diagonal near $p^\star$ while keeping the number of steps $K$ controlled. The estimates for $\Delta$ in milestones 7–8 require tracking $\lambda^\star(w(v))$ through $K=O(\log(1/\varepsilon)/\varepsilon^\beta)$ iterations of $w$, with a bounded-variation (possibly discontinuous) density. Measure-theoretic details absent from the paper also have to be supplied: changes of variables along a Lipschitz path, almost-everywhere differentiability of iterated compositions, and integrability of the dual variable.

Formalization scope

The Lean development lives in namespace ApproxIC.UpperBound. Every function of the value is a total function ℝ → ℝ and every condition quantifies over $S$ only. Committed conventions:

• $F$ is the interval integral of $f$; $\dot R$ is the explicit expression $\bar F(v)-vf(v)$, not a derivative of $R$.
• Mechanisms are required to be measurable (disclosed: $\mathbb E_v[t(v)]$ presumes it). $\Pi^\star$ is an sSup of the revenue image, which is nonempty and bounded above by $\bar v$.
• The goal is stated as $\forall m\in\mathcal M(\varepsilon),\ \Pi(m)-\Pi^\star(\mathcal M(0))\le C\varepsilon^{\alpha/(2\alpha-1)}\log(1/\varepsilon)$ for all $\varepsilon\in(0,\varepsilon_0]$, with $C,\varepsilon_0$ chosen after the instance and before $\varepsilon$. The infimum hypothesis on $|\dot R|$ ranges over $S\setminus\mathcal N_\ell$.
• Definition 1's constants are parameters of a predicate LocalPowerEnvelope.
• Paths carry an added, disclosed assumption: $w$ is Lipschitz on $[0,\nu_0]$ (eq. (9)'s $w$ is). $\dot w$ is deriv w.
• The thresholds are $\mathbb N$-indexed with index $0$ equal to $\bar v$, so the paper's $\nu_k$ is index $k+1$.
• Lemma 1's printed sign $(v-w(v))$ in $\Phi_2$ is read as $(w(v)-v)$, as in its proof and in Lemma 4. Lemma 4's printed "$\Phi_2(\lambda)=\int_x^{\bar v}\Delta$" is read as $\int_x^{\bar v}\Delta^+=\int_x^{\bar v}\Delta$. Lemmas 3 and 4 are stated for Lemma 2's explicit $\lambda^\star$.

The goal imports only the model file; paths, the dual and eq. (9) appear only in the milestones. A formalization in which $\tilde O$'s constants are chosen after $\varepsilon$, $\Pi^\star(\mathcal M(0))$ is replaced by a constant, or the revenue integral is allowed to vanish on non-measurable mechanisms is not this theorem and is ruled out by the statement.

A complete development needs interval integrals and the fundamental theorem of calculus for absolutely continuous functions, change of variables along monotone Lipschitz maps, BoundedVariationOn, real powers and logarithms, and iterates Nat.iterate. The duality lemma and the functional-equation solution are reusable for other single-agent screening problems with relaxed incentive constraints. Contributions to any milestone, and alternative proofs of the goal that bypass the path construction, are welcome.

Selected references

• S. R. Balseiro, O. Besbes, F. Castro, Mechanism Design under Approximate Incentive Compatibility, arXiv:2103.03403v2, 2022; Operations Research, 2024. https://arxiv.org/abs/2103.03403
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• J. Riley, R. Zeckhauser, Optimal Selling Strategies: When to Haggle, When to Hold Firm, Quarterly Journal of Economics 98(2), 1983. https://doi.org/10.2307/1885622

Motivation

Classical mechanism design assumes that agents best-respond exactly: a buyer who gains even an infinitesimal amount by misreporting will misreport. In practice agents face cognitive and computational costs, and a buyer may ignore a deviation that gains less than some small amount $\varepsilon$. A seller facing such a buyer only needs to satisfy the incentive constraints up to $\varepsilon$, and the natural question is how much revenue this relaxation is worth.

Balseiro, Besbes and Castro (arXiv:2103.03403v2, 2022; Operations Research, 2024) study this question in the simplest setting, one seller and one buyer with a single item. Their answer separates deterministic and randomized mechanisms. This mission formalizes the deterministic half: Theorem 2, which identifies the optimal deterministic $\varepsilon$-incentive-compatible mechanism and shows that its revenue gain over the classical optimum is exactly linear in $\varepsilon$.

Setting

The buyer's value $v$ for the item is drawn from a distribution $F$ with a density $f\ge0$ supported in $S=[0,\bar v]$, $\bar v>0$, with $\int_0^{\bar v}f=1$. Assumption 1 adds that $f$ has bounded variation on $S$. Write $F(v)=\int_0^v f$, $\bar F=1-F$, and $R(v)=v\,\bar F(v)$ for the revenue of a posted price $v$.

A direct mechanism $m=(x,t)$ assigns to each reported value $v$ an allocation probability $x(v)\in[0,1]$ and a payment $t(v)\in\mathbb R$. It is individually rational (IR) if $v\,x(v)-t(v)\ge0$ for all $v\in S$, and $\varepsilon$-incentive compatible (IC$_\varepsilon$) if

$$v\,x(v)-t(v)\ \ge\ v\,x(v')-t(v')-\varepsilon\qquad\text{for all }v,v'\in S.$$

$\mathcal M(\varepsilon)$ denotes the feasible mechanisms, and $\mathcal M_d(\varepsilon)=\{m\in\mathcal M(\varepsilon):x(S)\subseteq\{0,1\}\}$ the deterministic ones. The revenue is $\Pi(m)=\int_0^{\bar v}t(v)f(v)\,dv$ and $\Pi^\star(\mathcal M)=\sup_{m\in\mathcal M}\Pi(m)$. At $\varepsilon=0$ the optimum $\Pi^\star(\mathcal M(0))$ is attained by a posted price at any maximizer $p^\star$ of $R$ on $S$.

The hard/soft floor mechanism $m_d(p,s)$, $p\le s$, allocates the item to every report $v\ge p$; a report in $[p,s)$ pays its own value and a report $v\ge s$ pays $s$:

$$x_d(v)=\mathbf 1\{v\ge p\},\qquad t_d(v)=v\,\mathbf 1\{v\in[p,s)\}+s\,\mathbf 1\{v\ge s\}.$$

Formalization targets

Goal: Theorem 2 (pp. 24–25)

Under Assumption 1:

1. for every $\varepsilon>0$ some $m_d(p,p+\varepsilon)$, $p\in[0,\bar v]$, lies in $\mathcal M_d(\varepsilon)$, earns at least as much as every mechanism of $\mathcal M_d(\varepsilon)$, and maximizes $\Pi(m_d(p',p'+\varepsilon))$ over $p'\in[0,\bar v]$;

$$\Pi^\star(\mathcal M_d(\varepsilon))-\Pi^\star(\mathcal M(0))=\Theta(\varepsilon),$$

that is, there are $c,C,\varepsilon_0>0$ with $\Pi^\star(\mathcal M(0))+c\varepsilon\le\Pi^\star(\mathcal M_d(\varepsilon))\le\Pi^\star(\mathcal M(0))+C\varepsilon$ for all $\varepsilon\in(0,\varepsilon_0]$.

Milestones

• §2.1, p. 13: a posted price at $p^\star\in\arg\max_S R$ is optimal for $(\mathcal P_0)$, so $\Pi^\star(\mathcal M(0))=R(p^\star)$.
• Appendix B, p. 53: $m_d(r,r+\varepsilon)\in\mathcal M_d(\varepsilon)$ for every $r\in S$.
• Appendix B, p. 53: $\Pi(m_d(r,r+\varepsilon))=\int_r^{r+\varepsilon}vf(v)\,dv+(r+\varepsilon)\bar F(r+\varepsilon)=r\bar F(r)+\int_r^{r+\varepsilon}\bar F(v)\,dv$.
• Appendix B, eq. (23), pp. 52–53: every $m\in\mathcal M_d(\varepsilon)$ has payments bounded pointwise by those of some $m_d(r,r+\varepsilon)$, hence $\Pi(m)\le\Pi(m_d(r,r+\varepsilon))$.

Significance

Theorem 2 settles what deterministic mechanisms can do against an $\varepsilon$-optimizing buyer: the gain is linear in $\varepsilon$, no more and no less. The lower half shows that any optimal approximately incentive compatible mechanism gains at least order $\varepsilon$; the upper half shows that a seller who wants more must randomize. Together with the paper's Theorems 1 and 3 (other missions of this series), which give the rate $\varepsilon^{\alpha/(2\alpha-1)}$ for randomized mechanisms under a curvature condition on $R$, it locates the full spectrum of achievable gains between $\varepsilon$ and $\varepsilon^{1/2}$. The hard/soft floor form is also a practical design: a posted price followed by a pay-your-bid band of width $\varepsilon$.

The result is proved in the paper's online appendix. To the best of our knowledge it has no machine-checked proof; the classical posted-price optimality has a formalization on Prove2Me under the stronger assumption of a strictly positive density, and this mission needs it for densities that may vanish.

Difficulty

The obvious argument for "an optimal deterministic mechanism is a hard/soft floor" starts from an optimal mechanism, which need not exist a priori, and takes its allocation right-continuous "without loss of generality". Neither step is available for an arbitrary measurable mechanism: the allocation set $\{x=1\}$ may have no least element, and changing $x$ on a null set can break IC$_\varepsilon$ at individual points. The domination milestone is therefore stated for every deterministic mechanism. The revenue identity needs integration by parts for an absolutely continuous $F$ whose density may vanish or be discontinuous, and the comparison with $\Pi^\star(\mathcal M(0))$ needs the classical posted-price optimality without positivity of $f$. The lower bound needs the optimal price to sit strictly inside $(0,\bar v)$ and $\bar F$ to stay bounded away from zero just above it.

Formalization scope

Values are reals and every function is a total function $\mathbb R\to\mathbb R$; only its values on $S=[0,\bar v]$ matter. Mechanisms are required to be measurable (implicit in $\mathbb E_v[t(v)]$); IR and IC$_\varepsilon$ then make $t$ bounded on $S$, so revenue integrals are genuine. $\Pi^\star$ is a supremum (sSup) of a nonempty set of revenues bounded above by $\bar v$. The goal's $\Theta(\varepsilon)$ is the conjunction of the paper's $\mathcal O$ and $\Omega$ (p. 13), with constants depending on the distribution but chosen before $\varepsilon$, written as "some deterministic mechanism earns at least $\Pi^\star(\mathcal M(0))+c\varepsilon$, every one earns at most $\Pi^\star(\mathcal M(0))+C\varepsilon$"; $\Pi^\star(\mathcal M(0))$ stays a supremum and is not replaced by $R(p^\star)$. The payment region of $m_d$ is $[p,s)$ as in the proof (the theorem prints $[p,s]$, which double-counts at $v=s$). The hard floor ranges over $[0,\bar v]$, so the soft floor $p+\varepsilon$ may exceed $\bar v$.

The domination statement quantifies over all of $\mathcal M_d(\varepsilon)$, not over monotone or right-continuous mechanisms, and the $\Theta(\varepsilon)$ constants may not depend on $\varepsilon$; either restriction would trivialize the result.

The development needs interval integrals, integration by parts for absolutely continuous functions, and continuity of $\bar F$. The posted-price optimality milestone is reusable for every single-buyer revenue question and is welcome as a stand-alone contribution.

Selected references

• S. R. Balseiro, O. Besbes, F. Castro, Mechanism Design under Approximate Incentive Compatibility, arXiv:2103.03403v2, 2022; Operations Research, 2024. https://arxiv.org/abs/2103.03403v2
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• J. Riley, R. Zeckhauser, Optimal Selling Strategies: When to Haggle, When to Hold Firm, Quarterly Journal of Economics 98(2), 1983. https://doi.org/10.2307/1885622

Motivation

Many proof-of-stake blockchains do not let every participant produce blocks. Instead, token holders elect a small committee of block producers, and the committee runs a Byzantine agreement protocol among itself. EOS, for example, elects 21 producers by approval voting: each token holder approves a set of candidates, and the 21 candidates with the most approvals form the committee. Byzantine agreement protocols are safe only while a large enough fraction of the committee is honest, typically more than two thirds, so the security of the whole chain rests on a question of social choice: does approval voting, with voters who see only noisy information about the candidates, elect a committee with enough honest members?

Benhaim, Falk and Tsoukalas (arXiv:2110.08673v2, Management Science 2023) model this election and analyse it. Their main result, Theorem 3, shows that whatever strategies the voters use, as long as the honest candidates are approved with probability at least a fixed margin $\delta$ above the dishonest ones, the probability of electing an honest committee converges to one exponentially fast in the number of voters. This mission formalizes that result.

Setting

There are $n$ voters and $m$ candidates (block producers), and a committee of size $k\le m$ is to be elected. Each voter $i$ submits an approval ballot $\mathcal C_{v_i}$, a subset of the candidates. The score of candidate $j$ is the number of voters approving it,

$$\operatorname{score}(j)=X_j=\bigl|\{\,i : j\in\mathcal C_{v_i}\}\bigr| .$$

The elected committee $\mathbb T$ consists of $k$ candidates with the highest scores. When several candidates tie at the lowest elected score, or when fewer than $k$ candidates have a non-zero score, the paper resolves the choice adversarially. Formally, a set $T$ of candidates is an admissible committee if $|T|=k$ and $X_b\le X_a$ for every $a\in T$ and $b\notin T$.

Each candidate is honest or dishonest. Let $\mathcal M$ denote the set of dishonest candidates. For a tolerance $p\in[0,1]$ (for instance $p=1/3$), the committee is honest, written $\mathbb T=H$, if it has at least $\lceil(1-p)k\rceil$ honest members. Because ties and filling are adversarial, $\mathbb T=H$ means that every admissible committee has at least $\lceil(1-p)k\rceil$ members outside $\mathcal M$.

The ballots are random: they are drawn on a probability space, independently across voters, while the approvals inside a single ballot may depend on each other in any way. The vote probability $p_{ij}=\Pr[j\in\mathcal C_{v_i}]$ is the probability that voter $i$ approves candidate $j$. The candidates' types are fixed throughout, and all randomness is in the ballots.

Formalization targets

Goal: Theorem 3 (p. 22)

Suppose there are a set $\mathcal H$ of honest candidates with $|\mathcal H|\ge(1-p)k$ and a $\delta>0$ with $\min_{i,\,j\in\mathcal H}p_{ij}\ge\max_{i,\,j\in\mathcal M}p_{ij}+\delta$. Then

$$\Pr[\mathbb T=H]\ \ge\ 1-2m^2e^{-\delta^2 n/2}.$$

Milestones (in the order the proof on p. 48 uses them)

1. Opening claim of the proof (p. 48). If every member of $\mathcal H$ outscores every member of $\mathcal M$, then $\mathbb T=H$ (deterministic).
2. Theorem 1 (pp. 15–16). Each vote count is Poisson binomial:

$$\Pr[X_j=x]=\sum_{|A|=x}\ \prod_{i\in A}p_{ij}\prod_{i\notin A}(1-p_{ij}).$$

3. Theorem 6 (p. 50). Chernoff–Hoeffding for a Poisson binomial $X$ with mean $n\bar p$: $\Pr[X>n\bar p+t]\le e^{-2t^2/n}$ and $\Pr[X<n\bar p-t]\le e^{-2t^2/n}$ for $t>0$.
4. (82). For $j_h\in\mathcal H$, $j_m\in\mathcal M$: $\Pr[X_{j_h}\le X_{j_m}]\le 2e^{-\delta^2n/2}$.
5. (83). $\Pr[X_{j_m}<X_{j_h}\ \forall j_h\in\mathcal H,\ j_m\in\mathcal M]\ge1-2m^2e^{-\delta^2n/2}$.

Significance

The theorem is the paper's answer to its title question. Its bound holds for every voting behaviour, including the threshold and cardinal strategies the paper studies and strategies with arbitrary correlation inside a ballot. So the security guarantee does not depend on voters coordinating or on knowing the signal model. All it needs is that signals are informative by a margin $\delta$. The bound also shows the trade-off quantitatively: the failure probability grows quadratically in the number of candidates $m$ and decays exponentially in the number of voters $n$. This is the basis of the paper's Corollaries 1 and 2 on the threshold and cardinal strategies.

The paper proves the result on paper (Appendix B.2, p. 48), using a Chernoff–Hoeffding bound it cites from Dubhashi and Panconesi. As far as the platform's index shows, no machine-checked version of the result or of its committee model exists. The mission contributes the first formal model of $k$-winner approval voting with adversarial tie-breaking on Prove2Me, a formal statement of the Poisson-binomial law of approval counts, and the one-sided Hoeffding bound for sums of independent Bernoulli variables in the $e^{-2t^2/n}$ form. The formalization also records three places where the printed text needs correcting (see Formalization scope).

Difficulty

There are two difficulties. The first is the committee predicate. Ties and under-filled committees are resolved by an adversary, so $\mathbb T=H$ is a statement about every admissible committee, not about one top-$k$ list. The reduction from honesty to the score-separation event has to handle both the case where all of $\mathcal H$ is elected and the case where some member of $\mathcal H$ is left out, so that every elected candidate outscores it.

The second is the concentration step. The vote counts of different candidates are not independent, because each voter's ballot ties the approvals together, so no argument that treats the $m$ counts as independent variables applies. The paper's own step from the gap to (82), the split (80)/(81), uses strict inequalities and is false when the two thresholds coincide at an attained integer value; the printed Hoeffding bound (Theorem 6) is strict as well, so the printed chain does not close as written at that boundary.

Formalization scope

• Voters are Fin n and candidates Fin m, both 0-based. A random ballot is a measurable map Ω → (Fin m → Bool) on a probability space (Ω, P). The ballots are mutually independent (iIndepFun), and each voter's ballot law is otherwise arbitrary. This generalises the paper's Gaussian signal model and its strategy classes, which are not formalized, and the paper's per-type probabilities $p^h_i,p^m_i$ become per-candidate $p_{ij}$. The cap $|\mathcal C_v|\le t$ of Definition 2 is not imposed. The printed statements are special cases.
• $\mathbb T=H$ is the predicate "every set $T$ with $|T|=k$ and no outsider scoring above a member has $|T\setminus\mathcal M|\ge\lceil(1-p)k\rceil$", with an integer ceiling. A formalization in which some admissible committee is honest, or in which the committee is chosen by a fixed tie-breaking rule, is a different and weaker theorem. Without the condition $|T|=k$ the predicate would be trivial. An admissible committee exists for every score vector when $k\le m$.
• Standing assumptions that are made explicit: $k\le m$ (p. 9), $0\le p\le1$ ($p$ is the tolerated fraction, which the paper never bounds; the opening claim of the proof fails for $p<0$), independence across voters (§5.1.2), and measurability of each ballot.
• The min/max gap of Theorem 3 is stated pairwise for all voters $i,i'$, all $j_h\in\mathcal H$ and all $j_m\in\mathcal M$. This is equivalent when both sets are nonempty and avoids undefined extrema otherwise.
• Corrected slips: Theorem 6 is stated for $t>0$ and $n\ge1$, since it is false for negative $t$ and divides by $n$. (80)/(81) are not posed, and (82) is stated as a bound on $\Pr[X_{j_h}\le X_{j_m}]$.
• Infrastructure needed: Mathlib's independence, Measure.real, sub-Gaussian concentration for bounded independent variables, and Finset.powersetCard. The committee definitions and the Poisson-binomial law can be reused by later missions on voting and on the companion single-voter result. Proofs of any milestone are welcome, and so are alternative routes to the goal.

Selected references

• A. Benhaim, B. H. Falk, G. Tsoukalas, Scaling Blockchains: Can Committee-Based Consensus Help?, Management Science, 2023; preprint arXiv:2110.08673v2, 2022. https://arxiv.org/abs/2110.08673v2 (DOI 10.1287/mnsc.2022.03177)
• D. P. Dubhashi, A. Panconesi, Concentration of Measure for the Analysis of Randomized Algorithms, Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511581274
• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58(301), 1963. https://doi.org/10.1080/01621459.1963.10500830

Motivation

Classical mechanism design assumes that agents are perfect optimizers: a mechanism is incentive compatible if no buyer gains anything, however small, by misreporting. In practice buyers face cognitive and computational costs, and a buyer may not bother to deviate for a gain below some threshold $\varepsilon$. Balseiro, Besbes and Castro, Mechanism Design under Approximate Incentive Compatibility (arXiv:2103.03403v2, 2022; Operations Research, 2024), ask how much additional revenue a seller can extract when the incentive constraints only need to hold up to $\varepsilon$.

A known benchmark answers this at order $\sqrt\varepsilon$. It comes from a rounding argument attributed to Noam Nisan, used in mechanism design to transform an approximately incentive compatible mechanism into an exactly incentive compatible one (see e.g. Balcan, Blum, Hartline and Mansour, FOCS 2005). The paper states this benchmark as its Proposition 1 and proves it in its online appendix "for completeness". This mission formalizes that benchmark; the paper's sharper, instance-dependent rates are the subject of the other missions of this series.

Setting

A seller sells a single item to one buyer. The buyer's value $v$ is drawn from a distribution $F$ with a density $f\ge 0$ supported in $S=[0,\bar v]$, $\bar v>0$, with $\int_0^{\bar v} f=1$.

A direct mechanism $m=(x,t)$ assigns to each reported value $v\in S$ an allocation probability $x(v)\in[0,1]$ and a payment $t(v)\in\mathbb R$ (payments may be negative). Given $\varepsilon\ge 0$, the mechanism is

• individually rational (IR) if $v\cdot x(v)-t(v)\ge 0$ for all $v\in S$;
• $\varepsilon$-incentive compatible (IC$_\varepsilon$) if $v\cdot x(v)-t(v)\ge v\cdot x(v')-t(v')-\varepsilon$ for all $v,v'\in S$.

$\mathcal M(\varepsilon)$ denotes the set of mechanisms satisfying IR and IC$_\varepsilon$ (problem $(\mathcal P_\varepsilon)$ of the paper). For $\varepsilon=0$ this is the classical feasible set, and $\mathcal M(0)\subset\mathcal M(\varepsilon)$. The revenue of $m$ is $\Pi(m)=\mathbb E_v[t(v)]=\int_0^{\bar v}t(v)f(v)\,dv$, and the optimal revenue under $\varepsilon$-IC is

$$\Pi^\star(\mathcal M(\varepsilon))=\sup_{m\in\mathcal M(\varepsilon)}\Pi(m).$$

The quantity of interest is the revenue gain $\Pi^\star(\mathcal M(\varepsilon))-\Pi^\star(\mathcal M(0))$.

In the Lean development the model is ApproxIC.Rounding.Model (fields vbar, f) with the predicate Model.Standing; mechanisms are Mech (fields x, t); the sets and values are Mset M ε, revenue M m and optRev M ε.

Formalization targets

Goal: Proposition 1 (p. 15)

$$\Pi^\star(\mathcal M(\varepsilon))-\Pi^\star(\mathcal M(0))=\mathcal O(\varepsilon^{1/2}),$$

in the paper's notation (p. 13): there are $C>0$ and $\varepsilon_0>0$, which may depend on the distribution, such that for every $\varepsilon\in(0,\varepsilon_0]$ and every $m\in\mathcal M(\varepsilon)$,

$$\Pi(m)-\Pi^\star(\mathcal M(0))\le C\sqrt\varepsilon .$$

Milestones (Appendix A, proof of Proposition 1, p. 38)

Fix $m=(x,t)\in\mathcal M(\varepsilon)$ and $\delta\in(0,1)$, and let $v^\star_\delta(v)\in\arg\max_{w\in S}\{v\cdot x(w)-(1-\delta)t(w)\}$.

1. The rounded mechanism $\tilde m=(x(v^\star_\delta(\cdot)),(1-\delta)t(v^\star_\delta(\cdot)))$ lies in $\mathcal M(0)$.
2. For $v'=v^\star_\delta(v)$: $t(v')\ge t(v)-\varepsilon/\delta$.
3. The non-asymptotic bound

$$\Pi(m)-\Pi^\star(\mathcal M(0))\le\frac{\delta}{1-\delta}\Pi^\star(\mathcal M(0))+\frac{\varepsilon}{\delta}\le 2\delta\,\Pi^\star(\mathcal M(0))+\frac{\varepsilon}{\delta}\qquad(\delta\le 1/2).$$

Significance

The result. Proposition 1 gives a distribution-free shape for the value of relaxing incentive compatibility: an $\varepsilon$-optimizing buyer can be exploited for at most order $\sqrt\varepsilon$ extra revenue. It is the starting point against which the paper measures its main contributions: an instance-dependent upper bound of order $\tilde{\mathcal O}(\varepsilon^{\alpha/(2\alpha-1)})$ (Theorem 1) and a matching lower bound (Theorem 3) for distributions whose revenue curve has local $\alpha$-power envelopes around the optimal price, and the $\Theta(\varepsilon)$ rate for deterministic mechanisms (Theorem 2). Since $\alpha/(2\alpha-1)>1/2$ for every $\alpha>1$, these show that the $\sqrt\varepsilon$ benchmark is not tight for such distributions. The rounding step itself (milestone 1) is the standard device for converting approximately incentive compatible mechanisms into exactly incentive compatible ones, and is reused across mechanism design.

Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal single-buyer model with $\varepsilon$-IC mechanisms that the other missions of the series share, and a formal version of Nisan's rounding argument for a continuum of types.

Difficulty

The paper's proof is short, but it is written for an argmax that is attained and a rounded mechanism that is tacitly measurable. In a formal treatment, the selection $v^\star_\delta$ must be chosen so that $\tilde m$ is measurable and its expected payment is defined. Exact incentive compatibility forces $\tilde x$ to be nondecreasing on $S$, and that monotonicity has to be established and then turned into measurability. The revenue comparison $\mathbb E_v[\tilde t(v)]\ge(1-\delta)(\mathbb E_v[t(v)]-\varepsilon/\delta)$ needs the integrability of $t\cdot f$, which comes from IR and IC$_\varepsilon$ bounding $t$ on $S$, not from an assumption. The milestone-3 bound carries no attainment hypothesis, so a proof must also handle the case in which the maximum over $S$ is not attained. Finally, $\Pi^\star(\mathcal M(0))$ is a supremum, and its nonnegativity (used in $\delta/(1-\delta)\le 2\delta$) and its finiteness must be derived from the feasible set.

Formalization scope

• Values, allocations and payments are total functions $\mathbb R\to\mathbb R$; every condition quantifies over $S=[0,\bar v]$ only, and the revenue integral is over $[0,\bar v]$.
• Standing assumptions (the density half of the paper's Assumption 1): $\bar v>0$, $f\ge 0$, $f=0$ off $[0,\bar v]$, $f$ integrable on $[0,\bar v]$ with integral $1$. The bounded-variation half of Assumption 1 is not used by Proposition 1 and is not assumed.
• Added hypothesis: mechanisms in $\mathcal M(\varepsilon)$ have measurable $x$ and $t$, so that $\mathbb E_v[t(v)]$ is meaningful.
• $\Pi^\star$ is the supremum (sSup) of the revenue image of $\mathcal M(\varepsilon)$, which is nonempty (the zero mechanism) and bounded above by $\bar v$; the goal and milestone 3 are stated for every $m\in\mathcal M(\varepsilon)$, which is equivalent to the bound on the supremum. $\Pi^\star(\mathcal M(0))$ is never replaced by the posted-price revenue.
• $\varepsilon^{1/2}$ is Real.sqrt ε. The constants $C$ and $\varepsilon_0$ are quantified after the distribution and before $\varepsilon$; quantifying them after $\varepsilon$ would make the goal trivial.
• Milestones 1 and 2 take the argmax selection $v^\star_\delta$ as a map vs with values in $S$ attaining the maximum, as the page assumes. The rounded mechanism is set to $0$ off $S$; its measurability is part of the conclusion, not a hypothesis.
• Restricting $\mathcal M(\varepsilon)$ to deterministic mechanisms, to nonnegative payments, or defining $\Pi^\star(\mathcal M(0))$ by the optimal posted-price revenue would change the statement and is ruled out.

Needed infrastructure: monotone functions are measurable, interval integrals of bounded measurable functions against an integrable density, and suprema of bounded real sets, all in Mathlib. Contributions of the rounding lemma in reusable form (for general type sets) are welcome.

Selected references

• S. R. Balseiro, O. Besbes, F. Castro, Mechanism Design under Approximate Incentive Compatibility, arXiv:2103.03403v2, 2022; Operations Research, 2024. https://arxiv.org/abs/2103.03403
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• M.-F. Balcan, A. Blum, J. D. Hartline, Y. Mansour, Mechanism Design via Machine Learning, 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS'05), pp. 605–614, 2005. https://doi.org/10.1109/SFCS.2005.50