All missions

Why transaction fee mechanisms

A blockchain confirms a limited number of transactions per block. Users attach fees (bids) to their transactions; the block producer (the miner) chooses which transactions to include and collects some of the fees. The rule that maps bids to confirmations, payments and miner revenue is a transaction fee mechanism (TFM). Because the miner is itself a strategic party that can collude with users, inject fake transactions or drop real ones, a TFM must resist more deviations than an ordinary auction.

Roughgarden (arXiv:2012.00854, 2020) formalized the desiderata for Ethereum's EIP-1559. Chung and Shi (arXiv:2111.03151, SODA 2023) proved that no TFM can be both dominant-strategy incentive compatible for users and 1-side-contract-proof while giving the miner positive revenue: in that setting the miner's revenue must be zero. Chen, Simchi-Levi, Zhao and Zhou (arXiv:2209.13099, Operations Research 2025) relax dominant-strategy to Bayesian incentive compatibility, with valuations drawn i.i.d. from a known law, and construct a mechanism that escapes the zero-revenue barrier.

Setting

There are $n$ users and a block of size $k$. User $i$ has a valuation $v_i\in[0,1]$; valuations are i.i.d. draws from a law $V_0$ on $[0,1]$, and $c_\rho=\mathbb E_{v\sim V_0}[v^2]$. Users submit bids $\mathbf b\in[0,1]^n$.

A TFM $M=(\mathbf a,\mathbf p,r)$ consists of an allocation rule $a_i(\mathbf b)$ (the probability that user $i$ is confirmed), a payment rule $p_i(\mathbf b)$ (paid by user $i$ if confirmed) and a miner revenue rule $r(\mathbf b)$. User $i$'s utility is $u_i(b_i,\mathbf b_{-i};v_i)=a_i(\mathbf b)(v_i-p_i(\mathbf b))$; the miner's utility is $r(\mathbf b)$.

The properties studied are:

• U-BNIC: if the others bid truthfully, bidding $v_i$ maximizes $\mathbb E_{\mathbf b_{-i}\sim V_0^{n-1}}[u_i(b_i,\mathbf b_{-i};v_i)]$;
• 1-SCP: the miner and one user cannot raise $u_i+r$ by changing that user's bid;
• UIR: $u_i(v_i,\mathbf b_{-i};v_i)\ge0$ for all $\mathbf b_{-i}$;
• BF: $r(\mathbf b)\le\sum_ia_i(\mathbf b)p_i(\mathbf b)$;
• $(C,N)$-U-SP: when $n>N$, a truthful user cannot raise her expected utility, counting the utilities of her fake identities at value $0$, by injecting $l\le Cn$ fake bids.

Mechanism 3 confirms $k$ transactions by weighted sampling without replacement with weights $w_j=e^{mb_j}$; $a_i(\mathbf b)$ is the resulting inclusion probability. Its payment is the Myerson payment of this allocation plus a quadratic variation term

$$\theta_i(\mathbf b)=-\tfrac12hb_i^2\Bigl(\frac{\sum_{j\ne i}b_j^2}{c_\rho(n-1)}-1\Bigr),$$

and the miner receives $\tilde r(\mathbf b)=\frac12h\bigl(\sum_ib_i^2-\sum_{i<j}b_i^2b_j^2/(c_\rho(n-1))\bigr)$.

Formalization targets

Goal: Theorem 4 (Main Theorem)

For any $k\ge1$, $n\ge2$ and $m,h\ge0$, Mechanism 3 is U-BNIC and 1-SCP. For any $\lambda_0>e/(e-1)$ and $n\ge\max\{\lambda_0k,30\}$, with $m=m_\#(\lambda_0)=\min\{\frac12\ln\frac1{\ln(\lambda_0/(\lambda_0-1))},1\}$, it is UIR and BF for every

$$h\in\Bigl[0,\ g(\lambda_0)\frac{2kc_\rho(n-1)}{en^2}\Bigr].$$

Finally, there is an absolute constant $K$ such that for every $C\in[0,1)$ the mechanism is $(C,K/(1-C))$-U-SP.

Milestones

1. Lemma 1 (Myerson's Lemma) and Lemma EC.3: U-DSIC, respectively 1-SCP, are equivalent to a monotone allocation with a constrained payment.
2. Observation 1 and Theorem 2: an admissible variation term added to the auxiliary (Myerson) mechanism yields U-BNIC and 1-SCP.
3. Lemma 2: the quadratic term $(\theta,\tilde r)$ is admissible.
4. EC.4.4.1: the sampling allocation is monotone in the own bid.
5. (EC.131) and (EC.134)–(EC.135): $\partial a_i/\partial b_i\ge\frac kn\frac{g(\lambda_0)}e$ and $a_ip_i\ge\frac{g(\lambda_0)}{2e}\frac kn b_i^2$.
6. Lemma EC.4 and Proposition EC.1: adding an item to weighted sampling without replacement never raises an existing item's inclusion probability, so a fake bid never helps in the auxiliary mechanism.

Significance

Theorem 4 shows that Bayesian incentive compatibility suffices to give the miner positive revenue while keeping users truthful, blocking miner–user collusion and Sybil attacks, and keeping the mechanism individually rational and budget feasible. The expected miner revenue is $\frac14hnc_\rho$, a constant fraction of the optimum for fixed $c_\rho$ once $n\ge\max\{\lambda_0k,30\}$. The auxiliary-variation decomposition (Theorem 2) is a general recipe that applies to any monotone allocation.

None of this has been machine-checked. A complete development would give a verified Myerson lemma for allocation rules with general block size. Mathlib has no such lemma, and the version already on the platform covers single-unit auctions only. It would also give a formal treatment of inclusion probabilities in weighted sampling without replacement (Plackett–Luce sampling), with monotonicity and the "adding an item" comparison. Both are used well beyond blockchains: in ranking, survey sampling and randomized auctions.

The printed definition (18), $c_\rho=\int_0^1\rho^2$, is a slip: the paper's own proofs use $c_\rho=\mathbb E[v^2]$, and under $\int\rho^2$ the first clause fails (for the uniform law a value-1 user gains by shading her bid). The mission states the corrected theorem.

Difficulty

The U-BNIC and 1-SCP clause reduces, through Theorem 2, to monotonicity of the sampling allocation and to Lemma 2, which is a second-moment computation. Monotonicity is the first obstacle. The inclusion probability is a sum over all injective draw sequences, and raising one weight raises some terms and lowers others, so a term-by-term comparison fails. The paper uses a coupling through a common uniform sequence (Algorithm 1). Lemma EC.4 needs the same coupling.

UIR and BF need a quantitative lower bound on $\partial a_i/\partial b_i$ that is uniform in the other bids and in $k\le n/\lambda_0$. The obvious bound loses a factor that tends to zero as $k/n\to1/\lambda_0$, and the explicit constant $g(\lambda_0)$ comes from a careful choice of $m$. The U-SP clause for general $k$ is only sketched in the paper ("in a similar way"). Its fake-bid bookkeeping, with mechanisms at different bid counts and their own $h_\eta$, has to be written out in full.

Formalization scope

Users are Fin n. Bids, values and the other users' bids range over $[0,1]$, and $\mathbf b_{-i}$ is a vector in $[0,1]^n$ whose $i$-th entry is overwritten. $V_0$ is any probability measure on $\mathbb R$ with $V_0([0,1])=1$ and $c_\rho=\int t^2\,dV_0>0$, a generalization of the paper's density assumption. Interim expectations are Bochner integrals against the product measure $V_0^{\otimes n}$ with coordinate $i$ overwritten. U-BNIC and U-SP require the integrands to be integrable, so that a non-existent expectation, which Lean evaluates to $0$, cannot make them hold vacuously.

The allocation sums the outcome probabilities (24) over injective sequences, so $k\ge n$ gives $a_i=1$. Payments are payments-if-confirmed and expected payments are $a_ip_i$. The auxiliary payment is written in the form (EC.137), $a_ip_i=a_ib_i-\int_0^{b_i}a_i$. 1-SCP is the ex-post deviation of the miner together with one user's bid. The $O(\frac1{1-C})$ in U-SP is an absolute constant $K$, chosen before $\lambda_0$, $k$, $V_0$, the $h_\eta$ and $C$. Lemma 1, Lemma EC.3 and Theorem 2 are stated for allocations differentiable in the own bid, as their formulas presuppose.

Definitions: Model, Properties, Decomposition, Sampling, Mechanism3 and Constants, in the namespace BlockchainTFM. The Myerson-type lemmas and the sampling lemmas are reusable on their own. Contributions on the sampling coupling and on the envelope argument behind Lemma 1 are particularly welcome.

Selected references

• X. Chen, D. Simchi-Levi, Z. Zhao, Y. Zhou, Bayesian Mechanism Design for Blockchain Transaction Fee Allocation, arXiv:2209.13099v7, 2024; Operations Research, 2025. https://arxiv.org/abs/2209.13099
• H. Chung, E. Shi, Foundations of Transaction Fee Mechanism Design, SODA 2023. https://arxiv.org/abs/2111.03151
• T. Roughgarden, Transaction Fee Mechanism Design for the Ethereum Blockchain: An Economic Analysis of EIP-1559, 2020. https://arxiv.org/abs/2012.00854
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58

Motivation

Many resource allocation problems arrive one request at a time: an ad exchange decides which campaign gets an impression, a network admits or routes a call, a cloud provider schedules a job. Each decision earns a reward and consumes several budgets, and it cannot be revisited. The usual benchmark is the offline optimum, the best total reward attainable with the whole request sequence known in advance. Dual-based algorithms handle the online problem by pricing the resources through Lagrange multipliers and treating each request greedily against those prices.

Balseiro, Lu and Mirrokni (arXiv:2011.10124) analyse a single algorithm of this kind, dual mirror descent. It updates the prices by online mirror descent and needs no knowledge of the request distribution. Earlier dual methods (Devanur–Hayes 2009, Agrawal–Wang–Ye 2014, Devanur et al. 2019) estimate prices from samples or solve auxiliary linear programs, and they assume linear or concave rewards. This paper allows non-concave rewards, non-linear consumption and non-convex or integral action sets. It shows that the same algorithm has sublinear regret under i.i.d. input, a constant competitive ratio under adversarial input, and good behaviour under several non-stationary inputs. This mission formalizes the i.i.d. result, Theorem 1.

Setting

There are $m\ge1$ resources and a horizon of $T$ periods. A request $s\in S$ consists of a compact feasible set $X_s\subseteq\mathbb R^d_+$ with $0\in X_s$, a reward function $f_s\ge0$ and a consumption function $b_s$ with values in $\mathbb R^m_+$ and $b_s(0)=0$. The total budget is $T\rho$, where $\rho_j>0$ for every $j$. For a request sequence $\vec\gamma=(\gamma_1,\dots,\gamma_T)$ the offline optimum is

$$\mathrm{OPT}(\vec\gamma)=\max\Big\{\sum_{t=1}^T f_t(x_t): x_t\in X_t,\ \sum_{t=1}^T b_t(x_t)\le T\rho\Big\}.$$

Assumption 1 asks for constants $\bar f,\bar b\ge0$ such that $0\le f_s\le\bar f$ and $\|b_s\|_\infty\le\bar b$ on $X_s$, and such that $\max_{x\in X_s}\{f_s(x)-\mu^\top b_s(x)\}$ is attained for every $\mu\ge0$. Write $\underline\rho=\min_j\rho_j$ and $\bar\rho=\max_j\rho_j$.

Algorithm 1 is given a reference function $h$, a step size $\eta>0$ and an initial price vector $\mu_1\in\mathbb R^m_+$, and starts with $B_1=T\rho$. In period $t$ it computes $\tilde x_t\in\arg\max_{x\in X_t}\{f_t(x)-\mu_t^\top b_t(x)\}$. It plays $x_t=\tilde x_t$ if $b_t(\tilde x_t)\le B_t$ and $x_t=0$ otherwise, and sets $B_{t+1}=B_t-b_t(x_t)$. It then takes the subgradient $g_t=\rho-b_t(\tilde x_t)$ and updates

$$\mu_{t+1}\in\arg\min_{\mu\in\mathbb R^m_+}\ g_t^\top\mu+\frac1\eta V_h(\mu,\mu_t),\qquad V_h(x,y)=h(x)-h(y)-\nabla h(y)^\top(x-y).$$

Its reward is $R(A|\vec\gamma)=\sum_t f_t(x_t)$. Assumption 2 requires that $h$ be differentiable or essentially smooth in $\mathbb R^m_+$, and $\sigma$-strongly convex in $\|\cdot\|_1$ there.

Formalization targets

Goal: Theorem 1

For every $T\ge1$ and every probability law $P$ on $S$,

$$\mathbb E_{\vec\gamma\sim P^T}\big[\mathrm{OPT}(\vec\gamma)-R(A|\vec\gamma)\big]\le C_1+C_2\eta T+\frac{C_3}{\eta},$$

with $C_1=\bar f\bar b/\underline\rho$ and $C_2=(\bar b+\bar\rho)^2/(2\sigma)$. The constant $C_3$ is the largest Bregman divergence $V_h(\mu,\mu_1)$ over the $m+1$ points $\mu\in\{0,(\bar f/\rho_1)e_1,\dots,(\bar f/\rho_m)e_m\}$. The algorithm is fixed before $P$, so the bound holds for the worst-case regret $\sup_P$. With $\eta\asymp T^{-1/2}$ it is $O(\sqrt T)$.

Milestones, in the order the proof uses them

1. Step 1: before the stopping time $\tau_A$ (the first period in which some resource comes within $\bar b$ of its budget), the budget check never fails.
2. (10): the expected reward up to $\tau_A$ is at least $\mathbb E[\tau_A\bar D(\bar\mu_{\tau_A}|P)]$ minus a complementary-slackness term. Here $\bar D(\mu|P)=\mathbb E_{s\sim P}[f^*_s(\mu)]+\rho^\top\mu$ is the expected dual objective.
3. Proposition 5: the regret bound of online mirror descent on a convex set, with $\ell_1$ strong convexity and $\ell_\infty$-bounded subgradients.
4. (11): this bound, applied to $w_t(\mu)=\mu^\top(\rho-b_t(x_t))$ up to $\tau_A$.
5. Proposition 1: weak duality, $\mathrm{OPT}(\vec\gamma)\le D(\mu|\vec\gamma)$.
6. (12): $\mathbb E[\mathrm{OPT}]\le\tau\bar D(\mu|P)+(T-\tau)\bar f$.
7. The pivot bound: if $\tau_A<T$, choosing $\mu=(\bar f/\rho_j)e_j$ for an exhausted resource $j$ turns (11) into the constant $C_1$.

Significance

The theorem gives an $O(\sqrt T)$ regret bound for an algorithm that knows neither the request distribution nor the horizon's statistics. It holds without convexity of the rewards, the consumption or the action sets, and the constants do not grow with the number of resources once norms are matched to the problem ($\ell_\infty$ in the primal, $\ell_1$ in the dual). Choosing different reference functions turns the same statement into bounds for projected subgradient descent ($h=\tfrac12\|\mu\|_2^2$) and for multiplicative weights ($h=\sum_j\mu_j\log\mu_j$). The paper's lower bound of order $\sqrt T$ (Lemma 1, from Arlotto–Gurvich) shows the rate cannot be improved in general.

The result is proved in the paper. As far as a search of the platform shows (October 2026), none of its statements has a machine-checked proof. Proved platform theorems give online mirror descent bounds under other hypotheses: closed domains, Legendre reference functions, Euclidean norms. This mission adds the online allocation model, a formal Algorithm 1 with its budget check, and the probabilistic argument that connects them.

Difficulty

The natural first attempt is to bound $\mathrm{OPT}$ by the dual function at a fixed price and compare it with the algorithm period by period. This fails because the algorithm stops playing its proposed actions once a budget runs out, and that can happen at a random time. The proof therefore works up to the stopping time $\tau_A$ and needs three separate ingredients:

• an optional-stopping argument to replace the realized rewards by the expected dual objective (10);
• a regret bound of mirror descent against an adaptively chosen pivot (11);
• the observation that, if a resource is nearly exhausted, the pivot $(\bar f/\rho_j)e_j$ pays for the lost periods.

The expected dual objective is evaluated at random, history-dependent prices. So the measurability of the run, of the argmax selection and of $\mathrm{OPT}$ must be handled explicitly. When $h$ is only essentially smooth, one also has to show that the mirror step stays in the open orthant, where $\nabla h$ exists.

Formalization scope

• Representation. Resources are Fin m, actions Fin d → ℝ, and periods Fin T counted from $0$. A request type $S$ carries $X_s$, $f_s$, $b_s$ (DualMirrorAlloc.Requests).
• Optima. $\mathrm{OPT}$ and $f^*$ are real suprema (sSup). Under the model and Assumption 1 these sets are nonempty and bounded, so the suprema are the true values.
• The run. Algorithm 1 is a recursion on the state $(\mu_t,B_t)$ that reads only past requests. The budget check is coordinatewise; the budget is updated with the action played and the price with the action proposed.
• Selections. The argmax in (3) and the minimizer in (4) are arbitrary selections act, md with the optimality property, and every selection is covered.
• Bregman divergence. $\nabla h$ is the derivative within $\mathbb R^m_+$ (fderivWithin). Assumption 2.1 keeps both branches: differentiable within the orthant, or essentially smooth relative to it. Strong convexity (2.2) is required where the derivative exists, $\mu_1$ is such a point, and the norms are written as $\sum_j|v_j|$ and coordinatewise bounds.
• Expectation. The i.i.d. expectation is the integral under Measure.pi (fun _ : Fin T => P) for an arbitrary probability measure $P$ on a measurable space $S$, with the algorithm fixed first.
• Measurability. The hypotheses are joint measurability of $(s,\mu)\mapsto f_s(\tilde x)$ and $(s,\mu)\mapsto b_s(\tilde x)$, measurability of $s\mapsto f_s(0)$, of the mirror step, and of $\mathrm{OPT}$. Without them Lean's integral of a non-measurable function would be $0$ and the statement could hold vacuously. The step size satisfies $\eta>0$, since at $\eta=0$ the term $C_3/\eta$ would be read as $0$ in Lean.
• Stopping time. $\tau_A$ ranges over $\{0,\dots,T-1\}$. With the search starting at $1$, the Step-1 claim is false.

A complete development needs the following:

• optional stopping for a bounded stopping time on the product space;
• Danskin-type facts for $f^*$;
• the first-order optimality condition and three-point identity for the Bregman projection;
• for essentially smooth $h$, the fact that the mirror step stays interior.

The online mirror descent bound (Proposition 5) and the model of Algorithm 1 can be reused for the paper's other input models. Proofs of any milestone are welcome, as are proofs of Proposition 5 by other means.

Selected references

• S. R. Balseiro, H. Lu, V. Mirrokni, The Best of Many Worlds: Dual Mirror Descent for Online Allocation Problems, arXiv:2011.10124v3, 2021; Operations Research (forthcoming). https://arxiv.org/abs/2011.10124v3
• H. H. Bauschke, J. M. Borwein, P. L. Combettes, Essential smoothness, essential strict convexity, and Legendre functions in Banach spaces, Communications in Contemporary Mathematics 3(4), 615–647, 2001. https://doi.org/10.1142/S0219199701000524
• A. Beck, M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3), 167–175, 2003. https://doi.org/10.1016/S0167-6377(02)00231-6
• G. Chen, M. Teboulle, Convergence analysis of a proximal-like minimization algorithm using Bregman functions, SIAM Journal on Optimization 3(3), 538–543, 1993. https://doi.org/10.1137/0803026
• S. Agrawal, Z. Wang, Y. Ye, A dynamic near-optimal algorithm for online linear programming, Operations Research 62(4), 876–890, 2014. https://doi.org/10.1287/opre.2014.1289
• A. Arlotto, I. Gurvich, Uniformly bounded regret in the multisecretary problem, Stochastic Systems 9(3), 231–260, 2019. https://doi.org/10.1287/stsy.2018.0028

Motivation

A seller offers one item to one buyer whose valuation lies in $[0,\bar v]$ and whose valuation distribution $F$ is not known. Robust mechanism design asks for a selling mechanism that performs well against every distribution consistent with the seller's partial information. Without restrictions on the menu, the optimal robust mechanism randomizes over a continuum of prices, which is hard to explain and to implement. S. Wang, The Power of Simple Menus in Robust Selling Mechanisms (arXiv:2310.17392v3, 2024; Management Science, 2025), asks how much is lost when the seller may randomize over at most $n$ prices only, and finds that very small menus (two or three prices) already recover most of the robust performance.

The paper's tool for this question is Theorem 1: once the $n$ price levels are fixed, the robust problem is a finite linear program. Every closed form in the paper (support, mean and quantile information) and every numerical study is a solution of that program.

The result extends Theorem 1 of Wang, Liu and Zhang (Minimax regret robust screening with moment information, 2024) from moment information and continuous menus to general ambiguity sets of the form (2) and finite menus.

Setting

An $n$-level pricing mechanism posts price $v_l$ with probability $x_l$, where $0\le v_1\le\dots\le v_n\le\bar v$ and $x$ lies in the probability simplex; $\Pi_n$ is the set of such mechanisms. A buyer with valuation $w$ pays in expectation $t(w)=\sum_{l:\,v_l\le w}x_lv_l$, so the revenue against a distribution $F$ on $[0,\bar v]$ is $\mathrm{Rev}(\pi,F)=\int t\,dF$. The clairvoyant benchmark is the best posted-price revenue $\mathrm{Rev}(\mathrm{OPT},F)=\max_{p\in[0,\bar v]}p\,(1-F(p-))$.

The seller knows only that $F$ lies in the ambiguity set

$$\mathcal F=\Bigl\{F\in\mathcal P([0,\bar v]):\int\phi_k\,dF\ge0,\ k=1,\dots,K\Bigr\},$$

where each $\phi_k$ is bounded, piecewise continuous with finitely many segments, and nondecreasing within each segment (Assumption 1). Indicator constraints give support, quantile and multi-segment information; $\phi(w)=w-\mu$ gives a mean bound. The competitive ratio of $\pi$ is

$$\mathrm{CR}(\pi)=\inf_{F\in\mathcal F}\frac{\mathrm{Rev}(\pi,F)}{\mathrm{Rev}(\mathrm{OPT},F)} .$$

For Theorem 1, let $\mathcal B=\{b_1<\dots<b_m\}\subset(0,\bar v)$ be the breakpoints of the $\phi_k$, let $u_1\le\dots\le u_{n+m}$ be the price levels and breakpoints in ascending order, $u_{n+m+1}=\bar v$, let $\underline\phi_{k,j}=\lim_{w\to u_j-}\phi_k(w)$ and $S_j=\{l:v_l<u_j\}$.

Formalization targets

Goal: Theorem 1 (Finite-LP), corrected

Under Assumption 1 with breakpoint set $\mathcal B$, the constraint qualification and a common closing side (below), for every probability vector $x$

$$\mathrm{CR}(v,x)=\sup\Bigl\{r\ge0:\ \exists\lambda\ge0,\ \sum_k\underline\phi_{k,j}\lambda_{k,i}\le\sum_{l\in S_j}v_lx_l\ (j<i),\ r\,u_i+\sum_k\underline\phi_{k,j}\lambda_{k,i}\le\sum_{l\in S_j}v_lx_l\ (j\ge i)\Bigr\},$$

and $\sup_x\mathrm{CR}(v,x)$ equals the optimal value of the linear program (4).

Milestones, in proof order

1. Homogenization (proof of Proposition 1, p.ec6): $\inf_{F\in\mathcal F}\mathrm{Rev}(\pi,F)/(1-F(p-))$ equals a linear program over finite measures $H_p$ with $H_p([p,\bar v])=1$.
2. Per-price strong duality (p.ec7), under the constraint qualification.
3. Proposition 1 (p.10): $\mathrm{CR}(\pi)$ equals the value of the semi-infinite program (3), for every $\pi\in\Pi_n$ and as optimal values.
4. Constraint reduction (proof of Theorem 1, p.ec8), under the common closing side: only the constraints at $w\to u_j-$ matter.
5. $\lambda$-reduction (p.ec9): one multiplier column per grid cell gives (4).

Significance

Theorem 1 replaces a max-min problem over distributions and price densities with a linear program of $n+K(n+m+1)+1$ variables for each choice of price levels. The paper's Lemma 1 and Propositions 2–8 (optimal $n$-level mechanisms for support, mean and quantile sets) and its grid searches over price levels are all solutions of this program, so a machine-checked Theorem 1 is the common foundation for each of them.

The mission also states which hypotheses the reformulation needs. As printed, Theorem 1 and Proposition 1 are false (counterexamples below), and the platform already records the predecessor statements, WangMinimaxRegret.Reformulation.theorem_1 and its duality step eq_3_4, as Disproved. The corrected statements keep the program (4) and the paper's support, quantile, multi-segment and mean examples. Each correction is necessary (a counterexample satisfies every other hypothesis); their sufficiency is argued but not yet proved, which is part of what this mission asks for. No part of this paper has been formalized before; the homogenization step has a Proved analogue for moment sets (WangMinimaxRegret.Reformulation.eq_2_3).

Difficulty

The printed proof dualizes nature's problem at each price $p$ by Sion's minimax theorem. Neither side is compact: $H_p$ has unbounded mass and the multipliers are unbounded. The step fails for $K=1$, $0<c<\bar v$, $\phi(w)=\min(w-c,0)$, a single price $c$: here $\mathcal F=\mathcal P([c,\bar v])$ and $\mathrm{CR}=c/\bar v$, yet (3) and (4) have value $0$, because the constraints at $w\uparrow c$ force $r\,p\le0$. The same set written as $\phi=\mathbb 1[w\ge c]-1$ gives the correct $c/\bar v$. The program depends on how $\mathcal F$ is written, the competitive ratio does not. The correction is a constraint qualification: every $\phi_k$ is a step function, or some $F_0\in\mathcal F$ satisfies the non-step constraints strictly.

The reduction to left limits assumes that $\sum_k\lambda_k\phi_k$ attains its supremum on each cell at the cell's right end. With $\phi_1=\mathbb 1[w\le\omega]-1$, $\phi_2=\mathbb 1[w\ge\omega]-1$ and one price $v_1<\omega$, $\mathcal F=\{\delta_\omega\}$ and $\mathrm{CR}=v_1/\omega$, but (4) is unbounded: at $\omega$ the sum exceeds both of its one-sided limits. The correction is a common closing side: at each breakpoint all $\phi_k$ are left-continuous, or all are right-continuous.

A proof therefore needs a duality argument without compactness (a finite-dimensional reduction for step functions, a Slater-type argument otherwise), and limits at the grid points together with the closedness of finitely generated cones.

Formalization scope

Valuations, prices and the $\phi_k$ are real; laws are Borel probability measures on $\mathbb R$ that give no mass to the complement of $[0,\bar v]$, and each constraint of (2) carries integrability. The payment is the step function $t(w)=\sum_{v_l\le w}x_lv_l$, with the atom at $w$ included. All values (competitive ratio, the programs (3), (4) and the intermediate programs) lie in EReal, so an unbounded program has value $+\infty$. The competitive ratio ranges over the laws with $\mathrm{Rev}(\mathrm{OPT},F)>0$: a law with zero benchmark gives $0/0$. The merged grid is a hypothesis (a monotone vector whose values are $\mathcal V+\mathcal B$ as multisets, ties kept), indices are 0-based, and at a grid point $u_j=0$ the left limit is replaced by $\phi_k(0)$. The paper's "$0<b_1$, $b_m<\bar v$" is read as: no $\phi_k$ jumps at $0$ or $\bar v$. $K=0$, zero probabilities and tied prices are allowed; $\mathcal F$ is not assumed nonempty.

The theorems are statements of equality of values. A reading that compares only optimal values over $x$ would drop half of the goal; the goal states the per-mechanism equality as well. The verification files prove that the support example satisfies every hypothesis of the goal, that the indexing of (4) reproduces the ratio $c/\bar v$ of Proposition 2 for $n=1$, and that the second counterexample violates the closing-side condition.

Needed infrastructure: Lebesgue integration against finite measures, Mathlib's Function.leftLim, stdSimplex, and LP duality for finitely many constraints (closedness of finitely generated cones is Proved on the platform as ConvexCone.isClosed_finite_cone). The duality milestone, a strong-duality theorem for measure programs with piecewise monotone constraint functions under a constraint qualification, is reusable beyond this mission. Proofs of any milestone are welcome, as are counterexamples if a corrected statement turns out to be false.

Selected references

• S. Wang, The Power of Simple Menus in Robust Selling Mechanisms, arXiv:2310.17392v3, 2024; Management Science, 2025. https://arxiv.org/abs/2310.17392
• S. Wang, S. Liu, J. Zhang, Minimax Regret Robust Screening with Moment Information, Manufacturing & Service Operations Management 26(3), 2024. https://doi.org/10.1287/msom.2023.0072
• M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8(1), 1958. https://doi.org/10.2140/pjm.1958.8.171
• R. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58

Motivation

Data-driven decisions under uncertainty start from $S$ historical samples $\hat z_1,\dots,\hat z_S$ of a random outcome and a cost $f(x,z)$ of a decision $x$. Minimizing the sample average cost overfits: the decision performs worse out of sample than the sample average suggests. Two models hedge against this with the type-1 Wasserstein distance around the empirical distribution $\mathbb P^\dagger$.

Wasserstein distributionally robust optimization (DRO) fixes a radius $\theta$ and minimizes the worst expected cost over all distributions within distance $\theta$ of $\mathbb P^\dagger$ (Mohajerin Esfahani and Kuhn 2018; Gao and Kleywegt 2023). Robust satisficing (RS) fixes instead a cost target $\tau$ and minimizes the fragility $k$, the rate at which the expected cost may exceed $\tau$ per unit of Wasserstein distance (Long, Sim and Zhou 2023). DRO suits a cost-driven decision maker who can name a plausible radius; RS suits a goal-driven one who can name a target. Sim, Zhao and Zhou (2023) observed that the two produce the same solutions in linear regression with an unbounded support.

Wang, Ran, Zhou and He (Manufacturing & Service Operations Management, 2025; this mission follows the authors' manuscript) show that the two models trace the same family of optimal solutions in general convex problems, and give the map between the parameters. The direction RS → DRO, Theorem 1, is the goal of this mission.

Setting

Let $\mathcal X$ be a set of decisions in a real vector space, $\mathcal Z$ a support set, $\rho(z,z')\ge0$ a transport cost with $\rho(z,z)=0$, and $\hat z_1,\dots,\hat z_S\in\mathcal Z$ the samples. The worst-case loss of a decision $x$ and a multiplier $k\ge0$ is

$$h(x,k)=\frac1S\sum_{s\in[S]}\sup_{z\in\mathcal Z}\big\{f(x,z)-k\,\rho(z,\hat z_s)\big\}\in(-\infty,+\infty].$$

By Wasserstein duality the two models reformulate as follows (pp.7–8 of the paper).

• Problem (DRO) with radius $\theta\ge0$, written DRO($\theta$): minimize $\tau+k\theta$ over triples $(\tau,k,x)$ with $x\in\mathcal X$, $k\ge0$ and $h(x,k)\le\tau$.
• Problem (RS) with target $\tau$, written RS($\tau$): minimize $k$ over pairs $(x,k)$ with $x\in\mathcal X$, $k\ge0$ and $h(x,k)\le\tau$. Its optimal value is the RS value function $\kappa(\tau)\in[0,\infty]$ (written $k^*(\tau)$ in the appendix), which is $+\infty$ when RS($\tau$) is infeasible.

Three constants frame the targets. The empirical optimum is $Z_0=\inf_{x\in\mathcal X}\frac1S\sum_s f(x,\hat z_s)$. The robust optimum is $\bar\tau=\inf_{x\in\mathcal X}\sup_{z\in\mathcal Z}f(x,z)$. The largest transport radius is $\bar\theta=\frac1S\sum_s\sup_{z\in\mathcal Z}\rho(z,\hat z_s)$. The subdifferential $\partial\kappa(\tau)$ is the set of $\alpha$ with $\kappa(\tau)<\infty$ and $\kappa(\tau')\ge\kappa(\tau)+\alpha(\tau'-\tau)$ for all $\tau'$.

In Lean the data form DRORSEquiv.Model (fields X, Z, ρ, zhat, f), and the objects are worstCaseLoss, IsFeasible, IsRSOptimal, IsDROOptimal, rsValue ($\kappa$), empiricalOptimum ($Z_0$), tauBar, thetaBar and subdiff.

Formalization targets

Goal: Theorem 1 (corrected)

Assume $\mathcal X$ is convex, $f(\cdot,z)$ is convex on $\mathcal X$ for every $z\in\mathcal Z$, $\bar\tau$ is finite, and $Z_0\le\tau_{rs}\le\bar\tau$.

(a) If $\tau_{rs}<\bar\tau$, or $\tau_{rs}=\bar\tau$ and either $\bar\theta<\infty$ or $\kappa=\infty$ on $(-\infty,\tau_{rs})$, then

$$\exists\,\theta^*\ge0\ \ \forall\,(x^*,k^*)\text{ optimal for RS}(\tau_{rs}):\quad(\tau_{rs},k^*,x^*)\text{ is optimal for DRO}(\theta^*).$$

(b) For every optimal $(x^*,k^*)$ of RS($\tau_{rs}$) and every $\alpha\in\partial\kappa(\tau_{rs})$: if $\tau_{rs}<\bar\tau$ then $\alpha<0$; and if $\alpha<0$ then $(\tau_{rs},k^*,x^*)$ is optimal for DRO($-1/\alpha$).

The printed theorem is corrected in two places. At $\tau_{rs}=\bar\tau$ with $\bar\theta=\infty$ it fails ($f=1-1/(1+z)$ on $[0,\infty)$) unless $\bar\tau$ is the left end of $\operatorname{dom}\kappa$, where the radius $0$ works. The formula $\theta^*=-1/\alpha$ needs $\alpha<0$, because $0\in\partial\kappa(\bar\tau)$ can occur ($f=z$ on $[0,1]$). Each theorem item lists its differences from the source.

Milestones

The milestones follow the proof in Appendix A (pp.33–34): the boundary cases $\tau_{rs}=Z_0$ (radius $0$) and $\tau_{rs}=\bar\tau$ (radius $\theta\ge\bar\theta$); the rewriting of DRO($\theta$) as $\min_{\tau\ge Z_0}\tau+\theta\kappa(\tau)$; Lemma 1 ($\kappa$ convex, with $\mathcal X$ convex added); $\kappa$ nonincreasing; nonempty bounded $\partial\kappa$ on $\operatorname{int}(\operatorname{dom}\kappa)$; negativity of subgradients below $\bar\tau$ when RS($\tau_{rs}$) has an optimum; and the fact that a negative subgradient $\alpha$ makes $\tau_{rs}$ minimize $\tau+\kappa(\tau)(-1/\alpha)$.

Significance

Theorem 1 says that a decision maker who fixes a cost target loses nothing relative to one who fixes a Wasserstein radius: every RS solution is a DRO solution for the radius $-1/\alpha$, with $\alpha$ a subgradient of the RS value function. Together with the easy converse (Proposition 1), it lets results proved for one model transfer to the other: out-of-sample guarantees, tractable reformulations, and the choice of a parameter by cross-validation. The paper builds on it the equivalence for adaptive two-stage models (Theorem 2) and for the globalized models GDRC and GRS (Theorems 3–5).

The paper's result is proved on paper, but the proof leaves gaps that a formal proof has to close: the endpoint $\bar\tau$ needs $\bar\theta<\infty$; $0\notin\partial\kappa$ needs attainment of $\kappa$; Lemma 1 uses convexity of $\mathcal X$ without stating it; and the left end of $\operatorname{dom}\kappa$ (where the radius $0$ works) is not treated. No part of the result has a machine-checked proof yet. The convex-analysis milestones (convexity of a parametric value function in $[0,\infty]$, subgradients of an extended-valued convex function of one variable) are reusable for other value-function arguments.

Difficulty

The obvious argument is the paper's: make $\tau_{rs}$ a stationary point of $g(\tau)=\tau+\theta^*\kappa(\tau)$. It fails in three places. First, $\kappa$ is an infimum that need not be attained, so convexity (Lemma 1) needs an $\varepsilon$-argument in $[0,\infty]$, and the sign argument for subgradients fails without an optimal RS solution. Second, a subgradient exists only in the interior of $\operatorname{dom}\kappa$, which can start strictly above $Z_0$. At its left end no subgradient need exist, and the radius $\theta^*=0$ must be used instead. Third, at $\bar\tau$ the subgradient can be $0$, and the case needs a separate argument through $\bar\theta$, which works only when $\bar\theta$ is finite. Clause (b) is short, since a DRO-feasible $(\tau,k,x)$ has $k\ge\kappa(\tau)$. The case analysis behind clause (a) is the substance.

Formalization scope

The formalization works with the reformulated Problems (DRO) and (RS) themselves, not with the measure-level problems (1) and (2). The standing assumptions of p.7 (Polish $(\mathcal Z,\rho)$, $f(x,\cdot)\in L^1(\mathbb P^\dagger)$, bounded growth rate) are not used. The decision space is any real vector space, $\rho$ is any cost with $\rho\ge0$ and $\rho(z,z)=0$, the samples lie in $\mathcal Z$, and $S\ge1$; samples are indexed by Fin S. $h$, $Z_0$, $\bar\tau$, $\bar\theta$ are computed in EReal, and $\kappa$ in ℝ≥0∞. RS-optimality and DRO-optimality range over the full feasible sets, with $\tau$ ranging over all reals in DRO. The subdifferential is empty where $\kappa=\infty$. Each $-1/\alpha$ carries the hypothesis $\alpha<0$, since Lean's $-1/0=0$ would otherwise make the radius $0$ by default.

Clause (a) quantifies one radius over all optimal RS solutions ($\exists\theta^*$ before $\forall$). If RS($\tau_{rs}$) has no optimal solution, clause (a) holds for any radius, and this is the intended reading, since the theorem speaks of "the optimal solution". The measure-level Wasserstein objects already on the platform are not imported.

Contributions are welcome on any milestone. Lemma 1 and the subdifferential facts are independent of the DRO setting and are natural first targets.

Selected references

• Z. Wang, L. Ran, M. Zhou, L. He, On the Equivalence and Performance of Distributionally Robust Optimization and Robust Satisficing Models, Manufacturing & Service Operations Management, 2025 (authors' manuscript followed here). https://doi.org/10.1287/msom.2023.0531
• D. Z. Long, M. Sim, M. Zhou, Robust Satisficing, Operations Research 71(1):61–82, 2023. https://doi.org/10.1287/opre.2021.0238
• R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research 48(2), 2023. https://doi.org/10.1287/moor.2022.1275
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
• M. Sim, L. Zhao, M. Zhou, Tractable Robust Supervised Learning Models, SSRN 3981205, 2023. https://ssrn.com/abstract=3981205
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Why structured bandits

In a multi-armed bandit a learner repeatedly pulls one of finitely many arms and observes a random reward, trying to earn as much as an omniscient learner who knows the best arm. In many operations problems the arms are not unrelated: in dynamic pricing the probability of no sale is monotone in the price, in assortment or dosage problems mean rewards vary in a Lipschitz, linear or convex way across arms. Such structural information can make some arms cheap to rule out and others impossible to rule out without sampling them, and a learner that ignores it pays avoidable regret.

The asymptotic cost of learning under structure is known exactly. Graves and Lai (1997) showed that every uniformly good policy has regret at least $C(P)\log T$, where $C(P)$ is the value of a semi-infinite optimization problem over exploration rates; Combes, Magureanu and Proutière (2017) gave an algorithm (OSSB) attaining it by solving that problem in every round. Van Parys and Golrezaei (Management Science, 2024; preprint arXiv:2007.07302v3) proposed DUSA, which reaches the same bound while solving the convex dual of a relaxation of the problem, and only in rounds where a cheap one-dimensional test says that the collected information is insufficient. This mission formalizes their main regret guarantee.

The model

There are finitely many arms $X$ and a finite set $\mathfrak R\subset[0,\infty)$ of possible rewards. A reward distribution is a table $Q=(Q(r,x))$ in

$$\mathcal P_\Omega=\Big\{Q\ge0:\ \sum_{r\in\mathfrak R}Q(r,x)=1\ \forall x\in X\Big\}.$$

In round $t$ the learner pulls $x_t$ and receives $R_t(x_t)$, where the rewards $R_t(x)$ are independent across arms and rounds with law $P(\cdot,x)$. The true $P$ is unknown except that it lies in a known structure set $\mathcal P\subseteq\mathcal P_\Omega$, closed, convex and with non-empty interior (relative to the affine hull of $\mathcal P_\Omega$). Write $x^\star(P)$ for the set of optimal arms, $\mathrm{Rew}^\star(P)$ for the optimal mean, $\tilde X(P)$ for the suboptimal arms and $\Delta(x,P)$ for the gaps. The regret of a policy is $\mathrm{Reg}_\pi(T,P)=T\,\mathrm{Rew}^\star(P)-\sum_{t\le T}\mathbb E[\sum_r rP(r,x_t)]$.

A distribution $Q\in\mathcal P$ is deceitful for an arm $x'$ if it agrees with $P$ on the optimal arms but makes $x'$ better than them. With the information distance $I$ (the Kullback–Leibler divergence), $\mathrm{Dist}(\eta,x',P)=\inf_{Q\in\mathrm{Deceit}(x',P)}\sum_{x\in\tilde X(P)}\eta(x)I(P(x),Q(x))$, and the lower-bound constant is

$$C(P)=\inf_{\eta\ge0}\sum_{x\in\tilde X(P)}\eta(x)\Delta(x,P)\quad\text{s.t.}\quad\mathrm{Dist}(\eta,x,P)\ge1\ \ \forall x\in\tilde X(P).$$

Assumption 1 defines $\mathcal P'$: distributions in the interior of $\mathcal P$ with a unique optimal arm and no borderline suboptimal arm.

DUSA keeps a counter $s_t$ of exploration rounds, reference rates $\eta'_t$ and dual certificates $\mu_t$. In each round it checks, through a dual function $\mathrm{Dual}$, whether the counts $N_t/\log t$ already certify $\mathrm{Dist}\ge1+\epsilon$ for every empirically deceitful arm. If so, it exploits; otherwise it explores, calling a shallow update (a projection, Algorithm 2) and a deep update (a strongly convex program, Algorithm 3).

Formalization targets

Goal: Theorem 3

For $P\in\mathcal P'$ and $0<\epsilon<1/|X|$, every run of DUSA satisfies

$$\limsup_{T\to\infty}\frac{\mathrm{Reg}_\pi(T,P)}{\log T}\le(1+\epsilon)\Big(C(P)+\epsilon\big(1+\textstyle\sum_{x}\Delta(x,P)\big)\Big), \qquad \limsup_{T\to\infty}\frac{\mathbb E[s_T]}{\log T}\le(1+\epsilon)|X|^2\big(\|\eta'_\epsilon(P)\|_\infty+\epsilon\big).$$

Milestones

The milestones follow the proof in Appendix D:

1. Lemma 5 and Lemma 6, two concentration bounds (Hoeffding at a stopping time; the information distance of empirical distributions), stated for every non-anticipating policy.
2. Lemma 7, the finite regret of exploitation rounds with a badly estimated empirical optimum.
3. Lemma 1 (weak and strong duality between $\mathrm{Dual}$ and $\mathrm{Dist}$) and Lemma 8, which turns a passed test into the event (39).
4. Lemma 9, openness of the unique-optimum region and continuity of $\mathrm{Rew}_{\max}$ (corrected; see below).
5. Lemmas 10 and 11, deterministic counting facts about exploration rounds.
6. Propositions 4 and 5, existence and continuity of the deep update on $\mathcal P'$ and stability of the shallow update.

Significance

Clause (21) together with the Graves–Lai lower bound shows that DUSA is asymptotically optimal up to $\epsilon$ in every structured bandit of this class, which covers unstructured, Lipschitz, linear, convex, unimodal, dispersion and divergence structures. Clause (22) shows that the convex programs are solved only $O(\log T)$ times, which is the computational point of the algorithm. Lemma 6, a concentration inequality for $\sum_xN_t(x)I(P_t(x),P(x))$ for arbitrary discrete distributions, is of independent use in nonparametric bandits.

The result is proved in the paper. No part of it is machine-checked: the platform holds asymptotic optimality results for unstructured bandits (KL-UCB, Thompson sampling) but nothing for structured ones. A complete development would be the first formal proof of asymptotic optimality under structural information, and the duality and continuity milestones are reusable for other algorithms built on the Graves–Lai program.

Difficulty

The obvious approach, a per-arm regret decomposition with concentration of each arm's mean, does not reach $C(P)$: the lower bound couples the arms through $\mathrm{Dist}$, and the right exploration rate of one arm depends on the estimates of all of them. The proof needs (i) duality to relate the sufficient-information test to $\mathrm{Dist}$ at the empirical distribution, (ii) continuity of the deep update on $\mathcal P'$ and stability of the shallow update near $P$, so that targets computed from estimates converge to the target at $P$, and (iii) concentration of the information distance uniformly over random sample sizes. Each of these is a separate piece of analysis (convex duality with Slater's condition, parametric optimization, martingale concentration).

Formalization scope

Arms form a nonempty Fintype, rewards a Finset ℝ of nonnegative reals, and distributions are functions R → X → ℝ with the product topology. The paper's $\mathcal P$ is written S. Interior means the interior relative to the affine hull of $\mathcal P_\Omega$ (App. B). $I$, $\mathrm{Dist}$, $C$, $\mathrm{Rew}_{\max}$ and $\mathrm{Dual}$ take values in EReal, with $\inf\emptyset=+\infty$; the shallow update returns an Option (none is $+\infty$). The environment is an independent reward table with law $P$ plus an independent randomization seed. DUSA is a policy built from a DusaRules structure: the order of the initial pulls, the initial values, each tie-break and the deep update's fallback are free fields, and every theorem holds for all of them. $\limsup a_T/\log T\le b$ is stated as "for every real $c>b$, eventually $a_T\le c\log T$".

Three deviations are declared in the items. Assumption 1(2) is printed for all arms and is then never satisfied, so it is read over suboptimal arms; under the literal reading $\mathcal P'$ is empty and the goal would be vacuous. Lemma 9(ii) is false as printed when $P$ has two optimal arms and is stated for $P$ with a unique optimal arm, the case the proof treats. Lemma 7's proof bounds each gap by one, and as printed the lemma fails for large rewards (two Bernoulli-type arms with rewards $\{0,M\}$, $M>2000$), so its bound is multiplied by $\max(1,\max_x\Delta(x,P))$, which is the printed bound whenever every gap is at most one.

The development needs finite-dimensional convex duality, parametric continuity of strongly convex programs, and martingale concentration for empirical distributions of a non-anticipating policy. Contributions to any milestone, and general lemmas on these three topics, are welcome.

Selected references

• B. Van Parys, N. Golrezaei, Optimal Learning for Structured Bandits, Management Science, 2024; preprint arXiv:2007.07302v3, 2023. https://arxiv.org/abs/2007.07302
• T. L. Graves, T. L. Lai, Asymptotically efficient adaptive choice of control laws in controlled Markov chains, SIAM Journal on Control and Optimization 35(3):715–743, 1997.
• R. Combes, S. Magureanu, A. Proutière, Minimal Exploration in Structured Stochastic Bandits, NeurIPS 2017. https://arxiv.org/abs/1711.00400
• S. Magureanu, R. Combes, A. Proutière, Lipschitz Bandits: Regret Lower Bounds and Optimal Algorithms, COLT 2014, PMLR 35:975–999. https://proceedings.mlr.press/v35/magureanu14.html

Selling a ranked list of products

Online retailers show products in a fixed order, and a customer reads the list from the top. Models of this behavior, the cascade click model, come from sponsored search (Craswell et al., 2008; Aggarwal et al., 2008) and now drive assortment and ranking decisions. Najafi, Duenyas, Jasin and Uichanco combine it with the classical problem of pricing a limited inventory over a finite horizon (Gallego and van Ryzin, 1994, 1997). They ask whether a simple, re-optimization-free policy can price a whole ranked list with a loss that grows only logarithmically in the scale of the problem. Earlier work reached logarithmic loss by a linear correction of the rates, for models whose deterministic problem is convex (Jasin, 2014). In the cascade model it is not convex.

Setting

There are $J$ products in a fixed order, and $T$ periods. In each period a customer arrives with probability $\lambda$. She examines product $1$; at product $j$ she buys with the conditional purchase rate $\alpha_j\in[0,u]$, set through the price $p_j(\alpha_j)$, and otherwise continues with probability $\zeta_j$. The arrival rate at $j$ and the expected purchase rate are

$$\sigma_j(a)=\lambda\prod_{i<j}(1-a_i)\zeta_i,\qquad v_j(a)=\sigma_j(a)a_j .$$

Let $r_j(\alpha)=\alpha p_j(\alpha)$, the revenue rate, strictly concave with $|r_j''|\le w$. The deterministic problem DET maximizes $\sum_t\sum_j\sigma_j(\alpha_t)r_j(\alpha_{tj})$ over schedules with $\sum_t\sigma_j(\alpha_t)\alpha_{tj}\le y_j$, and its value is $V^D$. It has a stationary optimal solution $a^D$ under mild conditions.

The Cascade Correction (CC) policy starts from $v^D=v(a^D)$. In period $t$ it sets

$$\hat v_t=v^D-\delta^v_t,\qquad \delta^v_t=\sum_{s<t}\frac{\Delta_s}{T-s},\qquad \hat\sigma_{t,1}=\lambda,\quad \hat\sigma_{t,j+1}=\zeta_j(\hat\sigma_{tj}-\hat v_{tj}),$$

where $\Delta_s$ is the demand error of period $s$, and it applies $\hat\alpha_{tj}=\hat v_{tj}/\hat\sigma_{tj}$ when the product is in stock and this rate is admissible, and the turn-off price otherwise.

In the asymptotic regime, horizon and inventory are scaled to $N=kT$ and $Y=ky$, the values are $V^{k,D}$ for DET and $V^{k,CC}$ for the policy.

Formalization targets

Goal: the logarithmic loss (Theorem 3, p.25)

If $a^D\in[L,U]^J$ for some $0<L<U<1$ and $|r_j'|$ is bounded on $[L,U]$, then there is $\Psi_2>0$ independent of $k\ge1$ with

$$V^{k,D}-V^{k,CC}\le\Psi_2(1+\log k).$$

The constant may depend on the instance, on $(T,y)$ and on $a^D$. It is quantified before $k$.

Stationarity of DET

Lemma EC.1, Claim EC.2, the domination of every schedule by a stationary one, Lemma 4 and Lemma 5 ($a^D_j<u$), and the scaling $V^{k,D}=kV^D=kT\tilde V^D$.

The analysis of the policy

The expansion (17), the bound $\|\delta^\sigma\|_\infty\le Q\|\delta^v\|_\infty$, Lemma EC.2 (below a threshold the policy follows its ideal path), $\sum_t\mathbf E[(\delta^v_{tj})^2]=O(\log k)$, Lemma EC.3 ($\mathbf E[k-\tau^k]\le1+\Psi\log k$), Observation 1, the decomposition $\mathbf E[R^{k,CC}(1,\tau^k-1)]=\Phi_1+\Phi_2$, Observation 6, and $\Phi_2\ge-O(\log k)$.

Significance

Theorem 3 says that a policy which solves DET once, and only a triangular linear system in every period, loses $O(\log k)$ against an upper-bound benchmark. In particular the relative loss is $O(\log k/k)$. The paper's other guarantee, for the fixed-price policy, is $O(\sqrt k)$. The correction acts on the expected purchase rates and recovers conditional rates as a ratio of two corrected terms, and this is the idea that makes a linear correction work without convexity.

The result is proved on paper but has no machine-checked proof, and the formalization adds more than a check. The published proof needs repair at several points, each of which leaves the $O(\log k)$ intact: the reduction to binding constraints is not valid, the threshold conditions fail at $\lambda=1$, Observation 1 claims an equality that is false, and Observation 2 uses an orthogonality that is false. Lemma 4 needs continuity of $r_j$ at $0$, and Lemma 5 needs $\lambda>0$. The items state the repaired results and record each repair. The mission also adds to the platform a finite path-law treatment of an adaptive pricing policy.

Difficulty

DET is not concave in the rates: the objective mixes the rates of different products through $\sigma_j$. So the Jensen argument that gives stationarity in standard revenue management does not apply to the rates, and the argument has to go through the value function in the arrival rates and inventories.

For the policy, the natural idea is the linear correction of conditional rates, and it fails to apply: the demand errors are errors in $v$, and $a=v/\sigma$ is a ratio of two random quantities. The applied rate is then nonlinear in the correction. A second-order expansion of the revenue gives linear terms in the correction summed up to a random time. These do not vanish, since a sum of martingale terms up to $\tau$ is not a stopped martingale. They have to be estimated against the tail of $\tau$.

Formalization scope

Rates are the actions: rates lie in $[0,u]$, covering $\Omega_\alpha=[0,u]$ and $(0,u]$, and rate $0$ is the turn-off price, with revenue $0$. Concavity is assumed on $(0,u]$ only. A period's outcome is a sold product or no sale, so the law of a policy is an explicit finite sum over outcome paths, with no measure theory in any statement; the general path law is its own definition. A policy maps the list of past outcomes to rates. The state of CC is a fold over the history, with natural-number inventories. Periods and products are 0-based in Lean. Scaling uses a real $k\ge1$ with $kT$ and $ky_j$ integers; the inventory $y$ is real.

$V^{k,D}$ in the goal is the supremum of DET for the scaled problem, not a formula in $a^D$, and $V^{k,CC}$ is the realized revenue under the policy's own law, not a quantity at the ideal rates or a stopped sum. The verification files prove that the suprema are true suprema, that the path law is a probability, and that the hypotheses of the goal are jointly satisfiable on a worked instance, with $V^{2,D}=1/2$ and $V^{2,CC}=1/4$. So the goal is not vacuous, and the correction is not trivial.

A complete development needs: the concavity of $R^D$ by induction on products; a Jensen argument for the domination; a compactness argument for Lemma 4; orthogonality of martingale differences and Doob's maximal inequality, for the finite path law (the platform has both on filtered measure spaces); and a stopped-sum estimate for Observation 1. The finite-path martingale lemmas are reusable beyond this mission. Contributions that prove them in general form are welcome, and so are proofs that avoid the printed reduction to binding constraints, as the items already do.

Theorem 1 ($V^*\le V^D$), the fixed-price bound of Theorem 2, and the structural Lemmas 1–3 are not part of this mission.

Selected references

• S. Najafi, I. Duenyas, S. Jasin, J. Uichanco, Multi-product Dynamic Pricing with Limited Inventories under a Cascade Click Model, SSRN abstract_id=3362921 (2023); Manufacturing & Service Operations Management (2023). https://ssrn.com/abstract=3362921, https://doi.org/10.1287/msom.2021.0504
• 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
• G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1) (1997). https://doi.org/10.1287/opre.45.1.24
• S. Jasin, Reoptimization and Self-Adjusting Price Control for Network Revenue Management, Operations Research 62(5) (2014). https://doi.org/10.1287/opre.2014.1294
• N. Craswell, O. Zoeter, M. Taylor, B. Ramsey, An Experimental Comparison of Click Position-Bias Models, WSDM (2008). https://doi.org/10.1145/1341531.1341545
• G. Aggarwal, J. Feldman, S. Muthukrishnan, M. Pál, Sponsored Search Auctions with Markovian Users, WINE (2008). https://doi.org/10.1007/978-3-540-92185-1_48