{"id":"palomar/PALOMAR-2026-10-12-000006","url":"https://github.com/JD-Jones-ASES/thg-gradient-curve/tree/134788107eb28be0459555383a482a350bc953a4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-12-000006-v1.json","repo":"https://github.com/JD-Jones-ASES/thg-gradient-curve","tags":["math.OC","msc:90C25","msc:90C30","msc:49M37","convex-optimization","gradient-descent","lean-formalization"],"score":0,"title":"Sharp last-iterate bounds and extremal trajectories for constant-step gradient descent","trust":"high","domain":"math.OC","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.OC","summary":"Exact final-gradient bounds for convex functions with Lipschitz gradient on real Hilbert spaces, under an initial-distance bound, for every horizon and nonnegative constant step. The factor is the maximum of reciprocal linear progress and the quadratic oscillation power, with genuine smooth convex attaining examples. The formalization includes the joint progress potential, complete sampled equality trajectories in both strict branches and at balance, and a direct transfer from actual constrained proximal minimizers to sharp residual and terminal objective-residual bounds. All ten principal…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-12","reactions":{},"formalized":true,"formalizes":[{"title":"Last-Iterate Performance of Gradient Descent and Relaxed Proximal Point via s-Composability","identifier":"","relationship":"adapts"},{"title":"Smooth Strongly Convex Interpolation and Exact Worst-case Performance of First-order Methods","identifier":"","relationship":"formalizes"}]}