×

A proof-theoretic bound extraction theorem for \(\mathrm{CAT}(\kappa)\)-spaces. (English) Zbl 1420.03140

Summary: 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 \(\mathrm{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.

MSC:

03F10 Functionals in proof theory
53C22 Geodesics in global differential geometry
58D17 Manifolds of metrics (especially Riemannian)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ariza-Ruiz, D., A. Fernández-León, G. López-Acedo, and A. Nicolae, Chebyshev sets in geodesic spaces, Journal of Approximation Theory 207:265-282, 2016. · Zbl 1347.41037
[2] Berg, I. D., and I. G. Nikolaev, A \[KK\]-quadrilateral cosine characterization of Aleksandrov spaces of curvature bounded above. arXiv:1512.01736v1, 2015. · Zbl 1079.03046
[3] Bridson, M. R., and A. Haefliger, Metric Spaces of Non-positive Curvature, Springer, Berlin, 1999. · Zbl 0988.53001
[4] Cho, S., A variant of continuous logic and applications to fixed point theory. arXiv:1610.05397, 2016. · Zbl 1362.37015
[5] Espínola, R., and A. Fernández-León, CAT \[(\kappa )\](κ)-spaces, weak convergence and fixed points. Journal of Mathematical Analysis and Applications 353:410-427, 2009. · Zbl 1182.47043
[6] Gerhardy, P., and U. Kohlenbach, General logical metatheorems for functional analysis, Transactions of American Mathematical Society 360:2615-2660, 2008. · Zbl 1130.03036
[7] Günzel, D., and U. Kohlenbach, Logical metatheorems for abstract spaces axiomatized in positive bounded logic, Advances in Mathematics 290:503-551, 2016. · Zbl 1402.03078
[8] Kohlenbach, U., Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin’s proof for Chebycheff approximation, Annals of Pure and Applied Logic 64:27-94, 1993. · Zbl 0795.03086
[9] Kohlenbach, U., Proof Theory and Computational Analysis, Electronic Notes in Theoretical Computer Science, vol. 13, Elsevier, Amsterdam, 1998, 34 pp. · Zbl 0917.68196
[10] Kohlenbach, U., Some logical metatheorems with applications in functional analysis, Transactions of the American Mathematical Society 357(1):89-128, 2005. · Zbl 1079.03046
[11] Kohlenbach, U., Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Monographs in Mathematics, Springer, Berlin, 2008, 536 pp. · Zbl 1158.03002
[12] Kohlenbach, U., On the quantitative asymptotic behavior of strongly nonexpansive mappings in Banach and geodesic spaces, Israel Journal of Mathematics 216:215-246, 2016. · Zbl 1358.47038
[13] Kohlenbach, U., Recent progress in proof mining in nonlinear analysis, To appear in forthcoming book with invited papers by recipients of the Gödel Centenary Research Prize Fellowship.
[14] Leuştean, L., and A. Nicolae, Effective results on nonlinear ergodic averages in CAT \[(\kappa )\](κ) spaces, Ergodic Theory and Dynamical Systems 36:2580-2601, 2016. · Zbl 1362.37015
[15] Pia̧tek, B., Halpern iteration in CAT \[(\kappa\] κ) spaces, Acta Mathematica Sinica, English Series 27:635-646, 2011. · Zbl 1326.47093
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.