Optimization

Motivation

Stochastic gradient descent (SGD) minimizes an objective that is an expectation, $F(x) = \mathbb E_{i\sim\mathcal D} f_i(x)$, by stepping along the gradient of one randomly drawn component at a time. It is the workhorse of large-scale machine learning, where $F$ is an average loss over training examples, and it also contains the randomized Kaczmarz method for linear systems, where each component is a single squared residual $\frac12(\langle a_i, x\rangle - b_i)^2$ (Strohmer & Vershynin 2009).

For smooth, strongly convex objectives, the question is how fast a fixed step size drives the iterates to the minimizer $x_\star$, and how the rate depends on the smoothness constants $L_i$ of the components. Bach & Moulines (2011) showed that an iteration count scaling with the squared conditioning $\mathbb E L_i^2/\mu^2$ suffices. Needell, Srebro and Ward (arXiv:1310.5715v5, Theorem 2.1) replaced this by a dependence that is linear in the uniform conditioning $\sup L/\mu$. Their theorem is the base of the rest of the paper: Corollary 2.2 (choice of step size), the importance-sampling results of Section 3 (weighting components by $L_i$), and the Kaczmarz rates of Section 5 are all derived from it.

Timeline:

• 1951, Robbins and Monro: stochastic approximation.
• 2009, Strohmer and Vershynin: expected linear convergence of randomized Kaczmarz with rows sampled proportionally to their squared norms.
• 2011, Bach and Moulines: fixed-step SGD on strongly convex smooth objectives, with an iteration count of order $\log(\varepsilon_0/\varepsilon)(\mathbb E L_i^2/\mu^2 + \sigma^2/(\mu^2\varepsilon))$.
• 2013–2015, Needell, Srebro and Ward: the bound below, linear in $\sup L/\mu$, and its importance-sampling and Kaczmarz corollaries.

Setting

Let $\mathcal D$ be a probability distribution, the source distribution, on an arbitrary measurable index space $I$. Let $\mathcal H$ be a real Hilbert space (for example $\mathbb R^d$ with the Euclidean norm $\|\cdot\|_2$), and let $f_i : \mathcal H \to \mathbb R$, $i \in I$, be a family of functions. The objective is

$$F(x) = \mathbb E_{i\sim\mathcal D} f_i(x),$$

and $x_\star$ is a minimizer of $F$. The paper assumes:

1. each $f_i$ is convex and differentiable, and its gradient $\nabla f_i$ is Lipschitz with constant $L_i$: $\|\nabla f_i(x) - \nabla f_i(y)\|_2 \le L_i\|x - y\|_2$;
2. $F$ is $\mu$-strongly convex: $\langle x - y, \nabla F(x) - \nabla F(y)\rangle \ge \mu\|x - y\|_2^2$ for all $x, y$.

The number $\sup L$ is an almost-sure upper bound on $L_i$, and the residual is

$$\sigma^2 = \mathbb E\|\nabla f_i(x_\star)\|_2^2,$$

which vanishes exactly when $x_\star$ is a stationary point of every component (the realizable case).

The SGD iterates with fixed step size $\gamma$ start at $x_0 \in \mathcal H$ and follow (2.2):

$$x_{k+1} = x_k - \gamma\nabla f_{i_k}(x_k),$$

where $i_0, i_1, \dots$ are drawn independently from $\mathcal D$. The iterate $x_k$ is a random point that depends on $i_0, \dots, i_{k-1}$. In Lean these objects are objective D f, residual D f xstar, iidLaw D (the law of the index sequence) and sgdIter f γ x0 k ω in the namespace SGDKaczmarz.SGD.

Formalization targets

Goal: Theorem 2.1, (2.4)

If $0 < \gamma < 1/\sup L$, then for every $k \ge 0$

$$\mathbb E\|x_k - x_\star\|_2^2 \le \Bigl[1 - 2\gamma\mu(1 - \gamma\sup L)\Bigr]^k\|x_0 - x_\star\|_2^2 + \frac{\gamma\sigma^2}{\mu(1 - \gamma\sup L)},$$

where the expectation is over the sampling of $\{i_k\}$. The constants are the paper's; nothing is left unfixed.

Milestones

In the order of the paper's proof (Appendix A):

• (A.1): at a minimizer $x_\star$ of a function with $L$-Lipschitz gradient, $\frac{1}{2L}\|\nabla f(x) - \nabla f(x_\star)\|_2^2 \le f(x) - f(x_\star)$;
• Lemma A.1 (co-coercivity): $\|\nabla f(x) - \nabla f(y)\|_2^2 \le L\langle x - y, \nabla f(x) - \nabla f(y)\rangle$;
• the pathwise one-step bound on $\|x_k - x_\star - \gamma\nabla f_i(x_k)\|_2^2$;
• unbiasedness: $\mathbb E\nabla f_i(x) = \nabla F(x)$;
• the expected one-step recursion $\mathbb E\|x_{k+1} - x_\star\|_2^2 \le (1 - 2\gamma\mu(1 - \gamma\sup L))\|x_k - x_\star\|_2^2 + 2\gamma^2\sigma^2$ for $\gamma \le 1/\sup L$;
• the unrolled recursion, with the finite geometric sum $2\sum_{j<k}(1 - 2\gamma\mu(1 - \gamma\sup L))^j\gamma^2\sigma^2$.

Significance

The bound has two terms: a contraction at rate $1 - 2\gamma\mu(1 - \gamma\sup L)$ and a floor proportional to $\gamma\sigma^2$. Choosing $\gamma$ to balance them (Corollary 2.2) gives an iteration count of order $\log(\varepsilon_0/\varepsilon)(\sup L/\mu + \sigma^2/(\mu^2\varepsilon))$, linear rather than quadratic in the conditioning. In the realizable case $\sigma^2 = 0$ it is a pure linear rate. Reweighting the distribution by $L_i$ turns $\sup L$ into the average $\bar L = \mathbb E L_i$ (Section 3), and specializing to least squares yields convergence rates for randomized Kaczmarz with uniform, weighted and hybrid row selection (Section 5). These consequences are stated in terms of Theorem 2.1, so a formal version of the theorem is the prerequisite for formalizing any of them.

The result is proved on paper (Appendix A.2). The work here is to formalize that proof: co-coercivity in a Hilbert space, differentiation of $F = \mathbb E f_i$ under the expectation, and the passage from a conditional one-step bound to the unconditional bound over an i.i.d. sequence. To our knowledge no machine-checked proof of Theorem 2.1 exists. The platform has formal results on projected SGD with decaying steps and on the finite-sum Kaczmarz iteration, which state different results.

Difficulty

The one-step algebra is routine once co-coercivity is available. What is hard is making the expectation rigorous. On the page, "$\mathbb E\|x_{k+1} - x_\star\|^2$" in the recursion is an expectation over the index $i_k$ alone, with $x_k$ held fixed. Iterating it requires that $x_k$ be a measurable function of $i_0, \dots, i_{k-1}$, that $i_k$ be independent of it, and that expectations of possibly non-integrable nonnegative quantities be handled without junk values. The unbiasedness step $\mathbb E\nabla f_i = \nabla F$ is a differentiation under the integral sign in a possibly infinite-dimensional space, and it needs a dominating bound that comes from the almost-sure bound on $L_i$ together with the finiteness of $\sigma^2$. A tempting shortcut, assuming $\nabla f_i(x_\star) = 0$ for every $i$, gives only the realizable special case $\sigma^2 = 0$ and is not the theorem.

Formalization scope

• Space. $\mathcal H$ is a complete real inner-product space with its Borel σ-algebra and a second-countable topology (every separable Hilbert space, including $\mathbb R^d$). Separability makes the iterates random variables.
• Gradients. These are Mathlib's gradient. Assumption (1) is LipschitzWith (L i) (gradient (f i)) with L i : ℝ≥0, together with Differentiable ℝ (f i) and ConvexOn ℝ Set.univ (f i) for every $i$.
• The objective. $F$ is the Bochner integral $x \mapsto \int f_i(x)\,d\mathcal D$, under the hypothesis that $i \mapsto f_i(x)$ is integrable for every $x$. The gradient maps $i \mapsto \nabla f_i(x)$ are assumed measurable.
• Strong convexity. Assumption (2) is stated in the paper's gradient-monotone form for gradient (objective D f). Differentiability of $F$ is not assumed separately: it follows whenever $\sigma^2 < \infty$ (milestone "unbiasedness").
• The constant $\sup L$. It is any real number with $L_i \le \sup L$ almost surely. This is equivalent to the paper's essential supremum, because the bound is increasing in $\sup L$.
• Step-size conditions. $\gamma < 1/\sup L$ is written γ * supL < 1 (and $\gamma \le 1/\sup L$ as γ * supL ≤ 1), with $0 < \gamma$ and $0 < \mu$.
• Expectations. $\mathbb E\|x_k - x_\star\|^2$ and $\sigma^2$ are lower Lebesgue integrals in $[0,\infty]$: the first over the infinite product law Measure.infinitePi of the index sequence, the second over $\mathcal D$. A non-integrable iterate therefore cannot satisfy the bound vacuously, and $\sigma^2 = \infty$ makes the right side $\infty$, which is the paper's meaning.
• Indexing. $x_0$ is the initial point and $x_k$ is the point after $k$ steps.
• Hypotheses. The co-coercivity lemma carries convexity of $f$, which its proof uses and without which it is false. No hypothesis such as $\nabla f_i(x_\star) = 0$, $\sigma^2 < \infty$ or $\mu \le \sup L$ is added to the goal.

Infrastructure that a complete development needs, and that is reusable beyond this mission:

• co-coercivity of gradients of smooth convex functions on Hilbert spaces;
• differentiation under the expectation for families with uniformly Lipschitz gradients;
• the tower property for a measurable recursion driven by Measure.infinitePi.

Contributions of any of these as separate lemmas are welcome.

Selected references

• D. Needell, N. Srebro, R. Ward, Stochastic gradient descent, weighted sampling, and the randomized Kaczmarz algorithm, arXiv:1310.5715v5, 2015 (Mathematical Programming 155, 2016). https://arxiv.org/abs/1310.5715v5
• F. Bach, E. Moulines, Non-asymptotic analysis of stochastic approximation algorithms for machine learning, NIPS 2011. https://hal.science/hal-00608041
• T. Strohmer, R. Vershynin, A randomized Kaczmarz algorithm with exponential convergence, J. Fourier Anal. Appl. 15(2):262–278, 2009. https://doi.org/10.1007/s00041-008-9030-4
• H. Robbins, S. Monro, A stochastic approximation method, Ann. Math. Statist. 22:400–407, 1951. https://doi.org/10.1214/aoms/1177729586
• Y. Nesterov, Introductory Lectures on Convex Optimization, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Polynomial optimization asks for the minimum $f^*$ of a polynomial $f$ over a set $K\subseteq\mathbb R^n$ cut out by polynomial inequalities. Lasserre's moment relaxation (Lasserre 2001) replaces the minimization over points by a minimization over probability measures on $K$, and then over linear functionals on polynomials that satisfy semidefinite constraints. The bridge between measures and semidefinite constraints is Putinar's theorem (Putinar 1993): on a compact basic semialgebraic set with an Archimedean description, a linear functional comes from a measure exactly when it is nonnegative on the quadratic module of the constraints.

Many problems of practical size are invariant under a group of linear transformations: permutations of variables, sign changes, rotations of a polygon. Gatermann and Parrilo (2004) showed how such symmetry block-diagonalizes sums-of-squares programs. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486, Math. Oper. Res. 2013) carry the reduction to the moment side. Their first step, Theorem 3.2, is a symmetric version of Putinar's theorem: for invariant data it suffices to consider functionals that are themselves invariant, and these are characterized by positivity of symmetrized localizing forms. This mission formalizes that theorem.

Setting

Write $\mathbb R[X]=\mathbb R[X_1,\dots,X_n]$. Let $G$ be a finite subgroup of $\mathrm{GL}_n(\mathbb R)$. A matrix $\sigma\in G$ acts on points by $x\mapsto\sigma x$ and on polynomials by

$$p^\sigma(x):=p(\sigma^{-1}x),$$

the linear substitution $X_i\mapsto\sum_j(\sigma^{-1})_{ij}X_j$. A polynomial is $G$-invariant if $p^\sigma=p$ for every $\sigma\in G$.

Fix $g_1,\dots,g_m\in\mathbb R[X]$ and the feasible set

$$K=\{x\in\mathbb R^n:\ g_j(x)\ge0,\ j=1,\dots,m\}.$$

Assumption 2.1 requires $K$ to be compact and some polynomial $u=u_0+\sum_j u_jg_j$, with sums of squares $u_0,\dots,u_m$, to have a compact superlevel set $\{u\ge0\}$. Put $g_0:=1$.

A linear map $L^G:\mathbb R[X]\to\mathbb R$ is $G$-linear if $L^G(f)=L^G(f^\sigma)$ for all $f$ and all $\sigma\in G$. Its symmetrized localizing forms are

$$\mathcal L^G_{g_j}(p,q)=L^G\Big(\frac1{|G|}\sum_{\sigma\in G}(p\cdot q)^\sigma\cdot g_j\Big),\qquad 0\le j\le m.$$

For a Borel measure $\mu$ on $\mathbb R^n$, $\mu^\sigma(B)=\mu(\sigma^{-1}(B))$ is its image under $x\mapsto\sigma x$, and $\mu$ is $G$-invariant if $\mu^\sigma=\mu$ for all $\sigma\in G$. A measure on $K$ is one with $\mu(\mathbb R^n\setminus K)=0$.

Formalization targets

Goal: Theorem 3.2

If the $g_j$ are $G$-invariant and Assumption 2.1 holds, then for a $G$-linear $L^G$: $\exists\,\mu\ \text{finite, $G$-invariant, on }K:\ \ L^G(p)=\int p\,d\mu\ \ \forall p \quad\Longleftrightarrow\quad \mathcal L^G_{g_j}(p,p)\ge0\ \ \forall p\in\mathbb R[X],\ \forall\, 0\le j\le m.$

Milestones

1. Theorem 2.2 (Putinar). Under Assumption 2.1, a linear $L$ is integration against a probability measure on $K$ iff $L(1)=1$ and $L(s_0+\sum_js_jg_j)\ge0$ for all sums of squares $s_0,\dots,s_m$.
2. Averaging identity (p. 10). For $G$-linear $L^G$: $L^G(p)=\frac1{|G|}\sum_\sigma L^G(p^\sigma)=L^G\big(\frac1{|G|}\sum_\sigma p^\sigma\big)$.
3. Only-if computation (p. 11). For a finite $G$-invariant $\mu$ on compact $K$ and invariant $g_j$: $\int\frac1{|G|}\sum_\sigma(f^2)^\sigma g_j\,d\mu=\int f^2g_j\,d\mu\ge0$.
4. If computation (p. 11). For $G$-linear $L^G$ and invariant $g$: $\mathcal L^G_g(h,h)=L^G(h^2g)$.
5. Invariance from moments (p. 11). A finite measure on compact $K$ with $\int h\,d\mu=\int h^\sigma d\mu$ for every polynomial $h$ and every $\sigma\in G$ is $G$-invariant.

Significance

The result. Theorem 3.2 turns the moment relaxation of a $G$-invariant problem into one over $G$-linear functionals. Such a functional is determined by its values on the invariant ring $\mathbb R[X]^G$, so its moment variables are indexed by a basis of invariants instead of all monomials (Example 3.3 of the paper: five variables instead of fifteen for $C_4$ on $\mathbb R^4$ in degree 2). The block-diagonalized relaxations and the convergence result of §3 (Theorems 3.4–3.7) rest on it.

Formalizing it. The theorem is proved in the paper, modulo Putinar's theorem, which is cited. Neither Putinar's theorem nor any Archimedean Positivstellensatz is in Mathlib or on the platform. A complete formalization therefore needs (i) Putinar's theorem itself, in its dual moment form, and (ii) the determinacy of compactly supported finite measures by polynomial moments in several variables. Both are reusable well beyond this paper: every moment-SOS hierarchy result in the literature cites them.

Difficulty

The group-theoretic steps (milestones 2–4) are finite averaging and change of variables. The weight of the theorem sits in two analytic facts. The first is Putinar's theorem: nonnegativity on the quadratic module is an algebraic condition, and producing a measure from it requires the Archimedean hypothesis of Assumption 2.1 in an essential way; without that hypothesis the statement is false in general. The second is that the measure Putinar's theorem returns has to be shown $G$-invariant. Equality of the polynomial moments of $\mu$ and $\mu^\sigma$ does not by itself identify two measures; it does so here because both are finite and carried by a compact set, where polynomials are dense in the continuous functions. A further detail: Putinar's theorem is stated for normalized functionals, and Theorem 3.2 is not normalized, so the degenerate case $L^G(1)=0$ must be shown to force $L^G=0$.

Formalization scope

Polynomials are MvPolynomial (Fin n) ℝ, points Fin n → ℝ, and $G$ a Subgroup (GL (Fin n) ℝ) with a Fintype instance. The action on polynomials is the linear substitution aeval, so $G$ is an arbitrary finite matrix group, not only a permutation group. Sums of squares are Mathlib's IsSumSq. "psd" for the symmetric form $\mathcal L^G_{g_j}$ means $\mathcal L^G_{g_j}(p,p)\ge0$ for every polynomial $p$, with no degree truncation; $j=0$ ($g_0=1$) is included. Measures live on the Borel σ-algebra of $\mathbb R^n$, $\mu^\sigma$ is Measure.map along the continuous (hence measurable) map $x\mapsto\sigma x$, and "measure on $K$" is $\mu(\mathbb R^n\setminus K)=0$.

Committed conventions and disclosed readings:

• Finite measure. The paper writes "a $G$-invariant measure on $K$". It is formalized as a finite Borel measure; this is the reading that makes $\int p\,d\mu$ meaningful for every polynomial, and finite measures on a compact set make every polynomial integrable.
• No normalization. As on the page, Theorem 3.2 has neither $L^G(1)=1$ nor a probability measure; Theorem 2.2 has both.
• Direction of $\mu^\sigma$. With $\mu^\sigma$ the image of $\mu$ under $\sigma$, one has $\int h^\sigma d\mu=\int h\,d\mu^{\sigma^{-1}}$, where the paper writes $\int h\,d\mu^\sigma$. Statements quantify over all $\sigma\in G$, so the difference does not change their content.

Trivializing formalizations are ruled out: integrals are taken only against finite measures carried by a compact set, so no statement holds because a Bochner integral of a non-integrable function is $0$; positivity is through the forms on all of $\mathbb R[X]$, not replaced by pointwise nonnegativity; and the invariance of $\mu$ is a conclusion of milestone 5, never a hypothesis.

Contributions welcome: Putinar's theorem (milestone 1) and multivariate moment determinacy on compact sets are the reusable infrastructure; the averaging milestones are a natural first entry point.

Selected references

• C. Riener, T. Theobald, L. Jansson Andrén, J. B. Lasserre, Exploiting symmetries in SDP-relaxations for polynomial optimization, Math. Oper. Res. 38(1):122–141, 2013. arXiv:1103.0486v3, doi:10.1287/moor.1120.0558
• M. Putinar, Positive polynomials on compact semi-algebraic sets, Indiana Univ. Math. J. 42(3):969–984, 1993. doi:10.1512/iumj.1993.42.42045
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM J. Optim. 11(3):796–817, 2001. doi:10.1137/S1052623400366802
• K. Gatermann, P. A. Parrilo, Symmetry groups, semidefinite programs, and sums of squares, J. Pure Appl. Algebra 192:95–128, 2004. doi:10.1016/j.jpaa.2003.12.011

Why saddle points matter for nonconvex learning

Training a model in machine learning usually means minimizing a nonconvex function $f:\mathbb R^d\to\mathbb R$ with first-order methods. Finding a global minimum of a general nonconvex function is NP-hard, so the classical guarantee for gradient descent (GD), $x_{t+1}=x_t-\eta\nabla f(x_t)$, is weaker: with step size $\eta=1/\ell$ it reaches a point with $\|\nabla f(x)\|\le\varepsilon$ within $\ell(f(x_0)-f^\star)/\varepsilon^2$ iterations, independently of the dimension (Nesterov, 1998). Such a point can be a saddle point. For many learning problems (matrix sensing and completion, phase retrieval, dictionary learning, tensor decomposition), every approximate second-order stationary point is an approximate global minimum, so an algorithm that avoids saddle points solves the problem.

Jin, Netrapalli, Ge, Kakade and Jordan (arXiv:1902.04811, J. ACM 2021) show that simple perturbed versions of GD and SGD find approximate second-order stationary points in essentially the number of iterations GD needs for first-order stationarity, up to polylogarithmic factors in the dimension. Their §5 gives a short, self-contained proof for a variant of perturbed GD (Algorithm 4). That proof is the subject of this mission.

Timeline:

• 2015: Ge, Huang, Jin and Yuan show that noisy SGD escapes strict saddle points in polynomial time.
• 2017: Jin, Ge, Netrapalli, Kakade and Jordan (ICML) prove that perturbed GD finds an $\varepsilon$-second-order stationary point in $\tilde O(\ell\Delta_f/\varepsilon^2)$ iterations, with a geometric argument on the "stuck region".
• 2019: arXiv:1902.04811 extends this to SGD and simplifies the deterministic proof through the improve or localize lemma (Lemma 21). §5 of that paper is formalized here.

Setting

Let $f:\mathbb R^d\to\mathbb R$, $d\ge1$, with gradient $\nabla f$ and Hessian $\nabla^2 f$; $\|\cdot\|$ is the Euclidean norm on vectors and the spectral norm on matrices. Assumption A: $f$ is $\ell$-gradient Lipschitz, $\|\nabla f(x_1)-\nabla f(x_2)\|\le\ell\|x_1-x_2\|$, and $\rho$-Hessian Lipschitz, $\|\nabla^2f(x_1)-\nabla^2f(x_2)\|\le\rho\|x_1-x_2\|$. A point $x$ is an $\varepsilon$-second-order stationary point ($\varepsilon$-SOSP) if

$$\|\nabla f(x)\|\le\varepsilon\qquad\text{and}\qquad\nabla^2 f(x)\succeq-\sqrt{\rho\varepsilon}\,I .$$

Write $f^\star=\inf f$ and $\Delta_f=f(x_0)-f^\star$.

Algorithm 4 (Perturbed GD, Variant). With step size $\eta$, radius $r$, time interval $\mathscr T$ and tolerance $\varepsilon$, start with $t_{\text{perturb}}=0$. At iteration $t$: if $\|\nabla f(x_t)\|\le\varepsilon$ and $t-t_{\text{perturb}}>\mathscr T$, replace $x_t$ by $x_t-\eta\xi_t$ with $\xi_t\sim\mathrm{Uniform}(B_0(r))$ and set $t_{\text{perturb}}=t$; then $x_{t+1}=x_t-\eta\nabla f(x_t)$. The parameters are those of Eq. (6):

$$\eta=\frac1\ell,\quad r=\frac{\varepsilon}{400\iota^3},\quad\mathscr T=\frac{\ell}{\sqrt{\rho\varepsilon}}\,\iota,\quad\mathscr F=\frac{1}{50\iota^3}\sqrt{\frac{\varepsilon^3}{\rho}},\quad\mathscr S=\frac{1}{4\iota}\sqrt{\frac{\varepsilon}{\rho}},$$

where $\iota$ is a logarithmic factor, and $\omega=2^{2-\iota}\ell\mathscr S$.

Formalization targets

Goal: Theorem 18

For $T=\lceil 8\max\{\Delta_f\mathscr T/\mathscr F,\ \Delta_f/(\eta\varepsilon^2)\}\rceil$ (which equals $\lceil400\iota^4\ell\Delta_f/\varepsilon^2\rceil$) and every $\iota\ge1$ with

$$\frac{T\ell\sqrt d}{\sqrt{\rho\varepsilon}}\,\iota^2 2^{8-\iota}\le\delta,$$

with probability at least $1-\delta$ over the perturbations,

$$\#\{t<T:\ x_t\text{ is an }\varepsilon\text{-SOSP}\}\ \ge\ T/2 .$$

The paper writes the count as $\tilde O(\ell\Delta_f/\varepsilon^2)$ with $\iota=c\log(d\ell\Delta_f/(\rho\varepsilon\delta))$.

Milestones, in the order the proof uses them

1. Lemma 19 (descent): $f(x_{t+1})-f(x_t)\le-\eta\|\nabla f(x_t)\|^2/2$ for $\eta\le1/\ell$.
2. Lemma 21 (improve or localize): $\|x_\tau-x_0\|\le\sqrt{2\eta t(f(x_0)-f(x_t))}$ for $t\ge\tau>0$.
3. Lemma 22 (coupling sequence): if $\lambda_{\min}(\nabla^2f(\tilde x))\le-\sqrt{\rho\varepsilon}$ and two GD runs start within $\eta r$ of $\tilde x$, $\eta r_0$ apart along the bottom eigenvector with $r_0>\omega$, one of them decreases $f$ by $\mathscr F$ within $\mathscr T$ steps.
4. Volume display (§5, proof of Lemma 20, p. 15): $w\,\mathrm{Vol}(\mathbb B^{d-1}_0(a))/\mathrm{Vol}(\mathbb B^d_0(a))=\frac{w}{a\sqrt\pi}\frac{\Gamma(d/2+1)}{\Gamma(d/2+1/2)}\le\frac wa\sqrt{d/\pi}$.
5. Lemma 20 (escaping saddle points): at $\tilde x$ with $\|\nabla f(\tilde x)\|\le\varepsilon$ and $\lambda_{\min}\le-\sqrt{\rho\varepsilon}$,

$$\mathbb P\bigl(f(x_{\mathscr T})-f(\tilde x)\le-\mathscr F/2\bigr)\ge1-\frac{\ell\sqrt d}{\sqrt{\rho\varepsilon}}\,\iota^22^{8-\iota}\quad\text{for }x_0=\tilde x+\eta\xi .$$

Significance

The result. Theorem 18 says that adding occasional small random perturbations to gradient descent costs only a polylogarithmic factor over the first-order rate $\ell\Delta_f/\varepsilon^2$ and buys second-order stationarity. Combined with the landscape results above, it gives polynomial-time guarantees for gradient methods on those learning problems. Lemma 20, on its own, is a quantitative statement that strict saddle points are unstable under perturbed GD; Lemmas 21 and 22 are reusable tools for any analysis of first-order methods near saddle points.

Formalizing it. The results are proved in the paper; none of them is formalized. A formal development would give machine-checked versions of the descent lemma for Hessian-Lipschitz functions, the improve-or-localize lemma, the coupling argument and the probabilistic escape bound. It would also settle the issue disclosed under Formalization scope.

Difficulty

Lemmas 19 and 21 are short. The difficulty is in Lemma 22 and Lemma 20. The obvious approach, linearizing GD around the saddle and following the unstable eigendirection, fails because the stuck region (starting points that do not escape within $\mathscr T$ steps) has no simple shape once $f$ is not quadratic. The coupling argument controls the difference of two runs instead. It needs an induction in which the non-quadratic error term stays below half of the leading term for all $\mathscr T$ steps, with the constants of Eq. (6) used exactly ($2\eta\rho\mathscr S\mathscr T=1/2$). Lemma 20 then turns a statement about pairs of points into a measure bound: a set whose every line parallel to $e_1$ meets it in a segment of length at most $\eta\omega$ has volume at most $\eta\omega$ times the $(d-1)$-volume of the ball. In Lean this needs Fubini over a rotated coordinate system and measurability of the stuck region. Theorem 18 requires a probabilistic accounting over the whole run, under the product law of the perturbations.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with $d\ge1$. The Hessian is fderiv ℝ (gradient f) x, the derivative of the gradient map, with the operator norm. Statements about $\lambda_{\min}$ use the quadratic form: $\lambda_{\min}(H)\le-c$ is "some unit $v$ has $\langle Hv,v\rangle\le-c$", and $H\succeq-cI$ is "$\langle Hv,v\rangle\ge-c\|v\|^2$ for all $v$". $\mathrm{Uniform}(B_0(r))$ is normalized Lebesgue measure on the open ball. Algorithm 4 is a deterministic function of the perturbation vectors, which have the product law on $(\mathbb R^d)^T$. The $t$-th iterate is the point tested at the start of iteration $t$, and "half of its iterations" counts $t\in\{0,\dots,T-1\}$. Probability statements bound the failure event from above.

The paper's $\tilde O(\cdot)$ is instantiated as the proof does:

• the parameters are exactly Eq. (6), and $T=\lceil8\max\{\Delta_f\mathscr T/\mathscr F,\Delta_f/(\eta\varepsilon^2)\}\rceil$ (p. 16);
• $\iota$ is any real $\ge1$ satisfying the proof's condition $(T\ell\sqrt d/\sqrt{\rho\varepsilon})\iota^22^{8-\iota}\le\delta$, in place of $\iota=c\log(d\ell\Delta_f/(\rho\varepsilon\delta))$. The printed argument of the logarithm changes under rescaling $x\mapsto\lambda x$ while every quantity in the proof does not, so the printed choice can give $\iota\le0$;
• $\mathscr T$ is a natural number equal to $\ell\iota/\sqrt{\rho\varepsilon}$, with no rounding, because the proof uses $x_{\mathscr T}$ and $2\eta\rho\mathscr S\mathscr T=1/2$ exactly;
• $\ell\ge\sqrt{\rho\varepsilon}$ (footnote 1, p. 14), $\iota\ge1$, $\eta>0$ and $f$ bounded below are the standing assumptions of §5.

A Hessian not tied to $f$, an arbitrary unit vector in place of the bottom eigenvector in Lemma 22, a per-realization or existential statement in place of the product-law probability, or a vacuous $\iota$ would each trivialize the statements; none is used.

Disclosed gap. The proof of Theorem 18 (p. 16) bounds the number of perturbations by applying Lemma 20 at each one. Algorithm 4 also perturbs at points that are already $\varepsilon$-SOSPs, where Lemma 20 does not apply, and the $\mathscr T$ iterations after such a perturbation are not counted. The goal is posed as printed; a solver who finds it false should report this in the discussion. The milestones do not depend on the gap.

Needed infrastructure: second-order Taylor bounds for Hessian-Lipschitz functions, symmetry of the Hessian and existence of a bottom eigenvector, volumes of Euclidean balls (in Mathlib through $\Gamma$), a Fubini-type slicing bound for sets of bounded width along a direction, and measurability of the GD iterates. The volume-ratio and slicing lemmas are reusable beyond this mission. Proofs of any milestone, and alternative proofs, are welcome.

Selected references

• C. Jin, P. Netrapalli, R. Ge, S. M. Kakade, M. I. Jordan, On Nonconvex Optimization for Machine Learning: Gradients, Stochasticity, and Saddle Points, arXiv:1902.04811v2 (2019); J. ACM 68(2), 2021. https://arxiv.org/abs/1902.04811
• C. Jin, R. Ge, P. Netrapalli, S. M. Kakade, M. I. Jordan, How to Escape Saddle Points Efficiently, ICML 2017. https://arxiv.org/abs/1703.00887
• R. Ge, F. Huang, C. Jin, Y. Yuan, Escaping From Saddle Points — Online Stochastic Gradient for Tensor Decomposition, COLT 2015. https://arxiv.org/abs/1503.02101
• Y. Nesterov, Introductory Lectures on Convex Programming, Volume I: Basic Course, 1998; Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• Y. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Math. Program. 108 (2006). https://doi.org/10.1007/s10107-006-0706-8

Motivation

Many optimization problems minimize the average of component losses: one loss per observation, machine, or term in an objective. When an algorithm can inspect one component at a time, the number of component queries is a useful measure of work. A component oracle can provide more than a value or subgradient: a proximal point summarizes a global minimization involving that component. Woodworth and Srebro ask whether this stronger access reduces the worst-case number of queries for nonsmooth finite sums. Their deterministic lower bound answers the question in the regime of convex Lipschitz components on a bounded Euclidean ball (Woodworth and Srebro, 2016, Theorem 1).

The paper studies deterministic and randomized algorithms separately. This mission concerns the deterministic claim in Section 4.1 and its Appendix B.1 proof. The result is relevant to algorithms that alternate among components and use both local subgradient information and component prox computations. The exact oracle matters: a lower bound for an approximate or restricted oracle would not settle the claim made for the stronger one in this paper (Woodworth and Srebro, 2016, pp. 1, 4–5).

Setting

Let $m\ge2$ and let $f_1,\ldots,f_m:\mathbb R^d\to\mathbb R$ be convex functions. Their finite-sum objective is $F(x)=m^{-1}\sum_{i=1}^m f_i(x)$, minimized over the closed Euclidean ball $\mathcal X=\{x:\|x\|\le B\}$ for $B>0$. Each component is $L$-Lipschitz on $\mathcal X$ when $|f_i(x)-f_i(y)|\le L\|x-y\|$ for points $x,y$ in that ball. The paper's notation paragraph prints $f(x)-f(x)$ in this definition; the two-point condition is the intended reading (p. 3).

A query chooses a component index $i$, a point $x\in\mathbb R^d$, and $\beta>0$. The component oracle returns the value $f_i(x)$, a subgradient of $f_i$ at $x$, and a point minimizing $f_i(u)+(\beta/2)\|x-u\|^2$ over $u\in\mathcal X$. The subgradient is global: its defining inequality holds against every point in $\mathbb R^d$. A deterministic algorithm chooses its next query from the ordered responses to its previous queries. The oracle is exact and makes a fixed response choice for each query. The paper allows algorithms without a span restriction and defines a round by how many distinct components have been queried, not by how many total queries have occurred (pp. 1, 4–5).

For the appendix milestones, $v_0,\ldots,v_k$ are orthonormal directions and $\delta_{i,r}\in\{0,1\}$ records whether component $i$ was missed in round $r$. The hard components $f_i$ and their truncations $f_i^t$ are the explicit absolute-value sums in equations (6) and (7). These objects support the lower-bound analysis; they do not restrict the theorem's quantified algorithm or hard instance (pp. 5, 11–12).

Formalization targets

Deterministic oracle lower bound

There are absolute constants $c,C>0$ such that, for every $m\ge2$, $L,B>0$, and $0<\varepsilon<LB/12$, some dimension $d\le C mLB/\varepsilon$ defeats every deterministic algorithm: for that algorithm there are convex $L$-Lipschitz components and a valid oracle whose first $c mLB/\varepsilon$ query points all obey

$$F(x_n)-F(x^*)\ge\varepsilon,$$

where $x^*$ minimizes $F$ on $\mathcal X$. This is the paper's $\Omega(mLB/\varepsilon)$ conclusion. The constants are absolute, and the dimension bound expresses its $O(mLB/\varepsilon)$ clause (Theorem 1, p. 5).

Supporting targets

Appendix B.1 supplies five milestones: the formula and attained minimum of the average hard function, its error gap for a point orthogonal to an unrevealed direction, the query-count inequality, and Lemmas 2 and 3 on subgradient and proximal-response consistency. The first three are quantitative claims for the normalized $L=B=1$ construction; the last two say that answers derived from a truncated component can remain valid for the final component (pp. 11–13).

Significance

The theorem puts a worst-case limit on deterministic methods that can ask for a component prox point as well as a subgradient. Its factor of $m$ says that access to individual components does not remove the cost of discovering information spread across the finite sum. The paper compares this lower bound with its deterministic upper bounds, making the query rate tight up to constants in this regime (Woodworth and Srebro, 2016, Table 1 and Theorem 1).

The mathematical result is proved in the paper; this mission asks for a machine-checked proof of its faithful formal statement. The model of exact component queries, deterministic response histories, and constrained proximal minimizers can also support related oracle-complexity developments. None of the new theorem items in this proposal has a machine-checked proof yet. The already published global subgradient definition is reused as a reference.

Difficulty

The theorem concerns every deterministic algorithm, including one whose future queries depend on all responses so far. A single hard function fixed without regard to that interaction does not capture the adversarial information limit established by the paper. The proof must also show that each answer exposed during the interaction is genuinely a value, subgradient, and constrained prox point for one completed family of component functions. Lemma 2 handles the subgradient requirement, while Lemma 3 handles the more global proximal requirement. The latter is delicate because equation (3) minimizes over the ball, whereas the appendix displays an unconstrained calculation (pp. 11–13).

The printed formula in equation (6) can have Lipschitz constant greater than one, contrary to a sentence on page 11. This affects an explicit constant in the proof, though the theorem's $\Omega$ rate survives rescaling. A verified development must establish a valid uniform Lipschitz bound and carry its normalization into the final constants (Appendix B.1, p. 11).

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d) with its Euclidean inner product and norm. Components use Fin m, a zero-based encoding of the paper's $1,\ldots,m$. Query number zero is the first query; a bound on $(n+1)$ represents the number of queries made through query $n$. The proximal operation is a predicate describing all minimizers over $\mathcal X$; each legal query has $\beta>0$. The oracle is memoryless and exact for every query, even when its point lies outside $\mathcal X$. Candidate points in the goal are the algorithm's query points. The dimension is chosen before the algorithm, as the appendix construction permits. The finite average is an explicit sum and $x^*$ is an explicit feasible minimizer, avoiding a default-valued real infimum.

The milestones use $k\ge1$, orthonormal directions, binary indicators, and $\sum_i\delta_{i,r}=\lfloor m/2\rfloor$ where the average is involved. Their normalization is $L=B=1$. Natural-number division represents $\lfloor m/2\rfloor$, and a finite interval starting at one prevents the term $v_{r-1}$ from underflowing. The goal quantifies over every deterministic algorithm and demands a valid oracle and an attained minimum; the hard directions, indicators, rounds, and truncations occur only in supporting statements. This rules out a fixed easy instance or an oracle allowed to return arbitrary answers.

The development needs Mathlib's Euclidean-space, convexity, finite-sum, and orthonormal-family libraries and the published global-subgradient definition. Contributions that establish the five milestones, a uniform Lipschitz bound for the hard functions, or the algorithm-dependent construction are within scope. The other deterministic smooth regimes and the randomized results have separate problems and are outside this mission.

Selected references

• B. Woodworth and N. Srebro, Tight Complexity Bounds for Optimizing Composite Objectives, NeurIPS, 2016; arXiv:1605.08003v3, 2019 revision. arXiv

Motivation

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

Such duality theorems have been proved under progressively weaker hypotheses:

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

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

Setting

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1, (D)

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

The Lean development lives in the namespace ShortWDRODual.Legendre.

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

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

Selected references

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

Motivation

A constraint $\mathbb E[v(x,\tilde z)] \le w$ on a decision $x$ requires the distribution of the random vector $\tilde z$. In practice that distribution is known only partially: its support, a few moments, or the probability mass of some regions estimated from data. Distributionally robust optimization asks that the constraint hold for every distribution consistent with this information. Wiesemann, Kuhn and Sim (Optimization Online 3757, 2013; Oper. Res. 62(6), 2014) proposed one standardized format for this information. Their format contains, as special cases, many ambiguity sets used earlier: support and moment information (Delage and Ye, 2010), and mean–covariance and directional-deviation information (Goh and Sim, 2010). They then characterized exactly when a worst-case expectation constraint over such a set has a finite conic reformulation. This mission formalizes that characterization: the paper's Theorem 1 and the steps of its proof.

Setting

The uncertain parameters are $\tilde z \in \mathbb R^P$, and an auxiliary random vector $\tilde u \in \mathbb R^Q$ may be added to describe structure of $\tilde z$. A proper cone $\mathcal K$ is a closed convex cone with $\mathcal K \cap(-\mathcal K) = \{0\}$ and nonempty interior. Write $x \preccurlyeq_{\mathcal K} y$ for $y - x \in \mathcal K$, and $\mathcal K^\star = \{y : x^\top y \ge 0\ \forall x \in \mathcal K\}$ for the dual cone. For indices $i \in \mathcal I = \{1,\dots,I\}$ the confidence sets are

$$\mathcal C_i = \{(z,u) : C_i z + D_i u \preccurlyeq_{\mathcal K_i} c_i\},$$

with matrices $C_i, D_i$, vectors $c_i$ and proper cones $\mathcal K_i$. The ambiguity set is

$$\mathcal P = \Big\{\mathbb P : \mathbb E_{\mathbb P}[A\tilde z + B\tilde u] = b,\ \ \mathbb P[(\tilde z,\tilde u) \in \mathcal C_i] \in [\underline p_i,\overline p_i]\ \ \forall i \in \mathcal I\Big\},$$

where $0 \le \underline p_i \le \overline p_i \le 1$. The paper imposes three conditions:

• (C1) $\mathcal C_I$ is bounded and $\underline p_I = \overline p_I = 1$;
• (C2) some $\mathbb P \in \mathcal P$ meets every non-degenerate probability bound strictly;
• (C3) the constraint function is a maximum of finitely many bi-affine pieces,

$$v(x,z) = \max_{l = 1,\dots,L} \big[(S_l z + s_l)^\top x + \mathbf t_l^\top z + t_l\big].$$

The distributionally robust constraint (3) is $\mathbb E_{\mathbb P}[v(x,\tilde z)] \le w$ for all $\mathbb P \in \mathcal P$.

A set $A$ is strictly included in $B$, written $A \Subset B$, if $A$ lies in the interior of $B$. The nesting condition (N) requires that any two distinct confidence sets be strictly nested or disjoint. For each $i$, $\mathcal A(i) = \{i\} \cup \{i' : \mathcal C_i \Subset \mathcal C_{i'}\}$ indexes the confidence sets containing $\mathcal C_i$.

Formalization targets

Goal: Theorem 1 (pp. 10–11)

Under (C1)–(C3), (N) and the two regularity conditions (S1)–(S2) described below, the constraint (3) holds if and only if there are $\beta \in \mathbb R^K$, $\kappa,\lambda \in \mathbb R^I_+$ and $\phi_{il} \in \mathcal K_i^\star$ such that, for all $i \in \mathcal I$ and $l$,

$$b^\top\beta + \sum_{i}\big[\overline p_i\kappa_i - \underline p_i\lambda_i\big] \le w,\qquad c_i^\top\phi_{il} + s_l^\top x + t_l \le \sum_{i' \in \mathcal A(i)}[\kappa_{i'} - \lambda_{i'}],$$ $$C_i^\top\phi_{il} + A^\top\beta = S_l^\top x + \mathbf t_l,\qquad D_i^\top\phi_{il} + B^\top\beta = 0.$$

Milestones

1. Theorem 1, sufficiency. The system implies (3), under (C1), (C3) and (N) alone.
2. Lemma 1 (p. 34). For a strictly feasible conic confidence set, the semi-infinite constraint $v(x,z) + f^\top z + g^\top u \le h$ on the set holds iff multipliers $\phi_l \in \mathcal K^\star$ exist with $c^\top\phi_l + s_l^\top x + t_l \le h$, $C^\top\phi_l = S_l^\top x + \mathbf t_l + f$ and $D^\top\phi_l = g$.
3. The dual of the moment problem (p. 35). Constraint (3) holds iff some $\beta$, $\kappa,\lambda \ge 0$ have objective value $\le w$ and satisfy $[Az+Bu]^\top\beta + \sum_i \mathbf 1_{\mathcal C_i}(z,u)[\kappa_i - \lambda_i] \ge v(x,z)$ on $\mathcal C_I$.
4. The partition step (p. 35). Under (N), the indicator constraint on $\mathcal C_I$ is equivalent to constraints with the constant $\sum_{\mathcal A(i)}$ on the pieces $\overline{\mathcal C}_i = \mathcal C_i \setminus \bigcup_{\mathcal C_{i'} \Subset \mathcal C_i} \mathcal C_{i'}$.
5. The boundary step (pp. 35–36). The $i$-th constraint holds on $\overline{\mathcal C}_i$ iff it holds on all of $\mathcal C_i$.

Significance

When the $\mathcal K_i$ are orthants, second-order cones or semidefinite cones, Theorem 1 turns the semi-infinite, measure-valued constraint (3) into a linear, conic-quadratic or semidefinite system of size polynomial in the data. The paper's Theorem 2 shows that when nesting fails, even checking $\mathcal P \neq \emptyset$ is strongly NP-hard. Theorem 1 is therefore the tractable side of a sharp dividing line. The paper builds its conservative approximation for non-nested sets (Theorem 3) and its lifting results (Section 3) on it.

The result is proved in the paper; nothing here is open. The formalization contributes two things. First, the duality theory for finite moment problems over measures on a compact set, and conic strong duality for strictly feasible sets: neither exists in Mathlib as stated. Second, a corrected statement. As printed, the "only if" direction of Theorem 1 is false, because (C2) does not give the strong duality the proof attributes to it. No machine-checked version of Theorem 1 is known.

Difficulty

The sufficiency half is weak duality: a pointwise inequality on $\mathcal C_I$ integrated against any $\mathbb P \in \mathcal P$. The necessity half needs three facts.

• Strong duality, with attainment, for an infinite-dimensional linear program over nonnegative measures. Here the obvious reference to a general conic duality theorem needs a constraint qualification on all moment constraints jointly, and (C2) controls only the probability bounds.
• A geometric step: under (N), a constraint imposed on $\overline{\mathcal C}_i$ extends to all of $\mathcal C_i$. This uses convexity of $v$ in $(z,u)$ together with the compactness of $\mathcal C_i$ and the strict inclusion of its descendants.
• Conic duality with dual attainment for each confidence set (Lemma 1), which fails without strict feasibility.

Formalization scope

Vectors are Fin n → ℝ, products are Matrix.mulVec and dotProduct, and the outcome space is (Fin nP → ℝ) × (Fin nQ → ℝ) with its Borel $\sigma$-algebra. The index set is Fin (nI + 1), 0-based, with $\mathcal C_I$ = Fin.last nI. Probabilities are μ.real. Constraint (3) is stated in its "for all $\mathbb P$" form, so no supremum of reals appears. The scalar $t_l$ and the vector $\mathbf t_l$ are separate fields.

Every member of $\mathcal P$ is a probability measure with finite first moment, so $\mathbb E_{\mathbb P}[A\tilde z + B\tilde u]$ is a genuine integral and not Lean's default value $0$. The expectation $\mathbb E_{\mathbb P}[v(x,\tilde z)]$ is genuine as well, since $v$ grows at most linearly. Hypothesis (C2) keeps $\mathcal P$ nonempty, so (3) cannot hold vacuously. A sorry-free sanity file exhibits two nested intervals for which all hypotheses of the goal hold at once.

Hypotheses added to the paper's, each needed for a true statement:

• (S1) moment-problem regularity. Every small common shift of $b$ and of each probability interval stays feasible over finite measures on $\mathcal C_I$. It is needed because with $\mathcal C_1$ the unit disk, $\mathbb E[\tilde z_1] = 1$, $v = z_2$ and $w = 0$, constraint (3) holds but the system has no solution.
• (S2) strict feasibility of every confidence set. It is needed because a confidence set that is a single boundary point of a second-order cone constraint admits no dual multipliers in Lemma 1.
• $\mathcal C_i \subseteq \mathcal C_I$ and $P + Q \ge 1$ in the partition and boundary steps. In dimension zero a set is strictly included in itself and $\overline{\mathcal C}_i$ can be empty.

(S1) also excludes some instances the page allows: $\overline p_i = 0$ or $\underline p_i = 1$ for $i \ne I$, and expectation rows that cannot be shifted in every direction by measures on $\mathcal C_I$.

The sufficiency milestone drops (C2) and the standing bounds $0 \le \underline p_i \le \overline p_i \le 1$, which only strengthens it.

Needed infrastructure, all reusable: conic duality for closed convex cones, Lagrangian duality for linear programs over finite measures on a compact set, and the extension of a convex inequality from the boundary of a compact set. Contributions of any of these as separate lemmas are welcome.

Selected references

• W. Wiesemann, D. Kuhn, M. Sim, Distributionally Robust Convex Optimization, Optimization Online preprint 3757, version of September 22, 2013. https://optimization-online.org/wp-content/uploads/2013/02/3757.pdf ; Operations Research 62(6):1358–1376, 2014. https://doi.org/10.1287/opre.2014.1314
• A. Shapiro, On duality theory of conic linear problems, in Semi-Infinite Programming, chapter 7, Kluwer, 2001 (reference [56] of the paper; the result the proof of Theorem 1 cites as Proposition 3.4).
• E. Delage, Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• J. Goh, M. Sim, Distributionally robust optimization and its tractable approximations, Operations Research 58(4):902–917, 2010. https://doi.org/10.1287/opre.1090.0712
• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization, SIAM, 2001. https://doi.org/10.1137/1.9780898718829