All missions

Selecting many products over a short season

An online retailer choosing which low-demand products to display, and to stock in its urban warehouses, faces an unusual learning problem. Thousands of products must be chosen at once, the selection can change only a few times per season, and sales data arrive only for the products that were offered. Jin, Simchi-Levi, Wang, Wang and Yang (arXiv:1903.07844v2) model this as a stochastic linear semi-bandit in which the number $K$ of selections per period is large and the number $T$ of periods is small. Their study uses data from Alibaba Tmall.

The problem belongs to a line of work on linear bandits. Abbasi-Yadkori, Pál and Szepesvári (2011) gave the OFUL algorithm and its confidence ellipsoids for one action per period. Chu, Li, Reyzin and Schapire (2011) bounded the sum of confidence widths used in the analysis. Qin, Chen and Zhu (2014) and Wen, Kveton and Ashkan (2015) studied richer semi-bandit models, but their bounds carry terms such as $K\sqrt{dT}$, which are of little use when $K$ is large and $T$ is small.

The model and the algorithm

There are $N$ products, each with a known feature vector $x_i\in\mathbb R^d$, and an unknown parameter $\theta^*\in\mathbb R^d$ with $\|\theta^*\|\le1$, $\|x_i\|\le1$. Product $i$ has positive sales with probability $\mu(i)=x_i^\top\theta^*\in[0,1]$. In each period $t\in[T]$ the retailer offers a set $S_t$ of $K$ products and observes binary outcomes $r_{t,i}$ for $i\in S_t$, which are independent across products and periods. The regret against an optimal $K$-set $S^*$ is

$$R(T)=\sum_{t=1}^T\sum_{i\in S^*}\mu(i)-\sum_{t=1}^T\sum_{i\in S_t}\mu(i).$$

ConsUCB keeps the matrices $A_t$ and vectors $b_t$ of regularized least squares, with $A_0=I$ and $b_0=0$, and the estimate $\theta_t=A_{t-1}^{-1}b_{t-1}$. Within a period it selects $K$ products one at a time. The $k$-th selection maximizes, over the products not yet selected, the score

$$p_{t,k}(i)=x_i^\top\theta_t-\alpha\sqrt{x_i^\top A_{t-1}^{-1}x_i}+2\alpha\sqrt{x_i^\top A_{t,k-1}^{-1}x_i},$$

where $A_{t,0}=A_{t-1}$ and $A_{t,k}=A_{t,k-1}+x_jx_j^\top$ for the selected product $j$. The second radical shrinks after each selection, using features only: no outcome of the period is seen until all $K$ products are chosen.

Formalization targets

Goal: Theorem 3

For $d\ge1$, $1\le K\le N$, $T\ge1$, $\delta\in(0,1)$, every instance, every optimal set $S^*$ and every tie-break depending on the observed history, ConsUCB with $\alpha=\sqrt{d\ln((1+N+TN)/\delta)}+1$ satisfies, with probability at least $1-\delta$,

$$R(T)\le K+\alpha K+10\alpha\sqrt{dKT\log(KT)}.$$

This is the explicit bound printed at the end of the proof; it implies the theorem's $\tilde O(K\sqrt d+d\sqrt{KT})$.

Milestones

In the order of the proof: the confidence event (4), the monotonicity of the widths, the inequalities (5)–(6), Proposition 1, the regret decomposition, the first line of the final display, the boundary terms, Lemma 2 with the correction $KT\ge2$, and the rewriting of the bound in $\tilde O$ form.

What the result gives

Theorem 3 splits the regret into a fixed cost $\tilde O(K\sqrt d)$, independent of $T$, and a variable cost $\tilde O(d\sqrt{KT})$. The same paper shows that the standard upper confidence bound algorithm has fixed cost $\tilde O(Kd^{3/2})$ and at least $\Omega(K\min(d,T))$. ConsUCB therefore improves the fixed cost by a factor of $d$, which is what matters when $T$ is small, since the total reward over the season is of order $KT$. Since an $\Omega(K)$ regret in the first period cannot be avoided, the fixed cost is optimal up to a factor $\tilde O(\sqrt d)$.

The result is proved in the paper; no machine-checked proof is known. The formalization adds a checked account of the within-period selection argument and a statement that makes the constants, the tie-breaking and the failure event explicit. It also records one defect: Lemma 2 as printed fails at $K=T=1$, a gap in the proof of Theorem 3 that closes with one line, since there $R(T)\le KT\le K+\alpha K$.

Where the difficulty lies

Within a period, $K$ selections must be made before any outcome of that period is seen. The obvious argument treats the period as one optimistic choice of $K$ products, all scored with $A_{t-1}$. It then has to compare the width of a selected product under $A_{t-1}$ with its width after the earlier selections of the same period, and that comparison is what produces the fixed cost $\tilde O(Kd^{3/2})$, which the paper's lower bound $\Omega(K\min(d,T))$ shows is not an artefact of a loose analysis in $d$ alone. Any improvement must change the algorithm, and the new score no longer equals the upper confidence bound: for $k\ge2$ it can fall below it, so the usual optimism step does not apply.

The probabilistic step has its own care: the confidence event must hold for a run in which the design vectors of a period are chosen sequentially, at horizon $T+1$, including $d=1$.

Formalization scope

All declarations are in the namespace ShrinkingUCB, over Mathlib; the conventions below are binding.

• Vectors are Fin d → ℝ, norms are written $\sqrt{v\cdot v}$, and Matrix.inv is the inverse (every $A_{t,k}$ dominates $I$, so it is genuine). Logarithms are natural.
• Periods and selections are $1$-based. ConsUCB is a recursion on an outcome table, so every object is a deterministic function of the table, evaluated at the table realized at $\omega$.
• Outcomes form a table of independent Bool variables, with the algorithm reading only the offered entries. A tie-break is a deterministic function of the observed history, the selections so far in the period and the tied set. It cannot read an unobserved outcome; a rule that could would make the goal false, and restricting to one fixed rule would weaken it.
• Failure probabilities are stated as $P(\text{bad})\le\delta$ with the outer measure.
• The bound is kept at $K=T=1$, and no regime such as $K\gg T$ is assumed. A statement with a hard-coded tie-break, a matching of $A_{t-1}$ and $A_{t,k-1}$ in the score, or an added $KT\ge2$ is not this theorem.

A complete development needs a self-normalized bound along the observation sequence ordered within periods, a bound on the sum of unsquared widths, and the bookkeeping that the $K$ selections are distinct. Published tools such as ImprovedLinBandits.OFUL.confidence_ellipsoid and BanditAlgorithm.elliptical_potential_lemma are relevant but are not stated in this form. Contributions of the linear algebra of rank-one updates are reusable beyond this mission and welcome.

Selected references

• R. Jin, D. Simchi-Levi, L. Wang, X. Wang, S. Yang, Shrinking the Upper Confidence Bound: A Dynamic Product Selection Problem for Urban Warehouses, arXiv:1903.07844v2, 2019. https://arxiv.org/abs/1903.07844
• Y. Abbasi-Yadkori, D. Pál, C. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NIPS, 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
• W. Chu, L. Li, L. Reyzin, R. Schapire, Contextual Bandits with Linear Payoff Functions, AISTATS, 2011. https://proceedings.mlr.press/v15/chu11a.html
• L. Qin, S. Chen, X. Zhu, Contextual Combinatorial Bandit and its Application on Diversified Online Recommendation, SIAM SDM, 2014. https://doi.org/10.1137/1.9781611973440.53
• Z. Wen, B. Kveton, A. Ashkan, Efficient Learning in Large-Scale Combinatorial Semi-Bandits, ICML, 2015. https://proceedings.mlr.press/v37/wen15.html

Why pricing along one vector

Charging every customer segment its own optimal prices is the most a seller can extract with a posted price per segment, and solving each segment's problem is often easy. Finding one optimal non-personalized price vector is harder, because aggregate demand may be much more complex than the segments' demands, so single-factor heuristics are used instead. A natural question is how much is lost.

For one product, Bergemann, Castro and Weintraub bound the ratio of personalized to uniform profit by two when each type's profit is concave and demand is positive on a common compact set; Malueg and Snyder bound it by the number of types under milder conditions; and Elmachtoub, Gupta and Hamilton give bounds in terms of summary statistics of the demand distribution. For several products, Berbeglia and Joret analyse uniform pricing in the special case of envy-free pricing. Gallego and Berbeglia state the first tight bound of this kind for general multi-product demand, against the personalized optimum rather than the non-personalized one.

The pricing model

A firm sells a finite nonempty set $N$ of products to customer types $t\in T$, distributed according to a probability measure $\mu$. In the paper $T$ is finite with weights $\theta_j>0$; its remark on p.5 extends the result to continuous types. Write $d_{t,i}(p)\ge0$ for the demand of type $t$ for product $i$ at the price vector $p\ge0$. The type profit is $R_t(p)=\sum_{i\in N}p_id_{t,i}(p)$ and the aggregate profit is $R(p)=\int R_t(p)\,d\mu(t)$.

Let $\bar p_t$ be an optimal price vector of type $t$ (Assumption A0: optimal prices exist and are positive and finite). The personalized profit is $\bar{\mathcal R}=\int R_t(\bar p_t)\,d\mu(t)$. Pricing along a positive vector $f$ earns $\mathcal R^f=\sup_{q>0}R(qf)$; $f=e$ is uniform pricing. For $q\ge0$, the filtered demand $G(q)$ is the $f$-weighted demand at the personalized optima, keeping the pairs $(i,t)$ with $q\le\bar p_{t,i}/f_i$, and $H(q)=\int\sum_{i\in N}f_id_{t,i}(qf)\,d\mu(t)$. Assumption A1 is $G(q)\le H(q)$ for all $q\ge0$. Finally, $q_{\min}$ and $q_{\max}$ are the infimum and supremum of the ratios $\bar p_{t,i}/f_i$.

Formalization targets

The bound

$$\bar{\mathcal R}\le\Bigl(1+\ln\frac{q_{\max}}{q_{\min}}\Bigr)\mathcal R^f$$

for every finite nonempty product set, every probability space of types, every positive $f$ and every selection $\bar p$ of optimal prices, under A0 and A1, with $q_{\min}>0$ and integrable demands.

Exact tightness

For every $\rho>1$ there is an instance with one product, $f=1$, $q_{\min}=1$, $q_{\max}=\rho$, $\mathcal R^f>0$ and

$$\bar{\mathcal R}=(1+\ln\rho)\,\mathcal R^f .$$

Best constant over finite instances

For every $\rho>1$ and $c<1+\ln\rho$ there is an instance with one product, $f=1$, finitely many types, $q_{\min}=1$, $q_{\max}=\rho$, $\mathcal R^f>0$ and $\bar{\mathcal R}>c\,\mathcal R^f$.

All three are clauses of the goal theorem, SingleFactorPricing.LogBound.theorem_1. The milestones are the displayed steps of the paper's proof (the integral forms of the profits, the split at $q_{\min}$, the identity $R(qf)=qH(q)$, the pointwise bound on $qG(q)$) and its tight instance.

What the result gives

Since $\mathcal R^f\le\mathcal R^*\le\bar{\mathcal R}$, where $\mathcal R^*$ is the optimal non-personalized profit, one inequality yields a guarantee for single-factor heuristics against non-personalized pricing and a bound on the value of personalization. The constant depends only on the spread of the optimal prices measured against $f$, not on the number of products or types. For example, $\bar p_{ij}\in[h,7.38h]$ gives $\bar{\mathcal R}\le3\mathcal R^e$. The paper also gives sufficient conditions for A1 that hold in linear, multinomial logit and envy-free models, and uses the bound to compare linear with non-linear pricing.

The result is proved in the paper. This mission adds a machine-checked version: the bound over a general type space, where the paper only remarks that the proof carries over; both meanings of tightness, of which the paper states neither separately; and an explicit probability law for the instance. No formalization of this bound for general demand is known. The platform has narrower statements of the same shape: RevenueOrdered.UDPmin.uniform_pricing_log_ratio_bound for envy-free pricing and ValuePersPricing.Deviation.theorem_2 for one product.

Where the difficulty lies

The obvious comparison fails. Personalized optimal prices need not lie on a single ray $\{qf\}$, so no single $q$ can be compared with them, and A1 compares two sums at the same $q$ rather than two profits. The bound therefore has no term-by-term proof, and the factor $\beta$ is not visible from any one type.

Three points need care in Lean. Over a general type space, $\bar{\mathcal R}$ involves an exchange of integrals for functions that are only assumed integrable in the type. The second line of the printed chain contains $\int R(qf)\,dq/q$, and nothing makes $q\mapsto R(qf)$ measurable. And "tight" cannot mean equality with finitely many types: when $q_{\min}<q_{\max}$ and $\mathcal R^f>0$, $G$ is a step function and equality is impossible, so the exact statement and the finite statement are independent, and the instance for each needs its own computation.

Formalization scope

The type space is T with a probability measure μ, and demand is d : T → (N → ℝ) → N → ℝ with N a nonempty Fintype. Non-negativity and optimality are required for $p\ge0$ only. KallMayerSLP.ICC.discreteLaw θ id, a published finite law, recovers the paper's finite model, and regularity is then automatic. $q_{\min}$, $q_{\max}$ and $\mathcal R^f$ are fixed by IsGLB, IsLUB and IsLUB, so a real ⨆ is not used; $\mathcal R^f$ need not be attained. The filter uses the paper's non-strict inequality. The optimality of $\bar p$ stays in AssumptionA0 although the bound does not use it, so that $\bar{\mathcal R}$ is the personalized optimum and not the profit of arbitrary prices. There is no cost vector (footnote 1 of the paper).

Trivial tightness is excluded: the clauses assert $\mathcal R^f>0$, and LogBoundInstance fixes $q_{\min}=1$ and $q_{\max}=\rho$ as the true infimum and supremum of the ratios, not bounds on them.

A complete development needs integrals over the product of the type space and $(0,\infty)$, the logarithmic integral, the moments and tail of the truncated law tailLaw, and an explicit family of finite instances for the last clause. The definitions are general enough to reuse for the other results of the paper. Proofs of the milestones and of the goal are welcome, as are the omitted results (Corollary 1, Proposition 1, Theorem 2), which would be separate statements.

Selected references

• G. Gallego, G. Berbeglia, Bounds and Heuristics for Multi-Product Personalized Pricing, arXiv preprint, 2021. https://arxiv.org/abs/2102.03038
• G. Berbeglia, G. Joret, Assortment optimisation under a general discrete choice model: A tight analysis of revenue-ordered assortments, Algorithmica 82(4), 2020. https://arxiv.org/abs/1606.01371
• D. Bergemann, F. Castro, G. Y. Weintraub, Uniform pricing versus third-degree price discrimination, Cowles Foundation Discussion Paper, 2020. https://cowles.yale.edu/sites/default/files/2022-08/d2213-r.pdf
• A. N. Elmachtoub, V. Gupta, M. Hamilton, The value of personalized pricing, Management Science, 2021. https://doi.org/10.1287/mnsc.2020.3821
• D. A. Malueg, C. M. Snyder, Bounding the relative profitability of price discrimination, International Journal of Industrial Organization 24(5), 2006. https://doi.org/10.1016/j.ijindorg.2005.11.006

Motivation

Retailers sell seasonal and perishable goods under markdown pricing: the posted price may fall over the selling season but never rise. Fashion, consumer electronics and grocery chains use markdowns because customers and regulators react badly to price increases and because markdown schedules are easy to communicate. The revenue management literature measures a pricing policy by its revenue loss against the fluid (deterministic) benchmark as inventory and horizon grow together.

Timeline:

• Gallego and van Ryzin (1994) showed that the best fixed price, computed from the fluid problem, loses $O(k^{1/2})$ when inventory and horizon are scaled by $k$, and that this order cannot be improved for fixed prices (doi:10.1287/mnsc.40.8.999).
• Maglaras and Meissner (2006) and Jasin (2014) obtained much smaller losses with re-optimization and real-time adjustment policies; Jasin's linear rate correction loses $O(\ln k)$ (doi:10.1287/opre.2014.1317). These policies move prices up and down and are not markdown policies.
• Chen and Jasin (Operations Research 2023; author's version SSRN 3740871) gave a markdown readjustment policy with $N$ monotone price updates and proved a loss of $O(k^{1/(N+2)}(\ln k)^{2\alpha}N)$ for every $\alpha>1/2$ (SSRN 3740871).

Setting

A seller holds $x_0\ge1$ units and sells over $[0,T]$. Customers arrive as a Poisson process with rate $\lambda$; each buys one unit iff her valuation, which lies in $[0,V]$, is at least the posted price. At price $v$ a customer buys with probability $\bar F(v)$, the purchase rate. Since $\bar F$ is a decreasing bijection of $[0,V]$ onto $[0,1]$, a purchase rate $\rho$ determines the price $\bar F^{-1}(\rho)$, and the revenue rate is $R(\rho)=\rho\bar F^{-1}(\rho)$. The model assumes (A2) that $R$ is strictly concave with a maximizer $\rho^*\in(0,1)$ and (A3) that $|R|,|R'|,|R''|\le C$.

The fluid rate is $\rho^d=\min\{x_0/(\lambda T),\rho^*\}$ and the fluid value is $\bar J(x_0,T)=\lambda TR(\rho^d)$.

The policy updates the price at times $t_n=T[1-(x_0+1)^{-n/(N+2)}]$, $n=1,\dots,N$, with $t_0=0$, $t_{N+1}=T$ (equation (14)). On $[t_n,t_{n+1})$ it posts $\bar F^{-1}(\rho_n)$ until stock-out, where $\rho_0=(\rho^d-\eta_0)^+$ and

$$\rho_n=\max\Big\{\Big(\rho^d-\eta_n-\sum_{m=0}^{n-1}\frac{\Delta_m}{\lambda(T-t_{m+1})}\Big)^+,\ \rho_{n-1}\Big\},$$

with $(\cdot)^+$ the projection onto $[0,1]$, $\Delta_m=S_m-\lambda(t_{m+1}-t_m)\rho_m$ the deviation of the realized sales $S_m$ from their mean, and shift terms $\eta_n$ given by equation (15) with a parameter $\alpha>1/2$. The maximum makes $\rho_n$ non-decreasing, so prices only fall. $J^{\pi^{\mathrm{Re}}_\searrow}(x_0,T)$ is the expected revenue of this policy. In the asymptotic setting the $k$-th problem has inventory $kx_0$ and horizon $kT$.

Formalization targets

Goal: Theorem 4

For $k$ large and every $N\ge1$ with $N\le\max\{0,\lfloor \ln(x_0^{(k)}+1)/(4\alpha\ln\ln(x_0^{(k)}+1))-2\rfloor\}$,

$$J^{\pi^{\mathrm{Re}}_\searrow}\big(x_0^{(k)},T^{(k)}\big)\ \ge\ \bar J\big(x_0^{(k)},T^{(k)}\big)-O\big(k^{\frac1{N+2}}(\ln k)^{2\alpha}N\big),$$

with the constant depending only on the model, $T$, $x_0$ and $\alpha$, and uniform in $N$.

Milestones

The milestones follow Appendix B of the paper: Lemma 7 (the schedules satisfy $\eta_0>\dots>\eta_N$ and $\sum_n(t_{n+1}-t_n)\eta_n=0$); the coupling bound (EC.2) with an uncapped process $(\hat\rho_n,\hat S_n)$ that ignores inventory; the second-order Taylor bound after (EC.2) with error terms $A_1,A_2$; the closed form (EC.3) of $\hat\rho_n$ on a good event $\mathcal G$; Lemma EC.1 (bounds on $A_1,A_2$); Lemma EC.2 (inventory balancing, corrected); Lemma EC.3 (expected overselling); Lemma EC.5 (a Poisson tail bound with random rate); Lemma EC.4 ($\mathbb P(\mathcal G^c)\le3N\exp(-0.05(\ln(x_0^{(k)}+1))^{2\alpha})$).

Significance

Theorem 4 shows that the monotonicity constraint costs little: with $N=1$ the loss is $O(k^{1/3}(\ln k)^{2\alpha})$, already below the $O(k^{1/2})$ of any fixed price, and letting $N$ grow like $\ln k/\ln\ln k$ brings it to a polylogarithmic order. The policy is explicit (two closed-form schedules and a one-line update), so the bound is a guarantee for an implementable markdown rule; the same construction is used in the paper for pricing with strategic customers.

The result is proved on paper. To our knowledge none of it is formalized; the platform has Gallego–van Ryzin's fluid bound and fixed-price results, which this mission does not need (it compares against the explicit value $\bar J$). The mission adds a machine-checked version of the full Appendix B argument and corrects Lemma EC.2, whose printed identity holds only when $x_0\le\lambda T\rho^*$.

Difficulty

The policy is a nonlinear feedback rule: the projection and the running maximum make $\rho_n$ a non-smooth function of all past sales, and the sales are themselves capped by the inventory. A direct Taylor expansion of the revenue around $\rho^d$ fails because $\rho_n$ is not a linear function of the sales deviations. The argument controls this by passing to the uncapped process (paying for overselling separately), proving that on the good event the projection and the maximum are inactive, and showing that the good event fails with superpolynomially small probability. The last step needs a concentration bound for Poisson counts whose rate is itself random, uniformly over a number of updates $N$ that grows with $k$; this uniformity is where the condition on $N$ enters.

Formalization scope

The model is a structure Model with the survival function $\bar F$ as primitive (continuous, strictly decreasing on $[0,V]$, $\bar F(0)=1$, $\bar F(V)=0$), $\bar F^{-1}$ as the inverse on $[0,V]$, and A2 for $R$ on $[0,1]$ and A3's derivative bounds on the open interval $(0,1)$ (nothing is asked at the endpoints); continuity of $R''$ is not assumed. The continuous-time process is not built: the demand counts of the intervals $[t_n,t_{n+1})$ have, given the past, Poisson laws with mean $\lambda(t_{n+1}-t_n)\rho_n$ (thinning and independent increments), and seqPoissonLaw is that exact joint law on $\mathbb N^{N+1}$. The actual policy sells $\min(D_n,X_n)$ in interval $n$; the uncapped process sells $D_n$. The constant of the goal is chosen before $k$ and $N$, and the condition on $N$ is evaluated at $x_0^{(k)}=kx_0$; a fixed admissible $N$ is a special case. Upper bounds on unbounded nonnegative quantities use the lower Lebesgue integral, so a non-integrable variable cannot make them vacuous. The lemmas of Appendix B are stated for every instance satisfying the setting ($\rho^d>\eta_0$, $\lambda T>1$, the condition on $N$), which includes the $k$-th problems for large $k$.

Reusable parts: the sequential Poisson law with history-dependent rates and the mixed-Poisson tail bound (Lemma EC.5) apply to any policy that sets a constant price on each of finitely many intervals. Welcome contributions: proofs of the milestones, in particular Lemma EC.5 and the coupling bound (EC.2), and a general lemma identifying expectations under seqPoissonLaw with iterated Poisson expectations.

Selected references

• Y. Chen, S. Jasin, Simple Monotonic Readjustment Policies with Applications to Markdown Pricing and Pricing in the Presence of Strategic Customers, Operations Research, 2023; author's version with e-companion, SSRN 3740871 (2023-10-09). https://ssrn.com/abstract=3740871, https://doi.org/10.1287/opre.2020.0774
• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8), 1994. https://doi.org/10.1287/mnsc.40.8.999
• S. Jasin, Reoptimization and Self-Adjusting Price Control for Network Revenue Management, Operations Research 62(5), 2014. https://doi.org/10.1287/opre.2014.1317

Motivation

Two literatures study how to split a resource among agents who report private information. Fair division of divisible goods asks for allocations that are proportional, efficient and resistant to misreporting (Steinhaus 1948; Cole, Gkatzelis and Goel 2013). Wagering mechanisms let bettors with subjective beliefs about a future event bet against each other, and ask for individual rationality, incentive compatibility and budget balance (Lambert et al. 2008; journal version, 2015). Freeman, Pennock and Vaughan observe that, once a wagering mechanism is read as a sale of Arrow–Debreu securities (Freeman, Lahaie and Pennock 2017), the two problems are the same problem: a bet is a share of the securities, and the securities are divisible goods.

The paper (AAAI'19; extended preprint, 2018, which is the basis here; journal version in Management Science, 2024) makes this precise as a correspondence between the two classes of mechanisms, and uses it to move mechanisms and impossibility results from one side to the other. This mission formalizes the correspondence itself (§3).

Setting

There are $n$ agents and $m$ goods (fair division) or $m$ outcomes of a random variable $X$ (wagering). Each agent reports a point $\hat{\mathbf v}_i$ (or $\hat{\mathbf p}_i$) of the probability simplex $\Delta_m=\{x\in\mathbb R^m: x_j\ge0,\ \sum_j x_j=1\}$: normalized additive values of the goods, or subjective probabilities of the outcomes. Each agent also has a weight $e_i>0$ (entitlement) or wager $w_i>0$, with $E=\sum_i e_i$ and $W=\sum_i w_i$. The value of a bundle $\mathbf z$ for values $\mathbf x$ is $\mathbf x(\mathbf z)=\sum_j x_jz_j$.

An allocation mechanism $\mathcal A$ maps $(\hat{\mathbf v},\mathbf e)$ to a feasible allocation: $\mathcal A_{i,j}\ge0$ and $\sum_i\mathcal A_{i,j}\le1$ for every good $j$. A wagering mechanism $\mathcal B$, in security form, maps $(\hat{\mathbf p},\mathbf w)$ to numbers $\mathcal B_{i,j}\ge0$ of type-$j$ securities, each paying $1$ if $X=j$. $\mathcal A$ and $\mathcal B$ are corresponding mechanisms (Definition 10) if

$$\mathcal B_{i,j}(\hat{\mathbf p},\mathbf w)=W\,\mathcal A_{i,j}(\hat{\mathbf p},\mathbf w)\quad\text{for all inputs, } i,\ j.$$

The properties compared are: proportionality ($\hat v_i(\mathcal A_i)\ge e_i/E$), Pareto optimality over feasible allocations, and weak / strict incentive compatibility (truthful reporting maximizes true value) on the allocation side; individual rationality (some report guarantees expected payoff at least $w_i$), weak / strict budget balance ($\sum_i\mathcal B_{i,j}\le W$, resp. $=W$), weak / strict incentive compatibility, and side-bet Pareto optimality (no zero-sum re-trade of securities, keeping holdings nonnegative, weakly helps every agent and strictly helps one) on the wagering side.

Formalization targets

Goal: the correspondence

For all $n,m$, the conjunction of four clauses:

1. $\mathcal A\mapsto W\mathcal A$ maps allocation mechanisms into valid weakly budget-balanced wagering mechanisms, $\mathcal B\mapsto\mathcal B/E$ maps those back into allocation mechanisms, the maps are mutually inverse, and $\mathcal B=W\mathcal A\iff\mathcal A=\mathcal B/E$.
2. (Theorem 1) For corresponding $\mathcal A,\mathcal B$: $\mathcal A$ weakly (strictly) IC $\iff$ $\mathcal B$ weakly (strictly) IC.
3. (Theorem 2) For corresponding $\mathcal A,\mathcal B$ with $\mathcal A$ weakly IC: $\mathcal A$ proportional $\iff$ $\mathcal B$ individually rational.
4. (Theorem 3, corrected) For a valid $\mathcal A$ and corresponding $\mathcal B$:

$$\mathcal A\text{ Pareto optimal}\iff\mathcal B\text{ side-bet Pareto optimal and }\sum_i\mathcal B_{i,j}(\hat{\mathbf p},\mathbf w)=W\text{ whenever }\hat p_{k,j}>0\text{ for some }k.$$

Milestones

The two validity claims of p.4; the two halves of the proof of Theorem 1 (A.1) and Theorem 1; the two halves of the proof of Theorem 2 (A.2, the direction "proportional ⇒ individually rational" without IC) and Theorem 2; the three steps of the proof of Theorem 3 (A.3) and the corrected Theorem 3.

Significance

The correspondence lets every wagering mechanism be used as an allocation rule for divisible goods with no money, and every allocation rule be run as a bet. The paper's Table 1 and §4 use it to read off, for example, that weighted score wagering mechanisms give proportional, strictly incentive-compatible, envy-free allocations, and that no-arbitrage wagering mechanisms are not envy-free. Impossibility results transfer the same way (§6): Schummer's theorem that the only incentive-compatible, Pareto-optimal allocation mechanisms are dictatorial carries over to wagering, and the welfare bound of Han et al. (2011) for incentive-compatible allocation carries over too.

The results are proved in the paper; none is formalized. The formalization adds two things. First, a reusable model layer for mechanisms on profiles of simplex points, which fixes the quantifier structure of IC, IR, proportionality and both Pareto notions, where informal statements are loose (which report the IR guarantee may depend on; over which alternatives Pareto optimality ranges). Second, a check of the printed statements. The "only if" direction of Theorem 3 is false as printed: a Pareto-optimal allocation mechanism may leave a good unallocated when every agent reports zero value for it, so its corresponding wagering mechanism need not be strictly budget balanced. The goal states the minimal corrected equivalence.

Difficulty

Each proof is a short calculation, and the obstacle is getting the definitions to line up. Two steps need care. In Theorem 2 proportionality is about reported values and individual rationality about true beliefs, so the transfer needs weak incentive compatibility to replace the IR report by the truthful one. In Theorem 3 the "if" direction is printed as "a Pareto-improving allocation consists of agents swapping goods", which is only true when the improving allocation wastes nothing; an improving allocation may itself waste goods, and must first be completed before its difference from $\mathcal A$ becomes a side bet. The "only if" direction relies on "some agent who values it positively", who need not exist, and that is where the printed statement fails.

Formalization scope

Agents are Fin n, goods / outcomes Fin m, both 0-based. Reports, true values and beliefs are points of Mathlib's stdSimplex ℝ (Fin m); weights and wagers are strictly positive vectors (PosVec n), whose sum is both $E$ and $W$. Allocation and wagering mechanisms share one type, total functions of (profile, positive vector); validity is a predicate (IsAllocMech, IsWagerMech). Unilateral deviations are Function.update. Pareto alternatives are feasible allocations. Strict IC is weak IC plus strictness on every misreport. The side-bet nonnegativity condition is entrywise. Corresponding A B is the form $\mathcal B=W\mathcal A$. Theorems 1 and 2 and the inverse identities are stated for arbitrary elements of Mech, without the validity predicates, which their arguments do not use.

Positivity of weights is essential: with $E=0$ the inverse map $\mathcal B/E$ is meaningless, and unnormalized reports would change what proportionality means. No hypothesis is needed for $n=0$ or $m=0$.

Everything is finite sums over Fin; no measure theory or analysis is needed. The model definitions are reusable for later formalizations of §4 (weighted score wagering mechanisms, envy-freeness). Proofs of the milestones, and of the goal from the milestones, are welcome.

Selected references

• R. Freeman, D. M. Pennock, J. W. Vaughan, An Equivalence Between Wagering and Fair-Division Mechanisms, extended preprint of the AAAI'19 paper, 2018 (the citation basis of this mission). https://www.jennwv.com/papers/wagering-fair-division-full.pdf ; AAAI'19 version: https://doi.org/10.1609/aaai.v33i01.33011957
• R. Freeman, J. Witkowski, J. W. Vaughan, D. M. Pennock, An Equivalence Between Fair Division and Wagering Mechanisms, Management Science 70(10):6704–6723, 2024. https://doi.org/10.1287/mnsc.2022.02615
• N. S. Lambert, J. Langford, J. Wortman, Y. Chen, D. Reeves, Y. Shoham, D. M. Pennock, Self-Financed Wagering Mechanisms for Forecasting, ACM EC, 2008; journal version An Axiomatic Characterization of Wagering Mechanisms, Journal of Economic Theory, 2015. https://doi.org/10.1016/j.jet.2014.03.012
• R. Cole, V. Gkatzelis, G. Goel, Mechanism Design for Fair Division: Allocating Divisible Items without Payments, ACM EC, 2013. https://arxiv.org/abs/1212.1522
• H. Steinhaus, The Problem of Fair Division, Econometrica 16:101–104, 1948.
• R. Freeman, S. Lahaie, D. M. Pennock, Crowdsourced Outcome Determination in Prediction Markets, AAAI, 2017.

Selling a service without seeing the bids

A seller offers a service to a set of buyers, each with a private value, and a feasibility constraint limits which sets of buyers can be served together. This is the basic single-parameter problem of mechanism design. Milgrom and Segal proposed clock auctions for it, and designed one for reallocating radio frequency licenses (Milgrom and Segal 2020). In a clock auction each bidder faces a personal price that only rises, and may leave at any time. The format is transparent, a buyer needs to answer only price offers, and the winners never reveal their values.

The cost of the format is the question. Dütting, Gkatzelis and Roughgarden showed that a deterministic clock auction with no information about the values attains no bounded approximation to the optimal welfare, even with two maximal feasible sets (Dütting et al. 2014). Feldman, Gkatzelis, Gravin and Schoepflin (arXiv:2202.09291v1) show that information about the values removes this obstacle, for every downward-closed constraint. This mission formalizes the version with full knowledge of the distributions.

Setting

Let $N$ be a finite set of buyers, with values $v=(v_i)_{i\in N}$, $v_i\ge 0$. A feasibility constraint $\mathcal F\subseteq 2^N$ is downward-closed if every subset of a member is a member. Its maximal feasible sets form the collection $\mathcal S=(S_1,\dots,S_k)$, and $k$ is the parameter of the result.

In the Bayesian setting each $v_i$ is drawn independently from a distribution $D_i$, and the seller knows $D=\times_i D_i$. The benchmark is the expected optimal welfare

$$\mathrm{OPT}=\mathbb E_{v\sim D}\Big[\max_{F\in\mathcal F}\sum_{i\in F}v_i\Big].$$

A single-price clock auction (Mechanism 1) computes a vector of prices $p$ from public information, which here includes $D$, and offers $p_i$ once to each buyer. A buyer stays exactly when $p_i\le v_i$. Among those who stayed the auction selects a feasible subset $F$, serves $F$, and charges each member $p_i$. It is deterministic when the prices and the selection rule involve no randomness. The selected set depends on the values only through the set of buyers who stayed.

Formalization targets

Goal: Theorem 1

There is an absolute constant $C>0$ such that every downward-closed constraint with $k$ maximal sets and every product distribution admit a deterministic single-price clock auction with

$$\mathrm{OPT}\le C\cdot\max\{1,\log\log k\}\cdot\mathbb E_{v\sim D}[\mathrm{auc}(v)].$$

The constant is not fixed in the statement, so the goal survives any improvement.

Milestones

For $S\in\mathcal S$ let $S(t,v)=\{i\in S\mid v_i>t\}$, and let $t_S$ be the least $t$ with $\mathbb E_v|S(t,v)|\le\log k$.

1. Lemma 2. Uniform concentration of $|S(x,v)|$ on $[0,t)$, at the explicit rate $2/k^8$.
2. Equation (1). $\mathrm{OPT}\le\mathrm{LOW}+\mathrm{HIGH}$, with $\mathrm{OPT}$ as a maximum over $\mathcal S$.
3. Equation (2). $\mathrm{HIGH}\le\mathrm{HIGH\text-CORE}+\mathrm{HIGH\text-TAIL}$.
4. Equation (3). $\mathrm{LOW}\le\mathrm{LOW\text-CORE}+\mathrm{LOW\text-TAIL}$.
5. Section 3.2, p.10. The bound on $\mathrm{LOW\text-CORE}$.
6. Claims 13 and 14. The zero-price auction covers $\mathrm{HIGH\text-TAIL}$ and $12$-approximates $\mathrm{LOW}$.
7. Lemma 3. Some uniform price $p$ satisfies $\Delta\le C(1+\log m)\cdot W(p)$.
8. Section 3.2, p.11. $W(p)$ is the expected welfare of a uniform-price auction.

Significance

The theorem shows that the impossibility for deterministic clock auctions is a statement about missing information, not about the clock format, and that a very restricted member of the class already beats a logarithmic barrier. Sequential posted-price mechanisms, which must serve every buyer who accepts, cannot do better than $O(\log k/\log\log k)$ even when the maximal sets are disjoint (Rubinstein 2016). The single-price auction differs from them only by deferring the choice of whom to serve until all buyers have answered, and that gains an exponential factor. The same benchmark decomposition is reused in the paper's limited-information and prior-free results.

The result is proved in the paper, and no machine-checked proof of it is known. Formalizing it adds a definition of Bayesian single-price clock auctions and a machine-checked core-tail decomposition of an expected maximum over feasible sets. Formalized clock auctions so far concern budget-feasible procurement with descending prices, which is a different model. Two printed steps of the proofs do not hold as written, while the lemmas do: the display on p.20 in the proof of Lemma 3, and the exact doubling in the proof of Lemma 2, which needs repair for distributions with atoms. A complete formalization must supply these arguments.

Difficulty

The maximum over $k$ sets defeats the two obvious estimates. Replacing the maximum by a sum loses a factor $k$. Bounding it by the largest expected set value fails, because with heavy-tailed values the realized maximum can far exceed every set's mean. The natural single-threshold approach of posted pricing fails too, since it must commit to each acceptance as it happens.

Independence is needed twice, and in the second use a bidder's own value is correlated with the event that the bidder's set has many high values, so the expectation does not factor as written. A further obstacle is that the distributions are arbitrary: atoms mean that the expected count above a threshold can jump, so an exact solution of $\mathbb E_v|S(t,v)|=\log k$ need not exist.

Formalization scope

Lean conventions:

• The bidders are a Fintype N, and 𝓕 : Finset (Finset N) with ∅ ∈ 𝓕, which excludes only the empty family.
• Values lie in ℝ≥0. The laws ν i are arbitrary probability measures: atoms, unbounded supports and infinite means are all allowed.
• All expectations are ℝ≥0∞-valued lower integrals, so no integrability hypothesis appears and the benchmark cannot collapse to a junk 0.
• The paper's log is base 2 (it writes $\ln 2$ for the natural logarithm), and the thresholds $t_S$ and the cutoff $10\log k$ use Real.logb 2. In the goal and in Lemma 3 the base is absorbed by the existential constant, and Real.log is used there. The factor is $\max\{1,\log\log k\}$, because $\log\log k$ is $0$ at $k=1$ and negative at $k=2$. In Lemma 3 the factor is $1+\log m$, because the literal $\log m$ fails at $m=1$.
• tS is an infimum, footnote 2's reading. Statements using it assume $k\ge2$.

A trivializing formalization is ruled out by the auction structure: price does not see the values and select reads only the set of acceptors, so the auction cannot be VCG, which would have factor $1$.

The development needs the product measure on N → ℝ≥0, a multiplicative Chernoff bound for sums of independent non-identical indicators, and layer-cake integration. Those parts, and the decomposition itself, are reusable beyond this mission. Contributions welcome are the milestones above and the general Chernoff bound. Theorems 4, 6 and 9 of the paper are outside this mission.

Selected references

• M. Feldman, V. Gkatzelis, N. Gravin, D. Schoepflin, Bayesian and Randomized Clock Auctions, arXiv preprint, 2022. https://arxiv.org/abs/2202.09291
• P. Dütting, V. Gkatzelis, T. Roughgarden, The Performance of Deferred-Acceptance Auctions, EC 2014; Mathematics of Operations Research 42(4), 2017. https://doi.org/10.1145/2600057.2602861
• P. Milgrom, I. Segal, Clock Auctions and Radio Spectrum Reallocation, Journal of Political Economy 128(1), 2020. https://doi.org/10.1086/704074
• A. Rubinstein, Beyond Matroids: Secretary Problem and Prophet Inequality with General Constraints, STOC 2016. https://doi.org/10.1145/2897518.2897540

Motivation

In bilateral trade a seller and a buyer each hold a private valuation for one good, and an intermediary (a platform or broker) decides at which price the good changes hands. Myerson and Satterthwaite showed that no mechanism can be at once efficient, incentive compatible, individually rational and budget balanced (Myerson–Satterthwaite 1983). Among mechanisms that are dominant-strategy incentive compatible, individually rational and exactly budget balanced, only posted fixed prices survive. A platform facing a stream of seller/buyer pairs therefore has to learn a good fixed price from experience.

Cesa-Bianchi, Cesari, Colomboni, Fusco and Leonardi (arXiv:2109.12974v1, 2021; later in Mathematics of Operations Research, 2024) study this as a regret-minimization problem and map out the attainable rates under full and realistic feedback and under stochastic and adversarial valuations. This mission formalizes their positive result for realistic feedback, the setting of an actual posted-price mechanism, where the learner only sees whether each side accepted the price.

Setting

Valuations, prices and gains live in $[0,1]$. The gain from trade of price $p$ for a seller with valuation $s$ and a buyer with valuation $b$ is

$$\mathrm{GFT}(p,s,b)=(b-s)\,\mathbb I\{s\le p\le b\}.$$

In each round $t=1,\dots,T$ a fresh pair $(S_t,B_t)$ arrives, the learner posts $P_t\in[0,1]$, and under realistic feedback it observes only the two bits $\mathbb I\{S_t\le P_t\}$ and $\mathbb I\{P_t\le B_t\}$; the gain $\mathrm{GFT}(P_t,S_t,B_t)$ stays hidden. In the stochastic i.i.d. setting with independent valuations the pairs are i.i.d. with law $\mu_S\otimes\mu_B$. The bounded-density assumption asks $\mu_S(A)\le M\,\mathrm{Leb}(A)$ and $\mu_B(A)\le M\,\mathrm{Leb}(A)$ for every Borel set $A$. The learner randomizes through i.i.d. uniform draws $U_1,U_2,\dots$ on $[0,1]$ that are independent of the valuations.

The regret of a pricing strategy is

$$R_T=\sup_{p\in[0,1]}\mathbb E\Big[\sum_{t=1}^T\mathrm{GFT}(p,S_t,B_t)-\sum_{t=1}^T\mathrm{GFT}(P_t,S_t,B_t)\Big].$$

A $K$-armed bandit strategy $\alpha$ chooses, in each round, an arm in $[K]$ as a measurable function of its own uniform draws and of the rewards it has observed. Its regret $R^\nu_\tau(\alpha)$ after $\tau$ rounds is taken against i.i.d. reward vectors with law $\nu$ on $[0,1]^K$, and a distribution-free bound $\mathcal R_\tau(\alpha)$ bounds $R^\nu_\tau(\alpha)$ for every such $\nu$.

Scouting Bandits (SB, Algorithm 3) uses a grid $q_k=k/(K+1)$, $k\in[K]$. For $T_0$ rounds it posts uniform prices $U_t$ and forms $\widehat F_k=\frac1{T_0}\sum_{s\le T_0}\mathbb I\{q_k\le U_s\le B_s\}$ and $\widehat G_k=\frac1{T_0}\sum_{s\le T_0}\mathbb I\{S_s\le U_s\le q_k\}$, both computable from the feedback. It then runs $\alpha$ on the grid, posting $q_{I_t}$ and feeding $\alpha$ the surrogate reward $Z_{H,t}(I_t)=\mathbb I\{S_t\le q_{I_t}\}\widehat F_{I_t}+\mathbb I\{q_{I_t}\le B_t\}\widehat G_{I_t}$.

Formalization targets

Goal: Theorem 3

For every $T\ge T_0$,

$$R_T(\mathrm{SB})\le T_0+\left(\frac{4M}{K+1}+\sqrt{\frac{2\pi}{T_0}}\right)(T-T_0)+\mathcal R_{T-T_0}(\alpha),$$

and, for every $C\ge0$, there is $c$ depending only on $C$ such that if $\mathcal R_\tau(\alpha^{K,\tau})\le C\sqrt{K\tau}$ for all $K\ge1$ and $\tau$, then SB with $\alpha^{K,T-T_0}$, $T_0=\lceil T^{2/3}\rceil$ and $K=\lceil T^{1/3}\rceil$ has

$$R_T(\mathrm{SB})\le c\,M\,T^{2/3}\qquad\text{for every }T\ge1.$$

Milestones

1. Lemma 1, eqs. (1)–(4): the Decomposition lemma, from the pointwise identity to $\mathbb E[\mathrm{GFT}(p,S,B)]=\mathbb P[S\le p]\,\mathbb P[p\le U\le B]+\mathbb P[p\le B]\,\mathbb P[S\le U\le p]$ for independent $S,B,U$ with $U$ uniform.
2. Corollary of Lemma 1: bounded densities make $p\mapsto\mathbb E[\mathrm{GFT}(p,S,B)]$ $4M$-Lipschitz on $[0,1]$.
3. Lemma 2: this function is upper semicontinuous and has a maximizer $p^\star\in[0,1]$.
4. (9): $R_T(\mathrm{SB})\le T_0+\sum_{t>T_0}\mathbb E[\mathrm{GFT}_t(p^\star)-\mathrm{GFT}_t(P_t)]$.
5. Terms (I)–(VI): (I) $\le\frac{4M}{K+1}(T-T_0)$; (II) $=0$; (III) $\le\mathcal R_{T-T_0}(\alpha)$; per round, the bias of the played surrogate reward is at most (V) + (VI); (V), (VI) $\le\sqrt{\pi/2}/\sqrt{T_0}$, so (IV) $\le\sqrt{2\pi/T_0}\,(T-T_0)$.

Significance

Theorem 3 gives an $O(MT^{2/3})$ regret for posted-price bilateral trade under realistic feedback, and Theorem 4 of the paper shows that $T^{2/3}$ cannot be improved in this setting. Theorems 5 and 6 show that dropping independence or bounded densities makes linear regret unavoidable, so the hypotheses of Theorem 3 are where learning becomes possible. The reduction itself is reusable: any minimax-optimal bandit algorithm plugged into SB inherits the rate.

The result is proved in the paper. No machine-checked proof of it, of the Decomposition lemma, or of the bandit reduction exists on the platform. Formalizing it adds a checked version of a regret bound whose proof combines a measure-theoretic identity, a discretization argument, a conditioning argument for a randomized learner, and a uniform deviation bound.

Difficulty

Posting a price $p$ reveals only $\mathbb P[S\le p]$ and $\mathbb P[p\le B]$ in the long run, while the expected gain also depends on integrals over prices away from $p$. A standard bandit algorithm run directly on prices therefore does not see its own reward, and the obvious approach of treating each grid price as an arm fails.

In the formal proof, the steps that need the most care are probabilistic. Term (III) needs that, conditionally on the scouting estimates $H$, the bandit phase is a genuine run of $\alpha$ on i.i.d. reward vectors in $[0,1]^K$. This uses $\widehat F_k+\widehat G_k\le1$ almost surely, the independence of $H$ from the bandit-phase data, and a disintegration of the product measure. Term (IV) conditions on the history before round $t$. Terms (V) and (VI) need the univariate Dvoretzky–Kiefer–Wolfowitz inequality with Massart's constant, which is open on the platform as OfflineCensoredPricing.Identifiability.lemma_A_2 and is not posed again here.

Formalization scope

Rounds $1,\dots,T$ are indices of Fin T. The sample space is $(\text{Fin }T\to\mathbb R\times\mathbb R)\times(\text{Fin }T\to\mathbb R)$ with the law $(\mu_S\otimes\mu_B)^{\otimes T}\otimes\mathrm{Unif}[0,1]^{\otimes T}$, so i.i.d. sampling, independent valuations and independence of the learner's randomization are built into the measure. Valuation laws are probability measures on $\mathbb R$ concentrated on $[0,1]$. The density bound is imposed on each marginal law, which every joint density bounded by $M$ implies. The regret is the real supremum over $p\in[0,1]$, and all its expectations lie in $[-T,T]$. The grid is grid K k = (k+1)/(K+1) for k : Fin K.

A bandit strategy is a sequence of measurable maps from (uniforms, past real rewards) to Fin K. Admissible reward laws are probability measures on $\mathbb R^K$ concentrated on $[0,1]^K$, with correlated arms allowed. SB uses one uniform sequence for both its scouting prices and $\alpha$'s randomization. Its prices depend on the valuations only through the realistic feedback bits. $T_0\ge1$, $K\ge1$, and $T\ge T_0$ are hypotheses.

Measurability of $\alpha$ is part of the strategy, so the expectations are not junk. In (b) the constant $c$ is quantified before the bandit family, the laws, $M$ and $T$. The family is indexed by $K\ge1$, because there is no strategy over zero arms, and by the horizon it is tuned to, because MOSS takes the horizon as an input; one strategy for each $K$ is the case that does not depend on the horizon.

The development needs product measures, conditional independence on finite products, and a DKW bound. The definitions of the bandit game and its regret apply to any i.i.d. bandit problem with correlated arms. Contributions are welcome on any milestone, especially Lemma 1 (Fubini on $[0,1]^2$) and the conditioning steps (III) and (IV).

Selected references

• N. Cesa-Bianchi, T. Cesari, R. Colomboni, F. Fusco, S. Leonardi, Bilateral Trade: A Regret Minimization Perspective, arXiv:2109.12974v1, 2021; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2109.12974v1
• R. B. Myerson, M. A. Satterthwaite, Efficient mechanisms for bilateral trading, Journal of Economic Theory 29(2), 1983. https://doi.org/10.1016/0022-0531(83)90048-0
• J.-Y. Audibert, S. Bubeck, Minimax policies for adversarial and stochastic bandits, COLT 2009. https://hal.science/hal-00834882
• P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Annals of Probability 18(3), 1990. https://doi.org/10.1214/aop/1176990746

Motivation

A two-sided market has sellers who hold goods and buyers who want them, each with a private value. A mechanism that reallocates the goods should be truthful (no agent gains by misreporting her value), individually rational (no agent is worse off for participating) and budget-balanced (the mechanism neither injects nor keeps money). Myerson and Satterthwaite showed that already for one buyer and one seller no mechanism has all three properties and always trades efficiently (Myerson–Satterthwaite 1983). The question is therefore how much of the optimal social welfare such a mechanism can guarantee.

Braun and Kesselheim (arXiv:2105.15032v1, 2021; Mathematics of Operations Research, 2022) answer it for matroid double auctions by transferring the balanced-threshold technique of one-sided prophet inequalities (Kleinberg–Weinberg 2012) to two-sided markets.

Timeline.

• 1983: Myerson and Satterthwaite prove the impossibility for bilateral trade.
• 2016: Colini-Baldeschi, de Keijzer, Leonardi and Turchetta design truthful, strongly budget-balanced matroid double auctions with prices based on quantiles (SODA 2016). Braun and Kesselheim cite their ratio of $\frac1{16}$, and the ratio $\frac1{3+\sqrt3}$ of Dütting et al. (2020), as the best previous guarantees (p.3).
• 2020: Colini-Baldeschi, Goldberg, de Keijzer, Leonardi, Roughgarden and Turchetta introduce direct-trade budget balance (ACM TEAC 2020).
• 2021: Braun and Kesselheim prove the strongly budget-balanced $\frac13$-approximation (Theorem 1, the goal of this mission). They also give a weakly budget-balanced, $\frac12$-competitive online mechanism (Theorem 2), which is not part of this mission.

Setting

There is a finite set $B$ of buyers and a finite set $S$ of sellers, disjoint. Each seller holds one item, all items are identical, and each buyer wants at most one item. A matroid $\mathcal M_B=(B,\mathcal I_B)$ on the buyers restricts which sets of buyers may be served. Agent $a$'s value $v_a\ge0$ for an item is drawn independently from a known law $\mathcal D_a$; $\mathbf v$ is the profile.

An allocation serves a set $B'\in\mathcal I_B$ of buyers and lets a set $K\subseteq S$ of sellers keep their own item, with $|B'|+|K|\le|S|$; its welfare is $\sum_{i\in B'}v_i+\sum_{j\in K}v_j$. The benchmark is $\mathbf E_{\mathbf v}[\max_{X^*}\mathbf v(X^*)]$.

For served buyers $A_B$ and $r$ items left for buyers, $\mathrm{OPT}_B(\mathbf v\mid A_B,r)$ is the best set $B'\subseteq B\setminus A_B$ with $B'\cup A_B\in\mathcal I_B$ and $|B'\cup A_B|\le r$. Buyer $i$'s threshold is

$$p_i(A_B,r)=\mathbf E_{\tilde{\mathbf v}}\big[\tilde{\mathbf v}(\mathrm{OPT}_B(\tilde{\mathbf v}\mid A_B,r))-\tilde{\mathbf v}(\mathrm{OPT}_B(\tilde{\mathbf v}\mid A_B\cup\{i\},r))\big],$$

or $\infty$ if $i$ cannot be feasibly added. Seller $j$'s threshold is $p_j=\mathbf E[\tilde v_j]$. The price of a trade is $p_{i,j}(A_B,r)=\frac13(p_i(A_B,r)+p_j)$.

Mechanism 1 (Algorithm 1, p.9) repeatedly pairs the remaining buyer with the largest threshold and the remaining seller with the smallest one. Infeasible buyers are discarded. Otherwise the seller is asked first: if her value exceeds the price she keeps her item and $r$ drops by one. If not, the buyer is asked, buys if her value exceeds the price, and leaves either way.

Formalization targets

Goal: Theorem 1 (p.10)

Mechanism 1 is DSBB, DSIC and IR for all buyers and sellers, and

$$\mathbf E_{\mathbf v}\big[\mathbf v(A(\mathbf v))\big]\ \ge\ \tfrac13\,\mathbf E_{\mathbf v}\big[\max_{X^*}\mathbf v(X^*)\big].$$

It is stated for every finite market (empty sides allowed), every matroid, every family of independent laws on $[0,\infty)$ with finite means, and every fixed tie-breaking order.

Milestones

• Lemma 3: DSBB, DSIC and IR.
• Lemma 4: the $\frac13$ guarantee.
• Lemma 5: a seller keeping her item costs at most what a sale would cost.
• Inequalities (1), (2) of Lemma 6's proof and Lemmas 6 and 7: prices are monotone.
• Lemma 8: the adapted Kleinberg–Weinberg Proposition 2.
• The base-value bound and inequalities (4) and (5) of Lemma 4's proof.

Lemmas 5–7 and inequality (2) carry the minimal correction "the buyer is not already served"; without it the printed statements fail on one-buyer instances.

Significance

The theorem gives a mechanism that satisfies all of the properties Myerson–Satterthwaite forces a trade-off between, except exact efficiency, and loses at most a factor 3. Every trade is a bilateral exchange at a single price. The prices are posted and depend only on the distributions, so the mechanism is simple to run and to explain. The proof splits the welfare into a base value covered by prices and a surplus above them. This turns one-sided balanced-price arguments into two-sided ones, and the paper reuses the template for knapsack and combinatorial double auctions.

The result is proved on paper. The platform has the one-sided matroid prophet inequality of Kleinberg and Weinberg, but nothing for two-sided markets: no budget-balance notion, no seller incentives, no double-auction mechanism. A complete development adds the first machine-checked two-sided result and checks the corrections to Lemmas 5–7.

Difficulty

Buyer incentives are routine: a buyer is asked at most once, at a price independent of her report. The difficulty sits elsewhere:

• Seller truthfulness depends on the order of offers. Buyers are taken in decreasing threshold while $A_B$ and $r$ stay fixed, so the prices offered to the current seller only decrease. Without that order, DSIC fails.
• The welfare bound cannot compare the mechanism with the optimum allocation by allocation. It needs ghost samples $\mathbf v'$, $\tilde{\mathbf v}$ (independent copies of $\mathbf v$) and the fact that an agent's offer does not depend on her own value, so that her value can be exchanged with a ghost value.
• Matroid facts. The price monotonicity rests on the exchange property of the matroid truncated to rank $r$: the pointwise thresholds grow when $r$ shrinks and are submodular when $A_B$ grows. The surplus bound needs that the thresholds of any independent extension sum to at most the remaining optimum.
• Measurability. The mechanism's run is a measurable function of $\mathbf v$, and every integrand is integrable under finite means.

Formalization scope

Agents are B ⊕ S with Fintype. The matroid is a Mathlib Matroid B with M.E = univ. Values are real, each $\mathcal D_a$ is a probability measure with $\mathcal D_a((-\infty,0))=0$ and an integrable identity, and the profile law is Measure.pi D. Thresholds and prices live in WithTop ℝ ($\infty=\top$). Ties are broken by injective ranks rkB, rkS, quantified over. The comparisons are strict, as printed. Algorithm 1 is a step function iterated $|B|+|S|$ times, with a log of offers. An outcome records served buyers, keeping sellers, buyer payments and seller receipts. IsDSBB asks for a set of trades with distinct buyers and sellers that explains the allocation and makes each buyer's payment equal to the seller's receipt. IsDSIC and IsIR quantify over all report profiles in $[0,\infty)$. Ghost samples are integrals over the product of two copies of Measure.pi D.

The approximation clause compares against the maximum over feasible allocations, not against $\mathbf v(\mathrm{OPT}_B(\mathbf v))+\sum_jv_j$. Because non-integrable integrands integrate to $0$, the integrability hypotheses must stay: without them the clause could hold for the wrong reason.

Useful infrastructure beyond this mission: maximum-weight independent sets in truncated matroids (greedy optimality, exchange), submodularity of $Y\mapsto\mathrm{OPT}_B(\mathbf v\mid Y,r)$, and measurability of finite iterated decision procedures. Proofs of any milestone, and of the monotonicity lemmas as stand-alone matroid facts, are welcome.

Selected references

• A. Braun, T. Kesselheim, Truthful Mechanisms for Two-Sided Markets via Prophet Inequalities, arXiv:2105.15032v1, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/2105.15032v1
• R. Kleinberg, S. M. Weinberg, Matroid Prophet Inequalities, STOC 2012. https://arxiv.org/abs/1201.4764
• R. Colini-Baldeschi, B. de Keijzer, S. Leonardi, S. Turchetta, Approximately Efficient Double Auctions with Strong Budget Balance, SODA 2016. https://doi.org/10.1137/1.9781611974331.ch98
• R. Colini-Baldeschi, P. W. Goldberg, B. de Keijzer, S. Leonardi, T. Roughgarden, S. Turchetta, Approximately Efficient Two-Sided Combinatorial Auctions, ACM Transactions on Economics and Computation, 2020. https://doi.org/10.1145/3381523
• R. B. Myerson, M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory, 1983. https://doi.org/10.1016/0022-0531(83)90048-0
• P. Dütting, M. Feldman, T. Kesselheim, B. Lucier, Prophet Inequalities Made Easy, FOCS 2017. https://arxiv.org/abs/1612.03161

Pricing perishable, capacity-limited resources online

A seller who allocates resources that appear and expire over time (machine slots in a cloud, rooms on given nights, edges of a matching market that change from round to round) often cannot run an auction for every user. A posted price mechanism announces prices before the user arrives and lets the user buy her preferred bundle; it is truthful for myopic users because the prices do not depend on what the user reports. Emek, Lavi, Niazadeh and Shi (arXiv:2005.01869v2, later in Mathematics of Operations Research, 2024) ask how well such a mechanism can learn prices online when valuations are chosen by an adversary and inventory is limited. The difficulty is that the natural benchmark is stateful: a good pricing rule reacts to how much of each resource is left, and inventory couples the rounds. The paper's answer, Theorem 3.10, is a mechanism whose regret against the best inventory-dependent pricing policy in a finite class is sublinear in the number of rounds.

Setting

A DRACC instance (dynamic resource allocation with capacity constraints) has rounds $t=1,\dots,T$ and finitely many resources. Resource $i$ arrives at round $t_a(i)$, departs after round $t_e(i)$ (with $1\le t_a(i)\le t_e(i)\le T$) and carries $c(i)\in\{1,\dots,C\}$ units. The active set $A_t$ consists of the resources with $t_a(i)\le t\le t_e(i)$, and $|A_t|\le W$. User $t$ has a valuation $v_t:2^{A_t}\to[0,1)$ with $v_t(\emptyset)=0$, otherwise arbitrary. Facing prices $p$, she buys one unit of each resource in her demand set

$$\hat A^p_t=\operatorname*{argmax}_{A\subseteq A_t}\Big(v_t(A)-\sum_{i\in A}p(i)\Big),$$

with ties broken by a fixed order, and pays $\hat q^p_t=\sum_{i\in\hat A^p_t}p(i)$. The inventory vector $\lambda_t$ records the remaining units; a price vector is feasible for $\lambda_t$ if every price lies in $(0,1]$ and every exhausted active resource is priced at $1$, which no user buys since valuations are below $1$.

A pricing policy $\gamma$ maps the active set and an inventory vector to a feasible price vector. Played on its own, it generates its own inventory trajectory $\lambda^\gamma_t$ and revenue $\sum_{t}\hat q^{\gamma}_t$. A randomized mechanism posts $p_t$ using only $A_1,\dots,A_t$, the capacities of arrived resources and the valuations $v_1,\dots,v_{t-1}$. Its regret with respect to a finite class $\Gamma$ of policies is

$$\max_{\gamma\in\Gamma}\sum_{t=1}^T\hat q^{\gamma}_t-\mathbb E\Big[\sum_{t=1}^T\hat q^{p_t}_t\Big].$$

Formalization targets

Goal: Theorem 3.10

There is an absolute constant $K$ such that for all $C,W,T$ and every finite nonempty $\Gamma$ some non-anticipating, always feasible randomized mechanism satisfies, on every DRACC instance,

$$\mathrm{Regret}\le K\,T^{\frac12\left(1+\frac{CW}{CW+1}\right)}\sqrt{\log|\Gamma|}.$$

Milestones

The proof passes through an abstract model, the dynamic deterministic MDP (Dd-MDP), in which an adversary picks a transition function $g_t$ and a reward function $f_t$ each round. The milestones, in proof order, are:

1. DRACC instances are Dd-MDPs (§3.1, Eq. (4)): policy simulations and revenues coincide.
2. Facts about the randomized chasing oracle of Theorem 3.4: its prices are feasible, dominate the target's, and never sell a "Bad" resource; in a "Following" round it copies the target or sells nothing; a Following round does not raise the potential $\phi$.
3. Steps (I)–(III) of the proof of Theorem 3.6, and $\mathbb E[\#\mathrm{Missing}]\le CW/\varepsilon^{CW}$.
4. Theorem 3.6: DRACC Dd-MDPs are $O(T^{CW/(CW+1)})$-chasable:

$$\mathrm{CR}\le K_0\,T^{\frac{CW}{CW+1}}.$$

5. Theorem 3.7 (Kalai–Vempala): online learning with switching cost $\Delta\ge1$ has regret $O(\sqrt{\Delta T\log|\Gamma|})$.
6. Theorem 3.8: the algorithm C&S has regret $O(\sqrt{\sigma T\log|\Gamma|})$ on $\sigma$-chasable Dd-MDPs, for $|\Gamma|\ge2$.

Significance

The theorem gives the first vanishing-regret guarantee for posted pricing against a stateful benchmark with arbitrary (not even monotone) valuations, and the paper derives from it learning guarantees for online job scheduling and matching over dynamic bipartite graphs (Corollaries 4.1–4.4). The bound degrades as $CW$ grows, and Theorem 3.11 shows that some dependence on $C$ and $W$ is unavoidable: if $CW=\Omega(T)$, every posted price mechanism has regret $\Omega(T)$. The abstract part, Theorem 3.8, applies to any Dd-MDP satisfying chasability, beyond pricing.

The results are proved in the paper; none of them has a machine-checked proof. Formalizing them requires a precise account of what an online randomized mechanism may know, of policy regret along the policy's own trajectory, and of an online-learning algorithm with switching cost. The Theorem 3.7 statement here corrects the printed one (it needs $\Delta\ge1$), and the Theorem 3.8 statement corrects the printed one by $\sigma\ge1$ and $|\Gamma|\ge2$; the first episode of C&S costs up to $\sigma$, which the paper's switch count misses.

Difficulty

The obvious approach, running an experts algorithm over the policies in $\Gamma$, fails because the reward of a policy depends on the inventory state it has built up; switching to a policy in the middle of the horizon does not recover that policy's reward, since the mechanism's inventory differs from the policy's. Proposition 3.1 of the paper shows that general Dd-MDPs force regret $\Omega(T)$, and Proposition 3.3 that no deterministic chasing strategy has $o(T)$ chasing regret on DRACC. The central difficulty is to follow a target policy whose inventory differs from the mechanism's own, from an arbitrary starting inventory, at a cost sublinear in $; with arbitrary valuations, raising the price of one resource can change which other resources the buyer takes, so the comparison between the two inventory trajectories cannot be done resource by resource.

Formalization scope

Resources are natural numbers and an instance's resources are a finite set; the number of resources is not bounded. Inventory vectors are functions $\mathbb N\to\mathbb N$ that vanish off the active set, price vectors are functions $\mathbb N\to\mathbb R$ with values in $(0,1]$, and a policy takes the active set as an explicit argument. Ties are broken by an arbitrary injective rank on bundles (every lexicographic order is one). The instance is fixed before the coins (an oblivious adversary); the expectation is over the mechanism's coins only, and the benchmark is each policy's revenue along its own trajectory. The constant $K$ is absolute, chosen before $C$, $W$, $T$ and $\Gamma$, and $\log$ is natural.

A mechanism that reads $v_t$ before posting $p_t$, or one chosen after the instance, could play the best policy in hindsight and trivialize the goal; the non-anticipation predicate and the quantifier order $\exists$ mechanism $\forall$ instance rule this out, as the same order $\exists$ oracle $\forall$ instance does in Theorem 3.6.

The development needs a randomized-online-algorithm vocabulary for Dd-MDPs, chasing oracles, online learning with switching cost (the experts setting of Kalai and Vempala), product measures of i.i.d. coins, and the DRACC model. The Dd-MDP, chasing and OLSC definitions are independent of pricing and reusable. Contributions to any milestone, including a formal proof of the Kalai–Vempala switching-cost bound, are welcome.

Selected references

• Y. Emek, R. Lavi, R. Niazadeh, Y. Shi, Stateful Posted Pricing with Vanishing Regret via Dynamic Deterministic Markov Decision Processes, arXiv:2005.01869v2, 2020; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2005.01869
• A. Kalai, S. Vempala, Efficient algorithms for online decision problems, Journal of Computer and System Sciences 71(3), 2005. https://doi.org/10.1016/j.jcss.2004.10.016