The finitary content of sunny nonexpansive retractions

The goal of proof mining is to extract quantitative information out of proofs in mainstream mathematics which are not necessarily fully constructive. Often, such proofs make use of strong mathematical principles, but a preliminary analysis may show that they are not actually needed, so the proof may be carried out in a system of strength corresponding roughly to first-order arithmetic. Following a number of significant advances in this vein by Kohlenbach in 2011 and by Kohlenbach and Leuștean in 2012, we now tackle a long-standing open question: the quantitative analysis of the strong convergence of resolvents in classes of Banach spaces more general than Hilbert spaces.

This result was proven for the class of uniformly smooth Banach spaces by Reich in 1980. What we do is to analyze a proof given in 1990 by Morales, showing that adding the hypothesis of the space being uniformly convex, and thus still covering the case of L^p spaces, can serve to eliminate the strongest principles used in the proof by way of a modulus of convexity for the squared norm of such spaces. A further procedure of arithmetization brings the proof down to System T so the proper analysis may proceed. After obtaining a non-effective realizer of the metastability statement, this is majorized in order to obtain the desired rate. Subsequent considerations calibrate this bound to T_1. It particular, this result completes some analyses that had previously been obtained only partially, yielding rates of metastability within the above-considered class of Banach spaces for the Halpern and Bruck iterations.

These results are joint work with Ulrich Kohlenbach.

References:

[1] U. Kohlenbach, A. Sipoș, The finitary content of sunny nonexpansive retractions. arXiv:1812.04940 [math.FA], 2018. Preprint. Up-to-date version at: https://www2.mathematik.tu-darmstadt.de/~kohlenbach/resolvent-paper.pdf