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.