Effective metastability of Halpern iterates in CAT(0) spaces

TL;DR

This paper derives an explicit rate of metastability for Halpern iterations of nonexpansive mappings in CAT(0) spaces, using proof mining techniques to extract computational content from an otherwise non-constructive proof.

Contribution

It introduces the first application of proof mining to a convergence proof involving Banach limits and the axiom of choice, providing effective bounds in this context.

Findings

Established a uniform rate of metastability for Halpern iterations in CAT(0) spaces

Demonstrated the use of proof mining to extract explicit bounds from non-constructive proofs

Extended the methodology to proofs involving Banach limits and the axiom of choice

Abstract

This paper provides an effective uniform rate of metastability (in the sense of Tao) on the strong convergence of Halpern iterations of nonexpansive mappings in CAT(0) spaces. The extraction of this rate from an ineffective proof due to Saejung is an instance of the general proof mining program which uses tools from mathematical logic to uncover hidden computational content from proofs. This methodology is applied here for the first time to a proof that uses Banach limits and hence makes a substantial reference to the axiom of choice.