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

The discrete optimal transport problem between two histograms is a linear program, and much of the algorithmic theory of optimal transport is the theory of solving that linear program well. Chapter 3 of Peyré and Cuturi's Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019) surveys the classical combinatorial solvers: the network simplex, dual ascent methods, and the auction algorithm. Dual ascent methods work entirely with the dual variables, the Kantorovich potentials $(f, g)$: they keep a feasible pair of potentials and improve it step by step until it is optimal. The specialisation of this idea to assignment problems is the Hungarian algorithm of Kuhn (1955), and its general form is the primal-dual method for network flow problems presented in Bertsimas and Tsitsiklis, Introduction to Linear Optimization (1997, §7.7), on which §3.6 of the book is modelled.

The mathematical engine of every dual ascent method is one alternative: a feasible pair of potentials is either already optimal, or it can be improved along a direction of a very special, combinatorial form. This mission formalizes that alternative (Proposition 3.6 of the book) together with the results it rests on.

Setting

Fix integers $n, m \ge 1$, a cost matrix $C \in \mathbb{R}^{n\times m}$, and two histograms $a \in \Sigma_n$, $b \in \Sigma_m$, where $\Sigma_n = \{a \in \mathbb{R}^n_+ : \sum_i a_i = 1\}$ is the probability simplex. Write $[\![n]\!] = \{1, \dots, n\}$ for the row indices and, following the book, $[\![m]\!]' = \{1', \dots, m'\}$ for the column indices.

The couplings between $a$ and $b$ form the transportation polytope

$$U(a,b) = \{P \in \mathbb{R}^{n\times m}_+ : P\mathbb{1}_m = a,\ P^{\mathsf T}\mathbb{1}_n = b\},$$

and the primal problem is $\mathrm{L}_C(a,b) = \min_{P\in U(a,b)} \langle C, P\rangle$ with $\langle C, P\rangle = \sum_{i,j} C_{i,j}P_{i,j}$. A pair of vectors $(f, g) \in \mathbb{R}^n \times \mathbb{R}^m$ is dual feasible, written $(f,g) \in R(C)$, when $f_i + g_j \le C_{i,j}$ for all $(i, j)$. The dual problem (3.4) is

$$\mathrm{L}_C(a,b) = \max_{(f,g)\in R(C)} \langle f, a\rangle + \langle g, b\rangle .$$

For a feasible pair $(f, g)$, a pair of indices $(i, j')$ is balanced if $f_i + g_j = C_{i,j}$ and inactive if $f_i + g_j < C_{i,j}$. A matrix $P$ and a pair $(f, g)$ are complementary if $P_{i,j} > 0$ implies $C_{i,j} = f_i + g_j$, that is, $P$ is supported on balanced pairs. For $S \subset [\![n]\!]$ the vector $\mathbb{1}_S \in \mathbb{R}^n$ has ones at the indices in $S$ and zeros elsewhere; likewise $\mathbb{1}_{S'} \in \mathbb{R}^m$ for $S' \subset [\![m]\!]'$.

Formalization targets

Goal: Proposition 3.6 (p. 416)

For $a \in \Sigma_n$, $b \in \Sigma_m$ and $(f,g) \in R(C)$: either $(f, g)$ is optimal for (3.4), or there exist $S \subset [\![n]\!]$, $S' \subset [\![m]\!]'$ and $\varepsilon_0 > 0$ such that for every $0 < \varepsilon \le \varepsilon_0$,

$$(\tilde f, \tilde g) = (f, g) + \varepsilon(\mathbb{1}_S, -\mathbb{1}_{S'}) \in R(C) \quad\text{and}\quad \langle \tilde f, a\rangle + \langle \tilde g, b\rangle > \langle f, a\rangle + \langle g, b\rangle .$$

Milestones

1. Proposition 3.3 (p. 405). If $P \in U(a,b)$ and $(f,g) \in R(C)$ are complementary, then $P$ is primal optimal and $(f,g)$ is dual optimal.
2. Proposition 3.5 (p. 415). If every balanced pair $(i, j')$ with $i \in S$ has $j' \in S'$, then $(f,g) + \varepsilon(\mathbb{1}_S, -\mathbb{1}_{S'}) \in R(C)$ for all sufficiently small $\varepsilon > 0$.
3. Objective change (proof of Proposition 3.6, pp. 416–417). The step changes the dual objective by exactly $\varepsilon(\mathbb{1}_S^{\mathsf T}a - \mathbb{1}_{S'}^{\mathsf T}b)$.
4. Labeled sets (proof of Proposition 3.6, pp. 416–417). If no coupling in $U(a,b)$ is complementary to $(f,g)$, then there are $S, S'$ with every balanced pair leaving $S$ landing in $S'$, and

$$\mathbb{1}_S^{\mathsf T}a - \mathbb{1}_{S'}^{\mathsf T}b > 0 .$$

Significance

The result. Proposition 3.6 says that non-optimality of a feasible dual pair is always witnessed by a direction with entries in $\{0, \pm 1\}$, determined by two index sets, which keeps the pair feasible for a positive step and strictly improves the objective. This is what makes dual ascent a finite combinatorial method rather than a generic linear-programming iteration: the search for an ascent direction reduces to a maximum-flow computation on the bipartite graph of balanced pairs. Combined with the step length of Proposition 3.5, it is the primal-dual method, which reduces to the Hungarian algorithm on assignment problems. Milestone 1 is the optimality certificate of complementary slackness, used throughout the book's chapter 3.

Formalizing it. These results are classical and proved in the book and in Bertsimas and Tsitsiklis; no machine-checked proof of them is known to exist. The mission produces a formal statement and proof of the optimality-or-ascent alternative for the discrete Kantorovich dual, together with the complementary-slackness certificate in the transport setting. Milestone 4 is a Hall-type statement (a supply–demand theorem on a bipartite graph) whose formal proof is reusable for other matching and transportation results.

Difficulty

Milestones 1–3 are short computations. The content of the goal is in milestone 4. The obvious argument is linear-programming duality: if $(f,g)$ is not optimal, some feasible direction improves the objective. But LP duality only produces an arbitrary real direction; the claim that a direction of the form $(\mathbb{1}_S, -\mathbb{1}_{S'})$ suffices is a combinatorial statement. The book obtains $S, S'$ as the labeled nodes of a maximal flow (Ford–Fulkerson) and argues through max-flow/min-cut; the flow bookkeeping printed on p. 417 is garbled, so the step from "no complementary coupling exists" to "$\mathbb{1}_S^{\mathsf T}a > \mathbb{1}_{S'}^{\mathsf T}b$ for a set closed under balanced edges" has to be supplied carefully. Separately, connecting "not optimal" to "no complementary coupling exists" needs the converse direction of complementary slackness or strong duality for the transport problem.

Formalization scope

Row and column indices are Fin n and Fin m (0-based); the primed column set $[\![m]\!]'$ is just Fin m. Cost matrices and couplings are Matrix (Fin n) (Fin m) ℝ; histograms and potentials are real functions on Fin n, Fin m; $\Sigma_n$ is Mathlib's stdSimplex ℝ (Fin n). Index sets $S, S'$ are Finsets and $\mathbb{1}_S$ is indicatorVec S. "Optimal for Problem (3.4)" is the predicate IsDualOptimal: feasible, and no feasible pair has a larger objective (no real infimum or supremum is used, so no junk value can enter). The book's "for a small enough $\varepsilon > 0$" is stated as "for every $\varepsilon \in (0, \varepsilon_0]$", which is equivalent because $R(C)$ is convex and the objective is linear.

Standing assumptions, all from the book: $(f, g)$ is dual feasible (p. 415, "In what follows, $(f,g)$ is a feasible dual pair in $R(C)$"); $a, b$ are histograms in the simplex (used for the goal and milestone 4; without equal masses the dual is unbounded and optimality fails for every pair). Milestone 4 replaces the book's flow hypothesis "the throughput is strictly smaller than 1" by the equivalent flow-free statement "no coupling in $U(a,b)$ is complementary to $(f,g)$"; flows, capacities and the labeling algorithm appear in no statement.

The goal admits a trivializing formalization: allowing an arbitrary direction $(u, v)$ instead of $(\mathbb{1}_S, -\mathbb{1}_{S'})$ turns Proposition 3.6 into plain non-optimality of a linear program. The statement here fixes the direction to $(\mathbb{1}_S, -\mathbb{1}_{S'})$ exactly as the book does.

A complete development needs finite LP duality or complementary slackness for the transportation problem, and a max-flow/min-cut or Hall-type theorem on bipartite graphs with vertex capacities. Both are reusable well beyond this mission. Contributions welcome: proofs of the milestones, a self-contained proof of milestone 4 by induction or by a max-flow argument, and alternative proofs of the goal through LP duality plus a vertex argument.

Selected references

• G. Peyré, M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073 (§3.1–3.3, §3.6, pp. 400–417)
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §7.7 (the primal-dual method) and pp. 305–308 (Ford–Fulkerson and the labeling algorithm).
• H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2(1–2):83–97, 1955. https://doi.org/10.1002/nav.3800020109
• L. R. Ford, D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5

Motivation

Optimal transport compares two probability distributions by the least cost of moving one onto the other. When the ground cost is itself a distance, $c(x,y)=d(x,y)$, the resulting quantity is the 1-Wasserstein distance $\mathcal W_1$, also called the earth mover's distance. It is the transport distance most used in practice for comparing histograms, images and point clouds, and it is the setting of Chapter 6 of G. Peyré and M. Cuturi, Computational Optimal Transport (FnT ML 2019).

For general costs the dual problem has two potentials $(f,g)$ coupled by the constraint $f(x)+g(y)\le c(x,y)$. For a metric cost the dual collapses to a single potential constrained to be 1-Lipschitz. This is the Kantorovich–Rubinstein formula (Kantorovich and Rubinstein, 1958, cited by the book on p. 473), the basis of dual computations of $\mathcal W_1$: network-flow algorithms, the discrete linear programs of §6.1, and Wasserstein GANs, whose critics are 1-Lipschitz networks (Arjovsky, Chintala and Bottou, 2017). Proposition 6.1 of the book is the step that makes the collapse happen. It describes exactly which functions arise as $c$-transforms when $c=d$.

Setting

Let $(\mathcal X,d)$ be a metric space and take $\mathcal Y=\mathcal X$ with ground cost $c(x,y)=d(x,y)$. For a real function $f$ on $\mathcal X$ its $c$-transform (the book's (5.1)) is

$$f^c(y)=\inf_{x\in\mathcal X}\, d(x,y)-f(x),\qquad y\in\mathcal X .$$

The infimum can be $-\infty$ when the family is unbounded below. A function of the form $g^c$ is called $c$-concave. The Lipschitz constant of $f$ is

$$\mathrm{Lip}(f)=\sup\left\{\frac{|f(x)-f(y)|}{d(x,y)} : (x,y)\in\mathcal X^2,\ x\ne y\right\},$$

and $f$ is 1-Lipschitz when $\mathrm{Lip}(f)\le 1$, i.e. $|f(x)-f(y)|\le d(x,y)$ for all $x,y$.

For the discrete companion, fix points $z_1,\dots,z_N\in\mathcal X$ and probability histograms $a,b\in\Sigma_N$ (nonnegative entries summing to one). Let $D_{k,\ell}=d(z_k,z_\ell)$. The couplings $U(a,b)$ are the nonnegative $N\times N$ matrices with row sums $a$ and column sums $b$. The optimal transport cost is $L_D(a,b)=\min_{P\in U(a,b)}\langle D,P\rangle$ with $\langle D,P\rangle=\sum_{k,\ell}D_{k,\ell}P_{k,\ell}$.

Formalization targets

Goal: Proposition 6.1 (p. 472)

For every real function $f$ on $\mathcal X$:

$$\bigl(\exists\, g\in\mathcal C(\mathcal X):\ f=g^c\bigr)\iff \mathrm{Lip}(f)\le 1, \qquad\text{and}\qquad \mathrm{Lip}(f)\le1\ \Longrightarrow\ f^c=-f .$$

Milestones (from the book's proof, pp. 472–473)

1. If $f=g^c$ is real valued, then $|f(x)-f(y)|\le d(x,y)$ for all $x,y$.
2. If $\mathrm{Lip}(f)\le1$ and $g=-f$, then $g^c(y)=\inf_x\,[d(x,y)+f(x)]=f(y)$ for every $y$.
3. If $\mathrm{Lip}(f)\le1$, then $f^c(y)=\inf_x\,[d(x,y)-f(x)]=-f(y)$ for every $y$.

Companion: the discrete formula (6.2) (p. 473)

$$L_D(a,b)=\max_{\mathbf f\in\mathbb R^N}\Bigl\{\sum_k \mathbf f_k(a_k-b_k) : \forall (k,\ell),\ |\mathbf f_k-\mathbf f_\ell|\le d(z_k,z_\ell)\Bigr\},$$

with the minimum on the left and the maximum on the right both attained.

The mission also references the measure-theoretic Kantorovich–Rubinstein theorem already proved on the platform (WassersteinDRO.Duality.kantorovich_rubinstein). It is the book's (6.1) on a normed space.

Significance

The result. Proposition 6.1 identifies the $c$-concave functions for a metric cost with the 1-Lipschitz functions, and shows that the $c$-transform of such a function is $-f$. Starting from the dual problem in a single potential, the book then replaces $(g,g^c)$ by $(g^c,-g^c)$. This yields (6.1), $\mathcal W_1(\alpha,\beta)=\max_{\mathrm{Lip}(f)\le1}\int f\,\mathrm d(\alpha-\beta)$. Consequently $\mathcal W_1$ is a norm on measures of zero total mass. In the discrete case the dual is the finite program (6.2), whose constraints only involve pairs of support points. The min-cost-flow formulations and the Lipschitz-critic methods built on $\mathcal W_1$ all start from this characterization.

Formalizing it. The proposition and (6.2) are classical, with complete proofs in the book. The mission produces machine-checked versions in a form that later chapters of this series can reuse. (6.2) is the discrete, linear-programming form of Kantorovich–Rubinstein duality, and the referenced platform theorem does not imply it without further work. To the best of this mission's search of the platform, neither Proposition 6.1 nor (6.2) has been formalized there. Villani's double-conjugate theorem $(\psi^c)^c=\psi$ for $c$-concave $\psi$ is published, but it is a different statement.

Difficulty

Proposition 6.1 is short; its content is the characterization, not a long argument. One point needs care: an infimum over an arbitrary metric space can be $-\infty$. The statement "$f=g^c$" therefore carries the information that the infimum is finite at every point. An encoding in which the infimum of an unbounded family silently becomes $0$ would make the forward direction false, or decide it by a default value. The discrete companion (6.2) is a genuine duality theorem. It needs both the attainment of the transport minimum and a strong-duality argument specialised to a metric cost matrix. Ordinary LP duality yields two potentials, and the reduction to a single 1-Lipschitz potential is exactly Proposition 6.1 on the finite set $\{z_1,\dots,z_N\}$.

Formalization scope

• $\mathcal X$ is an arbitrary Lean MetricSpace; no compactness, completeness or separability is assumed, since the book's §6.1 assumes only that $d$ is a distance.
• The $c$-transform is the published MongeKantorovichYao.cConjugate, applied to the cost $(x,y)\mapsto d(x,y)$. Its infimum is taken in EReal over all $x\in\mathcal X$, so it never takes a default value. "$f=g^c$" is an equality in EReal with $f$ real valued.
• $\mathrm{Lip}(f)\le1$ is Mathlib's LipschitzWith 1 f, which is equivalent to the book's supremum formula.
• In the goal, $g$ ranges over continuous real functions (the book's $\mathcal C(\mathcal X)$). The book's $f\in\mathcal C(\mathcal X)$ is not assumed: both sides of the equivalence force $f$ to be 1-Lipschitz, hence continuous. Milestone 1 allows any real $g$, which is more general than the book's statement.
• No Nonempty assumption: for empty $\mathcal X$ every claim holds trivially, and for nonempty $\mathcal X$ the infimum ranges over a nonempty family.
• In (6.2), indices are Fin N. The two measures are written on common points $z_k$, which need not be distinct, and $\mathcal W_1(\alpha,\beta)$ is the discrete cost $L_D(a,b)$ of (2.11).
• The statement is not trivialised by its encoding: a sorry-free check shows that $f^c$ equals $-\infty$, not a junk value, on an unbounded-below example. The hypotheses of (6.2) are satisfiable, with $ab^\top\in U(a,b)$.

Contributions welcome: proofs of the milestones and goal, and a proof of (6.2), via finite LP duality and the milestones or via the referenced measure-theoretic theorem.

Selected references

• G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073 (arXiv: https://arxiv.org/abs/1803.00567)
• L. V. Kantorovich and G. S. Rubinstein, On a space of totally additive functions, Vestn. Leningrad Universitet 13:52–59, 1958 (Russian; no stable online link located, cited after the book's bibliography).
• C. Villani, Optimal Transport: Old and New, Grundlehren der mathematischen Wissenschaften 338, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
• M. Arjovsky, S. Chintala and L. Bottou, Wasserstein Generative Adversarial Networks, ICML 2017. https://arxiv.org/abs/1701.07875

Motivation

Comparing histograms is a basic operation in statistics, computer vision and machine learning: a bag of image descriptors, a word-frequency vector, a discretized density. When the bins carry a geometry (colors that are close to one another, words with related meanings), a comparison that ignores the geometry, such as an $\ell^p$ norm between the histogram vectors, treats a small shift of mass to a neighboring bin as severely as a shift to a distant bin. Optimal transport compares two histograms by the cheapest way to move one onto the other, with costs read off a ground distance between bins. Rubner, Tomasi and Guibas introduced it to image retrieval as the earth mover's distance (Rubner et al. 2000), and it has since been used for document classification (Kusner et al. 2015) and as a training loss (Frogner et al. 2015).

These uses rely on the transport cost being a distance, so that nearest-neighbor search, clustering and the geometry of the space of histograms behave as expected. This mission formalizes the statement that it is one: Proposition 2.2 of Peyré and Cuturi, Computational Optimal Transport (2019), the discrete form of the classical fact that the $p$-Wasserstein distance is a metric (Villani 2003, Theorem 7.3).

Setting

Fix $n\ge1$ and write $[\![n]\!]=\{1,\dots,n\}$. The probability simplex is

$$\Sigma_n=\Big\{a\in\mathbb R^n_+ : \textstyle\sum_{i=1}^n a_i=1\Big\};$$

its elements are histograms. For $a,b\in\Sigma_n$ the set of couplings (2.10) is

$$U(a,b)=\{P\in\mathbb R^{n\times n}_+ : P\mathbb 1_n=a,\ P^{\top}\mathbb 1_n=b\},$$

the nonnegative matrices with row sums $a$ and column sums $b$; $P_{i,j}$ is the mass sent from bin $i$ to bin $j$. For a cost matrix $C$, the Kantorovich problem (2.11) is

$$L_C(a,b)=\min_{P\in U(a,b)}\langle C,P\rangle,\qquad \langle C,P\rangle=\sum_{i,j}C_{i,j}P_{i,j}.$$

A matrix $D\in\mathbb R^{n\times n}_+$ is a distance on $[\![n]\!]$ if it is symmetric, $D_{i,j}=0$ exactly when $i=j$, and $D_{i,k}\le D_{i,j}+D_{j,k}$ for all $i,j,k$. For $p\ge1$, write $D^p=(D_{i,j}^p)_{i,j}$ for the entrywise power. The $p$-Wasserstein distance (2.17) is

$$\mathrm W_p(a,b)=L_{D^p}(a,b)^{1/p}.$$

In the Lean development these are couplings a b, frob C P, otCost C a b, powCost D p and W D p a b in the namespace CompOT.Metric.

Formalization targets

Goal: Proposition 2.2 (p. 377)

For a distance matrix $D$ and $p\ge1$, for all $a,b,c\in\Sigma_n$,

$$\mathrm W_p(a,b)=\mathrm W_p(b,a),\quad \mathrm W_p(a,b)\ge0,\quad \mathrm W_p(a,b)=0\iff a=b,\quad \mathrm W_p(a,c)\le\mathrm W_p(a,b)+\mathrm W_p(b,c).$$

Milestones, from the book's proof (pp. 377–379)

1. $\mathrm{diag}(a)$ is an optimal coupling in $U(a,a)$ for $D^p$ and $\mathrm W_p(a,a)=0$.
2. If $a\ne b$, every $P\in U(a,b)$ has $P_{i,j}\ne0$ for some $i\ne j$.
3. If $a\ne b$, then $\mathrm W_p(a,b)>0$.
4. $\mathrm W_p(a,b)=\mathrm W_p(b,a)$.
5. Gluing. With $\tilde b_j=b_j$ if $b_j>0$ and $\tilde b_j=1$ otherwise, for $P\in U(a,b)$ and $Q\in U(b,c)$,

$$S=P\,\mathrm{diag}(1/\tilde b)\,Q\in U(a,c).$$

6. Minkowski chain. For the same $P,Q,S$,

$$\langle S,D^p\rangle^{1/p}\le\langle P,D^p\rangle^{1/p}+\langle Q,D^p\rangle^{1/p}.$$

The case $p=1$ of the goal's attainment and triangle inequality is already proved on the platform, in another encoding (couplings as functions on $V\times V$ for a finite metric space $V$): MarkovMixing.transport_metric, included here as a reference item. The goal for general $p\ge1$ is new.

Significance

The result. Proposition 2.2 makes $(\Sigma_n,\mathrm W_p)$ a metric space whose metric depends on the ground distance $D$. This is what entitles later chapters of the book to speak of Wasserstein barycenters, geodesics and Lipschitz properties of the transport cost, and it underlies the use of $\mathrm W_p$ as a loss or a retrieval distance. Remark 2.15 of the same page records that for $0<p\le1$ it is $\mathrm W_p^p$, not $\mathrm W_p$, that is a distance, so the restriction $p\ge1$ is substantive.

Formalizing it. The result is classical and fully proved in the book; it has not been machine-checked for general $p$ in this discrete matrix form. The platform's $p=1$ result uses a different encoding of couplings, so this mission supplies the matrix-form transportation polytope $U(a,b)$, the cost $L_C$ and $\mathrm W_p$ shared with the other missions of this series, plus a discrete gluing lemma and a Minkowski step stated for arbitrary couplings, which are reusable in any finite transport argument.

Difficulty

Symmetry and definiteness are short once the minimum in $L_{D^p}$ is known to be attained, which needs compactness of $U(a,b)$; strict positivity for $a\ne b$ fails for an infimum that is not attained. The triangle inequality is the substantial part. The direct idea of composing the two transport plans as $PQ$ does not give a coupling: the composition must be renormalized by the middle histogram $b$, and $b$ may have zero entries, on which a naive $1/b_j$ is undefined. The renormalized matrix must then be shown to have the right marginals, which uses that $P_{i,j}=0$ wherever $b_j=0$. The final step needs Minkowski's inequality for weighted $\ell^p$ sums together with the triangle inequality of $D$ and the monotonicity of $t\mapsto t^p$; for $p<1$ it fails.

Formalization scope

Indices $[\![n]\!]$ are Fin n (0-based). Histograms are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and $\Sigma_n$ is Mathlib's stdSimplex ℝ (Fin n); histograms may have zero entries. $L_C(a,b)$ is a real infimum over the subtype $U(a,b)$, and every theorem assumes the histograms lie in $\Sigma_n$, where $U(a,b)$ is nonempty (it contains $ab^{\top}$) and compact. That attainment is part of what a solver proves; it is not a hypothesis. The exponent $p$ is a real number with $p\ge1$, and all powers are real powers. The book's "positive" is read as $\mathrm W_p\ge0$; strict positivity is the clause $\mathrm W_p(a,b)=0\iff a=b$. The hypotheses of the goal are exactly those of the page: $D_{i,j}\ge0$, (i)–(iii), and $p\ge1$. The milestones carry the same setting, and milestones 5 and 6 are stated for all couplings instead of only optimal ones, since the proof does not use optimality there.

A trivializing formalization is ruled out: without the simplex hypotheses $U(a,b)$ can be empty and the real infimum would be $0$, making "$\mathrm W_p(a,b)=0$" true for unrelated histograms; and the four claims are stated about $\mathrm W_p$ itself, not about the glued coupling or about a minimum over a set assumed nonempty.

Needed infrastructure: compactness and nonemptiness of $U(a,b)$ and attainment of $L_C$; transposition of couplings; the gluing construction; Minkowski's inequality for finite weighted sums (Mathlib has Real.Lp_add_le and its weighted variants). Proofs of any milestone are welcome, as are reusable lemmas on $U(a,b)$.

Selected references

• G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073 (Proposition 2.2, p. 377).
• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, AMS, 2003. https://doi.org/10.1090/gsm/058
• Y. Rubner, C. Tomasi and L. J. Guibas, The Earth Mover's Distance as a Metric for Image Retrieval, International Journal of Computer Vision 40(2):99–121, 2000. https://doi.org/10.1023/A:1026543900054
• M. Kusner, Y. Sun, N. Kolkin and K. Weinberger, From Word Embeddings to Document Distances, ICML 2015. https://proceedings.mlr.press/v37/kusnerb15.html
• C. Frogner, C. Zhang, H. Mobahi, M. Araya-Polo and T. Poggio, Learning with a Wasserstein Loss, NeurIPS 2015. https://arxiv.org/abs/1506.05439
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, AMS, 2009, Lemma 14.3 (the $p=1$ case on the platform). https://doi.org/10.1090/mbk/058

Why discrete Kantorovich duality

Optimal transport between two histograms is a linear program: move mass $a_i$ out of each source bin $i$ and deliver mass $b_j$ to each target bin $j$ at unit cost $C_{i,j}$, as cheaply as possible. Its dual replaces the transport plan by a pair of price vectors and is the basis of most of the computational methods in G. Peyré and M. Cuturi's Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019, doi:10.1561/2200000073): the dual ascent and Hungarian methods, the auction algorithm, the semi-discrete solvers of Chapter 5, and the dual reading of Sinkhorn's algorithm in Chapter 4. The book states the duality as Proposition 2.4 and derives it from linear programming strong duality (Bertsimas and Tsitsiklis, Introduction to Linear Optimization, 1997, Theorem 4.4). Remark 2.21 gives it an economic reading: a vendor sets a collection price $f_i$ at each warehouse and a delivery price $g_j$ at each factory, and the best price the vendor can charge while staying below every shipping cost equals the optimal transport cost.

This is the third mission in a series on the book. It covers §2.5 (Dual Problem, pp. 382–385) and §3.1–3.3 (Kantorovich Linear Programs, C-Transforms, Complementary Slackness, pp. 400–405).

Setting

Indices run over $\llbracket n\rrbracket=\{1,\dots,n\}$ and $\llbracket m\rrbracket$. A histogram is a vector in the probability simplex $\Sigma_n=\{a\in\mathbb R^n_+ : \sum_i a_i = 1\}$. Fix $a\in\Sigma_n$, $b\in\Sigma_m$ and a cost matrix $C\in\mathbb R^{n\times m}$; no sign or metric condition is imposed on $C$.

• The couplings (2.10) are $\mathbf U(a,b)=\{P\in\mathbb R_+^{n\times m}: P\mathbb 1_m=a,\ P^{\mathsf T}\mathbb 1_n=b\}$.
• The Kantorovich problem (2.11) is $L_C(a,b)=\min_{P\in\mathbf U(a,b)}\langle C,P\rangle$, with $\langle C,P\rangle=\sum_{i,j}C_{i,j}P_{i,j}$.
• The admissible dual variables (2.21) are $\mathbf R(C)=\{(f,g)\in\mathbb R^n\times\mathbb R^m : f_i+g_j\le C_{i,j}\ \forall i,j\}$, written $f\oplus g\le C$.
• The $C$-transform of $f\in\mathbb R^n$ is $(f^C)_j=\min_i C_{i,j}-f_i$, and the $\bar C$-transform of $g\in\mathbb R^m$ is $(g^{\bar C})_i=\min_j C_{i,j}-g_j$ (§3.2).
• $P$ and $(f,g)$ are complementary w.r.t. $C$ (Definition 3.1) if $C_{i,j}=f_i+g_j$ whenever $P_{i,j}>0$.

In Lean these are couplings, frob, IsOptimalCoupling, dualFeasible, dualObj, IsDualOptimal, cTransform, cbarTransform and Complementary in the namespace CompOT.Duality.

Formalization targets

Goal: Proposition 2.4 (p. 382)

$$L_C(a,b)=\max_{(f,g)\in\mathbf R(C)}\ \langle f,a\rangle+\langle g,b\rangle .$$

Stated with both extrema attained: there are an optimal coupling $P$ and a dual optimal pair $(f,g)$ with $\langle C,P\rangle=\langle f,a\rangle+\langle g,b\rangle$.

Milestones

1. Weak duality (Remark 2.21, p. 385): $\langle C,P\rangle\ge\sum_{i,j}P_{i,j}(f_i+g_j)=\langle f,a\rangle+\langle g,b\rangle$ for $P\in\mathbf U(a,b)$ and $(f,g)\in\mathbf R(C)$.
2. The $C$-transform is the best second potential (§3.2, p. 403): $(f,f^C)\in\mathbf R(C)$, and $g\le f^C$ whenever $(f,g)\in\mathbf R(C)$.
3. Semi-dual inequality (§3.2, p. 403): $\langle f,a\rangle+\langle g,b\rangle\le\langle f,a\rangle+\langle f^C,b\rangle$ for $(f,g)\in\mathbf R(C)$.
4. Proposition 3.1 (pp. 403–404): $f\le f'\Rightarrow f^C\ge f'^C$; $f^{C\bar C}\ge f$ and $g^{\bar CC}\ge g$; $f^{C\bar CC}=f^C$.
5. Proposition 3.3 (p. 405): complementary feasible solutions are primal and dual optimal.
6. Proposition 3.2 (p. 404): for optimal $P^\star$ and $(f^\star,g^\star)$, $P^\star_{i,j}(C_{i,j}-f^\star_i-g^\star_j)=0$ for all $(i,j)$.
7. The semi-dual (3.5) (p. 403): $L_C(a,b)=\max_{f\in\mathbb R^n}\langle f,a\rangle+\langle f^C,b\rangle$.

Milestones 6 and 7 are consequences of the goal; milestones 1 and 5 do not need it.

Significance

Proposition 2.4 is the finite-dimensional form of Kantorovich duality. It turns the optimal cost into a maximum over price vectors, so that any admissible pair of prices certifies a lower bound on $L_C(a,b)$ and an optimal pair certifies optimality of a plan through complementary slackness (Propositions 3.2 and 3.3). The $C$-transform reduces the dual to a concave maximization in one vector (3.5), which is the form used for semi-discrete transport and for stochastic dual methods; Proposition 3.1 shows that alternating $C$- and $\bar C$-transforms stalls after one round.

All of these results are classical and proved in the book or by direct reference to linear programming. General-form LP strong duality, weak duality and complementary slackness are already machine-checked on the platform (LinearOptimization.lp_strong_duality and its siblings, from the Bertsimas–Tsitsiklis series); measure-theoretic weak Kantorovich duality is also on the platform with integrability hypotheses. What this mission adds is the book's own discrete statements in the book's notation, as a base that later missions of the series (dual ascent, auction, entropic duality) can cite, with the $C$-transform calculus of §3.2 formalized for real-valued finite costs.

Difficulty

Weak duality, the $C$-transform facts and Proposition 3.3 are finite computations with sums and minima. The content of the mission is the equality in Proposition 2.4 together with attainment of both the minimum and the maximum. Attainment of the minimum needs compactness and nonemptiness of $\mathbf U(a,b)$; attainment of the maximum is not a compactness argument, since $\mathbf R(C)$ is unbounded (it is invariant under $(f,g)\mapsto(f+t,g-t)$). Reducing Proposition 2.4 to the general LP statement requires an explicit translation of $\mathbf U(a,b)$ and $\mathbf R(C)$ into the general-form primal–dual pair, including the sign conventions of equality-constrained primal variables and free dual variables. The Lagrangian argument on p. 382–383 exchanges a min and a max without justification beyond "always possible for linear programs", so it does not yield a proof by itself.

Formalization scope

Indices are 0-based (Fin n, Fin m); matrices are Matrix (Fin n) (Fin m) ℝ; all quantities are real. Histograms are encoded as a ∈ stdSimplex ℝ (Fin n), the book's standing convention for $(a,b)$, and every statement involving $a$ or $b$ carries it; this also forces $n,m\ge1$. Zero entries in $a$ and $b$ are allowed. Optimality of a plan and of a dual pair are predicates quantifying over the whole feasible set, never real ⨅/⨆, so no junk value from an empty or unbounded set can enter. The $C$-transforms are real infima over a finite index set; statements that use them without histograms assume $n\ge1$ (and $m\ge1$ where the $\bar C$-transform appears), because Lean's infimum over an empty index is $0$.

The goal cannot be satisfied trivially: it asserts existence of a plan that is optimal against every coupling and a pair that is optimal against every admissible pair, with equal values; dropping either optimality clause, or the equal-mass hypotheses, changes the theorem.

Two printed slips are corrected and disclosed in the item notes: Proposition 3.2 prints $C_{i,j}-f^\star_i+g^\star_j$ where its proof uses $C_{i,j}-f^\star_i-g^\star_j$, and Propositions 3.2 and 3.3 refer to the primal and dual as "(2.24)" and "(2.11)", meaning the discrete primal (2.11) and dual (2.20).

Useful infrastructure: the platform's general-form LP strong duality (included as a reference item), Mathlib's stdSimplex and finite infima. Contributions welcome: proofs of each milestone, a direct proof of Proposition 2.4 by reduction to the LP theorem, and alternative proofs of the goal.

Selected references

• G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Theorem 4.4, strong duality).
• L. Kantorovich, On the transfer of masses, Doklady Akademii Nauk SSSR 37:199–201, 1942 (English translation: J. Math. Sci. 133:1381–1382, 2006). https://doi.org/10.1007/s10958-006-0049-2

Motivation

A probability model $\mu$ for a random element $X$ is rarely known exactly. Distributionally robust performance analysis replaces the single expectation $E_\mu[f(X)]$ by its worst case over all models within a prescribed distance of $\mu$. When the distance is an optimal-transport cost, the neighbourhood contains models whose support differs from that of $\mu$. That matters in stochastic-process applications such as ruin probabilities for insurance reserves, where the natural alternatives (a compensated Poisson process against a Brownian motion) are mutually singular and likelihood-based divergences such as Kullback–Leibler are infinite.

Blanchet and Murthy (arXiv:1604.01446, Math. Oper. Res. 2019) prove that the worst-case expectation over an optimal-transport ball equals a one-dimensional dual problem. They assume only that the underlying space is Polish, the cost lower semicontinuous and the performance function upper semicontinuous and integrable.

Timeline. Esfahani and Kuhn (arXiv:1505.05116, 2015/2018) obtained a dual reformulation for Wasserstein balls around empirical measures on $\mathbb R^d$. Gao and Kleywegt (arXiv:1604.02199, 2016) proved a general duality whose proof, as Blanchet and Murthy note, uses the local compactness of the space. Blanchet and Murthy (2016, v2 2017) removed local compactness and continuity of the cost. This covers path spaces such as $C[0,T]$ and $D[0,T]$.

Setting

Let $S$ be a Polish space with Borel σ-algebra $\mathcal B(S)$, and let $\mu$ be a probability measure on $S$ (the baseline model).

• Cost (A1). $c : S\times S\to[0,\infty)$ is lower semicontinuous, and $c(x,y)=0$ if and only if $x=y$.
• Performance function (A2). $f : S\to\mathbb R$ is upper semicontinuous and $\mu$-integrable.
• Budget. $\delta>0$.

The primal feasible set $\Phi_{\mu,\delta}$ consists of the probability measures $\pi$ on $S\times S$ whose first marginal is $\mu$ and whose transport cost satisfies $\int c\,d\pi\le\delta$. The second marginal of $\pi$ is the alternative model. The primal objective is $I(\pi)=\int f(y)\,d\pi(x,y)$, and the primal value is

$$I=\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}.$$

The universal σ-algebra $\mathcal U(S)$ is the intersection of the completions of $\mathcal B(S)$ under all probability measures. Write $m\mathcal U(S;\bar{\mathbb R})$ for the $\mathcal U(S)$-measurable functions $S\to[-\infty,\infty]$. The dual feasible set $\Lambda_{c,f}$ consists of the pairs $(\lambda,\varphi)$ with $\lambda\ge0$, $\varphi\in m\mathcal U(S;\bar{\mathbb R})$ and $\varphi(x)+\lambda c(x,y)\ge f(y)$ for all $x,y$. The dual objective is $J(\lambda,\varphi)=\lambda\delta+\int\varphi\,d\mu$, and the dual value is $J=\inf\{J(\lambda,\varphi):(\lambda,\varphi)\in\Lambda_{c,f}\}$. Finally,

$$\varphi_\lambda(x)=\sup_{y\in S}\{f(y)-\lambda c(x,y)\}\in\mathbb R\cup\{\infty\}.$$

Formalization targets

Goal: Theorem 1

Under (A1) and (A2):

1. strong duality,

$$\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}=\inf\{J(\lambda,\varphi):(\lambda,\varphi)\in\Lambda_{c,f}\};$$

2. there is $\lambda^*\ge0$ such that $(\lambda^*,\varphi_{\lambda^*})$ is a dual optimizer;
3. a feasible $\pi^*$ and a feasible $(\lambda^*,\varphi_{\lambda^*})$ with finite $J(\lambda^*,\varphi_{\lambda^*})$ are optimal with $I(\pi^*)=J(\lambda^*,\varphi_{\lambda^*})$ if and only if the complementary slackness conditions hold:

$$f(y)-\lambda^*c(x,y)=\varphi_{\lambda^*}(x)\ \ \pi^*\text{-a.s.},\qquad \lambda^*\Big(\int c\,d\pi^*-\delta\Big)=0.$$

The "if" direction is stated without the finiteness assumption.

Milestones

Weak duality $I\le J$ (5). Lemma 15. Strong duality with a primal optimizer on compact $S$, first for continuous costs (Proposition 5), then for lower semicontinuous ones (Proposition 6). Universal measurability of $\varphi_\lambda$ (§4.2). Lemma 16. The restricted dual bound of Proposition 7. Lemma 8. The univariate formula (9):

$$I=\inf_{\lambda\ge0}\Big\{\lambda\delta+E_\mu\Big[\sup_{y\in S}\{f(y)-\lambda c(X,y)\}\Big]\Big\}.$$

Significance

The result. Formula (9) turns an infinite-dimensional optimization over probability measures into a one-dimensional convex minimization that involves only the baseline $\mu$. A modeller can therefore evaluate it by sampling from $\mu$. Theorem 1 is the input for the worst-case probability formula for closed sets (Theorem 3 of the paper) and for the existence of worst-case transport plans (Corollary 1). Its complementary slackness conditions describe the structure of every worst-case plan: mass is moved from $x$ to maximizers of $f(z)-\lambda^*c(x,z)$, and the budget is exhausted whenever $\lambda^*>0$.

Formalizing it. The result is proved on paper. To our knowledge it has no machine-checked proof. The only related statement on Prove2Me is a special case (empirical baseline, bounded continuous loss, power-of-norm cost on $\mathbb R^m$). A complete development would contain duality on compact spaces via Fenchel duality, the extension to σ-compact supports, and measurable-selection arguments for universally measurable functions. The measurable-selection part reuses Bertsekas–Shreve's analytic-set theory, which is already posed on the platform.

Difficulty

The obvious route copies Kantorovich duality. That route fails here because the feasible set $\Phi_{\mu,\delta}$ fixes only one marginal, so it is not tight on a non-compact space. Prokhorov compactness is available only on compact pieces $S_n\times S_n$. The duality must then be transported to the whole space by a limiting argument that keeps control of the dual multipliers.

A second obstacle is measurability. For a merely lower semicontinuous cost on a non-locally-compact space, $\varphi_\lambda$ need not be Borel measurable, so the dual must range over universally measurable functions. Removing the restriction $y\in S_\pi$ from the envelope (Lemma 8) needs a measurable selection theorem. Arguments that assume closed balls are compact do not apply in the target spaces $C[0,T]$ and $D[0,T]$.

Formalization scope

• Space and costs. S carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]. The cost is a real-valued curried function c : S → S → ℝ; (A1) is the structure AssumptionA1; (A2) is UpperSemicontinuous f together with Integrable f μ; and 0 < δ is assumed throughout.
• Extended reals. $I$, $J$, $I(\pi)$, $J(\lambda,\varphi)$ and $\varphi_\lambda$ live in EReal. The integral of an extended-real function is $\int\varphi^+-\int\varphi^-$ with lower Lebesgue integrals, and $\infty-\infty$ evaluates to $-\infty$. A coupling with $\int f^-\,d\pi=\infty$ therefore never raises $I$, which is the paper's reading in footnote 2.
• Measurability and integrals. Universal measurability is the published BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable. For such $\varphi$ the lower integral equals the integral against the completion of $\mu$.
• Variants. The dual feasible set takes a set $K$: with $K=S$ it is (6b), and with $K=S_\pi$ it is (29).
• Hidden hypothesis. The "only if" part of Theorem 1(b) carries the hypothesis $J(\lambda^*,\varphi_{\lambda^*})<\infty$. Without it the equivalence fails when $I=J=\infty$.
• Ruled-out trivializations. A primal that fixes both marginals (or neither), a dual over Borel-measurable $\varphi$, and a Bochner integral for $\int f\,d\pi$ (which is $0$ off $L^1(\pi)$) all describe different problems and are ruled out by the definitions.
• Infrastructure and contributions. Needed: Fenchel duality on $C_b(S\times S)$ and its dual $M(S\times S)$ (Riesz–Markov–Kakutani), Prokhorov's theorem, Sion's minimax theorem, and Jankov–von Neumann selection. Several are on the platform or in Mathlib, and all are reusable beyond this mission. Proofs of the milestones in any order, and of the posed Bertsekas–Shreve tools, are welcome.

Selected references

• J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2):565–600, 2019. arXiv:1604.01446v2, doi:10.1287/moor.2018.0936
• R. Gao and A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, 2016. arXiv:1604.02199
• P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171:115–166, 2018. arXiv:1505.05116
• D. Bertsekas and S. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978, Chapter 7. MIT open copy
• C. Villani, Optimal Transport: Old and New, Springer, 2008. doi:10.1007/978-3-540-71050-9