Optimization

Motivation

Many convex problems met in practice — least squares with a rank-deficient matrix, dual problems of linearly constrained programs, $\min_x g(Ax)$ with a strongly convex $g$ and a wide matrix $A$ — are not strongly convex: their optimal set is a whole affine piece rather than a point. The classical linear-rate theory of first order methods assumes strong convexity, yet these methods are observed to converge linearly on such problems as well.

Necoara, Nesterov and Glineur (arXiv:1504.06298v4, 2016; Math. Program. 175, 2019) introduce a hierarchy of relaxations of strong convexity, all measured relative to the projection onto the optimal set, and prove linear convergence of the projected gradient method, the fast gradient method and feasible descent methods under them. This mission formalizes the result on the fast gradient method (FGM) for the first and strongest relaxation, quasi-strong convexity: an accelerated linear rate, with $\sqrt{\kappa_f/L_f}$ in place of $\kappa_f/L_f$, under the condition that all extrapolated points share one projection onto the optimal set.

Nesterov's estimate-sequence technique (Nesterov, Introductory Lectures on Convex Optimization, 2004, §2.2) gives the rate $(1-\sqrt{\mu})^k$ for strongly convex functions. The paper shows that the same argument survives when strong convexity is replaced by the quasi-strong inequality at the projection, provided the projections of the points $y^k$ do not move.

Setting

Work in $\mathbb{R}^n$ with the Euclidean inner product $\langle u, v\rangle = u^\top v$ and norm $\|\cdot\|$. Problem (P) is

$$f^* = \min_{x \in X} f(x),$$

with $X \subseteq \mathbb{R}^n$ closed and convex and $f$ convex and differentiable with $L_f$-Lipschitz gradient: $\|\nabla f(x) - \nabla f(y)\| \le L_f\|x - y\|$. The optimal set $X^* = \{x \in X : f(x) = f^*\}$ is assumed nonempty. For a closed set $S$, $[u]_S$ denotes a nearest point of $u$ in $S$.

$f$ is quasi-strongly convex with constant $\kappa_f > 0$ (Definition 1, inequality (10)) if, with $\bar x = [x]_{X^*}$,

$$f^* \ge f(x) + \langle \nabla f(x), \bar x - x\rangle + \frac{\kappa_f}{2}\|x - \bar x\|^2 .$$

The condition number is $\mu_f = \kappa_f / L_f$.

The fast gradient method (FGM) starts from $x^0 = y^0 \in X$ and iterates, for $k \ge 0$,

$$x^{k+1} = \Big[y^k - \tfrac{1}{L_f}\nabla f(y^k)\Big]_X, \qquad y^{k+1} = x^{k+1} + \beta\,(x^{k+1} - x^k), \qquad \beta = \frac{\sqrt{L_f} - \sqrt{\kappa_f}}{\sqrt{L_f} + \sqrt{\kappa_f}} .$$

The gradient mapping at $y$ is $g(y) = L_f(y - y^+)$ with $y^+ = [y - \frac{1}{L_f}\nabla f(y)]_X$.

The analysis uses the estimate functions of Lemma 1: for $\alpha_k \in (0,1)$, $\lambda_0 = 1$, $\lambda_{k+1} = (1-\alpha_k)\lambda_k$, $\phi_0(z) = f(y^0) + \frac{\kappa_f}{2}\|z - y^0\|^2$ and

$$\phi_{k+1}(z) = (1-\alpha_k)\phi_k(z) + \alpha_k\Big(f(x^{k+1}) + \tfrac{1}{2L_f}\|g(y^k)\|^2 + \langle g(y^k), z - y^k\rangle + \tfrac{\kappa_f}{2}\|z - y^k\|^2\Big).$$

Formalization targets

Goal: Theorem 14 (p. 25)

If all iterates $y^k$ of (FGM) have the same nearest point $y^*$ in $X^*$, then

$$f(x^k) - f^* \le \big(1 - \sqrt{\mu_f}\big)^k \cdot 2\big(f(x^0) - f^*\big) \qquad \forall k \ge 0 .$$

Milestones

1. (54), p. 24. For every $x \in \mathbb{R}^n$: $f^* \ge f(x^+) + \langle g(x), \bar x - x\rangle + \frac{1}{2L_f}\|g(x)\|^2 + \frac{\kappa_f}{2}\|\bar x - x\|^2$.
2. Lemma 1, p. 24. If $[y^k]_{X^*} = y^*$ for all $k$ and $x^{k+1} = [y^k - \frac1{L_f}\nabla f(y^k)]_X$, then $\phi_k(y^*) \le (1-\lambda_k)f^* + \lambda_k\phi_0(y^*)$.
3. Lemma 2, p. 25. If moreover $f(x^k) \le \min_z \phi_k(z)$ for all $k$, then $f(x^k) - f^* \le \lambda_k\big(f(x^0) - f^* + \frac{\kappa_f}{2}\|y^* - y^0\|^2\big)$.
4. Proof of Theorem 14, pp. 25–26. The (FGM) iterates satisfy $f(x^k) \le \min_z \phi_k(z)$ for the constant choice $\alpha_k = \sqrt{\mu_f}$.
5. Proof of Theorem 14, p. 26. $\frac{\kappa_f}{2}\|x^0 - \bar x^0\|^2 \le f(x^0) - f^*$ for $x^0 \in X$.

Significance

The theorem gives the accelerated linear rate $(1-\sqrt{\mu_f})^k$ for a class strictly larger than the strongly convex functions. By Remark 1 (p. 27), on an unconstrained problem $\min_x g(Ax)$ (FGM) keeps $y^k$ in $y^0 + \operatorname{Range}(A^\top)$, so the projection onto $X^* = \{x : Ax = t^*\}$ never moves; with Theorem 8 of the paper (quasi-strong convexity of $g(Ax)$ for strongly convex smooth $g$) this covers such problems, and Section 6.1 applies it to consistent linear systems $Ax = b$, where $\frac12\|Ax - b\|^2$ is not strongly convex when $A$ has a nontrivial kernel.

The result is proved in the paper; nothing here is open mathematically. It has no machine-checked proof: the Nesterov-method items already on the platform concern strongly convex or sublinear settings and do not cover quasi-strong convexity or the same-projection condition. A complete development produces a reusable formal estimate-sequence argument, the gradient-mapping inequality (29) for points outside the feasible set, and the quadratic-growth consequence of (10).

Difficulty

The estimate-sequence argument needs a quadratic lower model of $f$ at the point where it is evaluated. Under strong convexity this lower model holds between any two points; under quasi-strong convexity it holds only between a point and its projection onto $X^*$. Lemma 1 evaluates $\phi_k$ at a single point $y^*$ for every $k$, so it needs the projections of all $y^k$ to coincide; the obvious attempt to run the strongly convex proof with $\bar y^k$ changing from step to step fails at the induction step (57). This is why the same-projection hypothesis is part of the theorem rather than an artifact.

The second difficulty is bookkeeping: condition (58) concerns the minimum of the recursively defined quadratics $\phi_k$, which has no closed form in the statement, and it must be matched against the momentum step of (FGM); this is the only place where the specific value of $\beta$ enters.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n). The projection $[u]_S$ is the predicate IsNearest S u p ($p \in S$ minimises $\|u - p\|$), never a choice function; FGM runs are sequences satisfying this predicate at every step, with $x^0 = y^0 \in X$ and 0-based indices (the page's "for $k \ge 1$" is a slip).
• $X^*$ is the set of minimisers of $f$ on $X$, and a minimiser $x^*$ is a binder, so $X^*$ is never empty and $f^* = f(x^*)$ is never defined by an infimum.
• Disclosed addition. The page states (P) with $f$ defined on $X$, but applies (54) "for all $x \in \mathbb{R}^n$" at the extrapolated points $y^k$, which may lie outside $X$. The formalization therefore assumes differentiability, convexity, the Lipschitz gradient and (10) on all of $\mathbb{R}^n$ (QuasiStrongEverywhere). For $X = \mathbb{R}^n$, the case of Remark 1, these are exactly the paper's hypotheses.
• The page omits the squares in $\frac{\kappa_f}{2}\|\bar x - x\|$ of (54) and $\frac{\gamma_0}{2}\|y^* - y^0\|$ of (59); the statements carry the squares, which the proofs use.
• No hypothesis $\kappa_f \le L_f$ is added; it follows from the others unless $X^* = \mathbb{R}^n$, where the theorem is trivial. Condition (58) is written as $f(x^k) \le \phi_k(z)$ for every $z$, avoiding a real infimum.
• Trivializing formalizations are ruled out: a projection defined by choice, an empty optimal set, a gradient that is a junk value off a differentiability set, and a same-projection hypothesis weakened to mere existence are all excluded by the binders.
• Remark 1 is not posed. A development needs the descent lemma for $L$-smooth functions, the variational characterization of the Euclidean projection onto a closed convex set, and the algebra of quadratic estimate functions; all three are reusable. Proofs of any milestone are welcome independently.

Selected references

• I. Necoara, Yu. Nesterov, F. Glineur, Linear convergence of first order methods for non-strongly convex optimization, arXiv:1504.06298v4, 2016; Math. Program. 175 (2019) 69–107. https://arxiv.org/abs/1504.06298v4, https://doi.org/10.1007/s10107-018-1232-1
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• H. Karimi, J. Nutini, M. Schmidt, Linear convergence of gradient and proximal-gradient methods under the Polyak–Łojasiewicz condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636

Distributed learning with noisy gradients

Many learning and estimation problems are solved by a network of agents: each agent holds part of the data, can talk only to its neighbours, and wants to compute the minimizer of the average of all agents' objectives. Examples are sensor networks, multi-robot systems, and data-parallel training without a central server (Nedić and Ozdaglar 2009; Lian et al. 2017). In these settings the agents rarely know their exact gradients; they sample them, one data point or one mini-batch at a time.

Gradient tracking methods let each agent keep, next to its estimate of the minimizer, a running estimate of the network-average gradient. With exact gradients they converge linearly with a constant stepsize (Qu and Li 2018; Nedić, Olshevsky and Shi 2017), which plain distributed gradient descent does not. S. Pu and A. Nedić (Math. Program. 187 (2021) 409–457) analysed the same scheme when every gradient is replaced by an unbiased noisy sample, and called it DSGT (distributed stochastic gradient tracking). This mission formalizes their constant-stepsize result, Theorem 1.

Setting

There are $n$ agents. Agent $i$ holds a cost $f_i:\mathbb R^p\to\mathbb R$, and the agents seek

$$x^*\in\arg\min_{x\in\mathbb R^p} f(x),\qquad f(x)=\frac1n\sum_{i=1}^n f_i(x).$$

Each $f_i$ is $\mu$-strongly convex with $L$-Lipschitz gradient: $\langle\nabla f_i(x)-\nabla f_i(x'),x-x'\rangle\ge\mu\|x-x'\|^2$ and $\|\nabla f_i(x)-\nabla f_i(x')\|\le L\|x-x'\|$.

Noisy gradients. At time $k$ agent $i$ draws a random sample $\xi_{i,k}$ and observes $g_i(x,\xi_{i,k})$, with $\mathbb E[g_i(x,\xi_{i,k})]=\nabla f_i(x)$ and $\mathbb E\|g_i(x,\xi_{i,k})-\nabla f_i(x)\|^2\le\sigma^2$; the samples are independent.

The network. Agents are coupled by a nonnegative doubly stochastic matrix $\mathbf W=[w_{ij}]$ (rows and columns sum to $1$), with $w_{ij}>0$ exactly when $i$ and $j$ communicate, some $w_{ii}>0$, and a connected undirected communication graph. The number

$$\rho_w=\Big\|\mathbf W-\tfrac1n\mathbf 1\mathbf 1^\top\Big\|_2<1,$$

the spectral norm, measures how fast one round of averaging brings the agents together.

DSGT. Each agent keeps $x_{i,k}$ and a tracker $y_{i,k}$. Stacking them as rows of $\mathbf x_k,\mathbf y_k\in\mathbb R^{n\times p}$ and writing $G(\mathbf x,\boldsymbol\xi)$ for the matrix with rows $g_i(x_i,\xi_i)$, the method with constant stepsize $\alpha>0$ is

$$\mathbf x_{k+1}=\mathbf W(\mathbf x_k-\alpha\mathbf y_k),\qquad \mathbf y_{k+1}=\mathbf W\mathbf y_k+G(\mathbf x_{k+1},\boldsymbol\xi_{k+1})-G(\mathbf x_k,\boldsymbol\xi_k),$$

started from a deterministic $\mathbf x_0$ and $\mathbf y_0=G(\mathbf x_0,\boldsymbol\xi_0)$. The two error measures are the distance of the average $\bar x_k=\frac1n\sum_ix_{i,k}$ to $x^*$ and the consensus error $\|\mathbf x_k-\mathbf 1\bar x_k\|^2=\sum_i\|x_{i,k}-\bar x_k\|^2$.

Formalization targets

Goal: Theorem 1

Fix $\Gamma>1$ and a stepsize $\alpha$ below the explicit threshold (7) of the paper (a minimum of three expressions in $\rho_w$, $\|\mathbf W-\mathbf I\|$, $\mu$, $L$, $\Gamma$). Then a certain explicit $3\times3$ matrix $\mathbf A$ has spectral radius $\rho(\mathbf A)<1$, and with $M_\sigma=[3\alpha^2L^2+2(\alpha L+1)(n+1)]\sigma^2$,

$$\limsup_{k\to\infty}\mathbb E\|\bar x_k-x^*\|^2\le\frac{\Gamma+1}{\Gamma}\frac{\alpha\sigma^2}{\mu n}+\frac{\Gamma+1}{\Gamma-1}\,\frac{4\alpha^2L^2(1+\alpha\mu)(1+\rho_w^2)\rho_w^2}{\mu^2n(1-\rho_w^2)^3}\,M_\sigma,$$ $$\limsup_{k\to\infty}\mathbb E\|\mathbf x_k-\mathbf 1\bar x_k\|^2\le\frac{\Gamma+1}{\Gamma-1}\,\frac{4\alpha^2(1+\rho_w^2)\rho_w^2(2\alpha^2L^3\sigma^2+\mu M_\sigma)}{\mu(1-\rho_w^2)^3}.$$

The constants are the paper's, so the goal is stated with them.

Companion: Corollary 1

Under a further stepsize condition (13), $\rho(\mathbf A)\le1-\frac{\Gamma-1}{\Gamma+1}\alpha\mu$.

Milestones

The milestones follow the paper's proof: the tracking identity (6); Lemma 1 on $\rho_w$; the one-step conditional estimates of Lemmas 2–4 and the auxiliary Lemmas 8–9; the linear system of inequalities (21) and its iterate (22); the determinant criterion Lemma 5; the bound $\det(\mathbf I-\mathbf A)>0$ under the relations (23)–(25); and the lower bound (27) on the auxiliary parameter $\beta$.

Significance

The first term of the bound on $\mathbb E\|\bar x_k-x^*\|^2$, $\alpha\sigma^2/(\mu n)$ up to the factor $(\Gamma+1)/\Gamma$, is the error of centralized stochastic gradient descent that averages $n$ samples per step; it does not depend on the network. The network enters only through terms of order $\alpha^2$. So for small stepsizes a decentralized method with gradient tracking pays nothing in the limiting error for having no central server. Theorem 1 is one of the standard references for this statement in decentralized stochastic optimization.

The result is proved in the paper, with constants. It has no machine-checked proof that we know of. Formalizing it produces a checked development of the linear-system method for distributed algorithms: conditional moment bounds for coupled stochastic recursions, a $3\times3$ linear system of inequalities between expectations, and a Perron–Frobenius criterion for its stability. The same pattern recurs in the analysis of many gradient-tracking and variance-reduced decentralized methods.

Difficulty

The obvious argument would bound each error by itself, but the three quantities $\mathbb E\|\bar x_k-x^*\|^2$, $\mathbb E\|\mathbf x_k-\mathbf 1\bar x_k\|^2$ and $\mathbb E\|\mathbf y_k-\mathbf 1\bar y_k\|^2$ feed into one another, and none of them contracts on its own. The tracker error in particular depends on the next iterate, which itself depends on the current noise, so the cross terms do not vanish in conditional expectation and must be estimated separately (Lemmas 8 and 9).

Once the coupled system is set up, its stability needs the spectral radius of a nonnegative $3\times3$ matrix whose entries depend on all constants at once, and the explicit limiting bounds need its inverse. The determinant criterion of Lemma 5 rests on Perron–Frobenius theory, which Mathlib provides only in part.

Formalization scope

Stacked variables are Fin n → EuclideanSpace ℝ (Fin p). Every matrix norm is written out: $\|\mathbf x-\mathbf 1\bar x\|^2=\sum_i\|x_i-\bar x\|^2$ (Frobenius), $\|\mathbf W-\mathbf I\|$ is the Frobenius norm of the $n\times n$ matrix, and $\rho_w$ is the operator norm of $\mathbf W-\frac1n\mathbf 1\mathbf 1^\top$ on Euclidean $\mathbb R^n$. Spectral radii are taken over $\mathbb C$, so complex eigenvalues count. Expectations are Bochner integrals, and every bounded expectation comes with an integrability conclusion. "$\limsup_k a_k\le B$" is stated as "for every $\varepsilon>0$, eventually $a_k\le B+\varepsilon$". $\mathcal F_k$ is the σ-algebra generated by $\boldsymbol\xi_0,\dots,\boldsymbol\xi_{k-1}$, and conditional statements hold almost surely.

Standing assumptions and additions, all stated in the items:

1. Assumptions 3–4 on $\mathbf W$ are hypotheses of every statement about the iterates, although Theorem 1 cites only Assumptions 1–2.
2. Independence of the noise is mutual independence of all $\xi_{i,k}$; $g_i$ is jointly measurable; $p\ge1$.
3. $\rho_w>0$, because $\beta$, $\mathbf A$ and (7) divide by $\rho_w$.
4. $3\alpha L\le1$ in (20), (21), (22) and Theorem 1: the last step of the paper's proof of (20) needs it, and (7) does not imply it in general (for $\rho_w=0.01$, $\Gamma=1.1$, $\mu=L$ it allows $\alpha\approx0.48/L$).

The goal speaks only about the DSGT iterates, $x^*$ and the matrix $\mathbf A$; it does not assume the linear system (21), $\rho(\mathbf A)<1$ or any estimate of the proof. The clause of Theorem 1 that $\sup_{l\ge k}\mathbb E[\cdot]$ approaches the limsup at the rate $\mathcal O(\rho(\mathbf A)^k)$ carries an unquantified constant and is not formalized: the paper's proof yields only the envelope (22) and the limit of its right-hand side, not a rate at which $\sup_{l\ge k}\mathbb E[\cdot]$ reaches the limsup; the envelope (22) is a milestone. Theorem 2 (diminishing stepsizes) is the subject of the second mission of the series.

A complete development needs conditional expectations of functions of independent samples, a Frobenius-norm calculus for stacked vectors, the consensus contraction of Lemma 1, and the Perron–Frobenius facts behind Lemma 5. The last two are reusable beyond this mission. Proofs of any milestone, and of the deterministic matrix lemmas in particular, are welcome independently.

Selected references

• S. Pu, A. Nedić, Distributed stochastic gradient tracking methods, Mathematical Programming 187 (2021) 409–457. https://doi.org/10.1007/s10107-020-01487-0
• A. Nedić, A. Olshevsky, W. Shi, Achieving geometric convergence for distributed optimization over time-varying graphs, SIAM J. Optim. 27 (2017) 2597–2633. https://arxiv.org/abs/1607.03218
• G. Qu, N. Li, Harnessing smoothness to accelerate distributed optimization, IEEE Trans. Control Netw. Syst. 5 (2018) 1245–1260. https://arxiv.org/abs/1605.07112
• A. Nedić, A. Ozdaglar, Distributed subgradient methods for multi-agent optimization, IEEE Trans. Automat. Control 54 (2009) 48–61. https://doi.org/10.1109/TAC.2008.2009515
• X. Lian, C. Zhang, H. Zhang, C.-J. Hsieh, W. Zhang, J. Liu, Can decentralized algorithms outperform centralized algorithms? A case study for decentralized parallel stochastic gradient descent, NeurIPS 2017. https://arxiv.org/abs/1705.09056

Motivation

Distributionally robust stochastic optimization (DRSO) chooses a decision $x$ to minimize the worst expected loss $\sup_{\mu\in\mathfrak M}\mathbb E_\mu[\Psi(x,\xi)]$ over an ambiguity set $\mathfrak M$ of probability distributions, instead of the expectation under one estimated distribution. When $\mathfrak M$ is a ball around a nominal distribution $\nu$ (often the empirical distribution of data) in the Wasserstein distance, the set contains distributions with supports different from that of $\nu$, and the worst case is driven by how far mass can be moved and how fast the loss grows along the way. This makes Wasserstein balls a standard choice in data-driven optimization, statistical learning and operations research.

The inner problem, a supremum over an infinite-dimensional set of measures, is not directly computable. Gao and Kleywegt (arXiv:1604.02199v3) show that it equals a minimization over a single scalar multiplier, for an arbitrary Polish space and nominal distribution and a merely measurable loss.

Timeline. Esfahani and Kuhn (2018, doi:10.1007/s10107-017-1172-1) proved a strong duality for $p=1$ and empirical $\nu$ on $\mathbb R^m$, giving finite convex reformulations for piecewise-affine losses. Blanchet and Murthy (2019, doi:10.1287/moor.2018.0936) proved duality for general optimal transport costs on Polish spaces under upper semicontinuity of the loss, with a dual over pairs $(\lambda,\varphi)$. Gao and Kleywegt's result, first posted in 2016 and published in Mathematics of Operations Research (2023, doi:10.1287/moor.2022.1275), covers every order $p\in[1,\infty)$, every nominal $\nu$ and every measurable loss with finite growth rate, with a dual in one variable.

Setting

Let $(\Xi,d)$ be a Polish space (complete, separable metric) with its Borel $\sigma$-algebra, $\mathcal P(\Xi)$ the Borel probability measures, $p\in[1,\infty)$ and $\theta>0$. The decision variable is suppressed: $\Psi:\Xi\to\mathbb R$ is a Borel measurable loss with $\Psi\in L^1(\nu)$ for a fixed nominal distribution $\nu\in\mathcal P(\Xi)$.

The Wasserstein distance of order $p$ is given by

$$W_p^p(\mu,\nu)=\inf\Big\{\int_{\Xi\times\Xi}d^p(\xi,\zeta)\,\gamma(d\xi,d\zeta):\ \gamma\in\mathcal P(\Xi\times\Xi),\ \pi^1_\#\gamma=\mu,\ \pi^2_\#\gamma=\nu\Big\}.$$

The primal value is the worst-case expectation over the Wasserstein ball,

$$v_P=\sup_{\mu\in\mathcal P(\Xi)}\Big\{\int_\Xi\Psi\,d\mu:\ W_p(\mu,\nu)\le\theta\Big\}.$$

The regularization operator is $\Phi(\lambda,\zeta)=\inf_{\xi\in\Xi}\{\lambda d^p(\xi,\zeta)-\Psi(\xi)\}\in\mathbb R\cup\{-\infty\}$, the dual objective is $h(\lambda)=\lambda\theta^p-\int_\Xi\Phi(\lambda,\zeta)\,\nu(d\zeta)$, and the dual value is $v_D=\inf_{\lambda\ge0}h(\lambda)$. The growth rate of $\Psi$ is

$$\kappa=\inf\Big\{\lambda\ge0:\int_\Xi\Phi(\lambda,\zeta)\,\nu(d\zeta)>-\infty\Big\}\in[0,\infty],$$

with $\kappa=\infty$ if no $\lambda$ qualifies. The lemmas also use the near-optimal distances $\overline D(\lambda,\zeta)$ and $\underline D(\lambda,\zeta)$, the limits as $\varepsilon\downarrow0$ of the largest and smallest $d^p(\xi,\zeta)$ over $\varepsilon$-minimizers $\xi$ of $\lambda d^p(\cdot,\zeta)-\Psi$.

In Lean these objects are DRSOWass.Duality.wassPow, vP, Phi, dualObj, vD, growthRate, DUpper, DLower.

Formalization targets

Goal: Theorem 1 (p. 17)

If $\kappa<\infty$, then

$$v_P=v_D<\infty.$$

This is the printed theorem: an equality of values together with finiteness. It fixes no constant and needs no regularity of $\Psi$ beyond measurability and integrability.

Milestones

1. Proposition 1, weak duality $v_P\le v_D$ (no growth condition).
2. Lemma 3(i), (ii), (v): $\nu$-measurability of $\Phi(\lambda,\cdot)$, $\overline D$, $\underline D$, $\overline D_0$, $\underline D_0$, and $\nu$-measurable selections of near-optimal and far points.
3. Lemma 4(i)–(iii): monotonicity, upper semicontinuity and concavity of $\Phi(\cdot,\zeta)$, the bound $(\lambda_2-\lambda_1)\overline D(\lambda_2,\zeta)\le-\Psi(\zeta)-\Phi(\lambda_1,\zeta)$, and one-sided derivative bounds.
4. Lemma 5: $h$ is $\infty$ on $[0,\kappa)$, finite on $(\kappa,\infty)$, convex, lower semicontinuous, coercive, and has a minimizer $\lambda^*\in[\kappa,\infty)$.
5. Lemmas 6 and 7: explicit $\varepsilon$-optimal distributions in the ball, built from push-forwards of $\nu$, in the cases $\lambda^*>\kappa$, $\lambda^*=\kappa=0$ and $\lambda^*=\kappa>0$.

Significance

The result. Strong duality turns the worst-case expectation over a Wasserstein ball into a convex problem in one scalar, $\min_{\lambda\ge0}\{\lambda\theta^p-\int\Phi(\lambda,\zeta)\,\nu(d\zeta)\}$, where $\Phi$ is a Moreau–Yosida-type regularization of $-\Psi$. For finite-supported $\nu$ this yields finite-dimensional reformulations of DRSO; the paper derives from it the structure of worst-case distributions (Corollaries 1 and 2) and applications to two-stage problems, point processes and Gaussian nominal distributions. The growth rate $\kappa$ separates the finite case (this theorem) from the case $v_P=\infty$ (Proposition 2).

Formalizing it. The theorem is proved in the paper; to the best of current knowledge none of it is machine-checked. The mission produces a formal statement of the duality on general Polish spaces, together with reusable pieces: extended-valued integrals, the regularization operator and its one-sided derivatives, measurable selection on Polish spaces, and push-forward constructions of near-optimal measures. Formal proofs of Lemma 3 also give measurable-selection tools that Mathlib does not yet provide in this form.

Difficulty

Weak duality is a one-line Lagrangian argument. The difficulty is attainment from the primal side: one must construct, for every $\varepsilon>0$, a distribution in the ball whose expectation is within $\varepsilon$ of $v_D$. A worst-case distribution need not exist (when $\lambda^*=\kappa>0$ mass escapes to infinity), so a compactness argument on $\mathcal P(\Xi)$ fails; and $\Psi$ is only measurable, so the infimum defining $\Phi(\lambda,\zeta)$ cannot be reduced to a countable one, and the measurability of $\Phi(\lambda,\cdot)$ and of near-optimal transport maps needs projection and measurable-selection theorems for analytic sets. The case analysis on whether the dual minimizer exceeds $\kappa$ is forced by the possible non-differentiability of $h$ at $\kappa$.

Formalization scope

• $\Xi$ carries MetricSpace, CompleteSpace, SecondCountableTopology and BorelSpace instances; $\nu$ is a probability measure; $d^p$ is dist ξ ζ ^ p with real $p\ge1$.
• $\Psi$ is assumed Borel measurable in addition to $\Psi\in L^1(\nu)$; the paper's p. 5 states the theorem for a measurable $\Psi$, and $\int\Psi\,d\mu$ for $\mu\ne\nu$ requires it.
• $W_p^p$ is the published RWPI.SqrtLasso.transportCost with cost $d^p$, an infimum over probability couplings in $[0,\infty]$; $W_p(\mu,\nu)\le\theta$ is written $W_p^p(\mu,\nu)\le\theta^p$.
• Integrals that may be infinite are the published ModelRiskOT.Duality.extIntegral, $\int\varphi^+-\int\varphi^-$ in $[-\infty,\infty]$ (with $\infty-\infty=-\infty$). $\Phi$, $h$, $v_P$, $v_D$ are EReal-valued; $\kappa$, $\overline D$, $\underline D$ are ENNReal-valued, so $\kappa=\infty$ is representable and the empty infimum is $\infty$.
• $\limsup_{\varepsilon\downarrow0}$ and $\liminf_{\varepsilon\downarrow0}$ in $\overline D$, $\underline D$ are written as the monotone infimum and supremum over $\varepsilon>0$. $\nu$-measurability is null-measurability for functions and almost-everywhere measurability for maps $\Xi\to\Xi$.
• Repaired or adjusted statements: Lemma 4(i)'s sup inequality is stated for $\varepsilon>0$ (the printed $\varepsilon=0$ case fails when an arg min is empty); in Lemma 6, (7)'s weights $p_1,p_2$ are read as $p_1^\varepsilon,p_2^\varepsilon$; Lemma 5(v) carries $\kappa<\infty$; Lemma 4(iii)'s right derivative is a limit in $(-\infty,\infty]$.
• A trivializing formalization is ruled out: integrals are not Bochner integrals (which would give a non-integrable $\mu$ the value $0$), $\kappa$ is not a real infimum (which would give $0$ when no $\lambda$ qualifies), and the supremum in $v_P$ ranges over probability measures in the ball only, which is nonempty because it contains $\nu$.

A complete development needs couplings and gluing in Mathlib's measure theory, the measurable projection theorem and a measurable selection theorem on Polish spaces, and one-sided derivatives of concave extended-valued functions; the first three are reusable well beyond this mission. Proofs of any milestone, alternative proofs of the goal (e.g. through the Blanchet–Murthy dual), and the companion result Proposition 2 ($\kappa=\infty\Rightarrow v_P=v_D=\infty$) are welcome.

Selected references

• R. Gao, A. J. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, arXiv:1604.02199v3, 2022; Mathematics of Operations Research, 2023. https://arxiv.org/abs/1604.02199
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44(2), 2019. https://doi.org/10.1287/moor.2018.0936
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9

Distributed optimization over directed, changing networks

In distributed optimization, $n$ agents cooperatively minimize the average $f(x)=\frac1n\sum_{i=1}^n f_i(x)$ of private cost functions $f_i:\mathbb R^p\to\mathbb R$, exchanging information only with their current neighbours in a communication network. The model covers sensor networks, multi-robot coordination and machine learning with data split across machines, where no node can see the whole objective. In many of these systems communication is one-directional (broadcast radios with unequal ranges, asymmetric links) and the network changes over time.

Directed links raise a specific obstacle: a node cannot in general choose weights that are both row and column stochastic, because it knows its out-degree but not how its messages are combined by others. The push-sum (ratio consensus) protocol of Kempe, Dobra and Gehrke (2003) circumvents this with column stochastic weights and a scalar correction. Nedić and Olshevsky (2015) combined it with diminishing-step subgradient methods over time-varying directed graphs, obtaining sublinear rates. Gradient tracking methods (Xu, Zhu, Soh and Xie, 2015; Qu and Li, 2016) and EXTRA (Shi, Ling, Wu and Yin, 2015) reached linear rates with constant steps on undirected or static graphs. Nedić, Olshevsky and Shi (arXiv 2016, SIAM J. Optim. 2017) proved geometric convergence of gradient tracking over graphs that are both time-varying and directed; this mission formalizes that result.

Setting

The agents are $\{1,\dots,n\}$. At each time $k$ there is a set $\mathcal A(k)$ of arcs; an arc $j\to i$ means agent $j$ can send to agent $i$. The out-degree $d^{\rm out}_j(k)$ counts the agents $i\ne j$ with $j\to i$ in $\mathcal A(k)$.

Assumption 6. There is $\tilde B_\ominus>0$ such that for every $t\ge0$ the union of the arc sets over the window $t\tilde B_\ominus,\dots,(t+1)\tilde B_\ominus-1$ is strongly connected. Put $B_\ominus=2\tilde B_\ominus-1$.

Assumption 7. The mixing matrix $C(k)$ has $C_{ij}(k)=1/(d^{\rm out}_j(k)+1)$ if $i=j$ or $j\to i\in\mathcal A(k)$, and $0$ otherwise; each $C(k)$ is column stochastic.

Each $f_i$ is differentiable with $L_i$-Lipschitz gradient (Assumption 4) and $\mu_i$-strongly convex with $\mu_i\ge0$, some $\mu_i>0$ (Assumption 5). Write $L=\max_iL_i$, $\bar\mu=\frac1n\sum_i\mu_i$, $\bar\kappa=L/\bar\mu$, and $x^*$ for the minimizer of $f$.

Iterates are $n\times p$ matrices whose row $i$ belongs to agent $i$; $\nabla\mathbf f(\mathbf x)$ has rows $\nabla f_i(x_i)$, and $\|\cdot\|_F$ is the Frobenius norm. Push-DIGing starts from $\mathbf x(0)=\mathbf u(0)$, $\mathbf y(0)=\nabla\mathbf f(\mathbf x(0))$, $\mathbf v(0)=\mathbf 1$ and iterates, with step size $\alpha>0$ and $V(k)=\operatorname{diag}\{\mathbf v(k)\}$,

$$\mathbf u(k+1)=C(k)(\mathbf u(k)-\alpha\mathbf y(k)),\quad \mathbf v(k+1)=C(k)\mathbf v(k),\quad \mathbf x(k+1)=V(k+1)^{-1}\mathbf u(k+1),$$ $$\mathbf y(k+1)=C(k)\mathbf y(k)+\nabla\mathbf f(\mathbf x(k+1))-\nabla\mathbf f(\mathbf x(k)).$$

The constants of the rate are $\tilde\tau=n^{-(2+nB_\ominus)}$, $Q_1=2n(1+\tilde\tau^{-nB_\ominus})/(1-\tilde\tau^{nB_\ominus})$, $\|V^{-1}\|^1_{\max}=\sup_{k,i}1/v_i(k)$ and, for an integer $B$,

$$\delta=Q_1\big(1-\tilde\tau^{nB_\ominus}\big)^{\frac{B-1}{nB_\ominus}},\qquad J_2=3Q_1\|V^{-1}\|^1_{\max}\bar\kappa B\big(\delta+Q_1(B-1)\big)(1+\sqrt n)\big(1+4\sqrt n\sqrt{\bar\kappa}\big).$$

Formalization targets

Goal: Theorem 18

For $n\ge2$, $B\ge B_\ominus$ with $\delta<1$, and every step size

$$0<\alpha<\frac{1.5(1-\delta)^2}{\bar\mu J_2},$$

there is $C>0$ with $\|\mathbf x(k)-\mathbf 1(x^*)^\top\|_F\le C\lambda^k$ for all $k$, where $0<\lambda<1$ is

$$\lambda=\sqrt[2B]{1-\alpha\bar\mu/1.5}\ \text{ if }\ \alpha\le\frac{1.5\big(\sqrt{J_2^2+(1-\delta^2)J_2}-\delta J_2\big)^2}{\bar\mu J_2(J_2+1)^2},\qquad \lambda=\sqrt[B]{\sqrt{\alpha\bar\mu J_2/1.5}+\delta}\ \text{ otherwise}.$$

Milestones

The paper's proof runs a small gain argument around the cycle $\mathbf q\to\mathbf z\to\check{\mathbf h}\to\check{\mathbf x}\to\mathbf q$, where $\mathbf q(k)=\mathbf x(k)-\mathbf 1(x^*)^\top$, $\mathbf z$ are gradient increments, $\mathbf h(k)=V(k)^{-1}\mathbf y(k)$ and $\check{\ }$ is the deviation from the row average. The milestones are the paper's own statements: the equivalent recursion (48) in terms of the row stochastic $\tilde R(k)=V(k+1)^{-1}C(k)V(k)$; the bound (49) $\|V^{-1}\|^1_{\max}\le n^{nB_\ominus}$ and row stochasticity of $\tilde R(k)$; Lemma 13 ($B$-step contraction by $\delta$); Lemmas 14–17 (the four arrows); Lemma 8 (an error bound for inexact gradient descent); Theorem 3 (the small gain theorem) and Lemma 4.

Significance

The theorem gives a geometric rate, with explicit constants, for a first-order method that uses only out-degree information, constant step sizes, one gradient per agent per round, and networks that are directed and need only be strongly connected jointly over windows. Before it, linear rates for distributed gradient methods required undirected or static graphs. The explicit $\lambda$ quantifies how the rate degrades with $n$, $B_\ominus$ and the condition number $\bar\kappa$. The result is proved in the paper; to the extent known, no machine-checked proof exists. A formalization yields a checked statement of the rate together with reusable components: the ergodic-norm small gain theorem, the push-sum weight bound, and the inexact gradient lemma, which also serve the companion DIGing mission on undirected graphs.

Difficulty

The natural Lyapunov approach fails: with asymmetric, time-varying weights there is in general no quadratic function that decreases at every step, and the consensus error contracts only over windows of $B$ iterations. The analysis therefore works with ergodic norms $\max_{k\le K}\lambda^{-k}\|\mathbf s(k)\|_F$ and chains four inequalities. Two further inputs come from outside the paper: the lower bound $v_i(k)\ge n^{-nB_\ominus}$ (Corollary 2(b) of Nedić–Olshevsky 2015) and the contraction of products of row stochastic matrices with entries bounded below on arcs (Lemma 5 of Nedić–Ozdaglar 2010), both of which a complete development has to prove.

Formalization scope

Stacked iterates are functions Fin n → EuclideanSpace ℝ (Fin p); agents are indexed from 0 and time from 0. An arc $j\to i$ is a pair (j, i) in a finite set A k. The weights $\mathbf v(k)$ are defined from $C$ alone, so $\|V^{-1}\|^1_{\max}$ is a constant of the graph sequence; it enters statements as a number with the hypothesis that it is the least upper bound of $\{1/v_i(k)\}$, never as a real supremum. Real powers are Real.rpow. The ergodic norm is the truncated maximum; the untruncated supremum is replaced by its pointwise meaning.

Four hypotheses are added to the page, each disclosed in the statements:

1. Assumption 7 includes the self-weight $C_{jj}(k)=1/(d^{\rm out}_j(k)+1)$. The printed rule assigns weights on arcs only, which makes column sums $d/(d+1)$; the paper's agent updates (p. 21) and analysis use the push-sum convention.
2. The step-size interval is open on the right: at $\alpha=1.5(1-\delta)^2/(\bar\mu J_2)$ the printed formula gives $\lambda=1$.
3. $B\ge B_\ominus$, required by Lemma 13, makes "large enough" precise.
4. $n\ge2$: at $n=1$ the constant $Q_1$ has a zero denominator.

The goal states only the hypotheses of Theorem 18 and the rate; it does not assume any of the arrows, gains, auxiliary parameters $\beta,\eta$ or ergodic-norm bounds, so it cannot be discharged by assembling hypotheses.

A complete development needs matrix-product contraction bounds for push-sum, Frobenius-norm calculus on stacked matrices, and strong convexity estimates for inexact gradient steps. The small gain theorem, Lemma 8 and the push-sum lemmas are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

• A. Nedić, A. Olshevsky, W. Shi, Achieving geometric convergence for distributed optimization over time-varying graphs, SIAM J. Optim. 27 (2017) 2597–2633; arXiv:1607.03218v3. https://arxiv.org/abs/1607.03218 — https://doi.org/10.1137/16M1084316
• A. Nedić, A. Olshevsky, Distributed optimization over time-varying directed graphs, IEEE Trans. Automat. Control 60 (2015) 601–615. https://arxiv.org/abs/1303.2289
• A. Nedić, A. Olshevsky, Stochastic gradient-push for strongly convex functions on time-varying directed graphs, arXiv:1406.2075, 2014. https://arxiv.org/abs/1406.2075
• D. Kempe, A. Dobra, J. Gehrke, Gossip-based computation of aggregate information, Proc. 44th IEEE FOCS, 2003, 482–491. https://doi.org/10.1109/SFCS.2003.1238221
• W. Shi, Q. Ling, G. Wu, W. Yin, EXTRA: an exact first-order algorithm for decentralized consensus optimization, SIAM J. Optim. 25 (2015) 944–966. https://arxiv.org/abs/1404.6264
• G. Qu, N. Li, Harnessing smoothness to accelerate distributed optimization, arXiv:1605.07112, 2016. https://arxiv.org/abs/1605.07112
• J. Xu, S. Zhu, Y. C. Soh, L. Xie, Augmented distributed gradient methods for multi-agent optimization under uncoordinated constant stepsizes, Proc. 54th IEEE CDC, 2015, 2055–2060.

Motivation

Many learning and risk-averse decision problems minimize a function of an expectation that is itself passed through another function: $F(x)=f(g(x))$ with $g(x)=\mathbb E[G(x,\xi)]$. Examples are mean–deviation risk measures, stochastic variational inequalities rewritten as minimization, and policy evaluation in reinforcement learning. Only noisy samples of $g$, of its Jacobian and of $\nabla f$ are available, and the plug-in estimate $\nabla g(x)^\top\nabla f(G)$ of $\nabla F(x)$ is biased because $f$ is nonlinear. Classical stochastic gradient analysis does not apply directly.

Timeline of sample complexities for smooth nonconvex two-level problems, measured by the number of samples needed to reach an $\varepsilon$-stationary point:

• 2017 — Wang, Fang and Liu (Math. Program.) introduce stochastic compositional gradient descent with two time scales; the unconstrained nonconvex rate is $O(\varepsilon^{-4})$ in their measure.
• 2017 — Wang, Liu and Fang (JMLR) accelerate it to $O(\varepsilon^{-2.25})$ for smooth unconstrained problems, still with two time scales.
• 2019–2020 — Ghadimi, Ruszczyński and Wang (arXiv:1812.01094, SIAM J. Optim. 2020) propose NASA, a single-time-scale method with one sample per iteration, and prove $O(\varepsilon^{-2})$ for constrained problems. This mission formalizes that result.

Setting

Problem (1.1) is

$$\min_{x\in X} F(x)=f(g(x)),$$

where $f:\mathbb R^m\to\mathbb R$ and $g:\mathbb R^n\to\mathbb R^m$ are continuously differentiable, $X\subseteq\mathbb R^n$ is closed and convex, and nothing is convex. Assumption 2 asks that $f$, $g$, $\nabla f$, $\nabla g$ be Lipschitz with constants $L_f,L_g,L_{\nabla f},L_{\nabla g}$; then $\nabla F$ is Lipschitz with $L_{\nabla F}=L_g^2L_{\nabla f}+L_fL_{\nabla g}$. $F^*$ is the infimum of $F$ over $X$.

For $\beta>0$ the subproblem solution is $\bar y(x,z,\beta)=\operatorname{argmin}_{y\in X}\{\langle z,y-x\rangle+\frac\beta2\|y-x\|^2\}=\Pi_X(x-z/\beta)$, with $\Pi_X$ the Euclidean projection. A pair $(x,z)$ is judged by the optimality measure

$$V(x,z)=\|\bar y(x,z,1)-x\|^2+\|z-\nabla F(x)\|^2,$$

which vanishes exactly when $z=\nabla F(x)$ and $-\nabla F(x)$ lies in the normal cone to $X$ at $x$.

The NASA method (Algorithm 1) keeps three sequences: iterates $x^k\in X$, gradient averages $z^k$ and value averages $u^k$. With parameters $a,b>0$, regularization $\beta>0$ and stepsizes $\tau_k\in(0,1/a]$:

$$x^{k+1}=x^k+\tau_k(\bar y(x^k,z^k,\beta)-x^k),\quad z^{k+1}=(1-a\tau_k)z^k+a\tau_k[J^{k+1}]^\top s^{k+1},\quad u^{k+1}=(1-b\tau_k)u^k+b\tau_kG^{k+1}.$$

Assumption 1 governs the oracle. Given $\mathcal F_k$, the outputs $G^{k+1}$, $J^{k+1}$ and $s^{k+1}$ are conditionally unbiased for $g(x^{k+1})$, $\nabla g(x^{k+1})$ and $\nabla f(u^k)$. Their second moments are bounded by $\sigma_G^2,\sigma_J^2,\sigma_s^2$, and $s^{k+1}$, $J^{k+1}$ are conditionally independent. The analysis rests on the merit function $W(x,z,u)=a(F(x)-F^*)-\eta(x,z)+\frac\gamma2\|g(x)-u\|^2$, where $\eta$ is the optimal value of the subproblem.

Formalization targets

Goal: Theorem 2(c), (3.37)

With $a=b=1$, $\beta=\big(\frac{(1+\alpha)^2}{\alpha}L_g^2+\frac\alpha4\big)L_{\nabla f}$ for some $\alpha>0$, $\tau_0=1$, $\tau_k=1/\sqrt N$ for $k\ge1$, $N\ge2$, and $R$ uniform on $\{1,\dots,N-1\}$:

$$\mathbb E[V(x^R,z^R)]\le\frac4{\sqrt N-1}\Big(\frac2{\alpha L_{\nabla f}}\big[\max(L_1,L_2)+\max(1,\beta^2)\big]\big[W(x^0,z^0,u^0)+\hat\sigma^2\big]+\sigma_J^2\sigma_s^2\Big).$$

The constants $L_1,L_2$ (3.32) and $\hat\sigma^2$ are explicit in the problem data. This is the paper's headline rate, and every other statement of the mission feeds it.

Milestones

1. Lemma 1: $\|\bar y(x,z,1)-x\|\le\max(1,\beta)\|\bar y(x,z,\beta)-x\|$.
2. Lemma 2: $\nabla F$ is $L_{\nabla F}$-Lipschitz.
3. Lemma 3: $\eta$ has an $L_{\nabla\eta}$-Lipschitz gradient in $(x,z)$.
4. (3.21): $\langle z,d\rangle+\beta\|d\|^2\le0$ for the subproblem step $d$.
5. Lemma 4: the pathwise descent inequality $c\sum\tau_k(\|d^k\|^2+\|g(x^k)-u^k\|^2)\le W(x^0,z^0,u^0)+\sum r^{k+1}$.
6. Proposition 1(a): moment bounds on $z^k$ and $d^k$.
7. Proposition 1(b): $\sum\mathbb E[r^{k+1}]\le\hat\sigma^2\sum\tau_k^2$.
8. (3.29): $V(x,z)\le\max(1,\beta^2)\|d\|^2+\|z-\nabla F(x)\|^2$.
9. Theorem 2(a): the weighted gradient-tracking error.
10. Theorem 2(b): the bound on $\mathbb E[V(x^R,z^R)]$ for general admissible stepsizes.

Significance

The result. Theorem 2(c) gives $\mathbb E[V(x^R,z^R)]\le\varepsilon$ after $O(\varepsilon^{-2})$ iterations with one oracle call each. That matches the complexity of stochastic gradient descent on single-level smooth nonconvex problems, so the nested structure costs only constants. The bound holds with constraints, and $z^R$ comes with a certified estimate of $\nabla F(x^R)$. The same merit-function technique underlies later single-time-scale methods for multi-level and conditional stochastic optimization.

Formalizing it. The result is proved on paper, not formalized. A machine-checked proof requires the whole chain, Lemma 4 through Theorem 2, to be stated with constants that the argument actually supports. Several printed constants do not meet that bar (see Formalization scope), so the formalization also certifies a corrected version of the theorem. The deterministic milestones (Lemmas 1–3, (3.21), (3.29)) are general facts about Euclidean projections and value functions of strongly convex subproblems, and other projected-gradient developments can reuse them.

Difficulty

The obvious approach fails. Analyzing $F(x^k)$ alone does not work because the step uses $z^k$, a biased and correlated estimate of $\nabla F(x^k)$, and its error does not vanish at a single time scale. The analysis instead tracks the coupled potential $W$. Each of its three terms needs a different tool: the descent lemma for $F$, the smoothness of the value function $\eta$ (Lemma 3, which needs differentiability of a parametric minimum), and a recursion for $u^k$. These pieces must combine under the single coupling condition (3.16). The probabilistic part is delicate as well. The cross terms vanish only in expectation, they require conditional independence of $J^{k+1}$ and $s^{k+1}$, and their integrability is not automatic. Theorem 2(a) adds a weighted unrolling of the $z$-recursion through the products $\Gamma_k$ and the summation condition (3.30).

Formalization scope

Points live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). Jacobians are continuous linear maps with the operator norm, and $\nabla g(x)^\top$ is the adjoint. The projection is a function $P$ with the published predicate SpectralProjGrad.Shared.IsProjOnto X P, and $\bar y(x,z,\beta)=P(x-\beta^{-1}z)$. $\eta$ is the subproblem objective evaluated at $\bar y$, and Lemma 3 places $(x,z)$ in the $L^2$ product WithLp 2 (ℝⁿ × ℝⁿ). $F^*$ is sInf over $X$, and $F$ is assumed bounded below on $X$. The regularization $\beta_k\equiv\beta$ and the stepsizes are deterministic.

The randomness lives on a standard Borel probability space. Assumption 1 is stated with respect to any filtration to which $x^k,z^k,u^k$ are adapted, which includes the paper's natural filtration. It requires square-integrable oracle outputs, so that no conditional-expectation hypothesis is vacuous. Statements printed with conditional expectations on the left and constants on the right (Proposition 1, Theorem 2(a)) are stated in total expectation, which is what the proofs establish. Every conclusion about an expectation includes the integrability of the integrand, so a bound cannot hold because a non-integrable integral defaults to $0$. $\mathbb E[V(x^R,z^R)]$ is the $\tau$-weighted average of $\mathbb E[V(x^k,z^k)]$ over $k=1,\dots,N-1$ (3.34). Lemma 4 is deterministic: it holds along every path of the recursions, whatever the oracle outputs. The recursions tie $y^k$ to the projection and $z^k,u^k$ to the oracle outputs, so the goal cannot be satisfied by arbitrary sequences or by a vacuous oracle.

Corrections to printed constants, each stated in the item's Formalization Note:

• (3.18): the noise term of $r^{k+1}$ carries $\gamma b^2$, not $b^2$. The printed Lemma 4 has a counterexample.
• (3.26): $\hat\sigma^2$ uses $aL_{\nabla F}$, $\max(\sigma_J^2\sigma_s^2,\|z^0\|^2)/\beta^2$ (the $k=0$ term) and $\gamma b^2\sigma_G^2$.
• (3.33): the coefficient of $\max(1,\beta^2)\hat\sigma^2$ is $1/c$, not $a\bar c/c$. The two agree when $a\bar c=1$.
• (3.37): the denominator is $\alpha L_{\nabla f}$, not $\alpha L_{\nabla F}$, since the proof sets $c=\alpha L_{\nabla f}/4$. The proof also fixes $\gamma=\alpha L_{\nabla f}$ in $W$ and $\hat\sigma^2$.
• Proposition 1(a): the bound $\mathbb E\|z^k\|^2\le\sigma_J^2\sigma_s^2$ is false conditionally on $\mathcal F_{k-1}$ and is stated in expectation.
• Hypotheses the proofs use but the statements omit: $\tau_k\le1$, $b\tau_k\le1$, $a\beta\ge c$ and $\gamma b\ge2c$, $\tau_0=1/a$ (Theorem 2(a),(b)), $N\ge2$, and $L_{\nabla f}>0$.

The second claim (3.38) of Theorem 2(c) is excluded: its printed constant is smaller than what the proof gives. Theorem 3 (asymptotics) and the ASA variant of §4 are out of scope. Contributions are welcome at every milestone. Solvers will need Euclidean projection characterizations, differentiability of the squared distance to a convex set, conditional-independence product rules for conditional expectations, and Abel-type summation for the $\Gamma_k$ weights.

Selected references

• S. Ghadimi, A. Ruszczyński, M. Wang, A Single Time-Scale Stochastic Approximation Method for Nested Stochastic Optimization, arXiv:1812.01094v2, 2019; SIAM J. Optim. 30(1), 2020. https://arxiv.org/abs/1812.01094
• M. Wang, E. X. Fang, H. Liu, Stochastic compositional gradient descent: algorithms for minimizing compositions of expected-value functions, Math. Program. 161, 2017. https://doi.org/10.1007/s10107-016-1017-3
• M. Wang, J. Liu, E. X. Fang, Accelerating stochastic composition optimization, JMLR 18(105), 2017. https://jmlr.org/papers/v18/16-504.html
• S. Ghadimi, G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23(4), 2013. https://doi.org/10.1137/120880811
• A. Ruszczyński, Nonlinear Optimization, Princeton University Press, 2006.