All missions

Why the worst case matters

Distributionally robust optimization (DRO) replaces the expected loss $E_{P_0}[\ell(\beta^{\mathsf T}X)]$ of a linear decision rule $\beta$ by its worst case over all data laws $P$ within transport distance $\delta$ of the baseline $P_0$. When $P_0$ is an empirical distribution this covers regularized regression and classification (Blanchet, Kang, Murthy 2019; Esfahani, Kuhn 2018). The optimal value is one number; a practitioner also wants to know which distribution realizes it, the adversary's best response. It shows which data points the robust model guards against, it gives stress-test scenarios, and its structure is what the paper's comparative statics (Theorem 7) and iterative schemes build on.

J. Blanchet, K. Murthy and F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes (arXiv:1810.02403v3; Math. Oper. Res. 47(2), 2022), answer this for a state-dependent Mahalanobis cost. Theorem 6 of that paper describes the worst-case distribution through the solution of the one-dimensional dual problem. This mission formalizes Theorem 6.

Setting

The data $X$ take values in $\mathbb R^d$ with law $P_0$, a Borel probability measure. The decision $\beta$ ranges over a convex set $B\subseteq\mathbb R^d$ (a standing assumption of the paper). Moving mass from $x$ to $x'$ costs

$$c(x,x')=(x-x')^{\mathsf T}A(x)(x-x'),$$

where $A(x)$ is positive definite. Assumption 1 asks that $c$ be lower semicontinuous and that $\rho_{\min}\|v\|^2\le v^{\mathsf T}A(x)v\le\rho_{\max}\|v\|^2$ for $P_0$-almost every $x$, with $\rho_{\min}>0$. The optimal transport cost $D_c(P_0,P)$ is the least value of $E_\pi[c(X,X')]$ over couplings $\pi$ of $P_0$ and $P$. For $\delta>0$ the worst-case objective is

$$\sup_{P:\,D_c(P_0,P)\le\delta}E_P\bigl[\ell(\beta^{\mathsf T}X)\bigr].\tag{6}$$

Assumption 2 asks that the loss $\ell:\mathbb R\to\mathbb R$ be convex, that the growth exponent $\kappa=\inf\{s\ge0:\sup_u(\ell(u)-su^2)<\infty\}$ be finite, and that $E_{P_0}\|X\|^4<\infty$.

The dual side is built from

$$F(\gamma,\beta,\lambda;x)=\ell\bigl(\beta^{\mathsf T}x+\gamma\sqrt\delta\,\beta^{\mathsf T}A(x)^{-1}\beta\bigr)-\lambda\sqrt\delta\bigl(\gamma^2\beta^{\mathsf T}A(x)^{-1}\beta-1\bigr),$$

the robust loss $\ell_{\rm rob}(\beta,\lambda;x)=\sup_{\gamma}F$, the dual objective $f_\delta(\beta,\lambda)=E_{P_0}[\ell_{\rm rob}(\beta,\lambda;X)]\in\mathbb R\cup\{\infty\}$ and the maximizer set $\Gamma^*(\beta,\lambda;x)=\arg\max_\gamma F(\gamma,\beta,\lambda;x)$. By the paper's Theorem 1, (6) equals $\inf_{\lambda\ge0}f_\delta(\beta,\lambda)$, and a minimizer $\lambda_*(\beta)$, the dual optimizer, exists. The threshold is $\lambda_{thr}(\beta)=\kappa\sqrt\delta\,\mathrm{ess\,sup}_{P_0}\,\beta^{\mathsf T}A(X)^{-1}\beta$; below it $f_\delta=\infty$.

Formalization targets

Goal: Theorem 6(c)

Let $\beta\ne0$ and $\lambda_*(\beta)>\lambda_{thr}(\beta)$. Let $G_\pm(x)\in\Gamma^*(\beta,\lambda_*(\beta);x)$ be measurable selections with the largest and smallest square, $\bar c=E[G_+^2\beta^{\mathsf T}A(X)^{-1}\beta]$, $\underline c=E[G_-^2\beta^{\mathsf T}A(X)^{-1}\beta]$, and let $Z\sim\mathrm{Bernoulli}(q)$ be independent of $X$ with $q=(\bar c-1)/(\bar c-\underline c)\in[0,1]$. Then

$$X^*=X+\sqrt\delta\,\bigl(ZG_-+(1-Z)G_+\bigr)A(X)^{-1}\beta,\qquad E[c(X,X^*)]=\delta,$$

and the law of $X^*$ attains the supremum in (6).

Milestones

• Lemma 1: $\Gamma^*\ne\emptyset$ and $\ell_{\rm rob}<\infty$ when $\lambda>\kappa\sqrt\delta\,\beta^{\mathsf T}A(x)^{-1}\beta$, and $\ell_{\rm rob}=\infty$ below that; hence $\{\lambda>\lambda_{thr}\}\subseteq\{f_\delta<\infty\}\subseteq\{\lambda\ge\lambda_{thr}\}$.
• Lemma 3(a): $\sqrt\delta|g|\beta^{\mathsf T}A(x)^{-1}\beta\le1+C_1\varepsilon^{-1}(1+|\beta^{\mathsf T}x|)$ for $g\in\Gamma^*$ once $\lambda\ge(\kappa+\varepsilon)\sqrt\delta\beta^{\mathsf T}A(x)^{-1}\beta$.
• Proposition 2 (a) and its $\lambda$-part: the one-sided $\lambda$-derivatives of $\ell_{\rm rob}$ are the minimum and the maximum of $-\sqrt\delta(\gamma^2\beta^{\mathsf T}A(x)^{-1}\beta-1)$ over $\Gamma^*$.
• The one-sided $\lambda$-derivatives of $f_\delta$ on $\{\lambda>\lambda_{thr}\}$:

$$\partial_\pm f_\delta/\partial\lambda=\sqrt\delta\bigl(1-E[\beta^{\mathsf T}A(X)^{-1}\beta\,\inf/\sup_{g\in\Gamma^*}g^2]\bigr).$$

• [Blanchet–Murthy 2019, Theorem 1]: strong duality and complementary slackness (already proved on the platform).

Companion statements

Theorem 6(a): $\lambda_*>0$ unless $\ell$ is constant. Theorem 6(b): $\lambda_*\ge\lambda_{thr}$. Theorem 6(d), as the paper's example: for $\ell(u)=u^2-|u|(1-e^{-|u|})$, $P_0=\delta_0$, $A=I$ and $\|\beta\|=1$, $\lambda_*=\lambda_{thr}=\sqrt\delta$ and no distribution attains the value $\delta$. Theorem 6(e), with Lemma 8: if $\ell''\le M$ and $\lambda_*>\tfrac12M\sqrt\delta\,\mathrm{ess\,sup}\,\beta^{\mathsf T}A(X)^{-1}\beta$, then $\Gamma^*$ is a singleton $\{G(x)\}$ almost surely and the law of $X+\sqrt\delta G(X)A(X)^{-1}\beta$ is the unique worst case.

Significance

The result reduces a search over all probability measures to a scalar problem per data point. Each point is pushed along the single direction $A(x)^{-1}\beta$, by an amount read off the maximizers of $F$, and the budget $\delta$ is always spent completely. When the maximizer is not unique, randomization between two extreme maximizers is needed and suffices. Part (d) shows that the threshold condition cannot be removed, and part (e) gives a deterministic transport map (a Monge solution) under smoothness. Theorem 7 of the paper, the monotone growth of worst-case displacements in $\delta$, is a statement about the random variable $G$ produced here.

None of these statements has been machine-checked before. The general strong duality with complementary slackness of Blanchet–Murthy (arXiv:1604.01446) is proved on the platform, so this mission connects that abstract theorem to an explicit worst-case law. A formal proof also has to settle one point the printed text leaves loose: which extreme maximizers enter the mixture (see Formalization scope).

Difficulty

The first idea is to take the pointwise maximizers of $F$ at $\lambda_*$ and push $P_0$ forward. That works only when the maximizer is unique and the budget constraint happens to be tight. In general the maximizer set is not a singleton, and the derivative of $f_\delta$ at $\lambda_*$ only lies between a left and a right derivative. Turning the first-order condition $\partial_+f_\delta\ge0\ge\partial_-f_\delta$ into an exact cost $\delta$ needs three things. The one-sided derivatives must be identified as expectations over $\Gamma^*$, an envelope theorem under an integral with a non-compact parameter set. The extreme maximizers must be compact and measurably selectable. Finally the resulting coupling must be certified optimal through complementary slackness. Each step needs a hypothesis that is easy to lose: the growth control of Lemma 3, the essential supremum in $\lambda_{thr}$, measurability of selections.

Formalization scope

Points of $\mathbb R^d$ are EuclideanSpace ℝ (Fin d), $\beta^{\mathsf T}x$ is the inner product, and $\beta^{\mathsf T}A(x)^{-1}\beta$ is quadInv A β x. $\ell_{\rm rob}$ and $f_\delta$ are extended-real valued; $f_\delta$ uses the published extended integral ModelRiskOT.Duality.extIntegral. The worst-case objective (6) is the published primal problem primalValue: a supremum over couplings $\pi$ with first marginal $P_0$ and $\int c\,d\pi\le\delta$ (primalFeasible). A distribution attains (6) when a coupling with that second marginal has value primalValue. The random worst case $X^*$ is encoded by the joint law of $(X,X^*)$, a mixture of two graph couplings, because $E[c(X,X^*)]$ depends on the pair. A dual optimizer is a real $\lambda_*\ge0$ minimizing $f_\delta(\beta,\cdot)$ on $[0,\infty)$.

Standing hypotheses on every statement: $P_0$ a probability measure, Assumptions 1 and 2, $\delta>0$, $B$ convex. The following departures from the printed text are disclosed in each item:

• In (c), $G_\pm$ are the selections of extreme square used in the proof (p. 40), not $\inf\Gamma^*$ and $\sup\Gamma^*$ as printed; a two-point example shows the printed choice can fail.
• In (e), "for every $x$" is read as "for $P_0$-almost every $x$", which is what the proof gives.
• Lemma 8 is stated for $\beta\ne0$.
• Proposition 2 is formalized for part (a) and the $\lambda$-derivatives only.

Every expectation used in the goal ($\bar c$, $\underline c$) carries an integrability conjunct. The cost identity and optimality are asserted for the measure itself, so no junk value of a non-integrable integral can make the goal hold vacuously. A statement asserting only first-order conditions for $\lambda_*$ would not be Theorem 6. The goal asserts primal attainment and the exact cost.

Needed infrastructure, reusable beyond this mission: envelope (Danskin) theorems for one-sided derivatives of suprema, differentiation of convex integral functionals, measurable selection of argmax sets, and complementary slackness through the published Blanchet–Murthy theorem. Contributions of any of these as standalone lemmas are welcome.

Selected references

• J. Blanchet, K. Murthy, F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Math. Oper. Res. 47(2), 2022. arXiv:1810.02403v3, doi:10.1287/moor.2021.1178
• J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2), 2019. arXiv:1604.01446
• J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, J. Appl. Probab. 56(3), 2019. doi:10.1017/jpr.2019.49
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171, 2018. doi:10.1007/s10107-017-1172-1
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (Proposition 7.50, measurable selection).

Motivation

The alternating direction method of multipliers (ADMM) solves linearly constrained problems whose objective splits into separately treatable blocks. For two blocks, $\min\{\theta_1(x_1)+\theta_2(x_2) : A_1x_1+A_2x_2=b\}$, it alternates one minimisation of the augmented Lagrangian in each block with a multiplier update. Its convergence for closed convex $\theta_1,\theta_2$ has been known since the work of Glowinski–Marrocco (1975) and Gabay–Mercier (1976), and the survey of Boyd, Parikh, Chu, Peleato and Eckstein (2011) made it a standard tool in statistics, imaging and machine learning.

Many applications have three or more blocks: robust principal component analysis with noisy and incomplete data, latent-variable graphical model selection, image alignment. Practitioners therefore apply the direct extension of ADMM, which simply cycles through all blocks in Gauss–Seidel order before updating the multiplier. Whether this extension converges for convex problems remained open for years: convergence was known under extra assumptions (strong convexity with a restricted penalty, Han–Yuan 2012; orthogonality of coefficient matrices, Section 2 of the source paper), and modified schemes with correction steps were proposed precisely because no proof was available.

Chen, He, Ye and Yuan (Math. Program., 2014) settled the question negatively by an explicit three-block example. This mission formalizes that example and the paper's main theorem.

Setting

Problem (1.1). Given $A_i\in\mathbb R^{p\times n_i}$, $b\in\mathbb R^p$, closed convex sets $\mathcal X_i\subseteq\mathbb R^{n_i}$ and convex functions $\theta_i:\mathbb R^{n_i}\to\mathbb R$ $(i=1,2,3)$, with a nonempty solution set,

$$\min\ \theta_1(x_1)+\theta_2(x_2)+\theta_3(x_3)\quad\text{s.t.}\quad A_1x_1+A_2x_2+A_3x_3=b,\ x_i\in\mathcal X_i .$$

Augmented Lagrangian (1.6). For a penalty $\beta>0$ and multiplier $\lambda\in\mathbb R^p$,

$$\mathcal L_{\mathcal A}(x_1,x_2,x_3,\lambda)=\sum_{i=1}^3\theta_i(x_i)-\lambda^T(A_1x_1+A_2x_2+A_3x_3-b)+\tfrac{\beta}{2}\|A_1x_1+A_2x_2+A_3x_3-b\|^2 .$$

Direct extension of ADMM (1.5). From $(x_2^k,x_3^k,\lambda^k)$: $x_1^{k+1}$ minimises $\mathcal L_{\mathcal A}(\cdot,x_2^k,x_3^k,\lambda^k)$ over $\mathcal X_1$; $x_2^{k+1}$ minimises $\mathcal L_{\mathcal A}(x_1^{k+1},\cdot,x_3^k,\lambda^k)$ over $\mathcal X_2$; $x_3^{k+1}$ minimises $\mathcal L_{\mathcal A}(x_1^{k+1},x_2^{k+1},\cdot,\lambda^k)$ over $\mathcal X_3$; and $\lambda^{k+1}=\lambda^k-\beta(A_1x_1^{k+1}+A_2x_2^{k+1}+A_3x_3^{k+1}-b)$. A sequence satisfying these four conditions for every $k$ is a run (IsRun15).

The example. System (3.1) is $A_1x_1+A_2x_2+A_3x_3=0$ with columns $A_i\in\mathbb R^3$, scalar unknowns, zero objective, $b=0$ and $\mathcal X_i=\mathbb R$; its unique solution is $x=0$ when $[A_1,A_2,A_3]$ is nonsingular. The paper takes

$$A=(A_1,A_2,A_3)=\begin{pmatrix}1&1&1\\1&1&2\\1&2&2\end{pmatrix}\qquad(3.10),$$

the instance example310. With the scaled multiplier $\mu=\lambda/\beta$, the state is $z=(x_2,x_3,\mu_1,\mu_2,\mu_3)\in\mathbb R^5$ (stateVec). The $5\times5$ matrices $L$ (3.6) and $R$ (3.7) are built from the inner products $A_i^TA_j$ and the columns, and $M=L^{-1}R$ (3.9).

Formalization targets

Goal: Theorem 3.1

For the instance (3.10), which satisfies the standing assumptions of (1.1), there are a three-dimensional subspace $S\subseteq\mathbb R^5$ and a nonzero linear functional $\varphi$ on $S$ such that for every $\beta>0$ and every starting point with

$$\bigl(x_2^0,\,x_3^0,\,\lambda^0/\beta\bigr)\in S,\qquad \varphi\bigl(x_2^0,x_3^0,\lambda^0/\beta\bigr)>0,$$

a run of (1.5) from $(x_2^0,x_3^0,\lambda^0)$ exists and no such run converges.

Milestones

1. (3.4)–(3.5): on (3.1), every run satisfies $x_1^{k+1}=\frac{1}{A_1^TA_1}(-A_1^TA_2x_2^k-A_1^TA_3x_3^k+A_1^T\mu^k)$ and $Lz^{k+1}=Rz^k$, with $L,R$ independent of $\beta$.
2. (3.8)–(3.9): $z^k=M^kz^0$.
3. $L$, $R$, $M$ for (3.10): the printed $5\times5$ matrices, $\det L=54$ and $M=L^{-1}R$.
4. $\rho(M)=|d_1|=|d_2|>1$: $M$ has a non-real eigenvalue of maximal modulus, and that modulus exceeds $1$.
5. (3.12)–(3.13): a three-dimensional real subspace and a nonzero functional $\varphi$ on it such that $\|M^kz\|\to\infty$ whenever $\varphi(z)\neq0$.

Significance

The theorem shows that convexity alone does not make the cyclic three-block ADMM convergent, and the failure is robust: it holds for every penalty parameter and for an open half of a three-dimensional subspace of starting points, on a problem as simple as a nonsingular homogeneous linear system with zero objective. It explains why later convergent variants add assumptions (strong convexity, orthogonality, small step sizes, randomised block order) or modify the scheme, and it is the standard reference for that fact in the operator-splitting literature.

The result is proved in the paper; no machine-checked version is known. A formal version produces a certified negative example for the most widely used multi-block splitting heuristic, a reusable formal model of the extended ADMM (Problem, augLag, IsRun15) on which convergent variants can later be stated, and a worked instance of turning a numerically presented spectral argument (the paper prints its eigen-decomposition to four digits) into exact statements.

Difficulty

The first step, that the iteration on (3.1) is linear in $(x_2,x_3,\mu)$ and independent of $\beta$, is elementary but requires extracting minimisers of convex quadratics from the minimiser conditions of the run. The main difficulty is exact spectral information about a specific $5\times5$ rational matrix whose characteristic polynomial is $x$ times an irreducible quartic over $\mathbb Q$ with two pairs of complex roots of moduli about $1.0278$ and $0.9044$. The paper's evidence is a floating-point eigen-decomposition; a proof must instead locate the roots exactly, for example by certified bounds, and must show that the divergent component is present for a whole real subspace of starting points rather than for one numerically chosen vector. Finally, unboundedness of the scaled state has to be transferred back to the original sequence $(x_1^k,x_2^k,x_3^k,\lambda^k)$ for every $\beta>0$.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin p) (Fin n) ℝ, and $\|r\|^2$ in (1.6) is the dot product $r\cdot r$. Each $\theta_i$ is real-valued and convex on all of $\mathbb R^{n_i}$; "closed" is automatic for such functions and is not stated separately. "Argmin" is read as "a minimiser": the run predicate does not select a minimiser, and the goal asserts that a run exists, so the non-convergence claim is not vacuous. The paper's blocks and multiplier components are 1-based, the Lean components 0-based. Convergence of the sequence is convergence of $(x_1^k,x_2^k,x_3^k,\lambda^k)$ in the product topology; $x_1^0$ is never read by (1.5). "Divergent" means "not convergent". The "continuously dense half space of dimension 3" is $\{z\in S:\varphi(z)>0\}$ for a three-dimensional subspace $S$ and nonzero linear $\varphi$, expressed in the coordinates $(x_2^0,x_3^0,\lambda^0/\beta)$; $S$ and $\varphi$ are chosen before $\beta$, as in the paper. Requiring $\dim S=3$ and $\varphi\neq0$ rules out the trivial choices $S=\{0\}$ or $\varphi=0$. Eigenvalues are complex roots of the characteristic polynomial; a statement using only real eigenvalues would be wrong, since the only real eigenvalue of $M$ is $0$. Norms enter only through "$\to\infty$", where the choice of norm on $\mathbb R^5$ is irrelevant. The rounded numbers of (3.11) are not used anywhere.

Every object is defined in ExtADMM.Diverge.Setting. The general definitions (problem, augmented Lagrangian, run) are written for arbitrary dimensions and are intended for reuse by later missions on multi-block splitting. Contributions welcome: proofs of the milestones, exact root localisation for the quartic factor of the characteristic polynomial, and general lemmas such as "a real matrix with an eigenvalue of modulus above one has unbounded orbits on a real subspace".

Selected references

• C. Chen, B. He, Y. Ye, X. Yuan, The direct extension of ADMM for multi-block convex minimization problems is not necessarily convergent, Mathematical Programming 155 (2016) 57–79. https://doi.org/10.1007/s10107-014-0826-5
• D. Gabay, B. Mercier, A dual algorithm for the solution of nonlinear variational problems via finite element approximation, Computers & Mathematics with Applications 2 (1976) 17–40. https://doi.org/10.1016/0898-1221(76)90003-1
• R. Glowinski, A. Marrocco, Sur l'approximation, par éléments finis d'ordre un, et la résolution, par pénalisation-dualité, d'une classe de problèmes de Dirichlet non linéaires, RAIRO Analyse Numérique 9 (1975) 41–76. https://doi.org/10.1051/m2an/197509R200411
• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed optimization and statistical learning via the alternating direction method of multipliers, Foundations and Trends in Machine Learning 3 (2011) 1–122. https://doi.org/10.1561/2200000016
• D. Han, X. Yuan, A note on the alternating direction method of multipliers, Journal of Optimization Theory and Applications 155 (2012) 227–238. https://doi.org/10.1007/s10957-012-0003-z

Motivation

Deciding whether a planar graph is 3-colorable is NP-complete, so a large part of the theory of planar graph coloring looks for simple local conditions that guarantee 3-colorability. Grötzsch's theorem (1959) is the model result: every triangle-free planar graph is 3-colorable. Forbidding triangles is not the only possibility, and in 1976 Richard Steinberg asked whether forbidding cycles of two other lengths suffices.

Steinberg's Conjecture (1976). Every planar graph with no cycles of length four or five is 3-colorable.

The conjecture drove four decades of work on planar coloring. It was surveyed by Borodin as one of the central problems of the area (Borodin 2013, §7), and it was one of the six graph theory problems ranked with the highest importance in the Open Problem Garden.

Timeline:

• 1976. Steinberg poses the conjecture (Steinberg 1993 records its history).
• 1991. Erdős suggests the relaxation: find the smallest $k$ such that every planar graph with no cycles of lengths $4, \dots, k$ is 3-colorable. Abbott and Zhou show $k \le 11$ (Ars Combin. 32, 1991).
• 1995. Sanders and Zhao improve this to $k \le 9$ (Graphs Combin. 11, 1995).
• 2005. Borodin, Glebov, Raspaud and Salavatipour prove $k \le 7$: planar graphs without cycles of lengths 4 to 7 are 3-colorable (JCTB 93).
• 2007. Voigt shows that the list-coloring analogue fails: there is a planar graph without 4- and 5-cycles that is not 3-choosable (Discrete Math. 307, 2007).
• 2016. Cohen-Addad, Hebdige, Král', Li and Salgado construct a counterexample, so the conjecture is false (arXiv:1604.05108; J. Combin. Theory Ser. B, 2017).

Setting

All graphs are finite and simple. A cycle of length $k$ in a graph $H$ is a sequence of $k \ge 3$ pairwise distinct vertices $v_0, \dots, v_{k-1}$ with $v_i v_{i+1}$ an edge for each $i$ (indices mod $k$). $H$ has no cycles of length four or five if no cycle of $H$ has length $4$ or $5$; triangles and cycles of length at least six are allowed. A 3-coloring of $H$ assigns one of three colors to each vertex so that adjacent vertices get different colors, and $H$ is 3-colorable if it has one. The distance $d_H(u,v)$ is the number of edges of a shortest $u$–$v$ path. $H$ is planar if it can be drawn in the plane without crossing edges.

The paper builds its counterexample in three steps, from three concrete graphs given as drawings.

1. $G_1$ (Figure 1) has 15 vertices $a, \dots, o$ and 23 edges. Its contact vertices are $a$, $b$, $c$.
2. $G_2$ (Figure 2) consists of three copies of $G_1$ glued along contact vertices around a central triangle $def$. It has 42 vertices and 72 edges, and its contact vertices are $a$, $b$, $c$.
3. $G$ (Figure 3) consists of four copies of $G_2$ glued at a central vertex $a$, together with the extra vertices $b$, $e$, $e'$ and twelve extra edges. It has 166 vertices and 300 edges.

In the Lean development these are the definitions G1, G2 and G. The hypothesis "no cycles of length four or five" is the definition NoFourFiveCycle.

Formalization targets

Goal: Theorem 3 (p. 4)

$$\exists\, H \text{ finite, planar}:\quad H \text{ has no cycle of length } 4 \text{ or } 5 \ \text{ and } \ H \text{ is not 3-colorable}.$$

This is the paper's main theorem and exactly the negation of Steinberg's Conjecture. It leaves the witness free, so any counterexample proves it.

Milestones

1. Lemma 1 (p. 2): $G_1$ has no 4- or 5-cycle; no 3-coloring gives $a, b, c$ the same color; and $d(a,b) = d(a,c) = 3$, $d(b,c) = 4$.
2. Lemma 2 (p. 3): $G_2$ has no 4- or 5-cycle; no 3-coloring gives $a, b, c$ the same color; and the contacts are pairwise at distance $4$.
3. $G$ has no cycle of length four or five (proof of Theorem 3, p. 5).
4. $G$ has no 3-coloring (proof of Theorem 3, p. 5).
5. $G$ is planar (§2, p. 2, and Figure 3).
6. $G_1$ and $G_2$ are planar (§2, p. 2, and Figures 1–2).

Milestones 3–5 together give the goal, with $G$ as the witness.

Significance

The result. Theorem 3 settles a 40-year-old problem negatively. It shows that forbidding 4- and 5-cycles is not a local condition that forces 3-colorability, which redirects the Erdős relaxation: the threshold $k$ for "no cycles of lengths $4, \dots, k$" lies in $\{6, 7\}$, since $k \le 7$ is known and $k = 5$ is now excluded. The paper notes that the same graph also disproves the Strong Bordeaux Conjecture and the Novosibirsk 3-Color Conjecture.

Formalizing it. The theorem is proved, and the proof is short. As far as is known it has no machine-checked version. Every claim in the proof is a finite statement about explicit graphs, so the work here is to verify the three gadgets and the gluing arguments in Lean, including planarity of an explicit 166-vertex graph, which is asserted in the paper only through its figures. Planarity, cycle structure and coloring of a concrete graph of this size are a useful benchmark for computational verification in Lean.

Difficulty

The obvious approach is brute force: $G$ is a fixed finite graph, so in principle each claim can be decided. In practice decide is not workable at this size. Excluding 4- and 5-cycles means quantifying over walks of a 166-vertex graph. Non-3-colorability is a search over $3^{166}$ assignments unless it is reduced, as the paper does, through the gadget lemmas. The planarity witness needs explicit coordinates for 166 points and a check of all $\binom{300}{2}$ pairs of segments, in exact arithmetic. The gluing arguments ("a cycle through two copies has length at least six") are where the paper's distance claims are used. Turning those claims into statements about Mathlib walks on unions of embedded copies is the conceptual work.

Formalization scope

Lean representation and conventions:

• Graphs are Mathlib SimpleGraphs. G1 lives on Fin 15, with $a, \dots, o \mapsto 0, \dots, 14$. G2 lives on Fin 42, with $a, b, c, d, e, f \mapsto 0, \dots, 5$, and G lives on Fin 166, with $a, b, c, c', e, e', d, f, d', f' \mapsto 0, \dots, 9$.
• Copies. G2 is literally (⨆ k, G1.map (copy2 k)) ⊔ the triangle $def$, with explicit embeddings copy2 k : Fin 15 ↪ Fin 42. G is (⨆ k, G2.map (copyG k)) ⊔ the twelve extra edges, with copyG k : Fin 42 ↪ Fin 166. The contact tables are in each definition's statement. A local check confirms the edge counts 23, 72 and 300, and that G agrees edge for edge with an independent transcription of Figure 3.
• Cycles are Mathlib walks p : H.Walk v v with p.IsCycle, and their length is p.length.
• 3-colorings are H.Coloring (Fin 3), and 3-colorability is H.Colorable 3. "No 3-coloring gives $a, b, c$ one color" is ∀ C, ¬ (C a = C b ∧ C b = C c). Colorings in which two of the three share a color are still allowed, as in the paper.
• Distance is SimpleGraph.dist. Its junk value $0$ for unreachable pairs is never hit, because every asserted distance is positive.
• Planarity is the published straight-line predicate OPG37357.IsPlanar: an injective placement of the vertices in $\mathbb R^2$ in which no vertex lies inside an edge segment and edges with four distinct endpoints have disjoint segments. For finite simple graphs it is equivalent to planarity by Fáry's theorem, and it implies topological planarity.
• The goal's witness is a graph on Fin n. This loses no generality for finite graphs, and the empty graph cannot serve as a trivial witness because it is 3-colorable.

The following trivializing formalizations are ruled out. Closed walks, instead of cycles, would exclude every graph with an edge. Girth is not used: $G$ contains triangles. Lemmas 1 and 2 do not assert that $a$ and $b$ get different colors, which would be false for $G_1$. An infinite or unspecified vertex type is not allowed for the witness.

Welcome contributions: decision procedures or certificates for short cycles and colorings of explicit finite graphs; a straight-line embedding of $G$ with rational coordinates; lemmas on cycles and distances in graphs glued from embedded copies, which are reusable for other gadget constructions; and proofs of Lemmas 1–2 by computation or by the paper's arguments.

Selected references

• V. Cohen-Addad, M. Hebdige, D. Král', Z. Li, E. Salgado, Steinberg's Conjecture is false, J. Combin. Theory Ser. B 122 (2017), 452–456; preprint arXiv:1604.05108v2. https://arxiv.org/abs/1604.05108v2
• O. V. Borodin, Colorings of plane graphs: A survey, Discrete Math. 313 (2013), 517–539. https://doi.org/10.1016/j.disc.2012.11.011
• O. V. Borodin, A. N. Glebov, A. Raspaud, M. R. Salavatipour, Planar graphs without cycles of length from 4 to 7 are 3-colorable, J. Combin. Theory Ser. B 93 (2005), 303–331. https://doi.org/10.1016/j.jctb.2004.11.001
• D. P. Sanders, Y. Zhao, A note on the three color problem, Graphs Combin. 11 (1995), 91–94. (Reference [11] of arXiv:1604.05108v2.)
• R. Steinberg, The state of the three color problem, in: Quo Vadis, Graph Theory?, Ann. Discrete Math. 55 (1993), 211–248. (Reference [12] of arXiv:1604.05108v2.)
• M. Voigt, A non-3-choosable planar graph without cycles of length 4 and 5, Discrete Math. 307 (2007), 1013–1015. (Reference [13] of arXiv:1604.05108v2.)

Motivation

A decision maker wants to choose $x$ in a compact set $X\subseteq\mathbb R^n$ to minimize an expected cost $c(x,\mathbb P^\star)=\mathbb E_{\mathbb P^\star}[\gamma(x,\xi)]$, but the distribution $\mathbb P^\star$ of $\xi$ is unknown; only independent samples $\xi_1,\dots,\xi_T$ are available. The standard remedy, minimizing the cost under the empirical distribution, is known to produce decisions whose realized cost exceeds the in-sample estimate: the "optimizer's curse" of decision analysis (Smith and Winkler, 2006) and overfitting in statistics. Distributionally robust optimization (DRO) replaces the empirical distribution by a worst case over a set of nearby distributions. Many such sets have been proposed, and the question of which one is best has no answer unless "best" is made precise.

Van Parys, Mohajerin Esfahani and Kuhn (arXiv:1704.04118v3, published in Management Science 67(6), 2021) give such a precise meaning. They ask for the least conservative data-driven decision rule whose out-of-sample disappointment decays exponentially at a prescribed rate $r$ under every possible data-generating distribution, and they prove that DRO over a relative-entropy ball of radius $r$ is that rule. This mission formalizes the prescription half of the result (Theorem 7 of the paper), in which decisions, not only cost estimates, are optimized. The prediction half (Theorem 4) is the subject of mission 1 of this series, and the extension to continuous state spaces (Theorem 10) is mission 3. All page and result numbers below refer to the arXiv version v3 (22 Dec 2019).

Setting

The random parameter takes values in a finite set $\Xi=\{1,\dots,d\}$. The model class is the probability simplex $\mathcal P=\{\mathbb P\in\mathbb R^d_+:\sum_i\mathbb P(i)=1\}$ with the topology inherited from $\mathbb R^d$. The cost $\gamma(x,i)$ is continuous in $x$ for each $i$, and $c(x,\mathbb P)=\sum_i\mathbb P(i)\gamma(x,i)$. From a sample path the decision maker forms the empirical distribution $\hat{\mathbb P}_T(i)=\frac1T\sum_{t=1}^T\mathbb 1_{\xi_t=i}$. When the samples are drawn independently from $\mathbb P$, the probability of an event about $\hat{\mathbb P}_T$ is written $\mathbb P^\infty(\cdot)$.

A data-driven predictor is a continuous function $\hat c:X\times\mathcal P\to\mathbb R$; $\hat c(x,\hat{\mathbb P}_T)$ estimates $c(x,\mathbb P^\star)$. A function $f:\mathcal P\to X$ is quasi-continuous if for every $\mathbb P$, every $\epsilon>0$ and every neighbourhood $U$ of $\mathbb P$ there is a non-empty open $V\subseteq U$ on which $\|f(\mathbb P)-f(\mathbb Q)\|\le\epsilon$ (the set $V$ need not contain $\mathbb P$). A data-driven prescriptor induced by $\hat c$ is a quasi-continuous $\hat x:\mathcal P\to X$ with $\hat x(\mathbb P')\in\arg\min_{x\in X}\hat c(x,\mathbb P')$ for every $\mathbb P'$. The family $\mathcal X$ consists of all such pairs $(\hat c,\hat x)$.

The prescription disappointment of a pair under a model $\mathbb P$ is

$$\mathbb P^\infty\big(c(\hat x(\hat{\mathbb P}_T),\mathbb P)>\hat c(\hat x(\hat{\mathbb P}_T),\hat{\mathbb P}_T)\big),$$

the probability that the true cost of the prescribed decision exceeds its in-sample estimate. Pairs are ordered by their in-sample optimal values: $(\hat c_1,\hat x_1)\preceq_{\mathcal X}(\hat c_2,\hat x_2)$ iff $\hat c_1(\hat x_1(\mathbb P'),\mathbb P')\le\hat c_2(\hat x_2(\mathbb P'),\mathbb P')$ for all $\mathbb P'$. Problem (6) of the paper is the vector optimization problem

$$\min_{(\hat c,\hat x)\in\mathcal X}{}^{\preceq_{\mathcal X}}\ (\hat c,\hat x)\quad\text{s.t.}\quad\limsup_{T\to\infty}\frac1T\log\mathbb P^\infty\big(c(\hat x(\hat{\mathbb P}_T),\mathbb P)>\hat c(\hat x(\hat{\mathbb P}_T),\hat{\mathbb P}_T)\big)\le-r\quad\forall\,\mathbb P\in\mathcal P,$$

and a pair is strongly optimal if it is feasible and $\preceq_{\mathcal X}$ every feasible pair.

The relative entropy is $I(\mathbb P',\mathbb P)=\sum_i\mathbb P'(i)\log(\mathbb P'(i)/\mathbb P(i))$, with $0\log(0/p)=0$ and $p'\log(p'/0)=+\infty$. The distributionally robust predictor and prescriptor are

$$\hat c_r(x,\mathbb P')=\sup_{\mathbb P\in\mathcal P}\{c(x,\mathbb P):I(\mathbb P',\mathbb P)\le r\},\qquad \hat x_r(\mathbb P')\in\arg\min_{x\in X}\hat c_r(x,\mathbb P'),$$

with $\hat x_r$ quasi-continuous (Definition 7). The estimator realization $\mathbb P'$ is the first argument of $I$, the reverse of the usual Kullback–Leibler ball.

Formalization targets

Goal: Theorem 7 (p. 20)

$$r>0\ \Longrightarrow\ (\hat c_r,\hat x_r)\ \text{is strongly optimal in (6), for every quasi-continuous selector }\hat x_r .$$

Milestones

1. Proof of Theorem 7, p. 21 (Bledsoe 1952): a quasi-continuous $\hat x:\mathcal P\to X$ is continuous on a dense subset of $\mathcal P$.
2. Proof of Theorem 7, p. 21 (Berge 1963): for $X$ compact and $\hat c$ continuous, $\mathbb P'\mapsto\hat c(\hat x(\mathbb P'),\mathbb P')$ is continuous for every arg-min selector $\hat x$.
3. Proposition 4, p. 20: for $r\ge0$ a quasi-continuous selector $\hat x_r$ exists.
4. Theorem 6, p. 20: for $r\ge0$, $(\hat c_r,\hat x_r)$ is feasible in (6).
5. Theorem 8, (21), p. 22: $\mathbb P^\infty\big(c(\hat x_r(\hat{\mathbb P}_T),\mathbb P)>\hat c_r(\hat x_r(\hat{\mathbb P}_T),\hat{\mathbb P}_T)\big)\le(T+1)^de^{-rT}$ for every $T\ge1$.

Context from mission 1

The proof of Theorem 7 also uses results posed as milestones of mission 1 of this series: the large deviation bounds of Theorem 1, (7a) and (7b) (p. 12); the continuity of $\hat c_r$ (Proposition 3, p. 16); the inclusion of the disappointment set in $\{I(\cdot,\mathbb P)>r\}$ from the proof of Theorem 3 (pp. 16–17); and the construction of a perturbed model $\mathbb P_2>0$ with $I(\mathbb P'_0,\mathbb P_2)<r$ from the proof of Theorem 4 ((14)–(16), pp. 17–18). They are not posed again here.

Significance

Theorem 7 says that no decision rule whose prescriptions disappoint with probability decaying at rate $r$ can report a smaller in-sample optimal value than relative-entropy DRO, at any realization of the data. It turns a modelling choice (which ambiguity set to use) into a consequence of a statistical requirement, and it identifies the radius $r$ of the ball with the decay rate of the out-of-sample disappointment. Theorem 8 complements this with a finite-sample bound that holds before any data are observed.

The theorem is proved in the paper, and its proof is short given the earlier results; there is no machine-checked version. A complete formalization adds a finite-alphabet Sanov theorem with the infinity convention of the relative entropy, an elementary theory of quasi-continuous functions on the simplex (density of continuity points, selection of quasi-continuous minimizers from an upper semicontinuous arg-min map), and Berge's maximum theorem in the form used here. The paper itself only sketches several steps (the construction of $\mathbb P_1,\mathbb P_2$ "exactly as in the proof of Theorem 4", and the proof of Theorem 8 is omitted).

Difficulty

Theorem 7 does not follow from the predictor result (Theorem 4). The order $\preceq_{\mathcal X}$ compares only the in-sample optimal values, so a competing pair may use a predictor that lies below $\hat c_r$ away from its own minimizers, and the pointwise comparison of predictors that settles Theorem 4 says nothing about such a pair. What the data can detect is governed by the large deviations of $\hat{\mathbb P}_T$, which only see sets with non-empty interior in $\mathcal P$, while the competitor's prescriptor need not be continuous. Without quasi-continuity of $\hat x$ the argument breaks: a selector that jumps to a cheaper decision only on a set with empty interior is invisible to the data, and the theorem is not claimed for such selectors. The existence half (Proposition 4) rests on a selection theorem for upper semicontinuous set-valued maps on Baire spaces (Matejdes 1987, Corollary 4), for which there is no Mathlib counterpart.

Formalization scope

Lean conventions:

• $\Xi$ is Fin d, and $\mathcal P$ is the subtype of stdSimplex ℝ (Fin d) with its subspace topology.
• $X$ is a compact subset of EuclideanSpace ℝ (Fin n), with decisions in the subtype ↥X and the Euclidean distance; $\gamma$ is continuous in $x$ for each $i$. These are the standing assumptions of §2 (p. 5).
• The relative entropy is valued in EReal, equal to $+\infty$ unless $\mathbb P(i)=0\Rightarrow\mathbb P'(i)=0$.
• $\mathbb P^\infty(\hat{\mathbb P}_T\in\mathcal D)$ is the finite sum over sample paths in $\Xi^T$ of $\prod_t\mathbb P(\xi_t)$. For $T=0$ every such event has probability $0$, and Theorem 8 is posed for $T\ge1$.
• The decay rate $\limsup\frac1T\log p_T\le-r$ is encoded without logarithms: for every $r'<r$, eventually $p_T\le e^{-r'T}$.
• $\hat x_r$ is a hypothesis-bound function, quasi-continuous and an arg-min selector of $\hat c_r$, never a chosen one.
• Proposition 4 additionally assumes $X\ne\emptyset$.

Ruled out:

• A rate written with Real.log would treat a probability that vanishes as having rate $0$.
• A real-valued relative entropy would give finite values where the paper has $+\infty$.
• Competing pairs without continuity of $\hat c$ or quasi-continuity of $\hat x$ make the theorem false.

Each of these makes the statement different from the paper's, and none is used.

Reusable infrastructure includes quasi-continuity (with the Bledsoe density theorem), Berge's maximum theorem for the minimum value, and finite-alphabet large deviations for empirical distributions. Contributions of any of these, or of the mission 1 milestones, are welcome.

Selected references

• B. P. G. Van Parys, P. Mohajerin Esfahani, D. Kuhn, From Data to Decisions: Distributionally Robust Optimization is Optimal, Management Science 67(6), 2021; preprint arXiv:1704.04118v3, 2019. https://arxiv.org/abs/1704.04118v3
• W. Bledsoe, Neighborly functions, Proceedings of the American Mathematical Society 3:114–115, 1952.
• C. Berge, Topological Spaces: Including a Treatment of Multi-Valued Functions, Vector Spaces, and Convexity, 1963, pp. 115–116.
• M. Matejdes, Sur les sélecteurs des multifonctions, Mathematica Slovaca 37(1):111–124, 1987.
• J. E. Smith, R. L. Winkler, The optimizer's curse: Skepticism and postdecision surprise in decision analysis, Management Science 52(3):311–322, 2006. https://doi.org/10.1287/mnsc.1050.0451

Motivation

Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks. At step $n$ it keeps an exponential moving average $m_n$ of stochastic gradients and an exponential moving average $v_n$ of their squared coordinates, corrects both for their initialization at zero (the bias correction or debiasing step), and moves the iterate by $-\gamma\,\hat m_n/(\varepsilon + \sqrt{\hat v_n})$ coordinatewise. Despite its use, its convergence on nonconvex objectives was poorly understood when Barakat and Bianchi wrote their paper: Reddi, Kale and Kumar (2018) exhibited convex online problems on which constant-parameter Adam fails to converge, and earlier analyses either dropped the bias correction or replaced Adam by a modified algorithm.

Barakat and Bianchi (arXiv:1810.02263v4, SIAM J. Math. Data Sci. 2021) study Adam through the ODE method: as the step size $\gamma \to 0$ with $1-\alpha \sim a\gamma$ and $1-\beta \sim b\gamma$, the interpolated iterates follow a non-autonomous ordinary differential equation, the continuous-time version of Adam. This mission formalizes their convergence theorem for that ODE (Theorem 3.2): trajectories started as Adam is started, with zero moment estimates, approach the critical points of the objective.

Setting

Let $F : \mathbb R^d \to \mathbb R$ be continuously differentiable with locally Lipschitz gradient $\nabla F$, and let $S : \mathbb R^d \to \mathbb R^d$ be locally Lipschitz. In the paper $F(x) = \mathbb E f(x,\xi)$ is the objective and $S(x) = \mathbb E\,\nabla f(x,\xi)^{\odot 2}$ the coordinatewise second moment of the stochastic gradient; §7 only uses the two properties above. Assume $F$ is coercive ($F(x) \to +\infty$ as $\|x\| \to \infty$) and $S(x) > 0$ coordinatewise for every $x$. Fix constants $a, b, \varepsilon > 0$ with $b \le 4a$.

The state is $z = (x, m, v) \in \mathcal Z = \mathbb R^d \times \mathbb R^d \times \mathbb R^d$, and $\mathcal Z_+$ is the part where $v \ge 0$. All vector operations are coordinatewise. The Adam field (3.3) is, for $t > 0$,

$$h(t, z) = \Big( -\frac{(1-e^{-at})^{-1}\, m}{\varepsilon + \sqrt{(1-e^{-bt})^{-1} v}},\ a(\nabla F(x) - m),\ b(S(x) - v) \Big),$$

and (ODE) is $\dot z(t) = h(t, z(t))$. The factors $(1-e^{-at})^{-1}$ and $(1-e^{-bt})^{-1}$ are the continuous-time bias corrections; they blow up as $t \downarrow 0$. A global solution with initial condition $(x_0, 0, 0)$ is a continuous $z : [0, +\infty) \to \mathcal Z_+$, continuously differentiable on $(0,+\infty)$, satisfying (ODE) for every $t > 0$, with $z(0) = (x_0, 0, 0)$. The critical set is $\mathcal S = \{x : \nabla F(x) = 0\}$.

The proof passes through the autonomous field $h_\infty(z) = \lim_{t\to\infty} h(t,z) = (-m/(\varepsilon+\sqrt v),\ a(\nabla F(x)-m),\ b(S(x)-v))$, its semiflow $\Phi$ on $\mathcal Z_+$, and the notions of equilibrium point, strict Lyapunov function and asymptotic pseudotrajectory (APT) of a semiflow.

Formalization targets

Goal: Theorem 3.2

Assume in addition that $F(\mathcal S)$ has empty interior in $\mathbb R$. For every global solution $z = (x, m, v)$ with initial condition $(x_0, 0, 0)$, the set $\mathcal S$ is non-empty and

$$\lim_{t\to\infty} d(x(t), \mathcal S) = 0, \qquad \lim_{t\to\infty} m(t) = 0, \qquad \lim_{t\to\infty} \big(S(x(t)) - v(t)\big) = 0 .$$

The theorem does not claim that $x(t)$ converges; convergence to a single critical point needs a Łojasiewicz condition (Theorem 3.4, a separate mission).

Milestones

The milestones are the numbered results of §7.1–7.3 used in the proof, in the order the proof uses them: positivity of $v$ along solutions (Lemma 7.4); decrease of $V_\infty$ along $h_\infty$ (Lemma 7.5, autonomous part); compactness of trajectories (Propositions 7.6, 7.7) and lower bounds on $v$ (Lemma 7.8); well-posedness of the autonomous system and its semiflow (Proposition 7.13); the abstract limit-set theorem for APTs (Proposition 7.14, quoted from Benaïm); the strict Lyapunov function $W_\delta(x,m,v) = V_\infty(x,m,v) - \delta\langle\nabla F(x), m\rangle + \delta\|S(x)-v\|^2$ (Proposition 7.15); and the APT property of the (ODE) solution (Proposition 7.17).

Significance

Theorem 3.2 is the deterministic core of the paper's analysis of Adam. Combined with the paper's tracking result (constant-step Adam converges in probability to the ODE solution as $\gamma \to 0$, Theorem 4.3) it says that for small steps Adam's iterates spend their time near critical points of $F$; it is also the input of the decreasing-step almost-sure convergence theorem (Theorem 5.2) and of the convergence-rate theorem (Theorem 3.4), which both rely on the same Lyapunov function and limit-set argument. The condition $b \le 4a$ under which the Lyapunov function decreases is satisfied by the default parameters $\alpha = 0.9$, $\beta = 0.999$.

The result is proved in the paper; to the best of current knowledge it has not been machine-checked. The mission produces a formal proof of the theorem, and reusable formal statements about semiflows on metric spaces: strict Lyapunov functions, and the limit set of a relatively compact asymptotic pseudotrajectory.

Difficulty

The obvious route is to show that $V(t, z(t)) = F(x) + \tfrac12\|m\|^2_{U(t,v)^{-1}}$ decreases and apply LaSalle's invariance principle. This fails on two counts. First, (ODE) is non-autonomous, and LaSalle's principle is a statement about autonomous systems: the derivative of $V$ along the flow vanishes only on a set that depends on $t$. Second, the field is singular: $h(\cdot, z)$ blows up at $t = 0$ and $h(t, \cdot)$ is not Lipschitz near $v = 0$, because of $\sqrt v$, so neither existence and uniqueness nor continuous dependence on initial data come from standard theorems. The energy $V_\infty(z) = \lim_{t\to\infty} V(t,z)$ of the autonomous limit $\dot z = h_\infty(z)$ is a Lyapunov function but not a strict one: it is constant along some non-equilibrium orbits, so non-increase of an energy alone does not identify the limit points.

Formalization scope

Each block $x, m, v$ lives in EuclideanSpace ℝ (Fin d) and $\mathcal Z$ is their product; Mathlib's norm on the product is the maximum of the three Euclidean norms, which is equivalent to the Euclidean norm of $\mathbb R^{3d}$ and changes no statement. $F$ and $S$ are abstract, with the hypotheses of the paper's §7 (Assumptions 7.1, 7.2, 2.3, 2.4); this generality implies the printed theorem for the $F$, $S$ of (2.2). Solutions are maps $\mathbb R \to \mathcal Z$ constrained only on $[0, +\infty)$ (or $[0, T)$), and the equation is required at $t > 0$ only. The field is extended off $\mathcal Z_+$ by $v \mapsto |v|$, as on p. 12 of the paper. A semiflow is Mathlib's Flow ℝ≥0 M, on the subtype $\mathcal Z_+$ or on a compact subset of it. The semiflow $\Phi$ in the milestones is always assumed to be the flow of $(\mathrm{ODE}_\infty)$, never an arbitrary flow. The APT and limit-set definitions are the published StochApproxDyn.LimitSet ones.

The goal is stated for every global solution of the specific field (3.3), and keeps "$\mathcal S$ is non-empty" in the conclusion. A statement about some solution of an unspecified field, or with "$F(\mathcal S)$ has empty interior" strengthened to "$\mathcal S$ is finite", is a different theorem and does not count.

A complete development needs: Grönwall-type comparison and chain-rule arguments along $C^1$ trajectories; well-posedness of the autonomous system on $\mathcal Z_+$ and continuity of its flow; and the limit-set theory of asymptotic pseudotrajectories (Benaïm 1999), adapted to strict Lyapunov functions in the paper's sense. The last part is independent of Adam and reusable in stochastic approximation. Contributions to any milestone are welcome; Propositions 7.13 and 7.14 are the largest pieces of infrastructure.

Selected references

• A. Barakat, P. Bianchi, Convergence and Dynamical Behavior of the ADAM Algorithm for Nonconvex Stochastic Optimization, SIAM J. Math. Data Sci. 3(1), 2021; arXiv:1810.02263v4. https://arxiv.org/abs/1810.02263v4
• D. P. Kingma, J. Ba, Adam: A Method for Stochastic Optimization, ICLR 2015. https://arxiv.org/abs/1412.6980
• S. J. Reddi, S. Kale, S. Kumar, On the Convergence of Adam and Beyond, ICLR 2018. https://arxiv.org/abs/1904.09237
• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999. https://doi.org/10.1007/BFb0096509

Motivation

A decision based on observed data can change when the data law differs from the one used to choose it. Distributionally robust optimization addresses this by evaluating each decision against a family of nearby probability laws. Optimal transport gives one way to define “nearby”: a candidate law is admissible when probability mass can be moved from the baseline law at a bounded expected cost. For a linear decision rule, the resulting worst-case expectation is usually harder to optimize than an ordinary sample-average loss. Blanchet, Murthy, and Zhang identify a dual objective whose variables are the decision vector and a scalar transport multiplier, then study its curvature near the multipliers that actually minimize it (Blanchet–Murthy–Zhang, 2022).

The paper proves that this dual objective is jointly strongly convex on a specified region for sufficiently small transport radius. This matters because ordinary convexity allows flat directions in the joint decision–multiplier space. The joint lower Hessian bound gives local curvature in every direction with one positive modulus that remains independent of the radius apart from the paper's explicit factor $\sqrt{\delta}$ (Theorem 4, p. 11).

Setting

Let $X\in\mathbb R^d$ have a baseline probability law $P_0$, and let a decision be a vector $\beta$ in a nonempty compact convex set $B\subseteq\mathbb R^d$. The loss of a possible outcome $x$ is $\ell(\beta^{\mathsf T}x)$ for a convex function $\ell:\mathbb R\to\mathbb R$. A state-dependent positive-definite matrix $A(x)$ sets the cost of moving mass from $x$ to $x'$:

$$c(x,x')=(x-x')^{\mathsf T}A(x)(x-x').$$

Assumption 1 requires this cost to be lower semicontinuous and the eigenvalues of $A(x)$ to lie between positive constants $\rho_{\min}$ and $\rho_{\max}$ for $P_0$-almost every $x$. Assumption 2 requires at most quadratic growth of $\ell$ and a finite fourth moment of $P_0$. The ambiguity radius $\delta$ is positive (Assumptions 1–2, pp. 9–10).

The paper's dual objective is an expectation under the known law $P_0$. Write $q_A(\beta,x)=\beta^{\mathsf T}A(x)^{-1}\beta$. For a scalar $\lambda\ge0$ and an auxiliary scalar $\gamma$, set

$$F(\gamma,\beta,\lambda;x) =\ell\bigl(\beta^{\mathsf T}x+\gamma\sqrt\delta\,q_A(\beta,x)\bigr) -\lambda\sqrt\delta\bigl(\gamma^2q_A(\beta,x)-1\bigr), \qquad f_\delta(\beta,\lambda)=\mathbb E_{P_0}\!\left[\sup_{\gamma\in\mathbb R}F(\gamma,\beta,\lambda;X)\right].$$

This value may be $+\infty$. Under the paper's duality conditions, minimizing $f_\delta(\beta,\lambda)$ over $\lambda\ge0$ gives the worst-case loss at $\beta$ (Theorem 1 and (7), p. 10).

Formalization targets

Assumption 3 bounds $\ell''$ above by $M>0$ and excludes an almost surely zero $\ell'(\beta^{\mathsf T}X)$ for each $\beta\in B$. Assumption 4 makes $B$ compact. Lemma 6 supplies positive constants $\underline L,\overline L$ bounding $\mathbb E_{P_0}[\ell'(\beta^{\mathsf T}X)^2]$ uniformly over $B$. With $R_\beta=\sup_{\beta\in B}\|\beta\|$, the constants $K_1,K_2$ are those of (28), and

$$\mathbb V_\delta=\{(\beta,\lambda):\beta\in B,\ \lambda\ge0,\ K_1\|\beta\|\le\lambda\le K_2\|\beta\|\}.$$

Theorem 3 first gives a bounded Hessian on $\mathbb V_\delta$ and a positive lower bound on its $\beta$ block when $0<\delta<\delta_0$, with the explicit $\delta_0$ from p. 36. The goal, Theorem 4, adds Assumption 5: $\ell$ is locally strongly convex and, at each $\beta\in B$, the loss derivative and the linear score are simultaneously separated from zero with positive probability. It asserts the joint bound

$$\exists\,\delta_1\in(0,\delta_0),\ \kappa_1>0\quad \forall\,\delta\in(0,\delta_1),\ \forall\,\theta\in\mathbb V_\delta:\quad \nabla^2 f_\delta(\theta)\succeq\sqrt\delta\,\kappa_1 I_{d+1}.$$

The order of the quantifiers is part of the target: $\kappa_1$ works for every sufficiently small $\delta$ (Theorems 3–4, p. 11).

Significance

The Hessian bound makes the joint dual parameters locally identifiable by curvature on a region that contains every dual optimizer. In the paper, this structure also underlies the analysis of algorithms and of how the optimizer changes with the transport radius (Proposition 1, p. 11; §3 and §5.4). Theorem 4 is already proved in the paper; this mission asks for its machine-checked formalization, together with the stated bounds on multipliers, the maximizing scalar, and the intermediate curvature results. The general optimal-transport integral used here already has a published Prove2Me definition from Blanchet and Murthy's earlier model-risk work. The new definitions specify this paper's Mahalanobis model, regions, and smoothness assumptions.

Difficulty

Convexity alone gives only a nonnegative Hessian; it cannot produce a strictly positive joint lower bound. Even curvature of $\ell$ does not by itself control directions that combine a change in $\beta$ with a change in $\lambda$. The inner supremum over $\gamma$ can become infinite outside its effective domain, while at $\beta=0$ its maximizer ceases to be unique. The theorem therefore needs a region where the dual objective is finite and differentiable and a probabilistic condition that prevents the relevant score and derivative from vanishing together. The target keeps the actual $\sqrt\delta$ scale instead of settling for a radius-dependent positive constant (§2.2.2 and Remark 4, pp. 10–12, 39).

Formalization scope

Lean uses EuclideanSpace ℝ (Fin d) for $\mathbb R^d$, a Borel probability measure for $P_0$, and EReal for $f_\delta$ and the inner supremum. The reused extended-real integral records the $+\infty$ and $-\infty$ cases; the Hessian is taken only where $f_\delta$ is finite on a neighborhood and its real representative is differentiable there. Quadratic Hessian forms use $\|v_\beta\|^2+v_\lambda^2$, since Lean's product norm is not the paper's Euclidean norm. The compact set $B$ is explicitly nonempty, and the positive ambiguity radius $\delta$ is quantified inside the goal so that $\delta_1$ and $\kappa_1$ are uniform in $\delta$. Theorem 3 additionally assumes $R_\beta>0$ for the proof's explicit formula for $\delta_0$: nonempty compact $B=\{0\}$ would make that formula zero. Assumption 5 already gives $R_\beta>0$ in the goal.

The goal retains Assumption 5's per-decision quantifiers. That assumption itself excludes $0\in B$: its strict score event is empty at $\beta=0$. Intermediate statements where the printed wording includes $\beta=0$ but the claim fails there state $\beta\ne0$ explicitly. Lemma 5 also states the differentiability and positive-multiplier conditions needed for its derivative and division. Proposition 9(b)'s printed strict curvature-margin inequality is corrected to the nonstrict inequality derived in its proof; its original wording is preserved in the milestone quotation. The claims are about the expectation $f_\delta$, with $\kappa_1$ independent of $\delta$, rather than a pointwise or merely convex substitute.

A complete development needs measurable extended-real integration, the matrix quadratic form and its inverse, almost-everywhere spectral bounds, differentiability under an expectation, and Hessian estimates for an optimized scalar. The transport integral, the assumptions and constants, and the multiplier bounds are intended as reusable interfaces for the companion missions. Contributions that close the listed lemmas or add the paper's omitted second-order kernel formula are within scope.

Selected references

• José Blanchet, Karthyek Murthy, and Fan Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Mathematics of Operations Research 47(2), 2022. arXiv:1810.02403v3; DOI:10.1287/moor.2021.1178.
• José Blanchet and Karthyek Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research 44(2), 2019. arXiv:1604.01446v2.