Probability

Motivation

In ordinary statistical learning, a hypothesis is chosen from training data drawn from a distribution $P$ and judged by its risk under that same $P$. In practice the test distribution often differs from the training one: covariate shift, domain drift, adversarial perturbation of inputs. Distributionally robust learning replaces the risk at $P$ by the worst risk over a neighbourhood of $P$. When the neighbourhood is a ball in a Wasserstein distance, the perturbed distributions may move mass to nearby points of the instance space rather than only reweight the observed ones, which makes the model a natural description of small domain drifts and adversarial perturbations (Esfahani–Kuhn 2018, Gao–Kleywegt 2016, Sinha–Namkoong–Duchi 2018).

Lee and Raginsky (NeurIPS 2018) asked whether minimising the empirical version of this worst-case risk learns: does the empirical minimiser come close, in worst-case risk, to the best hypothesis of the class, at the usual $1/\sqrt n$ rate? Their §3.2 answers yes when every hypothesis is uniformly Lipschitz. Their §3.3, the subject of this mission, removes that assumption: one hypothesis with controlled growth is enough.

Setting

The instance space $\mathcal Z$ is a Polish metric space with metric $d_{\mathcal Z}$ and Borel $\sigma$-algebra; fix $p\ge1$. For Borel probability measures $P,Q$ on $\mathcal Z$, the $p$-Wasserstein distance is

$$W_p(P,Q)=\Bigl(\inf_{M}\ \mathbf E_M[d^p_{\mathcal Z}(Z,Z')]\Bigr)^{1/p},$$

the infimum over couplings $M$ of $P$ and $Q$. For a radius $\varrho>0$, $B^W_{\varrho,p}(P)=\{Q:W_p(P,Q)\le\varrho\}$ is the Wasserstein ball around $P$.

A hypothesis is a function $f:\mathcal Z\to\mathbb R$, read as a loss; a hypothesis class is a set $\mathcal F$ of them. The risk of $f$ under $Q$ is $R(Q,f)=\int f\,dQ$. The local worst-case risk and the local minimax risk are

$$R_{\varrho,p}(P,f)=\sup_{Q\in B^W_{\varrho,p}(P)}R(Q,f),\qquad R^*_{\varrho,p}(P,\mathcal F)=\inf_{f\in\mathcal F}R_{\varrho,p}(P,f).$$

Given i.i.d. samples $Z_1,\dots,Z_n\sim P$ with empirical distribution $P_n=\frac1n\sum_i\delta_{Z_i}$, the local minimax ERM is

$$\hat f\in\arg\min_{f\in\mathcal F}R_{\varrho,p}(P_n,f).$$

The standing assumptions are:

• Assumption 1. $\mathcal Z$ is bounded: $\mathrm{diam}(\mathcal Z)=\sup_{z,z'}d_{\mathcal Z}(z,z')<\infty$.
• Assumption 2. Every $f\in\mathcal F$ is upper semicontinuous with $0\le f(z)\le M$.
• Assumption 4. Some $f_0\in\mathcal F$ satisfies $f_0(z)\le C_0\,d^p_{\mathcal Z}(z,z_0)$ for all $z$, for some $C_0\ge0$ and $z_0\in\mathcal Z$.

The complexity of $\mathcal F$ is measured by the entropy integral $\mathfrak C(\mathcal F)=\int_0^\infty\sqrt{\log\mathcal N(\mathcal F,\|\cdot\|_\infty,u)}\,du$, where $\mathcal N$ is the covering number of $\mathcal F$ in the uniform norm.

Formalization targets

Goal: Theorem 3, display (11)

Under Assumptions 1, 2 and 4, for every $\delta\in(0,1)$, with probability at least $1-\delta$,

$$R_{\varrho,p}(P,\hat f)-R^*_{\varrho,p}(P,\mathcal F)\le\frac{48\,\mathfrak C(\mathcal F)}{\sqrt n}+\frac{24\,C_0(2\,\mathrm{diam}(\mathcal Z))^p}{\sqrt n}\Bigl(1+\Bigl(\frac{\mathrm{diam}(\mathcal Z)}{\varrho}\Bigr)^p\Bigr)+3M\sqrt{\frac{\log(2/\delta)}{2n}}.$$

Milestones

1. Proposition 4 (Gao–Kleywegt strong duality): $R_{\varrho,p}(Q,f)=\min_{\lambda\ge0}\{\lambda\varrho^p+\mathbf E_Q[\varphi_{\lambda,f}(Z)]\}$ with $\varphi_{\lambda,f}(z)=\sup_{z'}\{f(z')-\lambda d^p_{\mathcal Z}(z,z')\}$, in the bounded setting.
2. Lemma 2: the optimal dual multiplier of a minimiser of $R_{\varrho,p}(Q,\cdot)$ lies in $\Lambda=[0,\,C_0 2^{p-1}(1+(\mathrm{diam}(\mathcal Z)/\varrho)^p)]$.
3. (C.2): for an achiever $f^*$ of $R^*_{\varrho,p}(P,\mathcal F)$, $R_{\varrho,p}(P_n,f^*)-R_{\varrho,p}(P,f^*)\le\int\varphi_{\lambda^*,f^*}\,d(P_n-P)$.
4. (C.3): $R_{\varrho,p}(P,\hat f)-R_{\varrho,p}(P_n,\hat f)\le\sup_{\varphi\in\Phi}\int\varphi\,d(P-P_n)$, with $\Phi=\{\varphi_{\lambda,f}:\lambda\in\Lambda,f\in\mathcal F\}$.
5. (C.4): with probability at least $1-\delta/2$, the left side of (C.3) is at most $2\mathfrak R_n(\Phi)+M\sqrt{2\log(2/\delta)/n}$, where $\mathfrak R_n$ is the expected Rademacher average.
6. (C.5): with probability at least $1-\delta/2$, $R_{\varrho,p}(P_n,f^*)-R_{\varrho,p}(P,f^*)\le M\sqrt{\log(2/\delta)/(2n)}$.
7. Lemma 5: $\mathfrak R_n(\Phi)\le\frac{24}{\sqrt n}\mathfrak C(\mathcal F)+\frac{12C_0(2\,\mathrm{diam}(\mathcal Z))^p}{\sqrt n}(1+(\mathrm{diam}(\mathcal Z)/\varrho)^p)$.

The goal carries the paper's constants. The mission does not ask for sharper constants; a proof of the stated bound closes it.

Significance

The result. Theorem 3 is a generalisation guarantee for Wasserstein distributionally robust ERM that needs no uniform smoothness of the class. The uniformly Lipschitz assumption of the companion Theorem 2 fails for most classes of interest when $p>1$: a function with $\sup_{z,z'}(f(z')-f(z))/d^p_{\mathcal Z}(z,z')<\infty$ is constant (p. 6). Assumption 4 holds, for example, for regression with quadratic loss whenever the predictor class contains the zero predictor (p. 6). The second term of (11) decreases as $\varrho$ grows, which quantifies how a larger ambiguity set screens out non-smooth hypotheses (Remark 4).

Formalizing it. The theorem has a published pen-and-paper proof (Appendix C.5 of the arXiv version); it has no machine-checked proof. A formalization produces machine-checked statements of the dual characterisation of Wasserstein worst-case risk on a bounded Polish space, of a symmetrization-plus-McDiarmid uniform deviation bound for a parametrised class, and of a Dudley-entropy bound on a product class. The proof (C.5) on p. 16 starts from an achiever $f^*$ of $R^*_{\varrho,p}(P,\mathcal F)$, which need not exist; the goal is stated without that assumption, so a complete proof also handles the infimum.

Difficulty

The obvious argument decomposes the excess risk through $f^*$ and bounds $R_{\varrho,p}(P,\hat f)-R_{\varrho,p}(P_n,\hat f)$ by a uniform deviation over $\mathcal F$. That step fails: $R_{\varrho,p}(\cdot,f)$ is a supremum over a ball of measures, not an expectation, so it is not an empirical process in $f$. Passing to the dual makes it one, but the dual multiplier $\hat\lambda$ depends on the sample and has no a priori bound, so the class $\{\varphi_{\lambda,f}\}$ over all $\lambda\ge0$ is too large. Without uniform smoothness of $\mathcal F$ there is no obvious a priori bound on $\hat\lambda$, and the entropy of the resulting two-parameter class must still be controlled at rate $1/\sqrt n$. Strong duality itself (Proposition 4) needs the existence of optimal couplings and a measurable-selection argument on a Polish space; it is not in Mathlib.

Formalization scope

• $\mathcal Z$ is a MetricSpace with BorelSpace and PolishSpace instances; Assumption 1 is Bornology.IsBounded (Set.univ : Set 𝒵), and $\mathrm{diam}(\mathcal Z)$ is Metric.diam Set.univ. Throughout, $p\ge1$ and $\varrho>0$ (the paper's standing choice, p. 3).
• The Wasserstein distance and ball are the published definitions WassersteinLinOpt.Ball.wassersteinDist and wassersteinBall, which range over all Borel probability measures; on a bounded space this equals the paper's $\mathcal P_p(\mathcal Z)$ ball.
• Local risks, $\varphi_{\lambda,f}$, $\Lambda$, $\Phi$ and $\mathfrak R_n$ are real-valued suprema and infima, used only for classes bounded in $[0,M]$, where they are finite.
• The sample is a point of $\mathcal Z^n$ under $P^{\otimes n}$. "With probability at least $1-\delta$" means the outer measure of the failure set is at most $\delta$; this equals the probability when the set is measurable and is stronger otherwise.
• The ERM is a sample-indexed function $\hat f$ with hypotheses $\hat f(\omega)\in\mathcal F$ and minimality of $R_{\varrho,p}(P_n,\cdot)$. These hypotheses presuppose that an empirical minimiser exists, as (7) does. No measurability of $\hat f$ is assumed.
• The covering number is internal (centres in $\mathcal F$). $\mathfrak C(\mathcal F)$ is valued in $[0,\infty]$, and every bound containing it assumes $\mathfrak C(\mathcal F)<\infty$: otherwise the paper's bound is $+\infty$, while its conversion to a real number would be $0$.
• Proposition 4 is stated for bounded upper semicontinuous $f$ on bounded $\mathcal Z$, the only case the paper uses. The printed statement covers every usc $f$ and every $Q\in\mathcal P_p(\mathcal Z)$.
• (C.2) and (C.5) assume an achiever $f^*$, as printed; the goal does not.

The following formalizations would trivialize the goal and are ruled out: a bound for each fixed $f\in\mathcal F$ in place of $R^*_{\varrho,p}(P,\mathcal F)$; an $\hat f$ defined by Classical.choose of an unproved existence; a supremum over all measures instead of over the ball; and the real conversion of an infinite $\mathfrak C(\mathcal F)$.

The infrastructure is reusable beyond this mission: Wasserstein strong duality on Polish spaces (Proposition 4 specialises the general optimal-transport duality of Blanchet–Murthy 2019, whose transport-plan form is a proved theorem on the platform as ModelRiskOT.Duality.theorem_1); Dudley's entropy bound for sub-Gaussian processes indexed by infinite classes; and McDiarmid's inequality for suprema of empirical processes. Contributions of these general tools, as separate theorems, are welcome. Source: the arXiv v2 preprint, which is the NeurIPS 2018 camera-ready text followed by the supplementary appendices.

Selected references

• J. Lee, M. Raginsky, Minimax statistical learning with Wasserstein distances, NeurIPS 2018; arXiv:1705.07815v2. https://arxiv.org/abs/1705.07815
• R. Gao, A. J. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, arXiv:1604.02199, 2016. https://arxiv.org/abs/1604.02199
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44(2), 2019. https://doi.org/10.1287/moor.2018.0936
• 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
• A. Sinha, H. Namkoong, J. Duchi, Certifying some distributional robustness with principled adversarial training, ICLR 2018; arXiv:1710.10571. https://arxiv.org/abs/1710.10571
• R. M. Dudley, The sizes of compact subsets of Hilbert space and continuity of Gaussian processes, Journal of Functional Analysis 1, 1967. https://doi.org/10.1016/0022-1236(67)90017-1

Motivation

Data-driven decision making estimates the cost of a decision from training data and then optimizes that estimate. The optimized estimate is biased downwards: the decision that looks best on the training data tends to disappoint on fresh data. Distributionally robust optimization counters this by optimizing the worst case of the estimate over all distributions within a radius $r$ of the empirical distribution, measured by a chosen distance function $R$. Many distance functions are in use (φ-divergences, Wasserstein distances, moment sets), and the choice is usually justified by tractability.

Bertsimas and Van Parys, Bootstrap robust prescriptive analytics (arXiv:1711.09974v2), measure disappointment on bootstrap data: resamples drawn with replacement from the training data. Their Theorem 6 shows that with the entropic bootstrap distance $B$ the bootstrap disappointment decays exponentially in the sample size at rate at least $r$. Proposition 1, the subject of this mission, is the converse: $B$ is the smallest distance function with this guarantee. Any distance that is strictly larger than $B$ near some distribution admits a nominal formulation whose disappointment decays strictly slower than $e^{-nr}$. The result is in the spirit of Van Parys, Esfahani and Kuhn (arXiv:1704.04118), where the relative entropy is shown to be the optimal ambiguity set for i.i.d. data.

Setting

The distinct training points form a finite set $\Omega_n$, written $\iota$ in Lean. A distribution on it is a vector $D\in\mathbb R^\iota$ with nonnegative entries summing to one; the simplex of all such vectors is $\mathcal D_n$. The training data have the empirical distribution $D_{\rm tr}\in\mathcal D_n$, which gives positive weight to every point of $\Omega_n$.

The bootstrap distance (Definition 6, Eq. (27)) is the relative entropy

$$B(D,D')=\sum_{i\in\iota}D_i\log\frac{D_i}{D'_i},$$

with $0\log0=0$ and $B(D,D')=+\infty$ if some $D_i>0=D'_i$.

A distribution distance function (Definition 4) is a map $R:\mathcal D_n\times\mathcal D_n\to(-\infty,+\infty]$ that is nonnegative, vanishes exactly on the diagonal ($R(D',D)=0$ iff $D'=D$), and is convex in its first argument. $B$ is one.

A bootstrap sample of size $n$ is $n$ independent draws from $D_{\rm tr}$ (Eq. (14)); its law is the product $D_{\rm tr}^n$, and its empirical distribution is $D_{{\rm bs}[n]}$, the frequency of each point of $\iota$ among the $n$ draws.

A nominal formulation here is a loss $G:\iota\to\mathbb R_+$ with cost estimator $\mathbb E_D[G]=\sum_iD_iG_i$. Its robust counterpart (Eq. (24)) replaces the estimate by $\sup\{\mathbb E_{D'}[G]: D'\in\mathcal D_n,\ R(D',D_{\rm tr})\le r\}$, and its disappointment set is

$$\mathcal R=\Big\{D\in\mathcal D_n:\ \mathbb E_D[G]>\sup_{D'\in\mathcal D_n,\ R(D',D_{\rm tr})\le r}\mathbb E_{D'}[G]\Big\},$$

the bootstrap distributions on which the realized cost exceeds the robust budget.

Formalization targets

Goal: Proposition 1 (p. 16)

Let $R$ be a distribution distance function, $D\in\mathcal D_n$ with $B(D,D_{\rm tr})=r$, and $\mathcal N\subseteq\mathcal D_n$ a neighbourhood of $D$, open in $\mathcal D_n$, on which $R(\cdot,D_{\rm tr})>r$. Then there is a loss $G\ge0$ whose disappointment set satisfies

$$-r<\liminf_{n\to\infty}\frac1n\log D^\infty_{\rm tr}\big[D_{{\rm bs}[n]}\in\mathcal R\big],$$

stated in Lean in the equivalent form: for some $\varepsilon>0$, eventually $D^n_{\rm tr}[D_{{\rm bs}[n]}\in\mathcal R]\ge e^{-n(r-\varepsilon)}$.

Milestones (Appendix B.2, p. 27, and Eq. (31), p. 16)

1. Separation. The $R$-ball $\{R(\cdot,D_{\rm tr})\le r\}$ and a convex open $\mathcal N$ on which $R>r$ are separated by a linear functional: $\mathbb E_D[G]\le a<\mathbb E_{D'}[G]$.
2. Inclusion. For such $G$ and $a$, ${\rm int}\,\mathcal N=\mathcal N\subseteq\mathcal R$.
3. Sanov's lower bound (31). $-\inf_{D\in{\rm int}\,\mathcal C}B(D,D_{\rm tr})\le\liminf_n\frac1n\log D^\infty_{\rm tr}[D_{{\rm bs}[n]}\in\mathcal C]$ for every set $\mathcal C$.
4. Convexity step. $B(\lambda D+(1-\lambda)D_{\rm tr},D_{\rm tr})\le\lambda B(D,D_{\rm tr})+(1-\lambda)B(D_{\rm tr},D_{\rm tr})<r$ for $\lambda\in(0,1)$.
5. Infimum below $r$. $\inf_{D'\in\mathcal N}B(D',D_{\rm tr})<r$.

Significance

Proposition 1 turns Theorem 6 from a sufficient condition into a characterization. Theorem 6 says the bootstrap distance guarantees disappointment rate $r$; Proposition 1 says no distance function that is larger than $B$ on an open set does, for some nominal formulation. A practitioner who wants the bootstrap guarantee with the least conservative ambiguity set therefore has no better choice than $B$ in this sense. The result is one instance of a pattern in data-driven optimization, where large-deviation rate functions appear as the optimal ambiguity sets.

The paper's proof is a short combination of three standard facts: strict separation of convex sets, Sanov's theorem, and convexity of relative entropy. None of the three is available on the platform in the form needed. Sanov's theorem for empirical distributions on a finite alphabet has no machine-checked proof in Mathlib or on the platform; the lower bound (31) is a self-contained, reusable result of independent interest. The separation step needs strict separation inside the affine hull of the simplex, which Mathlib provides only in the ambient vector space. The result is proved on paper; none of it is formalized.

Difficulty

The separation and convexity steps are routine once the relative topology of the simplex is handled. The central difficulty is the lower bound (31), a large-deviation lower bound for the empirical distribution of i.i.d. draws. The bootstrap probability of an event is a sum of multinomial probabilities over the empirical distributions with denominator $n$ that fall in the event, and the bound must hold for every point of the relative interior, including points on the boundary of the simplex, where some coordinates vanish and the distance $B$ is not differentiable. An argument that only treats distributions of full support, or only open sets of $\mathbb R^\iota$, does not cover these points.

A second difficulty is bookkeeping between the three topologies in play: the ambient space $\mathbb R^\iota$, the simplex $\mathcal D_n$, and the affine hull in which separation takes place.

Formalization scope

• $\Omega_n$ is a finite type $\iota$ with decidable equality; distributions are stdSimplex ℝ ι. Covariates, responses, neighbourhood weights and the decision $z$ are abstracted away: the nominal formulation is the estimator $D\mapsto\sum_iD_iG_i$ (the estimator (18) with $k=n$ and unit weights), so the robust prescription $z^r_{\rm tr}(x_0)$ plays no role.
• $D_{\rm tr}$ has all coordinates positive (the support convention of the paper).
• $B$ and $R$ are EReal-valued; convexity of $R$ is written out in EReal. The supremum defining $\mathcal R$ is an EReal supremum. It is never empty, because $D_{\rm tr}$ lies in the $R$-ball, so $\mathcal R$ cannot collapse to all of $\mathcal D_n$.
• The bootstrap law is the $n$-fold product Measure.pi of $\sum_iD_{{\rm tr},i}\,\delta_i$, with $D_{\rm tr}$ fixed while $n\to\infty$.
• "Open" and "int" are relative to $\mathcal D_n$. With the ambient topology, no nonempty subset of the simplex is open and every interior is empty, which would make Proposition 1 and (31) vacuous; this formalization rules that out, as it rules out a junk real logarithm ($\log0=0$) by using the explicit-$\varepsilon$ form of every rate statement.
• Disclosed additions: the separation milestone assumes $\mathcal N$ is convex, nonempty and inside the relative interior of the simplex; the infimum milestone assumes $r>0$, which holds in Proposition 1.

A complete development needs the method of types on a finite alphabet, strict separation in an affine subspace, and the convexity of relative entropy. The method-of-types lower bound is reusable well beyond this mission (hypothesis testing, large deviations of empirical measures). Proofs of any milestone, and alternative proofs of (31), are welcome.

Selected references

• D. Bertsimas, B. Van Parys, Bootstrap robust prescriptive analytics, arXiv:1711.09974v2, 2021; Mathematical Programming, 2021. https://arxiv.org/abs/1711.09974
• A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 2009 (Theorem 6.2.10, Sanov's theorem). https://doi.org/10.1007/978-3-642-03311-7
• B. Van Parys, P. Mohajerin Esfahani, D. Kuhn, From data to decisions: distributionally robust optimization is optimal, Management Science 67(6), 2021. https://arxiv.org/abs/1704.04118
• I. Csiszár, The method of types, IEEE Transactions on Information Theory 44(6), 1998. https://doi.org/10.1109/18.720546
• B. Efron, The Jackknife, the Bootstrap and Other Resampling Plans, SIAM, 1982. https://doi.org/10.1137/1.9781611970319

Motivation

A decision maker who must choose $x$ before observing an uncertain outcome $\xi$ usually does not know the distribution of $\xi$; only past observations $\xi_1,\dots,\xi_T$ are available. Data-driven optimization replaces the unknown expected cost by an estimate computed from the data. The simplest estimate, the sample average, is optimistically biased: the cost realized out of sample is, with probability close to one half, higher than predicted. Many corrections have been proposed: robust optimization over moment, $\phi$-divergence or Wasserstein ambiguity sets (Delage & Ye 2010; Ben-Tal et al. 2013; Bertsimas, Gupta & Kallus 2018), and empirical-likelihood methods (Lam 2019; Duchi, Glynn & Namkoong 2021). Each is justified by a guarantee it satisfies. Van Parys, Mohajerin Esfahani and Kuhn (arXiv:1704.04118; Management Science 67(6), 2021) ask a different question: among all estimates that satisfy a given guarantee, which one is the least conservative? Their answer singles out one distributionally robust predictor, built on the relative entropy, as the best possible one in a precise sense. This mission formalizes that answer for the prediction problem with finitely many outcomes.

Setting

The outcome $\xi$ takes values in $\Xi=\{1,\dots,d\}$. Decisions range over a compact set $X\subseteq\mathbb R^n$, and the cost $\gamma(x,i)$ is continuous in $x$ for each $i$. These are the standing assumptions of §2 (p. 5).

A model is a point $\mathbb P$ of the probability simplex $\mathcal P=\{\mathbb P\in\mathbb R^d_+:\sum_i\mathbb P(i)=1\}$, with the topology inherited from $\mathbb R^d$. Under a model the expected cost is $c(x,\mathbb P)=\sum_i\mathbb P(i)\gamma(x,i)$.

The data are $T$ independent draws from an unknown model. They enter only through the empirical distribution $\hat{\mathbb P}_T(i)=\frac1T\#\{t\le T:\xi_t=i\}$. Write $\mathbb P^\infty(\cdot)$ for probabilities when the samples are drawn from $\mathbb P$.

A data-driven predictor is a continuous function $\hat c:X\times\mathcal P\to\mathbb R$; the number $\hat c(x,\hat{\mathbb P}_T)$ estimates $c(x,\mathbb P)$. The set of all of them is $\mathcal C$. Its out-of-sample disappointment is the probability $\mathbb P^\infty\big(c(x,\mathbb P)>\hat c(x,\hat{\mathbb P}_T)\big)$ that the true cost exceeds the prediction.

The relative entropy of $\mathbb P'$ with respect to $\mathbb P$ is

$$I(\mathbb P',\mathbb P)=\sum_{i}\mathbb P'(i)\log\frac{\mathbb P'(i)}{\mathbb P(i)}\in[0,\infty],$$

with $0\log(0/p)=0$ and $p'\log(p'/0)=+\infty$ for $p'>0$.

For a threshold $r\ge0$, the distributionally robust predictor is

$$\hat c_r(x,\mathbb P')=\sup_{\mathbb P\in\mathcal P}\{c(x,\mathbb P):I(\mathbb P',\mathbb P)\le r\}.\tag{10}$$

It is the worst expected cost over all models under which the observed frequencies $\mathbb P'$ are not exponentially unlikely at rate more than $r$. The observed frequencies are the first argument of $I$.

Formalization targets

Goal: Theorem 4 (strong optimality)

The paper's meta-optimization problem (5) is

$$\min_{\hat c\in\mathcal C}{}^{\preceq_{\mathcal C}}\ \hat c\quad\text{s.t.}\quad\limsup_{T\to\infty}\frac1T\log\mathbb P^\infty\big(c(x,\mathbb P)>\hat c(x,\hat{\mathbb P}_T)\big)\le-r\quad\forall x\in X,\ \mathbb P\in\mathcal P,$$

where $\hat c_1\preceq_{\mathcal C}\hat c_2$ means $\hat c_1\le\hat c_2$ pointwise on $X\times\mathcal P$. A feasible $\hat c^\star$ is strongly optimal if $\hat c^\star\preceq_{\mathcal C}\hat c$ for every feasible $\hat c$. The goal is:

$$\text{If } r>0,\ \text{then } \hat c_r \text{ is strongly optimal in (5).}$$

This statement contains feasibility (continuity and the decay rate) and pointwise domination of every feasible competitor.

Milestones

1. Proposition 1(ii) and (iii): $I$ is jointly convex and lower semicontinuous on $\mathcal P\times\mathcal P$.
2. The supremum in (10) is attained.
3. Theorem 2: the strong LDP $\mathbb P^\infty(\hat{\mathbb P}_T\in\mathcal D)\le(T+1)^de^{-T\inf_{\mathcal D}I(\cdot,\mathbb P)}$.
4. Theorem 1: the weak LDP, upper bound (7a) and, for $\mathbb P>0$, lower bound (7b) with the interior of $\mathcal D$.
5. Proposition 2: the dual representation $\hat c_r(x,\mathbb P')=\min_{\alpha\ge\bar\gamma(x)}\alpha-e^{-r}\prod_i(\alpha-\gamma(x,i))^{\mathbb P'(i)}$, with a minimizer in an explicit interval.
6. Proposition 3 and Theorem 3: $\hat c_r$ is continuous, and is feasible in (5) for every $r\ge0$.
7. Display (15): a maximizer in the closed relative entropy ball can be approximated in cost by a strictly positive model in the open ball.

Two further statements are included without milestones: Proposition 1(i), the information inequality, and Theorem 5, the finite-sample bound $(T+1)^de^{-rT}$ on the disappointment of $\hat c_r$.

Significance

The theorem turns a choice among robust estimators into a uniqueness statement. If a decision maker asks only for a disappointment probability that decays exponentially at rate $r$ under every possible model, then $\hat c_r$ is the unique least conservative continuous predictor. Any predictor that is smaller anywhere fails the guarantee for some model. The reverse predictor (12) and the restricted predictor (13), which fix the other argument of $I$ or hedge only against models absolutely continuous with respect to the observed frequencies and are common in the literature, differ from $\hat c_r$ (Remark 3, pp. 15–16), so the theorem does not single them out. The companion missions of this series extend the result to predictor–prescriptor pairs (mission 2) and to compact continuous outcome spaces (mission 3).

The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. A formal development would also give Mathlib-level statements of the method of types: Sanov's theorem for finite alphabets in both its finite-sample and asymptotic forms, together with the convexity and semicontinuity of the relative entropy with the $+\infty$ convention. These are reusable far beyond this paper.

Difficulty

Feasibility (Theorem 3) is a direct consequence of the LDP upper bound, once the disappointment set is seen to lie outside the relative entropy ball. The difficulty is the optimality half. Showing that a competitor $\hat c$ with $\hat c(x,\mathbb P_0')<\hat c_r(x,\mathbb P_0')$ at a single point must be infeasible requires a lower bound on a disappointment probability. The obvious approach evaluates the LDP lower bound at a maximizer $\mathbb P_0$ of (10). That fails: the lower bound (7b) needs a strictly positive model, the maximizer usually lies on the boundary of the simplex and on the boundary of the ball $I(\mathbb P_0',\cdot)\le r$, and the bound is only in terms of the interior of the disappointment set. The argument has to move to a nearby model, and this uses the continuity of $\hat c$, the convexity of $I$, and the $+\infty$ convention of $I$ in its second argument. The asymptotic statements also require care with the logarithm of a vanishing probability.

Formalization scope

• Outcomes and models. $\Xi$ is Fin d. $\mathcal P$ is the subtype of stdSimplex ℝ (Fin d), so interiors and continuity are relative to $\mathcal P$, as footnote 1 (p. 12) requires.
• Decisions and cost. $X$ is a compact subset of EuclideanSpace ℝ (Fin n), and $\gamma : X\to\mathbb R^d$ is continuous in $x$ for each outcome.
• Relative entropy. $I$ is EReal-valued and is $+\infty$ whenever $\mathbb P(i)=0<\mathbb P'(i)$. A real-valued sum would give a finite value there under Lean's log 0 = 0, and so change $\hat c_r$.
• Probabilities. Sampling probabilities are finite sums over sample paths $\Xi^T$. The empirical distribution is defined for $T\ge1$; finite-sample statements assume $T\ge1$.
• Decay rates. Rates are stated without logarithms: $\limsup\frac1T\log p_T\le-r$ is written "for every $r'<r$, eventually $p_T\le e^{-r'T}$". The form through Real.log would give a never-disappointed predictor rate $0$, which makes Theorem 3 false.
• Infima. Infima of $I$ are taken in the extended reals.
• Competitors. They range over all jointly continuous functions on $X\times\mathcal P$. Dropping continuity makes Theorem 4 false.
• Sets $\mathcal D$. The LDP statements require Borel $\mathcal D\subseteq\mathcal P$, represented by MeasurableSet D in the simplex subtype.
• Display (15). The clause $0<r_2$ is dropped: it is unused, and it fails for $d=1$.

Welcome contributions: the method of types on Fin d (type classes, their cardinality bounds and probabilities); joint convexity and lower semicontinuity of the finite relative entropy with the $+\infty$ convention; and Berge's maximum theorem in the form used for Proposition 3. These are reusable beyond this mission. The definitions duplicate those of mission 2 of this series and are meant to be merged once published.

The source is the arXiv preprint arXiv:1704.04118v3 (22 Dec 2019); all theorem, display and page numbers refer to it.

Selected references

• B. P. G. Van Parys, P. Mohajerin Esfahani, D. Kuhn, From Data to Decisions: Distributionally Robust Optimization is Optimal, Management Science 67(6), 2021. Preprint arXiv:1704.04118v3. https://arxiv.org/abs/1704.04118v3 — https://doi.org/10.1287/mnsc.2020.3678
• T. M. Cover, J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006 (Theorems 2.6.3, 2.7.2, 11.4.1). https://doi.org/10.1002/047174882X
• A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998. https://doi.org/10.1007/978-1-4612-5320-4
• 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
• 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
• C. Berge, Topological Spaces, Oliver & Boyd, 1963 (pp. 115–116, maximum theorem).

Motivation

In statistical learning a hypothesis $f$ is chosen from a class $\mathcal F$ using $n$ samples drawn from an unknown distribution $P$, and its quality is measured by the risk $R(P,f) = \mathbf E_P[f(Z)]$. When the distribution at deployment time may differ from the one that generated the data (domain drift, adversarial perturbation, model misspecification), a natural replacement is the worst-case risk over a neighbourhood of $P$. Distributionally robust optimization with Wasserstein neighbourhoods takes these neighbourhoods to be balls in an optimal-transport distance, which compare distributions through the geometry of the instance space instead of through likelihood ratios. Wasserstein balls also contain distributions with support different from that of $P$, which divergence balls do not.

J. Lee and M. Raginsky, Minimax statistical learning with Wasserstein distances (NeurIPS 2018, arXiv:1705.07815), give generalization guarantees for the empirical version of this procedure, the local minimax ERM. Their analysis rests on the strong duality theorem of Gao and Kleywegt (arXiv:1604.02199), which turns the supremum over a Wasserstein ball into a minimization over one real multiplier $\lambda \ge 0$. This mission formalizes their Theorem 2, the excess-risk bound for a class of uniformly Lipschitz hypotheses, together with the steps of its proof. The source is the arXiv v2 preprint, which contains the NeurIPS camera-ready text and the supplementary appendices.

Setting

The instance space $\mathcal Z$ is a Polish space (complete separable metric space) with metric $d_{\mathcal Z}$, and it is bounded: $\operatorname{diam}(\mathcal Z) = \sup_{z,z'} d_{\mathcal Z}(z,z') < \infty$ (Assumption 1). Fix $p \ge 1$. The $p$-Wasserstein distance between Borel probability measures is

$$W_p(P,Q) = \Big(\inf_{M} \mathbf E_M\big[d^p_{\mathcal Z}(Z,Z')\big]\Big)^{1/p},$$

the infimum over couplings $M$ of $P$ and $Q$. For a radius $\varrho > 0$ the ball is $B^W_{\varrho,p}(P) = \{Q : W_p(P,Q) \le \varrho\}$.

The hypothesis class $\mathcal F$ consists of upper semicontinuous functions $f : \mathcal Z \to \mathbb R$ with $0 \le f \le M$ (Assumption 2). The local worst-case risk and the local minimax risk are

$$R_{\varrho,p}(P,f) = \sup_{Q \in B^W_{\varrho,p}(P)} R(Q,f), \qquad R^*_{\varrho,p}(P,\mathcal F) = \inf_{f \in \mathcal F} R_{\varrho,p}(P,f).$$

Given i.i.d. samples $Z_1,\dots,Z_n$ from $P$ with empirical distribution $P_n = \frac1n\sum_i \delta_{Z_i}$, the local minimax ERM is $\hat f \in \arg\min_{f \in \mathcal F} R_{\varrho,p}(P_n,f)$.

Assumption 3 asks that every $f \in \mathcal F$ be $L$-Lipschitz with one constant $L$: $f(z') - f(z) \le L\,d_{\mathcal Z}(z',z)$. The complexity of $\mathcal F$ is measured by the entropy integral

$$\mathfrak C(\mathcal F) = \int_0^\infty \sqrt{\log \mathcal N(\mathcal F,\|\cdot\|_\infty,u)}\,du,$$

where $\mathcal N(\mathcal F,\|\cdot\|_\infty,u)$ is the covering number of $\mathcal F$ in the uniform metric. The dual integrand of Gao–Kleywegt duality is $\varphi_{\lambda,f}(z) = \sup_{z'}\{f(z') - \lambda d^p_{\mathcal Z}(z,z')\}$.

Formalization targets

Goal: Theorem 2 (10)

Under Assumptions 1–3, for every $\delta \in (0,1)$, with probability at least $1-\delta$,

$$R_{\varrho,p}(P,\hat f) - R^*_{\varrho,p}(P,\mathcal F) \le \frac{48\,\mathfrak C(\mathcal F)}{\sqrt n} + \frac{48 L\cdot\operatorname{diam}(\mathcal Z)^p}{\sqrt n\cdot\varrho^{p-1}} + 3M\sqrt{\frac{\log(2/\delta)}{2n}}.$$

Milestones, in the order the proof uses them

1. Proposition 4 (8): $R_{\varrho,p}(Q,f) = \min_{\lambda\ge0}\{\lambda\varrho^p + \mathbf E_Q[\varphi_{\lambda,f}(Z)]\}$.
2. Lemma 1: the optimal dual multiplier satisfies $\tilde\lambda \le L\varrho^{-(p-1)}$.
3. (C.2): $R_{\varrho,p}(P_n,f^*) - R_{\varrho,p}(P,f^*) \le \int \varphi_{\lambda^*,f^*}\,d(P_n - P)$ for an achiever $f^*$.
4. (C.3) with $\Lambda = [0, L\varrho^{-(p-1)}]$ and $\Phi = \{\varphi_{\lambda,f} : \lambda \in \Lambda, f \in \mathcal F\}$: $R_{\varrho,p}(P,\hat f) - R_{\varrho,p}(P_n,\hat f) \le \sup_{\varphi\in\Phi}\int\varphi\,d(P - P_n)$.
5. (C.4): with probability at least $1-\delta/2$, $R_{\varrho,p}(P,\hat f) - R_{\varrho,p}(P_n,\hat f) \le 2\mathfrak R_n(\Phi) + M\sqrt{2\log(2/\delta)/n}$.
6. (C.5): with probability at least $1-\delta/2$, $R_{\varrho,p}(P_n,f^*) - R_{\varrho,p}(P,f^*) \le M\sqrt{\log(2/\delta)/(2n)}$.
7. The Rademacher bound of Appendix C.3: $\mathfrak R_n(\Phi) \le \frac{24}{\sqrt n}\mathfrak C(\mathcal F) + \frac{24L\operatorname{diam}(\mathcal Z)^p}{\sqrt n\,\varrho^{p-1}}$.

Significance

Theorem 2 says that robust ERM over a uniformly Lipschitz class is nearly optimal for the robust risk at the unknown distribution, with excess of order $1/\sqrt n$ and explicit constants. The dependence on $\varrho$ enters only through $\varrho^{-(p-1)}$; at $p = 1$ the bound does not depend on $\varrho$ and recovers the usual rate of ordinary ERM. The paper derives Corollaries 1 and 2 (regression with a Lipschitz link, and Gaussian-kernel classes) and the domain-adaptation bound of Theorem 4 from it. Lemma 1, which confines the dual multiplier to a fixed interval, is also used outside the theorem: Remark 3 proposes it as the search range for the fixed-$\lambda$ adversarial training of Sinha et al.

The result is proved in the paper; to our knowledge none of it has been machine-checked. What this mission adds is a verified version of a complete distributionally robust generalization argument: Gao–Kleywegt strong duality on a bounded Polish space, the multiplier bound, symmetrization and bounded differences for a class indexed by a function and a real parameter, and a Dudley entropy bound for that joint class. The paper's appendix states the Rademacher bound with a stray constant $C_0$ that belongs to a different assumption (Assumption 4); the milestone states the bound without it, which is what the proof gives and what the constant $48L$ of (10) needs.

Difficulty

The obvious route bounds $\sup_{f}|R_{\varrho,p}(P,f) - R_{\varrho,p}(P_n,f)|$ uniformly over $\mathcal F$. That needs uniform control of the dual multiplier for every $f$ and every empirical distribution, and without it the class $\{\varphi_{\lambda,f}\}$ is indexed by an unbounded $\lambda$, so its complexity is infinite. Lemma 1 resolves this only for the minimizers, which is why the argument is organized around $\hat f$ and an achiever $f^*$ rather than a uniform bound.

The formal difficulties are separate. Strong duality with attainment of the minimum is a measure-theoretic theorem about couplings on a Polish space (existence of optimal couplings, measurable selection of near-maximizers), none of which is in Mathlib for Wasserstein balls. The supremum over $\Phi$ must be shown measurable before its expectation means anything. Dudley's chaining bound over a separable, infinite index set is also missing from Mathlib in the form needed here. Finally, the theorem does not assume that $R^*_{\varrho,p}(P,\mathcal F)$ is attained, while the paper's proof uses an achiever $f^*$, so a complete proof needs an approximation argument that the paper does not write out.

Formalization scope

• $\mathcal Z$ is a MetricSpace with BorelSpace and PolishSpace instances, and Assumption 1 is Bornology.IsBounded (Set.univ : Set 𝒵). $\operatorname{diam}(\mathcal Z)$ is Metric.diam univ.
• $W_p$ and the ball are the published definitions WassersteinLinOpt.Ball.wassersteinDist and wassersteinBall. Membership in $\mathcal P_p(\mathcal Z)$ is automatic on a bounded space.
• The standing assumptions $p \ge 1$ and $\varrho > 0$ are binders of every item.
• Risks, the dual integrand $\varphi_{\lambda,f}$ and the Rademacher average are real suprema, infima and Bochner integrals. Under the binders each is over a nonempty set that is bounded on the relevant side, and each integrand is bounded and measurable.
• The covering number is the internal one (centres in $\mathcal F$), valued in $\mathbb N\cup\{\infty\}$, and $\mathfrak C(\mathcal F)$ is valued in $[0,\infty]$. Every item whose bound contains $\mathfrak C(\mathcal F)$ assumes $\mathfrak C(\mathcal F) < \infty$ and uses its real value. This is a disclosed pin: otherwise the bound is $+\infty$.
• Assumption 3 is ∀ f ∈ ℱ, ∀ z z', f z' - f z ≤ L * dist z' z, with one $L$ quantified before $\mathcal F$, and $0 \le L$ is a disclosed pin.
• The sample is ω : Fin n → 𝒵 with law Measure.pi (fun _ => P), and $n \ge 1$. "With probability at least $1-\delta$" means the outer measure of the failure set is at most $\delta$, for $0 < \delta < 1$.
• The ERM is a sample-indexed selection $\hat f$ with membership and minimality hypotheses, never Classical.choose. Such a selection exists exactly when empirical minimizers exist, which display (7) presupposes.
• "min" over $\lambda$ in Proposition 4 includes attainment, and the argmins of Lemma 1 and (C.2) are minimality hypotheses.

Trivializing formalizations are ruled out:

• Assumption 3 is not written with $L$ chosen after $f$, and $L \ge 0$ is not omitted.
• The stray $C_0$ is not in the Lean.
• The goal is about $R^*_{\varrho,p}(P,\mathcal F)$, not about a fixed competitor $f$.
• No probability is converted with toReal, and an infinite $\mathfrak C(\mathcal F)$ is never converted to $0$.

A complete development needs:

• Gao–Kleywegt duality for bounded upper semicontinuous losses;
• McDiarmid's and Hoeffding's inequalities on product measures;
• symmetrization;
• Dudley's entropy integral bound for sub-Gaussian processes indexed by a separable pseudometric space.

The last three are reusable well beyond this mission. Contributions of any of these as stand-alone results are welcome, as are proofs of the milestones.

Selected references

• J. Lee and M. Raginsky, Minimax statistical learning with Wasserstein distances, Advances in Neural Information Processing Systems 31 (NeurIPS 2018); arXiv:1705.07815v2. https://arxiv.org/abs/1705.07815
• R. Gao and A. J. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, Mathematics of Operations Research 48(2), 2023; arXiv:1604.02199. https://arxiv.org/abs/1604.02199
• A. Sinha, H. Namkoong and J. Duchi, Certifying some distributional robustness with principled adversarial training, ICLR 2018; arXiv:1710.10571. https://arxiv.org/abs/1710.10571
• M. Talagrand, Upper and Lower Bounds for Stochastic Processes, Springer, 2014. https://doi.org/10.1007/978-3-642-54075-2

Motivation

A two-stage stochastic program chooses a decision before uncertainty is observed and a recourse decision afterward. Its objective can involve the expected optimal value of the recourse problem. Even with linear constraints, evaluating that expectation can be difficult when the random input has many coordinates. Dyer and Stougie's 2006 complexity paper studied this question for stochastic programming. Hanasusanto, Kuhn and Wiesemann identified a false volume identity in one fixed-recourse argument, then supplied a quantitative replacement in their 2015 preprint. The replacement shows that sufficiently accurate expected-recourse values determine an exact counting answer.

The distinction matters to researchers designing numerical methods for stochastic programs. A hardness statement at a specified absolute accuracy identifies the scale at which a general exact-information guarantee would have strong complexity consequences. It does not say that useful approximations at coarser accuracy are unavailable. The present mission records the mathematical reduction behind the paper's Theorem 1 and its quantitative tolerance.

Setting

Let $k\ge1$. A realization $\xi=(\xi_1,\ldots,\xi_k)$ lies in the unit cube $C=[0,1]^k$, equipped with Lebesgue measure. This cube has volume one, so integration over it is expectation under the uniform law. Let $\alpha\in\mathbb R^k_+$ be nonnegative weights and $\beta\ge0$ a budget. The second-stage value $Q(\xi;\alpha,\beta)$ is the maximum of

$$\sum_{j=1}^k\xi_jy_j-\beta z$$

over $0\le z\le1$ and $0\le y_j\le\alpha_jz$ for each $j$. Its expected recourse value is $\mathcal Q(\alpha,\beta)=\int_C Q(\xi;\alpha,\beta)\,d\xi$. There is no first-stage decision in this instance of the model.

The knapsack polytope is $P(\alpha,\beta)=\{\xi\in C:\sum_j\alpha_j\xi_j\le\beta\}$, and $V(\alpha,\beta)$ denotes its volume. For integer weights and budget, its binary points correspond to subsets $S\subseteq\{1,\ldots,k\}$ with $\sum_{j\in S}\alpha_j\le\beta$. The #Parity count $D$ is the number of such subsets of even size minus the number of odd size. The paper invokes the counting complexity of this problem from Dyer and Frieze's 1988 volume paper.

For $i=0,\ldots,k$, define $\gamma_i=\beta+i/(k+1)$ and a square matrix $F$ by $F_{ic}=\gamma_i^{k-c}$ for $c=0,\ldots,k$. The first column has power $k$ and the last has power zero. This order matters: the first coordinate of the coefficient vector is the parity count. The matrix inverse is controlled by a column-sum bound of the kind studied by Gautschi in 1962.

Formalization targets

Goal: recourse values determine the count

Write $\varepsilon_3(\alpha)=1/[2k!(\|\alpha\|_1+2)^k(k+1)^{k+1}\prod_j\alpha_j]$ and $\delta_7(\alpha)=[\alpha_k\varepsilon_3(\alpha)/(1+\alpha_k)]^2$, exactly the right sides of (3) and (7). For positive integer weights, $\beta\le\sum_j\alpha_j$, and $0<\delta<\delta_7(\alpha)$, take any oracle $Q_\delta(t)$ with $|Q_\delta(t)-\mathcal Q(\alpha,t)|\le\delta$ at every nonnegative $t$. Set $h=2\sqrt\delta$ and

$$\widetilde g_i=\frac{Q_\delta(\gamma_i+h)-Q_\delta(\gamma_i)}{h}+1.$$

The target is that every solution of

$$F\widetilde x=\left(k!\prod_{j=1}^k\alpha_j\right)\widetilde g$$

satisfies $|\widetilde x_0-D|<1/2$. Nearest-integer rounding therefore recovers $D$.

Supporting targets

The milestones establish the value formula for the second-stage program, the inclusion–exclusion volume formula (8), the integer coefficient identity for the exact volume system, the inverse bound (4), the perturbation bound (6), the derivative identity in Lemma 2, a global volume-growth bound, and the finite-difference estimate in Theorem 1. Together they retain the paper's constants and its sequence from expected values to volume approximations to an exact count. Proposition 1 separately records why the earlier proposed identity $1-\mathcal Q=V$ fails.

Significance

The result certifies a concrete information transfer. A function returning expected-recourse values to the stated absolute tolerance also contains enough information to distinguish the exact even-minus-odd count of feasible binary points. The bound states how accurate those values must be as dimension and weights change; a qualitative assertion of hardness alone would hide that dependence. The paper concludes #P-hardness after accounting for the polynomial-time operations of the reduction. That complexity-class conclusion is part of the paper, while the Lean goal isolates the reduction's numerical correctness.

A complete formalization would give separately reusable results about cube integrals, knapsack volumes, perturbations of Vandermonde systems, and finite differences of expected hinge functions. The source paper proves the mathematical assertions; this proposal stages their Lean statements as open proof obligations. No machine-checked proof is claimed here. The companion counterexample also keeps the corrected argument anchored to the precise error it repairs.

Difficulty

The tempting identity $1-\mathcal Q(\alpha,\beta)=V(\alpha,\beta)$ fails: the expectation of the second-stage optimum is a positive-part expectation, while volume is a distribution function. The paper's Proposition 1 makes the discrepancy explicit for all-ones weights. Recovering volume requires differentiation with respect to the budget, and an approximate function value does not directly provide an accurate derivative. The difficulty is controlling both oracle error and the change of volume over a finite budget interval tightly enough that the final coefficient error is strictly below one half.

There are further exactness points. The column order of $F$ fixes which coefficient equals $D$. The $1$-norm in (4) is the maximum column sum of the inverse, not a generic matrix norm. The perturbation threshold contains $k!$, every weight, and the power $(k+1)^{k+1}$; losing one factor can invalidate the rounding guarantee.

Formalization scope

Lean uses vectors $\mathrm{Fin}(k)\to\mathbb R$, with zero-based indices; the paper's $\alpha_k$ is the final coordinate. Lebesgue measure is restricted to $C$, whose volume is one. The LP value is a real supremum of its feasible objective values. For the nonnegative weights used in the theorems, the feasible set is nonempty and bounded, so this represents the actual maximum. The expected value is a real integral over the cube. The matrix $F$ has descending powers, and its $1$-norm estimate is written as a bound on each inverse column sum. Binary vectors are represented by subsets; $D$ keeps the paper's even-minus-odd convention.

Positive weights are required where (3) and (7) divide by their product, and $\delta>0$ where $h$ divides a finite difference. The case $\beta>\sum_j\alpha_j$ is excluded from the main target because the paper first answers it directly with $D=0$. Lemma 2 excludes $\alpha=0,\beta=0$, where the claimed derivative fails to exist. The volume-growth milestone gives the content of the paper's $\mathcal Q''\le1/\alpha_k$ argument without requiring a second derivative at a kink; it applies across the actual interval starting at $\beta$. The printed determinant sign is also adjusted to the descending columns by asserting nonsingularity, which is what the proof uses. The second-stage value milestone retains only the optimal value, because the optimal decisions the page calls unique need not be unique at ties. The mission must use the LP and counting definitions above; replacing them with an arbitrary function assumed to have the desired derivative would empty the reduction.

The formal work requires measure and integration theory, finite polytope volume, finite sums over subsets, matrix inverses, and real inequalities. Contributions proving the eight milestones and any honest supporting lemmas are welcome. The setup does not encode polynomial-time computability, bit lengths, or a #P complexity class, so closure of the Lean goal alone is not a formal proof of the full complexity statement.

Selected references

• G. A. Hanasusanto, D. Kuhn and W. Wiesemann, A comment on “computational complexity of stochastic programming problems”, Optimization Online preprint 2015/03/4825, version of October 6, 2015; published in Mathematical Programming, 2016. Preprint.
• M. Dyer and L. Stougie, Computational complexity of stochastic programming problems, Mathematical Programming 106 (2006), 423–432. DOI.
• M. E. Dyer and A. M. Frieze, On the complexity of computing the volume of a polyhedron, SIAM Journal on Computing 17 (1988), 967–974. DOI.
• W. Gautschi, On inverses of Vandermonde and confluent Vandermonde matrices, Numerische Mathematik 4 (1962), 117–123. Scan.

Motivation

Prescriptive analytics chooses a decision $z$ from data after observing a context $x_0$: a retailer sets an order quantity after seeing the weather forecast, a hospital schedules staff after seeing the day of the week. A common recipe estimates the expected cost of each decision from the training observations closest to $x_0$ (nearest neighbours, or a kernel-weighted Nadaraya–Watson average) and then minimizes that estimate (Bertsimas and Kallus, 2020). The decision that minimizes an estimate tends to look better on the training data than it is: its estimated cost is optimistically biased. Bertsimas and Van Parys (arXiv:1711.09974v2) measure that optimism on resampled data. Bootstrap data are $n$ independent draws from the training distribution, in the sense of Efron (1979). A cost budget computed on the training data disappoints when the estimate on a bootstrap sample exceeds it. The paper replaces the nominal estimate by a robust budget, a worst case over all distributions within relative-entropy distance $r$ of the training distribution. Its Theorem 6 bounds the probability of disappointment by an explicit sum of exponentials in $n$.

This mission formalizes that theorem, together with the structural results its proof rests on and the Nadaraya–Watson special case, Corollary 2. The same paper's dual reformulation of the budget (Lemma 2) and its optimality statement for the relative entropy (Proposition 1) are the subject of two sibling missions.

Setting

The $n$ training points have a finite set $\Omega_n$ of distinct values. A distribution on $\Omega_n$ is a vector $D=(D_i)_{i\in\Omega_n}$ in the standard simplex; these form $\mathcal D_n$. The training distribution $D_{\mathrm{tr}}\in\mathcal D_n$ gives every point of $\Omega_n$ positive mass. The bootstrap distributions are

$$\mathcal D_{n,n}=\{D\in\mathcal D_n:\ nD_i\in\{0,1,\dots,n\}\ \forall i\}.$$

These are the possible empirical distributions $D_{\mathrm{bs}[n]}$ of $n$ independent draws from $D_{\mathrm{tr}}$.

Around the context $x_0$ the points of $\Omega_n$ are grouped into nested neighbourhoods $\emptyset=N^0\subseteq N^1\subseteq\dots\subseteq N^n=\Omega_n$. Each point $i$ carries a positive weight $w_i$ and, for a decision $z$, a loss $\ell_i=L(z,\bar y_i)$. Fix $k\in\{1,\dots,n\}$. The estimator (18) of a distribution $D$ averages the loss with weights $w_iD_i$ over the smallest neighbourhood $N^{j}$ with $D$-mass at least $k/n$. For $j\in[n]$, the partial estimator $E^{n,j}_D$ is the value of the linear program (22). Its domain is contained in

$$\mathcal D^j_n=\Big\{D\in\mathcal D_n:\ \sum_{i\in N^{j-1}}D_i\le\tfrac{k-1}{n},\ \ \tfrac kn\le\sum_{i\in N^j}D_i\Big\},$$

and off that domain $E^{n,j}_D=-\infty$.

The bootstrap distance is the relative entropy

$$B(D,D')=\sum_{i}D_i\log\frac{D_i}{D'_i}.$$

The partial robust budgets are $c^j_n=\sup\{E^{n,j}_D:\ D\in\mathcal D_n,\ B(D,D_{\mathrm{tr}})\le r\}$, the robust budget is $\bar c_n=\max_{j\in[n]}c^j_n$ (26), and the minimum radii are $r^j_n=\inf\{B(D,D_{\mathrm{tr}}):D\in\mathcal D^j_n\}$ (29).

Formalization targets

Goal: Theorem 6 (p. 15)

For every decision $z$,

$$\mathbb P\Big[E^n_{D_{\mathrm{bs}[n]}}[L(z,y)\,|\,x=x_0]>\bar c_n(z)\Big]\ \le\ \sum_{j\in[n]}\exp\big(-n\cdot\max\{r,r^j_n\}\big).$$

The bound holds for every $n$, $k$, neighbourhood chain, weight vector and radius, with no asymptotics.

Milestones

1. The domain inclusion (23), with $E^{n,j}_D=-\infty$ off $\mathcal D^j_n$ (p. 11).
2. The closed form of $E^{n,j}_D$ on $\mathcal D^j_n$ as a weighted average over $N^j$ (B.1, p. 26).
3. The sets $\mathcal D^j_n\cap\mathcal D_{n,n}$, $j\in[n]$, partition $\mathcal D_{n,n}$ (B.1, p. 26).
4. Theorem 1: $E^n_D=\max_{j\in[n]}E^{n,j}_D$ on $\mathcal D_{n,n}$ (p. 11).
5. Theorem 5, Csiszár's inequality: for every convex $\mathcal C\subseteq\mathcal D_n$ and $n\ge1$,

$$\mathbb P[D_{\mathrm{bs}[n]}\in\mathcal C]\le\exp\Big(-n\inf_{D\in\mathcal C}B(D,D_{\mathrm{tr}})\Big)\quad\text{(p. 14)}.$$

6. Each $\mathcal C_j=\{D\in\mathcal D^j_n:E^{n,j}_D>\bar c\}$ is convex (p. 15).
7. On $\mathcal D_{n,n}$, $E^n_D>\bar c$ if and only if $D\in\bigcup_{j}\mathcal C_j$ (p. 15).
8. $\inf_{D\in\mathcal C_j}B(D,D_{\mathrm{tr}})\ge\max\{r,r^j_n\}$ when $\bar c=\bar c_n$ (p. 15).
9. For Nadaraya–Watson, the disappointment set is convex and lies at bootstrap distance at least $r$ (B.6, p. 30).
10. Corollary 2: with $k=n$ the disappointment is at most $\exp(-n\cdot r)$ (p. 16).

Significance

Theorem 6 makes the radius $r$ an explicit statistical dial. The sum $\sum_j\exp(-n\max\{r,r^j_n\})$ can be computed from the training data, because each $r^j_n$ is a convex program. So a practitioner can choose $r$ for a target disappointment $b$, and the bound decays exponentially in $n$ at rate at least $r$. Corollary 2 gives a single exponential bound for Nadaraya–Watson: $r\ge\log(1/b)/n$ gives disappointment at most $b$. Together with the paper's Proposition 1, which shows that no smaller distance keeps the rate $-r$, the result explains why the relative entropy is the natural ambiguity measure for bootstrap guarantees.

On the formal side, the results are proved in the paper. Theorem 5 is cited there from Csiszár (1984), not reproved. The local platform search found no matching machine-checked statement of Theorem 6, Theorem 1 or Csiszár's convex-set inequality. A formal proof of Theorem 5 on a finite alphabet would be a reusable large-deviation tool: a finite-sample Sanov upper bound without polynomial prefactor, for empirical distributions of i.i.d. samples in any convex set. Theorem 1 and the partition lemma are the combinatorial facts behind the nearest-neighbours robust formulation of this paper.

Difficulty

Two steps carry the weight. The first is Theorem 5. The method of types alone gives $\mathbb P[D_{\mathrm{bs}[n]}\in\mathcal C]\le(n+1)^{|\Omega_n|}\exp(-n\inf_{\mathcal C}B)$, and its polynomial factor is fatal here: the goal has none. Removing it needs convexity of $\mathcal C$ in an essential way; the bound is false for general sets. The set $\mathcal C$ need not be closed and its infimum need not be attained. The second is Theorem 1. The estimator selects its neighbourhood depending on $D$, so it is neither linear nor concave in $D$. The disappointment event is therefore not convex, and Theorem 5 cannot be applied to it directly. Splitting it over the sets $\mathcal D^j_n$ needs the partition of $\mathcal D_{n,n}$. That partition fails off the grid $\mathcal D_{n,n}$: a mass strictly below $k/n$ is at most $(k-1)/n$ only for multiples of $1/n$.

Formalization scope

The support $\Omega_n$ is a finite type $\iota$, and a distribution is a vector ι → ℝ in stdSimplex ℝ ι. Covariates, responses, the context and the distance function of Definition 2 do not appear. The neighbourhoods are a chain N : ℕ → Finset ι with Monotone N, N 0 = ∅ and N n = univ, which abstracts Definition 2 and its tie-breaking. Weights are positive, losses are real-valued (Assumption 1 allows $+\infty$; no planned statement needs it), and nonnegativity and convexity of the loss are not assumed. The relative entropy is EReal-valued, with $0\log0=0$ and $B(D,D')=+\infty$ when $D'_i=0<D_i$. Every supremum and infimum that may be empty or unbounded is in EReal: an infeasible program (22) is $-\infty$, an empty $\mathcal D^j_n$ has $r^j_n=+\infty$, and $\exp(-n\cdot(+\infty))=0$. The bootstrap law is the product measure Measure.pi of $n$ copies of $\sum_iD_{\mathrm{tr},i}\delta_i$. The robust budget is the formulation (26), $\max_jc^j_n$, which the paper computes and which never exceeds (24). The theorem is stated for every decision $z$, not only for the robust prescriptor. The printed strict inequalities for the infima over $\mathcal C_j$ are stated as $\ge$.

Trivializing encodings are ruled out explicitly. Real sSup/sInf would turn infeasible programs and empty sets into a finite $0$. A real logarithm with a vanishing reference would give $B$ a finite junk value. A single draw or a non-product law would make Theorem 5 false. A chain without $N^0=\emptyset$ and $N^n=\Omega_n$ would break the partition. expNeg treats $+\infty$ explicitly so that an empty $\mathcal D^j_n$ contributes $0$, not $1$.

A complete development needs the method of types on a finite alphabet, I-projections onto convex sets of the simplex, and the Pythagorean inequality. The latter two are reusable well beyond this mission. Contributions to any milestone, or to a standalone finite-alphabet Csiszár inequality, are welcome.

Selected references

• D. Bertsimas and B. Van Parys, Bootstrap robust prescriptive analytics, arXiv:1711.09974v2, 2021. https://arxiv.org/abs/1711.09974
• I. Csiszár, Sanov property, generalized I-projection and a conditional limit theorem, Annals of Probability 12(3), 1984. https://doi.org/10.1214/aop/1176993227
• A. Dembo and O. Zeitouni, Large Deviations Techniques and Applications, Springer, 2nd ed., 2010. https://doi.org/10.1007/978-3-642-03311-7
• B. Efron, Bootstrap methods: another look at the jackknife, Annals of Statistics 7(1), 1979. https://doi.org/10.1214/aos/1176344552
• D. Bertsimas and N. Kallus, From predictive to prescriptive analytics, Management Science 66(3), 2020. https://doi.org/10.1287/mnsc.2018.3253