Probability

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

Motivation

A seller with a fixed stock must choose prices before knowing when customers will arrive or what they will be willing to pay. If customers can wait for a later price, the seller must also account for how today's price changes their purchasing decisions. Chen and Farias study this problem with strategic customers and identify a simple inventory-based policy that can be compared with the best attainable revenue. Their Theorem 1 shows that this policy, with discount rate $\beta=1/(1.42T)$ for a season of length $T$, earns at least $0.29$ of the optimal expected revenue. The policy posts the price that is optimal in the canonical discounted revenue-management problem with myopic customers (Gallego and van Ryzin, 1994; Farias and Van Roy, 2010) at the current inventory level. This mission targets the lower-bound half of its argument, stated as Lemma 9: a comparison between the policy's revenue over a fixed selling season and a discounted, infinite-horizon value. The latter comparison is meaningful independently of the paper's strategic-customer benchmark.

Setting

The seller begins with inventory $x_0\in\mathbb N$ and sells at most one item to each customer. Customers arrive at rate $\lambda>0$. Their nonnegative valuations have density $f$ with total mass one. Write $\bar F(p)=\int_p^\infty f(v)\,dv$ for the probability that a valuation exceeds price $p$. A customer who behaves myopically buys at a posted price $p$ exactly when the valuation is high enough, so sales occur at rate $\lambda\bar F(p)$ while that price is posted.

The paper's Assumption 1 concerns the virtual value $\psi(p)=p-\bar F(p)/f(p)$: it is nondecreasing on nonnegative prices and has a nonnegative root. The simple policy is built from a discount rate $\beta>0$ and an infinite-horizon Bellman value $V:\mathbb N\to\mathbb R$. It has $V(0)=0$ and, for $x\ge1$, satisfies the sign-corrected recursion

$$\beta V(x)=\sup_{p\ge0}\lambda\bar F(p)\bigl(p+V(x-1)-V(x)\bigr).$$

At inventory $x\ge1$ the root price $\pi(x)$ is the unique nonnegative solution of $\psi(\pi(x))=V(x)-V(x-1)$. The price posted just before a sale is $\pi(x)$, and the inventory then becomes $x-1$. At zero inventory the posted price is infinity and there are no more sales. The expected sum of prices paid at sales by time $T$ is denoted $J(x_0,T)$. These objects come from §§2–3.1 of the paper.

Formalization targets

The goal is Lemma 9, for every $\lambda,\beta,T>0$ and every initial inventory $x_0$:

$$V(x_0)\le\left(1+\frac{e^{-\beta T}}{\beta T}\right)J(x_0,T).$$

The coefficient is part of the target. No choice of $\beta$ is fixed. The milestones follow the results stated in the paper: inventory monotonicity of $V$, price monotonicity, pathwise monotonicity of the price and its revenue rate (Lemma 7), the expected-rate identity, revenue-per-time monotonicity (Lemma 8), the identification of $V$ with discounted policy revenue, and the comparison through an independent exponential horizon. The last milestone evaluates $\mathbb E[\max\{1,X/T\}]$ exactly for $X\sim\operatorname{Exp}(\beta)$.

Significance

The bound quantifies how much of the discounted value this explicit policy earns within a finite selling season. Its factor depends only on the dimensionless product $\beta T$; it does not depend on inventory, arrival rate or valuation density. Together with the paper's separate upper bound on its strategic benchmark, Lemma 9 contributes to the advertised $0.29$ comparison. The full comparison requires definitions and equilibrium arguments beyond this mission, so the goal here is precisely the fixed-horizon lower bound.

Chen and Farias proved these statements in the published paper. The Lean items in this proposal are statements awaiting machine-checked proofs. A completed development would establish the discounted-value verification step and the fixed-horizon comparison for an explicit pure-death sales process. Its constructions of inventory-dependent sale times and finite-horizon revenue could also be reused in other pricing models with Poisson arrivals.

Difficulty

The Bellman value is specified by an optimization equation, while $J(x_0,T)$ is defined from the actual sales process. Their equality at an exponential horizon does not follow by unfolding a definition. The price chosen through the virtual-value equation must be connected to the Bellman optimum, and the inventory-dependent process must be related to the same value. The paper also relies on the fact that the root price falls as inventory rises, citing Lemma 1 of Farias and Van Roy; that fact does not follow merely from monotonicity of $\psi$ without control of the marginal values $V(x)-V(x-1)$. Lemma 8 then concerns expected revenue over two different horizons, including paths that sell out early.

Formalization scope

The Lean model uses a nonnegative integrable density on $\mathbb R$, zero on negative valuations and normalized to mass one. It adds $f(p)>0$ for every $p\ge0$. This disclosed condition excludes bounded-support densities: without it the paper's quotient $\bar F(p)/f(p)$ can divide by zero and Lean would assign a spurious value. The paper says the root equation has a unique solution under Assumption 1, but nondecreasing $\psi$ alone does not guarantee existence or uniqueness. Accordingly, the root policy is characterized by its equation and an explicit uniqueness condition. The Bellman recursion uses a least-upper-bound predicate rather than a real supremum with a default value on an empty or unbounded set. The corrected sign in the recursion matches the paper's root equation and discounted-revenue equation.

For stock $x_0$, the model uses $x_0$ independent rate-one exponential clocks. At inventory $x$, the next holding time is the next clock divided by $\lambda\bar F(\pi(x))$. Sales are numbered $1,\ldots,x_0$, and sale $k$ earns $\pi(x_0-k+1)$. The law is the myopic sales process with intensity $\lambda\bar F(\pi(x))$. Expected revenues are lower integrals in the extended nonnegative reals; nonnegative prices make their real-to-extended conversion exact. An independent $X\sim\operatorname{Exp}(\beta)$ is represented by an outer integral over its law. The factor $\lambda$ missing from the paper's printed compensator display is restored, and the paper's intermediate $1+e^{-\beta T}/T$ is read with the missing $\beta$ restored.

The strategic-customer types, stopping rules, perfect Bayesian equilibrium, and the identification of the strategic policy's revenue with myopic-sales revenue are not formalized here. Neither are Theorem 1's $\mathrm{OPT}$ and $J^*$ benchmarks: their specification is not pinned down sufficiently in the paper for this proposal. In particular, $J$ is constructed from sale times and payments, never from $V$, and $V$ is specified by the Bellman equation, never as the policy's revenue. Contributions toward the goal include the individual milestones and reusable facts about the clock process, its revenue, and the exponential horizon.

Selected references

• Y. Chen and V. F. Farias, Robust Dynamic Pricing with Strategic Customers, Mathematics of Operations Research 43(4):1119–1142, 2018. DOI: 10.1287/moor.2017.0897.
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. DOI: 10.1287/mnsc.40.8.999.
• V. F. Farias and B. Van Roy, Dynamic Pricing with a Prior on Market Response, Operations Research 58(1):16–29, 2010. DOI: 10.1287/opre.1090.0729.
• P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer, 1981. DOI: 10.1007/978-1-4684-9477-8.

Motivation

A prophet inequality compares an online decision maker, who sees random values one at a time and must decide irrevocably, with a "prophet" who sees all values in advance. The classic result of Krengel, Sucheston and Garling (1977) and Samuel-Cahn (1984) says that for a single item and independent values a single threshold earns at least half of the expected maximum. In mechanism design the same inequalities describe posted-price mechanisms: a seller approaches buyers in sequence and offers each a menu of prices; each buyer takes the outcome it likes best. Such mechanisms are truthful, simple and online, so a prophet inequality for a feasibility constraint is a welfare guarantee for a practical selling procedure.

Before this paper, prophet inequalities were proved one constraint at a time (matroids, matroid intersections, polymatroids, unit-demand and combinatorial auctions), each with its own probabilistic argument. Dütting, Feldman, Kesselheim and Lucier (SIAM J. Comput. 49(3), 2020; conference version FOCS 2017) showed that a single extension theorem reduces all of them to a deterministic question about full-information instances.

Setting

There are $n$ agents $N=\{1,\dots,n\}$. Agent $i$ has an outcome space $X_i$ containing a null outcome $\varnothing$. An outcome profile is $\mathbf x=(x_1,\dots,x_n)$; $\mathbf x_{[i-1]}$ is $\mathbf x$ with the outcomes of agents $i,\dots,n$ replaced by $\varnothing$. The feasible profiles form a downward-closed set $\mathcal F$: removing outcomes keeps a profile feasible.

Agent $i$'s valuation $v_i:X_i\to[0,1]$ is drawn independently from a known distribution $\mathcal D_i$; $\mathcal D=\prod_i\mathcal D_i$. The welfare of $\mathbf x$ is $\mathbf v(\mathbf x)=\sum_iv_i(x_i)$, and $\mathbf v(\mathrm{OPT}(\mathbf v,S))$ is the largest welfare over a set $S$ of profiles. An outcome rule $\mathrm{ALG}$ maps each valuation profile to a feasible profile.

A pricing rule assigns a price $p_i(x_i\mid\mathbf y)\in[0,\infty]$ to outcome $x_i$ offered to agent $i$ when the partial allocation is $\mathbf y$, with price $\infty$ when $x_i$ cannot be feasibly added to $\mathbf y$. In the posted-price mechanism the agents are approached in index order; agent $i$ sees the prices given the allocation so far and takes an outcome maximizing its utility $v_i(x_i)-p_i(x_i\mid\mathbf y)$.

A set $\mathcal H$ of profiles is exchange compatible with $\mathbf x$ if $(y_i,\mathbf x_{-i})\in\mathcal F$ for every $\mathbf y\in\mathcal H$ and every $i$. For a fixed valuation profile $\mathbf v$, a pricing rule $p^{\mathbf v}$ is $(\alpha,\beta)$-balanced (Definition 3.1) with respect to $\mathrm{ALG}$ and an exchange-compatible family $(\mathcal F_{\mathbf x})_{\mathbf x}$ if for every $\mathbf x\in\mathcal F$

$$\text{(a)}\quad\sum_{i}p^{\mathbf v}_i(x_i\mid\mathbf x_{[i-1]})\ \ge\ \tfrac1\alpha\bigl(\mathbf v(\mathrm{ALG}(\mathbf v))-\mathbf v(\mathrm{OPT}(\mathbf v,\mathcal F_{\mathbf x}))\bigr),$$ $$\text{(b)}\quad\sum_{i}p^{\mathbf v}_i(x'_i\mid\mathbf x_{[i-1]})\ \le\ \beta\cdot\mathbf v(\mathrm{OPT}(\mathbf v,\mathcal F_{\mathbf x}))\quad\text{for all }\mathbf x'\in\mathcal F_{\mathbf x}.$$

Property (a) says the prices paid by $\mathbf x$ cover the welfare $\mathbf x$ blocks; (b) says that what remains available is not overpriced.

Formalization targets

Goal: Theorem 3.2 (p. 549)

If every $p^{\tilde{\mathbf v}}$ is $(\alpha,\beta)$-balanced with respect to one exchange-compatible family, post $\delta p$ with $p_i(x_i\mid\mathbf y)=\mathbb E_{\tilde{\mathbf v}}[p^{\tilde{\mathbf v}}_i(x_i\mid\mathbf y)]$ and $\delta=\alpha/(1+\alpha\beta)$. Then the welfare $\mathbf x(\mathbf v)$ of the mechanism satisfies

$$\mathbb E_{\mathbf v}\bigl[\mathbf v(\mathbf x(\mathbf v))\bigr]\ \ge\ \frac1{1+\alpha\beta}\,\mathbb E_{\mathbf v}\bigl[\mathbf v(\mathrm{ALG}(\mathbf v))\bigr].$$

Milestones

The steps of the paper's proof (pp. 549–550), in order: the prefix $\mathbf x_{[i-1]}(\mathbf v)$ does not depend on $v_i$; the per-agent utility bound against a deviation drawn from an independent sample $\mathbf v'$; (3.1); the bound (3.2) from property (b); (3.3); the pointwise revenue bound from property (a); (3.4); and welfare = utilities + revenue. Two applications complete the list: Claim 3.3 (the single-item price $\max_\ell v_\ell$ is $(1,1)$-balanced, which with the goal gives the classic factor 2) and the balancedness half of Theorem 4.2 for knapsack.

Significance

The theorem turns prophet inequalities into a deterministic design problem: to obtain a $1/(1+\alpha\beta)$ guarantee against any benchmark $\mathrm{ALG}$, it suffices to exhibit balanced prices for each fixed valuation profile. The paper uses it to rederive the single-item factor 2, to obtain $O(d)$ guarantees for combinatorial auctions with bundles of size $d$, a constant for knapsack, and bounds for MPH-$k$ valuations, sparse packing problems and multidimensional matroids. Because $\mathrm{ALG}$ can be any (for example polynomial-time) algorithm, the guarantee is relative to what can be computed, not only to the optimum.

The result is proved in the paper. As far as is known, no part of it has a machine-checked proof; the platform holds no posted-price framework of this generality. A formal proof would provide a reusable model of sequential posted-price mechanisms over arbitrary outcome spaces and a checked reduction that later formalizations of the applications can invoke instead of repeating a probabilistic argument.

Difficulty

The obvious argument fixes the realized valuations and charges each agent's purchase against the welfare it blocks. That fails because the prices are averages over a hypothetical profile $\tilde{\mathbf v}$, not the prices of the realized instance, and the set of outcomes still available depends on everyone's random values. The proof needs an independent copy $\mathbf v'$ of the valuations and the fact that the allocation before agent $i$ does not depend on $v_i$, so that $v_i$ and $v'_i$ can be exchanged without changing the distribution. Formally, the run of the mechanism is a recursion over agents, the exchange is a measure-preserving swap of coordinates of a product measure, the optimal value $\mathbf v(\mathrm{OPT}(\mathbf v,\mathcal F_{\mathbf x}))$ is a supremum that need not be attained, and the family $\mathcal F_{\mathbf x}$ may be empty.

Formalization scope

Agents are Fin n, 0-based; the index order is the order of Fin n. Outcomes are (X : Fin n → Type*) with a null profile nul. Valuation types V i are countable with the discrete σ-algebra (a disclosed restriction: the paper allows any distribution); this makes every function measurable and every bounded one integrable. A type w : V i values outcomes through val i w : X i → ℝ, with values in $[0,1]$ as on p. 547. The distribution is Measure.pi μ with every μ i a probability measure.

Prices are ℝ≥0∞-valued, ⊤ standing for $\infty$; the expected price is a Lebesgue integral in $[0,\infty]$. Property (a) passes its real right side through ENNReal.ofReal, and no price sum is ever converted to a real number, so an infinite price is never read as $0$. $\mathbf v(\mathrm{OPT}(\mathbf v,S))$ is the real supremum sSup of the welfare over $S$, equal to $0$ on $S=\varnothing$ as in the proof of Claim 3.3. Exchange compatibility of the family is required at every profile, not only feasible ones. The pricing-rule condition "$\infty$ when infeasible" is imposed at feasible partial allocations, which is where the paper defines prices.

Two standing assumptions are disclosed. First, the null outcome is free: $p^{\tilde{\mathbf v}}_i(\varnothing\mid\mathbf y)=0$ for feasible $\mathbf y$. Every pricing rule of the paper satisfies it, and without it the proof's deviation does not exist when $\mathcal F_{\mathbf x(\mathbf v)}=\varnothing$. Second, the agents' behaviour is a choice rule that sees only the agent's own type and the allocation so far, assumed utility-maximizing (finite price, best utility among finitely priced outcomes) at every feasible partial allocation. The constant $\delta=\alpha/(1+\alpha\beta)$ is written into the posted prices, not passed as a parameter.

A trivializing formalization is ruled out: the goal mentions only the run of the mechanism, the expected prices scaled by $\delta$, balancedness and the two expectations. It does not assume the utility or revenue bounds, it does not let an agent's choice see other agents' types, and a supplementary check confirms that its hypotheses are jointly satisfiable. Milestones that involve the proof's deviation $\mathrm{OPT}(\mathbf v',\mathcal F_{\mathbf x(\mathbf v)})$ are stated for an arbitrary selector from $\mathcal F_{\mathbf x}$, a generalization that avoids assuming that the supremum is attained. Theorem 4.2 is stated as $(2,1)$-balanced, which is what its proof establishes; the printed "$(1,2)$" is false.

Useful infrastructure, reusable beyond this mission: measure-preserving coordinate swaps for Measure.pi and products of product measures, ε-maximizer selection for bounded suprema, and induction principles for the sequential run. Contributions of proofs of individual milestones are welcome.

Selected references

• P. Dütting, M. Feldman, T. Kesselheim, B. Lucier, Prophet inequalities made easy: Stochastic optimization by pricing nonstochastic inputs, SIAM J. Comput. 49(3):540–582, 2020. https://doi.org/10.1137/20M1323850
• U. Krengel, L. Sucheston, Semiamarts and finite values, Bull. Amer. Math. Soc. 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, Ann. Probab. 12(4):1213–1216, 1984. https://doi.org/10.1214/aop/1176993150
• R. Kleinberg, S. M. Weinberg, Matroid prophet inequalities and applications to multi-dimensional mechanism design, Games Econom. Behav. 113:97–115, 2019. https://doi.org/10.1016/j.geb.2014.11.002
• S. Chawla, J. D. Hartline, D. Malec, B. Sivan, Multi-parameter mechanism design and sequential posted pricing, STOC 2010, 311–320. https://doi.org/10.1145/1806689.1806733

Motivation

In a multi-armed bandit, a decision maker repeatedly chooses an arm, observes a reward, and tries to learn which arm has the highest average reward while losing little reward during learning. A policy that requires the number of future pulls in advance cannot be used unchanged when stopping time is uncertain. Perchet and Rigollet study successive elimination (SE), which removes poorly performing arms from a shrinking active set and can run without knowing the realized horizon. Their Theorem 2.1 bounds its expected regret when the horizon is random and independent of rewards Perchet and Rigollet, 2013, Theorem 2.1.

The static-bandit theorem also supplies a concentration and elimination analysis used in the paper's broader study of bandits with covariates. This mission isolates that theorem and the intermediate estimates that make its quantitative constant explicit. The paper proves the result in §2, with a concentration lemma in the Appendix; the goal here is a machine-checked statement and, eventually, a machine-checked proof of that known result.

Setting

There are $K+1\ge2$ arms. For each arm $i$, the reward stack $Y_{i,1},Y_{i,2},\ldots$ lists the rewards that successive pulls of that arm will reveal. Rewards lie in $[0,1]$, are identically distributed along each arm, and have mean $f_i$. The stacks are mutually independent. Arms are indexed so that $f_1\le\cdots\le f_{K+1}$, and the last arm, denoted $*$, is uniquely best. Its gap from arm $i$ is $\Delta_i=f_*-f_i$. A gap is zero only for the best arm.

The policy works in rounds. At the start of round $\tau$, a nonempty set $I_\tau$ is active. It pulls each arm in $I_\tau$ once, in increasing index order, and computes the mean $\bar Y_i(\tau)$ from that arm's first $\tau$ rewards. It retains an arm when its mean is within $\gamma U(\tau,T)$ of the largest active mean, where $T\ge1$ is an integer, $\gamma\ge1$, and

$$\overline{\log}(x)=\max\{\log x,1\},\qquad U(\tau,T)=2\sqrt{\frac{2\overline{\log}(T/\tau)}{\tau}}.$$

Concatenating the rounds gives the pull sequence $\widehat\pi_1,\widehat\pi_2,\ldots$. For a horizon $N$, its regret is $R_N(\widehat\pi)=\sum_{t=1}^{N}\Delta_{\widehat\pi_t}$. If $N$ is random, independent of the reward stacks, and has mean $n$, the paper studies $\mathbb E R_N(\widehat\pi)$. For a threshold $\Delta>0$, let $\Delta^-$ be the largest arm gap strictly smaller than $\Delta$, or zero if none exists.

Formalization targets

The goal is Theorem 2.1, for every positive threshold $\Delta$:

$$\mathbb E R_N(\widehat\pi) \le 392\gamma^2\left(1+\frac nT\right) \frac K\Delta\, \overline{\log}\!\left(\frac{T\Delta^2}{18\gamma^2}\right) +n\Delta^-.$$

The $K$ in this formula counts suboptimal arms; there are $K+1$ arms in total. The paper writes $\Delta\ge0$ under a convention that division by zero is infinite. The real-valued Lean goal states the informative positive-threshold case.

The milestones include the Appendix's maximal Hoeffding–Azuma inequality and Lemma A.1, which controls all empirical averages up to a fixed time. In §2 they continue with the stopping-round estimate (2.2), the empirical-gap tail (2.5), the bound $\Phi_j(\tau)\le4\tau/T$ for a false elimination of the best arm, and the final comparison for $\phi(x)=\overline{\log}(a x^2)/x$. Each has its own statement so that a proof of the goal can import the exact estimate it needs.

Significance

The bound separates the cost of learning arms with gaps above $\Delta$ from the remaining regret represented by $n\Delta^-$. It applies when the policy uses a tuning value $T$ but the number of pulls actually made is the random variable $N$. Thus it gives a quantitative guarantee without asking the algorithm to know its stopping time in advance. Its constants and dependence on $T$, $n$, $K$, and $\gamma$ are explicit Perchet and Rigollet, 2013, §2.

The result is proved in the paper, while the Lean declarations in this proposal are open statements. Completing them would add a reusable formal account of elimination on a reward stack and of the Appendix's time-uniform concentration estimate. Mathlib and existing platform theorems contain related Hoeffding–Azuma tools, but this paper's peeling inequality, its particular stopping rule, and the random-horizon regret conclusion still require proofs in the stated model.

Difficulty

An ordinary concentration bound at one sample size does not control every round in which an arm could eliminate the best arm. Taking a naive union bound over all rounds loses the dependence on $T$ needed for the displayed regret constant. The Appendix instead states a maximal inequality and a bound that holds across a range of sample sizes. The regret calculation must then account for both kinds of error: removing the best arm and retaining a suboptimal arm for too long.

The stopping round depends on the gap through $U(\tau,T)$, which itself contains $\overline{\log}(T/\tau)$. Its upper bound, the event decomposition across ordered arms, and the final comparison of gap-dependent terms all retain the paper's exact constants. A proof that only establishes the asymptotic rate would not close this goal.

Formalization scope

Lean uses Fin (K+1) with zero-based indices, so its last element is the paper's arm $K+1$. The published stochastic-bandit definition supplies the mutually independent reward stack and arm means. The [0,1] bound, sorted means, and unique best arm are explicit assumptions. A separate martingale-difference definition supplies the Appendix's adapted, integrable sequence, including centering of its first term; the page's one-line definition leaves that first-step condition unstated. The concentration milestones require a nondegenerate interval $a<b$: the displayed maximal exponent divides by $(b-a)^2$, and Lemma A.1 is false at $a=b=0$ for a zero sequence and $\delta<1$.

The SE policy is a function of observed rewards in the stack. It uses the end-of-round test described in the text and proof of §2, with equality retained, since Policy 1's pseudocode tests at a different point in the round. The active set starts with all arms and remains nonempty; the total Lean pull function has a fallback value that is unreachable under the theorem's parameters. The policy never reads the unknown means. Empirical means and $U$ are used only at positive rounds.

The horizon is measurable and integrable, has mean $n$, and is independent of the entire reward stack. Since regret is bounded by the horizon, its expectation is a genuine integral rather than the default value of a non-integrable Lean integral. The positive-threshold condition avoids Lean's zero-valued division at $\Delta=0$. Finite maxima are taken over finite arm sets, and $\overline{\log}$ is kept distinct from the ordinary logarithm in the Appendix's bounds. The paper's printed $n$ in the logarithm of (2.7) and the final $\phi$ comparison is read as $T$, consistently with (2.2) and Theorem 2.1. Contributions to the concentration lemmas, stopping-round analysis, elimination events, and final regret proof all fit this scope.

Selected references

• V. Perchet and P. Rigollet, The multi-armed bandit problem with covariates, Annals of Statistics 41(2), 2013, 693–721. arXiv:1110.6084v3; DOI:10.1214/13-AOS1101.
• S. Bubeck and N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721.

Motivation

The adjacency matrix of an Erdős–Rényi random graph contains a large deterministic mean as well as random fluctuations. The mean affects the largest eigenvalue, while the centered fluctuations determine much of the remaining spectrum. A local spectral law must describe both pieces at a resolution fine enough to distinguish eigenvalues within a narrow energy window. Erdős, Knowles, Yau and Yin established such estimates for a broader class of sparse symmetric matrices and their noncentered rank-one deformations in Spectral statistics of Erdős–Rényi graphs I. This mission formalizes the paper's Theorem 2.9, with the centered-matrix law and eleven intermediate results of the paper as milestones.

The paper treats the graph matrix through a model that also allows other sparse distributions. Its parameters $q_N$ and $f_N$ separate sparsity from the size of the deterministic mean. That separation matters: the normalized resolvent trace can obey a local semicircle law even when the deformation produces a distinguished top eigenvalue. The formal target therefore concerns the deformed matrix itself, rather than replacing it with the centered matrix.

Setting

For each size $N$, let $H_N=(h_{ij})$ be a real symmetric random matrix. Entries indexed by the upper triangle are independent, centered, and have variance $1/N$. Their higher moments obey

$$\mathbf E|h_{ij}|^p\le\frac{C^p}{Nq_N^{p-2}},\qquad 3\le p\le(\log N)^{A_0\log\log N}.$$

The sparsity parameter $q_N$ lies between $(\log N)^{3\xi_N}$ and $C\sqrt N$, and the logarithmic parameter satisfies $1+a_0\le\xi_N\le A_0\log\log N$, with $a_0>0$ and $A_0\ge10$. Define $e_N=N^{-1/2}(1,\ldots,1)$ and the noncentered matrix $A_N=H_N+f_N|e_N\rangle\langle e_N|$, where $0\le f_N\le N^C$. The projection $|e_N\rangle\langle e_N|$ has every entry equal to $1/N$. These are Definitions 2.1 and 2.2 of the source paper, pp. 5–6.

For a complex number $z=E+i\eta$ with $\eta>0$, the resolvents are $G(z)=(H_N-zI)^{-1}$ and $\widetilde G(z)=(A_N-zI)^{-1}$. Their normalized traces are $m(z)=N^{-1}\operatorname{Tr}G(z)$ and $\widetilde m(z)=N^{-1}\operatorname{Tr}\widetilde G(z)$. The comparison object is the semicircle density $\rho_{\mathrm{sc}}(x)=(2\pi)^{-1}\sqrt{[4-x^2]_+}$ and its Stieltjes transform $m_{\mathrm{sc}}(z)=\int_{\mathbb R}\rho_{\mathrm{sc}}(x)/(x-z)\,dx$. Put $\kappa_E=\bigl||E|-2\bigr|$ and $D=\{E+i\eta:|E|\le\Sigma,\ 0<\eta\le3\}$ for a fixed $\Sigma\ge3$. These definitions appear in Section 2, pp. 7–9.

An $N$-dependent event has $(\xi,\nu)$-high probability when its failure probability is at most $\exp[-\nu(\log N)^{\xi_N}]$ for all sufficiently large $N$. The spectral estimates below refer to single events on which the claimed bound holds at every $z\in D$ simultaneously.

Formalization targets

Main goal: the local law for A

Theorem 2.9 assumes $\xi_N\sim(A_0/2)\log\log N$ and $q_N\ge(\log N)^{C_1\xi_N}$. Its first conclusion is that, with $(\xi,\nu)$-high probability, every $z=E+i\eta\in D$ satisfies

$$|\widetilde m(z)-m_{\mathrm{sc}}(z)|\le(\log N)^{C_2\xi_N}\left(\min\left\{\frac1{q_N^2\sqrt{\kappa_E+\eta}},\frac1{q_N}\right\}+\frac1{N\eta}\right).$$

Under the additional bound $f_N\le C_0\sqrt N$, its second conclusion controls every entry at every $z\in D$:

$$|\widetilde G_{ij}(z)-\delta_{ij}m_{\mathrm{sc}}(z)|\le(\log N)^{C_2\xi_N}\left(\frac1{q_N}+\sqrt{\frac{\operatorname{Im}m_{\mathrm{sc}}(z)}{N\eta}}+\frac1{N\eta}\right).$$

The constants $C_1,C_2$ are universal and positive. The probability exponent $\nu>0$ may depend on the fixed parameters named in the theorem. Both conclusions, including the extra condition on $f_N$ in the second, are retained from Theorem 2.9, pp. 9–10.

Milestones

The milestones follow the paper's own sequence of numbered results.

1. Properties of $m_{\mathrm{sc}}$ (Lemma 3.2): $|m_{\mathrm{sc}}|\sim1$, $|1-m_{\mathrm{sc}}^2|\sim\sqrt{\kappa_E+\eta}$, and the size of $\operatorname{Im}m_{\mathrm{sc}}$ inside and outside the spectrum.
2. Resolvent identities for minors (Lemma 3.4) and the self-consistent equation $G_{ii}=1/(-z-m_{\mathrm{sc}}-([v]-\Upsilon_i))$ (Lemma 3.10); both are deterministic.
3. Large deviation bounds for linear and quadratic forms in independent variables with the sparse moment decay (Lemma 3.8 (ii)).
4. The weak local semicircle law for $H$ (Theorem 3.1) on $D_L=\{|E|\le\Sigma,\ (\log N)^LN^{-1}\le\eta\le3\}$, $L\ge8\xi$.
5. Fluctuation averaging (Lemma 4.1 (4.2)): the average $[Z]=N^{-1}\sum_iZ_i$ of the fluctuation terms is much smaller than each $Z_i$.
6. The a priori norm bound $\|H\|\le2+(\log N)^\xi q^{-1/2}$ (Lemma 4.3) and the strong local law for $H$ (Theorem 2.8, the analogue of the goal for $f=0$).
7. Interlacing of the eigenvalues of $H$ and $A$ (Lemma 6.1) and the near-orthogonality $\sum_{\alpha\ne N}|\langle v_\alpha,e\rangle|^2=O(f^{-2})$ of $e$ to the non-top eigenvectors of $A$ (Corollary 6.7).
8. The trace comparison $|\widetilde\Lambda-\Lambda|\le\pi/(N\eta)$ (Lemma 7.1), which yields the first conclusion of the goal from Theorem 2.8.
9. Entrywise control of $\widetilde G$ on the event $\widetilde\Omega(\eta)$ that $\widetilde\Lambda_d+\widetilde\Lambda_o\le(\log N)^{-\xi}$ on the line $\operatorname{Im}z=\eta$: the off-diagonal bound $\widetilde\Lambda_o\le C\Phi$ (Proposition 7.6 (7.14)) and the diagonal bounds of Lemma 7.7, with $\Phi=(\log N)^\xi/q+(\log N)^{2\xi}(\sqrt{\operatorname{Im}\widetilde m/(N\eta)}+1/(N\eta))$.

Significance

The trace estimate gives quantitative control over spectral mass at local scales, including near the edges $E=\pm2$. The entrywise estimate says more: each resolvent entry is close to the diagonal semicircle approximation with an error that records both sparsity and finite-size effects. The paper's later results derive density-of-states and eigenvector statements from these local controls. Those consequences are outside this mission's goal.

The intended formal development supplies reusable definitions of sparse symmetric ensembles, high-probability events, semicircle transforms, and complex resolvents, followed by exact statements of the paper's estimates. Mathlib contains no local semicircle law, for Wigner or for sparse matrices, and no Stieltjes transform of the semicircle distribution; the local law, the large deviation bounds and the interlacing lemma are each reusable beyond this paper.

Difficulty

The deterministic rank-one comparison controls the normalized trace but does not by itself control each entry of $\widetilde G$. The entrywise estimate must account for the deformation and for fluctuations caused by sparse entries. Near the spectral edges, the stability scale of the semicircle transform changes with $\kappa_E+\eta$; a bound that is uniform in the bulk does not automatically retain the paper's edge behavior. The theorem also asks for one event covering a continuum of $z$ values, so a collection of separate fixed-$z$ probability bounds has the wrong quantifier order. These are substantive parts of Sections 3–7, beyond algebraic manipulation of resolvents.

Formalization scope

Lean represents all $H_N$ on one probability space and takes their entries to be real, symmetric, measurable random variables, independent in the upper triangle. Conditions involving $\log\log N$ and the moments hold for all sufficiently large $N$; this avoids impossible small-$N$ parameter bounds and matches the asymptotic theorem. The moment order $p$ is real, as in the paper. Each finite expectation has an explicit integrability condition. A single positive constant $C$ is used for the moment, sparsity, and deformation bounds: replacing several fixed constants by their maximum preserves all three inequalities.

Matrix indices use Fin N rather than the paper's $1,\ldots,N$. The resolvent is a complex matrix formed by coercing the real matrix before subtracting $zI$. Every result that uses it restricts $\eta>0$ eventually or explicitly; its inverse at a singular input is never used to make a claim. The semicircle transform is defined by the paper's integral, and $\sqrt{4-x^2}$ uses Lean's nonnegative square root, implementing the positive part. The high-probability predicate evaluates the measure of arbitrary sets, so it can state the intersection over all $z$ without a separate measurability assumption on that intersection. Positive $q_N$ and positive square-root arguments follow eventually from the model and $z\in D$.

The deterministic Lemmas 3.2, 3.4, 3.10, 6.1 and 7.1 are stated for every real symmetric matrix and every $z$ with $\eta>0$ (Lemma 3.2 on $D$); the paper's $D_L$ is contained there. Minors keep the original index names, and $G^{(\mathbb T)}_{kl}$ is only used for $k,l\notin\mathbb T$. $Z_i$ is the explicit expression of (3.15). Ordered eigenvalues are the sorted roots of the characteristic polynomial. Statements the paper makes "for fixed $z$" (Lemmas 4.1, 7.7, Proposition 7.6) are uniform in $z$: one threshold $N_0$ serves every $z$. The unnamed constants $C$, $\nu$, $K$ are chosen after the fixed parameters and before the random matrices; the universal $C_1,C_2$ come first.

Trivializing encodings are ruled out: every resolvent is taken at $\eta>0$, so the junk inverse of a singular matrix never enters; the model is satisfiable (independent Rademacher signs divided by $\sqrt N$ with $q_N=\sqrt N$ and $\xi_N=(A_0/2)\log\log N$ satisfy it for large $N$); each event of the goal is one intersection over all $z\in D$, not a family of pointwise bounds; the constants appear in the paper's order; and the goal is about $A=H+f|e\rangle\langle e|$ with $f$ allowed to be large, so it does not reduce to Theorem 2.8.

Part (iii) of Lemma 3.8 is not a milestone: the printed (3.22) omits the diagonal variance term $(N^{-2}\sum_i|B_{ii}|^2)^{1/2}$, without which it fails for Rademacher variables with $q\asymp\sqrt N$. Contributions of proofs of any milestone, and of the missing groundwork (Stieltjes transforms of measures, Schur complements of resolvents, moment bounds for sums of independent variables), are welcome.

Selected references

• L. Erdős, A. Knowles, H.-T. Yau and J. Yin, Spectral statistics of Erdős–Rényi graphs I: Local semicircle law, Annals of Probability 41(3B), 2013, pp. 2279–2375. arXiv:1103.1919v5; DOI:10.1214/11-AOP734.

Motivation

A decision maker who must choose $x$ to minimize an expected cost $\mathbb E_F[c(x;\xi)]$ rarely knows the distribution $F$ of the uncertain parameter $\xi$; what is available is a sample $\xi^1,\dots,\xi^N$. Sample average approximation (SAA) replaces $F$ by the empirical distribution. Data-driven distributionally robust optimization (DRO) instead minimizes the worst case of the expected cost over a set $\mathcal F_N$ of distributions built from the data, which protects against the error of the empirical distribution at small $N$. Many such sets have been proposed: moment sets (Delage and Ye, 2010), $\phi$-divergence balls (Ben-Tal et al., 2013), Wasserstein balls (Mohajerin Esfahani and Kuhn, 2018).

Bertsimas, Gupta and Kallus (arXiv:1408.4445v3; Mathematical Programming, 2018, doi:10.1007/s10107-017-1174-z) observe that each such set can be read as the confidence region of a statistical goodness-of-fit (GoF) test, and call the resulting method Robust SAA. A basic question for any such method is whether, as $N\to\infty$, its objective, optimal value and optimal solutions converge to those of the full-information problem. The paper answers it for all data-driven DROs at once, with a single property of the test.

Setting

The support $\Xi\subseteq\mathbb R^d$ of $\xi$ is closed, and $\mathcal P(\Xi)$ is the set of Borel probability distributions on $\Xi$ with the topology of weak convergence. The data $\xi^1,\xi^2,\dots$ are i.i.d. from an unknown $F\in\mathcal P(\Xi)$. A data-driven uncertainty set (DUS) map assigns to each sample $(\xi^1,\dots,\xi^N)$ a set $\mathcal F_N\subseteq\mathcal P(\Xi)$; it is the confidence region of the test that rejects a hypothesis $F_0$ exactly when $F_0\notin\mathcal F_N$. Decisions lie in a closed set $X\subseteq\mathbb R^{d_x}$, the cost is $c(x;\xi)$, and the robust objective is the worst-case expectation

$$\mathcal C(x;\mathcal F_N)=\sup_{F_0\in\mathcal F_N}\mathbb E_{F_0}[c(x;\xi)] .$$

A test is uniformly consistent (Definition 3) if, for every data-generating $F$, almost surely every sequence $F_N$ that does not converge weakly to $F$ lies outside $\mathcal F_N$ for infinitely many $N$. The admissible instances are those satisfying three assumptions: (1) $c(\cdot;\xi)$ is equicontinuous in $x$ uniformly over $\xi$; (2) $X$ is bounded, or $c$ is coercive in $x$ uniformly over a set $D$ of positive $F$-probability and bounded below off $D$; (3) $\Xi$ is bounded, or there is a growth function $\phi\ge0$ with $c(x;\xi)=O(\phi(\xi))$ whose expectation the DUS tracks: $\sup_{F_0\in\mathcal F_N}|\mathbb E_{F_0}\phi-\frac1N\sum_i\phi(\xi^i)|\to0$ almost surely. The convergence conditions are (18) $\mathcal C(x;\mathcal F_N)\to\mathbb E_F[c(x;\xi)]$ uniformly on compact subsets of $X$; (19) convergence of optimal values; and (20) every sequence of robust minimizers has a limit point, and all its limit points are true minimizers.

Formalization targets

Goal: Theorem 2

For a DUS map with nonempty sets,

$$\mathcal F_N\ \text{is uniformly consistent}\iff\Big[\forall F,X,c\ \text{satisfying Assumptions 1–3}:\ (18),(19),(20)\ \text{hold a.s.}\Big].$$

The statement carries no rates and no constants; it is a characterization, so it does not depend on any particular test.

Milestones

1. Proposition 8: under uniform consistency and Assumptions 1 and 3, almost surely $\mathbb E_{F_N}[c(x;\xi)]\to\mathbb E_F[c(x;\xi)]$ for every $x\in X$ and every sequence $F_N\in\mathcal F_N$.
2. Proposition 9: deterministically, convergence of $\mathcal C(x_N;\mathcal F_N)$ along every convergent $x_N\to x$ implies (18).
3. Theorem 2, "only if" side: uniform consistency implies (18)–(20) a.s. for every admissible instance.
4. Theorem 2, "if" side: if the test is not uniformly consistent, some admissible instance fails (18)–(20) with positive probability.
5. Theorem 3: if $\mathcal F_N$ always contains the empirical distribution and the test is $c$-consistent (Definition 5, consistency with respect to the expected costs only), then (18)–(20) hold a.s.
6. Proposition 4 (first sentence): a uniformly consistent test is consistent in the classical sense, $\mathbb P(F_0\notin\mathcal F_N)\to1$ for each $F_0\neq F$.

Significance

The result. Theorem 2 reduces the asymptotic analysis of a data-driven DRO to a property of a statistical test, which can be checked once per test rather than once per optimization model. The paper uses it to classify DUSs: the $\chi^2$ and G-tests on a finite support and the Kolmogorov–Smirnov, Kuiper, Cramér–von Mises, Watson and Anderson–Darling tests on the line are uniformly consistent (Theorems 4–5, separate missions of this series), while the test of marginals is not even consistent and so cannot give convergence for every cost. The necessity direction makes the property sharp: a weaker test always admits a well-behaved cost on which the DRO fails to converge. Theorem 3 explains the remaining cases where a DRO converges for one given cost.

Formalizing it. The result is proved in the paper (§10.5), but its proof leans on several standard facts used without detail: the portmanteau theorem, uniform integrability arguments from Billingsley's Convergence of Probability Measures, the Lévy continuity theorem with the Cramér–Wold device, and coercivity arguments carried over from the paper's Theorem 1. A machine-checked version would fix exactly which regularity of the cost these steps need; three such conditions are stated explicitly here (see the scope section). No part of the result is formalized elsewhere to our knowledge; the platform has no notion of a data-driven uncertainty set or of uniform consistency.

Difficulty

Uniform consistency is a statement about weak convergence, while (18)–(20) are statements about expectations of an unbounded, $x$-dependent cost under the members of $\mathcal F_N$. Weak convergence controls expectations only of bounded continuous functions, so the "only if" side must recover convergence of $\mathbb E_{F_N}[c(x;\xi)]$ from Assumption 3, which requires uniform integrability, and then upgrade pointwise convergence to uniform convergence on compacts and to convergence of minimizers when $X$ is unbounded. The tempting route through a single limiting minimization problem fails: the sets $\mathcal F_N$ change with the sample, the worst case is a supremum over infinitely many distributions, and the minimizers of $\mathcal C(\cdot;\mathcal F_N)$ could escape to infinity unless coercivity on $D$ transfers to every member of $\mathcal F_N$. The "if" side needs, from the mere failure of uniform consistency, a single admissible cost whose worst-case objective detects every failure of weak convergence.

Formalization scope

Points are EuclideanSpace ℝ (Fin d), distributions are ProbabilityMeasure ↥Ξ (whose topology is weak convergence), and the data live on the canonical product space $\Xi^{\mathbb N}$ with the product law, 0-indexed. "Almost surely" is ∀ᵐ, and in Definition 3 one null set serves every sequence $F_N$. An expectation over a member of $\mathcal F_N$ is $+\infty$ when the integrand is not integrable, never Lean's default $0$. Minima in (19)–(20) are infima in the extended reals, so the empty and unattained cases need no special treatment; (20) applies to sequences that are minimizers for all large $N$.

Four hypotheses are added to the page, each used by the paper's own proof: every $\mathcal F_N$ is nonempty (otherwise the worst case is $-\infty$ and uniform consistency is vacuous); $c(x;\cdot)$ is continuous on $\Xi$; the set $D$ of Assumption 2b is open; the growth function $\phi$ of Assumption 3b is continuous, with $\mathbb E_F\phi<\infty$ as fixed on p. 10 of the paper. Theorem 3 additionally assumes Assumption 2, which its proof uses. Proposition 4 assumes the rejection events are measurable. A formalization in which the worst case uses the raw Bochner integral, the supremum ranges over a possibly empty set, or (20) requires minimizers at $N=0$ would make the statements false or vacuous, and is ruled out.

A full development needs weak convergence and the portmanteau theorem (in Mathlib), uniform integrability and its relation to convergence of means under weak convergence, the strong law of large numbers for the growth function and the empirical measure, the Lévy continuity theorem in several dimensions (in Mathlib, via characteristic functions), and a countable convergence-determining class of bounded continuous functions. The uniform-integrability step and the path characterization of local uniform convergence (Proposition 9) are reusable beyond this mission. Contributions to any milestone are welcome; Proposition 9 is self-contained and deterministic.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Robust Sample Average Approximation, arXiv:1408.4445v3, 2016; Mathematical Programming 171 (2018). https://arxiv.org/abs/1408.4445v3, https://doi.org/10.1007/s10107-017-1174-z
• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3), 2010. https://doi.org/10.1287/opre.1090.0741
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
• P. Mohajerin Esfahani, D. Kuhn, Data-Driven Distributionally Robust Optimization Using the Wasserstein Metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1

Why sampling from $e^{-U}$ needs non-asymptotic guarantees

Bayesian inference, statistical physics and machine learning all ask for samples from a probability distribution $\pi$ on $\mathbb R^d$ whose density is known only up to a constant, $\pi(dx)\propto e^{-U(x)}dx$. The unadjusted Langevin algorithm (ULA) is the Euler–Maruyama discretisation of the Langevin diffusion, whose invariant law is $\pi$. It needs only gradients of $U$, has no accept/reject step, and is therefore cheap in high dimension. Without the Metropolis correction, however, the chain does not leave $\pi$ invariant, so its usefulness rests on quantitative bounds: how far, in total variation, the law of the $p$-th iterate is from $\pi$, as an explicit function of the dimension $d$, the step sizes and the regularity of $U$.

Durmus and Moulines (arXiv:1507.05021, Ann. Appl. Probab. 27(3), 2017) gave such bounds for constant and decreasing step sizes. Earlier work of Dalalyan (arXiv:1412.7392, 2017) treated strongly log-concave targets with constant steps. Durmus and Moulines cover nonincreasing step sequences and, among other regimes, potentials that are only strongly convex outside a ball; this mission formalizes that case.

Setting

Write $\|\cdot\|$ and $\langle\cdot,\cdot\rangle$ for the Euclidean norm and inner product of $\mathbb R^d$. The total variation norm of a difference of probability measures is

$$\|\mu-\nu\|_{\mathrm{TV}}=\sup\Big\{\Big|\int f\,d\mu-\int f\,d\nu\Big|: f\text{ Borel},\ |f|\le1\Big\},$$

which ranges in $[0,2]$.

The potential $U:\mathbb R^d\to\mathbb R$ satisfies two assumptions:

• L1: $U$ is differentiable and $\nabla U$ is $L$-Lipschitz;
• H3($M_s$): $U$ is convex and $\langle\nabla U(x)-\nabla U(y),x-y\rangle\ge m\|x-y\|^2$ whenever $\|x-y\|\ge M_s$, for some $M_s\ge0$, $m>0$.

The point $x^\star$ is a minimiser of $U$, and $\pi(dx)=e^{-U(x)}dx/\int e^{-U}$.

The Langevin diffusion is $dY_t=-\nabla U(Y_t)dt+\sqrt2\,dB^d_t$, with $B^d$ a standard $d$-dimensional Brownian motion. Its transition semigroup is $P_t(x,A)=\mathbb P(Y_t(x)\in A)$.

ULA with step sizes $(\gamma_k)_{k\ge1}$ is the chain

$$X_{k+1}=X_k-\gamma_{k+1}\nabla U(X_k)+\sqrt{2\gamma_{k+1}}Z_{k+1},$$

with $(Z_k)$ i.i.d. standard Gaussian. Its one-step kernel is $R_\gamma(x,\cdot)=\mathcal N(x-\gamma\nabla U(x),2\gamma I_d)$, and $\delta_xQ^n_\gamma=\delta_xR_{\gamma_1}\cdots R_{\gamma_n}$ is the law of $X_n$ started at $x$. Write $\Gamma_{n,p}=\sum_{k=n}^p\gamma_k$, and let $A(\gamma,x)=\sup_{k\ge0}\int\|\nabla U\|^2\,d(\delta_xQ^k_\gamma)$.

The explicit constants use

• $F(\lambda,a,c,\gamma,w)=\lambda^aw+c(-\lambda^\gamma\log\lambda)^{-1}$ and $G(\lambda,c,\gamma,w)=w+c(-\lambda^\gamma\log\lambda)^{-1}$;
• $\omega(\varepsilon,R)=R^2/\{2\Phi^{-1}(1-\varepsilon/2)\}^2$, with $\Phi$ the standard Gaussian distribution function;
• $\lambda=e^{-2m+\bar\gamma L^2}$ and $c=2(d+mM_s^2)$.

Formalization targets

Goal: Theorem 21 (p. 16)

Let $d\ge1$, and let $(\gamma_k)$ be positive and nonincreasing with $\gamma_1\le\bar\gamma<2mL^{-2}$. Then for all $0\le n<p$ and $x$,

$$\|\delta_xQ^p_\gamma-\pi\|_{\mathrm{TV}}\le2^{-1/2}L\Big(\sum_{k=n}^{p-1}\Big\{\tfrac{\gamma^3_{k+1}}3A(\gamma,x)+d\gamma^2_{k+1}\Big\}\Big)^{1/2}+C(\delta_xQ^n_\gamma)\kappa^{\Gamma_{n+1,p}}.$$

The three constants are explicit:

• the rate, $\log\kappa=-\frac m2\log2\,[\log\{(1+e^{m\omega(1/2,\max(1,M_s))/4})(1+\max(1,M_s))\}+\log2]^{-1}$;
• the constant of the first term, $A(\gamma,x)\le L^2G(\lambda,c,\gamma_1,\|x-x^\star\|^2)$;
• the constant of the second term, $C(\delta_xQ^n_\gamma)\le6+2(d/m+M_s^2)^{1/2}+2F^{1/2}(\lambda,\Gamma_{1,n},c,\gamma_1,\|x-x^\star\|^2)$.

Milestones, in the order of the proof (§5.1, p. 34)

1. (56), p. 30: for $dX_t=b(X_t)dt+dB^d_t$ with $b$ Lipschitz and monotone (G1), $\sup_{\|x-y\|\le R}\|P_t(x,\cdot)-P_t(y,\cdot)\|_{\mathrm{TV}}\le2(1-\varepsilon)$ for $t\ge\omega(\varepsilon,R)$.
2. Theorem 36, p. 33: under G1 and the contraction G3, $\|P_t(x,\cdot)-P_t(y,\cdot)\|_{\mathrm{TV}}\le2\{(1-\varepsilon)^{-1}+1+\|x-y\|\}\kappa^t$ with an explicit $\kappa$.
3. §5.1, p. 34: $\|P_t(x,\cdot)-\pi\|_{\mathrm{TV}}\le2\{3+\|x-x^\star\|+\int\|y-x^\star\|d\pi(y)\}\kappa^t$ for the Langevin semigroup.
4. §5.1, p. 34: $\int\|y-x^\star\|^2d\pi(y)\le d/m+M_s^2$.
5. Proposition 20, p. 16: $V(x)=\|x-x^\star\|^2$ satisfies $R_\gamma V\le\lambda^\gamma V+\gamma c$ for $\gamma\in(0,\bar\gamma]$.
6. Lemma 1, p. 5: such a drift gives $Q^n_\gamma V(x)\le F(\lambda,\Gamma_n,c,\gamma_1,V(x))$.
7. Proposition 2, p. 5: the decomposition bound (10), given the geometric ergodicity (3) of the diffusion.

The paper's proofs follow each statement in the body of the paper (§4.1, §4.12, §5, §5.1).

Significance

The theorem bounds the sampling error of ULA in total variation non-asymptotically, with a dimension-free contraction rate $\kappa$ and constants polynomial in $d$. With steps decreasing to zero and cumulative step size diverging, its bound gives convergence of $\delta_xQ^p_\gamma$ to $\pi$; for constant steps, the paper reports iteration counts of order $d\log d$ at a prescribed precision in Table 2. H3 covers log-concave targets whose potential can lack strong convexity inside a ball.

The result is proved in the paper but, as far as the platform's catalogue shows, not formalized anywhere. A formalization adds machine-checked versions of several reusable pieces:

• a Foster–Lyapunov moment bound for time-inhomogeneous Markov chains (Lemma 1);
• a Girsanov–Pinsker discretisation estimate for Euler schemes (Proposition 2);
• a reflection-coupling contraction for diffusions with monotone drift (56), Theorem 36.

Difficulty

The ULA chain is not reversible with respect to $\pi$, so the spectral and Dirichlet-form tools of reversible MCMC do not apply to it directly. The bound must instead compare the chain with the continuous diffusion.

That comparison needs Girsanov's theorem on path space and a uniform control of $\int\|\nabla U\|^2$ along a time-inhomogeneous chain.

The rate of the diffusion itself is the second obstacle. Without global strong convexity, synchronous coupling gives no contraction inside the ball $\|x-y\|<M_s$. An explicit rate requires a reflection coupling together with return-time estimates, and it has to be transferred through the time change between $dY=-\nabla U\,dt+\sqrt2dB$ and $dX=-\frac12\nabla U\,dt+dB$.

Formalization scope

The state space is the published EthierKurtz.SDEState d, i.e. EuclideanSpace ℝ (Fin d), and Brownian motion and strong solutions are the published EthierKurtz.IsStandardBrownian and EthierKurtz.SolvesBrownianSDE. The conventions are:

• Semigroup. A semigroup is pinned down by the laws of solutions. $P$ is the semigroup of $dX=b(X)dt+s\,dB$ when every strong solution from $x$, on every probability space, has time-$t$ law $P_t(x,\cdot)$. The Langevin case is $b=-\nabla U$, $s=\sqrt2$.
• Total variation. It is the $\sup_{|f|\le1}$ norm. Using $\sup_A|\mu(A)-\nu(A)|$ instead would halve every bound.
• ULA. The laws $\delta_xQ^n_\gamma$ are iterated Measure.bind with the Gaussian kernel $\mathcal N(x-\gamma\nabla U(x),2\gamma I_d)$. Steps are indexed from $1$, and $\Gamma_{n,p}=0$ for $p<n$.
• Moments. Upper-bounded moments ($Q^n_\gamma V$, $\int\|\nabla U\|^2$, $\int\|y-x^\star\|^2d\pi$) are lower Lebesgue integrals, so a non-integrable function cannot make a bound free. $A(\gamma,x)\le a$ is a bound for every $k$, not a real supremum.
• Normalisation of $\pi$. No hypothesis $\int e^{-U}<\infty$ is added; it follows from L1 and H3.
• Quantile. $\Phi^{-1}(u)=\inf\{z:\Phi(z)\ge u\}$.
• Logarithms and powers. $\lambda$, $\kappa$ lie in $(0,1)$, so the logarithms and real powers are genuine.

Several hypotheses are added or read in a particular way, and each is disclosed in the item's statement:

• $x^\star$. It is a bound variable with the hypothesis that it minimises $U$; the paper uses $x^\star$ in §3.3 without defining it.
• Proposition 20. The dimension is positive so its printed $c=2(d+mM_s^2)$ satisfies (6)'s requirement $c>0$; this is stated in Lean.
• Lemma 1. It carries the §2 standing assumption L1, which makes the Euler transition family measurable in its starting point. It is stated for Borel $V\ge0$ rather than $V\ge1$, because Theorem 21 applies it to $\|x-x^\star\|^2$.
• Proposition 2. It assumes (3) only at $\mu_0=\delta_xQ^n_\gamma$, with finite $C$ and a finite bound on $A(\gamma,x)$.
• (11). The printed $Q^k_\gamma(y,dz)$ is read as $Q^k_\gamma(x,dz)$.

The citations [20] (existence of solutions), [27] (Lindvall), [32] (Meyn–Tweedie) and Girsanov's theorem are used inside the proofs and are not restated.

The library work needed is substantial: Itô calculus for the reflection coupling, Girsanov's theorem, Pinsker's inequality in this norm, and generator–drift arguments for the moments of $\pi$. Contributions of any of these as standalone platform theorems are welcome.

Selected references

• A. Durmus, É. Moulines, Nonasymptotic convergence analysis for the unadjusted Langevin algorithm, Ann. Appl. Probab. 27(3), 2017; cited as arXiv:1507.05021v3. https://arxiv.org/abs/1507.05021
• A. S. Dalalyan, Theoretical guarantees for approximate sampling from smooth and log-concave densities, J. R. Stat. Soc. B 79(3), 2017. https://arxiv.org/abs/1412.7392
• T. Lindvall, L. C. G. Rogers, Coupling of multidimensional diffusions by reflection, Ann. Probab. 14(3), 1986. https://doi.org/10.1214/aop/1176992436
• S. P. Meyn, R. L. Tweedie, Stability of Markovian processes III: Foster–Lyapunov criteria for continuous-time processes, Adv. Appl. Probab. 25(3), 1993. https://doi.org/10.2307/1427522
• G. O. Roberts, R. L. Tweedie, Exponential convergence of Langevin distributions and their discrete approximations, Bernoulli 2(4), 1996. https://doi.org/10.2307/3318418