Extraction of effective uniform bounds from proofs based on sequential compactness via logical analysis

点击翻译按钮获取中文摘要

During the last 20 years an applied form of proof theory (``proof mining'') has emerged as a new area of mathematical logic. Here the focus is to use proof-theoretic transformations to extract new data such as effective bounds from concrete i(typically neffective) proofs in various areas of mathematics. Most systematically, this has resulted in many applications in nonlinear analysis (e.g. in metric fixed point theory as well as in ergodic theory). During the project KO 1737/5-1 the focus has been on the analysis of proofs that use strong as well as weak sequential compactness. In this application for a continuation of this project we will treat strong convergence results that have been established also with the use of principles such as Banach limits, ultraproducts, ultralimits and the Loeb measure, i.e. principles which involve the axiom of choice. W.r.t. Banach limits first surprising results have been established already during the past months. Many questions, however, are left open. In particular, this is the case for the extraction of a rate of metastability (in the sense of Tao) for the strong convergence of the resolvent of nonexpansive and - more generally - accretive operators in uniformly smooth Banach spaces from a proof due to Bruck and Reich which uses both weak compactness as well as Banach limits. Taken together with results obtained already during this project this would immediately yield rates of metastability for a nonlinear ergodic theorem due to Shioji and Takahashi as well for an iteration scheme due to Bruck for pseudocontrations proved to converge by Chidume and Zegeye). It is known that mos of the convergence results treated so far in this project, full effective rates of convergence do not exist and so one usually aims at weaker effective bounds on metastability (which - ineffectively - is equivalent to convergence) which are guaranteed to exist by proof-theoretic results of the applicant. Very recently, Avigad and Rute observed that in a particular case treated by us, a stronger effective and uniform bound on the number of so-called epsilon-fluctuations is possible. We intend to investigate whether this is a more general phenomenon which can be accounted for in logical terms.During the project so far new methods have been developed for extracting uniform bounds from proofs that make use of a nonprincipal ultrafilter U. However, these methods need to be incorporated into the general logical machinery of the logical metatheorems to apply to proofs using the ultrapower X/U of sbtract spaces X (frequently used in nonlinear analysis).Such extensions are also needed for new methods developed in the course of the project which guarantee the extractability of primitive recursive bounds from proof that use the Bolzano-Weierstrass principle in the form sating the existence of a Cauchy-subsequence without a rate of convergence (which is known to be impossible when such a rate is used).