Abstract
This entry develops reusable Isabelle/HOL infrastructure for first-order methods in smooth convex optimization. The central application is projected-gradient descent, but the development is organized around general-purpose interfaces for gradients, first-order convexity certificates, smooth quadratic upper bounds, descent and telescoping arguments, projection geometry, projected-gradient mappings, residual certificates, strong convexity, and linear convergence rates. The main purpose of the entry is not only to formalize a single convergence proof, but to separate the analytic, geometric, and algorithmic components of first-order convergence arguments into reusable Isabelle/HOL layers. The resulting library can be used as a basis for future formalizations of constrained first-order optimization methods.
License
Note
Generative AI tools, including ChatGPT and Codex, were used during the development process for brainstorming, proof-engineering assistance, code-organization suggestions, documentation drafting, and final sanity checks. All definitions, theorem statements, proofs, and documentation were reviewed, edited, and mechanically checked by the author, who takes full responsibility for the content of the submission.
Topics
Related publications
- A. Beck. First-Order Methods in Optimization. SIAM, 2017.
- D. P. Bertsekas. Nonlinear Programming. Athena Scientific, 1999.
- D. Bryant. Unconstrained Optimization. Archive of Formal Proofs, 2025.
- Y. Nesterov. Introductory Lectures on Convex Optimization: A Basic Course. Kluwer Academic Publishers, 2004.
Session Projected_Gradient_Descent
- Gradient_Preliminaries
- Convex_Differentiable
- Smooth_Convex
- Abstract_Descent
- Gradient_Descent
- Gradient_Descent_Rates
- Gradient_Descent_Convergence
- Projection_Geometry
- Projection_Optimization
- Projected_Gradient_Descent_Convergence
- Projected_Gradient_Mapping
- Projected_Gradient_Mapping_Rates
- Projected_Gradient_Descent_Residual_Convergence
- Strong_Convex
- Projected_Gradient_Descent_Linear_Rate
- Lipschitz_Smoothness
- Examples_Quadratic
- Examples_Projected_Quadratic
- Main_Results
- Examples_Using_Main_Results
- Projected_Gradient_Descent