Convex Optimization

Motivation

The alternating direction method of multipliers (ADMM) is a standard method for convex problems whose objective splits into two blocks coupled by a linear constraint (Gabay & Mercier 1976; Boyd et al. 2011). Many models in imaging, statistics and sparse or low-rank recovery have three or more blocks, and the scheme practitioners reach for first is the direct extension of ADMM: minimize the augmented Lagrangian over each block in turn, then update the multiplier. For years it was unknown whether this scheme converges in general.

Chen, He, Ye and Yuan (Math. Program., 2016) settled the question negatively: on a three-variable linear system with zero objective, the direct extension diverges for every penalty parameter (their Theorem 3.1). Their Section 4.1 then asks whether strong convexity of the objective rescues convergence. Han and Yuan (J. Optim. Theory Appl., 2012) had proved convergence for strongly convex objectives under a restriction on the penalty parameter determined by the strong convexity moduli. Theorem 4.1 shows that this restriction cannot simply be removed. This mission formalizes Theorem 4.1 and the three facts on p. 14 that support it.

Timeline:

• 1975–1976: Glowinski–Marrocco and Gabay–Mercier introduce two-block ADMM and prove its convergence.
• 2012: Han and Yuan prove convergence of the multi-block direct extension when every $\theta_i$ is strongly convex and $\beta$ is small enough.
• 2014 (authors' version), published 2016: Chen, He, Ye and Yuan give the first divergent example (Theorem 3.1) and its strongly convex variant (Theorem 4.1).

Setting

The three-block problem (1.1) is

$$\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,\quad x_i\in\mathcal X_i,$$

with $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$; the solution set is assumed nonempty.

For a penalty parameter $\beta>0$ and a multiplier $\lambda\in\mathbb R^p$, the augmented Lagrangian (1.6) is

$$\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)+\frac\beta2\|A_1x_1+A_2x_2+A_3x_3-b\|^2 .$$

The direct extension of ADMM (1.5) starts from $(x_2^0,x_3^0,\lambda^0)$ and, for $k\ge0$, sets $x_1^{k+1}$, $x_2^{k+1}$, $x_3^{k+1}$ to minimizers of $\mathcal L_{\mathcal A}$ over $\mathcal X_1,\mathcal X_2,\mathcal X_3$ in that order, each with the newest values of the other blocks, and then sets $\lambda^{k+1}=\lambda^k-\beta(A_1x_1^{k+1}+A_2x_2^{k+1}+A_3x_3^{k+1}-b)$.

A function $f$ is $m$-strongly convex if $f-\frac m2\|\cdot\|^2$ is convex.

The instance (4.1) is

$$\min\ 0.05x_1^2+0.05x_2^2+0.05x_3^2\quad\text{s.t.}\quad\begin{pmatrix}1&1&1\\1&1&2\\1&2&2\end{pmatrix}\begin{pmatrix}x_1\\x_2\\x_3\end{pmatrix}=0,$$

with scalar $x_i$, $\mathcal X_i=\mathbb R$ and $b=0$. Its unique solution is $x=0$. For $\beta=1$ the state after an iteration is $z=(x_2,x_3,\lambda_1,\lambda_2,\lambda_3)\in\mathbb R^5$, and $M_{41}$ denotes the $5\times5$ iteration matrix that maps $z^k$ to $z^{k+1}$.

Formalization targets

Goal: Theorem 4.1

For the model (1.1) with strongly convex objective, (1.5) is not necessarily convergent for all $\beta>0$. Formally, (4.1) satisfies the standing assumptions, each $\theta_i$ is $\tfrac1{10}$-strongly convex, and at $\beta=1$ there is a starting point $(x_2^0,x_3^0,\lambda^0)$ from which a run of (1.5) exists and

$$\text{no run }(x_1^k,x_2^k,x_3^k,\lambda^k)_{k\ge0}\text{ of (1.5) from it converges.}$$

The goal fixes the witness instance and $\beta=1$, because those are what the paper computes. It does not fix the starting point.

Milestones

1. Fixed matrix mapping. Every run of (1.5) on (4.1) with $\beta=1$ satisfies $z^{k+1}=M_{41}z^k$ for all $k$, with the explicit rational matrix $M_{41}$.
2. Spectral radius. $\rho(M_{41})$, the largest modulus of a complex eigenvalue, lies in $[1.00865,1.00875)$, i.e. equals $1.0087$ to the four decimals of the page.
3. Diverging powers. Some real $z\in\mathbb R^5$ has $\|M_{41}^kz\|\to\infty$.

Significance

Theorem 4.1 says that strong convexity of each $\theta_i$, on its own, does not make the three-block direct extension of ADMM converge. Convergence results for strongly convex models therefore have to restrict $\beta$, as Han and Yuan do, or modify the scheme. Examples of modified schemes are a shrunken multiplier step (discussed in §4.2 of the paper) and Gaussian back substitution (He, Tao & Yuan 2012). The example is also a concrete test case: any proposed sufficient condition for convergence has to exclude (4.1) at $\beta=1$.

The theorem is proved in the paper, but only in outline: the iteration matrix is not printed, the spectral radius is reported as the outcome of "a simple calculation", and the construction of a divergent starting point is "omitted for succinctness". A formalization makes each step explicit and machine-checked. That means the exact iteration matrix, a certified enclosure of its spectral radius, and a real starting point whose iterates are unbounded. As far as is known, none of these results has been machine-checked.

Difficulty

There are three separate difficulties.

• Reduction to a matrix. The method is defined by three minimizations, not by a formula, so the matrix recursion has to be derived from those minimizations.
• Certifying the spectral radius. The spectral radius is a property of a degree-5 characteristic polynomial with large rational coefficients. Its dominant roots are a non-real conjugate pair of modulus about $1.00874$, so the margin above $1$ is under one percent, and the rounding interval requested is narrow.
• From eigenvalue to divergence. A spectral radius above $1$ does not by itself give a divergent real trajectory. The dominant eigenvectors are complex, and the starting vector must be real yet have a nonzero component along the expanding pair.

A natural first idea is to argue that strong convexity of the objective forces the iterates toward the unique solution. This fails because the multiplier and the coupling between blocks are not controlled by the objective's curvature once $\beta$ is large relative to the moduli.

Formalization scope

Vectors in $\mathbb R^n$ are Fin n → ℝ and matrices are Matrix (Fin p) (Fin n) ℝ. The Euclidean square norm in (1.6) is written $r\cdot r$ (⬝ᵥ), never Mathlib's sup norm. Norms appear otherwise only in "$\|\cdot\|\to\infty$", where every norm on $\mathbb R^5$ gives the same meaning. Blocks are separate fields, and multiplier components are 0-based. A run is a predicate on sequences: "$x^{k+1}=\operatorname{Argmin}$" means "$x^{k+1}$ is a minimizer", and $x_1^0$ is never read. "Converges" means convergence of $(x_1^k,x_2^k,x_3^k,\lambda^k)$ in the product topology.

Strong convexity is Mathlib's StrongConvexOn Set.univ (1/10). The paper's "closed convex" $\theta_i$ are real-valued on all of $\mathbb R^{n_i}$, hence continuous, so only convexity is stated.

The quantifier "for all $\beta>0$" is read as "not for every $\beta>0$", witnessed at $\beta=1$. The stronger reading, divergence for every $\beta$, is false for (4.1), where the spectral radius is below $1$ for small $\beta$.

Trivializations ruled out. The goal asserts the existence of a run, so non-convergence cannot hold vacuously. Runs are characterized by minimizer conditions rather than an argmin choice function with junk values. Spectral statements are over $\mathbb C$ rather than over real eigenvalues only; the only real eigenvalue of $M_{41}$ is $0$.

What a complete development needs: first-order optimality for strictly convex scalar quadratics; existence and uniqueness of the subproblem minimizers; a certified root enclosure for a quartic with rational coefficients (via Rouché-type bounds, interval arithmetic or an explicit factorization over $\mathbb R$); and the passage from a dominant complex eigenpair to a real unbounded orbit. The last two are reusable for any linear-iteration divergence argument, including Theorem 3.1 of the same paper. Contributions of any of these lemmas, as separate theorems, are welcome.

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, Math. Program. 155 (2016) 57–79. https://doi.org/10.1007/s10107-014-0826-5
• D. Han, X. Yuan, A note on the alternating direction method of multipliers, J. Optim. Theory Appl. 155 (2012) 227–238. https://doi.org/10.1007/s10957-012-0003-z
• D. Gabay, B. Mercier, A dual algorithm for the solution of nonlinear variational problems via finite element approximation, Comput. Math. Appl. 2 (1976) 17–40. https://doi.org/10.1016/0898-1221(76)90003-1
• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed optimization and statistical learning via the alternating direction method of multipliers, Found. Trends Mach. Learn. 3 (2011) 1–122. https://doi.org/10.1561/2200000016

Motivation

A large share of the optimization problems solved in statistics, signal processing and machine learning have the composite form

$$\min_x\ \varphi(x) := f(x) + g(x),$$

where $f$ is smooth and $g$ is convex but possibly nonsmooth or extended-valued (a norm penalty, the indicator of a constraint set). The workhorse algorithm for such problems is the proximal gradient method, which takes a gradient step on $f$ followed by a proximal step on $g$. Its worst-case rate on convex problems is sublinear, yet in practice it often converges linearly. The classical explanation, going back to Luo and Tseng (1993) Ann. Oper. Res. 46, is an error bound condition: near the solution set, the distance to the minimizers is controlled by the length of the algorithm's own step. Under such a condition the method converges linearly.

The difficulty is that the error bound is stated in terms of the algorithm, not the problem. Drusvyatskiy and Lewis (arXiv:1602.06661, Math. Oper. Res. 43(3), 2018) showed that, for convex problems, it is equivalent to a purely geometric property of $\varphi$: quadratic growth away from the set of minimizers. This mission formalizes that equivalence (§3 of the paper) together with the three comparison results that build it.

Setting

Write $\mathbb R^n$ for Euclidean space with norm $\|\cdot\|$, $\overline{\mathbb R} = \mathbb R\cup\{\pm\infty\}$, and $\operatorname{dist}(x;Q) = \inf_{z\in Q}\|z-x\|$. A function $g:\mathbb R^n\to\overline{\mathbb R}$ is closed if it is lower semicontinuous. For real $r$, the sublevel set is $[\varphi\le r] = \{x:\varphi(x)\le r\}$.

The problem is (3.1): $g$ is a closed convex function, and $f:\mathbb R^n\to\mathbb R$ is convex, $C^1$-smooth, with $\beta$-Lipschitz gradient, $\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|$. Let $S$ be the (nonempty) set of minimizers of $\varphi = f+g$ and $\varphi^*$ its minimal value. For $t>0$ the proximal map is

$$\operatorname{prox}_{tg}(z) = \operatorname*{argmin}_y\Big\{g(y)+\tfrac1{2t}\|y-z\|^2\Big\},$$

the proximal gradient method iterates $x_{k+1} = \operatorname{prox}_{tg}(x_k - t\nabla f(x_k))$, and the prox-gradient mapping is

$$\mathcal G_t(x) = t^{-1}\big(x - \operatorname{prox}_{tg}(x - t\nabla f(x))\big),$$

so that $x_{k+1} = x_k - t\,\mathcal G_t(x_k)$ and $\mathcal G_t(x) = 0$ exactly at minimizers.

For $\nu>0$, $\varphi$ has quadratic growth with constant $\alpha>0$ if $\varphi(x)\ge\varphi^*+\frac\alpha2\operatorname{dist}^2(x;S)$ on $[\varphi\le\varphi^*+\nu]$ (3.12), and the error bound condition with parameters $(\gamma,\nu)$ holds if $\operatorname{dist}(x;S)\le\gamma\|\mathcal G_t(x)\|$ on the same sublevel set (Definition 3.1, (3.13)).

Formalization targets

Goal: Corollary 3.6 (p. 9)

$$\text{(3.12) with }\alpha\ \Longrightarrow\ \text{(3.13) with }\gamma = (2\alpha^{-1}+t)(1+\beta t),\qquad \text{(3.13) with }\gamma\ \Longrightarrow\ \text{(3.12) for every }\alpha\in(0,\gamma^{-1}),$$

for every step size $t>0$ and every $\nu>0$.

Milestones

For a closed convex $h$ with minimizers $S\neq\emptyset$ and minimal value $h^*$:

• Theorem 3.3 (pp. 6–7): quadratic growth on $[h\le h^*+\nu]$ with constant $\alpha$ implies $\operatorname{dist}(x;S)\le L\operatorname{dist}(0;\partial h(x))$ there with $L = 2\alpha^{-1}$; conversely the latter implies quadratic growth with any $\alpha\in(0,1/L]$.
• Theorem 3.4 (p. 7): the subdifferential bound with $L$ implies $\operatorname{dist}(x;S)\le\widehat L\,t^{-1}\|x-\operatorname{prox}_{th}(x)\|$ with $\widehat L = L+t$; conversely the latter implies the former with $L = \widehat L$.
• Theorem 3.5 (p. 8): for maximal monotone $G,\Phi$ with $\Phi = F + G$ and $F$ single-valued, the forward-backward step satisfies $\|\mathcal G_t(x)\|\le\operatorname{dist}(0;\Phi(x))$ (3.10), and if $F$ is $\beta$-Lipschitz,

$$(1-\beta t)\|\mathcal G_t(x)\|\ \le\ \|t^{-1}(x-\operatorname{prox}_{t\Phi}(x))\|\ \le\ (1+\beta t)\|\mathcal G_t(x)\|.\qquad(3.11)$$

• Theorem 3.2, second claim (p. 5, at $t=\beta^{-1}$): under the error bound, the iterates converge R-linearly to any limit point $x^*$, $\|x_{r+k}-x^*\|^2\le(1-\frac1{2\beta\gamma})^kC(\varphi(x_r)-\varphi^*)$.

Significance

The result. Corollary 3.6 converts a condition on an algorithm into a condition on the objective. Quadratic growth can be checked by hand in many models (strongly convex losses, polyhedral problems, problems with a sharp minimum), and once it holds, Theorem 3.2 gives linear convergence of the proximal gradient method with an iteration count of order $\frac\beta\alpha\ln\frac1\epsilon$, matching the rate familiar from strongly convex problems. The rest of the paper uses this equivalence as its main tool: §4 proves quadratic growth for structured problems $f(Ax)+g(x)$ under dual strict complementarity, and §§5–8 extend the comparison to prox-linear methods for nonconvex compositions. Theorems 3.3 and 3.4 are statements about a single closed convex function and are of independent use in the analysis of proximal point methods.

Formalizing it. All results here are proved on paper; none of them is machine-checked. The mission produces a Lean statement of the equivalence with the paper's explicit constants, and of the step-length comparison between the forward-backward and the proximal point methods for maximal monotone operators. Formal proofs require the existence, uniqueness and nonexpansiveness of resolvents and proximal maps, the subdifferential sum rule for a smooth plus a convex function, and a quadratic growth argument for convex functions; these are reusable well beyond this paper.

Difficulty

The forward direction is a chain of three inequalities, but each link compares objects that live in different worlds: the subdifferential of $\varphi$, the proximal map of $\varphi$, and the proximal map of $g$ evaluated at a gradient-shifted point. The proximal gradient step is not the proximal point step on $\varphi$, and the obvious attempt to compare $\mathcal G_t(x)$ with $\partial\varphi(x)$ directly gives only one inequality (3.10); the reverse comparison (3.11) needs the resolvent of the sum $\nabla f + \partial g$ and the Lipschitz constant of $\nabla f$. The converse half of Theorem 3.3 (error bound implies growth) is the deepest step: the paper omits its proof and cites Drusvyatskiy–Ioffe and Drusvyatskiy–Mordukhovich–Nghia. It has to pass from a pointwise bound on subgradients to a bound on function values over the whole sublevel set, which no single subgradient inequality provides.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $\overline{\mathbb R}$-valued functions are EReal-valued; $f$ is real-valued and $\varphi = f + g$ is computed in EReal. "Closed convex" is the published RockafellarMaxMono.Shared.ProperConvex (never $-\infty$, somewhere finite, convex) together with LowerSemicontinuous.
• $S$ is the set of minimizers, assumed nonempty as in the paper; $\varphi^*$ is a real number equal to $\varphi$ on $S$; $\operatorname{dist}$ is Metric.infDist; $\nu>0$ is real.
• Proximal maps and resolvents are predicates, never chosen functions: $p=\operatorname{prox}_{tg}(z)$ is the published GoldenRatioVI.Shared.IsProxPoint (fun y => t * g y) z p (same argmin for $t>0$), and resolvents are maps satisfying the published ThreeOpSplitting.Convergence.IsResolvent. Conditions are stated for every such point; existence and uniqueness are facts a solver proves.
• $\operatorname{dist}(0;\partial h(x))$ follows the convention $\operatorname{dist}(0;\emptyset) = +\infty$: an inequality "$a\le L\operatorname{dist}(0;\partial h(x))$" is stated as "$a\le L\|v\|$ for every $v\in\partial h(x)$". Using Metric.infDist 0 (∂h x), which is $0$ on the empty set, would turn (3.7) into the false claim that every point of the sublevel set where $\partial h$ is empty is a minimizer; this trivializing or falsifying encoding is ruled out.
• The subdifferential is the published ProxAlg.FixedPoint.subdifferential, the gradient is Mathlib's gradient.
• Theorem 3.2 is stated at $t = \beta^{-1}$ with $\beta>0$: the printed range $t\le\beta^{-1}$ relies on the descent inequality (3.2), which fails for smaller $t$. Its first claim (an iteration count) and Corollary 3.7 are not stated.

Contributions welcome: proofs of the milestones in any order, general lemmas on resolvents of maximal monotone operators and on proximal maps of EReal-valued convex functions, and a proof of the converse half of Theorem 3.3.

Selected references

• D. Drusvyatskiy, A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Math. Oper. Res. 43(3), 2018. arXiv:1602.06661v2 — https://arxiv.org/abs/1602.06661
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46/47:157–178, 1993. https://doi.org/10.1007/BF02096261
• D. Drusvyatskiy, A. D. Ioffe, Quadratic growth and critical point stability of semi-algebraic functions, Math. Program. 153(2):635–653, 2015 (reference [15] of the paper).
• D. Drusvyatskiy, B. S. Mordukhovich, T. T. A. Nghia, Second-order growth, tilt stability, and metric regularity of the subdifferential, J. Convex Anal. 21(4):1165–1192, 2014 (reference [19] of the paper).
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

Nesterov's accelerated gradient method minimizes a smooth convex function at the rate $\mathcal O(k^{-2})$ in the number of iterations $k$, against $\mathcal O(k^{-1})$ for plain gradient descent. Su, Boyd and Candès (arXiv:1503.01243) observed that, as the step size tends to zero, Nesterov's scheme becomes the second-order differential equation

$$\ddot x(t)+\frac{\alpha}{t}\dot x(t)+\nabla\Phi(x(t))=0\tag{1}$$

with $\alpha=3$, a heavy-ball system whose friction coefficient $\alpha/t$ vanishes as $t\to+\infty$ (asymptotic vanishing damping). Studying (1) in continuous time gives Lyapunov arguments that are then discretized into new algorithms.

Attouch, Chbani, Peypouquet and Redont (Math. Program. 168 (2018), DOI 10.1007/s10107-016-0992-8) analyse (1) for general $\alpha$. This mission formalizes their result for strongly convex $\Phi$, where the rate of convergence of (1) depends on $\alpha$ and improves without bound as $\alpha$ grows.

Timeline.

• 2014–2016: Su, Boyd and Candès prove $\Phi(x(t))-\min\Phi=\mathcal O(t^{-2})$ for convex $\Phi$ and $\alpha\ge3$, and $\mathcal O(t^{-3})$ for strongly convex $\Phi$ when $\alpha>9/2$ ([44, Theorem 4.2] in the paper).
• 2015 (this paper): every trajectory converges weakly to a minimizer when $\alpha>3$; for strongly convex $\Phi$ and every $\alpha>3$, the values, the squared distance to the minimizer and the squared velocity are $\mathcal O(t^{-2\alpha/3})$.

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$, and let $\Phi:\mathcal H\to\mathbb R$ be continuously differentiable with gradient $\nabla\Phi$. Fix $\alpha>0$ and $t_0>0$. A solution of (1) is a twice differentiable trajectory $x:[t_0,+\infty[\to\mathcal H$ with velocity $\dot x$ satisfying (1) at every $t\ge t_0$.

$\Phi$ is strongly convex with constant $\mu>0$ if

$$\Phi(y)\ge\Phi(x)+\langle\nabla\Phi(x),y-x\rangle+\frac\mu2\|x-y\|^2\qquad\text{for all }x,y\in\mathcal H.$$

Such a $\Phi$ has exactly one minimizer $x^*$, and $\min\Phi=\Phi(x^*)$.

For $\lambda\ge0$, $p\ge0$ the anchored energy is

$$\mathcal E^p_\lambda(t)=t^p\Big(t^2\big(\Phi(x(t))-\min\Phi\big)+\tfrac12\|\lambda(x(t)-x^*)+t\dot x(t)\|^2\Big),$$

a sum of nonnegative terms. The proof of the main theorem fixes

$$p=\tfrac23(\alpha-3),\qquad\lambda=\tfrac23\alpha,\qquad t_1=\max\Big\{t_0,\sqrt{p\lambda/\mu}\Big\}.$$

Formalization targets

Goal: Theorem 3.4 (p. 11)

For strongly convex $\Phi$ and $\alpha>3$, every solution $x$ of (1) converges strongly to the unique minimizer $x^*$, and

$$\Phi(x(t))-\min\Phi=\mathcal O\big(t^{-\frac23\alpha}\big),\qquad\|x(t)-x^*\|^2=\mathcal O\big(t^{-\frac23\alpha}\big),\qquad\|\dot x(t)\|^2=\mathcal O\big(t^{-\frac23\alpha}\big)\tag{25}$$

as $t\to+\infty$. The goal states the asymptotic form; the explicit constants are milestones.

Milestones (explicit forms, valid for $t\ge t_1$)

1. The derivative identity (10) for $\mathcal E^p_\lambda$ along solutions of (1), for any $\lambda,p\ge0$.
2. Its strongly convex upper bound (first display of the proof of Theorem 3.4).
3. (26): $\mathcal E^p_\lambda(t)\le\mathcal E^p_\lambda(t_1)+\frac{\lambda p}{4}t^p\|x(t)-x^*\|^2\le\mathcal E^p_\lambda(t_1)+\frac{\lambda p}{2\mu}t^p(\Phi(x(t))-\min\Phi)$.
4. (27): $\Phi(x(t))-\min\Phi\le2\mathcal E^p_\lambda(t_1)\,t^{-\frac23\alpha}$.
5. (28): $\|x(t)-x^*\|^2\le\frac2\mu(\Phi(x(t))-\min\Phi)\le\frac4\mu\mathcal E^p_\lambda(t_1)\,t^{-\frac23\alpha}$.
6. Last display of the proof: $\|\dot x(t)\|^2\le4\big(1+\sqrt{\alpha/(\alpha-3)}\big)^2\mathcal E^p_\lambda(t_1)\,t^{-\frac23\alpha}$.

Significance

The theorem shows that the rate of (1) on strongly convex functions is not capped at $\mathcal O(t^{-2})$ or $\mathcal O(t^{-3})$: the exponent $2\alpha/3$ grows linearly in $\alpha$, and it already exceeds $2$ for every $\alpha>3$. It extends [44, Theorem 4.2], which needs $\alpha>9/2$ and gives $\mathcal O(t^{-3})$. The same parametrized energy $\mathcal E^p_\lambda$ is the template for the discrete analyses of Nesterov-type algorithms with parameter $\alpha$, so its derivative identity (10) is reusable beyond this mission.

The result is proved on paper. To the best of current knowledge none of it is formalized: Mathlib has no theory of inertial dynamics, and the platform's strongly convex rates concern discrete methods. A completed mission gives a machine-checked Lyapunov analysis of a non-autonomous second-order ODE in a Hilbert space, with the explicit constants of the paper.

Difficulty

The derivative identity (10) is a computation, but it must be carried out with one-sided derivatives at $t_0$, real powers $t^p$, and the chain rule for $\Phi\circ x$ in an infinite-dimensional space. The obvious argument, that $\mathcal E^p_\lambda$ is nonincreasing, fails: even with the best choice of $p$ and $\lambda$ the bound on its derivative keeps a term $\frac{\lambda p}{2}t^p\langle x-x^*,\dot x\rangle$ of no fixed sign, and only for $t\ge t_1$ is the quadratic term in $\|x-x^*\|^2$ nonpositive. Passing from the differential inequality to (26) therefore needs integration on $[t_1,t]$ for functions known only through one-sided derivatives. The velocity bound then combines (26), (27) and (28) through square roots, and the goal additionally requires the existence of the minimizer in an infinite-dimensional space, which is a compactness argument (weak lower semicontinuity) and not an algebraic one.

Formalization scope

• $\mathcal H$ is any real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H), not $\mathbb R^n$. $\Phi$ is ContDiff ℝ 1 and $\nabla\Phi$ is Mathlib's gradient.
• A solution is a pair $(x,v)$ with $t_0>0$, where $x$ has derivative $v(t)$ and $v$ has derivative $-\frac\alpha t v(t)-\nabla\Phi(x(t))$ within $[t_0,+\infty[$ at every $t\ge t_0$; $\dot x$ is $v$.
• Strong convexity is the gradient inequality printed on p. 10, with $\mu>0$; $\min\Phi$ is written $\Phi(x^*)$ with $x^*$ a minimizer.
• $t^p$ is the real power, only evaluated at $t\ge t_0>0$; $p$, $\lambda$, $t_1$ are named definitions shared by the milestones.
• $\mathcal O$ in (25) is Asymptotics.IsBigO along atTop; strong convergence is norm convergence. The existence and uniqueness of $x^*$ are conclusions of the goal, not hypotheses, so the goal cannot be satisfied vacuously by an empty argmin; the strong-convexity hypothesis is satisfiable (e.g. $\Phi=\|\cdot\|^2$ with $\mu=2$, and $x\equiv0$ solves (1)).
• Theorem numbers and pages are those of the Optimization Online preprint 5179 (October 2015), not of the journal typesetting.

Useful infrastructure: the derivative of $\Phi\circ x$ via gradient, integration of differential inequalities on $[t_0,+\infty[$, and existence of minimizers of strongly convex continuous functions on Hilbert spaces. Proofs of any milestone, and of the goal from the milestones, are welcome.

Selected references

• H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing damping, Optimization Online preprint 5179, 2015. https://optimization-online.org/wp-content/uploads/2015/10/5179.pdf
• H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Math. Program. 168 (2018), 123–175. https://doi.org/10.1007/s10107-016-0992-8
• W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, J. Mach. Learn. Res. 17 (2016). https://arxiv.org/abs/1503.01243
• Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Math. Dokl. 27 (1983), 372–376.

Motivation

Proximal gradient methods are used to minimize an objective with one smooth part and one convex part whose proximal map can be evaluated. A small proximal gradient step is a practical stopping signal, but it indicates proximity to an optimizer only when the objective has an appropriate error bound. Section 4 of Drusvyatskiy and Lewis gives conditions for that bound in the structured problem $f(Ax)+g(x)$: the conditions concern the dual problem and the growth of the two component functions, rather than requiring strong convexity of their sum. This matters for problems with a nontrivial solution set and for penalties that are not strongly convex. The paper places this result after its §3 comparison of quadratic growth and proximal gradient error bounds (pp. 9–11).

Setting

Let $E_n=\mathbb R^n$ and $E_m=\mathbb R^m$, with their Euclidean inner products and norms. Let $A:E_n\to E_m$ be linear, $f:E_m\to\mathbb R$ be continuously differentiable and convex, and $g:E_n\to(-\infty,+\infty]$ be proper, lower semicontinuous, and convex. The primal objective and its minimizer set are

$$\varphi(x)=f(Ax)+g(x),\qquad S=\operatorname*{argmin}_{x\in E_n}\varphi(x).$$

The mission assumes $S$ is nonempty and bounded. Its minimum $\varphi^*$ is finite. For an extended-real function $h$, its Fenchel conjugate is $h^*(v)=\sup_z\{\langle v,z\rangle-h(z)\}$. The dual objective is $\Psi(y)=f^*(y)+g^*(-A^\top y)$, and $\bar y$ denotes a dual minimizer. The effective domain is $\operatorname{dom}h=\{z:h(z)<+\infty\}$; $\operatorname{ri}$ denotes relative interior. The paper assumes dual nondegeneracy, $0\in A^\top(\operatorname{ri}\operatorname{dom}f^*)+\operatorname{ri}\operatorname{dom}g^*$, and dual strict complementarity, $0\in\operatorname{ri}\partial\Psi(\bar y)$ (p. 10).

A closed convex function $h$ is firmly convex relative to $v$ when its tilt $h_v(x)=h(x)-\langle v,x\rangle$ grows at least quadratically away from its minimizers on each compact set. The positive coefficient may depend on the compact set. Theorem 4.2 assumes this property for $f$ at $\bar y$ and for $g$ at $-A^\top\bar y$ (Definition 4.1, p. 11).

For $t>0$, a proximal gradient step is $p=\operatorname{prox}_{tg}(x-t\nabla(f\circ A)(x))$, and its residual is $G_t(x)=t^{-1}(x-p)$. The error bound asks whether the distance from $x$ to $S$ is controlled by $\|G_t(x)\|$ whenever $x$ lies below a prescribed objective threshold (Definition 3.1, p. 5).

Formalization targets

Component and composite growth

The milestone path records the Kuhn–Tucker description of $S$, the relative-interior identity (4.3), the compact-set distance estimate (4.4), the two component inequalities (4.5), and the resulting quadratic growth of $\varphi$ on every sublevel set. In particular, for each $\nu>0$ there is $\mu>0$ such that

$$\varphi(x)\ge\varphi^*+\mu\operatorname{dist}^2(x,S) \quad\text{if }\varphi(x)\le\varphi^*+\nu.$$

These are the claims stated in §4 and in the proof of Theorem 4.2, pp. 10–11. The milestone for (4.5) retains the paper's printed $c,\alpha\ge0$ in its quotation, while the Lean statement uses positive constants, as Definition 4.1 requires for nontrivial quadratic growth.

Goal: a proximal gradient error bound

The goal is Theorem 4.2: under the conditions above, for every $t>0$ there exist $\gamma,\nu>0$ such that

$$\operatorname{dist}(x,S)\le\gamma\|G_t(x)\| \quad\text{whenever }\varphi(x)\le\varphi^*+\nu.$$

The formal statement makes explicit that $\nabla f$ has a Lipschitz constant. This is part of the §3 setting used by the paper's Corollary 3.6 to reach the displayed error bound. A companion statement, Theorem 4.5, pp. 12–13, says that the Moreau envelope of a firmly convex function retains firm convexity relative to the same vector.

Significance

The conclusion converts dual geometric information and component growth into an error bound expressed through a proximal gradient step. The residual is available when running the method, whereas the distance to $S$ is generally not. Combined with the paper's §3 results, the error bound yields local convergence guarantees for the proximal gradient method in structured convex problems (Corollary 3.6 and Theorem 4.2). The statement covers settings in which component functions have local quadratic growth after a tilt while the composite objective need not be strongly convex.

The research result is proved in the paper. The work of this mission is to formalize its exact assumptions and claims, including the convex dual and the relative-interior statements, then supply machine-checked proofs. The resulting Euclidean conjugate, firm-convexity, and structured-objective definitions can also support other convex optimization formalizations. The statements in this proposal are proof obligations; compiling the statements alone does not establish the theorems.

Difficulty

Component growth concerns distance to separate subdifferential inverse images. The desired error bound concerns distance to their intersection, which is the primal solution set. Two small component distances do not automatically control distance to an intersection: the sets can meet at a poor angle. The dual interior hypotheses supply the regularity needed in (4.4). The argument also changes the quantity being controlled from objective growth to a proximal gradient residual. Those two changes are the substantive steps a proof must justify; treating either as an unrestricted distance identity would change the theorem.

Formalization scope

The Lean spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); dimensions zero are permitted. The linear map is continuous, and $A^\top$ is its adjoint. Extended-real values use EReal; properness excludes $-\infty$ values, and lower semicontinuity encodes closedness. Conjugates take suprema in EReal, and the dual objective follows (4.2). Relative interior is intrinsicInterior ℝ. The published convex subdifferential, proper-convex predicate, and proximal-point predicate are imported as reference items because their meanings match the paper's objects. The paper's Euclidean conjugate is defined locally because the available published conjugate has a strong-dual codomain.

The minimum value is real and is pinned to the nonempty primal minimizer set. The dual point is pinned as a minimizer of $\Psi$. Proximal steps are expressed as argmin predicates, so no default result is chosen for a failed minimization. The firm-convexity predicate requires a nonempty minimizer set of the tilted function: otherwise Lean's real distance to the empty set would be zero while the source uses an infinite distance. The growth constant $\alpha$ of Definition 4.1 and the constants $c,\alpha$ of (4.5) are strictly positive: the page leaves the sign implicit or prints $\ge 0$, but with a zero constant every convex function would be firmly convex, contradicting the page's own example $x^4$, and the growth statements would be empty. The error bound is restricted to the stated sublevel set, and all of its constants are positive. The goal includes a nonnegative Lipschitz constant for $\nabla f$, disclosed because the source's §3 bridge to the error bound assumes one; the component-growth milestones do not assume it.

Contributions should establish the Euclidean convex-duality identities, the compact-set regularity estimate, the component and composite growth claims, and the proximal gradient conclusion. The Moreau-envelope preservation theorem is a separate companion target. None of the dual interior conditions or the firm-convexity assumptions may be replaced by a vacuous condition: the goal concerns their effect on the actual solution set of $f(Ax)+g(x)$.

Selected references

• D. Drusvyatskiy and A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Mathematics of Operations Research 43(3), 2018. arXiv:1602.06661v2.

Motivation

Peaceman–Rachford splitting and its relaxed forms solve the problem of minimizing a sum $f+g$ by evaluating the two proximal maps separately. This is useful when minimizing either function by itself is simple while minimizing their sum directly is not. Douglas–Rachford splitting is the half-relaxed case. Davis and Yin study which properties of $f$ and $g$ turn the basic convergence of this iteration into quantitative rates. Their Theorem 2.1 supplies the regularity estimates used throughout their later objective and fixed-point analyses (Davis and Yin, arXiv:1407.5210v3, §§1–2).

The theorem measures progress using a term that can respond to strong convexity, a Lipschitz gradient, or both. Its conclusions distinguish three observations of the same run: the best iterate found so far, a weighted average of the auxiliary points, and the current iterate. This distinction matters because a rate for a best iterate need not hold for every iterate; the authors explicitly leave open whether their best-iterate conclusion can be improved in that way (Davis and Yin, p. 9).

Setting

Let $H$ be a real Hilbert space. The functions $f,g:H\to(-\infty,+\infty]$ are closed, proper, and convex. For a positive step size $\gamma$, the proximal map of $f$ sends $z$ to the unique minimizer of $f(x)+\|x-z\|^2/(2\gamma)$. Define the reflection $R_f=2\operatorname{prox}_{\gamma f}-I$ and likewise $R_g$. The Peaceman–Rachford map is $T_{\mathrm{PRS}}=R_f\circ R_g$. Given relaxation parameters $\lambda_k\in(0,1]$, Algorithm 1 generates

$$z^{k+1}=(1-\lambda_k)z^k+\lambda_kT_{\mathrm{PRS}}z^k.$$

At $z^k$, set $x_g^k=\operatorname{prox}_{\gamma g}(z^k)$ and $x_f^k=\operatorname{prox}_{\gamma f}(R_gz^k)$. These points may differ, so the theorem tracks them separately. Their selected proximal subgradients are $\widetilde\nabla g(x_g^k)=\gamma^{-1}(z^k-x_g^k)$ and $\widetilde\nabla f(x_f^k)=\gamma^{-1}(R_gz^k-x_f^k)$. The tilde means a particular member of a subdifferential when the function is not differentiable (Lemma 1.1, p. 7).

Suppose $z^*$ is a fixed point of $T_{\mathrm{PRS}}$ and put $x^*=\operatorname{prox}_{\gamma g}(z^*)$. Each function $h\in\{f,g\}$ has a nonnegative strong-convexity parameter $\mu_h$ and a nonnegative smoothness parameter $\beta_h$. If $\beta_h>0$, the function is differentiable and its gradient is $\beta_h^{-1}$-Lipschitz; a zero parameter imposes no such property. For the selected subgradients at $x$ and $y$, define the regularity term

$$S_h(x,y)=\max\left\{\frac{\mu_h}{2}\|x-y\|^2,\frac{\beta_h}{2}\|\widetilde\nabla h(x)-\widetilde\nabla h(y)\|^2\right\}.$$

The partial relaxation weight is $\Lambda_k=\sum_{i=0}^k\lambda_i$. All of these conventions are from the paper's notation, Algorithm 1, and equations (1.13)–(1.14) (Davis and Yin, pp. 3–8).

Formalization targets

One-step and summed bounds

The goal first asserts the exact one-step inequality (2.1):

$$8\gamma\lambda_k\bigl(S_f(x_f^k,x^*)+S_g(x_g^k,x^*)\bigr)\le \|z^k-z^*\|^2-\|z^{k+1}-z^*\|^2+ \left(1-\frac1{\lambda_k}\right)\|z^{k+1}-z^k\|^2.$$

It also asserts that $\sum_{i\ge0}\lambda_i(S_f(x_f^i,x^*)+S_g(x_g^i,x^*))$ converges and that eight times $\gamma$ times this sum is at most $\|z^0-z^*\|^2$. These are Theorem 2.1's common quantitative bounds (p. 8).

Best-iterate, ergodic, and nonergodic rates

If the $\lambda_j$ are bounded below by a positive constant, the minimum through $k$ of each regularity term is $o(1/(k+1))$. The weighted averages of $x_f^i$ and $x_g^i$, together with the matching weighted averages of their selected subgradients, have regularity terms whose sum is at most $\|z^0-z^*\|^2/(8\gamma\Lambda_k)$. Finally, if the products $\lambda_j(1-\lambda_j)$ have a positive lower bound, the sum of the two current regularity terms is $o(1/\sqrt{k+1})$ (Theorem 2.1, p. 9).

Significance

Strong convexity makes the regularity term control squared distance to $x^*$; a positive smoothness parameter makes it control the difference between selected gradients. Theorem 2.1 therefore connects properties of the objectives to rates for quantities produced by Algorithm 1. The one-step bound is also the stated input to later linear-convergence arguments in the same paper (§4, pp. 13–16). Without this result, those applications lack their common quantitative estimate.

The paper proves Theorem 2.1. This mission asks for a machine-checked proof of its precise statement and supporting claims, not for a new asymptotic rate. The proximal-map and subdifferential definitions already exist as published formal objects; the reusable remaining work includes their quantitative inequalities and the summable-sequence rate facts. The draft goal and milestones are theorem statements with proof holes and do not yet constitute verified proofs.

Difficulty

The obvious inference from a finite sum of nonnegative regularity terms gives a bound on cumulative error, but it does not directly give little-$o$ rates for the current term. The theorem also separates a best-iterate conclusion from a last-iterate conclusion: the regularity terms need not be monotone, and the stronger condition on $\lambda_j(1-\lambda_j)$ is required for the latter. The ergodic conclusion concerns weighted averages of both points and subgradients, so bounding only the average of pointwise regularity terms does not by itself state the result (Theorem 2.1 and its discussion, pp. 8–9).

Formalization scope

Lean uses EReal for the objectives, a complete real inner-product space for $H$, and published predicates for closed proper convex functions, proximal maps, and subgradients. A proximal map is supplied as a function satisfying the minimization property; uniqueness under the stated assumptions makes it the paper's map. Selected subgradients are fixed difference quotients from Lemma 1.1. The parameters $\mu_f,\beta_f,\mu_g,\beta_g$ are nonnegative, and positive $\beta$ requires a real-valued differentiable function with $\beta^{-1}$-Lipschitz gradient. A fixed point $z^*$ states the solution-existence assumption in the form used by Theorem 2.1. No hypothesis asserts any conclusion of the theorem.

The finite minimum uses the nonempty index range $0,\ldots,k$; little-$o$ uses Mathlib's asymptotic relation at infinity. The denominators $\lambda_k$, $\Lambda_k$, and $\sqrt{k+1}$ are positive under the stated bounds. In supporting objective inequalities, conversion from EReal to real numbers occurs only at proximal outputs and points with subgradients, where function values are finite. The printed unweighted, repeated-$k$ subgradient sum in the ergodic clause is corrected to the $\lambda_i$-weighted average consistent with the page's definition of $\bar x_f^k$ and with the result it states. Contributions proving the exact goal, any milestone, or reusable proximal and sequence lemmas are in scope.

Selected references

• Damek Davis and Wotao Yin, Faster convergence rates of relaxed Peaceman–Rachford and ADMM under regularity assumptions, Mathematics of Operations Research 42(3), 2017; preprint arXiv:1407.5210v3, 2015. arXiv · DOI

Motivation

A Kalman filter estimates the hidden state $x$ of a linear system from observations $y$, assuming the joint law of $z = (x, y)$ is a known Gaussian. When that law is only approximately known, Shafieezadeh-Abadeh, Nguyen, Kuhn and Mohajerin Esfahani (arXiv:1809.08830v3, NeurIPS 2018) replace it by the worst Gaussian within a 2-Wasserstein ball of radius $\rho$ around a nominal Gaussian with covariance $\Sigma$. Their Theorem 2.5 shows that the resulting minimax estimation problem is equivalent to a finite nonlinear semidefinite program, program (5), whose objective is $f(S) = \mathrm{Tr}[S_{xx} - S_{xy}S_{yy}^{-1}S_{yx}]$.

Each step of the robust filter solves program (5), so the filter is only practical if (5) can be solved quickly. The paper solves it with a Frank–Wolfe method (Algorithm 2), which avoids projections by replacing the objective with its linearization at the current iterate and maximizing that linear function over the original feasible set. That inner problem, the direction-finding subproblem, is again a nonlinear SDP. The paper's Algorithm 1 solves it by a one-dimensional bisection, and Theorem 3.2 states that this bisection returns a feasible solution whose objective value is within a prescribed tolerance $\varepsilon$ of the optimum. This mission formalizes that guarantee.

Setting

Fix dimensions $n \ge 1$ (state) and $m$ (observation), $d = n + m$, and index coordinates so that the first $n$ belong to $x$. Let $\mathbb{S}^d_+$ and $\mathbb{S}^d_{++}$ denote the positive semidefinite and positive definite $d\times d$ matrices, and $\langle A, B\rangle = \mathrm{Tr}[A^\top B]$ the trace inner product. The data are a nominal covariance $\Sigma \in \mathbb{S}^d_{++}$ with smallest eigenvalue $\underline\sigma = \lambda_{\min}(\Sigma)$, a radius $\rho > 0$, a tolerance $\varepsilon > 0$, and the current Frank–Wolfe iterate $S \in \mathbb{S}^d_+$, written in blocks $S_{xx}, S_{xy}, S_{yx}, S_{yy}$.

The gradient matrix is

$$D = \nabla f(S) = [I_n, -G]^\top [I_n, -G], \qquad G = S_{xy}S_{yy}^{-1},$$

which is positive semidefinite and nonzero. The direction-finding subproblem (7b) is

$$\max_{L \succeq \underline\sigma I_d}\ \langle L, D\rangle \quad \text{s.t.}\quad \mathrm{Tr}\Big[L + \Sigma - 2\big(\Sigma^{1/2} L \Sigma^{1/2}\big)^{1/2}\Big] \le \rho^2 ;$$

its constraint says that the Gaussian with covariance $L$ lies within Wasserstein distance $\rho$ of the nominal Gaussian, and $\mathcal F$ denotes its feasible set. For $\gamma$ with $\gamma I_d \succ D$ the paper defines

$$h(\gamma) = \rho^2 - \big\langle \Sigma, (I_d - \gamma(\gamma I_d - D)^{-1})^2\big\rangle, \qquad L(\gamma) = \gamma^2 (\gamma I_d - D)^{-1}\Sigma(\gamma I_d - D)^{-1},$$ $$\Delta(\gamma) = \gamma(\rho^2 - \mathrm{Tr}[\Sigma]) - \langle L(\gamma), D\rangle + \gamma^2\langle(\gamma I_d - D)^{-1}, \Sigma\rangle .$$

Algorithm 1 takes the largest eigenvalue $\lambda_1$ of $D$ and a unit eigenvector $v_1$, and starts from the bracket $[LB, UB] = [\gamma_{\min}, \gamma_{\max}]$ with

$$\gamma_{\min} = \lambda_1\big(1 + \sqrt{v_1^\top\Sigma v_1}/\rho\big), \qquad \gamma_{\max} = \lambda_1\big(1 + \sqrt{\mathrm{Tr}[\Sigma]}/\rho\big).$$

Each pass sets $\gamma = (UB + LB)/2$ and $L = L(\gamma)$, replaces $LB$ by $\gamma$ if $h(\gamma) < 0$ and $UB$ by $\gamma$ otherwise, and the loop exits with output $L$ as soon as $h(\gamma) > 0$ and $\Delta(\gamma) < \varepsilon$.

Formalization targets

Goal: Theorem 3.2

For all inputs as above:

1. Soundness. At every pass $k$ whose exit test holds, with trial point $\gamma_k$,

$$L(\gamma_k) \in \mathcal F \quad\text{and}\quad \langle L', D\rangle \le \langle L(\gamma_k), D\rangle + \varepsilon \ \text{ for all } L' \in \mathcal F .$$

2. Termination. If $h$ has no zero at a dyadic point $\gamma_{\min} + j(\gamma_{\max} - \gamma_{\min})/2^k$, $0 < j \le 2^k$, then some pass satisfies the exit test.

The termination hypothesis is a correction: the printed theorem asserts that the algorithm outputs a solution, but if a trial point (or $\gamma_{\max}$) coincides exactly with the root of $h$, the upper end of the bracket becomes that root, all later trial points have $h < 0$, and the loop never exits. Soundness holds unconditionally. The normalization $\|v_1\| = 1$ is also added; the page says only "an eigenvector", and $\gamma_{\min}$ is not a lower bound for a rescaled one.

Milestones (App. A.3, p. 13, in the order the proof uses them)

• $L(\gamma) \in \mathcal F$ whenever $\gamma I_d \succ D$ and $h(\gamma) > 0$.
• Weak duality: $\langle L', D\rangle \le \gamma(\rho^2 - \mathrm{Tr}[\Sigma]) + \gamma^2\langle (\gamma I_d - D)^{-1}, \Sigma\rangle$ for all $L' \in \mathcal F$ and $\gamma \ge 0$ with $\gamma I_d \succ D$.
• The suboptimality display: if $h(\gamma^\star) = 0$ then $\langle L(\gamma^\star) - L(\gamma), D\rangle \le \gamma(\rho^2 - \mathrm{Tr}[\Sigma]) + \gamma^2\langle(\gamma I_d - D)^{-1}, \Sigma\rangle - \langle L(\gamma), D\rangle$.
• Lemma A.3: every root $\gamma^\star$ of $h$ with $\gamma^\star I_d \succ D$ lies in $[\gamma_{\min}, \gamma_{\max}]$.

Significance

Theorem 3.2 is what makes Algorithm 1 a valid linear-maximization oracle for the Frank–Wolfe method on program (5): the convergence analysis of Frank–Wolfe with inexact oracles requires exactly a feasible point whose linearized objective is within a known tolerance of the optimum. It also shows that the inner problem, a semidefinite program with a matrix square root in the constraint, reduces to a scalar root-finding problem once $D$ is diagonalized, which is why the robust filter runs at a cost comparable to an eigendecomposition per step.

The result is proved in the paper; no machine-checked version exists. The formal version adds what the paper leaves implicit: the termination edge case, the normalization of $v_1$, and the requirement $D \ne 0$ (here $n \ge 1$). The milestone statements on Lagrangian weak duality for the Wasserstein–Gaussian trust region and on the location of the multiplier are reusable for other covariance-robust programs of the same shape, such as Wasserstein shrinkage estimation.

Difficulty

The algorithm is elementary; the analysis is not. Feasibility of $L(\gamma)$ requires computing the matrix square root $(\Sigma^{1/2}L(\gamma)\Sigma^{1/2})^{1/2}$ in closed form and comparing eigenvalues of non-commuting products to obtain $L(\gamma) \succeq \underline\sigma I_d$. The dual bound is a semidefinite Lagrangian duality statement over a constraint involving a matrix square root, whose inner supremum (Lemma A.1, cited from earlier work) must be evaluated in closed form. Termination needs monotonicity and continuity of $h$ on $(\lambda_1, \infty)$ and a careful account of which side of the root each bisection update lands on; the obvious invariant "the root stays strictly inside the bracket" fails precisely in the excluded dyadic case.

Formalization scope

Matrices are indexed by Fin n ⊕ Fin m with blocks toBlocks₁₁ ($xx$), toBlocks₁₂ ($xy$), toBlocks₂₂ ($yy$). The feasible set $\mathcal F$ is the published definition WassersteinDRO.Shrinkage.sdpFeasibleSet ρ Σ σ, which uses the published positive semidefinite square root psdSqrt. Mathlib's matrix inverse returns $0$ on singular matrices; every statement involving $h$, $L$ or $\Delta$ assumes $\gamma I_d \succ D$ or works at trial points that lie above $\lambda_1$, and $S_{yy}^{-1}$ is allowed to be this junk value because the theorem admits any $S \in \mathbb{S}^d_+$ (then $D = \mathrm{diag}(I_n, 0)$). The constants $\underline\sigma$ and $\lambda_1$ are passed as reals together with hypotheses that pin them to the smallest eigenvalue of $\Sigma$ and the largest eigenvalue of $D$. The algorithm is modelled as its sequence of passes, not as a function returning an output, so a non-terminating run cannot silently produce a value.

A formalization that defines the output with a fuel bound or a default value, that states only optimality of $L(\gamma^\star)$ at the exact root, or that assumes termination as a hypothesis would not be Theorem 3.2; $\varepsilon$-suboptimality is stated against every feasible point, not against a supremum that could be a junk value.

A complete development needs the spectral theorem for symmetric matrices, uniqueness of the positive semidefinite square root, and semidefinite Lagrangian duality; Mathlib supplies the first two. Proofs of the milestones are welcome contributions.

Selected references

• S. Shafieezadeh-Abadeh, V. A. Nguyen, D. Kuhn, P. Mohajerin Esfahani, Wasserstein Distributionally Robust Kalman Filtering, NeurIPS 2018; arXiv:1809.08830v3. https://arxiv.org/abs/1809.08830
• V. A. Nguyen, D. Kuhn, P. Mohajerin Esfahani, Distributionally Robust Inverse Covariance Estimation: The Wasserstein Shrinkage Estimator, Optimization Online, 2018; arXiv:1805.07194 (reference [18] of the paper; source of Lemma A.1). https://arxiv.org/abs/1805.07194
• M. Jaggi, Revisiting Frank–Wolfe: Projection-Free Sparse Convex Optimization, ICML 2013 (reference [13]; Frank–Wolfe with approximate oracles). https://proceedings.mlr.press/v28/jaggi13.html

Motivation

Nesterov's accelerated gradient method and its proximal variant FISTA minimize a smooth convex function with a value gap of order $O(1/k^2)$ after $k$ iterations, against $O(1/k)$ for plain gradient descent. They are among the most widely used first-order methods in large-scale optimization, signal processing and machine learning. Su, Boyd and Candès (JMLR 2016) observed that, for $\alpha = 3$, the second-order differential equation

$$\ddot x(t) + \frac{\alpha}{t}\,\dot x(t) + \nabla\Phi(x(t)) = 0 \tag{1}$$

is a continuous-time limit of Nesterov's scheme, and proved $\Phi(x(t)) - \min\Phi = O(1/t^2)$ for $\alpha \ge 3$. A rate on the values says nothing about the trajectory itself: whether $x(t)$ (or the iterates $x_k$) converges at all was a long-standing question. The paper of Attouch, Chbani, Peypouquet and Redont answers it for $\alpha > 3$: every trajectory of (1) converges weakly to a minimizer of $\Phi$.

Timeline:

• 1983 — Nesterov introduces the accelerated gradient method with an $O(1/k^2)$ rate on the values.
• 2000 — Alvarez proves weak convergence of the trajectories of the heavy ball with friction, $\ddot x + \gamma\dot x + \nabla\Phi(x) = 0$, whose damping is constant (SIAM J. Control Optim. 38).
• 2009 — Beck and Teboulle extend it to composite problems (FISTA), still with a rate on the values only.
• 2014–2016 — Su, Boyd, Candès identify (1) as the continuous model of Nesterov's method and prove the $O(1/t^2)$ rate for $\alpha\ge3$.
• 2015 — Attouch, Chbani, Peypouquet, Redont prove weak convergence of the trajectories of (1) for $\alpha > 3$ (this mission), and of the iterates of the corresponding algorithms; Chambolle and Dossal obtain the discrete result independently. The case $\alpha = 3$ remains open.

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$, and let $\Phi:\mathcal H\to\mathbb R$ be a continuously differentiable convex function with gradient $\nabla\Phi$. Fix a damping parameter $\alpha>0$ and an initial time $t_0>0$. A solution of (1) on $[t_0,+\infty[$ is a pair of maps $x, v$ from the time axis to $\mathcal H$ such that, at every $t\ge t_0$, $x$ has derivative $v(t)$ and $v$ has derivative $-\frac{\alpha}{t}v(t) - \nabla\Phi(x(t))$. So $v=\dot x$, and $\ddot x$ satisfies (1). The damping coefficient $\alpha/t$ is singular at $0$ and vanishes as $t\to+\infty$; this is why the time origin is positive.

Three functions of time measure the progress of a solution:

• the global energy $W(t) = \frac12\|\dot x(t)\|^2 + \Phi(x(t))$;
• the anchored distance $h_z(t) = \frac12\|x(t)-z\|^2$ to a point $z\in\mathcal H$;
• when $\Phi$ has a minimizer $x^*$, the anchored energies, for $\lambda,\xi\ge0$,

$$\mathcal E_{\lambda,\xi}(t) = t^2\big(\Phi(x(t))-\min\Phi\big) + \tfrac12\|\lambda(x(t)-x^*) + t\dot x(t)\|^2 + \tfrac{\xi}{2}\|x(t)-x^*\|^2 .$$

$x(t)$ converges weakly to $\bar x$ as $t\to+\infty$ if $\langle x(t),y\rangle\to\langle\bar x,y\rangle$ for every $y\in\mathcal H$. A weak limit point of $x(t)$ is the weak limit of a sequence $x(s_n)$ with $s_n\to+\infty$. $\operatorname{argmin}\Phi$ is the set of minimizers of $\Phi$.

Formalization targets

Goal: Theorem 2.16

If $\operatorname{argmin}\Phi\ne\emptyset$ and $\alpha>3$, then for every solution $x$ of (1) there is $\bar x\in\operatorname{argmin}\Phi$ with

$$x(t)\rightharpoonup\bar x\qquad(t\to+\infty).$$

The goal asserts only the qualitative conclusion; no rate or constant enters it.

Milestones

1. Lemma 2.1 (energy dissipation): $\dot W(t) = -\frac{\alpha}{t}\|\dot x(t)\|^2$ for $t>t_0$; $W$ is nonincreasing with a limit in $\mathbb R\cup\{-\infty\}$, finite when $\Phi$ is bounded below.
2. (7): $\ddot h_z(t) + \frac{\alpha}{t}\dot h_z(t) + \Phi(x(t)) - \Phi(z) \le \|\dot x(t)\|^2$.
3. Lemma 2.2: $\int_{t_0}^t \frac1s(W(s)-\Phi(z))\,ds \le C - \frac1t\dot h_z(t) - \frac{3}{2\alpha}W(t)$ with an explicit constant $C$.
4. Theorem 2.3 i), ii) (minimizing property, every $\alpha>0$): $\lim W(t) = \lim \Phi(x(t)) = \inf\Phi\in\mathbb R\cup\{-\infty\}$, and every weak limit point of $x(t)$ is a minimizer.
5. Remark 2.6: the Lyapunov inequality for $\frac{d}{dt}\mathcal E_{\lambda,\xi}$, and monotonicity of $\mathcal E_{\lambda,\lambda(\alpha-\lambda-1)}$ for $\alpha\ge3$, $2\le\lambda\le\alpha-1$.
6. Theorem 2.14 ii) with (13), (15): for $\alpha>3$, $\|x(t)-x^*\|^2 \le \mathcal E_{2,2(\alpha-3)}(t_0)/(\alpha-3)$ and $\int_{t_0}^{\infty} t\|\dot x(t)\|^2\,dt \le \mathcal E_{2,2(\alpha-3)}(t_0)/(\alpha-3)$.
7. Lemma A.4: if $t\ddot w + \alpha\dot w \le g$ a.e. with $\alpha>1$, $g\ge0$ integrable and $w$ bounded below, then $[\dot w]_+$ is integrable and $\lim w(t)$ exists.
8. Lemma A.2 (Opial's lemma, continuous form).

Significance

The result. Theorem 2.16 is the first proof that the trajectories of the continuous Nesterov model converge, not only their values. The paper's discrete analysis parallels the continuous one and yields weak convergence of the iterates of Nesterov-type forward–backward algorithms for $\alpha>3$ (Theorem 5.3, a companion mission). The minimizing property (Theorem 2.3) holds for every $\alpha>0$, with no minimizer assumed, and shows that a bounded trajectory exists only if $\Phi$ has a minimizer. Strong convergence results under further geometric assumptions (Theorems 3.1–3.3) build directly on Theorem 2.16.

Formalizing it. All statements are proved on paper. None of them, nor the differential equation (1), is formalized on Prove2Me or in Mathlib; the discrete analogue (weak convergence of the unperturbed accelerated forward–backward iterates) exists on the platform as a separate result. A formal development provides: a reusable encoding of solutions of a non-autonomous second-order ODE in a Hilbert space; Lyapunov arguments with one-sided derivatives on a half-line; a continuous-time Opial lemma, which is the standard tool for weak convergence of evolution equations and of semigroups; and the scalar differential-inequality lemma A.4.

Difficulty

Lyapunov functions such as $W$ or $\mathcal E_{\alpha-1,0}$ give rates on the values but not convergence of $x(t)$: a decreasing energy says nothing about where the trajectory goes, and the minimizer set may be a continuum. The natural first idea, showing that $\|x(t)-x^*\|$ is eventually monotone as for the gradient flow, fails: the inertial term makes $h_{x^*}$ oscillate, and (7) controls only $t\ddot h + \alpha\dot h$, a second-order quantity. Making it usable requires integrability of $t\|\dot x(t)\|^2$ on $[t_0,+\infty[$, which is not available from the Su–Boyd–Candès energy and holds only for $\alpha>3$; the borderline $\alpha=3$ is open. In infinite dimension, convergence is genuinely weak: bounded sets are not compact, so the argument must identify weak limit points through weak lower semicontinuity of $\Phi$ and conclude through Opial's lemma.

Formalization scope

• Space. $\mathcal H$ is a real inner product space that is complete (InnerProductSpace ℝ H, CompleteSpace H); no finite dimension is assumed, since in finite dimension weak and norm convergence coincide.
• Potential. $\Phi:\mathcal H\to\mathbb R$ with ConvexOn ℝ Set.univ Φ and ContDiff ℝ 1 Φ; $\nabla\Phi$ is Mathlib's gradient. Minimizers are points $z$ with $\Phi(z)\le\Phi(y)$ for all $y$; $\min\Phi$ is written $\Phi(x^*)$ for such a point.
• Solutions. (1) is the first-order system $\dot x=v$, $\dot v=-\frac{\alpha}{t}v-\nabla\Phi(x)$, with derivatives within $[t_0,+\infty[$ at every $t\ge t_0$ and $t_0>0$. Existence of solutions is not assumed or proved: every statement concerns a given solution, as in the paper.
• Limits and integrals. Limits in $\mathbb R\cup\{-\infty\}$ are taken in EReal, $\inf\Phi$ as an EReal infimum. Improper integrals $\int_{t_0}^{+\infty}$ carry an explicit integrability conjunct; integrals over $[t_0,t]$ are interval integrals of continuous functions.
• Explicit constants. The constant $C$ of Lemma 2.2 and the bounds $\mathcal E_{2,2(\alpha-3)}(t_0)/(\alpha-3)$ of (13), (15) are stated exactly as the paper computes them.
• Trivializations ruled out. Weak convergence is not replaced by norm convergence, the derivative relations between $x$, $v$ and their energies are part of the hypotheses or conclusions (never a free deriv), and the solution predicate is non-vacuous: the constant trajectory for $\Phi=0$ and the explicit solution $x(t)=t^2$ of Example 2.5 satisfy it.
• Citation. Theorem numbers and pages refer to the Optimization Online preprint 5179 (October 2015), titled "…asymptotic vanishing damping", not to the Mathematical Programming typesetting.

Contributions of reusable infrastructure are welcome, in particular a continuous-time Opial lemma, weak lower semicontinuity of continuous convex functions on a Hilbert space along weakly convergent sequences, and integration-by-parts lemmas for one-sided derivatives on a half-line.

Selected references

• H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing damping, Optimization Online preprint 5179, 2015; published as …vanishing viscosity, Mathematical Programming 168 (2018) 123–175. https://optimization-online.org/wp-content/uploads/2015/10/5179.pdf, https://doi.org/10.1007/s10107-016-0992-8
• W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, Journal of Machine Learning Research 17 (2016) 1–43. https://jmlr.org/papers/v17/15-084.html
• F. Alvarez, On the minimizing property of a second order dissipative system in Hilbert spaces, SIAM Journal on Control and Optimization 38 (2000) 1102–1119. https://doi.org/10.1137/S0363012998335802
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bulletin of the AMS 73 (1967) 591–597. https://doi.org/10.1090/S0002-9904-1967-11761-0
• A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM Journal on Imaging Sciences 2 (2009) 183–202. https://doi.org/10.1137/080716542
• A. Chambolle, Ch. Dossal, On the convergence of the iterates of the "fast iterative shrinkage/thresholding algorithm", Journal of Optimization Theory and Applications 166 (2015) 968–982. https://doi.org/10.1007/s10957-015-0746-4