Operations Research

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

Motivation

Classical arbitrage pricing fixes one probability measure $P$ describing the market and asks for the cheapest way to dominate a payoff $P$-almost surely. When the model itself is uncertain, this choice is not available: a trader who only trusts a family $\mathcal P$ of possible models wants a hedge that works under every one of them. Two literatures meet here. Robust (model-independent) finance studies hedging that must hold for all paths, as in the martingale-optimal-transport approach to option bounds (Beiglböck, Henry-Labordère, Penkner, 2013). Nondominated model uncertainty studies families $\mathcal P$ with no single reference measure, as in the quasi-sure analysis of Denis–Martini (2006) and the volatility-uncertainty literature. Bouchard and Nutz (2015) give a discrete-time framework that contains both extremes (all measures on a path space; a single measure) and prove the fundamental theorems and superhedging duality for it.

Timeline of the dominated and robust predecessors:

• 1990. Dalang, Morton and Willinger prove the discrete-time fundamental theorem of asset pricing (FTAP) for one measure.
• 2001. Kabanov and Stricker give a short proof of the closedness of the superhedgeable cone behind the DMW theorem. The proof of Theorem 2.2 follows their argument.
• 2013. Acciaio, Beiglböck, Penkner, Schachermayer prove a model-independent FTAP for a pathwise no-arbitrage notion, with options.
• 2015. Bouchard and Nutz prove the FTAP, the superhedging theorem and the second FTAP under a nondominated family $\mathcal P$, with dynamic trading in stocks and static trading in finitely many options.

Setting

Fix a horizon $T\in\mathbb N$ and a Polish space $\Omega_1$. Paths are $\omega=(\omega_1,\dots,\omega_T)\in\Omega=\Omega_1^T$, and $\Omega_t=\Omega_1^t$ holds the first $t$ coordinates. Information at time $t$ is the universal completion $\mathcal F_t$ of the Borel $\sigma$-field of $\Omega_t$.

For each $t<T$ and history $\omega\in\Omega_t$, a nonempty convex set $\mathcal P_t(\omega)$ of probability measures on $\Omega_1$ describes the possible laws of the next coordinate. Its graph must be an analytic set. The set of models $\mathcal P$ consists of all products $P=P_0\otimes P_1\otimes\cdots\otimes P_{T-1}$ whose kernels choose $P_t(\omega)\in\mathcal P_t(\omega)$. A property holds $\mathcal P$-quasi surely (q.s.) if it holds $P$-a.s. for every $P\in\mathcal P$.

There are $d$ stocks with Borel prices $S_t:\Omega_t\to\mathbb R^d$ and $e$ options $g=(g^1,\dots,g^e)$, Borel on $\Omega$, bought or sold at time $0$ at price $0$. A semistatic strategy $(H,h)$ consists of a predictable $H$ and a vector $h\in\mathbb R^e$; its terminal gain is

$$H\bullet S_T+hg=\sum_{u=1}^T H_u\,(S_u-S_{u-1})+\sum_{i=1}^e h^ig^i .$$

No-arbitrage NA($\mathcal P$) says that a gain which is q.s. nonnegative is q.s. zero. The superhedging price of a claim $f$ is

$$\pi(f)=\inf\{x\in\mathbb R:\ \exists (H,h),\ x+H\bullet S_T+hg\ge f\ \ \mathcal P\text{-q.s.}\}.$$

The dual objects are the martingale measures $Q\lll\mathcal P$, meaning $Q\ll P$ for some $P\in\mathcal P$. Under $Q$ the stock $S$ is a martingale and $E_Q[g^i]=0$ for all $i$; they form the set $\mathcal Q$. Given a weight $\varphi\ge1$, set $\mathcal Q_\varphi=\{Q\in\mathcal Q: E_Q[\varphi]<\infty\}$. Expectations of arbitrary measurable functions use the convention $E[f]=E[f^+]-E[f^-]$ with $\infty-\infty=-\infty$.

Formalization targets

Goal: Theorem 5.1(b)

Let $\varphi\ge1$ be a random variable with $|g^i|\le\varphi$, let NA($\mathcal P$) hold, and let $f$ be upper semianalytic with $|f|\le\varphi$. Then

$$\pi(f)=\sup_{Q\in\mathcal Q_\varphi}E_Q[f]\in(-\infty,\infty],$$

and some $(H,h)$ satisfies $\pi(f)+H\bullet S_T+hg\ge f$ $\mathcal P$-q.s.

Milestones

The milestones follow the paper's proof:

1. General setting (§2). Closedness of the superhedgeable cone under q.s. convergence (Theorem 2.2), and existence of optimal strategies (Theorem 2.3).
2. One-period market (§3). The fundamental lemma (Lemma 3.3), the one-period FTAP (Theorem 3.1), approximation lemmas (Lemmas 3.5, 3.6) and one-period duality (Theorem 3.4).
3. Expectation bound (Lemma A.2). The elementary bound $E_Q[f]\le x$ for a superhedge under a consistent local martingale measure.
4. Multi-period market without options (§4). Local characterization of NA (Lemma 4.6, Theorem 4.5), measurable one-step duality (Lemma 4.10), dynamic superhedging (Lemma 4.13) and duality (Theorem 4.9).
5. With options (§5). The first and second fundamental theorems (Theorem 5.1(a), (c)).

Significance

The superhedging theorem identifies the robust price of a claim as a supremum of linear prices. This turns a hedging problem into an optimization over measures, which is how robust option bounds are computed in practice. Remark 1.4 of the paper gives another consequence: every martingale inequality $E[f(M_1,\dots,M_T)]\le a$ follows from a pathwise inequality $f\le a+H\bullet S_T$. The first and second fundamental theorems make the nondominated framework a complete analogue of the classical theory. NA($\mathcal P$) is equivalent to $\mathcal P$ and $\mathcal Q$ sharing their polar sets, and replicable claims are those whose price is the same under every martingale measure.

All results are proved in the paper. None of them, nor the classical dominated discrete-time FTAP, is formalized in Lean or Mathlib as far as is known. A formalization produces machine-checked statements of the model (analytic random sets, products of universally measurable kernels, quasi-sure analysis) and proofs of the fundamental theorems on top of it. Alternative arguments and extensions (portfolio constraints, infinitely many options) are also welcome.

Difficulty

There is no reference measure. Two dominated tools therefore fail. Closedness in $L^0(P)$ cannot be applied, because convergence must hold quasi surely. A Hahn–Banach separation in a single $L^p(P)$ space cannot produce martingale measures either. The paper argues one period at a time instead and glues the periods together measurably. That gluing is where the work lies. The one-period dual value $\mathcal E_t(f)(\omega)$ and the one-period hedge $y(\omega)$ must depend measurably on the history $\omega$, but the value function of a Borel claim need not be Borel. The argument therefore runs in the class of upper semianalytic functions and needs measurable selection theorems for analytic sets. A recursion that tries to keep everything Borel breaks down at the first step.

Formalization scope

• Spaces. $\Omega_t$ is Fin t → Ω₁ with [PolishSpace Ω₁] [BorelSpace Ω₁]. Measures are Borel measures, and $\mathcal F_t$-measurability is universal measurability. The published definition BertsekasShreve.AnalyticSelection.Measurability is reused for this.
• Models. $\mathfrak P(\Omega_1)$ is Mathlib's ProbabilityMeasure with the weak topology. $\mathcal P$ is generated by Borel Markov kernels lying in $\mathcal P_t(\cdot)$ almost surely; this is the paper's equivalent formulation on p. 4.
• Strategies. Lean's H u is the paper's $H_{u+1}$, a universally measurable function of the first $u$ coordinates.
• Values in EReal. Expectations of non-integrable functions are the extended expectation $E[f^+]-E[f^-]$. Prices are EReal infima with $\inf\emptyset=+\infty$, and suprema over $\mathcal Q_\varphi$ are EReal suprema.
• Settings. The §2 and §3 milestones are stated in the paper's more general settings: a general filtered space, and a one-period market on an arbitrary measurable space.
• Citations. Page numbers are those of the arXiv v3 reprint (arXiv:1305.6008v3), not the journal's pp. 823–859.

Two encodings would trivialize the mission and are excluded. Replacing $\mathcal P$ by an arbitrary set of measures drops the product structure that the theorems need. Bochner integrals for $E_Q[f]$ would return $0$ on non-integrable claims and make the duality meaningless. Neither encoding is used.

A complete development needs:

• analytic and universally measurable sets and the Jankov–von Neumann selection theorem;
• products of universally measurable kernels;
• quasi-sure analysis;
• relative interiors and separation in $\mathbb R^d$;
• discrete-time local and generalized martingales.

The selection and kernel infrastructure is reusable well beyond this paper, for instance in dynamic programming on Borel spaces. Contributions of these foundations are welcome.

Selected references

• B. Bouchard, M. Nutz, Arbitrage and duality in nondominated discrete-time models, Ann. Appl. Probab. 25(2) (2015) 823–859. https://arxiv.org/abs/1305.6008 , https://doi.org/10.1214/14-AAP1011
• R. C. Dalang, A. Morton, W. Willinger, Equivalent martingale measures and no-arbitrage in stochastic securities market models, Stochastics Stochastics Rep. 29 (1990) 185–201. https://mathscinet.ams.org/mathscinet-getitem?mr=1041035
• B. Acciaio, M. Beiglböck, F. Penkner, W. Schachermayer, A model-free version of the fundamental theorem of asset pricing and the super-replication theorem, Math. Finance 26(2) (2016) 233–251. https://arxiv.org/abs/1301.5568
• M. Beiglböck, P. Henry-Labordère, F. Penkner, Model-independent bounds for option prices — a mass transport approach, Finance Stoch. 17(3) (2013) 477–501. https://arxiv.org/abs/1106.5929
• L. Denis, C. Martini, A theoretical framework for the pricing of contingent claims in the presence of model uncertainty, Ann. Appl. Probab. 16 (2006) 827–852. https://mathscinet.ams.org/mathscinet-getitem?mr=2244434
• Y. Kabanov, C. Stricker, A teachers' note on no-arbitrage criteria, Séminaire de Probabilités XXXV, Lecture Notes in Math. 1755 (2001) 149–152. https://mathscinet.ams.org/mathscinet-getitem?mr=1837282
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (Chapter 7, analytic sets and measurable selection).

Motivation

A chance-constrained program minimizes a cost $f(x)$ over decisions $x\in\mathbb R^n$ subject to the requirement that a random constraint holds with probability at least $1-\alpha$: $\mathbb P\big(C(x,\xi)\le0\big)\ge1-\alpha$, where $C(x,\xi)=\max_{j=1,\dots,m}c_j(x,\xi)$ collects $m$ constraint functions and $\alpha\in(0,1)$ is a risk level. Such constraints model reliability requirements in power systems, finance and engineering design. They are hard to handle numerically: the probability is rarely available in closed form, its sample estimate is a step function of $x$, and the feasible region is in general nonconvex.

Peña-Ordieres, Luedtke and Wächter (arXiv:1905.07377v2; SIAM J. Optim. 30(3), 2020, DOI 10.1137/19M1261985) replace the probability by a smoothed sample quantile, which turns the chance constraint into a single smooth nonlinear constraint, and solve the resulting problem with a trust-region method built on an $\ell_1$ exact penalty, in the spirit of the S$\ell_1$QP method for regular nonlinear programs (Nocedal and Wright). This mission formalizes the analytic core of that method: the smoothed quantile is well defined and has a bounded, Lipschitz gradient, and the piecewise quadratic model used to compute trust-region steps agrees with the penalty function up to second order.

Setting

Fix $\varepsilon>0$. The smoothed indicator $\Gamma_\varepsilon:\mathbb R\to[0,1]$ equals $1$ on $(-\infty,-\varepsilon]$, $0$ on $[\varepsilon,\infty)$, and a strictly decreasing function $\gamma_\varepsilon$ in between, chosen so that $\Gamma_\varepsilon$ is differentiable (equation (2.2)). The concrete choice is the quartic kernel (2.6),

$$\gamma_\varepsilon(y)=\tfrac{15}{16}\Big(-\tfrac15(y/\varepsilon)^5+\tfrac23(y/\varepsilon)^3-y/\varepsilon+\tfrac8{15}\Big),$$

which makes $\Gamma_\varepsilon$ twice continuously differentiable.

Fix a sample $\xi_1,\dots,\xi_N$ of the random vector. For $z\in\mathbb R^N$, the smoothed $(1-\alpha)$-quantile $Q_\varepsilon(z)$ is the number $q$ solving

$$\sum_{i=1}^N\Gamma_\varepsilon(z_i-q)=(1-\alpha)N. \tag{2.3}$$

It is applied to the vector $C^N(x)$ with entries $[C^N(x)]_i=\max_jc_j(x,\xi_i)$, and the smoothed sample problem requires $Q_\varepsilon(C^N(x))\le0$.

With deterministic constraints $g:\mathbb R^n\to\mathbb R^p$ and a penalty parameter $\pi>0$, the exact penalty function is

$$\varphi_\pi(x)=f(x)+\pi\Big(\|[g(x)]^+\|_1+[Q_\varepsilon(C^N(x))]^+\Big). \tag{5.3}$$

The trust-region step at $x$ minimizes the model

$$m(x,H;d)=f(x)+\nabla f(x)^{\mathsf T}d+\tfrac12d^{\mathsf T}Hd+\pi\Big(\|[g(x)+\nabla g(x)^{\mathsf T}d]^+\|_1+[\widetilde Q_\varepsilon(C^N(x);\widetilde C^N(x;d)-C^N(x))]^+\Big), \tag{5.6}$$

where $H$ is a symmetric matrix, $\widetilde Q_\varepsilon(z;p)=Q_\varepsilon(z)+\nabla Q_\varepsilon(z)^{\mathsf T}p$ and $[\widetilde C^N(x;d)]_i=\max_j\{c_j(x,\xi_i)+\nabla c_j(x,\xi_i)^{\mathsf T}d\}$.

Formalization targets

Goal: Proposition 5.3

If $f$ and $g$ have Lipschitz gradients, each $c_j(\cdot,\xi_i)$ is $L$-Lipschitz with $L'$-Lipschitz gradient, $\gamma_\varepsilon$ is the quartic kernel and $(1-\alpha)N\notin\mathbb Z$, then for fixed $L_H$ there is a constant $K$ with

$$|\varphi_\pi(x+d)-m(x,H;d)|\le K\|d\|^2\qquad\text{for all }x,d\in\mathbb R^n,\ H=H^{\mathsf T},\ \|H\|\le L_H .$$

The constant is not specified, so the goal survives any sharpening of the estimate.

Milestones

1. Lemma 2.1: equation (2.3) has a unique solution when $\gamma_\varepsilon$ is strictly decreasing, $\Gamma_\varepsilon$ is differentiable and $(1-\alpha)N\notin\mathbb Z$.
2. Gradient formula (proof of Proposition 4.1): $[\nabla Q_\varepsilon(z)]_i=\Gamma'_\varepsilon(z_i-Q_\varepsilon(z))/\sum_j\Gamma'_\varepsilon(z_j-Q_\varepsilon(z))$.
3. Gradient bounds: the denominator is at most $-\kappa<0$ uniformly in $z$, and $0\le[\nabla Q_\varepsilon(z)]_i\le1$.
4. Proposition 4.1: $Q_\varepsilon$ has bounded Lipschitz continuous gradients.
5. Linearization bound (5.7)–(5.8): $\|C^N(x+d)-\widetilde C^N(x;d)\|_2\le\sqrt N\,L'\|d\|^2$.
6. Proposition 5.1 (companion): a local minimum $x^*$ of the quantile-constrained problem (5.1) gives the local minimum $(x^*,C^N(x^*))$ of the lifted problem (5.2).

Significance

Proposition 5.3 is the hypothesis under which the trust-region convergence theory of Conn, Gould and Toint (cited as Theorem 5.4, from their Theorem 11.2.5) applies: it guarantees that the method of §5 converges to stationary points of $\varphi_\pi$. Combined with the exact-penalty result of Curtis and Overton (cited as Theorem 5.2), which says that for $\pi$ large enough local minimizers of the smoothed problem are local minimizers of $\varphi_\pi$, this justifies solving the smoothed chance-constrained problem by minimizing $\varphi_\pi$. Proposition 4.1 is independently useful: it says that the smoothed quantile can be handed to any smooth nonlinear solver as a constraint with a bounded, Lipschitz gradient.

The results are proved in the paper. None of them has a machine-checked proof that this mission is aware of. A formalization would also settle two points the printed proofs leave thin: the uniform lower bound on the denominator in Proposition 4.1, which the paper asserts without argument, and the existence part of Lemma 2.1, whose printed proof argues only uniqueness.

Difficulty

The model error splits into three parts. The $f$ and $g$ parts are standard Taylor estimates. The quantile part is the substance. First, $Q_\varepsilon$ is defined only implicitly, so its differentiability needs the implicit function theorem, and its gradient bound needs a lower bound on $\big|\sum_j\Gamma'_\varepsilon(z_j-Q_\varepsilon(z))\big|$ that is uniform over all $z\in\mathbb R^N$, not just pointwise. The pointwise statement is easy: some sample lies strictly inside the smoothing window. The uniform statement needs a quantitative version of that fact, which uses the fractional part of $(1-\alpha)N$. Second, $C^N$ is a maximum of smooth functions and is not differentiable, so the model linearizes each $c_j$ before taking the maximum; one has to show this costs only $O(\|d\|^2)$, uniformly in $x$.

Formalization scope

All objects are defined in one module, SmoothCCP.PenaltyModel.Setting. Decisions and directions live in EuclideanSpace ℝ (Fin n), so gradients and $d^{\mathsf T}Hd$ are inner products. $H$ is a self-adjoint continuous linear operator and $\|H\|$ is its operator norm. Sample values are a fixed list ξs : Fin N → Ξ; this mission involves no probability. $Q_\varepsilon$ is a function on Fin N → ℝ (sup norm), defined as the least root of (2.3) via sInf. Its gradient is the Fréchet derivative. $\Gamma'_\varepsilon$ is deriv of the smoothed indicator, which is differentiable for the quartic kernel, including at $\pm\varepsilon$. The maximum over $j$ uses Finset.sup' and needs $m\ge1$ (the paper's §5 has $m>1$). The Euclidean norm on $\mathbb R^N$ appears explicitly only in milestone 5, where it is written $\sqrt{\sum_i(\cdot)^2}$ to match the printed factor $\sqrt N$.

Standing hypotheses: $\varepsilon>0$, $0<\alpha<1$, $N\ge1$, and $(1-\alpha)N\notin\mathbb Z$. From Proposition 4.1 on, $\gamma_\varepsilon$ is the quartic kernel. Three readings are disclosed in the goal's statement. The Lipschitz hypotheses (5.4)–(5.5) are assumed on all of $\mathbb R^n$ and per component $c_j$, because the conclusion ranges over all $x,d\in\mathbb R^n$. The quartic kernel and $(1-\alpha)N\notin\mathbb Z$ are assumed because the proof uses Proposition 4.1. The $O(\|d\|^2)$ constant is quantified after all data and $L_H$ and before $x$, $d$, $H$.

$Q_\varepsilon$ is the paper's quantile, defined from (2.3), not a function assumed to satisfy it. A statement in which the uniform constant may depend on $x$, $d$ or $H$, or in which (2.3) has no root, would be trivial and is excluded.

A complete development needs the implicit function theorem for $Q_\varepsilon$ (Mathlib's HasStrictFDerivAt.implicitFunction or a one-dimensional argument), first-order Taylor bounds for functions with Lipschitz gradients, and elementary facts about the quartic kernel. The Taylor bounds and the facts about maxima of linearizations are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• A. Peña-Ordieres, J. R. Luedtke, A. Wächter, Solving chance-constrained problems via a smooth sample-based nonlinear approximation, SIAM J. Optim. 30(3), 2020. Preprint arXiv:1905.07377v2. https://arxiv.org/abs/1905.07377v2, https://doi.org/10.1137/19M1261985
• J. Nocedal, S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006 (the S$\ell_1$QP method). https://doi.org/10.1007/978-0-387-40065-5
• F. E. Curtis, M. L. Overton, A sequential quadratic programming algorithm for nonconvex, nonsmooth constrained optimization, SIAM J. Optim. 22(2), 2012, pp. 474–500. https://doi.org/10.1137/090780201
• A. R. Conn, N. I. M. Gould, Ph. L. Toint, Trust-Region Methods, SIAM, 2000. https://doi.org/10.1137/1.9780898719857

Motivation

A chance-constrained program asks for a decision that satisfies uncertain constraints with high probability rather than surely:

$$\min_{x\in X} f(x) \quad\text{s.t.}\quad \mathbb P\bigl(c_j(x,\xi)\le 0,\ j=1,\dots,m\bigr)\ge 1-\alpha. \tag{1.1}$$

Such models appear in power-system operation, portfolio selection, chemical-process and reservoir management, and other settings where requiring the constraints for every realization is too conservative (Nemirovski–Shapiro 2006; the paper's introduction lists applications). The probability is rarely available in closed form, and when the distribution of $\xi$ is only accessible through samples, the feasible set of the empirical counterpart is a union of polyhedral-like pieces: it is non-smooth and non-convex, and the empirical quantile introduces many spurious local minima (Peña-Ordieres, Luedtke, Wächter 2020, §2).

Peña-Ordieres, Luedtke and Wächter replace the indicator inside the empirical probability by a smooth kernel with bandwidth $\varepsilon$, which turns the sample constraint into a differentiable one suitable for nonlinear programming solvers. This mission formalizes the paper's consistency result: as the sample size grows and the bandwidth shrinks, jointly, the optimal values and optimal solutions of the smoothed sample problem converge to those of the true problem with probability one.

Timeline. Consistency of sample approximations of chance constraints with the plain empirical cdf goes back to Pagnoncelli, Ahmed, Shapiro 2009 (reference [36] of the paper; its Propositions 2.1 and 2.2). Luedtke–Ahmed 2008 gave finite-sample feasibility guarantees for the same empirical approximation. Convergence with respect to a smoothing parameter alone was studied by Geletu, Hoffmann, Klöppel and Li (SIAM J. Optim. 27, 2017), Hong, Yang, Zhang 2011 and Hu, Hong and Zhang (IIE Trans. 45, 2013) (references [15], [25], [26] of the paper). Peña-Ordieres–Luedtke–Wächter 2020 (SIAM J. Optim. 30(3)) treat both parameters simultaneously; Theorem 3.5 of the preprint arXiv:1905.07377v2 is the result posed here.

Setting

Decisions are vectors $x\in\mathbb R^n$ restricted to a closed set $X$. The random data $\xi$ takes values in a measurable space $\Xi$ with law $\mathbb P_\xi$. The constraints are aggregated into one scalar function $C(x,\xi)=\max_j c_j(x,\xi)$, and the risk level is $\alpha\in(0,1)$.

• True distribution function. $F(t;x)=\mathbb P_\xi(C(x,\xi)\le t)$. The true feasible region is $X_\alpha=\{x\in X\mid F(0;x)\ge 1-\alpha\}$; the optimal solution set and value of (1.1) are $S$ and $v^*$.
• Smoothed indicator. For $\varepsilon>0$, $\Gamma_\varepsilon(y)$ equals $1$ for $y\le-\varepsilon$, $0$ for $y\ge\varepsilon$, and $\gamma_\varepsilon(y)$ in between, where $\gamma_\varepsilon:[-\varepsilon,\varepsilon]\to[0,1]$ is strictly decreasing, symmetric ($\gamma_\varepsilon(-y)=1-\gamma_\varepsilon(y)$), and makes $\Gamma_\varepsilon$ differentiable. The paper's concrete choice is the quartic kernel (2.6).
• Smoothed distribution functions. $F_\varepsilon(t;x)=\int\Gamma_\varepsilon(C(x,\xi)-t)\,d\mathbb P_\xi$, and, for an i.i.d. sample $\xi_1,\dots,\xi_N$,

$$F^N_\varepsilon(t;x)=\frac1N\sum_{i=1}^N\Gamma_\varepsilon\bigl(C(x,\xi_i)-t\bigr).$$

• Smoothed sample problem (2.4). $\min_{x\in X} f(x)$ subject to $F^N_\varepsilon(0;x)\ge1-\alpha$, with optimal solution set $S^N_\varepsilon$ and value $v^N_\varepsilon$.

The standing assumptions are: Assumption 3.1, for each $x\in X$ the random variable $C(x,\xi)$ has a continuous distribution; Assumption 3.2, $C$ is Carathéodory, i.e. $C(x,\cdot)$ is measurable for each $x\in X$ and $C(\cdot,\xi)$ is continuous for almost every $\xi$; Assumption 3.3, some optimal solution $\bar x$ of (1.1) is a limit of points $x\in X$ with $F(0;x)>1-\alpha$.

Formalization targets

Goal: Theorem 3.5

If $X$ is compact, $f$ is continuous and Assumptions 3.1–3.3 hold, then with probability one, as $N\to\infty$ and $\varepsilon\to0$ jointly,

$$S^N_\varepsilon\neq\emptyset\ \text{eventually},\qquad v^N_\varepsilon\to v^*,\qquad \mathbb D(S^N_\varepsilon,S)=\sup_{x\in S^N_\varepsilon}\operatorname{dist}(x,S)\to0 .$$

Milestones

1. Uniform law of large numbers (proof of Theorem 3.4): w.p.1, $\sup_{\varepsilon\in(0,1]}\sup_{x\in U}|F^N_\varepsilon(0;x)-F_\varepsilon(0;x)|\to0$ as $N\to\infty$, for compact $U\subseteq X$.
2. Removal of the smoothing (proof of Theorem 3.4): $\sup_{x\in U}|F_\varepsilon(0;x)-F(0;x)|\to0$ as $\varepsilon\to0^+$.
3. Theorem 3.4: w.p.1, $\sup_{x\in U}|F^N_\varepsilon(0;x)-F(0;x)|\to0$ as $N\to\infty$ and $\varepsilon\to0$.
4. Eventual nonemptiness of $S^N_\varepsilon$ (proof of Theorem 3.5).
5. (3.3): $\liminf v^N_\varepsilon\ge v^*$ w.p.1.
6. (3.4): $\limsup v^N_\varepsilon\le v^*$ w.p.1.

Significance

Theorem 3.5 justifies solving the smooth problem (2.4) in place of (1.1): with enough samples and a small enough bandwidth, global solutions of the surrogate approximate global solutions of the chance-constrained program, and the optimal values agree in the limit. Unlike earlier results it controls the two approximation errors, sampling and smoothing, at once, so no order of limits has to be chosen in practice. It is the asymptotic counterpart of the paper's finite-sample feasibility bound (Theorem 3.13) and the theoretical basis for the trust-region method of §5.

The result is proved in the paper, with two steps imported from Shapiro–Dentcheva–Ruszczyński, second edition (a uniform law of large numbers, Theorem 7.53, and a convergence-of-expectations result, Theorem 4.91) and the deviation statement deferred to Theorem 5.3 there. None of these results, and no consistency theorem for sample approximations of chance constraints, is machine-checked on Prove2Me or, as far as is known, elsewhere. A formal proof requires writing the imported steps out for the specific integrands of this problem and completing the solution-set argument the paper leaves to the reference.

Difficulty

The pointwise statements are routine; the uniformity is not. The integrand $\Gamma_\varepsilon(C(x,\xi))$ converges, as $\varepsilon\to0$, to the indicator $\mathbf 1\{C(x,\xi)\le0\}$, which is discontinuous in $x$ wherever $C(x,\xi)=0$. A uniform law of large numbers for a family that degenerates into indicators needs the no-atom Assumption 3.1 at every point of $U$, not only at the limit. Moreover, the smoothing functions $\gamma_\varepsilon$ for different $\varepsilon$ are unrelated, so the family is not continuous in $\varepsilon$, and a Glivenko–Cantelli argument over a joint parameter $(x,\varepsilon)$ cannot be applied directly. The convergence of solution sets needs, in addition, that the limit of feasible points of (2.4) is feasible for (1.1), which uses the continuity of $F(0;\cdot)$ on $X$; that continuity again rests on Assumptions 3.1 and 3.2.

Formalization scope

• Decisions are Fin n → ℝ with the sup norm. Assumption 3.3 is stated for every radius, so the norm choice does not change it.
• The sample is an infinite sequence ξ : ℕ → Ω → Ξ of measurable, independent maps on a probability space, each with law $\mathbb P_\xi$; $F^N_\varepsilon$ uses the first $N$ draws.
• "As $N\to\infty$ and $\varepsilon\to0$" is the product filter atTop ×ˢ 𝓝[>] 0 on $\mathbb N\times\mathbb R$, with $\varepsilon>0$ because $\Gamma_\varepsilon$ needs it; one null set serves every conclusion of a statement.
• Assumption 3.1 is "no atoms": $\mathbb P_\xi(C(x,\xi)=y)=0$ for all $x\in X$, $y\in\mathbb R$. Assumption 3.2 is measurability of $C(x,\cdot)$ on $X$ plus almost-sure continuity of $C(\cdot,\xi)$ on $\mathbb R^n$.
• The family $\gamma_\varepsilon$ is any family with each member admissible; no relation across $\varepsilon$ is assumed. The quartic kernel (2.6) is admissible for every $\varepsilon>0$, so the hypothesis is satisfiable.
• The feasible set of (2.4) is $\{x\in X\mid F^N_\varepsilon(0;x)\ge1-\alpha\}$, the form the paper's proof uses. The quantile $Q^{1-\alpha}_\varepsilon$ of (2.4) is defined only when $(1-\alpha)N\notin\mathbb Z$, which fails for infinitely many $N$ when $\alpha$ is rational; where it is defined, the two feasible sets coincide.
• The optimal value is the real infimum, which Lean sets to $0$ on an empty set. The goal therefore asserts eventual nonemptiness of $S^N_\varepsilon$ itself, and (3.3)–(3.4) are stated as bounds on $f$ over the feasible set of (2.4), which imply the liminf and limsup without reading an infimum over a possibly empty set. The deviation $\mathbb D$ is stated pointwise ("every point of $S^N_\varepsilon$ is eventually within $\eta$ of $S$"), with $S$ nonempty by Assumption 3.3, so the distance to the empty set never arises.
• Iterated limits (first $N$, then $\varepsilon$), a null set chosen after $\eta$, or a feasible set defined through $Q_\varepsilon$ with its junk value would each be a different and weaker statement; none is used.

The definitions layer (Γ_ε, admissibility, $F$, $F_\varepsilon$, $F^N_\varepsilon$, $X_\alpha$, the shifted sample sets (3.2)) is shared with the companion mission on finite-sample feasibility. A uniform law of large numbers for almost-surely continuous, bounded integrands on a compact parameter set, and convergence of optimal values under uniform convergence of constraint functions, are reusable beyond this mission; contributions of either as standalone lemmas are welcome.

Selected references

• A. Peña-Ordieres, J. R. Luedtke, A. Wächter, Solving chance-constrained problems via a smooth sample-based nonlinear approximation, SIAM J. Optim. 30(3), 2020; preprint arXiv:1905.07377v2, 2020. https://arxiv.org/abs/1905.07377, https://doi.org/10.1137/19M1261985
• A. Shapiro, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, second edition, 2014 (Theorems 4.91, 5.3, 7.53; reference [40] of the paper). https://doi.org/10.1137/1.9781611973433
• B. K. Pagnoncelli, S. Ahmed, A. Shapiro, Sample average approximation method for chance constrained programming: theory and applications, J. Optim. Theory Appl. 142, 2009, pp. 399–416. https://doi.org/10.1007/s10957-009-9523-6
• J. Luedtke, S. Ahmed, A sample approximation approach for optimization with probabilistic constraints, SIAM J. Optim. 19, 2008, pp. 674–699. https://doi.org/10.1137/070702928
• L. J. Hong, Y. Yang, L. Zhang, Sequential convex approximations to joint chance constrained programs: a Monte Carlo approach, Oper. Res. 59, 2011, pp. 617–630. https://doi.org/10.1287/opre.1100.0910
• A. Nemirovski, A. Shapiro, Convex approximations of chance constrained programs, SIAM J. Optim. 17, 2006, pp. 969–996. https://doi.org/10.1137/050622328