Convex Optimization

Motivation

Matrix completion asks for a low-rank matrix from a small random subset of its entries. It models collaborative filtering (recommendation systems), sensor-network localisation, and structure from motion. In practice the revealed entries are corrupted by noise, and the most widely used estimator is nuclear-norm regularized least squares: fit the observed entries in squared error while penalizing the sum of singular values. The estimator is a convex program, so it is solved reliably by proximal and singular-value-thresholding methods, and it needs no knowledge of the rank.

Its statistical accuracy was not understood. In the noiseless case, convex relaxation recovers the matrix exactly from nearly the information-theoretic minimum number of samples (Candès–Recht 2009, Candès–Tao 2010, Gross 2011). With noise, the available bounds for the plain convex program (Candès–Plan 2010) give $\|Z_{\rm cvx}-M^\star\|_F\lesssim\sigma n^{3/2}$ under random noise. That can be a factor of order $\sqrt{n^2p}$ above the oracle lower bound, and the numerical performance of the program is far better. Sharper rates were known only for modified estimators: Negahban–Wainwright 2012 add a spikiness constraint, Koltchinskii–Lounici–Tsybakov 2011 use a different estimator. In 2019, Chen, Chi, Fan, Ma and Yan (arXiv:1902.07698; SIAM J. Optim. 30(4), 2020, doi:10.1137/19M1290000) showed that the unmodified convex program attains near-optimal error in the Frobenius, entrywise and spectral norms simultaneously. Their argument goes through nonconvex gradient descent. This mission formalizes that theorem.

Setting

The unknown matrix is $M^\star\in\mathbb R^{n\times n}$ of rank $r\ge1$, with singular value decomposition $M^\star=U^\star\Sigma^\star V^{\star\top}$. The columns of $U^\star,V^\star\in\mathbb R^{n\times r}$ are orthonormal, and $\Sigma^\star=\mathrm{diag}(\sigma^\star_1,\dots,\sigma^\star_r)$ with $\sigma_{\max}=\max_k\sigma^\star_k$, $\sigma_{\min}=\min_k\sigma^\star_k>0$ and condition number $\kappa=\sigma_{\max}/\sigma_{\min}$. Write $\|A\|_{2,\infty}$ for the largest Euclidean norm of a row of $A$. $M^\star$ is $\mu$-incoherent if $\|U^\star\|_{2,\infty}\le\sqrt{\mu r/n}$ and $\|V^\star\|_{2,\infty}\le\sqrt{\mu r/n}$ (Definition 1). Incoherence says that the energy of $M^\star$ is not concentrated on a few rows or columns.

Under Assumption 1, each index $(i,j)$ enters the observed set $\Omega$ independently with probability $p$. One observes $M_{ij}=M^\star_{ij}+E_{ij}$ for $(i,j)\in\Omega$, where the $E_{ij}$ are i.i.d., zero-mean, and have sub-Gaussian norm $\|E_{ij}\|_{\psi_2}=\sup_{q\ge1}q^{-1/2}(\mathbb E|E_{ij}|^q)^{1/q}\le\sigma$. Let $\mathcal P_\Omega$ keep the entries indexed by $\Omega$ and zero the rest. The convex estimator is any minimizer $Z_{\rm cvx}$ of

where $\|Z\|_*$ is the nuclear norm, $\|\cdot\|$ is the spectral norm and $\|\cdot\|_\infty$ is the largest absolute entry.

Formalization targets

Goal: Theorem 2

Suppose $n^2p\ge C\kappa^4\mu^2r^2n\log^3n$ and $\sigma\sqrt{n/p}\le c\,\sigma_{\min}/\sqrt{\kappa^4\mu r\log n}$. Then with probability $1-O(n^{-3})$, every minimizer of (3) satisfies

Every best rank-$r$ approximation $Z_{{\rm cvx},r}$ is within $n^{-3}\frac\sigma{\sigma_{\min}}\sqrt{n/p}\,\|M^\star\|$ of $Z_{\rm cvx}$ in Frobenius norm, and satisfies the same three bounds.

Milestones

1. Deterministic layer: Lemma 20 (balancing an SVD factorization), Claim 3, Claim 2 and Lemma 2. Lemma 2 says that a point $(X,Y)$ with $\|\nabla f(X,Y)\|_F\le c\frac{\sqrt{c_{\rm inj}p}}{\kappa}\frac\lambda p\sqrt{\sigma_{\min}}$ for the factored objective

satisfies $\|XY^\top-Z_{\rm cvx}\|_F\le2304\,\frac{\kappa}{c_{\rm inj}\sqrt{\sigma_{\min}}}\|\nabla f(X,Y)\|_F$ under Conditions 1–2. 2. Probabilistic layer: Lemma 3 (Condition 1(a)), Lemma 19, Lemmas 7 and 8, and Lemma 4. Lemma 4 gives Conditions 1(b) and 2 uniformly over an $\ell_{2,\infty}$ neighbourhood of the truth. 3. Algorithmic layer: Lemma 5, the error bounds and the small-gradient iterate of gradient descent started at the truth, and (31), its consequence for $X^tY^{t\top}-M^\star$.

Significance

The bounds of Theorem 2 match the minimax lower bounds up to logarithmic factors when $r$ and $\kappa$ are bounded. This holds in all three norms and for noise of any size below a threshold. The theorem also shows that the convex solution is nearly of rank $r$. Neither statement requires modifying the estimator, so practitioners running standard solvers get the guarantee as is. The entrywise bound (11b) shows an implicit regularization: the convex program spreads its error over all entries without being told to.

The theorem has a complete published proof. What this mission adds is a machine-checked version, which has value of its own here. The proof chains about twenty lemmas, including a leave-one-out analysis of gradient descent with polynomially many iterations. Its constants are hidden behind "$\lesssim$" at nearly every step. The formal development fixes the quantifier order of every such constant. It also records the hypotheses the proof uses without stating them, such as the independence of the sampling pattern from the noise. No part of this paper has been formalized before. The deterministic layer (Lemmas 20, 2, Claims 2–3) applies to any Burer–Monteiro factorization of a nuclear-norm problem, not only to this one.

Difficulty

The obvious approach is to analyse the convex program directly through a dual certificate, as in the noiseless theory. With noise there is no exact recovery, and the certificate approach loses a factor polynomial in $n$. The difficulty is to transfer statistical bounds from a point one can control, the nonconvex iterate, to a point one cannot construct, the convex minimizer. The two are compared through an approximate first-order condition. That comparison is useful only if injectivity and concentration hold uniformly over all factor pairs near the truth, because the iterates depend on $\Omega$ and on the noise. A fixed-tangent-space injectivity bound, the usual tool, does not suffice. The entrywise control of the iterates requires leave-one-out sequences, and those sequences make up most of the appendix.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ and factors Matrix (Fin n) (Fin r) ℝ, using the published matrix_completion_basic, _svd and _tangent definitions (nuclear norm, SVD data, $\mathcal P_\Omega$, $\mathcal P_T$, spectral, Frobenius and entrywise norms). $M^\star$ comes with an explicit SVD with $r\ge1$ positive singular values, so its rank is exactly $r$. Definition 1 is MatrixCompletion.A0. The sub-Gaussian bound is the moment form of [Ver12, Definition 5.7] above, not Mathlib's MGF form. The randomness lives on an arbitrary probability space. The sampling indicators and the noise entries are each mutually independent, and the two families are independent of each other. This last independence is an added hypothesis, which the paper's proofs use. "With probability $1-O(n^{-k})$" is stated as an outer-measure bound $C_{\rm fail}n^{-k}$ on the failure event. Every unnamed constant ("$\lesssim$", "sufficiently large $C$", "sufficiently small $c$") is an existential placed before $n$ and all data, together with an $n_0$. Explicit constants of the paper are kept: the exponents $-3$ and $-10$, $\lambda/8$, $1/(32\kappa)$, $72\kappa$, $8\sqrt\kappa$, $t_0=n^{18}$, $n^{-5}$, the factors $3$ in (31), the $1/n^3$ in (12), and $2304=32\cdot72$ in Lemma 2.

The goal keeps the randomness in the statement. A version with fixed $\Omega$ and $E$ that assumes Conditions 1–2 or the conclusions of Lemma 5 would be Lemma 2 plus (31), not Theorem 2, and is not acceptable as a proof of the goal. The goal quantifies over every minimizer of (3) and every best rank-$r$ approximation. Excluded: Theorem 1 (the $r,\kappa=O(1)$ corollary), the noise condition of Remark 4, approximate minimizers (Remark 6), Lemmas 1 and 6, and the internal lemmas of the leave-one-out analysis (App. D), which solvers may add as supporting theorems. The development needs nuclear-norm subgradients, Weyl's inequality, matrix Bernstein and spectral-norm bounds for sparse random matrices. These are reusable well beyond this mission, and contributions of them are welcome. Theorem and equation numbers are those of the authors' preprint (Sep. 2019, arXiv:1902.07698) and may differ in the SIAM typesetting.

Selected references

• Y. Chen, Y. Chi, J. Fan, C. Ma, Y. Yan, Noisy Matrix Completion: Understanding Statistical Guarantees for Convex Relaxation via Nonconvex Optimization, SIAM J. Optim. 30(4), 2020. https://doi.org/10.1137/19M1290000 (preprint: https://arxiv.org/abs/1902.07698)
• E. J. Candès, B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9, 2009. https://doi.org/10.1007/s10208-009-9045-5
• E. J. Candès, Y. Plan, Matrix Completion With Noise, Proc. IEEE 98(6), 2010. https://doi.org/10.1109/JPROC.2009.2035722
• S. Negahban, M. J. Wainwright, Restricted strong convexity and weighted matrix completion: optimal bounds with noise, J. Mach. Learn. Res. 13, 2012. https://jmlr.org/papers/v13/negahban12a.html
• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, Ann. Statist. 39(5), 2011. https://doi.org/10.1214/11-AOS894
• C. Ma, K. Wang, Y. Chi, Y. Chen, Implicit Regularization in Nonconvex Statistical Estimation, Found. Comput. Math. 20, 2020. https://doi.org/10.1007/s10208-019-09429-9
• R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, CUP, 2012. https://arxiv.org/abs/1011.3027

Motivation

Distributionally robust optimization (DRO) chooses a decision $\theta$ that minimizes the expected loss under the worst distribution in an ambiguity set $\mathcal K$ of plausible distributions, $\min_\theta\sup_{P\in\mathcal K}\int l(\theta,\xi)\,dP(\xi)$. It sits between stochastic optimization, which trusts a single distribution, and worst-case robust optimization, which trusts none. The inner supremum is a problem of moments, studied since Stieltjes and made computable by duality (Isii 1962; Shapiro 2001; Bertsimas and Popescu 2005). Existing tractable reformulations require the ambiguity set to be described by finitely many moments, a $\phi$-divergence or a Wasserstein ball, and they usually require a structural property of the loss: affine or quadratic form, or a known Lipschitz constant.

Zhu, Jitkrittum, Diehl and Schölkopf (AISTATS 2021; arXiv:2006.06981) describe the ambiguity set through kernel mean embeddings: a distribution is represented by its mean in a reproducing kernel Hilbert space, and the ambiguity set is the set of distributions whose embedding lies in a convex set $\mathcal C$ of that space. Moment sets, MMD balls, scenario polytopes and the whole space (worst-case RO) all arise for suitable kernels and sets $\mathcal C$. Their Generalized Duality Theorem (Theorem 3.1) turns the inner worst-case problem into a minimization over a function of the RKHS that majorizes the loss, with no assumption on the loss beyond upper semicontinuity.

Setting

Let $\mathcal X$ be a compact metric space (in the paper, a compact $\mathcal X\subset\mathbb R^d$) with its Borel $\sigma$-algebra, and $\mathcal P$ the set of Borel probability measures on $\mathcal X$. Let $\mathcal H$ be a real Hilbert space and $\varphi:\mathcal X\to\mathcal H$ a continuous feature map; $k(x,y)=\langle\varphi(x),\varphi(y)\rangle_{\mathcal H}$ is then a continuous positive definite kernel, and an element $f\in\mathcal H$ acts on $\mathcal X$ by the reproducing property $f(\xi)=\langle f,\varphi(\xi)\rangle_{\mathcal H}$ (rkhsEval).

• The mean embedding of $P\in\mathcal P$ is $\mu_P=\int\varphi\,dP\in\mathcal H$ (meanEmbedding).
• For $\mathcal C\subseteq\mathcal H$, the ambiguity set is $\mathcal K_{\mathcal C}=\{P\in\mathcal P:\mu_P\in\mathcal C\}$ (ambiguitySet).
• The support function of $\mathcal C$ is $\delta^*_{\mathcal C}(f)=\sup_{\mu\in\mathcal C}\langle f,\mu\rangle_{\mathcal H}\in[-\infty,\infty]$ (supportFun).
• A loss is a function $l:\Theta\times\mathcal X\to[-\infty,\infty)$, where $\Theta$ is an arbitrary set of decisions; $\int l\,dP$ is the extended-real expectation.

For fixed $\theta$ (written $l=l(\theta,\cdot)$), the primal inner problem (11) and the dual inner problem (12) are

(primalValue, dualValue, with the constraint IsDualFeasible). Assumption 3.1 of the paper asks that each $l(\theta,\cdot)$ be proper (not identically $-\infty$) and upper semicontinuous, that $\mathcal C$ be closed and convex, and that $\mathrm{ri}(\mathcal K_{\mathcal C})\neq\emptyset$.

The PDF prints no page numbers; every page cited in this mission is the PDF page of arXiv:2006.06981v3.

Formalization targets

Goal: Theorem 3.1 (Generalized Duality), p. 5

Under the hypotheses above, with $\mathcal K_{\mathcal C}\ne\emptyset$,

and consequently $\mathrm{(P)}=\inf_\theta\mathrm{(P)}_\theta=\inf_\theta\mathrm{(D)}_\theta=\mathrm{(D)}$, the equality of the Kernel DRO problem (2) and its dual (4).

Milestones (the proof of Proposition A.1, pp. 13–15, and Appendix D, pp. 22–23)

1. The reproducing identity $\int f\,dP=\langle f,\mu_P\rangle_{\mathcal H}$ (p. 13).
2. Lemma D.1: $\int(l-f_0-f)\,dP\le0$ for all $P$ iff $l\le f_0+f$ on $\mathcal X$.
3. Weak duality: $\int l\,dP\le f_0+\delta^*_{\mathcal C}(f)$ for $P\in\mathcal K_{\mathcal C}$ and feasible $(f_0,f)$ (p. 6).
4. Lemmas D.2–D.4: $\mathcal T(\mathcal P)=\{\mu_P\}$, $\mathcal C\cap\mathcal T(\mathcal P)$ and $\mathcal K_{\mathcal C}$ are compact.
5. Primal attainment (p. 15), via the upper semicontinuity of $P\mapsto\int l\,dP$ (a supporting lemma the paper uses without stating).
6. The separation (14), the sign $\tau<0$ with the rescaled dual feasible point, and $\mathrm{(D)}\le\mathrm{(P)}+\epsilon$ (p. 15).
7. Proposition A.1: $\mathrm{(P)}_\theta=\mathrm{(D)}_\theta$ (p. 13).

Companions

Lemma A.2 (complementarity (19)), Corollary 3.1.3 (the optimal majorant interpolates $l$ $P^*$-a.e.), the support function $\frac1N\sum_i f(\xi_i)+\epsilon\|f\|_{\mathcal H}$ of the RKHS norm ball (Table 1), and the weak-duality content of Corollary 3.1.1 for integral probability metrics.

Significance

The theorem replaces an optimization over probability measures by a semi-infinite program over $(f_0,f)\in\mathbb R\times\mathcal H$, whose objective is explicit for the common choices of $\mathcal C$ (Table 1). The majorant $f_0+f$ needs no Lipschitz constant and no parametric form of the loss, and the dual variable $f^*$ doubles as a witness function for the MMD. This is the basis of the paper's batch and stochastic functional gradient algorithms, and it places moment-based DRO, scenario optimization, MMD-ball DRO and worst-case RO in one framework.

The result is proved on paper; it has no machine-checked proof that we know of. Formalizing it builds the duality theory of moment problems with infinitely many moment constraints, on top of Mathlib's Hilbert spaces, Bochner integrals and the weak topology on probability measures. The formal statements also fix points the paper leaves loose: the infimum in place of the printed "min", the reading of the Slater condition, and the role of the continuity of the kernel.

Difficulty

Weak duality is a two-line computation. The work is strong duality. The paper's route separates the cone $A=\{(\int1\,dP,\int\varphi\,dP,\int l\,dP):P\in\mathrm{co}(\mathcal P)\}$ from $B_\epsilon=\{(1,\mu,t+\epsilon):\mu\in\mathcal C\}$ in $\mathbb R\times\mathcal H\times\mathbb R$. A Hahn–Banach strict separation needs one set compact or the two at positive distance, and $A$ is neither obviously closed nor bounded. The step goes through only because $\mathcal K_{\mathcal C}$ is compact in the weak topology and $P\mapsto\int l\,dP$ is upper semicontinuous, which also gives primal attainment and the sign $\tau<0$. The loss may take the value $-\infty$, so every expectation lives in $[-\infty,\infty)$. The infinite primal case also needs an argument of its own.

Formalization scope

• $\mathcal X$ is a compact metric space with a Borel $\sigma$-algebra; a compact subset of $\mathbb R^d$ is an instance. $\mathcal P$ is ProbabilityMeasure X with its topology of weak convergence; the paper's MMD topology agrees with it for a universal continuous kernel.
• The RKHS is in feature-map form: a real Hilbert space $\mathcal H$ and a continuous $\varphi$. Continuity of the kernel is not written in Assumption 3.1 but is used by Appendix D.
• Losses are X → EReal, upper semicontinuous, never $+\infty$, and not identically $-\infty$. Expectations use the published definition WassersteinDRO.Duality.erealExpectation, which for such losses is the usual $\int l\,dP\in[-\infty,\infty)$.
• Support function, primal and dual values are extended reals. $\delta^*_\emptyset=-\infty$; $\delta^*_{\mathcal H}(f)=+\infty$ for $f\ne0$; an empty ambiguity set gives primal value $-\infty$; an infeasible dual gives $+\infty$. The sum $f_0+\delta^*_{\mathcal C}(f)$ adds a real to an extended real, so $+\infty+(-\infty)$ never occurs.
• The Slater clause $\mathrm{ri}(\mathcal K_{\mathcal C})\ne\emptyset$ names no topology on measures and is used only to obtain a primal solution (p. 15). It is read as $\mathcal K_{\mathcal C}\ne\emptyset$, which it implies under any reading, so the formal goal is at least as strong as the paper's.
• Every printed "min" is read as an infimum. Dual attainment is not proved and can fail: for $\mathcal X=[0,1]$, $\varphi(x)=x$, $\mathcal C=(-\infty,0]$ and $l(x)=\sqrt x$, the dual infimum $0$ is not attained.
• The dual variable ranges over $\mathcal H$, never over arbitrary functions on $\mathcal X$. Over all bounded functions, the choice $f=l$ would make the duality trivial (Example 3.3). The goal is also not closed by unfolding: for $\mathcal C=\mathcal H$ it says $\sup_P\int l\,dP=\sup_\xi l(\xi)$, worst-case RO.
• Corollary 3.1.2 (p. 6) is not stated: it is false under Assumption 3.1 alone (for $\mathcal C=\mathcal H$ and $l=\mathbf 1_{\{0\}}$, (2) equals $1$ while (6) equals $0$).

Reusable pieces: the kernel mean embedding and its continuity on ProbabilityMeasure X, compactness of RKHS ambiguity sets, and the upper semicontinuity of $P\mapsto\int l\,dP$ for upper semicontinuous $l$ (a portmanteau-type fact not yet in Mathlib). Proofs of any milestone are welcome. So are support-function computations for the other rows of Tables 1 and 3.

Selected references

• J.-J. Zhu, W. Jitkrittum, M. Diehl, B. Schölkopf, Kernel Distributionally Robust Optimization: Generalized Duality Theorem and Stochastic Approximation, AISTATS 2021 (PMLR 130); cited here as arXiv:2006.06981v3, 2021. https://arxiv.org/abs/2006.06981
• A. Shapiro, On duality theory of conic linear problems, in Semi-Infinite Programming, Kluwer, 2001. https://doi.org/10.1007/978-1-4757-3403-4_7
• K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14, 1962. https://doi.org/10.1007/BF02868641
• D. Bertsimas, I. Popescu, Optimal inequalities in probability theory: a convex optimization approach, SIAM Journal on Optimization 15(3), 2005. https://doi.org/10.1137/S1052623401399903
• A. Gretton, K. Borgwardt, M. Rasch, B. Schölkopf, A. Smola, A kernel two-sample test, Journal of Machine Learning Research 13, 2012. https://jmlr.org/papers/v13/gretton12a.html
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050

Motivation

Many problems in signal processing, statistics and machine learning take the form $\min_x \Phi(x)+\Psi(x)$, where $\Psi$ is smooth and $\Phi$ is convex but nonsmooth (a norm, the indicator of a constraint set). The forward-backward method takes a gradient step on $\Psi$ followed by a proximal step on $\Phi$. Its accelerated, inertial version — FISTA of Beck and Teboulle, built on Nesterov's method — reaches the rate $O(1/k^2)$ for the objective values. In practice the gradient or the proximal step is computed only approximately, so it matters whether the accelerated method survives errors, and whether its iterates converge at all, not only its objective values.

• 1983–2009. Nesterov introduces the accelerated gradient method with rate $O(1/k^2)$; Güler extends it to proximal steps; Beck and Teboulle publish FISTA (SIAM J. Imaging Sci. 2009). Convergence of the FISTA iterates themselves remains open.
• 2011. Schmidt, Le Roux and Bach show that the $O(1/k^2)$ value rate of accelerated proximal-gradient methods persists under errors that decay fast enough (NeurIPS 2011).
• 2014–2015. Su, Boyd and Candès read Nesterov's scheme as a discretization of $\ddot x+\frac{\alpha}{t}\dot x+\nabla\Phi(x)=0$ (JMLR 2016). Chambolle and Dossal prove weak convergence of the iterates when the inertial coefficient is $\frac{k-1}{k+\alpha-1}$ with $\alpha>3$, without errors (JOTA 2015).
• 2015. Attouch, Chbani, Peypouquet and Redont (this source) treat the dynamics and the algorithm together, and prove value rates and weak convergence of the iterates for the version with errors.

Setting

Let $\mathcal H$ be a real Hilbert space. Let $\Phi:\mathcal H\to\mathbb R\cup\{+\infty\}$ be proper, lower semicontinuous and convex, and let $\Psi:\mathcal H\to\mathbb R$ be convex and continuously differentiable, with gradient $\nabla\Psi$ Lipschitz continuous with constant $L$. Write $\Theta=\Phi+\Psi$ and $S=\operatorname{argmin}\Theta$.

The proximal map of $s\Phi$ ($s>0$) sends $x$ to the unique minimizer of $\xi\mapsto\Phi(\xi)+\frac1{2s}\|\xi-x\|^2$.

Fix $\alpha>0$, a step $s$ with $0<s<1/L$, and perturbations $g_k\in\mathcal H$. The perturbed inertial forward-backward algorithm (55) generates

With $g_k=0$ and $\alpha=3$ this is FISTA. The analysis uses $z_k=\frac{k+\alpha-1}{\alpha-1}y_k-\frac{k}{\alpha-1}x_k$ and, for $x^*\in S$, the energy

Formalization targets

Goal: Theorem 5.3

If $S\neq\emptyset$, $\alpha>3$, $0<s<1/L$ and $\sum_k k\|g_k\|<+\infty$, then

The goal makes no claim about rates of the iterates and no claim of strong convergence.

Value rate: Theorem 5.1

For $\alpha\ge3$, with an explicit constant $C$ depending on $x_0$, $y_0$, $x^*$ and $\sum_j(j+\alpha-1)\|g_j\|$,

Milestones

The proof's steps, in order: the proximal-gradient inequality (63); the energy step (66); the discrete Gronwall–Bellman Lemma A.9; the bound (68) on $\|z_k-x^*\|$; Theorem 5.1; the descent inequality (69); the velocity bound (72); the second-order inequality (80) for $h_k=\frac12\|x_k-x^*\|^2$; Lemma A.5; Opial's Lemma A.3.

Significance

The result. Theorem 5.3 gives convergence of the iterates of a FISTA-type method that tolerates computational error, and summability estimates that are stronger than the $O(1/k^2)$ value rate: $\sum_k k(\Theta(x_k)-\min\Theta)<\infty$ implies the rate $o(1/k^2)$ along the sequence. The summability condition $\sum_k k\|g_k\|<\infty$ is the discrete counterpart of $\int t\|g(t)\|\,dt<\infty$ for the perturbed dynamics, which makes the algorithm a faithful discretization of the continuous model studied in the same paper. For $\alpha=3$ (FISTA itself) convergence of the iterates was not known when the paper was written.

Formalizing it. The unperturbed case ($g_k\equiv0$) is already on Prove2Me and proved: the weak convergence theorem and the energy, descent and summability facts (namespace NesterovFB), and the proximal-gradient inequality, which this mission reuses as milestone (63). This mission poses the perturbed statements, which no existing item covers: the error terms change the energy step, require boundedness of $(z_k)$ through a Gronwall-type argument, and turn the Fejér-type estimate into an inhomogeneous one. The discrete Gronwall–Bellman and Opial lemmas are reusable well beyond this paper.

Difficulty

Without errors the energy $\mathcal G(k)$ is nonincreasing and every estimate follows from summing (66). With errors, (66) has the extra term $2s(k+\alpha-1)\langle g_k,z_{k+1}-x^*\rangle$, which can only be summed once $(z_k)$ is known to be bounded — and the bound on $z_k$ itself comes from the energy. The circularity is broken only by an implicit quadratic inequality and a discrete Gronwall–Bellman argument; a direct summation fails. The same issue reappears for the velocities, where (71) bounds $k^2\|x_{k+1}-x_k\|^2$ in terms of itself. Finally, weak convergence needs that $\lim\|x_k-x^*\|$ exists for every minimizer; for the inertial scheme $\|x_k-x^*\|$ is not monotone, and one must pass through the second-order inequality (80) and Lemma A.5 rather than a Fejér argument.

Formalization scope

$\mathcal H$ is a real inner product space, complete; nothing is finite-dimensional, and weak convergence is the published WeakTendsto ($\langle x_k,v\rangle\to\langle\bar x,v\rangle$ for every $v$), not norm convergence. $\Phi$ is EReal-valued with IsProperClosedConvex, and $\operatorname{prox}_{s\Phi}$ is a map $P$ with IsProx s Φ P (published definitions). $\Theta$ is the published NesterovFB.Rates.theta Φ Ψ; that definition names its arguments the other way round (nonsmooth first). $L$ is a nonnegative real and "$0<s<1/L$" is written $0<s$, $sL<1$. The algorithm is the predicate IsPerturbedRun on two sequences $x,y:\mathbb N\to\mathcal H$; $y_0$ is free, which covers every value of the unspecified $x_{-1}$. Series are Summable statements, sums such as $\sum_j(j+\alpha-1)\|g_j\|$ are tsums used only under the summability hypothesis.

Two printed statements are corrected as their proofs require. In Theorem 5.3 iii) the limit minimizes $\Phi+\Psi$ (the page says $\operatorname{argmin}\Phi$, the proof applies Opial's lemma with $S=\operatorname{argmin}(\Phi+\Psi)$). In Theorem 5.1 the constant uses $\sqrt{\mathcal G(0)/(\alpha-1)}$, the quantity the proof derives, instead of the printed $\sqrt{\mathcal E(0)/(\alpha-1)}$. Theorem 5.1 and (68) assume $\Phi(x_0)<+\infty$ so that the constant is a real number; Theorem 5.3 does not.

A trivializing formalization is ruled out: the step condition is $sL<1$ rather than $s<1/L$ (which is unsatisfiable for $L=0$ in Lean), and a sorry-free check confirms that $\Phi=\Psi=0$, $g=0$, $P=\mathrm{id}$ and constant sequences satisfy every hypothesis of the goal, so the hypotheses are jointly satisfiable.

Theorem numbers and pages are those of the Optimization Online preprint 5179 (October 2015), not of the Mathematical Programming typesetting. Welcome contributions: proofs of the appendix lemmas A.3, A.5, A.9 (independent of the algorithm), of (66) and (69) from the referenced inequality (63), and the chain (68) → Theorem 5.1, (72), (80) → Theorem 5.3.

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 ; published as …asymptotic vanishing viscosity, Math. Program. 168 (2018). https://doi.org/10.1007/s10107-016-0992-8
• A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sci. 2 (2009). https://doi.org/10.1137/080716542
• A. Chambolle, Ch. Dossal, On the convergence of the iterates of the "fast iterative shrinkage/thresholding algorithm", J. Optim. Theory Appl. 166 (2015). https://doi.org/10.1007/s10957-015-0746-4
• 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
• M. Schmidt, N. Le Roux, F. Bach, Convergence rates of inexact proximal-gradient methods for convex optimization, NeurIPS 2011. https://arxiv.org/abs/1109.2415
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73 (1967). https://doi.org/10.1090/S0002-9904-1967-11761-0