Operations Research

Motivation

Many stochastic models evolve on two time scales: a fast component that equilibrates quickly and a slow component driven by it. Planetary motion, climate models, geophysical flows and intracellular reaction networks are standard examples, and multiscale numerical methods for them approximate the slow component by a reduced equation. Such approximations are only useful with an error bound, and for the fully coupled case, where the fast and slow equations each depend on both components and the slow equation contains a large fluctuating drift, rates of convergence were missing.

Röckner and Xie (Ann. Probab. 49 (2021) 1205–1236) treat this case with only Hölder continuous coefficients and obtain explicit rates in four regimes. This mission poses the first regime, the classical averaging principle.

Timeline. Papanicolaou, Stroock and Varadhan (1977) proved the diffusion approximation for $\alpha_\varepsilon=\beta_\varepsilon=\gamma_\varepsilon$ with a compact fast state space and time-independent coefficients. Pardoux and Veretennikov (2001, 2003, 2005) treated a noncompact homogeneous case with $c\equiv0$ and $\alpha_\varepsilon=\gamma_\varepsilon$ by martingale problems and the Poisson equation. Rates for the averaging principle when $c=H\equiv0$ were obtained by several authors, e.g. Givon (2007) and Liu (2010). Röckner and Xie (2021) give rates for the fully coupled system with Hölder coefficients in all four regimes.

Setting

Let $x\in\mathbb R^{d_1}$ (fast) and $y\in\mathbb R^{d_2}$ (slow), $d_1,d_2\ge1$. For small parameters $\alpha_\varepsilon,\beta_\varepsilon,\gamma_\varepsilon>0$ tending to $0$, with $\alpha_\varepsilon^2/\beta_\varepsilon\to0$, the two-scale system (1.4) is

$$dX^\varepsilon_t=\alpha_\varepsilon^{-2}b(X^\varepsilon_t,Y^\varepsilon_t)dt+\beta_\varepsilon^{-1}c(X^\varepsilon_t,Y^\varepsilon_t)dt+\alpha_\varepsilon^{-1}\sigma(X^\varepsilon_t,Y^\varepsilon_t)dW^1_t,$$ $$dY^\varepsilon_t=F(t,X^\varepsilon_t,Y^\varepsilon_t)dt+\gamma_\varepsilon^{-1}H(t,X^\varepsilon_t,Y^\varepsilon_t)dt+G(t,X^\varepsilon_t,Y^\varepsilon_t)dW^2_t,$$

with $X^\varepsilon_0=x$, $Y^\varepsilon_0=y$ and independent Brownian motions $W^1,W^2$.

Freezing $y$ gives the frozen equation $dX^y_t=b(X^y_t,y)dt+\sigma(X^y_t,y)dW^1_t$ (1.7), with generator $\mathscr L_0(x,y)=\sum_{ij}a^{ij}\partial^2_{x_ix_j}+\sum_ib^i\partial_{x_i}$, $a=\sigma\sigma^*/2$, and invariant probability measure $\mu^y$. A function is centered if its $\mu^y$-average vanishes for every $y$. The standing assumptions are: (Aσ), uniform nondegeneracy of $\sigma\sigma^*$; (Ab), $\lim_{|x|\to\infty}\sup_y\langle x,b(x,y)\rangle=-\infty$; (AG), uniform nondegeneracy of $GG^*$; (AH), $H$ is centered; and (2.7), the analogue of (Ab) for $b+\kappa c$, $\kappa>0$ small.

The averaged coefficients of Regime 1 are $\hat F_1(t,y)=\int F(t,x,y)\mu^y(dx)$ and $\hat G_1=(\int GG^*(t,x,y)\mu^y(dx))^{1/2}$, and the averaged equation (2.9) is $d\hat Y^1_t=\hat F_1(t,\hat Y^1_t)dt+\hat G_1(t,\hat Y^1_t)dW^2_t$, $\hat Y^1_0=y$.

Regularity is measured in weighted Hölder classes: $C^{\delta,\vartheta}_p$ (index $\delta$ in $x$, $\vartheta$ in $y$, polynomial growth in $x$), its bounded version $C^{\delta,\vartheta}_b$, the time-dependent $C^{\vartheta/2,\delta,\vartheta}_p$, the class $L^\infty_p$ of measurable functions of polynomial growth, and $C^{2+\vartheta}_b(\mathbb R^{d_2})$ for test functions.

Formalization targets

Goal: Theorem 2.3(i)

In Regime 1, $\alpha_\varepsilon/\gamma_\varepsilon\to0$ and $\alpha_\varepsilon^2/(\beta_\varepsilon\gamma_\varepsilon)\to0$, assume $b,\sigma\in C^{\delta,\vartheta}_b$, $F,H,G\in C^{\vartheta/2,\delta,\vartheta}_p$ with $\vartheta\in(0,2]$, $c\in L^\infty_p$ and $\alpha_\varepsilon^\vartheta/\gamma_\varepsilon\to0$. Then for every $T>0$ and $\varphi\in C^{2+\vartheta}_b$,

$$\sup_{t\in[0,T]}\big|\mathbb E\varphi(Y^\varepsilon_t)-\mathbb E\varphi(\hat Y^1_t)\big|\le C_T\Big(\frac{\alpha_\varepsilon^\vartheta}{\gamma_\varepsilon}+\frac{\alpha_\varepsilon^2}{\gamma_\varepsilon^2}+\frac{\alpha_\varepsilon^2}{\beta_\varepsilon\gamma_\varepsilon}\Big).$$

Milestones

1. Lemma 4.1: mollification in $(t,y)$ at scales $n^{-2}$ and $n^{-1}$ costs $n^{-\vartheta}$ and gains $n^{2-\vartheta}$ on $\partial_t$ and $\nabla_y^2$.
2. Lemma 4.2: for centered $f$, $\mathbb E\int_0^tf(s,X^\varepsilon_s,Y^\varepsilon_s)ds\le C_t(\alpha_\varepsilon^\vartheta+\alpha_\varepsilon^{\vartheta\wedge1}\alpha_\varepsilon/\gamma_\varepsilon+\alpha_\varepsilon^2/\beta_\varepsilon)$.
3. Lemma 4.4(i): in Regime 1, $\mathbb E\,\gamma_\varepsilon^{-1}\int_0^tf\,ds\le C_t(\alpha_\varepsilon^\vartheta/\gamma_\varepsilon+\alpha_\varepsilon^2/\gamma_\varepsilon^2+\alpha_\varepsilon^2/(\beta_\varepsilon\gamma_\varepsilon))$.
4. Lemma 5.1 ($k=1$): $\hat{\mathcal G}_1=\hat G_1\hat G_1^*/2$ is uniformly nondegenerate and $\hat F_1,\hat{\mathcal G}_1\in C^{\vartheta/2,\vartheta}_b$.

Significance

The result. The theorem gives a rate for the weak error of the averaging principle under Hölder regularity only, and the rate depends only on the regularity in the slow variable $y$, not on $\delta$. It covers the fully coupled case, in which the slow equation contains the singular drift $\gamma_\varepsilon^{-1}H$, and it identifies the extra condition $\alpha_\varepsilon^\vartheta/\gamma_\varepsilon\to0$ under which this drift averages out. For $c=H\equiv0$ it reduces to the rate $\alpha_\varepsilon^\vartheta$ (Remark 2.5), optimal for $\vartheta=2$. Error bounds of this kind are what heterogeneous multiscale methods need to be quantitative.

Formalizing it. The result is proved in the paper; nothing in it is machine-checked. A formalization needs an Itô calculus for weak solutions, the elliptic Poisson equation in $x$ with parameter $y$ (the companion mission's Theorem 2.1), and the parabolic Kolmogorov equation of the averaged SDE. The two fluctuation lemmas are stated for general centered functions and are reusable for other limit theorems.

Difficulty

The obvious argument writes $\mathbb E\varphi(Y^\varepsilon_T)-\mathbb E\varphi(\hat Y^1_T)$ through the Kolmogorov equation of the averaged SDE and Itô's formula, which leaves $\mathbb E\int_0^T(\mathscr L_1-\hat{\mathscr L}_1)\tilde u\,ds$ and $\gamma_\varepsilon^{-1}\mathbb E\int_0^TH\cdot\nabla_y\tilde u\,ds$. Both integrands are centered but only Hölder continuous in $(t,y)$, so the standard corrector argument, which applies Itô's formula to the solution of the Poisson equation along $(X^\varepsilon,Y^\varepsilon)$, needs derivatives in $t$ and $y$ that do not exist. The term with $\gamma_\varepsilon^{-1}$ is a central-limit-scale fluctuation, which is why its control needs the regime conditions. Existence and regularity of the averaged coefficients also have to come from the Poisson equation, since $\mu^y$ is not explicit.

Formalization scope

Spaces are EuclideanSpace ℝ (Fin d). Coefficients are $b,c:\mathbb R^{d_1}\times\mathbb R^{d_2}\to\mathbb R^{d_1}$, $\sigma$ a $d_1\times d_1$ matrix, $F,H:\mathbb R_+\times\mathbb R^{d_1}\times\mathbb R^{d_2}\to\mathbb R^{d_2}$, $G$ a $d_2\times d_2$ matrix. The Itô layer (Brownian motion, Itô integral, Itô processes, SDE solutions) is the published Peng1990.SMP.Stochastic. A solution of (1.4) is a weak solution: any filtered probability space, any Brownian motion for that filtration, any progressive process satisfying the integral equation. The theorem compares every weak solution of (1.4) with every weak solution of (2.9). The paper does not prove existence for (1.4), so the statement is conditional on solutions, as it is used in the paper. A sanity file shows the parameter hypotheses are consistent ($\alpha_\varepsilon=\varepsilon$, $\beta_\varepsilon=\gamma_\varepsilon=\varepsilon^{1/2}$) and that (2.7) holds for a bounded dissipative drift.

Committed conventions and readings of the page:

• $\mu^y$ is any family of probability measures that are infinitesimally invariant for $\mathscr L_0$ with $a=\sigma\sigma^*/2$, the generator of (1.7). Under the standing assumptions this is the unique invariant measure.
• (2.7) is read with $\kappa=\alpha_\varepsilon^2/\beta_\varepsilon$, the factor that actually multiplies $c$ in the fast drift, for all small $\kappa>0$.
• $\hat G_1$ is any measurable matrix field with $\hat G_1\hat G_1^*=\int GG^*\,d\mu^y$, which covers the printed square root.
• The Hölder classes include polynomial growth, constrain all lower $y$-derivatives, and take their constants uniformly in time, including in the time-Hölder clause.
• The constants $C_T$, $C_t$, $C_0$ exist after all data are fixed (coefficients, $\mu$, $T$, $\varphi$, $x$, $y$, the parameter functions) and before $\varepsilon$ or $n$.
• Lemma 4.1 takes $f$ on all of $\mathbb R$ in time, since (4.1) evaluates $f$ at negative times, and assumes the kernels have the finite moments $\int|r|^{\vartheta/2}\rho_1<\infty$, $\int|z|^\vartheta\rho_2<\infty$ that its proof uses; without them (4.2) fails for a Cauchy-type kernel.
• Solutions are Itô processes in the sense of the referenced layer: progressive, with $\sup_{t\le T}\mathbb E|Z_t|^2<\infty$ and square-integrable diffusion integrands.
• Lemma 4.4(i) carries the Regime 1 limits of its label.
• Lemmas 4.2 and 4.4(i) are one-sided, as printed, and include integrability of the path integral in their conclusion.

A formalization in which the expectations are junk Bochner integrals, the constant depends on $\varepsilon$, or a single strong solution is fixed would be a different and weaker statement; the posed statements rule these out.

Not posed: Regimes 2–4 of Theorem 2.3 and Lemma 4.4(ii)–(iv). The printed $\hat G_3=\hat G_4$ differs by a factor $2$ in the $H\Phi^*$ term from the generator used in the proof, so a faithful statement needs a correction that is left to moderation. Regime 2 needs the Poisson solution $\Phi$ in the averaged drift. Lemma 5.2 is also not posed: as printed, $u_k(t,y)=\mathbb E\varphi(\hat Y^k_t(y))$ solves (5.1) only for time-independent coefficients, and its class $C^{(2+\vartheta)/2,2+\vartheta}_b$ has time index above $1$, which the paper's notations do not define. Contributions toward Itô's formula for these processes, the Poisson equation (companion mission 1) and parabolic Schauder theory are welcome.

Selected references

• M. Röckner, L. Xie, Diffusion approximation for fully coupled stochastic differential equations, Ann. Probab. 49(3) (2021) 1205–1236. https://doi.org/10.1214/20-AOP1475
• G. Papanicolaou, D. Stroock, S. R. S. Varadhan, Martingale approach to some limit theorems, Duke Turbulence Conference, Duke Univ. Math. Ser. III (1977).
• E. Pardoux, A. Yu. Veretennikov, On the Poisson equation and diffusion approximation. I, Ann. Probab. 29 (2001) 1061–1085. https://doi.org/10.1214/aop/1015345596
• E. Pardoux, A. Yu. Veretennikov, On Poisson equation and diffusion approximation. II, Ann. Probab. 31 (2003) 1166–1192. https://doi.org/10.1214/aop/1055425774
• E. Pardoux, A. Yu. Veretennikov, On the Poisson equation and diffusion approximation. III, Ann. Probab. 33 (2005) 1111–1133. https://doi.org/10.1214/009117905000000062
• D. Givon, Strong convergence rate for two-time-scale jump-diffusion stochastic differential systems, Multiscale Model. Simul. 6 (2007) 577–594. https://doi.org/10.1137/060673345
• D. Liu, Strong convergence of principle of averaging for multiscale stochastic dynamical systems, Commun. Math. Sci. 8 (2010) 999–1020.
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28 (1990) 966–979 (source of the Itô layer). https://doi.org/10.1137/0328054

Motivation

In a financial market with a single probability model, the Optional Decomposition Theorem describes the processes that can be dominated by trading. If a process $V$ is a supermartingale under every equivalent martingale measure, then it can be written as an initial value plus a stochastic integral against the stock price, minus an increasing process that represents consumption. El Karoui and Quenez proved it for diffusion models (SIAM J. Control Optim. 33 (1995)) and Kramkov for locally bounded semimartingales (Probab. Theory Related Fields 105 (1996)). It is the step that turns the superhedging price, a supremum of expectations over martingale measures, into an actual dynamic hedging strategy.

Model uncertainty replaces the single model by a set $\mathcal P$ of probability measures that may be mutually singular. This happens, for example, when volatility is only known to lie in an interval. There is then no reference measure, "almost surely" becomes "quasi surely" (outside a set that is null under every model), and the classical proofs, which rely on one dominating measure, do not apply. Bouchard and Nutz (Ann. Appl. Probab. 2015, arXiv:1305.6008) built the discrete-time theory of this setting: no-arbitrage, the fundamental theorem of asset pricing, superhedging duality and, in §6, a nondominated optional decomposition. This mission formalizes that last result.

Timeline:

• 1995: El Karoui and Quenez, optional decomposition in diffusion models.
• 1996: Kramkov, for locally bounded semimartingales.
• 2014: Nutz, superreplication duality under model uncertainty in discrete time (Finance Stoch. 18 (2014)).
• 2015: Bouchard and Nutz, the fundamental theorem, superhedging duality and the optional decomposition in nondominated discrete time (Theorem 6.1).

Setting

Fix a Polish space $\Omega_1$, a horizon $T \in \mathbb N$ and $d \in \mathbb N$. Let $\Omega_t := \Omega_1^t$ for $t = 0, \dots, T$. Then $\Omega_0$ is a single point and $\Omega := \Omega_T$, and a point of $\Omega_t$ is read as the first $t$ coordinates of a path. The $\sigma$-field $\mathcal F_t$ is the universal completion of $\mathcal B(\Omega_t)$.

For each $t < T$ and each node $\omega \in \Omega_t$ a nonempty convex set $\mathcal P_t(\omega)$ of probability measures on $\Omega_1$ is given, and its graph is an analytic set. The set of possible models $\mathcal P$ consists of all products $P_0 \otimes P_1 \otimes \cdots \otimes P_{T-1}$ whose kernels take values in $\mathcal P_t(\cdot)$. A set is $\mathcal P$-polar if it is null under every $P \in \mathcal P$. A property holds $\mathcal P$-quasi surely (q.s.) if it holds outside a polar set.

Stock prices $S_t : \Omega_t \to \mathbb R^d$ are Borel. A strategy $H \in \mathcal H$ is predictable: $H_u$ is a function of the first $u-1$ coordinates. The wealth at time $t$ is

$$H \bullet S_t = \sum_{u=1}^t H_u \Delta S_u, \qquad \Delta S_u = S_u - S_{u-1}.$$

NA($\mathcal P$) holds if $H \bullet S_T \ge 0$ q.s. implies $H \bullet S_T = 0$ q.s. A martingale measure is a probability $Q$ under which $S$ is a martingale. The set

$$\mathcal Q = \{Q \lll \mathcal P : Q \text{ is a martingale measure}\}$$

contains those $Q$ that are absolutely continuous with respect to some $P \in \mathcal P$ (written $Q \lll \mathcal P$). A function $f$ with values in $[-\infty, \infty]$ is upper semianalytic if every set $\{f > c\}$ is analytic.

At one node $\omega \in \Omega_t$, the increment $\Delta S_{t+1}(\omega, \cdot)$ defines a one-period market under $\mathcal P_t(\omega)$, with its own no-arbitrage condition NA($\mathcal P_t(\omega)$) and one-period martingale measures $\mathcal Q_t(\omega)$. The conditional sublinear expectation is

$$\mathcal E_t(f)(\omega) = \sup_{Q \in \mathcal Q_t(\omega)} E_Q[f(\omega, \cdot)].$$

Formalization targets

Goal: Theorem 6.1 (nondominated optional decomposition)

Let NA($\mathcal P$) hold and let $V$ be an adapted process such that $V_t$ is upper semianalytic and in $L^1(Q)$ for all $Q \in \mathcal Q$ and $t \in \{1, \dots, T\}$. Then the following are equivalent:

1. $V$ is a supermartingale under each $Q \in \mathcal Q$;
2. there exist $H \in \mathcal H$ and an adapted increasing process $K$ with $K_0 = 0$ such that

$$V_t = V_0 + H \bullet S_t - K_t \quad \mathcal P\text{-q.s.}, \qquad t = 0, 1, \dots, T.$$

Milestones

• Lemma 4.6: the set $N_t$ of nodes where NA($\mathcal P_t(\omega)$) fails is universally measurable, and it is polar under NA($\mathcal P$).
• Theorem 4.5: NA($\mathcal P$) holds if and only if every $N_t$ is polar, if and only if every $P \in \mathcal P$ is absolutely continuous with respect to some $Q \in \mathcal Q$.
• Lemma 4.10: $\mathcal E_t(f)$ is upper semianalytic, and there is a universally measurable $y$ with

$$\mathcal E_t(f)(\omega) + y(\omega)\,\Delta S_{t+1}(\omega, \cdot) \ge f(\omega, \cdot) \quad \mathcal P_t(\omega)\text{-q.s.}$$

at every arbitrage-free node where $f(\omega,\cdot) > -\infty$ q.s.

• (6.1): under condition 1 of the goal, $\mathcal E_t(V_{t+1}) \le V_t$ $\mathcal P$-q.s. for every $t < T$.

Significance

The decomposition is the dynamic counterpart of superhedging duality. Duality identifies the price $\sup_{Q} E_Q[f]$. The optional decomposition, applied to the process of conditional superhedging prices, produces one strategy that superhedges under all models at once and a nonnegative increasing process recording the surplus. The proof works in a nondominated model with one strategy $H$ that is measurable in the universal completion, and this is what makes the theorem usable under volatility or model uncertainty, where no single model can be singled out. The equivalence also characterizes the processes that are supermartingales under every $Q \in \mathcal Q$: up to a polar set they are exactly the wealth processes of strategies that consume.

The result is proved in the paper; no part of it has a machine-checked proof, on the platform or in Mathlib. Mathlib has martingales, conditional expectation and analytic sets. It has no quasi-sure analysis, no product of measurable selectors of a random set of measures, no conditional sublinear expectation and no superhedging. The mission produces a machine-checked development of the one-period-to-multi-period machinery of the paper (Theorem 4.5, Lemmas 4.6 and 4.10) and of the decomposition itself.

Difficulty

With one dominating measure, the classical proof works under a fixed equivalent martingale measure and uses conditional expectations and a single null-set structure. Here the measures in $\mathcal P$ may be mutually singular, so conditional expectations under different $Q$ disagree off their supports, and no countable family of measures controls all null sets. The proof has to work node by node, $\omega \mapsto \mathcal P_t(\omega)$. Every object built at a node (the worst-case conditional expectation, a near-optimal measure, a hedging ratio) must then be glued back together measurably in $\omega$. Borel measurability is not preserved by taking suprema over the random set $\mathcal Q_t(\omega)$. Upper semianalyticity is, but only together with measurable selection theorems for analytic sets (Jankov–von Neumann) and the universal completion. The first idea, which is to apply the classical theorem under each $P \in \mathcal P$ separately, fails. It gives one strategy per model, and in general uncountably many models cannot be aggregated into one strategy.

Formalization scope

The Lean development uses the following conventions.

• Paths and measures. $\Omega_t$ is Fin t → Ω₁, and measures are Borel. $\mathcal F_t$-measurability is universal measurability, which is the published platform definition BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable.
• Polar sets. A polar set is null in outer measure under every model. The exceptional sets in the statements are universally measurable, and for such sets this agrees with the paper's definition.
• The model set. $\mathcal P$ consists of the laws of Borel Markov kernels that lie in $\mathcal P_t$ almost surely, which is the paper's equivalent formulation on p. 4.
• Processes. A process is a family V t : (Fin t → Ω₁) → ℝ, so adaptedness is built into the type.
• Strategies. The Lean strategy H u is the paper's $H_{u+1}$.
• Expectations. Expectations of functions with values in $[-\infty, \infty]$ follow (1.1) in EReal, with $\infty - \infty = -\infty$. Suprema over $\mathcal Q_t(\omega)$ are taken in EReal.
• Options. The setting has no options ($e = 0$).
• Page numbers. Pages and indices are those of the arXiv v3 reprint (arXiv:1305.6008v3), not the journal pagination 823–859.

The increasing process $K$ must be adapted and nondecreasing on every path. Dropping monotonicity would make condition 2 trivially true, with $K := V_0 + H \bullet S - V$ for any $H$. Integrability and supermartingale properties are always stated with explicit $Q$-integrability, so Bochner integrals of non-integrable functions cannot make a statement vacuous.

The development needs the following infrastructure:

• analytic sets and measurable selection (some of it exists for Bertsekas–Shreve on the platform);
• measurability of $(\omega, Q) \mapsto E_Q[f(\omega,\cdot)]$;
• products of kernels;
• the one-period fundamental theorem and superhedging duality.

These pieces are shared with the companion mission Arbitrage and Duality in Nondominated Discrete-Time Models I, which formalizes the superhedging theorem. Contributions to either side are welcome. The paper derives (ii) ⇒ (i) from Lemma A.1, a classical fact about local and generalized martingales under one measure, which is not posed as a milestone here.

Selected references

• B. Bouchard, M. Nutz, Arbitrage and duality in nondominated discrete-time models, Ann. Appl. Probab. 25(2), 823–859, 2015. https://doi.org/10.1214/14-AAP1011, arXiv:1305.6008v3 https://arxiv.org/abs/1305.6008
• N. El Karoui, M.-C. Quenez, Dynamic programming and pricing of contingent claims in an incomplete market, SIAM J. Control Optim. 33, 29–66, 1995. MR1311659, https://mathscinet.ams.org/mathscinet-getitem?mr=1311659
• D. O. Kramkov, Optional decomposition of supermartingales and hedging contingent claims in incomplete security markets, Probab. Theory Related Fields 105, 459–479, 1996. MR1402653, https://mathscinet.ams.org/mathscinet-getitem?mr=1402653
• M. Nutz, Superreplication under model uncertainty in discrete time, Finance Stoch. 18, 791–803, 2014. MR3255751, https://mathscinet.ams.org/mathscinet-getitem?mr=3255751
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete Time Case, Mathematics in Science and Engineering 139, Academic Press, 1978. MR0511544, https://mathscinet.ams.org/mathscinet-getitem?mr=0511544

Motivation

In online allocation, requests arrive one at a time and each must be accepted or rejected on arrival, using a limited budget of resources. Revenue management, ad allocation and hiring all fit this pattern. A natural benchmark for an online policy is the prophet, or Offline: the decision maker who sees the whole arrival sequence in advance and acts optimally on it. The regret of a policy is the expected gap between Offline's value and the policy's value. Policies that track a fixed solution of a fluid relaxation lose on the order of $\sqrt T$ (Proposition 1 of the paper), so the question is whether a simple adaptive policy can achieve regret bounded independently of $T$ and of the budget.

The simplest such problem is the multi-secretary problem: hire at most $B$ of $T$ sequentially arriving candidates, each drawn i.i.d. from finitely many ability classes. Arlotto and Gurvich (Stochastic Systems 2019) showed that a budget-ratio policy has regret bounded uniformly in $T$ and $B$, using a martingale argument. Vera and Banerjee (SSRN 3158062; Management Science 2021) introduced the compensated coupling, a sample-path identity that expresses the regret of any online policy as the compensation Offline must be paid to follow it. They used it to prove constant regret for a simple re-solve-and-threshold rule, the Fluid Bayes Selector, with the explicit constant $r_{\max}\sum_{j>1}2/p_j$. This mission formalizes that result together with the compensated coupling it rests on.

Setting

A finite-horizon online decision problem has states $S$, arrival types $\Theta$, actions $A$, a transition function $T(a,s,j)$, a reward function $R(a,s,j)$, and a set $\mathcal F(s)$ of feasible actions in each state. Time is counted as time to go: decisions are made at $t=T,T-1,\dots,1$, and $\theta^t$ is the type arriving at time-to-go $t$. A standing assumption requires the best feasible reward in every state to be attained and to lie in a fixed bounded interval.

Given the whole arrival sequence, Offline's value obeys the Bellman equation

$$V^{\mathrm{off}}(0,s)=0,\qquad V^{\mathrm{off}}(t,s)=\max_{a\in\mathcal F(s)}\{R(a,s,\theta^t)+V^{\mathrm{off}}(t-1,T(a,s,\theta^t))\}.$$

An online policy chooses a feasible action at each time from the arrivals observed so far. Starting from $S^T=s_0$ it produces a state process $S^t$ and a value $V^{\mathrm{on}}=\sum_{t}R(\pi^{\mathrm{on}}(t,S^t,\theta^t),S^t,\theta^t)$, and its regret on a path is $\mathrm{Reg}=V^{\mathrm{off}}(T,s_0)-V^{\mathrm{on}}$. An action is satisfying for Offline at $(t,s)$ when it attains the Bellman maximum. The disagreement set $Q(t,a,s)$ is the set of paths on which it does not, and the marginal compensation $\partial R(t,a,s)$ is the amount by which it falls short.

In the multi-secretary problem there are $n$ classes with rewards $r_1\ge r_2\ge\dots\ge r_n\ge0$ and arrival probabilities $p_j>0$, i.i.d. over time (multinomial arrivals). The state is the remaining budget $b$. Accepting needs $b\ge1$, earns $r_j$ and lowers the budget by one; rejecting earns nothing. With $\bar p_j=\sum_{i\le j}p_i$, the Fluid Bayes Selector (Algorithm 2, in the rounded form of Appendix B.3) behaves as follows at time-to-go $t$ with budget $b$. If $b=0$ it rejects. Otherwise it always accepts class $1$, and it accepts a class $j>1$ iff $b/t\ge\bar p_j-p_j/2$.

Formalization targets

Goal: Theorem 2 (p. 18)

For every horizon $T$ and every initial budget $B$,

$$\mathbb E[\mathrm{Reg}]\ \le\ r_{\max}\sum_{j>1}\frac{2}{p_j}\ \le\ \frac{2(n-1)\,r_{\max}}{p_{\min}},$$

where $r_{\max}=\max_jr_j$ and $p_{\min}=\min_jp_j$. The goal keeps the paper's explicit constant: neither $T$ nor $B$ appears in it.

Milestones

1. Lemma 1 (Compensated Coupling), pathwise: $\mathrm{Reg}=\sum_{t\in[T]}\partial R(t,\pi^{\mathrm{on}}(t,S^t,\theta^t),S^t)\,\mathbf 1_{Q(t,S^t)}$ for any online policy of any problem.
2. Lemma 1, in expectation: $\mathbb E[\mathrm{Reg}]\le\max_{a,j}\partial r(a,j)\sum_t\mathbb P[Q(t,S^t)]$.
3. Eq. (18): $\mathbb P[X-\mathbb E X\le-t\varepsilon]$ and $\mathbb P[X-\mathbb E X\ge t\varepsilon]$ are at most $e^{-2\varepsilon^2t}$ for $X\sim\mathrm{Bin}(t,\alpha)$.
4. Appendix B.3, conditions (1)–(2): when Offline is not satisfied rejecting or accepting the current arrival.
5. Appendix B.3, disagreement bound: $q_1(t,b)=0$ and $q_j(t,b)\le e^{-p_j^2t/2}$ for $j>1$, uniformly in the budget $b$.
6. Appendix B.3, total compensation: $\sum_{t\le T}q(t,B^t)\le\sum_{j>1}p_j\sum_{t\le T}e^{-p_j^2t/2}\le\sum_{j>1}2/p_j$.

Significance

The result. Theorem 2 gives the best known regret bound for the multi-secretary problem with an explicit, simple constant. The compensated coupling (Lemma 1) holds for any finite-horizon problem with exogenous arrivals. It turns a regret bound into a bound on disagreement probabilities, and the paper reuses it for online packing, online matching and general online allocation, and for Bayes Selectors whose disagreement probabilities are only estimated.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of the compensated coupling, is known to us. The mission produces a reusable formal model of finite-horizon online decision problems with an Offline benchmark. It also produces a formal compensated-coupling identity that applies to any policy, and a binomial Chernoff–Hoeffding bound in elementary finite-sum form. Each of these supports other missions on prophet benchmarks, resolving heuristics and network revenue management.

Difficulty

Comparing the online policy with one fixed offline solution does not work: Offline's optimal decisions change with every future arrival, and tracking a single offline plan only gives regret of order $\sqrt T$. The compensated coupling avoids this by re-coupling Offline to Online at every step. That shifts the difficulty to two places. The first is an exact description of when Offline's Bellman equation disagrees with the policy, which involves ties between equal rewards and the boundary budget $b=0$. The second is a bound on the conditional probability of disagreement that is uniform over all budgets. That conditional probability is a binomial tail evaluated at a budget that is itself random but independent of the remaining arrivals.

Formalization scope

Lean conventions:

• Types are Fin n with [NeZero n], and Lean index 0 is the paper's class $1$.
• The ordering $r_1\ge\dots\ge r_n$ is Antitone r, so ties are allowed.
• Rewards are real and non-negative. This is the paper's implicit assumption (rewards are abilities), made explicit.
• The probabilities satisfy $p_j>0$ and $\sum_jp_j=1$.
• Time is time-to-go. θ t is the arrival at time-to-go t, and the counts $Z(t)$ include the current arrival.
• Feasibility is an explicit set of actions rather than a reward of $-\infty$. Offline's value is a real supremum over feasible actions, which equals the Bellman maximum under the standing assumption.
• Offline is the integer full-information optimum of the Bellman equation (2). It is not defined through an LP relaxation.
• For the multi-secretary goal, the expectation is the explicit finite sum over the $n^T$ type sequences weighted by $\prod_tp_{\theta^t}$. Lemma 1's expectation bound is stated on an abstract probability space with integrable regret.
• $\mathbb E[\mathbb P[Q\mid S^t]]$ is written as $\mathbb P[Q]$ (tower property).
• The maximal compensation $\max_{a,j}\partial r(a,j)$ is replaced by any upper bound $C$ on the compensations of feasible actions.
• Conditions (1)–(2) of Appendix B.3 are stated through counts of future arrivals with a better (or equal) reward, which is the exact Bellman characterization. The paper phrases them through a solution $X^{\star t}$ of $(P^\star_t)$, which is not unique when rewards tie.
• The disagreement bounds are stated for every fixed budget $b$, and the total-compensation bound for every budget sequence. Since $B^t$ is independent of the last $t$ arrivals, these imply the paper's statements at the random budget $B^t$.

The policy is the rounded rule of Appendix B.3, which always accepts class $1$ when the budget is positive. Algorithm 2 read literally would reject class $1$ when $b<tp_1/2$, and the bound $\sum_{j>1}$, which excludes class $1$, is proved for the Appendix B.3 rule. The policy is defined by its explicit thresholds and not through an arbitrary optimal solution of the fluid LP, because with tied rewards that LP has several solutions.

A formalization that replaced the expectation by a Bochner integral of a non-measurable function, or Offline by a fluid relaxation, would make the bound trivial or a different theorem. Both are excluded by construction.

Contributions are welcome at every level: proofs of the milestones, a proof of Eq. (18) from Mathlib's sub-Gaussian machinery, and lemmas computing Offline's value in the multi-secretary problem (the top-$b$ rewards among the remaining arrivals), which are reusable beyond this mission.

Selected references

• A. Vera and S. Banerjee, The Bayesian Prophet: A Low-Regret Framework for Online Decision Making, SSRN 3158062 (Management Science 67(3), 2021). https://doi.org/10.2139/ssrn.3158062
• A. Arlotto and I. Gurvich, Uniformly bounded regret in the multisecretary problem, Stochastic Systems 9(3), 2019. https://doi.org/10.1287/stsy.2018.0028
• D. Dubhashi and A. Panconesi, Concentration of Measure for the Analysis of Randomized Algorithms, Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511581274

Motivation

Sinkhorn distributionally robust optimization (Wang, Gao and Xie, arXiv:2109.11926) hedges a learning or decision problem against distribution shift. It minimizes the worst-case expected loss over all distributions within an entropically regularized optimal-transport distance (the Sinkhorn distance) of a nominal distribution $\widehat{\mathbb P}$. Strong duality, the subject of the first mission of this series, reduces the problem at a fixed Lagrange multiplier $\lambda>0$ to minimizing an objective of nested-expectation form,

$$F(\theta)=\mathbb E_{x\sim\widehat{\mathbb P}}\Big[\lambda\epsilon\log\mathbb E_{z\sim\mathbb Q_{x}}\big[e^{f_\theta(z)/(\lambda\epsilon)}\big]\Big].$$

A logarithm sits between the two expectations, so a mini-batch of samples gives a biased estimate of $F$ and of its subgradients, and stochastic gradient methods do not apply directly. Problems of this shape are known as conditional stochastic optimization (Hu, Chen and He 2020, 2021; references [54], [55] of arXiv:2109.11926v5). The paper's algorithmic contribution is a biased stochastic mirror descent (BSMD) for this objective, with two subgradient estimators and explicit complexity guarantees. This mission formalizes that guarantee, Theorem 2 of the paper.

Setting

The decision $\theta$ lives in a closed convex set $\Theta\subseteq\mathbb R^{d_\theta}$. A norm $\|\cdot\|$ on $\mathbb R^{d_\theta}$ satisfies $\mathfrak c\|\cdot\|_2\le\|\cdot\|\le\mathfrak d\|\cdot\|_2$ with $\mathfrak c>0$ (Assumption EC.1), and has dual norm $\|\cdot\|_*$. A distance generating function $\omega$ is continuously differentiable on $\Theta$ and $\kappa$-strongly convex with respect to $\|\cdot\|$. It induces the Bregman divergence $D_\omega(\theta,\theta')=\omega(\theta')-\omega(\theta)-\langle\nabla\omega(\theta),\theta'-\theta\rangle$ and the prox-mapping $\mathrm{Prox}_\theta(y)=\arg\min_{\theta'\in\Theta}\{\langle y,\theta'-\theta\rangle+D_\omega(\theta,\theta')\}$.

The data are a probability measure $\widehat{\mathbb P}$ and a Markov kernel $x\mapsto\mathbb Q_x$ on a measurable space $\mathcal Z$, fixed $\lambda,\epsilon>0$, and a loss $f_\theta(z)$. Assumption 2 requires three things: (I) $f_\theta(z)$ is convex in $\theta$; (II) it is $L_f$-Lipschitz in $\theta$ for the Euclidean norm; (III) $0\le f_\theta(z)\le B$ for $\theta\in\Theta$. Write $K=B/(\lambda\epsilon)$.

The level-$\ell$ approximation replaces the inner expectation by an average of $2^\ell$ i.i.d. draws:

$$F^\ell(\theta)=\mathbb E\Big[\lambda\epsilon\log\Big(2^{-\ell}\textstyle\sum_{j=1}^{2^\ell}e^{f_\theta(z_j)/(\lambda\epsilon)}\Big)\Big],\qquad x\sim\widehat{\mathbb P},\ z_j\mid x\sim\mathbb Q_x .$$

Its sample subgradient is $g^\ell$. The SG estimator is $v^{SG}=g^L$. The RT-MLMC estimator draws a level $\hat\ell\in\{0,\dots,L\}$ with probability $p_\ell=2^{-\ell}/(2-2^{-L})$ and returns $p_{\hat\ell}^{-1}G^{\hat\ell}$, where $G^\ell$ is the antithetic difference between the level-$\ell$ subgradient and the average of its two half-sample versions. BSMD iterates $\theta_{t+1}=\mathrm{Prox}_{\theta_t}(h\,v(\theta_t))$, $t=0,\dots,T-1$, with a fresh sample at every step.

Formalization targets

Goal: Theorem 2 with the explicit parameters of its proof

For $\delta>0$ let $L=\max\big(1,\lceil\log_2(2\lambda\epsilon e^{2K}/\delta)\rceil\big)$, $\theta^*\in\arg\min_\Theta F$, $\bar\theta^*\in\arg\min_\Theta F^L$ and $D=D_\omega(\theta_0,\bar\theta^*)$. With the SG estimator and

$$T=\Big\lceil\frac{8L_f^2D}{\kappa\mathfrak c^2\delta^2}\Big\rceil,\qquad h=\sqrt{\frac{2\kappa\mathfrak c^2D}{TL_f^2}},$$

or with the RT-MLMC estimator, $M^2=2(L+1)L_f^2e^{4K}/\mathfrak c^2$ and

$$T=\Big\lceil\frac{16(L+1)L_f^2De^{4K}}{\kappa\mathfrak c^2\delta^2}\Big\rceil,\qquad h=\sqrt{\frac{2\kappa D}{TM^2}},$$

the average $\hat\theta$ of the iterates is δ-optimal:

$$\mathbb E[F(\hat\theta)]-F(\theta^*)\le\delta .$$

Milestones

1. §4.1.1 (p. 15): $\mathbb E g^\ell$ is a subgradient of $F^\ell$, $\mathbb E G^\ell=\mathbb E g^\ell-\mathbb E g^{\ell-1}$, and hence $\mathbb E v^{RT\text{-}MLMC}=\mathbb E v^{SG}$.
2. Lemma EC.6 (I): $|F^\ell-F|\le\lambda\epsilon e^{2K}2^{-(\ell+1)}$ on $\Theta$.
3. Lemma EC.6 (III): $\mathbb E\|g^\ell\|_2^2\le L_f^2$ and $\mathbb E\|G^\ell\|_2^2\le L_f^2e^{4K}2^{-\ell}$.
4. Lemma EC.7: BSMD with subgradient bias $\Delta_F$ and second moment $M_*^2$ satisfies $\mathbb E[F(\hat\theta)-F(\theta^*)]\le2\Delta_F+M_*\sqrt{2D/(\kappa T)}$.
5. The RT-MLMC second-moment bound $\mathbb E\|v^{RT\text{-}MLMC}\|_*^2\le2(L+1)L_f^2e^{4K}/\mathfrak c^2$ (p. ec20).

Significance

Theorem 2 converts into sample complexities: $O(\delta^{-2})$ draws from $\widehat{\mathbb P}$ with either estimator. From $\mathbb Q_x$, SG needs $O(\lambda\epsilon e^{2K}\delta^{-3})$ draws and RT-MLMC $\tilde O(K^2e^{4K}\delta^{-2})$. The $\widehat{\mathbb P}$-rate matches the lower bound for general convex stochastic programming. This is what makes Sinkhorn DRO computationally competitive with empirical risk minimization, and it is the inner oracle of the paper's bisection search over $\lambda$ (Theorem 3, not part of this mission). Lemma EC.7 is a reusable statement in its own right: mirror descent with uniformly biased stochastic subgradients loses only an additive $2\Delta_F$.

The result is proved in the paper, partly by citation: the bias and variance bounds are attributed to Hu et al. and the BSMD bound to Nemirovski et al. To our knowledge none of it is machine-checked. The mission produces a self-contained Lean proof and, along the way, a formal mirror-descent analysis with biased oracles and an MLMC variance bound for log-sum-exp functionals.

Difficulty

The obvious route is to treat $v$ as an unbiased stochastic subgradient of $F$ and cite standard stochastic mirror descent. That fails because $\mathbb E v$ is a subgradient of $F^L$, not of $F$. Closing the gap requires the uniform bias bound of Lemma EC.6 (I), a second-order Taylor bound for $\log$ on $[1,e^K]$ against the variance of a sample mean. The RT-MLMC bound requires the antithetic cancellation in $G^\ell$ to be exhibited explicitly. The naive bound $\|G^\ell\|\le2L_f$ gives no decay in $\ell$, and the estimator's second moment then grows like $2^L$ instead of $L$. Finally, the expectation over a run of $T$ dependent iterates needs a careful product-measure argument: the iterate $\theta_t$ is a function of $\xi_0,\dots,\xi_{t-1}$, and $\xi_t$ is independent of it.

Formalization scope

• Representation. $\mathbb R^{d_\theta}$ is EuclideanSpace ℝ (Fin d). The mirror norm is a function with the norm axioms and Assumption EC.1, and its dual norm is a real supremum over its unit ball. $\nabla\omega$ is a gradient within $\Theta$.

• Prox-mapping. It is a map characterized by its argmin property on $\Theta$.

• The kernel. $\mathbb Q$ is an arbitrary Markov kernel. This contains the paper's Gibbs kernel $\mathbb Q_{x,\epsilon}$, which the BSMD analysis never uses.

• Subgradients. "$\nabla_\theta$" always means a selected subgradient; no differentiability of the loss is assumed. $g^\ell$ and $G^\ell$ are given in explicit chain-rule form, the same selected subgradients in every block.

• Randomness. A run of length $T$ is driven by $T$ i.i.d. samples under Measure.pi. The RT-MLMC sample is $(\hat\ell,x,z_1,\dots,z_{2^L})$, with level $\hat\ell$ reading the first $2^{\hat\ell}$ draws.

• Measurability and integrability. The prox-mapping and the subgradient selector are measurable. Every expectation in a conclusion comes with its integrability, which rules out a vacuous reading in which a non-integrable quantity has expectation $0$.

• Explicit forms of the paper's $O(\cdot)$. The paper writes $O(\cdot)$ and $\tilde O(\cdot)$; its proof (p. ec20) yields the hyper-parameters stated above. They are fixed in the goal, not quantified existentially:

  • $L=\max(1,\lceil\log(2\lambda\epsilon e^{2K}/\delta)/\log2\rceil)$ for both estimators;
  • SG: $T=\max(1,\lceil8L_f^2D/(\kappa\mathfrak c^2\delta^2)\rceil)$ and $h=\sqrt{2\kappa\mathfrak c^2D/(TL_f^2)}$;
  • RT-MLMC: $M^2=2(L+1)L_f^2e^{4K}/\mathfrak c^2$, $T=\max(1,\lceil16(L+1)L_f^2De^{4K}/(\kappa\mathfrak c^2\delta^2)\rceil)$ and $h=\sqrt{2\kappa D/(TM^2)}$.

  The max 1 guards enforce the paper's $L\in\mathbb N_+$ and $T\ge1$. The sample counts are not stated as Lean claims, since they follow by construction: per iteration, one draw from $\widehat{\mathbb P}$, plus $2^L$ draws from $\mathbb Q_x$ for SG or $(L+1)/(2-2^{-L})$ in expectation for RT-MLMC. Remark EC.1 prints the latter as $L/(2-2^{-L})$.

• Two corrections to the printed text.

  • The output averages $\theta_0,\dots,\theta_{T-1}$. The paper prints $\theta_1,\dots,\theta_T$, for which Lemma EC.7 has a two-dimensional counterexample with $T=1$ (in the Lemma EC.7 item).
  • The RT-MLMC constant $M^2$ keeps the factor $\mathfrak c^{-2}$ that the paper's display drops; the paper's $T$ already carries it. Both versions agree in the Euclidean case $\mathfrak c=1$.

• Contributions welcome. Proofs of the milestones. A reusable Lean development of stochastic mirror descent with biased oracles. The MLMC bias and variance lemmas for $\log$ of a sample mean. A follow-up mission on the bisection search (Theorem 3).

Selected references

• J. Wang, R. Gao, Y. Xie, Sinkhorn Distributionally Robust Optimization, arXiv:2109.11926v5, 2025. https://arxiv.org/abs/2109.11926v5
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust Stochastic Approximation Approach to Stochastic Programming, SIAM J. Optim. 19(4):1574–1609, 2009 (reference [77] of arXiv:2109.11926v5).
• Y. Hu, X. Chen, N. He, Sample Complexity of Sample Average Approximation for Conditional Stochastic Optimization, SIAM J. Optim. 30(3):2103–2133, 2020 (reference [54] of arXiv:2109.11926v5).
• Y. Hu, X. Chen, N. He, On the Bias-Variance-Cost Tradeoff of Stochastic Optimization, NeurIPS 2021 (reference [55] of arXiv:2109.11926v5).
• J. H. Blanchet, P. W. Glynn, Unbiased Monte Carlo for Optimization and Functions of Expectations via Multi-Level Randomization, Winter Simulation Conference, 3656–3667, 2015 (reference [22] of arXiv:2109.11926v5).

Motivation

Distributionally robust optimization (DRO) hedges a decision against uncertainty in the data distribution. It minimizes the worst-case expected loss over an ambiguity set of distributions around a nominal one, typically the empirical distribution of the data. Ambiguity sets built from the Wasserstein (optimal-transport) distance are standard in operations research and machine learning, because they contain distributions with supports different from the nominal one. A known drawback is that the worst case is attained at discrete distributions, which is unrealistic when the true distribution is continuous.

Wang, Gao and Xie (arXiv:2109.11926v5) replace the Wasserstein distance by the Sinkhorn distance, the entropically regularized optimal-transport cost of Cuturi (NeurIPS 2013). Their main theorem is a strong duality result: the infinite-dimensional worst-case problem over a Sinkhorn ball equals a one-dimensional convex minimization. This mission formalizes that theorem.

Timeline:

• 2013: Cuturi introduces the Sinkhorn distance as a fast surrogate for optimal transport.
• 2016–2023: strong duality for Wasserstein DRO, by Gao and Kleywegt (arXiv:1604.02199), Blanchet and Murthy (arXiv:1604.01446), and Zhang, Yang and Gao (arXiv:2205.00362).
• 2021–2025: Wang, Gao and Xie prove strong duality for Sinkhorn DRO for a general measurable sample space, a measurable loss and an arbitrary nominal distribution.

Setting

Let $\mathcal Z$ be a measurable space. The data are:

• a nominal probability distribution $\widehat{\mathbb P}$;
• a σ-finite reference measure $\nu\neq0$;
• a transport cost $c:\mathcal Z\times\mathcal Z\to[0,\infty]$;
• a regularization parameter $\epsilon>0$ and a radius $\rho\in\mathbb R$;
• a loss $f:\mathcal Z\to\mathbb R\cup\{\infty\}$.

For a probability distribution $\mathbb P$, the Sinkhorn distance (Definition 1, with reference measures $\widehat{\mathbb P}$ and $\nu$) is

$$\mathcal W_\epsilon(\widehat{\mathbb P},\mathbb P)=\inf_{\gamma\in\Gamma(\widehat{\mathbb P},\mathbb P)}\mathbb E_{(x,y)\sim\gamma}\Big[c(x,y)+\epsilon\log\frac{d\gamma(x,y)}{d\widehat{\mathbb P}(x)\,d\nu(y)}\Big],$$

where $\Gamma(\widehat{\mathbb P},\mathbb P)$ is the set of couplings with these marginals. The primal value is the worst-case expected loss over the Sinkhorn ball,

$$V=\sup\big\{\mathbb E_{\mathbb P}[f]:\ \mathcal W_\epsilon(\widehat{\mathbb P},\mathbb P)\le\rho\big\}.$$

The dual problem uses three more objects. The kernel distribution is $d\mathbb Q_{x,\epsilon}(z)\propto e^{-c(x,z)/\epsilon}\,d\nu(z)$. The adjusted radius is $\bar\rho=\rho+\epsilon\,\mathbb E_{x\sim\widehat{\mathbb P}}[\log\mathbb E_{z\sim\nu}e^{-c(x,z)/\epsilon}]$. The dual value is

$$V_D=\inf_{\lambda\ge0}\Big\{\lambda\bar\rho+\lambda\epsilon\,\mathbb E_{x\sim\widehat{\mathbb P}}\Big[\log\mathbb E_{z\sim\mathbb Q_{x,\epsilon}}\big[e^{f(z)/(\lambda\epsilon)}\big]\Big]\Big\},$$

where the objective at $\lambda=0$ is $\operatorname{ess\,sup}_\nu f$.

Assumption 1 requires:

• $c$ is measurable and, for $\widehat{\mathbb P}$-a.e. $x$, finite $\nu$-a.e.;
• $\mathbb E_\nu e^{-c(x,\cdot)/\epsilon}<\infty$ for $\widehat{\mathbb P}$-a.e. $x$;
• $f$ is measurable;
• every coupling with first marginal $\widehat{\mathbb P}$ disintegrates along $\widehat{\mathbb P}$.

Condition 1 asks for some $\lambda>0$ with $\mathbb E_{\mathbb Q_{x,\epsilon}}[e^{f/(\lambda\epsilon)}]<\infty$ for $\widehat{\mathbb P}$-a.e. $x$.

Formalization targets

Goal: Theorem 1 (strong duality)

Under Assumption 1:

$$\text{(I) }\ \exists\,\mathbb P:\ \mathcal W_\epsilon(\widehat{\mathbb P},\mathbb P)\le\rho\iff\bar\rho\ge0;\qquad \text{(II) }\ \bar\rho\ge0\implies V=V_D.$$

(III) If $\bar\rho>0$, then $V=V_D<\infty$ when the dual objective is finite at some $\lambda>0$, and $V=V_D=\infty$ otherwise.

(IV) If $\bar\rho>0$ and Condition 1 holds, then $0$ is the unique dual minimizer if and only if

$$\operatorname{ess\,sup}_\nu f<\infty\quad\text{and}\quad\bar\rho\ge\epsilon\,\mathbb E_{x\sim\widehat{\mathbb P}}\big[\log\big(1/\mathbb Q_{x,\epsilon}(A)\big)\big],\qquad A=\{f=\operatorname{ess\,sup}_\nu f\}.$$

Milestones

The milestones are the numbered lemmas of the paper's proof, in the order the proof uses them:

• Lemma EC.2: the Gibbs variational principle, $\sup_{\mathbb P\ll\nu}\mathbb E_{\mathbb P}[f-\tau\log\frac{d\mathbb P}{d\nu}]=\tau\log\mathbb E_\nu e^{f/\tau}$.
• Lemma EC.3: measurability of the inner value $x\mapsto v_x(\lambda)$.
• Lemma 1: weak duality $V\le V_D$.
• Lemma 2: a KL-constrained reformulation of the primal problem.
• Lemma EC.4: existence of a dual minimizer.
• Lemma 3: the first-order condition (9) and uniqueness when $\lambda^*>0$.
• Lemma EC.5: the criterion for $\lambda^*=0$.

Significance

The result. Theorem 1 turns a supremum over an infinite-dimensional set of distributions into a scalar convex program. That program can be solved by first-order methods using only samples from $\widehat{\mathbb P}$ and from the kernels $\mathbb Q_{x,\epsilon}$, which is the basis of the paper's algorithm (Section 4). The proof also constructs the worst-case distribution: it is absolutely continuous with respect to $\nu$, not discrete. Theorem 1(IV) says exactly when the ambiguity constraint is binding. The finite-support conic reformulation (Corollary 1) and the closed form for linear losses (Example 1) both follow from the theorem.

Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. Formalization adds two things. First, it pins down the extended-valued conventions: $V$, $V_D$ and $f$ all take values in $[-\infty,\infty]$, and the paper does not specify how undefined expectations and the $\lambda=0$ objective are treated. Second, it checks every case of the proof, including the degenerate ones. Doing so has already corrected two statements; see Formalization scope.

Difficulty

Weak duality (Lemma 1) is Lagrangian relaxation plus the Gibbs principle. The difficulty is the reverse inequality $V\ge V_D$. Interchanging the supremum over distributions with the infimum over $\lambda$ requires a minimax theorem. The usual minimax theorems need compactness or semicontinuity in the distribution variable. The paper's setting has neither: $\mathcal Z$ is an arbitrary measurable space, $f$ is only measurable and may be $+\infty$, and $\widehat{\mathbb P}$ is arbitrary. So a minimax theorem cannot be applied directly.

The proof instead constructs near-optimal primal distributions from the dual minimizer. This needs three separate cases:

• $\lambda^*>0$, with a first-order condition;
• $\lambda^*=0$, with a distribution concentrated on the essential maximizers of $f$;
• Condition 1 fails, with a truncation argument.

Each case needs integrability facts about $\mathbb E_{\mathbb Q_{x,\epsilon}}[e^{f/(\lambda\epsilon)}]$ in which $x$ and $\lambda$ interact. Disintegrating couplings (Assumption 1(IV)) and making the extended-valued expectations meaningful are a further source of work in Lean.

Formalization scope

All values (primal value, Sinkhorn distance, dual objective) are EReal. Expectations are the published DupacovaWets.Consistency.expect: $\int g^+-\int g^-$, with lower Lebesgue integrals in $[0,\infty]$ and the convention $\infty-\infty=+\infty$. The Bochner integral appears only in $\bar\rho$, which every theorem assumes finite.

Further conventions:

• Sinkhorn distance. The cost and the entropy form a single integrand. A coupling not absolutely continuous with respect to $\widehat{\mathbb P}\otimes\nu$ contributes $+\infty$. An infeasible primal has $V=-\infty$.
• Dual objective. The value at $\lambda=0$ is defined as Mathlib's essSup f ν, not as a limit. Logarithms are ENNReal.log, so $\log\infty=\infty$ and $\log 0=-\infty$; $e^{+\infty}=+\infty$.
• Kernels. $\mathbb Q_{x,\epsilon}$ is a normalized withDensity measure. Families $\{\gamma_x\}_{x\in\operatorname{supp}\widehat{\mathbb P}}$ are Markov kernels on all of $\mathcal Z$.

Hypotheses added to the page:

• $\nu$ is σ-finite and nonzero;
• $\epsilon>0$;
• $x\mapsto\log\mathbb E_\nu e^{-c(x,\cdot)/\epsilon}$ is $\widehat{\mathbb P}$-integrable, so that $\bar\rho\in\mathbb R$.

"$\nu\{0\le c<\infty\}=1$" is read as "$\nu$-a.e.". "$\lambda^*=0$" is read as "$0$ is the unique dual minimizer".

Corrections to the paper:

• Theorem 1(III). The paper's version with Condition 1 is false: a.e.-finite inner expectations do not make the dual objective finite. A counterexample on $\mathbb N$ is in the goal's note. The goal is stated with the integrated condition "the dual objective is finite at some $\lambda>0$".
• Lemma 3. The lemma is stated under the added hypothesis that the dual objective is finite at some $\lambda_1<\lambda^*$ (and is not $-\infty$ at $\lambda^*$). Without it, $\lambda^*$ can sit at the edge of the domain where the objective is finite, and (9) fails.

No statement involves an $O(\cdot)$ constant.

A formalization that lets an undefined Sinkhorn integrand evaluate to $-\infty$ (Mathlib's $\top+\bot=\bot$) is ruled out: it would put every distribution into the ball and make the theorem trivial. The combined integrand and the $+\infty$ convention exclude this.

A complete development needs:

• a Gibbs/Donsker–Varadhan variational principle for σ-finite reference measures and extended-valued functions;
• disintegration of couplings;
• convexity and differentiation of $\lambda\mapsto\lambda\log\mathbb E e^{f/\lambda}$.

The first two are reusable well beyond this mission. Contributions toward any milestone, and toward these general lemmas, are welcome.

Selected references

• J. Wang, R. Gao, Y. Xie, Sinkhorn Distributionally Robust Optimization, arXiv:2109.11926v5, 2025. https://arxiv.org/abs/2109.11926
• M. Cuturi, Sinkhorn Distances: Lightspeed Computation of Optimal Transport, NeurIPS, 2013. https://arxiv.org/abs/1306.0895
• R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research, 2023. https://arxiv.org/abs/1604.02199
• J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research, 2019. https://arxiv.org/abs/1604.01446
• L. Zhang, J. Yang, R. Gao, A Short and General Duality Proof for Wasserstein Distributionally Robust Optimization, Operations Research, 2024. https://arxiv.org/abs/2205.00362