(D.2) — one damped Hessian step decreases f by (σγ/2)‖∇f‖²

Proved

FatkhullinPolyak.HessStep.damped_step_descent

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

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

Let $f:\mathbb{R}^n\to\mathbb{R}$ be twice differentiable and $\mu$ -strongly convex with $\mu>0$ , with $L$ -Lipschitz gradient, and let the damping factor satisfy $0<\sigma\le\mu/L$ . For a point $x$ let $\gamma=\|\nabla f(x)\|^2/\langle\nabla^2 f(x)\nabla f(x),\nabla f(x)\rangle$ be the step size of (6.1), and let $x^+=x-\sigma\gamma\nabla f(x)$ be one step of the damped method. Then

f(x^+)\le f(x)-\frac{\sigma\gamma}{2}\,\|\nabla f(x)\|^2.

This is the conclusion of the chain (D.2), with $x=x_j$ and $x^+=x_{j+1}$ . Combined with $\gamma\ge 1/L$ and strong convexity it gives the global linear rate (6.4) of the damped method.

Formalization Note The positivity $\sigma>0$ is not written on the page; it is implicit in calling $\sigma\gamma_j$ a damped step, and is added as a hypothesis. At a stationary point $\gamma=0$ (Lean's $0/0=0$ ) and both sides equal $f(x)$ . Conventions for strong convexity, smoothness and the Hessian form are those of (D.1).

Preamble

import Mathlib
import Definitions.Def_FatkhullinPolyak_HessStep_hessianStepMethod

Formal statement

namespace FatkhullinPolyak.HessStep

theorem damped_step_descent {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (μ L σ : ℝ)
    (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‖)
    (hσ : 0 < σ) (hσL : σ ≤ μ / L)
    (x : EuclideanSpace ℝ (Fin n)) :
    f (x - (σ * hessStep f x) • gradient f x) ≤
      f x - σ * hessStep f x / 2 * ‖gradient f x‖ ^ 2 := by sorry

end FatkhullinPolyak.HessStep

Source

Fatkhullin, Polyak, Optimizing Static Linear Feedback: Gradient Method, arXiv:2004.09875v2, p. 19, Appendix D.4, Eq. (D.2) (final inequality)

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, L, \sigma$ be real numbers.

The step size is

\gamma(x)=\frac{\|\nabla f(x)\|^2}{D^2f(x)[\nabla f(x),\nabla f(x)]},

where $D^2 f(x)$ is the second Fréchet derivative of $f$ at $x$ (as a bilinear form), and division by $0$ gives $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\ge0$ with $a+b=1$ ,

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

The gradient is $L$ -Lipschitz: $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$ .
$0<\sigma$ and $\sigma\le \mu/L$ , where $\mu/L$ is taken to be $0$ when $L=0$ .

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

f\big(x-\sigma\gamma(x)\,\nabla f(x)\big)\;\le\; f(x) - \frac{\sigma\,\gamma(x)}{2}\,\|\nabla f(x)\|^2.

Degenerate cases.

If $L=0$ , then $\mu/L=0$ by the division convention, so hypothesis 5 would require $0<\sigma\le 0$ and cannot be satisfied.
If $L<0$ , then $\mu/L<0$ , and hypothesis 5 is again unsatisfiable.
In both of those cases the statement is vacuous.
If $\nabla f(x)=0$ , then $\gamma(x)=0$ and the claim is $f(x)\le f(x)$ .
If $n=0$ , the space is the single point $0$ , hypothesis 4 holds for any $L$ , and the conclusion is $f(0)\le f(0)$ .

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