Optimal Transport

The Monge optimal transport problem on the real line with the classical distance cost $|x-y|$ famously fails to have a unique solution. Juillet (2019) restored uniqueness by considering the strictly concave power costs $|x-y|^p$ with $p<1$ and letting $p\to 1^-$: the limit selects a distinguished optimal plan, the excursion coupling, built from the level sets of the difference $F_\sigma=F_\mu-F_\nu$ of the cumulative distribution functions. This mission formalizes the completed-graph construction, the generalized Banach indicatrix identities of Bertoin-Yor, the alternating crossing structure of almost every level, and the marginal identities for the crossing counting measures. It culminates in Propositions 3.5-3.6: every monotone transport plan is concentrated on the paired routes, and the marginals uniquely determine the coupling carried by those routes, including in the presence of atoms.

This mission formalizes the key implication 3=>4 in Juillet's Main Theorem.

Motivation

Optimal transport asks for the cheapest way to move one distribution of mass onto another. Monge posed the problem in 1781 for maps; Kantorovich (1942) relaxed it to transference plans (couplings), turning it into an infinite-dimensional linear program with a dual: maximize the total revenue $\int\psi\,d\mu+\int\varphi\,d\nu$ of pickup and delivery prices that never exceed the cost, $\psi(x)+\varphi(y)\le c(x,y)$. The equality of the two values — Monge–Kantorovich duality — underlies much of modern optimal transport, with uses in economics (matching markets, principal–agent problems), probability, and PDE.

This mission formalizes the duality theorem and its proof as presented in Colin Yao, Monge–Kantorovich and Transportation Theory (paper dated September 10, 2023), whose proof follows Villani's Optimal Transport: Old and New and, for the weak inequality, Galichon's Optimal Transport Methods in Economics.

Setting

$X$ and $Y$ are Polish spaces (separable, completely metrizable) with their Borel σ-algebras; $\mu$ and $\nu$ are Borel probability measures on $X$ and $Y$; $c : X\times Y\to[0,\infty)$ is a continuous cost function.

• A transference plan is a probability measure $\pi$ on $X\times Y$ with marginals $\mu$ and $\nu$; $\Pi(\mu,\nu)$ denotes the set of such plans.
• The Kantorovich problem is $\min_{\pi\in\Pi(\mu,\nu)}\int c\,d\pi$.
• The dual problem is $\sup\{\int\psi\,d\mu+\int\varphi\,d\nu\}$ over bounded continuous $\psi,\varphi$ with $\psi(x)+\varphi(y)\le c(x,y)$ everywhere.
• A set $\Gamma\subseteq X\times Y$ is $c$-cyclically monotone if $\sum_{i=1}^N c(x_i,y_i)\le\sum_{i=1}^N c(x_i,y_{i+1})$ (with $y_{N+1}=y_1$) for all finite families of points of $\Gamma$; a plan is $c$-cyclically monotone if it is concentrated on such a set.
• The $c$-conjugate of $\psi$ is $\psi^c(y)=\inf_x(c(x,y)-\psi(x))$; $\psi$ is $c$-concave if $\psi(x)=\inf_y(c(x,y)-\varphi(y))$ for some $\varphi$; its $c$-subdifferential is $\partial_c\psi=\{(x,y):\psi^c(y)+\psi(x)=c(x,y)\}$.

Formalization targets

Goal (Theorem 4.1)

$$\min_{\pi\in\Pi(\mu,\nu)}\int_{X\times Y}c\,d\pi=\sup_{\substack{\psi\in C_b(X),\ \varphi\in C_b(Y)\\ \psi(x)+\varphi(y)\le c(x,y)}}\Big(\int_X\psi\,d\mu+\int_Y\varphi\,d\nu\Big),$$

including existence of a minimizing plan; the common value may be $+\infty$.

Milestones (in the order of the source)

1. Weak duality, inequality (3.1): $\inf\ge\sup$.
2. Proposition 4.4: a $c$-cyclically monotone plan exists between uniform empirical measures.
3. Lemma 4.16: plans with marginals in tight families form a tight family.
4. Proposition 4.17: a $c$-cyclically monotone plan exists for general marginals.
5. Proposition 4.22: the support of a $c$-cyclically monotone plan lies in $\partial_c\psi$ for a $c$-concave $\psi$ (bounded $c$).
6. Theorem 4.25: $(\psi^c)^c=\psi$ for $c$-concave $\psi$.
7. Proposition 4.31: duality for bounded continuous $c$.
8. Theorem 4.32: $\int f\,d\mu=\int f\,d\pi$ for a plan with marginal $\mu$.

Significance

Duality converts a minimization over measures into a maximization over functions; it characterizes optimal plans by the complementary-slackness condition that they are concentrated on $\{\psi(x)+\varphi(y)=c(x,y)\}$, and it is the entry point to Brenier's theorem, the Kantorovich–Rubinstein formula for the Wasserstein-1 distance, and the economic applications discussed in Section 5 of the source. The result is classical and proved in the literature; the work here is to formalize the known proof and to supply reusable infrastructure (couplings, $c$-cyclical monotonicity, $c$-transforms) on top of Mathlib's measure theory.

Difficulty

The weak inequality is a short integration argument; the reverse inequality is where the work lies. Finite-dimensional linear-programming duality does not pass to general measures directly: one must produce a cyclically monotone plan as a limit of discrete approximations (tightness and Prokhorov's theorem, closedness of the cyclic-monotonicity condition under weak convergence), build a potential $\psi$ from chains of cost differences, and control measurability and integrability of $\psi$ and $\psi^c$. Passing from bounded to unbounded nonnegative costs requires an additional approximation argument, which the source only sketches (Section 4.5).

Formalization scope

Lean namespace MongeKantorovichYao; one definition file provides transference plans, $c$-cyclical monotonicity, $c$-conjugates, $c$-concavity and $c$-subdifferentials. Conventions: marginals are pushforwards along the projections; $c$-conjugates are extended-real infima (no default values); the transport cost in the goal is the $[0,\infty]$-valued integral of the nonnegative cost, and both sides of the goal are compared in the extended reals, so the infinite-cost case is included and no integrability hypothesis is added. The dual side ranges over bounded continuous functions with the constraint imposed at every point. Proposition 4.22 is stated for bounded $c$ (as used in Proposition 4.31), since with unbounded costs a real-valued potential need not exist. Infrastructure that may be missing from Mathlib: Prokhorov-type compactness of tight families of probability measures, weak convergence of empirical measures, and lower semicontinuity of $\pi\mapsto\int c\,d\pi$.

Selected references

• C. Villani, Optimal Transport: Old and New, Grundlehren der mathematischen Wissenschaften 338, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
• A. Galichon, Optimal Transport Methods in Economics, Princeton University Press, 2016.
• L. V. Kantorovich, On the translocation of masses, Dokl. Akad. Nauk SSSR 37 (1942).

Why reduce scenarios

Multistage and two-stage stochastic programs are solved numerically on a discrete probability distribution: a finite set of scenarios $\omega_1,\dots,\omega_N$ with probabilities $p_1,\dots,p_N$. The size of the resulting optimization problem grows with $N$, and scenario sets produced by sampling or by historical data are often far too large to be solved directly. Scenario reduction replaces the original distribution by one supported on a small subset of the scenarios, chosen so that the optimal value and solutions of the stochastic program change as little as possible.

Stability theory for stochastic programs (Rachev and Römisch, 2002) shows that this change is controlled by a probability distance of Fortet–Mourier type, which for discrete measures is bounded by the value of a transportation problem. Dupačová, Gröwe-Kuska and Römisch (2003) turned this into a combinatorial problem and proposed greedy backward and forward heuristics. Heitsch and Römisch (2003) gave faster versions of both heuristics; the forward version, fast forward selection, is the subject of this mission. Implementations of these reduction heuristics are distributed with the GAMS modelling system (SCENRED) and are used in energy and finance applications of stochastic programming.

Setting

Let $E$ be a finite-dimensional real vector space with a norm $\|\cdot\|$, let $\omega_0\in E$, and let $h:[0,\infty)\to[0,\infty)$ be continuous and nondecreasing with $h(0)=0$. The cost between two points of $E$ is

$$c(\omega,\tilde\omega)=\max\bigl\{1,\,h(\|\omega-\omega_0\|),\,h(\|\tilde\omega-\omega_0\|)\bigr\}\,\|\omega-\tilde\omega\| .$$

It is nonnegative, symmetric, and zero on the diagonal.

The original distribution is $P=\sum_{i=1}^N p_i\delta_{\omega_i}$ with $p_i>0$ and $\sum_i p_i=1$. Deleting the scenarios in a set $J\subset\{1,\dots,N\}$ and assigning new weights $q_j\ge 0$, $\sum_{j\notin J}q_j=1$, to the kept ones gives $Q=\sum_{j\notin J}q_j\delta_{\omega_j}$. The distance $D(J;q)$ between $P$ and $Q$ is the optimal value of the transportation problem

$$D(J;q)=\min\Bigl\{\sum_{i=1}^N\sum_{j\notin J}c(\omega_i,\omega_j)\eta_{ij}:\ \eta_{ij}\ge 0,\ \sum_{i}\eta_{ij}=q_j,\ \sum_{j\notin J}\eta_{ij}=p_i\Bigr\}.$$

The reduction cost of deleting $J$ is

$$D_J=\sum_{i\in J}p_i\min_{j\notin J}c(\omega_i,\omega_j),$$

and the optimal reduction problem (8) minimizes $D_J$ over all $J$ with $\#J=N-n$, where $n$ is the number of scenarios to keep.

Forward selection builds the kept set greedily. With $J^{[0]}=\{1,\dots,N\}$ and $J^{[i]}=\{1,\dots,N\}\setminus\{u_1,\dots,u_i\}$, it chooses

$$u_i\in\arg\min_{u\in J^{[i-1]}}D_{J^{[i-1]}\setminus\{u\}},\qquad i=1,\dots,n. \tag{16}$$

Fast forward selection (Algorithm 2.4) computes the same choices through an updated cost matrix: $c^{[1]}_{ku}=c(\omega_k,\omega_u)$, $c^{[i]}_{ku}=\min\{c^{[i-1]}_{ku},c^{[i-1]}_{ku_{i-1}}\}$, $z^{[i]}_u=\sum_{k\in J^{[i-1]}\setminus\{u\}}p_kc^{[i]}_{ku}$, and $u_i\in\arg\min_{u\in J^{[i-1]}}z^{[i]}_u$.

Formalization targets

Goal: Theorem 2.5

For $1\le n\le N$ and every run $u_1,\dots,u_n$ of Algorithm 2.4, with any tie-breaking in the arg min,

$$u_i\ \text{satisfies (16)}\quad\text{and}\quad z^{[i]}_{u_i}=D_{J^{[i]}}\qquad(i=1,\dots,n).$$

Milestones

1. Theorem 2.1 (redistribution). For $J$ with at least one kept scenario, $D_J=\min_q D(J;q)$, and the minimum is attained at $\bar q_j=p_j+\sum_{i\in J,\,j(i)=j}p_i$ for every choice of nearest kept scenarios $j(i)$.
2. Eq. (10). $D_{\{1,\dots,N\}\setminus\{u\}}=\sum_{i=1}^Np_ic(\omega_i,\omega_u)$, so (8) with $\#J=N-1$ is problem (10).
3. Eq. (12). The sum $lb$ of the $N-n$ smallest single-deletion costs $p_l\min_{j\neq l}c(\omega_l,\omega_j)$, taken in the greedy order (11), is at most $D_J$ for every $J$ with $\#J=N-n$.
4. Optimality condition (p. 191). If each $l_i$ has a nearest other scenario outside $\{l_1,\dots,l_{N-n}\}\setminus\{l_i\}$, then $\{l_1,\dots,l_{N-n}\}$ solves (8).
5. Eq. (17), unrolled recursion. For any index sequence, $c^{[i]}_{ku}=\min_{j\notin J^{[i-1]}\setminus\{u\}}c(\omega_k,\omega_j)$ for $u\in J^{[i-1]}$.
6. Eq. (17), conclusion. For any index sequence, $z^{[i]}_u=D_{J^{[i-1]}\setminus\{u\}}$ for $u\in J^{[i-1]}$.

Significance

Theorem 2.5 certifies that the cheap update of Algorithm 2.4 (one pairwise minimum per matrix entry and step) produces exactly the greedy forward selection defined through the reduction costs, and that the running objective $z^{[i]}_{u_i}$ is the reduction cost of the scenarios deleted so far. Combined with Theorem 2.1, $z^{[i]}_{u_i}$ is the optimal transportation distance between $P$ and the best measure on the kept scenarios, which is the quantity practitioners monitor to decide how many scenarios to keep. The lower bound (12) and the optimality condition give a posteriori quality certificates for any reduced set.

All results of this mission are proved in the paper or in the works it cites (Dupačová et al., 2003); none is open. To the best of a platform search, none has been machine-checked. The mission provides a verified specification of a widely deployed algorithm, a formal link between a combinatorial set-covering objective and a finite transportation problem, and definitions (reduction cost, transportation plans with a partially free target marginal, greedy runs with arbitrary tie-breaking) reusable by the regular-tree missions of this series and by later scenario-tree construction papers.

Difficulty

The mathematics is elementary; the difficulty is bookkeeping. The recursion for $c^{[i]}$ refers to the previous step's column $u_{i-1}$, which itself was updated, so unrolling it to a minimum over $\{u,u_1,\dots,u_{i-1}\}$ is an induction on $i$ in which the index sets $J^{[i]}$, the 1-based step counter and the complement structure all move together. The natural first attempt, identifying $c^{[i]}_{ku}$ with the minimum over the complement of $J^{[i]}$, is off by one step: the correct set is the complement of $J^{[i-1]}\setminus\{u\}$, which contains $u$ itself. For Theorem 2.1 the lower bound requires using that $c(\omega_i,\omega_i)=0$ for kept scenarios and that every plan ships all of $p_i$ somewhere outside $J$; the attainment part requires constructing the plan explicitly from the choice $j(\cdot)$, including scenarios for which several kept scenarios are equally near.

Formalization scope

• Scenarios are ω : Fin N → E with E a finite-dimensional real normed space; the paper's closed set $\Omega\subset\mathbb R^s$ plays no role beyond containing the scenarios and is omitted. Scenarios need not be distinct.
• $h$ is a function ℝ → ℝ with the paper's assumptions imposed on $[0,\infty)$ (IsGrowthFunction); every theorem carries them, together with $p_i>0$ and $\sum_ip_i=1$.
• The functions $f_0$, $g$ and the stochastic program (1)–(2) that motivate $c$ appear in no statement.
• $D(J;q)$ is the paper's finite transportation problem (p. 188), not the Kantorovich functional on measures. Weights $q$ and plans $\eta$ are indexed by all of $\{1,\dots,N\}$ with entries at deleted indices fixed to $0$.
• $D_J$ requires a proof that the complement of $J$ is nonempty; minima are Finset.inf', never a real infimum with a default value.
• Algorithm 2.4 is a relation on sequences u : ℕ → Fin N with 1-based steps. $c^{[i]}$ is the printed recursion, extended to all indices; runs are any sequences satisfying the arg-min conditions, so every tie-breaking rule is covered.
• The paper's standing restriction $n<N$ is relaxed to $n\le N$ in Theorem 2.5; the statement remains true at $n=N$.
• A trivializing formalization is ruled out: defining $c^{[i]}$ or $z^{[i]}$ directly as the minimum over the selected set or as $D_{J^{[i-1]}\setminus\{u\}}$ would make Theorem 2.5 hold by definition, and proving it for one fixed tie-breaking rule would prove less than the paper; neither is done.
• Proofs of the milestones, alternative proofs of Theorem 2.1 via LP duality, and a verified executable implementation of Algorithm 2.4 are all welcome.

Selected references

• H. Heitsch, W. Römisch, Scenario Reduction Algorithms in Stochastic Programming, Computational Optimization and Applications 24 (2003), 187–206. https://doi.org/10.1023/A:1021805924152
• J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: an approach using probability metrics, Mathematical Programming 95 (2003), 493–511. https://doi.org/10.1007/s10107-002-0331-0
• S. T. Rachev, W. Römisch, Quantitative stability in stochastic programming: the method of probability metrics, Mathematics of Operations Research 27 (2002), 792–818. https://doi.org/10.1287/moor.27.4.792.304

Motivation

Stochastic programs are solved in practice on a finite set of scenarios: a discrete probability distribution $P=\sum_{i=1}^N p_i\delta_{\omega_i}$ that approximates the true distribution of the uncertain data. The size of the resulting deterministic problem grows with $N$, and for multistage models it grows very fast, so $N$ is often reduced before solving. The question is which scenarios to delete and how to reweight the remaining ones so that the optimal value and solutions of the stochastic program change as little as possible.

Dupačová, Gröwe-Kuska and Römisch (Math. Program. Ser. A 95 (2003) 493–511) answered this with probability metrics. Stability results for stochastic programs bound the change of the optimal value by a Fortet–Mourier type distance, which is in turn bounded by a Kantorovich functional $\hat\mu_c$ (an optimal transport cost). Scenario reduction then becomes: find a measure $Q$ supported on a subset of the scenarios with $\hat\mu_c(P,Q)$ small. Section 3 of the paper solves the weight part of this problem in closed form. That result, together with the heuristics built on it (backward reduction and forward selection), became the standard scenario-reduction method, implemented for example in the GAMS tool SCENRED.

Setting

Let $\Omega$ be a set and $c:\Omega\times\Omega\to\mathbb R_+$ a cost function with $c(\omega,\tilde\omega)=0$ if and only if $\omega=\tilde\omega$, and $c(\omega,\tilde\omega)=c(\tilde\omega,\omega)$ (conditions (C1)–(C2), p. 498). The original distribution has scenarios $\omega_1,\dots,\omega_N\in\Omega$ with weights $p_i>0$ and $\sum_i p_i=1$. Write $c_{ij}=c(\omega_i,\omega_j)$.

A set $J\subset\{1,\dots,N\}$ of scenarios is deleted. The reduced measure is $Q=\sum_{j\notin J}q_j\delta_{\omega_j}$ with reduced weights $q_j\ge0$, $\sum_{j\notin J}q_j=1$. A transport plan from $P$ to $Q$ is a nonnegative matrix $(\eta_{ij})_{i\le N,\,j\notin J}$ with row sums $\sum_{j\notin J}\eta_{ij}=p_i$ and column sums $\sum_i\eta_{ij}=q_j$. The Kantorovich functional (10) is the value of this transportation problem,

$$D(J;q)=\min\Big\{\sum_{i}\sum_{j\notin J}c_{ij}\eta_{ij}:\ \eta\ \text{a transport plan from }P\text{ to }Q\Big\},$$

and $D_J=\min\{D(J;q): q\ \text{reduced weights}\}$ is the best distance achievable once $J$ is fixed. The optimal deletion problem (13) asks for $\min\{D_J:\#J=k\}$ for a given $1\le k<N$.

In the Lean development these objects are IsReducedWeight, IsTransportPlan, transportCost, transportValue ($D(J;q)$), optWeightsValue ($D_J$) and optimalDeletionValue (the value of (13)), all in the namespace ScenarioReduction.Redistribution.

Formalization targets

Goal: Theorem 2 (optimal weights), p. 500

For every $J\neq\{1,\dots,N\}$,

$$D_J=\min\Big\{D(J;q): q_j\ge0,\ \sum_{j\notin J}q_j=1\Big\}=\sum_{i\in J}p_i\min_{j\notin J}c(\omega_i,\omega_j),$$

and the minimum is attained at the optimal redistribution rule $\bar q_j=p_j+\sum_{i\in J_j}p_i$, where $J_j=\{i\in J: j(i)=j\}$ and $j(i)\in\arg\min_{j\notin J}c(\omega_i,\omega_j)$, for every such choice of $j(\cdot)$.

Milestones

1. Primal–dual representation of $D(J;q)$ (first display of the proof, p. 501): the transportation problem and its linear-programming dual both attain $D(J;q)$.
2. Lower bound (p. 501): $\sum_{i\in J}p_i\min_{k\notin J}c_{ik}\le D(J;q)$ for every feasible $q$.
3. Upper bound at $\bar q$ (p. 501): $\bar q$ is feasible and $D(J;\bar q)\le\sum_{i\in J}p_i\min_{j\notin J}c_{ij}$.
4. Theorem 3 (p. 501): for weights prescribed by $q_j=p_j+\lambda_jp_J$, $D(J;q)\le\sum_{i\in J}p_i\sum_{j\notin J}\lambda_jc(\omega_i,\omega_j)$, with equality if $\#J=1$ and $c$ satisfies the triangle inequality.
5. Theorem 4 (p. 503): the greedy recursions (16) and (17) give a lower and an upper bound for $\min\{D_J:\#J=k\}$, and the backward set $\{l_1,\dots,l_k\}$ is optimal under a nonemptiness condition.

Significance

Theorem 2 reduces the continuous part of scenario reduction to a formula: once the set of kept scenarios is chosen, the best reweighting is to move the mass of every deleted scenario to a nearest kept scenario, and the resulting distance is an explicit sum. This leaves only the combinatorial choice of $J$, which Theorem 4 brackets by two greedy procedures; these are the backward-reduction and forward-selection algorithms of the paper and of later work by Heitsch and Römisch. Theorem 3 covers the case in which the reduced weights are fixed by the modeller, for instance to keep a uniform distribution uniform.

The results are proved in the paper by elementary linear-programming arguments. As far as is known, none of them has a machine-checked proof. Formalizing them produces a verified finite transportation-problem layer with a general (not necessarily metric) cost and a deleted index set, and verified correctness certificates for the two standard scenario-reduction heuristics.

Difficulty

The upper bound of Theorem 2 is a direct construction. The content lies in the lower bound, which must hold for every reweighting $q$ simultaneously; this needs the dual side of the transportation problem, and the full primal–dual representation (Milestone 1) requires strong duality for a transportation problem with only the kept columns, which Mathlib does not provide in this form. A naive argument that bounds each plan row by row gives the lower bound directly for plans, but relating it to $D(J;q)$ as an infimum also requires that plans exist and that the infimum is attained. In Theorem 4, the recursions (16) and (17) are greedy and do not in general produce optimal sets; the lower bound works only because its inner minimum ranges over all $j\neq l$, not over the kept scenarios.

Formalization scope

Scenarios are indexed by Fin N (0-based), scenarios are a function ω : Fin N → Ω into an arbitrary type Ω, the cost is c : Ω → Ω → ℝ, and weights, plans and dual variables are real-valued functions on Fin N and Fin N × Fin N. Only the entries at kept indices $j\notin J$ enter any constraint, cost or objective. No measure theory is used: the index-level transportation problem is the paper's own representation of $\hat\mu_c$ for discrete measures (p. 495). Every theorem carries the standing assumptions of Section 3: $c\ge0$, (C1), (C2), $p_i>0$ and $\sum_ip_i=1$. Measurability of $c$ and conditions (C3) and (C4) concern $\Omega\subset\mathbb R^s$ and play no role for finitely supported measures; they are dropped, so the statements are more general than the page. The hypothesis $J\neq\{1,\dots,N\}$, implicit in Theorem 2, is stated explicitly; in Theorem 4, $1\le k<N$ plays this role.

$D(J;q)$ and $D_J$ are real infima (sInf) of transport costs and are only asserted about where the underlying sets are nonempty and bounded below; "min" is stated as attainment (IsLeast), not as an equality of infima. $D(J;q)$ is defined as the transportation problem and is not defined by the closed form $\sum_{i\in J}p_i\min_{j\notin J}c_{ij}$; under that definition Theorem 2 would be trivial, and it is ruled out here. Likewise the reduced-weight constraint does not force $q=\bar q$.

Needed infrastructure: finite transportation problems with nonnegativity and marginal constraints, existence of optimal plans (compactness of the feasible polytope), and LP duality for transportation problems. The transportation-problem layer is reusable beyond this mission. Contributions welcome: proofs of the milestones, a general strong-duality result for finite transportation problems, and the examples of p. 502 (single scenario deletion, keeping one scenario).

Selected references

• J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: An approach using probability metrics, Math. Program. Ser. A 95 (2003) 493–511. https://doi.org/10.1007/s10107-002-0331-0
• S. T. Rachev, Probability Metrics and the Stability of Stochastic Models, Wiley, 1991.
• H. Heitsch, W. Römisch, Scenario reduction algorithms in stochastic programming, Comput. Optim. Appl. 24 (2003) 187–206. https://doi.org/10.1023/A:1021805924152
• W. Römisch, R. Schultz, Stability analysis for stochastic programs, Ann. Oper. Res. 30 (1991) 241–266. https://doi.org/10.1007/BF02204819

Motivation

A logistic regression model is fitted on finitely many samples, and the quantity a practitioner cares about is the misclassification risk of the fitted classifier on new data. Its empirical counterpart, the training error, is biased downwards, and classical generalization bounds give it an additive margin that depends on a complexity measure of the model class rather than on the data at hand.

Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) take a distributionally robust route. They surround the empirical distribution of the training data by a ball of distributions in the Wasserstein metric and, for a given weight vector, compute the largest and the smallest misclassification probability over that ball. Their Theorem 3 shows that both extremes are optimal values of explicit linear programs. Combined with a measure-concentration result for the empirical distribution in the Wasserstein metric (Fournier and Guillin, PTRF 2015), the two values bracket the true risk with a prescribed confidence. The same Wasserstein-ball construction underlies the data-driven optimization framework of Mohajerin Esfahani and Kuhn (Math. Program. 2018).

Setting

Let $V$ be the feature space $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and let labels take the values $y\in\{-1,+1\}$. The feature-label space is $\Xi = V\times\{-1,+1\}$ with points $\xi=(x,y)$. A weight vector $\beta$ acts on features by $x\mapsto\langle\beta,x\rangle$; its dual norm is $\|\beta\|_* = \sup_{\|x\|\le1}\langle\beta,x\rangle$.

Metric (Definition 2). For a weight $\kappa>0$,

$$d\big((x,y),(x',y')\big) = \|x-x'\| + \kappa\,|y-y'|/2 .$$

Changing a label costs $\kappa$; moving a feature costs its norm distance.

Wasserstein distance (Definition 1). For distributions $\mathbb Q,\mathbb P$ on $\Xi$, $W(\mathbb Q,\mathbb P)$ is the infimum of $\int d(\xi,\xi')\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ of $\mathbb Q$ and $\mathbb P$. The Wasserstein ball of radius $\varepsilon\ge0$ is $\mathbb B_\varepsilon(\mathbb P) = \{\mathbb Q : W(\mathbb Q,\mathbb P)\le\varepsilon\}$.

Data. Training samples $(\hat x_i,\hat y_i)$, $i=1,\dots,N$, define the empirical distribution $\hat{\mathbb P}_N = \frac1N\sum_{i=1}^N\delta_{(\hat x_i,\hat y_i)}$.

Classifier and risk. Logistic regression models $\operatorname{Prob}(y\mid x) = [1+\exp(-y\langle\beta,x\rangle)]^{-1}$ (eq. (1)). The classifier is $f_\beta(x)=+1$ if $\operatorname{Prob}(+1\mid x)>0.5$ and $-1$ otherwise, and its risk under the data-generating distribution $\mathbb P$ is $\mathfrak R(\beta) = \mathbb P[y\ne f_\beta(x)]$.

Worst- and best-case risks.

$$\mathfrak R_{\max}(\beta) = \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}\big],\qquad \mathfrak R_{\min}(\beta) = \inf_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}\big].$$

The worst case counts a nonpositive margin, the best case a strictly negative one.

The linear programs. For data $(\hat x_i,\hat y_i)$, a weight vector $\hat\beta$ and variables $\lambda\in\mathbb R$, $s,r,t\in\mathbb R^N$, program (10a) minimizes $\lambda\varepsilon + \frac1N\sum_i s_i$ subject to, for every $i$,

$$1 - r_i\hat y_i\langle\hat\beta,\hat x_i\rangle\le s_i,\quad 1 + t_i\hat y_i\langle\hat\beta,\hat x_i\rangle - \lambda\kappa\le s_i,\quad r_i\|\hat\beta\|_*\le\lambda,\quad t_i\|\hat\beta\|_*\le\lambda,\quad r_i,t_i,s_i\ge0 .$$

Program (10b) has the same objective and bounds, with the signs of the two margin terms exchanged.

Formalization targets

Goal: Theorem 3 (i)–(ii)

For every $\kappa>0$, $\varepsilon\ge0$, $N\ge1$, all samples and every weight vector $\hat\beta$, both programs attain their minima $v$ and $w$, and

$$\mathfrak R_{\max}(\hat\beta) = v,\qquad \mathfrak R_{\min}(\hat\beta) = 1-w .$$

The identities hold for each fixed $\hat\beta$, so they apply to any $\hat\beta$ computed from the data.

Milestone: Theorem 3(i) alone

$\mathfrak R_{\max}(\hat\beta)$ equals the minimum of (10a).

Milestones: the confidence clauses

If the training samples are i.i.d. from $\mathbb P$ and the radius is such that $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, then for any sample-dependent $\hat\beta$

$$\mathbb P^N\{\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-\eta,\qquad \mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\}\ge1-\eta,$$ $$\mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-2\eta .$$

Significance

The result. Theorem 3 replaces an optimization over an infinite-dimensional set of distributions by a linear program with $3N+1$ variables and $4N$ constraints plus sign constraints. That makes the worst- and best-case misclassification probabilities computable at the scale of the training set, for any norm on the features whose dual norm can be evaluated. With the confidence clauses, the two values are data-driven upper and lower confidence bounds on the out-of-sample risk of the classifier actually deployed, including one fitted on the same data.

Formalizing it. The paper states Theorem 3 without proof in the main text; the argument is deferred to a technical appendix. No part of it is machine-checked. A formal proof needs the evaluation of a worst-case probability of a closed set over a type-1 Wasserstein ball around a discrete distribution, and the analogous best-case probability of an open set. Both are reusable in any Wasserstein-robust treatment of chance constraints or classification error.

Difficulty

The objective $\mathbf 1_{\{y\langle\beta,x\rangle\le0\}}$ is neither continuous nor concave, so the duality theorems for Wasserstein balls stated for continuous or Lipschitz losses do not apply directly. Upper semicontinuity of the indicator of a closed set is what matters, and the strict inequality in $\mathfrak R_{\min}$ has to be handled as the complement of a closed set. The transport cost couples a norm on the features with a discrete label-flip cost, so a sample can reach the misclassification region either by moving its feature to the hyperplane $\langle\hat\beta,x\rangle=0$ or by flipping its label, and the two options interact through the shared budget $\varepsilon$. Distances to the hyperplane are measured in the given norm and produce the dual norm $\|\hat\beta\|_*$. The degenerate weight $\hat\beta=0$ (every point on the hyperplane) must come out correctly without any division by $\|\hat\beta\|_*$.

Formalization scope

The feature space is a finite-dimensional real normed space V with an arbitrary norm, standing for $(\mathbb R^n,\|\cdot\|)$; the Euclidean norm is not assumed. A weight vector is a continuous linear functional V →L[ℝ] ℝ, and $\|\hat\beta\|_*$ is its operator norm, which is exactly the dual norm. Labels are Bool with an explicit embedding $\text{true}\mapsto+1$, $\text{false}\mapsto-1$; the metric of Definition 2 is written literally. The Wasserstein distance is ℝ≥0∞-valued, probabilities and expectations of indicators are measure values in $[0,\infty]$, and suprema and infima range exactly over the probability measures in the ball. "min" in (10a)/(10b) is formalized as attainment (IsLeast) of the objective over the feasible set. Samples are indexed by Fin N with $N\ge1$.

The following choices differ from a literal reading of the page:

• The paper says the risk "can be expressed as" $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$. This fails on the hyperplane $\langle\beta,x\rangle=0$, where $f_\beta(x)=-1$ is correct for $y=-1$. The mission defines $\mathfrak R(\beta)=\mathbb P[y\ne f_\beta(x)]$ from (1) and includes the true statement $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}]\le\mathfrak R(\beta)\le\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$ as a helper item.
• The choice $\varepsilon=\varepsilon_N(\eta)$ of (8) and the measure-concentration theorem behind it (Theorem 2) are not formalized. The confidence clauses take their conclusion, $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, as a hypothesis, and "with probability $1-\eta$" is read as "with probability at least $1-\eta$". The printed level $1-2\eta$ is kept for the two-sided bound.

Swapping the strict and non-strict inequalities in $\mathfrak R_{\max}$ and $\mathfrak R_{\min}$, restricting the supremum to measures supported on the sample points, or replacing the ball by a set that excludes non-discrete distributions would each change the theorem. None of these is an acceptable reformulation of the goal.

Useful infrastructure: couplings of a discrete measure with an arbitrary one, the distance from a point to a closed half-space in a general norm, and LP-duality arguments for fractional-knapsack-type programs. Proofs of the helper and confidence items, and any reusable lemma about worst-case probabilities of closed sets over Wasserstein balls, are welcome.

Selected references

• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28 (NIPS 2015). https://papers.nips.cc/paper/2015/hash/cc1aa436277138f61cda703991069eaf-Abstract.html
• N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://doi.org/10.1007/s00440-014-0583-7
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018). https://doi.org/10.1007/s10107-017-1172-1

Motivation

Logistic regression is among the most widely used classification methods in statistics and machine learning. Its maximum-likelihood estimator minimizes the average logloss on the training data and is known to overfit when data are scarce; practitioners respond with ad hoc regularization, typically a norm penalty on the weight vector. Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015, arXiv:1509.09259) replace the empirical average by a worst case over all distributions within a Wasserstein ball around the empirical distribution. The resulting model has a finite convex reformulation, contains classical and norm-regularized logistic regression as special cases, and comes with out-of-sample guarantees. It is one of the early instances of Wasserstein distributionally robust optimization in learning, building on the duality theory of Mohajerin Esfahani and Kuhn (Math. Program. 2018, arXiv:1505.05116); the regularization interpretation was later extended to general losses by Shafieezadeh-Abadeh, Kuhn and Mohajerin Esfahani (JMLR 2019, arXiv:1710.10016).

Setting

Let $V$ be the feature space $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and let $\|\beta\|_* = \sup_{\|x\|\le1}\langle\beta,x\rangle$ be the dual norm of a weight vector $\beta$. Labels are $y\in\{-1,+1\}$, and the feature-label space is $\Xi = V\times\{-1,+1\}$. The logloss of $\beta$ at $(x,y)$ is

$$l_\beta(x,y) = \log\big(1+\exp(-y\langle\beta,x\rangle)\big).$$

For a label weight $\kappa>0$, the metric of Definition 2 on $\Xi$ is

$$d\big((x,y),(x',y')\big) = \|x-x'\| + \kappa\,|y-y'|/2 ,$$

so that changing a label costs $\kappa$. The Wasserstein distance $W(\mathbb Q,\mathbb P)$ between probability distributions on $\Xi$ (Definition 1) is the infimum of $\int d(\xi,\xi')\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ of $\mathbb Q$ and $\mathbb P$, and $\mathbb B_\varepsilon(\mathbb P) = \{\mathbb Q : W(\mathbb Q,\mathbb P)\le\varepsilon\}$. Given training samples $(\hat x_i,\hat y_i)_{i=1}^N$, the empirical distribution is $\hat{\mathbb P}_N = \frac1N\sum_i\delta_{(\hat x_i,\hat y_i)}$, and the distributionally robust logistic regression problem (6) is

$$\hat J = \inf_\beta\ \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)} \mathbb E^{\mathbb Q}\big[l_\beta(x,y)\big].$$

Program (7) has variables $\beta$, $\lambda\in\mathbb R$, $s\in\mathbb R^N$, objective $\lambda\varepsilon + \frac1N\sum_i s_i$, and constraints $l_\beta(\hat x_i,\hat y_i)\le s_i$, $l_\beta(\hat x_i,-\hat y_i)-\lambda\kappa\le s_i$ for all $i$, and $\|\beta\|_*\le\lambda$.

Formalization targets

Goal: Theorem 1 (tractable reformulation)

For every $\varepsilon\ge0$, $\kappa>0$, $N\ge1$ and every norm on the feature space,

$$\inf_\beta\ \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[l_\beta] \;=\; \inf\Big\{\lambda\varepsilon+\tfrac1N\textstyle\sum_i s_i : (\beta,\lambda,s)\text{ feasible for (7)}\Big\},$$

and for $\varepsilon>0$ the infimum of (7) is attained.

Milestones

1. §3.1 — the feasible set of (7) is convex.
2. §2 — for $\varepsilon=0$ the worst-case expected logloss is the empirical average logloss, so (6) reduces to classical logistic regression (2).
3. Theorem 1 for fixed $\beta$ — $\sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[l_\beta]$ equals the attained minimum of (7) over $(\lambda,s)$ with $\beta$ fixed.
4. Remark 2, eq. (9) — at an optimal solution $(\hat\beta,\hat\lambda,\hat s)$,

$$\hat J = \hat\lambda\varepsilon + \mathbb E^{\hat{\mathbb P}_N}[l_{\hat\beta}] + \tfrac1N\textstyle\sum_i\max\{0,\hat y_i\langle\hat\beta,\hat x_i\rangle-\hat\lambda\kappa\}.$$

5. Remark 1 — as $\kappa\to\infty$ the optimal value of (7) converges to $\inf_\beta \varepsilon\|\beta\|_* + \frac1N\sum_i l_\beta(\hat x_i,\hat y_i)$.
6. Theorem 2, implication — if $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, then $\mathbb P^N\{\mathbb E^{\mathbb P}[l_{\hat\beta}]\le\hat J\}\ge1-\eta$.

Significance

Theorem 1 turns a minimax problem over an infinite-dimensional family of distributions into a finite convex program whose size grows linearly in $N$; with the $\ell_1$, $\ell_2$ or $\ell_\infty$ norm it is a standard exponential-cone or conic program. Remark 1 explains norm-regularized logistic regression as a distributionally robust model: the regularizer is the dual norm of the transport cost on features, and the regularization weight is the radius of the ambiguity set. Remark 2 exposes an additional term that accounts for label noise and vanishes as label changes become prohibitively expensive. Theorem 2 makes the optimal value $\hat J$ a certificate on the out-of-sample logloss whenever the ball contains the true distribution.

The paper's proofs are in a technical appendix and have not been machine-checked. Mathlib contains no Wasserstein distributionally robust duality. This mission produces a formal statement of the reformulation with an arbitrary norm and a label-dependent cost, together with formal versions of the paper's printed consequences of it (Remarks 1 and 2, the $\varepsilon=0$ reduction, and the implication in Theorem 2).

Difficulty

The worst-case expectation ranges over every Borel probability distribution within transport distance $\varepsilon$ of the empirical distribution, including distributions with unbounded support and distributions that move mass across labels. Exhibiting good distributions in the ball shows only that the robust value is at least the value of (7); the reverse inequality must control every distribution in the ball at once, and nothing in the definition of the ball bounds its elements' supports. The obvious simplification, restricting attention to distributions supported on finitely many points, again yields only a one-sided bound unless the supremum is shown to be approached by such distributions. The label term of the metric couples the two label classes, so results for a pure norm cost on the features do not apply directly, and the dual norm enters through an arbitrary norm rather than the Euclidean one.

Formalization scope

• The feature space is an abstract finite-dimensional real normed space V standing for $(\mathbb R^n,\|\cdot\|)$ with an arbitrary norm; weights are continuous linear functionals V →L[ℝ] ℝ, and $\|\beta\|_*$ is their operator norm, which is exactly the dual norm. Labels are Bool, embedded as $\pm1$; the label $-y$ is Boolean negation. The metric of Definition 2 is written literally.
• The Wasserstein distance is of type 1, valued in $[0,\infty]$, with couplings ranging over all probability measures on $\Xi\times\Xi$ with the two prescribed marginals. The ball consists of probability measures.
• Expectations of the positive logloss are lower Lebesgue integrals in $[0,\infty]$, and the supremum over the ball is taken there; the optimal value of (7) is the infimum of its (nonnegative) objective over the feasible set, also in $[0,\infty]$. A Bochner integral, which vanishes on non-integrable functions, would make the worst case trivially finite and is not used.
• The standing hypotheses are $\kappa>0$, $\varepsilon\ge0$, $N\ge1$.
• Correction. The paper prints "min" in (7) for all $\varepsilon\ge0$. At $\varepsilon=0$ the minimum can fail to be attained ($V=\mathbb R$, $N=1$, $\hat x_1=1$, $\hat y_1=+1$: the value is $0$ but every feasible point has positive objective). The goal states the value identity for $\varepsilon\ge0$ and attainment for $\varepsilon>0$.
• Remark 1 is formalized as convergence of optimal values as $\kappa\to\infty$; a metric with $\kappa=\infty$ is not formalized. Only convexity, not tractability, of (7) is stated. The first claim of Theorem 2 (the radius (8) and the light-tail assumption) is not formalized; the confidence of the ball event is a hypothesis of milestone 6.
• A formalization in which the ball is taken only over distributions supported on the training samples, or in which the label term of the metric is dropped, trivializes the second constraint group of (7) and is ruled out: the ball here contains every Borel probability distribution on $\Xi$ within the prescribed distance.
• Infrastructure needed and reusable beyond this mission: type-1 optimal transport on product spaces with a label component, couplings and their marginals, and elementary properties of the logloss as a function of $\beta$. Contributions of such supporting lemmas as independent theorems are welcome.

Selected references

• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28 (NIPS 2015). https://arxiv.org/abs/1509.09259
• P. Mohajerin Esfahani, 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
• N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://arxiv.org/abs/1312.2128
• S. Shafieezadeh-Abadeh, D. Kuhn, P. Mohajerin Esfahani, Regularization via Mass Transportation, Journal of Machine Learning Research 20 (2019). https://arxiv.org/abs/1710.10016