Appendix D.4 — one-step decrease of the Hessian-step gradient method (6.1)

Proved

FatkhullinPolyak.HessStep.hessStep_one_step_bound

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

gradient-descentlipschitz-hessianp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1step-size

Let $f:\mathbb{R}^n\to\mathbb{R}$ be twice differentiable and $\mu$ -strongly convex with $\mu>0$ , and let its Hessian be Lipschitz continuous with constant $M$ in the operator norm. For a point $x$ write $g=\nabla f(x)$ and let

\gamma=\frac{\|g\|^2}{\langle\nabla^2 f(x)g,g\rangle}

be the step size of the method (6.1). Then the next iterate $x^+=x-\gamma g$ satisfies

f(x^+)\le f(x)-\frac12\gamma\|g\|^2\Bigl(1-\frac{M\gamma^2}{3}\|g\|\Bigr).

In the notation of the paper, with $x=x_j$ , $x^+=x_{j+1}$ and $\varphi_j=f(x_j)$ , this is $\varphi_{j+1}\le\varphi_j-\frac12\gamma_j\|\nabla f(x_j)\|^2\bigl(1-\frac{M\gamma_j^2}{3}\|\nabla f(x_j)\|\bigr)$ . It shows the method decreases $f$ as long as $M\gamma_j^2\|\nabla f(x_j)\|<3$ , which is the basis of the local linear rate (6.3).

Formalization Note The page derives this display inside the proof of Theorem 6.1, whose standing hypotheses include $\mu$ -strong convexity; it is kept here because the inequality uses $\gamma\ge 0$ , which convexity guarantees. The Lipschitz constant of the gradient is not needed and is not assumed. At a stationary point $\gamma=0$ by Lean's convention $0/0=0$ , and both sides equal $f(x)$ . Strong convexity is Mathlib's StrongConvexOn Set.univ μ f, with modulus $\frac{\mu}{2}\|x-y\|^2$ .

Preamble

import Mathlib
import Definitions.Def_FatkhullinPolyak_HessStep_hessianStepMethod

Formal statement

namespace FatkhullinPolyak.HessStep

theorem hessStep_one_step_bound {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (μ M : ℝ)
    (hf : Differentiable ℝ f) (hf' : Differentiable ℝ (fderiv ℝ f))
    (hμ : 0 < μ) (hconv : StrongConvexOn Set.univ μ f)
    (hM : ∀ x y : EuclideanSpace ℝ (Fin n),
      ‖fderiv ℝ (fderiv ℝ f) x - fderiv ℝ (fderiv ℝ f) y‖ ≤ M * ‖x - y‖)
    (x : EuclideanSpace ℝ (Fin n)) :
    f (x - hessStep f x • gradient f x) ≤
      f x - (1 / 2) * hessStep f x * ‖gradient f x‖ ^ 2 *
        (1 - M * hessStep f x ^ 2 / 3 * ‖gradient f x‖) := by sorry

end FatkhullinPolyak.HessStep

Source

Fatkhullin, Polyak, Optimizing Static Linear Feedback: Gradient Method, arXiv:2004.09875v2, p. 19, Appendix D.4 (proof of Theorem 6.1), third display

Read-back

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

Let $n\in\mathbb{N}$ (possibly $0$ ), let $f:\mathbb{R}^n\to\mathbb{R}$ with the Euclidean inner product and norm, and let $\mu, M$ be real numbers.

Two quantities appear in the statement:

$Q_f(x;v) = D^2 f(x)[v,v]$ is the second Fréchet derivative of $f$ at $x$ applied to $(v,v)$ .
$\gamma(x)$ is the step size

\gamma(x) = \frac{\|\nabla f(x)\|^2}{Q_f(x;\nabla f(x))},

with division by $0$ giving $0$ .

The hypotheses are:

$f$ is differentiable everywhere, and $x\mapsto Df(x)$ is differentiable everywhere.
$\mu>0$ .
$f$ is $\mu$ -strongly convex on all of $\mathbb{R}^n$ : 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 Hessian is $M$ -Lipschitz in operator norm: for all $x,y$ , $\|D^2 f(x)-D^2 f(y)\|\le M\|x-y\|$ .

The conclusion is that for every $x\in\mathbb{R}^n$ ,

f\big(x - \gamma(x)\nabla f(x)\big) \;\le\; f(x) - \tfrac12\,\gamma(x)\,\|\nabla f(x)\|^2\left(1 - \frac{M\,\gamma(x)^2}{3}\,\|\nabla f(x)\|\right).

The parenthesized factor may be negative. In that case the right-hand side exceeds $f(x)$ , and the statement does not assert a decrease.

Degenerate cases.

If $\nabla f(x)=0$ , then $\gamma(x)=0$ by the division convention, and the claim is $f(x)\le f(x)$ .
If $n=0$ , everything is trivial: the space is the single point $0$ , and the conclusion is $f(0)\le f(0)$ .
If $n\ge1$ , hypothesis 4 forces $M\ge 0$ .
If $n = 0$ , $M$ may be any real number.

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