Optimization

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

Motivation

In an aggregative game, each player's decision affects a common quantity, such as total production or total demand. An agent may be able to calculate its own preferred response while lacking direct access to that aggregate. Koshal, Nedić, and Shanbhag study how agents can estimate it by exchanging information only with neighbours on a communication graph. Their asynchronous gossip algorithm lets one randomly selected agent contact a neighbour at each tick; both agents update their estimates and decisions. The constant stepsize regime matters when agents cannot steadily reduce their stepsizes or want to keep responding to new information. It gives an error bound rather than exact convergence: the decisions remain near an equilibrium by an amount controlled by the step, the game, and the graph. The model and this bound are from Koshal, Nedić, and Shanbhag, 2016.

The same paper analyzes a synchronous scheme with diminishing steps and a gossip scheme with update-count steps. This mission isolates the constant-step case in §4.3, and targets the equal-probability, equal-stepsize display at the end of that section. It uses the paper's numbered Lemmas 2, 3, and 11 and relations (30), (31), (44), and (55) as intermediate targets. The restriction to the final special case is material: the argument printed for general player-specific steps and update probabilities has gaps in (53) and (54), while both problematic terms disappear when the steps and update probabilities are equal.

Setting

There are $N$ players, each choosing $x_i$ from a nonempty compact convex set $K_i\subseteq\mathbb R^n$. Write $K=\prod_iK_i$ for feasible profiles and $\bar K=\{\sum_i x_i:x_i\in K_i\}$ for feasible aggregates. Player $i$ has a component map $F_i(x_i,u)$, evaluated at its own decision and an aggregate argument. At a feasible profile $x$, the game map is $\phi(x)_i=F_i(x_i,\sum_jx_j)$. An equilibrium target is the solution $x^*$ of the variational inequality $\operatorname{VI}(K,\phi)$: for every $x\in K$, $\sum_i\langle x_i-x_i^*,\phi(x^*)_i\rangle\ge0$. The paper derives this map from player payoff gradients under its Assumption 1; the present formalization starts with the component maps used by the algorithm.

A connected undirected graph lists the players that may exchange information. At tick $k$, a uniform random player $I^k$ wakes and contacts a neighbour $J^k$ with probability $p_{I^kJ^k}>0$. These draws are independent across ticks. Only the contacted pair average their current estimates $v_i^k$ to obtain $\hat v_i^k$, then project a step using $F_i(x_i^k,N\hat v_i^k)$ onto $K_i$. All agents update their estimate by $v_i^{k+1}=\hat v_i^k+x_i^{k+1}-x_i^k$; for agents outside the pair this leaves both state variables unchanged. The mean estimate is $y^k=N^{-1}\sum_i v_i^k$. Lemma 2 identifies it with the mean decision. The update probability of player $i$ is $p_i=N^{-1}(1+\sum_jp_{ji})$. These definitions and the discrete gossip algorithm are given in §4.1 of the source.

Formalization targets

Constant-step error bound

Suppose $\phi$ is strongly monotone with modulus $\mu>0$, every player uses the same positive step $\alpha$, and all update probabilities equal $p$. Let $C$ bound the gradient evaluations as in Lemma 3. Let $\lambda\in(0,1)$ be a mean-square contraction constant for the gossip matrix $D(k)=W(k)-N^{-1}\mathbf1\mathbf1^\top$, as in (30). If $\bar L_i$ are the aggregate Lipschitz constants of Assumption 3 and $M$ bounds the diameter of each $K_i$, put $B=(\max_i\bar L_i)NM$. Under the inherited assumptions of Proposition 4 and $0<\alpha<1/(2\mu p)$, the goal is existence and uniqueness of $x^*$ together with the last display on PDF page 29:

$$\limsup_{k\to\infty}\mathbb E\|x^k-x^*\|^2 \le \frac{\alpha}{\mu}\left(2C^2N+\frac{BC\sqrt{2nN}}{1-\sqrt\lambda}\right).$$

The milestones separately assert the unique VI solution, the aggregate identity, the bounded gradient evaluations, the contraction estimates (30)–(31), the one-step disagreement relation (44), Lemma 11's limiting disagreement bounds, and the equal-case recursion (55). Together they expose the quantities appearing in the target without weakening its constant or its dependence on $n$ and $N$.

Significance

The bound separates the effects of the step, game regularity, number of agents, decision dimension, and communication quality. In particular, for fixed other parameters the right-hand side scales linearly in $\alpha$ and worsens as $\lambda$ approaches one. It is a quantitative guarantee for a decentralized procedure that sees neighbour messages instead of the exact aggregate. The VI existence and uniqueness target also identifies the equilibrium to which the error is measured. The paper proves the special case in its concluding bound on page 29, subject to the domain correction described below; it is not an unresolved research conjecture.

Formalizing the result produces a reusable interface for graph gossip matrices, random pair draws, relational Euclidean projection, and nonnegative expected disagreement. The intermediate contraction and tracking statements can support other constant-step distributed optimization arguments. The theorem declarations in this proposal are open Lean proof obligations; a successful local build checks their types and definitions, not the mathematical claims. Contributions that establish these obligations, sharpen a bound under the same model, or isolate reusable probability and projection results are in scope.

Difficulty

The estimates $v_i^k$ are coupled to both random pair averaging and the agents' decision changes, so graph connectivity alone does not state a numerical disagreement bound. The proof has to respect the actual distribution of waking and contacted agents when moving from a one-player inequality to an expected profile error. The printed general version illustrates the risk: Assumption 8 controls changes in $x_i$ at a fixed aggregate and therefore cannot justify (53), where the aggregate changes; (54) also replaces coefficients on signed terms by their minimum. The final equal-step, equal-probability case removes these two obstacles, but still requires the exact constants in Lemma 11 and the error recursion.

Formalization scope

Players are indexed by Fin N, decisions use EuclideanSpace ℝ (Fin n), and a profile's squared Euclidean norm is the sum of squared block norms. Coordinate vectors across players also use a Euclidean norm; the ordinary Lean norm on Fin N → ℝ would be a supremum norm. The run starts from a deterministic feasible profile. This fixes the initial state before the independent discrete gossip draws, representing the source's Poisson-clock protocol at its tick times. A projection is a nearest-point relation on a nonempty compact convex set, with no arbitrary value on an empty set. Positive contact probabilities on all graph edges keep the connected graph active.

Assumption 1 is expressed through nonempty compact convex $K_i$ and continuity of $F_i$ on $K_i\times\bar K$, the part of the payoff regularity used by the algorithm. Assumption 3 is stated for every aggregate argument in $\mathbb R^n$, a disclosed strengthening of its printed domain $\bar K$: $N\hat v_i^k$ can leave $\bar K$, as the paper's footnote on page 10 acknowledges. Assumption 8 remains a hypothesis inherited from Proposition 4 even though its term vanishes for equal steps. The constants $C$, $\lambda$, and $M$ carry their defining bounds as hypotheses; the conclusion does not assume Lemma 11 or (55). Expected nonnegative quantities use extended-real lintegrals and an extended-real limit superior, preventing a failed Bochner integral from silently becoming zero. The formalization asserts existence of a VI solution, so an empty solution set cannot trivialize the goal.

Selected references

• J. Koshal, A. Nedić, and U. V. Shanbhag, Distributed Algorithms for Aggregative Games on Graphs, Operations Research 64(3):680–704, 2016. arXiv:1605.00267v2; DOI:10.1287/opre.2016.1501.

Motivation

Lasserre's hierarchy is a sequence of semidefinite relaxations for minimizing a polynomial over a set defined by polynomial equations and inequalities (Lasserre 2001). Under the archimedean condition its optimal values converge to the true minimum, but only asymptotically in general; in practice the hierarchy is often exact at a small relaxation order. J. Nie's paper (arXiv:1206.0319v2, Math. Program. 146 (2014)) explains this gap in two steps. Its Theorem 1.1 shows that finite convergence follows when the classical optimality conditions of nonlinear programming hold at every global minimizer. Its Theorem 1.2, the subject of this mission, shows that those optimality conditions hold at every local minimizer for all input data outside the zero set of finitely many polynomials in the coefficients. Together the two results give finite convergence of Lasserre's hierarchy for generic archimedean problems.

The genericity statement is also of independent interest in nonlinear programming: it says that degenerate local minimizers (failing constraint qualification, strict complementarity or second order sufficiency) are an algebraically exceptional phenomenon for polynomial data of fixed degrees.

Setting

Fix $n$ variables $x=(x_1,\dots,x_n)$ and write $\mathbb R[x]_d$ for the real polynomials of degree at most $d$. Problem (1.1) is

$$\min f(x)\quad\text{s.t.}\quad h_i(x)=0\ (i\in[m_1]),\qquad g_j(x)\ge 0\ (j\in[m_2]),$$

with feasible set $K$. For $u\in K$ the active set is $J(u)=\{j: g_j(u)=0\}$. At $u$:

• the constraint qualification condition (CQC) holds if $\nabla h_1(u),\dots,\nabla h_{m_1}(u),\nabla g_j(u)$ ($j\in J(u)$) are linearly independent;
• Lagrange multipliers $\lambda,\mu$ satisfy (1.3) $\nabla f(u)=\sum_i\lambda_i\nabla h_i(u)+\sum_j\mu_j\nabla g_j(u)$ and (1.4) $\mu_jg_j(u)=0$, $\mu_j\ge0$;
• strict complementarity (1.5) is $\mu_j+g_j(u)>0$ for all $j$;
• with $L=f-\sum_i\lambda_ih_i-\sum_{j\in J(u)}\mu_jg_j$, the second order sufficiency condition (1.7) is $v^T\nabla^2L(u)v>0$ for every $v\neq0$ orthogonal to all active constraint gradients.

The input data are the coefficient vectors of $(f,h,g)\in\mathbb R[x]_{d_0}\times\prod_i\mathbb R[x]_{d_i}\times\prod_j\mathbb R[x]_{d'_j}$; a polynomial in the coefficients is a real polynomial evaluated at that vector. The paper's Condition 4.3 lists four families of such polynomials: resultants $\mathrm{Res}$ and discriminants $\Delta$ (§2.4) of subsets of the constraints, and the polynomials $\mathscr R$ of (4.6) and $\mathscr D$ of (4.11), which detect a complex projective solution of the homogenised critical-point systems (4.5) and (4.10). Homogenisation is $\tilde p(\tilde x)=x_0^{d}p(x/x_0)$ at the nominal degree $d$, with $\tilde x=(x_0,\dots,x_n)$.

Formalization targets

Goal: Theorem 1.2

For positive degrees $d_0,d_i,d'_j$ there are polynomials $\phi_1,\dots,\phi_L$ in the coefficients such that

$$\exists\,(f,h,g)\text{ admissible with }\textstyle\prod_l\phi_l\neq0,\qquad\text{and}\qquad \prod_l\phi_l(f,h,g)\neq0\ \Longrightarrow\ \text{CQC, (1.5), (1.7) at every local minimizer of (1.1).}$$

Milestones

1. Proposition 4.1: there is $\mathscr R$ with $\mathscr R(p_0,\dots,p_k;q)=0$ iff (4.5) has a solution $0\neq\tilde x\in\mathbb C^{n+1}$; and $\mathscr R\neq0$ excludes solutions of (4.4) in $\mathbb C^n$.
2. Proposition 4.2: there is $\mathscr D$ with $\mathscr D(p_0,\dots,p_k)=0$ iff (4.10) has a solution with $\tilde x\neq0$, $y\neq0$; and $\mathscr D\neq0$ makes the KKT system (4.2) nonsingular.
3. Proposition 4.4: at $u\in K$ with multipliers satisfying (1.3) and $\mu_jg_j(u)=0$, items (a)–(d) of Condition 4.3 give at most $n-m_1$ active constraints, CQC, $\lambda_i\neq0$ and $\mu_j\neq0$ on $J(u)$, and $\det H(u)\neq0$ for $H(u)=\left[\begin{smallmatrix}\nabla^2L(u)&G(u)^T\\G(u)&0\end{smallmatrix}\right]$.
4. Lemma 4.6: at a local minimizer where $G(u)$ has full rank, (1.7) holds iff $\det H(u)\neq0$.
5. Proposition 4.5: Condition 4.3 implies CQC, strict complementarity and SOSC at every local minimizer.
6. Appendix A: $\mathscr R$ and $\mathscr D$ do not vanish identically on the input space of given positive degrees.

Significance

The theorem gives the second half of the paper's explanation of finite convergence: combined with Theorem 1.1, Lasserre's hierarchy converges in finitely many steps for all archimedean problems with input outside a proper algebraic subset. Section 5 of the paper derives further consequences, for instance that Marshall's boundary Hessian condition holds on a Zariski open set of data, and that Putinar-type certificates exist generically on the boundary of the cone of nonnegative polynomials. Beyond polynomial optimization, the statement is a precise algebraic form of the folklore that "generic nonlinear programs are nondegenerate".

The result is proved in the paper; no machine-checked version is known. A formalization fixes the exact quantifier structure (the printed statement is vacuous without a nonvanishing clause, and two items of Proposition 4.4 need an extra hypothesis), and builds reusable infrastructure: projective elimination over $\mathbb C$, homogenisation at a nominal degree, and the bordered-Hessian characterization of second order sufficiency.

Difficulty

The local part (Proposition 4.4, Lemma 4.6, Proposition 4.5) is linear algebra plus first and second order necessary conditions. The global part is not. Proposition 4.1 and 4.2 need the main theorem of elimination theory: the set of coefficient vectors for which a homogeneous (or bihomogeneous) system has a nonzero complex solution is Zariski closed, defined by polynomials in the coefficients. Mathlib has the univariate resultant only. Appendix A, which shows these polynomials do not vanish identically, has to control the homogenised systems both at finite points and at points at infinity ($x_0=0$), where only the leading forms of the data are seen. Reasoning over $\mathbb R$ alone does not suffice: the set of data whose real system is solvable is not the zero set of a polynomial.

Formalization scope

Polynomials are MvPolynomial (Fin n) ℝ, points are Fin n → ℝ, and gradients and Hessians are formal partial derivatives. Homogenised polynomials have complex coefficients in n + 1 variables, variable 0 being $x_0$, and homogenisation uses the nominal degree $d$, not the actual degree. CQC is linear independence of an indexed family (repeated gradients count twice). The optimality conditions are bundled: CQC together with one multiplier pair satisfying (1.3), (1.4), (1.5) and (1.7); under CQC the multipliers are unique.

Condition 4.3 is encoded through the defining properties of Res, Δ, $\mathscr R$ and $\mathscr D$ (unsolvability of the corresponding complex projective systems) rather than through the polynomials themselves; since the goal is existential in the polynomials, this is not a weakening. Coefficient variables exist for monomials of every degree, so the goal's nonvanishing clause is asserted at an admissible input: a formal polynomial that is nonzero but vanishes on all admissible data (such as the variable of a monomial of degree $d_0+1$) does not satisfy it. Without that clause the printed theorem would be satisfied by $\phi_1=0$.

Hypotheses added to the page, each disclosed in the statements: $m_1\le n$ in Propositions 4.4 and 4.5 (Condition 4.3's standing assumption; Theorem 1.2 is stated for all $m_1$, as printed), the nonvanishing clause in Theorem 1.2, and item (a) of Condition 4.3 in Proposition 4.4 ii)–iv) (with item (b) alone, $n=1$, $g_1=x+x^2$, $g_2=-x+x^2$, $u=0$ violates CQC). Proposition 4.2's nonsingularity is asserted at all complex critical pairs.

A complete development needs projective elimination theory over $\mathbb C$ (reusable well beyond this mission), multivariate resultants and discriminants as polynomial functions of coefficients, Euler's identity for forms, and genericity facts about critical points of polynomial programs. Contributions to any of these, and direct proofs of the local milestones, are welcome.

Selected references

• J. Nie, Optimality conditions and finite convergence of Lasserre's hierarchy, Math. Program. 146 (2014); preprint arXiv:1206.0319v2, 2013. https://arxiv.org/abs/1206.0319v2, https://doi.org/10.1007/s10107-013-0680-x
• J.B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM J. Optim. 11(3) (2001) 796–817. https://doi.org/10.1137/S1052623400366802
• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977 (Theorem I.5.7A, elimination). https://doi.org/10.1007/978-1-4757-3849-0
• I. Gelfand, M. Kapranov, A. Zelevinsky, Discriminants, Resultants, and Multidimensional Determinants, Birkhäuser, 1994. https://doi.org/10.1007/978-0-8176-4771-1

Motivation

Polynomial optimization asks for the global minimum of a polynomial $f$ over a set $K \subseteq \mathbb R^n$ cut out by polynomial equations and inequalities. It contains nonconvex quadratic programming, max-cut, and many problems from control and engineering. Lasserre's hierarchy (Lasserre 2001) replaces this problem by a sequence of semidefinite programs whose optimal values $f_k$ increase towards the true minimum $f_{\min}$. Under the archimedean condition, Putinar's Positivstellensatz (Putinar 1993) gives asymptotic convergence $f_k \to f_{\min}$.

In computations the hierarchy usually reaches $f_{\min}$ exactly at a small order (Henrion and Lasserre), while the theory guaranteed only the limit. Known failures of finite convergence were special constructions, for example the Motzkin polynomial on the unit ball. Nie (2014) resolves this gap: finite convergence holds whenever the classical optimality conditions of nonlinear programming hold at every global minimizer.

Timeline. Lasserre (2001) introduces the hierarchy and proves $f_k \to f_{\min}$ under archimedeanness. Laurent (2007) and Nie (2013) prove finite convergence when $h = 0$ has finitely many complex, respectively real, solutions. Marshall (2006, 2009) introduces the boundary hessian condition and proves that it yields a representation of $f - f_{\min}$ in the quadratic module. Nie (arXiv 2012, Math. Program. 2014) shows that the classical optimality conditions imply the boundary hessian condition, and derives finite convergence.

Setting

Fix polynomials $f, h_1, \dots, h_{m_1}, g_1, \dots, g_{m_2} \in \mathbb R[x]$, $x \in \mathbb R^n$, and the problem

$$\min f(x) \quad \text{s.t.} \quad h_i(x) = 0 \ (i \in [m_1]),\quad g_j(x) \ge 0 \ (j \in [m_2]),$$

with feasible set $K$ and minimum value $f_{\min}$. Put $g_0 := 1$. A polynomial is SOS if it is a sum of squares of polynomials. For $k \in \mathbb N$ the truncated ideal and the truncated quadratic module are

$$\langle h\rangle_{2k} = \Big\{\sum_{i} \phi_i h_i : \deg(\phi_i h_i) \le 2k\Big\}, \qquad Q_k(g) = \Big\{\sum_{j=0}^{m_2} \sigma_j g_j : \sigma_j \text{ SOS},\ \deg(\sigma_j g_j) \le 2k\Big\},$$

and $Q(g) = \bigcup_k Q_k(g)$. The order-$k$ relaxation is $\max \gamma$ s.t. $f - \gamma \in \langle h\rangle_{2k} + Q_k(g)$, with optimal value $f_k$. The archimedean condition asks that $R - \sum_i x_i^2 \in \langle h\rangle_{2t} + Q_t(g)$ for some $t$ and some $R > 0$. The hierarchy has finite convergence if $f_k = f_{\min}$ for some $k$.

At a point $u$ with active set $J(u) = \{j : g_j(u) = 0\}$:

• the constraint qualification (CQC) asks that $\nabla h_i(u)$ ($i \in [m_1]$) and $\nabla g_j(u)$ ($j \in J(u)$) be linearly independent;
• multipliers $\lambda, \mu$ satisfy (1.3)–(1.4) if $\nabla f(u) = \sum_i \lambda_i \nabla h_i(u) + \sum_j \mu_j \nabla g_j(u)$, $\mu_j g_j(u) = 0$ and $\mu_j \ge 0$;
• strict complementarity (SCC) asks $\mu_j + g_j(u) > 0$ for all $j$;
• second order sufficiency (SOSC) asks $v^T \nabla^2_x L(u) v > 0$ for all nonzero $v$ orthogonal to every $\nabla h_i(u)$ and every active $\nabla g_j(u)$, where $L = f - \sum_i \lambda_i h_i - \sum_{j \in J(u)} \mu_j g_j$.

The boundary hessian condition (BHC) at $u$ asks for local parameters $t_1, \dots, t_\ell$ of the variety $V_{\mathbb R}(h)$ near $u$ such that $t_j = g_{\nu_j}$ for $j \le r$ and $K$ is locally $\{t_1, \dots, t_r \ge 0\}$. In these parameters the linear part of $f$ must be $a_1 t_1 + \dots + a_r t_r$ with all $a_j > 0$, and its quadratic part on $t_1 = \dots = t_r = 0$ must be positive definite.

Formalization targets

Goal: Theorem 1.1

If the archimedean condition holds and CQC, SCC and SOSC hold at every global minimizer of the problem, then

$$\exists\, k \in \mathbb N : \quad f_k = f_{\min}.$$

The goal fixes no order $k$ and no rate; it asserts exactly the paper's finite convergence.

Milestones

1. Theorem 3.1: at a local minimizer, CQC + SCC + SOSC imply BHC.
2. Theorem 2.4 (Marshall): archimedean and BHC at every global minimizer imply $f - f_{\min} \in I(V_{\mathbb R}(h)) + Q(g)$.
3. Real Nullstellensatz: $p \equiv 0$ on $V_{\mathbb R}(h)$ implies $p^{2e} + \sigma_2 \in \langle h\rangle$ for some SOS $\sigma_2$.
4. $1 + t + c t^{2e}$ is SOS for some $c > 0$ ($e \ge 1$).
5. The $\varepsilon$-argument: a representation $f - f_{\min} \in I(V_{\mathbb R}(h)) + Q(g)$ makes $\gamma = f_{\min} - \varepsilon$ feasible at one order $k_0$ for all $\varepsilon > 0$.
6. $f_k \le f_{\min}$ for all $k$ and $\{f_k\}$ is nondecreasing.
7. Companion, Proposition 3.4: if every relaxation attains its value and the first order condition fails at a global minimizer, there is no finite convergence.

Significance

The theorem turns an algebraic question (does a degree-bounded certificate of $f - f_{\min} + \varepsilon$ exist uniformly in $\varepsilon$?) into conditions checkable by linear algebra at the minimizers. Combined with the paper's second main result, that these conditions hold off a proper Zariski-closed set of input data, it shows that finite convergence of Lasserre's hierarchy is generic under archimedeanness. This is the theoretical explanation for the finite convergence observed in practice, and it underlies later work on flat truncation and the detection of optimality in moment relaxations.

Formalizing it produces the first machine-checked statements of Lasserre's hierarchy, truncated quadratic modules and the boundary hessian condition on the platform. The paper's own argument (Theorem 3.1 and the $\varepsilon$-argument) is short. Two cited results it rests on, Marshall's Theorem 9.5.3 and the Real Nullstellensatz, are proved in the literature but, as far as is known, have no formal proof in Mathlib or elsewhere. The result itself is proved (Nie 2014); none of it is formalized.

Difficulty

The obvious route is Putinar's Positivstellensatz applied to $f - f_{\min} + \varepsilon$. It gives a certificate for each $\varepsilon > 0$, but its degree grows as $\varepsilon \to 0$, so it yields only $f_k \to f_{\min}$. Finite convergence needs a certificate whose degree is bounded uniformly in $\varepsilon$, which is a statement about $f - f_{\min}$ itself, a polynomial that vanishes on $K$ and is therefore not strictly positive. Putinar's theorem says nothing there. Marshall's theorem supplies the missing representation under the boundary hessian condition, and its proof uses local real-analytic geometry at the zeros of $f - f_{\min}$, together with real algebra of quadratic modules.

Theorem 3.1 asks for a smooth local parametrization of $V_{\mathbb R}(h)$ whose first coordinates are prescribed constraint functions, and for control of the Taylor coefficients of $f$ in those parameters; Mathlib has the analytic ingredients but no such constructions for real varieties. The Real Nullstellensatz depends on the theory of real fields and real ideals. Neither cited result is available in Mathlib.

Formalization scope

Polynomials are MvPolynomial (Fin n) ℝ, points are Fin n → ℝ, and the paper's indices $1, \dots, m$ are Fin m; $m_1 = 0$ or $m_2 = 0$ is allowed. Gradients and Hessians come from formal partial derivatives. SOS is Mathlib's IsSumSq. $f_k$ is a supremum in EReal (it is $-\infty$ when the relaxation is infeasible). $f_{\min}$ is a real number that is the least value of $f$ on $K$, which excludes only $K = \emptyset$. The archimedean condition is the truncated form of p. 2, equivalent to §2.2's. $I(V)$ is Mathlib's vanishingIdeal. The multipliers of SCC and SOSC are the ones that satisfy (1.3)–(1.4). The boundary hessian condition is encoded with a $C^\infty$ parametrization $\Psi$ of $V_{\mathbb R}(h)$ near $u$ that is an immersion and a homeomorphism onto its image, together with nonsingularity of $u$ in the real-algebraic sense ($n - \ell$ polynomials vanishing on $V_{\mathbb R}(h)$ with independent gradients at $u$); Marshall's analytic parameters give the same condition, because both requirements are invariant under a change of parameters that fixes $t_1, \dots, t_r$.

Several encodings would make the statements trivial or false, and the formalization excludes them. Degree bounds are per term, on each $\phi_i h_i$ and each $\sigma_j g_j$ (including $\sigma_0$), never on the sum. $f_k$ is never a real sSup, which would be $0$ on an infeasible relaxation. CQC is linear independence of an indexed family, not of a set, so repeated gradients are dependent. The boundary hessian condition is not defined through the chart of the proof of Theorem 3.1. Finite convergence is $f_k = f_{\min}$, not $f - f_{\min} \in \langle h\rangle_{2k} + Q_k(g)$.

A complete development needs: truncated quadratic modules and their monotonicity; univariate SOS criteria; the Real Nullstellensatz; Marshall's representation theorem; and local parametrizations of real varieties at nonsingular points (Theorem 3.1). The definitions of the hierarchy and of the optimality conditions are reusable for any work on moment-SOS relaxations. Proofs of any milestone are welcome, as are proofs of the cited results under weaker hypotheses.

Selected references

• J. Nie, Optimality conditions and finite convergence of Lasserre's hierarchy, Math. Program. 146 (2014) 97–121; preprint arXiv:1206.0319v2 (2013). https://arxiv.org/abs/1206.0319
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM J. Optim. 11 (2001) 796–817. https://doi.org/10.1137/S1052623400366802
• M. Putinar, Positive polynomials on compact semi-algebraic sets, Indiana Univ. Math. J. 42 (1993) 969–984. https://doi.org/10.1512/iumj.1993.42.42045
• M. Marshall, Positive Polynomials and Sums of Squares, Mathematical Surveys and Monographs 146, AMS, 2008 (Theorem 9.5.3). https://doi.org/10.1090/surv/146
• M. Marshall, Representations of non-negative polynomials, degree bounds and applications to optimization, Canad. J. Math. 61 (2009) 205–221. https://doi.org/10.4153/CJM-2009-010-4
• J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Springer, 1998 (Corollary 4.1.8). https://doi.org/10.1007/978-3-662-03718-8

Why saddle points matter for stochastic gradient methods

Most training objectives in machine learning are smooth and nonconvex, and they are minimized by stochastic gradient descent (SGD) and its variants. For nonconvex $f$ the classical guarantee is convergence to an $\epsilon$-first-order stationary point, $\|\nabla f(x)\|\le\epsilon$: Ghadimi and Lan (arXiv:1309.5549) showed that SGD reaches one in $\tilde O(\epsilon^{-4})$ stochastic gradient queries, independently of the dimension. A first-order stationary point may be a saddle point, however, and for many problems (matrix sensing and completion, phase retrieval, tensor decomposition, dictionary learning) every second-order stationary point is a global minimum. For these problems, a guarantee for second-order stationary points is a guarantee of global optimality.

Timeline:

• 2015. Ge, Huang, Jin and Yuan (arXiv:1503.02101) proved that noisy SGD escapes strict saddle points in polynomial time, with a large polynomial dependence on $d$ and $1/\epsilon$.
• 2017. Jin, Ge, Netrapalli, Kakade and Jordan (arXiv:1703.00887) showed that gradient descent with occasional perturbations finds an $\epsilon$-second-order stationary point in $\tilde O(\ell\Delta_f/\epsilon^2)$ iterations, only polylogarithmically worse than plain gradient descent for first-order points.
• 2019. The paper of this mission, Jin, Netrapalli, Ge, Kakade and Jordan (arXiv:1902.04811; J. ACM 68(2), 2021), extends this to the stochastic setting with norm-subGaussian gradient noise: perturbed SGD needs $\tilde O(\epsilon^{-4})$ queries when the stochastic gradients are Lipschitz and $\tilde O(d\epsilon^{-4})$ in general.

Setting

Let $f:\mathbb R^d\to\mathbb R$ be bounded below with $f^\star=\inf f$, and write $\Delta_f=f(x_0)-f^\star$. 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^2 f(x_1)-\nabla^2 f(x_2)\|\le\rho\|x_1-x_2\|$ in operator norm. A point $x$ is an $\epsilon$-second-order stationary point if

$$\|\nabla f(x)\|\le\epsilon\qquad\text{and}\qquad\lambda_{\min}(\nabla^2 f(x))\ge-\sqrt{\rho\epsilon}.$$

The algorithm sees only a stochastic gradient $g(x;\theta)$ with $\theta\sim\mathcal D$. Assumption B asks that $\mathbb E\,g(x;\theta)=\nabla f(x)$ and that the error is norm-subGaussian: $\mathbb P(\|g(x;\theta)-\nabla f(x)\|\ge t)\le2e^{-t^2/(2\sigma^2)}$ for $t\ge0$. The optional Assumption C asks that each $g(\cdot;\theta)$ is $\tilde\ell$-Lipschitz. The two cases combine into

$$\mathfrak N=1+\min\Big\{\frac{\sigma^2}{\epsilon^2}+\frac{\tilde\ell^2}{\ell\sqrt{\rho\epsilon}},\ \frac{\sigma^2d}{\epsilon^2}\Big\},$$

with $\tilde\ell=+\infty$ when Assumption C is not used.

Perturbed SGD (PSGD, Algorithm 2) draws $\theta_t\sim\mathcal D$ and an independent Gaussian $\xi_t\sim\mathcal N(0,(r^2/d)I)$ at every step and updates

$$x_{t+1}=x_t-\eta\big(g(x_t;\theta_t)+\xi_t\big).$$

Formalization targets

Goal: Theorem 16

For a log factor $\iota$, the proof uses the parameters of Eq. (8): $\eta=1/(\iota^9\ell\mathfrak N)$, $r=\iota\epsilon\sqrt{\mathfrak N}$, $\mathscr T=\lceil\iota/(\eta\sqrt{\rho\epsilon})\rceil$, $\mathscr F=\iota^{-5}\sqrt{\epsilon^3/\rho}$, and runs for $T=\lceil100\max\{\Delta_f\mathscr T/\mathscr F,\Delta_f/(\eta\epsilon^2)\}\rceil=\tilde O(\ell\Delta_f\mathfrak N/\epsilon^2)$ iterations. The goal states that there is an absolute constant $\mu_0$ such that, for $\iota\ge\mu_0(1+\log Q)$ with $Q=d\,\mathfrak N\max\{1,\ell\Delta_f/\epsilon^2\}(\ell/\sqrt{\rho\epsilon})/\delta$,

$$\mathbb P\Big(\#\{t<T:\ x_t\ \text{is an }\epsilon\text{-second-order stationary point}\}\ge T/2\Big)\ge1-\delta.$$

Milestones

The proof's two engines, in the paper's order: the concentration inequalities for norm-subGaussian martingale differences (Lemmas 36–39), the descent lemma (Lemma 23), improve-or-localize (Lemma 24), the coupling analysis around a saddle point (Lemmas 27–31), escape from a saddle point (Lemma 25), and the two claims that bound the number of iterates with large gradient and the number near saddle points.

Significance

The theorem shows that adding isotropic Gaussian noise to SGD suffices to find second-order stationary points at essentially the cost SGD pays for first-order points: $\tilde O(\epsilon^{-4})$ queries when Assumption C holds (matching Ghadimi–Lan up to logarithms) and $\tilde O(d\epsilon^{-4})$ in general. Combined with landscape results such as "every second-order stationary point is a global minimum", it yields global convergence of a simple first-order stochastic method from arbitrary initialization for the problems listed above.

The result is proved on paper. As far as is known, none of it is machine-checked: neither the escape-from-saddle-point argument by coupling sequences nor the vector-valued concentration inequalities of Appendix C, whose proofs the paper defers to a separate technical note (arXiv:1902.03736). Formalizing them yields reusable norm-subGaussian martingale bounds in $\mathbb R^d$, a checked version of the coupling technique that later saddle-escape analyses reuse, and a check of every constant hidden in the paper's $\tilde O(\cdot)$.

Difficulty

The descent lemma alone cannot rule out that the iterates stall near a strict saddle point, where the gradient is small and the negative curvature is invisible to first-order information. The obvious argument, which says that the perturbation has a component along the negative eigendirection and that component grows, fails as stated: the stochastic gradient noise, the Hessian's variation along the trajectory, and the perturbation all interact over $\mathscr T$ steps. Controlling these interactions needs concentration bounds for vector-valued martingales whose scale is itself random (Lemma 37), which have no counterpart in Mathlib. Bounding how often the iterates can return to saddle regions over the whole run is a separate difficulty, since the times at which the iterates are near a saddle point are random.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with $d\ge1$; the Hessian is the derivative of the gradient map, and $\lambda_{\min}$ is the Rayleigh-quotient infimum over the unit sphere. The randomness is the infinite product measure of the pairs $(\theta_t,\xi_t)$, and the PSGD run is a deterministic function of it. Conventions committed to:

• Explicit constants in place of $\tilde O(\cdot)$. The paper writes $\eta=\tilde\Theta(1/(\ell\mathfrak N))$, $r=\tilde\Theta(\epsilon\sqrt{\mathfrak N})$ (Eq. (4)) and $\tilde O(\ell\Delta_f\mathfrak N/\epsilon^2)$; the statements use the proof's Eq. (8) and its $T$, with $\mathscr T$ and $T$ rounded up to integers. Every "absolute constant $c$" of a lemma is an existential quantified before the dimension, the oracle, the function and all parameters, so it cannot depend on them.
• Calibration of $\iota$. The printed $\iota=\mu\log(d\ell\Delta_f\mathfrak N/(\rho\epsilon\delta))$ is not invariant under rescaling $x\mapsto\lambda x$ and can be non-positive. The goal and the two claims assume $\iota\ge\mu_0(1+\log Q)$ with the scale-invariant $Q$ above.
• Hypotheses made explicit. $\rho>0$, $\epsilon>0$, $0<\delta<1$, $\sqrt{\rho\epsilon}\le\ell$ (the paper's footnote 1, p. 14), $\sigma>0$, joint measurability of $g$, and integrability of the stochastic gradients. Assumption B and Condition 35 hold for $t\ge0$, since the printed "$\forall t\in\mathbb R$" cannot be satisfied.
• Corrections. Lemma 29 requires $\eta\gamma>0$, Lemma 37 has failure probability $2d(\log(B/b)+1)e^{-\iota}$, and Lemma 25 is stated at $t_0=0$ from a deterministic saddle point, the case the paper proves.

A formalization that keeps the printed "$\forall t\in\mathbb R$" in Assumption B, or allows $\sigma=0$ in the tail bound, makes every statement vacuous or trivial; both are excluded. Infrastructure needed: norm-subGaussian vectors and their martingale concentration (reusable well beyond this mission), Gaussian anti-concentration in one direction, and stopping-time arguments for the Markov chain of PSGD. Contributions to any milestone, and to the concentration layer in particular, 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, P. Netrapalli, R. Ge, S. M. Kakade, M. I. Jordan, A Short Note on Concentration Inequalities for Random Vectors with SubGaussian Norm, arXiv:1902.03736, 2019. https://arxiv.org/abs/1902.03736
• 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
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM J. Optim. 23(4), 2013. https://arxiv.org/abs/1309.5549

Motivation

Adversarial training asks a classifier to work even after an input has been changed within a prescribed perturbation budget. Tsipras, Santurkar, Engstrom, Turner, and Mądry studied why the classifier that performs best on ordinary inputs can behave very differently under these changes. Their explicit model separates one reliably predictive feature from many individually weak features. It lets the same distribution support a highly accurate ordinary classifier and a less accurate but robust classifier Tsipras et al., §2.1–2.2. This mission formalizes the paper's comparison for soft-margin support vector machines at the population level.

The model is relevant to anyone using a training objective as a proxy for performance under perturbations. Its conclusion concerns the optimizer of an expected loss, not the effect of a particular finite sample or optimization algorithm. That distinction makes the example a direct statement about the objectives being optimized.

Setting

A label $y$ is drawn uniformly from $\{-1,+1\}$. An input $x$ has $d+1$ real coordinates. Its first coordinate, $x_1$, equals $y$ with probability $p$ and $-y$ with probability $1-p$, where $p\ge1/2$. Conditional on $y$, each of the remaining coordinates is an independent Gaussian variable with mean $\eta y$ and variance one, independently of $x_1$. Thus $x_1$ is a moderately reliable feature while the other coordinates can be weak predictors individually. These are exactly the ingredients of distribution $D$ in equation (3) Tsipras et al., p. 4.

For a weight vector $w$, the linear classifier $f_w$ assigns the sign of $w^\top x$. Its standard accuracy is the probability that $f_w(x)=y$ for a fresh pair $(x,y)$ from $D$. Its robust accuracy at radius $\varepsilon$ is the probability that this equality holds for every perturbation $\delta$ with $\|\delta\|_\infty\le\varepsilon$. Both accuracies average the two labels with probability $1/2$ each.

The soft-margin SVM objective combines expected hinge loss and quadratic regularization:

$$J_\lambda(w)=\mathbb E_D\!\left[\max\{0,1-yw^\top x\}\right] +\frac{\lambda}{2}\|w\|_2^2.$$

The distributional adversarial objective replaces the hinge loss for each observed pair by its maximum over the $\ell_\infty$ ball before taking the expectation:

$$J^{\mathrm{adv}}_{\varepsilon,\lambda}(w)= \mathbb E_D\!\left[ \max_{\|\delta\|_\infty\le\varepsilon} \max\{0,1-yw^\top(x+\delta)\}\right] +\frac{\lambda}{2}\|w\|_2^2.$$

This order follows equation (2), the distributional adversarial loss Tsipras et al., pp. 2, 16–18.

Formalization targets

The goal is Theorem 2.2 Tsipras et al., p. 6. Under $d\ge1$, $1/2\le p\le0.975$, and $\eta\ge4/\sqrt d$, a global minimizer $w^*$ of $J_\lambda$ whose squared Euclidean norm is one satisfies

$$\operatorname{StdAcc}(f_{w^*})>0.99, \qquad \operatorname{RobAcc}_{\varepsilon}(f_{w^*})<0.01 \quad\text{for every }\varepsilon\ge2\eta.$$

For a global minimizer of $J^{\mathrm{adv}}_{\varepsilon_{\mathrm{tr}},\lambda}$ with $\varepsilon_{\mathrm{tr}}\ge2\eta$ and either $\varepsilon_{\mathrm{tr}}<2p-1$ or $p=1/2$, the target is

$$\operatorname{StdAcc}(f_{w^*}) =\operatorname{RobAcc}_{\varepsilon}(f_{w^*})=p \quad\text{for every }0\le\varepsilon<1.$$

The milestone list follows Appendix D's stated claims: the Gaussian law of the pooled weak feature, Lemmas D.1–D.5, and the displayed adversarial objective identity. The lemmas give nonstrict $99\%$ and $1\%$ bounds where the theorem states strict inequalities Tsipras et al., pp. 16–18.

Significance

The result gives a concrete distribution on which the ordinary population hinge objective favors weak features enough to achieve near-perfect standard accuracy while remaining vulnerable to a small coordinatewise perturbation. The adversarial objective instead selects a classifier using the first feature, whose standard and robust accuracies are both $p$. It therefore distinguishes the behavior of the two objectives even without sampling error or a particular training algorithm.

The paper proves these claims informally. The Lean items here compile as definitions and theorem statements with open proofs; they are not yet machine-checked proofs. A completed development would supply the Gaussian probability estimates, optimizer properties, and accuracy calculations needed to close the statements. The law of a pooled Gaussian vector and the relation between $\ell_\infty$ perturbations and the $\ell_1$ weight norm are reusable beyond this example.

Difficulty

The first weak feature alone carries little information, but their normalized sum has a strong Gaussian signal. Consequently, reasoning about one coordinate at a time does not determine what the ordinary SVM minimizer predicts. The theorem also concerns every global minimizer with the stipulated norm, so testing a convenient weight vector does not settle it. The stated strict accuracy constants require quantitative Gaussian tails and an optimizer comparison at the specified $p$ and $\eta$ thresholds. In the adversarial part, the conclusion about accuracy $p$ requires more than proving that weak-feature weights vanish: the remaining first-feature coefficient must have the correct sign and be nonzero.

Formalization scope

Lean represents an input as a function on Fin (d+1); index zero is the paper's $x_1$, and index i.succ is $x_{i+2}$. The function norm is the sup norm, so $\|\delta\|\le\varepsilon$ is exactly the $\ell_\infty$ ball. Squared $\ell_2$ norm and $\ell_1$ norm of a weight vector are written as $\sum_iw_i^2$ and $\sum_i|w_i|$. The conditional law is a product of the two-point first-feature law and the independent Gaussian weak-feature law, assembled into one input vector. GaussianReal's variance argument is one. Labels and predictions are real $\pm1$, and a zero score is assigned $-1$. The tie has probability zero for the nondegenerate classifiers in the theorem.

The robust event can be outside the Borel sigma algebra. Its measure in Lean is an outer measure, agreeing with probability under completion. Gaussian affine hinge functions are integrable; the adversarial hinge has the explicit finite closed form supplied by a milestone when the radius is nonnegative. The supremum is over exactly the admissible perturbations. The mission does not reduce the target to a chosen classifier or assume any of the milestone conclusions as goal hypotheses.

Several hypotheses make implicit conditions or a necessary correction explicit. The condition $d\ge1$ prevents $4/\sqrt d$ from becoming Lean's default value at zero. Appendix D assumes that $\lambda>0$ has been tuned so an ordinary global minimizer has $\|w^*\|_2=1$; that is represented directly. Evaluation radii are nonnegative, so their balls are not empty. The upper bound $\varepsilon_{\mathrm{tr}}<2p-1$ is needed for the second claim: for larger training radii the zero vector may minimize the adversarial objective and its constant classifier has accuracy $1/2$, contrary to the printed sentence when $p>1/2$. At $p=1/2$ that constant classifier has accuracy $1/2=p$, so the case $p=1/2$ is kept for every training radius. This correction is disclosed rather than silently attributing it to the paper. Appendix D's displayed maximum outside expectation also differs from equation (2); the formalization follows (2), whose per-sample maximum has the displayed closed form. The paper's proof specializes to $\eta=4/\sqrt d$ although Theorem 2.2 states $\eta\ge4/\sqrt d$; the target retains the printed theorem's range.

Selected references

• Dimitris Tsipras, Shibani Santurkar, Logan Engstrom, Alexander Turner, and Aleksander Mądry, Robustness May Be at Odds with Accuracy, International Conference on Learning Representations, 2019. arXiv:1805.12152v5.