A computational study of a class of recursive inequalities

TL;DR

This paper investigates the convergence behavior of sequences satisfying certain recursive inequalities, providing conditions for computable convergence rates and applying these findings to nonlinear analysis proofs, including subgradient algorithms.

Contribution

It introduces new conditions for convergence rates of recursive inequalities and demonstrates their application in extracting computational content from nonlinear analysis proofs.

Findings

Established conditions for computable convergence rates.

Provided examples of recursive inequalities in nonlinear analysis.

Applied results to subgradient algorithms.

Abstract

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.