LisMath Seminar 

26/06/2018, 14:40 — 15:10 — Room 6.2.33, Faculty of Sciences of the Universidade de Lisboa
Pedro Pinto, LisMath, Faculdade de Ciências, Universidade de Lisboa

The Bounded Functional Interpretation and Proof Mining

Proof mining is the research program that aims to analyse proofs of mathematical theorems in order to extract hidden quantitative information — such as rates of convergence, rates of metastability and rates of asymptotic regularity. Proof theoretical tools like Kohlenbach's monotone functional interpretation ([1]), a variant of Gödel’s Dialectica, are of standard use. A newer functional interpretation was introduced by Ferreira and Oliva in 2005 ([2]), dubbed the bounded functional interpretation (BFI). The focus of my research was the better understanding of the BFI in the context of proof mining.

I will show a general technique that allows the elimination of weak sequential compactness arguments in the analysis of certain types of proofs. It also gives a better understanding of previous quantitative results done Kohlenbach ([3]) where this argument was already eliminated. This technique was also employed to produce a first quantitative version of Bauschke's theorem ([4]).

Other results, in the context of the proximal point algorithm ([5], [6]), were also analysed with the BFI and their first quantitative versions were obtained.

These results are new and the first practical application of the BFI in the proof mining program.

Bibliography:

[1] Kohlenbach, Ulrich. Applied proof theory: proof interpretations and their use in mathematics. Springer Science & Business Media, 2008.

[2] Ferreira, Fernando, and Paulo Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic 135.1-3 (2005): 73-112.

[3] Kohlenbach, Ulrich. On quantitative versions of theorems due to FE Browder and R. Wittmann. Advances in Mathematics 226.3 (2011): 2764-2795.

[4] Bauschke, Heinz H. The approximation of fixed points of compositions of nonexpansive mappings in Hilbert space. Journal of Mathematical Analysis and Applications 202.1 (1996): 150-159.

[5] H. K. Xu, Iterative algorithms for nonlinear operators. J. Lond. Math. Soc. 66(1) (2002): 240-256.

[6] Boikanyo, Oganeditse A., and G. Morosanu. Inexact Halpern-type proximal point algorithm. Journal of Global Optimization 51.1 (2011): 11-26.