Mechanism Design

Motivation

A seller who sells over two periods, at a full price now and a discount later, loses revenue to strategic customers who wait for the discount. Waiting is costly to the customer only through availability risk: if inventory is scarce, the product may be gone by the second period. Inventory is usually known to the firm and not to its customers, so the firm can try to shape how scarce the product looks. Drakopoulos, Jain and Randhawa (SSRN 3191629, version of April 17, 2020) study this as a problem of Bayesian persuasion (Kamenica and Gentzkow, AER 2011) with many receivers: the firm commits to prices and to a signaling policy before it learns its inventory, and then sends each customer a recommendation.

Their two main results separate public from private information. Theorem 1 (p. 15): with a public signal, seen by all customers, the firm earns no more than with prices alone. Theorem 2 (p. 17): with personalized signals, which may depend on each customer's valuation and be randomized independently across customers, a simple Buy/Wait/No mechanism is optimal and strictly beats every public mechanism when the low inventory level is small. Personalized recommendations are the kind of information online retailers and travel platforms send (low-stock alerts, buy-now prompts).

Setting

There is a unit mass of customers with valuations distributed on $V=[0,b]$ with density $f$ and complementary distribution $\bar F(v)=\int_v^b f$; the hazard rate $f/\bar F$ is non-decreasing. The firm's inventory $Q$ is high, $q_H=1$ (enough for everyone), with probability $P(H)\in(0,1)$, and low, $q_L\in(0,1]$, with probability $P(L)=1-P(H)$. The monopoly price is $p^m=\arg\max_p p\bar F(p)$, and $\bar F^{-1}(q)$ is the valuation at which a mass $q$ of customers lies above.

A straightforward mechanism fixes prices $p_1,p_2\ge0$ and, after seeing $Q$, draws a latent index $k$ from a finite set with a state-dependent law; given $(Q,k)$, each $v$-customer is independently told Buy (in period 1), Wait (buy in period 2) or No. A customer who requests the product in a period with $s$ units left and demand of mass $D$ from the others gets it with probability $\mathrm{avail}(s,D)$: $0$ if $s\le0$, $1$ if $D\le s$, $s/D$ otherwise (random rationing). The mechanism is obedient if every customer (for almost every $v$) weakly prefers to follow her recommendation, given the availabilities she can expect conditional on it: (Buy-1)–(No), p. 40. The firm's revenue is the expected value of rationed sales $p_1\min\{D_1,Q\}+p_2\min\{D_2,(Q-D_1)^+\}$. A mechanism is public when the recommendations depend only on $(k,v)$ and obedience holds for each realized $k$.

The personalized mechanism (PS1)–(PS2), p. 17, sets $p_1=\bar F^{-1}(q_L)$. In state $L$ it tells customers with $v\ge p_1$ to buy and the rest No; in state $H$ it tells $v\ge p_1$ to buy with probability

$$\sigma_H(v)=\min\Big\{\frac{P(L)}{P(H)}\frac{v-p_1}{p_1-p_2},1\Big\}\tag{13}$$

and to wait otherwise, tells $p_2\le v<p_1$ to wait, and $v<p_2$ No. The price $p_2$ solves $\bar F(p_2)-p_2f(p_2)=\bar F(\bar v)$ (14) with $\bar v=\sup\{v:\sigma_H(v)<1\}$ (15).

Formalization targets

Goal: Theorem 2

If $q_L\le\bar F(p^m)$, then (14) has a root $p_2\in(0,p_1)$, and for every such root the mechanism (PS2) is obedient, its revenue $R_{private}$ is at least that of every obedient mechanism at any prices, and

$$R_{private}>R^*_\phi=P(L)\,\bar p_1\bar F(\bar p_1)+P(H)\,p^m\bar F(p^m),\qquad \bar p_1=\max\{\bar F^{-1}(q_L),p^m\}.\tag{11}$$

Milestones

1. Lemma 2 (p. 35): the L-state profit $\phi(t,p)$ of a public threshold $t$ satisfies $\phi(t,p)\le\max\{(\bar F^{-1}(q_L)-p)q_L,0\}$, and for $q_L<\bar F(p)$ its unique maximizer is $\bar F^{-1}(q_L)$.
2. Theorem 1 (c) (p. 15): $R^*_\phi$ is the largest revenue of a public mechanism.
3. Lemma 3 (p. 44): at fixed prices $p_1>p_2$, the $(t^*,p_1,p_2)$-mechanism built from an optimal threshold $t^*$ of the one-parameter program (A.16) is obedient, earns its value $\bar D(p_1,p_2)$, and is optimal among obedient mechanisms with those prices.
4. Lemma 4 (p. 44, corrected reading): if $\bar F(p_2)>q_L$, then $\bar D(p_1,p_2)\le\bar D(\bar F^{-1}(q_L),p_2)$.
5. (16) (p. 17): (PS2) is obedient and earns

$$R_{private}=P(H)p_2\bar F(p_2)+P(H)(p_1-p_2)\bar F(\bar v)+P(L)\int_{p_1}^{\bar v}(v-p_1)\,dF(v)+P(L)p_1q_L.$$

Significance

The result says that the value of information in this market lies entirely in its personalization: public information is worthless (Theorem 1), and private recommendations strictly raise revenue whenever low inventory is scarce relative to the monopoly market. The optimal mechanism is explicit and has a simple form, with the low-type firm selling out exactly in period 1 and the high-type firm mimicking it as far as incentive compatibility allows; in the paper's uniform example ($q_L=P(H)=1/2$) revenue rises from $1/4$ to $13/48$. The proof technique, a relaxation to a linear program over signal profiles followed by a dual reduction to a single threshold, is a template for many-receiver persuasion problems with congestion.

The theorems are proved in the paper; none of them has a machine-checked proof. The mission produces a formal model of strategic customers under rationing and personalized signaling, and the formal versions of the five steps. Two printed steps need correction to be true and are stated in corrected form (Lemma 4's tie case, the location of the root of (14)); formal proofs settle that the corrections suffice.

Difficulty

The obvious argument is a pointwise one: for each valuation, the Buy incentive constraint caps the high-state Buy probability given the low-state one, so set every cap tight. It fails because the availabilities in the constraints depend on the aggregate masses that the recommendations themselves create, so the constraints for different valuations are coupled; the paper resorts to an infinite-dimensional linear program and asserts strong duality without proof (p. 41). Lemma 4 is the algebraically heavy step (pp. 46–50): an envelope argument over the threshold combined with the hazard-rate monotonicity. Theorem 2 then needs a one-dimensional optimization in $p_2$, the existence of a root of (14) (a fixed-point equation, since $\bar v$ depends on $p_2$), and the case $p_2>p_1$, which the paper never treats.

Formalization scope

The paper's game (Definitions 1–2: a continuum of customers, Bayesian Nash equilibrium, sender-preferred selection) is re-expressed as the class its proofs reduce to by the revelation principle (p. 39, footnote 5): obedient straightforward mechanisms with aggregate masses. Revenue optimality over this class is what Theorem 2 asserts after that reduction. The latent index is finite (Fin n, for every n); it carries the correlation between customers' signals that public signals need. Obedience is required for almost every valuation, as in Definition 1.

Committed conventions: $V=[0,b]$, $b>0$, $f$ continuous on $[0,b]$ and positive on $[0,b)$; $0<P(H)<1$, $0<q_L\le1$; $q_H=1$ and customer mass $1$. Availability is avail above; at zero demand it is $1$ with stock left and $0$ without. (14) is written $\bar F(p_2)-p_2f(p_2)=\bar F(\bar v)$. In (PS2)(a) "$v>p_1$" is taken as $v\ge p_1$ (a null set). (B) is read with $\min\{\cdot,1\}$. The program (A.16) keeps the no-Buy mechanism ($\bar F(t)=0$), which the printed version drops. "The optimal mechanism" is stated as "an optimal mechanism" (ties exist). Lemmas 3–4 take $p_2<p_1$, implicit in the paper's divisions; the goal ranges over all prices $p_1,p_2\ge0$, including $p_2>p_1$ (p. 8). Milestone (16) is stated at the prices of (PS1): $p_1=\bar F^{-1}(q_L)$ and $p_2\in[0,p_1)$ a root of (14).

Trivializing formalizations are ruled out: revenue counts rationed sales, not $p_1D_1+p_2D_2$; obedience is the printed conditional constraint multiplied by the probability of the recommendation, never divided by a possibly zero probability; availability never uses Lean's $x/0=0$; the goal carries the existence of a root of (14), so "for every root" is not vacuous; the mechanism class contains public and correlated mechanisms; and $R_{private}$ is the revenue of the mechanism (PS2), tied to the formula (16) by a milestone.

A complete development needs: the density measure on $[0,b]$ and its tail function $\bar F$, monotonicity and continuity of $\bar F$ and its inverse, the quasi-concavity of $p\bar F(p)$ under a non-decreasing hazard rate, and bounds for the rationing function. The hazard-rate and $\bar F^{-1}$ lemmas are reusable for other pricing models. Contributions of helper lemmas, of a primal proof of Lemma 3 avoiding the duality argument, and of the case $p_2>p_1$ are welcome.

Selected references

• K. Drakopoulos, S. Jain, R. S. Randhawa, Persuading Customers to Buy Early: The Value of Personalized Information Provisioning, SSRN working paper 3191629, version of April 17, 2020. https://ssrn.com/abstract=3191629
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6):2590–2615, 2011. https://doi.org/10.1257/aer.101.6.2590
• D. Bergemann, S. Morris, Information Design: A Unified Perspective, Journal of Economic Literature 57(1):44–95, 2019. https://doi.org/10.1257/jel.20181489

Motivation

Sellers sometimes offer a customer a choice among individual products and a product whose final item is revealed only after purchase. Airlines, for example, can sell a fixed itinerary alongside a discounted option that leaves one feature unspecified. The seller must decide whether this opaque product earns enough to justify limiting how much individual item prices can differ. Elmachtoub and Hamilton study this question for unit-demand customers who know their own values for the possible items. Their 2021 paper identifies two conditions under which the best menu of opaque products earns at least as much as the best separate item prices.

The comparison matters because the opaque menu uses less item-specific pricing information. The seller gives every item one price and gives opaque products of equal size the same price. The theorem says that this constrained format can still match discriminatory pricing when the valuation law is symmetric and either customers assess opaque products pessimistically or valuations have only two levels. The paper also supplies counterexamples outside those conditions; the symmetry and customer-type hypotheses are substantive.

Setting

There are $N\ge2$ items. A customer has a nonnegative valuation vector $v=(v_1,\ldots,v_N)$, sampled from a probability law $F$. A menu option has a price and a valuation. Its utility is valuation minus price. The customer buys one option of greatest utility when that utility is nonnegative. If several options have greatest utility, the customer buys one with the highest price. Remaining ties at the same price do not affect revenue. A customer may also buy nothing, yielding zero revenue.

In discriminatory pricing (DP), the seller assigns a nonnegative price $p_i$ to each item and offers only the individual items. Write $R_{\mathrm{DP}}(p_1,\ldots,p_N)$ for expected revenue and $R_{\mathrm{DP}}$ for its optimum over item-price vectors.

In opaque selling (OPQ), the seller offers the items at a common price $p$ and also offers every set $S$ of at least two items. A set of size $k$ costs $p^k$, independent of which items it contains. A pessimistic customer values $S$ at $\min_{i\in S}v_i$; a risk-neutral customer values it at $|S|^{-1}\sum_{i\in S}v_i$. Both value a singleton at its item value. A customer is pessimistic with probability $\alpha$ and risk-neutral with probability $1-\alpha$, independently of the valuation vector. The expected revenue of a price menu is $R_{\mathrm{OPQ}}^\alpha(p,p^2,\ldots,p^N)$; its optimum is $R_{\mathrm{OPQ}}^\alpha$.

A law $F$ is exchangeable if permuting the coordinates of $v$ leaves its joint distribution unchanged. Coordinates may be correlated, and they need not be independent. A law is two-valued when there are real numbers $a<b$ such that almost every valuation vector has every coordinate in $\{a,b\}$. This says the same pair applies to the entire vector, rather than allowing a different pair at each coordinate.

Formalization targets

Theorem 1: revenue dominance

For exchangeable $F$, nonnegative valuations, and $0\le\alpha\le1$, the target is

$$\bigl(\alpha=1\ \text{or}\ F\text{ is two-valued}\bigr) \quad\Longrightarrow\quad R_{\mathrm{OPQ}}^\alpha\ge R_{\mathrm{DP}}.$$

The first case covers any exchangeable law, including discrete laws with ties, when all customers are pessimistic. The second covers every mix of customer types when the valuations take two common values. Neither case requires independent item values. This mission retains both cases in one goal because that is Theorem 1 as stated in the paper.

The milestones trace the two cases. They identify the equal probabilities of valuation-order events, the value of the best opaque subset at a fixed size, the pessimistic dominance case, the three candidate DP price vectors under two values, the conditional revenue identity printed as display (1), the opaque price ladder's revenue for both customer types, and the two-valued dominance case. Each milestone is attached to a passage in the proof of Theorem 1.

Significance

The theorem gives a comparison of optimal revenues, not just a comparison of one chosen menu with one chosen price vector. For a seller with exchangeable valuations, it guarantees that size-based opaque prices can recover at least the revenue available from item-specific prices in either named regime. Outside those regimes, the paper's counterexamples prevent extending that guarantee merely by relaxing the hypotheses.

The result is proved in the cited paper; the goal here is a machine-checked version of its statement and proof. A formal development would establish the choice rule for finite menus, expectations for discrete and continuous valuation laws, permutation symmetry, finite order statistics, and the behavior of size-based menus at utility and price ties. These components are reusable in later formalizations of unit-demand pricing and opaque-product models. The present mission starts with unproved Lean theorem statements; compiling those statements does not certify the paper's argument.

Difficulty

One tempting argument treats the opaque menu as discriminatory pricing with the valuation order known to the seller. That comparison overlooks a restriction: the same price must be attached to each product size, so a price that is useful for the highest-valued item need not be useful for every realized ordering. The paper explicitly notes that the apparent information advantage alone would also suggest dominance in settings where dominance fails.

Ties create another obstacle. The probability formulas displayed for DP and OPQ in the selling-model section use inequalities that can count a tied purchase more than once. The paper sets aside ties for exposition in that section, yet the two-valued case necessarily has them. A faithful proof has to use the stated customer choice rule and the highest-price tie-break, rather than treating those displayed sums as definitions for discrete laws. The two-valued case also requires tracking how revenue changes with the number of high valuations, without assuming independent coordinates.

Formalization scope

Items are represented by Fin N and valuation profiles by functions Fin N → ℝ; the paper's item indices start at one, while Lean's start at zero. The probability law is a measure on profiles with a probability-measure instance and almost-sure nonnegative coordinates. Exchangeability means invariance of this law under every coordinate permutation. Two-valued support is an almost-sure condition on the whole profile. No independence or density assumption is included.

The menu contains every nonempty item set. Singletons stand for the ordinary items at their common price; sets of equal larger size share an opaque price. All seller prices are nonnegative. Revenue is the highest price among options with maximal nonnegative utility, with zero when no option qualifies. This directly represents the rule on page 8, including discrete laws. The pessimistic valuation is a finite minimum and the risk-neutral valuation a finite average. Customer type is mixed independently of the valuation law, so the OPQ expectation is the $\alpha$-weighted sum of the two type-specific expectations.

Expected revenues and optimal revenues use extended nonnegative reals $[0,\infty]$. The optima are suprema over nonnegative prices; existence of a maximizing price vector is not assumed. This avoids default values for an unbounded real supremum and records possible infinite revenue. Prices for unused cardinalities are nonnegative but have no effect on the menu. The order statistic sorts the coordinates with multiplicity; it is not defined through the subset identity it is meant to satisfy.

The goal is not implied by a degenerate model: the revenue function charges the highest price among utility maximizers and sells only at nonnegative utility; the optimal revenues range over nonnegative prices; exchangeability is invariance under every coordinate permutation. Contributions toward the finite-menu choice lemmas, permutation-invariant integration, order-statistic identity, two-valued DP structure, and the two cases are within scope.

Selected references

• A. N. Elmachtoub and M. L. Hamilton, The Power of Opaque Products in Pricing, Management Science, 2021, doi:10.1287/mnsc.2020.3750. This mission uses the author's 54-page manuscript, pinned locally by SHA-256 ccd5b53ae01d607eca3b7df8549f418f52245b99bb2dfa050b6f5c4878a3cffe; its printed and PDF page numbers agree.

Motivation

Online marketplaces such as Airbnb, Upwork and eBay match buyers and sellers but do not set transaction prices. They earn revenue through commissions (a fraction of the transaction price) and subscription fees (a fixed charge per transaction), and they often differentiate these fees by participant type. Prices then form endogenously, as a competitive equilibrium of the market the fees induce. Choosing revenue-maximizing fees is therefore a bilevel problem: the platform optimizes over fees, and every choice of fees changes the equilibrium prices and trades. Birge, Candogan, Chen and Saban (SSRN 3259716; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2019.0853) show that, despite its nonconvexity, this problem is solved exactly by a convex program, and they characterize all optimal fee profiles. The rest of their paper, which compares commissions with subscriptions and studies how the network shapes revenue, rests on this result.

Setting

There are finitely many seller types $\mathcal S$ and buyer types $\mathcal B$. A bipartite compatibility network $E\subseteq\mathcal S\times\mathcal B$ says which types can trade; every type has degree at least one. Type $i$ consists of a continuum of sellers of mass $s_i>0$, and type $j$ of buyers of mass $b_j>0$. A type-$j$ buyer's value is distributed according to $F_{b_j}$ on $[0,\bar v_{b_j}]$, and a type-$i$ seller's reservation value according to $F_{s_i}$ on $[0,\bar v_{s_i}]$, with $\bar v\in\mathbb R_+\cup\{\infty\}$. A buyer who trades with a type-$i$ seller incurs a disutility $c_i\ge 0$. Assumption 1 asks that each $F$ be continuous, continuously differentiable and strictly increasing on $(0,\bar v)$, with bounded mean. Its inverse is $F^{-1}$.

The platform picks commissions $\gamma=(\gamma^s,\gamma^b)$ and subscriptions $\mu=(\mu^s,\mu^b)$ in $\Gamma\times\mathcal U$: $\gamma^s_i\in[0,1]$ and $\gamma^b_j,\mu^s_i,\mu^b_j\ge0$. A competitive equilibrium $(p,x,q^s,q^b)\in\mathcal X(\gamma,\mu)$ consists of prices $p\ge 0$, flows $x_{ij}\ge0$ on $E$ and supplies and demands with

$$q^s_i=s_iF_{s_i}\big((1-\gamma^s_i)p_i-\mu^s_i\big),\qquad q^b_j=b_j\Big[1-F_{b_j}\Big(\min_{i':(i',j)\in E}\{(1+\gamma^b_j)p_{i'}+c_{i'}\}+\mu^b_j\Big)\Big],$$

markets clearing ($q^s_i=\sum_jx_{ij}$, $q^b_j=\sum_ix_{ij}$), and buyers trading only with their cheapest compatible sellers. The revenue problem (3) is

$$V_{opt}=\max\ \sum_{(i,j)\in E}(\gamma^s_i+\gamma^b_j)p_ix_{ij}+\sum_{(i,j)\in E}(\mu^s_i+\mu^b_j)x_{ij}\quad\text{s.t. }(p,x,q^s,q^b)\in\mathcal X(\gamma,\mu),\ (\gamma,\mu)\in\Gamma\times\mathcal U.$$

Assumption 2 asks that $uF^{-1}_{b_j}(1-u)$ and $-uF^{-1}_{s_i}(u)$ be strictly concave in $u\in[0,1]$, a regularity condition on both sides of the market. The relaxation (7) is

$$\tilde V_{opt}=\max_{x,q^s,q^b}\ h(q^s,q^b)=\sum_{j}F^{-1}_{b_j}\Big(1-\frac{q^b_j}{b_j}\Big)q^b_j-\sum_iF^{-1}_{s_i}\Big(\frac{q^s_i}{s_i}\Big)q^s_i-\sum_ic_iq^s_i$$

over flows on $E$ with marginals $(q^s,q^b)$, $q^b\le b$ and $q^s\le s$.

Formalization targets

Goal: Theorem 1 (p. 13)

Let $(\bar x,\bar q^s,\bar q^b)$ be an optimal solution of (7). Then (i)

$$V_{opt}\ \text{is attained and}\ V_{opt}=\tilde V_{opt}=h(\bar q^s,\bar q^b),$$

and every optimal solution of (3) has supply-demand vector $(\bar q^s,\bar q^b)$. (ii) For $(\gamma,\mu)\in\Gamma\times\mathcal U$ with $\gamma^s<1$, with $\tilde\gamma^s_i=1/(1-\gamma^s_i)$, $\tilde\mu^s_i=\mu^s_i/(1-\gamma^s_i)$, $\tilde\gamma^b_j=1/(1+\gamma^b_j)$ and $\tilde\mu^b_j=\mu^b_j/(1+\gamma^b_j)$, the pair is optimal if and only if some $p\ge0$ and some optimal flow $x$ of (7) solve the linear system (8a)–(8f).

Milestones

In the order the proof uses them:

• Proposition 1: equilibria exist and are essentially unique.
• Corollary 1: equilibrium revenue is well defined.
• The bound (6): every equilibrium is feasible for (7), with revenue at most $h(q^s,q^b)$.
• Lemma EC.1(ii): regularity of the pieces of $h$.
• Proposition EC.1(i), (iv), (v), (iii) at problem (7): existence, uniqueness of $(\bar q^s,\bar q^b)$, $\bar q^b<b$, and KKT multipliers (EC.3).
• Step (i-2): the subscription-only fees (EC.104) attain $\tilde V_{opt}$.
• Theorem 1(i) on its own.

Significance

The result turns a nonconvex bilevel problem into a convex network-flow problem with separable concave objective: the optimal supply-demand vector is computed without reference to fees or prices. Part (ii) describes the whole set of optimal fees as solutions of a linear feasibility system, which is what the paper uses to compare fee structures: a subscription-only profile is always optimal (Step (i-2)), and the comparisons with homogeneous and one-sided fees (Propositions 4–6) and the analysis of which network positions earn surplus (Theorems 2–3) start from it. No machine-checked version of these results exists on the platform. The mission formalizes the statement chain of the paper's proof (main text and e-companion), including the equilibrium existence and uniqueness of Proposition 1 and the KKT theory of the relaxation.

Difficulty

The bound $V_{opt}\le\tilde V_{opt}$ is a rearrangement. Equality needs an equilibrium that realizes the optimum of (7), and the natural candidate prices are the dual variables of (7). These need not exist with finite values in general: the objective pieces $F^{-1}_{b_j}(1-q/b_j)q$ and $F^{-1}_{s_i}(q/s_i)q$ can have infinite slope at the boundary, for instance for unbounded supports. The proof therefore needs the boundary-slope facts of Lemma EC.1(ii) and a "special" KKT system in derivative form. Proposition 1 needs its own convex program for the equilibrium and is the deepest milestone. In part (ii) the optimal flow of (7) is not unique, so necessity has to use the flow of the equilibrium, not a fixed optimal flow.

Formalization scope

Types are arbitrary finite types; flows are functions $\mathcal S\to\mathcal B\to\mathbb R$ whose values off $E$ are never read. The upper end $\bar v$ of each support is in WithTop ℝ, and $F^{-1}(u)=\inf\{v\ge0:F(v)\ge u\}$ is defined from $F$. The standing assumptions of pp. 7–8 (positive masses, $c\ge0$, degree at least one, each $F$ a continuous CDF extended to $\mathbb R$) are explicit hypotheses. Two conventions concern unbounded supports, where $F^{-1}(1)=\infty$. The feasible set of (7) requires $q^s_i<s_i$ when $\bar v_{s_i}=\infty$, since the paper's objective is $-\infty$ at $q^s_i=s_i$. For the same sellers, Assumption 2 is posed on $[0,1)$; on $[0,1]$ with a finite stand-in value it would be unsatisfiable. "Optimal solutions exist" is stated as attainment (IsGreatest). An optimal fee pair is one for which some equilibrium attains $V_{opt}$. Slopes $g'_j$, $h'_i$ are limits of derivatives from inside the interval (footnote 22). Proposition EC.1 is posed only at the instance (7); the general framework problem (EC.1) is not formalized.

Theorem 1(ii) is stated with an optimal flow of (7), because the printed version with the fixed $\bar x$ is false when optimal flows are not unique. The sentence "the optimal commission-subscription vector is not unique" is not posed. Ruled out as trivializing: defining the revenue of an equilibrium as $h(q^s,q^b)$ instead of (3a); reading "optimal solutions exist" as an unattained supremum; an equilibrium without the buyers' minimum in (2b) or the cheapest-seller restriction (2d); a feasible set of (7) that admits $q^s_i=s_i$ for unbounded sellers at a finite junk cost; and an Assumption 2 that no unbounded seller distribution satisfies.

A complete development needs basic facts on generalized inverses of continuous CDFs, existence and KKT theory for separable concave maximization over a flow polytope (not in Mathlib), and equilibrium existence for Proposition 1. The concave-programming layer is reusable beyond this mission. Proofs of individual milestones, and sanity checks such as uniform or exponential markets, are welcome. The paper's proofs are in its e-companion, which is part of the cited SSRN file (EC.1.1, pp. ec2–ec6; EC.2.1; EC.3.1, pp. ec38–ec44).

Selected references

• J. R. Birge, O. Candogan, H. Chen, D. Saban, Optimal Commissions and Subscriptions in Networked Markets, SSRN abstract 3259716, version of 2019-09-13 (cited version, with e-companion). https://ssrn.com/abstract=3259716
• Same, Manufacturing & Service Operations Management, published version. https://doi.org/10.1287/msom.2019.0853
• L. S. Shapley, M. Shubik, The assignment game I: The core, International Journal of Game Theory 1, 1971. https://doi.org/10.1007/BF01753437

Motivation

A seller with one item and several buyers whose values are private but drawn from known, independent distributions can maximize expected revenue with Myerson's optimal auction (Myerson, 1981). That auction depends on every distribution through virtual values, asks buyers to report their values, and allocates through a computation that buyers must trust. A sequential posted-price (SPP) mechanism is far simpler: the seller fixes one take-it-or-leave-it price per buyer and approaches the buyers one at a time. Posted prices are common in practice, and no buyer reports anything. The natural question is how much revenue this simplicity costs, measured as the worst-case ratio between the best SPP revenue and the optimal revenue.

Timeline. Chawla, Hartline, Malec and Sivan (2010) showed that sequential posted prices earn at least $1 - (1 - 1/n)^n \ge 1 - 1/e \approx 0.632$ of the optimal revenue in the single-unit setting with $n$ independent buyers. Azar, Chiplunkar and Kaplan (2018) improved this to $0.6346$ for $n \ge 74$, which gave the best universal bound before the present paper. No SPP mechanism can guarantee more than about $0.745$ even for i.i.d. values (Hill and Kertz, 1982; Correa et al., 2017). Beyhaghi, Golrezaei, Paes Leme, Pál and Sivan (Operations Research, 2021; arXiv:1807.03435) proved the universal bound $0.6543$, valid for every $n$, together with $n$-dependent, multi-unit and matroid results and a bound of $0.6620$ for eager second-price auctions. This mission formalizes their single-unit universal bound.

Setting

There are $n$ buyers $i \in [n]$. Buyer $i$ has a value $v_i$ drawn from a probability distribution $\mu_i$ on $\mathbb R$, independently across buyers; the profile $v = (v_1,\dots,v_n)$ has law $\mu_1 \otimes \cdots \otimes \mu_n$.

SPP$(p)$. Given prices $p = (p_1,\dots,p_n)$, the mechanism approaches buyers in decreasing order of price, offers $p_i$ to buyer $i$ while the item is unsold, and sells to the first buyer with $v_i \ge p_i$ at price $p_i$. Its revenue at the profile $v$ is therefore $\max\{p_i : v_i \ge p_i\}$ (zero if nobody accepts), and $\mathrm{SPP}(p)$ denotes its expectation.

Threshold mechanisms (the benchmark). By the taxation principle (Lemma 1 of the paper, cited from Nisan et al.), a deterministic truthful mechanism is described by thresholds $t_i(v_{-i}) \ge 0$ depending only on the other buyers' values: buyer $i$ wins and pays $t_i$ when $v_i \ge t_i$. In the single-unit setting, almost surely at most one buyer weakly exceeds their threshold. The expected revenue is $\mathrm{Opt} = \mathbb E[\sum_i t_i \mathbf 1\{v_i \ge t_i\}]$. Define

$$s^\star_i(\tau) = \mathbb P[v_i \ge t_i \ge \tau], \qquad s^\star(\tau) = \sum_i s^\star_i(\tau),$$

so that $\mathrm{Opt} = \int_0^\infty s^\star(\tau)\,d\tau$ (Equation (1)).

Two pricing rules. Myersonian prices post to buyer $i$ the threshold $t'_i = t_i(v'_{-i})$ computed on an independent re-sample of the other buyers' values, freshly for each $i$; MP is the resulting expected revenue and $m(\tau)$ the probability that some buyer has $v_i \ge t'_i \ge \tau$. The uniform price rule posts the same price $\tau$ to everyone; $\mathrm{UP} = \sup_{\tau \ge 0}\mathrm{SPP}(\tau,\dots,\tau)$.

The factor-revealing program (FR). With $f(x) = 1 - e^{-x}$,

$$\mathrm{FR} = \max_{s}\ \int_0^\infty s(\tau)\,d\tau \quad\text{s.t.}\quad 0 \le s(\tau) \le \min(1, 1/\tau)\ \ \forall \tau \ge 0,\quad \int_0^\infty f(s(\tau))\,d\tau \le 1,\quad s \text{ weakly decreasing}.$$

Formalization targets

Goal: Theorem 1 (p. 13)

For every $n$, every independent value distributions and every single-unit threshold mechanism with finite expected revenue $\mathrm{Opt}$, there is a vector of nonnegative prices $p$ with

$$\mathrm{SPP}(p) \ \ge\ 0.6543 \cdot \mathrm{Opt}.$$

The prices depend on the instance; the constant does not.

Milestones, in the order the proof uses them

1. Equation (1), p. 12: $\mathrm{Opt} = \int_0^\infty s^\star(\tau)\,d\tau$ and $s^\star$ is weakly decreasing.
2. Inequality (2), p. 14: $\tau\, s^\star(\tau) \le \mathrm{SPP}(\tau,\dots,\tau)$ for $\tau \ge 0$, hence $\sup_{\tau \ge 0}\tau s^\star(\tau) \le \mathrm{UP}$; and $s^\star \le 1$.
3. Lemma 2, Inequality (5), p. 15: $\mathbb P[Z_\tau = 0] \le (1 - s^\star(\tau)/n)^n \le e^{-s^\star(\tau)}$, where $Z_\tau$ counts buyers with $v_i \ge t'_i \ge \tau$.
4. Inequalities (3)–(4), p. 14: $\mathrm{MP} = \int_0^\infty m(\tau)\,d\tau$ and $m(\tau) \ge 1 - e^{-s^\star(\tau)}$.
5. Solving Problem (FR), p. 15: the root $\tau^\star > 1$ of $(1 - e^{-1}) + \int_1^{\tau^\star}(1 - e^{-1/\tau})\,d\tau = 1$ is unique and lies in $[1.6955, 1.6965]$.
6. Solving Problem (FR), p. 15: the optimal value of (FR) is attained and equals $1 + \ln\tau^\star$, which is at most $1.5283$.

The intermediate statement $\max(\mathrm{MP}, \mathrm{UP}) \ge 0.6543 \cdot \mathrm{Opt}$, the "best of Myersonian and uniform" form shown first in the proof, is context only: Theorem 1 asserts one deterministic price vector, and that is the goal.

Significance

The result. Theorem 1 was the first improvement over $1 - 1/e$ for single-unit posted pricing that holds for every number of buyers and for arbitrary (regular or irregular) independent distributions. It quantifies the price of simplicity of posted pricing against the optimal auction, and its method (two pricing rules, each giving one constraint on the revenue curve $s^\star$, and a factor-revealing program over all curves meeting both) is reused in the paper for $n$-dependent, multi-unit, position-auction and eager second-price bounds.

Formalizing it. The result is proved on paper; no machine-checked version exists. A formalization checks the probabilistic core, the solution of an infinite-dimensional program, and the numerical constants. The printed constants carry rounding slips ($\tau^\star = 1.696$ is a rounding of $1.69572\ldots$; $1 + \ln\tau^\star = 1.52810\ldots$, printed as $1.5283$), which the milestones state precisely. The paper's normalization $\max(\mathrm{MP}, \mathrm{UP}) = 1$ silently assumes that Opt is finite; the formal statement makes that hypothesis explicit.

Difficulty

The Myersonian rule alone gives only $1 - 1/e$, and the paper's example (values uniform on $[1, 1+\epsilon]$) shows this is tight for it; the uniform rule alone is also bounded away from 1. The improvement comes only from combining them, and the combination is expressed as an optimization over all decreasing curves $s$: the step that the obvious argument misses is the exact solution of (FR), whose optimum must be guessed and certified for an infinite-dimensional program with a nonlinear constraint. The probabilistic step is subtle as well: the true thresholds $t_i$ are correlated across buyers, and Lemma 2 holds only for the independently re-sampled $t'_i$. Finally, the theorem claims a single deterministic price vector, so the random Myersonian prices and a possibly unattained best uniform price must both be converted into one concrete $p$, with the slack between $0.6543$ and $1/\mathrm{FR} = 0.65440\ldots$ absorbing the approximation.

Formalization scope

Buyers are Fin n; values have law Measure.pi μ with each μ i a probability measure on ℝ; values need not be nonnegative. Revenues and probabilities are in ℝ≥0∞ (lower Lebesgue integrals and measures), never Bochner integrals, so that a non-integrable revenue cannot become a junk zero. The SPP revenue at a profile is the closed form $\max\{p_i : v_i \ge p_i\}$ of the price-ordered sale. A threshold mechanism is a family t i v with t i measurable, nonnegative, independent of coordinate i, and almost surely at most one buyer with t i v ≤ v i. Myersonian prices are read from a fresh copy of the whole profile per buyer, independent of everything else. In (FR) the constraint $s(\tau) \le \min(1, 1/\tau)$ is encoded as $s(\tau) \le 1$ and $\tau s(\tau) \le 1$.

Benchmark. The goal is stated for every single-unit threshold mechanism, which is the taxation-principle form of Lemma 1; for the optimal mechanism's thresholds it is the printed theorem, and the paper's proof never uses optimality. Lemma 1 and Myerson's theorem are cited by the paper and are not part of the mission. The one added hypothesis on the goal, finiteness of Opt, is necessary: without it some single-unit threshold mechanisms have infinite revenue while every posted-price revenue is finite.

Ruled out. The SPP revenue is the revenue of the actual sequential sale, not a free function; thresholds may not depend on the buyer's own value (that would allow full surplus extraction) and must be single-unit feasible (otherwise Opt could be $n$ times any posted-price revenue); the constant is the explicit $0.6543$, not an existential one.

Out of scope. Theorem 2 ($n$-dependent bounds), Theorem 3 and Lemmas 3–4 (multi-unit), Lemmas 5–7 and Theorem 4 (position auctions), the partition-matroid claim and Proposition 1 (matroids), Lemma 8 and Theorems 5–6 (eager second-price auctions), Inequality (6) of Lemma 2, the $(1-1/e)$ illustration of §4.1, and the numerical tables.

Infrastructure. The development needs the layer-cake formula for lower integrals, independence under product measures, the AM–GM inequality and $(1 - y/n)^n \le e^{-y}$, all in Mathlib, plus a numerical certificate for the root of a transcendental equation. The threshold-mechanism and SPP definitions are reusable for the multi-unit and matroid results of the same paper. Proofs of any milestone, alternative arguments, and sharper constants are welcome.

Selected references

• H. Beyhaghi, N. Golrezaei, R. Paes Leme, M. Pál, B. Sivan, Improved Revenue Bounds for Posted-Price and Second-Price Mechanisms, Operations Research 69(6), 2021. arXiv:1807.03435v4. https://arxiv.org/abs/1807.03435
• R. B. 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, D. L. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, STOC 2010. https://doi.org/10.1145/1806689.1806733
• Y. Azar, A. Chiplunkar, H. Kaplan, Prophet Secretary: Surpassing the 1 − 1/e Barrier, ACM EC 2018, 303–318. https://doi.org/10.1145/3219166.3219182
• J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted Price Mechanisms for a Random Stream of Customers, ACM EC 2017, 169–186. https://doi.org/10.1145/3033274.3085137
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Theorem 9.36.

Motivation

When customers request a customized product, their requests can reveal information about what they value. A seller can use that information when setting a price, while a customer can choose a request with the resulting price in mind. The question is whether customers with different preferences can make different requests in equilibrium. Liang Guo's The Voice of Customers in Customization, §3.3, studies this question in a two-type model of buyer-led product design, called O-Learning. It compares O-Learning with a separate game in which the seller chooses quality after a customer's cheap-talk message. This mission concerns only the O-Learning game.

Proposition 3 of the SSRN author copy identifies when a particular cheap-signaling equilibrium exists: each type asks for the quality it would prefer if its type were known. Section 3.3 then asks whether a different pair of requests could separate the types when that equilibrium fails. The Appendix, under “No Other Separating Equilibrium under the O-Learning Customization,” establishes nonexistence below the same threshold. It is this latter claim, for every request pair and every admissible off-path belief, that is the mission's target.

Setting

A buyer has one-unit demand and a privately known quality preference $\theta\in\{\theta_H,\theta_L\}$, where $\theta_H>\theta_L>0$. A fraction $\alpha\in(0,1)$ of buyers have the high preference. Quality is a real number $q\ge0$. Producing or delivering a product of quality $q$ costs $kq^2$, while preparing to sell it costs $sq^2$, with $k,s>0$. The latter is sunk before the price is determined. These are the assumptions of §2 of the paper, pp. 5–9.

Under O-Learning, the buyer requests a quality. The seller observes the request, forms a perceived type $\hat\theta$, and accepts or rejects. If rejected, both parties receive zero. If accepted, the price-setting stage follows the paper's reduced-form bargaining rule: the seller has the opportunity to make the price offer with probability $\gamma\in(0,1)$ and the buyer has it with probability $1-\gamma$. The buyer's expected payoff, conditional on acceptance, is equation (9):

$$\mu(q,\theta,\hat\theta) =\gamma\max\{\theta q-\hat\theta q,0\} +(1-\gamma)\max\{\theta q-kq^2,0\}.$$

The seller accepts precisely when $\gamma(\hat\theta q-kq^2)-sq^2\ge0$, including equality. A separating pure-strategy equilibrium consists of two distinct, nonnegative requests $q_H$ and $q_L$, plus a belief about the buyer's type after each possible request. The seller identifies the correct type at $q_H$ and $q_L$; away from those two requests its belief can vary. Given that belief and the seller's acceptance rule, neither buyer type can improve its payoff by making any other nonnegative request. The pricing stage is represented by the payoff formula rather than by a separate bargaining game, as in §3.3 of the source.

For a buyer whose type is known, equation (10) gives the complete-information request

$$q^*(\theta)=\min\left\{\frac{\gamma\theta}{s+\gamma k},\frac{\theta}{2k}\right\}.$$

Proposition 3 defines three ratios and their combined threshold:

$$\Lambda_{H1}=\frac{\gamma(s+k)}{(1-\gamma)s},\qquad \Lambda_{H2}=\frac{1+\gamma}{1-\gamma},\qquad \Lambda_L=\frac{s}{\gamma k},\qquad \Lambda=\max\{\min(\Lambda_{H1},\Lambda_{H2}),\Lambda_L\}.$$

The prior $\alpha$ is part of the model, although the separation threshold does not depend on it.

Formalization targets

No separation below the threshold

The goal says that, whenever the standing assumptions hold,

$$\frac{\theta_H}{\theta_L}<\Lambda \quad\Longrightarrow\quad \text{there is no separating pure-strategy equilibrium of the O-Learning game}.$$

Equivalently, the existence of any such equilibrium requires $\theta_H/\theta_L\ge\Lambda$. The goal quantifies over all pairs of nonnegative requests and all belief functions consistent at those requests. It does not prescribe the requests $q^*(\theta_H),q^*(\theta_L)$ or Proposition 3's supporting off-path beliefs.

The milestone list follows the two failure regimes stated in the Appendix, pp. 28–29. When $\theta_H/\theta_L<\min\{\Lambda_{H1},\Lambda_{H2}\}$, it first identifies the low type's equilibrium request and then rules out separation. When $\theta_H/\theta_L<\Lambda_L$, it records the form of $q^*$ and the bounds on acceptable equilibrium requests before ruling out separation in either order of $q_H$ and $q_L$. These are the author's stated intermediate claims, with their source text attached to each milestone.

Significance

Proposition 3 shows when the two complete-information requests can be sustained as a separating equilibrium. The Appendix result strengthens the interpretation of its threshold: below $\Lambda$, changing the requests or the off-path beliefs cannot restore separation. This matters for the paper's comparison of who controls quality design and when customization can reveal preferences. Without the nonexistence result, the failure of the cheap-signaling request profile would leave open another separating profile with distorted qualities.

The result is proved in the SSRN author copy, and this mission asks for a machine-checked version of that proof. The proposed definitions and statements compile as Lean declarations, but their proofs are open. A completed development would also supply reusable calculations about the seller's acceptance range and buyer payoffs with quadratic costs and endogenous beliefs. The milestones identify these specific pieces of work; they do not claim that a general signaling-game library is already formalized.

Difficulty

Ruling out just the request profile $q^*$ would be insufficient. An equilibrium candidate can use another pair of qualities and can assign either type to requests outside its path. Acceptance changes the payoff discontinuously: a request that would be attractive if accepted instead pays zero when rejected. The buyer's conditional payoff also contains two $\max\{\cdot,0\}$ terms, so a polynomial formula obtained on an accepted range need not hold at every quality. The main challenge is to control all deviations and beliefs under the actual acceptance rule, while maintaining the strict threshold inequalities in both failure regimes.

Formalization scope

Lean uses a two-constructor buyer type, a model with real parameters $\theta_H,\theta_L,\alpha,\gamma,k,s$, and a predicate for the paper's standing assumptions: $\theta_H>\theta_L>0$, $0<\alpha<1$, $0<\gamma<1$, $k>0$, and $s>0$. Requests and deviations are restricted to $q\ge0$. Beliefs are total functions from real requests to the two named types, constrained only at the equilibrium requests. Seller acceptance is the printed inequality and accepts at equality; a rejected request pays zero. The conditional payoff retains both maxima from equation (9), and $\Lambda$ is the printed expression, not a value defined through equilibrium existence. No fixed cost for learning or customization is included, as in the paper's main analysis.

The equilibrium predicate does not fix off-path beliefs, require the requests to equal $q^*$, or replace seller acceptance with a derived threshold. The proof therefore cannot become a restatement of Proposition 3. The local O-Learning definitions duplicate the draft model of the companion mission because unpublished drafts cannot be imported. The paper's last sentence on p. 19 calls the cheap-signaling equilibrium “the only separating equilibrium.” The Appendix proves nonexistence when the ratio is below $\Lambda$; it does not establish global uniqueness when the ratio is above it, and global uniqueness is false. This mission states the Appendix's precise claim.

Selected references

• Liang Guo, The Voice of Customers in Customization, SSRN working paper 3994319, author copy dated 2023-11-29, §§2 and 3.3, Proposition 3 and Appendix pp. 28–29. SSRN; Management Science DOI.

Motivation

Advertising platforms repeatedly sell opportunities to show an advertisement. The opportunity's features, such as audience and placement, affect each advertiser differently, while advertisers limit their average spending. This makes the efficiency of an auction a question about both heterogeneous values and budgets. The paper by Balseiro, Kroer, and Kumar studies this setting with a continuum of buyer types and context-dependent values. It constructs equilibria by value pacing, in which a buyer scales values before bidding. This mission asks how much attainable value those equilibria preserve when budgets cap useful value.

Earlier efficiency bounds for second-price auctions concern a different, non-Bayesian multi-item model. In particular, the half guarantee discussed by Azar and coauthors, as discussed in §5 of the paper uses a no-overbudgeting condition that the present pacing equilibria need not satisfy. Balseiro, Kroer, and Kumar prove their bound under their own contextual and in-expectation budget model; the distinction matters when interpreting the constant. Their existence and revenue-equivalence results also make it possible to speak about the same pacing-based allocation across standard auction payment rules. These claims and the limitation of the earlier assumption are explained in §5 of the paper.

Setting

An item has a context $\alpha\in A\subset\mathbb R^d$, with $d\ge2$. There are $n\ge2$ buyers. Each buyer has a private type $\theta=(w,B)$: the vector $w\in(0,U)^d$ assigns a positive weight to every context feature, and $B\in(B_{\min},U)$ is the buyer's budget, where $0<B_{\min}<U$. The buyer's value for the item is $w^\top\alpha$. A context is drawn from a distribution $F$ and buyers' types are drawn independently from a distribution $G$; both distributions have densities. The context and type ranges are the spaces $A$ and $\Theta=(0,U)^d\times(B_{\min},U)$ of §2. The reserve price is zero throughout the efficiency section.

A pacing function $\mu:\Theta\to\mathbb R_{\ge0}$ scales type $\theta$'s value to $w^\top\alpha/(1+\mu(\theta))$. Let $H^\mu_\alpha(x)$ be the probability that the maximum paced value among $n-1$ independent competitors is at most $x$. The first-price bid $\beta^\mu(\theta,\alpha)$ applies the paper's bid function $\sigma^\mu_\alpha$ to the paced value. A buyer may choose a context-dependent bid, subject to an in-expectation budget: expected payment over contexts and competitors must not exceed $B$. The buyer's dual function $q^\mu(\theta,t)$ is the supremum of its Lagrangian over such bids at multiplier $t\ge0$.

The relevant pacing equilibria are fixed points of the correspondence $C_0^*$. Its domain $X_0$ consists of measurable, integrable pacing functions in $[0,\omega/B_{\min}]$ with total variation at most $V_0=(d+1)U^{d+1}\omega/B_{\min}$, where $\omega$ is the supremum of possible values. For a given $\mu\in X_0$, $C_0^*(\mu)$ minimizes the average dual objective $\mathbb E_{\theta\sim G}[q^\mu(\theta,\widehat\mu(\theta))]$ over $\widehat\mu\in X_0$. These are the objects of §3.3, including its multivariate definition of total variation.

An allocation $x$ assigns nonnegative shares $x_i(\alpha,\theta_1,\ldots,\theta_n)$ summing to one. For buyer $i$, keep $\theta_i=(w_i,B_i)$ fixed while averaging $w_i^\top\alpha\,x_i$ over the context and the other types. The buyer's liquid welfare is the smaller of this interim value and $B_i$; total liquid welfare $\mathrm{LW}(x)$ sums its expectation over each buyer's own type. For an equilibrium pacing function $\mu\in C_0^*(\mu)$, $x^\mu$ allocates to a highest paced bidder. Definitions 5 and 6 use this allocation to define the worst equilibrium liquid welfare relative to the optimal allocation.

Formalization targets

The main target is the Theorem 3 guarantee, stated for every measurable allocation $x$ and every equilibrium pacing function $\mu$:

$$\mathrm{LW}(x^\mu)\ge\tfrac12\,\mathrm{LW}(x).$$

The universal comparison expresses the paper's price-of-anarchy bound $\mathrm{PoA}\ge1/2$. It leaves no optimum or worst equilibrium as an arbitrary variable. The two milestones are the dual derivative identity and the first-order budget and complementary-slackness conditions stated in §3.2:

$$\partial_t q^\mu(\theta,t)=B-\mathrm{payment}(b_t),\qquad \mathrm{payment}(b_{t^*})\le B,\quad t^*(B-\mathrm{payment}(b_{t^*}))=0.$$

Here $b_t(\alpha)=\sigma^\mu_\alpha(w^\top\alpha/(1+t))$ and $t^*$ minimizes $q^\mu(\theta,\cdot)$ over nonnegative multipliers. The milestones are posed in the zero-reserve setting used by the main target.

Significance

The theorem gives an explicit welfare guarantee despite private budgets, correlated values across buyers through a shared context, and equilibrium bidding that depends on those budgets. It applies to the allocation induced by pacing in every standard auction covered by the paper, since those auctions have the same equilibrium allocation even when payment rules differ Balseiro, Kroer, and Kumar, §4–5. Without an efficiency bound, existence of a pacing equilibrium alone would give no quantitative assurance about the allocation it produces.

The result has a mathematical proof in the paper's online appendix; it is an open formalization target here. A complete development would connect measurable Bayesian auctions, the buyer's nonconvex dual problem, the bounded-variation fixed-point domain, and interim liquid welfare. The definitions of interim welfare, dual expenditure, and multivariate variation can support other budgeted auction results. The source PDF held for this mission contains the published main article but not its online appendix, where the proofs and auxiliary lemmas appear.

Difficulty

The expected budget applies to each buyer type after averaging over contexts and opponents, while liquid welfare caps that same type's interim value before averaging over types. Moving the budget cap across the expectation changes the quantity. The natural first-price tie convention also awards the good to every highest bidder for the buyer optimization problem, while a welfare allocation must give total share one. The proof must reconcile the dual account of expenditure with a feasible allocation and preserve these different orders of expectation. The dual objective is a supremum over bids, so its derivative cannot be obtained merely by differentiating a chosen closed formula without justifying that formula and the maximizing bid.

Formalization scope

Lean represents a context by Fin d → ℝ and a buyer type by its weight vector and real budget. Value is the explicit finite sum $\sum_i w_i\alpha_i$. The model requires a nonempty bounded measurable context set in the positive orthant, absolutely continuous probability laws $F$ and $G$ supported on their stated domains, measurable reserves and pacing, $n\ge2$, and $0<B_{\min}<U$. Boundedness of $A$ makes $\omega$ finite; these conditions make the domain and integrals implicit in the article well posed. The welfare target assumes zero reserves as §5 does.

Admissible bids are measurable and nonnegative on $A$, with integrable expected payment. The dual is defined by its supremum over bids. Total variation is extended-real-valued and uses Euclidean lengths of test fields; thus infinite variation cannot satisfy the $X_0$ bound through a real supremum's default value. Allocations are measurable and simplex-valued on the model domain. At a tied highest bid, $x^\mu$ splits the item equally; ties have probability zero under these equilibria, as the paper states by its appendix Lemma 6(d). The closed simplex permits zero shares, correcting the paper's notation $\mathbb R_+$ in Definition 5, which §2.1 otherwise calls strictly positive. The universal welfare inequality avoids default real infimum and supremum values on pathological sets. Contributions to the measurable bidding, variation, duality, and welfare infrastructure are all useful within this scope.

Selected references

• Santiago R. Balseiro, Christian Kroer, and Rachitesh Kumar, Contextual Standard Auctions with Budgets: Revenue Equivalence and Efficiency Guarantees, Management Science, Articles in Advance, 2023. DOI: 10.1287/mnsc.2023.4719.

Motivation

Most online advertising is sold by auction, one impression at a time, to advertisers who manage a budget over many auctions rather than a value for a single one. Since 2019 the major ad exchanges have moved from second price to first price auctions, in which the winner pays its own bid. A budget-constrained advertiser in a first price auction must therefore shade its bids twice: once because of the budget, and once because of the payment rule. Whether these two effects admit a coherent equilibrium, and of what form, is the question behind Balseiro, Kroer and Kumar, Contextual Standard Auctions with Budgets: Revenue Equivalence and Efficiency Guarantees (Management Science, 2023, doi:10.1287/mnsc.2023.4719).

Earlier work on pacing equilibria treated second price auctions, where truthful bidding is dominant without budgets (Balseiro, Besbes and Weintraub 2015; Conitzer et al. 2022). In first price auctions with a single deterministic item, an equilibrium may fail to exist (the paper's Online Appendix A). The paper restores existence by letting items carry a random context and values depend on it linearly. This mission formalizes its first main result, Theorem 1: an equilibrium of a simple, interpretable form exists.

Setting

An item has a context $\alpha\in A\subset\mathbb R^d_{+}$, a feature vector drawn from a law $F$ with a density. There are $n$ buyers. Each buyer has a type $\theta=(w,B)$, a weight vector $w$ and a budget $B$, drawn independently from a law $G$ with a density on

$$\Theta=(0,U)^d\times(B_{\min},U).$$

Buyer $(w,B)$ values item $\alpha$ at $w^T\alpha$, and $\omega:=\sup_{(w,B)\in\Theta,\alpha\in A}w^T\alpha$. The seller reveals $\alpha$, then runs a first price auction with a public reserve price $r(\alpha)$: a bid $b(\alpha)$ wins if $b(\alpha)\ge\max(r(\alpha),\{\beta(\theta_i,\alpha)\}_i)$, where $\beta$ is the strategy of the $n-1$ competitors, and the winner pays its bid. A budget only needs to hold in expectation over $\alpha$ and the competitors' types.

A strategy $\beta^*:\Theta\times A\to\mathbb R_{\ge0}$ is a symmetric first price equilibrium (SFPE, Definition 1) if for $G$-almost every type $(w,B)$ the bid function $\beta^*(w,B,\cdot)$ solves

$$\max_{b:A\to\mathbb R_{\ge0}}\ \mathbb E\big[(w^T\alpha-b(\alpha))\mathbb 1\{b(\alpha)\ge\max(r(\alpha),\{\beta^*(\theta_i,\alpha)\}_i)\}\big]\ \ \text{s.t.}\ \ \mathbb E\big[b(\alpha)\mathbb 1\{\cdots\}\big]\le B .$$

A pacing function $\mu:\Theta\to\mathbb R_{\ge0}$ scales values down to paced values $w^T\alpha/(1+\mu(w,B))$. Let $H^\mu_\alpha$ be the distribution function of the highest of $n-1$ i.i.d. paced values, and for $x\ge r(\alpha)$ let

$$\sigma^\mu_\alpha(x)=x-\int_{r(\alpha)}^x\frac{H^\mu_\alpha(s)}{H^\mu_\alpha(x)}\,ds,$$

with $\sigma^\mu_\alpha(x)=0$ if $H^\mu_\alpha(x)=0$ and $\sigma^\mu_\alpha(x)=x$ if $x<r(\alpha)$. The value pacing–based strategy (Definition 2) is

$$\beta^\mu(w,B,\alpha)=\sigma^\mu_\alpha\Big(\frac{w^T\alpha}{1+\mu(w,B)}\Big).$$

For a buyer facing competitors who use $\beta^\mu$, the dual function is $q^\mu(w,B,t)=\sup_b\mathbb E[(w^T\alpha-(1+t)b(\alpha))\mathbb 1\{\cdots\}]+tB$ for $t\ge0$.

Formalization targets

Goal: Theorem 1 (p. 7)

$$\exists\,\mu:\Theta\to\mathbb R_{\ge0}\quad\text{such that}\quad \beta^\mu\ \text{is an SFPE}.$$

Milestones

• Lemma 1 (p. 8): for every type and every $t\ge0$, $\sigma^\mu_\alpha(w^T\alpha/(1+t))$ maximizes the Lagrangian $\mathbb E[(w^T\alpha/(1+t)-b(\alpha))\mathbb 1\{\cdots\}]$.
• Proposition 1 (p. 8): on a set $\Theta'$ of full $G$-measure, for every $\mu$, a minimizer $t^*$ of $q^\mu(w,B,\cdot)$ over $t\ge0$ makes $\sigma^\mu_\alpha(w^T\alpha/(1+t^*))$ optimal for the budget-constrained problem $Q^\mu(w,B)$.
• Lemma 2 (p. 10): the smallest minimizer $\ell^\mu(w,B)$ of $q^\mu(w,B,\cdot)$ over $[0,\omega/B_{\min}]$ is nondecreasing in each $w_i$ and nonincreasing in $B$.
• Lemma 3 (p. 10): $\ell^\mu\in L_1(\Theta)$ and its total variation is at most $V_0=(d+1)\max(U^d,U^{d+1})\,\omega/B_{\min}$. The paper prints $(d+1)U^{d+1}\omega/B_{\min}$, which agrees when $U\ge1$. For $U<1$ the printed bound fails by a rescaling argument, and the mission corrects the exponent to $d$ there.
• Lemma 4 (p. 10): $\mathcal X_0=\{\mu\in L_1(\Theta):0\le\mu\le\omega/B_{\min},\ V(\mu,\Theta)\le V_0\}$ is nonempty, compact and convex in $L_1(\Theta)$; $f(\mu,\hat\mu)=\mathbb E_G[q^\mu(w,B,\hat\mu(w,B))]$ is continuous; $C^*_0(\mu)=\arg\min_{\hat\mu\in\mathcal X_0}f(\mu,\hat\mu)$ is upper hemicontinuous with nonempty, convex, compact values.
• Lemma 5 (p. 10): a fixed point $\mu\in C^*_0(\mu)$ satisfies $\mu(w,B)\in\arg\min_{t\in[0,\omega/B_{\min}]}q^\mu(w,B,t)$ almost surely.
• Proposition 2 (p. 9): some $\mu$ satisfies $\mu(w,B)\in\arg\min_{t\ge0}q^\mu(w,B,t)$ almost surely.

The paper states that Proposition 2 combined with Proposition 1 implies Theorem 1.

Significance

Theorem 1 says that budget-constrained buyers in contextual first price auctions have an equilibrium that is described by one scalar per type: shade the value by the factor $1/(1+\mu(w,B))$, then bid as an unconstrained buyer would in an i.i.d. first price auction against paced competitors. This is the object on which the rest of the paper is built: revenue equivalence across standard auctions (Theorem 2) and a liquid-welfare price of anarchy of at least $1/2$ (Theorem 3) are both statements about pacing-based equilibria. Practically, it supports the use of pacing for budget management in first price auctions, with pacing multipliers computed as for second price auctions.

The result is proved in the paper; every proof is in its online appendix, which is not part of the source this mission cites. Nothing in the paper is formalized. A formalization would check a strong-duality argument for a non-convex problem and an infinite-dimensional fixed-point argument whose topology the authors chose with care, and it would produce reusable pieces: multivariate total variation, compactness of bounded-variation sets in $L_1$, and the first price equilibrium bid against an arbitrary (possibly atomic) value distribution with a reserve price.

Difficulty

The buyer's problem $Q^\mu(w,B)$ is not convex in the bid function, so standard convex duality does not give strong duality; Proposition 1 needs a direct argument combining Lagrangian optimality (Lemma 1), differentiability of $q^\mu$ in $t$, and complementary slackness. Lemma 1 itself cannot quote the textbook first price equilibrium, because the paced value distribution $\lambda^\mu_\alpha$ may have atoms and the reserve price creates discontinuities.

The fixed point lives in an infinite-dimensional space of pacing functions. The obvious topologies fail: the set $\mathcal X$ of bounded pacing functions is not compact in any $L_p$, and in the weak-* topology of $L_\infty$ upper hemicontinuity of the best-response correspondence is hard to obtain; restricting to Lipschitz functions loses the property that best responses stay in the set. The paper restricts to functions of bounded total variation, which requires the monotonicity of Lemma 2 and the variation bound of Lemma 3.

Formalization scope

Contexts are Fin d → ℝ, types are pairs (w, B) : (Fin d → ℝ) × ℝ, and $w^T\alpha$ is the explicit sum $\sum_i w_i\alpha_i$. A single Model structure holds $d,n,U,B_{\min},A,F,G,r$, and Model.Standing collects the assumptions of §2.2 together with four that the paper uses without stating them: $n\ge2$, $B_{\min}<U$, $A$ nonempty and bounded (so $\omega<\infty$), and measurability of $A$ and $r$. Pacing functions are measurable functions on $\mathbb R^d\times\mathbb R$ that are nonnegative on $\Theta$; values off $\Theta$ are irrelevant since $G(\Theta^c)=0$.

The conventions fixed in Lean:

• Ties win: the indicator is $b(\alpha)\ge\max(\cdots)$, as in the paper's tie-breaking rule.
• An admissible bid function is measurable, nonnegative on $A$, and has an integrable payment integrand. The problem of Definition 1, $Q^\mu$, $q^\mu$ and the Lagrangian of Lemma 1 all range over this class.
• An SFPE is jointly measurable in $(\theta,\alpha)$, so Theorem 1 must produce a measurable strategy.
• $q^\mu$ is the supremum over bids of p. 7, not the closed form of p. 8. $\sigma^\mu_\alpha$ has an explicit branch for $H^\mu_\alpha(x)=0$.
• Argmins are stated as membership plus IsMinOn, over $t\ge0$ in Propositions 1–2 and over $[0,\omega/B_{\min}]$ in Lemma 5 and $\ell^\mu$, as printed.
• $V(u,\Omega)$ takes values in EReal, with Euclidean $\|\phi(x)\|\le1$ and test fields supported in $\Omega$; $L_1(\Theta)$ is with respect to Lebesgue measure. Lemma 4 is stated on the image of $\mathcal X_0$ in Lp ℝ 1 (volume.restrict Θ), in its norm topology.

A formalization in which $q^\mu$ is defined by its closed form, in which non-integrable payments count as zero, or in which the strategy need not be measurable would make the milestones easier without proving the paper's theorem; these readings are excluded by the definitions above.

A complete development needs: first price equilibrium bids for general atomic distributions with reserves; measurability of parametric integrals; a duality argument for one-dimensional Lagrangian relaxations; multivariate bounded variation and its compact embedding in $L_1$ of a box; and the Kakutani–Fan–Glicksberg theorem in a locally convex space. The bounded-variation and fixed-point parts are reusable beyond this mission. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

• S. R. Balseiro, C. Kroer, R. Kumar, Contextual Standard Auctions with Budgets: Revenue Equivalence and Efficiency Guarantees, Management Science, Articles in Advance, 2023. https://doi.org/10.1287/mnsc.2023.4719
• S. R. Balseiro, O. Besbes, G. Y. Weintraub, Repeated Auctions with Budgets in Ad Exchanges: Approximations and Design, Management Science 61(4), 2015. https://doi.org/10.1287/mnsc.2014.2022
• V. Conitzer, C. Kroer, E. Sodomka, N. E. Stier-Moses, Multiplicative Pacing Equilibria in Auction Markets, Operations Research 70(2), 2022. https://doi.org/10.1287/opre.2021.2167
• V. Krishna, Auction Theory, 2nd ed., Academic Press, 2009.
• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised ed., CRC Press, 2015.