General logical metatheorems for functional analysis

By Philipp Gerhardy, Ulrich Kohlenbach. 2005

128 citations recorded by the source corpus.

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, Holder-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.

Subfields: Computational Theory and Mathematics, Control and Systems Engineering, Geometry and Topology

View Paper: https://www.semanticscholar.org/paper/5bc0fe0616853bc8edb01b513399a13bb4303fab

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

In Control and Systems Engineering

In Geometry and Topology

Citations in the corpus

LOCAL STABILITY OF ERGODIC AVERAGES (2007, background): “We are grateful to Ulrich Kohlenbach and James Cum-mings for comments and corrections.”
PROOF-THEORETIC METHODS IN NONLINEAR ANALYSIS (2019, unknown): “Example: for monotone T ∗ one defines T ∗ &X→X T ≡ ∀n ∈ N, x ∈ X[n ≥ d(a, x)→ T ∗(n) ≥ d(a, T (x))] (see [21, 34]).”
Effective metastability of Halpern iterates in CAT(0) spaces (2011, background): “There are general logical metatheorems due to the first author [21] and Gerhardy and the first author [14] that guarantee the extractability of computable and highly uniform such bounds Φ(k, g) from large classes of (even highly ineffective) proofs.”
Asymptotically nonexpansive mappings in uniformly convex hyperbolic spaces (2007, methodology): “Precise definitions for all this can be found in [13, 4].”