Optimal Transport

Motivation

Wasserstein distributionally robust optimization (DRO) replaces the empirical risk $\mathbb E_{P_n}[f]$ of a loss $f$ by its worst case over all distributions within Wasserstein distance $\rho$ of the empirical law $P_n$. Gao, Chen and Kleywegt (arXiv:1712.06050; Operations Research, 2024, doi:10.1287/opre.2022.2383) show that, for small radii, this worst-case risk is the empirical risk plus $\rho$ times a variation of the loss (a norm of its gradient or local slope), up to a remainder. This links DRO to gradient-norm regularization, as used in adversarial training and in data-driven newsvendor and pricing models.

For smooth losses the remainder is of order $\rho^2$. Many losses used in practice are only piecewise smooth: hinge, ReLU networks, newsvendor costs, $\theta z \wedge 1$. Near the set $\mathcal D_f$ where the pieces meet, the first-order expansion fails, and the paper's Theorem 1(I)–(II) carries an extra boundary term $M\,\mathbb E_{P_n}[(\rho - d(z,\mathcal D_f))_+]$. Theorem 1(III) shows that this term is small with high probability, uniformly over the loss class, provided the data distribution does not concentrate near the non-smooth points. This mission formalizes that probabilistic bound.

Setting

Let $(\mathcal Z, d)$ be a metric space with its Borel $\sigma$-algebra, $P_{\rm true}$ a probability measure on $\mathcal Z$, and $z_1, \dots, z_n$ an i.i.d. sample from $P_{\rm true}$, with empirical law $P_n = \frac1n\sum_i \delta_{z_i}$. The sampling law is the product $P_\otimes = P_{\rm true}^{\otimes n}$ on $\mathcal Z^n$, and $\mathbb E_\otimes$ is its expectation. The formal statements also assume the metric space is second countable.

Let $\mathcal F$ be a set of losses $f : \mathcal Z \to \mathbb R$, and for each $f$ let $\mathcal D_f \subseteq \mathcal Z$ be its non-smooth set: for a piecewise smooth $f$ with pieces $\mathcal Z_{f,1}, \dots, \mathcal Z_{f,K_f}$, the union of the pairwise intersections of their closures (Assumption 1). The paper assumes $\mathcal D_f$ is $P_{\rm true}$-null. The distance to a set is $d(z, D) = \inf_{\tilde z\in D} d(z,\tilde z)$, with $d(z,\varnothing) = +\infty$.

The objects of the mission are:

• the boundary gap $(\rho - d(z, \mathcal D_f))_+$ and the near indicator $\mathbf 1\{d(z,\mathcal D_f) < \rho\}$;
• the indicator class $\mathcal I_\rho = \{z\mapsto \mathbf 1\{d(z,\mathcal D_f)<\rho\} : f\in\mathcal F,\ \mathcal D_f\neq\varnothing\}$;
• the empirical Rademacher complexity $\mathfrak R_n(\mathcal H) = \mathbb E_\sigma\bigl[\sup_{h\in\mathcal H}\frac1n\sum_i\sigma_i h(z_i)\bigr]$ of a class $\mathcal H$, with i.i.d. uniform signs $\sigma_i$, and the Rademacher complexity $\mathbb E_\otimes[\mathfrak R_n(\mathcal H)]$;
• Assumption 3 (bounded density):

$$\limsup_{\delta\downarrow 0}\ \sup_{f\in\mathcal F:\,\mathcal D_f\ne\varnothing}\frac{P_{\rm true}\{z : 0 < d(z,\mathcal D_f) < \delta\}}{\delta} < \infty.$$

In Lean the boundary gap is the shared WassVarReg.PInf.boundaryGap; nearIndicator, indicatorClass, empRademacher, rademacher and Assumption3 are in WassVarReg.Boundary. The sample law is the published MinimaxWass.DataDep.sampleLaw.

Formalization targets

Goal: Theorem 1(III), first display (p. 8)

Under Assumption 3 there exist $\bar\rho, C > 0$ such that for all $n\ge1$, $t>0$ and $0\le\rho<\bar\rho$, with probability at least $1-e^{-t}$, for every $f\in\mathcal F$,

$$\mathbb E_{P_n}\bigl[(\rho - d(z,\mathcal D_f))_+\bigr] \le C\rho^2 + 2\rho\,\mathbb E_\otimes[\mathfrak R_n(\mathcal I_\rho)] + \rho\sqrt{\frac{t}{2n}}.$$

The constants $C$ and $\bar\rho$ are left unspecified; they depend only on Assumption 3.

Milestones

1. Lemma EC.5 (p. ec4): for a class $\mathcal H$ of measurable functions with values in $[0,M]$, with probability at least $1-e^{-t}$, $\mathbb E_{P_n}[h] \le \mathbb E_{P_{\rm true}}[h] + 2\,\mathbb E_\otimes[\mathfrak R_n(\mathcal H)] + M\sqrt{t/(2n)}$ for all $h\in\mathcal H$.
2. Assumption 3 bounds the true mass (proof of Lemma EC.11, p. ec11): $\mathbb E_{P_{\rm true}}[\mathbf 1\{d(z,\mathcal D_f)<\rho\}] \le C\rho$ for $0\le\rho<\bar\rho$, uniformly in $f$.
3. Lemma EC.11 (p. ec11): with probability at least $1-e^{-t}$, for every $f$, $\mathbb E_{P_n}[\mathbf 1\{d(z,\mathcal D_f)<\rho\}] \le C\rho + 2\,\mathbb E_\otimes[\mathfrak R_n(\mathcal I_\rho)] + \sqrt{t/(2n)}$.
4. Gap versus mass (p. ec11): $\mathbb E_{P_n}[(\rho-d(z,\mathcal D_f))_+] \le \rho\,\mathbb E_{P_n}[\mathbf 1\{d(z,\mathcal D_f)<\rho\}]$.

Significance

The result. With $\rho_n = \rho_0/\sqrt n$ and a class $\mathcal I_\rho$ of bounded complexity, the right side of the goal is $O_p(1/n)$. Combined with Theorem 1(I)–(II), it gives the paper's conclusion that $p$-Wasserstein DRO with $p\in(1,\infty]$ is asymptotically equivalent to empirical variation regularization, $\min_f\{\mathbb E_{P_n}[f] + \rho_n\mathcal V_{P_n,q}(f)\} + O_p(1/n)$, for non-smooth losses, uniformly over the class. Without it, the boundary term is only bounded by $M\rho$, and the expansion has no better accuracy than first order. Assumption 3 is the condition under which the non-smooth set does not matter statistically.

Formalizing it. The result is proved in the paper; it has no machine-checked proof. Its proof composes a uniform deviation bound (McDiarmid's inequality plus symmetrization) with a bounded-density estimate. The mission produces a general Rademacher deviation bound for bounded classes on an arbitrary metric space with a measurability guard, reusable by any statistical-learning mission, and fixes the printed constant of Lemma EC.5 ($M\sqrt{2t/n}$ on the page, $M\sqrt{t/(2n)}$ from its proof).

Difficulty

The deterministic parts are short. The difficulty is in Lemma EC.5. McDiarmid's inequality must be applied to the uniform deviation over an arbitrary, possibly uncountable, class. Symmetrization must then be carried out with Bochner integrals over $\mathcal Z^n\times\mathcal Z^n$ and a finite sign space. Neither tool is in Mathlib in this form. A tempting shortcut, bounding each fixed $h$ by Hoeffding's inequality and taking a union bound, fails: the class is infinite, and the bound must hold simultaneously for all $f$ inside a single event. A second point is Assumption 3: it controls only the shell $0 < d(z,\mathcal D_f) < \delta$, so the mass of $\{d = 0\}$ has to come from the null closure of $\mathcal D_f$.

Formalization scope

• Space and sample. $\mathcal Z$ is a metric space with [MeasurableSpace Z] [BorelSpace Z] [SecondCountableTopology Z] in the goal-level statements. Second countability is an added technical hypothesis used throughout this paper's mission series. A sample is ω : Fin n → Z with $n\ge1$, and its law is Measure.pi. Empirical means are $\frac1n\sum_{i : \mathrm{Fin}\,n}$.
• Distance to a set. Metric.infEDist, which is $+\infty$ on $\varnothing$. A loss with $\mathcal D_f=\varnothing$ thus has boundary gap $0$ and is excluded from $\mathcal I_\rho$, as on the page. The real-valued Metric.infDist (which is $0$ on $\varnothing$) would give such a loss gap $\rho$ and is not used.
• The non-smooth sets are an arbitrary family D : (Z → ℝ) → Set Z. The goal-level statements assume each $\mathcal D_f$ is closed and $P_{\rm true}$-null, the standing consequence of its construction in Assumption 1. The details of the piecewise smooth loss model are not needed for this probability estimate.
• Probabilities are written as $P_\otimes\{\omega : \neg\,\forall f\in\mathcal F, \dots\}\le e^{-t}$, with the quantifier over $\mathcal F$ inside the event (an outer measure for uncountable $\mathcal F$).
• Rademacher complexity. The sign expectation is an average over $\{\pm1\}^n$. Suprema are real suprema of classes with values in $[0,M]$; an empty class gives $0$. $\mathbb E_\otimes$ is a Bochner integral.
• Measurability guard (added): the uniform deviation, the empirical Rademacher complexity and the double-sample deviation of the class are measurable. This holds, for instance, for countable $\mathcal F$, and the paper leaves it implicit.
• Quantifier order. $\bar\rho$ and $C$ are chosen before $n$ and $t$, which is stronger than the page's order. The radius satisfies $\rho\ge0$.
• Not stated. The second display of Theorem 1(III) and the "Moreover" part of Lemma EC.11, which use Dudley's entropy integral: their proof bounds the empirical Rademacher complexity, while Lemma EC.5 needs its expectation.
• Trivialization ruled out. The Rademacher term is that of the specific class $\mathcal I_\rho$ built from the sets $\mathcal D_f$. It is not a free constant, and no hypothesis assumes the conclusion of Lemma EC.5.

Contributions welcome: a general McDiarmid inequality for product measures, a symmetrization lemma for measurable classes, and proofs of the milestones in any order.

Selected references

• R. Gao, X. Chen, A. J. Kleywegt, Wasserstein Distributionally Robust Optimization and Variation Regularization, Operations Research, 2024. arXiv:1712.06050, doi:10.1287/opre.2022.2383
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Theorem 26.5. doi:10.1017/CBO9781107298019
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Series 141, 1989. doi:10.1017/CBO9781107359949.008
• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Ch. 5. doi:10.1017/9781108627771

Why relate heat flow and curvature?

Heat flow gives an analytic way to describe how functions spread on a space. Optimal transport gives a metric way to describe how probability measures move on the same space. On a smooth Riemannian manifold, a lower Ricci curvature bound constrains both motions. The problem addressed by Ambrosio, Gigli and Savaré is to identify the corresponding relationship when the underlying space need not be a manifold. A Dirichlet form can specify a heat flow even when there are no smooth coordinates, while a Wasserstein distance can measure transport between probability measures. Theorem 4.17 connects these two descriptions for Riemannian energy measure spaces.

The paper proves the implication from the Bakry–Émery condition $BE(K,\infty)$ to the Riemannian curvature-dimension condition $RCD(K,\infty)$. Its printed theorem is an equivalence; the paper cites the reverse implication from earlier work in the proof on p. 58. This mission targets the implication established here, with the source's exact assumptions.

Setting

Let $X$ be a complete, separable metric space with a Borel measure $m$. A Dirichlet form $\mathcal E$ assigns a nonnegative energy to square-integrable functions, is quadratic and lower semicontinuous, and decreases under normal contractions. Its associated heat flow $P_t$ evolves a function over time. The associated carré du champ $\Gamma(f)$ measures the energy density of a function. Functions with energy density at most one define an intrinsic distance

$$d_{\mathcal E}(x,y)=\sup\{|\psi(y)-\psi(x)|:\psi\text{ is continuous and }\Gamma(\psi)\le1\ m\text{-a.e.}\}.$$

For the Riemannian energy measure space in this mission, this intrinsic distance is the metric of $X$. The structure also requires the paper's upper regularity and continuous-representative properties. The growth condition $(MD.exp)$ controls the measure of large balls. In the $BE(K,\infty)$ condition, a weak second-derivative inequality for the heat flow has curvature parameter $K$ and no finite-dimensional correction term. These assumptions are stated at the start of §4 and govern the §4 milestones even when an individual theorem does not repeat them. See Definitions 3.6 and 3.16 and the opening of §4.

Write $\mathcal P_2(X)$ for the probability measures with finite second moment, $W_2$ for their quadratic Wasserstein distance, and $\operatorname{Ent}_m(\rho)$ for entropy relative to $m$. The heat flow has a dual action $H_t$ on measures. The target $RCD(K,\infty)$ asks for a curve $H_t\rho$ from every $\rho\in\mathcal P_2(X)$ that satisfies the following evolution variational inequality against every $\nu\in\mathcal P_2(X)$ of finite entropy, at every $t>0$:

$$\frac{d^+}{dt}\frac{W_2^2(H_t\rho,\nu)}2 +\frac K2W_2^2(H_t\rho,\nu) +\operatorname{Ent}_m(H_t\rho) \le\operatorname{Ent}_m(\nu).$$

The definition also includes full support, local finiteness, the exponential growth condition, and the length-space property. See Definition 3.1.

Formalization targets

The goal is the forward implication of Theorem 4.17:

$$\text{Riemannian energy measure space}+(MD.exp)+BE(K,\infty) \quad\Longrightarrow\quad RCD(K,\infty).$$

Three milestones supply central results from the paper. The final assertions of Theorem 3.17 give the dual measure flow and its absolute continuity after positive time. Corollary 3.18 identifies $BE(K,\infty)$ with the $W_2$ contraction $W_2((P_t f)m,(P_t g)m)\le e^{-Kt}W_2(fm,gm)$ on probability densities. A companion item, Theorem 4.8, gives an entropy bound for $H_t\mu$ when $\mu$ has finite second moment:

$$\operatorname{Ent}_m(H_t\mu) \le\frac{r^2+\int_X d^2(x,x_0)\,d\mu(x)}{2I_{2K}(t)} -\log m(B_r(x_0)),\qquad r,t>0.$$

The third milestone, Theorem 4.16, bounds the distance and entropy at the heat-evolved endpoint of a regular curve $\rho_s$:

$$W_2^2(\rho_0,H_t\rho_1)+2t\operatorname{Ent}_m(H_t\rho_1) \le R_K(t)^2\int_0^1|\dot\rho_s|^2\,ds +2t\operatorname{Ent}_m(\rho_0),\qquad R_K(t)=t/I_K(t).$$

The milestone list follows the source labels and constants in §4.

What the result provides

The conclusion turns an analytic curvature bound on a heat semigroup into a transport statement about entropy on probability measures. It therefore identifies a concrete set of Dirichlet-form hypotheses under which the heat evolution has the metric behavior demanded by $RCD(K,\infty)$. The result applies in the paper's metric measure setting, where the space may lack a smooth tensor calculus. The $RCD$ conclusion carries convergence from every initial measure in $\mathcal P_2(X)$ and the inequality for all finite-entropy comparison measures.

The mathematical implication is proved in the cited paper. The proposed Lean statements are open proof targets: their declarations compile with placeholders, and no machine-checked proof of this implication is asserted here. A complete development would connect Dirichlet-form calculus, probability measures, entropy, and Wasserstein geometry in reusable interfaces. The dual-flow and regular-curve definitions are especially useful beyond this theorem.

Main difficulty

The heat flow is initially specified on square-integrable functions, whereas the target is an inequality for probability measures, including measures without an initial density. A bound on $\Gamma(P_t f)$ by itself controls functions almost everywhere; it does not immediately produce the pointwise dual flow or the right derivative of $W_2^2$ required by Definition 3.1. The action estimate also begins with regular curves, while the target quantifies over every initial measure in $\mathcal P_2(X)$. These changes of domain and regularity are the central mathematical obstacles; simply renaming the heat semigroup as a measure flow leaves the target unjustified.

Formalization scope

Lean uses real-valued function representatives for $L^2(X,m)$, with almost-everywhere congruence in the Dirichlet form and heat flow. Measures use the Borel sigma algebra. The source uses its $m$-completion; the formalization treats quantities invariant under $m$-almost-everywhere equality, and this convention is explicit in the definition layer. The metric is complete and second countable, and its equality with $d_{\mathcal E}$ is part of the energy-measure-space predicate. A sigma-finiteness instance is carried where entropy or measure operations need it; it follows from the source's measure-growth setting. The dual flow and the $L^1$ extension are bound by predicates that specify their action on densities. The mollifier for a regular curve is bound by the conditions of (2.17), while the action is the infimum of squared admissible speeds, which equals the integral of the squared metric derivative.

Wasserstein costs use $\mathbb R_{\ge0}\cup\{\infty\}$, and entropy uses extended real values. Theorem 4.8 restricts $r,t$ to positive numbers, so the ball mass and $I_{2K}(t)$ used in its formula have the intended domain. Theorem 4.16 also uses $t>0$, making $R_K(t)=t/I_K(t)$ meaningful, including at $K=0$. The goal requires an EVI flow beginning at each $\rho\in\mathcal P_2(X)$ and the inequality at every positive time; allowing a vacuous flow or checking only almost every time would not express Definition 3.1. Contributions may establish the milestone statements and the companion Theorem 4.8, develop the omitted intermediate estimates from §4, or prove the goal from the source's full argument.

Selected references

• L. Ambrosio, N. Gigli and G. Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Annals of Probability 43(1), 2015, 339–404. arXiv:1209.5786v4.

Motivation

A lower bound on Ricci curvature can be expressed in two ways that make sense far beyond smooth manifolds. The Eulerian way bounds the gradient of the heat semigroup: Bakry and Émery's $\Gamma_2$-calculus gives $|\nabla \mathsf P_t f|^2 \le e^{-2Kt}\,\mathsf P_t|\nabla f|^2$. The Lagrangian way bounds how heat flow moves probability measures in optimal transport distance: $W_2(\mathsf H_t\mu,\mathsf H_t\nu)\le e^{-Kt}W_2(\mu,\nu)$. On Riemannian manifolds the two are equivalent (von Renesse–Sturm 2005). Kuwada (2010) showed that the equivalence is a general duality between a pointwise gradient bound with a constant $C(t)$ and $W_2$-contraction with the same constant, valid on length metric measure spaces.

Ambrosio, Gigli and Savaré (arXiv:1209.5786v4, Ann. Probab. 2015) needed this duality in a setting with no doubling or Poincaré inequality, where the semigroup comes from an abstract Dirichlet form and is only defined almost everywhere. Their §3.2 builds the dual semigroup on probability measures and proves the contraction (Theorem 3.5). Combined with their Theorem 3.17 it gives Corollary 3.18, the step that links the Bakry–Émery condition $\mathrm{BE}(K,\infty)$ to $W_2$-contraction and, later in the paper, to $\mathrm{RCD}(K,\infty)$.

Setting

Let $(X,\mathsf d)$ be a complete separable metric space with a Borel measure $m$ of full support such that $m(B_r(x))<\infty$ for every ball (condition (MD)). The space is a length space if $\mathsf d(x_0,x_1)$ is the infimum of the lengths of curves joining $x_0$ to $x_1$ (3.2).

A Dirichlet form $\mathcal E$ on $L^2(X,m)$ is a lower semicontinuous quadratic form with dense domain that does not increase under normal contractions; it is strongly local if $\mathcal E(f,g)=0$ whenever $f+a$ and $g$ have disjoint supports. Its heat flow $(\mathsf P_t)_{t\ge0}$ solves $\frac{d}{dt}\mathsf P_tf=\Delta_{\mathcal E}\mathsf P_tf$ in $L^2$. It is mass preserving if $\int\mathsf P_tf\,dm=\int f\,dm$ (2.12).

$\mathrm{Lip}_b(X)$ denotes bounded Lipschitz functions, $|Df|(x)=\limsup_{y\to x}|f(y)-f(x)|/\mathsf d(y,x)$ the slope, and $\mathscr P(X)$ the Borel probability measures. The Wasserstein cost is

$$W_2^2(\mu,\nu)=\inf\Big\{\int\mathsf d^2(x,y)\,d\boldsymbol\gamma(x,y):\ \boldsymbol\gamma\text{ a coupling of }\mu,\nu\Big\}\in[0,\infty].$$

Two hypotheses on the semigroup, with $C:[0,\infty)\to[0,\infty)$ bounded on every $[0,T]$:

$$\text{(3.15)}\quad \mathsf P_tf\in\mathrm{Lip}_b(X),\ \ \mathrm{Lip}(\mathsf P_tf)\le C(t)\,\mathrm{Lip}(f),\qquad \text{(3.16)}\quad |D\tilde{\mathsf P}_tf|^2(x)\le C^2(t)\,\tilde{\mathsf P}_t|Df|^2(x),$$

for $f\in\mathrm{Lip}_b(X)\cap L^2(X,m)$. Under (3.15) the map $fm\mapsto(\mathsf P_tf)m$ extends uniquely to a weakly continuous dual semigroup $\mathsf H_t:\mathscr P(X)\to\mathscr P(X)$, and $\tilde{\mathsf P}_tf(x)=\int f\,d\mathsf H_t\delta_x$ is the pointwise version of $\mathsf P_t$ (Proposition 3.2).

Formalization targets

Goal: Theorem 3.5 (forward direction)

Under (MD), the length property, (2.12), (3.15) and (3.16), for every $t\ge0$ and $\mu,\nu\in\mathscr P(X)$,

$$W_2(\mathsf H_t\mu,\mathsf H_t\nu)\le C(t)\,W_2(\mu,\nu).$$

The constant $C(t)$ is left free; the goal is the duality itself, not a particular curvature bound.

Milestones

• Proposition 3.2 (i): existence and uniqueness of $\mathsf H_t$, with $W_{(\beta)}(\mathsf H_t\mu,\mathsf H_t\nu)\le(C(t)\vee1)W_{(\beta)}(\mu,\nu)$ and $W_1(\mathsf H_t\mu,\mathsf H_t\nu)\le C(t)W_1(\mu,\nu)$.
• Proposition 3.2 (ii)–(iv): $\tilde{\mathsf P}_t$ preserves $C_b(X)$, agrees $m$-a.e. with $\mathsf P_t$, satisfies the duality $\int f\,d\mathsf H_t\mu=\int\tilde{\mathsf P}_tf\,d\mu$, and is continuous at $t=0$.
• Lemma 3.3: a Fatou-type upper bound $\limsup_n\int f_n\,d\mu_n\le\int f\,d\mu$ for weakly converging $\mu_n$.
• Lemma 3.4: for $f\in\mathrm{Lip}_b(X)$ nonnegative with bounded support and the Hopf–Lax map $Q_1f(x)=\inf_y f(y)+\tfrac12\mathsf d^2(y,x)$,

$$\tilde{\mathsf P}_tQ_1f(x)-\tilde{\mathsf P}_tf(y)\le\tfrac12C^2(t)\,\mathsf d^2(x,y).$$

• (3.26): the contraction for Dirac masses, $W_2^2(\mathsf H_t\delta_x,\mathsf H_t\delta_y)\le C^2(t)\,\mathsf d^2(x,y)$.

Significance

The theorem turns a pointwise, infinitesimal estimate on functions into a global estimate on measures. In the paper, with $C(t)=e^{-Kt}$ it gives the $W_2$-contraction of the heat flow under $\mathrm{BE}(K,\infty)$ (Corollary 3.18). That contraction is an ingredient of the identification of the heat flow with the $\mathrm{EVI}_K$ gradient flow of the entropy (Theorem 4.17). The argument of §3.2 avoids doubling and local Poincaré assumptions on the metric measure space (p. 26), which is what makes it usable for the general Energy measure spaces of the paper.

The result is proved in the literature: in Kuwada's paper, and in the form posed here in §3.2 of the source. As far as a search of the Prove2Me catalogue shows, none of it is formalized: there is no Wasserstein distance on a general metric space, no dual semigroup of a Dirichlet form, and no Hopf–Lax semigroup on metric spaces. The mission asks for formal proofs of the known argument; the dual semigroup, Lemma 3.3 and the Hopf–Lax estimates are reusable on their own.

Difficulty

The semigroup acts on $L^2$ classes, while (3.16) and the contraction are statements at every point; the bridge is the pointwise version $\tilde{\mathsf P}_t$, which exists only through the dual semigroup and its weak continuity. The direct approach, applying the gradient bound along a geodesic between $x$ and $y$, fails because $W_2$ is not a supremum over Lipschitz functions of a linear quantity. The route goes through the quadratic Kantorovich duality and the Hopf–Lax semigroup on a metric space, neither of which is available in Mathlib, and through limits of integrals against varying measures $\mathsf H_t\delta_{y}$. Passing from Dirac masses to arbitrary $\mu,\nu$ needs a measurable selection of optimal plans.

Formalization scope

• Elements of $L^2(X,m)$ are functions; every predicate is invariant under $m$-a.e. equality. The σ-algebra is Borel rather than its $m$-completion.
• The heat flow $\mathsf P$ and the dual semigroup $\mathsf H$ are binders pinned by predicates (IsHeatSemigroup, IsDualSemigroup), not constructions. IsDualSemigroup requires $\mathsf H_t(fm)=(\mathsf P_tf)m$ for probability densities $f\in L^1\cap L^2$ and weak continuity on $\mathscr P(X)$, which determines $\mathsf H_t$ on $\mathscr P(X)$. Choosing $\mathsf H$ as anything else (e.g. the identity) does not satisfy the predicate, so the goal is not trivialized that way. Dropping the length property would change the statement.
• (3.15) is stated as "every Lipschitz constant $K$ of $f$ gives the Lipschitz constant $C(t)K$ of a version of $\mathsf P_tf$". (3.16) and the conclusions are in $[0,\infty]$; $W_2$ appears squared.
• Mass preservation is stated on $L^1\cap L^2$, where the heat flow is pinned.
• The paper states Theorem 3.5 as an equivalence; only the direction proved there is posed, the converse being cited from Kuwada.
• The paper prints Lemma 3.4 with an absolute value, which fails at $x=y$; the one-sided inequality its proof gives, and (3.26) uses, is the stated form.
• Lemma 3.3 assumes $f$ integrable; this only excludes the case $\int f\,d\mu=+\infty$, where the claim is trivial.

Contributions welcome: the quadratic Kantorovich duality on Polish spaces, Hopf–Lax calculus on length spaces, measurable selection of optimal plans, and the portmanteau-type Lemma 3.3.

Selected references

• L. Ambrosio, N. Gigli, G. Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Ann. Probab. 43(1), 2015. https://arxiv.org/abs/1209.5786
• K. Kuwada, Duality on gradient estimates and Wasserstein controls, J. Funct. Anal. 258, 2010. https://doi.org/10.1016/j.jfa.2010.01.010
• M.-K. von Renesse, K.-T. Sturm, Transport inequalities, gradient estimates, entropy, and Ricci curvature, Comm. Pure Appl. Math. 58, 2005. https://doi.org/10.1002/cpa.20060
• L. Ambrosio, N. Gigli, G. Savaré, Metric measure spaces with Riemannian Ricci curvature bounded from below, Duke Math. J. 163, 2014. https://arxiv.org/abs/1109.0222
• D. Bakry, M. Émery, Diffusions hypercontractives, Séminaire de Probabilités XIX, LNM 1123, 1985. https://doi.org/10.1007/BFb0075847

Motivation

Curvature bounds on a smooth Riemannian manifold control diffusion and the behavior of probability measures. Metric measure spaces extend these questions to limits that need not be smooth. A useful curvature condition must continue to hold when a sequence of spaces converges. Ambrosio, Gigli, and Savaré prove that their analytic Bakry–Émery curvature-dimension condition has this stability property for Riemannian energy measure spaces under Sturm–Gromov–Hausdorff convergence Ambrosio–Gigli–Savaré, Theorem 5.8. The result connects a condition stated through heat flow and Dirichlet forms with convergence stated through distances between probability measures.

The article's §5.2 first defines the convergence of spaces and of functions living in different $L^2$ spaces, then states the stability theorem. This order matters: the measure changes with the space, so ordinary convergence of functions on one fixed measured space cannot express the claim Ambrosio–Gigli–Savaré, Definitions 5.4 and 5.6.

Setting

A metric measure space $(X,d,m)$ consists of a complete separable metric space $(X,d)$ and a measure $m$. The class $\mathcal P_2(X)$ contains probability measures with finite second moment. The squared Wasserstein distance $W_2^2(\mu,\nu)$ is the infimum of the mean squared transport cost $d(x,y)^2$ over couplings of $\mu$ and $\nu$.

A sequence $(X_n,d_n,m_n)$ Sturm–Gromov–Hausdorff converges to $(X_\infty,d_\infty,m_\infty)$ when there is a complete separable ambient metric space $Z$ and distance-preserving embeddings $\iota_n:X_n\to Z$, including $\iota_\infty$, such that $W_2((\iota_n)_\#m_n,(\iota_\infty)_\#m_\infty)\to0$. The embeddings need not be onto. This definition compares measures on different spaces after placing them in one ambient space; it does not assume that the original spaces coincide Ambrosio–Gigli–Savaré, Definition 5.4.

An energy measure space has a strongly local Dirichlet form $\mathcal E$, its associated heat flow $P_t$, a carré du champ $\Gamma$, and an intrinsic distance $d_{\mathcal E}$ agreeing with $d$. The Cheeger energy $\operatorname{Ch}_m$ is the relaxed integral of one half the squared local slope. A Riemannian energy measure space also has the upper-regularity and continuous-representative properties of Definition 3.16. The paper writes $\mathcal E=2\operatorname{Ch}_m$ in this situation Ambrosio–Gigli–Savaré, Definitions 3.6 and 3.16 and Theorem 3.14.

The Bakry–Émery condition $\mathrm{BE}(K,N)$ bounds a second-order expression involving the heat flow, the carré du champ, curvature parameter $K$, and dimension parameter $N$. The formalization uses the paper's weak distributional form (2.33), writing $\nu=1/N\ge0$; $\nu=0$ represents $N=\infty$. This is the same $K$ and $N$ for every source space and for the limit Ambrosio–Gigli–Savaré, Definition 2.4 and (2.33).

Formalization targets

Supporting convergence results

Remark 5.5 asserts that the Cheeger energy is invariant under an isometric embedding. Lemma 5.7 supplies two criteria (squared norms, or entropies of bounded densities) for convergence of scalar functions across changing measures and shows that continuous maps of linear growth preserve this convergence. Lemma 5.9 says that, in the RCD setting, both heat-flow outputs and their generators converge. These are the mission's formal milestones Ambrosio–Gigli–Savaré, pp. 63–66.

Stability goal

For Riemannian energy measure spaces $(X_n,d_n,m_n,\mathcal E_n)$ with $m_n\in\mathcal P_2(X_n)$ and $\mathrm{BE}(K,N)$, Theorem 5.8 asks for

$$(X_n,d_n,m_n)\xrightarrow{\mathrm{SGH}}(X_\infty,d_\infty,m_\infty) \quad\Longrightarrow\quad (X_\infty,d_\infty,m_\infty,2\operatorname{Ch}_{m_\infty}) \text{ is Riemannian and satisfies }\mathrm{BE}(K,N).$$

The goal includes the assertion that the limit energy is a Dirichlet form; quadraticity is part of the conclusion. It covers finite $N$ and $N=\infty$ with the same statement Ambrosio–Gigli–Savaré, Theorem 5.8.

Significance

The theorem permits analytic curvature-dimension bounds to survive convergence even when the carrier spaces, measures, and $L^2$ spaces vary. Without a stability statement, a bound verified separately on approximating spaces would give no such bound for their metric measure limit. The theorem also ensures that the limit Cheeger energy retains the quadratic structure required for the Riemannian theory Ambrosio–Gigli–Savaré, Theorem 5.8 and its proof.

The result is proved in the cited paper. The remaining work here is a machine-checked development of its definitions and proof, including the convergence of heat flows and generator terms across changing measures. The statements in this proposal are proof targets; they are not presented as already machine-checked. The definitions of SGH convergence and graph-law convergence can also support other stability questions for metric measure spaces.

Difficulty

The difficulty is that each $P_t^n$ acts on a different $L^2(X_n,m_n)$, while $\mathrm{BE}(K,N)$ is an inequality involving the semigroup, its generator, and integrals against $m_n$. Convergence of the underlying measures alone does not imply convergence of those functions or of their squared terms. In particular, pointwise convergence on a common carrier is not even a statement available before choosing embeddings and representatives. The paper's separate notion of function convergence addresses this gap Ambrosio–Gigli–Savaré, Definitions 5.4 and 5.6 and Lemma 5.9.

Formalization scope

Lean keeps the spaces indexed by $n$: Xn n, m n, E n, and P n. The goal uses SGH convergence as an existential ambient realization, rather than assuming the paper's common-space reduction (5.10). The source heat flows and the truncation profile $S$ are named by their defining properties; they are the paper's determined objects. The limit heat flow is not assumed to exist: the $\mathrm{BE}(K,N)$ conclusion is stated for every family satisfying the heat-flow characterization of $2\operatorname{Ch}_{m_\infty}$. Functions represent $L^2$ classes, and the common Setting layer records almost-everywhere invariance. The measurable spaces are Borel; the paper's completed measurable structures are represented through measurable versions and almost-everywhere relations.

The formal goal assumes that $m_\infty$ has full support on $X_\infty$. Definition 3.6 requires this, while §5.2 explicitly warns that the ambient SGH limit may fail to be fully supported. The full-support condition makes the theorem refer to the intended limit carrier. The goal does not assume that the limit already is a Riemannian energy measure space or satisfies $\mathrm{BE}(K,N)$.

Function convergence uses graph laws on $X\times\mathbb R^k$. The chosen product metric is Mathlib's max metric; any fixed finite product metric yields the same $W_2$ convergence in this setting. The squared Wasserstein distance is extended nonnegative, so a missing finite coupling does not turn into a false real value. The limit energy is defined as $2\operatorname{Ch}_{m_\infty}$, with no free energy parameter. Measurable representatives are explicit when forming pushforwards. Lemma 5.9 is stated on a common, fully supported RCD carrier; this narrows its ambient application and is recorded for review. Contributions to the Cheeger-energy invariance, changing-measure function convergence, heat-flow stability, and final BE passage are all within scope.

Selected references

• Luigi Ambrosio, Nicola Gigli, Giuseppe Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Annals of Probability 43(1), 2015, 339–404. arXiv:1209.5786v4, DOI:10.1214/14-AOP907.

Why barycenters of histograms matter

A barycenter summarizes several objects by minimizing a weighted sum of distances to them. For probability histograms, ordinary coordinatewise averages depend strongly on how the bins are labeled. Optimal transport instead lets mass move between bins and charges for those moves through a cost matrix. The resulting Wasserstein barycenter can reflect the geometry of the bins: nearby bins can exchange mass at a lower cost than distant ones. Peyré and Cuturi use this construction in their treatment of variational transport problems, including shape interpolation and the representation of a measure as a barycenter of other measures. The finite histogram problem in this mission is the entropically regularized version developed in §9.2 of their textbook.

The computational question is how to connect three ways of describing the same solution: a histogram that is the barycenter, transport matrices coupling it to the inputs, and vectors of dual potentials. Proposition 9.1 on p. 530 identifies the dual potentials behind the scaling factors of the optimal transport matrices. This is the second proposition numbered 9.1 in the chapter; the one on p. 519 concerns derivatives with respect to histograms.

Finite histogram setting

There are $S$ input histograms. Source $s$ has $n_s$ bins and a probability vector $b_s$, while the barycenter has $n$ bins. The real matrix $C_s\in\mathbb R^{n\times n_s}$ gives the cost of transporting a unit of mass from barycenter bin $i$ to input bin $j$. A weight vector $\lambda\in\Sigma_S$ has nonnegative entries summing to one; $\Sigma_k$ denotes the probability simplex on $k$ bins. The unregularized barycenter problem (9.10) minimizes $\sum_s\lambda_s L_{C_s}(a,b_s)$ over $a\in\Sigma_n$, where $L_{C_s}$ is the minimum transport cost with marginals $a$ and $b_s$.

For a regularization parameter $\varepsilon>0$, the entropic transport cost $L^\varepsilon_{C_s}(a,b_s)$ minimizes $\langle C_s,P_s\rangle-\varepsilon H(P_s)$ over nonnegative coupling matrices $P_s$ with row marginal $a$ and column marginal $b_s$. Here $\langle C_s,P_s\rangle=\sum_{i,j}C_{s,ij}P_{s,ij}$ and $H(P_s)=\sum_{i,j}(-P_{s,ij}\log P_{s,ij}+P_{s,ij})$, with $0\log0=0$. The Gibbs kernel is $K_{s,ij}=e^{-C_{s,ij}/\varepsilon}$.

The book also writes the regularized barycenter as a weighted KL projection. Its variables are the matrices $(P_s)_s$; each matrix has column marginal $b_s$, and every matrix has the same row marginal. That shared row marginal is $a$, so the optimization can be expressed without carrying $a$ as a separate variable. The generalized matrix divergence is $\mathrm{KL}(P_s\mid K_s)=\sum_{i,j}[P_{s,ij}\log(P_{s,ij}/K_{s,ij})-P_{s,ij}+K_{s,ij}]$, using the continuous value at $P_{s,ij}=0$. See (9.15)–(9.17) in Peyré and Cuturi.

Formalization targets

The goal is Proposition 9.1 on p. 530. The dual variables are row potentials $f_s\in\mathbb R^n$ and column potentials $g_s\in\mathbb R^{n_s}$. They maximize

$$\sum_s\lambda_s\left[\langle g_s,b_s\rangle-\varepsilon\sum_{i,j}e^{f_{s,i}/\varepsilon}K_{s,ij}e^{g_{s,j}/\varepsilon}\right] \quad\text{subject to}\quad \sum_s\lambda_s f_s=0.$$

The theorem asserts that the primal and dual optima are attained, that every optimal primal family and every optimal dual family satisfy

$$P_{s,ij}=e^{f_{s,i}/\varepsilon}K_{s,ij}e^{g_{s,j}/\varepsilon},$$

and that the dual maximum is the minimum value of the entropic barycenter objective (9.15). The milestone targets are the scalar and matrix versions of the KL conjugate (9.22), followed by the closed form maximizer of one $g_s$ block, corresponding to the update (9.18). These statements retain the source's finite matrix setting and are listed in the order in which their concepts enter the dual formulation.

What the result supplies

The scaling formula turns the optimal couplings into a product of a row factor, a fixed positive kernel, and a column factor. It identifies those factors with exponentials of dual potentials and gives a constrained maximization problem whose value is the entropic barycenter cost. Thus a solver can reason about the couplings, the barycenter marginal, or the potentials while referring to one theorem that connects them. The book uses the same variables to describe the iterative scaling updates on pp. 529–531 and later illustrates barycenters of shapes and surface measures; those applications depend on interpreting the matrix factors correctly. Peyré and Cuturi give the mathematical proposition and its argument. A complete Lean proof of the proposition and its supporting KL identities is the work this mission calls for; the statements here are draft targets rather than machine-checked solutions.

Where the difficulty lies

The potential program is a constrained optimization problem, while the transport problem constrains nonnegative matrices by two kinds of marginals. Equality of their optimum values must preserve the normalization constants in generalized KL. The exponential form alone does not establish that a proposed matrix has the required marginals, nor does a feasible matrix alone identify dual potentials. In addition, the assertion concerns every optimizer: a choice of zero source weight would leave that source's coupling unconstrained by the objective, and a zero target entry would put a logarithmic column update on the boundary. These are substantive edge cases of the formulas, not merely notation.

Formalization scope

Lean uses Fin S, Fin n, and Fin (n_s) for the finite index sets; these are zero based versions of the book's one based indices. Histograms and potentials are real vectors, costs and couplings are real matrices, and the Gibbs kernel is defined entrywise. The theorem requires $S,n,n_s>0$, $\varepsilon>0$, strictly positive weights $\lambda_s$ that sum to one, and strictly positive input histograms $b_s$ that each sum to one. The strict positivity of weights and input entries is an explicit restriction beyond (9.15)–(9.21), needed for a statement about every optimizer and finite logarithmic potentials. Entropy uses $0\log0=0$ on nonnegative couplings. The shared row marginal is constructed by the constraints on the $P_s$; it is not a free histogram unrelated to them.

The definition layer includes finite matrix pairing, entropy, generalized KL, the Gibbs kernel, feasibility, and primal and dual objective functions. The KL conjugate identities and the block optimizer are separate theorem targets so they can be reused in other entropic transport developments. The main theorem asserts primal and dual attainment as well as their relationship; it does not assume strong duality or an optimal scaling as an input. The page has slips in the dimensions of the marginal equations and a missing subscript on $K$ in (9.17); the Lean statements use the dimensions specified by $P_s\in\mathbb R^{n\times n_s}$. The optional cost-gradient Proposition 9.2 on pp. 519–520 and the $f_s$ block update (9.19)–(9.20) lie outside this proposal.

Selected references

• Gabriel Peyré and Marco Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. DOI: 10.1561/2200000073.

Motivation

Optimal transport compares two distributions by finding the least expensive way to move mass between them. For finite histograms, the resulting linear program is precise but its optimal coupling can be sparse. In applications where the coupling represents traffic, matching, or a differentiable loss, a sparse plan may be undesirable or expensive to compute repeatedly. Peyré and Cuturi describe how adding an entropy term selects a diffuse coupling and leads to matrix scaling algorithms that can be used on large finite problems (Peyré and Cuturi, 2019, Chapter 4).

The entropic dual gives a second view of the same regularized problem. Its variables are real vectors attached to the two marginal constraints. Unlike the ordinary Kantorovich dual, the objective has no explicit feasibility constraints and is smooth. This permits calculations in the log domain, which the book introduces because direct scaling with exponentials can suffer from numerical overflow or underflow when the regularization parameter is small relative to the costs (Peyré and Cuturi, 2019, §4.4). This mission targets the exact relationship between the regularized minimum, the smooth dual maximum, and the scaling factors.

Setting

Fix positive integers $n,m$. A histogram $a\in\Sigma_n$ is a vector with nonnegative entries summing to one; $b\in\Sigma_m$ is defined similarly. Strict positivity is required for the attained dual maximum and log-domain updates; the primal scaling and Kantorovich-feasibility statements also cover zero-entry histograms. A coupling $P\in U(a,b)$ is an $n\times m$ matrix with nonnegative entries, row sums $a$, and column sums $b$. A real matrix $C$ assigns cost $C_{ij}$ to each transfer from row $i$ to column $j$, and $\langle C,P\rangle=\sum_{i,j}C_{ij}P_{ij}$ is its transport cost.

The book uses the entropy $H(P)=-\sum_{i,j}P_{ij}(\log P_{ij}-1)$, with $0\log0=0$. For $\varepsilon>0$, the regularized cost is $L_C^\varepsilon(a,b)=\min_{P\in U(a,b)}\{\langle C,P\rangle-\varepsilon H(P)\}$. The Gibbs kernel has entries $K_{ij}=\exp(-C_{ij}/\varepsilon)$. Given potentials $f\in\mathbb R^n$ and $g\in\mathbb R^m$, the smooth dual objective is $Q(f,g)=\langle f,a\rangle+\langle g,b\rangle-\varepsilon\sum_{i,j}e^{f_i/\varepsilon}K_{ij}e^{g_j/\varepsilon}$. These are the finite-dimensional objects of (4.1), (4.2), and (4.30) in the source (Peyré and Cuturi, 2019, pp. 425, 428, 448).

Formalization targets

Attained entropic duality

The goal is Proposition 4.4. There are an optimal coupling $P$ and potentials $(f,g)$ at which the dual reaches its maximum, with the common value

$$L_C^\varepsilon(a,b) =\langle C,P\rangle-\varepsilon H(P) =\max_{f',g'} Q(f',g').$$

For every maximizing pair $(f',g')$, the same optimal coupling satisfies

$$P_{ij}=e^{f'_i/\varepsilon}K_{ij}e^{g'_j/\varepsilon}.$$

Thus the dual potentials determine the scaling vectors $u=e^{f'/\varepsilon}$ and $v=e^{g'/\varepsilon}$ in (4.12). The maximum is an attained maximum of a real function, as stated in the book, rather than an unrestricted real infimum or supremum that might take a default value on a bad input (Peyré and Cuturi, 2019, Proposition 4.4).

Supporting results

The milestones follow the source's statements. Proposition 4.3 gives existence, uniqueness, and the Gibbs scaling of the primal optimizer. Remark 4.21 gives the two partial-gradient formulas and the closed log-domain block updates. Proposition 4.5 states that an entropic dual maximizer is a feasible pair of ordinary Kantorovich potentials, so its linear objective is bounded above by the unregularized cost $L_C(a,b)$ (Peyré and Cuturi, 2019, pp. 432, 449, 452–453).

Significance

The equality establishes that the matrix scaling variables and the dual potentials describe the same optimal coupling. It lets a computation based on scaling be interpreted as maximizing a smooth objective, and it gives exact marginal-error expressions through the dual gradients. Feasible Kantorovich potentials obtained at the optimum also provide a lower bound on the ordinary transport cost. These statements explain why log-domain updates represent the same mathematical problem as entropic transport, even when direct exponentiation is numerically fragile (Peyré and Cuturi, 2019, §§4.4–4.5).

The results are established in the textbook; the open work here is their Lean formalization. A completed development would provide reusable finite coupling, entropy, Gibbs-kernel, and smooth-dual interfaces, together with the existence and differentiability results needed to connect them. It would also distinguish a primal optimum, a dual maximum, and a feasible potential without relying on informal convention. The mission does not assert that these textbook results are new, and no machine-checked proof of these exact statements is claimed here.

Difficulty

The unconstrained dual objective has a symmetry: shifting every coordinate of $f$ by one constant and every coordinate of $g$ by its negative leaves the value unchanged. Consequently, the set of maximizers is not bounded in the ordinary product space. Positivity of the marginals matters for attaining a maximum with finite real potentials; if a marginal entry is zero, the corresponding potential can escape toward negative infinity. On the primal side, the entropy formula must be valid at zero entries even though optimality links it to strictly positive exponential scalings. The formal argument must connect these boundary conventions and the finite-dimensional optimization statements without turning the maximum into a junk real supremum (Peyré and Cuturi, 2019, Proposition 4.4 and Remark 4.21).

Formalization scope

The Lean development represents indices by Fin n and Fin m, matrices by Matrix (Fin n) (Fin m) ℝ, and histograms by Mathlib's stdSimplex. Positive dimensions and $\varepsilon>0$ appear throughout. Strictly positive marginal entries are required for the attained dual maximum and log-domain updates; the other statements permit zero entries. The book assumes positive weights for discrete measures in Remark 2.1; the marginal positivity is also required for the attained dual maximum and the logarithmic updates. The cost matrix itself may have arbitrary real entries. Entropy uses Real.negMulLog, which implements $0\log0=0$ on the nonnegative couplings where it is applied.

The primal optimum is a predicate on a coupling and its objective, rather than a chosen matrix. The unregularized $L_C$ is a real infimum used only when simplex marginals make its feasible set nonempty and bounded. The dual objective is a finite sum. Its gradients are stated as one-variable derivatives in each coordinate, and each block update is characterized as the unique maximizer with the other block fixed. The complete development needs Mathlib's finite sums, real exponential and logarithm, calculus, finite-dimensional topology, and optimization facts. Contributions that establish these shared interfaces or the four milestone statements are in scope.

Propositions 4.7 and 4.8 are excluded from this proposal because their printed bounds compare a dual linear objective with $L_C^\varepsilon$ where the accompanying arguments instead support a comparison with the unregularized $L_C$; (4.47) also has a sign discrepancy. The milestone list therefore avoids encoding a false inequality (Peyré and Cuturi, 2019, pp. 453–454).

Selected references

• Gabriel Peyré and Marco Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6), 2019, pp. 355–607. DOI: 10.1561/2200000073.

Why ask whether a Wasserstein distance is Hilbertian

Kernel methods, multidimensional scaling and low-distortion embeddings all work best on data whose distance comes from a Hilbert space. A distance $d$ on a set $\mathcal Z$ is Hilbertian when $\mathcal Z$ can be mapped into a Hilbert space so that $d$ becomes the norm distance; for such a $d$, the kernel $e^{-d^p/t}$ is positive definite for $0\le p\le 2$ and $t>0$ (Berg, Christensen and Ressel, 1984), and the classical Euclidean toolbox applies. Optimal transport distances are popular for comparing probability measures, so it is natural to ask whether they are Hilbertian. In dimension one the answer is yes for $\mathcal W_2$: the map sending a measure to its quantile function is an isometry into $L^2([0,1])$, and between univariate Gaussians $\mathcal W_2$ is the Euclidean distance between (mean, standard deviation). Peyré and Cuturi, Computational Optimal Transport (FnT ML 2019), §8.3, show that this does not extend to the plane: for $p=1,2$ and $d\ge2$ the $p$-Wasserstein distance on $\mathbb R^d$ is not Hilbertian (Proposition 8.2, p. 507).

The tool is a classical characterization. Schoenberg (1938) proved that a distance is Hilbertian exactly when its square is conditionally negative definite; Berg, Christensen and Ressel (1984, Prop. 3.2) give the modern form. The easy direction turns non-embeddability into a finite check, and the book's proof of Proposition 8.2 performs that check numerically on 35 measures supported on the four corners of the unit square (Figure 8.6, p. 508). Stronger, quantitative statements are known: planar $\mathcal W_1$ does not even embed into $L^1$ with bounded distortion (Naor and Schechtman, 2007), and Andoni, Naor and Neiman (2018) study which powers of Wasserstein distances embed.

Setting

Let $\mathcal Z$ be a set. A function $\varphi:\mathcal Z\times\mathcal Z\to\mathbb R$ is negative definite (Definition 8.3, p. 501, in the conditional form used in §8.3) if it is symmetric and, for every $n\ge0$, every $x_1,\dots,x_n\in\mathcal Z$ and every $r\in\mathbb R^n$ with $\sum_ir_i=0$,

$$\sum_{i,j=1}^n r_ir_j\,\varphi(x_i,x_j)\le0 .$$

A function $d:\mathcal Z\times\mathcal Z\to\mathbb R$ is Hilbertian (Definition 8.4, p. 506) if there are a real Hilbert space $\mathcal H$ and a map $\phi:\mathcal Z\to\mathcal H$ with $d(z,z')=\|\phi(z)-\phi(z')\|_{\mathcal H}$ for all $z,z'$.

On $\mathbb R^d$ with the Euclidean norm $\|\cdot\|_2$, let $\mathcal P_p(\mathbb R^d)$ be the Borel probability measures $\mu$ with $\int\|x\|_2^p\,d\mu<\infty$. A coupling of $\mu$ and $\nu$ is a measure $\pi$ on $\mathbb R^d\times\mathbb R^d$ whose two marginals are $\mu$ and $\nu$, and the $p$-Wasserstein distance (2.18) is

$$\mathcal W_p(\mu,\nu)=\Big(\inf_{\pi}\int\|x-y\|_2^p\,d\pi(x,y)\Big)^{1/p},$$

finite on $\mathcal P_p(\mathbb R^d)$. For points $x_1,\dots,x_n$ and a histogram $a\in\Sigma_n$ (nonnegative, summing to one) the discrete measure is $\sum_ia_i\delta_{x_i}$; for two histograms $a,b$, $U(a,b)$ is the set of nonnegative matrices with row sums $a$ and column sums $b$, and $L_C(a,b)=\min_{P\in U(a,b)}\sum_{i,j}C_{i,j}P_{i,j}$ (2.11).

The configuration of the book's proof consists of the corners $x^1=[0,0]$, $x^2=[1,0]$, $x^3=[0,1]$, $x^4=[1,1]$ of the unit square, the 35 histograms of $\Sigma_4$ with entries in $\{0,\tfrac14,\tfrac12,\tfrac34,1\}$, and the centering matrix $J=I_n-\tfrac1n\mathbb 1_{n,n}$.

Formalization targets

Goal: Proposition 8.2

For $d\ge2$ and $p\in\{1,2\}$,

$$\mathcal W_p \text{ on } \mathcal P_p(\mathbb R^d) \text{ is not Hilbertian.}$$

Milestones

1. Proposition 8.1, proved direction (pp. 506–507): if $d$ is Hilbertian then $d^2$ is negative definite.
2. Squared distance (p. 507): $\mathcal W_p^2$ on $\mathcal P_p(\mathbb R^d)$ is not negative definite, $d\ge2$, $p=1,2$.
3. Reduction to the plane (proof of Prop. 8.2): if $\mathcal W_p^2$ on $\mathcal P_p(\mathbb R^d)$, $d\ge2$, were negative definite, so would be $\mathcal W_p^2$ on $\mathcal P_p(\mathbb R^2)$.
4. Discrete measures (Remark 2.13, p. 375): $\mathcal W_p\big(\sum_ia_i\delta_{x_i},\sum_jb_j\delta_{x_j}\big)^p=L_C(a,b)$ with $C_{i,j}=\|x_i-x_j\|_2^p$.
5. Centering criterion (proof of Prop. 8.2): a matrix $M$ admits a zero-sum $r$ with $r^\top Mr>0$ if and only if $JMJ$ has a positive eigenvalue.
6. The grid counterexample (proof of Prop. 8.2, Figure 8.6): for $p=1,2$ there are grid histograms $a^1,\dots,a^n$ and a zero-sum $r$ with

$$\sum_{i,j}r_ir_j\,\mathcal W_p^2\Big(\sum_k a^i_k\delta_{x^k},\sum_k a^j_k\delta_{x^k}\Big)>0.$$

Significance

A Hilbertian distance gives positive definite Gaussian and Laplace kernels, Euclidean multidimensional scaling and Johnson–Lindenstrauss dimension reduction for free. Proposition 8.2 says none of these can be obtained for $\mathcal W_1$ or $\mathcal W_2$ on $\mathbb R^d$, $d\ge2$, by an isometric embedding; this is why the literature turned to approximate embeddings, sliced distances and entropic surrogates (pp. 507–508). The negative-definiteness test of milestone 1 is a reusable certificate for non-embeddability of any finite metric.

The result is known, and the book's proof is a floating-point eigenvalue computation. The formal content of this mission is a machine-checked proof with an exact certificate: rational or algebraic Wasserstein distances between explicit discrete measures and an explicit zero-sum vector. As far as this mission is aware, no formal proof of the statement exists in Mathlib or on the platform. Schoenberg's converse is cited by the book and is not part of the mission.

Difficulty

The abstract part is short: expanding $\|\phi(z_i)-\phi(z_j)\|^2$ and using $\sum_ir_i=0$ gives milestone 1. The obstacle is the certificate. The book observes that $J\mathbf D_p^2J$ has a positive top eigenvalue (about $1.2$ for $p=1$ and $0.7$ for $p=2$), but a proof needs exact transport costs between the chosen measures, each the value of a small linear program whose optimality has to be established (for instance by a dual certificate), together with a vector $r$ for which the quadratic form is provably positive. For $p=1$ the costs involve $\sqrt2$, the diagonal of the square. A second, separate difficulty is connecting the measure-theoretic $\mathcal W_p$ to the discrete program (milestone 4) and transporting a counterexample from $\mathbb R^2$ into $\mathbb R^d$ (milestone 3), both of which require working with couplings as measures on a product space.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin d); $\mathcal W_p$ is the published definition WassersteinDRO.Duality.wassersteinDistance (an $[0,\infty]$-valued infimum over all measures with the two marginals, raised to $1/p$), converted to a real number. The distance is considered on $\mathcal P_p(\mathbb R^d)$, the set where it is finite; outside it the real conversion is a junk $0$. The book names no domain; since the counterexample consists of finitely supported measures, the finite computation gives non-Hilbertianity on $\mathcal P_p$ and on every smaller set containing those measures.
• Negative definiteness is conditional. Definition 8.3 as printed quantifies over all $r$; under that reading no nonzero squared distance is negative definite, so Proposition 8.1 would be false and "not negative definite" trivially true. The zero-sum condition, used by the book in the proof of Proposition 8.1, is part of the definition; this rules out the trivial formalization.
• Hilbert spaces are real, complete inner-product spaces in the universe of $\mathcal Z$. Indices are 0-based (Fin n). Histograms are real vectors; the reduction milestone is stated for every $p\ge1$.
• Discrete transport objects ($U(a,b)$, $L_C$) are redefined in this mission's namespace CompOT.NotHilbertian, duplicating chunk II of the series.

Contributions welcome: the forward direction of Schoenberg's characterization, the discrete-measure bridge (reusable wherever discrete optimal transport meets measure-theoretic couplings), the isometric-embedding invariance of $\mathcal W_p$, and exact certificates for the grid computation.

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
• I. J. Schoenberg, Metric spaces and positive definite functions, Transactions of the AMS 44(3):522–536, 1938. https://doi.org/10.1090/S0002-9947-1938-1501980-0
• C. Berg, J. P. R. Christensen and P. Ressel, Harmonic Analysis on Semigroups, Graduate Texts in Mathematics 100, Springer, 1984. https://doi.org/10.1007/978-1-4612-1128-0
• A. Naor and G. Schechtman, Planar earthmover is not in $L_1$, SIAM Journal on Computing 37(3):804–826, 2007. https://doi.org/10.1137/05064206X
• A. Andoni, A. Naor and O. Neiman, Snowflake universality of Wasserstein spaces, Annales scientifiques de l'École normale supérieure 51(3):657–700, 2018. https://arxiv.org/abs/1509.08677

Motivation

Discrete optimal transport between two histograms is a linear program. Its feasible set, the transportation polytope, has been studied since Hitchcock (1941) and Kantorovich, and the structure of its vertices underlies the classical algorithms for the problem: the north-west corner rule produces a vertex, and the network simplex moves from vertex to vertex. A linear program with a nonempty bounded feasible set attains its minimum at a vertex, so knowing what vertices look like tells us what optimal transport plans can be assumed to look like.

This mission is the fourth of a series formalizing G. Peyré and M. Cuturi, Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019). It covers §3.4.1 of the book, Tree Structure of the Support of All Vertices of U(a, b) (pp. 405–407), whose single numbered result, Proposition 3.4, states that the support of a vertex is a forest. The book credits the result to Brualdi, Combinatorial Matrix Classes (2006, Theorem 8.1.2).

Setting

Fix integers $n, m$ and histograms $a \in \Sigma_n$, $b \in \Sigma_m$. The transportation polytope is

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

the set of nonnegative $n\times m$ matrices whose row sums are $a_1,\dots,a_n$ and whose column sums are $b_1,\dots,b_m$. Histograms are nonnegative and sum to one; $U(a,b)$ is the set of couplings between them. The cost of a plan $P$ for a cost matrix $C$ is $\langle C, P\rangle = \sum_{i,j} C_{ij}P_{ij}$.

A point $x$ of a set $S$ is an extremal point (vertex) of $S$ if, whenever $y, z \in S$ and $x = (y+z)/2$, necessarily $x = y = z$.

Take $n$ source nodes $V = \{1,\dots,n\}$ and $m$ target nodes $V' = \{1',\dots,m'\}$. The complete bipartite graph between them has the $nm$ edges $(i, j')$. For a matrix $P$, the support $S(P)$ is the set of edges $(i,j')$ with $P_{ij} > 0$, and the support graph is $G(P) = (V\cup V', S(P))$. A transport plan is a flow on the complete bipartite graph, with $a_i$ leaving node $i$ and $b_j$ entering node $j'$; $G(P)$ records the edges the flow actually uses.

Formalization targets

Goal: Proposition 3.4 (p. 406)

If $P$ is an extremal point of $U(a,b)$, then

$$G(P) \text{ has no cycles}\qquad\text{and}\qquad \#\{(i,j) : P_{ij}\ne 0\} \le n + m - 1 .$$

Milestones (proof of Proposition 3.4, p. 407)

1. If $G(P)$ has a cycle, there is a nonzero matrix $E$ with $E\mathbb 1_m = 0$, $E^\top\mathbb 1_n = 0$, and $E_{ij} \ne 0 \Rightarrow P_{ij} > 0$.
2. For such an $E$ and $P \in U(a,b)$, both $P + tE$ and $P - tE$ lie in $U(a,b)$ for some $t > 0$.
3. A graph with $k$ nodes and no cycles has at most $k-1$ edges.
4. For $P \ge 0$, the edges of $G(P)$ correspond one-to-one to the nonzero entries of $P$.

Companion (§3.4, p. 405)

For $a \in \Sigma_n$, $b \in \Sigma_m$ and any cost $C$, some minimizer of $\langle C, P\rangle$ over $U(a,b)$ is an extremal point of $U(a,b)$.

Significance

Proposition 3.4 is the sparsity statement of discrete optimal transport: a vertex of $U(a,b)$ moves mass along at most $n+m-1$ source–target pairs, out of $nm$ possible. With the companion, some optimal plan is that sparse. This is what makes the network simplex method a combinatorial algorithm on spanning trees of the bipartite graph (§3.5 of the book), and it is the reason the north-west corner rule (§3.4.2) can produce a feasible vertex with a tree support. The same fact, specialized to $n = m$ and uniform histograms, is one step on the way from Kantorovich's relaxation back to Monge's assignment problem.

The result is classical and proved; it has not, to our knowledge, been formalized. Mathlib has the transportation polytope only implicitly (no dedicated definition), and it has the edge count of trees (SimpleGraph.IsTree.card_edgeFinset) but not the corresponding bound for forests. The mission produces a machine-checked link between the convex geometry of $U(a,b)$ and the combinatorics of its support graph, reusable by later missions of the series on the network simplex and on the assignment problem.

Difficulty

The convex-geometric half is elementary; the work is in the passage between a cycle of a graph and a matrix. The cycle is an object of Mathlib's graph library (a closed walk with distinct vertices in a graph on $V \sqcup V'$), while the perturbation is a matrix indexed by $V \times V'$. An informal picture of a cycle as a list of edges hides what the matrix statement needs: each source and each target must be visited at most once, and Mathlib's cycles are walks whose distinctness conditions have to be carried to the matrix level.

The edge bound for forests is not packaged in Mathlib either: it counts the edges of a tree, a connected acyclic graph, while the support graph of a vertex is in general disconnected, and the empty graph must be handled.

Formalization scope

All objects live in the namespace CompOT.Vertices. Indices are Fin n and Fin m (0-based; the book's $[\![n]\!] = \{1,\dots,n\}$). Matrices are Matrix (Fin n) (Fin m) ℝ, and $U(a,b)$ is the set of matrices with nonnegative entries, row sums $a$ and column sums $b$. Extremality is the book's midpoint definition, relative to the set: the points $y, z$ in $x = (y+z)/2$ range over $U(a,b)$ only. This rules out the trivializing reading in which $y, z$ range over all matrices (no point would then be extremal and the goal would be vacuous); conversely, the sanity file shows a non-extremal coupling, so extremality is not automatic either.

The support graph is a SimpleGraph (Fin n ⊕ Fin m) with Sum.inl i adjacent to Sum.inr j exactly when $P_{ij} > 0$ and no other adjacencies. The book calls the edges $(i,j')$ directed, but the cycles of its proof alternate between sources and targets, so "no cycles" is Mathlib's SimpleGraph.IsAcyclic of this undirected graph. The number of nonzero entries is the cardinality of $\{(i,j) : P_{ij} \ne 0\}$.

The goal, feasibility milestone and companion carry $a \in \Sigma_n$, $b \in \Sigma_m$, the book's standing notation for histograms (p. 360). These hypotheses make the index sets nonempty, so natural-number subtraction in the bound $n+m-1$ agrees with the book's integer expression.

Useful infrastructure, reusable beyond this mission: the forest edge bound for finite simple graphs, and the correspondence between cycles of a bipartite graph and signed matrices with zero line sums. Contributions of either as standalone lemmas are welcome.

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
• R. A. Brualdi, Combinatorial Matrix Classes, Cambridge University Press, 2006, §8.1. https://doi.org/10.1017/CBO9780511721182
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 2.7.
• F. L. Hitchcock, The distribution of a product from several sources to numerous localities, Journal of Mathematics and Physics 20:224–230, 1941. https://doi.org/10.1002/sapm1941201224