BRICS RS-00-9 U. Kohlenbach: Effective Uniform Bounds on the Krasnoselski-Mann Iteration BRICS

Basic Research in Computer Science

Effective Uniform Bounds on the Krasnoselski-Mann Iteration

Ulrich Kohlenbach BRICS Report Series RS-00-9 ISSN 0909-0878 May 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, Ulrich Kohlenbach.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/00/9/

Effective uniform bounds on the Krasnoselski-Mann iteration

Ulrich Kohlenbach

BRICS^{∗}

Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C, Denmark kohlenb@brics.dk

April 2000

Abstract

This paper is a case study in proof mining applied to non-effective proofs in nonlinear functional anlysis. More specifically, we are concerned with the fixed point theory of nonexpansive selfmappings f of convex sets C in normed spaces. We study the Krasnoselski iteration as well as more general so-called Krasnoselski-Mann iterations. These iterations converge to fixed points of f only under special compactness conditions and even for uniformly convex spaces the rate of convergence is in general not computable in f (which is related to the non-uniqueness of fixed points). However, the iterations yield approximate fixed points of arbitrary quality for general normed spaces and bounded C (asymptotic regularity). In this paper we apply general proof theoretic results obtained in previous papers to non-effective proofs of this regularity and extract uniform explicit bounds on the rate of the asymptotic regularity. We start off with the classical case of uniformly convex spaces treated already by Krasnoselski and show how a logically motivated modification allows to obtain an improved bound.

∗Basic Research in Computer Science, Centre of the Danish National Research Foundation.

Already the analysis of the original proof (from 1955) yields an elementary proof for a result which was obtained only in 1990 with the use of the deep Browder-Göhde-Kirk fixed point theorem. The improved bound from the modified proof gives applied to various special spaces results which previously had been obtained only by ad hoc calculations and which in some case are known to be optimal. The main section of the paper deals with the general case of arbitrary normed spaces and yields new results including a quantitative analysis of a theorem due to Borwein, Reich and Shafrir (1992) on the asymptotic behaviour of the general Krasnoselski-Mann iteration in arbitrary normed spaces even for unbounded sets C. Besides providing explicit bounds we also get new qualitative results concerning the independence of the rate of convergence of the norm of that iteration from various input data. In the special case of bounded convex sets, where by well-known results of Ishikawa, Edelstein/O’Brian and Goebel/Kirk the norm of the iteration converges to zero, we obtain uniform bounds which do not depend on the starting point of the iteration and the nonexpansive function and the normed space X and, in fact, only depend on the error ε, an upper bound on the diameter of C and some very general information on the sequence of scalars λ_{k} used in the iteration. Even non-effectively only the existence of bounds satisfying weaker uniformity conditions was known before except for the special situation, where λ_{k} := λ is constant. For the unbounded case, no quantitative information was known so far.

1 General introduction

This paper is another case study in the project of ‘proof mining’^{1} in analysis by which we mean the logical analysis of mathematical proofs (typically using non-effective analytical tools) with the aim of extracting new numerically relevant information (e.g. effective uniform bounds or algorithms etc.) hidden in the proofs.^{2}

Let us discuss in more detail what kind of numerical information we are aiming at. Many problems in numerical (functional) analysis are concerned with the construction of solutions x of certain equations A(x), where x is element of some Polish space (typically with additional structure) and A(x) can be written as F (x) = 0 for some continuous function F : X → IR (usually A, and hence F, will depend on certain parameters a which again belong to Polish spaces). The construction of a solution for A quite often involves two distinct steps:

1The term ‘proof mining’ (instead of G. Kreisel’s ‘unwinding of proofs’) for the activity of extracting additional information hidden in given proofs using proof theoretic tools was suggested to the author by Professor Dana Scott.

2For a different case study in analysis in the context of best approximation theory see [21],[22].

For other kinds of logical analyses of specific proofs see [32] and [35].

1) Approximate solutions (also called ‘ε-solutions’) x_{n} ∈ X satisfying A_{\frac{1}{n}} (x_{n}) with

A_{ε}(x) :≡ (|F (x)| < ε)

are constructed (uniformly in the parameters of A).

2) One shows, using e.g. compactness arguments, that either (x_{n})_{n∈IN} itself or some subsequence converges to a solution of A(x).

It is the non-effectivity of the second step which in many cases prevents one from being able to compute a solution x̂ of A effectively within a prescribed error \frac{1}{k}, i.e. to compute a function n(k) such that d_{X}(x_{n(k)}, x̂) < \frac{1}{k}. Even when X := K is compact and x̂ is uniquely determined, so that (x_{n}) itself converges to x̂, explicit a-priori bounds (in particular not depending on x̂ itself) on the rate of convergence of that sequence are often not provided in numerical analysis (due to the ineffectivity of the proof of the uniqueness of x̂).^{3} In several papers we have shown how proof theoretic techniques can be applied to extract certain quantitative information (so-called uniform moduli of uniqueness which generalize the concept of strong unicity as used e.g. in Chebycheff approximation theory) even from highly non-constructive uniqueness proofs and how effective rates of convergence can be obtained using this information (see [25] for an introduction to this and [21],[22],[23] for concrete applications to approximation theory). In this paper we are concerned with applications to the first of the two steps mentioned above in situations where an effective solution of 2) is not possible (mainly due to the lack of uniqueness).

These applications to 1) fall under (an extension of) the general logical scheme as our previous applications to 2) where an instance of. In a series of papers ([23],[24],[25],[27] among others) we have developed general meta-theorems which guarantee the extractability of uniform bounds from proofs which are allowed to make use of substantial parts of analysis. In particular, we specified situations where (due to the fact that only weak forms of induction are used) exponential and even polynomial bounds are guaranteed. Furthermore, these results show that many lemmas used in such proofs do not need to be analysed (since they do not contribute to the bound) because of their logical form. The proofs of these meta-theorems actually provide an extraction algorithm (based on certain proof-theoretic transformations of the specific proof to be analyzed). So applied to a given proof p in analysis we get another proof p^{∗} which provides more numerical information. When this transformation is carried out explicitly we obtain a new ordinary mathematical proof of a stronger statement which no longer relies on any logical tools at all. Of course, the general proof-theoretic algorithm will usually be used only as a guideline but not followed step by step in the actual construction of p^{∗} (unless this is necessary). The special case of our general meta-theorems which is relevant for the present paper has the following form: Let X be a Polish space, K a compact metric space and A_{1} a purely existential property. If a theorem of the form

3See also [31] for an interesting discussion of this and related points.

(∗) ∀n ∈ IN∀x ∈ X∀y ∈ K∃m ∈ INA_{1}(n, x, y, m)

has been proved in certain formal systems T for (fragments of) analysis, then one can extract a computable uniform bound Φ(n, x)^{4} for ∃m, i.e.

∀n ∈ IN∀x ∈ X∀y ∈ K∃m ≤ Φ(n, x)A_{1}(n, x, y, m).

An important feature of the bound Φ(n, x) is that it does not depend on y ∈ K. Typically, ∃mA_{1} is monotone in m so that the bound Φ(n, x) actually realizes the quantifier. In [25] we have specified a system PBA of polynomially bounded analysis which guarantees that Φ(n, x) will be a polynomial. If we add the exponential function to PBA we obtain a system EBA which guarantees that Φ uses at most a finite iteration of exp (so if exp is not iterated at all the bound will be exponential in n relative to x). Whereas for our first application in the present paper (theorem 3.9 below) this result for PBA is already sufficient for providing the general logical framework, our analysis of a proof from [4] carried out in theorem 4.5 needs an extended version due to the use of a principle used in that proof which is not available in PBA or EBA. Whereas these systems contain quite some parts of nonconstructive analysis, principles based on sequential compactness are not included. The significant and highly non-trivial impact of such principles for the extraction of bounds has been determined completely in [27] and [28]. We only discuss the results for the particular simple case of the principle

PCM(a_{k}) :≡ [∀n(0 ≤ a_{n+1} ≤ a_{n}) → ∃a ∈ IR_{+}( lim_{n→∞} a_{n} = a)]

4This bound (as well as the logical form of A_{1}) will in general depend on the specific representation of x ∈ X used in T .

of convergence for bounded monotone sequences (a_{n})_{n∈IN} of reals, as it is this principle which is used in the proof from [4] we are going to analyse. In systems like PBA, real numbers are represented as Cauchy sequences of rational numbers with fixed rate of convergence. Because of this representation PCM(a_{n}) is a fairly strong principle equivalent to

(+) ∀n(0 ≤ a_{n+1} ≤ a_{n}) → ∃f : IN → IN∀k, m(m ≥ f(k) → a_{f(k)} − a_{m} ≤ \frac{1}{k + 1}).

Because of the existence of the ‘Cauchy modulus f’, ‘∀(a)_{n} PCM(a_{n})’ is equivalent to the principle of so-called arithmetical comprehension which potentially creates bounds of huge complexity when added to systems like PBA, EBA (see [28]). What we showed in [27] is, that things are quite different when PCM(a_{n}) is only applied to sequences (a_{n}) in a given proof of a theorem (∗) which can be explicitly defined in terms of the parameters n, x, y of (∗). Then, relative to PBA and EBA, the use of PCM(a_{n}) can be reduced to its arithmetical version^{5}

PCM_{ar}(a_{n}) :≡ [∀n(0 ≤ a_{n+1} ≤ a_{n}) → ∀k∃n∀m(m ≥ n → a_{n} − a_{m} ≤ \frac{1}{k + 1})] .

By further proof theoretic considerations, the use of PCM_{ar} can even be reduced to that of its so-called ‘no-counterexample interpretation’ (or ‘Herbrand normal form’)

PCM_{ar}^{H}(a_{n}) :≡ [∀n(0 ≤ a_{n+1} ≤ a_{n}) → ∀k, g∃n(g(n) ≥ n → a_{n} − a_{g(n)} ≤ \frac{1}{k + 1})] .

The computational significance of this reduction is, that in contrast to the quantifier dependency ‘∀k∃n’ in PCM_{ar}, which in general has no computable bound, the quantifier ‘∃n’ in PCM_{ar}^{H} can be bounded (uniformly in k, g and an upper bound N ∈ IN of a_{0}) by Ψ̂(k, g, N) := max_{i≤(k+1)N} Ψ(i, g), where Ψ(k, g) is the k-times iteration of g

applied to 0, i.e.

Ψ(0, g) := 0, Ψ(k + 1, g) := g(Ψ(k, g))

(see [27] for details on all this). We like to stress, that this quantitative bound for PCM_{ar}^{H}(a_{n}) only depends on (a_{n}) via an upper bound N ≥ a_{0} whereas a bound for ∃n in PCM_{ar}(a_{n}) of course has to depend on (a_{n}). So the reduction from PCM_{ar}(a_{n}) to PCM_{ar}^{H}(a_{n}) also provides an important independence from (a_{n}) which will play a crucial role in our proof of corollaries 4.6 and 4.8 below. We have seen that the use of PCM(a_{n}) for definable (a_{n}) contributes to the bound Φ by Ψ̂. By finite iteration, Ψ (and hence Ψ̂) is able to produce arbitrary primitive recursive growth rates. However, in practice it will usually only be applied to some fixed functions g which can explicitly defined in terms of the parameters of the problem. It is the construction of these functions which plays a crucial role in the process of proof mining. This fact is clearly reflected in the bounds we obtain in theorem 4.5 and corollary 4.6 below (see the definition of α̂ in these results).^{6}

5Because of (+), PCM(a_{n}) essentially is the so-called Skolem normal form of PCM_{ar}(a_{n}). In general it is NOT possible (in a context like PBA or EBA) to reduce the use of the Skolem normal form of an arithmetical principle A to A itself. The fact that this IS possible for PCM_{ar} makes profound use of the fact that this principle satisfies a strong monotonicity property, see [26].

We have discussed the logical background of the results in the present paper in some detail in order to convince the reader, that these results are just special instances of a general scheme for proof mining. Once one is familiar with this scheme, one can almost mechanically produce improvements of existence theorems in analysis of the kind we illustrate here using examples from fixed point theory.

2 Applications to the fixed point theory of nonexpansive mappings

The examples which we will treat in this paper are taken from the fixed point theory of nonexpansive mappings f : C → C, for certain sets C in normed spaces X. The well-known Banach fixed point theorem tells us that contractive mappings f always have a unique fixed point if X is complete and C is closed and that the sequence x_{k+1} := f(x_{k}) starting from any x_{0} ∈ C effectively converges to that fixed point. For nonexpansive functions f (i.e. functions which are Lipschitz continuous with Lipschitz constant λ = 1), in general fixed points only exist if C is closed convex and bounded (by the Browder-Göhde-Kirk fixed point theorem, see theorem 3.3 below). If X is a uniformly convex Banach space, C ⊂ X is closed convex and bounded and f(C) is a compact subset of C, then a fixed point of f can be approximated by the following Krasnoselski iteration (see theorem 3.4 below)^{7}

6In the concrete application in this paper it is mainly the reduction from PCM_{ar} to PCM_{ar}^{H} which plays a significant role in the proof mining. The (in general much more complicated) reduction from PCM to PCM_{ar} is almost straightforward. However, we expect that this will be different for other examples. In any case, we believe that the fact that our applications to concrete proofs reflect crucial steps of the general proof-theoretic reduction and are instances of a general meta-theorem (which at least under an additional compactness assumption predicts the type of results we obtain), makes it justified to call them genuine applications of logic in the sense discussed in [10].

x_{k+1} := \frac{1}{2}(x_{k} + f(x_{k})), x_{0} ∈ C arbitrary.

However, the situation still is quite different from the Banach fixed point theorem since

1) f may have several fixed points,

2) a fact closely related to the non-uniquenes of the fixed point is, that the rate of convergence of the Krasnoselski iteration to its limit is not computable uniformly in f and x_{0} (see [29]).

So the Krasnoselski iteration does not provide an algorithm for the computation of a fixed point of f (with prescribed precision) but it can be used to find effectively approximate fixed points. Since (x_{k}) converges to some fixed point of f and f is continuous it is clear that for a sufficiently large n on, x_{m} (m ≥ n) will be an approximate fixed point:

(∗)∀ε > 0∃n ∈ IN∀m ≥ n(∥x_{m} − f(x_{m})∥ < ε).

Because of the simple monotonicity property (see lemma 3.8 below)

∥x_{m+1} − f(x_{m+1})∥ ≤ ∥x_{m} − f(x_{m})∥

the formula

∀m ≥ n(∥x_{m} − f(x_{m})∥ < ε)

is equivalent to

∥x_{n} − f(x_{n})∥ < ε,

which (given a representation of real numbers as Cauchy sequences of rational numbers with fixed rate of convergence) is ∈ Σ_{1}^{0}. That is why we are able to extract an algorithm for n in (∗) uniformly in x_{0} and f (if X, C have a computable representation). Let us assume for the moment that C := K itself is compact. Then the standard proof (as given in e.g. [3]) of the Krasnoselski fixed point theorem (more precisely of its consequence (∗) above) directly fits into the general extraction scheme discussed above. Besides basic arithmetical reasoning only the existence of a fixed point y ∈ K of f (which follows from the Schauder fixed point theorem) is used to show (∗). Since the statement

7Due to a much more general result from [16], which we will discuss below, the assumption of X being uniformly convex actually is superfluous.

(a) ∃y ∈ K(∥f(y) − y∥ = 0)

has the logical form of those assumptions which do not contribute to the growth of extractable bounds and which furthermore can be reduced to their ε-weakening

(b) ∀ε > 0∃y ∈ K(∥f(y) − y∥ < ε)

and since furthermore the starting point x_{0} ∈ K belongs to a compact set and the set of all nonexpansive mapping f : K → K is also compact, we know a-priori that the extractability of a uniform bound (of low complexity) for n in (∗) which does not depend on x_{0} or f (but only on ε and a modulus of uniform convexity) is guaranteed whose verification only uses (b). The actual extraction shows that instead of the compactness only the boundedness of K is needed. This is even true for the reduction of (a) to (b) which allows furthermore to remove the assumption on K being closed (and X being complete), since the existence of approximate fixed points (but not of fixed points) can be shown without these assumptions. This, of course, is an a-posteriori information which was not guaranteed by a general logical result. Nevertheless, the a-priori information provided for the special case with K being compact prompted the search for such uniform bounds. As a result we get for an arbitrary convex bounded subset C ⊂ X a uniform bound for (∗) depending only on ε, a modulus of uniform convexity η of X and an upper bound for the diameter of C. The bound itself is not new: for the special compact case it is essentially already contained in Krasnoselski’s original paper ([30]) and was proved for the case of closed bounded convex sets in [18] using the deep Browder-Göhde-Kirk fixed point theorem. We nevertheless carry out the analysis because it shows two phenomena:

1) the possibility of replacing the existence of fixed points by the existence of ε-fixed points which allows to give a complete elementary verification of the bound (without assuming X complete or C being closed). 2) There is a logical modification of the proof from [3] which makes use of the above mentioned no-counterexample interpretation PCM_{ar}^{H} of PCM_{ar} and allows to make use of a certain multiplicative property many moduli η satisfy, by which we obtain (for such moduli) a numerically better result. As a special instance of this we get a bound which is polynomially in ε of degree p for the spaces L_{p} with p ≥ 2 (a result which (for this special case only) first was obtained in 1990 in [18] by an ad hoc calculation). For X := IR, C := [0, 1] we even get a linear bound (see also [18], p.192).

What is more interesting is that the authors conjecture in that very paper that ‘it seems unlikely’ ([18]), p. 191) that such bounds could easily be obtained in more general situations where X is not required to be uniformly convex. More specifically, in [12](p. 101) it is considered to be ‘unlikely’ that bounds which only depend on C via an upper bound for the diameter of C exist at all in this general case. It is exactly this general situation which we study in the final and main section of the paper. As a special corollary of a more general result we obtain that in contrast to this conjecture in [12] such uniform bounds not only exist (even for more general socalled Mann iterations, see corollary 4.8) but can be easily described (see corollaries 4.10 and 4.6 below).^{8} Let us discuss this in more detail. We consider strong generalizations of Krasnoselski’s result due to [16],[8],[11] and [4]. In [16] it is shown that Krasnoselski’s fixed point theorem even holds without the assumption of X being uniformly convex. Even much more general so-called Krasnoselski-Mann iterations

x_{k+1} := (1 − λ_{k})x_{k} + λ_{k}f(x_{k})

are allowed, where λ_{k} is a sequence in [0, 1] which is divergent in sum and satisfies

lim sup_{k→∞} λ_{k} < 1.

In particular, it is proved in [16] that for such iterations

(I) lim_{k→∞} ∥x_{k} − f(x_{k})∥ = 0,

where X is an arbitrary normed linear space, C a bounded convex subset of X and f : C → C is nonexpansive. This result is further generalized in [4] to the case where C no longer is required to be bounded. Then one has

(II) lim_{k→∞} ∥x_{k} − f(x_{k})∥ = r_{C}(f),

where

r_{C}(f) := inf_{x∈C} ∥x − f(x)∥

will in general be strictly positive. We give a complete quantitative analysis of (II) (see theorem 4.5) as an instance of our general result on the extractability of bounds from proofs using PCM(a_{k}) for a sequence (a_{k})_{k∈IN} which is definable in the parameters of the problem. In the case at hand (a_{k})_{k∈IN} is just (∥x_{k}−f(x_{k})∥)_{k∈IN}. We then specialize the resulting bound to the case where C is bounded and derive a uniform bound for (I) which only depends on ε, an upper bound d_{C} for the diameter d(C) of C and some quite weak information on (λ_{k}) (see corollary 4.6). None of the papers [16],[8],[11],[4] contains any bounds and in fact [8] and [11] use non-trivial functional theoretic embeddings to show (ineffectively) the existence of a common number k ∈ IN which satisfies ∥x_{k} − f(x_{k})∥ < ε uniformly for all starting points x_{0} ([8])^{9} and all nonexpansive functions f ([11]). This uniformity comes for free out of our proof analysis. Moreover, as already mentioned we also have a new strong uniformity concerning C as the bounds only depend on d_{C} and to some extent also a uniformity w.r.t. (λ_{k}) (corollary 4.8). All this shows that the authors of the papers listed were not aware of the uniform bounds hidden in their proofs (note that the proof in [16] essentially is contained as a special case in the proof from [4] we are analyzing, so that the logical analysis of the former is even simpler than our proof analysis for the stronger result (II)). Only in the special case of λ_{k} = λ being constant a uniform (and in fact optimal quadratic) bound was known before (in 1996) by [1], however, with an extremely complicated proof involving computer assisted parts.^{10} This clearly indicates the usefulness of analysing noneffective proofs logically even if one is not particularly interested in the numerical details of the bounds themselves (or the bounds obtained happen to be too bad to be useful in practice). In many cases such explicit bounds immediately show the independence of the quantity in question from certain input data.^{11}

8See also the discussion at the end of this paper.

3 Effective uniform bounds on the Krasnoselski iteration in uniformly convex spaces

Definition 3.1 Let (X, ∥ · ∥) be a normed linear space and S ⊆ X be a subset of X. A function f : S → S is called nonexpansive if

(∗) ∀x, y ∈ S(∥f(x) − f(y)∥ ≤ ∥x − y∥).

9This paper only considers the special case where λ_{k} := λ is constant.

10In this paper, again the noneffectivity of all the proofs mentioned above is stressed.

11Another example for this: the explicit uniform constants of strong unicity for Chebycheff approximation which we extracted in [21],[22] by analysing classical uniqueness proofs for the best Chebycheff approximation (known already since about 1905-1917) immediately implied the existence of a common constant of unicity for compact sets K of functions f ∈ C[a, b], if inf_{f∈K} dist(f, H) > 0 (H a Haar space), a fact that was proved in approximation theory only in 1976 without providing any bounds (see [15]).

Definition 3.2 ([6]) A normed linear space (X, ∥ · ∥) is called uniformly convex if

∀ε > 0∃δ > 0∀x, y ∈ X(∥x∥, ∥y∥ ≤ 1 ∧ ∥x − y∥ ≥ ε → ∥\frac{1}{2}(x + y)∥ ≤ 1 − δ).

A function η : (0, 2] → (0, 1] providing such a δ := η(ε) > 0 for given ε > 0 is called a modulus of uniform convexity.

The following fundamental existence theorem for fixed points of nonexpansive mappings and uniformly convex Banach spaces was proved independently by Browder, Göhde and Kirk (note that no compactness assumption is made in this result):

Theorem 3.3 ([5],[13],[17]) Let (X, ∥ · ∥) be a uniformly convex Banach space, C ⊆ X a non-empty convex closed and bounded subset of X and f : C → C a nonexpansive mapping. Then f has a fixed point.^{12}

Another fundamental theorem in the fixed point theory for nonexpansive mappings is the following result due to Krasnoselski, which shows that (under an additional compactness condition, which by the Schauder fixed point theorem guarantees the existence of a fixed point) a fixed point of f can be approximated by a special iteration sequence:

Theorem 3.4 (Krasnoselski [30]) Let K be a non-empty convex closed and bounded set in a uniformly convex Banach space (X, ∥ · ∥) and f a nonexpansive mapping of K into a compact subset of K. Then for every x_{0} ∈ K, the sequence

x_{k+1} := \frac{x_{k} + f(x_{k})}{2}

converges to a fixed point z ∈ K of f.

Remark 3.5 Note that the iteration x_{k+1} := f(x_{k}) from the Banach fixed point theorem in general fails to converge in the setting of theorem 3.4: Take X := IR (with the absolute value as norm), K := [0, 1] and f(x) := 1 − x. X is uniformly convex, K is compact and convex, and f : K → K is nonexpansive, but the sequence defined by x_{0} := 0, x_{k+1} := f(x_{k}) alternates between 0 and 1.

12For a nice counterexample showing that the assumption of X being uniformly convex is necessary, see [7](p.37).

One can show that there cannot be an effective procedure to compute a rate of convergence of the iteration in the Krasnoselski fixed point theorem uniformly in f and the starting point x ∈ K of the iteration (see [29]). This already holds for the special case of X := IR and K := [0, 1] and the fixed starting point x_{0} := 0 as there exists no computable function F from the set of all nonexpansive functions f : [0, 1] → [0, 1] into [0, 1] which computes uniformly in f a fixed point of f (this is closely related to the fact that such a function F cannot be continuous with respect to the maximum norm ∥f∥_{∞}). Logically, this ineffectivity in Krasnoselski’s theorem corresponds to the fact the statement that (x_{k})_{k∈IN} converges is Π_{3}^{0}. On the other hand if we consider the weaker question of how far we have to go in the iteration to obtain an ε-fixed point, then we notice that the logical form of the statement

(∗) ∀k ∈ IN∃n ∈ IN(∥x_{n} − f(x_{n})∥ < \frac{1}{k + 1})

is Π_{2}^{0} (assuming that real numbers are represented as Cauchy sequences with fixed rate of convergence so that <_{IR}∈ Σ_{1}^{0}) and hence we can find a witness n by unbounded search (effectively in k, f, ∥·∥ and the starting point of the iteration). In the following we extract a bound (and hence in view of lemma 3.8 below a realization) for n from the standard proof of theorem 3.4 (and hence of its corollary (∗)) as it is given in [3].

Definition 3.6 Let (X, ∥ · ∥) be a normed linear space, S a subset of X, f : S → S and ε > 0. A point x ∈ S is called ε-fixed point of f if ∥x − f(x)∥ ≤ ε.

Lemma 3.7 Let (X, ∥·∥) be a normed linear space, ∅ ≠ C ⊆ X convex with bounded diameter d(C) < ∞ and f : C → C nonexpansive. Then f has ε-fixed points in C for every ε > 0.

Proof: To reduce the situation to the Banach fixed point theorem we use the following well-known construction (see e.g. [4] but also [13]): f_{t}(x) := (1 − t)f(x) + tc for some c ∈ C and t ∈ (0, 1]. f_{t} : C → C is a contraction and therefore Banach’s fixed point theorem applies. Note furthermore that the completeness assumption in Banach’s theorem is needed only to guarantee the existence of a limit of the Cauchy sequence (f_{t}^{n}(c))_{n∈IN}, where f_{t}^{n} denotes the n-times iteration of f_{t}, which is not necessary to ensure that f_{t}^{n}(c) is an ε-fixed point of f_{t} for sufficiently large n and hence (for t := ε/d(C)) a 2ε-fixed point of f. That is why we don’t have to assume that X is complete or that C is closed. □

The following lemma belongs to the ‘folklore’ of the subject. We include its simple proof for the sake of completeness.

Lemma 3.8 Let (X, ∥ · ∥) be a normed linear space, C ⊆ X be a convex subset of X and f : C → C a nonexpansive function. Let x_{0} ∈ C be arbitrary and define x_{k+1} := \frac{x_{k}+f(x_{k})}{2}. Then

∀k(∥x_{k+1} − f(x_{k+1})∥ ≤ ∥x_{k} − f(x_{k})∥).

Proof:

∥x_{k+1} − f(x_{k+1})∥ = ∥\frac{1}{2}x_{k} + \frac{1}{2}f(x_{k}) − f(\frac{1}{2}x_{k} + \frac{1}{2}f(x_{k}))∥ =
∥(\frac{1}{2}x_{k} − \frac{1}{2}f(x_{k})) + (f(x_{k}) − f(\frac{1}{2}x_{k} + \frac{1}{2}f(x_{k})))∥ ≤
∥\frac{1}{2}x_{k} − \frac{1}{2}f(x_{k})∥ + ∥f(x_{k}) − f(\frac{1}{2}x_{k} + \frac{1}{2}f(x_{k}))∥ ≤
∥\frac{1}{2}x_{k} − \frac{1}{2}f(x_{k})∥ + ∥x_{k} − (\frac{1}{2}x_{k} + \frac{1}{2}f(x_{k}))∥ =
\frac{1}{2}∥x_{k} − f(x_{k})∥ + \frac{1}{2}∥x_{k} − f(x_{k})∥ = ∥x_{k} − f(x_{k})∥. □

Quantitative analysis of the proof of theorem 3.4 in [3]: We now give two quantitative versions of the consequence (∗) of theorem 3.4. The first one follows directly the proof of the theorem as given in [3]. The second one uses a logical modification of that proof which is motivated by our general elimination procedure for PCM_{ar}. This second analysis allows to take into account in a very easy way a property which is satisfied by many moduli of uniform convexity, e.g. for all spaces L_{p} with p ≥ 2, which makes it possible to improve the results obtained from the first, direct analysis for such spaces. General logical preliminaries: Let us for the moment assume that K itself is compact. In Bonsall’s [3] proof of theorem 3.4 the following is established (where x_{0} := x, x_{k+1} := (x_{k} + f(x_{k}))/2 is the Krasnoselski iteration starting from x):

∀x ∈ K∀ε > 0(∃y ∈ K(f(y) = y) ∧ ∀k(∥f(x_{k}) − x_{k}∥ ≥ ε) → lim_{n→∞} ∥x_{n} − y∥ = 0)

and hence

∀x ∈ K∀ε > 0(∃y ∈ K(f(y) = y) ∧ ∀k(∥f(x_{k}) − x_{k}∥ ≥ ε) → ∃n(∥x_{n} − y∥ < ε)), where the existence of a fixed point y ∈ K is derived from the Schauder fixed point theorem. This can be rephrased in the following form

\begin{matrix}∀x, y ∈ K∀ε > 0∃k, n, l ∈ IN \\ \underbrace{(∥f(y) − y∥ ≤ \frac{1}{l + 1} ∧ ∥f(x_{k}) − x_{k}∥ ≥ ε → ∃ñ ≤ n(∥xñ − y∥ < ε))}_{∈Σ_{1}^{0}} . \end{matrix}

By our general results on the extractability of uniform bounds we know a priori (using the compactness of K as well as of the space of all nonexpansive mappings f : K → K) that we can extract bounds K(ε), N(ε), L(ε) (and hence because of the monotonicity in k, n, l of the formula above, which follows from lemma 3.8, also realizations) for k, n, l which are independent of x, y ∈ K and f and only depend on ε > 0 (and a modulus of uniform convexity η of X). Since we may assume that L(ε) > \frac{1}{ε} and since by the nonexpansivity of f

∥f(y) − y∥ ≤ ε ∧ ∥xñ − y∥ ≤ ε → ∥f(xñ) − xñ∥ ≤ 3ε,

this yields

∃n ≤ max (K(ε), N(ε))(∥f(x_{n}) − x_{n}∥ ≤ 3ε)

and so again by lemma 3.8

∀n ≥ max (K(ε), N(ε))(∥f(x_{n}) − x_{n}∥ ≤ 3ε).

Thus we have obtained a uniform bound and at the same time reduced the assumption ‘∃y ∈ K(f(y) = y)’ to ‘∀ε > 0∃y ∈ K(∥f(y) − y∥ < ε)’. In particular, as the bound does not depend on y, the computation of such an approximate fixed point and hence an analysis of the proof of its existence is not needed. The actual extraction of the bound carried out below reveals that such uniform bounds K, N, L even exist when the compactness assumption on K is replaced by the boundedness of K. Since by lemma 3.7 the existence of approximate fixed points (but not of fixed points) in this much more general setting is even guaranteed for spaces X which are not complete, we can remove this assumption as well and the result is proved without appeal to any fixed point theorem other than Banach’s (actually only its ε-version):

Theorem 3.9 (Direct analysis of Bonsall’s [3] proof of theorem 3.4) Let (X, ∥ · ∥) be a uniformly convex normed space with modulus of convexity η : (0, 2] → (0, 1] and C ⊆ X be a non-empty convex set with

d(C) := sup_{x_{1},x_{2}∈C} ∥x_{1} − x_{2}∥ ≤ d_{C} ∈ Q_{+}^{∗}.

Let f : C → C be a nonexpansive function. Define for arbitrary x ∈ C

x_{0} := x, x_{k+1} := \frac{x_{k} + f(x_{k})}{2}.

Then

∀x ∈ C∀ε > 0∀k ≥ h(ε, d_{C})(∥x_{k} − f(x_{k})∥ ≤ ε),

where h(ε, d_{C}) := ⌈\frac{ln(4d_{C})−ln(ε)}{η(ε/(d_{C}+1))}⌉ for ε < d_{C} and h(ε, d_{C}) := 0 otherwise.

Proof: The theorem is trivial for ε ≥ d_{C}. So we can assume that ε < d_{C}. By lemma 3.7, f has ε-fixed points x_{ε} ∈ C, ∥f(x_{ε}) − x_{ε}∥ < ε for every ε > 0. Let δ > 0 be such that δ < min(1, \frac{ε}{12h(ε,d_{C})}) and let y ∈ C be a δ-fixed point of f, i.e.

(1) ∥y − f(y)∥ < δ.

Assume that

(2) ∥x_{k} − f(x_{k})∥ = ∥(x_{k} − y) − (f(x_{k}) − y)∥ > ε.

Then

(3) ∥\frac{x_{k} − y}{∥x_{k} − y∥ + δ} − \frac{f(x_{k}) − y}{∥x_{k} − y∥ + δ} ∥ > \frac{ε}{∥x_{k} − y∥ + δ} ≥ \frac{ε}{d_{C} + 1}.

Because of

(4) ∥f(x_{k}) − y∥ ≤^{(1)} ∥f(x_{k}) − f(y)∥ + δ ≤ ∥x_{k} − y∥ + δ,

we have

(5) ∥\frac{x_{k} − y}{∥x_{k} − y∥ + δ} ∥ , ∥\frac{f(x_{k}) − y}{∥x_{k} − y∥ + δ} ∥ ≤ 1

and therefore

(6) ∥\frac{1}{2} (\frac{x_{k} − y}{∥x_{k} − y∥ + δ} + \frac{f(x_{k}) − y}{∥x_{k} − y∥ + δ} )∥ ≤ 1 − η(ε/(d_{C} + 1)).

Hence

(7) \{ \begin{matrix}∥x_{k+1} − y∥ = ∥\frac{1}{2}(x_{k} + f(x_{k})) − y∥ = ∥\frac{1}{2}(x_{k} − y + f(x_{k}) − y)∥ ≤ \\ (1 − η(ε/(d_{C} + 1)))(∥x_{k} − y∥ + δ). \end{matrix}

Therefore, if (2) holds for all k ≤ k_{0} := h(ε, d_{C}) − 1 then

(8) \{ \begin{matrix}∥x_{k_{0}+1} − y∥ ≤ (1 − η(ε/(d_{C} + 1)))^{k_{0}+1}∥x_{0} − y∥ + ∑_{i=1}^{k_{0}+1}(1 − η(ε/(d_{C} + 1)))^{i} · δ \\ ≤ (1 − η(ε/(d_{C} + 1)))^{k_{0}+1} · d_{M} + (k_{0} + 1)δ ≤ (1 − η(ε/(d_{C} + 1)))^{k_{0}+1} · d_{C} + \frac{ε}{12}. \end{matrix}

We now show that

(9) (1 − η(ε/(d_{C} + 1)))^{k_{0}+1} · d_{C} ≤ \frac{ε}{4}.

Proof of (9): If η(ε/(d_{C} + 1)) = 1, then the claim holds trivially. Otherwise, (9) is equivalent to

k_{0} + 1 ≥ \frac{ln(ε/4d_{C})}{ln(1 − η(ε/(d_{C} + 1)))}.

Since ln(1) = 0 and \frac{d}{dx}ln(x) = \frac{1}{x} ≥ 1 for all x ∈ (0, 1], we get

− ln(1 − η(ε/(d_{C} + 1))) ≥ η(ε/(d_{C} + 1)).

Together with − ln(ε/4d_{C}) = log(4d_{C}) − ln(ε) this yields (9).

(8) and (9) together imply

(10) ∀k ≤ h(ε, d_{C}) − 1(∥x_{k} − f(x_{k})∥ > ε) → ∥x_{h(ε,d_{C})} − y∥ ≤ \frac{ε}{3}.

Since f is nonexpansive and y is an \frac{ε}{3}-fixed point of f the right-hand side of the implication yields ∥x_{h(ε,d_{C})} − f(x_{h(ε,d_{C})})∥ ≤ ε. So

(11) ∃k ≤ h(ε, d_{C})(∥x_{k} − f(x_{k})∥ ≤ ε)

and hence by lemma 3.8 above

(12) ∀k ≥ h(ε, d_{C})(∥x_{k} − f(x_{k})∥ ≤ ε),

which concludes the proof of the theorem. □ Theorem 3.10 (Analysis of a modification of Bonsall’s [3] proof of thm.3.4) Under the same hypotheses as in theorem 3.9 we obtain

∀x ∈ C∀ε > 0∀k ≥ h(ε, d_{C})(∥x_{k} − f(x_{k})∥ ≤ ε), where h(ε, d_{C}) := ⌈_{\frac{4·d_{C}}{ε·η( \frac{ε}{d_{C} +1} )}}⌉ for ε < d_{C} and h(ε, d_{C}) := 0 otherwise. Moreover, if η(ε) can be written as η(ε) = ε · η̃(ε) with

(∗) ∀ε_{1}, ε_{2} > 0(ε_{1} ≥ ε_{2} → η̃(ε_{1}) ≥ η̃(ε_{2})),

then the bound h(ε, d_{C}) can be replaced (for ε < d_{C}) by

h̃(ε, d_{C}) := ⌈\frac{2 · d_{C}}{ε · η̃(\frac{ε}{d_{C}+1})}⌉ .

Proof: By lemma 3.7, f has ε-fixed points x_{ε} ∈ C, ∥f(x_{ε}) − x_{ε}∥ < ε for every ε > 0. Let δ > 0 be such that δ < min(1, \frac{ε}{3}, \frac{ε}{12} · η(ε/(d_{C} + 1))) and let y ∈ C be a δ-fixed point of f, i.e.

(1) ∥y − f(y)∥ < δ.

Assume that

(2) ∥x_{k} − y∥ ≥ \frac{ε}{3} and

(3) ∥x_{k} − f(x_{k})∥ = ∥(x_{k} − y) − (f(x_{k}) − y)∥ > ε.

As in the proof of theorem 3.9 one shows that

(4) ∥\frac{1}{2} (\frac{x_{k} − y}{∥x_{k} − y∥ + δ} + \frac{f(x_{k}) − y}{∥x_{k} − y∥ + δ} )∥ ≤ 1 − η(ε/(d_{C} + 1)).

Hence

(5) \{ \begin{matrix}∥x_{k+1} − y∥ = ∥\frac{1}{2}(x_{k} + f(x_{k})) − y∥ = ∥\frac{1}{2}(x_{k} − y + f(x_{k}) − y)∥ ≤ \\ ∥x_{k} − y∥ + δ − (∥x_{k} − y∥ + δ) · η(ε/(d_{C} + 1)) ≤^{(2)} \\ ∥x_{k} − y∥ + δ − \frac{ε}{3} · η(ε/(d_{C} + 1)) ≤ ∥x_{k} − y∥ − \frac{ε}{4} · η(ε/(d_{C} + 1)). \end{matrix}

Define

n_{ε} := ⌈ \frac{d_{C}}{\frac{ε}{4} · η(ε/(d_{C} + 1))}⌉ = ⌈\frac{4 · d_{C}}{ε · η(ε/(d_{C} + 1))}⌉ .

If (2), (3) both hold for all k ≤ n_{ε}, then (5) yields (6) ∥x_{n_{ε}+1} − y∥ < ∥x_{0} − y∥ − d_{C}, which contradicts the choice of d_{C} by which ∥x_{k} − y∥ ∈ [0, d_{C}] for all k ∈ IN. Hence

(7) ∃k ≤ n_{ε}(∥x_{k} − y∥ ≤ \frac{ε}{3} ∨ ∥x_{k} − f(x_{k})∥ ≤ ε).

By the choice of δ,(1) and the nonexpansivity of f, the first disjunct also implies that ∥f(x_{k}) − x_{k}∥ ≤ ε and so by the preceding lemma

(8) ∀k ≥ n_{ε}(∥x_{k} − f(x_{k})∥ ≤ ε).

The last claim in the theorem follows by choosing y ∈ C as a δ-fixed point of f with δ < min(1, \frac{ε}{3}, \frac{ε}{2} · η̃(ε/(d_{C} + 1))) and the following modifications of (4), (5) to

(4)^{∗} ∥\frac{1}{2} (\frac{x_{k} − y}{∥x_{k} − y∥ + δ} + \frac{f(x_{k}) − y}{∥x_{k} − y∥ + δ} )∥ ≤ 1 − η(ε/(∥x_{k} − y∥ + δ)).

(5)^{∗} \{ \begin{matrix}∥x_{k+1} − y∥ = ∥\frac{1}{2}(x_{k} + f(x_{k})) − y∥ = ∥\frac{1}{2}(x_{k} − y + f(x_{k}) − y)∥ ≤ \\ ∥x_{k} − y∥ + δ − (∥x_{k} − y∥ + δ) · η(ε/(∥x_{k} − y∥ + δ)) = \\ ∥x_{k} − y∥ + δ − ε · η̃(ε/(∥x_{k} − y∥ + δ)) ≤^{(∗)} ∥x_{k} − y∥ + δ − ε · η̃(ε/(d_{C} + 1)) \\ ≤ ∥x_{k} − y∥ − \frac{ε}{2} · η̃(ε/(d_{C} + 1)) \end{matrix}

(note that we can apply η to ε/(∥x_{k} − y∥ + δ) since (3) and

∥f(x_{k}) − y∥ ≤^{(1)} ∥f(x_{k}) − f(y)∥ + δ ≤ ∥x_{k} − y∥ + δ

imply

ε ≤ ∥x_{k} − y∥ + ∥f(x_{k}) − y∥ ≤ 2(∥x_{k} − y∥ + δ)

and therefore

ε/(∥x_{k} − y∥ + δ) ∈ (0, 2]).

□

If we disregard for a moment the diameter estimate d_{C} in the bounds in theorems 3.9 and 3.10 and put ε := 2^{−n}, then we see that the bound from theorem 3.9 essentially is n/η(2^{−n}), whereas the first bound in theorem 3.10 is only about 2^{n}/η(2^{−n}). If, however, η(ε) can be written as ε · η̃(ε) with η̃ satisfying (∗), then theorem 3.10 roughly gives 1/η(2^{−n}) which is better than the bound from theorem 3.9. It is this fact that we will use in the example below to obtain a polynomial bound for L_{p} (p ≥ 2) which is of degree p.

Examples: It is well-known that the Banach spaces L_{p} with 1 < p < ∞ are uniformly convex (this was first proved in [6], see also [20]). For p ≥ 2, the following explicit modulus η_{p} of uniform convexity was obtained in [14]

η_{p}(ε) := 1 − (1 − (ε/2)^{p})^{1/p}.

One easily shows (using the derivative of x^{1/p}) that (for (0, 2])

η_{p}(ε) ≥ \frac{ε^{p}}{p2^{p}} .

Hence \frac{ε^{p}}{p2^{p}} is a modulus of convexity as well. Since

\frac{ε^{p}}{p2^{p}} = ε · η̃_{p}(ε)

with

η̃_{p}(ε) = \frac{ε^{p−1}}{p2^{p}}

satisfying (∗) in the theorem above, we obtain the following

Corollary 3.11 Let p ≥ 2, C ⊆ L_{p} a non-empty convex subset with d(C) ≤ d_{C} ∈ Q_{+}^{∗}, f : C → C nonexpansive and (x_{k})_{k∈IN} defined as in the theorem. Then

∀x ∈ C∀ε > 0∀k ≥ ⌈\frac{d_{C}p(d_{C} + 1)^{p−1}2^{p+1}}{ε^{p}} ⌉ (∥x_{k} − f(x_{k})∥ ≤ ε).

Note the bound in corollary 3.11 only depends on p, ε and an upper bound d_{C} of d(C) but not on x ∈ C or f.

For the case X := IR, C := [0, 1], theorem 3.10 even gives a linear bound, since ε/2 is a modulus of uniform convexity in this case and η̃(ε) := \frac{1}{2} satisfies (∗).

Remark 3.12 Our result in corollary 3.11 can easily be improved by replacing (d_{C} + 1) by (d_{C} + δ) for any δ > 0 and so in the limit by d_{C}. In [18], using a direct calculation based on the modulus of uniform convexity for L_{p}, essentially the same result is obtained (only with a better constant as the factor ‘p2^{p+1}’ is missing). For a linear bound in the case [0, 1], [18] refer to an unpublished result of J. Alexander. Note, however, that our bounds in these examples, where derived just as a special case from the general bound in theorem 3.10.

4 Effective uniform bounds on the Krasnoselski-Mann iteration in arbitrary normed spaces

Throughout this section, (X, ∥ · ∥) will be an arbitrary normed linear space, C ⊆ X a non-empty convex subset of X and f : C → C a nonexpansive mapping. We consider the so-called Krasnoselski-Mann iteration (which is more general than the Krasnoselski iteration and due to Mann [33]) generated starting from an arbitrary x ∈ C by

x_{0} := x, x_{k+1} := (1 − λ_{k})x_{k} + λ_{k}f(x_{k}),

where (λ_{k})_{k∈IN} is a sequence of real numbers in [0, 1]. For background information on this iteration and plenty of references see [4].

Lemma 4.1 ([4]) For all k ∈ IN and x, x^{∗} ∈ C :

1) ∥x_{k+1} − f(x_{k+1})∥ ≤ ∥x_{k} − f(x_{k})∥,

2) ∥x_{k+1} − x_{k+1}^{∗}∥ ≤ ∥x_{k} − x_{k}^{∗}∥.

Proof: 1) Similarly to lemma 3.8 above.

2) ∥x_{k+1} − x_{k+1}^{∗}∥ = ∥(1 − λ_{k})(x_{k} − x_{k}^{∗}) + λ_{k}(f(x_{k}) − f(x_{k}^{∗})∥ ≤ (1 − λ_{k})∥x_{k} − x_{k}^{∗}∥ + λ_{k}∥f(x_{k}) − f(x_{k}^{∗})∥ ≤ ∥x − x^{∗}∥, because of the non-expansivity

of f. □

For the results in this section we assume (following [4]) that (λ_{k})_{k∈IN} is divergent in sum, which can be expressed (since λ_{k} ≥ 0) as

(A) ∀n, i ∈ IN∃k ∈ IN (∑_{j=i}^{i+k} λ_{j} ≥ n) .

We also assume (again as in [4]) that

(B) lim sup_{k→∞} λ_{k} < 1.

Define

r_{C}(f) := inf_{x∈C} ∥x − f(x)∥.

Theorem 4.2 ([4]) ^{13} Suppose that (λ_{k})_{k∈IN} satisfies the conditions (A) and (B). Then for any starting point x ∈ C and the Krasnoselski-Mann iteration (x_{n}) starting from x we have

∥x_{n} − f(x_{n})∥ →^{n→∞} r_{C}(f).

Corollary 4.3 ([16],[11],[4]) Under the assumptions of theorem 4.2 plus the additional assumption that C has bounded diameter d(C) < ∞ the following holds:

∀x ∈ C∀ε > 0∃nIN∀m ≥ n(∥x_{m} − f(x_{m})∥ ≤ ε).

Proof: Follows from theorem 4.2 and lemma 3.7. □

Remark 4.4 In [11] it is actually shown that one can choose n in the corollary independently of x ∈ C and f. Whereas in [11] a complicated functional theoretic embedding into the space of all nonexpansive mappings is used to derive this uniformity statement, it trivially follows from our quantitative analysis in corollary 4.6 below which even provides an explicit effective description of such a uniform n. For a more restricted iteration the existence of a bound n independent of x was also obtained by [8] using, however, also a universal embedding theorem (due to Banach and Mazur). The use of non-trivial functional theoretic arguments in [11] and [8] to obtain the (ineffective) existence of a uniform n clearly indicates that the authors were not aware of explicit effective uniform bounds hidden in the proof of lim_{k→∞} ∥f(x_{k}) − x_{k}∥ = 0 as given e.g. in [11] and its generalization in [4] which we will

analyze now.^{14}

Quantitative analysis of the proof of theorem 4.2 in [4]:

General logical preliminaries: As we have discussed above, we only can expect to be able to extract a bound ∀x∃y ≤ Φ(x)A(x, y) from a non-constructive proof if A is a purely existential formula. Since the statement in theorem 4.2 involves two implicative assumptions on (λ_{k})_{k∈IN} as well as the existence of r_{C}(f), it prima facie does not have the required form. However, it can be reformulated such as to have the right logical form by enriching the input (λ_{k})_{k∈IN}, f, x, ε by additional data K ∈ IN, α : IN × IN → IN and x^{∗} ∈ C. Let us first examine conditions (A) and (B) on (λ_{k})_{k∈IN} :

13With the additional assumption that λ_{k} is bounded away from zero, this result is also proved in [34].

14For a more detailed discussion, see the final section of this paper.

An explicit version of (A) asks for a function α : IN×IN → IN realizing the existential quantifier, i.e.

(A_{α}) ∀n, i ∈ IN ( ∑_{j=i}^{i+α(i,n)} λ_{j} ≥ n) .

(B) states the existence of a K ∈ IN such that

λ_{k} ≤ 1 − \frac{1}{K}

from some index k_{0} on. Since k_{0} only contributes an additive constant to our bound we may assume for simplicity that k_{0} = 0. So let

(B_{K}) ∀k ∈ IN(λ_{k} ≤ 1 − \frac{1}{K}).

We now formulate the theorem more explicitly as follows:

(∗) \begin{cases}∀(λ_{k}) ∈ [0, 1]^{IN}∀f : C → C∀x, x^{∗} ∈ C∀K, α∀ε > 0∃n ∈ IN \\ (f nonexpans. ∧ (A_{α}) ∧ (B_{K}) → ∥x_{n} − f(x_{n})∥ < ∥x^{∗} − f(x^{∗})∥ + ε). \end{cases}

Note that by lemma 4.1.1), (∗) immediately implies theorem 4.2. By our representation of real numbers by which ≤_{IR}∈ Π_{1}^{0} and <_{IR}∈ Σ_{1}^{0}, the implication

(f nonexpansive ∧ (A_{α}) ∧ (B_{K}) → ∥x_{n} − f(x_{n})∥ < ∥x^{∗} − f(x^{∗})∥ + ε)

is equivalent to a purely existential formula. The proof of (∗) only uses tools formalizable in EBA plus the principle PCM(∥x_{k} − f(x_{k})∥) (discussed in the introduction) applied to (∥x_{k} − f(x_{k})∥)_{k∈IN} and a complicated inequality due to [11]. This inequality can be treated just as another purely universal implicative premise and does therefore not increase the logical complexity of the theorem (nor is its proof needed to be analysed). Since, furthermore, the Hilbert cube [0, 1]^{IN} is a compact space, our general results discussed discussed in the introduction guarantee (at least for complete separable X and definable C)^{15} the existence of an effective bound for n which does not depend on (λ_{k}) directly but which may possibly depend on K, α, x, x^{∗}, f, ε and γ. This information on what type of result we should look for is a significant application of our logical approach to the specific proof of theorem 4.2 which would not have been visible without the reformulation of the theorem focusing on its logical form. We also know a-priori from our general logical meta-theorem, that a uniform bound on n which does not depend on x, x^{∗} ∈ C, γ > 0 and f is extractable if C is compact (and hence has bounded diameter). For the bound we actually extract, the dependence on x, x^{∗}, f, γ can already be eliminated as soon as we have an upper bound on the diameter d(C) of C. This stronger uniformity result is an a-postiori information we get for free just by examining the extracted bound (compare this with remark 4.4 and the discussion in the final section of this paper). Extraction of the bound: We now proceed to the actual extraction of the bound from the proof of theorem 4.2 which we present here in a usual mathematical style without following step by step a fixed proof theoretic procedure.

15The actually extracted bound will in fact turn out to be valid for arbitrary normed linear spaces X and convex subsets C ⊂ X. Note that the convexity assumption on C is purely universal.

Let x^{∗} ∈ C and define

(1) γ := ∥x^{∗} − f(x^{∗})∥.

Let furthermore ε > 0 and x ∈ C be arbitrary and let M ∈ IN be such that

(2) M ≥ \frac{1 + 2∥x − x^{∗}∥}{ε}.

Let δ > 0 be so small that

(3) δ exp(K(M + 1)) < 1,

where K ∈ IN satisfies

(4) ∀k ∈ IN(λ_{k} ≤ 1 − \frac{1}{K}).

Let α : IN × IN → IN be such that^{16}

(5) ∀i, n ∈ IN(n ≤ S_{i,α(i,n)} ≤ n + 1),

where

(6) S_{i,n} := ∑_{s=i}^{i+n−1} λ_{s}.

16Since λ_{k} ∈ [0, 1) this can always be achieved.

Consider the Krasnoselski-Mann iteration (x_{n})_{n∈IN} starting from x. By lemma 4.1.1), the sequence (∥x_{n} − f(x_{n})∥)_{n∈IN} ⊂ [0, ∥x − f(x)∥] is monotone decreasing and hence convergent. Thus there exists an i such that

(7) ∥x_{i} − f(x_{i})∥ − ∥x_{i+α(i,M)} − f(x_{i+α(i,M)})∥ ≤ δ.

Suppose that

(8) ∥x_{i} − f(x_{i})∥ ≥ γ + ε.

The proof in [4] uses the following inequality which is derived from a fundamental inequality due to [11] and which holds for all i, n ∈ IN

(9) S_{i,n} · ∥x_{i} − f(x_{i})∥ ≤ ∥x_{i} − x_{i+n}∥ + P_{i,n} · (∥x_{i} − f(x_{i})∥ − ∥x_{i+n} − f(x_{i+n})∥),

where

(10) P_{i,n} := ∏_{s=i}^{i+n−1} \frac{1}{1 − λ_{s}} .

As in [16] one shows that

(11) ∀i, n ∈ IN(P_{i,n} ≤ exp(K · S_{i,n})).

In [4](p.23), the following inequality is established ((x_{k}^{∗}) is the Krasnoselski-Mann iteration starting from x^{∗})

(12) ∥x_{i}^{∗} − x_{i+n}^{∗}∥ ≤ S_{i,n} · ∥x_{i}^{∗} − f(x_{i}^{∗})∥ ≤^{l.4.1.1)} S_{i,n} · ∥x^{∗} − f(x^{∗})∥.

Together with lemma 4.1.2) we obtain

(13) \{ \begin{matrix}S_{i,α(i,M)} · (γ + ε) ≤^{(8)} S_{i,α(i,M)} · ∥x_{i} − f(x_{i})∥ ≤^{(9,7)} ∥x_{i} − x_{i+α(i,M)}∥ + δP_{i,α(i,M)} \\ ≤ ∥x_{i} − x_{i}^{∗}∥ + ∥x_{i}^{∗} − x_{i+α(i,M)}^{∗}∥ + ∥x_{i+α(i,M)}^{∗} − x_{i+α(i,M)}∥ + δP_{i,α(i,M)} \\ ≤^{4.1.2)} 2∥x − x^{∗}∥ + ∥x_{i}^{∗} − x_{i+α(i,M)}^{∗}∥ + δP_{i,α(i,M)} \\ ≤^{(12)} 2∥x − x^{∗}∥ + S_{i,α(i,M)} · ∥x^{∗} − f(x^{∗})∥ + δP_{i,α(i,M)}. \end{matrix}

Hence

(14) \{ \begin{matrix}1 + 2∥x − x^{∗}∥ ≤^{(2)} M · ε ≤^{(5)} εS_{i,α(i,M)} \\ ≤^{(1)} S_{i,α(i,M)}(γ + ε − ∥x^{∗} − f(x^{∗})∥) ≤^{(13)} 2∥x − x^{∗}∥ + δP_{i,α(i,M)} \\ ≤^{(11)} 2∥x − x^{∗}∥ + δ exp(K · S_{i,α(i,M)}) \\ ≤^{(5)} 2∥x − x^{∗}∥ + δ exp(K(M + 1)) <^{(3)} 2∥x − x^{∗}∥ + 1, \end{matrix}

which is a contradiction. Therefore ∥x_{i} − f(x_{i})∥ < γ + ε. It remains to construct a function h(x, f, K, α, M) which is a bound i ≤ h(x, f, K, α, M) for i in (7): Define

α̃(i, M) := i + α(i, M)

and the m-times iteration α̂ of λi.α̃(i, M)

α̂(0, M) := α̃(0, M) and α̂(m + 1, M) := α̃(α̂(m, M), M).

It is clear that

(15) ∀i(α̂(i, M) ≤ α̂(i + 1, M)).

Claim:^{17}

∃i ≤ ⌈\frac{∥x − f(x)∥}{δ}⌉ − · 1(∥x_{_{α}(i,M)} − f(x_{_{α}(i,M)})∥ − ∥x_{_{α}(i+1,M)} − f(x_{_{α}(i+1,M)}∥ ≤ δ).

Proof of Claim: Let j := ⌈\frac{∥x−f(x)∥}{δ}⌉ − · 1 and suppose the claim is false. Then

∀i ≤ j(∥x_{_{α}(i,M)} − f(x_{_{α}(i,M)})∥ − ∥x_{_{α}(i+1,M)} − f(x_{_{α}(i+1,M)}∥ > δ).

Since by lemma 4.1.1) the sequence (∥x_{i} − f(x_{i})∥)_{i∈IN} is decreasing and – by (15) – λi.α̂(i, M) is monotone, we obtain

\begin{matrix}∥x_{_{α}(0,M)} − f(x_{_{α}(0,M)})∥ − ∥x_{_{α}(j+1,M)} − f(x_{_{α}(j+1,M)})∥ \\ > δ · (j + 1) ≥ ∥x − f(x)∥, \end{matrix}

which is a contradiction to the fact that ∀n ∈ IN(∥x_{n} − f(x_{n})∥ ∈ [0, ∥x − f(x)∥]) and finishes the proof of the claim. Using that

(16) ∀i(α̂(i + 1, M) = α̂(i, M) + α(α̂(i, M), M),

the claim yields

(17) \{ \begin{matrix}∃i ≤ ⌈\frac{∥x−f(x)∥}{δ}⌉ − · 1 \\ (∥x_{_{α}(i,M)} − f(x_{_{α}(i,M)})∥ − ∥x_{_{α}(i,M)+α(_{α}(i,M),M)} − f(x_{_{α}(i,M)+α(_{α}(i,M),M)}∥ ≤ δ). \end{matrix}

17n − · 1 := max(0, n − 1).

Hence – using again the monotonicity of λi.α̂(i, M) – a bound for i in (∗) is given by α̂(⌈(∥x − f(x)∥/δ)⌉ − · 1, M). Since we can put δ := \frac{1}{2 exp(K(M+1))} we obtain

h(x, f, K, α, M) := α̂(⌈2∥x − f(x)∥ exp(K(M + 1))⌉ − · 1, M)

with M ∈ IN such that

M ≥ \frac{1 + 2∥x − x^{∗}∥}{ε}

as bound for an i such that

∥x_{i} − f(x_{i})∥ < γ + ε

and therefore (using again lemma 4.1.1)

∀i ≥ h(x, f, K, α, M)(∥x_{i} − f(x_{i})∥ < γ + ε).

We now show that we can replace (5) by the more flexible requirement^{18}

(5)′ ∀i, n ∈ IN(α(i, n) ≤ α(i + 1, n) ∧ n ≤ S_{i,α(i,n)}).

Assume that α satisfies (5)′. Define

α^{∗}(i, n) := min m ∈ IN[n ≤ ∑_{s=i}^{i+m−1} λ_{s}].

Then

∀i, n ∈ IN(n ≤ S_{i,α^{∗}(i,n)} ≤ n + 1),

since λ_{s} ≤ 1. Hence by the logical analysis carried out so far we obtain the bound h(ε, x, x^{∗}, f, K, α^{∗}). In this bound, α^{∗} can be replaced by α since

h(ε, x, x^{∗}, f, K, α^{∗}) ≤ h(ε, x, x^{∗}, f, K, α),

which is a consequence of

∀i, n ∈ IN(α̂^{∗}(i, n) ≤ α̂(i, n)),

which can be proved by an easy induction on i. Put together we have established the following

α_{+}(i, n) := max_{j≤i}(α(j, n)).

18Note that the first conjunct can always be achieved without violating the second one by using

Theorem 4.5 Let (X, ∥ · ∥) be a normed linear space, C ⊆ X a non-empty convex subset and f : C → C a nonexpansive mapping. Let (λ_{k})_{k∈IN} be a sequence in [0, 1] which is divergent in sum and satisfies

∀k ∈ IN(λ_{k} ≤ 1 − \frac{1}{K})

for some K ∈ IN. Let α : IN × IN → IN be such that

∀i, n ∈ IN(α(i, n) ≤ α(i + 1, n)) and

∀i, n ∈ IN(n ≤ ∑_{s=i}^{i+α(i,n)−1} λ_{s}).

Let (x_{n})_{n∈IN} be the Krasnoselski-Mann iteration

x_{n+1} := (1 − λ_{n})x_{n} + λ_{n}f(x_{n}), x_{0} := x

starting from x ∈ C. Then the following holds

∀x, x^{∗} ∈ C∀ε > 0∀n ≥ h(ε, x, x^{∗}, f, K, α)(∥x_{n} − f(x_{n})∥ < ∥x^{∗} − f(x^{∗})∥ + ε),

where

h(ε, x, x^{∗}, f, K, α) := α̂(⌈2∥x − f(x)∥ · exp(K(M + 1))⌉ − · 1, M),
with M := ⌈\frac{1+2∥x−x^{∗}∥}{ε}⌉ and
α̂(0, M) := α̃(0, M), α̂(m + 1, M) := α̃(α̂(m, M), M) with
α̃(m, M) := m + α(m, M) (m ∈ IN)

(Instead of M we may use any upper bound IN ∋ M̃ ≥ \frac{1+2∥x−x^{∗}∥}{ε}). Likewise, we may resplace ∥x − f(x)∥ by any upper bound).

Corollary 4.6 Let (X, ∥ · ∥) be a normed linear space, C ⊆ X a non-empty convex subset with bounded diameter d(C) < ∞ and f : C → C a nonexpansive mapping. Let (λ_{k})_{k∈IN} be a sequence in [0, 1] which is divergent in sum and satisfies

∀k ∈ IN(λ_{k} ≤ 1 − \frac{1}{K})

for some K ∈ IN. Let α : IN × IN → IN be such that

∀i, n ∈ IN(α(i, n) ≤ α(i + 1, n)) and

∀i, n ∈ IN(n ≤ ∑_{s=i}^{i+α(i,n)−1} λ_{s}).

Let (x_{n})_{n∈IN} be the Krasnoselski-Mann iteration

x_{n+1} := (1 − λ_{n})x_{n} + λ_{n}f(x_{n}), x_{0} := x

starting from x ∈ C. Then the following holds

∀x ∈ C∀ε > 0∀n ≥ h(ε, d(C), K, α)(∥x_{n} − f(x_{n})∥ ≤ ε),

where

h(ε, d(C), K, α) := α̂(⌈2d(C) · exp(K(M + 1))⌉ − 1, M), with M := ⌈\frac{1+2d(C)}{ε}⌉ and

α̂(0, M) := α̃(0, M), α̂(m + 1, M) := α̃(α̂(m, M), M) with

α̃(m, M) := m + α(m, M) (m ∈ IN)

(Instead of M, d(C) we may use any upper bounds Q_{+}^{∗} ∋ d_{C} ≥ d(C) and IN ∋ M̃ ≥ \frac{1+2d_{C}}{ε}).

Proof: The corollary follows from theorem 4.5 and lemma 3.7 by noticing that ∥x − f(x)∥, ∥x − x^{∗}∥ ≤ d(C). □

Remark 4.7 The behaviour of the bound in corollary 4.6 w.r.t. d(C) can be improved as follows: if d(C) is different from 1 we renorm the space by the multiplicative factor \frac{1}{d(C)}. Then h(ε, 1, K, α) gives the rate of the asymptotic regularity w.r.t. this

new norm and hence h(\frac{ε}{d(C)}, 1, K, α) for the original norm. This result could have been obtained also directly from the proof of theorem 4.5 above by noticing that instead of ‘1 + 2∥x − x^{∗}∥’ in (2) we could have used ‘l + 2∥x − x^{∗}∥’ for any positive l (so in particular l := d(C)) and then taking δ := \frac{l}{2 exp(K(M+1))} to

satisfy (3) with l instead of 1 at the right-hand side.

Corollary 4.8 Let d, ε > 0, K ∈ IN and β : IN → IN an arbitrary function. Then there exists an n ∈ IN such that for any normed space X, any convex set C ⊆ X such that d(C) ≤ d, any nonexpansive function f : C → C, any sequence λ_{k} ∈

[0, 1 − \frac{1}{K}] satisfying n ≤ ∑_{s=0}^{β(n)} λ_{s} (for all n ∈ IN) and any starting point x_{0} ∈ C of the

corresponding Krasnoselski-Mann iteration the following holds

∀m ≥ n(∥x_{m} − f(x_{m})∥ < ε).

Proof: Follows immediately from corollary 4.6 noticing that if n ≤ ∑_{s=0}^{β(n)} λ_{s}, then also

n ≤ ∑_{s=i}^{i+α(i,n)−1} λ_{s}, where α(i, n) := β(n + i) − i + 1. But this implies n ≤ ∑_{s=i}^{i+α_{+}(i,n)−1} λ_{s},

where α_{+}(i, n) := max_{j≤i}(α(j, n)) satisfies α_{+}(i, n) ≤ α_{+}(i + 1, n). □

Remark 4.9 Using the reasoning from the proof of corollary 4.8 one can rewrite the bounds in theorem 4.5 and corollary 4.6 to depend on β : IN → IN satisfying

n ≤ ∑_{s=0}^{β(n)} λ_{s}

instead of α. We only have to replace α by β̆(i, n) := max_{j≤i}(β(n + j) − j + 1).

Corollary 4.10 Let (X, ∥ · ∥), C, f be as in corollary 4.6, k ∈ IN, k ≥ 2 and λ_{n} ∈ [\frac{1}{k}, 1 − \frac{1}{k}] for all n ∈ IN. Consider the Krasnoselski-Mann iteration x_{n+1} := (1 − λ_{n})x_{n} + λ_{n}f(x_{n}) starting from x_{0} := x ∈ C. Then the following holds:

∀x ∈ C∀ε > 0∀n ≥ g(ε, d(C))(∥x_{n} − f(x_{n})∥ ≤ ε),

where

g(ε, d(C)) := kM · ⌈2d(C) exp(k(M + 1))⌉ with M := ⌈\frac{1 + 2d(C)}{ε}⌉ .

Proof: We can put in corollary 4.6 α(i, M) := kM. One easily proves that α̂(i, M) := k(i + 1)M. The corollary now follows from corollary 4.6. □

5 Evaluation of the results of the case study

We have seen that there are interesting proofs in non-linear functional analysis (and specifically in fixed point theory) which fall under general proof theoretic results on the extractability of uniform bounds we had obtained in previous papers. We applied these results to essentially two proofs

1) A standard proof from [3] (from the year 1962)^{19} of the well-known Krasnoselski fixed point theorem.

2) A proof from [4] (which contains as a special case a proof from [11] from 1982) for a general result on the asymptotic behaviour of the Krasnoselski-Mann iteration in arbitrary normed spaces (generalizing a result from Ishikawa [16]).

Results on 1): Logical analysis of a proof from 1955/62 yielded uniform bounds together with an elementary verification for arbitrary bounded convex sets C. Under slightly less general conditions and with the use of the deep Browder-Göhde-Kirk fixed point theorem our bound in theorem 3.9 was obtained only in 1990 ([18]) (The compact case is due already to Krasnoselski). Moreover, a logical modification of the proof using PCM_{ar}^{H} (with g(n) = n + 1 as index function in PCM_{ar}^{H}(a_{n})) allowed to improve this bound under a further condition usually satisfied by moduli of uniform convexity (theorem 3.10). Applying this general bound to L_{p} (p ≥ 2) resulted in a polynomial bound of degree p (a result which for this special case was obtained in [18] by an ad hoc calculation). For X := IR and C := [0, 1] we even get a linear bound out of our general result (see also [18], p.192).

Results on 2): Logical analysis of the proof in [4] (resp. [11]) yielded the following results:

For the first time we obtain explicit bounds for Ishikawa’s result on the asymptotic behaviour of the general Krasnoselski-Mann iteration in arbitrary normed spaces X and for bounded sets C (corollary 4.6). Moreover, our bounds are uniform in the sense that they only depend on the error ε and an upper bound d_{C} of the diameter of C (and some data from the sequence of scalars λ_{k} used in defining the iteration) but not on the nonexpansive function f, the starting point x_{0} ∈ C of the iteration or other C-data. Only the non-effective existence of a bound independent of f and x_{0} was known before (see [11] where a non-trivial functional theoretic embedding is used to obtain this uniformity after ∥x_{k} − f(x_{k})∥ → 0 has been established by the proof we are analysing).^{20} In fact, [18] explicitly mentions the non-effectivity of all these results and states that ‘it seems unlikely that such estimates would be easy to obtain in general setting’ (p.191) and therefore only studies the special ‘tractable’ (p.191) case of uniformly convex spaces due to Krasnoselski. For bounds which, moreover, only depend on C via d_{C} (corollary 4.8) not even the ineffective existence was known so far and in fact still in [12] (p.101) conjectured as ‘unlikely’ to be true (incidentally by the same authors whose proof of ∥x_{k} − f(x_{k})∥ → 0 in [11] does yield such a bound by logical analysis!). Only in the special case of λ_{k} := λ ∈ (0, 1) being constant, a uniform (and in fact optimal quadratic) bound was recently discovered using computer aided proofs involving hypergeometric functions (see [1], where again the non-effectivity of all known proofs of the full Ishikawa result is stressed) and only for λ_{k} := \frac{1}{2} a classically proved result of that type has been obtained subsequently (see [2]). This result, of course, is numerically better than our exponential bound in corollary 4.10 when specialised to λ = \frac{1}{2}. However, as the authors concede, their extremely complicated method does not extend to the case of non-constant sequences (λ_{k}). ^{21} Our bound for the general case of unbounded C treated in [4] (theorem 4.5) is apparently all new.

19Krasnoselski’s original proof from 1955 is very similar to that as far as we can judge from the russian text.

References

[1] Baillon, J, Bruck, R.E., The rate of asymptotic regularity is 0(\frac{1}{\sqrt{n}}). Theory and applications of nonlinear operators of accretive and monotone type, Lecture Notes in Pure and Appl. Math. 178, pp. 51-81, Dekker, New York, 1996.

[2] Bruck, R.E., A simple proof that the rate of asymptotic regularity of (I + T)/2 is O(1/\sqrt{n}). Recent advances on metric fixed point theory (Seville, 1995), pp. 11–18, Ciencias, 48, Univ. Sevilla, Seville, 1996.

[3] Bonsall, F.F., Lectures on some fixed point theorems of functional analysis. Tata Institute of Fundamental Research. Bombay 1962.

20See [9] for a recent interesting application of this uniformity.

21Very recently, Kirk ([19]) obtained a new proof of the uniform (w.r.t. x_{0} and f) Ishikawa result for the special case λ_{k} = λ (again using a functional theoretic embedding) even in the more general setting of so-called directionally nonexansive mappings. It would be interesting to see what quantitative results a logical analysis of that proof would provide. We are grateful to Professor Kirk for bringing the work of Baillon and Bruck to our attention and for communicating to us his recent papers [9],[19].

[4] Borwein, J., Reich, S., Shafrir, I., Krasnoselski-Mann iterations in normed spaces. Canad. Math. Bull. 35, pp. 21-28 (1992).

[5] Browder, F.E., Nonexpansive nonlinear operators in a Banach space. Proc. Nat. Acad. Sci. U.S.A. 54, pp. 1041-1044 (1965).

[6] Clarkson, J.A., Uniformly convex spaces. Trans. Amer. Math. Soc. 40, pp. 396-414 (1936).

[7] Deimling, K., Nonlinear Functional Analysis. Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, xiv+450 pp., 1985.

[8] Edelstein, M., O’Brian, R.C., Nonexpansive mappings, asymptotic regularity and successive approximations. J. London Math. Soc. 17, pp. 547-554 (1978).

[9] Espinola, R., Kirk, W.A., Fixed points and approximated fixed points in product spaces. Preprint.

[10] Feferman, S., Kreisel’s ‘Unwinding Program’. In: P. Odifreddi (ed.), Kreiseliana: about and around Georg Kreisel, A.K. Peters, Wellesley Massachusetts, pp. 247-273 (1996).

[11] Goebel, K., Kirk, W.A., Iteration processes for nonexpansive mappings. In: Singh, S.P., Thomeier, S., Watson, B., eds., Topological Methods in Nonlinear Functional Analysis. Contemporary Mathematics 21, AMS, pp. 115-123 (1983).

[12] Goebel, K., Kirk, W.A., Topics in metric fixed point theory. Cambridge studies in advanced mathematics 28, Cambridge University Press 1990.

[13] Göhde, D., Zum Prinzip der kontraktiven Abbildung. Math. Nachrichten 30, pp. 251-258 (1965).

[14] Hanner, O., On the uniform convexity of L_{p} and l_{p}. Ark. Mat. 3, pp. 239-244 (1956).

[15] Henry, M.S., Schmidt, D., Continuity theorems for the product approximation operator. In: Law, A.G., Sahney, B.N. (eds.), Theory of Approximation with Applications, pp. 24-42, Academic Press, New York (1976).

[16] Ishikawa, S., Fixed points and iterations of a nonexpansive mapping in a Banach space. Proc. Amer. Math. Soc. 59, pp. 65-71 (1976).

[17] Kirk, W.A., A fixed point theorem for mappings which do not increase distances. Amer. Math. Monthly 72, pp. 1004-1006 (1965).

[18] Kirk, W.A., Martinez-Yanez, C., Approximate fixed points for nonexpansive mappings in uniformly convex spaces. Annales Polonici Mathematici 51, pp. 189-193 (1990).

[19] Kirk, W.A., Nonexpansive mappings and asymptotic regularity. To appear in: Nonlinear Analysis.

[20] Koethe, G., Topoplogische Lineare Räume. Springer-Verlag Berlin-Göttingen-Heidelberg, VI+456 pp., 1960.

[21] Kohlenbach, U., Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin’s proof for Chebycheff approximation. Ann. Pure Appl. Logic 64, pp. 27–94 (1993).

[22] Kohlenbach, U., New effective moduli of uniqueness and uniform a–priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory. Numer. Funct. Anal. and Optimiz. 14, pp. 581–606 (1993).

[23] Kohlenbach, U., Analysing proofs in analysis. In: W. Hodges, M. Hyland, C. Steinhorn, J. Truss, editors, Logic: from Foundations to Applications. European Logic Colloquium (Keele, 1993), pp. 225–260, Oxford University Press (1996).

[24] Kohlenbach, U., Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals. Arch. Math. Logic 36, pp. 31–71 (1996).

[25] Kohlenbach, U., Proof theory and computational analysis.

Electronic Notes in Theoretical Computer Science 13, Elsevier (http://www.elsevier.nl/locate/entcs/volume13.html), 34 pages (1998).

[26] Kohlenbach, U., Elimination of Skolem functions for monotone formulas in analysis. Arch. Math. Logic 37, pp. 363-390 (1998).

[27] Kohlenbach, U., Arithmetizing proofs in analysis. In: Larrazabal, J.M. et al. (eds.), Proceedings Logic Colloquium 96 (San Sebastian), Springer Lecture Notes in Logic 12, pp. 115–158 (1998).

[28] Kohlenbach, U., Things that can and things that can’t be done in PRA. Ann. Pure Appl. Logic 102, pp. 223-245 (2000).

[29] Kohlenbach, U., On the computational content of the Krasnoselski fixed point theorem. In preparation.

[30] Krasnoselski, M. A., Two remarks on the method of successive approximation. Usp. Math. Nauk (N.S.) 10, pp. 123-127 (1955) (Russian).

[31] Linz, Peter, A critique of numerical analysis. Bull. Amer. Math. Soc. 19, pp. 407-416 (1988).

[32] Luckhardt, H., Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. J. Symbolic Logic 54, pp. 234-263 (1989).

[33] Mann, W.R., Mean value methods in iteration. Proc. Amer. Math. Soc. 4, pp. 506-510 (1953).

[34] Reich, S., Shafrir, I., Nonexpansive iterations in hyperbolic spaces. Nonlinear Analysis, Theory, Methods and Applications 15, pp. 537-558 (1990).

[35] Schwichtenberg, H., Refined Program Extraction from Classical Proofs. To appear in: Proceedings of 1999 Marktobersdorf Summer School.

Recent BRICS Report Series Publications

RS-00-9 Ulrich Kohlenbach. Effective Uniform Bounds on the Krasnoselski-Mann Iteration. May 2000. 34 pp.

RS-00-8 Nabil H. Mustafa and Aleksandar Pekeč. Democratic Consensus and the Local Majority Rule. May 2000. 38 pp.

RS-00-7 Lars Arge and Jakob Pagter. I/O-Space Trade-Offs. April 2000. To appear in 7th Scandinavian Workshop on Algorithm Theory, SWAT ’98 Proceedings, LNCS, 2000.

RS-00-6 Ivan B. Damgård and Jesper Buus Nielsen. Improved Non-Committing Encryption Schemes based on a General Complexity Assumption. March 2000. 24 pp.

RS-00-5 Ivan B. Damgård and Mads J. Jurik. Efficient Protocols based on Probabilistic Encryption using Composite Degree Residue Classes. March 2000. 19 pp.

RS-00-4 Rasmus Pagh. A New Trade-off for Deterministic Dictionaries. February 2000.

RS-00-3 Fredrik Larsson, Paul Pettersson, and Wang Yi. On Memory-Block Traversal Problems in Model Checking Timed Systems. January 2000. 15 pp. Appears in Graf and Schwartzbach, editors, Tools and Algorithms for The Construction and Analysis of Systems: 6th International Conference, TACAS ’00 Proceedings, LNCS 1785, 2000, pages 127–141.

RS-00-2 Igor Walukiewicz. Local Logics for Traces. January 2000. 30 pp.

RS-00-1 Rune B. Lyngsø and Christian N. S. Pedersen. Pseudoknots in RNA Secondary Structures. January 2000. 15 pp. To appear in Fourth Annual International Conference on Computational Molecular Biology, RECOMB ’00 Proceedings, 2000.

RS-99-57 Peter D. Mosses. A Modular SOS for ML Concurrency Primitives. December 1999. 22 pp.

RS-99-56 Peter D. Mosses. A Modular SOS for Action Notation. December 1999. 39 pp. Full version of paper appearing in Mosses and Watt, editors, Second International Workshop on Action Semantics, AS ’99 Proceedings, BRICS Notes Series NS-99-3, 1999, pages 131–142.