\subsection{Fej\'er monotonicity, regularity and metastability}\label{subsec:fejer}

Most convergence proofs in convex optimization have the same skeleton: the iterates are Fej\'er monotone with
respect to the solution set, some residual tends to zero, and a compactness or regularity argument finishes the
proof. Proof mining has analysed this skeleton once and for all. Kohlenbach, Leu\c{s}tean and Nicolae extracted
uniform rates of metastability for (generalized) Fej\'er monotone sequences whenever the convergence proof uses
compactness, covering the proximal point algorithm and iterations of firmly nonexpansive, asymptotically
nonexpansive and strictly pseudo-contractive maps in $W$-hyperbolic spaces \cite{KohlenbachLeusteanNicolae2018}.
Kohlenbach, L\'opez-Acedo and Nicolae showed that a modulus of regularity turns the same skeleton into a rate of
convergence, and conversely that a uniform rate of convergence yields a modulus of regularity
\cite{KohlenbachLopezAcedoNicolae2019}; Pischke extended this to a general notion of Fej\'er monotonicity
\cite{Pischke2025Optim}, and Kohlenbach and Pinto revisited it recently \cite{KohlenbachPinto2026JCA}. In this
light, \cref{thm:B} is the specialization to gradient descent of a general theorem, and \cref{thm:E}
is a case where the specific geometry of an algorithm beats the general bound in its dependence on $D/\eps$: for
gradient descent in $\R^d$ the number of fluctuations is linear in $D/\eps$, whereas the general compactness-based
bound is of order $(8\sqrt d\,D/\eps)^d$.

Proof mining has also produced explicit rates for many specific methods: Halpern-type proximal point algorithms
\cite{Kohlenbach2020JNCA,LeusteanPinto2021COAP,Kohlenbach2022OptimLett}, the proximal point algorithm in uniformly
convex spaces \cite{Kohlenbach2021JCA}, abstract proximal point algorithms \cite{LeusteanNicolaeSipos2018JOGO},
multi-parameter and viscosity schemes \cite{DinisPinto2021JCA,KohlenbachPinto2022JMAA}, inconsistent feasibility
problems \cite{Sipos2022OptimLett}, subgradient methods for equilibrium problems \cite{PischkeKohlenbach2022NumAlg},
set-valued monotone and accretive operators, for which new logical metatheorems were needed
\cite{Pischke2024JML,KohlenbachPischke2023PTRSA}, and continuous-time quasi-Fej\'er monotone dynamical systems such
as gradient flows \cite{FreundPischke2026QuasiFejerDynamical}.

\subsection{Stochastic optimization}\label{subsec:stochastic}

Stochastic approximation is the newest frontier. Its convergence theorems rest on the Robbins--Siegmund theorem for
almost-supermartingales, which implies Doob's convergence theorem and therefore admits no computable rates in
general. Neri and Powell gave a quantitative Robbins--Siegmund theorem with explicit, learnable rates of uniform
(metastable) convergence \cite{NeriPowell2026AAP}, building on their analysis of crossings and fluctuations of
stochastic processes \cite{NeriPowell2025TAMSB}. Neri, Pischke and Powell turned this into an abstract effective
convergence theorem for stochastic approximation, covering Dvoretzky's theorem and stochastic quasi-Fej\'er monotone
sequences \cite{NeriPischkePowell2025abstract}, and into generalized fluctuation bounds under compactness
\cite{NeriPischkePowell2026fluct}. Pischke and Powell obtained linear rates of asymptotic regularity for stochastic
Halpern and Krasnosel'ski\u{\i}--Mann schemes and translated them into oracle complexity bounds
\cite{PischkePowell2026JOTA}; see \cite{NeriPischke2025FMS} for an overview of proof mining in probability theory. The
logical classification of the underlying almost-sure convergence theorems is still open (\cref{prob:stochastic}).