Documentation

LeanPool.PLAcceleratedNesterovLean

Accelerated Nesterov convergence under local Polyak-Lojasiewicz conditions #

Source: arxiv:2603.21516 Authors: Max Obreiter, Tobias Steinbrecher, Robert Foerster Status: verified Main declarations: PLAcceleratedNesterovLean.nesterov_pl_accelerated_rate Tags: optimization, numerical-analysis, gradient-methods, polyak-lojasiewicz, differential-geometry MSC: 49M37, 65K05, 58C15

This project formalizes accelerated Nesterov convergence under a local Polyak-Lojasiewicz condition near a smooth minimizer manifold, including public embedded-manifold and C3 theorem statements with an explicit exponential rate.