All missions

Motivation

In a budget-feasible procurement auction an auctioneer with a budget $B$ buys services from strategic sellers. Each seller knows privately what providing the service costs, and the auctioneer wants a set of services of maximum value without paying more than $B$ in total. The model was introduced by Singer (FOCS 2010) and is used to study crowdsourcing, data acquisition from individuals, and influence maximization in networks, where the value of a set of sellers typically shows diminishing returns: it is submodular.

Most of the mechanisms known for this problem are randomized, or are deterministic only when the auctioneer's valuation is monotone, i.e. adding a seller never lowers the value. Amanatidis, Kleer and Schäfer named the existence of deterministic budget-feasible constant-factor mechanisms for submodular valuations the most intriguing open problem of the area. Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239, Operations Research 2025) give deterministic clock auctions for these settings. In a clock auction each bidder only ever sees a sequence of decreasing take-it-or-leave-it prices, which makes truthful behaviour obvious to the bidders. This mission covers §4 of that paper: the first deterministic budget-feasible mechanism with a constant approximation ratio for general, not necessarily monotone, submodular valuations.

Timeline. Singer (2010) gave the first budget-feasible mechanisms for monotone submodular valuations. Chen, Gravin and Lu (SODA 2011) improved the constants. Amanatidis, Kleer and Schäfer (EC 2019) gave a randomized 505-approximate mechanism for non-monotone submodular valuations and introduced the idea of building two disjoint tentative sets simultaneously. Balkanski et al. (2021) give a deterministic clock auction for this class with approximation ratio 64.

Setting

There are $n$ bidders $N = \{0, \dots, n-1\}$. Bidder $i$ has a private cost $c_i \ge 0$, the least payment it accepts. The auctioneer has a budget $B > 0$ and a valuation $v : 2^N \to \mathbb{R}_{\ge 0}$ that is submodular: $v(S) + v(T) \ge v(S \cap T) + v(S \cup T)$ for all $S, T \subseteq N$. The marginal contribution of $T$ to $S$ is $v(T \mid S) = v(S \cup T) - v(S)$. A set $O$ is budget feasible if $\sum_{i \in O} c_i \le B$, and $OPT$ is the largest value of a budget-feasible set.

Simultaneous-Iterative-Pruning (Mechanism 3) works in phases with a target $\widetilde{OPT}_t$ that starts at $\max_i v(\{i\})$ and doubles in each phase. In phase $t$ it grows two disjoint tentative sets $S^1_t$ and $S^2_t$. At each step it picks a bidder $i$ and an index $k \in \{1,2\}$ maximizing $v(\{i\} \mid S^k_t)$, offers the price $p_i \leftarrow \min\{p_i,\ v(\{i\} \mid S^k_t)\cdot B/\widetilde{OPT}_t\}$, and adds $i$ to $S^k_t$ if it accepts. A bidder who rejects leaves the auction for good. A phase ends when one of the two sets reaches the target or no bidder remains to be offered a price. The two sets of the previous phase are set aside during a phase. After the last phase $\hat t$, an unconstrained submodular maximization subroutine $\mathrm{USM}$ is applied to the four sets of the last two phases, giving $T^k_j = \mathrm{USM}(S^k_j)$. The mechanism returns the best of the six sets $S^1_{\hat t-1}, S^2_{\hat t-1}, T^1_{\hat t}, T^2_{\hat t}, T^1_{\hat t-1}, T^2_{\hat t-1}$, minus its last added bidder if the prices of its bidders exceed $B$. The subroutine is required to be a 2-approximation: $\mathrm{USM}(X) \subseteq X$ and $2\,v(\mathrm{USM}(X)) \ge v(Y)$ for all $Y \subseteq X$.

Formalization targets

Goal: Theorem 5 (p. 12)

For every non-negative submodular $v$, costs $c \ge 0$, budget $B > 0$ and 2-approximate subroutine $\mathrm{USM}$, the set $S$ and prices $p$ returned by Simultaneous-Iterative-Pruning satisfy

$$\sum_{i \in S} p_i \le B \qquad\text{and}\qquad v(O) \le 64\, v(S) \ \text{ for every budget-feasible } O.$$

Milestones

• Lemma 6 (p. 12): the bidders of a budget-feasible $O$ rejected in phase $t \le \hat t$ have value $v(O^-_t) \le 6\,\widetilde{OPT}_t$. The page prints "$\ge$", a typo the proof corrects.
• Corollary 1 (p. 13): the bidders of $O$ still active at the end of phase $t$ have value $v(O^+_t) \ge v(O) - 12\,\widetilde{OPT}_t$.
• Lemma 7 (p. 13): one of the six candidates has value at least $v(O)/32$.
• Budget feasibility (p. 12): $\sum_{i \in S} p_i \le B$.
• Pruning step (p. 14): $v(S)$ is at least half the value of every candidate.

Significance

Theorem 5 shows that, for budget-feasible procurement with submodular valuations, determinism costs only a constant factor even without monotonicity. Before this paper no deterministic mechanism, polynomial-time or not, achieved a constant ratio for non-monotone submodular valuations. The mechanism is also a clock auction, whose interface to the bidders is a sequence of decreasing prices. The constant 64 is not claimed to be tight, and better constants are open.

No part of this paper is formalized anywhere that we know of. A machine-checked proof would verify an argument whose bookkeeping is easy to get wrong: two simultaneous tentative sets, sets of the previous phase put aside and later returned to the pool, prices that are lowered across phases, and a pruning step whose case analysis depends on the phase a candidate comes from. The formalization already surfaced two issues in the printed text. Lemma 6 states the wrong inequality. And for $n = 1$ it needs $v(\emptyset) = 0$, a normalization the paper never assumes.

Difficulty

The approach of the monotone case does not carry over. There, the value of the active optimal bidders is bounded by the value of all active bidders, and that fails once adding a bidder can lower the value. The proof therefore has to account separately for the optimal bidders the auction rejects (Lemma 6, which uses both tentative sets of a phase to absorb the rejected bidders) and for those it keeps, whose value is recovered only through the unconstrained maximization step applied to the four tentative sets of the last two phases (Lemma 7). Budget feasibility needs the fact that every accepted bidder's marginal contribution was non-negative when it was added. Otherwise its offered price would have been negative and it would have rejected. The final pruning step must not lose more than half the value. This holds because a removed bidder's marginal contribution is at most the initial target, while the best candidate exceeds twice that whenever a removal happens.

Formalization scope

Bidders are Fin n and sets of bidders are Finset (Fin n). The tentative sets are lists in insertion order, so that "the last bidder added" is defined; the candidate $T^k_j$ is the sublist of $S^k_j$ of the bidders that lie in $\mathrm{USM}(S^k_j)$. Valuations, costs and prices are real. The model's standing assumptions appear as hypotheses: $v \ge 0$, $v$ submodular (the published definition NonmonotoneSubmod.Shared.Submodular), and $c_i \ge 0$. A bidder offered the price $x$ accepts iff $c_i \le x$. Every argmax breaks ties by the least bidder index (in line 5, least bidder first, then $k = 1$ before $k = 2$; in line 12, the first maximizer in the printed order). The paper fixes no tie rule, and its claims hold for any.

Added hypotheses: $B > 0$ everywhere (the paper says only "a budget $B$"), and, in Lemma 6 only, "$n \ge 2$ or $v(\emptyset) = 0$", which excludes the one-bidder instances where the printed lemma fails. The theorems quantify over every subroutine $\mathrm{USM}$ with the 2-approximation guarantee. The paper's example of such a subroutine (Buchbinder et al.) is randomized, and a deterministic 2-approximation exists (Buchbinder and Feldman 2018). The phase loop runs with fuel $n + 2$. For non-negative submodular $v$ this is enough unless $\max_i v(\{i\}) = 0$, in which case $v \equiv 0$ and every statement is trivial.

Out of scope: running time (Lemma 12 and the "polynomial-time" clause) and the incentive properties. The clock-auction property is built into the definition, as every price update is a minimum with the old price. A Lean function is deterministic.

The goal cannot be satisfied trivially. It is stated about the mechanism's actual output for every non-negative submodular $v$ and every admissible subroutine, and the approximation compares $v(S)$ with every budget-feasible set rather than a supremum. Requiring $\mathrm{USM}$ to be an exact maximizer would weaken the theorem and is not done. Contributions of general lemmas on submodular functions (subadditivity of non-negative submodular functions, telescoping marginal sums along a list) are reusable well beyond this mission.

Selected references

• E. Balkanski, P. Garimidi, V. Gkatzelis, D. Schoepflin, X. Tan, Deterministic Budget-Feasible Clock Auctions, arXiv:2107.09239v2, 2021; Operations Research, 2025. https://arxiv.org/abs/2107.09239
• Y. Singer, Budget Feasible Mechanisms, FOCS 2010. https://doi.org/10.1109/FOCS.2010.78
• N. Chen, N. Gravin, P. Lu, On the Approximability of Budget Feasible Mechanisms, SODA 2011. https://arxiv.org/abs/1007.3801
• G. Amanatidis, P. Kleer, G. Schäfer, Budget-Feasible Mechanism Design for Non-Monotone Submodular Objectives: Offline and Online, EC 2019; Mathematics of Operations Research 47(3), 2022. https://arxiv.org/abs/1905.00848
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5), 2015. https://doi.org/10.1137/130929205
• N. Buchbinder, M. Feldman, Deterministic Algorithms for Submodular Maximization Problems, ACM Trans. Algorithms 14(3), 2018. https://doi.org/10.1145/3184990

Motivation

A portfolio manager who observes side information, the covariate $X$ (a market state, a set of signals), wants to choose a portfolio for the asset returns $Y$ given the current value $x_0$ of that covariate. Estimating the conditional law of $Y$ given $X=x_0$ from $N$ joint samples is fragile: typically no sample has $\hat x_i=x_0$ exactly, and a nearest-neighbour or kernel estimate inherits all the noise of the few samples near $x_0$. Nguyen, Zhang, Wang, Blanchet, Delage and Ye robustify this decision with optimal transport: they let an adversary perturb the empirical joint distribution within a transport budget and evaluate the portfolio by its worst conditional expected loss over the perturbed distributions. This mission formalizes their main reformulation result for the general case, a fiber of positive radius with a positive mass requirement.

Setting

Let $\mathcal X$ and $\mathcal Y$ be Polish spaces. The data are $N\ge1$ samples $(\hat x_i,\hat y_i)\in\mathcal X\times\mathcal Y$, $i\in[N]$, with empirical distribution $\hat{\mathbb P}=N^{-1}\sum_i\delta_{(\hat x_i,\hat y_i)}$. Ground costs $\mathbb D_{\mathcal X}$ and $\mathbb D_{\mathcal Y}$ give the joint cost $\mathbb D((x,y),(x',y'))=\mathbb D_{\mathcal X}(x,x')+\mathbb D_{\mathcal Y}(y,y')$, and the optimal transport cost $\mathbb W(\mathbb Q,\hat{\mathbb P})$ is the least expected cost $\mathbb E_\pi[\mathbb D]$ over couplings $\pi$ of $\mathbb Q$ and $\hat{\mathbb P}$. The ambiguity set is the ball

$$\mathbb B_\rho=\{\mathbb Q\in\mathcal M(\mathcal X\times\mathcal Y):\mathbb W(\mathbb Q,\hat{\mathbb P})\le\rho\}.$$

The neighbourhood of the observed covariate is $\mathcal N_\gamma(x_0)=\{x:\mathbb D_{\mathcal X}(x,x_0)\le\gamma\}$, and $\mathcal N_\gamma(x_0)\times\mathcal Y$ is the fiber set. For a fixed portfolio the loss is a function $\ell:\mathcal Y\to\mathbb R$, and the quantity of interest is the worst-case conditional expected loss

$$\sup\Big\{\mathbb E_{\mathbb Q}[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)]:\ \mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X\in\mathcal N_\gamma(x_0))\ge\varepsilon\Big\},$$

where $\varepsilon>0$ is a minimum mass the adversary must leave on the fiber, so that the conditional expectation is well defined.

Three more data enter the result. The minimum radius $\rho_{\min}(x_0,\gamma,\varepsilon)$ is the least $\mathbb W(\mathbb Q,\hat{\mathbb P})$ over $\mathbb Q$ with fiber mass at least $\varepsilon$. The index sets are $\mathcal I_1=\{i:\hat x_i\in\mathcal N_\gamma(x_0)\}$ and $\mathcal I_2=[N]\setminus\mathcal I_1$. The boundary distances are $d_i=\inf_{x\in\partial\mathcal N_\gamma(x_0)}\mathbb D_{\mathcal X}(x,\hat x_i)$. The dual set $\mathcal V$ (display (16)) consists of the tuples $(\lambda,s,\nu^+,\nu^-,\phi,\varphi,\psi)$ with $\lambda,\psi\in\mathbb R^N_+$, $s\in\mathbb R^N$, $\nu^\pm,\varphi\ge0$, $\phi\in\mathbb R$, subject to

$$\phi-d_i\varphi+\psi_i-s_i\ge0\ (i\in\mathcal I_1),\quad \phi+d_i\varphi+\psi_i-s_i\ge0\ (i\in\mathcal I_2),\quad \nu^+-\nu^-+\Big(\sum_{i\in\mathcal I_1}d_i-N\rho\Big)\varphi-\sum_i\psi_i\ge0,\quad \varphi\ge\lambda_i.$$

Formalization targets

Goal: Theorem 4.4

For $\gamma>0$, $\varepsilon>0$ and $\rho>\rho_{\min}(x_0,\gamma,\varepsilon)$,

$$\sup_{\substack{\mathbb Q\in\mathbb B_\rho\\ \mathbb Q(X\in\mathcal N_\gamma(x_0))\ge\varepsilon}}\mathbb E_{\mathbb Q}[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)]=\inf\Big\{\phi+\frac{\nu^+}{N\varepsilon}-\frac{\nu^-}{N}:\ (\lambda,s,\nu^+,\nu^-,\phi,\varphi,\psi)\in\mathcal V,\ s_i\ge\sup_{y\in\mathcal Y}\{\ell(y)-\lambda_i\mathbb D_{\mathcal Y}(y,\hat y_i)\}\ \forall i\Big\}.$$

Milestones

1. Representation (24) of $\mathbb B_\rho$ as the set of averages $N^{-1}\sum_i\pi_i$ of probability measures with $N^{-1}\sum_i\mathbb E_{\pi_i}[\mathbb D(\cdot,(\hat x_i,\hat y_i))]\le\rho$.
2. Proposition 2.5: $\rho_{\min}$ is the value of a fractional knapsack linear program, and a feasible $\mathbb Q$ exists iff $\rho\ge\rho_{\min}$.
3. Reduction (proof of Theorem 4.4, pp. 48–49): the worst case equals a supremum over weights $p_i\in[0,1]$ and laws $\mu_0^i$ on $\mathcal Y$ of $\sum_ip_i\mathbb E_{\mu_0^i}[\ell]/\sum_ip_i$, under a transport budget and $\sum_ip_i\ge N\varepsilon$.
4. Conic duality (p. 50) for one sample: $\sup\{\mathbb E_{\mu}[\upsilon\ell]:\mathbb E_\mu[\upsilon\mathbb D_{\mathcal Y}(\cdot,\hat y)]\le\theta\}=\inf_{\lambda\ge0}\theta\lambda+\upsilon\sup_y\{\ell(y)-\lambda\mathbb D_{\mathcal Y}(y,\hat y)\}$ for $\theta>0$.
5. LP duality (29) (pp. 50–51): the supremum of $\sum_i\theta_i\lambda_i+\upsilon_is_i$ over the Charnes–Cooper variables $(\upsilon,t)$ and the budgets $\theta$ equals the infimum of $\phi+(N\varepsilon)^{-1}\nu^+-N^{-1}\nu^-$ over $\mathcal V$.

Significance

The theorem turns an infinite-dimensional problem, a supremum over probability measures on $\mathcal X\times\mathcal Y$ of a ratio of integrals, into a program in $O(N)$ real variables whose only infinite part is the per-sample supremum $\sup_y\{\ell(y)-\lambda_i\mathbb D_{\mathcal Y}(y,\hat y_i)\}$. For the losses used in portfolio selection (mean–variance, CVaR) this supremum has a closed form or a conic representation, and the outer minimization over portfolios becomes a single convex program; this is how the paper computes its conditional robust portfolios. It is the most general of the paper's four cases (Figure 1, p. 12); the companion missions of this series treat a singleton fiber ($\gamma=0$) and a zero mass requirement ($\varepsilon=0$).

The result is proved in the paper, not formalized anywhere. A machine-checked version requires, and would leave behind, an optimal-transport representation of Wasserstein balls around empirical measures, a Dirac-nominal conic duality for moment problems, and finite-dimensional linear programming duality, none of which is in Mathlib.

Difficulty

The conditional expectation is a ratio, so the problem is not a linear program in $\mathbb Q$ and the standard Wasserstein DRO duality does not apply directly. Passing to finitely many sample weights requires that leaving the fiber from a sample inside it costs exactly $d_i$, which depends on the geometry of the neighbourhood and not only on Assumption 2.4. The two duality steps are of different kinds: an infinite-dimensional one over laws on $\mathcal Y$, where the loss is only measurable, and a finite-dimensional linear program whose strong duality must be certified from $\rho>\rho_{\min}$. The representation of the ball needs an optimal coupling, which is an existence theorem on Polish spaces.

Formalization scope

• $\mathcal X$, $\mathcal Y$ are Polish Borel spaces; $[N]$ is Fin N with $N\ge1$; samples may repeat.
• $\mathbb W$ is the published RWPI.SqrtLasso.transportCost, an infimum over couplings of a lower integral of the $[0,\infty]$-valued cost; the ball compares it with ENNReal.ofReal ρ.
• Expectations of the loss are the published ModelRiskOT.Duality.extIntegral, $\int\ell^+-\int\ell^-$ in the extended reals. Both sides of the goal are extended reals; the infimum over an empty set is $+\infty$.
• The loss is an arbitrary measurable $L:\mathcal Y\to\mathbb R$, standing for $\ell(\cdot,\alpha,\beta)$ at any fixed feasible $(\alpha,\beta)$; no boundedness or continuity is assumed.
• Assumption 2.4 (separable, symmetric, nonnegative, continuous costs; unique projections onto $\mathcal N_\gamma(x_0)$; vicinity of boundary points) is a hypothesis of every statement. $\partial$ is the topological frontier in $\mathcal X$; $\kappa_i$ and $d_i$ are real infima.
• Added hypotheses. A boundary-regularity predicate: $\partial\mathcal N_\gamma(x_0)\ne\emptyset$, $d_i$ is the greatest lower bound of $\mathbb D_{\mathcal X}(x,\hat x_i)$ over $x\notin\mathcal N_\gamma(x_0)$ for $i\in\mathcal I_1$, and $d_i=\kappa_i$ for $i\in\mathcal I_2$. The proof uses both facts, and neither follows from Assumption 2.4 for a general continuous cost; both hold when $\mathbb D_{\mathcal X}$ is a norm distance. Measurability of $L$. In the conic duality milestone, $\theta>0$.
• Ruled out. The conditional expectation is never evaluated at a $\mathbb Q$ with zero fiber mass (the supremum ranges only over $\mathbb Q$ with mass at least $\varepsilon>0$); no Bochner integral of a possibly non-integrable loss appears; $\rho\ge0$ follows from $\rho>\rho_{\min}$, so ofReal never collapses a negative radius; and the supremum ranges exactly over $\mathbb B_\rho$ intersected with the mass constraint, not over all measures.
• Welcome contributions: existence of optimal couplings on Polish spaces, the decomposition of couplings with a finitely supported marginal, a Dirac-nominal moment duality, and LP strong duality in the form needed for (29). These are reusable well beyond this paper.

Selected references

• V. A. Nguyen, F. Zhang, S. Wang, J. Blanchet, E. Delage, Y. Ye, Robustifying conditional portfolio decisions via optimal transport, arXiv:2103.16451v3, 2024; Operations Research, 2025. https://arxiv.org/abs/2103.16451
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44(2), 2019. https://arxiv.org/abs/1604.01446
• C. Villani, Optimal Transport: Old and New, Springer, 2009 (Theorem 4.1, existence of optimal couplings). https://doi.org/10.1007/978-3-540-71050-9
• A. Charnes, W. W. Cooper, Programming with linear fractional functionals, Naval Research Logistics Quarterly 9, 1962. https://doi.org/10.1002/nav.3800090303
• M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8(1), 1958. https://doi.org/10.2140/pjm.1958.8.171

Motivation

A portfolio manager who observes side information, such as a vector of market covariates $x_0$ today, wants a decision that performs well conditionally on that information: the relevant risk is the expected loss of the portfolio given that the covariate equals, or is close to, $x_0$. Estimating this conditional loss from $N$ historical pairs $(\hat x_i,\hat y_i)$ of covariates and returns is fragile, since few or no samples may lie near $x_0$. Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451, Operations Research 2025) robustify the conditional decision with an optimal-transport ambiguity set: the worst case of the conditional expected loss is taken over all distributions within transport budget $\rho$ of the empirical distribution.

Conditioning makes this worst case delicate. The adversary may move mass away from the conditioning set, and a conditional expectation on a set of probability zero is undefined. Section 4.1 of the paper treats a neighbourhood of positive radius $\gamma$ around $x_0$ and requires only that the conditioning set have positive probability. This mission formalizes the result showing that, when the budget is below an explicit threshold $\rho_{\max}$, the requirement "positive probability" is automatically "probability at least $\underline\varepsilon$", with $\underline\varepsilon>0$ the value of a small linear program.

Setting

Let $\mathcal X$ and $\mathcal Y$ be Polish spaces carrying their Borel $\sigma$-algebras, with ground costs $\mathbb D_{\mathcal X}$ and $\mathbb D_{\mathcal Y}$ and the separable joint cost $\mathbb D((x,y),(x',y'))=\mathbb D_{\mathcal X}(x,x')+\mathbb D_{\mathcal Y}(y,y')$. The data are $N\ge1$ samples $(\hat x_i,\hat y_i)$, $i\in[N]$, and the empirical distribution is $\widehat{\mathbb P}=N^{-1}\sum_i\delta_{(\hat x_i,\hat y_i)}$.

The optimal transport cost $\mathbb W(\mathbb Q,\widehat{\mathbb P})$ is the infimum of $\mathbb E_\pi[\mathbb D]$ over couplings $\pi$ of $\mathbb Q$ and $\widehat{\mathbb P}$, and the ambiguity set is the ball $\mathbb B_\rho=\{\mathbb Q:\mathbb W(\mathbb Q,\widehat{\mathbb P})\le\rho\}$ of probability measures on $\mathcal X\times\mathcal Y$.

The covariate neighbourhood is $\mathcal N_\gamma(x_0)=\{x:\mathbb D_{\mathcal X}(x,x_0)\le\gamma\}$, and $\mathcal N_\gamma(x_0)\times\mathcal Y$ is the fiber set. For a loss $\ell:\mathcal Y\to\mathbb R$ (the loss $y\mapsto\ell(y,\alpha,\beta)$ of a fixed portfolio decision), the worst-case conditional loss under a mass requirement is

$$\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X\in\mathcal N_\gamma(x_0))\ \ge\ \varepsilon}\ \mathbb E_{\mathbb Q}\big[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)\big],$$

and problem (12) replaces "$\ge\varepsilon$" by "$>0$".

Two derived quantities organize §4.1. The maximal budget $\rho_{\max}(x_0,\gamma)$ is the least transport cost of a distribution that puts no mass on the fiber. Write $\mathcal I_1=\{i:\hat x_i\in\mathcal N_\gamma(x_0)\}$ and $\mathcal I_2$ for its complement, and let $d_i$ be the cost from $\hat x_i$ to the boundary $\partial\mathcal N_\gamma(x_0)$. Assumption 2.4 asks that the costs be symmetric, non-negative and continuous, with $\mathbb D=0$ exactly on the diagonal, that each $\hat x_i$ have a unique projection onto $\mathcal N_\gamma(x_0)$, and that every boundary point be approached from outside the neighbourhood.

Formalization targets

Goal: Proposition 4.3 (p. 19)

For $\gamma>0$ and $0\le\rho<\rho_{\max}(x_0,\gamma)$, let

$$\underline\varepsilon=\min\Big\{\tfrac1N\textstyle\sum_{i\in\mathcal I_1}p_i:\ p\in[0,1]^N,\ \tfrac1N\sum_{i\in\mathcal I_1}d_i(1-p_i)\le\rho\Big\}.$$

Then $\underline\varepsilon>0$, and for every loss $\ell$

$$\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X\in\mathcal N_\gamma(x_0))>0}\mathbb E_{\mathbb Q}[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)]=\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X\in\mathcal N_\gamma(x_0))\ge\underline\varepsilon}\mathbb E_{\mathbb Q}[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)].$$

Milestones

1. Display (24), p. 47: $\mathbb Q\in\mathbb B_\rho$ if and only if $\mathbb Q=N^{-1}\sum_i\pi_i$ for probability measures $\pi_i$ with $N^{-1}\sum_i\mathbb E_{\pi_i}[\mathbb D_{\mathcal X}(X,\hat x_i)+\mathbb D_{\mathcal Y}(Y,\hat y_i)]\le\rho$.
2. Proposition 4.1, p. 18: $\rho_{\max}(x_0,\gamma)=N^{-1}\sum_{i\in\mathcal I_1}d_i$.
3. Proof of Proposition 4.3, p. 47: for $\rho<\rho_{\max}$, $\inf_{\mathbb Q\in\mathbb B_\rho}\mathbb Q(X\in\mathcal N_\gamma(x_0))>0$.
4. Proof of Proposition 4.3, pp. 47–48: for $\rho>0$, $\inf_{\mathbb Q\in\mathbb B_\rho}\mathbb Q(X\in\mathcal N_\gamma(x_0))=\underline\varepsilon$.

Significance

Proposition 4.3 removes the degenerate constraint "positive probability" from the conditional robust problem whenever the budget is below $\rho_{\max}$. The degenerate constraint defines a feasible set that is not closed, and conditional expectations along it can involve divisions by arbitrarily small masses; after the reduction, the problem has a positive, explicitly computable mass requirement $\underline\varepsilon$, and the finite-dimensional dual reformulation of Theorem 4.4 (which needs a positive mass requirement) applies. Together with Proposition 4.2, which shows that above $\rho_{\max}$ the worst case degenerates to $\sup_y\ell(y,\alpha,\beta)$, it gives a complete picture of the regime $\gamma>0$, $\varepsilon=0$. The LP defining $\underline\varepsilon$ is a fractional knapsack problem, solvable greedily.

The paper proves these results; none of them has a machine-checked proof. The mission produces a formal account of the transport-ball representation (24) on Polish spaces, the closed form of $\rho_{\max}$, and the reduction itself. It also records, with explicit counterexamples, where the printed arguments need additional hypotheses (see Formalization scope).

Difficulty

The obvious argument fixes $\mathbb Q\in\mathbb B_\rho$, splits it as $N^{-1}\sum_i\pi_i$, and bounds the cost of the mass that each $\pi_i$ moves out of the fiber. Two steps resist. The splitting with the exact budget $\le\rho$ requires an optimal coupling, so attainment of the transport infimum on Polish spaces is needed. And the bound "moving a fraction $1-p_i$ of sample $i$ out of the fiber costs at least $d_i(1-p_i)$" needs the cost of leaving $\mathcal N_\gamma(x_0)$ from $\hat x_i$ to equal the boundary cost $d_i$, which is not implied by continuity of $\mathbb D_{\mathcal X}$. Identifying the infimal fiber mass with the LP value also requires approximating boundary points from outside the neighbourhood, so the LP minimum is approached but not attained by measures in the ball.

Formalization scope

Spaces are Polish with Borel $\sigma$-algebras; $[N]$ is Fin N with $N\ge1$; repeated samples are allowed. The transport cost is the published RWPI.SqrtLasso.transportCost (an infimum over couplings with first marginal $\mathbb Q$ and second marginal $\widehat{\mathbb P}$, lower Lebesgue integrals of a $[0,\infty]$-valued cost); the paper's "min" is not built into it. Expectations of the loss are $\int\ell^+-\int\ell^-$ in the extended reals (published ModelRiskOT.Duality.extIntegral). Worst-case values are suprema in EReal over probability measures. The loss is an arbitrary function $\ell:\mathcal Y\to\mathbb R$, which covers every decision $(\alpha,\beta)$. $\kappa_i$ and $d_i$ are infima (sInf), and $\partial$ is the topological frontier in $\mathcal X$.

Hypotheses beyond the page, all disclosed in the statements:

• Every statement about $\gamma>0$ carries Assumption 2.4 and a predicate BoundaryRegular: the boundary of $\mathcal N_\gamma(x_0)$ is nonempty, for $i\in\mathcal I_1$ the infimum of $\mathbb D_{\mathcal X}(x,\hat x_i)$ over $x\notin\mathcal N_\gamma(x_0)$ is $d_i$, and for $i\in\mathcal I_2$, $d_i=\kappa_i$. It holds for norm distances; without it Proposition 4.1 fails for some continuous costs.
• $\rho\ge0$, the paper's standing $\rho\in\mathbb R_+$.
• Milestone 4 is stated for $\rho>0$: at $\rho=0$ a sample on the boundary has $d_i=0$ but cannot be moved, and the identity fails.

The formalization excludes the trivializing readings: no conditional expectation is evaluated at a distribution with zero fiber mass, no Bochner integral of a possibly non-integrable loss is used, a negative $\rho$ cannot enter through ENNReal.ofReal, and the suprema range exactly over the probability measures of $\mathbb B_\rho$ satisfying the stated mass constraint. "Equivalent" is formalized as equality of the inner suprema for every loss, which is stronger than equality of the min–max values.

A complete development needs couplings and gluing for finitely supported marginals, existence of optimal couplings for continuous costs on Polish spaces, and finite LP facts (attainment, positivity). The transport-ball representation and the optimal-coupling existence are reusable beyond this mission. Proofs of any milestone, and of the representation (24) in particular, are welcome.

Selected references

• V. A. Nguyen, F. Zhang, S. Wang, J. Blanchet, E. Delage, Y. Ye, Robustifying conditional portfolio decisions via optimal transport, arXiv:2103.16451v3, 2024; Operations Research, 2025. https://arxiv.org/abs/2103.16451
• C. Villani, Optimal Transport: Old and New, Grundlehren der mathematischen Wissenschaften 338, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44(2), 2019. https://doi.org/10.1287/moor.2018.0936

Motivation

A forecaster who issues a probability distribution for a multivariate quantity, such as the joint demand at several locations or the joint returns of several assets, is often judged not on the whole distribution but on a region it implies: the set of outcomes whose cumulative probability, or smoothed density, exceeds a threshold. Such level sets are the multivariate counterpart of quantiles, and they are used as risk regions and as summaries of joint distributions in management science (Abbas, Budescu and Gu 2010) and in density level set estimation (Cadre 2006). To compare competing level set forecasts against realized data, one needs a consistent scoring function: a loss $l(A, y)$ of a candidate set $A$ and an outcome $y$ whose expectation under the true distribution is smallest at the true level set. For univariate quantiles the answer is classical (the quantile or pinball loss, Gneiting 2011); for general multivariate level sets, the paper notes, scores had not been studied beyond density level sets and univariate quantiles.

Meng, Taylor, Ben Taieb and Li (Operations Research, 2025) obtain such scores by decomposing their $L^2$ scoring rule for multivariate distributions into an integral, over the threshold $\alpha$, of scores for the level sets of a smoothed density. This mission formalizes that construction: Theorem 2 of the paper.

Setting

Write $\mathbb R^d$ for $d$-dimensional space with Lebesgue measure $\mathcal L^d$ and the componentwise order ($z \ge y$ means $z_j \ge y_j$ for all $j$). The unknown distribution of the observation $Y$ is a probability measure $P_Y$ on $\mathbb R^d$; the paper writes $f_Y$ for its generalized density. Fix a kernel $w : \mathbb R^d \to \mathbb R$ and a nonnegative integrable weight $h$. The smoothed density is the convolution

$$(f_Y * w)(z) = \int_{\mathbb R^d} w(z - s)\, dP_Y(s).$$

For $w = u = \mathbb 1\{\cdot \ge 0\}$ (the Heaviside function) it is the multivariate CDF $F_Y(z) = P_Y\{s \le z\}$.

The $\alpha$ level set of a function $g$ is (display (9), p. 12)

$$L(g;\alpha) = \{ z \in \mathbb R^d : g(z) \ge \alpha \}.$$

A function $l(A, y)$ of a Borel set $A \subseteq \mathbb R^d$ and a realization $y$ is a consistent scoring function for $L(f_Y * w; \alpha)$ if $\mathbb E_{P_Y}[l(A, \bullet)]$ is minimized at $A = L(f_Y * w;\alpha)$, and strictly consistent if that set is the only minimizer (p. 12). The level set score is (display (11), p. 13)

$$(S')^\Gamma(A, y; w, h, \alpha) = \int_{\mathbb R^d} \bigl(\alpha - w(z - y)\bigr)\, \mathbb 1\{z \in A\}\, h(z)\, dz,$$

and the $L^2$ scoring rule of the paper is (display (3), p. 8)

$$S'(P_X, y; w, h) = \int_{\mathbb R^d} (f_X * w)^2(z)\, h(z)\, dz - 2 \int_{\mathbb R^d} (f_X * w)(z)\, w(z - y)\, h(z)\, dz.$$

In Lean these are smooth, levelSet, scoreΓ, S', cdf and heaviside in the definition item MultivarScores.LevelSet.Setting.

Formalization targets

The paper's Theorem 2 (p. 13) reads:

Let $\mathcal V^d$, $h$, and $w$ satisfy Assumption 1 in the appendix, and $w$ is nonnegative. Let $\alpha > 0$, and let $A \subseteq \mathbb R^d$ be an arbitrary Borel set. Suppose $(S')^\Gamma(A, \bullet; w, h, \alpha)$ is finite $\mathcal L^d$-a.e. and $(S')^\Gamma(A, \bullet; w, h, \alpha) f_Y(\bullet)$ is integrable. Then the following expression defines a consistent scoring function for the $\alpha$ level set $L(f_Y * w; \alpha)$: $(S')^\Gamma(A, y; w, h, \alpha) = \int_{\mathbb R^d} (\alpha - w(z - y))\, \mathbb 1\{z \in A\}\, h(z)\, dz$. (11) If $h$ is nonzero $\mathcal L^d$-a.e. and $L(f_Y * w; \alpha)$ equals the closure of $\{f_Y * w > \alpha\}$, it is strictly consistent. Moreover, with $A = L(f_X * w; \alpha)$, the integral of (11) with respect to $\alpha$ is precisely half of the $L^2$ score in (3), i.e., $\tfrac12 S'(P_X, y; w, h) = \int_0^\infty (S')^\Gamma(L(f_X * w; \alpha), y; w, h, \alpha)\, d\alpha$.

Goal: consistency

For every Borel $A$ and every $\alpha > 0$,

$$\mathbb E_{P_Y}\bigl[(S')^\Gamma(L(f_Y * w;\alpha), \bullet; w, h, \alpha)\bigr] \le \mathbb E_{P_Y}\bigl[(S')^\Gamma(A, \bullet; w, h, \alpha)\bigr].$$

This is the part of Theorem 2 that holds exactly as printed, and it is the goal.

Strict consistency (milestone)

If moreover $h \ne 0$ a.e., $\mathcal L^d\{f_Y * w = \alpha\} = 0$, and $\mathcal L^d(A \,\triangle\, L(f_Y * w;\alpha)) \ne 0$, the inequality is strict. The null-set condition replaces the printed closure condition (see Formalization scope).

Layer-cake decomposition (milestone)

$$\tfrac12 S'(P_X, y; w, h) = \int_0^\infty (S')^\Gamma\bigl(L(f_X * w;\alpha), y; w, h, \alpha\bigr)\, d\alpha.$$

The other milestones are the steps of the paper's proof (pp. 33–34): the per-realization difference $\Delta''$ (p. 33), the expected difference (19) (p. 34), and two companions: the CDF level set score (13) is consistent for $L(F_Y;\alpha)$ (p. 16), and in dimension one it equals the quantile score up to a term depending only on $y$ (Remark 2, p. 17).

Significance

Theorem 2 supplies consistent scoring functions for a whole family of multivariate level sets at once, one for each kernel $w$: CDF level sets (from $w = u$), density level sets (from $w = \delta_0$) and lower-partial-moment level sets. It thereby gives a way to rank and compare multivariate region forecasts, and in one dimension recovers the full class of quantile scores (Remark 2). The layer-cake identity explains the relation between a distribution score and its level set scores, generalizing the classical identity $\mathrm{CRPS} = 2\int_0^1(\text{quantile score})\,d\alpha$ (display (10)); the paper relates its CDF level set score to the Vorob'ev quantile scores of Fissler, Frongillo, Hlavinová and Rudloff (2021).

The result is proved in the paper's appendix (pp. 33–34). It has no machine-checked proof that this mission is aware of. Formalizing it fixes the exact integrability conditions under which the expectations exist (the paper states them loosely in Assumption 1), and it repairs the strict consistency clause, whose printed sufficient condition does not imply what the proof uses.

Difficulty

The core of consistency is a sign argument, but every quantity in it is an integral over $\mathbb R^d$ against $h$ or against $P_Y$, and none of them is a priori finite: $w$ need not be bounded or integrable, and $(S')^\Gamma(A, y)$ must be integrable in $y$ for the true level set as well as for the candidate $A$, although the paper assumes it only for $A$. Exchanging the $y$- and $z$-integrals therefore needs a product-integrability condition, not pointwise finiteness. The layer-cake milestone requires the layer cake formula for two different measures ($h\,dz$ and $w(z-y)h(z)\,dz$), with powers $2$ and $1$, followed by an exchange that keeps the sign of the second term; a nonnegative (lower) integral cannot express the difference. The strict clause needs a measure-theoretic condition on the boundary $\{f_Y * w = \alpha\}$; a topological condition on closures, as printed, is not enough.

Formalization scope

• $\mathbb R^d$ is Fin d → ℝ with volume and the Pi order; $d$ is any natural number. A distribution is a probability measure P : Measure (E d); every integral is a Bochner integral.
• The kernel $w$ is a measurable function. The paper allows a local Borel measure, so that $w = \delta_0$ gives the density level set score (12); that case is not formalized.
• Standing assumptions. $w \ge 0$ and $\alpha > 0$ (Theorem 2), $h \ge 0$ measurable and integrable (Assumption 1(a)), $A$ Borel.
• Integrability. Assumption 1 and Theorem 2's "$(S')^\Gamma(A,\bullet)$ finite a.e. and $(S')^\Gamma(A,\bullet)f_Y$ integrable" are pinned down as the single hypothesis that $(s, z) \mapsto w(z - s)h(z)$ is integrable for $P_Y \otimes \mathcal L^d$. With $w, h \ge 0$ it covers every Borel set at once, including $L(f_Y * w;\alpha)$. The layer-cake milestone uses Assumption 1(b)/(c) for the given $y$ and the almost-everywhere integrability of $w(z - \cdot)$ under $P_X$.
• No class $\mathcal V^d$. The consistency statement is pointwise in $P_Y$; its convexity is never used.
• Strict consistency is stated under $\mathcal L^d\{f_Y * w = \alpha\} = 0$ and $h \ne 0$ a.e., and "only minimizer" is read modulo $\mathcal L^d$-null sets. The printed condition "$L(f_Y * w;\alpha)$ equals the closure of $\{f_Y * w > \alpha\}$" does not imply the null-set property the proof uses: for $d = 1$, $P_Y = \delta_0$, $w = \alpha + \mathrm{dist}(\cdot, C)$ with $C$ a fat Cantor set, the closure condition holds but $\mathbb R \setminus C$ scores as well as $L$.
• Level sets use $\ge$, as in (9). The proof's partition by $\{f_Y * w > \alpha\}$ is a printed slip; the milestones use $A \setminus L$ and $L \setminus A$.
• Ruled out. Because a Bochner integral of a non-integrable function is $0$, dropping the integrability hypotheses, letting $A$ range over non-measurable sets, or fixing particular $w$ or $h$ would trivialize or change the statements; none of these is done.
• Infrastructure: Mathlib's layer cake (MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul and relatives in Mathlib/MeasureTheory/Integral/Layercake.lean) and Fubini–Tonelli (integral_prod). A reusable lemma for $\int\!\!\int g(z) w(z - s) h(z)\,dz\,dP(s) = \int g(z)(f_P * w)(z)h(z)\,dz$ is welcome; it also serves the companion mission on the $L^2$ scoring rules.

Selected references

• X. Meng, J. W. Taylor, S. Ben Taieb, S. Li, Scores for Multivariate Distributions and Level Sets, Operations Research, 2025; preprint arXiv:2002.09578v6, 2023. https://arxiv.org/abs/2002.09578
• T. Gneiting, A. E. Raftery, Strictly Proper Scoring Rules, Prediction, and Estimation, Journal of the American Statistical Association 102(477), 359–378, 2007. https://doi.org/10.1198/016214506000001437
• T. Gneiting, Making and Evaluating Point Forecasts, Journal of the American Statistical Association 106(494), 746–762, 2011. https://doi.org/10.1198/jasa.2011.r10138
• T. Fissler, R. Frongillo, J. Hlavinová, B. Rudloff, Forecast Evaluation of Quantiles, Prediction Intervals, and Other Set-Valued Functionals, Electronic Journal of Statistics 15(1), 1034–1084, 2021. https://doi.org/10.1214/21-EJS1808
• A. E. Abbas, D. V. Budescu, Y. Gu, Assessing Joint Distributions with Isoprobability Contours, Management Science 56(6), 997–1011, 2010. https://doi.org/10.1287/mnsc.1100.1157
• E. H. Lieb, M. Loss, Analysis, 2nd ed., Graduate Studies in Mathematics 14, AMS, 2001. https://doi.org/10.1090/gsm/014

Motivation

Quantile-based risk measures are the regulatory standard in banking and insurance, and Lambda Value-at-Risk (ΛVaR), introduced by Frittelli, Maggis and Peri (2014), generalises Value-at-Risk by letting the confidence level vary with the loss: large losses can be judged at a stricter level than small ones. When several agents (desks of a bank, members of a reinsurance pool, insurer and reinsurer) share one aggregate risk, each measuring their part with their own ΛVaR, the natural question is how the risk should be split to minimise the total measured risk. This is the risk-sharing problem, studied for VaR and Expected Shortfall by Embrechts, Liu and Wang (2018) and for ΛVaR under a common probability by Xia and Hu (2025).

Liu and Schied (2025) treat the same question when the agents disagree about, or are uncertain of, the probability model. Each agent's beliefs are encoded by a capacity, a monotone set function that need not be additive, which covers worst-case and best-case evaluations over a set of probability measures. This mission concerns their Section 6, where allocations are required to be comonotonic: every agent's share increases with the aggregate loss. Comonotonic sharing rules out arrangements in which one agent gains when another loses.

Timeline of the relevant results:

• 2014: Frittelli, Maggis and Peri define ΛVaR.
• 2018: Embrechts, Liu and Wang solve risk sharing for VaR and ES under a common probability.
• 2022: Liu, Mao, Wang and Wei (Theorem 6) find that, for VaR with Wasserstein-ball ambiguity, the optimal comonotonic allocation gives all the risk to one agent.
• 2025: Xia and Hu treat comonotonic risk sharing of ΛVaR under a single probability $\mathbb P$ (their Theorem 11).
• 2025: Liu and Schied extend it to heterogeneous capacities (Theorem 4, the goal of this mission).

Setting

Let $(\Omega,\mathcal F)$ be a measurable space and $\mathcal X$ a set of real random variables containing all bounded ones (the paper's examples are the bounded random variables and all random variables). A capacity is a set function $w:\mathcal F\to[0,1]$ that is increasing, with $w(\emptyset)=0$ and $w(\Omega)=1$. It is continuous if $w(A_n)\to0$ whenever $A_n\downarrow\emptyset$. It is atomless if some bounded random variable $Y$ makes $x\mapsto w(Y>x)$ continuous. A probability measure is a continuous capacity.

Let $\mathcal H_I$ be the set of increasing functions $\Lambda:\mathbb R\to(0,1)$. For $\Lambda\in\mathcal H_I$ and a capacity $w$,

$$\Lambda\mathrm{VaR}^w(X)=\inf\{x\in\mathbb R: w(X>x)\le\Lambda(x)\}\in[-\infty,\infty],\qquad\inf\emptyset=\infty .$$

For constant $\Lambda\equiv p$ this is the Choquet quantile $\mathrm{VaR}^w_p$.

There are $n\ge1$ agents. An allocation of $X$ is $(X_1,\dots,X_n)\in\mathcal X^n$ with $X_1+\dots+X_n=X$. It is comonotonic if there are increasing $f_1,\dots,f_n$ with $X_i=f_i(X_1+\dots+X_n)$, and its components have the same sign if no two of them take strictly opposite signs in any state. Write $\mathbb A_n^+(X)$ for these allocations and

$$\boxplus_{i=1}^n\rho_i(X)=\inf\Big\{\sum_{i=1}^n\rho_i(X_i):(X_1,\dots,X_n)\in\mathbb A_n^+(X)\Big\}$$

for the comonotonic inf-convolution. A minimiser is an optimal allocation.

Formalization targets

Goal: Theorem 4

Let $\Lambda_i\in\mathcal H_I$ and let $w_1,\dots,w_n$ be continuous capacities.

1. If $\Lambda_i\mathrm{VaR}^{w_i}(X)\ge0$ for all $i$, then

$$\boxplus_{i=1}^n\Lambda_i\mathrm{VaR}^{w_i}(X)=\min_{i\in[n]}\Lambda_i\mathrm{VaR}^{w_i}(X),\tag{11}$$

and $X_{i_0}=X$, $X_i=0$ ($i\ne i_0$) is optimal for every $i_0\in\arg\min_i\Lambda_i\mathrm{VaR}^{w_i}(X)$. 2. If every $\Lambda_i$ is constant on $(-\infty,0)$, then (11) holds for all $X\in\mathcal X$. 3. If $n\ge2$, the capacities are equal and atomless and the $\Lambda_i$ are equal, then (11) holds for all $X\in\mathcal X$ if and only if $\Lambda_1$ is constant on $(-\infty,0)$.

All three parts are posed as one theorem.

Milestones (proof of Theorem 4, Appendix D)

• Reduction to splits (p. 39): $\boxplus_i\Lambda_i\mathrm{VaR}^{w_i}(X)=\inf\{\sum_i\Lambda_i\mathrm{VaR}^{w_i}(f_i(X)):(f_i)\in\mathbb F_n\}$, where $\mathbb F_n$ is the set of increasing continuous $f_1,\dots,f_n$ with $f_i(0)=0$ and $\sum_if_i=\mathrm{id}$.
• Change of variables (p. 39): $\Lambda_i\mathrm{VaR}^{w_i}(f_i(X))=f_i\big((\Lambda_i\circ f_i)\mathrm{VaR}^{w_i}(X)\big)$.
• (14) (p. 40): $f_i\big((\Lambda_i\circ f_i)\mathrm{VaR}^{w_i}(X)\big)\ge f_i\big(\Lambda_i\mathrm{VaR}^{w_i}(X)\big)$ when $\Lambda_i\mathrm{VaR}^{w_i}(X)\ge0$, and for every $X$ when $\Lambda_i$ is constant on $(-\infty,0)$.
• (15) (p. 40): $\sum_i\Lambda_i\mathrm{VaR}^{w_i}(f_i(X))\ge\sum_if_i(\Lambda_i\mathrm{VaR}^{w_i}(X))\ge\min_i\Lambda_i\mathrm{VaR}^{w_i}(X)$ when every $\Lambda_i\mathrm{VaR}^{w_i}(X)\ge0$, and for every $X$ when every $\Lambda_i$ is constant on $(-\infty,0)$.

Significance

Theorem 4 says that, among comonotonic arrangements, nothing beats handing the whole risk to the agent with the smallest ΛVaR, for any heterogeneous beliefs given by continuous capacities. It extends the single-probability result of Xia and Hu (2025, Theorem 11). The characterisation in part 3 marks the boundary of that conclusion: for risks with negative ΛVaR the one-agent arrangement remains optimal exactly when the confidence level does not vary on the negative half-line. For applications this separates the reinsurance-style problems, where losses are nonnegative and the answer is extreme, from the general case, where it is not.

The result is proved in the preprint and has no machine-checked counterpart. A formal development provides a first Lean treatment of ΛVaR under non-additive set functions and of comonotonic allocations defined through increasing functions of the aggregate, and checks a proof whose printed version has a gap (see Difficulty). The definitions are reusable by the companion missions on the same paper (robust ΛVaR, inf-convolution of ΛVaRs).

Difficulty

The upper bound in (11) is immediate from the one-agent allocation. The lower bound needs the reduction of comonotonic same-sign allocations to splits of the identity, which uses that a family of increasing functions summing to the identity on the range of $X$ extends to continuous, $1$-Lipschitz functions on $\mathbb R$ vanishing at $0$. ΛVaR does not commute with $f_i$, so the second step is a change of variables that moves $f_i$ into the level function. The comparison $(\Lambda_i\circ f_i)\mathrm{VaR}\ge\Lambda_i\mathrm{VaR}$ then holds only where $\Lambda_i\circ f_i\le\Lambda_i$, which depends on the sign of the argument.

For part 2 the printed proof asserts $\Lambda_i\circ f_i\le\Lambda_i$ whenever $\Lambda_i$ is constant on $(-\infty,0)$. That fails when $\Lambda_i$ jumps at $0$ and $f_i$ vanishes on part of the negative half-line, so the printed step does not prove the claim. The claim itself survives, and a correct argument must handle that case separately. Part 3 needs an explicit risk built from an atomless capacity at which the inf-convolution falls strictly below the minimum, and capacities are not additive, so the usual distributional constructions are unavailable.

Formalization scope

Lean namespace LambdaVaRAmb.Comono; one definition file and six theorem files. Conventions:

• Capacities are Set Ω → ℝ with the axioms imposed on measurable sets. ΛVaR, the inf-convolution, sums and minima live in EReal, so $\inf\emptyset=+\infty$ and an unbounded-below set gives $-\infty$, as in the paper. "Increasing" is Monotone. Agents are Fin n with $n\ge1$, and sums of random variables are pointwise.
• $\mathcal X$ is any set of real functions whose members are measurable, which contains every bounded measurable function, and which is closed under $(X-c)\mathbb 1_A+d$ and under $f(X)$ for increasing $1$-Lipschitz $f$ with $f(0)=0$. Both of the paper's examples qualify.
• "sign$(X_i)$ are the same" is read as $X_iX_j\ge0$ pointwise. The literal reading with sign$(0)=+1$ would make Theorem 4's own optimal allocation inadmissible whenever $X$ takes a negative value.
• Part 3 carries $n\ge2$: for $n=1$ equation (11) holds for every $X$, and the "necessary" direction fails. "$w_1=\dots=w_n$" is equality on measurable sets.
• In the milestones, $f_i$ at $\pm\infty$ means its monotone limit, which is how the page's $f_i\big((\Lambda_i\circ f_i)\mathrm{VaR}^{w_i}(X)\big)$ is read when that value is infinite.
• The (14)-and-(15)-for-all-$X$ milestone poses only the printed conclusion, not the false intermediate step.

Trivialising encodings are excluded. Infima are taken in EReal, never as a real sInf that collapses to $0$. No sum in the statements can meet $\top+\bot$. The admissible set $\mathcal X$ is constrained rather than arbitrary. The hypotheses are satisfiable, since a probability measure is a continuous capacity and constant levels lie in $\mathcal H_I$.

Welcome contributions include the reduction to $\mathbb F_n$ (a reusable fact about comonotonic decompositions), the ΛVaR change-of-variables identity, and the atomless-capacity construction of part 3.

Selected references

• P. Liu and A. Schied, Lambda Value-at-Risk under ambiguity and risk sharing, arXiv preprint, 2025. https://arxiv.org/abs/2511.00717
• M. Frittelli, M. Maggis and I. Peri, Risk measures on 𝒫(ℝ) and Value at Risk with probability/loss function, Mathematical Finance 24(3), 2014. https://doi.org/10.1111/mafi.12004
• P. Embrechts, H. Liu and R. Wang, Quantile-based risk sharing, Operations Research 66(4), 2018. https://doi.org/10.1287/opre.2017.1716
• F. Liu, T. Mao, R. Wang and L. Wei, Inf-convolution, optimal allocations, and model uncertainty for tail risk measures, Mathematics of Operations Research 47(3), 2022, pp. 2494–2519.
• Z. Xia and T. Hu, Optimal risk sharing for lambda value-at-risk, Advances in Applied Probability 57, 2025, pp. 171–203.
• D. Denneberg, Non-Additive Measure and Integral, Kluwer, 1994. https://doi.org/10.1007/978-94-017-2434-0

Motivation

A bidder in repeated first-price auctions faces a learning problem with two kinds of side information. Their private value is a context that changes every round, and the outcome of one bid reveals something about other bids (graph feedback across actions) and about other values (cross learning across contexts). Han, Zhou and Weissman (arXiv:2003.09795v7) abstract this structure into partially ordered contextual bandits and show that, when contexts are iid, an arm-elimination policy has regret $\widetilde O(\sqrt{\alpha\beta T})$ (Theorem 5), with no polynomial dependence on the number of contexts or actions.

Theorem 6 of the same paper asks whether this survives when contexts are chosen by an adversary. It does not: with adversarial contexts every policy suffers regret polynomial in $\min\{\alpha M, K\}$. This separation is what forces the paper to look beyond the partially ordered structure for its $\widetilde O(\sqrt T)$ adversarial-value result (Theorem 2). The lower bound is also of independent interest for contextual bandits with cross learning (Balseiro et al., NeurIPS 2019) and with feedback graphs (Alon et al., COLT 2015).

Setting

A stochastic contextual bandit with graph feedback and cross learning (Definition 2, p. 14) has a horizon $T$, $M$ contexts $\mathcal C$, $K$ actions $\mathcal A$, a joint reward law $P$ on $[0,1]^{\mathcal C\times\mathcal A}$ with means $R_{c,a}$, and a directed graph $G=(\mathcal A,E)$ without self-loops. In round $t$ the learner sees a context $c_t$, picks $a_t$, nature draws a fresh reward vector $r_t\sim P$, and the learner observes $r_{t,c,a}$ for every context $c$ and every $a\in I_t=\{a_t\}\cup\{a:(a_t,a)\in E\}$. The regret (5) is

$$R_T(\pi)=\sum_{t=1}^T\Big(\max_{a\in\mathcal A}R_{c_t,a}-R_{c_t,a_t}\Big).$$

The independence number $\alpha$ of $G$ is the size of a largest set of actions with no edge between any two of them; for a partial order, $\beta$ is the size of a largest set of pairwise incomparable elements.

The instance is a partially ordered contextual bandit (Definition 3, pp. 16–17) if $G$ is a DAG equal to its own transitive closure, so that $a_1\preceq_G a_2$ iff $a_1=a_2$ or $(a_1,a_2)\in E$ is a partial order, and there is a partial order $\preceq_{\mathcal C}$ on contexts with $c_1\preceq_{\mathcal C}c_2\Rightarrow a^\star(c_1)\preceq_G a^\star(c_2)$ for optimal actions $a^\star(c)\in\arg\max_a R_{c,a}$.

A policy $\pi$ chooses $a_t$ from its internal randomness, the contexts $c_1,\dots,c_t$ and the earlier observations. The context sequence is oblivious: fixed in advance, possibly depending on $\pi$ but not on its random draws.

Formalization targets

Goal: Theorem 6 in the regime of its proof

For integers $\alpha\ge1$, $M\ge1$, with $K=(\alpha+1)M$, $K^3\le T$ and $M\mid T$: there is a feedback graph $G$ on $K$ actions with independence number $\alpha$ such that for every policy $\pi$ there are a reward law $P$ (making $(G,P)$ partially ordered with the total order on contexts, $\beta=1$) and contexts $(c_t)$ with

$$\mathbb E[R_T(\pi)]\ \ge\ \frac{\sqrt{KT}}{32e^3}.$$

Because $\alpha M\le K$, this is at least $\frac1{32e^3}\min\{\sqrt{\alpha MT},\sqrt{KT},T^{2/3}\}$, the printed form of Theorem 6, in this regime.

Milestones

Along the proof (pp. 22–24): the construction is a partially ordered contextual bandit with $\beta=1$ and independence number $\alpha$; properties 1–4 of the mean rewards; property 5, the KL divergence of the observed rewards; the regret decomposition (7); the testing lemma (Lemma 13, p. 36)

$$\frac1n\sum_{i=1}^nQ_i(\Psi\ne i)\ \ge\ \frac1{2n}\sum_{i=2}^n e^{-D_{\mathrm{KL}}(Q_1\|Q_i)};$$

the self-referential inequality (8)

$$R_T\ \ge\ \frac{\sqrt{KT}}{16e^3}\exp\Big(-\frac{16KR_T}{3T}\Big),\qquad R_T=\max_u\mathbb E_u[R_T(\pi)];$$

and the final step $R_T\ge\sqrt{KT}/(32e^3)$.

Significance

The theorem separates stochastic from adversarial contexts. Under iid contexts, Theorem 5 gives $\widetilde O(\sqrt{\alpha\beta T})$; with adversarial contexts, even when $\beta=1$, regret must grow like $\sqrt{\alpha MT}$, matching the upper bound of Theorem 4 up to logarithms. For first-price auctions with adversarial values (Remark 2), the bound shows that the partially ordered structure alone cannot give $\widetilde O(\sqrt T)$; the paper's $\widetilde O(\sqrt T)$ algorithm must use the extra correlation of auction rewards.

The paper proves the theorem in full. As far as we know, none of it has been formalized; in particular, no machine-checked version of a Bayesian multi-hypothesis lower bound for bandits with graph feedback and cross learning exists. A formal proof will produce reusable pieces: Lemma 13 is a general testing inequality; the KL chain rule for adaptively collected bandit observations, with feedback revealed on a graph, is needed for any information-theoretic bandit lower bound; and the interaction model is shared with the paper's upper bounds.

Difficulty

The standard minimax argument for $K$-armed bandits compares two instances that differ in one arm, and the regret follows directly from a testing error. Here that argument fails: feedback graphs and cross learning mean that pulling one arm can reveal everything, and a policy may pay to explore. The proof instead plays a uniform prior over $(\alpha+1)^M$ instances and obtains an inequality in which the maximal regret $R_T$ appears on both sides, (8). If the regret is small, the policy has not explored enough to tell the instances apart, which in turn forces large regret. Making this rigorous requires the chain rule of KL divergence over the adaptively chosen observations, the specific ordering of contexts (decreasing over blocks, so early observations say nothing about late optimal actions), and the regime $K^3\le T$ to close the self-referential bound.

Formalization scope

• Contexts are Fin M, rounds Fin T (paper index = Lean index + 1). The goal uses actions Fin K; the construction uses Fin M × Fin (α + 1), with $j=0$ the action $(i,0)$.
• A reward law is a measure on Fin M → A → ℝ. Definition 2 requires a probability measure carried by $[0,1]^{M\times K}$ and a graph without self-loops. Means are integrals, and $\max_a$ is a supremum over the finite action set.
• Definition 3's "DAG equal to its transitive closure" is encoded as "no self-loops and transitive". The printed $\arg\max$ is read as a selection of maximisers.
• Independence numbers are exact: a set of the given size exists, and none is larger.
• Policies are randomized and non-anticipating. The action is a measurable function of the internal randomness (an arbitrary probability space), the contexts so far and the past observations, and the argument types enforce non-anticipation. An observation is the reward vector with unrevealed coordinates set to $0$; the learner knows its own action, so this carries exactly the revealed rewards. Deterministic-only policies would give a weaker theorem, and they are not the class used.
• Expected regret integrates over the internal randomness and iid reward vectors, with the context sequence fixed.
• KL divergence is Mathlib's $[0,\infty]$-valued klDiv. In Lemma 13, $e^{-\infty}$ is read as $0$, so an infinite divergence cannot be truncated to $0$ and inflate the right side.
• The reduction from general $(M,K,T)$ by "dummy contexts and actions" (p. 21) is not formalized. It needs $\min\{K,(\alpha+1)M,T^{1/3}\}\ge\alpha+1$, and the printed theorem is false at $K=1$. The hypotheses $M\mid T$ and $\alpha\ge1$ replace the paper's "without loss of generality".
• Property 5 assumes $u_c\neq0$, because for $u_c=0$ the two laws coincide. (7) is stated for each $u$, which implies the printed form for the maximum.

Needed infrastructure: Bernoulli product measures and their KL divergence, the KL chain rule for the law of an adaptive interaction, and a Bretagnolle–Huber-type inequality. Contributions of these general lemmas, and of the measurability facts for the interaction, are welcome.

Selected references

• Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, Operations Research, 2025; preprint arXiv:2003.09795v7. https://arxiv.org/abs/2003.09795
• Z. Gao, Y. Han, Z. Ren, Z. Zhou, Batched Multi-armed Bandits Problem, NeurIPS 2019 (source of Lemma 13). https://arxiv.org/abs/1904.01763
• S. Balseiro, N. Golrezaei, M. Mahdian, V. Mirrokni, J. Schneider, Contextual Bandits with Cross-learning, NeurIPS 2019. https://arxiv.org/abs/1809.09582
• N. Alon, N. Cesa-Bianchi, O. Dekel, T. Koren, Online Learning with Feedback Graphs: Beyond Bandits, COLT 2015. https://arxiv.org/abs/1502.07617
• A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794