  We examine the convergence properties of sequences of nonnegative real
numbers that satisfy a particular class of recursive inequalities, from the
perspective of proof theory and computability theory. We first establish a
number of results concerning rates of convergence, setting out conditions under
which computable rates are possible, and when not, providing corresponding
rates of metastability. We then demonstrate how the aforementioned quantitative
results can be applied to extract computational information from a range of
proofs in nonlinear analysis. Here we provide both a new case study on
subgradient algorithms, and give overviews of a selection of recent results
which each involve an instance of our main recursive inequality. This paper
contains the definitions of all relevant concepts from both proof theory and
mathematical analysis, and as such, we hope that it is accessible to a general
audience.
