Theorem 6.1 — the Hessian-step gradient method converges linearly: locally (6.3), and globally when damped (6.4)

Proved

FatkhullinPolyak.HessStep.hessian_step_linear_rate

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

gradient-descentlinear-convergencep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1step-sizestrong-convexity

Let $f:\mathbb{R}^n\to\mathbb{R}$ be a twice differentiable, $\mu$ -strongly convex function ( $\mu>0$ ) whose gradient $\nabla f$ is Lipschitz continuous with constant $L$ and whose Hessian $\nabla^2 f$ is Lipschitz continuous with constant $M$ (operator norm). Let $x_*$ be its global minimizer. Consider the gradient method (6.1)

x_{j+1}=x_j-\gamma_j\nabla f(x_j),\qquad \gamma_j=\frac{\|\nabla f(x_j)\|^2}{\langle\nabla^2 f(x_j)\nabla f(x_j),\nabla f(x_j)\rangle}.

Then:

Local linear rate. If $\delta>0$ and the initial point $x_0$ satisfies

M\sqrt{2L\bigl(f(x_0)-f(x_*)\bigr)}\le 3\mu^2(1-\delta),\tag{6.2}

then the iterates of (6.1) satisfy, for every $j\ge0$ ,

f(x_j)-f(x_*)\le\bigl(f(x_0)-f(x_*)\bigr)\Bigl(1-\frac{\mu\delta}{L}\Bigr)^j.\tag{6.3}

Global linear rate of the damped method. If $0<\sigma\le\mu/L$ , then for every initial point $x_0$ the iterates of the damped method $x_{j+1}=x_j-\sigma\gamma_j\nabla f(x_j)$ satisfy, for every $j\ge0$ ,

f(x_j)-f(x_*)\le\bigl(f(x_0)-f(x_*)\bigr)\Bigl(1-\frac{\mu\sigma}{L}\Bigr)^j.\tag{6.4}

The step size of (6.1) uses one Hessian–vector product and no knowledge of $L$ or $\mu$ . The theorem justifies it for nonquadratic strongly convex functions: linear convergence near the minimizer, and from any starting point once the step is damped by $\sigma\le\mu/L$ .

Formalization Note Both claims share the hypotheses of the theorem as printed, including the Lipschitz Hessian, although the damped claim does not use $M$ . The damping positivity $\sigma>0$ is implicit on the page and added. Condition (6.2) is a hypothesis on $x_0$ only. When $\delta>1$ it cannot hold (its left side is nonnegative), so claim 1 is then vacuous, as on the page. The minimizer is taken as a hypothesis ( $f(x_*)\le f(y)$ for all $y$ ), not constructed. At a stationary iterate the step is $0/0=0$ in Lean, so the method stays at the minimizer and both bounds still hold. Strong convexity is Mathlib's StrongConvexOn Set.univ μ f (modulus $\frac{\mu}{2}\|x-y\|^2$ ). $L$ and $M$ are real constants in the Lipschitz inequalities $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ and $\|\nabla^2 f(x)-\nabla^2 f(y)\|\le M\|x-y\|$ .

Preamble

import Mathlib
import Definitions.Def_FatkhullinPolyak_HessStep_hessianStepMethod

Formal statement

namespace FatkhullinPolyak.HessStep

theorem hessian_step_linear_rate {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (μ L M : ℝ)
    (xstar : EuclideanSpace ℝ (Fin n))
    (hf : Differentiable ℝ f) (hf' : Differentiable ℝ (fderiv ℝ f))
    (hμ : 0 < μ) (hconv : StrongConvexOn Set.univ μ f)
    (hL : ∀ x y : EuclideanSpace ℝ (Fin n), ‖gradient f x - gradient f y‖ ≤ L * ‖x - y‖)
    (hM : ∀ x y : EuclideanSpace ℝ (Fin n),
      ‖fderiv ℝ (fderiv ℝ f) x - fderiv ℝ (fderiv ℝ f) y‖ ≤ M * ‖x - y‖)
    (hmin : ∀ y : EuclideanSpace ℝ (Fin n), f xstar ≤ f y) :
    (∀ (δ : ℝ) (x₀ : EuclideanSpace ℝ (Fin n)), 0 < δ →
        M * Real.sqrt (2 * L * (f x₀ - f xstar)) ≤ 3 * μ ^ 2 * (1 - δ) →
        ∀ j : ℕ, f (hessIter f x₀ j) - f xstar ≤ (f x₀ - f xstar) * (1 - μ * δ / L) ^ j) ∧
    (∀ σ : ℝ, 0 < σ → σ ≤ μ / L → ∀ (x₀ : EuclideanSpace ℝ (Fin n)) (j : ℕ),
        f (dampedHessIter f σ x₀ j) - f xstar ≤ (f x₀ - f xstar) * (1 - μ * σ / L) ^ j) := by sorry

end FatkhullinPolyak.HessStep

Source

Fatkhullin, Polyak, Optimizing Static Linear Feedback: Gradient Method, arXiv:2004.09875v2, p. 13, Theorem 6.1, Eqs. (6.1)-(6.4); proof in Appendix D.4, p. 19

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

The statement concerns a real-valued function $f:\mathbb{R}^n\to\mathbb{R}$ on $n$ -dimensional Euclidean space, where the dimension $n\in\mathbb{N}$ is arbitrary and may be $0$ . It also involves real numbers $\mu, L, M$ and a point $x^\star\in\mathbb{R}^n$ . It uses two iteration schemes, $\mathrm{hessIter}$ and $\mathrm{dampedHessIter}$ , taken from the imported module Definitions.Def_FatkhullinPolyak_HessStep_hessianStepMethod. That module's code is not shown here, so this read-back cannot say what they compute. All it can say is how they are used:

$\mathrm{hessIter}(f, x_0, j)$ is a point of $\mathbb{R}^n$ , determined by $f$ , a starting point $x_0$ and an index $j\in\mathbb{N}$ . Below it is written $x_j$ .
$\mathrm{dampedHessIter}(f, \sigma, x_0, j)$ is a point of $\mathbb{R}^n$ , determined by $f$ , a real parameter $\sigma$ , $x_0$ and $j$ . Below it is written $y_j$ .

Nothing in the statement says whether $x_j$ or $y_j$ equals $x_0$ at $j=0$ . Nothing says how either one behaves when some quantity it uses is undefined, for example a non-invertible matrix or a division by zero.

Hypotheses (all assumed together):

$f$ is differentiable everywhere on $\mathbb{R}^n$ .
The map $x\mapsto Df(x)$ , which sends a point to the Fréchet derivative of $f$ there (a linear functional), is itself differentiable everywhere. So $f$ is twice differentiable with second derivative $D^2 f(x)$ .
$\mu>0$ .
$f$ is $\mu$ -strongly convex on all of $\mathbb{R}^n$ , in this sense: for all $x,y$ and all $a,b\ge 0$ with $a+b=1$ ,

f(ax+by)\le a f(x)+b f(y)-ab\,\tfrac{\mu}{2}\|x-y\|^2.

The gradient is $L$ -Lipschitz: for all $x,y$ ,

\|\nabla f(x)-\nabla f(y)\|\le L\,\|x-y\|.

$L$ is not separately assumed to be positive. 6. The second derivative is $M$ -Lipschitz in operator norm: for all $x,y$ ,

\|D^2 f(x)-D^2 f(y)\|\le M\,\|x-y\|.

$M$ is not separately assumed to be nonnegative. 7. $x^\star$ is a global minimizer: $f(x^\star)\le f(y)$ for every $y\in\mathbb{R}^n$ .

Write $f^\star = f(x^\star)$ .

Conclusion. The theorem asserts that both of the following hold.

(A) Undamped scheme. Take any real $\delta>0$ and any starting point $x_0$ satisfying

M\sqrt{2L\,(f(x_0)-f^\star)}\;\le\;3\mu^2(1-\delta).

Then for every $j\in\mathbb{N}$ :

f(x_j)-f^\star\;\le\;(f(x_0)-f^\star)\Bigl(1-\frac{\mu\delta}{L}\Bigr)^{j}.

Here $\sqrt{\cdot}$ is the real square root, which by convention returns $0$ for a negative argument. $\delta$ has no upper bound in the statement.

(B) Damped scheme. Take any real $\sigma$ with

0<\sigma\le \frac{\mu}{L}.

Then for every starting point $x_0$ (with no condition on $x_0$ ) and every $j\in\mathbb{N}$ :

f(y_j)-f^\star\;\le\;(f(x_0)-f^\star)\Bigl(1-\frac{\mu\sigma}{L}\Bigr)^{j}.

Degenerate cases:

The case $n=0$ . $\mathbb{R}^0$ has exactly one point. Then $f$ is constant and every point, including $x^\star$ , $x_0$ , $x_j$ and $y_j$ , is that one point. Hypotheses 5 and 6 hold for every real $L$ and $M$ , including negative ones. Both conclusions reduce to $0\le 0$ and hold trivially.
Division by $L=0$ . Lean returns $0$ for division by zero, so $\mu\delta/L$ and $\mu/L$ are both $0$ . The factor in (A) is then $1$ , and (B) is vacuous because no $\sigma$ satisfies $0<\sigma\le 0$ . (B) is also vacuous whenever $L<0$ .
The case $n\ge 1$ . The hypotheses together imply $L\ge\mu>0$ (strong convexity bounds how fast the gradient changes from below) and $M\ge 0$ . So the square-root argument in (A) is nonnegative.
Large $\delta$ in (A). If $\delta>1$ , the right-hand side of the condition is negative, so the condition cannot hold and (A) says nothing. If $\delta=1$ , the condition requires $M=0$ or $f(x_0)=f^\star$ .
The case $j=0$ . Both bounds read $f(\text{iterate}_0)-f^\star\le f(x_0)-f^\star$ , since $r^0=1$ for every real $r$ , including $0^0=1$ . Whether this is trivially true depends on the unseen definitions of the two schemes.
Starting at the minimum. If $f(x_0)=f^\star$ , both conclusions claim $f(\text{iterate}_j)\le f^\star$ for every $j$ . Together with hypothesis 7, this means every iterate attains the minimum value.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph