% =====================================================================
\section{Two toolkits}\label{sec:prelim}
% =====================================================================

This section is written for two audiences. \Cref{subsec:rm,subsec:weihrauch,subsec:pm} introduce the logical
tools for readers from optimization; \cref{subsec:convex} fixes the convex-analytic facts used throughout for
readers from logic. Experts can skip either part.

\subsection{Reverse mathematics}\label{subsec:rm}

Reverse mathematics, initiated by Friedman \cite{Friedman1975} and developed by Simpson and many others
\cite{Simpson2009SOSOA,Hirschfeldt2014,DzhafarovMummert2022}, asks which set-existence axioms are needed to prove a
given theorem of ordinary mathematics. The setting is second-order arithmetic: variables range over natural
numbers and over sets of natural numbers, and every structure of interest (a real number, a continuous function,
a separable metric or Banach space, a countable graph) is coded by a set of naturals. Theorems are compared over
a weak base theory, and the remarkable empirical fact is that most theorems are either provable in the base
theory or \emph{equivalent} to one of four stronger systems. These five systems are:

\begin{description}[nosep,leftmargin=1.2em,font=\normalfont\itshape]
\item[$\RCA$] (recursive comprehension): $\Delta^0_1$ comprehension and $\Sigma^0_1$ induction. Its minimal
$\omega$-model consists of the computable sets; it formalizes computable mathematics with classical logic.
\item[$\WKL$] $\RCA$ plus weak K\H{o}nig's lemma: every infinite binary tree has an infinite path. This is the
compactness of Cantor space and of $[0,1]$.
\item[$\ACA$] arithmetical comprehension. Over $\RCA$ it is equivalent to the existence of the range of every
one-to-one function, i.e.\ to the existence of the halting set relative to any set
\cite[Lemma III.1.3]{Simpson2009SOSOA}. Its minimal $\omega$-model consists of the arithmetical sets.
\item[$\ATR$] arithmetical transfinite recursion: arithmetical comprehension iterated along any countable
well-ordering.
\item[$\PiCA$] $\Pi^1_1$ comprehension: the existence of the hyperjump.
\end{description}
Each system proves the previous one, and none proves the next. Real numbers are coded by fast Cauchy sequences
of rationals, and continuous functions between complete separable metric spaces by countable sets of
``neighbourhood conditions'' \cite[II.6]{Simpson2009SOSOA}. Statements of the form $x\le y$ or $f(x)\le c$ about
reals are $\Pi^0_1$, and strict inequalities are $\Sigma^0_1$; this simple fact controls much of what follows.

\subsection{Computable analysis and Weihrauch complexity}\label{subsec:weihrauch}

Reverse mathematics measures the axioms a theorem needs; computable analysis
\cite{Weihrauch2000,BrattkaHertlingWeihrauch2008} measures how hard its existential quantifier is to witness.
A real $x$ is \emph{computable} if a machine can output rational approximations with error $2^{-n}$ on input $n$;
\emph{left-c.e.}\ (resp.\ \emph{right-c.e.}) if it is the supremum (infimum) of a computable sequence of
rationals; \emph{d.c.e.}\ if it is a difference of two left-c.e.\ reals (these are called weakly computable in
\cite{AmbosSpiesWeihrauchZheng2000WeaklyComputable}; we avoid that name, which has other meanings in the Weihrauch
literature); and \emph{limit computable} ($\Delta^0_2$) if it is the limit of a
computable sequence of rationals. The computable reals are exactly those that are both left-c.e.\ and
right-c.e., and
$\{\text{left-c.e.}\}\cup\{\text{right-c.e.}\}\subsetneq\{\text{d.c.e.}\}\subsetneq
\{\text{limit computable}\}$ \cite{AmbosSpiesWeihrauchZheng2000WeaklyComputable}.
A closed set $A\subseteq[0,1]^n$ is \emph{co-c.e.}\ if its complement is the union of a computable sequence of
rational open boxes; this is the information about $A$ that is available when $A$ is the solution set of a
computable optimization problem.

Weihrauch reducibility \cite{BrattkaGherardiPauly2021} compares computational problems, viewed as multivalued
maps from instances to solutions. A problem $P$ is \emph{Weihrauch reducible} to $Q$, written $P\lev Q$, if
there are computable maps $\Phi,\Psi$ such that for every instance $p$ of $P$, $\Phi(p)$ is an instance of $Q$
and $\Psi(p,q)$ is a solution of $p$ whenever $q$ is a solution of $\Phi(p)$; for \emph{strong} reducibility
$\slev$, $\Psi$ has no access to $p$. The problems used in this paper are the following.
\begin{itemize}[nosep]
  \item $\lm$: given a convergent sequence in Baire space (or in $\R$), output its limit. It is the
  Weihrauch counterpart of $\ACA$ (more precisely, of a single Turing jump).
  \item $\MCT$: given a nondecreasing sequence in $[0,1]$, output its supremum. $\MCT\seqv\lm$
  \cite[Fact 11.26]{BrattkaGherardiMarcone2012}.
  \item $\Cch_X$ (closed choice): given a nonempty co-c.e.\ closed $A\subseteq X$, output a point of $A$.
  $\Cch_{[0,1]}\seqv\WKLp$, and finding a maximizer of a continuous function on $[0,1]$ is strongly equivalent
  to it \cite[Theorems 7.23 and 8.3]{BrattkaGherardiPauly2021}, \cite{Brattka2016Historical}.
  \item $\CC_X$ (connected choice) and $\XC_n$ (convex choice): $\Cch_X$ restricted to connected sets, resp.\ to
  convex subsets of $[0,1]^n$. Since the closed connected and the closed convex subsets of $[0,1]$ are the closed
  intervals, $\XC_1=\CC_{[0,1]}\seqv\IVT$ \cite[Theorem 6.2]{BrattkaGherardi2011BSL},
  \cite[Theorem 7.34]{BrattkaGherardiPauly2021}. The hierarchy $\XC_n$ was studied by Le Roux and Pauly
  \cite{LeRouxPauly2015LMCS} and Kihara and Pauly \cite{KiharaPauly2019TAMC}.
\end{itemize}
A problem is \emph{non-uniformly computable} if every computable instance has a computable solution. $\IVT$ and
all $\XC_n$ have this property; $\WKLp$ and $\lm$ do not.

\subsection{Proof mining}\label{subsec:pm}

Proof mining, in Kohlenbach's formulation \cite{Kohlenbach2008APT,Kohlenbach2019ICM}, extracts explicit
quantitative information from proofs that do not visibly contain it. Its tools are proof interpretations
(G\"odel's functional interpretation, Kreisel's no-counterexample interpretation, and their monotone variants),
and its guarantees are \emph{logical metatheorems} \cite{Kohlenbach2005TAMS,GerhardyKohlenbach2008TAMS}: if
a statement of the form $\forall x\,\exists n\,A(x,n)$, with $A$ suitably restricted and $x$ ranging over a
(possibly abstract) metric, normed or Hilbert space, is provable in a suitable formal system, then there is a
computable bound on $n$ that depends only on \emph{majorants} of the data (norm bounds, Lipschitz constants,
moduli), not on the data themselves, and not on the space.

Convergence is not of this form. ``$(x_k)$ is Cauchy'' reads
$\forall\eps\,\exists n\,\forall i,j\ge n\;\norm{x_i-x_j}\le\eps$, a $\Pi^0_3$ statement (the matrix
$\norm{x_i-x_j}\le\eps$ is $\Pi^0_1$), and a rate of
convergence (a bound on $n$) is in general not computable. Its no-counterexample interpretation is
\emph{metastability}, popularized by Tao \cite{Tao2008ETDS}: for every $\eps>0$ and $F\colon\N\to\N$ there is $n$
with $\norm{x_i-x_j}<\eps$ for $i,j\in[n,n+F(n)]$. This is $\forall\exists$ in form, and metatheorems produce
rates of metastability $\Phi(\eps,F)$ that are uniform in the above sense. Between rates and metastability lie
bounds on \emph{fluctuations} (see \cref{subsec:fluct}) and \emph{learnability with bounded mind changes}
\cite{AvigadRute2015,KohlenbachSafarik2014}. Two further notions recur:
a \emph{modulus of uniqueness} for $F$ with unique zero $x^\ast$ is a $\delta$ with
$\abs{F(x)}<\delta(\eps)\Rightarrow\norm{x-x^\ast}<\eps$ \cite{Kohlenbach1993Chebycheff};
a \emph{modulus of regularity} is a $\rho$ with $\abs{F(x)}<\rho(\eps)\Rightarrow\dist(x,F^{-1}(0))<\eps$
\cite{KohlenbachLopezAcedoNicolae2019}.

\subsection{Convex toolkit}\label{subsec:convex}

\begin{definition}\label{def:pair}
Let $\Hil$ be $\R^d$ or a separable Hilbert space and $L>0$. A \emph{convex $L$-smooth pair} is a pair of
continuous maps $f\colon\Hil\to\R$, $g\colon\Hil\to\Hil$ such that for all $x,y\in\Hil$
\begin{equation}\label{eq:pair}
  f(x)+\ip{g(x)}{y-x}\;\le\; f(y)\;\le\; f(x)+\ip{g(x)}{y-x}+\tfrac L2\norm{y-x}^2 .
\end{equation}
\end{definition}

Classically, \eqref{eq:pair} holds if and only if $f$ is convex and differentiable with $\nabla f=g$ and $g$ is
$L$-Lipschitz \cite[Theorem 2.1.5]{Nesterov2004}. In second-order arithmetic, \eqref{eq:pair} quantifies over reals,
but by continuity it is equivalent, provably in $\RCA$, to the same inequalities for all rational points, a
$\Pi^0_1$ condition on the codes; no theory of derivatives is needed. We write $S=\argmin f$ and $f^\ast=\inf f$, and
study \emph{gradient descent with step $1/L$}:
\begin{equation}\label{eq:gd}
  x_{k+1} = x_k - \tfrac1L\, g(x_k).
\end{equation}
When $S\neq\emptyset$ we write $D=\dist(x_0,S)$; in statements meant for $\RCA$, where this distance need not exist
as a real, we use $\norm{x_0-z}$ for some $z\in S$ instead.

\begin{lemma}\label{lem:basic}
Let $(f,g)$ be a convex $L$-smooth pair and let $(x_k)$ follow \eqref{eq:gd}. Then:
\begin{enumerate}[nosep,label=\textup{(\alph*)}]
  \item $f(x_{k+1})\le f(x_k)-\frac1{2L}\norm{g(x_k)}^2$;
  \item for every $z$: $\norm{x_{k+1}-z}^2\le\norm{x_k-z}^2+\frac2L\big(f(z)-f(x_{k+1})\big)$;
  \item if $z\in S$, then $\sum_{j=1}^k(f(x_j)-f^\ast)\le\frac L2\norm{x_0-z}^2$ and
  $f(x_k)-f^\ast\le L\norm{x_0-z}^2/(2k)$;
  \item $\norm{x_{k+1}-x_k}$ is non-increasing, and $\norm{g(x_k)}\le 2L\norm{x_0-z}/(k-1)$ for $z\in S$ and
  $k\ge 2$.
\end{enumerate}
Items (a) and (b) hold, with $1/L$ replaced by $t_k$, for variable steps $t_k\in(0,1/L]$. Each item is provable in
$\RCA$.
\end{lemma}

\begin{proof}
(a) is the right inequality of \eqref{eq:pair} with $x=x_k$, $y=x_{k+1}$. For (b), expand
$\norm{x_{k+1}-z}^2=\norm{x_k-z}^2-\frac2L\ip{g(x_k)}{x_k-z}+\frac1{L^2}\norm{g(x_k)}^2$, bound the middle term
with the left inequality of \eqref{eq:pair}, $\ip{g(x_k)}{x_k-z}\ge f(x_k)-f(z)$, and the last term with (a).
For (c), take $z\in S$ in (b), sum, and use that $f(x_j)$ is non-increasing. For (d), \eqref{eq:pair} implies co-coercivity,
$\ip{g(x)-g(y)}{x-y}\ge\frac1L\norm{g(x)-g(y)}^2$ (apply the right inequality of \eqref{eq:pair} to
$y\mapsto f(y)-\ip{g(x)}{y}$ as in \cite[Theorem 2.1.5]{Nesterov2004}), so $I-g/L$ is nonexpansive and the
steps do not grow. With $m=\lceil k/2\rceil$, (a) and (c) then give
$(k-m)\norm{g(x_{k-1})}^2/(2L)\le f(x_m)-f^\ast\le L\norm{x_0-z}^2/(2m)$, and $m(k-m)\ge(k-1)^2/4$.
In $\RCA$, each item is a $\Pi^0_1$ statement about reals proved by $\Pi^0_1$ induction on $k$.
\end{proof}

Taking $z$ in $S$ in (b) shows that the iterates are \emph{Fej\'er monotone} with respect to $S$:
$\norm{x_{k+1}-z}\le\norm{x_k-z}$ for every $z\in S$. Taking $z$ to be a later iterate gives the
self-contraction property of \cref{lem:selfcontracted}.