This paper is part of a case study in proof mining applied to non-effective proofs in nonlinear functional analysis. More specifically, we are concerned with the fixed point theory of nonexpansive selfmappings f of convex sets C in normed spaces. We study Krasnoselski and more general so-called Krasnoselski-Mann iterations which converge to fixed points of f under certain compactness conditions. But, as we show, already for uniformly convex spaces in general no bound on the rate of convergence can be computed uniformly in f. However, the iterations yield even without any compactness assumption and for arbitrary normed spaces approximate fixed points of arbitrary quality for bounded C (asymptotic regularity, Ishikawa 1976). We apply proof theoretic techniques (developed in previous papers) to non-effective proofs of this regularity and extract effective uniform bounds (with elementary proofs) on the rate of the asymptotic regularity. We first consider the classical case of uniformly convex spaces which goes back to Krasnoselski (1955) and show how a logically motivated modification allows to obtain an improved bound. Moreover, we get a completely elementary proof for a result which was obtained in 1990 by Kirk and Martinez-Yanez only with the use of the deep Browder-Göhde-Kirk fixed point theorem. In section 4 we report on new results () we established for the general case of arbitrary normed spaces including new quantitative versions of Ishikawa's theorem (for bounded C) and its extension due to Borwein, Reich and Shafrir (1992) to unbounded sets C. Our explicit bounds also imply new qualitative results concerning the independence of the rate of asymptotic regularity from various data.
Cca 2000 : Computability and Complexity in Analysis: Computability and Complexity in Analysis. International Workshop No4, Swansea , Royaume-uni (17/09/2000), 2001, p. 119-145
Computability; Theorem proving; Contraction; Convex set; Fixed point theorem
Main Research Area:
CCA 2000 : computability and complexity in analysis;Computability and complexity in analysis. International workshop