Proof mining with the bounded functional interpretation

In this doctoral thesis, we will see how the bounded functional interpretation of Ferreira and Oliva [13] can be used and contribute to the Proof Mining program, a program which aims to extract computational information from mathematical theorems using proof-theoretic techniques. We present a method for the elimination of sequential weak compactness arguments from the quantitative analysis of certain mathematical results. This method works as a “macro” and allowed us to obtain quantitative versions of important results of F. E. Browder [6], R. Wittmann [51] and H. H. Bauschke [2] in fixed point theory in Hilbert spaces. Although Browder’s and Wittmann’s theorems were previously analyzed by Kohlenbach using the monotone functional interpretation, it was not clear why such analyses did not require the use of functionals defined by bar recursion. This phenomenon is now fully understood, by a theoretical justification for the elimination of sequential weak compactness in the context of the bounded functional interpretation. Bauschke’s theorem is an important generalization of Wittmann’s theorem and its original proof is also analyzed here. The analyses of these results also required a quantitative version of a projection argument which turned out to be simpler when guided by the bounded functional interpretation than when using the monotone functional interpretation. In the context of the theory of monotone operators, results due to Boikanyo/Moro¸sanu [5] and Xu [52] for the strong convergence of variants of the proximal point algorithm were analyzed and bounds on the metastablility property of these iterations obtained. These results are the first applications of the bounded functional interpretation to the proof mining of concrete mathematical results