Search

We show that the asymptotic regularity and the strong convergence of the modified Halpern iteration due to T.-H. Kim and H.-K. Xu and studied further by A. Cuntavenapit and B. Panyanak and the Tikhonov–Mann iteration introduced by H. Cheval and L. Leuştean as a generalization of an iteration due to Y. Yao et al. that has recently been studied by Boţ et al. can be reduced to each other in general geodesic settings. This, in particular, gives a new proof of the convergence result in Boţ et al. together with a generalization from Hilbert to CAT(0) spaces. Moreover, quantitative rates of asymptotic regularity and metastability due to K. Schade and U. Kohlenbach can be adapted and transformed into rates for the Tikhonov–Mann iteration corresponding to recent quantitative results on the latter of H. Cheval, L. Leuştean and B. Dinis, P. Pinto, respectively. A transformation in the converse direction is also possible. We also obtain rates of asymptotic regularity of order O(1/n) for both the modified Halpern (and so in particular for the Halpern iteration) and the Tikhonov–Mann iteration in a general geodesic setting for a special choice of scalars.

We develop a general proof-theoretic framework for various classes of set-valued operators, including maximally as well as cyclically monotone and rectangular operators and we discuss a treatment for sums of set-valued operators A , B in that context such that all of the previous fits into logical metatheorems on bound extractions. In particular, we introduce quantitative forms for A being (weakly) uniformly rectangular with witnessing moduli. Based on this, we give quantitative forms of the Brezis–Haraux theorem that use such moduli as input. It turns out that a modulus for weak uniform rectangularity, which can be extracted even from non-effective proofs of rectangularity, is sufficient while the bound gets simpler in the case of a modulus for A being uniform rectangular which can be extracted from semi-constructive proofs. We use our results to explain recent proof minings in the context of Bauschke’s solution to the zero displacement conjecture and its extensions to other classes of functions than metric projections as instances of logical metatheorems. This article is part of the theme issue ‘Modern perspectives in Proof Theory’.

In this note we show that proof-theoretic uniform boundedness or bounded collection principles which allow one to formalize certain instances of countable Heine–Borel compactness in proofs using abstract metric structures must be carefully distinguished from an unrestricted use of countable Heine–Borel compactness.

In a recent paper, Bauschke et al. study $$\rho $$ ρ -comonotonicity as a generalized notion of monotonicity of set-valued operators A in Hilbert space and characterize this condition on A in terms of the averagedness of its resolvent $$J_A.$$ J A . In this note we show that this result makes it possible to adapt many proofs of properties of the proximal point algorithm PPA and its strongly convergent Halpern-type variant HPPA to this more general class of operators. This also applies to quantitative results on the rates of convergence or metastability (in the sense of T. Tao). E.g. using this approach we get a simple proof for the convergence of the PPA in the boundedly compact case for $$\rho $$ ρ -comonotone operators and obtain an effective rate of metastability. If A has a modulus of regularity w.r.t. $$zer\, A$$ z e r A we also get a rate of convergence to some zero of A even without any compactness assumption. We also study a Halpern-type variant HPPA of the PPA for $$\rho $$ ρ -comonotone operators, prove its strong convergence (without any compactness or regularity assumption) and give a rate of metastability.

In this paper we analyze, based on an interplay between ideas and techniques from logic and geometric analysis, a pursuit-evasion game. More precisely, we focus on a uniform betweenness property and use it in the study of a discrete lion and man game with an $\varepsilon$-capture criterion. In particular, we prove that in uniformly convex bounded domains the lion always wins and, using ideas stemming from proof mining, we extract a uniform rate of convergence for the successive distances between the lion and the man. As a byproduct of our analysis, we study the relation among different convexity properties in the setting of geodesic spaces., Change of title. Minor revision

We extract quantitative information (specifically, a rate of metastability in the sense of Terence Tao) from a proof due to Kazuo Kobayasi and Isao Miyadera, which shows strong convergence for Cesàro means of non-expansive maps on Banach spaces.

In this paper we introduce the concept of modulus of regularity as a tool to analyze the speed of convergence, including the linear convergence and finite termination, for classes of Fejer monotone sequences which appear in fixed point theory, monotone operator theory, and convex optimization. This concept allows for a unified approach to several notions such as weak sharp minima, error bounds, metric subregularity, Holder regularity, etc., as well as to obtain rates of convergence for Picard iterates, the Mann algorithm, the proximal point algorithm and the cyclic projection method. As a byproduct we obtain a quantitative version of the well-known fact that for a convex lower semi-continuous function the set of minimizers coincides with the set of zeros of its subdifferential and the set of fixed points of its resolvent.

In the setting of hyperbolic spaces, we show that the convergence of Browder-type sequences and Halpern iterations respectively entail the convergence of their viscosity version with a Rakotch map. We also show that the convergence of a hybrid viscosity version of the Krasnoselskii-Mann iteration follows from the convergence of the Browder type sequence. Our results follow from proof-theoretic techniques (proof mining). From an analysis of theorems due to T. Suzuki, we extract a transformation of rates for the original Browder type and Halpern iterations into rates for the corresponding viscosity versions. We show that these transformations can be applied to earlier quantitative studies of these iterations. From an analysis of a theorem due to H.-K. Xu, N. Altwaijry and S. Chebbi, we obtain similar results. Finally, in uniformly convex Banach spaces we study a strong notion of accretive operator due to Brezis and Sibony and extract an uniform modulus of uniqueness for the property of being a zero point. In this context, we show that it is possible to obtain Cauchy rates for the Browder type and the Halpern iterations (and hence also for their viscosity versions).

We use techniques originating from the subdiscipline of mathematical logic called `proof mining' to provide rates of metastability and - under a metric regularity assumption - rates of convergence for a subgradient-type algorithm solving the equilibrium problem in convex optimization over fixed-point sets of firmly nonexpansive mappings. The algorithm is due to H. Iiduka and I. Yamada who in 2009 gave a noneffective proof of its convergence. This case study illustrates the applicability of the logic-based abstract quantitative analysis of general forms of Fej\'er monotonicity as given by the second author in previous papers., Comment: 14 pages

We investigate two weak fragments of the double negation shift schema, which are motivated, respectively, from Spector’s consistency proof of ACA0 and from the negative translation of RCA0, as well as double negated variants of logical principles. Their interrelations over both intuitionistic arithmetic and analysis are completely solved.

This paper provides an explicit polynomial rate of asymptotic regularity for (in general inconsistent) feasibility problems in Hilbert space. In particular, we give a quantitative version of Bauschke’s solution of the zero displacement problem as well as of various generalizations of this problem. The results in this paper have been obtained by applying a general proof-theoretic method for the extraction of effective bounds from proofs due to the author (‘proof mining’) to Bauschke’s proof.

Starting in 2005, general logical metatheorems have been developed that guarantee the extractability of uniform effective bounds from large classes of proofs of theorems that involve abstract metric structures X. In this paper we adapt this to the class of CAT\((\kappa \))-spaces X for \(\kappa >0\) and establish a new metatheorem that explains specific bound extractions that recently have been achieved in this context as instances of a general logical phenomenon.

This paper studies proofs of strong convergence of various iterative algorithms for computing the unique zeros of set-valued accretive operators that also satisfy some weak form of uniform accretivity at zero. More precisely, we extract explicit rates of convergence from these proofs which depend on a modulus of uniform accretivity at zero, a concept first introduced by A. Koutsoukou-Argyraki and the first author in 2015. Our highly modular approach, which is inspired by the logic-based proof mining paradigm, also establishes that a number of seemingly unrelated convergence proofs in the literature are actually instances of a common pattern.

We give explicit rates of asymptotic regularity for iterations of strongly nonexpansive mappings T in general Banach spaces as well as rates of metastability (in the sense of Tao) in the context of uniformly convex Banach spaces when T is odd. This, in particular, applies to linear norm-one projections as well as to sunny nonexpansive retractions. The asymptotic regularity results even hold for strongly quasi-nonexpansive mappings (in the sense of Bruck), the addition of error terms and very general metric settings. In particular, we get the first quantitative results on iterations (with errors) of compositions of metric projections in CAT(ĸ)-spaces (ĸ > 0). Under an additional compactness assumption we obtain, moreover, a rate of metastability for the strong convergence of such iterations.

In this paper we show that normed structures which can be axiomatized in positive bounded logic (in the sense of Henson and Iovino) admit proof-theoretic metatheorems (as developed by the second author since 2005) on the extractability of explicit uniform bounds from proofs in the respective theories. We apply this to design such metatheorems for abstract Banach lattices, L p - and C ( K ) -spaces as well as bands in L p ( L q ) -Bochner spaces. We also show that a proof-theoretic uniform boundedness principle can serve in many ways as a substitute for the model-theoretic use of ultrapowers of Banach spaces.

We give explicit bounds on the computation of approximate common fixed points of one-parameter strongly continuous semigroups of nonexpansive mappings on a subset C of a general Banach space. Moreover, we provide the first explicit and highly uniform rate of convergence for an iterative procedure to compute such points for convex C. Our results are obtained by a logical analysis of the proof (proof mining) of a theorem by T. Suzuki.

We use techniques of proof mining to extract a uniform rate of metastability (in the sense of Tao) for the strong convergence of approximants to fixed points of uniformly continuous pseudocontractive mappings in Banach spaces which are uniformly convex and uniformly smooth, i.e. a slightly restricted form of the classical result of Reich. This is made possible by the existence of a modulus of uniqueness specific to uniformly convex Banach spaces and by the arithmetization of the use of the limit superior. The metastable convergence can thus be proved in a system which has the same provably total functions as first-order arithmetic and therefore one may interpret the resulting proof in Gödel’s system [Formula: see text] of higher-type functionals. The witness so obtained is then majorized (in the sense of Howard) in order to produce the final bound, which is shown to be definable in the subsystem [Formula: see text]. This piece of information is further used to obtain rates of metastability to results which were previously only analyzed from the point of view of proof mining in the context of Hilbert spaces, i.e. the convergence of the iterative schemas of Halpern and Bruck.

In this note we show that over a strong (semi-)intuitionistic base theory, the recursive comprehension principle $${\Delta^0_1}$$Δ10 -CA does not imply the disjunctive Markov principle MP$${^{\vee}}$$?.

Along the line of Hirst-Mummert [9] and Dorais [4], we analyze the relationship between the classical provability of uniform versions Uni(S) of Π2-statements S with respect to higher order reverse mathematics and the intuitionistic provability of S. Our main theorem states that (in particular) for every Π2-statement S of some syntactical form, if its uniform version derives the uniform variant of over a classical system of arithmetic in all finite types with weak extensionality, then S is not provable in strong semi-intuitionistic systems including bar induction in all finite types but also nonconstructive principles such as Kőnig's lemma and uniform weak Kőnig's lemma . Our result is applicable to many mathematical principles whose sequential versions imply .

We extract rates of convergence and rates of metastability (in the sense of Tao) for convergence results regarding abstract Cauchy problems generated by ϕ-accretive at zero operators A : D ( A ) ( ⊆ X ) → 2 X where X is a real Banach space, proved in [8] , by proof-theoretic analysis of the proofs in [8] and having assumed a new, stronger notion of uniform accretivity at zero, yielding a new notion of modulus of accretivity. We compute the rate of metastability for the convergence of the solution of the abstract Cauchy problem generated by a uniformly accretive at zero operator to the unique zero of A via proof mining based on a result by the first author. Finally, we apply our results to a special class of Cauchy problems considered in [8] . This work is the first application of proof mining to the theory of partial differential equations.

This paper provides a quantitative version of the classical image recovery problem to find an ϵ -approximate solution of the problem. The rate of asymptotic regularity of the iteration schemas, connected with the problem of image recovery, coincides with the existing optimal and quadratic bound for Krasnoselskii–Mann iterations. We then provide explicit effective and uniform bounds on the approximate fixed points of the mappings under consideration to be an approximate solution of the image recovery problem up to a uniform change from ϵ to δ ( ϵ ) . When combined, these results provide algorithms with explicit rates of convergence for the recovery of an ϵ -perturbation of the original image in different settings.

The workshop "Mathematical Logic: Proof Theory, Construc- tive Mathematics" was centered around proof-theoretic aspects of current mathematics, constructive mathematics and logical aspects of computational complexity.

This paper discusses what kind of quantitative information one can extract under which circumstances from proofs of convergence statements in analysis. We show that from proofs using only a limited amount of the law-of-excluded-middle, one can extract functionals ( B , L ) , where L is a learning procedure for a rate of convergence which succeeds after at most B ( a ) -many mind changes. This ( B , L ) -learnability provides quantitative information strictly in between a full rate of convergence (obtainable in general only from semi-constructive proofs) and a rate of metastability in the sense of Tao (extractable also from classical proofs). In fact, it corresponds to rates of metastability of a particular simple form. Moreover, if a certain gap condition is satisfied, then B and L yield a bound on the number of possible fluctuations. We explain recent applications of proof mining to ergodic theory in terms of these results.

We give a quantitative version of the strong convergence of Bruck's iteration schema for Lipschitzian pseudocontractions in Hilbert space.

The purpose of this paper is to extract an explicit effective and uniform bound on the rate of asymptotic regularity of an iteration schema involving a finite family of nonexpansive mappings. The results presented in this paper contribute to the general project of proof mining as developed by the second author as well as generalize and improve various classical and corresponding quantitative results in the current literature. More precisely, we give a rate of asymptotic regularity of an iteration schema due to Kuhfittig for finitely many nonexpansive mappings in the context of uniformly convex hyperbolic spaces. The rate only depends on an upper bound on the distance between the starting point and some common fixed point, a lower bound 1 / N ≤ λ n ( 1 − λ n ) , the error ϵ > 0 and a modulus η of uniform convexity.

This paper provides an effective uniform rate of metastability (in the sense of Tao) on the strong convergence of Halpern iterations of nonexpansive mappings in CAT(0) spaces. The extraction of this rate from an ineffective proof due to Saejung is an instance of the general proof mining program which uses tools from mathematical logic to uncover hidden computational content from proofs. This methodology is applied here for the first time to a proof that uses Banach limits and hence makes a substantial reference to the axiom of choice., Comment: some typos corrected

In this paper, we use techniques which originate from proof mining to give rates of asymptotic regularity and metastability for a sequence associated to the composition of two firmly nonexpansive mappings. German Science Foundation Dirección General de Enseñanza Superior

In recent years, proof theoretic transformations (so-called proof interpretations) that are based on extensions of monotone forms of Godel’s famous functional (‘Dialectica’) interpretation have been used systematically to extract new content from proofs in abstract nonlinear analysis. This content consists both in effective quantitative bounds as well as in qualitative uniformity results. One of the main ineffective tools in abstract functional analysis is the use of sequential forms of weak compactness. As we recently verified, the sequential form of weak compactness for bounded closed and convex subsets of an abstract (not necessarily separable) Hilbert space can be carried out in suitable formal systems that are covered by existing metatheorems developed in the course of the proof mining program. In particular, it follows that the monotone functional interpretation of this weak compactness principle can be realized by a functional Ω ∗ definable from bar recursion (in the sense of Spector) of lowest type. While a case study on the analysis of strong convergence results (due to Browder and Wittmann resp.) that are based on weak compactness indicates that the use of the latter seems to be eliminable, things apparently are different for weak convergence theorems such as the famous Baillon nonlinear ergodic theorem. For this theorem we recently extracted an explicit bound on a metastable (in the sense of T. Tao) version of this theorem that is primitive recursive relative to (a somewhat restricted form of) Ω ∗ . In the current paper we for the first time give the construction of Ω ∗ (in the form needed for the unwinding of Baillon’s theorem). As a corollary to the fine analysis of the use of bar recursion in this construction we obtain that Ω ∗ elevates arguments in T n at most to resulting functionals in T n + 2 (here T n is the fragment of Godel’s T with primitive recursion restricted to the type level n ). In particular, one can conclude from this that our bound on Baillon’s theorem is at least definable in T 4 .

This paper gives an explicit and effective rate of convergence for an asymptotic regularity result ‖ T x n − x n ‖ → 0 due to Chidume and Zegeye in 2004 [14] where ( x n ) is a certain perturbed Krasnoselski–Mann iteration schema for Lipschitz pseudocontractive self-mappings T of closed and convex subsets of a real Banach space. We also give a qualitative strengthening of the theorem by Chidume and Zegeye, by weakening the assumption of the existence of a fixed point. For the bounded case, our bound is polynomial in the data involved.

We give quantitative versions of strong convergence results due to Baillon, Bruck and Reich for iterations of nonexpansive odd (and more general) operators in uniformly convex Banach spaces.

We prove a result relating the author’s monotone functional interpretation to the bounded functional interpretation due to Ferreira and Oliva. More precisely we show that (over model of majorizable functionals) largely a solution for the bounded interpretation also is a solution for monotone functional interpretation although the latter uses the existence of an underlying precise witness. This makes it possible to focus on the extraction of bounds (as in the bounded interpretation) while using the conceptual benet of having precise realizers at the same time without having to construct them.

This paper is another case study in the program of logically analyzing proofs to extract new (typically effective) information (‘proof mining’). We extract explicit uniform rates of metastability (in the sense of T. Tao) from two ineffective proofs of a classical theorem of F.E. Browder on the convergence of approximants to fixed points of nonexpansive mappings as well as from a proof of a theorem of R. Wittmann which can be viewed as a nonlinear extension of the mean ergodic theorem. The first rate is extracted from Browder's original proof that is based on an application of weak sequential compactness (in addition to a projection argument). Wittmann's proof follows a similar line of reasoning and we adapt our analysis of Browder's proof to get a quantitative version of Wittmann's theorem as well. In both cases one also obtains totally elementary proofs (even for the strengthened quantitative forms) of these theorems that neither use weak compactness nor the existence of projections anymore. In this way, the present article also discusses general features of extracting effective information from proofs based on weak compactness. We then extract another rate of metastability (of similar nature) from an alternative proof of Browder's theorem essentially due to Halpern that already avoids any use of weak compactness. The paper is concluded by general remarks concerning the logical analysis of proofs based on weak compactness as well as a quantitative form of the so-called demiclosedness principle. In a subsequent paper these results will be utilized in a quantitative analysis of Baillon's nonlinear ergodic theorem.