${\mathbb R}$ -树和双曲空间中的证明挖掘
Proof mining in ${\mathbb R}$-trees and hyperbolic spaces
摘要：
本文是由Kohlenbach开发的证明挖掘的一般项目的一部分。“证明挖掘”是指对数学证明进行逻辑分析，目的是提取隐藏在证明中的新的数字相关信息。我们提出的逻辑亚定理类的空间从泛函分析和双曲几何，如Gromov双曲空间，${\mathbb R}$树和一致凸双曲空间。我们的定理是适应这些结构的Gerhardy和Kohlenbach以前的元定理，他们保证先验，在非常一般的逻辑条件下，存在一致的界限。我们也给出了一个应用在非线性泛函分析，更具体地说，在度量不动点理论。因此，我们证明了一致凸双曲空间中非扩张映象的Krasnoselski-Mann迭代的渐近正则性速度的一致界是我们的一个亚定理的一个例子.
英文摘要：
This paper is part of the general project of proof mining, developed by Kohlenbach. By "proof mining" we mean the logical analysis of mathematical proofs with the aim of extracting new numerically relevant information hidden in the proofs. We present logical metatheorems for classes of spaces from functional analysis and hyperbolic geometry, like Gromov hyperbolic spaces, ${\mathbb R}$-trees and uniformly convex hyperbolic spaces. Our theorems are adaptations to these structures of previous metatheorems of Gerhardy and Kohlenbach, and they guarantee a-priori, under very general logical conditions, the existence of uniform bounds. We give also an application in nonlinear functional analysis, more specifically in metric fixed-point theory. Thus, we show that the uniform bound on the rate of asymptotic regularity for the Krasnoselski-Mann iterations of nonexpansive mappings in uniformly convex hyperbolic spaces obtained in a previous paper is an instance of one of our metatheorems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
