Statistics

Motivation

An online decision maker often sees information about a customer, patient, or request before choosing an action. A bandit with covariates models this setting when the reward of every available action is initially unknown and only the reward of the chosen action is observed. A method must learn which action works best for which covariates while paying for exploratory choices. Perchet and Rigollet studied this problem for smooth reward functions and measured how quickly a policy can approach the performance of an oracle that knows every arm's mean reward Perchet and Rigollet, 2013.

A fixed grid divides the covariate space at one resolution everywhere. It can spend pulls distinguishing arms in regions where their difference is already large, while leaving too few observations in regions where they are close. Adaptively binned successive elimination (ABSE) instead refines a region only while several arms remain plausible there. The paper proves a regret rate controlled jointly by the smoothness of the reward functions and the probability of encountering near ties. Its Theorem 5.1 is the target of this mission.

Setting

There are $K\ge2$ arms and covariates $X_t$ in the unit cube $\mathcal X=[0,1]^d\subset\mathbb R^d$, with $d\ge1$. At time $t$, the policy sees $X_t$, chooses an arm, and sees that arm's reward. The random vectors consisting of the covariate and all potential arm rewards are independent across times. Covariates have a common probability law $P_X$ with a density between constants $0<\underline c\le\overline c$. Every reward lies in $[0,1]$; for arm $i$ its conditional mean given $X_t=x$ is $f^{(i)}(x)\in[0,1]$. The paper does not require the complete reward vectors to be identically distributed across time. These conventions come from §3.1, pp. 10–11.

At $x$, write $f^*(x)=\max_i f^{(i)}(x)$. Write $f^\sharp(x)$ for the largest mean strictly below $f^*(x)$, and set $f^\sharp(x)=f^*(x)$ when every arm ties. The difference $f^*(x)-f^\sharp(x)$ is the positive gap wherever a genuinely suboptimal arm exists. The smoothness condition requires $|f^{(i)}(x)-f^{(i)}(x')|\le L\|x-x'\|^\beta$ for every arm, with the Euclidean norm, $0<\beta\le1$, and $L>0$. The margin condition, with $\alpha>0$, $0<\delta_0<1$, and $C_0>0$, says

$$P_X\{0<f^*(X)-f^\sharp(X)\le\delta\}\le C_0\delta^\alpha\qquad(0\le\delta\le\delta_0).$$

These are the assumptions defining the paper's class $\mathcal M^K_{\mathcal X}(\alpha,\beta,L)$ §3.2, pp. 12–13.

ABSE starts with the whole cube. Each live dyadic cell runs a copy of successive elimination on its inherited arms. One round pulls each remaining arm once. After a complete round, an arm is eliminated if its empirical mean falls more than twice the radius $U(s,n|B|^d)$ below the largest empirical mean, where $|B|$ is the cell's side length and $U$ uses $\overline{\log}(x)=\max\{\log x,1\}$. The cell splits after its specified stopping round if it has at least two active arms and is below the maximum depth $k_0$. Each child receives the survivors. The policy takes $d,\beta,L,K,n$ as parameters and uses the current covariate and rewards it actually observed Policy 3, p. 22.

Formalization targets

Goal: Theorem 5.1, finite margin exponent

The goal is the finite-$\alpha$ part of Theorem 5.1, p. 22. Fix $d\ge1$, $0<\beta\le1$, $L>0$, $\alpha>0$ with $\alpha\beta\le d$, $0<\delta_0<1$, $C_0>0$ and $0<\underline c\le\overline c$. There is one constant $C>0$, depending on these parameters but not on $K$, $n$ or the machine, such that for every $K\ge2$, every $n\ge K\log K$ and every machine of the class,

$$\mathbb E R_n(\widetilde\pi)\le Cn\left(\frac{K\log K}{n}\right)^{\frac{\beta(\alpha+1)}{2\beta+d}}.$$

Here $\widetilde\pi$ is ABSE and $R_n$ is its cumulative regret against an arm of maximum conditional mean at each covariate. The goal asserts the shape of the rate with an unspecified constant, which is the paper's form.

Milestones

In attack order:

1. Lemma A.1 (p. 28): a maximal Hoeffding–Azuma inequality, $\mathbb P\{\exists t\le T:\bar Z_t\ge\sqrt{2(b-a)^2t^{-1}\log(4T/(\delta t))}\}\le\delta$ for bounded martingale differences.
2. (5.3) (p. 21): $\ell_B\le C_\ell|B|^{-2\beta}\,\overline{\log}(n|B|^{2\beta+d})$, the number of rounds a cell spends before it may split.
3. (5.10) (p. 26): if arm $i$ has gap above $8c_0|B|^\beta$ at a point of $B$, then the cell mean of the arm $\check\imath$ that is best at that point exceeds the cell mean of $i$ by at least $\tfrac32\varepsilon_{B,\ell_B}$.
4. The display before (5.6) (p. 25): $\sum_{|B|=2^{-k}}q_B\le c_2 2^{k(d-\beta\alpha)}$, where $q_B$ is the conditional probability of a near tie inside $B$.
5. (5.5) (p. 24): the pathwise decomposition $r_n^{\mathrm{born}}(B)=r_n^{\mathrm{live}}(B)+\sum_{B'\in\mathrm{burst}(B)}r_n^{\mathrm{born}}(B')$ of regret along the tree.
6. Theorem 5.1, $\alpha=\infty$ (p. 22): when the margin region $\{0<f^\star-f^\sharp\le\delta_0\}$ has probability zero, $\mathbb E R_n(\widetilde\pi)\le CK\log n$.

Significance

The result provides a performance guarantee for a policy that adapts its spatial resolution to observed evidence, under a class of nonparametric reward functions. It permits a direct comparison with a fixed-bin policy under the same smoothness and margin conditions. The paper proves the rate and discusses optimality in a minimax sense when $K=2$ §5, pp. 22–27. This mission asks for a machine-checked proof of the stated finite-$\alpha$ regime; the Lean goal and milestones are currently open statements, so the paper's proof is the mathematical source rather than a completed formal proof.

A completed development would make the stochastic model, adaptive policy, cell geometry, and concentration estimates reusable for other contextual bandit analyses.

Difficulty

The main difficulty is the feedback loop between decisions and observations. A cell receives samples only when the covariate lands there, and its available arms depend on eliminations in its ancestors. Applying an ordinary concentration inequality to a fixed sequence of arm rewards does not by itself justify the bound at these random birth and stopping times. The formal proof must track the inherited active sets and the samples collected after each birth, then combine local error bounds across the tree. The appendix's maximal inequality controls a range of round counts; the regret argument also uses the small probability of covariates with nearly tied arm means §5, pp. 23–27 and Lemma A.1, p. 28.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin d) and a probability measure on its unit cube. The lower density bound ensures every valid dyadic cell has positive probability, so its conditional mean is defined by a real quotient. A consistent half-open boundary assignment turns the paper's cells, which are specified up to Lebesgue-null boundaries, into a partition on every path. The policy is a recursive state machine: at time $t$ it receives $X_t$, chooses an arm from its prior state, and updates with only the reward of that arm. It does not receive the unknown means or any unobserved potential reward. The existential constant in the goal is quantified before $K$, $n$, the sample space, and the machine.

The finite-$\alpha$ goal includes $\alpha\beta\le d$. The printed theorem omits it, although the proof uses it. Without it, a two-arm machine with constant means $1$ and $0$ has regret from the policy's first exploratory round, while the printed bound tends to zero when $\alpha$ is large. The $\alpha=\infty$ clause reads the margin condition as $P_X(0<f^\star-f^\sharp\le\delta_0)=0$, the limit of $C_0\delta^\alpha$ for $\delta<1$, because the page does not define it. The (5.3) milestone uses $\overline{\log}$: the printed ordinary logarithm can be nonpositive at a finest cell, while the left side is a positive integer. The cell parameter $T_B=n|B|^d$ and bursting after a full round follow Policy 3 and the proof where nearby prose or pseudocode differs. Lemma A.1 adds $\mathbb EZ_1=0$ and $a<b$, both implicit on the page. The constants $c_2$ and $C_\ell$ are existential and placed after the class parameters, because the page's explicit $c_2=c_1^\alpha/\underline c$ omits the margin constant $C_0$.

The probabilistic error displays (5.6)–(5.9) and (5.11)–(5.14) are not milestones. They are statements about the events $\mathcal A_B=\{\underline{\mathcal I}_B\subseteq\mathcal I_B\subseteq\bar{\mathcal I}_B\}$ and $\mathcal G_B$, which the page leaves undefined for cells that are never born or never finish $\ell_B$ rounds. The decomposition (5.8) also leaves out arms of $\underline{\mathcal I}_B$ that were eliminated at an ancestor of $B$. A faithful encoding of these events is welcome as a contribution.

A complete proof needs measurable recursive policies, conditional expectations and independence, dyadic-cell volume and nesting facts, concentration for arm observations at adaptive times, and sums over tree depths. Contributions establishing these interfaces and the paper's intermediate bounds are welcome. The result must apply to every machine in the stated class. Each of the following would change the theorem: a policy that reads the unknown $f^{(i)}$ or unobserved rewards (the oracle has zero regret), a constant chosen after the machine, a covariate law that is not a probability measure on the cube, Hölder continuity in the sup norm instead of the Euclidean norm, or dropping the density lower bound (cells of zero mass would make $\bar f_B$ a junk value). The paper's proofs are in §5 (pp. 23–27) and its Appendix (p. 28).

Selected references

• Jean-Yves Audibert and Alexandre B. Tsybakov, Fast learning rates for plug-in classifiers, Annals of Statistics 35(2):608–633, 2007, DOI:10.1214/009053606000001217.
• Eyal Even-Dar, Shie Mannor and Yishay Mansour, Action elimination and stopping conditions for the multi-armed bandit and reinforcement learning problems, Journal of Machine Learning Research 7:1079–1105, 2006, jmlr.org/papers/v7/evendar06a.
• Philippe Rigollet and Assaf Zeevi, Nonparametric bandits with covariates, COLT 2010, pp. 54–66, arXiv:1003.1630.
• Vianney Perchet and Philippe Rigollet, The multi-armed bandit problem with covariates, Annals of Statistics 41(2):693–721, 2013, pinned arXiv:1110.6084v3, DOI:10.1214/13-AOS1101.

Motivation

Wasserstein distributionally robust optimization (DRO) replaces the empirical risk $\mathbb E_{P_n}[f]$ of a loss $f$ by its worst case over all distributions within Wasserstein distance $\rho$ of the empirical law $P_n$. Gao, Chen and Kleywegt (arXiv:1712.06050; Operations Research, 2024, doi:10.1287/opre.2022.2383) show that, for small radii, this worst-case risk is the empirical risk plus $\rho$ times a variation of the loss (a norm of its gradient or local slope), up to a remainder. This links DRO to gradient-norm regularization, as used in adversarial training and in data-driven newsvendor and pricing models.

For smooth losses the remainder is of order $\rho^2$. Many losses used in practice are only piecewise smooth: hinge, ReLU networks, newsvendor costs, $\theta z \wedge 1$. Near the set $\mathcal D_f$ where the pieces meet, the first-order expansion fails, and the paper's Theorem 1(I)–(II) carries an extra boundary term $M\,\mathbb E_{P_n}[(\rho - d(z,\mathcal D_f))_+]$. Theorem 1(III) shows that this term is small with high probability, uniformly over the loss class, provided the data distribution does not concentrate near the non-smooth points. This mission formalizes that probabilistic bound.

Setting

Let $(\mathcal Z, d)$ be a metric space with its Borel $\sigma$-algebra, $P_{\rm true}$ a probability measure on $\mathcal Z$, and $z_1, \dots, z_n$ an i.i.d. sample from $P_{\rm true}$, with empirical law $P_n = \frac1n\sum_i \delta_{z_i}$. The sampling law is the product $P_\otimes = P_{\rm true}^{\otimes n}$ on $\mathcal Z^n$, and $\mathbb E_\otimes$ is its expectation. The formal statements also assume the metric space is second countable.

Let $\mathcal F$ be a set of losses $f : \mathcal Z \to \mathbb R$, and for each $f$ let $\mathcal D_f \subseteq \mathcal Z$ be its non-smooth set: for a piecewise smooth $f$ with pieces $\mathcal Z_{f,1}, \dots, \mathcal Z_{f,K_f}$, the union of the pairwise intersections of their closures (Assumption 1). The paper assumes $\mathcal D_f$ is $P_{\rm true}$-null. The distance to a set is $d(z, D) = \inf_{\tilde z\in D} d(z,\tilde z)$, with $d(z,\varnothing) = +\infty$.

The objects of the mission are:

• the boundary gap $(\rho - d(z, \mathcal D_f))_+$ and the near indicator $\mathbf 1\{d(z,\mathcal D_f) < \rho\}$;
• the indicator class $\mathcal I_\rho = \{z\mapsto \mathbf 1\{d(z,\mathcal D_f)<\rho\} : f\in\mathcal F,\ \mathcal D_f\neq\varnothing\}$;
• the empirical Rademacher complexity $\mathfrak R_n(\mathcal H) = \mathbb E_\sigma\bigl[\sup_{h\in\mathcal H}\frac1n\sum_i\sigma_i h(z_i)\bigr]$ of a class $\mathcal H$, with i.i.d. uniform signs $\sigma_i$, and the Rademacher complexity $\mathbb E_\otimes[\mathfrak R_n(\mathcal H)]$;
• Assumption 3 (bounded density):

$$\limsup_{\delta\downarrow 0}\ \sup_{f\in\mathcal F:\,\mathcal D_f\ne\varnothing}\frac{P_{\rm true}\{z : 0 < d(z,\mathcal D_f) < \delta\}}{\delta} < \infty.$$

In Lean the boundary gap is the shared WassVarReg.PInf.boundaryGap; nearIndicator, indicatorClass, empRademacher, rademacher and Assumption3 are in WassVarReg.Boundary. The sample law is the published MinimaxWass.DataDep.sampleLaw.

Formalization targets

Goal: Theorem 1(III), first display (p. 8)

Under Assumption 3 there exist $\bar\rho, C > 0$ such that for all $n\ge1$, $t>0$ and $0\le\rho<\bar\rho$, with probability at least $1-e^{-t}$, for every $f\in\mathcal F$,

$$\mathbb E_{P_n}\bigl[(\rho - d(z,\mathcal D_f))_+\bigr] \le C\rho^2 + 2\rho\,\mathbb E_\otimes[\mathfrak R_n(\mathcal I_\rho)] + \rho\sqrt{\frac{t}{2n}}.$$

The constants $C$ and $\bar\rho$ are left unspecified; they depend only on Assumption 3.

Milestones

1. Lemma EC.5 (p. ec4): for a class $\mathcal H$ of measurable functions with values in $[0,M]$, with probability at least $1-e^{-t}$, $\mathbb E_{P_n}[h] \le \mathbb E_{P_{\rm true}}[h] + 2\,\mathbb E_\otimes[\mathfrak R_n(\mathcal H)] + M\sqrt{t/(2n)}$ for all $h\in\mathcal H$.
2. Assumption 3 bounds the true mass (proof of Lemma EC.11, p. ec11): $\mathbb E_{P_{\rm true}}[\mathbf 1\{d(z,\mathcal D_f)<\rho\}] \le C\rho$ for $0\le\rho<\bar\rho$, uniformly in $f$.
3. Lemma EC.11 (p. ec11): with probability at least $1-e^{-t}$, for every $f$, $\mathbb E_{P_n}[\mathbf 1\{d(z,\mathcal D_f)<\rho\}] \le C\rho + 2\,\mathbb E_\otimes[\mathfrak R_n(\mathcal I_\rho)] + \sqrt{t/(2n)}$.
4. Gap versus mass (p. ec11): $\mathbb E_{P_n}[(\rho-d(z,\mathcal D_f))_+] \le \rho\,\mathbb E_{P_n}[\mathbf 1\{d(z,\mathcal D_f)<\rho\}]$.

Significance

The result. With $\rho_n = \rho_0/\sqrt n$ and a class $\mathcal I_\rho$ of bounded complexity, the right side of the goal is $O_p(1/n)$. Combined with Theorem 1(I)–(II), it gives the paper's conclusion that $p$-Wasserstein DRO with $p\in(1,\infty]$ is asymptotically equivalent to empirical variation regularization, $\min_f\{\mathbb E_{P_n}[f] + \rho_n\mathcal V_{P_n,q}(f)\} + O_p(1/n)$, for non-smooth losses, uniformly over the class. Without it, the boundary term is only bounded by $M\rho$, and the expansion has no better accuracy than first order. Assumption 3 is the condition under which the non-smooth set does not matter statistically.

Formalizing it. The result is proved in the paper; it has no machine-checked proof. Its proof composes a uniform deviation bound (McDiarmid's inequality plus symmetrization) with a bounded-density estimate. The mission produces a general Rademacher deviation bound for bounded classes on an arbitrary metric space with a measurability guard, reusable by any statistical-learning mission, and fixes the printed constant of Lemma EC.5 ($M\sqrt{2t/n}$ on the page, $M\sqrt{t/(2n)}$ from its proof).

Difficulty

The deterministic parts are short. The difficulty is in Lemma EC.5. McDiarmid's inequality must be applied to the uniform deviation over an arbitrary, possibly uncountable, class. Symmetrization must then be carried out with Bochner integrals over $\mathcal Z^n\times\mathcal Z^n$ and a finite sign space. Neither tool is in Mathlib in this form. A tempting shortcut, bounding each fixed $h$ by Hoeffding's inequality and taking a union bound, fails: the class is infinite, and the bound must hold simultaneously for all $f$ inside a single event. A second point is Assumption 3: it controls only the shell $0 < d(z,\mathcal D_f) < \delta$, so the mass of $\{d = 0\}$ has to come from the null closure of $\mathcal D_f$.

Formalization scope

• Space and sample. $\mathcal Z$ is a metric space with [MeasurableSpace Z] [BorelSpace Z] [SecondCountableTopology Z] in the goal-level statements. Second countability is an added technical hypothesis used throughout this paper's mission series. A sample is ω : Fin n → Z with $n\ge1$, and its law is Measure.pi. Empirical means are $\frac1n\sum_{i : \mathrm{Fin}\,n}$.
• Distance to a set. Metric.infEDist, which is $+\infty$ on $\varnothing$. A loss with $\mathcal D_f=\varnothing$ thus has boundary gap $0$ and is excluded from $\mathcal I_\rho$, as on the page. The real-valued Metric.infDist (which is $0$ on $\varnothing$) would give such a loss gap $\rho$ and is not used.
• The non-smooth sets are an arbitrary family D : (Z → ℝ) → Set Z. The goal-level statements assume each $\mathcal D_f$ is closed and $P_{\rm true}$-null, the standing consequence of its construction in Assumption 1. The details of the piecewise smooth loss model are not needed for this probability estimate.
• Probabilities are written as $P_\otimes\{\omega : \neg\,\forall f\in\mathcal F, \dots\}\le e^{-t}$, with the quantifier over $\mathcal F$ inside the event (an outer measure for uncountable $\mathcal F$).
• Rademacher complexity. The sign expectation is an average over $\{\pm1\}^n$. Suprema are real suprema of classes with values in $[0,M]$; an empty class gives $0$. $\mathbb E_\otimes$ is a Bochner integral.
• Measurability guard (added): the uniform deviation, the empirical Rademacher complexity and the double-sample deviation of the class are measurable. This holds, for instance, for countable $\mathcal F$, and the paper leaves it implicit.
• Quantifier order. $\bar\rho$ and $C$ are chosen before $n$ and $t$, which is stronger than the page's order. The radius satisfies $\rho\ge0$.
• Not stated. The second display of Theorem 1(III) and the "Moreover" part of Lemma EC.11, which use Dudley's entropy integral: their proof bounds the empirical Rademacher complexity, while Lemma EC.5 needs its expectation.
• Trivialization ruled out. The Rademacher term is that of the specific class $\mathcal I_\rho$ built from the sets $\mathcal D_f$. It is not a free constant, and no hypothesis assumes the conclusion of Lemma EC.5.

Contributions welcome: a general McDiarmid inequality for product measures, a symmetrization lemma for measurable classes, and proofs of the milestones in any order.

Selected references

• R. Gao, X. Chen, A. J. Kleywegt, Wasserstein Distributionally Robust Optimization and Variation Regularization, Operations Research, 2024. arXiv:1712.06050, doi:10.1287/opre.2022.2383
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Theorem 26.5. doi:10.1017/CBO9781107298019
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Series 141, 1989. doi:10.1017/CBO9781107359949.008
• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Ch. 5. doi:10.1017/9781108627771

Motivation

Retailers set prices and stock levels without knowing how demand responds to price. They must learn the demand curve from their own sales while still earning money, which is the exploration–exploitation trade-off of dynamic pricing with learning (den Boer 2015). Two features of practice make the problem harder than the textbook bandit. First, demand is censored: when the shelf runs empty, the firm sees only its sales $\min\{d_t,y_t\}$, not the demand $d_t$. Second, firms change prices rarely, because of menu costs and customer reaction, so a policy may change its price at most $m$ times over the whole horizon (Cheung, Simchi-Levi and Wang 2017).

Chen, Chao and Wang study a firm facing both features at once, in a parametric model where the demand distribution is known up to a parameter. For the well-separated case they give an algorithm, Algorithm-I, whose regret grows as $T^{1/(m+1)}$, and they show that no admissible policy does better in general. This mission formalizes the upper bound. A companion mission formalizes the lower bound.

Setting

A firm sells one product over periods $t=1,\dots,T$. At the start of period $t$ it holds inventory $x_t$ (with $x_1=0$). It chooses a price $p_t\in\mathcal P=[p^l,p^h]$ and an order-up-to level $y_t\in\mathcal Y=\{y^l,\dots,y^h\}$ with $y_t\ge x_t$, and the order arrives at once. Demand $d_t$ then has probability mass function $f(\cdot;p_t,z)$ on $\{d^l,d^l+1,\dots,d^h\}$, where $d^h\le+\infty$ and the parameter $z$ lies in $\mathcal Z=[z^l,z^h]$, $0\le z^l\le z^h$. Unmet demand is lost, and the firm observes only the sales $\min\{d_t,y_t\}$. Leftover stock carries over, $x_{t+1}=(y_t-d_t)^+$. Each unit left over costs $h\ge0$ and each lost sale costs $b\ge0$. The single-period expected profit is

$$G(p,y,z)=p\,\mathbb E[D(p,z)]-h\,\mathbb E[y-D(p,z)]^+-(b+p)\,\mathbb E[D(p,z)-y]^+ .$$

For each $y$, $p^*_y(z)$ is an optimal price, $\max_{p\in\mathcal P}G(p,y,z)=G(p^*_y(z),y,z)$, and the clairvoyant value is $G^*(z)=\max_{(p,y)\in\mathcal P\times\mathcal Y}G(p,y,z)$.

A policy's decision in period $t$ may depend only on past decisions and past sales. The regret of a policy is

$$R(T)=T\,G^*(z)-\mathbb E[V^\phi(T,z)]=\sum_{t=1}^T\mathbb E\big[G^*(z)-G(p_t,y_t,z)\big].$$

The family is well-separated (Definition 1) if for every price the pmfs $f(\cdot;p,z)$, $z\in\mathcal Z$, are pairwise distinct.

Algorithm-I splits the horizon into $m+1$ stages of lengths $I_i=\lceil T^{i/(m+1)}\rceil$ for $i\le m$, with $I_{m+1}=T-\sum_{i\le m}I_i$. Stage $i$ uses one price $\hat p_i$ and the order-up-to target $\tilde y_i$. The target equals the planned level $\hat y_i$, raised by $\Delta\ge1$ when $\hat y_i=d^l$ so that the sales carry information. At the end of the stage the algorithm computes the censored-data maximum-likelihood estimate $\hat z_i$ (5). It then sets the next stage's decisions to a maximizer of $G(\cdot,\cdot,\hat z_i)$ (6). It changes its price at most $m$ times.

Formalization targets

Goal: Theorem 1

Under Assumption A (regularity of $G$ and of $p^*_y$ near the true $z$), Assumption 1 (Fisher-information bounds, a positive lower bound on the pmf, strict monotonicity of $f(d^l;p,\cdot)$), Definition 1, and the condition that every optimal order-up-to level exceeds $d^l$, there is $K_6>0$ such that for all large $T$

$$R(T)\le K_6\,T^{\frac1{m+1}} .$$

The constant may depend on the model, the true parameter and the algorithm's inputs. The rate $T^{1/(m+1)}$ is the content.

Milestones

1. Theorem B1: if an estimator satisfies $\mathbb P\{\|\hat z-z\|\ge\epsilon\}\le K_{14}e^{-nK_{15}\epsilon^2}+K_{16}/n$, then the plug-in decision has optimality gap $G^*(z)-\mathbb E[G(\hat p^*,\hat y^*,z)]\le K_{17}/n$.
2. Proposition 1: the censored MLE satisfies $\mathbb P\{|z-\hat z_i|\ge\epsilon\}\le K_3e^{-K_4I_i\epsilon^2}+K_5/I_i$.
3. Per-stage estimation regret (p. 25): $\mathbb E[G^*(z)-G(\hat p_i,\hat y_i,z)]\le K_{17}/I_{i-1}$.
4. (25): the summed estimation regret is at most a constant times $mT^{1/(m+1)}$.
5. (26): $\mathbb P(\hat y_i\ne\tilde y_i)\le K/I_{i-1}$, so exploration after stage 1 is rare.

Significance

The upper bound shows that a budget of $m$ price changes costs only a $T^{1/(m+1)}$ regret even under censoring. With $m$ of order $\log T$ the rate drops to logarithmic (Theorem 3 of the paper). Together with the matching lower bound (Theorem 2), it identifies the exact price of limiting price changes in this model. Theorem B1 is a general transfer principle, from a large-deviation bound on an estimate to a $1/n$ optimality gap of the plug-in decision. It allows continuous and discrete decisions together and needs no unique optimizer. It is reusable for any parametric learning problem with that structure. Proposition 1 is a large-deviation bound for maximum likelihood from censored, dependent, non-identically distributed data. The paper notes that such results were not previously available in the statistics literature.

The results are proved in the paper's appendices. None of them has a machine-checked proof. A formalization would check the regret decomposition (23), the stagewise bookkeeping with ceilings, and the large-deviation argument for the censored MLE. It would also make the reading of several loosely stated steps exact (see Formalization scope).

Difficulty

The obvious argument plugs a consistent estimator into the optimizer and bounds the regret by the estimation error. It fails twice. The error of $\hat z_i$ is of order $I_{i-1}^{-1/2}$, so a Lipschitz bound on the profit would give regret of order $I_i/\sqrt{I_{i-1}}$ per stage, which is too large. The $1/n$ rate of Theorem B1 needs the first-order condition at an interior optimum and the exact gap $\delta$ between optimal and suboptimal discrete levels. Second, the data are censored and dependent. The censoring level $y_t$ depends on carried inventory, which depends on past demand and on past prices. The classical large-deviation results for maximum likelihood assume i.i.d. uncensored samples (Borovkov 1998) and do not apply. Proposition 1 needs a separate argument that the inventory target is reached in most periods with high probability.

Formalization scope

The model is encoded with a scalar parameter. $\mathcal P$, $\mathcal Y$ and $\mathcal Z$ are as above. The pmf is positive exactly on $\{d^l,\dots,d^h\}$ and sums to one, and $d^h=+\infty$ is allowed. The expected profit $G$ is built from these sums. $G^*(z)$ is the finite maximum $\max_{y}G(p^*_y(z),y,z)$ for a price selection $p^*$, not a real supremum. Periods are 0-based in Lean, while stages keep the paper's indices. Expectations and probabilities are sums over demand paths $d\in\mathbb N^T$ weighted by $\prod_tf(d_t;p_t,z)$, the law of the path under the algorithm, taken in $[0,\infty]$. Every regret summand is nonnegative.

Algorithm-I reads demand only through sales. Step 2's arg max is any maximizer of the censored product likelihood, which exists by compactness. Step 3's arg max is $\hat y$, any maximizer of $y\mapsto G(p^*_y(\hat z),y,\hat z)$, together with the price $p^*_{\hat y}(\hat z)$ of Assumption A(iii). This is the decision the proof of Theorem B1 analyses. Proposition 1's "large enough $i$" is read as "large enough $T$, uniformly in the stage and in $\epsilon$". Theorem B1 is stated for a scalar price and level and a parameter in $\mathbb R^k$.

Three hypotheses are added and disclosed. Differentiability of $f$ in $z$ is presupposed by Assumption 1. Finiteness of the mean demand is needed for (4) when $d^h=\infty$. The condition $d^l\le y^l$ is needed because Step 1 defines the target only for $\hat y\ge d^l$. "The optimal order-up-to level exceeds $d^l$" is read for every optimal level.

A trivializing formalization is ruled out. Regret and probabilities are path sums of nonnegative terms, not Bochner integrals that vanish on non-integrable inputs. $T^{1/(m+1)}$ is a real power. The hypotheses are jointly satisfiable: a Bernoulli instance with $\mathcal Y=\{1\}$, $\mathcal P=[1,2]$, $\mathcal Z=[2/3,4/5]$, $f(0;p,z)=zp/2$ satisfies all of them, together with explicit selections, and this has been verified in Lean.

A complete development needs the following:

• Hoeffding-type concentration for dependent bounded sums;
• a large-deviation bound for the censored log-likelihood;
• Taylor's theorem with integral remainder on an interval;
• bookkeeping lemmas for the stage lengths $\lceil T^{i/(m+1)}\rceil$.

Theorem B1 and the model definitions are reusable for the paper's later results (Theorems 3, 5, 6), which repeat these arguments. Contributions to any milestone are welcome, including alternative proofs of Proposition 1.

Selected references

• B. Chen, X. Chao, Y. Wang, Data-Based Dynamic Pricing and Inventory Control with Censored Demand and Limited Price Changes, Operations Research (technical note), 2020; read in the SSRN revision of 2020-02-10. https://doi.org/10.1287/opre.2020.1993, https://ssrn.com/abstract=2700747
• W. C. Cheung, D. Simchi-Levi, H. Wang, Dynamic Pricing and Demand Learning with Limited Price Experimentation, Operations Research 65(6), 2017. https://doi.org/10.1287/opre.2017.1629
• J. Broder, P. Rusmevichientong, Dynamic Pricing under a General Parametric Choice Model, Operations Research 60(4), 2012. https://doi.org/10.1287/opre.1120.1057
• A. A. Borovkov, Mathematical Statistics, Gordon and Breach, 1998.
• A. V. den Boer, Dynamic pricing and learning: Historical origins, current research, and new directions, Surveys in Operations Research and Management Science 20(1), 2015. https://doi.org/10.1016/j.sorms.2015.03.001

Motivation

A seller who changes prices while learning demand faces two costs: a price experiment may earn less revenue now, while insufficient experimentation leaves later prices poorly calibrated. Customer features make the balance harder because both willingness to buy and sensitivity to price may vary between customers. Ban and Keskin study this problem when the number of recorded features can be large relative to the selling horizon. Their known-support policy, ILSX, provides the upper bound formalized here Ban and Keskin, 2021, §§2 and 4.1.

The paper's result is a statement about learning a demand model while serving sequential customers, rather than about fitting that model after all observations are available. A price at period $t$ must use information then available, including the arriving customer's features but excluding that customer's demand shock. The seller therefore needs a policy whose expected revenue loss can be bounded uniformly over the unknown parameters in a specified model Ban and Keskin, 2021, pp. 5552–5556.

Setting

In each period $t=1,2,\ldots$, a customer arrives with a feature vector $Z_t\in\mathbb R^d$. The seller observes the augmented vector $X_t=[1;Z_t]$, posts a price $p_t\in[\ell,u]$ with $0<\ell<u$, and then observes demand. In the linear demand model, demand equals

$$D_t=\alpha\cdot X_t+(\beta\cdot X_t)p_t+\varepsilon_t.$$

The intercept and slope vectors $\alpha,\beta$ are unknown. The seller knows the sparsity structure $\mathcal S$: outside this set of coordinate indices, both parameter vectors vanish. The compressed parameter $\theta_{\mathcal S}=(\alpha_{\mathcal S},\beta_{\mathcal S})$ lies in a compact coordinate rectangle $\Theta_{\mathcal S}$, and $s=|\mathcal S|\ge1$. The compressed customer vector is $X_{\mathcal S,t}=(X_{t,i})_{i\in\mathcal S}$ Ban and Keskin, 2021, pp. 5552–5555.

At price $p$, expected single-period revenue is $r(p,\theta_{\mathcal S},x)=p[\alpha_{\mathcal S}\cdot x+(\beta_{\mathcal S}\cdot x)p]$. The clairvoyant price is $\varphi(\theta_{\mathcal S},x)=-(\alpha_{\mathcal S}\cdot x)/(2\beta_{\mathcal S}\cdot x)$ when the slope is negative. The paper assumes this price is in $(\ell,u)$ throughout its model domain. Expected regret $\Delta^{\pi}_{\theta_{\mathcal S}}(T)$ is the expected sum, through period $T$, of the clairvoyant revenue minus the revenue at the policy's price Ban and Keskin, 2021, (2)–(4), p. 5553–5554.

The ILSX policy charges one fixed experimental price $m_1$ at periods $1,4,9,\ldots$ and a distinct price $m_2$ at periods $2,5,10,\ldots$. At every other period it estimates the compressed demand parameter by least squares using experimental observations, projects the estimate onto $\Theta_{\mathcal S}$, and applies $\varphi$ to the projected estimate and the current customer vector. Both prices lie in $[\ell,u]$ Ban and Keskin, 2021, (7), (8), (12), pp. 5555–5556.

Formalization targets

The goal is Theorem 2: for the stated model and ILSX policy, a finite positive constant $C$ exists such that

$$\Delta^{\mathrm{ILSX}(m_1,m_2)}_{\theta_{\mathcal S}}(T)\le Cs\sqrt T\log T\qquad(\theta_{\mathcal S}\in\Theta_{\mathcal S},\ T\ge2).$$

The constant is chosen after the model, shock process, experimental prices, and estimator selection are fixed, but before the parameter and horizon. The theorem and Remark 5 are on pp. 5556–5557 of Ban and Keskin, 2021.

The milestones reproduce the paper's route into this claim: the experimental-period count following (7); the growth bound (15) for the price-variation statistic $J_t$; Lemma 1's minimum-eigenvalue probability bound for the experimental information matrix $\widetilde{\mathcal J}_{\mathcal S,t}$; and Lemma 2's high-probability bound for its noise-driven estimation error. The least-squares error identity (11) is included as a supporting item on invertible samples, not as a milestone. The constants and thresholds in these targets remain existential where the article leaves them existential Ban and Keskin, 2021, pp. 5555–5556.

Significance

The theorem gives a guarantee for a concrete pricing policy under feature-dependent price sensitivity. The bound grows with the horizon at order $\sqrt T\log T$ for a fixed known support, with an explicit factor $s$ in the published statement. It lets a seller compare the cost of this policy with the revenue of a seller who knew the demand coefficients before pricing. The paper presents its result as matching its lower-bound benchmark up to logarithmic factors, under the paper's respective hypotheses Ban and Keskin, 2021, Theorems 1–2, pp. 5554–5556.

The mathematical result was published in 2021. This mission seeks a machine-checked statement and proof of the known-support guarantee and its stated intermediate results. The checked Prove2Me prior-art catalog contains featureless dynamic-pricing results and separate least-squares results, but no matching formalization of ILSX. A completed development would add reusable definitions for a feature-dependent price regressor, experimental information matrix, nonanticipating estimator selection, and expected regret. The article places its proofs in an electronic companion, which is not included in the held source PDF; this mission does not reproduce those proofs as source material.

Difficulty

The policy learns from a sparse set of deliberately chosen periods, while its regret accumulates at every period. A pointwise least-squares identity alone does not control the regret: the information matrix can be singular at early periods, and the customer features and shocks are random. In particular, the printed inverse identity (11) says “for all $t\ge2$”, although at $t=2$ the matrix has rank at most two and cannot be invertible when $s\ge2$. The formal statement therefore confines the inverse identity to invertible samples. Lemma 2's event also includes invertibility so a default inverse of a singular matrix cannot make its error bound automatic Ban and Keskin, 2021, (9)–(11), Lemma 2, p. 5556.

Formalization scope

Lean uses one-based periods and a support subtype of the augmented feature coordinates. Coordinate zero is the paper's intercept coordinate one. The parameter has coordinates $(j,i)$ for demand intercept or price slope $j\in\{0,1\}$ and support index $i\in\mathcal S$. The regressor $[1;p]\otimes X_{\mathcal S,t}$ gives the information matrix in (10). Euclidean squared norms are explicit sums of squares, and the minimum-eigenvalue claim is the equivalent Rayleigh inequality. The parameter rectangle is nonempty, and its Euclidean projection is coordinatewise clamping.

The standing assumptions are $d\ge1$, $s\ge1$, $0<\ell<u$, distinct experimental prices in $[\ell,u]$, bounded i.i.d. features with mean zero and positive-definite covariance, and a fixed shock process with conditional mean zero, bounded conditional second moment, and finite conditional exponential moments near zero. The feature process is measurable and integrable. The model additionally states independence of the next customer's features from the past primitives, the reading of the paper's joint probability construction used here. The slope is negative and the clairvoyant price lies in $(\ell,u)$ for every allowed parameter and realized feature. These conditions ensure that the price formula represents a genuine revenue maximum. The phrase about continuous features having positive measure in the interior of their domains is omitted because the page does not specify the domains or a reference measure Ban and Keskin, 2021, §2, pp. 5552–5554.

The estimator is any measurable minimizer of the experimental least-squares objective for histories with at least two observations. Its type depends only on earlier observations; at nonexperimental periods the recorded pseudo-observations are ignored by the objective. The shock law is fixed while the parameter varies. Expected regret uses a nonnegative integral, and conditional second and exponential moments use nonnegative conditional expectations. The theorem binds $C$ before the parameter and horizon, while leaving support size fixed with the model. Consequently, the stronger uniformity in $s$ suggested by Remark 5 is outside this statement. These choices exclude vacuous integrals, unconstrained estimators, and accidental bounds from a singular matrix inverse. Work on the probability estimates, least-squares identity, and regret bound is welcome under these exact definitions.

Selected references

• G.-Y. Ban and N. B. Keskin, Personalized Dynamic Pricing with Machine Learning: High-Dimensional Features and Heterogeneous Elasticity, Management Science 67(9):5549–5568, 2021. DOI: 10.1287/mnsc.2020.3680.

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

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