All missions

Motivation

In online selection, items reveal information one at a time, and each decision to accept an item is irrevocable. A matroid constraint permits some subsets and excludes others; it covers choices such as selecting linearly independent vectors or acyclic edges. A fractional solution can assign an acceptance probability to each item, but independent activations can produce a set that violates the constraint. An online contention resolution scheme (OCRS) turns these activations into a feasible selection while respecting the order in which items arrive. The matroid result of Feldman, Svensson and Zenklusen gives a guarantee that survives even when an adversary knows all random outcomes before choosing the arrival order.

This mission concerns the paper's matroid theorem, Theorem 2.1. The same paper develops schemes for matching and knapsack constraints and a rule for combining schemes for intersecting constraints. Those results are separate missions in this series. Here the central question is how much of a fractional matroid point can be retained by a deterministic greedy rule as each active item is revealed.

Setting

Let $N$ be a finite ground set and let $M$ be a matroid on $N$. Its independent subsets form a down-closed family $\mathcal F$: if $I$ is independent, every subset of $I$ is independent. The rank $r(S)$ of $S\subseteq N$ is the maximum size of an independent subset of $S$. The matroid independence polytope is

$$P_{\mathcal F}=\left\{x\in\mathbb R^N_{\ge0}:x(S):=\sum_{e\in S}x_e\le r(S)\text{ for all }S\subseteq N\right\}.$$

Its points have $0\le x_e\le1$. For a point $x$, the active set $R(x)$ contains each $e$ independently with probability $x_e$. A deterministic greedy OCRS assigns a down-closed family $\mathcal F_x\subseteq\mathcal F$ to $x$ and accepts an active element when adding it to the already accepted set stays in $\mathcal F_x$. The empty set belongs to every $\mathcal F_x$. The rule depends on $x$ before the active set and arrival order are revealed.

An element $e$ is selectable for an active set $A$ if $I\cup\{e\}\in\mathcal F_x$ for every $I\subseteq A$ with $I\in\mathcal F_x$. A greedy OCRS is $(b,c)$-selectable if this event has probability at least $c$ for every $x\in bP_{\mathcal F}$ and every $e\in N$. The event implies that $e$ can be added regardless of which eligible active elements arrived first. These definitions are from §1.1 of the paper.

Formalization targets

Matroid OCRS

For every $b\in[0,1]$ and every finite loopless matroid $M$, the target is a deterministic greedy OCRS with

$$\Pr\left[I\cup\{e\}\in\mathcal F_x\text{ for all }I\subseteq R(x),\ I\in\mathcal F_x\right]\ge 1-b \quad\text{for every }x\in bP_{\mathcal F},\ e\in N.$$

The loopless condition is a disclosed correction to the printed Theorem 2.1: a loop cannot belong to any independent singleton, so its selectability is zero. The printed bound would demand positive selectability for that loop whenever $b<1$. The theorem keeps the paper's constant $1-b$ exactly.

Supporting targets

The milestones reproduce six statements from §2.1–2.1.1, in attack order: validity of a family defined by a chain $\varnothing=N_\ell\subsetneq\cdots\subsetneq N_0=N$ of matroid minors (independence of the union of layer-wise independent sets is Soto, Theorem 5.1); a characterization of selectability through span in one layer; monotonicity of the first chain set as coordinates of $x$ increase; the description of the base polytope $P_{\mathcal B}=\{x\in P_{\mathcal F}:x(N)=r(N)\}$ as the set of maximal vectors of $P_{\mathcal F}$; the weighted span bound of Lemma 2.4,

$$\sum_{e\in N}x_e\Pr[e\in\operatorname{span}(R(x)\cup S)]\le b\cdot\bigl(x(N)+(1-b)\,r(S)\bigr),$$

strict when $S\neq\varnothing$; and the proper-inclusion conclusion $S\subsetneq N$ of Corollary 2.5. They expose the distinct matroid and probability claims on which the main theorem rests.

Significance

The theorem gives a fixed greedy family for each fractional point, with a per-element probability guarantee that is independent of the arrival order. Offline contention resolution schemes for matroids were introduced by Chekuri, Vondrák and Zenklusen; the online, almighty-adversary version here is stronger. A solver can use that guarantee as the matroid component in larger online selection problems. In the source paper it feeds the intersection and application results; those applications require further models and statements beyond this mission. The factor $1-b$ makes the tradeoff explicit: using a more heavily scaled fractional point raises the risk of contention.

The result is proved in the cited paper. This mission asks for a machine-checked Lean proof of its corrected statement and the source's supporting claims. A successful development would add reusable finite representations of independent activation, matroid polytope inequalities, span probabilities, and chain families. It would also make the loop boundary explicit, preventing a formally false version of the printed theorem from being published as a target.

Difficulty

Independent activation does not itself respect matroid independence. A greedy family that simply contains every independent set can make an element unavailable after earlier active elements are accepted, and the arrival order can expose the worst such history. The central issue is therefore a uniform selectability event: the same element must remain addable after every feasible subset of the active set. The paper measures that obstruction through spans in successive matroid minors. The first chain set must be proper so that the construction can continue, which is why the strict part of the weighted span inequality matters.

Formalization scope

The ground set is a finite Lean type, subsets are Finsets, and Mathlib's Matroid supplies independence, closure, contraction and restriction. Matroid rank is converted from Mathlib's extended natural rank to a real number; finiteness makes this conversion finite on every subset. The independence and base polytopes are defined by the paper's inequalities. The scalar multiple $bP$ is pointwise set scalar multiplication, including $b=0$.

Probabilities are finite sums of product weights over all active sets. In particular, the event in Lemma 2.4 uses $\operatorname{span}(R(x)\cup S)$, whereas the recurrence defining $S$ uses $\operatorname{span}((R(x)\cup S_i)\setminus\{e\})$. These are separate definitions. Every point used for activation lies in $[0,1]^N$, as enforced by the polytope and $b\in[0,1]$. The base-polytope condition on Corollary 2.5 is the standing assumption stated before the lemma in the source.

The loopless condition applies to the goal, to Corollary 2.5, and to the strict clause of Lemma 2.4 only; its non-strict clause, the chain statements and the monotonicity statement hold for every matroid and are stated without it. Three trivializing formalizations are ruled out: every greedy family must contain the empty set, so an empty family cannot satisfy selectability vacuously; every member of a greedy family must be independent in $M$, so $\mathcal F_x=2^N$ is not admissible; and every point used for activation lies in $[0,1]^N$, so $\Pr[R(x)=A]$ is a genuine probability. The quantified scheme depends only on $x$, and its success condition ranges over every feasible subset of the realized active set. Contributions that establish the chain family's independence, finite probability identities, and rank or closure facts are within scope. Polynomial-time implementation and the Monte Carlo estimates of Lemma 2.6 are outside this mission's mathematical target.

Selected references

• Moran Feldman, Ola Svensson and Rico Zenklusen, Online Contention Resolution Schemes, arXiv:1508.00142v2, 2015; published as Online Contention Resolution Schemes with Applications to Bayesian Selection Problems, SIAM Journal on Computing, 2021. Preprint.
• Chandra Chekuri, Jan Vondrák and Rico Zenklusen, Submodular Function Maximization via the Multilinear Relaxation and Contention Resolution Schemes, SIAM Journal on Computing, 2014. arXiv:1105.4593.
• José A. Soto, Matroid Secretary Problem in the Random-Assignment Model, SIAM Journal on Computing, 2013. arXiv:1007.2140.

Motivation

Minimum-cost flow is a standard model for routing a quantity through a network while paying a cost on each arc. Unit capacities arise when each input arc can carry at most one unit; they include flow formulations of several matching and assignment problems. Goldberg, Kaplan, Hed and Tarjan analyze a cost-scaling algorithm for this setting. Their second-phase argument depends on a bound on the excess left in a pseudoflow when every excess vertex has undergone enough potential increases. This mission formalizes that bound, Lemma 5 of their STACS 2015 paper. The published paper gives an $O(\min\{m^{1/2},n^{2/3}\}\,m\log(nC))$ running-time bound for its unit-capacity algorithm; the running-time statement itself is outside this mission.

Setting

A network has a finite vertex set $V$ and an arc set $E$ that contains both orientations of each input arc. Write $n=|V|$. Every input arc has capacity one; its reverse has capacity zero and opposite cost. Write $m$ for the number of input arcs, so $|E|=2m$. The paper assumes no parallel or antiparallel input arcs, allowing an arc to be identified by its ordered endpoints. Costs are antisymmetric between orientations.

A pseudoflow $f$ assigns an antisymmetric quantity to each arc and respects its capacity. Its excess at $v$ is the sum $e_f(v)$ of incoming flow. Positive excess means that $v$ has flow to discharge; negative excess is a deficit. A circulation is a pseudoflow with zero excess at every vertex. An arc is residual for $f$ when its residual capacity $u_f(v,w)=u(v,w)-f(v,w)$ is positive. For vertex prices $p$, its reduced cost is $c_p(v,w)=c(v,w)-p(v)+p(w)$. A pseudoflow is $\varepsilon$-optimal at $p$ when every residual arc has reduced cost at least $-\varepsilon$. These are the paper's conventions on p. 408.

At the start of a cost scale, let $f'$ be a circulation that is $2\varepsilon$-optimal at prices $p'$. During the scale, $f$ is a pseudoflow that is $\varepsilon$-optimal at prices $p$. The potential increase in scale units is $d(v)=(p(v)-p'(v))/\varepsilon$. Put $\lambda=\min\{\sqrt m,n^{2/3}\}$. The second phase begins when every excess vertex has $d(v)\ge\lambda$; the paper also states that every deficit then has $d(v)=0$ and that the levels $d(v)$ are integral. The remaining excess is $X(f)=\sum_{v:e_f(v)>0}e_f(v)$.

The comparison graph has arcs $E^+=\{(v,w)\in E:f'(v,w)>f(v,w)\}$ and vertices $V$. An excess–deficit cut $Y\subseteq E^+$ meets every path in this graph from an excess vertex to a deficit vertex. Thus a cut is measured among comparison arcs, not among arbitrary arcs of the original network. Lemmas 3 and 4 of the paper establish the level and cut bounds on which the excess estimate rests.

Formalization targets

The goal is Lemma 5 on p. 410, stated with both constants obtained in its proof. Under the cost-scale conditions above, and the divisibility conventions in footnotes 5–6, its two cases are

$$\lambda=\sqrt m\quad\Longrightarrow\quad X(f)\le 3\lambda,$$ $$\lambda=n^{2/3}\quad\Longrightarrow\quad X(f)\le36\lambda.$$

The second case also assumes that six divides the integer $\lambda$; the first uses divisibility by three. The goal keeps the two conclusions separate so that the stronger $3\lambda$ bound is retained when $\sqrt m$ determines the scale. Its milestone list follows the paper: Lemma 3 bounds $d(v)-d(w)$ by three on an arc of $E^+$; Lemma 4 bounds total excess by a cut; and the proof of Lemma 5 supplies the cut bands and the two size estimates. The bands use the exact three-level and six-level ranges printed on p. 410.

Significance

The result connects a condition on price increases to a numerical bound on the amount of flow still needing discharge. Combined with the paper's time per unit of remaining excess, this is the bound needed for its second-phase running-time estimate. The two regimes show how the same cost-scale state can be controlled by either the number of input arcs or the number of vertices. Without the excess bound, the paper's argument gives no comparable limit on the remaining work at the phase transition.

The paper proves Lemma 5, but this particular unit-capacity excess argument has no matching theorem in the platform catalog checked for this mission. The network, circulation and pseudoflow interfaces are already published as reusable definitions from earlier cost-scaling work. A completed machine-checked development would add the cut argument and band counts to those interfaces. Those facts can also support other analyses that compare an entry circulation with an intermediate pseudoflow; this mission does not claim to formalize the algorithm's entire execution or its running-time model.

Difficulty

The main obstacle is linking local price inequalities to a global bound on excess. A reduced-cost inequality controls a single residual arc, while excess may move through a path and is measured over many vertices. The comparison graph $G^+$ is essential: on a residual arc outside $E^+$, the level difference used by Lemma 3 is not available. Counting all residual arcs as if they were comparison arcs would therefore not justify the cut bound. There is a separate counting issue: the represented network has both directions of each input arc, so using $|E|$ for $m$ changes the constant in the square-root case.

Formalization scope

Lean represents the network by a finite symmetric arc set with real capacities and antisymmetric real costs. A local unit-capacity predicate marks each reverse pair as capacities $(1,0)$ or $(0,1)$; $m$ counts the capacity-one orientations. Flows are real valued as on p. 408. Integer costs on that page are generalized to real costs because Lemmas 3–5 use only antisymmetry and reduced-cost inequalities. No result here depends on cost integrality.

The formalization takes the cost-scale state as hypotheses: $\varepsilon>0$, entry circulation and $2\varepsilon$-optimality, current $\varepsilon$-optimality, integral levels, level at least $\lambda$ at excess vertices, and zero level at deficits. It takes $\lambda$ as a natural number equal to $\min\{\sqrt m,n^{2/3}\}$ and records the paper's divisibility simplifications. The indexed pigeonhole milestones also require $\lambda>0$ so their index ranges are nonempty; the goal includes the zero-arc boundary without requiring an index. Cuts use reachability after deleting a subset of $E^+$, equivalent to meeting every excess-to-deficit path. The proof of Lemma 5 prints “cut in $G_f$”; the formalized claim uses $G^+$, the graph for which Lemma 3 gives the required level control and Lemma 4 states its bound.

The definition layer, path-cut lemma and finite counting arguments are the reusable infrastructure. Contributions that establish these exact statements, their necessary elementary flow identities, or a machine-checked goal proof are in scope. Counting $m$ with reverse arcs, allowing cuts outside $E^+$, using arbitrary real levels in place of integral ones, or replacing both cases by the weaker $36\lambda$ bound does not express this target.

Selected references

• A. V. Goldberg, H. Kaplan, S. Hed and R. E. Tarjan, Minimum Cost Flows in Graphs with Unit Capacities, 32nd International Symposium on Theoretical Aspects of Computer Science, LIPIcs 30, pp. 406–419, 2015. doi:10.4230/LIPIcs.STACS.2015.406.

Motivation

Lower bounds for interactive decision making (bandits, reinforcement learning, and the general decision making with structured observations framework of Foster, Kakade, Qian and Rakhlin, arXiv:2112.13487) compare what a learner observes under two different environments. A learner's whole interaction history is generated one step at a time: each observation is drawn from a conditional law that depends on everything seen before. Statistical estimation guarantees, by contrast, are stated one step at a time, as bounds on the divergence between the conditional laws at each round. Passing from the per-step guarantees to a statement about the laws of entire histories requires a chain rule for the divergence in use.

For the Kullback–Leibler divergence the chain rule is an identity. The paper's guarantees, however, are stated in the squared Hellinger distance, which is bounded, symmetric, and the natural loss for density estimation with the logarithmic loss. Hellinger distance has no exact chain rule. Lemma A.13 of the paper (App. A.2, p. 73) supplies an approximate one, losing a factor logarithmic in the number of steps, and the paper uses it in the proof of its main regret lower bound (Theorem 3.2, via App. C.1.3).

Setting

Fix $n \in \mathbb N$ and finite sets $\mathcal X_1, \dots, \mathcal X_n$. A sequence is $x = (x_1, \dots, x_n)$ with $x_i \in \mathcal X_i$, and $x_{1:i-1} = (x_1, \dots, x_{i-1})$ denotes its prefix; $\mathcal X^{(i-1)} = \prod_{t=1}^{i-1} \mathcal X_t$.

For probability distributions $p, q$ on a finite set, the squared Hellinger distance, the Hellinger distance and the Kullback–Leibler divergence are

$$D^2_{\mathrm H}(p, q) = \sum_a \big(\sqrt{p(a)} - \sqrt{q(a)}\big)^2, \qquad D_{\mathrm H} = \sqrt{D^2_{\mathrm H}}, \qquad D_{\mathrm{KL}}(p\,\|\,q) = \sum_a p(a) \log\frac{p(a)}{q(a)},$$

the last one set to $+\infty$ when $p$ charges a point that $q$ does not. Note that the paper's $D^2_{\mathrm H}$ carries no factor $\tfrac12$, so $0 \le D^2_{\mathrm H} \le 2$.

A family of sequential kernels $P = (P^{(i)})_{i=1}^n$ assigns to each $i$ and each prefix $x_{1:i-1}$ a probability distribution $P^{(i)}(\cdot \mid x_{1:i-1})$ on $\mathcal X_i$. Its sequential law is the law of $X_1, \dots, X_n$ under $X_i \sim P^{(i)}(\cdot \mid X_{1:i-1})$:

$$\mathbb P(x) = \prod_{i=1}^n P^{(i)}(x_i \mid x_{1:i-1}).$$

For a second family $Q$ with law $\mathbb Q$, the quantity controlled by per-step estimation is

$$\mathbb E_{\mathbb P}\Big[\sum_{i=1}^n D^2_{\mathrm H}\big(P^{(i)}(\cdot \mid X_{1:i-1}), Q^{(i)}(\cdot \mid X_{1:i-1})\big)\Big].$$

In Lean these are IsSeqKernel, seqLaw and condHellingerSum, with hellingerSq and klDivDiscrete the published discrete divergences.

Formalization targets

Goal: Lemma A.13, (97), for $n \ge 2$

$$D^2_{\mathrm H}(\mathbb P, \mathbb Q) \le 10^2 \log(n) \cdot \mathbb E_{\mathbb P}\Big[\sum_{i=1}^n D^2_{\mathrm H}\big(P^{(i)}(\cdot \mid X_{1:i-1}), Q^{(i)}(\cdot \mid X_{1:i-1})\big)\Big].$$

The constant $10^2$ is the paper's; the shape that matters downstream is the logarithmic dependence on $n$ with no assumption on the kernels beyond their being probability kernels.

Companion: Lemma A.13, (98)

If $V \ge e$ and $P^{(i)}(A \mid x_{1:i-1}) \le V\, Q^{(i)}(A \mid x_{1:i-1})$ for every $i$, prefix and event $A$, then $D^2_{\mathrm H}(\mathbb P, \mathbb Q) \le 3\log(V) \cdot \mathbb E_{\mathbb P}[\sum_i D^2_{\mathrm H}(P^{(i)}, Q^{(i)})]$.

Milestones

1. Lemma A.10 (p. 72): $D_{\mathrm{KL}}(p\,\|\,q) \le (2 + \log V)\, D^2_{\mathrm H}(p, q)$ under a likelihood-ratio bound $V$ (referenced, finite case).
2. Lemma A.5 (p. 71): $D^2_{\mathrm{TV}} \le D^2_{\mathrm H} \le D_{\mathrm{KL}}$ (referenced, finite case).
3. The triangle inequality for $D_{\mathrm H}$ (proof of Lemma A.13, p. 73).
4. The chain rule $D_{\mathrm{KL}}(\mathbb Q\,\|\,\mathbb P) = \mathbb E_{\mathbb Q}[\sum_i D_{\mathrm{KL}}(Q^{(i)}\,\|\,P^{(i)})]$ for sequential laws (p. 73).
5. Convexity of $D^2_{\mathrm H}$ in its second argument (p. 74).
6. Lemma A.11 (p. 72), the multiplicative Pinsker-type inequality: $|\mathbb E_P h - \mathbb E_Q h| \le \sqrt{2R(\mathbb E_P h + \mathbb E_Q h) D^2_{\mathrm H}(P, Q)}$ and $\mathbb E_P h \le 3\mathbb E_Q h + 4R\, D^2_{\mathrm H}(P, Q)$ for $0 \le h \le R$.

Significance

The result. Inequality (97) converts per-round Hellinger estimation error into a bound on the Hellinger distance between the laws of complete interaction histories, under no boundedness assumption on likelihood ratios. In the paper this is the step that lets the lower bound of Theorem 3.2 relate any algorithm's behaviour under a reference model to its behaviour under alternatives, and hence express the minimax regret through the decision-estimation coefficient. Without it, only the KL chain rule is available, which requires bounded likelihood ratios (the situation of (98)) or loses more than a logarithmic factor. Lemma A.11, a milestone here, is used independently in the same lower bound and in the paper's tabular reinforcement learning analysis.

Formalizing it. The lemma is proved in the paper; no machine-checked proof exists. The published layer on the platform has the discrete divergences and the comparisons of Lemmas A.5 and A.10; the sequential-law objects, the triangle inequality, the convexity of $D^2_{\mathrm H}$, the discrete chain rule and Lemma A.11 are new. A completed development gives a reusable chain-rule toolkit for any later formalization of lower bounds over adaptive interaction histories.

Difficulty

The squared Hellinger distance does not tensorize along adaptive sequences: the natural attempt to write $1 - \tfrac12 D^2_{\mathrm H}(\mathbb P, \mathbb Q)$ as a product of conditional affinities fails because the conditional affinities are random, depending on the prefix, and their expectation does not factor. Bounding $D^2_{\mathrm H}$ by $D_{\mathrm{KL}}$ and applying the KL chain rule fails in the other direction: the conditional KL divergences are not controlled by the conditional Hellinger distances unless the likelihood ratios are bounded, and in (97) they are not. The difficulty is to obtain a bound that pays only $\log n$ for an unbounded ratio, with explicit constants that survive the final numerical comparison.

Formalization scope

• Finite alphabets. The paper works over measurable spaces. This mission formalizes the finite-alphabet case, as the published FoundationsRL divergence layer does: each $\mathcal X_i$ is a Fintype, distributions are probability vectors, expectations are finite sums. Coordinates are indexed by Fin n (0-based) and the alphabets may differ from coordinate to coordinate.
• Kernels. A kernel family is a function P i x of the whole sequence that is a probability vector and depends only on the coordinates j < i; this is what makes seqLaw P the law the paper describes.
• Added hypothesis $n \ge 2$ in (97). The paper states (97) for every $n$; at $n = 1$ the right side vanishes because $\log 1 = 0$ while the left side is positive whenever $P^{(1)} \ne Q^{(1)}$, and the proof's last step $2(6\log(96n) + \tfrac{18}{96n}) \le 10^2\log n$ holds only for $n \ge 2$. The goal is stated for $n \ge 2$, with the constant unchanged.
• Likelihood ratios are stated multiplicatively, $P(A) \le V\,Q(A)$, so that a zero denominator does not make a hypothesis vacuous; KL divergences are compared to Hellinger distances in $[0, \infty]$.
• Lemma A.11 holds "almost surely under $P$ and $Q$", which becomes: $0 \le h \le R$ at every point charged by $P$ or $Q$.
• Ruling out trivial forms. The goal's hypotheses are satisfiable with $\mathbb P \ne \mathbb Q$ and $n \ge 2$ (checked in a sanity file). A formalization in which the kernels may read coordinates beyond the prefix, in which $\log$ is applied to $n \le 1$, or in which the ratio bound of (98) is checked through a quotient that is vacuous at zero denominators, is not the paper's statement.

Contributions welcome: proofs of any milestone and of the fact that seqLaw is a probability vector.

Selected references

• D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv:2112.13487v3, 2023. https://arxiv.org/abs/2112.13487
• Y. Yang, A. Barron, An asymptotic property of model selection criteria, IEEE Transactions on Information Theory 44(1), 1998. https://doi.org/10.1109/18.650993
• Y. Polyanskiy, Y. Wu, Lecture Notes on Information Theory, 2014. https://people.lids.mit.edu/yp/homepage/data/itlectures_v5.pdf
• D. J. Foster, A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, arXiv:2312.16730v1, 2023. https://arxiv.org/abs/2312.16730

Motivation

Neural networks trained by empirical risk minimization are sensitive to small, deliberately chosen perturbations of their inputs ("adversarial examples"). A standard defence is adversarial training: at each step, perturb the training example to increase the loss, then take a gradient step at the perturbed point. Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571, ICLR 2018) recast adversarial training as distributionally robust optimization over a Wasserstein ball around the data distribution, and replaced the hard ball constraint by a Lagrangian penalty. The resulting procedure perturbs each example by solving a penalized inner maximization, and the paper shows that, when the penalty is large enough relative to the smoothness of the loss, this inner problem is strongly concave and therefore tractable.

This mission formalizes the paper's computational guarantee, Theorem 2: stochastic gradient descent on the penalized robust objective, with an inexact adversary, reaches an approximate stationary point at the rate of smooth nonconvex stochastic optimization. The analysis follows Ghadimi and Lan's argument for nonconvex SGD (arXiv:1309.5549), adapted to a gradient oracle that is biased by the inexact inner maximization.

Setting

Parameters $\theta$ live in $\Theta=\mathbb R^d$ and data in a set $Z\subseteq\mathbb R^m$; both spaces carry the Euclidean norm $\|\cdot\|_2$. Data are drawn from a probability distribution $P_0$ on $Z$.

A transportation cost $c:Z\times Z\to[0,\infty)$ measures how expensive it is to move a data point $z_0$ to $z$. Assumption A: $c$ is continuous, $c(z,z)=0$, and for each $z_0\in Z$ the map $z\mapsto c(z,z_0)$ is $1$-strongly convex. The canonical example is $c(z,z_0)=\tfrac12\|z-z_0\|_2^2$.

A loss $\ell(\theta;z)$ has partial gradients $\nabla_\theta\ell$ and $\nabla_z\ell$. Assumption B: these gradients are Lipschitz in each argument,

$$\|\nabla_\theta\ell(\theta;z)-\nabla_\theta\ell(\theta';z)\|\le L_{\theta\theta}\|\theta-\theta'\|,\quad \|\nabla_z\ell(\theta;z)-\nabla_z\ell(\theta;z')\|\le L_{zz}\|z-z'\|,$$ $$\|\nabla_\theta\ell(\theta;z)-\nabla_\theta\ell(\theta;z')\|\le L_{\theta z}\|z-z'\|,\quad \|\nabla_z\ell(\theta;z)-\nabla_z\ell(\theta';z)\|\le L_{z\theta}\|\theta-\theta'\|.$$

For a penalty $\gamma>0$, the robust surrogate and the robust objective are

$$\varphi_\gamma(\theta;z_0)=\sup_{z\in Z}\{\ell(\theta;z)-\gamma c(z,z_0)\},\qquad F(\theta)=\mathbb E_{P_0}[\varphi_\gamma(\theta;Z)].$$

By Wasserstein duality, $F(\theta)$ equals the worst-case expected loss over all distributions $P$, penalized by $\gamma$ times the transport distance from $P$ to $P_0$.

Algorithm 1 (with $\Theta=\mathbb R^d$ and constant stepsize $\alpha$): from $\theta^0$, for $t=0,\dots,T-1$, draw $z^t\sim P_0$ independently, find an $\epsilon$-approximate maximizer $\hat z^t\in Z$, meaning $\ell(\theta^t;\hat z^t)-\gamma c(\hat z^t,z^t)\ge\varphi_\gamma(\theta^t;z^t)-\epsilon$, and set $\theta^{t+1}=\theta^t-\alpha\nabla_\theta\ell(\theta^t;\hat z^t)$.

Formalization targets

Goal: Theorem 2 (p. 6)

Let $\gamma>L_{zz}$, $L_\varphi=L_{\theta\theta}+L_{\theta z}L_{z\theta}/(\gamma-L_{zz})$, $\Delta_F\ge F(\theta^0)-\inf_\theta F(\theta)$, and assume $\mathbb E\|\nabla F(\theta)-\nabla_\theta\varphi_\gamma(\theta;Z)\|_2^2\le\sigma^2$ for all $\theta$. With $\alpha=\sqrt{\Delta_F/(L_\varphi T\sigma^2)}$ and $T\ge L_\varphi\Delta_F/\sigma^2$,

$$\frac1T\sum_{t=0}^{T-1}\mathbb E\big[\|\nabla F(\theta^t)\|_2^2\big]-\frac{4L_{\theta z}^2}{\gamma-L_{zz}}\,\epsilon\le4\sigma\sqrt{\frac{L_\varphi\Delta_F}{T}}.$$

Milestones

1. (4), p. 4: for $\gamma\ge L_{zz}$, $z\mapsto\ell(\theta;z)-\gamma c(z,z_0)$ is $(\gamma-L_{zz})$-strongly concave.
2. Lemma 1, p. 5: the supremum $\bar f(\theta)=\sup_{z\in Z}f(\theta,z)$ of a $\lambda$-strongly concave family satisfying Assumption B is differentiable, with $\nabla\bar f(\theta)=\nabla_\theta f(\theta,z_\star(\theta))$, a $(L_{z\theta}/\lambda)$-Lipschitz maximizer and a $(L_{\theta\theta}+L_{\theta z}L_{z\theta}/\lambda)$-Lipschitz gradient.
3. §2.1, p. 6: $\varphi_\gamma(\cdot;z_0)$ has $L_\varphi$-Lipschitz gradient $\nabla_\theta\varphi_\gamma(\theta;z_0)=\nabla_\theta\ell(\theta;z_\star(z_0,\theta))$.
4. (31) and (32), p. 40: the descent inequality for an $L_\varphi$-smooth objective, and its form with the bias $\delta=g-\nabla_\theta\varphi_\gamma$ separated, for $\alpha\le1/L_\varphi$.
5. The bias bound, p. 41: $\|\delta\|_2^2\le 2L_{\theta z}^2\epsilon/(\gamma-L_{zz})$.
6. The one-step bound in conditional expectation and the averaged bound, p. 41:

$$\frac1T\sum_{t<T}\mathbb E\|\nabla F(\theta^t)\|_2^2\le2\hat\epsilon+\frac{2\Delta_F}{\alpha T}+2L_\varphi\alpha\sigma^2,\qquad\hat\epsilon=\frac{2L_{\theta z}^2}{\gamma-L_{zz}}\epsilon,$$

for every constant stepsize $0<\alpha\le1/L_\varphi$. The goal is this bound at the balancing stepsize.

Significance

The result. Theorem 2 certifies that the robust training procedure is no harder, in iteration count, than ordinary nonconvex SGD: the stationarity measure decays as $T^{-1/2}$, and the inexactness of the adversary enters only as an additive term proportional to $\epsilon$, independent of $T$. This is what licenses running a few steps of gradient ascent for the inner problem rather than solving it exactly. It also explains the role of the penalty: the guarantee requires $\gamma>L_{zz}$, so smoothness of the loss in the data (smooth activations rather than ReLUs) is what makes the robust problem tractable.

Formalizing it. The result and its proof are published; nothing here is open. To our knowledge none of it is machine-checked. A formal proof would add a verified Danskin-type theorem for strongly concave suprema with explicit Lipschitz constants (Lemma 1), which is reusable well beyond this paper, and a verified nonconvex SGD analysis with a biased oracle, including the measure-theoretic bookkeeping (independence of the fresh sample from the current iterate, differentiation under the integral) that the paper's proof compresses into one line.

Difficulty

The deterministic inequalities (31), (32) and the bias bound are short. The weight sits elsewhere. First, Lemma 1 requires differentiability of a supremum over a possibly unbounded set, with the maximizer depending on $\theta$; the paper invokes a Danskin-type theorem that is not in Mathlib, and the cost $c$ is not assumed differentiable, so the first-order optimality conditions for the inner problem must be derived from strong convexity alone. Second, the expectation step uses $\mathbb E[\nabla_\theta\varphi_\gamma(\theta^t;z^t)\mid\theta^t]=\nabla F(\theta^t)$, which needs both differentiation under the integral sign for $F$ and the independence of $z^t$ from $\theta^t$ along the run. Third, finiteness of every expectation along the run is not assumed and must be propagated from step to step.

Formalization scope

Lean representation: $\Theta$ and $\mathbb R^m$ are EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m); $Z$ is a set in the latter. The loss is a function on all of $\mathbb R^d\times\mathbb R^m$; its partial gradients are required at points of $Z$ and the Lipschitz conditions on $Z$ only. Strong convexity is Mathlib's StrongConvexOn, whose modulus convention matches the paper. Suprema are sSup over the image of $Z$. $F$ is a Bochner integral, and $\varphi_\gamma(\theta;\cdot)$ is assumed $P_0$-integrable for every $\theta$. The run is driven by $(z^0,\dots,z^{T-1})\sim P_0^{\otimes T}$ (Measure.pi). The expectations in the conclusion and in the variance hypothesis are lower Lebesgue integrals in $[0,\infty]$; the $\epsilon$-term of Theorem 2 is moved to the right-hand side.

Hypotheses made explicit that the paper leaves implicit: $\gamma>L_{zz}$ (the paper writes $\gamma\ge L_{zz}$ but divides by $\gamma-L_{zz}$); $Z$ nonempty, convex and closed; Lipschitz constants nonnegative; $\sigma>0$, $\Delta_F>0$, $T\ge1$, $\epsilon\ge0$; $F$ bounded below (so $\inf_\theta F$ is a real number); integrability of $\varphi_\gamma(\theta;\cdot)$; $P_0(Z)=1$; joint measurability of the oracle $(\theta,z_0)\mapsto\hat z(\theta,z_0)$; and, in (32) and the later milestones, $0<\alpha\le1/L_\varphi$, which the paper assumes "in the rest of the proof". Lemma 1 is specialized to the Euclidean norm, the case Theorem 2 uses. The cost $c$ is not assumed differentiable.

A trivializing formalization is ruled out: the run uses an oracle tied to $\varphi_\gamma$ by the $\epsilon$-gap and to $Z$ by membership, $\varphi_\gamma$ is the supremum of the penalized loss over $Z$, $F$ is its $P_0$-integral, and the hypotheses are satisfiable (for instance $\ell(\theta;z)=\tfrac12\|\theta\|^2$, $c(z,z_0)=\tfrac12\|z-z_0\|^2$, $Z=\mathbb R^m$, $P_0$ a point mass, $\epsilon=0$). Expectations as lower integrals prevent a non-integrable $\|\nabla F(\theta^t)\|^2$ from being read as $0$.

Infrastructure a complete development needs: the descent lemma for functions with Lipschitz gradient; first-order characterizations of strong concavity on a convex set; a Danskin/envelope theorem for strongly concave suprema; differentiation under the integral for $F$; and conditional-expectation bookkeeping for Markov-type recursions driven by i.i.d. samples on a finite product space. The first three are reusable in any minimax or bilevel analysis. Contributions to any milestone, or to these supporting facts as separate lemmas, are welcome.

Selected references

• A. Sinha, H. Namkoong, R. Volpi, J. Duchi, Certifying Some Distributional Robustness with Principled Adversarial Training, ICLR 2018; arXiv:1710.10571v5, 2020. https://arxiv.org/abs/1710.10571
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. https://doi.org/10.1137/120880811
• J. F. Bonnans, A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research 48(2), 2023; arXiv:1604.02199. https://arxiv.org/abs/1604.02199

Motivation

Distributionally robust optimization (DRO) evaluates a decision against a collection of probability distributions near an empirical one. In a finite scenario model, the familiar construction puts a divergence ball around the histogram of observed scenarios. Lam's empirical construction instead gives one weight to each observation, even when several observations have the same value. The distinction matters because a sample can contain repeated values and can omit some points of the stated support. The paper uses a Burg-entropy ball on those observation weights to recover statistical guarantees for an expected loss, despite the empirical ball having low probability of containing the true distribution. Lam, §§2.1–2.3, pp. 5–9.

Proposition 1 identifies what this observation-level construction becomes when the random quantity has finite support: its lower and upper DRO values coincide with values from a Burg-divergence ball on the support histogram. This links a method defined on individual data points to the standard finite-scenario formulation. The radius uses a one-degree-of-freedom chi-square quantile because the paper calibrates an expected value at a fixed decision; it does not use the $k-1$ degrees of freedom associated with estimating a full $k$-point distribution. Lam, Proposition 1, p. 11, and the discussion on pp. 8–9.

Setting

Fix a decision $x$ and a real loss $h(x;s_i)$ at each of $k$ support points $s_1,\ldots,s_k$. A sample of size $n$ has an assignment $c(j)$ telling which support point produced observation $j$. Write $n_i$ for the number of assignments to point $i$ and $\hat p_i=n_i/n$ for the empirical histogram. The support points need not all appear in the sample. The decision and loss only determine a finite vector of loss values; no probability space is needed for this deterministic comparison. Lam, §2.1, p. 6, and Proposition 1, p. 11.

The empirical Burg ball $\mathcal U_n(\eta)$ consists of observation weights $w_1,\ldots,w_n$ that are nonnegative, sum to one, and obey $-n^{-1}\sum_j\log(nw_j)\le\eta$. The support Burg ball $\mathcal U'_{\mathrm{Burg}}(\eta)$ consists of support weights $p_1,\ldots,p_k$ that are nonnegative, sum to one, are absolutely continuous with respect to $\hat p$, and obey $-\sum_i\hat p_i\log(p_i/\hat p_i)\le\eta$. At an observed point, finite Burg divergence requires $p_i>0$; at an unobserved point, absolute continuity requires $p_i=0$. Lam, (13)–(15), pp. 5–6; (19), p. 8; (28), p. 11.

For a support weight vector $p$, the expected loss is $\sum_i p_i h(x;s_i)$. For an observation weight vector $w$, it is $\sum_j w_j h(x;s_{c(j)})$. The empirical lower and upper values are the minimum and maximum over $\mathcal U_n(\eta)$; the support values use $\mathcal U'_{\mathrm{Burg}}(\eta)$. The same empirical ball is used for both bounds. Lam, (26)–(28), p. 11.

Formalization targets

The goal is Proposition 1. For every $n>0$, every assignment of the sample to finite support points, every fixed decision $x$, and every $\kappa\ge0$, set $\eta=\kappa/(2n)$. Then

$$\min_{w\in\mathcal U_n(\eta)}\sum_{j=1}^n w_jh(x;s_{c(j)}) =\min_{p\in\mathcal U'_{\mathrm{Burg}}(\eta)}\sum_{i=1}^k p_ih(x;s_i),$$ $$\max_{w\in\mathcal U_n(\eta)}\sum_{j=1}^n w_jh(x;s_{c(j)}) =\max_{p\in\mathcal U'_{\mathrm{Burg}}(\eta)}\sum_{i=1}^k p_ih(x;s_i).$$

The printed proposition takes $\kappa=\chi^2_{1,1-\alpha}$. The deterministic identity holds at every nonnegative $\kappa$, including zero. The two milestones record the source proof's statements that a feasible support vector gives a feasible observation vector with the same objective value, and conversely that a feasible observation vector gives a feasible support vector with the same objective value. Lam, Proposition 1, p. 11, proof p. 24.

Significance

The identity lets a finite-support user compute the empirical DRO values with one variable per distinct support point instead of one per observation, without changing either bound. It also shows precisely how Lam's empirical calibration relates to a conventional histogram-based divergence model: the ambiguity sets have different coordinates, but the resulting extrema of any loss constant on each class agree. This is the finite-support interpretation stated immediately after Theorem 2, and it explains the radius comparison on pp. 8–9. Lam, pp. 8–9 and Proposition 1, p. 11.

The result is proved in the paper; the remaining task is a machine-checked proof of the two transformations and the equality of extrema. The published formal library already contains the observation-level $\phi$-divergence ball and its robust upper mean, and a shared setting supplies the Burg generator and lower empirical value. This mission adds the support histogram, its Burg ball, and the bridge between the two representations. Those definitions and transformations can also be reused for other finite-support losses. The paper's separate pointwise coverage and consistency results are goals of other missions in this series. Lam, Theorems 2–3 and Proposition 1, pp. 11–12.

Difficulty

Repeated observations make the two weight spaces different: the empirical problem has $n$ coordinates and the support problem has $k$. Simply identifying coordinates loses multiplicities in both the normalization and the logarithmic divergence. Empty classes create a second boundary case, since no observation weight can be assigned to an unobserved support point. A statement that silently permits such mass changes the support optimization value. The full reduction must preserve feasible objective values in both directions, for the lower and upper extrema. Lam, proof of Proposition 1, p. 24.

Formalization scope

Lean uses Fin n for observations and Fin k for support points, with zero-based indices, a class map $c$, real loss values, and the paper's Burg generator valued in EReal. Nonpositive likelihood ratios receive $+\infty$. The empirical ball reuses the published PhiDivRobust.Counterpart.probUncertaintySet; its upper value is the published GenEmpLik.Expansion.robustMean. The lower value is a real infimum over the same ball. The condition $n>0$ and the nonnegative radius make both feasible value sets nonempty and bounded, so the real infimum and supremum mean the paper's minimum and maximum. The histogram can have zero entries. Lam, (19), (26)–(28), pp. 8, 11.

Display (28) omits a condition from the preceding definition of a divergence ball: $p$ must be absolutely continuous with respect to $\hat p$. Without it, an unobserved support point can receive positive mass and Proposition 1 is false. The formal support ball includes $\hat p_i=0\Rightarrow p_i=0$ from (13)–(14). It also requires $p_i>0$ where $\hat p_i>0$, because Lean's real logarithm returns zero at zero whereas the paper's Burg divergence is infinite there. These conditions, together with $n>0$, exclude trivial values from empty balls, division by zero, and logarithms at invalid weights. The decision set $\Theta$ is omitted because the paper fixes one $x$ and the result holds for every such $x$. Lam, (13)–(14), pp. 5–6, and (28), p. 11.

The development needs finite-sum identities, elementary properties of the probability simplex, the logarithm's concavity, and bounds on the extrema of bounded nonempty finite-dimensional value sets. Contributions that establish the two direction statements, or reusable facts about aggregation of finite probability weights, directly advance this mission. The paper's uniform calibration theorem, Theorem 4, is outside this scope: it needs a Donsker class, a data-dependent chi-square process, and its supremum quantile, none of which enters Proposition 1. Lam, Theorem 4, pp. 13–14.

Selected references

• Henry Lam, Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization, arXiv:1605.09349v1, 2016; published in Operations Research 67(4), 2019. arXiv, DOI.

Motivation

A prophet inequality compares an online decision maker, who sees random inputs one at a time and must commit irrevocably, with a "prophet" who sees all inputs in advance. The classic single-item version (Krengel–Sucheston, Samuel-Cahn) says that a well-chosen fixed threshold earns at least half of the expected maximum. In mechanism design the same statement reads: a posted-price mechanism, which offers each arriving buyer a take-it-or-leave-it menu of prices, extracts a constant fraction of the optimal expected welfare, and does so in a way that is truthful, simple and order oblivious.

Dütting, Feldman, Kesselheim and Lucier (SIAM J. Comput. 49 (2020)) reduce the construction of such prices to a deterministic question. If, for every fixed valuation profile $v$, one can find prices $p^v$ that are balanced — high enough to pay for the welfare an early allocation destroys, low enough that whatever is still feasible stays affordable — then the expected prices $\mathbb E_{\tilde v}[p^{\tilde v}]$, suitably scaled, give a prophet inequality. This is their Theorem 3.2 for $(\alpha,\beta)$-balanced prices. For combinatorial auctions with bundles of size at most $d$, MPH-$k$ valuations and related settings, the natural prices only satisfy a weaker condition, in which the affordability bound may also spend a multiple of the benchmark welfare. Theorem 3.5, the subject of this mission, is the extension theorem for that weak balancedness; it is what turns the paper's Theorem 4.1 (bundle size $d$) and Theorem 1.6 (MPH-$k$) into $O(d)$- and $O(k)$-approximate posted-price mechanisms.

Setting

There are $n$ agents $N=\{1,\dots,n\}$. Agent $i$ has an outcome space $X_i$ containing a null outcome $\emptyset$; outcome profiles are $x\in X=X_1\times\cdots\times X_n$. For $S\subseteq N$, $x_S$ gives $x_i$ to the agents in $S$ and $\emptyset$ to the others, and $x_{[i-1]}$ keeps only the agents before $i$. The feasible profiles form a set $\mathcal F\subseteq X$ that is downward closed ($x\in\mathcal F\Rightarrow x_S\in\mathcal F$).

Agent $i$ has a valuation $v_i:X_i\to[0,1]$, drawn independently from a known distribution $\mathcal D_i$; $\mathcal D=\prod_i\mathcal D_i$. The welfare of $x$ is $v(x)=\sum_i v_i(x_i)$, and $v(\mathrm{OPT}(v,S))=\sup_{x\in S}v(x)$ (zero on $S=\emptyset$). An allocation rule $\mathrm{ALG}$ maps every valuation profile to a feasible outcome.

A pricing rule assigns prices $p_i(x_i\mid y)\in[0,\infty]$ to outcome $x_i$ offered to agent $i$ given the partial allocation $y$, with $p_i(x_i\mid y)=\infty$ when $(x_i,y_{-i})\notin\mathcal F$. In the posted-price mechanism the agents are approached in index order; agent $i$ sees the prices $p_i(\cdot\mid x_{[i-1]})$ and buys a utility-maximizing outcome, utility being $v_i(x_i)-p_i(x_i\mid x_{[i-1]})$.

A family $(\mathcal F_x)_{x\in X}$ of sets of profiles is exchange compatible if $(y_i,x_{-i})\in\mathcal F$ for every $x\in X$, $y\in\mathcal F_x$ and $i$. Given $\alpha>0$ and $\beta_1,\beta_2\ge0$, a pricing rule $p^v$ is weakly $(\alpha,\beta_1,\beta_2)$-balanced (Definition 3.4) with respect to $\mathrm{ALG}$ and $(\mathcal F_x)$ if for every $x\in\mathcal F$

$$\text{(a)}\quad \sum_i p^v_i(x_i\mid x_{[i-1]})\ \ge\ \tfrac1\alpha\bigl(v(\mathrm{ALG}(v))-v(\mathrm{OPT}(v,\mathcal F_x))\bigr),$$ $$\text{(b)}\quad \sum_i p^v_i(x'_i\mid x_{[i-1]})\ \le\ \beta_1\,v(\mathrm{OPT}(v,\mathcal F_x))+\beta_2\,v(\mathrm{ALG}(v))\quad\text{for all }x'\in\mathcal F_x.$$

A collection $(p^v)_{v}$ is weakly balanced if one exchange-compatible family works for every $v$.

Formalization targets

Goal: Theorem 3.5 (p. 551)

If $(p^v)_v$ is weakly $(\alpha,\beta_1,\beta_2)$-balanced with $\beta_1+\beta_2\ge1/\alpha$, then with

$$\delta=\frac1{\beta_1+\max\{2\beta_2,1/\alpha\}},\qquad p_i(x_i\mid y)=\mathbb E_{\tilde v}\bigl[p^{\tilde v}_i(x_i\mid y)\bigr],$$

the posted-price mechanism with prices $\delta p$, approaching agents in index order, satisfies

$$\mathbb E_v\Bigl[\sum_i v_i(x_i(v))\Bigr]\ \ge\ \frac1{\alpha(2\beta_1+4\beta_2)}\,\mathbb E_v\bigl[v(\mathrm{ALG}(v))\bigr].$$

Milestones (Appendix A, pp. 559–560)

1. Each agent's utility in the run is nonnegative.
2. (A.1): the total expected utility is at least the value of a ghost-sample deviation $x'(v,v')\in\mathcal F_{x(v)}$ minus its expected price.
3. (A.2): property (b) bounds that price by $\delta\beta_1\mathbb E[\tilde v(\mathrm{OPT}(\tilde v,\mathcal F_{x(v)}))]+\delta\beta_2\mathbb E[\tilde v(\mathrm{ALG}(\tilde v))]$.
4. (A.3): $\mathbb E[\sum_iu_i]\ge(1-\delta\beta_1)\,\mathbb E[\tilde v(\mathrm{OPT}(\tilde v,\mathcal F_{x(v)}))]-\delta\beta_2\,\mathbb E[\tilde v(\mathrm{ALG}(\tilde v))]$.
5. (A.4): property (a) bounds the expected revenue from below.
6. Case 1, $\beta_2\ge1/(2\alpha)$, $\delta=1/(\beta_1+2\beta_2)$: the goal's bound.
7. Case 2, $\beta_2<1/(2\alpha)$, $\delta=1/(\beta_1+1/\alpha)$: the bound with constant $(1-\alpha\beta_2)/(1+\alpha\beta_1)$.
8. Case 2's last step: $(1-\alpha\beta_2)/(1+\alpha\beta_1)\ge1/(\alpha(2\beta_1+4\beta_2))$ under the theorem's constraints.

Significance

The result. Theorem 3.5 is the second of the paper's two extension theorems. Its hypothesis is a deterministic, full-information property of prices, which is often checkable by a direct combinatorial argument; its conclusion is a Bayesian guarantee for an online, truthful mechanism. The paper instantiates it with weakly $(1,1,d-1)$-balanced fractional prices for combinatorial auctions with bundle size at most $d$ (Theorem 4.1) and for MPH-$k$ valuations (Theorem 1.6), obtaining approximation ratios linear in $d$ and $k$, where $(\alpha,\beta)$-balancedness alone would not apply.

Formalizing it. The theorem is proved on paper; no machine-checked version exists. The mission produces a formal account of the sequential posted-price mechanism with history-dependent prices (an online run defined by recursion over the agents), of the ghost-sample argument, and of the case analysis in $\delta$. The definitions are general enough that the paper's applications — and other balanced-price arguments — can be stated on top of them. The printed proof has a slip: (A.1) is printed as an equality but only the inequality "$\ge$" holds; the formalization states the inequality.

Difficulty

Two steps carry the content. First, the utility bound (A.1): agent $i$ could have bought its part of the deviation $x'(v,v')$, but that deviation is defined from the run on a different profile. The argument needs that the partial allocation $x_{[i-1]}(v)$ does not depend on $v_i$ — the mechanism is online — and that exchanging $v_i$ with an independent copy $v'_i$ preserves the joint law. Making this exchange rigorous on a product measure, and handling an empty $\mathcal F_{x(v)}$ (where no deviation exists and the bound must come from $u_i\ge0$), is where the work lies. Second, $v(\mathrm{OPT}(v,\mathcal F_x))$ is a supremum that need not be attained, so "buy your part of OPT" must be replaced by near-optimal selections and a limit.

The tempting shortcut of treating weak balancedness as $(\alpha,\beta_1+\beta_2)$-balancedness and applying Theorem 3.2 does not work: property (b) of Definition 3.1 bounds prices by a multiple of $v(\mathrm{OPT}(v,\mathcal F_x))$ alone, which can be zero while $v(\mathrm{ALG}(v))$ is not.

Formalization scope

Agents are Fin n, 0-based: the paper's agent $i$ is index $i-1$, and "the order they are indexed" is the order of Fin n. Prices take values in ENNReal with $\infty=\top$; price sums are never converted to reals, and property (a) passes its right side through ENNReal.ofReal (a negative bound becomes $0$, which is the page's meaning). $v(\mathrm{OPT}(v,S))$ is the real supremum sSup, zero on the empty set, meaningful because values lie in $[0,1]$.

Valuations are given by type spaces $V_i$ and an evaluation $\mathrm{val}_i(w,x_i)\in[0,1]$. The type spaces are countable with discrete σ-algebras — a disclosed restriction of the paper's general distributions, which makes every function measurable and every bounded one integrable. The null outcome is assumed free at feasible partial allocations ($p^{\tilde v}_i(\emptyset\mid y)=0$ for $y\in\mathcal F$): every pricing rule in the paper has this property, and the proof needs its consequence $u_i(v)\ge0$. Exchange compatibility is required for all $x\in X$, as printed. The agents' behaviour is a choice rule that sees only the agent's own type and the earlier agents' outcomes and maximizes utility at every feasible partial allocation; at infeasible ones no requirement is made. The constant $\delta$ is written literally inside the posted prices, never as a free parameter.

The milestones (A.1)–(A.4) are stated for an arbitrary $\delta>0$, and (A.1)–(A.2) for an arbitrary selector into $\mathcal F_{x(v)}$ in place of the maximizer, with an explicit zero when $\mathcal F_{x(v)}=\emptyset$; both are generalizations of the printed steps. A statement in which the agents' optimality hypothesis can never be met, or in which an infinite price sum is read as $0$, would make the goal vacuous; the encoding above excludes both, and a sorry-free one-agent instance in the workspace confirms that all hypotheses of the goal can hold together.

Needed infrastructure: product measures and the swap of one coordinate with an independent copy, lower integrals of ENNReal-valued prices, the recursion defining the run, and near-maximizers of bounded suprema. The model and mechanism definitions are reusable for the paper's other extension theorem (Theorem 3.2) and its applications. Contributions are welcome on any milestone; the pure inequality of Case 2 is self-contained.

Selected references

• P. Dütting, M. Feldman, T. Kesselheim, B. Lucier, Prophet inequalities made easy: Stochastic optimization by pricing nonstochastic inputs, SIAM Journal on Computing 49(3):540–582, 2020. https://doi.org/10.1137/20M1323850
• U. Krengel, L. Sucheston, Semiamarts and finite values, Bulletin of the AMS 83(4):745–747, 1977. https://doi.org/10.1090/S0002-9904-1977-14378-4
• E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Annals of Probability 12(4):1213–1216, 1984. https://doi.org/10.1214/aop/1176993150
• R. Kleinberg, S. M. Weinberg, Matroid prophet inequalities, STOC 2012, 123–136. https://doi.org/10.1145/2213977.2213991

Why reduce scenarios with the cost in view

A two-stage stochastic programme chooses a decision $z$ before an uncertain parameter $\xi$ is revealed and pays a cost $c(z;\xi)$. When $\xi$ is known only through $n$ data points, or through a law with many atoms, the expected cost is expensive to optimize, and practitioners replace the law by a small set of $m$ reduced scenarios. Classical scenario reduction chooses these scenarios to be close to the data in a Wasserstein distance, without looking at the cost (Dupačová, Gröwe-Kuska and Römisch, 2003; Rujeerapaiboon, Schindler, Kuhn and Wiesemann, 2022). Bertsimas and Mundru (Operations Research, 2023) propose problem-dependent scenario reduction: the distance between two scenarios measures how much the optimal decision for one costs when evaluated on the other. Their method needs, for each cluster of data, the scenario that minimizes a cost-dependent dissimilarity, which they replace by a convex upper bound, problem (16).

Theorem 3 of the paper is the sanity check for that upper bound. For the simplest cost to which it applies and a single reduced scenario ($m=1$), under a symmetry assumption on the law, the minimizer of the upper bound is the mean of $\xi$, which is also what Wasserstein scenario reduction returns for $m=1$. This mission formalizes that statement.

Setting

Decisions and parameters both live in $\mathbb R^d$, with the Euclidean inner product $z'\xi$. The feasible set is a polytope

$$\mathcal Z = \{ z\in\mathbb R^d_+ : Pz\le q\},$$

for a matrix $P\in\mathbb R^{r\times d}$ and a vector $q\in\mathbb R^r$, assumed nonempty and bounded. The cost is $c(z;\xi)=\max\{z'\xi,0\}$, a special case of the piecewise bilinear costs $\max_{1\le t\le k} z'A_t\xi$ of (15) (take $k=2$, $A_1=I$, $A_2=0$).

An optimal-decision map is any function $z^*:\mathbb R^d\to\mathbb R^d$ with $z^*(\xi)\in\arg\min_{z\in\mathcal Z} z'\xi$ for every $\xi$; for a vector $v$, $\mathcal Z^*(v)=\arg\min_{z\in\mathcal Z} z'v$ is the whole set of minimizers. The set of cost-reducing parameters is

$$\mathcal U=\Big\{\xi : \min_{z\in\mathcal Z} z'\xi<0\Big\}.$$

For a candidate reduced scenario $\zeta\in\mathbb R^d$, the per-scenario upper-bound loss is

$$L(\xi,\zeta)=\max\Big\{\max_{z\in\mathcal Z} z'(\xi-2\zeta),\,0\Big\}+2\max\{z^*(\xi)'\zeta,\,0\}.$$

For this cost it is the optimal value, in the auxiliary variables $(\lambda,\theta,\gamma)$, of the per-point linear programme in (16). With a random parameter $\xi$ of law $\mu$, the upper-bound objective for $m=1$ is $\mathbb E[L(\xi,\zeta)]$. The squared cost for Wasserstein reduction to one atom is $W(\zeta)=\int\|\xi-\zeta\|_2^2\,d\mu$; (4) takes its square root, which preserves minimizers.

Assumption 5 (p. 24) asks:

• (a) $\xi$ has a continuous distribution on $\mathcal U$ and density $0$ elsewhere;
• (b) the mean $\bar\xi=\mathbb E[\xi]$ is finite and $z^*(\bar\xi)'\bar\xi>0$;
• (c) the law of $\xi$ is symmetric about $\bar\xi$, that is, $\xi$ and $2\bar\xi-\xi$ are equal in distribution.

Formalization targets

Goal: Theorem 3 (p. 24)

Under Assumption 5, for every measurable optimal-decision map $z^*$,

$$\mathbb E\big[L(\xi,\bar\xi)\big]\;\le\;\mathbb E\big[L(\xi,\zeta)\big]\quad\text{and}\quad W(\bar\xi)\le W(\zeta)\qquad\text{for all }\zeta\in\mathbb R^d.$$

The page's "the solution … is simply the mean" is read as "the mean is a minimizer", which is what the proof concludes; uniqueness is not claimed.

Milestones (steps of the proof, pp. 24–25)

1. For each $\xi$, $\zeta\mapsto L(\xi,\zeta)$ is convex.
2. $L(\xi,\zeta)\le\big|\max_{z\in\mathcal Z} z'(\xi-2\zeta)\big|+2|\zeta'z^*(\xi)|\le(\|\xi-2\zeta\|_1+2\|\zeta\|_1)\max_{z\in\mathcal Z}\|z\|_\infty\le(\|\xi\|_1+4\|\zeta\|_1)\max_{z\in\mathcal Z}\|z\|_\infty$.
3. With probability one, $2\bar\xi-\xi\in\mathcal U$ and $\mathcal Z^*(2\bar\xi-\xi)$ is a singleton.
4. Under symmetry, $\mathbb E[z^*(2\bar\xi-\xi)]=\mathbb E[z^*(\xi)]$.
5. If $z^*(\bar\xi)'\bar\xi>0$ then $z'\bar\xi\ge z^*(\bar\xi)'\bar\xi>0$ for every $z\in\mathcal Z$.

Significance

The upper bound (16) is the computational core of the paper's Algorithm 1: each alternating-minimization step solves one instance of it per cluster. Theorem 3 is the only result in the paper that identifies its minimizer in closed form, and it shows that, in a symmetric case, the cost-aware reduction agrees with the classical one at $m=1$. It is the paper's justification that the upper bound is a sensible surrogate and not an arbitrary convex relaxation.

The argument is a variant of the mean-minimizes-the-surrogate result of Elmachtoub and Grigas for the SPO+ loss (Management Science, 2022, Proposition 6(a)), with both terms clipped at zero and with a law living only on $\mathcal U$ instead of all of $\mathbb R^d$. Theorem 3 is proved on paper; it has not been formalized, and on Prove2Me the Elmachtoub–Grigas statement is posed but open. The work here is to formalize the known proof, including the measure-theoretic steps the paper treats in one sentence each: integrability of the loss, exchange of the subdifferential and the expectation, and the almost-sure uniqueness of linear minimizers over a polytope.

Difficulty

Convexity of the objective and a vanishing subgradient at $\bar\xi$ would settle the theorem, but two steps of that argument are not routine. First, the objective is not differentiable everywhere, and the subdifferential of $\zeta\mapsto\mathbb E[L(\xi,\zeta)]$ is not in general the expectation of the pointwise subdifferentials: the exchange needs the integrable bound of milestone 2 and the almost-sure uniqueness of milestone 3. Second, that uniqueness is a statement about the geometry of polytopes and about the law of the reflected parameter $2\bar\xi-\xi$ together: neither convexity nor absolute continuity alone gives it. The clipping at zero adds a third point: one has to check that it is inactive at $\zeta=\bar\xi$ almost surely, which is where Assumption 5a's support condition on $\mathcal U$ and Assumption 5b enter. Dropping either half of Assumption 5a breaks the argument: a two-atom symmetric law can put both atoms where $\mathcal Z^*(2\bar\xi-\xi)$ is a whole edge, and a law charging the complement of $\mathcal U$ can make the first clipping active at $\bar\xi$.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin d) and $z'\xi$ is ⟪z, ξ⟫_ℝ. Decision and parameter spaces coincide ($n_z=d$), as the cost $z'\xi$ requires.
• $\mathcal Z$ is polytope P qv, with the hypotheses that it is nonempty and bounded (§1 of the paper assumes $\mathcal Z$ nonempty and compact; the polytope is closed).
• The maximum and minimum of $z'v$ over $\mathcal Z$ and the argmin set are the published definitions SmartPTO.Fisher.xi, SmartPTO.Fisher.zstar and SmartPTO.Fisher.Wstar; "symmetric about its mean" is the published SmartPTO.Fisher.CentrallySymmetric.
• $z^*$ is a function zsel with the hypothesis that zsel ξ is a minimizer for every $\xi$, and it is assumed measurable (needed for $\mathbb E[z^*(\xi)]$; not on the page). The theorem holds for every such selection; uniqueness of minimizers is not assumed.
• The law is a probability measure $\mu$. Assumption 5a is two hypotheses: $\mu\ll$ Lebesgue and $\mu(\mathbb R^d\setminus\mathcal U)=0$. Full support is not assumed and would contradict the second. Assumption 5b is integrability of $\xi$ plus $z^*(\bar\xi)'\bar\xi>0$ with $\bar\xi=\int\xi\,d\mu$.
• The goal is stated on $\mathbb E[L(\xi,\zeta)]$, the first display of the proof, not on the linear programme (16) with its auxiliary variables; for this cost the two coincide by LP duality (Proposition 3's proof), and Theorem 3 is the population, $m=1$ version.
• Expectations are Bochner integrals, which return $0$ for non-integrable integrands. Under the stated hypotheses $\xi\mapsto L(\xi,\zeta)$ is dominated by $(\|\xi\|_1+4\|\zeta\|_1)\max_{z\in\mathcal Z}\|z\|_\infty$ and is integrable, so the goal is not satisfied by junk values; integrability and measurability hypotheses must not be weakened.
• The Wasserstein clause uses an extended nonnegative integral for $W$. This expresses the theorem without adding a second-moment hypothesis absent from Assumption 5. With a finite second moment it is the usual squared Wasserstein objective; with an infinite second moment every one-atom value is infinite, so the clause has only the extended-value meaning.

Useful infrastructure, reusable beyond this mission: support functions of polytopes and their directional derivatives; the fact that a linear function has a unique minimizer over a polytope for Lebesgue-almost every cost vector; differentiation of convex integral functionals under the integral sign. Contributions of any of these as stand-alone lemmas are welcome.

The source is the authors' accepted manuscript (MIT DSpace, "Submitted to Operations Research"), not the published article; all page and theorem numbers refer to the manuscript, whose printed page numbers equal its PDF page numbers.

Selected references

• D. Bertsimas and N. Mundru, Optimization-based Scenario Reduction for Data-Driven Two-stage Stochastic Optimization, Operations Research, 2023 (author manuscript, MIT DSpace). https://doi.org/10.1287/opre.2022.2265
• A. N. Elmachtoub and P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 2022. https://doi.org/10.1287/mnsc.2020.3922
• J. Dupačová, N. Gröwe-Kuska and W. Römisch, Scenario reduction in stochastic programming: an approach using probability metrics, Mathematical Programming 95, 2003. https://doi.org/10.1007/s10107-002-0331-0
• N. Rujeerapaiboon, K. Schindler, D. Kuhn and W. Wiesemann, Scenario Reduction Revisited: Fundamental Limits and Guarantees, Mathematical Programming 191, 2022. https://doi.org/10.1007/s10107-018-1269-1