## Abstract

This paper addresses new developments in the ongoing proof mining programme, i.e. the use of tools from proof theory to extract effective quantitative information from prima facie ineffective proofs in analysis. Very recently, the current authors developed a method of extracting rates of metastability (as defined by Tao) from convergence proofs in nonlinear analysis that are based on Banach limits and so (for all that is known) rely on the axiom of choice. In this paper, we apply this method to a proof due to Shioji and Takahashi on the convergence of Halpern iterations in spaces *X* with a uniformly Gâteaux differentiable norm. We design a logical metatheorem guaranteeing the extractability of highly uniform rates of metastability under the stronger condition of the uniform smoothness of *X*. Combined with our method of eliminating Banach limits, this yields a full quantitative analysis of the proof by Shioji and Takahashi. We also give a sufficient condition for the computability of the rate of convergence of Halpern iterations.

## 1. Introduction

The topic of computable analysis started with Alan Turing's seminal paper [1] in which he defined the notion of a computable real number as one which has a computable binary (or decimal) expansion. While being the right notion for single real numbers, it does not lead to the proper notion of computable functions on reals as even the function *x*,*y*↦*x*+*y* would not be computable. This was corrected by Turing [2] by giving up the uniqueness of the representation allowing (following Brouwer) overlapping intervals, which is equivalent to the currently used definition in terms of computable Cauchy sequences of rational numbers with computable Cauchy rate (see [3], for much more detailed information). As this definition has already highlighted, the issue of effective rates of convergence and other effective bounds plays an important role in computable analysis. Often, however, the use of ineffective reasoning in analysis (both via the use of classical logic as well as by introducing non-computable objects) provides an obstacle for obtaining effective information. This is particularly ubiquitous in the area of abstract nonlinear analysis.

Starting in Kohlenbach [4] and continued in Gerhardy & Kohlenbach [5], Leuştean [6] and Kohlenbach [7], general logical metatheorems have been developed that guarantee the extractability of highly uniform effective (and actually subrecursive) bounds (whose complexity reflects that of the proof principles used) from large classes of (prima facie highly ineffective proofs) nonlinear functional analysis (‘proof mining’). Here by ‘uniform’ we refer to the fact that the bounds are independent from metrically majorizable input data (without any compactness condition). For this to hold, it is crucial that no separability conditions on the underlying structures must be imposed as the uniform version of separability is total boundedness and so (modulo completeness) compactness. Because structures such as complete metric or Banach spaces usually are represented (in proof theory as well as in reverse mathematics and computable analysis) as completions of countable dense substructures, this requires a novel treatment of these structures. The approach is to ‘hardwire’ such an abstract space *X* as a kind of atom to the formal system (a suitable system of arithmetic or analysis formulated in the language of functionals of all finite types over ) by adding a new base type *X* and all finite types over the two base types (of course, also several spaces *X*_{1},…,*X*_{n} can be treated simultaneously; see [7]). Then appropriate constants and axioms for the respective structure treated have to be added. The crucial conditions are:

— that the constants added can be majorized by functionals already definable in or that they have a type , in which case they can be essentially majorized by themselves; and

— that the new axioms have a monotone functional interpretation [7] (in the set-theoretic model or—if bar recursion is needed, which is not the case here though—in the model of majorizable functionals) by the same functionals that suffice for the interpretation of and the majorization of the new constants.

The second point is automatically satisfied if the additional axioms are all purely universal (and the quantified variables have sufficiently low types), which will be the case in this paper.

Structures treated so far are:

— bounded metric, hyperbolic and CAT(0)-spaces, (real) normed, uniformly convex and inner product spaces also with abstract bounded convex subsets

*C*⊆*X*in the normed case [4];— unbounded metric, hyperbolic and CAT(0)-spaces and (real) normed spaces also with unbounded convex subsets [5];

— Gromov

*δ*-hyperbolic spaces, -trees and uniformly convex hyperbolic spaces [6]; and— complete metric and normed spaces [7].

Some obvious classes of spaces are missing in this list as they do not have the right uniformity built in to have a monotone functional interpretation. As mentioned already, this is the case for separable spaces as the monotone functional interpretation of separability upgrades the latter to the total boundedness of metrically bounded subsets and hence (in the presence of completeness and closedness) to compactness. Compact metric spaces, however, are much easier to treat via their representation as a continuous image of the Cantor space (which is explicitly given in our formal framework). Another badly behaved class are the strictly convex Banach spaces that (under monotone functional interpretation) get upgraded to uniformly convex Banach spaces.

Because our systems are based on full classical logic, the theorems to be proved essentially have to be of the form of ∀∃-sentences in order to allow for the existence of effective bounds.

Many theorems in nonlinear analysis are of the form that certain iterations (*x*_{n}) built up using some operator *T*:*X*→*X* and a starting point *x*∈*X* (perhaps further involving some sequence of scalars (*λ*_{n}) typically in [0,1]) are strongly convergent. Because the Cauchy property is ∀∃∀ rather than ∀∃, one has to express this in the (ineffectively equivalent) Herbrand normal form from logic
which—in the context of Cauchy statements—has been called metastability by Tao [8,9].^{1} The aforementioned metatheorems now guarantee the extractability of effective bounds *Φ*(*k*,*g*) on ‘∃*n*’ (in logic referred to as the Kreisel ‘no-counterexample interpretation’; see [12,13]), which are highly uniform in the sense that they—in addition to *k*,*g*—depend only on norm bounds for *x* and majorants for *T*
as well as certain moduli that make some assumptions on (*λ*_{n}) explicit. For large classes of maps *T* (e.g. for non-expansive ones, which are the only ones needed in this paper), the computation of *T** is trivial. This is also the case when *T*:*C*→*C*, where *C* is a bounded (convex) subset (as will be the case throughout this paper). Thus the bound is (essentially) independent from *x* and *T* as well as the underlying space *X* (except for data such as a modulus of uniform convexity, etc.).

Kohlenbach [14] extracted such a ‘rate of metastability’ *Φ*(*k*,*g*) for Halpern iterations
for non-expansive self-mappings *T*:*C*→*C* of a convex subset of a Hilbert space from a proof due to Wittmann [15] of the strong convergence of (*x*_{n}) (provided that *C* is bounded or—weaker—*T* has a fixed point). Wittmann's result has received considerable attention as it is an important nonlinear generalization of the well-known von Neumann mean ergodic theorem (see [16,17] for effective metastable versions) as (*x*_{n}) coincides with the Cesàro mean for linear *T*.

Recently [18], the current authors extracted an explicit rate of metastability from a proof of a generalization of Wittmann's theorem to CAT(0)-spaces by Saejung [19]. This result constitutes a significant extension of the hitherto context of proof mining as Saejung's proof makes use of Banach limits whose existence (for all that is known) requires some substantial use of the axiom of choice. Nevertheless, we developed a method to convert such proofs into more elementary proofs that no longer rely on Banach limits and can be analysed by the existing logical machinery. Banach limits were introduced in the subject of Halpern iterations by Bruck & Reich [20] (in this connection, see also [21], §§ 12 and 14).

In this paper, we extract a rate of metastability for another generalization (owing to [22]) of Wittmann's theorem, namely to Banach spaces with a uniformly Gâteaux differentiable norm. The significance of this is twofold:

— As the proof again uses Banach limits, we further substantiate our claim that the machinery developed in Kohlenbach & Leuştean [18] to eliminate arguments based on Banach limits is indeed a general method. In fact, we can literally re-use most of the technical lemmas from Kohlenbach & Leuştean [18], showing the striking modularity of this proof-theoretic approach based on (monotone) functional interpretation.

— The proof is based on the existence of a uniformly continuous (in a suitable sense) so-called duality mapping

*J*, which also plays an important role in numerous other proofs in the nonlinear analysis. In §2, we indicate how this structure can be nicely incorporated into the framework of the logical metatheorems referred to earlier.

In our paper, all Banach spaces are real Banach spaces.

## 2. A logical metatheorem for real Banach spaces with a norm-to-norm uniformly continuous duality selection map

In this paper, we study a proof that uses a smoothness property of Banach spaces, namely that the norm is uniformly Gâteaux differentiable. It turns out that this notion is not uniform enough to have a monotone functional interpretation or rather that the latter requires that the space even has a uniformly Fréchet differentiable norm, i.e. it is uniformly smooth.

The uniform smoothness of a space *X* can be universally axiomatized, once a constant representing (a suitable notion of) a modulus of uniform smoothness is given. Then the corresponding metatheorem will guarantee the extractability of an effective uniform bound that (in addition to its usual input data) will depend only on *τ*_{X}. In the concrete application given in this paper, it indeed will be the uniform smoothness (rather than uniform Gâteaux differentiability of the norm) that we need for this. This is via the norm-to-norm uniform continuity on bounded sets of the normalized duality map *J* of *X* which holds in uniformly smooth spaces, whereas uniform Gâteaux differentiability implies only the norm-to-weak* uniform continuity of *J*.

### Definition 2.1

Let *X* be a Banach space and *X** its dual space. Then the mapping
is called the (normalized) duality mapping of *X*. Here 〈*x*,*y*〉 denotes *y*(*x*).

By the Hahn–Banach theorem, it follows that *Jx* is always non-empty. If *X* is smooth (i.e. has a Gâteaux differentiable norm), then *Jx* is always single-valued and also the converse holds (see [23], theorems 4.3.1 and 4.3.2). This single-valued mapping is norm-to-norm uniformly continuous on bounded subsets, provided that *X* is uniformly smooth and a modulus of uniform continuity can be obtained from a modulus of uniform smoothness for *X* (see proposition 2.5 below; for more general information on the duality map and its background, see [24,25]). In our application, we need only a function *J*:*X*→*X**, which selects in a uniformly continuous way a point from the duality set and will not insist on the latter being single-valued.

Let us define a *space with a uniformly continuous duality selection map* (*X*,*J*) to be a real Banach space *X* together with a mapping *J*:*X*→*X** satisfying

〈

*x*,*Jx*〉=∥*x*∥^{2}=∥*Jx*∥^{2}for all*x*∈*X*, and*J*is norm-to-norm uniformly continuous on any bounded subsets of*X*.

Obviously, it suffices to require that *J* is norm-to-norm uniformly continuous on any open ball *B*_{d}(0) (respectively, closed ball ), *d*>0. By a *modulus* for the space with a uniformly continuous duality selection map (*X*,*J*), we shall understand a mapping such that, for all *d*>0, *ω*(*d*,⋅) is a modulus of uniform continuity for the restriction of *J* to , that is, for all *ε*>0 and ,
2.1

One can easily see that the existence of a modulus *ω* satisfying (2.1) is equivalent to the existence of such that, for any and *x*,*y*∈*B*_{d}(0),
2.2

Rather than having to formalize the proof of the existence of *J* and its continuity property, we directly add constants *J*_{X},*ω*_{X} and axioms (*J*_{X}) and (*J*_{X},*ω*_{X}) to the formal framework expressing that, for *x*∈*X*, *J*_{X}*x* represents a linear operator with ∥*J*_{X}*x*∥≤∥*x*∥ and *J*_{X}*xx*=∥*x*∥^{2}, which—taken together—yields ∥*J*_{X}*x*∥=∥*x*∥, i.e. *J*_{X}*xx*=∥*x*∥^{2}=∥*J*_{X}*x*∥^{2}, and that *J*_{X} is norm-to-norm uniformly continuous on any bounded ball *B*_{d}(0) with modulus of uniform continuity *ω*_{X}(*d*,⋅). Instead of using the operator norm and stating ∥*J*_{X}*x*−*J*_{X}*y*∥≤2^{−k}, we express things equivalently in the language of *X* as ∀*z*∈*X*(|*J*_{X}*xz*−*J*_{X}*yz*|≤2^{−k}⋅∥*z*∥).

In formulating (*J*_{X}) and (*J*_{X},*ω*_{X}), we rely on the formal framework from Kohlenbach [7] and the representation of real numbers, , etc., in terms of number-theoretic functions. *J*_{X} then is an object of type *X*→*X*→1 (where 1 denotes the type that is, the type of objects used to represent real numbers) and *ω*_{X} has type ,
It is easy to see that (*J*_{X}) and (*J*_{X},*ω*_{X}) (but not (*J*_{X}) alone) imply the extensionality of *J*_{X}
so that we can safely use *J*_{X} in the usual set-theoretic way (whereas with (*J*_{X}) extensionality holds only for provably equal arguments; see [7]).

Let be, for example, the finite type system for classical analysis WE-PA^{ω}+DC^{ω}+QF-AC and let be its extension by an abstract real normed space with the constants *J*_{X},*ω*_{X}, together with their above mentioned axioms, an abstract non-empty convex subset *C*⊆*X* and a completeness axiom stating the completeness of *X*/closedness of *C* (see [7] for details). Then the logical metatheorems for Banach spaces from Kohlenbach [7] hold if the extracted bound is allowed to depend on *ω*_{X}. We formulate here only a special instance of these theorems sufficient for our main application:

### Theorem 2.2

*Let* *be a purely existential formula containing only k,g,x,T,n free. Then the following rule holds: from a proof in* *of
**one can extract a computable* *bound such that
**holds in any (real) Banach space X with a duality selection map J (used to interpret J*_{X}*) that has ω as modulus of uniform norm-to-norm continuity (used to interpret ω*_{X}*) and any closed b-bounded convex subset C⊆X. If C is not bounded, then one has to choose b such that b≥∥x∥,∥x−Tx∥.*

Note that *Φ* does not depend on *x*,*T* and depends on *X*,*C* only via *ω* resp. *b*.

### Proof.

The proofs in Kohlenbach [4], theorem 3.30 for bounded *C* and in Gerhardy & Kohlenbach [5], corollary 6.6 for unbounded *C* easily extend to our situation (see also [5], remark 4.13) as both (*J*_{X}) and (*J*_{X},*ω*_{X}) are purely universal (here we use that are purely universal while is purely existential; see [7]) with quantified variables of low types, *ω*_{X} is trivially majorized by and *J*_{X} is majorized by (see [4], definition 2.9) with the Cantor pairing function *j* and using the obvious extension of ° from Kohlenbach [4], definition 2.9 from to because , where *J*_{X} is interpreted via . The completion axiom is incorporated as in Kohlenbach [7], pp. 433–434 and the closedness of *C* can also be easily expressed in a purely universal way similar to . ■

### Remark 2.3

The extraction of the bound proceeds by monotone functional interpretation [7] from the proof and its complexity faithfully reflects the complexity of the principles used in the proof. In our case in this paper, this will yield a *Φ* of very restricted complexity.

The strong convergence result for Halpern iterations in Shioji & Takahashi [22] is proved under the *hypothesis* that the sequence (*z*_{n}) of the fixed points of the contractions *T*_{n}(*y*):=(1/(*n*+1))*x*+(1−1/(*n*+1))*Ty* strongly converges (towards a fixed point of *T*), which is known in many cases such as for Hilbert spaces [26,27], the (complex) Hilbert ball ([21], §§ 24 and 27 and [28]), general CAT(0)-spaces [29] and also uniformly smooth Banach spaces [30] for bounded, closed and convex *C* (which covers our context). Under this assumption (in fact already under the assumption of the plain Cauchy property of (*z*_{n})), the proof of the strong convergence of the Halpern iteration (*x*_{n}) that results by our elimination of the use of Banach limits from the proof of Shioji & Takahashi [22] is basically constructive. Hence metatheorems for the constructive case [31] guarantee (and our proof displays this; see theorem 3.4) a uniform effective procedure to transform a rate of convergence for (*z*_{n}) into one for (*x*_{n}). The problem, however, is that, even in very simple cases (*X* being an effective Hilbert space and *T* a computable and linear non-expansive map), there is no computable rate of the former as (see [16]) there is no computable rate for the latter. In fact, to show that there is no effective operator that would effectively in a computable sequence of operators (*T*(*l*))_{l} produce a rate of convergence for (*z*_{n}) is almost trivial and holds already for and *C*:=[0,1] (similarly to [7], theorem 18.4). Only in certain cases, e.g. when, in particular, the norm ∥*z*∥ of the limit is known, does one get computable rates of (*z*_{n}) (but not uniform ones and without any complexity information as the argument is based on unbounded search): see theorem 3.4.

What, however, *can* be obtained in many cases (not only computably but with low complexity) is a (fully uniform) *rate of metastability* for (*z*_{n}). Since the latter only ineffectively implies the convergence of (*z*_{n}), it is this feature that makes the proof of the convergence of (*x*_{n}) non-constructive and forces us to also weaken the conclusion to the metastability of (*x*_{n}) (in logical terms, this corresponds to applying a so-called negative translation prior to the actual functional interpretation).^{2} So we actually use the above-mentioned metatheorem in the form where we have as an additional input a (majorant of a) rate *K*(*ε*,*g*) of metastability for (*z*_{n}) (or—equivalently—a self-majorizing such rate) and extract a bound on the metastability of (*x*_{n}) that depends in addition to *ε*,*g*,*b*,*ω* also on *K* (in the case at hand, it turns out that *K* does not even need to be majorizable as it is applied to only a single function *f** that is defined in terms of *g* and the other input data). For the Hilbert case (as well as the CAT(0)-case; see [18]), a simple primitive recursive such *K* has been extracted in Kohlenbach [14]. For the case of uniformly smooth Banach spaces [30] (i.e. the context of the present paper), this is to be left for future research.

### (a) Some examples

Let us recall that a Banach space *X* is

*uniformly convex*if for all*ε*∈(0,2] there exists*δ*∈(0,1] such that, for all*x*,*y*∈*X*, 2.3*uniformly smooth*whenever given*ε*>0 there exists*δ*>0 such that, for all*x*,*y*∈*X*, 2.4

A mapping *η*:(0,2]→(0,1] providing a *δ*:=*η*(*ε*) satisfying (2.3) for given *ε*∈(0,2] will be called a *modulus of uniform convexity*. Similarly, a function providing such a *δ*:=*τ*(*ε*) satisfying (2.4) is said to be a *modulus of uniform smoothness*.

### Remark 2.4

The property of *X* being a uniformly smooth Banach space with a modulus (formulated with 2^{−k} instead of *ε*/*δ*) can be axiomatized by a universal axiom over our framework (so that the logical metatheorems guarantee effective bounds depending additionally only on *τ*_{X}) as follows (using again that is universal while is existential):
where . Note that for *x* with ∥*x*∥>1 one has Conversely, for *x*∈*S*_{1} and *x*′:=2⋅*x* one has ∥*x*′∥=2>1 and So in the axiom above we indeed quantify over all vectors *x*∈*S*_{1}.

### Proposition 2.5

If

*X*is uniformly smooth with modulus*τ*, then*X** is uniformly convex with modulus*η*(*ε*)=*ε*/4⋅*τ*(*ε*/2).If

*X** is uniformly convex with modulus*η*, then*X*is a space with a uniformly continuous duality selection map with modulus*ω*(*d*,*ε*)=*ε*/3⋅*η*(*ε*/*d*) for all*ε*∈(0,2] and*d*≥1. For*d*<1 one can trivially define*ω*(*d*,*ε*)=*ω*(1,*ε*) for all*ε*>0, while, for*ε*>2, one defines*ω*(*d*,*ε*)=*ω*(*d*,2) for all*d*>0.

### Proof.

(i) A classical result states that *X* is uniformly smooth iff *X** is uniformly convex and the following Lindenstrauss duality formula holds (e.g. [32], proposition 1.e.2): for all *δ*>0
2.5where
2.6is the modulus of smoothness of *X*, while
2.7is the modulus of convexity of *X**. One can see easily that *ρ*_{X}(*δ*)≤*δε*/4≤*ε*/4⋅*τ*(*ε*/2) for all *δ*≤*τ*(*ε*/2). Apply now (2.5) with *δ*:=*τ*(*ε*/2) to get that *δ*_{X*}(*ε*)≥(*ε*/2)*τ*(*ε*/2)−*ρ*_{X}(*ε*/2)≥*η*(*ε*).

(ii) Let *ε*∈(0,2], *d*≥1 and *x*,*y*∈*B*_{d}(0) with ∥*x*−*y*∥≤*ω*(*d*,*ε*). W.l.o.g. we may assume that ∥*y*∥≥∥*x*∥ and also that ∥*y*∥>*ε*/2 since otherwise ∥*Jx*−*Jy*∥≤∥*Jx*∥+∥*Jy*∥=∥*x*∥+∥*y*∥≤*ε*.
Hence . By the uniform convexity of *X**, one gets that and so . ■

### Remark 2.6

If *η*(*ε*) can be written as , where then *ω* can be improved to observe that with this *ω*
and so as before ∥(1/∥*y*∥)*Jx*−(1/∥*y*∥)*Jy*∥<*ε*/∥*y*∥, i.e. ∥*Jx*−*Jy*∥<*ε*.

It is well known that the Banach spaces *L*_{p} with are both uniformly convex and uniformly smooth. A modulus of uniform convexity *η*_{p}(*ε*) is
Since is isometrically isomorphic with *L*_{p′}, where *p*′=*p*/(*p*−1) is the H older conjugate of *p*, we get (using remark 2.6) that *L*_{p} is a space with a uniformly continuous duality selection map with modulus for all *ε*∈(0,2] and *d*≥1.

## 3. An application to Halpern iterations

Let *X* be a Banach space, *C*⊆*X* a convex closed subset and *T*:*C*→*C* be a non-expansive mapping. The so-called *Halpern iteration* is defined as follows:
3.1where (*λ*_{n})_{n≥1} is a sequence in [0,1] and *x*,*u*∈*C*. We refer to Kohlenbach & Leuştean [18] for a discussion.

For *t*∈(0,1) and *u*∈*C*, define by . Because is a contraction, we apply Banach's contraction mapping principle to get a unique fixed point :
3.2

The following extension of Wittmann's result was obtained by Shioji & Takahashi [22] (see also [33] for an earlier result in this direction).

### Theorem 3.1

*Let X be a Banach space whose norm is uniformly Gâteaux differentiable, C⊆X be closed and convex and T:C→C be a non-expansive mapping with Fix(T)≠∅. Assume that*

*diverges and**converges; and**converges strongly to a fixed point z of T as t↓0.*

*Then the Halpern iteration converges strongly to z.*

In this paper, we obtain an effective version of theorem 3.1 by applying proof mining techniques to Shioji & Takahashi's proof, which is highly ineffective. Firstly, with the methods developed in Kohlenbach & Leuştean [18], we eliminate the use of Banach limits from the proof. Secondly, we extract an effective and highly uniform rate of metastability, which then is guaranteed to exist by theorem 2.2.

### Theorem 3.2

*Let (X,J) be a space with a uniformly continuous duality selection map with modulus ω, C⊆X be a bounded convex closed subset with diameter d*_{C}*, T:C→C a non-expansive mapping and x,u∈C. Let* *be such that M≥d*_{C}*.*

*Assume that* *with rate of convergence α,* *diverges with rate of divergence θ and* *converges with β being a Cauchy modulus of* *.*

*Let t*_{k}*:=1/(k+1), k≥1 and assume that* *is Cauchy with rate of metastability K, i.e.
*3.3*Then the Halpern iteration (x*_{n}*) is Cauchy and, for all ε∈(0,2) and* 3.4*where
*

### Remark 3.3

For the most important case *λ*_{n}:=1/(*n*+1), the moduli *θ*,*α*,*β* are all easily computable. In fact, one can avoid the use of the exponential *θ* by using instead of the divergence of (see [18] for details on this).

### Theorem 3.4

*Let λ*_{n}*:=1/(n+1), n≥1, t*_{k}*:=1/(k+1), k≥1 and denote* *by *.

*If K(ε) is a rate of convergence of**then the bound in theorem 3.2 gives a rate of convergence of (x*_{n}*).**If X is an effective Hilbert space and T,u are computable, then**has a computable rate of convergence iff ∥z−u∥ is computable, where**.*

### Proof.

(i) *K*(*ε*/2) is a witness (not only a bound) of metastability for any function *g* (i.e. we can take *K*_{1}:=*K*(*ε*/2) in (3.3)). Hence we can replace in the bound *Σ* from theorem 3.2 *K*(*ε*_{0},*f**) by *K*(*ε*_{0}/2), which makes the bound independent of *g* because *g* enters only via the definition of *f**. Also note that the maximum in the definition of *Γ* can be replaced by just taking *k*:=*K*(*ε*_{0}/2). Then (3.4) holds with *N*:=*Σ* for all *g* where now *Σ* is independent of *g*.

(ii) From Kohlenbach [14], p. 2789, it follows that a rate of convergence for is given by a rate of convergence of the non-decreasing and *M*-bounded sequence which is computable provided that the limit is computable. Conversely, if we have a computable rate of convergence for , then *z* and hence ∥*z*−*u*∥ is computable. ■

### (a) Technical lemmas

In the following, (*X*,*J*) is a space with a uniformly continuous duality selection map with modulus *ω*, *C*⊆*X* is a bounded convex closed subset with diameter *d*_{C} and *T*:*C*→*C* is a non-expansive mapping. We consider with *M*≥*d*_{C}. Thus, *M*≥∥*x*−*y*∥ for all *x*,*y*∈*C*.

### Lemma 3.5

3.5

### Proof.

Remark that . ■

Given a sequence (*a*_{n})_{n≥1} of real numbers, we shall consider for all *m*,*p*≥1 the average . As in Kohlenbach & Leuştean [18], the use of Banach limits in Shioji–Takahashi's proof can be eliminated in favour of elementary lemmas on the finitary objects *C*_{m,p}.

Let *x*,*u*∈*C*, *t*∈(0,1), (*λ*_{n}) be a sequence in [0,1], (*x*_{n}) be the Halpern iteration defined by (3.1) and given by (3.2). Define for all *n*≥1
3.6

Let us recall that (*x*_{n}) is said to be *asymptotically regular* if . A rate of convergence of (∥*x*_{n}−*Tx*_{n}∥) towards 0 will be called a rate of asymptotic regularity.

### Proposition 3.6

For all

*n*≥1, .If (

*x*_{n}) is asymptotically regular with rate of asymptotic regularity*φ*, then for all*ε*∈(0,2) 3.7where*P*(*ε*,*t*,*M*,*φ*)=⌈(6*M*^{2}/*tε*)*φ*(*tε*/6*M*)⌉.Assume that (

*x*_{n}) is asymptotically regular with rate of asymptotic regularity*φ*and that with rate of convergence . Then for all*ε*∈(0,2) 3.8where with*P*given by (ii) and*ε*′=*ε*/(*P*(*ε*/2,*t*,*M*,*φ*)+1).

### Proof.

For simplicity, we shall denote by *z*_{t}.

(i) Firstly, let us remark that *x*_{n}−*z*_{t}=(1−*t*)(*x*_{n}−*Tz*_{t})+*t*(*x*_{n}−*u*) so that, by (3.5), we get ∥*x*_{n}−*z*_{t}∥^{2}≤(1−*t*)^{2}∥*x*_{n}−*Tz*_{t}∥^{2}+2*t*〈*x*_{n}−*u*,*J*(*x*_{n}−*z*_{t})〉. On the other hand,
It follows that
so that 0≤(3*M*(1−*t*)^{2}/*t*)∥*x*_{n}−*Tx*_{n}∥+*tM*^{2}−2〈*u*−*z*_{t},*J*(*x*_{n}−*z*_{t})〉. We get finally that
(ii) Let *ε*∈(0,2) and denote *a*_{n}:=(3*M*/*t*)∥*x*_{n}−*Tx*_{n}∥. By (i) we get that for all *m*≥1, *p*≥1. Furthermore, with rate of convergence *φ*(*tε*/3*M*) and *L*:=3*M*^{2}/*t* is an upper bound for (*a*_{n}). Apply now [18], lemma 8.5 for (*a*_{n}).

(iii) We have that . Because ∥*x*_{n+1}−*z*_{t}∥, ∥*x*_{n}−*z*_{t}∥, ∥*u*−*z*_{t}∥≤*M* for all *n* and with rate of convergence , we obtain from the uniform continuity of *J* that with rate of convergence . Apply now (ii) and [18], lemma 8.4. ■

### Lemma 3.7

3.9

### Proof.

For simplicity, we shall denote by *z*_{t}. One has *x*_{n+1}−*z*_{t}=(1−*λ*_{n+1})(*Tx*_{n}−*z*_{t})+*λ*_{n+1}(*u*−*z*_{t}) and *Tx*_{n}−*z*_{t}=(*Tx*_{n}−*Tz*_{t})+*t*(*Tz*_{t}−*u*). Applying twice (3.5), we get that
■

### (b) Proof of theorem 3.2

Let *ε*∈(0,2) and be fixed. By Kohlenbach & Leuştean [18], proposition 6.1, we have that (*x*_{n}) is asymptotically regular with rate of asymptotic regularity *Φ* and with rate of convergence . To make the proof easier to read, we shall omit parameters for all the functionals that appear in the following. For *t*_{k}:=1/(*k*+1), let us denote simply by and by . By proposition 3.6(iii), we obtain that for each *k*≥0 and *n*≥*χ*_{k}(*ε*,*ω*).

We apply (3.3) for *ε*_{0} and *f** to get the existence of *K*_{1}≤*K*(*ε*_{0},*f**) such that for all *k*,*l*∈[*K*_{1},*K*_{1}+*f**(*K*_{1})]. Let *K*_{0}:=*K*_{1}+⌈1/*ε*_{0}⌉. Then ⌈1/*ε*_{0}⌉≤*K*_{0}≤*K*(*ε*_{0},*f**)+⌈1/*ε*_{0}⌉ and it is easy to see that for all *k*,*l*∈[*K*_{0},*K*_{0}+*f*(*K*_{0})].

Let . Then for all *n*≥1,
It follows that for all *n*≥*χ*_{K0}(*ε*^{2}/24,*ω*)=*χ**_{K0}(*ε*^{2}/12,*ω*). Applying lemma 3.7 with *t*:=1/(*P*+1), we get that, for all *n*≥1,
because *P*≥⌈2*M*^{2}/Δ*_{K0}(*ε*^{2}/4,*g*)⌉, hence 1/(*P*+1)≤Δ*_{K0}(*ε*^{2}/4,*g*)/2*M*^{2}. It follows that we can apply Kohlenbach & Leuştean [18], lemma 5.2 with *ε*:=*ε*^{2}/4 to conclude that for all *n*∈[*N*,*N*+*g*(*N*)], where . We conclude that

## Acknowledgements

U.K. has been supported by the German Science Foundation (DFG project KO 1737/5-1). L.L. was supported by a grant from the Romanian National Authority for Scientific Research, CNCS-UEFISCDI, project number PN-II-ID-PCE-2011-3-0383.

## Footnotes

One contribution of 18 to a Theme Issue ‘The foundations of computation, physics and mentality: the Turing legacy’.

↵1 There are, however, important situations in which even ineffective proofs guarantee effective rates of convergence, e.g. in the presence of uniqueness conditions [7,10,11] or in cases of monotone convergence [7].

↵2 That this can improve things even when applied to constructive proofs is discussed in Kohlenbach [7, p. 171].

- This journal is © 2012 The Royal Society