Convex Optimization

Motivation

Distributionally robust optimization (DRO) replaces the expected loss $E_{P_0}[\ell(\beta^{\mathsf T}X)]$ of a decision $\beta$ under a baseline distribution $P_0$ by its worst case over all distributions $P$ that are close to $P_0$. When closeness is measured by an optimal transport cost, the worst case over this infinite-dimensional ball has a one-dimensional dual: by Theorem 1 of Blanchet, Murthy and Zhang (arXiv:1810.02403v3, Math. Oper. Res. 47(2), 2022), building on the strong duality of Blanchet and Murthy (arXiv:1604.01446),

$$\sup_{P : D_c(P_0, P) \le \delta} E_P\big[\ell(\beta^{\mathsf T}X)\big] = \inf_{\lambda \ge 0} f_\delta(\beta, \lambda).$$

The robust problem $\inf_{\beta \in B} \sup_P E_P[\ell(\beta^{\mathsf T}X)]$ thus becomes a joint minimization of the dual objective $f_\delta$ over $(\beta, \lambda)$. Whether that minimization is a convex program, and on which set the objective is finite, decides whether first-order methods such as the stochastic gradient schemes of the same paper apply at all. This mission formalizes the paper's answer, Theorem 2.

Setting

The data $X$ take values in $\mathbb{R}^d$ with law $P_0$, a Borel probability measure. A decision is a vector $\beta$ in a convex set $B \subseteq \mathbb{R}^d$, the loss is $\ell(\beta^{\mathsf T}x)$ for $\ell : \mathbb{R} \to \mathbb{R}$, and $\delta > 0$ is the transport budget.

The transport cost is the state-dependent Mahalanobis cost $c(x, x') = (x - x')^{\mathsf T}A(x)(x - x')$ for a map $A$ from $\mathbb{R}^d$ to positive definite $d \times d$ matrices. Assumption 1: $c$ is lower semicontinuous (1a), and $\rho_{\min}\|v\|^2 \le v^{\mathsf T}A(x)v \le \rho_{\max}\|v\|^2$ for $P_0$-almost every $x$, with $\rho_{\min} > 0$ (1b). Write $q_\beta(x) = \beta^{\mathsf T}A(x)^{-1}\beta$.

Assumption 2: $\ell$ is convex, its growth exponent

$$\kappa = \inf\Big\{ s \ge 0 : \sup_{u \in \mathbb{R}} \big(\ell(u) - s u^2\big) < \infty \Big\}$$

is finite, and $E_{P_0}\|X\|^4 < \infty$.

For $\gamma \in \mathbb{R}$, $\lambda \ge 0$ and $x \in \mathbb{R}^d$ define, as in display (7),

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

the robust loss $\ell_{rob}(\beta, \lambda; x) = \sup_{\gamma \in \mathbb{R}} F(\gamma, \beta, \lambda; x) \in \mathbb{R} \cup \{+\infty\}$, its set of maximizers $\Gamma^*(\beta, \lambda; x)$, and the dual objective

$$f_\delta(\beta, \lambda) = E_{P_0}\big[\ell_{rob}(\beta, \lambda; X)\big] \in \mathbb{R} \cup \{\pm\infty\}.$$

The effective domain is $\mathbb{U} = \{(\beta, \lambda) \in B \times \mathbb{R}_+ : f_\delta(\beta, \lambda) < \infty\}$, and with the threshold $\lambda_{thr}(\beta) = \kappa\sqrt{\delta}\,\operatorname{ess\,sup}_{P_0} q_\beta$ the paper sets $\mathbb{U}_1 = \{\lambda > \lambda_{thr}(\beta)\}$ and $\mathbb{U}_2 = \{\lambda \ge \lambda_{thr}(\beta)\}$ inside $B \times \mathbb{R}_+$.

Formalization targets

Goal: Theorem 2 (p. 10)

Under Assumptions 1 and 2, $f_\delta : B \times \mathbb{R}_+ \to \mathbb{R} \cup \{\infty\}$ is proper and convex: $f_\delta > -\infty$ on $B \times \mathbb{R}_+$; for each $\beta \in B$ some $\lambda \ge 0$ has $f_\delta(\beta, \lambda) < \infty$; and for $\theta_1, \theta_2 \in B \times \mathbb{R}_+$, $\alpha \in [0, 1]$,

$$f_\delta\big(\alpha\theta_1 + (1 - \alpha)\theta_2\big) \le \alpha f_\delta(\theta_1) + (1 - \alpha) f_\delta(\theta_2).$$

Milestones

1. Lemma 3 (p. 32). For each $\varepsilon > 0$ there are $C_1, C_2 > 0$, not depending on $x$, $\beta$, $\lambda$, such that whenever $\lambda \ge (\kappa + \varepsilon)\sqrt{\delta}\,q_\beta(x)$ we have $\sqrt{\delta}|g|q_\beta(x) \le 1 + C_1\varepsilon^{-1}(1 + |\beta^{\mathsf T}x|)$ for every $g \in \Gamma^*(\beta, \lambda; x)$, and $\ell_{rob}(\beta, \lambda; x) \le \lambda\sqrt{\delta} + C_2(1 + \varepsilon + \varepsilon^{-1})(1 + |\beta^{\mathsf T}x|)^2$.
2. Display (25) (p. 32). $\sup_{\Delta \in \mathbb{R}^d}\{\ell(\beta^{\mathsf T}(x + \Delta)) - \tfrac{\lambda}{\sqrt\delta}(\Delta^{\mathsf T}A(x)\Delta - \delta)\} = \ell_{rob}(\beta, \lambda; x)$.
3. Lemma 2 (p. 16). $(\beta, \lambda) \mapsto \ell_{rob}(\beta, \lambda; x)$ is convex on $B \times \mathbb{R}_+$ for every $x$.
4. Lemma 1 (p. 16). $\Gamma^* \neq \emptyset$ and $\ell_{rob}$ finite if $\lambda > \kappa\sqrt{\delta}\,q_\beta(x)$; $\Gamma^* = \emptyset$ and $\ell_{rob} = \infty$ if $\lambda < \kappa\sqrt{\delta}\,q_\beta(x)$; consequently $\mathbb{U}_1 \subseteq \mathbb{U} \subseteq \mathbb{U}_2$.

Lemma 3 is stated with constants depending only on $\varepsilon$ (and the fixed data), as its proof produces them and as the paper's later arguments integrate bound (b) over $x$.

Significance

Theorem 2 is the structural fact behind the paper's algorithms: with Theorem 1 it turns a minimax problem over probability measures into a convex minimization in $d + 1$ real variables, on which the paper's strong convexity results (Theorems 3–5) and its stochastic gradient schemes are built. Lemma 1 identifies the effective domain up to its boundary, which tells an algorithm where the dual multiplier must lie, and Lemma 3 gives the growth control of the robust loss used throughout the appendix.

The results are proved in the paper; none of them has a machine-checked proof. The mission produces a Lean statement of the dual objective as an extended-real integral and of its convexity and properness, reusable by the other missions of this series (strong convexity near the optimizers, worst-case distributions, comparative statics in $\delta$), and contributions of formal proofs of the milestones and the goal.

Difficulty

The objective takes the value $+\infty$ on part of its domain: Lemma 1(b) shows that $\ell_{rob} = +\infty$ below the threshold, so the naive reading "$f_\delta$ is a real convex function" is false, and convexity must be handled for functions with values in $\mathbb{R} \cup \{\infty\}$, including the conventions $0 \cdot \infty = 0$ at the endpoints of the segment. Properness requires a bound on $\ell_{rob}$ that is integrable in $x$, so the constants of Lemma 3 must not depend on $x$; a bound that is only pointwise finite does not suffice. The identity (25) relates a supremum over $\mathbb{R}^d$ to a supremum over $\mathbb{R}$ through a change of the dual variable, and the two multipliers must be kept apart. Finally, the expectation in $f_\delta$ is an integral of an extended-real function whose measurability is not assumed but has to be derived from Assumption 1.

Formalization scope

$\mathbb{R}^d$ is EuclideanSpace ℝ (Fin d) and parameters $(\beta, \lambda)$ live in EuclideanSpace ℝ (Fin d) × ℝ. $\ell_{rob}$ is an EReal supremum; $f_\delta$ is the published ModelRiskOT.Duality.extIntegral, $\int \varphi^+\,dP_0 - \int \varphi^-\,dP_0$ with lower Lebesgue integrals. $\kappa$ is a real infimum and $\lambda_{thr}$ uses the real essential supremum; both are used only under Assumptions 1–2, which make them meaningful. Convexity of extended-real maps is written as the explicit inequality in EReal, since ConvexOn does not apply.

Standing assumptions carried by every statement: $P_0$ a probability measure, $\delta > 0$, $B$ convex (the paper's standing assumption). Conventions committed to: "for any $x$" in Lemmas 1–2 is every $x$, not almost every; Lemma 2 assumes only Assumption 1a and the convexity of $\ell$; the identity (25) is stated with the old multiplier written as $\lambda/\sqrt{\delta}$; the typo "$\beta A(x)^{-1}\beta$" in Lemma 1 is read as $\beta^{\mathsf T}A(x)^{-1}\beta$; the goal's "finite somewhere" is stated for each $\beta \in B$, so the goal is vacuous only when $B = \emptyset$. The fourth-moment condition of Assumption 2 is kept as printed.

A trivializing formalization is ruled out: "proper" is not encoded as "finite everywhere" (false by Lemma 1(b)), and pointwise convexity of $\ell_{rob}$ (Lemma 2) is a milestone, not the goal, which is about the expectation $f_\delta$.

A complete development needs: positive definite matrices and the quadratic minimization behind (25); continuity of convex functions and growth bounds; lower Lebesgue integrals of extended-real functions and their monotonicity and additivity; measurability of a supremum over $\gamma$ of continuous functions. The definitions layer is shared with the other four missions of this series. Proofs of any milestone and of the goal are welcome.

Selected references

• J. Blanchet, K. Murthy, F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Mathematics of Operations Research 47(2), 2022. arXiv:1810.02403v3, doi:10.1287/moor.2021.1178
• J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research 44(2), 2019. arXiv:1604.01446, doi:10.1287/moor.2018.0936

Motivation

Accelerated first-order methods for convex minimization, starting with Nesterov's 1983 scheme, reach the rate $f(x_k)-\min f=\mathcal O(1/k^2)$, which is optimal for the class of convex functions with Lipschitz gradient. Su, Boyd and Candès (NIPS 2014; JMLR 2016) showed that Nesterov's method is a discretization of the second-order ODE $\ddot x+\frac3t\dot x+\nabla f(x)=0$, and since then continuous-time inertial dynamics have been the main tool for designing and analysing accelerated algorithms: a Lyapunov argument for the ODE is found first, and then transcribed to the discrete scheme.

Nesterov-type methods oscillate. Adding to the dynamic a damping term driven by the Hessian, $\beta(t)\nabla^2f(x(t))\dot x(t)$, attenuates these oscillations, and because $\nabla^2f(x(t))\dot x(t)$ is the time derivative of $\nabla f(x(t))$, time discretizations of such dynamics remain first-order methods. Attouch, Chbani, Fadili and Riahi (arXiv:1907.10536, Math. Program. 2020) develop this programme. This mission formalizes its first result: a convergence-rate theorem for the continuous dynamic with general damping and time-scale functions.

Timeline.

• 2014: Su, Boyd and Candès identify $\ddot x+\frac3t\dot x+\nabla f(x)=0$ as the continuous limit of Nesterov's method and prove $\mathcal O(1/t^2)$.
• 2016: Attouch, Peypouquet and Redont (J. Differential Equations 261; reference [12] of arXiv:1907.10536) add the constant Hessian damping $\beta\nabla^2 f(x)\dot x$, prove $\mathcal O(1/t^2)$ for $\alpha>3$ and $\int t^2\|\nabla f(x(t))\|^2dt<\infty$.
• 2019–2020: Attouch, Chbani, Fadili and Riahi allow time-dependent $\beta(t)$ and a time scale $b(t)$, and isolate the growth conditions $(\mathcal G_2)$, $(\mathcal G_3)$ under which the Lyapunov argument works (Theorem 1 here).

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $f:\mathcal H\to\mathbb R$ be a convex function of class $\mathcal C^2$ that attains its minimum at some point $x^\star$. Fix a starting time $t_0>0$, a constant $\alpha\ge1$, and two non-negative continuous functions $\beta,b:[t_0,+\infty[\to\mathbb R_+$. These are the paper's standing assumptions (H).

A solution trajectory of

$$(\mathrm{DIN\text{-}AVD})_{\alpha,\beta,b}\qquad \ddot x(t)+\frac{\alpha}{t}\dot x(t)+\beta(t)\nabla^2 f(x(t))\dot x(t)+b(t)\nabla f(x(t))=0$$

is a twice differentiable curve $x:[t_0,+\infty[\to\mathcal H$ satisfying this equation at every $t\ge t_0$. The coefficient $\alpha/t$ is an asymptotically vanishing viscous damping, $\beta(t)$ weights the Hessian-driven damping, and $b(t)$ is a time-scale factor in front of the gradient.

When $\beta$ is differentiable, set

$$w(t):=b(t)-\dot\beta(t)-\frac{\beta(t)}{t},\qquad \delta(t):=t^2w(t).$$

The rate in Theorem 1 is expressed through $w$.

Formalization targets

Goal: Theorem 1

Assume $w$ is differentiable and the growth conditions

$$(\mathcal G_2)\quad b(t)>\dot\beta(t)+\frac{\beta(t)}{t},\qquad (\mathcal G_3)\quad t\dot w(t)\le(\alpha-3)w(t)$$

hold for all $t\ge t_0$. Then $w(t)>0$ and

$$f(x(t))-\min_{\mathcal H}f=\mathcal O\!\Big(\frac1{t^2w(t)}\Big),\qquad \int_{t_0}^{\infty}t^2\beta(t)w(t)\|\nabla f(x(t))\|^2dt<\infty,$$ $$\int_{t_0}^{\infty}t\big((\alpha-3)w(t)-t\dot w(t)\big)\big(f(x(t))-\min f\big)dt<\infty .$$

The goal leaves $\beta$ and $b$ general. Specific choices are the companions below.

Milestones

The paper's own proof steps, in order:

1. the derivative (3) of the energy $E(t)=\delta(t)(f(x(t))-f(x^\star))+\frac12\|v(t)\|^2$, where $v(t)=(\alpha-1)(x(t)-x^\star)+t(\dot x(t)+\beta(t)\nabla f(x(t)))$;
2. the identity $\dot v(t)=t[\dot\beta(t)+\beta(t)/t-b(t)]\nabla f(x(t))$;
3. the differential inequality (4);
4. the monotonicity of $E$ via (5)–(6);
5. the two integral bounds by $E(t_0)$.

Companions

• Theorem 3: $\beta(t)\equiv\beta$, $b(t)=1+\beta/t$, $\alpha\ge3$ give $\mathcal O(1/t^2)$ and, for $\beta>0$, $\int t^2\|\nabla f(x(t))\|^2<\infty$.
• Theorem 2: the Attouch–Peypouquet–Redont case $b\equiv1$, $\alpha>3$, with the same conclusions.

Significance

The result. Theorem 1 contains the $\mathcal O(1/t^2)$ rate of the continuous Nesterov dynamic as the case $\beta\equiv0$, $b\equiv1$, $\alpha\ge3$. It recovers the Attouch–Peypouquet–Redont theorem and the vanishing-coefficient system of Case 2 as special cases. The time scale $b$ gives faster rates $\mathcal O(1/(t^2w(t)))$ when $w$ grows. For $\beta>0$ it also gives the integral estimate on $\|\nabla f(x(t))\|^2$, which is the continuous counterpart of the fast decay of gradients proved for the algorithms (IPAHD) and (IGAHD) later in the paper.

Formalizing it. The result is proved in the paper, and nothing about it has been machine-checked. The mission produces:

• a reusable predicate for solutions of second-order ODEs with Hessian damping on a half-line;
• the Lyapunov identity and inequality for that predicate;
• a checked version of the integration step that turns a pointwise differential inequality into finite integrals.

Difficulty

The energy estimate is an exact computation that has to match term by term. The cross terms $\langle\nabla f(x(t)),\dot x(t)\rangle$ cancel only because $\delta=t^2w$ is chosen to match $\dot v$. That computation needs the chain rule $\frac{d}{dt}\nabla f(x(t))=\nabla^2 f(x(t))\dot x(t)$ in a Hilbert space.

The naive conclusion "$\dot E\le0$, so integrate (4)" hides two analytic steps:

• monotonicity from a one-sided derivative on a closed half-line;
• integrability on an unbounded interval of non-negative functions that need not be continuous, because $\dot w$ is only assumed to exist.

The (i) rate needs the positivity of $w$ from $(\mathcal G_2)$ to divide by $\delta(t)$.

Formalization scope

Lean conventions:

• $\mathcal H$ is a real inner product space that is complete. $\nabla f$ is Mathlib's gradient f, and $\nabla^2 f(x)u$ is fderiv ℝ (gradient f) x u.
• Trajectories are maps $\mathbb R\to\mathcal H$ with explicit velocity and acceleration maps, tied to them by HasDerivWithinAt on $[t_0,+\infty[$. Values before $t_0$ are irrelevant, and derivatives at $t_0$ are one-sided.
• $\dot\beta$ and $\dot w$ are explicit maps with derivative hypotheses. The paper writes them, so it presupposes they exist.
• $\min f$ is $f(x^\star)$ for a given global minimizer. $\mathcal O$ is =O[atTop], with constants depending on all data.
• "$\int<\infty$" is IntegrableOn on $[t_0,+\infty[$, never a bound on a Bochner integral that could be the junk value $0$.

These choices rule out trivial readings: Lean's zero value for the derivative of a non-differentiable function, an ODE with an unlinked velocity, and an integral that is zero because the integrand is not integrable. The goal assumes nothing about $E$, $v$ or (4)–(6), which appear only in milestones.

Companion items:

• Theorems 2 and 3 add $\beta>0$ to the gradient-integral claim. The paper derives it from Theorem 1 (ii), which carries a factor $\beta$, so it says nothing at $\beta=0$.
• Theorem 2 must cope with growth conditions that hold only for large $t$.

Contributions are welcome: the chain rule for gradient along a curve, a monotonicity lemma for one-sided derivatives on Ici, and the integrability lemma for non-negative functions bounded by a non-increasing energy.

Selected references

• H. Attouch, Z. Chbani, J. Fadili, H. Riahi, First-order optimization algorithms via inertial systems with Hessian driven damping, Math. Program. (2020); 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, J. Differential Equations 261, No. 10 (2016) 5734–5783 (as cited in arXiv:1907.10536v2, ref. [12]). https://arxiv.org/abs/1907.10536
• W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, NIPS 27 (2014) 2510–2518; journal version J. Mach. Learn. Res. 17 (2016). https://jmlr.org/papers/v17/15-084.html
• Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Math. Dokl. 27 (1983) 372–376.

Motivation

Accelerated first-order methods, such as Nesterov's method and FISTA, reach a convergence rate of $\mathcal O(1/k^2)$ on the objective values of a smooth convex function, against $\mathcal O(1/k)$ for plain gradient descent. Since the work of Su, Boyd and Candès (arXiv:1503.01243), these methods are studied through their continuous-time limits, second-order differential equations with a vanishing viscous damping $\frac{\alpha}{t}\dot x$. The trajectories of these equations, and the iterates of the corresponding algorithms, oscillate strongly around the minimizers.

Adding a Hessian-driven damping term $\beta(t)\nabla^2 f(x(t))\dot x(t)$ to the dynamic damps these oscillations while keeping the fast rate. The idea goes back to Alvarez, Attouch, Bolte and Redont (2002) and was developed for fast convex minimization by Attouch, Peypouquet and Redont (arXiv:1601.07113, J. Differential Equations 2016). Shi, Du, Jordan and Su (arXiv:1810.08907) showed that the gradient-correction term of Nesterov's method is exactly such a Hessian damping, observed in a high-resolution limit. Because $\nabla^2 f(x(t))\dot x(t)$ is the time derivative of $\nabla f(x(t))$, the Hessian never has to be evaluated after discretization, and the resulting algorithms are genuinely first-order.

Attouch, Chbani, Fadili and Riahi (arXiv:1907.10536, Math. Program. 2020) study the system (DIN-AVD)$_{\alpha,\beta,b}$, $\ddot x+\frac{\alpha}{t}\dot x+\beta(t)\nabla^2f(x)\dot x+b(t)\nabla f(x)=0$, with general time-dependent coefficients, and derive algorithms from it. This mission formalizes their first discrete result: the convergence rate of the implicit (proximal) discretization.

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$, and let $f:\mathcal H\to\mathbb R$ be a convex function of class $\mathcal C^1$ with gradient $\nabla f$, attaining its minimum at some point $x^\star$. Fix $\alpha\ge1$, a step size $h>0$ with $s=h^2$, and two non-negative sequences $(\beta_k)_{k\in\mathbb N}$ (the Hessian damping) and $(b_k)_{k\in\mathbb N}$ (the time scaling of the gradient).

For $\mu\ge0$ and $y\in\mathcal H$, the proximal point $\mathrm{prox}_{\mu f}(y)$ is the minimizer of $z\mapsto\mu f(z)+\tfrac12\|z-y\|^2$.

The Inertial Proximal Algorithm with Hessian Damping (IPAHD) generates a sequence $(x_k)_{k\in\mathbb N}$ by, for $k\ge1$,

$$\mu_k=\frac{k}{k+\alpha}\big(\beta_k\sqrt s+sb_k\big),\qquad y_k=x_k+\Big(1-\frac{\alpha}{k+\alpha}\Big)(x_k-x_{k-1})+\beta_k\sqrt s\Big(1-\frac{\alpha}{k+\alpha}\Big)\nabla f(x_k),$$ $$x_{k+1}=\mathrm{prox}_{\mu_kf}(y_k).$$

It is the implicit time discretization, with step $h$, of (DIN-AVD)$_{\alpha,\beta,b}$:

$$k(x_{k+1}-2x_k+x_{k-1})+\alpha(x_{k+1}-x_k)+\beta_khk\big(\nabla f(x_{k+1})-\nabla f(x_k)\big)+b_kh^2k\nabla f(x_{k+1})=0. \tag{8}$$

The rate is measured by the sequence

$$\delta_k:=h\big(b_khk-\beta_{k+1}-k(\beta_{k+1}-\beta_k)\big)(k+1), \tag{9}$$

under two growth conditions: $(\mathcal G_2^{\rm dis})$ $b_khk-\beta_{k+1}-k(\beta_{k+1}-\beta_k)>0$ and $(\mathcal G_3^{\rm dis})$ $\delta_{k+1}-\delta_k\le(\alpha-1)\frac{\delta_k}{k+1}$. They are the discrete counterparts of the conditions $(\mathcal G_2)$, $(\mathcal G_3)$ of the continuous analysis.

Formalization targets

Goal: Theorem 4 (p. 11)

If $(\mathcal G_2^{\rm dis})$ and $(\mathcal G_3^{\rm dis})$ hold for every $k\ge k_0$, for some $k_0\ge1$, then every sequence generated by (IPAHD) satisfies: $\delta_k>0$ for $k\ge k_0$, and

$$f(x_k)-\min_{\mathcal H}f=\mathcal O\Big(\frac1{\delta_k}\Big),\qquad \sum_k\delta_k\beta_{k+1}\|\nabla f(x_{k+1})\|^2<+\infty.$$

The rate is stated in terms of $\delta_k$, with no constant fixed in advance, so it covers every admissible choice of $(\beta_k)$ and $(b_k)$ at once.

Milestones (the steps of the proof, pp. 10–13)

1. Every run of (IPAHD) satisfies (8).
2. Under (8), $v_{k+1}-v_k=h C_k\nabla f(x_{k+1})$, where $v_k:=(\alpha-1)(x_k-x^\star)+k(x_k-x_{k-1}+\beta_kh\nabla f(x_k))$ and $C_k=\beta_{k+1}+k(\beta_{k+1}-\beta_k)-b_khk$.
3. $\tfrac12\|v_{k+1}\|^2-\tfrac12\|v_k\|^2\le-(\alpha-1)hC_k(f(x^\star)-f(x_{k+1}))-hC_k(k+1)(f(x_k)-f(x_{k+1}))$.
4. For the energy $E_k:=\delta_k(f(x_k)-f(x^\star))+\tfrac12\|v_k\|^2$: $E_{k+1}-E_k\le\big(\delta_{k+1}-\delta_k-(\alpha-1)\frac{\delta_k}{k+1}\big)(f(x_{k+1})-f(x^\star))$.
5. $f(x_k)-\min f\le E_{k_0}/\delta_k$ for $k\ge k_0$.
6. $E_{k+1}-E_k+h\big(\tfrac h2C_k^2+\delta_k\beta_{k+1}\big)\|\nabla f(x_{k+1})\|^2\le0$.

Significance

With $\beta_k\equiv\beta>0$ and $b_k=1+\beta/(hk)$ one gets $\delta_k=h^2k(k+1)$, so Theorem 4 gives the accelerated rate $\mathcal O(1/k^2)$ for a proximal algorithm with Hessian damping, together with the summability of $k^2\|\nabla f(x_{k+1})\|^2$, a fast decay of the gradients that the plain inertial proximal algorithm does not provide. The time-dependent coefficients let the user trade damping against speed, and Remark 2 of the paper gives $\mathcal O(1/(k(k+1)))$ under a uniform version of $(\mathcal G_2^{\rm dis})$. The proximal scheme only needs $f$ of class $\mathcal C^1$; the non-smooth case (Theorem 5) is obtained from it through the Moreau envelope.

The result is proved in the paper. As far as the platform's catalog shows, neither the algorithm nor any Lyapunov analysis of an inertial algorithm with Hessian-driven damping has been machine-checked. A formal proof would certify a discrete energy argument whose printed version contains an index slip (a dropped factor $k+1$ in an intermediate display on p. 12), and the definitions are reused by the other missions of this series.

Difficulty

The proof is a discrete Lyapunov argument, and the difficulty is bookkeeping rather than a single deep step. The coefficient $\delta_k$ is not chosen in advance: it is forced by the requirement that the terms $f(x_k)-f(x_{k+1})$ cancel in $E_{k+1}-E_k$, and the inequality for $\tfrac12\|v_{k+1}\|^2-\tfrac12\|v_k\|^2$ only closes after the signs of $C_k$, $\beta_{k+1}$ and $\alpha-1$ are used in the right places. The convexity of $f$ enters twice, at different points ($x^\star$ and $x_k$). Reading the proximal step as the first-order optimality condition $x_{k+1}+\mu_k\nabla f(x_{k+1})=y_k$ and converting it into (8) requires matching $\sqrt s$ with $h$ and the coefficient $1-\frac{\alpha}{k+\alpha}$ with $\frac{k}{k+\alpha}$. A naive direct estimate of $f(x_k)-\min f$ from the proximal inequality alone gives only the unaccelerated rate.

Formalization scope

The space is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H], $\nabla f$ is Mathlib's gradient f, convexity is ConvexOn ℝ Set.univ f and $\mathcal C^1$ is ContDiff ℝ 1 f. The minimizer is a point $x^\star$ with $f(x^\star)\le f(y)$ for all $y$, the concrete form of the paper's standing hypothesis $\mathrm{argmin}f\neq\emptyset$. The proximal step is the published predicate GoldenRatioVI.Shared.IsProxPoint: $x_{k+1}$ minimizes $\mu_kf(z)+\tfrac12\|z-y_k\|^2$. No proximal function with a junk value is defined. Sequences are indexed by $\mathbb N$, the recursion is required for $k\ge1$, and $x_0$, $x_1$ are free. $\mathcal O$ is =O[Filter.atTop] and the series is Summable in $\mathbb R$.

Hypotheses added relative to the printed theorem, all disclosed in the statements:

• $h>0$, $s=h^2$;
• $\beta_k,b_k\ge0$ for every $k$, the discrete analogue of the standing hypothesis (H), needed for $\mu_k\ge0$ and used in the proof;
• the growth conditions are assumed for $k\ge k_0$, with $k_0\ge1$.

At $k=0$, $(\mathcal G_2^{\rm dis})$ reads $-\beta_1>0$, so reading the conditions "for all $k$" would make every hypothesis set unsatisfiable and the theorem empty. A sorry-free check shows the hypotheses hold for $\beta\equiv0$, $b\equiv1$, $h=1$, $\alpha=4$, $k_0=2$. The goal statement mentions only $f$, the run and $\delta_k$; it does not refer to $v_k$, $E_k$ or $C_k$, and a formalization that assumes an energy inequality would not prove Theorem 4.

The definitions $\mu_k$, $y_k$, the run predicate, $\delta_k$, $C_k$, $v_k$ and $E_k$ live in one definition file. Proofs of the milestones are welcome individually; the identities (milestones 1–2) are algebra plus the first-order condition of the proximal step, and the inequalities (3–6) need the gradient inequality of a differentiable convex function. Theorem 5 (the non-smooth case) is not part of this mission.

Selected references

• H. Attouch, Z. Chbani, J. Fadili, H. Riahi, First-order optimization algorithms via inertial systems with Hessian driven damping, Math. Program., 2020; 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, J. Differential Equations 261 (2016), 5734–5783. https://arxiv.org/abs/1601.07113
• B. Shi, S. S. Du, M. I. Jordan, W. J. Su, Understanding the acceleration phenomenon via high-resolution differential equations, Math. Program., 2021. https://arxiv.org/abs/1810.08907
• W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, J. Mach. Learn. Res. 17 (2016). https://arxiv.org/abs/1503.01243

Motivation

Many first-order methods for convex minimization — the forward–backward (proximal gradient) method, alternating minimization, trust-region and majorization–minimization schemes — produce sequences that decrease the objective by an amount proportional to the squared step and whose step controls a subgradient at the new point. Luo and Tseng (Ann. Oper. Res. 1993) used such conditions together with error bounds to derive convergence rates, and Attouch, Bolte and Svaiter (Math. Program. 2013) isolated them as an abstract definition of descent sequences analysed through the Kurdyka–Łojasiewicz (KL) inequality. Those analyses give convergence and asymptotic rates, but not explicit complexity bounds with the constants in view.

Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234; Math. Program. 165, 2017) show that, for convex functions, the KL inequality yields such bounds: the values and iterates of every subgradient descent sequence are dominated by an explicit one-dimensional proximal recursion built from the desingularizing function. This is the paper's main theorem (Theorem 16), and the target of this mission.

Setting

Let $H$ be a real Hilbert space and $f : H \to (-\infty, +\infty]$ proper, lower semicontinuous and convex, with $\operatorname{argmin} f \neq \emptyset$ and, after a shift, $\min f = 0$. The subdifferential is

$$\partial f(x) = \{u \in H : f(y) \ge f(x) + \langle u, y - x\rangle \ \text{for all } y\},$$

and $\partial^0 f(x)$ denotes its least-norm element, with $\|\partial^0 f(x)\| = +\infty$ when $\partial f(x) = \emptyset$.

For $\bar r > 0$, the class $\mathcal K(0, \bar r)$ consists of the functions $\varphi$ continuous on $[0, \bar r)$ and $C^1$ on $(0, \bar r)$ with $\varphi(0) = 0$, $\varphi$ concave and $\varphi' > 0$. The function $f$ has the KL property on $[0 < f < \bar r]$ with desingularizing function $\varphi \in \mathcal K(0, \bar r)$ if

$$\varphi'(f(x))\,\|\partial^0 f(x)\| \ge 1 \qquad \text{whenever } 0 < f(x) < \bar r.$$

A sequence $(x_k)_{k \in \mathbb N}$ is a subgradient descent sequence with constants $a, b > 0$ if $x_0 \in \operatorname{dom} f$ and, for every $k \ge 1$,

• (H1) $f(x_k) + a\|x_k - x_{k-1}\|^2 \le f(x_{k-1})$;
• (H2) some $\omega_k \in \partial f(x_k)$ satisfies $\|\omega_k\| \le b\|x_k - x_{k-1}\|$.

Fix $0 < r_0 < \bar r$, put $\alpha_0 = \varphi(r_0)$, and let $\psi = (\varphi|_{[0, r_0]})^{-1} : [0, \alpha_0] \to [0, r_0]$, an increasing convex profile. Assumption (A): $\psi'$ is Lipschitz continuous on $[0, \alpha_0]$ with constant $\ell > 0$, and $\psi'(0) = 0$. With

$$\zeta = \frac{\sqrt{1 + 2\ell a b^{-2}} - 1}{\ell} > 0, \qquad \alpha_{k+1} = \operatorname{argmin}\Big\{\psi(u) + \tfrac{1}{2\zeta}(u - \alpha_k)^2 : u \ge 0\Big\},$$

$(\alpha_k)$ is the one-dimensional worst-case proximal sequence.

Formalization targets

Goal: Theorem 16

If $(x_k)$ is a subgradient descent sequence with $f(x_0) = r_0$ and (A) holds, then $x_k$ converges strongly to a minimizer $x^*$ and

$$f(x_k) \le \psi(\alpha_k) \quad (k \ge 0), \qquad \|x_k - x^*\| \le \frac{b}{a}\,\alpha_k + \sqrt{\frac{\psi(\alpha_{k-1})}{a}} \quad (k \ge 1).$$

Milestones

1. (20), in the proof of Theorem 14: while $f(x_k) > 0$ and $x_k \neq x_{k-1}$, $\varphi(f(x_k)) - \varphi(f(x_{k+1})) \ge \frac{a}{b}\big(2\|x_k - x_{k+1}\| - \|x_{k-1} - x_k\|\big)$.
2. Theorem 14: with only $f(x_0) \le r_0 < \bar r$, $x_k \to x^* \in \operatorname{argmin} f$ strongly and $\|x_k - x^*\| \le \frac{b}{a}\varphi(f(x_k)) + \sqrt{f(x_{k-1})/a}$ for $k \ge 1$.
3. (23): $(\alpha_k)$ exists, is positive, satisfies $\alpha_{k+1} = (I + \zeta\psi')^{-1}(\alpha_k)$, decreases strictly to $0$, and $\psi(\alpha_k) \to 0$.
4. (27): with $\beta_j = \varphi(f(x_j))$, every $k \ge 1$ with $f(x_k) > 0$ has $(\beta_{k-1} - \beta_k)/\psi'(\beta_k) \ge \zeta$.
5. Claim 1: for $\lambda^0 > \lambda^1 > 0$ and $\gamma > 0$, $(I + \lambda^0\psi')^{-1}(\gamma) < (I + \lambda^1\psi')^{-1}(\gamma)$.
6. Claim 2: proximal sequences with step sizes $\lambda^0_k \ge \lambda^1_k > 0$ from a common start in $(0, \alpha_0]$ satisfy $\beta^0_k \le \beta^1_k$.

Significance

Theorem 16 turns the qualitative KL convergence theory into explicit complexity: once a desingularizing function is known, the number of iterations needed to reach a given accuracy, for both the values and the iterates, can be read off a scalar recursion with constants $a$, $b$, $\ell$ taken from the method and the function. The authors apply it, through its corollaries, to obtain the linear rate of ISTA for $\ell^1$-regularized least squares and complexity bounds for projection methods for convex feasibility problems. The bound on $\|x_k - x^*\|$ holds even when $f$ has a continuum of minimizers.

The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. This mission asks for a Lean proof of Theorem 16 and of the six intermediate results its proof uses, each stated with the paper's exact constants.

Difficulty

The convergence part (Theorem 14) is set in an arbitrary Hilbert space: summability of the steps gives only a Cauchy sequence, identifying its limit as a minimizer needs a closedness property of $\partial f$ that is not available in Mathlib for EReal-valued functions, and the degenerate cases ($x_k = x_{k-1}$ or $f(x_k) = 0$ at some step) need separate treatment.

The complexity part requires one-dimensional analysis that Mathlib does not package: derivatives of the inverse $\psi = \varphi^{-1}$ on a closed interval, a descent inequality for $\psi$ when $\psi'$ is Lipschitz only on $[0, \alpha_0]$, and monotonicity of the scalar resolvents $(I + \lambda\psi')^{-1}$. The obvious approach, comparing $f(x_k)$ with $\psi(\alpha_k)$ one step at a time with the same step size, fails: the sequence $\varphi(f(x_k))$ is itself a proximal sequence for $\psi$, but with step sizes that vary with $k$ and are not known in advance.

Formalization scope

• $f$ is a function $H \to$ EReal satisfying the published GammaZero (never $-\infty$, somewhere finite, convex epigraph, lower semicontinuous), with CompleteSpace H. $\partial f$ is the published subgrad; $\min f = 0$ with $\operatorname{argmin} f \neq \emptyset$ is the hypothesis "$f \ge 0$ and $f$ vanishes somewhere".
• The KL inequality is required for every $v \in \partial f(x)$, which is the least-norm form with the convention $\|\partial^0 f(x)\| = +\infty$ off $\operatorname{dom}\partial f$. The class $\mathcal K(0, \bar r)$ is the published IsDesingularizer; $\varphi'$ is deriv φ, used only on $(0, \bar r)$.
• $\psi$ is a real function given as data with $\psi(\varphi(s)) = s$ on $[0, r_0]$; only its values on $[0, \alpha_0]$ matter. $\psi'$ is the derivative within $[0, \alpha_0]$, and the minimization in (22) runs over $[0, \alpha_0]$, the domain of $\psi$. The argmin is unique, so (22) is a predicate on sequences; (23) proves that the predicate is satisfiable, so Theorem 16 is not vacuous. Resolvent points $(I + \lambda\psi')^{-1}(\gamma)$ are likewise predicates.
• $\alpha_0 = \varphi(r_0)$, $\zeta$ and the coefficient $b/a$ are fixed by the data; none is existentially quantified. The inequality $f(x_k) \le \psi(\alpha_k)$ is stated in EReal.
• Claim 2 is printed with $\beta^0_0 = \beta^1_0 \in (0, r_0]$; the resolvents act on $[0, \alpha_0]$ and the claim is applied with $\beta_0 = \alpha_0$, so it is formalized on $(0, \alpha_0]$.
• Theorem numbers, equation numbers and pages refer to the arXiv version arXiv:1510.08234v3, not to the journal version.

Useful infrastructure, reusable beyond this mission: the inverse-function derivative on an interval, the one-dimensional descent lemma with a derivative Lipschitz on a closed interval, and monotonicity of scalar resolvents. Contributions of these as separate lemmas are welcome.

Selected references

• J. Bolte, T. P. Nguyen, J. Peypouquet, B. W. Suter, From error bounds to the complexity of first-order descent methods for convex functions, Math. Program. 165 (2017) 471–507. arXiv:1510.08234v3, doi:10.1007/s10107-016-1091-6
• H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137 (2013) 91–129. doi:10.1007/s10107-011-0484-9
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. doi:10.1007/BF02096261
• J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17 (2007) 1205–1223. doi:10.1137/050644641

Motivation

Accelerated gradient methods use information from earlier iterates to reduce the objective gap of a smooth convex optimization problem faster than ordinary gradient descent. Their behavior depends on the precise momentum rule. Attouch, Chbani, Fadili, and Riahi study a discrete rule with an additional difference of consecutive gradients, motivated by an inertial differential equation with Hessian driven damping. This mission concerns their inertial gradient algorithm with Hessian damping, called IGAHD, and the rates proved for it in Theorem 6 of the source paper. The result matters when one wants a rate for objective values together with control of the gradients seen during the run.

The paper appeared as a 2020 preprint and subsequently in Mathematical Programming. The mission follows the pinned arXiv version, whose theorem and equation numbers supply all citations here. The proximal and strongly convex algorithms elsewhere in the paper have separate missions; their dynamics and rate statements differ from IGAHD.

Setting

Let $H$ be a real Hilbert space and let $f:H\to\mathbb R$ be convex and differentiable. Assume that its gradient $\nabla f$ is $L$-Lipschitz: $\|\nabla f(u)-\nabla f(v)\|\le L\|u-v\|$ for every $u,v\in H$, where $L>0$. Choose a minimizer $x^*$, so $f(x^*)=\min_H f$. The positive step size $s$ satisfies $s\le1/L$. The momentum parameter $\alpha$ is at least $3$, and the damping parameter $\beta$ lies in $[0,2\sqrt{s})$.

Given $x_0,x_1\in H$, the algorithm takes the following two steps for every integer $k\ge1$:

$$\begin{aligned} y_k={}&x_k+\left(1-\frac{\alpha}{k}\right)(x_k-x_{k-1}) -\beta\sqrt{s}\bigl(\nabla f(x_k)-\nabla f(x_{k-1})\bigr) -\frac{\beta\sqrt{s}}{k}\nabla f(x_{k-1}),\\ x_{k+1}={}&y_k-s\nabla f(y_k). \end{aligned}$$

The paper sets $t_{k+1}=k/(\alpha-1)$ and $v_k=x_{k-1}-x^*+t_k(x_k-x_{k-1}+\beta\sqrt{s}\nabla f(x_{k-1}))$. Its Lyapunov quantity is $E_k=t_k^2(f(x_k)-f(x^*))+(2s)^{-1}\|v_k\|^2$ for $k\ge1$. These expressions are fixed by the source formulas (14)–(15), p. 15, not chosen to simplify a later proof.

Formalization targets

The central target is the full rate statement of Theorem 6. In the range where the paper's monotonicity argument applies, $E_k$ is eventually nonincreasing. For every IGAHD run,

$$f(x_k)-\min_H f=O(k^{-2})\quad(k\to\infty).$$

When $\beta>0$, the theorem also gives both weighted gradient summability claims:

$$\sum_{k\ge0} k^2\|\nabla f(y_k)\|^2<\infty, \qquad \sum_{k\ge0} k^2\|\nabla f(x_k)\|^2<\infty.$$

The milestone list follows claims the authors state while proving that target. It begins with the extended descent inequality (Lemma 1, (28)), records the identities for $t_k$ and $v_k$, and then captures the displayed energy and $\varepsilon$ inequalities. Remark 4 asks for the $O(k^{-3})$ bound on the smallest squared gradient norm among the first $k$ iterates; Remark 5 asks for the $O(k^{-2})$ objective gap at $y_k$. Those are companion statements and are not substituted for the main theorem.

Significance

The rate bounds give three kinds of information about one trajectory. The objective gap controls the values attained at the iterates. The two summable series imply that the gradients at both the extrapolated points and the iterates become small in a weighted aggregate sense when damping is positive. The paper then uses this series estimate to derive the best-iterate estimate of Remark 4 and the extrapolated-value estimate of Remark 5, all on p. 18.

The result is proved in the cited paper; the open work here is its Lean proof and the supporting smooth convex analysis. The development makes the precise discrete algorithm, the Lyapunov quantity, and the descent inequality reusable as mathematical interfaces. A complete formal proof would also make explicit where the author's finite-index monotonicity wording needs correction.

Difficulty

The usual smooth descent estimate alone gives a decrease after one gradient step, but the extrapolated point $y_k$ also carries a momentum term and a gradient difference. Its objective value is therefore not the same quantity as $f(x_k)$, and a direct comparison of successive objective values does not give the claimed summability. The source uses a stronger descent inequality with a squared difference of gradients. The energy change then contains a quadratic expression in $\nabla f(y_k)$ and $\nabla f(x_k)$ whose sign depends on $\beta<2\sqrt{s}$ and, at first, on how large $k$ is. Establishing that sign uniformly over the relevant tail of the run is the central obstruction.

Formalization scope

The Lean space is a complete real inner product space. Convexity is ConvexOn ℝ Set.univ f; differentiability is explicit because the phrase “whose gradient is $L$-Lipschitz” presupposes a gradient. The existence of a minimizer is represented by a selected $x^*$ with $f(x^*)\le f(z)$ for every $z$. Positive $L$ and positive $s$ make $s\le1/L$ meaningful. The algorithm is a predicate on sequences $x,y:\mathbb N\to H$, imposed from $k=1$ so no coefficient is divided by zero. The first two $x$ terms are free, and $y_0$ is unused. The $O$ statements use the filter at infinity, so finite initial terms do not affect them; summability uses the ordinary series over natural indices.

The printed claim that $(E_k)$ is nonincreasing from its first term is false for the paper's own definitions. On $H=\mathbb R$ with $f(u)=u^2/2$, $L=s=1$, $\alpha=3$, $\beta=0$, $x_0=0$, and $x_1=1$, one gets $E_1=0$ and $E_2=1/8$. The formal goal keeps eventual monotonicity, as supported by the proof on pp. 16–18. This correction is disclosed rather than treated as a new hypothesis. No energy decrease, gradient bound, or conclusion is assumed in the run predicate. The milestone definitions also specify $B_k$ exactly as on p. 17. Contributions to the goal, to the extended descent lemma, or to the explicit energy estimates are all useful; the definition layer and smooth convex lemmas can serve later optimization formalizations.

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, especially §3.2, pp. 15–18, and Appendix A.1, p. 34.