A computational study of a class of recursive inequalities

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 survey a number of recent results which each involve an instance of our main recursive inequality. All of the relevant concepts from both proof theory and mathematical analysis are defined and motivated within the paper itself, and as such, we hope that this work also forms an accessible overview of aspects of current research in applied proof theory.