Optimal Transport

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 based on observed data can change when the data law differs from the one used to choose it. Distributionally robust optimization addresses this by evaluating each decision against a family of nearby probability laws. Optimal transport gives one way to define “nearby”: a candidate law is admissible when probability mass can be moved from the baseline law at a bounded expected cost. For a linear decision rule, the resulting worst-case expectation is usually harder to optimize than an ordinary sample-average loss. Blanchet, Murthy, and Zhang identify a dual objective whose variables are the decision vector and a scalar transport multiplier, then study its curvature near the multipliers that actually minimize it (Blanchet–Murthy–Zhang, 2022).

The paper proves that this dual objective is jointly strongly convex on a specified region for sufficiently small transport radius. This matters because ordinary convexity allows flat directions in the joint decision–multiplier space. The joint lower Hessian bound gives local curvature in every direction with one positive modulus that remains independent of the radius apart from the paper's explicit factor $\sqrt{\delta}$ (Theorem 4, p. 11).

Setting

Let $X\in\mathbb R^d$ have a baseline probability law $P_0$, and let a decision be a vector $\beta$ in a nonempty compact convex set $B\subseteq\mathbb R^d$. The loss of a possible outcome $x$ is $\ell(\beta^{\mathsf T}x)$ for a convex function $\ell:\mathbb R\to\mathbb R$. A state-dependent positive-definite matrix $A(x)$ sets the cost of moving mass from $x$ to $x'$:

$$c(x,x')=(x-x')^{\mathsf T}A(x)(x-x').$$

Assumption 1 requires this cost to be lower semicontinuous and the eigenvalues of $A(x)$ to lie between positive constants $\rho_{\min}$ and $\rho_{\max}$ for $P_0$-almost every $x$. Assumption 2 requires at most quadratic growth of $\ell$ and a finite fourth moment of $P_0$. The ambiguity radius $\delta$ is positive (Assumptions 1–2, pp. 9–10).

The paper's dual objective is an expectation under the known law $P_0$. Write $q_A(\beta,x)=\beta^{\mathsf T}A(x)^{-1}\beta$. For a scalar $\lambda\ge0$ and an auxiliary scalar $\gamma$, set

$$F(\gamma,\beta,\lambda;x) =\ell\bigl(\beta^{\mathsf T}x+\gamma\sqrt\delta\,q_A(\beta,x)\bigr) -\lambda\sqrt\delta\bigl(\gamma^2q_A(\beta,x)-1\bigr), \qquad f_\delta(\beta,\lambda)=\mathbb E_{P_0}\!\left[\sup_{\gamma\in\mathbb R}F(\gamma,\beta,\lambda;X)\right].$$

This value may be $+\infty$. Under the paper's duality conditions, minimizing $f_\delta(\beta,\lambda)$ over $\lambda\ge0$ gives the worst-case loss at $\beta$ (Theorem 1 and (7), p. 10).

Formalization targets

Assumption 3 bounds $\ell''$ above by $M>0$ and excludes an almost surely zero $\ell'(\beta^{\mathsf T}X)$ for each $\beta\in B$. Assumption 4 makes $B$ compact. Lemma 6 supplies positive constants $\underline L,\overline L$ bounding $\mathbb E_{P_0}[\ell'(\beta^{\mathsf T}X)^2]$ uniformly over $B$. With $R_\beta=\sup_{\beta\in B}\|\beta\|$, the constants $K_1,K_2$ are those of (28), and

$$\mathbb V_\delta=\{(\beta,\lambda):\beta\in B,\ \lambda\ge0,\ K_1\|\beta\|\le\lambda\le K_2\|\beta\|\}.$$

Theorem 3 first gives a bounded Hessian on $\mathbb V_\delta$ and a positive lower bound on its $\beta$ block when $0<\delta<\delta_0$, with the explicit $\delta_0$ from p. 36. The goal, Theorem 4, adds Assumption 5: $\ell$ is locally strongly convex and, at each $\beta\in B$, the loss derivative and the linear score are simultaneously separated from zero with positive probability. It asserts the joint bound

$$\exists\,\delta_1\in(0,\delta_0),\ \kappa_1>0\quad \forall\,\delta\in(0,\delta_1),\ \forall\,\theta\in\mathbb V_\delta:\quad \nabla^2 f_\delta(\theta)\succeq\sqrt\delta\,\kappa_1 I_{d+1}.$$

The order of the quantifiers is part of the target: $\kappa_1$ works for every sufficiently small $\delta$ (Theorems 3–4, p. 11).

Significance

The Hessian bound makes the joint dual parameters locally identifiable by curvature on a region that contains every dual optimizer. In the paper, this structure also underlies the analysis of algorithms and of how the optimizer changes with the transport radius (Proposition 1, p. 11; §3 and §5.4). Theorem 4 is already proved in the paper; this mission asks for its machine-checked formalization, together with the stated bounds on multipliers, the maximizing scalar, and the intermediate curvature results. The general optimal-transport integral used here already has a published Prove2Me definition from Blanchet and Murthy's earlier model-risk work. The new definitions specify this paper's Mahalanobis model, regions, and smoothness assumptions.

Difficulty

Convexity alone gives only a nonnegative Hessian; it cannot produce a strictly positive joint lower bound. Even curvature of $\ell$ does not by itself control directions that combine a change in $\beta$ with a change in $\lambda$. The inner supremum over $\gamma$ can become infinite outside its effective domain, while at $\beta=0$ its maximizer ceases to be unique. The theorem therefore needs a region where the dual objective is finite and differentiable and a probabilistic condition that prevents the relevant score and derivative from vanishing together. The target keeps the actual $\sqrt\delta$ scale instead of settling for a radius-dependent positive constant (§2.2.2 and Remark 4, pp. 10–12, 39).

Formalization scope

Lean uses EuclideanSpace ℝ (Fin d) for $\mathbb R^d$, a Borel probability measure for $P_0$, and EReal for $f_\delta$ and the inner supremum. The reused extended-real integral records the $+\infty$ and $-\infty$ cases; the Hessian is taken only where $f_\delta$ is finite on a neighborhood and its real representative is differentiable there. Quadratic Hessian forms use $\|v_\beta\|^2+v_\lambda^2$, since Lean's product norm is not the paper's Euclidean norm. The compact set $B$ is explicitly nonempty, and the positive ambiguity radius $\delta$ is quantified inside the goal so that $\delta_1$ and $\kappa_1$ are uniform in $\delta$. Theorem 3 additionally assumes $R_\beta>0$ for the proof's explicit formula for $\delta_0$: nonempty compact $B=\{0\}$ would make that formula zero. Assumption 5 already gives $R_\beta>0$ in the goal.

The goal retains Assumption 5's per-decision quantifiers. That assumption itself excludes $0\in B$: its strict score event is empty at $\beta=0$. Intermediate statements where the printed wording includes $\beta=0$ but the claim fails there state $\beta\ne0$ explicitly. Lemma 5 also states the differentiability and positive-multiplier conditions needed for its derivative and division. Proposition 9(b)'s printed strict curvature-margin inequality is corrected to the nonstrict inequality derived in its proof; its original wording is preserved in the milestone quotation. The claims are about the expectation $f_\delta$, with $\kappa_1$ independent of $\delta$, rather than a pointwise or merely convex substitute.

A complete development needs measurable extended-real integration, the matrix quadratic form and its inverse, almost-everywhere spectral bounds, differentiability under an expectation, and Hessian estimates for an optimized scalar. The transport integral, the assumptions and constants, and the multiplier bounds are intended as reusable interfaces for the companion missions. Contributions that close the listed lemmas or add the paper's omitted second-order kernel formula are within scope.

Selected references

• José Blanchet, Karthyek Murthy, and Fan Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Mathematics of Operations Research 47(2), 2022. arXiv:1810.02403v3; DOI:10.1287/moor.2021.1178.
• José Blanchet and Karthyek Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research 44(2), 2019. arXiv:1604.01446v2.

Motivation

Distributionally robust optimization (DRO) replaces the expected loss $E_{P_0}[\ell(\beta^{\mathsf T}X)]$ of a decision $\beta$ under a baseline distribution $P_0$ by its worst case over all distributions $P$ that are close to $P_0$. When closeness is measured by an optimal transport cost, the worst case over this infinite-dimensional ball has a one-dimensional dual: by Theorem 1 of Blanchet, Murthy and Zhang (arXiv:1810.02403v3, Math. Oper. Res. 47(2), 2022), building on the strong duality of Blanchet and Murthy (arXiv:1604.01446),

$$\sup_{P : D_c(P_0, P) \le \delta} E_P\big[\ell(\beta^{\mathsf T}X)\big] = \inf_{\lambda \ge 0} f_\delta(\beta, \lambda).$$

The robust problem $\inf_{\beta \in B} \sup_P E_P[\ell(\beta^{\mathsf T}X)]$ thus becomes a joint minimization of the dual objective $f_\delta$ over $(\beta, \lambda)$. Whether that minimization is a convex program, and on which set the objective is finite, decides whether first-order methods such as the stochastic gradient schemes of the same paper apply at all. This mission formalizes the paper's answer, Theorem 2.

Setting

The data $X$ take values in $\mathbb{R}^d$ with law $P_0$, a Borel probability measure. A decision is a vector $\beta$ in a convex set $B \subseteq \mathbb{R}^d$, the loss is $\ell(\beta^{\mathsf T}x)$ for $\ell : \mathbb{R} \to \mathbb{R}$, and $\delta > 0$ is the transport budget.

The transport cost is the state-dependent Mahalanobis cost $c(x, x') = (x - x')^{\mathsf T}A(x)(x - x')$ for a map $A$ from $\mathbb{R}^d$ to positive definite $d \times d$ matrices. Assumption 1: $c$ is lower semicontinuous (1a), and $\rho_{\min}\|v\|^2 \le v^{\mathsf T}A(x)v \le \rho_{\max}\|v\|^2$ for $P_0$-almost every $x$, with $\rho_{\min} > 0$ (1b). Write $q_\beta(x) = \beta^{\mathsf T}A(x)^{-1}\beta$.

Assumption 2: $\ell$ is convex, its growth exponent

$$\kappa = \inf\Big\{ s \ge 0 : \sup_{u \in \mathbb{R}} \big(\ell(u) - s u^2\big) < \infty \Big\}$$

is finite, and $E_{P_0}\|X\|^4 < \infty$.

For $\gamma \in \mathbb{R}$, $\lambda \ge 0$ and $x \in \mathbb{R}^d$ define, as in display (7),

$$F(\gamma, \beta, \lambda; x) = \ell\big(\beta^{\mathsf T}x + \gamma\sqrt{\delta}\, q_\beta(x)\big) - \lambda\sqrt{\delta}\big(\gamma^2 q_\beta(x) - 1\big),$$

the robust loss $\ell_{rob}(\beta, \lambda; x) = \sup_{\gamma \in \mathbb{R}} F(\gamma, \beta, \lambda; x) \in \mathbb{R} \cup \{+\infty\}$, its set of maximizers $\Gamma^*(\beta, \lambda; x)$, and the dual objective

$$f_\delta(\beta, \lambda) = E_{P_0}\big[\ell_{rob}(\beta, \lambda; X)\big] \in \mathbb{R} \cup \{\pm\infty\}.$$

The effective domain is $\mathbb{U} = \{(\beta, \lambda) \in B \times \mathbb{R}_+ : f_\delta(\beta, \lambda) < \infty\}$, and with the threshold $\lambda_{thr}(\beta) = \kappa\sqrt{\delta}\,\operatorname{ess\,sup}_{P_0} q_\beta$ the paper sets $\mathbb{U}_1 = \{\lambda > \lambda_{thr}(\beta)\}$ and $\mathbb{U}_2 = \{\lambda \ge \lambda_{thr}(\beta)\}$ inside $B \times \mathbb{R}_+$.

Formalization targets

Goal: Theorem 2 (p. 10)

Under Assumptions 1 and 2, $f_\delta : B \times \mathbb{R}_+ \to \mathbb{R} \cup \{\infty\}$ is proper and convex: $f_\delta > -\infty$ on $B \times \mathbb{R}_+$; for each $\beta \in B$ some $\lambda \ge 0$ has $f_\delta(\beta, \lambda) < \infty$; and for $\theta_1, \theta_2 \in B \times \mathbb{R}_+$, $\alpha \in [0, 1]$,

$$f_\delta\big(\alpha\theta_1 + (1 - \alpha)\theta_2\big) \le \alpha f_\delta(\theta_1) + (1 - \alpha) f_\delta(\theta_2).$$

Milestones

1. Lemma 3 (p. 32). For each $\varepsilon > 0$ there are $C_1, C_2 > 0$, not depending on $x$, $\beta$, $\lambda$, such that whenever $\lambda \ge (\kappa + \varepsilon)\sqrt{\delta}\,q_\beta(x)$ we have $\sqrt{\delta}|g|q_\beta(x) \le 1 + C_1\varepsilon^{-1}(1 + |\beta^{\mathsf T}x|)$ for every $g \in \Gamma^*(\beta, \lambda; x)$, and $\ell_{rob}(\beta, \lambda; x) \le \lambda\sqrt{\delta} + C_2(1 + \varepsilon + \varepsilon^{-1})(1 + |\beta^{\mathsf T}x|)^2$.
2. Display (25) (p. 32). $\sup_{\Delta \in \mathbb{R}^d}\{\ell(\beta^{\mathsf T}(x + \Delta)) - \tfrac{\lambda}{\sqrt\delta}(\Delta^{\mathsf T}A(x)\Delta - \delta)\} = \ell_{rob}(\beta, \lambda; x)$.
3. Lemma 2 (p. 16). $(\beta, \lambda) \mapsto \ell_{rob}(\beta, \lambda; x)$ is convex on $B \times \mathbb{R}_+$ for every $x$.
4. Lemma 1 (p. 16). $\Gamma^* \neq \emptyset$ and $\ell_{rob}$ finite if $\lambda > \kappa\sqrt{\delta}\,q_\beta(x)$; $\Gamma^* = \emptyset$ and $\ell_{rob} = \infty$ if $\lambda < \kappa\sqrt{\delta}\,q_\beta(x)$; consequently $\mathbb{U}_1 \subseteq \mathbb{U} \subseteq \mathbb{U}_2$.

Lemma 3 is stated with constants depending only on $\varepsilon$ (and the fixed data), as its proof produces them and as the paper's later arguments integrate bound (b) over $x$.

Significance

Theorem 2 is the structural fact behind the paper's algorithms: with Theorem 1 it turns a minimax problem over probability measures into a convex minimization in $d + 1$ real variables, on which the paper's strong convexity results (Theorems 3–5) and its stochastic gradient schemes are built. Lemma 1 identifies the effective domain up to its boundary, which tells an algorithm where the dual multiplier must lie, and Lemma 3 gives the growth control of the robust loss used throughout the appendix.

The results are proved in the paper; none of them has a machine-checked proof. The mission produces a Lean statement of the dual objective as an extended-real integral and of its convexity and properness, reusable by the other missions of this series (strong convexity near the optimizers, worst-case distributions, comparative statics in $\delta$), and contributions of formal proofs of the milestones and the goal.

Difficulty

The objective takes the value $+\infty$ on part of its domain: Lemma 1(b) shows that $\ell_{rob} = +\infty$ below the threshold, so the naive reading "$f_\delta$ is a real convex function" is false, and convexity must be handled for functions with values in $\mathbb{R} \cup \{\infty\}$, including the conventions $0 \cdot \infty = 0$ at the endpoints of the segment. Properness requires a bound on $\ell_{rob}$ that is integrable in $x$, so the constants of Lemma 3 must not depend on $x$; a bound that is only pointwise finite does not suffice. The identity (25) relates a supremum over $\mathbb{R}^d$ to a supremum over $\mathbb{R}$ through a change of the dual variable, and the two multipliers must be kept apart. Finally, the expectation in $f_\delta$ is an integral of an extended-real function whose measurability is not assumed but has to be derived from Assumption 1.

Formalization scope

$\mathbb{R}^d$ is EuclideanSpace ℝ (Fin d) and parameters $(\beta, \lambda)$ live in EuclideanSpace ℝ (Fin d) × ℝ. $\ell_{rob}$ is an EReal supremum; $f_\delta$ is the published ModelRiskOT.Duality.extIntegral, $\int \varphi^+\,dP_0 - \int \varphi^-\,dP_0$ with lower Lebesgue integrals. $\kappa$ is a real infimum and $\lambda_{thr}$ uses the real essential supremum; both are used only under Assumptions 1–2, which make them meaningful. Convexity of extended-real maps is written as the explicit inequality in EReal, since ConvexOn does not apply.

Standing assumptions carried by every statement: $P_0$ a probability measure, $\delta > 0$, $B$ convex (the paper's standing assumption). Conventions committed to: "for any $x$" in Lemmas 1–2 is every $x$, not almost every; Lemma 2 assumes only Assumption 1a and the convexity of $\ell$; the identity (25) is stated with the old multiplier written as $\lambda/\sqrt{\delta}$; the typo "$\beta A(x)^{-1}\beta$" in Lemma 1 is read as $\beta^{\mathsf T}A(x)^{-1}\beta$; the goal's "finite somewhere" is stated for each $\beta \in B$, so the goal is vacuous only when $B = \emptyset$. The fourth-moment condition of Assumption 2 is kept as printed.

A trivializing formalization is ruled out: "proper" is not encoded as "finite everywhere" (false by Lemma 1(b)), and pointwise convexity of $\ell_{rob}$ (Lemma 2) is a milestone, not the goal, which is about the expectation $f_\delta$.

A complete development needs: positive definite matrices and the quadratic minimization behind (25); continuity of convex functions and growth bounds; lower Lebesgue integrals of extended-real functions and their monotonicity and additivity; measurability of a supremum over $\gamma$ of continuous functions. The definitions layer is shared with the other four missions of this series. Proofs of any milestone and of the goal are welcome.

Selected references

• J. Blanchet, K. Murthy, F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Mathematics of Operations Research 47(2), 2022. arXiv:1810.02403v3, doi:10.1287/moor.2021.1178
• J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research 44(2), 2019. arXiv:1604.01446, doi:10.1287/moor.2018.0936

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 classifier trained from finitely many examples can perform well on those examples while responding poorly to changes in the feature distribution or to mislabeled observations. Distributionally robust learning addresses this by choosing a classifier against every probability distribution within a specified distance of the empirical distribution. The resulting optimization appears to range over an infinite-dimensional family of distributions. Shafieezadeh-Abadeh, Kuhn, and Mohajerin Esfahani show that, for linear classification with a convex Lipschitz loss, this problem has an exact finite convex reformulation. That result is Theorem 3.11(ii) of the 2019 arXiv preprint, which is the source used here.

The authors' transport metric allows a data point's features to move and its binary label to flip, with separate prices for those two changes. This matters when robustness to inaccurate labels is part of the model. A label-preserving metric cannot express that choice. The paper builds on its Section 2 learning model and the transport duality developed in Appendix A.1; the present mission isolates the classification result and the intermediate statements used for it. The preprint's Corollary 3.14 specializes the result to logloss, while its Corollary 3.12 treats hinge loss. A logloss-specific reformulation and a label-preserving classification result already have proved statements on Prove2Me; the general convex-Lipschitz, finite label-cost theorem remains the target of this mission.

Setting

Let $V$ be a finite-dimensional real vector space with a chosen norm $\|\cdot\|$. Features are $x\in V$ and labels are $y\in\{-1,+1\}$. A linear classifier is a continuous linear functional $w:V\to\mathbb R$, with score $\langle w,x\rangle=w(x)$. Its dual norm $\|w\|_*$ is the operator norm induced by $\|\cdot\|$. Given $N\ge1$ training pairs $(\hat x_i,\hat y_i)$, their empirical distribution is $\hat P_N=N^{-1}\sum_{i=1}^N\delta_{(\hat x_i,\hat y_i)}$.

For $\kappa>0$, the transport cost between pairs is

$$d((x,y),(x',y'))=\|x-x'\|+\kappa\mathbf1_{y\ne y'}.$$

The Wasserstein distance $W(Q,P)$ is the least expected transport cost among joint distributions whose two marginals are $Q$ and $P$. For a radius $\rho\ge0$, the Wasserstein ball $\mathbb B_\rho(\hat P_N)$ contains probability distributions $Q$ satisfying $W(Q,\hat P_N)\le\rho$. The loss is $L(y\langle w,x\rangle)$, where $L:\mathbb R\to[0,\infty)$ is convex and Lipschitz continuous. The Lipschitz modulus $\operatorname{lip}(L)$ is the smallest Lipschitz bound for $L$, defined as the supremum of its difference quotients. These are the objects and standing conventions of Sections 1.1, 2, and 3.2 of the preprint.

Formalization targets

The goal is Theorem 3.11(ii): for every fixed $w$, the worst-case expected loss equals the value of program (18),

$$\sup_{Q\in\mathbb B_\rho(\hat P_N)}\mathbb E^Q[L(y\langle w,x\rangle)] = \inf_{\lambda,s}\left\{\lambda\rho+\frac1N\sum_{i=1}^{N}s_i: \begin{array}{l} L(\hat y_i\langle w,\hat x_i\rangle)\le s_i,\\ L(-\hat y_i\langle w,\hat x_i\rangle)-\kappa\lambda\le s_i\quad(i=1,\ldots,N),\\ \operatorname{lip}(L)\|w\|_*\le\lambda \end{array}\right\}.$$

Taking the infimum of both sides over $w$ gives equality between problem (4) and the full program (18). The fixed-$w$ identity is stated explicitly because it is the stronger assertion established in the proof. The milestone list follows the paper's appendix: Lemma A.1 converts the robust expectation into a scalar transport-price infimum; the label split isolates the two possible labels; Lemma A.3 evaluates the feature supremum; the ensuing display gives the program in terms of conjugate slopes; and the final identity identifies those slopes with $\operatorname{lip}(L)$. Each milestone is tied to its printed page in the preprint.

Significance

The theorem replaces a search over probability distributions by a finite convex program with one scalar $\lambda$ and one slack variable $s_i$ per sample, in addition to the classifier $w$. It makes the price of label changes explicit through $\kappa\lambda$ and the price of feature changes through $\operatorname{lip}(L)\|w\|_*$. Consequently, different convex Lipschitz classification losses can be treated within the same transport model rather than by deriving a new distributional optimization problem for each loss. The preprint applies the result to hinge, smoothed hinge, and logloss examples in the paragraphs following Theorem 3.11.

The result is proved in the cited paper. Its general statement and the paper's appendix milestones are not yet machine-checked in this mission. A verified development would connect the published definitions of the Wasserstein ball and Lipschitz modulus to an exact program-value theorem that later work can import. The loss-specific proved statements already available on Prove2Me provide useful comparisons, but their narrower losses or label-preserving transport costs do not replace this theorem.

Difficulty

The visible finite constraints contain no probability distributions, while the left-hand side optimizes over all probability measures in a Wasserstein ball. Establishing that the two values coincide requires control of the transport budget and the inner worst-case loss at the same time. The straightforward comparison of feasible values gives only one inequality. It does not show that every improvement allowed by a distribution can be represented by the scalar transport price and the samplewise constraints. The case $\rho=0$ also needs care: Lemma A.1's strong-duality proof cites a result for strictly positive radius, whereas the theorem itself allows zero radius and states an infimum rather than an attained minimum.

Formalization scope

Lean represents $V$ by an abstract finite-dimensional real normed space with its Borel measurable structure. This retains the arbitrary norm of $\mathbb R^n$ in the paper. Labels are Bool, interpreted as $+1$ and $-1$; the published DRLogReg_Reformulation_Core definition supplies their sign map, the metric, Wasserstein distance, ball, and empirical distribution. The published WassersteinDRO_Duality_lipschitzModulus definition supplies the exact Lipschitz modulus. The mission's own definitions add the general loss, the feasible set of (18), the fixed-classifier program value, and the effective domain $\Theta=\{\theta:L^*(\theta)<\infty\}$ of the convex conjugate. The same objects and conventions are used across all milestones.

All potentially infinite robust values are represented in $[0,\infty]$; the unbounded feature suprema in Lemma A.3 and the label split use extended reals. The standing loss condition $L\ge0$ comes from the paper's Section 2.1 loss codomain. It also makes the lower Lebesgue integral and the finite program's extended-nonnegative objective faithful. The sample size is positive, $\kappa>0$, and the goal allows $\rho=0$. Lemma A.1 separately assumes $\rho>0$, matching the strong-duality condition used on page 29. The printed extra index $j\in[J]$ in the page-35 classification display is carried in its verbatim milestone provenance but not in the Lean statement, because no $j$ exists in part (ii). The formalization does not obtain the theorem by restricting $L$ to a constant loss, by taking a singleton feature space, or by substituting an arbitrary Lipschitz bound for its modulus. Contributions that establish transport duality, the conjugate-domain slope identity, or the zero-radius case are directly reusable.

Selected references

• S. Shafieezadeh-Abadeh, D. Kuhn, and P. Mohajerin Esfahani, Regularization via Mass Transportation, arXiv preprint arXiv:1710.10016v3, 2019. Preprint.
• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, and D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28, 2015. Published Prove2Me formalization.

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.