The exact last-gradient bound for constant-step gradient descent in the strongly convex case

Dev D. Goyal

The exact last-gradient bound for constant-step gradient descent in the strongly convex case

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Selected result in this collection

Problem and result

Problem: Taylor–Hendrickx–Glineur Conjecture 3: last-iterate gradient norm of gradient descent
Posed in: Taylor, Hendrickx and Glineur, Mathematical Programming 161 (2017), 307–345, Conjecture 3 (Section 4.1.3)
Status: Proved
Result: Gradient descent with step h/L, 0 ≤ h ≤ 2, on L-smooth μ-strongly convex f on any real Hilbert space satisfies ‖∇f(x_N)‖ ≤ L‖x₀ − x*‖ max{p_N(μ/L, h), |1 − h|^N} for every N, with equality attained in one dimension.

Abstract

The exact final-gradient guarantee holds on every real Hilbert space for L > 0, 0 ≤ μ ≤ L, normalized step 0 ≤ h ≤ 2 and every natural horizon. Actual one-dimensional Huber and quadratic functions attain its two branches.

Details

Year: 2026
Discipline: Mathematics
Area: Convex optimization
Subject: Optimization
Result type: Standalone theorem and reproducible proof package
Formal proof: Standalone Lean package
Family: strong-gradient
Keywords: gradient descent, strongly convex optimization, worst-case analysis, performance estimation, Taylor–Hendrickx–Glineur conjecture, last-iterate gradient norm

Statement and scope

Formal scope. The actual-function upper bound and normalized actual-function attainment are formalized, including every horizon and closed parameter boundary. Sharpness for arbitrary L > 0 and radius R > 0 is proved by rescaling in the manuscript, without a separate Lean wrapper.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 338 KB
PDF on GitHub: papers/mathematics/strong-gradient/manuscript.pdf
LaTeX source: papers/mathematics/strong-gradient/manuscript.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/mathematics/strong-gradient/

Lean project

papers/mathematics/strong-gradient/lean/ 21 Lean files

Lakefile

papers/mathematics/strong-gradient/lean/lakefile.lean

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

The commands below are quoted from papers/mathematics/strong-gradient/VERIFICATION.md, which gives their context and working directory.

lake update
lake exe cache get

python3 verify.py --lean "$(elan which lean)" \
  --mathlib .lake/packages/mathlib --entry THGStrong \
  --audit-theorem THGStrong.Sharpness.attain_rate \
  --timeout 300 --output ../verification-replay

README: papers/mathematics/strong-gradient/README.md
Verification record: papers/mathematics/strong-gradient/VERIFICATION.md
Proof map: papers/mathematics/strong-gradient/PROOF_MAP.md
Authorship: papers/mathematics/strong-gradient/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Source. Prior results and source-comparison limits are stated in the manuscript. Historical priority is not certified.

Questions and answers

Is the Taylor–Hendrickx–Glineur conjecture on the final gradient norm proved?

This preprint proves the conjectured bound ‖∇f(x_N)‖ ≤ L‖x₀ − x*‖ max{p_N(μ/L, h), |1 − h|^N} for every 0 ≤ μ ≤ L, normalized step 0 ≤ h ≤ 2 and horizon N on any real Hilbert space, and shows one-dimensional Huber and quadratic functions attain it. Its stated contribution is the positive strong-convexity case: the formula and sharp examples are credited to Taylor, Hendrickx and Glineur, and the complete μ = 0 curve to Jones.

Does this follow from earlier exact rates for gradient descent?

According to the manuscript, no: converting the exact initial-function-gap rates of Rotaru, Glineur and Patrinos or Kim through f(x₀) − f* ≤ LR²/2 gives a weaker progress factor. The literature review is bounded by the sources cited through 29 October 2026, and the paper is an unrefereed preprint.

Is the proof formally verified?

The actual-function upper bound and normalized attainment are checked in Lean 4.19.0, including every horizon and closed parameter boundary. Sharpness for arbitrary L > 0 and radius R > 0 follows by a rescaling written in the manuscript, not a separate Lean theorem.

Cite

Citation file papers/mathematics/strong-gradient/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026stronggradient,
  author = {Goyal, Dev D.},
  title = {The Exact Last-Gradient Bound for Constant-Step Gradient Descent in the Strongly Convex Case},
  year = {2026},
  month = oct,
  note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/strong-gradient}
}