Optimal Transport

Decisions with covariate information

Many operational decisions are made after observing covariates that carry information about the uncertainty: a retailer sets inventory after seeing weather and calendar features that predict demand, a grid operator commits generation after seeing a load forecast. The decision problem is a conditional stochastic program: choose $z\in\mathcal Z$ to minimize $\mathbb E[c(z,Y)\mid X=x]$, where $Y$ is the uncertain quantity, $X$ the covariates and $x$ their observed value. The conditional distribution of $Y$ given $X=x$ is unknown; only joint data $\{(y^i,x^i)\}_{i=1}^n$ are available (Bertsimas and Kallus, 2020).

Kannan, Bayraksan and Luedtke (arXiv:2207.13554) proposed fitting a regression model and adding its empirical residuals to the point prediction at $x$, producing scenarios for a sample average approximation (the ER-SAA). With few data, any such sample average is optimistically biased: the optimal value underestimates the true cost of the chosen decision. Distributionally robust optimization (DRO) over a Wasserstein ball corrects this bias in the covariate-free case, where Mohajerin Esfahani and Kuhn (2018) showed that a suitably sized ball turns the DRO optimal value into an upper confidence bound on the out-of-sample cost. The paper formalized here (Kannan, Bayraksan and Luedtke, 2023) extends that guarantee to the residuals-based setting. Its main result, Theorem 7, is this mission's goal.

Setting

Let $\mathcal X=\mathbb R^{d_x}$, and give $\mathbb R^{d_y}$ and $\mathbb R^{d_z}$ the Euclidean norm $\|\cdot\|$. The model is

$$Y=f^*(X)+\varepsilon,$$

with regression function $f^*$ and zero-mean errors $\varepsilon\sim P_\varepsilon$ independent of $X$. The conditional distribution $P_{Y\mid X=x}$ is then the law of $f^*(x)+\varepsilon$. Let $c:\mathbb R^{d_z}\times\mathbb R^{d_y}\to\mathbb R$ be a cost and $\mathcal Z$ a nonempty compact feasible set. The true objective is $g(z;x)=\mathbb E[c(z,f^*(x)+\varepsilon)]$.

A known nonempty closed convex set $\mathcal Y\supseteq$ range of $Y$ is given, with orthogonal projection $\mathrm{proj}_{\mathcal Y}$ (the nearest-point map). The data are covariates $x^i$ and errors $\varepsilon^i$, with responses $y^i=f^*(x^i)+\varepsilon^i$ for $i\in[n]$. A regression estimate $\hat f_n$ built from the data has empirical residuals $\hat\varepsilon^i_n=y^i-\hat f_n(x^i)$. Two empirical distributions are compared: the true empirical distribution $P^*_n(x)$, which needs $f^*$, and the estimated empirical distribution $\hat P^{ER}_n(x)$, which is computable:

$$P^*_n(x)=\frac1n\sum_{i=1}^n\delta_{f^*(x)+\varepsilon^i},\qquad \hat P^{ER}_n(x)=\frac1n\sum_{i=1}^n\delta_{\mathrm{proj}_{\mathcal Y}(\hat f_n(x)+\hat\varepsilon^i_n)}.$$

Their scenarios differ by $\tilde\varepsilon^i_n(x)=(\hat f_n(x)-f^*(x))+(f^*(x^i)-\hat f_n(x^i))$, the prediction error at $x$ plus the estimation error at $x^i$.

For $p\in[1,\infty)$ the $p$-Wasserstein distance is $d_{W,p}(Q_1,Q_2)=\big(\inf_{\pi}\int\|y_1-y_2\|^p\,d\pi\big)^{1/p}$, with the infimum over couplings $\pi$ of $Q_1$ and $Q_2$. The ER-DRO problem (8) with radius $\zeta$ is

$$\hat v^{DRO}_n(x)=\min_{z\in\mathcal Z}\ \sup\Big\{\mathbb E_{Y\sim Q}[c(z,Y)]:\ Q\in\mathcal P(\mathcal Y),\ d_{W,p}(Q,\hat P^{ER}_n(x))\le\zeta\Big\},$$

with optimal solution $\hat z^{DRO}_n(x)$.

The radius (10) combines two allowances:

• Assumption 2 bounds the regression error: with probability at least $1-\alpha$, $\|f^*(x)-\hat f_n(x)\|^p$ and $\frac1n\sum_i\|f^*(x^i)-\hat f_n(x^i)\|^p$ are each at most $\kappa^p_{p,n}(\alpha,x)$.
• Lemma 2, quoted from Fournier and Guillin (2015), is an exponential concentration bound for $d_{W,p}(P^*_n(x),P_{Y\mid X=x})$ with constants $c_1,c_2$. It holds under the light-tail Assumption 1, $\mathbb E[\exp(\|\varepsilon\|^a)]<\infty$ for some $a>p$.

The radius is $\zeta_n(\alpha,x)=2\kappa_{p,n}(\alpha/4,x)+\kappa^{(2)}_{p,n}(\alpha)$. Its second term inverts Lemma 2 at level $\alpha/2$.

Formalization targets

Goal: Theorem 7 (finite sample certificate guarantee)

Under Assumptions 1 and 2 at $x$, $p\ne d_y/2$, i.i.d. errors, Lemma 2's bound with constants $c_1,c_2>0$ and $\alpha\in(0,1)$, the ER-DRO problem with radius $\zeta_n(\alpha,x)$ satisfies

$$\mathbb P\big\{g(\hat z^{DRO}_n(x);x)\le\hat v^{DRO}_n(x)\big\}\ge1-\alpha.$$

Milestones, in the order the paper's proof uses them

• (6): $\|\mathrm{proj}_{\mathcal Y}(\hat f_n(x)+\hat\varepsilon^i_n)-(f^*(x)+\varepsilon^i)\|\le\|\tilde\varepsilon^i_n(x)\|$.
• Lemma 3: $d_{W,p}(\hat P^{ER}_n(x),P_{Y\mid X=x})\le\big(\frac1n\sum_i\|\tilde\varepsilon^i_n(x)\|^p\big)^{1/p}+d_{W,p}(P^*_n(x),P_{Y\mid X=x})$.
• Lemma 4: the power mean of $\|\tilde\varepsilon^i_n(x)\|$ is at most the prediction error plus the power-mean estimation error.
• Lemma 5: $\mathbb P(V+W>C_1+C_2)\le\mathbb P(V>C_1)+\mathbb P(W>C_2)$.
• Lemma 6: $\mathbb P\{(\frac1n\sum_i\|\tilde\varepsilon^i_n(x)\|^p)^{1/p}>2\kappa_{p,n}(\alpha/4,x)\}\le\alpha/2$.
• Second display of the proof of Theorem 7: $\mathbb P\{d_{W,p}(P^*_n(x),P_{Y\mid X=x})>\kappa^{(2)}_{p,n}(\alpha)\}\le\alpha/2$.
• Third display: $\mathbb P\{d_{W,p}(\hat P^{ER}_n(x),P_{Y\mid X=x})>\zeta_n(\alpha,x)\}\le\alpha$.

Significance

Theorem 7 gives the ER-DRO optimal value a meaning a decision maker can use. The computed number $\hat v^{DRO}_n(x)$ bounds the true expected cost of the computed decision, with confidence $1-\alpha$, for every finite $n$. The scenarios are built from an estimated regression function, not from samples of the conditional distribution. The price is an enlarged radius: the covariate-free radius plus a term $2\kappa_{p,n}(\alpha/4,x)$ for the regression error. The same radius drives the paper's asymptotic optimality and rate results (Theorems 9–11).

The theorem is proved in the paper. No part of it is formalized. The covariate-free analogue, Theorem 3.5 of Mohajerin Esfahani and Kuhn, is formalized and proved on the platform (WassDDRO.Consistency.theorem_3_5). This mission adds three things:

• the regression layer: the projection inequality (6), the decomposition of Lemma 3 and the power-mean bounds;
• a precise account of the radius;
• a correction to it. The paper prints $\log(c_1\alpha^{-1})$ in $\kappa^{(2)}_{p,n}(\alpha)$, which sets Lemma 2's right-hand side to $\alpha$, not to the $\alpha/2$ the text states. The proof as printed then gives only $3\alpha/2$. The mission states the theorem with $\log(2c_1\alpha^{-1})$, the derivation the paper describes.

Difficulty

The obvious argument copies the covariate-free proof: treat $\hat P^{ER}_n(x)$ as an empirical distribution of $P_{Y\mid X=x}$ and apply a concentration inequality. This fails. The scenarios $\mathrm{proj}_{\mathcal Y}(\hat f_n(x)+\hat\varepsilon^i_n)$ are not samples from $P_{Y\mid X=x}$, and they are not independent: all of them share the data-dependent estimate $\hat f_n$. No concentration inequality applies to $\hat P^{ER}_n(x)$ directly. The regression error has to be separated from the sampling error, and each controlled by its own hypothesis, at a fixed covariate $x$.

On the formal side, Lemma 3 needs the triangle inequality for $d_{W,p}$ between arbitrary probability measures, which needs a gluing construction. Mathlib does not have it, and on the platform it is an open statement. Lemma 4 needs Minkowski's inequality for a normalized finite power mean. The probabilistic steps act on events whose measurability is not assumed.

Formalization scope

Conventions:

• $\mathbb R^{d}$ is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, and $d_y\ge1$.
• The data, the regression estimate $\hat f_n$ and the solution $\hat z^{DRO}_n(x)$ are arbitrary functions on a probability space $(\Omega,\mathbb P)$. Each probability is the outer measure of the displayed set, so no measurability of these objects is assumed.
• The responses are $y^i=f^*(x^i)+\varepsilon^i$. The projection is a given map with the nearest-point property on a nonempty closed convex $\mathcal Y$, and $f^*(x)+\varepsilon^i\in\mathcal Y$ is a hypothesis.
• $P_{Y\mid X=x}$ is the pushforward of $P_\varepsilon$ under $e\mapsto f^*(x)+e$.
• The paper's "for a.e. $x$" is handled pointwise. Assumption 2 (a function $\alpha\mapsto\kappa_{p,n}(\alpha,x)$) and Lemma 2's conclusion (constants $c_1,c_2>0$) are hypotheses at the given $x$ and sample size $n$.
• Lemma 2 itself is not posed; it is Fournier and Guillin's Theorem 2, already open on the platform. That theorem bounds $W_p^p$, while the paper transcribes the exponents for $d_{W,p}$. For $p>1$ and $d_y>2p$ the hypothesis may therefore be unsatisfiable. The mission keeps the paper's Lemma 2 as written.
• Distances are $[0,\infty]$-valued and the DRO value is an extended real. The worst case counts the distributions $Q$ in the ball under which $c(z,\cdot)$ is integrable. The conclusion of Theorem 7 is in failure form, $\mathbb P\{g>\hat v\}\le\alpha$.

The integrability hypothesis on $c(z,f^*(x)+\varepsilon)$ is necessary: without it the true law would not be counted in the worst case and the certificate would be vacuous. Centring the ball at $P^*_n(x)$ instead of $\hat P^{ER}_n(x)$ would trivialize the mission by removing the regression error, and is excluded.

Needed infrastructure, reusable beyond this mission: the gluing lemma and triangle inequality for $d_{W,p}$; Wasserstein bounds between empirical measures with matched atoms; nonexpansiveness of the metric projection onto a closed convex set. The general Wasserstein objects are the published WassersteinDRO.Duality definitions. Proofs of any milestone are welcome, as is a proof of Theorem 7 from the milestones.

Selected references

• R. Kannan, G. Bayraksan, J. R. Luedtke, Residuals-based distributionally robust optimization with covariate information, Mathematical Programming, 2023. https://doi.org/10.1007/s10107-023-02014-7
• R. Kannan, G. Bayraksan, J. R. Luedtke, Data-driven sample average approximation with covariate information, arXiv preprint, 2022. https://arxiv.org/abs/2207.13554
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
• N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162, 2015. https://doi.org/10.1007/s00440-014-0583-7
• D. Bertsimas, N. Kallus, From predictive to prescriptive analytics, Management Science 66, 2020. https://doi.org/10.1287/mnsc.2018.3253

Motivation

Wasserstein distributionally robust optimization (DRO) hedges a decision against every probability distribution within a given transport distance of a nominal one, typically the empirical distribution of data. The inner problem, the worst-case loss, is an optimization over an infinite-dimensional set of measures, and every practical use of Wasserstein DRO — tractable reformulations, statistical guarantees, regularization interpretations — rests on a strong duality theorem that replaces it with a one-dimensional minimization over a Lagrange multiplier.

Such duality theorems have been proved under progressively weaker hypotheses:

• Mohajerin Esfahani and Kuhn (2018) and Zhao and Guan (2018): empirical nominal distributions on subsets of $\mathbb R^d$, via conic duality.
• Blanchet and Murthy (2019): Polish spaces, lower semi-continuous costs and upper semi-continuous losses, via an approximation argument (arXiv:1604.01446).
• Gao and Kleywegt (2023): Polish spaces with costs that are powers of a metric and arbitrary measurable losses (arXiv:1604.02199).
• Zhang, Yang and Gao (2022, v4 2024): an arbitrary measurable space, an arbitrary measurable cost with values in $[0,\infty]$ and a measurable loss, with duality characterized exactly by an interchangeability principle (arXiv:2205.00362).

This mission formalizes the last of these, Theorem 1 of Zhang–Yang–Gao.

Setting

Let $(\mathcal X,\mathcal F,\widehat{\mathbb P})$ be a probability space, $f:\mathcal X\to\mathbb R$ a measurable loss with $\mathbb E_{\widehat{\mathbb P}}[f]>-\infty$, and $c:\mathcal X\times\mathcal X\to[0,\infty]$ a measurable transport cost with $c(x,x)=0$ (Assumption 1). Expectations take values in $\bar{\mathbb R}=[-\infty,\infty]$, and the convention $0\cdot\infty=\infty$ is used for products $\lambda c$.

The Kantorovich transport cost between $\widehat{\mathbb P}$ and a probability measure $\mathbb P$ is

$$\mathcal K_c(\widehat{\mathbb P},\mathbb P)=\inf_{\gamma\in\Gamma(\widehat{\mathbb P},\mathbb P)}\mathbb E_{(\widehat X,X)\sim\gamma}[c(\widehat X,X)],$$

where $\Gamma(\widehat{\mathbb P},\mathbb P)$ is the set of couplings with marginals $\widehat{\mathbb P}$ and $\mathbb P$. The worst-case loss is

$$\mathcal L(\rho)=\sup_{\mathbb P}\big\{\mathbb E_{X\sim\mathbb P}[f(X)]:\mathcal K_c(\widehat{\mathbb P},\mathbb P)\le\rho\big\},$$

with $\mathcal L(\rho)=-\infty$ for $\rho<0$. For $\lambda\ge0$ let $\phi_\lambda(\widehat x,x)=f(x)-\lambda c(\widehat x,x)$ and

$$\mathcal G(\lambda)=\mathbb E_{\widehat X\sim\widehat{\mathbb P}}\Big[\sup_{x\in\mathcal X}\phi_\lambda(\widehat X,x)\Big].$$

$\Gamma_{\widehat{\mathbb P}}$ is the set of probability measures on $\mathcal X\times\mathcal X$ with first marginal $\widehat{\mathbb P}$. A measurable $\phi:\mathcal X\times\mathcal X\to\mathbb R\cup\{-\infty\}$ satisfies the interchangeability principle (IP) if $\widehat x\mapsto\sup_x\phi(\widehat x,x)$ is $\widehat{\mathbb P}$-measurable (measurable for the completion of $\mathcal F$) and

$$\mathbb E_{\widehat X\sim\widehat{\mathbb P}}\Big[\sup_{x}\phi(\widehat X,x)\Big]=\sup_{\gamma\in\Gamma_{\widehat{\mathbb P}}}\mathbb E_{(\widehat X,X)\sim\gamma}[\phi(\widehat X,X)].$$

The Legendre transform of $h:\mathbb R\to\bar{\mathbb R}$ is $h^*(\lambda)=\sup_{\rho\in\mathbb R}\{\lambda\rho-h(\rho)\}$.

Formalization targets

Goal: Theorem 1, (D)

$\phi_\lambda$ satisfies (IP) for every $\lambda>0$ if and only if the supremum functions are $\widehat{\mathbb P}$-measurable and

$$\mathcal L(\rho)=\min_{\lambda\ge0}\Big\{\lambda\rho+\mathbb E_{\widehat X\sim\widehat{\mathbb P}}\Big[\sup_{x\in\mathcal X}\{f(x)-\lambda c(\widehat X,x)\}\Big]\Big\}\qquad\forall\rho>0.$$

The minimum is attained. Both sides may be $+\infty$.

Milestones

1. Lemma 1. $\mathcal L$ is bounded below by $\mathbb E_{\widehat{\mathbb P}}[f]$, increasing and concave on $[0,\infty)$.
2. (P-soft). For $\lambda>0$, $(-\mathcal L)^*(-\lambda)=\sup\{\mathbb E_{\mathbb P}[f]-\lambda\mathcal K_c(\widehat{\mathbb P},\mathbb P):\mathcal K_c<\infty\}$.
3. Theorem 1, first display. $(-\mathcal L)^*(-\lambda)=\sup_{\gamma\in\Gamma_{\widehat{\mathbb P}}}\mathbb E_\gamma[f(X)-\lambda c(\widehat X,X)]$ for $\lambda>0$.
4. Lemma 3. Properties of $\lambda\mapsto h^*(-\lambda)$ for a decreasing convex proper $h$ that is $+\infty$ on $(-\infty,0)$.
5. Lemma 2. $(-\mathcal L)^*(-\cdot)$ and $\mathcal G$ are bounded below by $\mathbb E_{\widehat{\mathbb P}}[f]$, decreasing, convex and lower semi-continuous on $[0,\infty)$ (two items).
6. Theorem 1, second display. $\mathcal L(\rho)=\min_{\lambda\ge0}\{\lambda\rho+\sup_{\gamma\in\Gamma_{\widehat{\mathbb P}}}\mathbb E_\gamma[f(X)-\lambda c(\widehat X,X)]\}$ for $\rho>0$: duality with no assumption beyond Assumption 1.
7. Theorem 1, third display. For fixed $\lambda>0$, $\phi_\lambda$ satisfies (IP) iff $(-\mathcal L)^*(-\lambda)=\mathcal G(\lambda)$.

Significance

The result. Theorem 1 separates Wasserstein DRO duality into two parts. The first, the second display, holds with no regularity at all: the worst-case loss always equals a one-dimensional minimum over $\lambda$ of a supremum over couplings with fixed first marginal. The second identifies exactly when that supremum can be moved inside the expectation, which is the form (D) used in applications: (D) holds for all radii if and only if (IP) holds. The question of when Wasserstein DRO has its standard dual becomes a question about measurable selection and measurable projection, which is studied in a companion mission of this series. The duality results of the timeline above become special cases in which (IP) can be verified.

Formalizing it. The results are proved in the paper; none of them has a machine-checked proof. A formalization produces a verified duality theorem at the level of generality of measurable spaces with extended-valued costs, together with a reusable layer: Kantorovich costs with values in $[0,\infty]$, extended-real expectations, and one-dimensional Legendre transforms of extended-real functions.

Difficulty

The proof is short on paper because it delegates to one-dimensional convex analysis: the involution $h^{**}=\operatorname{cl}h$ of the Legendre transform on $\mathbb R$ (Rockafellar, Theorem 12.2), applied to $-\mathcal L$. The work is in the extended reals. $\mathcal L$ can be $+\infty$ on all of $(0,\infty)$, $(-\mathcal L)^*$ can be identically $+\infty$, and the costs and products involve $0\cdot\infty$. Concavity of $\mathcal L$ on $[0,\infty)$ requires mixing near-optimal distributions and couplings, and lower semi-continuity of $\mathcal G$ requires Fatou's lemma for functions bounded below by $f$, not by $0$. The "only if" direction of the goal has to recover (IP) for every $\lambda>0$ from (D), which goes through biconjugation of $\mathcal G$ and the right continuity at $\lambda=0$ of both transforms. A proof that treats every value as finite does not cover the theorem.

Formalization scope

The Lean development lives in the namespace ShortWDRODual.Legendre.

• $\mathcal X$ is a measurable space and $\widehat{\mathbb P}$ a probability measure. The cost is ENNReal-valued and curried, c x̂ x, with the nominal point first. The loss is real-valued and measurable.
• $\mathcal K_c$ is the published RWPI.SqrtLasso.transportCost (infimum over probability couplings of the lower Lebesgue integral of $c$, in $[0,\infty]$).
• Expectations are the published ModelRiskOT.Duality.extIntegral, $\int\varphi^+-\int\varphi^-$ in EReal. This agrees with the paper whenever one part is finite. It assigns $-\infty$ to the undefined case $\infty-\infty$, so a law or coupling with an undefined expectation never raises a supremum.
• The ball constraint $\mathcal K_c\le\rho$ is compared in EReal, so that $\mathcal L(\rho)=-\infty$ for $\rho<0$. Reading it as $\mathcal K_c\le\max(\rho,0)$ would make every Legendre transform $+\infty$.
• $\lambda c$ uses the paper's $0\cdot\infty=\infty$ (Mathlib's product has $0\cdot\infty=0$). This matters for $\lambda=0$: the supremum is then over $\{x:c(\widehat x,x)<\infty\}$.
• "min" is attainment plus lower bound (IsLeast). Concavity, convexity and monotonicity of extended-real functions are stated as explicit inequalities with real weights. Lower semi-continuity "on $[0,\infty)$" is relative to $[0,\infty)$.
• $\widehat{\mathbb P}$-measurability is NullMeasurable. Disclosed reading: in the goal and in the fixed-$\lambda$ milestone, the measurability of the supremum functions is stated explicitly next to the duality formula, because the paper's expectation in (D) presupposes it and (IP) contains it. Lemma 2's statement on $\mathcal G$ assumes this measurability for $\lambda>0$, for the same reason.
• Ruled out: a goal that assumes (IP) and concludes (D) states only one direction. So does a goal that drops attainment, or uses Mathlib's $0\cdot\infty=0$. All three are weaker theorems.

A complete development needs the one-dimensional Fenchel–Moreau theorem for extended-real functions on $\mathbb R$, gluing and mixing of couplings with a fixed first marginal, and Fatou's lemma for extIntegral. Each is reusable well beyond this mission. Contributions of any of these as separate lemmas are welcome.

Selected references

• L. Zhang, J. Yang, R. Gao, A Short and General Duality Proof for Wasserstein Distributionally Robust Optimization, arXiv:2205.00362v4, 2024. https://arxiv.org/abs/2205.00362
• J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research 44(2):565–600, 2019. https://arxiv.org/abs/1604.01446
• R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research 48(2):603–655, 2023. https://arxiv.org/abs/1604.02199
• P. Mohajerin Esfahani, D. Kuhn, Data-driven Distributionally Robust Optimization Using the Wasserstein Metric, Mathematical Programming 171:115–166, 2018. https://arxiv.org/abs/1505.05116
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Model-free bounds for lookback options

A lookback option pays a function of the running maximum of the underlying asset over the life of the contract. When the prices of European call options of all strikes at the maturity are quoted, the risk-neutral law $\mu$ of the terminal price is known, but the law of the whole path is not. The robust (model-free) superhedging cost of the lookback payoff is the cheapest initial capital that, combined with a static position in the quoted calls and dynamic trading in the underlying, dominates the payoff in every model consistent with $\mu$.

Hobson (Finance Stoch. 1998) computed this cost for $g(x)=x$ by a pathwise inequality, and identified the extremal model through the Azéma–Yor solution of the Skorokhod embedding problem (Azéma–Yor 1979). Galichon, Henry-Labordère and Touzi (Ann. Appl. Probab. 2014, arXiv:1401.3921) recast model-free bounds as a dual stochastic control problem in which the marginal constraint is penalised by a Lagrange multiplier $\lambda$. Their Theorem 3.1 recovers Hobson's bound for every $C^1$ nondecreasing $g$ from that dual, with an explicit optimal multiplier and stopping time. The result is one of the founding examples of martingale optimal transport.

Setting

Let $B$ be a real Brownian motion with continuous paths and $B_0=0$, adapted to a filtration $(\mathcal F_t)_{t\ge0}$ with increments independent of the past, and let $X_t=X_0+B_t$ for a spot $X_0\in\mathbb R$. Write $X^*_\tau=\max_{t\le\tau}X_t$. Let $\mathcal T_\infty$ be the set of stopping times $\tau$ for which the stopped process $(X_{t\wedge\tau})_{t\ge0}$ is a uniformly integrable martingale.

The marginal is a probability measure $\mu$ on $\mathbb R$ with finite first moment and mean $\int x\,\mu(dx)=X_0$. Its call prices are $c(x)=\int(y-x)^+\mu(dy)$. The payoff is $\xi=g(X^*)$ with $g:\mathbb R\to\mathbb R_+$ of class $C^1$ and nondecreasing.

For a multiplier $\lambda:\mathbb R\to\mathbb R$ and $\tau\in\mathcal T_\infty$ set $J(\lambda,\tau)=\mathbb E[g(X^*_\tau)-\lambda(X_\tau)]$ and $u^\lambda(X_0,X_0)=\sup_{\tau\in\mathcal T_\infty}J(\lambda,\tau)$. The admissible multipliers are

$$\Lambda^\mu_0=\Big\{\lambda\in\mathbb L^1(\mu):\ \sup_{\tau\in\mathcal T_\infty}\mathbb E[\lambda(X_\tau)^-]<\infty\Big\},$$

and the reduced superhedging problem (3.7) is

$$U^\mu(\xi)=\inf_{\lambda\in\Lambda^\mu_0}\Big\{\int\lambda\,d\mu+u^\lambda(X_0,X_0)\Big\}.$$

The barycenter function is $b(x)=\int_{[x,\infty)}y\,\mu(dy)/\mu([x,\infty))$ for $\mu((x,\infty))>0$ and $b(x)=x$ otherwise. The Hardy–Littlewood transform $\mu^{HL}$ is the probability measure with

$$\mu^{HL}([y,\infty))=\inf_{\xi<y}\frac{c(\xi)}{y-\xi}.$$

The Azéma–Yor stopping time is $\tau^*=\inf\{t>0:X^*_t\ge b(X_t)\}$, and the candidate multiplier is

$$\lambda^*(x)=\int_{\ell^\mu}^{x}\!\int_{\ell^\mu}^{y}g'(b(\xi))\,\frac{b(d\xi)}{b(\xi)-\xi}\,dy ,$$

that is, the convex function vanishing below $\ell^\mu$ that solves the weak ODE (3.21) with $\psi=b^{-1}$.

Formalization targets

Goal: Theorem 3.1

If $\sup_{\tau\in\mathcal T_\infty}\mathbb E[g(X^*_\tau)]<\infty$ and $\mu^{HL}(g)=\int g\,d\mu^{HL}<\infty$, then

$$U^\mu(\xi)=\mu(\lambda^*)+J(\lambda^*,\tau^*)=\mu^{HL}(g).$$

The goal is the paper's theorem for the reduced problem (3.7), in its full two-equality form: the value, its attainment by $(\lambda^*,\tau^*)$, and its closed form.

Milestones

1. The Neumann condition (3.23) for Peskir's candidate $v^\psi$.
2. Lemma 3.1: $u^\lambda\le v^\psi$ for convex $\lambda\in\Lambda^\mu_0$ and every relaxed free boundary $\psi\in\Psi^\lambda$.
3. Step (1) of Lemma 3.2: $\mu(\lambda)-\lambda(X_0)=\int(c-c_0)\,d\lambda''$, with $c_0(x)=(X_0-x)^+$.
4. Lemma 3.2: $\mu(\lambda)+u^\lambda(X_0,X_0)\le g(X_0)+\int\varphi(\psi(m),m)g'(m)\,dm$.
5. The pointwise minimizations (3.27) and (3.28).
6. Steps (2) and (3) of Lemma 3.3: properties of $\lambda^*$, and the integration by parts giving $\mu^{HL}(g)$.
7. Lemma 3.3, the upper bound $U^\mu(\xi)\le\mu^{HL}(g)$.
8. The Azéma–Yor facts: $\tau^*\in\mathcal T_\infty$, $X_{\tau^*}\sim\mu$, $X^*_{\tau^*}\sim\mu^{HL}$.
9. The lower bound $U^\mu(\xi)\ge\mu^{HL}(g)$ of Section 3.4.

Significance

The theorem identifies the model-free price of a lookback payoff as an explicit functional of the call prices, $\mu^{HL}(g)$, and exhibits the extremal model (Brownian motion stopped at $\tau^*$) and the optimal static hedge ($\lambda^*$). It shows that the dual stochastic control formulation is sharp on a nontrivial path-dependent payoff, which is the template for later work on martingale optimal transport with path-dependent costs.

The result has been proved since 2014 (and Hobson's bound since 1998). It has not been formalized. A complete development would provide machine-checked versions of the Azéma–Yor embedding, the law of the maximum at the embedding, a verification theorem for a reflected optimal stopping problem with a nonsmooth obstacle, and the convex-analytic identities linking call prices to second-derivative measures. Each of these is reusable well beyond this paper.

Difficulty

The upper bound requires a verification argument for an optimal stopping problem of the pair $(X,X^*)$ with a reflection at the diagonal, where the candidate $v^\psi$ is only as regular as the convex multiplier $\lambda$: second derivatives are measures and the free boundary $\psi$ solves its ODE only in a relaxed sense. An Itô formula for $C^2$ functions does not apply; an Itô–Tanaka (local time) argument for concave functions of $X$, with the reflection term killed by the Neumann condition, is needed, followed by a localisation that uses uniform integrability and the integrability condition in $\Lambda^\mu_0$. The lower bound needs the Azéma–Yor embedding and the law of $X^*_{\tau^*}$, neither of which is in Mathlib; the naive appeal to "the embedding exists" does not give the joint law of the stopped value and the maximum.

Formalization scope

The Lean development lives in the namespace LookbackMOT.HL and uses Mathlib's IsBrownianReal, IsStoppingTime, stoppedProcess, stoppedValue, Martingale, UniformIntegrable and HasLaw. Committed conventions:

• What is formalized. The goal is the reduced problem (3.7), not the superhedging problem (2.6): (2.6) needs stochastic integrals, which Mathlib does not have. The bridge between them (Proposition 2.1, the claim (3.4), Proposition 3.1) is outside this mission. The theorem's hypothesis $\sup_{\mathbb P\in\mathcal P_\infty}\mathbb E^{\mathbb P}[\xi^+]<\infty$ is stated through Proposition 3.1 with $\lambda=0$ as $\sup_{\tau\in\mathcal T_\infty}\mathbb E[g(X^*_\tau)]<\infty$. The horizon $T$ disappears: the stopping problem is over $\mathcal T_\infty$ with time in $[0,\infty)$.
• Standing hypotheses. The Brownian motion lives on an arbitrary filtered probability space with everywhere-continuous paths and $B_0=0$; the paper's canonical space is one instance. The mean condition and integrability of $\mu$ (p. 7) are assumed throughout. The spot $X_0$ is any real number. $\mu([0,\infty))=1$ is assumed only in (3.27).
• Added conditions. Every $\tau\in\mathcal T_\infty$ is a.s. finite (implied by uniform integrability). Every $\lambda\in\Lambda^\mu_0$ is measurable.
• Expectations of payoffs are $\mathbb E[\varphi^+]-\mathbb E[\varphi^-]$ in the extended reals, with $\infty-\infty=-\infty$; value functions are extended reals.
• Derivatives. $\lambda'$ is the right derivative and $\lambda''$ its Stieltjes measure. The weak ODE (3.21) is used both as a change of variables ($\lambda''$ is the image of $g'(m)/(m-\psi(m))\,dm$ under $\psi$) and on intervals ($\lambda'(\psi(y_2))-\lambda'(\psi(y_1))=\int_{y_1}^{y_2}g'(m)/(m-\psi(m))\,dm$), the two forms the paper's proofs use.
• The multiplier $\lambda^*$. It is written as $\lambda^*(x)=\int_{X_0<m<r^\mu}g'(m)(x-b^{-1}(m))^+/(m-b^{-1}(m))\,dm$, the change of variables $m=b(\xi)$ in (3.14) and the solution of (3.21) with $\psi=b^{-1}$ that the proof of Lemma 3.3 uses. It agrees with the $b(d\xi)$ formula when $b$ is continuous; at the jumps of $b$ (atoms of $\mu$) the Lebesgue–Stieltjes reading of (3.14) can fail to be $\mu$-integrable.
• Measures given by identities. $\mu^{HL}$ and $\lambda''$ enter as measures satisfying their defining identities on intervals; each exists and is unique.
• Printed slips not copied. (3.12) prints the numerator $c(y)$; the formalization uses $c(\xi)$. $b$, $\mu^{HL}$ and $\lambda^*$ are extended from $x\ge0$ to all of $\mathbb R$ by the same formulas.

No trivializing reading is available. Payoff expectations are never Bochner integrals (which would be $0$ for non-integrable payoffs). $\tau\equiv0$ lies in $\mathcal T_\infty$ and $\lambda\equiv0$ in $\Lambda^\mu_0$, so neither the supremum nor the infimum is over an empty set. The predicates for $\mu^{HL}$ and $\lambda''$ are satisfiable (witnessed for $\mu=\delta_{X_0}$ in a sorry-free check). $X_\tau$ is only evaluated where $\tau<\infty$ a.s. Every division has a positive denominator on the sets that carry mass.

Contributions welcome: the Azéma–Yor embedding and the law of the maximum; an Itô–Tanaka or local-time calculus sufficient for concave functions of Brownian motion and its maximum; the call-price identities of convex analysis; and the analysis of $\mu^{HL}$.

Selected references

• A. Galichon, P. Henry-Labordère, N. Touzi, A stochastic control approach to no-arbitrage bounds given marginals, with an application to lookback options, Ann. Appl. Probab. 24 (2014) 312–336. https://arxiv.org/abs/1401.3921 (v1, the version cited)
• D. Hobson, Robust hedging of the lookback option, Finance Stoch. 2 (1998) 329–347. https://doi.org/10.1007/s007800050046
• J. Azéma, M. Yor, Une solution simple au problème de Skorokhod, Séminaire de Probabilités XIII, LNM 721 (1979) 90–115. https://doi.org/10.1007/BFb0070852
• G. Peskir, Optimal stopping of the maximum process: the maximality principle, Ann. Probab. 26 (1998) 1614–1640. https://doi.org/10.1214/aop/1022855875
• L. Carraro, N. El Karoui, J. Obłój, On Azéma–Yor processes, their optimal properties and the Bachelier–drawdown equation, Ann. Probab. 40 (2012) 372–400. https://arxiv.org/abs/0902.1328

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.