Proof Mining Seminar

Ulrich Kohlenbach (Technische Universität Darmstadt)
Recent Applications of Proof Mining in Optimization and Ergodic Theory

Abstract: We will give a brief introduction to proof mining and then discuss some new devlopments both on the logical side (with N. Pischke) as well as w.r.t. recent case studies. The latter concern linear rates of convergence for Tikhonov regularization methods (with H. Cheval and L. Leustean) and rates of asymptotic regularity and metastability for nonlinear ergodic theorems in uniformly convex Banach spaces (with A. Freund).

Nicholas Pischke (Technische Universität Darmstadt)
Proof mining for maximally monotone set-valued operators

Abstract: I discuss how proofs involving set-valued operators and their resolvents can be treated in higher-type arithmetic while attaining logical bound extraction theorems. In particular, I focus on a specific class of so-called ``maximally monotone" operators which are ubiquitous in the literature. In that context, I discuss how one can circumvent the logically complicated maximality statement by utilizing Minty's theorem, a fundamental result from monotone operator theory, and still obtain mathematically strong systems which allow for the explanation of most of the previous case studies involving said operators. This leads to a surprising and robust connection between the maximality statement and formal extensionality of the operator which I discuss in conjunction with various quantitative forms of (fragments of) the extensionality (viz. maximality) statement which can still be used in the context of the previously mentioned bound extraction theorems.

Pedro Pinto (Technische Universität Darmstadt)
The alternating Halpern-Mann iteration

Abstract: The Halpern and Krasnoselskii-Mann iterations are two important methods for approximating zeros of nonexpansive maps. Several proof mining results have focused on the study on these iterative schemas and variants thereof. Recently [1], together with Bruno Dinis, the alternating Halpern-Mann iteration (HM) was introduced for approximating common fixed points of two nonexpansive maps. As the name suggests, this method alternates between the Halpern and Krasnoselskii-Mann definitions. Under some conditions, it was possible to establish asymptotic regularity and strong convergence towards a common fixed point, in the setting of CAT(0) spaces. In this talk, we will look at the motivations behind this iteration, and discuss how such a strong convergence result was made possible by techniques and ideas from the proof mining program ([2]). In recent work [3], together with Laurențiu Leuștean, it was possible to generalize the asymptotic regularity result to UCW-hyperbolic spaces. We will discuss how this suggests that HM is a proper mixing of the Halpern and Mann iterations.
References: [1] B. Dinis, and P. Pinto. Strong convergence for the alternating Halpern-Mann iteration in CAT(0) spaces. arXiv:2112.14525, Submitted, 2021.
[2] F. Ferreira, L. Leuștean, and P. Pinto. On the removal of weak compactness arguments in proof mining. Advances in Mathematics, 354:106728, 2019.
[3] L. Leuștean, and P. Pinto. Rates of asymptotic regularity for the alternating Halpern-Mann iteration. arXiv:2206.02226, Submitted, 2022.
[4] U. Kohlenbach, and L. Leuștean. Effective metastability of Halpern iterates in CAT(0) spaces. Advances in Mathematics, 231(5):2526-2556, 2012.
[5] H. Cheval, and L. Leuștean. Quadratic rates of asymptotic regularity for the Tikhonov-Mann iteration. Optimization Methods and Software, 2022.
[6] H. Cheval, U. Kohlenbach, and L. Leuștean. On modified Halpern and Tikhonov-Mann iterations. arXiv:2203.11003, Submitted, 2022.

Paulo Oliva (Queen Mary University of London)
On the Borel-Cantelli Lemmas, the Erdős–Rényi Theorem, and the Kochen-Stone Theorem

Abstract: In this talk we present a quantitative analysis of the first and second Borel-Cantelli Lemmas and of two of their generalizations: the Erdős–Rényi Theorem, and the Kochen-Stone Theorem. We will see that the first three results have direct quantitative formulations, giving an explicit relationship between quantitative formulations of the assumptions and the conclusion. For the Kochen-Stone theorem, however, we can show that the numerical bounds of a direct quantitative formulation are not computable in general. Nonetheless, we obtain a quantitative formulation of the Kochen-Stone Theorem using Tao's notion of metastability.