Optimal Transport

Motivation

Ordinary least squares and its robust relatives (least absolute deviations, Huber, $\epsilon$-insensitive and quantile regression) fit a linear predictor by minimizing an average loss over the training sample. That average estimates the out-of-sample error poorly when the sample is small, and the usual fix is to add a regularization penalty such as a norm of the weights. Choosing that penalty is often a heuristic. Distributionally robust optimization gives one principled derivation of it: hedge against every data-generating distribution that is close to the empirical one in a Wasserstein distance, and minimize the worst-case expected loss.

S. Shafieezadeh-Abadeh, D. Kuhn and P. Mohajerin Esfahani, Regularization via Mass Transportation (arXiv:1710.10016v3, 2019; JMLR 20, 2019), show that for linear regression with a convex Lipschitz loss this worst-case problem is exactly a regularized empirical risk problem, with an explicit dual-norm penalty. The same identity appears for the logistic loss in Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn, Distributionally Robust Logistic Regression (NeurIPS 2015, arXiv:1509.09259). For a general convex loss it is Theorem 10 of the tutorial by Kuhn, Mohajerin Esfahani, Nguyen and Shafieezadeh-Abadeh (arXiv:1908.08729). Blanchet, Kang and Murthy (arXiv:1610.05627) obtain the square-root Lasso from a type-2 transport cost. This mission formalizes the regression theorem of the first paper, Theorem 3.1(ii) on p. 8. The source PDF is the arXiv preprint v3, and every page and label cited here refers to it.

Setting

Data. Inputs are $x\in\mathbb R^n$ and outputs are $y\in\mathbb R$. A pair is written $\xi=(x,y)\in\mathbb R^{n+1}$. The training samples are $(\hat x_i,\hat y_i)$ for $i=1,\dots,N$, and $\hat{\mathbb P}_N=\frac1N\sum_{i=1}^N\delta_{(\hat x_i,\hat y_i)}$ is their empirical distribution (§2.1, p. 5).

Hypotheses and loss. A weight vector $w\in\mathbb R^n$ defines the linear hypothesis $h(x)=\langle w,x\rangle$. A univariate convex loss $L:\mathbb R\to\mathbb R$ defines the regression loss $\ell(\langle w,x\rangle,y)=L(\langle w,x\rangle-y)$ (§3.1, p. 8). The residual $\langle w,x\rangle-y$ is the pairing of $\xi$ with the vector $(w,-1)$.

Norms. $\mathbb R^{n+1}$ carries an arbitrary norm $\|\cdot\|$ with dual norm $\|z\|_*=\sup\{\langle z,\xi\rangle:\|\xi\|\le1\}$ (§1.1, p. 4). The Lipschitz modulus of $L$ is $\mathrm{lip}(L)=\sup_{z\ne z'}|L(z)-L(z')|/|z-z'|$, and the convex conjugate is $L^*(\theta)=\sup_z\theta z-L(z)$ (§1.1).

Wasserstein ball. With transport cost $d(\xi,\xi')=\|\xi-\xi'\|$, the Wasserstein distance (Definition 2.2, p. 7) is

$$W(\mathbb Q,\mathbb Q')=\inf_\Pi\int d(\xi,\xi')\,\Pi(\mathrm d\xi,\mathrm d\xi'),$$

where the infimum runs over couplings $\Pi$ of $\mathbb Q$ and $\mathbb Q'$. The ball of radius $\rho\ge0$ is $\mathbb B_\rho(\hat{\mathbb P}_N)=\{\mathbb Q:\mathbb Q(\Xi)=1,\ W(\mathbb Q,\hat{\mathbb P}_N)\le\rho\}$ (3). The distributionally robust regression problem is

$$\inf_w\ \sup_{\mathbb Q\in\mathbb B_\rho(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[L(\langle w,x\rangle-y)\big].\qquad(4)$$

Formalization targets

Goal: Theorem 3.1(ii), p. 8

Let $\Xi=\mathbb R^{n+1}$, $\rho\ge0$, $N\ge1$, and let $L$ be nonnegative, convex and Lipschitz continuous. Then for every $w$

$$\sup_{\mathbb Q\in\mathbb B_\rho(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[L(\langle w,x\rangle-y)\big]=\frac1N\sum_{i=1}^NL(\langle w,\hat x_i\rangle-\hat y_i)+\rho\,\mathrm{lip}(L)\,\|(w,-1)\|_*,$$

so (4) and the regularized problem (6) have the same optimal value.

Milestones

1. Lemma A.1 (p. 28). The worst case over the ball equals $\inf_{\lambda\ge0}\lambda\rho+\frac1N\sum_i\sup_\xi[I(\xi)-\lambda d(\xi,\hat\xi_i)]$. This milestone is linked to the published, proved WassersteinDRO.Duality.strong_duality_worst_case_risk_v2, which covers it for $\rho>0$.
2. Lemma A.3 (p. 29). For $\gamma>0$, $\sup_\zeta L(\langle\beta,\zeta\rangle)-\gamma\|\zeta-\hat\zeta\|$ equals $L(\langle\beta,\hat\zeta\rangle)$ if $\mathrm{lip}(L)\|\beta\|_*\le\gamma$, and $+\infty$ otherwise.
3. End of the proof of Lemma A.3 (p. 30). $\mathrm{lip}(L)=\sup\{|\theta|:L^*(\theta)<\infty\}$.
4. The inf-over-$\lambda$ display in the proof of Theorem 3.1(ii) (pp. 30–31). The worst case equals $\inf\{\lambda\rho+\frac1N\sum_iL(\langle w,\hat x_i\rangle-\hat y_i):\lambda\ge0,\ \mathrm{lip}(L)\|(w,-1)\|_*\le\lambda\}$.

Significance

The result. The theorem turns an infinite-dimensional min–max problem over distributions into a finite convex program over $w$: an empirical average plus a norm penalty. The penalty is not $\|w\|_*$ but $\|(w,-1)\|_*$, because the transport cost moves outputs as well as inputs. It scales with the radius $\rho$ and with the Lipschitz modulus of the univariate loss. With the Huber, $\epsilon$-insensitive and pinball losses it gives Corollaries 3.2–3.4 of the paper. It also gives a statistical reading of the regularization weight as a Wasserstein radius, which the paper's §4 turns into generalization bounds.

Formalizing it. The theorem is proved in the paper; none of its items is formalized yet except Lemma A.1. Lemma A.1 is available in a general form (any $p\ge1$, any closed support set, $\rho>0$) as a proved platform theorem from the mission Wasserstein Distributionally Robust Optimization. The per-$w$ identity also follows from the proved WassersteinDRO.Duality.convex_loss_p1_v2 (Theorem 10 of the tutorial, also present as WassersteinDRO.Regularization.convex_loss_p1_v2; the public mission Wasserstein Distributionally Robust Optimization IV has it as goal) once one shows that $\mathrm{lip}(L\circ\langle(w,-1),\cdot\rangle)=\mathrm{lip}(L)\|(w,-1)\|_*$. No platform item states that factorization. What this mission adds is the paper's explicit form of the penalty, Lemma A.3 (the inner supremum for an arbitrary convex Lipschitz loss and an arbitrary norm), and the conjugate description of the Lipschitz modulus. The last two are reusable in classification (mission I of this series states them again in its own namespace) and in every Wasserstein-regularization result with linear hypotheses.

Difficulty

The obvious argument is to write the worst case as a supremum over perturbations of the samples and bound each perturbed loss by its Lipschitz constant. That gives only the inequality "$\le$", and only for one Lipschitz constant. The identity needs two further steps that this bound does not supply. First, the bound must be attained: the supremum over distributions has to be shown to reach $\rho\,\mathrm{lip}(L)\|(w,-1)\|_*$, a matching lower bound that a Lipschitz estimate cannot give. Second, $\mathrm{lip}(L)$ must be the modulus, not any constant: an upper Lipschitz constant $K>\mathrm{lip}(L)$ makes the identity false. In Lemma A.3 the case $\mathrm{lip}(L)\|\beta\|_*=\gamma$ sits exactly on the boundary between a finite and an infinite supremum. A further point is that the duality of Lemma A.1 needs $\rho>0$, while the theorem includes $\rho=0$.

Formalization scope

• Space. $\mathbb R^{n+1}$ with an arbitrary norm is an abstract finite-dimensional real normed space E with its Borel σ-algebra. A continuous linear isomorphism e : E ≃L[ℝ] (Fin n → ℝ) × ℝ reads off inputs and outputs. The theorem therefore covers every norm on $\mathbb R^{n+1}$; fixing a concrete norm would prove it for that norm only. The functional $(w,-1)$ is pairing e w, and $\|(w,-1)\|_*$ is its operator norm.
• Published objects. The ball, the worst case, the empirical distribution and the Lipschitz modulus are the published definitions WassersteinDRO_Duality_ambiguitySet, _worstCaseRisk_v2, _empiricalDistribution and _lipschitzModulus. The worst case is taken in the extended reals, and expectations follow the convention of nominalRisk_v2 (no junk value for non-integrable losses). $\mathrm{lip}(L)$ takes values in $[0,\infty]$.
• Standing assumptions. $L$ is nonnegative, convex on $\mathbb R$ and Lipschitz continuous; $N\ge1$; $\rho\ge0$; $\Xi=\mathbb R^{n+1}$. The paper's $L\ge0$ (§2.1) is imposed as the standing loss-function assumption.
• Reading of "equivalent". The paper does not define the word. The goal states the per-$w$ identity that the proof establishes plus equality of optimal values. Attainment of the infimum is not claimed.
• Corrections. The printed display on p. 30 omits a factor $\frac1N$ and carries a stray $|\theta|$ in the constraint; milestone 4 states the corrected identity. The printed Lemma A.1 omits $\rho>0$, which its proof uses; the linked platform theorem has it.
• Ruled out. The goal is not a restatement of Theorem 10 with $\mathrm{Lip}(\ell_w)$ of the composite loss: its right-hand side is the explicit average of (6) with $\mathrm{lip}$ of the univariate $L$ and the dual norm of $(w,-1)$.
• Welcome contributions. The factorization $\mathrm{lip}(L\circ\beta)=\mathrm{lip}(L)\|\beta\|_*$ for a linear functional $\beta$ on a finite-dimensional normed space, conjugate calculus for univariate convex functions, and the evaluation of the worst case at $\rho=0$.

Selected references

• S. Shafieezadeh-Abadeh, D. Kuhn, P. Mohajerin Esfahani, Regularization via Mass Transportation, arXiv:1710.10016v3, 2019; J. Mach. Learn. Res. 20(103), 2019. https://arxiv.org/abs/1710.10016
• D. Kuhn, P. Mohajerin Esfahani, V. A. Nguyen, S. Shafieezadeh-Abadeh, Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning, INFORMS TutORials, 2019. https://arxiv.org/abs/1908.08729
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171, 2018. https://arxiv.org/abs/1505.05116
• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, NeurIPS, 2015. https://arxiv.org/abs/1509.09259
• J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, J. Appl. Probab. 56(3), 2019. https://arxiv.org/abs/1610.05627
• D. P. Bertsekas, Convex Optimization Theory, Athena Scientific, 2009 (cited as [9] in the paper for Propositions 5.3.1 and 5.5.4).

Motivation

Wasserstein distributionally robust optimization (Wasserstein DRO) replaces the expected loss under an empirical distribution by the worst-case expected loss over all distributions within a Wasserstein distance $\rho$ of it. It is used in operations research, statistics and machine learning to guard decisions and predictors against the gap between the sample and the population. The statistical question it raises is how large $\rho$ must be for the robust loss to bound the true loss with high probability. Classical answers go through the concentration of the empirical measure in Wasserstein distance, which forces $\rho\asymp n^{-1/d}$ in dimension $d$: the curse of dimensionality.

Gao (arXiv:2009.04382; Operations Research, 2023) shows that a radius of order $n^{-1/2}$ suffices, independently of the dimension. The first ingredient, and the subject of this mission, is a new concentration inequality for the empirical mean of a single loss function, whose rate is governed by the Wasserstein regularizer itself.

Setting

Let $\mathcal Z$ be a separable Banach space with norm $\|\cdot\|$ and let $p\in[1,2]$. $\mathcal P_p(\mathcal Z)$ is the set of Borel probability measures with $\mathbb E[\|z\|^p]<\infty$, and the Wasserstein distance of order $p$ is

$$\mathcal W_p(\mathbb P,\mathbb Q)^p=\inf_\pi\ \mathbb E_{(\tilde z,z)\sim\pi}\big[\|\tilde z-z\|^p\big],$$

the infimum over couplings $\pi$ of $\mathbb P$ and $\mathbb Q$. For a loss $f:\mathcal Z\to\mathbb R$, a nominal distribution $\mathbb Q$ and a radius $\rho\ge0$, the Wasserstein regularizer is the excess of the robust loss over the nominal loss,

$$\mathcal R_{\mathbb Q,p}(\rho;f)=\sup_{\mathbb P\in\mathcal P_p(\mathcal Z)}\big\{\mathbb E_{\mathbb P}[f]:\mathcal W_p(\mathbb P,\mathbb Q)\le\rho\big\}-\mathbb E_{\mathbb Q}[f].$$

The data are $n$ i.i.d. samples $z_1,\dots,z_n$ from an unknown $\mathbb P_{\rm true}$; $\mathbb P_\otimes$ is their joint law and $\mathbb E_{\mathbb P_n}[f]=\frac1n\sum_i f(z_i)$ is the empirical loss. A distribution $\mathbb P$ satisfies the transportation-information inequality $T_p(\tau)$ if

$$\mathcal W_p(\mathbb Q,\mathbb P)\le\sqrt{\tau\,H(\mathbb Q\|\mathbb P)}\qquad\forall\,\mathbb Q\in\mathcal P_p(\mathcal Z),$$

with $H$ the relative entropy. $T_1$ holds for every distribution with a Gaussian moment $\mathbb E[e^{a\|z\|^2}]<\infty$, and $T_2$ (Talagrand's inequality) is implied by a log-Sobolev inequality.

The rate function is built from

$$\Phi_g(t)=\mathbb E_{z\sim\mathbb P_{\rm true}}\Big[\sup_{\tilde z\in\mathcal Z}\big\{t(g(\tilde z)-g(z))-\|\tilde z-z\|^p\big\}\Big],\qquad \mathcal I_p(\varepsilon;g)^p=\sup_{t>0}\{\varepsilon t-\Phi_g(t)\}.$$

Formalization targets

Goal: Theorem 1 (variation-based concentration, p. 7)

If $f\le M+L\|z\|^p$ with $M,L>0$ and $\mathbb P_{\rm true}$ satisfies $T_p(\tau)$, then for every $\varepsilon>0$

$$\mathbb P_\otimes\big\{\mathbb E_{\mathbb P_n}[f]-\mathbb E_{\mathbb P_{\rm true}}[f]<-\varepsilon\big\}\le\exp\big(-n\,\mathcal I_p(\varepsilon;-f)^2/\tau\big),$$

and for every $t>0$, with probability at least $1-e^{-t}$,

$$\mathbb E_{\mathbb P_{\rm true}}[f]\le\mathbb E_{\mathbb P_n}[f]+\mathcal R_{\mathbb P_{\rm true},p}\Big(\sqrt{\tfrac{\tau t}{n}};-f\Big).$$

Milestones

1. Lemma 4 (p. 21): if $\mathbb P$ satisfies $T_p(\tau)$, the product $\mathbb P^{\otimes n}$ satisfies $T_p(\tau n^{2/p-1})$ for the $\ell_p$ product distance $\mathsf d_p(z,\tilde z)^p=\sum_i\|z_i-\tilde z_i\|^p$.
2. Identity (5) (p. 21): the relative entropy of an exponential tilt, $H(\nu^{(g)}\|\nu)=\mathbb E_{\nu^{(g)}}[g]-\ln\mathbb E_\nu[e^g]$. Already proved on the platform and referenced.
3. Proposition 1 (p. 6): $\mathcal I_p(\cdot;f)$ inverts the regularizer, $\mathcal I_p(\mathcal R_{\mathbb P_{\rm true},p}(\rho;f);f)=\rho$ when the dual minimizer $\lambda_o$ of the strong-duality problem (1) exceeds the growth rate $\underline\lambda$ of $f$, and $\ge\rho$ when they coincide.
4. Lemma 5 (p. 21): the same two bounds for a general $F:\mathcal Z^n\to\mathbb R$ with $\mathbb E_\otimes[F]=0$ and $p$-growth, with rate $\mathcal J(\varepsilon;F)$ and bound $\mathcal R(\sqrt{\tau t/n};F)$.
5. Corollary 1 (p. 7), two items: for $p=1$ under a uniform Lipschitz bound, $\mathbb E_{\mathbb P_{\rm true}}[f]\le\mathbb E_{\mathbb P_n}[f]+\sqrt{\tau t/n}\,\|f\|_{\rm Lip}$; for $p=2$ under a Lipschitz gradient, the bound $\sqrt{\tau t/n}\,\|\|\nabla f\|_*\|_{\mathbb P_{\rm true},2}+\hbar\tau t/n$.

Significance

Theorem 1 says that the large-deviation rate of the empirical loss is the inverse of the Wasserstein regularizer, and that the regularizer at radius $\sqrt{\tau t/n}$ is a valid high-probability correction of the empirical loss. Neither involves the dimension of $\mathcal Z$ or the complexity of a covering of it. The paper builds its covering-number and local-Rademacher guarantees for Wasserstein DRO (Sections 4.1–4.2, the subject of two companion missions) on this single-function result, and Corollary 1 recovers, for $p=1$, the Lipschitz-norm bound known from transportation inequalities while sharpening it for $p=2$.

The results are proved in the paper; none is formalized. A complete development would give a machine-checked tensorization of transportation-information inequalities on Banach spaces and a Marton–Herbst-type concentration argument, both of which are used well beyond DRO.

Difficulty

The proof combines three ingredients that Mathlib does not yet connect. Tensorization (Lemma 4) needs disintegration of a measure on $\mathcal Z^n$ and the chain rule for relative entropy, together with a gluing of couplings and Hölder's inequality for the dimension constant. Lemma 5 combines $T_p$ with Kantorovich duality for the cost $\frac1n\mathsf d_p^p$ and the entropy of an exponential tilt, then optimizes a Young-inequality split over two parameters for $p<2$, and extends from bounded $F$ to $p$-growth by monotone truncation. Proposition 1 rests on the strong duality (1) of Gao and Kleywegt, an external result, and on the first-order optimality condition of a convex perspective function. A naive approach that bounds the deviation by $\mathcal W_p(\mathbb P_n,\mathbb P_{\rm true})$ fails: that distance decays like $n^{-1/d}$, which is exactly the curse the theorem avoids.

Formalization scope

The source is arXiv:2009.04382; its printed page numbers equal the PDF's. The Lean development lives in the namespace WassFSG.Conc and uses these conventions:

• $\mathcal Z$ is a real Banach space with its Borel $\sigma$-algebra and is second countable (separable), as the cited duality results require; $\mathcal W_p^p$ is the published optimal transport cost with cost $\|u-w\|^p$, and $H$ is Mathlib's klDiv.
• Expectations of a loss inside the robust supremum are extended integrals $\int f^+-\int f^-$ in $[-\infty,\infty]$; the regularizer is valued in $[-\infty,\infty]$.
• $\mathcal I_p^p$ and $\mathcal J^p$ are read as $\max(0,\sup_{t>0}\{\cdots\})\in[0,\infty]$, since the paper's declared codomain $\mathbb R_+\cup\{+\infty\}$ fails without it; an infinite rate gives the bound $0$, never $1$.
• Lemma 5's printed "min" is an infimum, and Proposition 1's printed limit $\underline\lambda$ is a $\limsup$.
• The product space carries the $\ell_p$-sum cost, not the sup metric.
• "With probability at least $1-\delta$" bounds the outer measure of the bad set by $\delta$; the sample size satisfies $n\ge1$.
• Added hypotheses: measurability and $\mathbb P_{\rm true}$-integrability of $f$ in Theorem 1 and Proposition 1, measurability of $F$ in Lemma 5, and a nontrivial $\mathcal Z$ and $\mathbb P_{\rm true}\in\mathcal P_p(\mathcal Z)$ (presupposed by the dual problem (1)) in Proposition 1.
• Theorem 1's growth hypothesis is kept as printed, an upper bound on $f$. When $-f$ has no $p$-growth bound, both conclusions hold trivially (the rate is $0$ and the regularizer is $+\infty$).

A formalization that reads an infinite $\mathcal I_p$ through a real coercion would turn the tail bound into the trivial bound $1$; the conventions above rule this out. Likewise a regularizer whose supremum ranged only over measures supported on the sample, or a $T_p$ condition over a restricted class of $\mathbb Q$, would be a different statement.

Contributions welcome: Lemma 4 and Corollary 1 are independent entry points; a proof of the duality (1) under the paper's growth condition would be reusable by every Wasserstein DRO mission.

Selected references

• R. Gao, Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality, Operations Research, 2023; preprint arXiv:2009.04382.
• R. Gao and A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research, 2023; arXiv:1604.02199.
• C. Villani, Optimal Transport: Old and New, Springer, 2009; doi:10.1007/978-3-540-71050-9.
• N. Gozlan and C. Léonard, Transport Inequalities. A Survey, Markov Processes and Related Fields, 2010; arXiv:1003.3852.
• F. Bolley and C. Villani, Weighted Csiszár–Kullback–Pinsker inequalities and applications to transportation inequalities, Annales de la Faculté des Sciences de Toulouse, 2005; doi:10.5802/afst.1095.

Motivation

Two-stage decision problems split decisions into a here-and-now decision $x$, taken before an uncertain parameter $\xi$ is observed, and a wait-and-see (recourse) decision $y$, taken after. Stochastic programming minimizes the expected total cost under a known distribution of $\xi$; robust optimization minimizes the worst-case cost over a support set. Distributionally robust optimization sits between the two: it minimizes the worst-case expected cost over an ambiguity set of distributions consistent with the available data. When the data are $I$ samples $\hat\xi_1,\dots,\hat\xi_I$, a natural ambiguity set is the ball of radius $\epsilon$ around the empirical distribution in the Wasserstein distance, which contains the two-stage stochastic program with a discrete distribution ($\epsilon = 0$) and, for a bounded support, the two-stage robust program (large $\epsilon$) as special cases.

Single-stage Wasserstein problems with piecewise-linear losses admit finite convex reformulations (Mohajerin Esfahani and Kuhn; Gao and Kleywegt). Two-stage problems are generically NP-hard, and the existing approaches were exponential-size reformulations or decision-rule restrictions. Hanasusanto and Kuhn (arXiv:1609.07505v3) show that two-stage distributionally robust linear programs over a 2-Wasserstein ball are equivalent to, or approximated arbitrarily well by, copositive programs of polynomial size: all the difficulty is moved into the cone. This mission formalizes that result, Theorem 5 of the paper, and the chain of lemmas behind it (§3, pp. 7–19).

Setting

The first-stage decision $x$ ranges over a set $\mathcal X\subseteq\mathbb R^{N_1}$ with cost $c^\top x$. The recourse function is the optimal value of a linear program,

$$Z(x,\xi) = \inf\{(Q\xi+q)^\top y : y\in\mathbb R^{N_2},\ T(x)\xi + h(x) \le Wy\},$$

where $T(x)\in\mathbb R^{M\times K}$ and $h(x)\in\mathbb R^M$ are affine in $x$ and $W\in\mathbb R^{M\times N_2}$; its value lies in $[-\infty,+\infty]$. The uncertain parameter takes values in the polyhedron $\Xi=\{\xi\in\mathbb R^K_+ : S\xi\le t\}$, assumed non-empty. The problem has complete recourse if $Wy^+>0$ for some $y^+$, and sufficiently expensive recourse if for every $\xi\in\Xi$ there is $p\ge0$ with $Q\xi+q = W^\top p$ (the dual recourse problem is feasible); the latter is a standing assumption.

The worst-case expectation is

$$\mathcal Z(x) = \sup\Big\{\mathbb E_{\mathbb P}[Z(x,\tilde\xi)] : \mathbb P(\Xi)=1,\ W_2(\mathbb P,\hat{\mathbb P}_I)\le\epsilon\Big\},\qquad \hat{\mathbb P}_I = \frac1I\sum_{i\in[I]}\delta_{\hat\xi_i},$$

with $W_2$ the 2-Wasserstein distance for the Euclidean cost. Problem (1) is: minimize $c^\top x + \mathcal Z(x)$ over $x\in\mathcal X$.

A symmetric matrix $M$ is copositive ($M\succeq_{\mathcal C}0$) if $v^\top Mv\ge0$ for all $v\ge0$, strictly copositive ($M\succ_{\mathcal C}0$) if $v^\top Mv>0$ for all nonzero $v\ge0$, and completely positive ($M\succeq_{\mathcal C^*}0$) if $M=BB^\top$ for an entrywise nonnegative $B$. The extended data stack the support constraints under the recourse data: $\mathcal Q=[Q;S]$, $\boldsymbol q=[q;-t]$, $\mathcal T(x)=[T(x);0]$, $\boldsymbol h(x)=[h(x);0]$, $\mathcal W=[[W,0],[0,-\mathbb I]]$ (in the paper, $\boldsymbol q$ and $\boldsymbol h$ are script letters).

For $\delta\ge0$, $\overline{\mathcal Z}_\delta(x)$ is the value of the copositive program (24): minimize $\epsilon^2\lambda + \frac1I\sum_i[s_i+\boldsymbol q^\top\psi_i-\lambda\|\hat\xi_i\|_2^2+\sum_j\phi_{ij}\boldsymbol q_j^2]$ over $\lambda\ge0$, $s_i$, $\psi_i$, $\phi_i$, subject to a $3\times3$ block matrix built from $\lambda$, $\phi_i$, $\psi_i$, $s_i$, $\hat\xi_i$ and the extended data being copositive for every $i$; $\delta$ enters only as $\delta\mathbb I$ in the middle diagonal block. $\underline{\mathcal Z}_\delta(x)$ is the value of the completely positive program (25), with objective $\frac1I\sum_i[\mathrm{tr}(\mathcal T(x)Y_i)+\boldsymbol h(x)^\top\gamma_i-\delta\,\mathrm{tr}(\Gamma_i)]$. At $\delta=0$ these are (10) and (14), with values $\overline{\mathcal Z}(x)$ and $\underline{\mathcal Z}(x)$. Problem (28) replaces $\mathcal Z(x)$ in (1) by $\overline{\mathcal Z}_\delta(x)$.

Formalization targets

Goal: Theorem 5 (pp. 18–19)

Under the standing assumptions,

1. if $\delta=0$ and (1) has complete recourse, (28) is equivalent to (1): $\inf(28)=\inf(1)$, with the same minimizers;
2. $\inf(1)\le\inf(28)$ at $\delta=0$;
3. $\inf(28)\le\inf(1)$ for every $\delta>0$;
4. if $\mathcal X$ is compact, $\inf(28)\to\inf(1)$ as $\delta\downarrow0$, and every cluster point of minimizers of (28) along $\delta_n\downarrow0$ minimizes (1).

Milestones, in the order the proof uses them

• Theorem 1 (p. 7): $\mathcal Z(x)$ equals a generalized moment problem (5) and, for $\epsilon>0$, the dual (6).
• Lemma 1 (p. 8): copositivity can be tested on vectors with last entry $1$.
• Theorem 2 (p. 8): $\mathcal Z(x)\le\overline{\mathcal Z}(x)$.
• Proposition 1 (p. 10): (10) and (14) are dual; formalized as weak duality $\underline{\mathcal Z}_\delta(x)\le\overline{\mathcal Z}_\delta(x)$.
• Lemma 2 (pp. 13–14): completely positive decompositions of feasible points of (14) give points of $\Xi$ and recession directions with feasible dual recourse solutions.
• Theorem 3 (p. 10): $\mathcal Z(x)=\underline{\mathcal Z}(x)$.
• Lemma 3 (p. 15): complete recourse implies $WW^\top\succ_{\mathcal C}0$.
• Lemma 4 (p. 16): a copositive Schur complement criterion.
• Theorem 4 (p. 16): under complete recourse, $\mathcal Z(x)=\underline{\mathcal Z}(x)=\overline{\mathcal Z}(x)$.
• Proposition 2 (p. 17): for $\delta>0$, $\overline{\mathcal Z}_\delta(x)=\underline{\mathcal Z}_\delta(x)$ is finite, and $\overline{\mathcal Z}_\delta(x)\to\mathcal Z(x)$ as $\delta\downarrow0$.

Significance

The result. Theorem 5 turns an infinite-dimensional min–sup–min problem into a single finite conic program whose size is polynomial in $K, J, M, N_1, N_2, I$. Replacing the copositive cone by any of the known inner approximation hierarchies then yields a sequence of tractable conservative approximations, which is how the paper obtains its numerical method. Item 4 states that without complete recourse nothing is lost asymptotically: the perturbed programs approximate (1) from below to arbitrary accuracy. The same statements cover classical two-stage robust optimization with bounded polyhedral uncertainty (Corollary 1).

Formalizing it. The result is proved in the paper; no machine-checked proof of it is known. A complete development would give the first formal treatment of copositive and completely positive duality, of the moment/dual reformulation of Wasserstein balls around an empirical distribution for extended-real losses, and of an epi-convergence argument for parametrized optimal values. The paper omits the proof of Proposition 1 ("Details are omitted for brevity"), so a formal proof also fills a gap in the written argument.

Difficulty

Lagrangian duality between (10) and (14) gives only $\underline{\mathcal Z}\le\overline{\mathcal Z}$, and Example 1 of the paper (p. 15) shows that this gap can be infinite: the obvious "dualize and invoke strong duality" argument fails without a constraint qualification, and the copositive cone has no tractable description from which one could be read off. The equality $\mathcal Z=\underline{\mathcal Z}$ is not a duality statement at all: it compares a supremum over probability measures with a supremum over completely positive moment matrices, and feasible moment matrices need not come from any distribution on $\Xi$ when $\Xi$ is unbounded. Theorem 1 already requires the moment and duality theory of Wasserstein balls for an extended-real, possibly discontinuous loss. Item 4 of the goal is an exchange of a limit in $\delta$ with an infimum over $x$, which fails without compactness and without lower semicontinuity of $\overline{\mathcal Z}_\delta$ in $x$, a property not visible from the definition of $\overline{\mathcal Z}_\delta$ as an infimum.

Formalization scope

The Lean development uses the namespace WassTwoStage.Copositive. Uncertain parameters live in EuclideanSpace ℝ (Fin K); matrices act on coordinate vectors, and stacked blocks are indexed by sum types (Fin N₂ ⊕ Fin J, Fin M ⊕ Fin J, and Fin K ⊕ ((Fin M ⊕ Fin J) ⊕ Unit) for the $3\times3$ block matrices). $T$ and $h$ are affine maps. Every optimal value, including $Z(x,\xi)$, $\mathcal Z(x)$, $\overline{\mathcal Z}_\delta(x)$, $\underline{\mathcal Z}_\delta(x)$ and the values of (1) and (28), is an infimum or supremum in EReal, so an infeasible copositive program has value $+\infty$. Limits are taken in the order topology of $[-\infty,+\infty]$, from the right. The expectation of the extended-real recourse value is $+\infty$ when its positive part has infinite integral. The Wasserstein ball, empirical distribution, expectation and copositivity are reused from published platform definitions.

The following hypotheses, implicit in the paper, are explicit binders: $I\ge1$; $\hat\xi_i\in\Xi$ for every $i$; $\Xi\neq\emptyset$; sufficiently expensive recourse; $\epsilon\ge0$ (and $\epsilon>0$ only for the dual (6)). "For any fixed $x\in\mathcal X$" is stated for every $x\in\mathbb R^{N_1}$. A minimizer for (28) is the first-stage part $x$ of a solution, minimizing $c^\top x+\overline{\mathcal Z}_\delta(x)$; the inner infimum need not be attained. The completely positive cone allows any finite number of columns. Item 2 of the goal drops the paper's assumption "(1) fails to have complete recourse", which the bound does not use.

The statement cannot be trivialized: $\mathcal Z(x)$ is defined as the supremum over the Wasserstein ball, not by (5) or (6); no Bochner integral (which returns $0$ for non-integrable integrands) and no real-valued sSup/sInf occur; copositivity quantifies over the whole nonnegative orthant, not over all of $\mathbb R^n$; and item 1 asserts equality of values and of minimizer sets, not an inequality.

A complete proof needs conic duality for the copositive/completely positive pair, the Wasserstein moment duality of Theorem 1, measurable selections, and lower semicontinuity and epi-convergence arguments. The cone and Schur-complement lemmas (Lemmas 1, 3, 4) and Theorem 1 are reusable beyond this mission. Proofs of individual milestones, alternative arguments, and supporting lemmas are welcome.

Selected references

• G. A. Hanasusanto and D. Kuhn, Conic Programming Reformulations of Two-Stage Distributionally Robust Linear Programs over Wasserstein Balls, Operations Research 66(3), 2018; arXiv:1609.07505v3, 2020. https://arxiv.org/abs/1609.07505
• P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171, 2018. https://arxiv.org/abs/1505.05116
• R. Gao and A. J. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, 2016. https://arxiv.org/abs/1604.02199
• S. Burer, On the copositive representation of binary and continuous nonconvex quadratic programs, Mathematical Programming 120(2):479–495, 2009. https://doi.org/10.1007/s10107-008-0223-z

Two-stage decisions under an ambiguous distribution

Two-stage stochastic linear programs model decisions taken in two steps: a first-stage decision $x$ is fixed before an uncertain parameter $\xi$ is observed, and a second-stage (recourse) decision $y$ adapts to $\xi$ afterwards. They underlie capacity planning, inventory and network design. In practice the distribution of $\xi$ is known only through samples $\hat\xi_1,\dots,\hat\xi_I$. Distributionally robust optimization replaces the unknown distribution by the worst case over an ambiguity set; a popular choice is a Wasserstein ball around the empirical distribution, because it contains the true distribution with high probability and yields out-of-sample guarantees (Mohajerin Esfahani and Kuhn, 2018).

Hanasusanto and Kuhn (arXiv:1609.07505, Operations Research 66(3), 2018) study when the resulting two-stage problem can be solved exactly. Section 3 of their paper gives a copositive reformulation for the 2-Wasserstein ball (the subject of a companion mission). Section 4, the subject of this mission, shows that when the uncertainty enters only the constraints of the recourse problem and the ball is a 1-Wasserstein ball with a polyhedral reference distance, the whole problem is a linear program.

Setting

Let $c\in\mathbb R^{N_1}$ and $\mathcal X\subseteq\mathbb R^{N_1}$ be the first-stage cost and feasible set, $q\in\mathbb R^{N_2}$ the second-stage cost, $W\in\mathbb R^{M\times N_2}$ the recourse matrix, and $T(x)\in\mathbb R^{M\times K}$, $h(x)\in\mathbb R^M$ affine functions of $x$. The recourse value at $\xi\in\mathbb R^K$ is

$$Z(x,\xi)=\inf\{\,q^\top y : y\in\mathbb R^{N_2},\ T(x)\xi+h(x)\le Wy\,\}\in[-\infty,+\infty].$$

The uncertainty affects only the constraints (in the paper's notation, $Q=0$), and there is no support constraint: $\Xi=\mathbb R^K$. The problem has sufficiently expensive recourse if some $p\ge 0$ satisfies $W^\top p=q$.

For scaling parameters $w_+,w_->0$ the reference distance is $d(\xi,\xi')=\|\xi-\xi'\|$ with

$$\|\xi\|=\sum_{k\in[K]}\max\{w_+\xi_k,\,-w_-\xi_k\}. \qquad (31)$$

Moving a unit of mass in the positive direction of coordinate $k$ costs $w_+$, in the negative direction $w_-$. The 1-Wasserstein ball $\mathcal B^1_\epsilon(\hat{\mathbb P}_I)$ consists of the probability measures $\mathbb P$ on $\mathbb R^K$ whose optimal transport cost to $\hat{\mathbb P}_I=\frac1I\sum_i\delta_{\hat\xi_i}$ under $d$ is at most $\epsilon$. The worst-case expectation and the two-stage problem (1) are

$$\mathcal Z(x)=\sup_{\mathbb P\in\mathcal B^1_\epsilon(\hat{\mathbb P}_I)}\mathbb E_{\mathbb P}[Z(x,\tilde\xi)],\qquad \inf_{x\in\mathcal X}\ c^\top x+\mathcal Z(x).$$

The dual norm of (31) is $\|z\|_*=\sup\{z^\top\xi:\|\xi\|\le 1\}$.

Formalization targets

Goal: Theorem 6

For $\epsilon>0$ and every $x\in\mathcal X$, $\mathcal Z(x)$ equals the optimal value of the linear program

$$\begin{aligned}\min\ \ &\epsilon\lambda+\frac1I\sum_{i\in[I]}q^\top y_i\\ \text{s.t.}\ \ &\lambda\ge 0,\quad T(x)\hat\xi_i+h(x)\le Wy_i\ \ \forall i\in[I],\\ &q^\top\phi_k\le\lambda,\ q^\top\psi_k\le\lambda,\ T(x)e_k/w_+\le W\phi_k,\ -T(x)e_k/w_-\le W\psi_k\ \ \forall k\in[K],\end{aligned}\qquad(32)$$

and consequently problem (1) has the optimal value of (32) minimized jointly over $x\in\mathcal X$ and the other variables with $c^\top x$ added to the objective.

Milestones, in the order of the paper's proof

1. Theorem 1 in this instance ($r=1$, gauge cost, $\Xi=\mathbb R^K$): $\mathcal Z(x)$ equals the moment problem (5) and, for $\epsilon>0$, the dual

$$\mathcal Z(x)=\inf_{\lambda\ge 0}\ \epsilon\lambda+\frac1I\sum_{i}\sup_{\xi\in\mathbb R^K}\big[Z(x,\xi)-\lambda\|\xi-\hat\xi_i\|\big].$$

2. Display (33): $\mathcal Z(x)=\inf\{\epsilon\lambda+\frac1I\sum_i\sup_{p\ge0,\,W^\top p=q}\,h(x)^\top p+(T(x)^\top p)^\top\hat\xi_i\ :\ \lambda\ge0,\ \|T(x)^\top p\|_*\le\lambda\ \forall p\ge0,\,W^\top p=q\}$.
3. The dual norm of (31): $\|z\|_*=\max_{k}\max\{z_k/w_+,\,-z_k/w_-\}$.
4. The constraint decomposition: the semi-infinite constraint of (33) holds if and only if, for each $k$, there are $\phi_k,\psi_k$ satisfying the four linear inequalities of (32).

Significance

Theorem 6 shows that the two-stage distributionally robust linear program over a 1-Wasserstein ball, which is a priori an optimization over infinitely many distributions, has a linear-programming reformulation with $O(I+K)$ blocks of variables and constraints. It covers distributionally robust least-absolute-deviation regression (Example 2 of the paper), where the reformulation becomes the empirical loss plus a dual-norm regularizer, and it contrasts with the paper's Theorem 7, which shows that for $p$-norm reference distances with $p>1$ the same problem is NP-hard.

The result is proved in the paper; there is no machine-checked proof. A formalization adds a verified chain from the measure-theoretic worst-case expectation to a finite linear program, including the conventions the paper leaves implicit: the extended-real values ($\mathcal Z(x)$ may be $+\infty$, and (32) may then be infeasible), the restriction $\epsilon>0$, and the first-stage cost in the objective.

Difficulty

Each step of the proof is classical, but the chain crosses several regimes. Theorem 1 is a Wasserstein strong duality result, and here it is applied to a loss $Z(x,\cdot)$ that is convex, possibly $+\infty$ on part of $\mathbb R^K$, and not upper semicontinuous, with a cost that is not symmetric; the standard published duality theorems assume an upper semicontinuous real-valued loss or a metric. The passage to (33) interchanges a supremum over $\xi$ with an infimum over the dual-norm ball and must handle the case where the dual recourse polyhedron is unbounded. Finally, every equivalence must hold in the extended reals: an argument that tacitly assumes finiteness proves a statement that fails exactly when the dual polyhedron has a recession direction.

Formalization scope

Vectors are Fin n → ℝ, samples are ξhat : Fin I → (Fin K → ℝ) with $I\ge1$, and $\mathbb R^K$ carries its product (Borel) σ-algebra. $T$ and $h$ are affine maps. The transport cost is the platform definition RWPI.SqrtLasso.transportCost (couplings with first marginal $\mathbb P$, second $\hat{\mathbb P}_I$), the empirical distribution is WassersteinDRO.Duality.empiricalDistribution, and expectations of the extended-real recourse value use WassersteinDRO.Duality.erealExpectation (value $+\infty$ whenever the positive part has infinite integral). Every optimal value is an extended-real infimum or supremum over its feasible set; no Bochner integral and no real-valued sInf/sSup is used.

Conventions made explicit, with reasons:

• $\epsilon>0$. The paper does not restrict $\epsilon$ in Theorem 6, but its proof starts from the dual (6), stated only for $\epsilon>0$, and the identity is false at $\epsilon=0$ when the dual recourse polyhedron has a recession direction $r$ with $T(x)^\top r\ne0$: then (32) is infeasible while $\mathcal Z(x)$ is the finite sample average.
• $c^\top x$ in (32). The printed objective of (32) omits the first-stage cost. The proof establishes the pointwise identity $\mathcal Z(x)=$ value of (32) at $x$, which is the goal's first part; the problem-level equivalence restores $c^\top x$.
• Asymmetric gauge. For $w_+\ne w_-$, (31) is not a norm, and Theorem 1 of the paper is stated for a metric. The paper applies it to (31) anyway; the milestone states that application, with the gauge cost in the orientation $d(\xi,\hat\xi_i)=\|\xi-\hat\xi_i\|$. The case $w_+=w_-$ is not imposed.
• Finite first moment. Membership in $\mathcal M^1(\mathbb R^K)$ is implied by finite transport cost to $\hat{\mathbb P}_I$ and is not repeated.
• The two "$1/N$" factors in the paper's proof are misprints for $1/I$.

A formalization in which $\mathcal Z$ is defined by (6), (33) or (32), in which the gauge is secretly symmetric, or in which expectations are Bochner integrals (zero for non-integrable functions) would make the goal trivial or different; the definitions here exclude each of these.

A complete development needs Wasserstein strong duality for a lower semicontinuous loss and cost (with a disintegration of couplings to pass to the moment problem (5)), LP strong duality and Farkas' lemma in the extended-real form, and a minimax interchange over a compact dual-norm ball. Wasserstein duality for general costs and extended-real LP duality are reusable well beyond this mission; contributions of either are welcome.

Selected references

• G. A. Hanasusanto, D. Kuhn, Conic Programming Reformulations of Two-Stage Distributionally Robust Linear Programs over Wasserstein Balls, Operations Research 66(3), 2018. Pinned version: arXiv:1609.07505v3. DOI 10.1287/opre.2017.1698.
• P. Mohajerin Esfahani, D. 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
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44(2), 2019. doi:10.1287/moor.2018.0936
• R. Gao, A. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, Mathematics of Operations Research 48(2), 2023. doi:10.1287/moor.2022.1275
• D. P. Bertsekas, Convex Optimization Theory, Athena Scientific, 2009 (Proposition 5.5.4, the minimax theorem used in the proof).

Motivation

In distributionally robust optimization, a decision is judged against probability laws near a nominal law rather than against the nominal law alone. The nominal law is often the empirical distribution of observed data. For a loss function, this produces a worst-case expected loss that depends on the size and geometry of the permitted changes to the data. The infinity-Wasserstein model restricts how far any observation can be moved, apart from null events in a coupling. It is a mathematical form of the bounded perturbations used in adversarial learning. Gao, Chen and Kleywegt study when this robust loss behaves like a regularizer based on variation or local slope.

For a finite data set, the nominal law has finite support. This makes the infinity-Wasserstein case especially concrete: each atom of the empirical law has a radius-limited set of possible destinations. Yet the objective still ranges over all probability measures, and the loss need not be bounded on a metric ball. The paper's finite-support duality result and its local-slope estimate together identify the regularization term that this distributional model produces.

Setting

Let $(Z,d)$ be a metric space and let $P,Q$ be probability laws on its Borel sets. A coupling $\pi$ of $P$ and $Q$ is a joint law on $Z\times Z$ with those two marginals. The infinity-Wasserstein distance is

$$W_\infty(P,Q)=\inf_{\pi\in\Gamma(P,Q)} \operatorname*{ess\,sup}_{(\tilde z,z)\sim\pi}d(\tilde z,z).$$

Given a real loss $f$ and a radius $\rho\ge0$, the robust value is the supremum of $\mathbb E_P[f]$ over all $P$ satisfying $W_\infty(P,Q)\le\rho$. The regularizer $R_{Q,\infty}(\rho;f)$ is this robust value minus $\mathbb E_Q[f]$. For observations $z_1,\ldots,z_n$, the empirical law is $P_n=n^{-1}\sum_{i=1}^n\delta_{z_i}$.

The one-sided local slope $|\partial f|(z)$ records the greatest limiting rate at which $f$ can increase under a perturbation that tends to $z$. The local growth $G_f(\delta,z)$ is the largest increase $f(\tilde z)-f(z)$ among destinations with $d(\tilde z,z)\le\delta$. A set $D_f$ marks the interfaces between pieces of a piecewise loss. Its boundary contribution at $z$ is $(\delta-d(z,D_f))_+$, where the distance to an empty set is infinite. These objects appear in Definition 2 and Assumption 5(I).

Formalization targets

Finite-support transport duality

For a nominal law $Q=\sum_j q_j\delta_{z_j}$, the first targets assert that an optimal coupling exists when $W_\infty(P,Q)$ is finite and that

$$\sup_{P:W_\infty(P,Q)\le\rho}\mathbb E_P[f] =\sum_j q_j\sup_{d(\tilde z,z_j)\le\rho}f(\tilde z).$$

This is Lemma EC.2 in the appendix. The values are allowed to be infinite when a local loss supremum is infinite; the printed assertion of unconditional finiteness is not included.

Consistency

For an upper semicontinuous loss, the Proposition 1 case $p=\infty$ asserts

$$\lim_{\rho\downarrow0}R_{P_n,\infty}(\rho;f)=0=R_{P_n,\infty}(0;f).$$

It is a companion statement: it says that the regularizer vanishes, while the main target says at which rate.

Local-slope regularization

The main target is Theorem 1(I), in its general-metric form from Appendix B under Assumption 5(I). If $\delta_0>0$, $M\ge0$, and the local growth obeys

$$|G_f(\delta,z)-\delta|\partial f|(z)| \le H(z)\delta^2+M(\delta-d(z,D_f))_+ \quad(0\le\delta<\delta_0),$$

then, for a sufficiently small radius, every nonempty empirical sample and every loss in the class satisfy

$$\left|R_{P_n,\infty}(\rho;f) -\rho\frac1n\sum_{i=1}^n|\partial f|(z_i)\right| \le\rho^2\frac1n\sum_{i=1}^n|H(z_i)| +M\frac1n\sum_{i=1}^n(\rho-d(z_i,D_f))_+.$$

The finite-support duality and the identity between the empirical regularizer and the average of $G_f(\rho,z_i)$ are the mission's intermediate targets. The printed $\rho_n^2$ in Lemma EC.9 is read as $\rho^2$, as in Theorem 1(I).

Significance

The estimate gives a precise first-order description of infinity-Wasserstein robustness: the mean local slope is its leading regularization term. The quadratic term measures local curvature or growth, while the boundary term records the effect of sample points close to interfaces between loss pieces. Setting $M=0$ gives the smooth-loss regime, where that interface correction vanishes. The result makes it possible to compare bounded data perturbations with explicit variation penalties using the same loss class and sample.

The paper proves the result. The formalization work here is to express its objects and quantified conditions in Lean, establish finite-support duality for the extended-real robust value, and then formalize the known local estimate. No machine-checked proof of these mission targets is claimed here. The transport and duality definitions can support other finite-support distributionally robust models; the local-slope definitions can be reused for other metric-space perturbation bounds.

Difficulty

The robust value is a supremum over probability laws, whereas the target bound is a finite average of pointwise quantities. Relating the two requires control of the infinity-Wasserstein constraint at every nominal atom, including cases where an infimum over couplings must be attained. A direct substitution of a pointwise supremum into an expectation does not establish the reverse inequality, and extended-real values need care when a loss is unbounded. At the local level, a slope is only a limit near a point; the inequality needed here holds uniformly for all losses, all points, and all sufficiently small radii, with a correction near $D_f$.

Formalization scope

The Lean metric space uses its Borel measurable structure and is second countable, so the distance on the product is measurable. It has no isolated points, matching §3.4. Losses in the class are measurable. Sample indices are Fin n with $n>0$, and $P_n$ is the published empirical probability law. Infinity-Wasserstein distance takes values in $[0,+\infty]$; robust values and local growth use extended reals. The theorem explicitly requires finite local slopes and finite growth values in the range where Assumption 5(I)'s real inequality is used. The regularizer is built from the supremum over all probability laws in the Wasserstein ball, and its finite-sample result states finiteness before converting its value to a real number. This rules out replacing the regularizer by the easier average of local growth.

The paper defines $D_f$ from intersections of closures of pieces and assumes it is null under a true law. The deterministic estimate uses only distances to $D_f$, so this mission treats $D_f$ as supplied data and does not require nullity. Likewise, $H\in L^1(P_{\rm true})$ is needed for the paper's statistical setting but the target evaluates $H$ only at finite sample points, so no true law appears in this statement. The radius bound is placed before the sample because Assumption 5(I) supplies one common $\delta_0$. These generalizations and the positive-radius reading of Assumption 5(I) are explicit in the item statements. Contributions toward the optimal-coupling lemma, extended-real finite-support duality, and the local estimate all advance the target.

Selected references

• R. Gao and A. J. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research, 2023; arXiv:1604.02199. Source of the duality theory for finite $p$ that Lemma EC.1 quotes.
• R. Gao, X. Chen and A. J. Kleywegt, Wasserstein Distributionally Robust Optimization and Variation Regularization, Operations Research, 2024; arXiv:1712.06050, source preprint dated 2020-10-30, especially Theorem 1(I), Assumption 5(I), Lemmas EC.2 and EC.9.

Motivation

Markov chain Monte Carlo methods approximate a target probability measure by the law after $n$ steps of a Markov chain. A quantitative guarantee for such a method is a bound on the distance between the law after $n$ steps and the target, or between the laws of two copies of the chain started from different initial distributions. A standard route to such bounds is contractivity in a Kantorovich (Wasserstein) distance: if one step of the chain contracts the distance between any two initial laws by a factor $e^{-c}<1$, the laws converge geometrically.

For many chains of practical interest, including Hamiltonian Monte Carlo with a numerical integrator, contractivity can only be proved on a bounded region of the state space. Outside it, the integrator may be unstable, or the coupling used to prove contraction may fail. Bou-Rabee, Eberle and Zimmer (arXiv:1805.00452, Ann. Appl. Probab. 30(3), 2020) isolate a general principle that turns such local contractivity into a global distance bound. It requires two Lyapunov functions: one controls how quickly the chain can leave the region of contraction, and one controls the distance once it has left. The principle is their Theorem 2.11. It is stated for an arbitrary Markov kernel on a complete separable metric space, and they apply it to adjusted numerical HMC (their Theorem 2.12).

Setting

Let $(S,\rho)$ be a complete separable metric space with Borel $\sigma$-algebra $\mathcal B(S)$, and let $\pi(x,dy)$ be a Markov transition kernel on $S$. For a probability measure $\nu$, the law after $n$ steps is $\nu\pi^n$, where $\pi^0(x,\cdot)=\delta_x$ and $\pi^{n+1}=\pi\pi^n$. For a non-negative function $f$, $(\pi f)(x)=\int f(y)\,\pi(x,dy)$.

A coupling of probability measures $\nu,\eta$ on $S$ is a probability measure on $S\times S$ with marginals $\nu$ and $\eta$; $C(\nu,\eta)$ is the set of couplings. The Kantorovich distance is

$$\mathcal W_\rho(\nu,\eta)=\inf_{\gamma\in C(\nu,\eta)}\int\rho(x,y)\,\gamma(dx\,dy)\in[0,\infty].$$

Assumption 2.3 asks for a constant $C\in(0,\infty)$ and measurable functions $\psi,\varphi:S\to(0,\infty)$ such that:

• (C1) main Lyapunov condition: for some $\lambda\in[1,\infty)$, $(\pi\psi)(x)\le\lambda\psi(x)$ whenever $\psi(x)\le C$;
• (C2) global Lyapunov condition: for some $\beta\in[1,\infty)$, $(\pi\varphi)(x)\le\beta\varphi(x)$ and $\rho(x,y)\le\varphi(x)+\varphi(y)$ for all $x,y$;
• (C3) local contractivity: there are a probability space $(\Omega,\mathcal A,P)$, a constant $c\in(0,\infty)$ and a measurable map $(X',Y'):S\times S\times\Omega\to S\times S$. For every $x,y$, the pair $(X'(x,y,\cdot),Y'(x,y,\cdot))$ is a coupling of $\pi(x,\cdot)$ and $\pi(y,\cdot)$, and $E[\rho(X'(x,y,\cdot),Y'(x,y,\cdot))]\le e^{-c}\rho(x,y)$ whenever $\psi(x)\le C$ and $\psi(y)\le C$.

Finally,

$$\delta(C)=\sup\Big\{\frac{\varphi(x)+\varphi(y)}{\psi(x)+\psi(y)}:x,y\in S,\ \psi(x)>C\text{ or }\psi(y)>C\Big\}\in[0,\infty].$$

Formalization targets

Goal: Theorem 2.11

Under Assumption 2.3, for every $n\in\mathbb N$ and all probability measures $\nu,\eta$ on $(S,\mathcal B(S))$,

$$\mathcal W_\rho(\nu\pi^n,\eta\pi^n)\le e^{-cn}\mathcal W_\rho(\nu,\eta)+\beta^n\lambda^{n-1}\Big(\int\psi\,d\nu+\int\psi\,d\eta\Big)\delta(C).\tag{42}$$

The constants are those of the paper and are not weakened. Each quantity may be infinite, and the bound is read in $[0,\infty]$.

Milestones

1. Lemma 6.1. If a measurable coupling contracts $\rho$ by $e^{-c}$ in one step from every pair in $A\times A$, then for every initial coupling $\gamma$ there is a coupled Markov chain $(X_n,Y_n)$ with $(X_0,Y_0)\sim\gamma$ and both marginals Markov with kernel $\pi$. Along this chain, $M_n=e^{c(n\wedge T)}\rho(X_{n\wedge T},Y_{n\wedge T})$ is a non-negative supermartingale, where $T$ is the exit time from $A\times A$.
2. (134). $e^{cn}E[\rho(X_n,Y_n);n\le T]\le E[M_n]\le\int\rho\,d\gamma$.
3. (135). $E[\rho(X_n,Y_n);n>T]\le\beta^nE[\psi(X_T)+\psi(Y_T);n>T]\,\delta(C)$, through the intermediate bounds by $\varphi$.
4. (136). $E[\psi(X_T)+\psi(Y_T);n>T]\le\lambda^{n-1}\big(\int\psi\,d\nu+\int\psi\,d\eta\big)$.

Significance

The result. Theorem 2.11 separates two tasks that are usually entangled in convergence proofs for Markov chains on unbounded spaces. One is a contraction estimate that only has to hold on a sublevel set $\{\psi\le C\}$. The other is a pair of drift conditions that control excursions out of that set. The second term of (42) is made small by choosing $C$ large, and the first by choosing $n$ large. In the paper this gives $\mathcal W^1$ bounds to the invariant measure for adjusted numerical HMC (Theorem 2.12), whose contraction (Theorems 2.4 and 2.7) is only established on a ball. The theorem uses nothing about HMC and applies to any chain with a locally contractive coupling and the two Lyapunov conditions. Examples are other discretized diffusions and Metropolis-adjusted samplers.

Formalizing it. The result is proved in the paper. As far as is known, it has no machine-checked proof. A formalization requires constructing a Markovian coupling on a general measurable space and working with a generalized, $[0,\infty]$-valued supermartingale stopped at an exit time. It also needs the Markov property with respect to the joint filtration of a coupled pair. Both pieces are reusable in coupling arguments for Markov chains in general.

Difficulty

Contraction on $\{\psi\le C\}^2$ gives no control once either copy leaves that set, and the exit time $T$ is random and may be infinite. The bound therefore has to be split at $T$. On $\{n\le T\}$ the contraction accumulates, which requires optional stopping for a supermartingale that need not be integrable, because $\int\rho\,d\gamma$ may be $+\infty$. On $\{n>T\}$ the distance at time $n$ has to be bounded by quantities at the random time $T$. This requires the Markov property of each copy with respect to the filtration of the pair: the event $\{T=k\}$ depends on both copies. A Markov property of each copy in its own filtration does not suffice. Finally, $\psi$ at the exit time has to be controlled by its initial integral, which is a second stopped supermartingale built from (C1).

Formalization scope

• $(S,\rho)$ is a Lean MetricSpace with its Borel $\sigma$-algebra, complete and separable; $\rho$ is dist. $\pi$ is a Markov kernel (Kernel S S with IsMarkovKernel), and $\nu\pi^n$ is the bind of $\nu$ with the $n$-fold composition of $\pi$.
• Every expectation of a non-negative quantity, every $\int\psi\,d\nu$, $\delta(C)$ and $\mathcal W_\rho$ is valued in $[0,\infty]$ (lower Lebesgue integrals, ℝ≥0∞). No Bochner integral appears, so a non-integrable quantity can never be replaced by a junk $0$. In particular, $\int\psi\,d\nu=\infty$ is allowed, as on the page.
• Couplings are the published definition MongeKantorovichYao.transferencePlans.
• (C3)'s probability space and coupling map are parameters of the theorem, which then holds for every such realization.
• $\lambda^{n-1}$ is an integer power, so $n=0$ is included (and (42) is then trivially true).
• Lemma 6.1's chain is the coordinate process on the path space $(S\times S)^{\mathbb N}$, which is determined up to its law. The supermartingale property is the generalized one, $E[M_{n+1};F]\le E[M_n;F]$ for $F\in\mathcal F_n$. Mathlib's Supermartingale requires integrability, which the page does not assume. The exit time is $\mathbb N\cup\{\infty\}$-valued, and $n\wedge T=n$ when the chain never leaves.
• The marginal Markov property is stated with respect to the filtration of the pair. This is what the proof of (135) and (136) uses, and it implies the marginal Markov property in each copy's own filtration.
• The proof on p. 43 applies Lemma 6.1 "with $A=\{\psi>C\}$". The set on which (C3) contracts and whose exit time is $T$ is $\{\psi\le C\}$, and that set is used. The text before (135) says "$\{n<T\}$" where its displays use $\{n>T\}$, and the displays are formalized.
• A formalization in which $\mathcal W_\rho$ or $\delta(C)$ is a real number obtained by truncating $+\infty$, or in which the measures need not be probability measures (so that the coupling set is empty and $\mathcal W_\rho=\infty$), would make (42) vacuous and is excluded.

A complete development needs Ionescu-Tulcea's construction of a Markov chain on a general measurable space (ProbabilityTheory.Kernel.traj in Mathlib), the measurability of the coupling kernel $(x,y)\mapsto P\circ(X',Y')(x,y,\cdot)^{-1}$, and optional stopping for $[0,\infty]$-valued supermartingales stopped at an exit time. Contributions are welcome on the milestones individually. The optional-stopping and joint-Markov-property lemmas are reusable beyond this mission.

Selected references

• N. Bou-Rabee, A. Eberle, R. Zimmer, Coupling and convergence for Hamiltonian Monte Carlo, Ann. Appl. Probab. 30(3), 2020. arXiv:1805.00452 (v2 is the version cited here).
• A. Joulin, Y. Ollivier, Curvature, concentration and error estimates for Markov chain Monte Carlo, Ann. Probab. 38(6), 2010. doi:10.1214/10-AOP541
• C. Villani, Optimal Transport: Old and New, Springer, 2009. doi:10.1007/978-3-540-71050-9