General logical metatheorems for functional analysis

Gerhardy, Philipp; Kohlenbach, Ulrich

doi:10.1090/S0002-9947-07-04429-7

General logical metatheorems for functional analysis
HTML articles powered by AMS MathViewer

by Philipp Gerhardy and Ulrich Kohlenbach PDF

Trans. Amer. Math. Soc. 360 (2008), 2615-2660 Request permission

Abstract:

In this paper we prove general logical metatheorems which state that for large classes of theorems and proofs in (nonlinear) functional analysis it is possible to extract from the proofs effective bounds which depend only on very sparse local bounds on certain parameters. This means that the bounds are uniform for all parameters meeting these weak local boundedness conditions. The results vastly generalize related theorems due to the second author where the global boundedness of the underlying metric space (resp. a convex subset of a normed space) was assumed. Our results treat general classes of spaces such as metric, hyperbolic, CAT(0), normed, uniformly convex and inner product spaces and classes of functions such as nonexpansive, Hölder-Lipschitz, uniformly continuous, bounded and weakly quasi-nonexpansive ones. We give several applications in the area of metric fixed point theory. In particular, we show that the uniformities observed in a number of recently found effective bounds (by proof theoretic analysis) can be seen as instances of our general logical results.

References

Marc Bezem, Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals, J. Symbolic Logic 50 (1985), no. 3, 652–660. MR 805674, DOI 10.2307/2274319
Jonathan Borwein, Simeon Reich, and Itai Shafrir, Krasnosel′ski-Mann iterations in normed spaces, Canad. Math. Bull. 35 (1992), no. 1, 21–28. MR 1157459, DOI 10.4153/CMB-1992-003-0
Martin R. Bridson and André Haefliger, Metric spaces of non-positive curvature, Grundlehren der mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences], vol. 319, Springer-Verlag, Berlin, 1999. MR 1744486, DOI 10.1007/978-3-662-12494-9
F. Bruhat and J. Tits, Groupes réductifs sur un corps local, Inst. Hautes Études Sci. Publ. Math. 41 (1972), 5–251 (French). MR 327923, DOI 10.1007/BF02715544
C. E. Chidume, On the approximation of fixed points of nonexpansive mappings, Houston J. Math. 7 (1981), no. 3, 345–355. MR 640975
W. G. Dotson Jr., On the Mann iterative process, Trans. Amer. Math. Soc. 149 (1970), 65–73. MR 257828, DOI 10.1090/S0002-9947-1970-0257828-6
Michael Edelstein and Richard C. O’Brien, Nonexpansive mappings, asymptotic regularity and successive approximations, J. London Math. Soc. (2) 17 (1978), no. 3, 547–554. MR 500642, DOI 10.1112/jlms/s2-17.3.547
J. Garcia-Falset, E. Llorens-Fuster, and S. Prus, The fixed point property for mappings admitting a center, Nonlinear Analysis 66 (2007), 1257–1274.
Philipp Gerhardy and Ulrich Kohlenbach, Strongly uniform bounds from semi-constructive proofs, Ann. Pure Appl. Logic 141 (2006), no. 1-2, 89–107. MR 2229932, DOI 10.1016/j.apal.2005.10.003
Kurt Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica 12 (1958), 280–287 (German, with English summary). MR 102482, DOI 10.1111/j.1746-8361.1958.tb01464.x
Kazimierz Goebel and W. A. Kirk, Iteration processes for nonexpansive mappings, Topological methods in nonlinear functional analysis (Toronto, Ont., 1982) Contemp. Math., vol. 21, Amer. Math. Soc., Providence, RI, 1983, pp. 115–123. MR 729507, DOI 10.1090/conm/021/729507
W. A. Howard, Appendix: Hereditarily majorizable function of finite type, Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Math., Vol. 344, Springer, Berlin, 1973, pp. 454–461. MR 0469712
Shiro Ishikawa, Fixed points and iteration of a nonexpansive mapping in a Banach space, Proc. Amer. Math. Soc. 59 (1976), no. 1, 65–71. MR 412909, DOI 10.1090/S0002-9939-1976-0412909-X
W. A. Kirk, Krasnosel′skiĭ’s iteration process in hyperbolic space, Numer. Funct. Anal. Optim. 4 (1981/82), no. 4, 371–381. MR 673318, DOI 10.1080/01630568208816123
W. A. Kirk, Nonexpansive mappings and asymptotic regularity, Nonlinear Anal. 40 (2000), no. 1-8, Ser. A: Theory Methods, 323–332. Lakshmikantham’s legacy: a tribute on his 75th birthday. MR 1768416, DOI 10.1016/S0362-546X(00)85019-1
S. C. Kleene, Recursive functionals and quantifiers of finite types. I, Trans. Amer. Math. Soc. 91 (1959), 1–52. MR 102480, DOI 10.1090/S0002-9947-1959-0102480-9
Ulrich Kohlenbach, A logical uniform boundedness principle for abstract metric and hyperbolic spaces, Proceedings of the 13th Workshop on Logic, Language, Information and Computation (WoLLIC 2006), Electron. Notes Theor. Comput. Sci., vol. 165, Elsevier Sci. B. V., Amsterdam, 2006, pp. 81–93. MR 2321765, DOI 10.1016/j.entcs.2006.05.038
—, Effective uniform bounds from proofs in abstract functional analysis, CiE 2005. New Computational Paradigms: Changing Conceptions of What is Computable (B. Cooper, B. Loewe, and A. Sorbi, eds.), Springer Publisher, To appear.
Ulrich Kohlenbach, Effective moduli from ineffective uniqueness proofs. An unwinding of de la Vallée Poussin’s proof for Chebycheff approximation, Ann. Pure Appl. Logic 64 (1993), no. 1, 27–94. MR 1241250, DOI 10.1016/0168-0072(93)90213-W
Ulrich Kohlenbach, Arithmetizing proofs in analysis, Logic Colloquium ’96 (San Sebastián), Lecture Notes Logic, vol. 12, Springer, Berlin, 1998, pp. 115–158. MR 1674949, DOI 10.1007/978-3-662-22110-5_{5}
Ulrich Kohlenbach, A quantitative version of a theorem due to Borwein-Reich-Shafrir, Numer. Funct. Anal. Optim. 22 (2001), no. 5-6, 641–656. MR 1849571, DOI 10.1081/NFA-100105311
Ulrich Kohlenbach, On the computational content of the Krasnoselski and Ishikawa fixed point theorems, Computability and complexity in analysis (Swansea, 2000) Lecture Notes in Comput. Sci., vol. 2064, Springer, Berlin, 2001, pp. 119–145. MR 1893075, DOI 10.1007/3-540-45335-0_{9}
Ulrich Kohlenbach, Uniform asymptotic regularity for Mann iterates, J. Math. Anal. Appl. 279 (2003), no. 2, 531–544. MR 1974043, DOI 10.1016/S0022-247X(03)00028-3
Ulrich Kohlenbach, Some computational aspects of metric fixed-point theory, Nonlinear Anal. 61 (2005), no. 5, 823–837. MR 2130066, DOI 10.1016/j.na.2005.01.075
Ulrich Kohlenbach, Some logical metatheorems with applications in functional analysis, Trans. Amer. Math. Soc. 357 (2005), no. 1, 89–128. MR 2098088, DOI 10.1090/S0002-9947-04-03515-9
Ulrich Kohlenbach and Branimir Lambov, Bounds on iterations of asymptotically quasi-nonexpansive mappings, International Conference on Fixed Point Theory and Applications, Yokohama Publ., Yokohama, 2004, pp. 143–172. MR 2144170
U. Kohlenbach and L. Leuştean, The approximate fixed point property in product spaces, Nonlinear Analysis 66 (2007), 806–818.
Ulrich Kohlenbach and Laurenţiu Leuştean, Mann iterates of directionally nonexpansive mappings in hyperbolic spaces, Abstr. Appl. Anal. 8 (2003), 449–477. MR 1983075, DOI 10.1155/S1085337503212021
U. Kohlenbach and P. Oliva, Proof mining: a systematic way of analyzing proofs in mathematics, Tr. Mat. Inst. Steklova 242 (2003), no. Mat. Logika i Algebra, 147–175; English transl., Proc. Steklov Inst. Math. 3(242) (2003), 136–164. MR 2054493
M. A. Krasnosel′skiĭ, Two remarks on the method of successive approximations, Uspehi Mat. Nauk (N.S.) 10 (1955), no. 1(63), 123–127 (Russian). MR 0068119
L. Leustean, A quadratic rate of asymptotic regularity for CAT(0)-spaces, J. Math. Anal. Appl. 325 (2007), no. 1, 386–399. MR 2273533, DOI 10.1016/j.jmaa.2006.01.081
—, Proof mining in R-trees and hyperbolic spaces, Electronic Notes in Theoretical Computer Science 165 (2006), 95–106.
Horst Luckhardt, Extensional Gödel functional interpretation. A consistency proof of classical analysis, Lecture Notes in Mathematics, Vol. 306, Springer-Verlag, Berlin-New York, 1973. MR 0337512, DOI 10.1007/BFb0060871
Hilton Vieira Machado, A characterization of convex subsets of normed spaces, K\B{o}dai Math. Sem. Rep. 25 (1973), 307–320. MR 326359
W. Robert Mann, Mean value methods in iteration, Proc. Amer. Math. Soc. 4 (1953), 506–510. MR 54846, DOI 10.1090/S0002-9939-1953-0054846-3
Anthony G. O’Farrell, When uniformly-continuous implies bounded, Irish Math. Soc. Bull. 53 (2004), 53–56. MR 2117500
Simeon Reich and Itai Shafrir, Nonexpansive iterations in hyperbolic spaces, Nonlinear Anal. 15 (1990), no. 6, 537–558. MR 1072312, DOI 10.1016/0362-546X(90)90058-O
Itai Shafrir, The approximate fixed point property in Banach and hyperbolic spaces, Israel J. Math. 71 (1990), no. 2, 211–223. MR 1088815, DOI 10.1007/BF02811885
Brailey Sims, Examples of fixed point free mappings, Handbook of metric fixed point theory, Kluwer Acad. Publ., Dordrecht, 2001, pp. 35–48. MR 1904273
Clifford Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, Proc. Sympos. Pure Math., Vol. V, American Mathematical Society, Providence, R.I., 1962, pp. 1–27. MR 0154801
Wataru Takahashi, A convexity in metric space and nonexpansive mappings. I, K\B{o}dai Math. Sem. Rep. 22 (1970), 142–149. MR 267565