Optimization

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

The Kalman filter estimates the hidden state of a linear system from noisy observations. At every step it solves a minimum mean square error (MMSE) estimation problem: given a joint normal distribution of a signal $x$ and an observation $y$, find the estimator $\psi(y)$ minimizing $\mathbb E[\|x-\psi(y)\|^2]$. The answer, the conditional mean, is optimal only if the model distribution is correct, and in practice the system matrices and noise covariances are estimated and misspecified.

Shafieezadeh-Abadeh, Nguyen, Kuhn and Mohajerin Esfahani (arXiv:1809.08830, NeurIPS 2018) replace the single model by a set of plausible models: all normal distributions within type-2 Wasserstein distance $\rho$ of a nominal normal distribution. The estimator is then chosen to minimize the worst-case mean square error over this set. Their Theorem 2.5 shows that this robust estimation problem, although posed over an infinite-dimensional space of estimators and a nonconvex set of distributions, has the same value as a finite convex program over covariance matrices, and that the robust estimator is affine. Applied at every time step, this yields the Wasserstein distributionally robust Kalman filter of the paper's §4.

This mission formalizes Theorem 2.5 together with the minimax theorem (Theorem 2.3) and the lemmas of its proof.

Setting

Let $n, m \ge 0$ and $d = n+m$. A point of $\mathbb R^d$ is $z = [x; y]$ with signal $x\in\mathbb R^n$ and observation $y\in\mathbb R^m$. A symmetric matrix $S \in \mathbb R^{d\times d}$ is partitioned as $S = \begin{bmatrix} S_{xx} & S_{xy}\\ S_{yx} & S_{yy}\end{bmatrix}$. $\mathbb S^d_+$ ($\mathbb S^d_{++}$) denotes the positive semidefinite (definite) matrices, $A \succeq B$ means $A-B\in\mathbb S^d_+$, $\langle A,B\rangle = \operatorname{Tr}[A^\top B]$, and $A^{1/2}$ is the positive semidefinite square root of $A\succeq 0$.

Normal distributions. $\mathcal N_d(c,S)$ is the normal distribution on $\mathbb R^d$ with mean $c$ and covariance $S\in\mathbb S^d_+$; singular $S$ is allowed. $\mathcal N_d$ is the set of all of them.

Wasserstein distance. For distributions $\mathbb Q_1,\mathbb Q_2$ on $\mathbb R^d$,

$$W_2(\mathbb Q_1,\mathbb Q_2) = \inf_{\pi} \Bigl(\int \|z_1-z_2\|^2\,\pi(dz_1,dz_2)\Bigr)^{1/2},$$

the infimum ranging over all distributions $\pi$ on $\mathbb R^d\times\mathbb R^d$ with marginals $\mathbb Q_1$ and $\mathbb Q_2$.

Ambiguity set. Fix $\mu = [\mu_x;\mu_y]\in\mathbb R^d$, $\Sigma\in\mathbb S^d_{++}$, the nominal distribution $\mathbb P=\mathcal N_d(\mu,\Sigma)$ and a radius $\rho\ge 0$. The Wasserstein ambiguity set is

$$\mathcal P = \{\mathbb Q\in\mathcal N_d : W_2(\mathbb Q,\mathbb P)\le\rho\}.$$

Robust estimation. Let $\mathcal L$ be the set of all measurable functions $\psi:\mathbb R^m\to\mathbb R^n$. The distributionally robust MMSE problem is

$$\inf_{\psi\in\mathcal L}\ \sup_{\mathbb Q\in\mathcal P}\ \mathbb E^{\mathbb Q}\bigl[\|x-\psi(y)\|^2\bigr], \tag{2}$$

and a distributionally robust MMSE estimator is a $\psi$ attaining the outer infimum. Nature's problem exchanges the two optimizations; a $\mathbb Q^\star\in\mathcal P$ attaining its outer supremum is a least favorable prior.

The finite program. With $\underline\sigma = \lambda_{\min}(\Sigma)$, program (5) maximizes $f(S)=\operatorname{Tr}[S_{xx}-S_{xy}S_{yy}^{-1}S_{yx}]$ over $S\in\mathbb S^d_+$ (with $S_{xx}\in\mathbb S^n_+$, $S_{yy}\in\mathbb S^m_+$) subject to

$$\operatorname{Tr}\bigl[S+\Sigma-2(\Sigma^{1/2}S\Sigma^{1/2})^{1/2}\bigr]\le\rho^2,\qquad S\succeq\underline\sigma I_d .$$

Formalization targets

Goal: Theorem 2.5 (p. 3)

1. The optimal value of (2) equals the optimal value of (5).
2. If $S^\star$ is optimal in (5), then

$$\psi^\star(y) = S^\star_{xy}(S^\star_{yy})^{-1}(y-\mu_y)+\mu_x$$

is a distributionally robust MMSE estimator. 3. For the same $S^\star$, $\mathbb Q^\star=\mathcal N_d(\mu,S^\star)$ lies in $\mathcal P$ and is a least favorable prior.

Existence and uniqueness of an optimal $S^\star$ are not part of the statement.

Milestones, in the order of the proof

• Proposition 2.2 (Gelbrich formula): for $\Sigma_1,\Sigma_2\succeq 0$,

$$W_2\bigl(\mathcal N_d(\mu_1,\Sigma_1),\mathcal N_d(\mu_2,\Sigma_2)\bigr)=\sqrt{\|\mu_1-\mu_2\|^2+\operatorname{Tr}\bigl[\Sigma_1+\Sigma_2-2(\Sigma_2^{1/2}\Sigma_1\Sigma_2^{1/2})^{1/2}\bigr]}.$$

• Lemma A.1: the closed form of $\sup_{S\succeq0}\langle D,S\rangle-\gamma\operatorname{Tr}[S-2(\Sigma^{1/2}S\Sigma^{1/2})^{1/2}]$ and its unique maximizer.
• (A.1b): under a fixed normal distribution, affine estimators $y\mapsto Gy+g$ achieve the minimum mean square error over $\mathcal L$.
• Theorem 2.3 (minimax theorem): $\inf_{\psi\in\mathcal L}\sup_{\mathbb Q\in\mathcal P}\mathbb E^{\mathbb Q}[\|x-\psi(y)\|^2] = \sup_{\mathbb Q\in\mathcal P}\inf_{\psi\in\mathcal L}\mathbb E^{\mathbb Q}[\|x-\psi(y)\|^2]$.
• Lemma A.2: the maximizer of $\langle S,D\rangle$ under the Wasserstein-type trace constraint, and $S^\star\succeq\underline\sigma I_d$.
• (A.6): for $S\succ0$, $\min_G\bigl\langle\begin{bmatrix}I_n&-G\\-G^\top&G^\top G\end{bmatrix},S\bigr\rangle=f(S)$, uniquely at $G^\star=S_{xy}S_{yy}^{-1}$.

Significance

The result. Theorem 2.5 gives the robust estimator in closed form from one optimal covariance matrix, and identifies the least favorable distribution as a normal distribution with the nominal mean. Together with Theorem 2.3 it shows that the pair $(\psi^\star,\mathbb Q^\star)$ is a saddle point: the robust estimator is the Bayesian estimator for the least favorable prior. For $\rho=0$ the program has the single feasible point $\Sigma$ and the estimator reduces to the classical conditional mean, so the theorem contains the Kalman update as a special case. The finite program is what makes the robust filter of §4 computable; the paper's §3 (formalized in the companion mission of this series) solves it with a Frank–Wolfe method.

Formalizing it. The result is proved in the paper; nothing here is open. No part of it is machine-checked yet. The Gelbrich formula for normal distributions (Proposition 2.2) is cited from the literature and has no formal proof in Mathlib; neither does Lemma A.1, cited from earlier work of the same authors. A closely related statement for a Wasserstein ball over all distributions around an elliptical nominal (Kuhn et al. 2019, Theorem 25) is posed on the platform as WassersteinDRO.Shrinkage.distributionally_robust_mmse_estimator; it is a different theorem, since the ambiguity set there is convex and contains non-normal distributions.

Difficulty

The ambiguity set $\mathcal P$ is not convex, because a mixture of normal distributions is generally not normal. The standard route to a minimax equality, Sion's theorem, needs convexity on nature's side and therefore does not apply to (2) directly; the obvious attempt to interchange the infimum and the supremum fails at this step. The space $\mathcal L$ of measurable estimators is infinite-dimensional, and the Wasserstein constraint is an infimum over couplings, so a proof must pass to finite-dimensional descriptions on both sides (means and covariances for $\mathbb Q$, affine maps for $\psi$) and justify each passage. The matrix-analytic parts involve the nonlinear map $S\mapsto(\Sigma^{1/2}S\Sigma^{1/2})^{1/2}$, for which Mathlib has square roots but little calculus.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin n ⊕ Fin m); the Sum.inl coordinates are $x$, the Sum.inr coordinates are $y$, and the blocks of a matrix are toBlocks₁₁, toBlocks₁₂, toBlocks₂₁, toBlocks₂₂.
• $\mathcal N_d(c,S)$ is Mathlib's multivariateGaussian c S with S.PosSemidef; only the nominal $\Sigma$ is required to be positive definite.
• $W_2$ is the published coupling-based WassersteinDRO.Shrinkage.wassersteinDistance 2 in $[0,\infty]$. The ambiguity set is defined through it, not through the Gelbrich formula; the formula is Proposition 2.2, a milestone.
• Expectations are lower Lebesgue integrals in $[0,\infty]$, with no integrability guard. A non-integrable estimator therefore has infinite risk and cannot lower the infimum through a junk value.
• The values of (2) and of nature's problem are in $[0,\infty]$; the value of (5) is the published sdpValue in EReal, and the two are compared through the coercion.
• $\underline\sigma$ is passed as a real number that is the least eigenvalue of $\Sigma$.
• "Equivalent" in Theorem 2.5 is read as the three claims above. A version that asserts only equality of values, or optimality of $\psi^\star$ among affine estimators only, is weaker than the theorem and is not the goal.
• Lemma A.2 carries the added hypothesis $\rho>0$, without which its algebraic equation has no admissible root.

A complete development needs the Gelbrich formula for (possibly degenerate) normal distributions, conditional means of jointly normal vectors, a minimax theorem for convex–concave functions on compact sets, Lagrangian duality for a convex semidefinite program, and calculus of the positive semidefinite square root. The first three are reusable well beyond this mission, and contributions of any of them as separate results are welcome.

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
• M. Gelbrich, On a formula for the L² Wasserstein metric between measures on Euclidean and Hilbert spaces, Mathematische Nachrichten 147, 1990. https://doi.org/10.1002/mana.19901470121
• V. A. Nguyen, D. Kuhn, P. Mohajerin Esfahani, Distributionally robust inverse covariance estimation, arXiv:1802.01981, 2018. https://arxiv.org/abs/1802.01981
• D. Kuhn, P. Mohajerin Esfahani, V. A. Nguyen, S. Shafieezadeh-Abadeh, Wasserstein distributionally robust optimization: theory and applications in machine learning, INFORMS TutORials, 2019; arXiv:1908.08729. https://arxiv.org/abs/1908.08729
• D. P. Bertsekas, Convex Optimization Theory, Athena Scientific, 2009.

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

Product framing in online retail

An online retailer does not show its catalogue at once. Products are arranged on a sequence of pages, and a consumer looks at the first few pages and then chooses among what she has seen, or leaves. Where a product is placed therefore decides whether it is considered at all. Gallego, Li, Truong and Wang (Operations Research, 2020) call the placement decision product framing. They show that the optimal framing problem is NP-hard even with two pages and a multinomial logit choice model, and give polynomial-time framing algorithms with constant performance guarantees.

The paper builds on the assortment optimization literature, where a seller chooses one set of products to offer under a choice model, and on work in which consideration sets depend on how products are presented. Davis, Topaloglu and Williamson (2015) studied a sequential assortment problem in which products are added over time. Two of their results, on how per-product revenue behaves when products are removed, are the structural inputs of this mission. Aouad and Segev (2016) studied a variant with one product per page under the MNL model, in which every product must be displayed.

Setting

There are $n$ products $[n]=\{1,\dots,n\}$, and product $i$ earns unit revenue $r_i$. The products are placed on $m$ pages, each holding at most $p$ products, and a product may be left undisplayed. A consumer views the first $X$ pages, where $X\in[m]$ is random with law $\lambda(x)=\mathbb P[X=x]$ and tail $\Lambda(x)=\mathbb P[X\ge x]$, independent of the framing. Her consideration set is the set of products on pages $1,\dots,X$.

A choice model gives, for each consideration set $S\subseteq[n]$, purchase probabilities $P(i,S)\ge0$ with $P(i,S)=0$ for $i\notin S$ and $\sum_{i\in S}P(i,S)\le1$. The expected revenue of $S$ is $R(S)=\sum_{i\in S}r_iP(i,S)$. The optimal framing value is

$$V^{OPT}=\max_{\text{framings}}\ \sum_{x\in[m]}\lambda(x)\,R(\text{products on pages }1,\dots,x),$$

the maximum over all placements with at most $p$ products per page (problem (1)). The cardinality-constrained assortment problem is $G(c)=\max_{|S|\le c}R(S)$ (problem (2)), and $U(x)=G(x\cdot p)$ is the best revenue from a consumer who sees $x$ pages.

The analysis rests on three assumptions:

• A1: $P(i,S)\ge P(i,T)$ whenever $i\in S\subseteq T$, a property of every random utility model.
• A2: problem (2) can be solved, here exactly.
• A3: $X$ is new better than used in expectation (NBUE): $q(x)=\mathbb E[X-x+1\mid X\ge x]\le q(1)=\mathbb E[X]$ for all $x\in[m]$.

The algorithm NEST($y$), for $y\in[m]$, first takes an optimal solution $S(y)$ of (2) with bound $y\cdot p$. Then, for $x=y-1$ down to $1$, it chooses $S(x)\subseteq S(x+1)$ of size $\min(|S(x+1)|,xp)$ whose per-product revenue $R(S(x))/|S(x)|$ is at least that of $S(x+1)$. Page $x$ displays $S(x)\setminus S(x-1)$, and pages after $y$ stay blank. $V^{NEST(y)}$ is the expected revenue of this framing, and $V^{NEST}=\max_{y\in[m]}V^{NEST(y)}$.

Formalization targets

Goal: Theorem 3 (p. 10)

$$V^{NEST}\ \ge\ \frac{6}{\pi^2}\,V^{OPT}$$

The goal holds under A1, A2 with $\varepsilon=0$ and A3, for every run of NEST($y$), $y\in[m]$. Here $6/\pi^2\approx0.608$.

Milestones

The milestones are the numbered results the proof of Theorem 3 uses, in the order it uses them:

1. Theorem 2, the clairvoyant bound $V^{OPT}\le\mathbb E[U(X)]$.
2. Lemma 1, from Davis et al.: some product can be removed from any $S$ with $|S|\ge2$ without lowering $R(S)/|S|$.
3. The existence of a NEST($y$) run.
4. Proposition 1: $V^{NEST(y)}\ge\frac{U(y)}{y}\mathbb E[\min(X,y)]$.
5. Lemma 2, from Davis et al.: $U(x)/x$ is decreasing.
6. Propositions 2 and 3, on the bound-revealing program (5),

$$\gamma=\min_{U,\Lambda}\ \max_{x\in[m]}\frac{U(x)}{x}\,\mathbb E[\min(X,x)],$$

taken over NBUE tails $\Lambda$ and functions $U\ge0$ that are increasing with $U(x)/x$ decreasing and $\mathbb E[U(X)]=1$. Proposition 3 states $1/\gamma=\max_\Lambda\mathbb E[X/\mathbb E[\min(X,Y)\mid X]]$. 7. Lemma 7 and Corollaries 5–6, comparing NBUE $X$ with an exponential variable of the same mean. 8. The evaluation $\mathbb E[W/(\mu(1-e^{-W/\mu}))]=\pi^2/6$ for $W$ exponential with mean $\mu$. 9. The bound $\gamma\ge6/\pi^2$.

Significance

Theorem 3 gives a constant-factor guarantee for a problem that is NP-hard under the same assumptions. The constant does not depend on the choice model beyond A1, on the number of pages, or on the page capacity, and the paper shows it is tight relative to the upper bound $\mathbb E[U(X)]$ (Proposition 4, in the geometric limit). NEST needs only a cardinality-constrained assortment oracle, which exists in polynomial time for the MNL and nested logit models. The same bound-revealing program, problem (5), is reused in the paper for joint framing and pricing (Theorem 7).

The paper proves the result in full. No part of it has been machine-checked. The mission formalizes the model and states the guarantee and every intermediate result. The proofs combine finite combinatorics (Lemmas 1 and 2, Proposition 1) with a comparison of a discrete NBUE law against the exponential distribution, and that comparison is reusable for other approximation analyses with the same structure. The equality of the exponential integral with $\sum_k k^{-2}$ connects to Mathlib's hasSum_zeta_two.

Difficulty

The upper bound (Theorem 2) and the lower bound (Proposition 1) are each elementary. The difficulty is to compare them uniformly over all choice models and all NBUE page-count laws. The ratio of $\max_y\frac{U(y)}{y}\mathbb E[\min(X,y)]$ to $\mathbb E[U(X)]$ depends on the whole function $U$ and the whole law of $X$, and the worst case cannot be read off from any single instance. Replacing the instance by the program (5) removes the choice model. Bounding the program still requires an optimization over distributions, and its value is attained only in a limit (Proposition 4).

The comparison with the exponential law goes through the increasing convex order. Here $X$ is a discrete law on $\{1,\dots,m\}$ and the comparison variable is continuous. The function $h(x)=x/\mathbb E[\min(Z,x)]$ to which Lemma 7 is applied is increasing and convex only on $[0,\infty)$, so a formal argument has to track the domain.

Formalization scope

Theorem numbers and pages are those of the authors' accepted manuscript (49 pp.), which differ from the journal typesetting. The conventions are:

• Products are Fin n. Pages are the naturals $1,\dots,m$, kept 1-based, with $m,p\ge1$.
• A framing is a map Fin n → ℕ: page $0$ means "not displayed", and each page $1,\dots,m$ holds at most $p$ products. $V^{OPT}$ is the maximum over the finite, nonempty set of feasible framings.
• The law $\lambda$ is a function on $[1,m]$, and $\Lambda$, $\mathbb E[\min(X,x)]$ and $\mathbb E[X]$ are finite sums. A3 is the paper's own $q$-form, and a conditional expectation on a null event imposes nothing.
• The exponential law is Mathlib's expMeasure with rate $1/\mathbb E[X]$. The independence in Corollary 6 is encoded by iterated integrals.
• The revenues are assumed nonnegative ("unit profit or revenue"). Lemma 1 fails for negative revenues.
• A2 is taken with $\varepsilon=0$, as the paper does after p. 8, and polynomial time is not modelled.
• "Increasing" and "decreasing" are weak.

NEST makes arbitrary choices, so a run is a predicate on its output. Theorem 3 is stated for every family of runs, and a separate milestone shows that runs exist. The value $V^{NEST(y)}$ is the expected revenue of the framing the run actually displays, not the closed form $\sum_x\lambda(x)R(S(\min(x,y)))$, whose equality with it is part of the proof of Proposition 1. A formalization that quantified over some run, that defined $V^{NEST(y)}$ by that closed form, or that assumed Lemma 2 for $U$ would not be Theorem 3.

Program (5) is stated with its tail variable $\Lambda$ and law $\lambda(x)=\Lambda(x)-\Lambda(x+1)$, $\Lambda(m+1)=0$. The page's typos are corrected in the statements and recorded in the notes: "$\mathbb E[U(x)]=1$" in (5), and the right-hand side of Corollary 5. Proposition 2 is formalized in its existential reading: some optimal solution of (5) has constant $\frac{U(x)}{x}\mathbb E[\min(X,x)]$.

A complete development needs:

• finite assortment combinatorics;
• the finite program (5) and its compactness;
• the increasing convex order between a discrete NBUE law and the exponential, through integrated tails;
• the integral $\int_0^\infty ue^{-u}/(1-e^{-u})\,du=\pi^2/6$.

The exponential comparison and the integral are reusable beyond this mission. Proofs of any milestone are welcome, including alternative proofs of Lemmas 1 and 2 from A1.

Selected references

• G. Gallego, A. Li, V.-A. Truong, X. Wang, Approximation Algorithms for Product Framing and Pricing, Operations Research, 2020. https://doi.org/10.1287/opre.2019.1875
• J. M. Davis, H. Topaloglu, D. P. Williamson, Assortment optimization over time, Operations Research Letters 43(6), 608–611, 2015. https://doi.org/10.1016/j.orl.2015.08.007
• A. Aouad, D. Segev, Display optimization for vertically differentiated locations under multinomial logit choice preferences, working paper, 2016 (as cited in the paper; later published in Management Science).
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

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