All missions

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

Motivation

In many recommendation and promotion settings the reward of showing an item depends on how long it has been since the item was last shown: a promoted product in a live-streaming session, a notification, a piece of content whose appeal recovers while it rests. Bandits with recovering rewards model this. Kleinberg and Immorlica (FOCS 2018) studied recharging bandits with concave recovery, Basu, Sen, Sanghavi and Shakkottai (NeurIPS 2019) blocking bandits, and Pike-Burke and Grünewälder (NeurIPS 2019) recovering bandits with parametric recovery. Simchi-Levi, Zheng and Zhu (arXiv:2106.14813) drop every shape assumption except monotonicity and boundedness, and ask how well a simple class of schedules can do when all recovery functions are known. This mission formalizes their offline guarantee.

Timeline:

• 2018: Kleinberg and Immorlica, recharging bandits with concave non-decreasing recovery; a concave-program upper bound (the special case of Lemmas 1–2 of this paper) and a randomized offline policy.
• 2019: Basu et al., blocking bandits (an arm is unavailable for a known time after a pull), a special case of this model; the greedy policy has a long-run $1-1/e$ guarantee there.
• 2021 (preprint), 2024 (Management Science): Simchi-Levi, Zheng and Zhu, general non-decreasing recovery; purely periodic policies with long-run ratio $\gamma_K$, tight up to logarithmic factors within that class, and an online learning version with $\tilde O(\sqrt T)$ regret.

Setting

There are $N$ arms. Pulling arm $i$ after it has been idle for $d$ periods pays the mean reward $R_i(d)$, where $R_i(0)=0$, $0\le R_i(d)\le R_{\max}$ and $R_i$ is non-decreasing in $d$ (no concavity). Every arm was last pulled at time $0$. In each period $t=1,2,\dots$ at most $K$ arms may be pulled.

For one arm, $F_{i,T}(x)$ is the best average reward over $[1,T]$ when the arm is pulled at most $xT$ times (problem (2)), and $F_i(x)=\limsup_T F_{i,T}(x)$ is its long-run value. The upper bound is

$$\mathrm{UB}_R[K]=\max\Big\{\sum_{i=1}^N F_i(x_i)\ :\ x\in[0,1]^N,\ \sum_i x_i\le K\Big\},$$

and $\mathrm{UB}_R[K]\cdot T$ bounds the offline optimum over horizon $T$. The supporting points $d^{(k)}_i$ are the points where $R_i$ meets its upper concave envelope $R^{cc}_i$.

A purely periodic policy gives each arm a period $d_i\in\mathbb Z_+\cup\{+\infty\}$ and an offset $t_i\in(-d_i,0]$ and pulls it at $t_i+kd_i$, $k\ge1$; it is a $K$-PPP if at most $K$ arms are pulled in any period. Algorithm 2 takes an optimal solution $x^*$ of the upper-bound program, lifts each coordinate to a frequency $1/d^{(k)}_i$, rounds every period up to the set $D[a]=\bigcup_{j\le a}\{(2j-1)2^\ell\}$, packs the arms with periods in each $\{(2j-1)2^\ell\}$ into at most $\lceil K_j\rceil$ groups that can each be served one arm per period, and keeps the $K$ groups of largest long-run reward. The Lean names follow the paper: F, FT, UB, supp, Rcc, roundUp, PPP, IsKPPP, IsRSRun (Algorithm 1), IsAlg2Run (Algorithm 2), gamma.

Formalization targets

Goal: Theorem 1

There is an absolute constant $C$ such that for every admissible instance and every $K\ge1$, Algorithm 2 has a run, every output $\pi$ of every run is a $K$-PPP, and for every $T\ge1$

$$\mathrm{Reward}_T(\pi)\ \ge\ \gamma_K\cdot\mathrm{UB}_R[K]\cdot T-C\,N\,R_{\max},\qquad \gamma_K=\max_{a\in\mathbb Z_+}\frac{a}{a+1}\cdot\frac{K}{K+a}.$$

The constant is not fixed in the statement; the paper's proof gives $C=2$.

Milestones

1. Claims 1–3 in the proof of Lemma 1: optimal schedules for the concave envelope use two consecutive gap lengths, and the long-run value is the interpolation of $R^{cc}_i(d)/d$ (Claim 1 carries a small correction: it needs $xT\ge1$).
2. Lemma 1: $F_i$ is piecewise linear concave with nodes $1/d^{(k)}_i$, values $R_i(d^{(k)}_i)/d^{(k)}_i$, flat beyond $1/d^{(1)}_i$, and $F_i\ge F_{i,T}$.
3. Lemma 2: $\mathrm{OPT}\le T\cdot\mathrm{UB}_R[K]$, and the program has an optimal solution with all but one coordinate in $\{0\}\cup\{1/d^{(k)}_i\}$.
4. Lemma 3: rounding to $D[a]$ loses at most a factor $a/(a+1)$.
5. Proof of Lemma 4, Part 1: the prefix-sum fact for periods $(2j-1)2^\ell$.
6. §4.2: the groups and display (5), $K[a]<\sum_i x_i+a$.
7. §4.3: $K[a]\le K+a$ and the long-run ratio $\frac a{a+1}\cdot\frac K{K+a}$.

Significance

Theorem 1 says that, with no assumption on the shape of recovery beyond monotonicity, a schedule that pulls every chosen arm at a fixed period loses only a factor $\gamma_K\ge 1/4$ against an upper bound on the optimum, and $1-\gamma_K=O(1/\sqrt K)$. The offline problem is NP-hard even within purely periodic policies, so a constant-factor guarantee for a simple, polynomial-time policy is the relevant benchmark. The paper's online results (an $\tilde O(\sqrt T)$ regret against $\gamma_K\cdot\mathrm{UB}_R[K]\cdot T$) are measured against exactly this quantity.

Formalizing it produces a checked statement of what "the policy returned by Algorithm 2" guarantees for every admissible run, including the boundary effects behind the $O(N)$ term. The result is proved in the paper; it has no machine-checked proof that we know of. The developments of the long-run value of a single arm (a limsup of a finite optimization), of dyadic period packing, and of top-$K$ averaging are reusable for other periodic-scheduling and recharging-bandit statements.

Difficulty

The obvious first idea is to schedule each arm at its optimal frequency $x^*_i$ directly. It fails twice: $1/x^*_i$ need not be an integer, and arbitrary periods cannot be interleaved (periods $2$ and $3$ always collide). The rounding to $D[a]$ makes the periods in each class divide one another, at a loss of $a/(a+1)$, and the packing step then costs a factor $K/(K+a)$; balancing the two gives $\gamma_K$. The single hardest piece is Lemma 1: $F_i$ is defined as a limsup of a finite combinatorial optimization, and identifying it with the piecewise-linear interpolation needs the exchange argument of Claim 1 and an asymptotic construction in Claim 2. Lemma 2's "all but one coordinate" uses the piecewise linearity of every $F_i$.

Formalization scope

Arms are Fin N, recovery functions ℕ → ℝ with the four admissibility conditions; the paper's $K\le N$ is not assumed. A schedule is a finite set of pull times in $[1,T]$, and every first gap is measured from time $0$. $F_{i,T}$ and $\mathrm{UB}_R[K]$ are suprema of the optimization problems themselves, and $F_i$ is the real Filter.limsup over $T\ge1$ of a sequence bounded in $[0,R_{\max}]$; $F_i$ is never defined by the closed form of Lemma 1. Periods live in WithTop ℕ with $\top=+\infty$. Concavity on $\{0,1,2,\dots\}$ means non-increasing increments. Algorithm 1 and Algorithm 2 are relations on runs: every choice the paper leaves open (the optimal $x^*$, the maximizer $a^*$, the grouping, the offsets, ties in the top-$K$ selection) is free, and the goal quantifies over all of them while also asserting that a run exists. That existence clause, and the requirement that groups number at most $\lceil K_j\rceil$ and that the selection be of maximal reward, rule out a vacuous relation or a trivially weak selection. The $O(N)$ term is $C\cdot N\cdot R_{\max}$ with $C$ chosen before the instance, so it cannot absorb the growth in $T$.

Not part of this mission: Theorem 2 (tightness), the online learning results (Theorem 3, Corollary 1, Proposition 2), the refined ratio of §6, and the running-time clauses of Lemma 4.

Contributions welcome: proofs of the milestones in any order; a general library for the upper concave envelope of a function on $\mathbb N$ and its supporting points; the 1-PPP construction for periods with a common odd part.

Selected references

• D. Simchi-Levi, Z. Zheng, F. Zhu, Offline Planning and Online Learning under Recovering Rewards, arXiv:2106.14813v2, 2021; Management Science, 2024. https://arxiv.org/abs/2106.14813
• R. Kleinberg, N. Immorlica, Recharging Bandits, FOCS 2018. https://arxiv.org/abs/1704.05919
• S. Basu, R. Sen, S. Sanghavi, S. Shakkottai, Blocking Bandits, NeurIPS 2019. https://arxiv.org/abs/1907.06819
• C. Pike-Burke, S. Grünewälder, Recovering Bandits, NeurIPS 2019. https://arxiv.org/abs/1910.14354
• A. Bar-Noy, R. Bhatia, J. Naor, B. Schieber, Minimizing Service and Operation Costs of Periodic Scheduling, Mathematics of Operations Research 27(3), 2002. https://doi.org/10.1287/moor.27.3.518.314

Small-loss guarantees under partial feedback

In adversarial online learning a learner chooses one of $d$ actions (arms) in each of $T$ rounds and suffers a loss in $[0,1]$. Classical regret bounds grow with the horizon, $O(\sqrt{T\log d})$. A small-loss bound replaces $T$ by the loss $L^\star$ of the best arm, which matters whenever good actions exist: routing traffic, choosing treatments, recommending items. With full information (all losses revealed each round) such bounds are standard. With partial information, where only some losses are observed, they were known only for pseudo-regret in special cases, as discussed in Lykouris, Sridharan and Tardos (arXiv:1711.03639v5), §1.2.

That paper gives a black-box reduction: any full-information learner with a small-loss guarantee becomes a learner for graph feedback with a high-probability small-loss guarantee. The bound depends on the independence number of the feedback graphs instead of the number of arms. This mission formalizes the reduction's central high-probability statement, Theorem 3.6, together with the chain of claims its proof rests on.

Timeline:

• 2006: Allenberg, Auer, Györfi and Ottucsák introduce freezing for small-loss pseudo-regret with bandit feedback.
• 2011: Mannor and Shamir introduce graph feedback (arXiv:1106.2436).
• 2013–2017: Alon et al. give Exp3-SET style $\tilde O(\sqrt{\alpha T})$ uniform bounds (arXiv:1409.8428).
• 2017–2022: Lykouris, Sridharan and Tardos extend freezing to graphs by double thresholding and obtain the first small-loss bounds there (arXiv:1711.03639; Mathematics of Operations Research, 2022).

Setting

There are $d$ arms. In round $t$ the adversary fixes an undirected feedback graph $G^t$ on the arms, which the learner sees before acting, and a loss vector $\ell^t\in[0,1]^d$. Both may depend on everything that happened in earlier rounds. The learner picks a distribution $w^t$, an arm $I(t)\sim w^t$ is drawn, and the learner observes $\ell^t_j$ for every $j$ in the closed neighbourhood $N^t_{I(t)}$ (the arm and its neighbours). A natural number $\alpha$ bounds the independent sets if no $G^t$ has more than $\alpha$ pairwise non-adjacent arms.

The $\varepsilon$-approximate regret against an arm $f$ is

$$\mathrm{ApxReg}(f,\varepsilon)=(1-\varepsilon)\sum_t\ell^t_{I(t)}-\sum_t\ell^t_f .$$

A full-information algorithm $A$ maps past loss vectors to a probability vector $p^t$. It has the guarantee $A(d,T)$ at parameter $\varepsilon'$ and range $L$ if $(1-\varepsilon')\sum_t\langle p^t,\ell^t\rangle-\sum_t\ell^t_f\le L\,A(d,T)/\varepsilon'$ for every loss sequence in $[0,L]$ and every arm $f$.

The Double-Threshold Freezing Algorithm (Algorithm 1) takes $A$, $\alpha$ and $\varepsilon'$ and sets $\gamma=\varepsilon'/(4\alpha)$ and $\gamma'=\gamma/3$. In each round it does the following.

1. It freezes $F_0=\{i:\sum_{j\in N_i}p_j<\gamma\}$.
2. It recursively freezes every remaining arm whose probability of being observed by unfrozen arms is below $\gamma'$; the result is $F=\bigcup_kF_k$.
3. It renormalizes, $w_i=p_i/(1-\sum_{j\in F}p_j)$ for $i\notin F$ and $w_i=0$ for $i\in F$, and draws $I(t)\sim w$.
4. It feeds $A$ the estimates $\tilde\ell_i=\ell_i/W_i$ for $i\in N_{I(t)}\setminus F$ and $\tilde\ell_i=0$ otherwise, where $W_i=\sum_{j\in N_i}w_j$.

Formalization targets

Goal: Theorem 3.6 with the corrected constant

Let $\varepsilon,\delta>0$ and $\varepsilon'=\varepsilon/5$. Suppose every $G^t$ has independent sets of at most $\alpha$ vertices and $A$ has the guarantee $A(d,T)$ at $\varepsilon'$ on the range $L=1/\gamma'=12\alpha/\varepsilon'$. Then Algorithm 1 satisfies

$$\Pr\Big[\exists f:\ \mathrm{ApxReg}(f,\varepsilon)>\frac{300\,\alpha\,\big(A(d,T)+3\log\frac{d+2}{\delta}\big)}{\varepsilon^2}\Big]\le\delta .$$

Milestones

The milestones follow the order of the proof:

• Claim 3.2: $\sum_{i\in F_0}p_i\le\alpha\gamma$.
• Claim 3.3: $\sum_{i\in\bigcup_{k\ge1}F_k}p_i\le3\sum_{i\in F_0}p_i$.
• Lemma 3.1: $\sum_{i\in F}p_i\le\varepsilon'$ and $w_i\le p_i/(1-\varepsilon')$ off $F$.
• Three properties of the estimator from the proof of Theorem 3.4: $0\le\tilde\ell_i\le1/\gamma'$; unbiased off $F$; negatively biased everywhere.
• Lemma 3.7: multiplicative Chernoff bounds for adapted $[0,1]$-valued sequences.
• Item 1 of the proof of Theorem 3.6: $\sum_t\ell^t_{I(t)}\le(1+\varepsilon')\sum_t\langle w^t,\ell^t\rangle+(1+\varepsilon')\ln(1/\delta')/\varepsilon'$ with probability $1-\delta'$.

Significance

The theorem turns approximate-regret guarantees of full-information learners into high-probability guarantees under graph feedback. The bound scales with $\alpha$ rather than $d$ and has no dependence on $T$. With the doubling trick of Lemma 3.8 it gives the paper's $\tilde O\big(\alpha^{1/3}(L^\star)^{2/3}\big)$ high-probability small-loss regret (Theorem 3.9). The same framework yields the paper's results for semi-bandits, contextual bandits and shifting comparators (§5).

Status. The paper states the bound with constant $100$, and that constant is false. A counterexample has $d=2$, complete graphs, $\alpha=1$, $\varepsilon=\delta=1/2$ and losses $(1,0)$ in every round. The learner $A$ has $A(d,T)=20$: it spends its regret budget on arm 1 first and then runs Hedge. Algorithm 1 then plays arm 1 for $26\,085$ rounds with certainty, so $\mathrm{ApxReg}(2,1/2)=13\,042.5$, above the printed bound of about $10\,495$. The proof bounds the estimated losses by $1/\gamma$, but only $1/\gamma'=3/\gamma$ holds (proof of Theorem 3.4). Carried through with $1/\gamma'$, the proof gives $300$, and the same family of instances shows that no smaller constant of this form works. No part of this chain has a machine-checked proof that this mission knows of. A complete formalization would check the corrected constant and the high-probability reduction.

Difficulty

The obvious approach uses importance weighting with uniform exploration, as in Exp3. It bounds the variance of the estimates through the loss of the worst arm, so it gives uniform rather than small-loss bounds. Freezing avoids this, but freezing one arm lowers the observation probability of its neighbours and can cascade. The central combinatorial step, Claim 3.3, bounds the cascade by a charging argument along the freezing order. The probabilistic difficulty is that the estimated losses fed to $A$ depend on the arms drawn, so the three concentration steps need a martingale (adapted) Chernoff bound with multiplicative error (Lemma 3.7) rather than Hoeffding's inequality. The final chain also has to track the estimator range $1/\gamma'$ correctly, which is exactly where the printed proof slips.

Formalization scope

Arms are Fin d and graphs are SimpleGraph (Fin d); closed neighbourhoods include the arm itself. Rounds are $0$-based and arm paths are Fin T → Fin d. The adversary is a deterministic map from the earlier arms to $(G^t,\ell^t)$; randomized adversaries are mixtures of deterministic ones. $A$ is a deterministic map from the list of past (estimated) loss vectors to a probability vector, and its guarantee is assumed only at $\varepsilon'=\varepsilon/5$, $L=1/\gamma'$ and horizon $T$. Probabilities are sums of path probabilities $\prod_tw^t_{I(t)}$, which sum to one. The bound is stated for all comparator arms at once, inside one event. The logarithm is natural. When every arm carrying probability is frozen (possible only for $\varepsilon'\ge1$, i.e. $\varepsilon\ge5$), the algorithm plays $p$; the goal is trivial there.

The goal is not vacuous. A learner with the guarantee and an adversary with nonempty graphs satisfying the $\alpha$ bound exist; the path probabilities sum to $1$; and the event is not empty in general (the counterexample makes it certain for the constant $100$). Lemma 3.7 is stated for an arbitrary filtration in Mathlib's measure-theoretic language and is reusable on its own. Contributions are welcome on each claim separately, on Lemma 3.7, and on a bridge from the path-sum model to Lemma 3.7.

Selected references

• T. Lykouris, K. Sridharan, É. Tardos, Small-loss bounds for online learning with partial information, arXiv:1711.03639v5, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1711.03639v5
• C. Allenberg, P. Auer, L. Györfi, G. Ottucsák, Hannan consistency in on-line learning in case of unbounded losses under partial monitoring, ALT 2006. https://doi.org/10.1007/11894841_20
• S. Mannor, O. Shamir, From bandits to experts: on the value of side-observations, NeurIPS 2011. https://arxiv.org/abs/1106.2436
• N. Alon, N. Cesa-Bianchi, C. Gentile, S. Mannor, Y. Mansour, O. Shamir, Nonstochastic multi-armed bandits with graph-structured feedback, SIAM J. Computing, 2017. https://arxiv.org/abs/1409.8428
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM J. Computing, 2002. https://doi.org/10.1137/S0097539701398375

Motivation

Two-player zero-sum extensive-form games (poker, negotiation, security games) are solved at scale by first-order methods. Writing each player's strategy in sequence form turns the computation of a Nash equilibrium into a bilinear saddle-point problem $\min_{x\in\mathcal X}\max_{y\in\mathcal Y}x^\top Ay$ over two polytopes, and methods such as Nesterov's excessive gap technique (EGT) and Nemirovski's mirror prox solve it at rate $O(1/T)$. Both need a distance-generating function (DGF) on each polytope, and their convergence bounds scale with the DGF's range divided by its strong-convexity modulus.

Hoda, Gilpin, Peña and Sandholm (2010) introduced dilated DGFs, which keep the proximal step computable in linear time. Kroer, Waugh, Kılınç-Karzan and Sandholm (2020) gave the dilated entropy explicit weights with modulus $1/M_Q$ in $\ell_1$, but their weights double at every level of the decision tree, so the range of the DGF grows like $2^{\mathfrak D_Q}$ in the depth $\mathfrak D_Q$. Farina, Kroer and Sandholm (arXiv:2105.12954v2, 2021; Operations Research, 2025) remove this exponential factor with the dilatable global entropy.

Setting

A sequential decision problem has a finite set $J$ of decision points; at each $j\in J$ a finite nonempty set of actions $A_j$; and for each $j$ a parent sequence $p_j$, the last decision point–action pair $ja$ before $j$, or the empty sequence $\varnothing$ if the player has not acted yet. The decision points form a tree. The sequences are $\Sigma=\{\varnothing\}\cup\{ja : j\in J, a\in A_j\}$, and $\mathcal C_\sigma=\{j : p_j=\sigma\}$ is the set of decision points that follow $\sigma$.

The sequence-form polytope is

$$Q=\Big\{x\in\mathbb R^\Sigma_{\ge0} : x_\varnothing=1,\ \sum_{a\in A_j}x_{ja}=x_{p_j}\ \forall j\in J\Big\},$$

and $M_Q=\max_{x\in Q}\|x\|_1$. The weights are defined from the leaves up by

$$\gamma_j=1+\max_{a\in A_j}\sum_{j'\in\mathcal C_{ja}}\gamma_{j'},\qquad \gamma_\varnothing=1+\sum_{j\in\mathcal C_\varnothing}\gamma_j,\qquad w_\sigma=\gamma_\sigma-\sum_{j\in\mathcal C_\sigma}\gamma_j ,$$

with $\gamma_{ja}:=\gamma_j$. The dilatable global entropy (Definition 4) is

$$\tilde\varphi(x)=w_\varnothing x_\varnothing\log x_\varnothing+\sum_{j\in J}\sum_{a\in A_j}w_{ja}x_{ja}\log x_{ja}+\sum_{j\in J}\gamma_j x_{p_j}\log|A_j| ,$$

and the dilated entropy with the same weights is $\varphi(x)=\gamma_\varnothing x_\varnothing\log x_\varnothing+\sum_j\gamma_j\big(x_{p_j}\log|A_j|+\sum_a x_{ja}\log(x_{ja}/x_{p_j})\big)$. In Lean these are seqFormPolytope, MQ, gamma, gammaRoot, weight, dge and dilatedEntropy over a SeqDecisionProblem.

Formalization targets

Goal: Theorems 4, 5 and 6

For every sequential decision problem:

1. $\tilde\varphi$ is continuous on $Q$, differentiable on $\operatorname{relint}Q$, nonnegative on $Q$, and vanishes somewhere on $Q$;
2. ($\ell_2$, Theorem 4) for all $x,x'\in\operatorname{relint}Q$,

$$\big(\nabla\tilde\varphi(x)-\nabla\tilde\varphi(x')\big)^\top(x-x')\ge\|x-x'\|_2^2;$$

3. ($\ell_1$, Theorem 5) for all $x,x'\in\operatorname{relint}Q$,

$$\big(\nabla\tilde\varphi(x)-\nabla\tilde\varphi(x')\big)^\top(x-x')\ge\tfrac1{M_Q}\|x-x'\|_1^2;$$

4. (range, Theorem 6 as corrected) for all $x,x'\in Q$,

$$\tilde\varphi(x)-\tilde\varphi(x')\le M_Q^2\max_{j\in J}\log|A_j| .$$

Milestones

In proof order: the weights satisfy $\gamma_j\ge1$ and $w_\sigma\ge1$ (Definition 4); $\tilde\varphi=\varphi$ on $Q$ (Theorem 3); $\operatorname{relint}Q\subseteq(0,1]^\Sigma$; $\tilde\varphi\ge0$ on $Q$, with the uniform strategy as its unique zero; Theorem 4; Theorem 5; $\gamma$ is largest at root decision points and $\gamma_j\le M_Q$; and $\sum_j x_{p_j}\le M_Q$ on $Q$.

Significance

The range bound, divided by the modulus, is the constant in the $O(1/T)$ rates of EGT and mirror prox. The Kroer et al. dilated entropy achieves range $2^{\mathfrak D_Q+2}M_Q^2\max_j\log|A_j|$ at the same $\ell_1$ modulus. The dilatable global entropy improves it by the factor $2^{\mathfrak D_Q+2}$, and because it coincides with a dilated entropy on $Q$ (Theorem 3), its proximal step keeps the linear-time closed form. In deep but narrow trees, where the number of decision points is linear in the depth, this replaces an exponential constant by a polynomial one.

The results are proved in the paper. No machine-checked version exists. The mission adds to the platform sequence-form strategies, tree-form decision problems and distance-generating functions on polytopes with boundary, none of which it has yet. Theorem 6 is formalized in corrected form: as printed it bounds the Bregman diameter $\max_{x,x'}D_{\tilde\varphi}(x\,\|\,x')$, which is infinite, while its proof bounds $\max_Q\tilde\varphi-\min_Q\tilde\varphi$, which is the quantity the convergence theorems use.

Difficulty

The ingredients are elementary, but none is a one-line unfolding. Theorem 3 telescopes logarithms across the tree using the flow constraints of $Q$, so it needs an induction over the tree. The minimum and its uniqueness are statements about every decision point at once, through entropy bounds on conditional distributions. For Theorems 4 and 5, the Hessian bound $\operatorname{diag}(w_\sigma/x_\sigma)\succeq I$ on $(0,1]^\Sigma$ must be turned into the gradient-monotonicity form of Definition 1 on $\operatorname{relint}Q$, where $\tilde\varphi$ is not twice differentiable at the boundary. The relative interior must first be identified: the open cube $(0,1)^\Sigma$ of the printed proof contains no point of $Q$, because $x_\varnothing=1$. The bound $\gamma_j\le M_Q$ relates a recursively defined weight to a maximum over the whole polytope.

Formalization scope

A decision problem is a structure with a finite type of decision points, finite nonempty action types, a parent map into Option (Σ j, A j) (none is $\varnothing$) and a well-founded child relation. There may be several roots, and $J$ may be empty. The weights $\gamma_j$ are defined by WellFounded.fix. $\tilde\varphi$ is the formula of Definition 4 on all of $\mathbb R^\Sigma$ with Mathlib's Real.log ($0\log0=0$), and $\nabla\tilde\varphi(x)^\top v$ is fderiv ℝ (dge P) x v. Because $x-x'$ is tangent to $Q$, the extension off $Q$ does not affect the inequalities. The relative interior is intrinsicInterior ℝ. The $\ell_1$ and $\ell_2$ norms are explicit sums, since Mathlib's norm on Seq P → ℝ is the sup norm. $M_Q$ is an sSup over $Q$ counting $x_\varnothing$. $\max_j\log|A_j|$ is the logarithm of the largest $|A_j|$, which is $0$ when $J$ is empty.

The DGF clause keeps differentiability on $\operatorname{relint}Q$ as a separate conjunct, so the strong-convexity clauses cannot hold through a junk derivative. The platform's existing DGF definitions require differentiability on all of $Q$, which the entropy lacks at the boundary, and are not used. A sanity file checks on the one-decision-point, two-action problem that $M_Q=2$, that the uniform strategy lies in $\operatorname{relint}Q$, and that the range clause is not trivial.

Contributions of general use are welcome: induction principles for tree-form decision problems, the bound $Q\subseteq[0,1]^\Sigma$, and a lemma turning a Hessian lower bound on a relatively open convex set into gradient monotonicity.

Selected references

• G. Farina, C. Kroer, T. Sandholm, Better Regularization for Sequential Decision Spaces: Fast Convergence Rates for Nash, Correlated, and Team Equilibria, arXiv:2105.12954v2, 2021; Operations Research, 2025. https://arxiv.org/abs/2105.12954v2
• C. Kroer, K. Waugh, F. Kılınç-Karzan, T. Sandholm, Faster algorithms for extensive-form game solving via improved smoothing functions, Mathematical Programming 179, 2020. https://doi.org/10.1007/s10107-018-1336-7
• S. Hoda, A. Gilpin, J. Peña, T. Sandholm, Smoothing techniques for computing Nash equilibria of sequential games, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0452
• Y. Nesterov, Excessive gap technique in nonsmooth convex minimization, SIAM Journal on Optimization 16(1), 2005. https://doi.org/10.1137/S1052623403422285
• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization, SIAM, 2001. https://doi.org/10.1137/1.9780898718829
• B. von Stengel, Efficient computation of behavior strategies, Games and Economic Behavior 14(2), 1996. https://doi.org/10.1006/game.1996.0050