Searcharxiv⌕ Search

arXiv subjects

Ulrich Kohlenbach

Publications and source records attributed to Ulrich Kohlenbach.

At least 19 recordsLinked to original sources
arXiv2026

Logical Metatheorems for Abstract Spaces axiomatized in Positive Bounded Logic II: Metric spaces and the model-theoretic uniformity principle

We extend the proof-theoretic treatment of uniform bound extraction from normed structures axiomatized in positive bounded logic [Advances in Mathematics, 290:503-551, 2016] (as developed for the model theory of Banach spaces) to the more general setting of abstract metric structures, including discrete structures viewed as classical first-order models. In particular, we establish uniform bound extraction theorems for our generalized framework for $\forall\exists$-sentences whose matrix is the negation of (an embedding of) a formula in positive bounded logic, whose proofs use saturation. In this way, we provide a formal explanation for the successes in the extraction of uniform bounds from nonstandard proofs given in [Advances in Mathematics, 343:567-623, 2019], which had informally followed the perspective of the monotone functional interpretation. As an application of the formal framework we develop, we provide novel explicit bounds for a structural theorem for stable subsets of groups given in [Mathematical Proceedings of the Cambridge Philosophical Society, 168(2):405-413, 2020].

math.LO↗
arXiv2026

On the Computational Content of Moduli of Regularity and their Logical Strength

We continue the investigation into the computational status of the existence of moduli of regularity (and their use for rates of convergence) in the sense of Kohlenbach, Lopez and Nicolae (2019), carried out w.r.t. classical reverse mathematics and Weihrauch degrees in a previous paper and determine the amount of LEM involved. We also show that the existence of a modulus of regularity always yields an algorithm for the computation of a zero in the case of continuous real-valued functions F on a compact metric space K (in F equipped with a modulus of uniform continuity and K given in standard representation) whenever such a zero exists. If K is a compact subset of a uniformly convex Banach space X and the zero set of F is convex one can compute even the zero of minimal norm. A modulus of regularity can also be used to compute the left-most infinite path of an infinite 0/1-tree. We also show that there is no proof-theoretically tame nonstandard uniformity principle which would make it possible to replace in the regularity assumption compactness by metric boundedness and still guarantee classically correct bounds.

cs.LO↗
arXiv2023

Fejér monotone sequences revisited

In this paper we introduce a localized and relativized generalization of the usual concept of Fejér monotonicity together with uniform and quantitative versions thereof and show that the main quantitative results obtained by the 1st author together with Nicolae and Leuştean in 2018 and with López-Acedo and Nicolae in 2019 respectively, extend to this generalization. Our framework, in particular, covers the sequence generated by the Dykstra algorithm while the latter is not Fejér-monotone in the ordinary sense. This gives a theoretical explanation why under a metric regularity assumption one obtains an explicit rate of convergence for Dykstra's algorithm which was proved recently by the 2nd author.

math.OC↗
arXiv2023

On modified Halpern and Tikhonov-Mann iterations

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.

math.OC↗
arXiv2022

R.E. Bruck, proof mining and a rate of asymptotic regularity for ergodic averages in Banach spaces

We analyze a proof of Bruck to obtain an explicit rate of asymptotic regularity for Cesàro means in uniformly convex Banach spaces. Our rate will only depend on a norm bound and a modulus $η$ of uniform convexity. One ingredient for the proof by Bruck is a result of Pisier, which shows that every uniformly convex (in fact every uniformly nonsquare) Banach space has some Rademacher type $q>1$ with a suitable constant $C_q$. We explicitly determine $q$ and $C_q$, which only depend on the single value $η(1)$ of our modulus. Beyond these specific results, we summarize how work of Bruck has inspired developments in the proof mining program, which applies tools from logic to obtain results in various areas of mathematics.

math.DS↗
arXiv2021

Quantitative analysis of a subgradient-type method for equilibrium problems

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ér monotonicity as given by the second author in previous papers.

math.OC↗
arXiv2021

Bounds for a nonlinear ergodic theorem for Banach spaces

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 nonexpansive maps on Banach spaces.

math.DS↗
arXiv2021

Quantitative translations for viscosity approximation methods in hyperbolic spaces

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).

math.FA↗
arXiv2020

A uniform betweenness property in metric spaces and its role in the quantitative analysis of the "Lion-Man" game

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.

math.MG↗
arXiv2020

Rates of convergence for iterative solutions of equations involving set-valued accretive operators

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.

math.OC↗
arXiv2020

The finitary content of sunny nonexpansive retractions

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 $T$ 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 $T_1$. 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.

math.FA↗
arXiv2018

Moduli of regularity and rates of convergence for Fejér monotone sequences

In this paper we introduce the concept of modulus of regularity as a tool to analyze the speed of convergence, including the finite termination, for classes of Fejér 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, Hölder regularity, etc., as well as to obtain rates of convergence for Picard iterates, the Mann algorithm, the proximal point algorithm and the cyclic algorithm. 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.

math.OC↗
arXiv2017

On proximal mappings with Young functions in uniformly convex Banach spaces

It is well known in convex analysis that proximal mappings on Hilbert spaces are $1$-Lipschitz. In the present paper we show that proximal mappings on uniformly convex Banach spaces are uniformly continuous on bounded sets. Moreover, we introduce a new general proximal mapping whose regularization term is given as a composition of a Young function and the norm, and formulate our results at this level of generality. It is our aim to obtain the corresponding modulus of uniform continuity explicitly in terms of a modulus of uniform convexity of the norm and of moduli witnessing properties of the Young function. We also derive several quantitative results on uniform convexity, which may be of interest on their own.

math.FA↗
arXiv2016

Proceedings Sixth International Workshop on Classical Logic and Computation

The workshop series intends to cover research that investigates the computational aspects of classical logic and mathematics. Its focus is on unwinding the computational content of logical principles and proof in mathematics based on these principles, aiming to bring together researchers from both fields and exchange ideas. Classical Logic and Computation (CL&C) 2016 was the sixth edition of this workshop series held as a satellite to FSCD 2016 on June 23, 2016 in Porto, Portugal. In this sixth edition we received 11 submissions of both short and full papers. Eight (8) of these were selected to present at the meeting in Porto, and five (5) full papers were initially accepted to appear at this EPTCS special volume of which one was subsequently withdrawn by its authors. An invited talk was given by Marc Bezem (U. of Bergen): Coherent Logic - an overview. Other topics covered by this years submissions included: computational content of proofs using nonstandard analysis, a structured grammar-based approach to the Herbrand content of proofs, semantics of the lambda-mu calculus, normalization of classical natural deduction proofs, proof mining of noneffective proofs in convex optimization and algebra by functional interpretations. I like to thank the members of the program committee for their excellent work: Steffen van Bakel (London), Stefano Berardi (Torino), Fernando Ferreira (Lisboa), Hugo de'Liguoro (Torino), Alexandre Miquel (Montevideo). Ulrich Kohlenbach (Darmstadt, PC Chair)

cs.LO↗
arXiv2012

Effective metastability of Halpern iterates in CAT(0) spaces

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.

math.FA↗
arXiv2010

On Tao's "finitary" infinite pigeonhole principle

In 2007, Terence Tao wrote on his blog an essay about soft analysis, hard analysis and the finitization of soft analysis statements into hard analysis statements. One of his main examples was a quasi-finitization of the infinite pigeonhole principle IPP, arriving at the "finitary" infinite pigeonhole principle FIPP1. That turned out to not be the proper formulation and so we proposed an alternative version FIPP2. Tao himself formulated yet another version FIPP3 in a revised version of his essay. We give a counterexample to FIPP1 and discuss for both of the versions FIPP2 and FIPP3 the faithfulness of their respective finitization of IPP by studying the equivalences IPP <-> FIPP2 and IPP <-> FIPP3 in the context of reverse mathematics. In the process of doing this we also introduce a continuous uniform boundedness principle CUB as a formalization of Tao's notion of a correspondence principle and study the strength of this principle and various restrictions thereof in terms of reverse mathematics, i.e., in terms of the "big five" subsystems of second order arithmetic.

math.LO↗
arXiv2008

A quantitative Mean Ergodic Theorem for uniformly convex Banach spaces

We provide an explicit uniform bound on the local stability of ergodic averages in uniformly convex Banach spaces. Our result can also be viewed as a finitary version in the sense of T. Tao of the Mean Ergodic Theorem for such spaces and so generalizes similar results obtained for Hilbert spaces by Avigad, Gerhardy and Towsner (arXiv:0706.1512v2 [math.DS]) and T. Tao (arXiv:0707.1117v1 [math.DS]).

math.DS↗