All missions

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

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

Motivation

First-order methods use function gradients to minimize an objective without solving a second-order subproblem at each iteration. Inertial methods also use the previous iterate, which can improve the convergence rate but complicates the choice of momentum and step size. Attouch, Chbani, Fadili, and Riahi study a family of such methods derived from continuous dynamical systems with Hessian driven damping. Their explicit strongly convex scheme, IGAHD-SC, uses a difference of consecutive gradients in addition to momentum and the current gradient. The difference represents the damping contribution without evaluating a Hessian matrix. Attouch et al., §5.2, pp. 28–29.

The question in this mission is quantitative. If the objective has strong curvature and a Lipschitz gradient, do the iterates, objective values, and a discounted sum of squared gradients decrease at the geometric rates claimed in Theorem 11? This is the final independent convergence theorem of the paper's series of discrete algorithms. Attouch et al., Theorem 11, p. 29.

Setting

Let $H$ be a real Hilbert space and $f:H\to\mathbb R$ a continuously differentiable objective. For $\mu>0$, the paper calls $f$ $\mu$-strongly convex when $z\mapsto f(z)-\frac\mu2\|z\|^2$ is convex. Let $x^*$ be a minimizer of $f$. The paper assumes that the gradient is $L$-Lipschitz for a positive constant $L$: $\|\nabla f(u)-\nabla f(w)\|\le L\|u-w\|$ for every $u,w\in H$. Strong convexity makes the minimizer unique. Attouch et al., Definition 1, p. 19; Theorem 11, p. 29.

Choose parameters $\beta\ge0$ and $s>0$, and write $r=\sqrt{\mu s}$. Starting from arbitrary $x_0,x_1\in H$, IGAHD-SC determines $x_{k+1}$ for $k\ge1$ by

$$x_{k+1}=x_k+\frac{1-r}{1+r}(x_k-x_{k-1}) -\frac{\beta\sqrt s}{1+r}\bigl(\nabla f(x_k)-\nabla f(x_{k-1})\bigr) -\frac{s}{1+r}\nabla f(x_k).$$

The two differences have different roles: $x_k-x_{k-1}$ is the inertial part, and $\nabla f(x_k)-\nabla f(x_{k-1})$ is the Hessian damping term in this explicit discretization. The algorithm is exactly the displayed scheme on p. 28, with its two starting points free. Attouch et al., (25) and (IGAHD-SC), p. 28.

Formalization targets

Theorem 11 assumes $\beta\le1/\sqrt\mu$ and the two smoothness bounds in (26). Define

$$q=\frac{1}{1+\frac12\sqrt{\mu s}},\qquad \theta=\frac{1}{1+\sqrt{\mu s}}.$$

Both constants lie strictly between zero and one. The mission's goal is the paper's three-part conclusion:

$$\|x_k-x^*\|=O(q^{k/2}),\qquad f(x_k)-f(x^*)=O(q^k),$$

and

$$\theta^k\sum_{j=0}^{k-2}\theta^{-j}\|\nabla f(x_j)\|^2=O(q^k) \quad (k\to\infty).$$

The milestones record the auxiliary vector and energy from the proof, their velocity and strong-convexity estimates, the gradient majorization, the one-step energy inequality, and the geometric energy bound. These are claims displayed by the authors on pp. 30–32, in the order in which they lead to the goal. Attouch et al., proof of Theorem 11, pp. 30–32.

Significance

The first two bounds give geometric decay of distance to the optimizer and of objective error for the specified parameter regime. The third controls a discounted accumulation of squared gradients. Together they describe more than convergence of the objective alone: the same run has explicit asymptotic rates for its points and gradient behavior. The rate constants depend on the strong-convexity parameter, step size, and allowed damping range. Attouch et al., Theorem 11, p. 29.

This result is proved in the cited paper; the open work here is its Lean formalization. A completed development would include a reusable representation of the explicit inertial run, a precise strong-convexity interface matching Definition 1, and the energy estimates that support the theorem. The formal statements in this proposal are proof targets, not claims that already have machine-checked proofs. The two comparison methods mentioned in Remark 10 use different discretizations or hypotheses, so their rate theorems cannot replace this target. Attouch et al., Remark 10, p. 29.

Difficulty

Ordinary smooth gradient descent is controlled by the current gradient and one step difference. Here the recurrence also contains the preceding gradient and the preceding step. A direct estimate of $f(x_{k+1})-f(x^*)$ does not isolate a contracting quantity. The paper therefore tracks an auxiliary vector and an energy involving both the objective gap and that vector; the precise coefficients in the two bounds of (26) are needed for the final one-step inequality. The proof's intermediate display on p. 31 also changes a gradient index between lines, so each formalized displayed claim needs scrutiny against the recurrence and the final p. 32 inequality. Attouch et al., proof of Theorem 11, pp. 30–32.

Formalization scope

Lean represents $H$ as a complete real inner-product space, $\nabla f$ by Mathlib's gradient, and the run as a predicate on a sequence $x:\mathbb N\to H$ obeying (IGAHD-SC) for every $k\ge1$. The source's arbitrary initial pair is preserved. A witness $x^*$ and the hypothesis that it minimizes $f$ express the nonempty argmin assumption without taking an infimum of real values. The strong-convexity definition is exactly Definition 1. Positive $s$, $\mu$, and $L$ make every square root and step-size denominator meaningful. The first bound in (26) is written $8\beta L\le\sqrt\mu$, which retains the paper's intended $\beta=0$ case; the paper later uses $0\le\beta$ explicitly, so it is included. Attouch et al., pp. 19, 28–32.

The rates use =O[Filter.atTop]. Lean writes $q^{k/2}$ as $(\sqrt q)^k$, and the sum through $k-2$ as Finset.range (k - 1). For $k=0,1$ the finite range is empty; the asymptotic claim concerns large $k$. The source prints $p$ in the sum limit and $j$ in its summand; both are read as $j$. The goal itself mentions the iterates, objective values, and gradients, without assuming an energy decay bound. A complete proof can contribute reusable inequalities for strongly convex functions with Lipschitz gradients and geometric recurrences, alongside the paper-specific run and energy lemmas.

Selected references

• H. Attouch, Z. Chbani, J. Fadili, and H. Riahi, First-order optimization algorithms via inertial systems with Hessian driven damping, Mathematical Programming, 2020; arXiv:1907.10536v2.

Motivation

The notebooks Ramanujan kept in India record identities, evaluations, transformations and general principles, usually presented without proofs. They preserve a working mathematician's collection rather than a textbook arranged around a sequence of prerequisite theorems. The Tata Institute of Fundamental Research published an unedited facsimile edition in 1957, making the manuscripts available for systematic study.

Bruce C. Berndt's Ramanujan's Notebooks, published by Springer in five parts in 1985, 1989, 1991, 1994 and 1998, supplies that study. The volumes examine the entries individually, proving them, correcting them where necessary, or explaining why they are false or lack a rigorous interpretation. Their subject matter ranges from magic squares and combinatorial identities to hypergeometric series, continued fractions, elliptic functions, modular equations, class invariants and asymptotic expansions.

This mission takes the results established in Berndt's treatment as formalization targets. The published arguments provide mathematical reference proofs. The remaining task is to express the results precisely and construct proofs checked by Lean.

Setting

An entry is a source claim identified by its chapter and local entry label in Berndt's series. The collection is organized around one Lean statement per entry that Berndt establishes. Where an entry contains separately identified parts, corollaries or examples, suffixes distinguish the corresponding statements while preserving their common source location. Intermediate steps of a printed proof do not automatically become additional targets.

The mission covers Chapters 1–39. Part I contains Chapters 1–9; Part II, Chapters 10–15; Part III, Chapters 16–21; Part IV, Chapters 22–31; and Part V, Chapters 32–39. The Part IV appendix on the first notebook and the Quarterly Reports treated in Part I also belong to the mission's scope, with their statements incorporated as they are added.

Declarations use the namespace RamanujanNotebooks and names of the form entry_<chapter>_<entry>, such as RamanujanNotebooks.entry_16_19. Shared definitions fix the meaning of recurring objects: q-shifted factorials, theta functions, hypergeometric series, continued-fraction convergents and the special functions used across chapters. Their domains, normalizations and indexing conventions are documented so that different entries refer to the same mathematical objects.

Formalization targets

The series has no single capstone theorem. Its goal item is therefore a representative entry: Chapter 16, Entry 19, Jacobi's triple product identity in Ramanujan's notation. This is in Part III, whose chapter develops q-series and theta functions.

For complex parameters $a,b$, Ramanujan's general theta function is

$$f(a,b)=\sum_{n\in\mathbb Z} a^{n(n+1)/2}b^{n(n-1)/2}.$$

Both exponents are nonnegative integers. Under $|ab|<1$, the series converges absolutely, and Entry 19 identifies it with an infinite product. Writing $q=ab$, the target is

$$f(a,b)=\prod_{m=0}^{\infty} (1+a q^m)(1+b q^m)(1-q^{m+1}), \qquad |ab|<1.$$

Equivalently, with the infinite q-Pochhammer symbol

$$(z;q)_\infty=\prod_{m=0}^{\infty}(1-zq^m),$$

the identity reads

$$f(a,b)=(-a;ab)_\infty(-b;ab)_\infty(ab;ab)_\infty.$$

The Lean statement uses ramanujanTheta and qPochInf, with the hypothesis ‖a * b‖ < 1. Proving this goal establishes the representative identity; completion of the collection is tracked through its member statements, one per entry.

Every entry is a separate statement of this mission, named RamanujanNotebooks.entry_<chapter>_<entry> (with suffixes for parts, corollaries and examples): 3,863 statements for Parts I–V, the Part IV appendix on the first notebook and the Quarterly Reports; the AMS Memoir 477 statements are being added. A chapter's statements are found by searching for its name prefix. The milestone list has one milestone per chapter, in source order, titled like “Part III · Ch. 16 — q-series and theta-functions”; each links one representative result and its description names the chapter's main results.

Statement conventions and source differences

The mathematical reference is what Berndt proves, with the hypotheses his argument requires. A notebook display alone is insufficient when its domain, convergence conditions or branch choices are unstated. Each target identifies its source and records the conditions under which the asserted equality, limit, transformation or asymptotic relation is established.

Corrected statements carry the explicit phrase “Differs from the printed source”. The accompanying note explains the difference and its origin: a correction supplied by Berndt, a restriction required by the proof, or a reading that resolves an ambiguity. A proposed repair supported only by numerical experiments requires further mathematical review before inclusion as a result established by the reference.

Entries that Berndt shows to be false are not stated as theorem targets. Neither are identities treated only formally, without a rigorous version. For example, Chapter 37's Entry 34 manipulates divergent series, while Entries 35–37 are shown false. Chapter 39 also contains formal claims and entries for which the book supplies no definite interpretation. Such omissions preserve the boundary between a proved result and a suggestive manuscript formula.

Numerical checks are recorded in theorem docstrings, including the tested parameters and the kind of comparison performed. They help detect indexing errors, sign errors and unsuitable domains. Agreement at sampled points is evidence about the transcription; it is not a proof of the universally quantified Lean statement.

Significance and status

The mission brings together source-linked statements of known results whose proofs otherwise remain dispersed across Berndt's commentary. Formal proofs can expose exactly which analytic hypotheses an identity needs and make the shared special-function definitions available for later developments. A proof of the triple product, for example, connects the series definition of the general theta function with its product representation, which recurs throughout the theta-function material.

The statements are proof targets. A declaration that type-checks has a meaningful Lean type; that check alone does not establish the proposition. The description makes no claim that the collection already has machine-checked proofs. Progress is measured by proofs of the individual targets with their stated hypotheses.

Difficulty

The entries vary considerably in their prerequisites. Finite algebraic and combinatorial identities can be approached with relatively little analytic infrastructure. Other chapters depend on convergence theory for continued fractions, transformations of theta and elliptic functions, modular forms, or class invariants.

Even a short equality can require substantial work before its expressions have the intended meaning. A divergent series cannot be interpreted as an ordinary sum, and a complex root or logarithm needs an appropriate branch convention. The central challenge is to preserve the object and domain of the reference result while supplying the formal infrastructure needed to prove it.

Formalization scope

Statements use real or complex variables according to the reference, with exceptional values, nonvanishing conditions and convergence ranges explicit. Infinite series are expressed with convergence assertions where necessary; continued fractions are represented through their convergents and limits. Integrals carry the hypotheses needed for their intended interpretation. Lean's total definitions of division, infinite sums and infinite products must not turn an undefined or divergent source expression into a trivial theorem.

Contributions should prove the registered statements using their shared definitions. Reusable lemmas about convergence, special functions and transformations are part of that work. Any suspected statement error should be reported with the declaration name, source location and a specific mathematical objection, so that the source relationship can be reviewed before a replacement is prepared.

Selected references

• S. Ramanujan, Notebooks, facsimile edition, Tata Institute of Fundamental Research, Bombay, 1957.
• B. C. Berndt, Ramanujan's Notebooks, Part I, Springer, 1985.
• B. C. Berndt, Ramanujan's Notebooks, Part II, Springer, 1989.
• B. C. Berndt, Ramanujan's Notebooks, Part III, Springer, 1991.
• B. C. Berndt, Ramanujan's Notebooks, Part IV, Springer, 1994.
• B. C. Berndt, Ramanujan's Notebooks, Part V, Springer, 1998.

Motivation

A fractional program minimizes a ratio $f(x)/g(x)$ over a set $S$. Nonconvex, nonsmooth ratios arise in the scale-invariant sparse signal recovery model $\min\|x\|_1/\|x\|_2$ over a polyhedron, in robust Sharpe-ratio optimization in finance, and in the Rayleigh quotient $x^\top Ax/x^\top Bx$ over a sphere; with $g\equiv1$ and $S=H$ the problem reduces to composite optimization $\min f^{\mathsf s}+f^{\mathsf n}$. The classical method of Dinkelbach (1967) and its proximal-gradient descendants assume a convex numerator and a concave or smooth denominator, which these models do not satisfy.

Boţ, Dao and Li (arXiv:2003.04124, Math. Oper. Res. 2022) propose the extrapolated proximal subgradient algorithm (e-PSG) for problems in which the numerator is the sum of a smooth convex and a nonsmooth nonconvex term and the denominator is only weakly convex, and they prove that its cluster points satisfy a first-order condition. This mission formalizes that subsequential convergence theorem (Theorem 4.5).

Setting

Let $H=\mathbb R^N$ with the Euclidean inner product, and let $S\subseteq H$ be nonempty, closed and convex. The problem is

$$\min_{x\in S}\ \frac{f(x)}{g(x)}.\qquad(\mathrm P)$$

Assumption 1. $f=f^{\mathsf s}+f^{\mathsf n}$, where $f^{\mathsf s}:H\to\mathbb R$ is continuously differentiable and convex with an $\ell$-Lipschitz gradient, $f^{\mathsf n}:H\to(-\infty,+\infty]$ is proper and lower semicontinuous, $S\cap\operatorname{dom}f\ne\emptyset$, and $f\ge0$ on $S\cap\operatorname{dom}f$.

Assumption 2. $g$ is finite and positive on $S$, continuous on an open set containing $S$, and either weakly convex with modulus $\beta$ on an open convex set containing $S$ (that is, $g+\frac\beta2\|\cdot\|^2$ is convex there), or regular (Fréchet and limiting subdifferentials coincide) and weakly convex with modulus $\beta$ on $S$.

The limiting subdifferential $\partial_L h(x)$ collects limits of Fréchet subgradients $u_k\in\widehat\partial h(x_k)$ along $x_k\to x$ with $h(x_k)\to h(x)$. A point $\bar x\in S$ is a lifted stationary point of (P) if

$$0\in g(\bar x)\,\partial_L(f+\iota_S)(\bar x)-f(\bar x)\,\partial_L g(\bar x),$$

where $\iota_S$ is $0$ on $S$ and $+\infty$ off $S$.

The boundedness condition (BC) asks for $0<m\le g\le M$ on $S\cap\operatorname{dom}f$. Algorithm 1 (e-PSG) starts from $x_{-1}=x_0\in S\cap\operatorname{dom}f$ with parameters $\delta>0$, $\zeta>0$ ($1-\sqrt\beta\zeta>0$) and extrapolation bounds $\bar\mu,\bar\kappa$ (in explicit ranges depending on $m,M,\ell$ under (BC), and $\bar\mu=\bar\kappa=0$ otherwise). At step $n$ it sets $\theta_n=f(x_n)/g(x_n)$, picks $g_n\in\partial_L g(x_n)$ and $0<\tau_n\le1/\max\{\sqrt\beta\theta_n/\zeta,\delta\}$, forms $u_n=x_n+\kappa_n(x_n-x_{n-1})$, $v_n=x_n+\mu_n(x_n-x_{n-1})$ with $\kappa_n\in[0,\bar\kappa]$, $\mu_n\in[0,\bar\mu\tau_n]$, and takes

$$x_{n+1}\in\operatorname*{argmin}_{x\in S}\Big(f^{\mathsf n}(x)+f^{\mathsf s}(u_n)+\langle\nabla f^{\mathsf s}(u_n),x-u_n\rangle+\tfrac1{2\tau_n}\|x-v_n-\tau_n\theta_ng_n\|^2+\tfrac\ell2\|x-u_n\|^2\Big).$$

Finally $S_0=\{x\in S: f(x)/g(x)\le f(x_0)/g(x_0)\}$.

Formalization targets

Goal: Theorem 4.5(iii)

If $S_0$ is bounded and $\liminf_n\tau_n=\bar\tau>0$, then every cluster point $\bar x$ of $(x_n)$ satisfies

$$\bar x\in S\cap\operatorname{dom}f,\qquad \lim_{n\to\infty}\frac{f(x_n)}{g(x_n)}=\frac{f(\bar x)}{g(\bar x)},\qquad \bar x\ \text{is lifted stationary.}$$

In the formal statement $g$ is in addition Lipschitz around every point of $S$; see Formalization scope.

Milestones, in proof order

1. Lemma 4.3: for $x,y\in S$ and $u\in\partial_L g(x)$, $\langle u,y-x\rangle\le g(y)-g(x)+\frac\beta2\|y-x\|^2$.
2. Lemma 4.4 (descent lemma), already on the platform.
3. Inequality (16): the one-step inequality from the subproblem.
4. Inequality (17): the ratio inequality, for every Young parameter $\omega>0$.
5. Theorem 4.5(i): $x_n\in S\cap\operatorname{dom}f$ and

$$\Big(\tfrac{f(x_{n+1})}{g(x_{n+1})}+c\|x_{n+1}-x_n\|^2\Big)+\alpha\|x_{n+1}-x_n\|^2\le\tfrac{f(x_n)}{g(x_n)}+c\|x_n-x_{n-1}\|^2$$

with the explicit constants (14), and convergence of $f(x_n)/g(x_n)$. 6. Theorem 4.5(ii): $(x_n)$ is bounded, $\|x_{n+1}-x_n\|\to0$, and $\sum_n\|x_{n+1}-x_n\|^2<\infty$. 7. The limit inequality at a cluster point (proof of Theorem 4.5(iii), p. 13).

Significance

Theorem 4.5 is the subsequential convergence result on which the paper's later results rest: with a Kurdyka–Łojasiewicz property of a merit function it upgrades to convergence of the whole sequence and to linear rates (Theorem 5.5), and under strict differentiability of $g$ lifted stationarity becomes ordinary stationarity (Corollary 4.6). The merit function $F_n=f(x_n)/g(x_n)+c\|x_n-x_{n-1}\|^2$ with explicit constants is the template for analyzing extrapolated proximal methods on ratio objectives.

The result is proved on paper; no machine-checked version exists. Formalizing it produces a verified descent analysis of an extrapolated proximal method for a nonconvex ratio, a formal subgradient inequality for weakly convex functions with respect to the limiting subdifferential, and a checked passage to the limit through limiting subdifferentials. It also pins down the hypotheses: the formal statement records a missing assumption of the printed theorem (below).

Difficulty

The ratio is not a sum, so the standard sufficient-decrease argument for proximal gradient methods does not apply directly: the subproblem linearizes $g$ through a limiting subgradient $g_n$ scaled by the current ratio $\theta_n$, and the descent of $f/g$ comes only after dividing by $g(x_{n+1})$, which ties the step size to $\theta_n$ and to bounds on $g$. Extrapolation adds a cross term $\langle x_{n+1}-x_n,x_n-x_{n-1}\rangle$ that the merit function must absorb, which is where the explicit ranges of $\bar\mu,\bar\kappa$ come from. At a cluster point, $f$ is only lower semicontinuous, so convergence of $f(x_{k_n})$ to $f(\bar x)$ must be extracted from the optimality of the subproblems, and the limits of $g_n$ must be shown to lie in $\partial_L g(\bar x)$. The naive approach of passing to the limit in the subproblem's optimality condition fails because $\partial_L(f^{\mathsf n}+\iota_S)$ has no sum rule in this generality.

Formalization scope

$H$ is EuclideanSpace ℝ (Fin N). Functions into $(-\infty,+\infty]$ are EReal-valued; properness is the published IsProperFn, and $\widehat\partial$, $\partial_L$ are the published IsRegularSubgrad and LimitingSubdiff. The denominator $g$ is real-valued on all of $H$: only its values and subgradients near $S$ enter, where the paper's $g$ is finite. Weak convexity "with modulus $\beta$" means that $\beta\ge0$ is a valid constant, not the smallest one. A run of Algorithm 1 is a predicate on the sequences $(x_n),(g_n),(\tau_n),(\kappa_n),(\mu_n)$; the argmin and $g_n$ are selections, never Classical.choose. $x_{-1}=x_0$. Ratios are real numbers (f x).toReal / g x, meaningful because the iterates stay in $\operatorname{dom}f$. The $\bar\kappa$-range of Step 1 is written as $\ell\bar\kappa^2<\frac{m\delta(1-\sqrt\beta\zeta)}M-\frac{2m\bar\mu}{\sqrt{mM}}$, avoiding division by $\ell$. $\liminf\tau_n>0$ is an eventual positive lower bound, which is equivalent since $\tau_n\le1/\delta$. Cluster points are MapClusterPt.

Correction. Under the second alternative of Assumption 2 alone, Theorem 4.5(iii) fails: for $S=[0,1]$, $g(x)=2-\sqrt x$ on $S$ and $f(x)=1-\sqrt x/4$, the iterates converge to $0$, where $\partial_Lg(0)=\emptyset$, so $0$ is not lifted stationary. The goal and the limit-inequality milestone therefore assume that $g$ is Lipschitz around every point of $S$, which holds automatically under the first alternative.

The trivializing formalizations are ruled out: the parameter ranges are inhabited (checked in Lean, including $\ell=0$), the goal quantifies over every cluster point of every run, and lifted stationarity requires actual limiting subgradients rather than an infDist that would be $0$ on an empty set.

Contributions welcome: the subgradient inequality for weakly convex functions, the descent lemma's use in (16), the limit arguments for limiting subdifferentials (the platform has the robustness property (3) as NonconvexSplitting.ProxGrad.limitingSubdiff_robust), and Fermat's rule for constrained minimizers of $\varphi+\iota_S$ — the last is reusable well beyond this mission.

Selected references

• R. I. Boţ, M. N. Dao, G. Li, Extrapolated Proximal Subgradient Algorithms for Nonconvex and Nonsmooth Fractional Programs, Math. Oper. Res. 47 (2022); arXiv:2003.04124v2. https://arxiv.org/abs/2003.04124
• W. Dinkelbach, On nonlinear fractional programming, Management Science 13 (1967) 492–498. https://doi.org/10.1287/mnsc.13.7.492
• B. S. Mordukhovich, Variational Analysis and Generalized Differentiation I, Springer, 2006. https://doi.org/10.1007/3-540-31247-1
• Y. Nesterov, Introductory Lectures on Convex Optimization, Springer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Many first-order optimization methods are discretizations of second-order differential equations. In the continuous system the velocity carries the momentum, and the damping terms decide how fast the trajectory settles at a minimizer. Attouch, Chbani, Fadili and Riahi study inertial systems with Hessian driven damping: a friction term proportional to $\nabla^2 f(x(t))\dot x(t)$, which damps the oscillations that plain heavy-ball and Nesterov-type dynamics show. Because $\nabla^2 f(x(t))\dot x(t)$ is the time derivative of $\nabla f(x(t))$, a discretization can use differences of gradients and never evaluate a Hessian. Attouch et al., §1, pp. 1–3.

For a $\mu$-strongly convex objective, the paper shows that the dynamic

$$\ddot x(t)+2\sqrt\mu\,\dot x(t)+\beta\nabla^2f(x(t))\dot x(t)+\nabla f(x(t))=0$$

makes $f(x(t))-\min f$ decay like $e^{-\frac{\sqrt\mu}{2}t}$ (Theorem 7, p. 19). Section 5.1 asks whether that rate survives an implicit (proximal) discretization. The answer is Theorem 9: the algorithm converges linearly, and the gradients also go to zero at a geometric rate. The authors remark that they know of no earlier result of this kind for such a proximal algorithm. Attouch et al., Theorem 9 and Remark 9, p. 23.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$, and let $f:H\to\mathbb R$ be convex and continuously differentiable, with gradient $\nabla f$. For $\mu>0$, $f$ is $\mu$-strongly convex when $z\mapsto f(z)-\frac\mu2\|z\|^2$ is convex (Definition 1, p. 19). Such an $f$ has at most one minimizer; write $x^\star$ for it.

For $\gamma>0$ and $y\in H$, the proximal point $\operatorname{prox}_{\gamma f}(y)$ is the minimizer of $z\mapsto\gamma f(z)+\frac12\|z-y\|^2$.

Fix $\beta\ge0$ and a step $s>0$ (the paper writes $s=h^2$ with $h$ the step size). Starting from arbitrary $x_0,x_1\in H$, the inertial proximal algorithm with Hessian damping for strongly convex functions, (IPAHD-SC), produces for $k\ge1$

$$\begin{cases} y_k=x_k+\Big(1-\frac{2\sqrt{\mu s}}{1+2\sqrt{\mu s}}\Big)(x_k-x_{k-1})+\beta\sqrt s\Big(1-\frac{2\sqrt{\mu s}}{1+2\sqrt{\mu s}}\Big)\nabla f(x_k),\\[4pt] x_{k+1}=\operatorname{prox}_{\frac{\beta\sqrt s+s}{1+2\sqrt{\mu s}}f}(y_k). \end{cases}$$

The first line is an extrapolation with momentum and an explicit gradient correction; the second is one implicit (proximal) step. Attouch et al., (IPAHD-SC), p. 23.

The rates are

$$q=\frac{1}{1+\frac12\sqrt{\mu s}},\qquad \theta=\frac{1}{1+\sqrt{\mu s}},$$

both in $]0,1[$, and the constant of the theorem is

$$E_1=f(x_1)-f(x^\star)+\tfrac12\Big\|\sqrt\mu(x_1-x^\star)+\tfrac{1}{\sqrt s}(x_1-x_0)+\beta\nabla f(x_1)\Big\|^2.$$

Formalization targets

Goal: Theorem 9

Assume $0\le\beta\le\frac{1}{2\sqrt\mu}$ and $\sqrt s\le\beta$. Then every sequence generated by (IPAHD-SC) satisfies, for every $k\ge1$,

$$\frac\mu2\|x_k-x^\star\|^2\le f(x_k)-\min_H f\le E_1q^{k-1},$$

and

$$\theta^k\sum_{j=0}^{k-2}\theta^{-j}\|\nabla f(x_j)\|^2=\mathcal O(q^k)\qquad(k\to+\infty).$$

Milestones

The milestone targets are the paper's displayed intermediate claims, in order:

1. the equivalent second-order form (20) of the algorithm;
2. the increment of the auxiliary vector $v_k=\sqrt\mu(x_k-x^\star)+\frac{1}{\sqrt s}(x_k-x_{k-1})+\beta\nabla f(x_k)$;
3. the two "elementary algebra" quadratic-form inequalities, Term 1 and Term 2;
4. the one-step inequality $\frac{1}{\sqrt s}(E_{k+1}-E_k)+\frac12\sqrt\mu E_{k+1}\le0$ for $E_k=f(x_k)-f(x^\star)+\frac12\|v_k\|^2$;
5. the energy decay (21), $E_k\le E_1q^{k-1}$;
6. the recursive inequality (22) for $Z_k=2\beta(f(x_k)-f(x^\star))+\sqrt\mu\|x_k-x^\star\|^2$;
7. the discounted gradient-sum bound (24).

Significance

Theorem 9 gives linear convergence of a proximal algorithm for a smooth strongly convex objective with no Lipschitz assumption on $\nabla f$ and no upper bound on the step in terms of a smoothness constant: the step condition $\sqrt s\le\beta\le\frac1{2\sqrt\mu}$ involves only the strong convexity modulus. It also gives a geometric rate for a weighted sum of squared gradients, which the authors present as new for proximal algorithms of this type. In §5.1.2 the same estimate, applied to the Moreau envelope, gives linear convergence for nonsmooth strongly convex objectives (Theorem 10), and §5.2 shows the explicit gradient counterpart (Theorem 11).

The result is proved in the paper. A formal development would certify the exact constants ($q$, $\theta$, and the factor $4E_1/\sqrt\mu$ in (24)) and the index bookkeeping of the gradient sums, where the printed proof contains small slips. It would also provide reusable proximal optimality and strong convexity results for later formalizations.

Difficulty

The continuous-time estimate of Theorem 7 does not transfer term by term to the discrete energy $E_k$. Its difference contains cross terms such as $\beta\mu\langle\nabla f(x_{k+1}),x_{k+1}-x^\star\rangle$ and $\sqrt\mu\langle\nabla f(x_{k+1}),x_{k+1}-x_k\rangle$, whose signs are not automatic. The upper bound on $\beta$ and the lower bound on $\sqrt s$ must both survive the resulting estimates. The gradient conclusion introduces a separate weighted sum, with different index ranges in Theorem 9 and the final displayed line of its proof. The algorithm begins at $k=1$ and uses two free initial points, $x_0$ and $x_1$.

Formalization scope

The Lean development works on a real Hilbert space H (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), with $\nabla f$ Mathlib's gradient f. Conventions:

• Hypotheses. $f$ is ConvexOn ℝ Set.univ f and ContDiff ℝ 1 f, and $\mu$-strongly convex in the literal sense of Definition 1 (HessianDamping.DINSC.IsStronglyConvex, convexity of $f-\frac\mu2\|\cdot\|^2$), with $0<\mu$. The standing assumption $\operatorname{argmin}f\neq\emptyset$ is a point $x^\star$ with $f(x^\star)\le f(y)$ for every $y$, so $\min_H f$ is $f(x^\star)$. The step $s$ is positive, as the page implies ($s=h^2$, $h>0$). The parameter hypotheses are $0\le\beta\le\frac1{2\sqrt\mu}$ and $\sqrt s\le\beta$, as printed.
• Algorithm. The proximal step is the published predicate GoldenRatioVI.Shared.IsProxPoint: $x_{k+1}$ minimizes $z\mapsto\gamma f(z)+\frac12\|z-y_k\|^2$. No proximal function is defined. A run imposes the step for every $k\ge1$; $x_0$ and $x_1$ are free.
• Rates and sums. $q$ and $\theta$ are written with Real.sqrt (μ * s). $\theta^{-j}$ is an integer power. $\sum_{j=0}^{k-2}$ is a sum over Finset.range (k - 1). $\mathcal O(q^k)$ is =O[Filter.atTop] with the constant allowed to depend on all the data. The side claims $0<q<1$ and $0<\theta<1$ are a conjunct of the goal.
• Not trivial. The goal does not assume the energy decay, and it does not state the result for a single parameter choice or a vacuous hypothesis set: the hypotheses hold, for example, for $f=\frac12\|\cdot\|^2$, $\mu=1$, $s=\frac1{16}$, $\beta=\frac14$. The goal also does not mention $v_k$, $E_k$ or $Z_k$; only the printed constant $E_1$ appears.

Infrastructure needed: the first-order optimality condition of a proximal step for a differentiable function, and the first-order characterization of strong convexity, $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac\mu2\|y-x\|^2$, from Definition 1. Both are reusable well beyond this mission, as is the iteration of linear recursive inequalities $a_k\le qa_{k-1}+b_k$. Contributions of either kind, and proofs of the individual milestones, are welcome.

Selected references

• H. Attouch, Z. Chbani, J. Fadili, H. Riahi, First-order optimization algorithms via inertial systems with Hessian driven damping, Mathematical Programming, 2020; preprint arXiv:1907.10536v2. https://arxiv.org/abs/1907.10536
• H. Attouch, J. Peypouquet, P. Redont, Fast convex minimization via inertial dynamics with Hessian driven damping, Journal of Differential Equations 261(10) (2016), 5734–5783. https://doi.org/10.1016/j.jde.2016.08.020
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Computational Mathematics and Mathematical Physics 4 (1964), 1–17. https://doi.org/10.1016/0041-5553(64)90137-5