% =====================================================================
\section{Proof mining: uniformity as complexity}\label{sec:proofmining}
% =====================================================================

Reverse mathematics tells us which convergence statements \emph{cannot} come with computable rates.
Proof mining tells us what \emph{can} be extracted anyway, and how. This section is a guide to the parts of
Kohlenbach's program that concern optimization; for full accounts see
\cite{Kohlenbach2008APT,Kohlenbach2019ICM,Kohlenbach2023Kreisel}.

\subsection{The logical form of a complexity bound}\label{subsec:logical-form}

A typical worst-case bound of first-order convex optimization reads: for every Hilbert space $\Hil$, every convex
$L$-smooth $f$ on $\Hil$, every $x_0$ and every minimizer $x^\ast$ with $\norm{x_0-x^\ast}\le D$, and every
$\eps>0$, there is $k$ with $f(x_k)-f(x^\ast)<\eps$; moreover $k\le N(L,D,\eps)$. The first half is a
$\forall\exists$ statement over an abstract Hilbert space. The general logical metatheorems of Kohlenbach and
Gerhardy--Kohlenbach \cite{Kohlenbach2005TAMS,GerhardyKohlenbach2008TAMS} say that whenever such a statement
is proved in a suitable formal system (roughly: classical analysis in all finite types with an abstract Hilbert
space added as a base type, plus dependent choice, but without axioms that make the space compact or separable),
the second half follows automatically, with a bound $N$ that depends only on majorants of the data: here $L$,
$D$ and $\eps$. Three features of optimization practice, long known from the theory of oracle complexity, are thus
\emph{explained} by logic.
\begin{enumerate}[nosep,label=(\roman*)]
  \item \emph{Dimension-freeness.} Bounds do not depend on the dimension, because the abstract space has none.
  \item \emph{Oracle-model uniformity.} Bounds do not depend on $f$ beyond its constants, which is the
  premise of the oracle complexity theory of Nemirovski and Yudin \cite{NemirovskyYudin1983}.
  \item \emph{Independence of the solution.} Bounds depend on $x^\ast$ only through $D$.
\end{enumerate}
The metatheorems also indicate where their uniformity guarantee stops: if the proof uses compactness of the space
(the Bolzano--Weierstrass step in \cref{thm:A}), the extracted bound depends on a modulus of total boundedness, and
if the statement is $\Pi^0_3$ (convergence), the extractable content is a rate of metastability. Metatheorems give
sufficient conditions and cannot by themselves show that a better bound is impossible; \cref{thm:A,thm:E} show that,
for gradient descent, both limits are genuine.

\Cref{lem:reflection} is a complement. Performance estimation problems
\cite{DroriTeboulle2014,TaylorHendrickxGlineur2017} compute exact worst cases of $K$ steps of a first-order method
by optimizing over Gram matrices of size $K+2$; they are exact for every dimension at least $K+2$, because the
iterates of a first-order method span a small subspace. Logically, this is a \emph{finite-dimensional reflection
principle} for first-order methods: if some instance in a Hilbert space violates a property of the first $K$ steps,
then some instance in dimension $K+2$ violates it. Metatheorems explain why bounds are dimension-free; reflection
explains why the worst cases can be computed in finite dimension, and (\cref{thm:E}(c)) why infinite-dimensional
pathologies leave finite-dimensional traces.

\subsection{A case study: rates for Halpern and Krasnosel'ski\u{\i}--Mann iterations}\label{subsec:halpern}

The history of rates for the two basic fixed-point iterations shows how the two communities have interacted.

\emph{Krasnosel'ski\u{\i}--Mann.} For $x_{n+1}=(1-\lambda_n)x_n+\lambda_nTx_n$ with $T$ nonexpansive on a bounded
convex set $C$ of a normed space, Baillon and Bruck \cite{BaillonBruck1996} proved
$\norm{x_n-Tx_n}\le\diam(C)/\sqrt{\pi\lambda(1-\lambda)n}$ for constant $\lambda$, and conjectured a bound of
the form $\kappa\diam(C)/\sqrt{\sum_{i\le n}\lambda_i(1-\lambda_i)}$ for general steps.
Kohlenbach \cite{Kohlenbach2001NFAO,Kohlenbach2003JMAA} extracted from a proof of Borwein, Reich and Shafrir a
rate of asymptotic regularity for general steps that depends on $C$ only through a bound on its diameter and is
independent of $x_0$ and $T$ (exponential in $1/\eps$). For general steps in Banach spaces this was the only known
rate until Cominetti, Soto and Vaisman \cite{CominettiSotoVaisman2014} proved the Baillon--Bruck conjecture
with $\kappa=1/\sqrt\pi$, crediting the uniformity to proof mining; the constant is sharp
\cite{BravoCominetti2018}.

\emph{Halpern.} For $x_{n+1}=\beta_nu+(1-\beta_n)Tx_n$, the first rate of asymptotic regularity was obtained
by proof mining (Leu\c{s}tean \cite{Leustean2007JUCS}, exponential in $1/\eps$), improved to a quadratic rate by
Kohlenbach \cite{Kohlenbach2011AdvMath} and Kohlenbach--Leu\c{s}tean \cite{KohlenbachLeustean2012AdvMath} together with
uniform rates of metastability for the strong convergence. (In this subsection a rate is called linear or quadratic
according to the dependence of the number of iterations on $1/\eps$; a linear rate means $\norm{x_k-Tx_k}=O(1/k)$, not
geometric convergence.) A linear rate was then found by Sabach and Shtern
\cite{SabachShtern2017}, the tight bound $\norm{x_k-Tx_k}\le2\norm{x_0-x^\ast}/(k+1)$ in Hilbert space by Lieder
\cite{Lieder2021} using performance estimation, and the optimal rate over all Mann-type iterations in normed spaces
by Contreras and Cominetti \cite{ContrerasCominetti2023}. Lieder notes explicitly that the first result of this
type came from proof mining; conversely, the Sabach--Shtern lemma was imported back into proof mining to obtain
linear rates in $W$-hyperbolic spaces \cite{ChevalKohlenbachLeustean2023,ChevalLeustean2024MathComp}.

The pattern is instructive. Logical methods reliably deliver \emph{uniformity} and \emph{first} bounds, often in
generality (normed or geodesic spaces, general step sizes) that the optimization literature reaches later.
Optimization methods (potential functions, performance estimation) deliver \emph{optimal constants}. The two are
complementary, and they meet in the dimension-freeness of the bounds: the metatheorems predict it, and
performance estimation exploits it by computing worst cases in dimension $K+2$.

\input{proofmining_fejer}

\subsection{The origins: best approximation}\label{subsec:approx}

Proof mining began, in part, with optimization. Best Chebyshev approximation by polynomials of degree $\le n$
is a convex minimization problem with a unique solution, and the classical uniqueness proofs are ineffective.
Kohlenbach \cite{Kohlenbach1993Chebycheff,Kohlenbach1993NFAO} extracted from them explicit moduli of
uniqueness, which are uniform a priori estimates for the constants of strong unicity, improving the known estimates
of Bridges by a factor $n$ in the exponent; Kohlenbach and Oliva \cite{KohlenbachOliva2003APAL} carried out the
analysis for $L^1$-approximation. In both cases the extracted moduli have the optimal dependence on $\eps$
\cite{Kohlenbach2023Kreisel}. In the language of \cref{thm:B}, these are moduli of uniqueness for specific convex
programs. A modulus of uniqueness $\delta$ turns any rate for the objective values into a rate for the iterates: if
$f(x_k)-f^\ast\le r(k)$ and $r(k)<\delta(\eps)$, then $\norm{x_k-x^\ast}<\eps$; \cref{thm:B}(b) is the special
case of gradient descent.