Statistics

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

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 decision maker who chooses $x$ to minimize an expected cost $c(x,\mathbb P)=\mathbb E_{\mathbb P}[\gamma(x,\xi)]$ rarely knows the distribution $\mathbb P$ of the random parameter $\xi$. What is available is a sample $\xi_1,\dots,\xi_T$. Any rule that turns the sample into a cost estimate can disappoint: the realized expected cost may exceed the estimate. In a cost-minimization context such underestimates are more harmful than overestimates, which is why distributionally robust optimization replaces the unknown $\mathbb P$ by a worst case over a set of distributions consistent with the data.

Van Parys, Mohajerin Esfahani and Kuhn (arXiv:1704.04118, Management Science 2021) asked which such rule is best. They define a data-driven predictor to be least conservative among all predictors whose probability of disappointment decays exponentially at a prescribed rate $r$, and they prove that a single predictor, the worst-case expected cost over a relative-entropy ball around the empirical distribution, is the unique strong solution. Their main results are for a finite set of outcomes $\Xi=\{1,\dots,d\}$. Section 5 extends the predictor result to an arbitrary compact $\Xi\subseteq\mathbb R^d$; this mission formalizes that extension. The version used throughout is the arXiv preprint arXiv:1704.04118v3 (22 December 2019), and every index below is the preprint's.

Setting

Fix compact sets $X\subseteq\mathbb R^n$ (decisions) and $\Xi\subseteq\mathbb R^d$ (outcomes), and a cost $\gamma:X\times\Xi\to\mathbb R$ that is jointly continuous.

• The model class $\mathcal P$ is the set of Borel probability distributions on $\Xi$, with the topology of weak convergence. $X\times\mathcal P$ carries the product topology.
• The model-based predictor is $c(x,\mathbb P)=\int_\Xi\gamma(x,\xi)\,\mathrm d\mathbb P(\xi)$.
• The relative entropy of $\mathbb P'$ with respect to $\mathbb P$ (Definition 8) is $I(\mathbb P',\mathbb P)=\int_\Xi\log\frac{\mathrm d\mathbb P'}{\mathrm d\mathbb P}\,\mathrm d\mathbb P'$ if $\mathbb P'\ll\mathbb P$, and $+\infty$ otherwise.
• Given independent samples $\xi_1,\dots,\xi_T$ from $\mathbb P$, the empirical distribution is $\hat{\mathbb P}_T=\frac1T\sum_{t=1}^T\delta_{\xi_t}$, and $\mathbb P^\infty$ denotes the law of the sample path.
• A data-driven predictor is a continuous function $\hat c:X\times\mathcal P\to\mathbb R$; the estimate after $T$ samples is $\hat c(x,\hat{\mathbb P}_T)$. Its out-of-sample disappointment is $\mathbb P^\infty\big(c(x,\mathbb P)>\hat c(x,\hat{\mathbb P}_T)\big)$.
• Problem (5): $\hat c$ is feasible if, for all $x\in X$ and $\mathbb P\in\mathcal P$,

$$\limsup_{T\to\infty}\frac1T\log\mathbb P^\infty\big(c(x,\mathbb P)>\hat c(x,\hat{\mathbb P}_T)\big)\le -r,$$

and strongly optimal if it is feasible and $\hat c(x,\mathbb P')\le\hat c'(x,\mathbb P')$ for all $(x,\mathbb P')$ and every feasible $\hat c'$.

• The distributionally robust predictor is $\hat c_r(x,\mathbb P')=\sup\{c(x,\mathbb P):\mathbb P\in\mathcal P,\ I(\mathbb P',\mathbb P)\le r\}$.
• $\bar\gamma(x)=\max_{\xi\in\Xi}\gamma(x,\xi)$ is the worst-case cost and $\Xi^\star(x)$ the set of its maximizers.

Formalization targets

Goal: Theorem 10 (p. 26)

$$r\ge0\ \Longrightarrow\ \hat c_r\text{ is feasible in (5)},\qquad r>0\ \Longrightarrow\ \hat c_r\text{ is strongly optimal in (5)}.$$

Both halves are in the goal. The case $r=0$ of feasibility is the statement that $\hat c_0=c$ is continuous.

Milestones

• Lemma 1 (p. 23): $c$ is continuous on $X\times\mathcal P$.
• Lemma 2 (33), p. 29: $\hat c_r$ equals a supremum over pairs $(\mathbb P_c,p)$ with $\mathbb P'\ll p\,\mathbb P_c\ll\mathbb P'$, where the mass $1-p$ is placed at cost $\bar\gamma(x)$.
• Lemma 3 (p. 31): the perturbed problem (34), $\hat c_{r,\epsilon}$, satisfies $\hat c_r\le\hat c_{r,\epsilon}\le\hat c_r+\epsilon$.
• Lemma 4 (35), p. 31:

$$\hat c_{r,\epsilon}(x,\mathbb P')\le\min_{\alpha\ge\bar\gamma(x)+\epsilon}\ \alpha-e^{-r}\exp\Big(\int_\Xi\log(\alpha-\gamma(x,\xi))\,\mathrm d\mathbb P'(\xi)\Big),$$

with a minimizer $\alpha^\star\le(\bar\gamma(x)+\epsilon-e^{-r}c(x,\mathbb P'))/(1-e^{-r})$, and with equality for $\epsilon>0$.

• Proposition 6 (p. 25): $\hat c_r$ is continuous on $X\times\mathcal P$ for $r\ge0$.
• Theorem 9 (24a)/(24b), p. 25: the weak large deviation principle for $\hat{\mathbb P}_T$ in the weak topology, with the closure $\operatorname{cl}\mathcal D$ in the upper bound and the interior in the lower bound.
• (41), p. 35: if $\mathbb P_0(\Xi^\star(x))<1$ and $c(x,\mathbb P_0)\ge\hat c_r(x,\mathbb P')$, then $I(\mathbb P',\mathbb P_0)\ge r$.
• Proposition 1(ii), (iii) in the general setting (p. 24): $I$ is jointly convex and jointly lower semicontinuous on $\mathcal P\times\mathcal P$.

Proposition 5, the dual representation (23) of $\hat c_r$ itself, is included as a further item; the proof of Theorem 10 goes through Lemmas 3–4 and does not use it.

Significance

Theorem 10 says that, on any compact outcome space, no continuous predictor is less conservative than $\hat c_r$ while keeping its disappointment probability below $e^{-rT}$ to first order in the exponent. Relative-entropy distributionally robust optimization is therefore not one choice among many ambiguity sets but the optimal one for this criterion, and the dual representation turns its evaluation into a one-dimensional convex problem. The paper also shows that the continuous-state analogue of its prescriptor result (Theorem 11) only holds up to an arbitrarily small shift, so the predictor statement formalized here is the clean part of the extension.

The results are proved in the paper; none is formalized. A complete development yields a formal Sanov-type weak large deviation principle for empirical measures in the weak topology, joint convexity and lower semicontinuity of the Kullback–Leibler divergence for probability measures on a compact metric space, and a measure-theoretic dual representation of a relative-entropy worst-case expectation. Mathlib has the Kullback–Leibler divergence klDiv and the weak topology on probability measures, but none of these three results.

Difficulty

The finite-state proof of feasibility bounds the disappointment through the large deviations upper bound over the disappointment set $\mathcal D$ itself. On a continuous space that bound only holds over the closure $\operatorname{cl}\mathcal D$ in the weak topology (24a), and the paper notes that this invalidates the finite-state argument (p. 25). The rate must then be controlled on a larger, closed set of empirical distributions, where the strict inequality defining a disappointment is lost; this is where the mass that $\mathbb P_0$ puts on the worst-case scenarios $\Xi^\star(x)$ starts to matter, as the hypothesis of (41) shows.

Continuity of $\hat c_r$ in the weak topology is the second obstacle. The supremum runs over an infinite-dimensional set of distributions, a worst-case distribution may put mass outside the support of $\mathbb P'$, and the integrals involved can diverge or take the value $-\infty$. Weak convergence controls integrals of bounded continuous functions only, and $\log(\alpha-\gamma)$ is unbounded below at $\alpha=\bar\gamma(x)$.

Formalization scope

• $\mathcal P$ is ProbabilityMeasure ↥Ξ for the Borel σ-algebra of the subtype, with Mathlib's weak-convergence topology. $X$ and $\Xi$ are compact subsets of Euclidean spaces, $\gamma:↥X\to↥\Xi\to\mathbb R$ is jointly continuous; these standing assumptions of §2 (p. 5) and §5 (p. 23) appear as hypotheses of every theorem. No other hypothesis is added. Nonemptiness of $\Xi$ is automatic wherever a distribution on $\Xi$ is in scope.
• $I$ is Mathlib's InformationTheory.klDiv, valued in $[0,\infty]$. It equals Definition 8, including the value $+\infty$ when $\mathbb P'\not\ll\mathbb P$ or when the log-likelihood ratio is not integrable.
• The empirical distribution is defined for $T\ge1$. The probability of an event about $\hat{\mathbb P}_T$ is the outer measure under the product measure $\mathbb P^{\otimes T}$, and is $0$ at $T=0$; all statements are asymptotic in $T$.
• Decay rates are stated without logarithms: $\limsup\frac1T\log p_T\le-s$ becomes "for every $r'<s$, eventually $p_T\le e^{-r'T}$", which is equivalent and handles $p_T=0$. A naive Real.log encoding would be wrong, since Lean sets $\log0=0$. Predictors must be continuous for the weak topology; dropping continuity, or replacing the weak topology by a finer one, changes the problem.
• The constraint $\int\log(\frac1p\frac{\mathrm d\mathbb P'}{\mathrm d\mathbb P_c})\,\mathrm d\mathbb P'\le r$ in (33)–(34) carries an explicit integrability requirement, so that a divergent integral fails the constraint instead of evaluating to $0$. The geometric mean $\exp\int\log(\alpha-\gamma)\,\mathrm d\mathbb P'$ follows the paper's convention $\log0=-\infty$; it is defined as $\inf_{\delta>0}\exp\int\log(\alpha+\delta-\gamma)\,\mathrm d\mathbb P'$, which is the same value for $\alpha\ge\bar\gamma(x)$.
• At the end of the proof of Theorem 10 the page writes "when $\epsilon>0$" for strong optimality; the theorem statement says $r>0$, which is what is formalized.

Contributions are welcome at every level: a Sanov upper and lower bound for empirical measures on compact metric spaces, convexity and lower semicontinuity of klDiv, and the measure-theoretic duality of Lemma 4 are each reusable beyond this mission.

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.04118
• I. Csiszár, A simple proof of Sanov's theorem, Bulletin of the Brazilian Mathematical Society 37(4), 2006. https://doi.org/10.1007/s00574-006-0023-1
• T. van Erven, P. Harremoës, Rényi divergence and Kullback–Leibler divergence, IEEE Transactions on Information Theory 60(7), 2014. https://doi.org/10.1109/TIT.2014.2320500
• A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998. https://doi.org/10.1007/978-1-4612-5320-4

Motivation

Training data describe one probability distribution, while a deployed prediction rule may be evaluated under a nearby distribution. Distributionally robust learning measures a rule by its worst expected loss over a specified set of nearby laws. This changes the question from how well the rule fits the observed sample to how well it performs when probability mass can move. Wasserstein distance supplies a geometric notion of “nearby”: moving mass farther across the instance space costs more. The setting is relevant to the domain drift discussed by Lee and Raginsky and to Wasserstein robust optimization as developed by Mohajerin Esfahani and Kuhn.

Theorem 1 of Lee and Raginsky's 2018 paper gives a finite-sample answer. It controls the local worst-case risk at the true population law using quantities computed from the empirical law, and also controls the empirical local worst-case risk using population quantities. Both assertions are simultaneous over the entire loss class. This mission concerns exactly those two probability inequalities and the displayed claims in Appendix C.1 that support them. The source is the pinned arXiv:1705.07815v2 preprint, containing the NeurIPS 2018 paper and its supplementary appendix.

Setting

The instance space $\mathcal Z$ is a bounded Polish metric space with distance $d_{\mathcal Z}$. A probability measure $P$ generates $n\ge1$ independent observations $Z_1,\ldots,Z_n$. Their empirical distribution is $P_n=n^{-1}\sum_{i=1}^n\delta_{Z_i}$. A loss $f:\mathcal Z\to\mathbb R$ has risk $R(Q,f)=\int f\,dQ$ under a probability law $Q$. The class $\mathcal F$ consists of upper semicontinuous losses satisfying $0\le f(z)\le M$ for every $f\in\mathcal F$ and $z\in\mathcal Z$, as in Assumption 2 of the paper.

For $p\ge1$, the $p$-Wasserstein distance $W_p(Q,P)$ is the least $p$th-power transport cost over couplings of $Q$ and $P$, raised to the power $1/p$. The Wasserstein ball $B^W_{\varrho,p}(P)$ consists of probability laws $Q$ with $W_p(Q,P)\le\varrho$, where $\varrho>0$. The local worst-case risk is

$$R_{\varrho,p}(P,f)=\sup_{Q\in B^W_{\varrho,p}(P)}R(Q,f).$$

The dual expression uses the envelope $\varphi_{\lambda,f}(z)=\sup_{z'\in\mathcal Z}\{f(z')-\lambda d_{\mathcal Z}(z,z')^p\}$ for $\lambda\ge0$. To measure the size of $\mathcal F$, let $\mathcal N(\mathcal F,\|\cdot\|_\infty,u)$ be its uniform-metric covering number at radius $u$. The entropy integral is $\mathfrak C(\mathcal F)=\int_0^\infty\sqrt{\log\mathcal N(\mathcal F,\|\cdot\|_\infty,u)}\,du$. These symbols match the local Lean setting and the source's notation.

Formalization targets

Theorem 1: two data-dependent risk bounds

For every $t>0$, the mission goal is the conjunction of the paper's two displays:

$$\mathbb P\!\left\{\exists f\in\mathcal F:\ R_{\varrho,p}(P,f)>\inf_{\lambda\ge0}\left[(\lambda+1)\varrho^p+\mathbb E_{P_n}\varphi_{\lambda,f}+\frac{M\sqrt{\log(\lambda+1)}}{\sqrt n}\right]+\frac{24\mathfrak C(\mathcal F)+Mt}{\sqrt n}\right\}\le 2e^{-2t^2},$$ $$\mathbb P\!\left\{\exists f\in\mathcal F:\ R_{\varrho,p}(P_n,f)>\inf_{\lambda\ge0}\left[(\lambda+1)\varrho^p+\mathbb E_P\varphi_{\lambda,f}+\frac{M\sqrt{\log(\lambda+1)}}{\sqrt n}\right]+\frac{24\mathfrak C(\mathcal F)+Mt}{\sqrt n}\right\}\le 2e^{-2t^2}.$$

The seven milestones preserve displayed claims from Appendix C.1: the deterministic comparison through the supremum deviation $X_\lambda$, its concentration and symmetrization bounds, the entropy-integral estimate with constant $24$, the fixed-$\lambda$ probability bound, and the integer-grid union and comparison with real multipliers. They are statements from the author's argument, ordered by their appearance. The goal retains both directions of the published theorem and every printed constant.

Significance

The first bound provides a sample-dependent certificate for the worst-case population loss of every member of $\mathcal F$ at once. The second compares the robust empirical quantity with a population envelope. Together they make it possible to assess what a local Wasserstein ambiguity set buys in finite samples, rather than relying only on asymptotic convergence. The complexity term depends on the geometry of the loss class through its covering numbers, following a line of empirical-process bounds also seen in Bartlett and Mendelson's study of Rademacher complexity. Lee and Raginsky emphasize that this class complexity can reflect hypotheses outside the support of the data-generating law.

The mathematical theorem is proved in the 2018 paper; the particular declarations in this mission remain open Lean goals. A complete formal development would connect probability inequalities for supremum processes to the published Wasserstein distance and ball, make the entropy integral and its measurability consequences explicit, and verify both directions of the final bound. The reusable output includes a precise internal uniform covering number and a finite-sample Rademacher process for metric-space loss classes.

Difficulty

A fixed multiplier $\lambda$ is easier to control than the infimum over all $\lambda\ge0$. A pointwise concentration bound alone does not produce a simultaneous statement over an uncountable multiplier set. The source's final formula contains a logarithmic multiplier penalty, and retaining its coefficient $M$ and the probability factor $2$ requires accounting for that parameter range exactly. Independently, the supremum over an arbitrary loss class is a genuine random variable only with enough regularity. The boundedness of individual losses does not by itself settle the measurability of their unrestricted supremum.

The envelope $\varphi_{\lambda,f}$ also mixes the metric geometry with empirical-process complexity. Estimating a class of envelopes must remain tied to the covering properties of the original class $\mathcal F$. Replacing the envelope class by a finite hand-picked subclass or assuming the desired concentration inequality as a new hypothesis would change the theorem being formalized.

Formalization scope

Lean uses a metric space with its Borel measurable structure and a Polish-space instance, together with boundedness of the whole carrier. The Wasserstein distance and ball are imported from the published WassersteinLinOpt.Ball definitions. Because the carrier is bounded, every probability measure has a finite $p$th moment, matching the source's $\mathcal P_p(\mathcal Z)$. The ball is a subtype of probability measures; its supremum is taken only over feasible laws. Sample outcomes are functions Fin n → 𝒵, and the product measure gives their independent common law. The empirical law is a normalized finite sum of Dirac masses, while $\mathbb E_{P_n}$ is written as its equal finite average.

The paper does not specify whether covering centres must lie in $\mathcal F$. This formalization uses the internal covering number, whose centres do; its value is at least the external covering number. The entropy integral is extended nonnegative and is required to be finite in statements that convert it to a real number. This disclosed restriction avoids the default conversion of $+\infty$ to zero and supports the separability needed for expected suprema. Milestones using $X_\lambda$ also require $\mathcal F$ to be nonempty, so a real supremum never acquires the empty-family default value. The empty-class case of Theorem 1 remains valid because its failure events are empty.

The source writes minima over nonnegative real multipliers and positive integers. The Lean statements use bounded-below real infima; for the final bound, the appendix's comparison holds at every multiplier, so this reading is at least as strong as the printed minimum. All radii are positive, $p\ge1$, $n\ge1$, and $t>0$ where it appears. Failure probabilities use outer measure of the sample event directly, with no conversion through toReal. The goal never quantifies over arbitrary distributions outside the Wasserstein ball, and expectations of supremum processes are guarded by the finite-entropy hypothesis. Contributions are welcome on the concentration, symmetrization, covering-number, and transport-risk interfaces as well as the goal itself.

Selected references

• Jaeho Lee and Maxim Raginsky, Minimax Statistical Learning with Wasserstein Distances, Advances in Neural Information Processing Systems 31, 2018. arXiv:1705.07815v2.
• Peyman Mohajerin Esfahani and Daniel Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: Performance guarantees and tractable reformulations, Mathematical Programming 171, 2018. DOI:10.1007/s10107-017-1172-1.
• Peter L. Bartlett and Shahar Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3, 2002. JMLR paper.

Motivation

Best subset selection asks for the linear model that fits a response best using only a few of many candidate predictors. In its penalized form it is the least-squares problem with an $L_0$ penalty, the number of nonzero coefficients. The problem is NP-hard. Mixed-integer optimization can solve it to certified optimality at moderate sizes (Bertsimas, King, Mazumder 2016), but statisticians who fit whole regularization paths with tens of thousands of predictors need something faster. Hazimeh and Mazumder (arXiv:1803.01454, Operations Research 2020) proposed cyclic coordinate descent for the $L_0$-penalized problem, the method that glmnet made standard for the lasso. Their algorithm underlies the L0Learn software package.

Coordinate descent on a convex smooth-plus-separable objective converges by classical arguments (Tseng 2001). Those arguments do not cover the $L_0$ penalty, which is discontinuous. The paper adds occasional spacer steps to plain cyclic coordinate descent and proves that the modified algorithm converges to a coordinate-wise minimum. This mission formalizes that convergence theorem.

Setting

Let $X\in\mathbb R^{n\times p}$ be a model matrix whose columns $X_1,\dots,X_p$ have unit Euclidean norm, and let $y\in\mathbb R^n$. For $\beta\in\mathbb R^p$ let

$$f(\beta)=\tfrac12\|y-X\beta\|^2+\lambda_1\|\beta\|_1+\lambda_2\|\beta\|_2^2,\qquad F(\beta)=f(\beta)+\lambda_0\|\beta\|_0,$$

with $\lambda_0>0$ and $\lambda_1,\lambda_2\ge0$; $\|\beta\|_0$ counts the nonzero coordinates. Problem (2) is $\min_\beta F(\beta)$. Its three named cases are (L0) ($\lambda_1=\lambda_2=0$), (L0L1) ($\lambda_1>0=\lambda_2$) and (L0L2) ($\lambda_1=0<\lambda_2$). $\mathrm{Supp}(\beta)=\{i:\beta_i\ne0\}$.

Fix all coordinates but the $i$-th. With unit-norm columns, minimizing $F$ over $\beta_i$ amounts to minimizing a scalar function of $\tilde\beta_i=\langle y-\sum_{j\ne i}X_j\beta_j,X_i\rangle$. The minimizer set is $\tilde T(\tilde\beta_i,\lambda_0,\lambda_1,\lambda_2)$ (7). The thresholding operator $T$ (12) picks one element of it:

$$T(a,\lambda_0,\lambda_1,\lambda_2)=\mathrm{sign}(a)\frac{|a|-\lambda_1}{1+2\lambda_2}\ \text{ if }\ \frac{|a|-\lambda_1}{1+2\lambda_2}\ge\sqrt{\frac{2\lambda_0}{1+2\lambda_2}},\qquad 0\ \text{ otherwise.}$$

A coordinate-wise (CW) minimum is a $\beta$ such that every $\beta_i$ minimizes $F$ in coordinate $i$ with the others fixed (Definition 2). A stationary solution is a $\beta$ whose lower directional derivative $F'(\beta;d)=\liminf_{\alpha\downarrow0}(F(\beta+\alpha d)-F(\beta))/\alpha$ is nonnegative in every direction $d$ (Definition 1).

Algorithm 1 (CDSS) takes an initial point $\beta^0$ and a positive integer $C$. It sweeps the coordinates cyclically. Each non-spacer step sets the current coordinate to $T(\tilde\beta_i,\lambda_0,\lambda_1,\lambda_2)$ and increments a counter for the resulting support. When the counter of a support $S$ reaches $Cp$, a spacer step follows: one sequential pass over the coordinates of $S$ with the $L_0$ term switched off, $\beta_i\leftarrow T(\tilde\beta_i,0,\lambda_1,\lambda_2)$. The counter of $S$ is then reset. The iterates $\beta^k$ count both kinds of step.

For (L0) and (L0L1) the paper adds Assumption 1: every $\min\{n,p\}$ columns of $X$ are linearly independent. It also adds Assumption 2, which constrains the initial point when $p>n$: $F(\beta^0)\le\lambda_0 n$ for (L0), and $F(\beta^0)\le\min_\beta f(\beta)+\lambda_0 n$ for (L0L1).

Formalization targets

Goal: Theorem 2 (p. 12)

For (L0), (L0L1) and (L0L2), under Assumptions 1–2 in the first two cases, there are $m$ and a support $S$ with

$$\mathrm{Supp}(\beta^k)=S\ \ (k\ge m),\qquad \beta^k\to B,\qquad B\text{ a CW minimum},\qquad \mathrm{Supp}(B)=S .$$

The two parts share $S$: the support stabilizes, and the limit is a CW minimum on that support.

Milestones

• Lemma 5, monotone descent: $F(\beta^{k+1})\le F(\beta^k)$ and $F(\beta^k)\downarrow F^*\ge0$.
• Lemma 6: $\|\beta^k\|_0\le\min\{n,p\}$ for (L0), (L0L1).
• Lemma 8: $\{\beta^k\}$ is bounded.
• Lemma 1: stationarity is equivalent to $\nabla_S f(\beta)=0$ on the support $S$.
• Lemma 9: along a support $S$ recurring in non-spacer steps, the spacer iterates eventually keep support $S$. Every subsequence with support $S$ converges to the unique minimizer $\beta^*$ of $f$ on $S$, and $|\beta^*_j|\ge\sqrt{2\lambda_0/(1+2\lambda_2)}$ on $S$.
• Lemma 10: the support of every limit point occurs infinitely often.
• Lemma 2: closed form of $\tilde T$.
• Lemma 11: for two limit points whose supports differ by one index $j$, $|B^{(2)}_j|$ exceeds $\sqrt{2\lambda_0/(1+2\lambda_2)}$, or equals it, according to whether $X_j$ is correlated with the smaller support.
• Lemma 12: zeroing a nonzero coordinate decreases $F$ by at least $\frac{1+2\lambda_2}{2}\big(|\beta^k_j|-\sqrt{2\lambda_0/(1+2\lambda_2)}\big)^2$.
• Lemma 3: the coordinatewise characterization (8) of CW minima, with the condition $|\tilde\beta_i|>\lambda_1$ of (5) on the support (see Formalization scope).

Significance

Theorem 2 guarantees that exact cyclic coordinate descent on Problem (2), with spacer steps, has a limit, and that the limit is a CW minimum. That class is strictly smaller than the stationary solutions and the fixed points of iterative hard thresholding ((4), p. 5). It also serves as the inner solver of the paper's local combinatorial search (Algorithm 2, Theorem 4). So the guarantee transfers to the partial-swap-inescapable minima studied in the companion mission. Support stabilization (part 1) is also what reduces the asymptotic analysis to smooth strongly convex coordinate descent on a fixed support (Theorem 3).

The result is proved in the paper; no machine-checked version exists. A formalization would check the convergence argument for a discontinuous objective, where the bookkeeping of supports, counters and step indices is easy to get wrong. It would also provide a reusable Lean model of $L_0$-penalized least squares and its thresholding operators.

Difficulty

The standard proof for cyclic coordinate descent needs a uniform decrease per step or a continuous objective. Neither holds here. A coordinate may switch between zero and a nonzero value infinitely often while $F$ decreases by arbitrarily small amounts, so the descent property alone gives neither support stabilization nor convergence of the iterates. Coordinates dropped infinitely often and coordinates added infinitely often must both be excluded. The tie-breaking rule in $T$ matters here: with the other choice on ties the algorithm is different. The exclusion of coordinates added infinitely often is only sketched in the paper (p. 43), and a complete proof has to supply it.

Formalization scope

Vectors are Fin p → ℝ with 0-based indices. Every norm is written as an explicit sum; Mathlib's sup norm on function types is never used. Unit-norm columns, $\lambda_0>0$, $\lambda_1,\lambda_2\ge0$ and $p\ge1$ are hypotheses. The case $\lambda_1,\lambda_2>0$, which the paper never names, is excluded from the statements about the algorithm's limits. $\mathrm{sign}$ is Real.sign. $T$ chooses the nonzero solution on ties, as in (12). The lower directional derivative takes values in EReal, since it is $+\infty$ in directions leaving the support. Lemma 3 is stated with the condition $|\tilde\beta_i|>\lambda_1$ on the support, taken from (5). The printed condition (8) omits it, and without it the equivalence fails for $\lambda_1>0$. Indices and pages throughout are those of arXiv:1803.01454v3.

Algorithm 1 is a deterministic state machine: iterate, cyclic pointer, the counter array Count, and a flag for a pending spacer step. The iterates are therefore defined from $\beta^0$ and $C$, not quantified over. The pointer advances only on non-spacer steps, following the pseudocode box; the prose formula $i=(k+1)\bmod(p+1)$ on p. 10 contradicts it. A statement about an arbitrary sequence satisfying a step predicate, or one that adds a step size or a sufficient-decrease hypothesis, would describe a different algorithm and is ruled out.

Useful infrastructure includes the scalar thresholding lemmas and coercivity of $f$ under Assumption 1 on supports of size at most $\min\{n,p\}$. Contributions of proofs for any milestone are welcome, as are lemmas on the state machine (descent of each step type, the counter bookkeeping).

Selected references

• H. Hazimeh, R. Mazumder, Fast Best Subset Selection: Coordinate Descent and Local Combinatorial Optimization Algorithms, Operations Research 68(5), 2020; arXiv:1803.01454v3. https://arxiv.org/abs/1803.01454
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
• P. Tseng, Convergence of a block coordinate descent method for nondifferentiable minimization, J. Optim. Theory Appl. 109, 2001. https://doi.org/10.1023/A:1017501703105
• A. Beck, Y. C. Eldar, Sparsity constrained nonlinear optimization: optimality conditions and algorithms, SIAM J. Optim. 23(3), 2013. https://doi.org/10.1137/120869778
• J. Friedman, T. Hastie, R. Tibshirani, Regularization paths for generalized linear models via coordinate descent, J. Stat. Softw. 33(1), 2010. https://doi.org/10.18637/jss.v033.i01