R-树和双曲空间中的证明挖掘和应用：一般空间类的逻辑亚定理的分析

理论计算机科学电子笔记165（2006）95-106www.elsevier.com/locate/entcsR-树和双曲空间中的证明挖掘LaurentiuLeustean1德国达姆施塔特工业大学数学系，Schlossgartenstrasse 7，64289 Darmstadt，和通过对罗马帝国的Mat h e m i m i o n S t o i l o l o n A c d e m y的ma th e min S t o i l o n S t o i l o l o nA c d e m y的分析，C al e a G r i v i t e i 21，P. O. Box1-462，布加勒斯特，罗马尼亚摘要本文是由Kohlenbach开发的证明挖掘的一般项目的一部分。 通过我们从泛函分析和双曲几何中给出了一般空间类的逻辑亚定理，如Gromov双曲空间，R-树和一致凸双曲空间（在Reich/Kirk/Kohlenbach）。我们的定理是适应这些结构的Gerhardy和Kohlenbach以前的元定理，他们保证先验，在非常一般的逻辑条件下，存在一致的界限。我们也给出了在非线性泛函分析中的应用，更具体地说，在度量不动点理论中。因此，我们证明了一致凸双曲空间中非扩张映射的Krasnoselski-Mann迭代的渐近正则性的一致界是我们的一个亚定理的一个例子关键词：证明挖掘，双曲空间，R-树，一致凸，渐近正则性，非扩张函数1引言本文是由Kohlenbach开发的证明挖掘的一般项目的一部分（详见[16]）。在[14]中，Kohlenbach证明了一般逻辑元定理，该元定理保证了在非常一般的逻辑条件下，从泛函分析中的大类证明中先验地提取一致界的可能性，而且它们提供了实际提取有效一致界和将原始证明转化为更强一致性结果的算法这些亚定理在Reich/Kirk/Kohlenbach意义下处理1电邮地址：leustean@mathematik.tu-darmstadt.de1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.05.03996L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）95（本文称之为W-双曲空间），CAT（0），（一致凸）赋范空间和内积空间。它们假设了底层度量空间的全局有界性。这些亚定理在[7]中通过用非常有限的局部有界性假设代替整个空间有界的假设而得到了极大的推广新的亚定理保证边界是一致的所有参数满足这些弱的局部有界性条件。证明是基于Güodel的泛函理论的一个综合，它是由空间X中的一个点a参数化的一种优化本文对超曲几何或几何群论中的重要结构：Gromov双曲空间、R-树和一致凸W-双曲空间给出了新的亚定理。这些新的亚定理是作为度量空间和W-双曲空间的已有亚定理的改进而得到的基于以下事实，在[7]中已经注意到：(i) 该语言可以通过可优化的常数来扩展。在这种情况下，所提取的边界然后另外取决于新常数的α-优数，(ii) 如果量化器的类型是适当的，则该理论可以通过使用新的可优化常数的纯普适公理来扩展。则该结论分别在所有度量空间（X，d）中成立.满足这些公理的W-双曲空间（X，d，W）（如果有的话，在新常数的适当解释在本文的最后一节，我们提出了一个应用在度量不动点理论。在[18]中，作者得到了一致凸W-双曲空间中非扩张映象的Krasnoselski-Mann迭代的渐近正则性速度的一致界。这些结果扩展到这个更一般的设置的一个定量版本的加强Groetsch我们在第4节中解释了这个一致界的可抽取性是我们一致凸W-双曲空间理论的定理的一个例子。对于CAT（0）-空间，渐近正则性的速率是二次的，因为CAT（0）-空间有一个2预赛在这一节中，我们给出了由Gerhardy和Kohlenbach [7]证明的度量空间和W-双曲空间的一般亚定理的一个非正式表示我们假设熟悉[14，7]。[14]中定义了（弱可拓）经典分析的形式系统Aω，我们请读者阅读本文，了解与此形式系统相关的所有未定义概念，以及Aω中有理数和实数的表示。抽象度量空间的理论Aω[X，d]−b在[7]中通过推广Aω到集合TX的所有有限类型在地面类型0和X，增加常数0X的类型X，和dX的类型X→X→1连同公理，使dX的伪度量。 类型X的对象之间的相等=X定义为：x=Xy：=L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）9597dX（x，y）= R0R.我们在续集中介绍了由Kohlenbach [14]引入的双曲空间的设置;参见[14，16]详细讨论这个和相关概念。为了区别于双曲空间、双曲几何和Gromov双曲空间的通常概念，我们称它们为W-双曲空间。W-双曲空间是三元组（X，d，W），其中（X，d）是度量空间，W：X×X×[0，1]→X使得对所有x，y，z，w∈X，λ1，λ2∈[0，1]，（W1）d（z，W（x，y，λ））≤（1−λ）d（z，x）+λd（z，y），（W 2） d（W（x，y，λ1），W（x，y，λ2））= |λ1− λ2|·d（x，y），（W3）W（x，y，λ）=W（y，x，1−λ），（W 4） d（W（x，z，λ），W（y，w，λ））≤（1 − λ）d（x，y）+λd（z，w）.如果x，y∈X且λ∈[0， 1]，则我们对W（x，y，λ）使用记法（1−λ）x<$λy。我们用[x，y]表示集合{（1−λ）x<$λy：λ∈[0， 1]}。 一个非空子集C<$X是凸的，如果对所有x，y∈C，[x，y]<$C。理论Aω[X，d，W]−b是由Aω[X，d]−b加上一个新的常数而类型X→X→1→X的WX以及适当的公理。若X是非空集，则全理论型结构Sω，X：=<$Sρ<$ρ∈TXN和X由S定义：=N，S：=X，S：= SSρ，其中SSρ是所有0X集合论函数Sρ→Sτρ→τ τ τ定义2.1我们说L（Aω[X，d]−b）的句子在非空度量空间（X，d）中成立，如果它在Aω[X，d]−b的模型中成立，通过让变量在全理论类型结构的适当论域上变化，Sω，X，其中集合X作为基类型X的论域; 0X被X的任意元素解释;dX被解释为dX（x，y）：=（d（x，y））<$。在非空W-双曲空间（X，d，W）中，L（A ω [ X，d，W ] − b）的一个句子成立的概念是由前一个概念通过将WX（x，y，λ1）解释为W（x，y，rλ）而得到的，其中rλ∈[0，1]是由yλ生成的唯一的非空句子.在Bovededefition中，λ›→λ用[14]来表示区间[0， 1]，数论函数N→N和（·）是一个语义算子，也在[14]中定义，对于任何实数x∈ [0，∞），它从所有代表中选择f∈NNofx a unique representative（x）<$∈NN满足一些（x）0（n）：=j（2k0， 2n+1− 1），Σ ΣK其中k0= maxk2n+1≤xj是Cantor配对函数。定义2.2 [15]一个类型ρ被称为小的，如果它的度≤ 1（即0 →.）。→ 0）或形式98L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）95ρ1→. →ρk→X，其中ρi为0型或X型。L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）9599ρ定义2.3 [15]一个公式A被称为一个公式A（分别为： 如果它具有形式AxσA0（x）（相应地，AxσA0（x）），其中A0是一个无数量因子的公式，σ中的类型很小。对于任意类型p∈TX，我们定义类型p^∈T，其结果是将类型X在p中的所有出现都用类型0表示。基于Bezem的x<$04ax0：<$x <$0 ≥0x，x<$04a xX：R≥RdX（x，a），0Xx104ax：y，y（y4ay→xy4axy）z，z（z4az→xz4axz）。ρ→ τ ρ τρˆτˆ限制到T型，关系4a与强优超性是一致的s-maj，因此，对于ρ∈T，我们将写s-majρ而不是4a，因为在这种情况参数a是不相关的。下面的定理是一个非常一般的元定理的简化版本，它首先由Kohlenbach [14]在有界度量（W-双曲）空间中证明，然后由Gerhardy和Kohlenbach推广到无界情况：定理2.4[7]设ρ是一个小型，B∈（xρ，n0）（分别为 C（xρ，m0））是an-仅包含x，n自由的公式（分别为仅包含x，m自由的公式）。假设常数0 X不出现在B，C中，Aω [X，d] −b<$$>xρ（<$nB<$（x，n）→<$mC<$（x，m））.（一）则存在一个可计算泛函Φ：Sρb→N使得在所有非空度量空间（X，d）中下列成立：对所有x∈Sρ，x ∈Sρb，如果存在a ∈X使得x<$4ax，则<$n ≤ Φ（x<$）B<$（x，n）→ <$m≤ Φ（x <$）C<$（x，m）.（二）该定理也适用于Aω [X，d，W] −b和非空W-双曲空间（X，d，W）。代替单一变量x，n，m和单一前提的是，我们可以有变量的元组和前提的有限合取。在元组x的情况下，我们必须要求对于元组x的所有分量，对于公共a∈X，我们有一个a-优数的元组X。3新的元定理在这一节中，我们将定理2.4推广到双曲几何或几何群论中的重要结构：Gromov双曲空间，R-树和一致凸W-双曲空间。正如我们已经指出的，为了得到这些新结构的亚定理，将它们的理论重新表述为Aω[X，d]−b的扩展就足够了，或者100L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）952Aω[X，d，W]−b通过具有适当类型的量化器的纯泛语句，并验证新常数（如果有的话）是a-可优化的。我们将在后面看到这是可能的。3.1Gromov双曲空间GromovGromov双曲空间的研究主要是由（Gromov）双曲群的问题所激发和主导的，而（Gromov）双曲群是几何群论的主要研究对象之一。在续集中，我们回顾了有关Gromov双曲空间的一些定义和基本事实。关于这一材料的更详细的说明，读者可参考[11，8，3]。设（X，d）是度量空间.给定三个点x，y，w，x和y相对于基点w的关系定义为：（x·y）w= 1（d（x，w）+d（y，w）− d（x，y））。它衡量了三角不等式成为等式的失败，并且它总是非负的定义3.1设δ≥0。 X称为δ-双曲，如果对所有的x，y，z，w∈X，（x·y）w≥ min {（x·z）w，（y·z）w}− δ。（3）我们说X是Gromov双曲的，如果它对某个δ ≥ 0是δ -双曲的。事实证明，该定义与基点w在这个意义上，如果Gromov积是关于一个基点的δ-双曲，那么它是关于任何基点的2δ-双曲通过解开Gromov乘积的定义，（3）可以重写为4点条件：对于所有x，y，z，w∈X，d（x，y）+d（z，w）≤ max {d（x，z）+d（y，w），d（x，w）+d（y，z）}+2 δ.（四）Gromov双曲空间的理论Aω[X，d，δ-双曲]−b通过如下扩展Aω[X，d]−b定义(i) 加上一个类型为1的常数δ1(ii) 添加公理δ≥R0R，xX，yX，zX，wX.dX（x，y）+RdX（z，w）≤RΣ≤Rmax R{dX（x，z）+RdX（y，w），dX（x，w）+RdX（y，z）}+R2·Rδ.L（Aω[X，d，δ-双曲]−b）在非空格罗莫夫双曲空间（X，d，δ）中成立的概念如定L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）951010义2.1所定义，通过将新常数δ1解释为δ1：=（δ）0。因为≤R是1，所以这两个公理是普适的。因此，为了适应定理2.4到Gromov双曲空间的理论，我们需要证明新102L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）951常数δ1是强可优的。很容易看出，如果（X，d，δ）是δ-双曲空间，且k∈N使得k≥δ，则δε：= λn.j（k·2 n+2，2 n+1−1）s-maj（δ）ε。定理3.2定理2.4对于Aω [X，d，δ-双曲] −b和非空Gromov双曲空间（X，d，δ）也成立，其中界Φ还依赖于k∈N使得k≥ δ。3.2R-树R-树的概念由Tits [21]引入，作为秩1群的局部Bruhat-Tits构建概念的推广，其本身推广了单纯树的概念。一个更一般的概念，即Λ-树，其中Λ是一个全序阿贝尔群，在Morgan和Shalen的工作中，它作为研究作用于双曲流形的群的重要工具出现[20]。关于R（Λ）-树的详细信息，我们参考[6]。接下来，我们回顾一些基本的定义。 设（X，d）是度量空间. X中的测地线是一个保持距离的映射γ：[a，b] →R，即d（γ（s），γ（t））= |s−t|对于所有s，t∈[a，b]。X中的测地线线段是X中测地线的像。如果γ：[a，b]→R是一条测地线，且x，y∈X使得γ（a）=x，γ（b）=y，我们说γ是从x到y的测地线，或者说测地线线段γ（[a，b]）连接x和y。X称为（唯一）测地线空间，如果每两点由（唯一）测地线连接。如果X是唯一测地空间，则我们用[x，y]表示连接x和y的唯一测地线段。定义3.3[21]X是一个R-树i ∈X是一个测地线空间，不包含圆的同胚像。我们注意到，在最初的定义中，Tits只考虑了R-树作为度量空间是完备的，但完备性的假设通常是不相关的。下面的命题给出了R-树的一些等价刻画，这些刻画可以在文献中找到.命题3.4设（X，d）是度量空间。以下是等价的：(i) X是一棵R树，(ii) X是唯一测地线，对所有x，y，z∈X，[y，x]<$[x，z]={x}<$[y，x]<$[x，z]=[y，z]。（五）(i.e.、如果两个测地线线段相交于一个点，则它们的并集是测地线线段。）(iii) X是0-双曲的测地空间，即满足不等式（4），δ = 0。R-树恰好是测地0-双曲空间这一事实是由Alperin和Bass [1，定理3.17]的一个非常重要的结果得出的，并且是本文的基本结论。L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）95103⎪。Σ使用我们的概念证明RW-双曲空间。命题3.5设（X，d）是度量空间。以下是等价的：(i) X是R-树;(ii) X是一个W-双曲空间，满足对所有x，y，z，w ∈ X，d（x，y）+d（z，w）≤ max {d（x，z）+d（y，w），d（x，w）+d（y，z）}。现在，我们准备定义R-树的形式理论Aω[X，d，W，R-树]−b这是由理论Aω[X，d，W]−b加上公理得到的：。xX，yX，zX，wX。dX（x，y）+RdX（z，w）≤R≤Rmax R{dX（x，z）+RdX（y，w），dX（x，w）+RdX（y，z）}。因此，Aω[X，d，W，R-树]−b是由Aω[X，d，W]− b通过添加一个泛公理而得到的定理3.6定理2.4对Aω [X，d，W，R-树] −b和非空R-树也成立。3.3一致凸W-双曲空间一致凸W-双曲空间的概念在[9，p.105]之后的[18]中定义定义3.7一个W-双曲空间（X，d，W）称为一致凸的，如果对任意r >0，且ε∈（0， 2]，存在δ∈（0， 1]，使得对所有a，x，y∈X，⎫d（x，a）≤r⎬1 1d（y，a）≤r⎪dx2 2≤（1 − δ）r。（六）d（x，y）≥εr一个映射η：（0，∞）×（0，2]→（0，1]对于给定的r >0和ε∈（0，2]有δ：=η（r，ε），称为一致凸模.使用标准连续性论证，我们可以证明以下等价刻画。命题3.8设（X，d，W）是W-双曲空间. 以下是等效的：(i) 存在η：（0，∞）×（0，2]→（0，1]使得（6）成立，(ii) 存在η：Q+×N→N使得对任意r∈Q+，k∈N，a，x，y∈X∗d（x，a）1− 2−η（r，k）r2 2L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）95105dX（x，a）R1−2X·Rr→dX（x，y）≤R2·Rr，n=0，k =0，r = 0，k= 0，r = 0，k = 0，k =在第二个公理中，我们表达了这样一个事实，即ηX是一个函数，其第一个参数是代码水平上的有理数。 函数q定义为：q（n）：=mink≤0n[k=Qn]（详见[12]）。由于R∈N1且≤R∈ N1，0 0我们的新理论是从Aω[X，d，W]−b通过添加两个泛公理 还很容易看出，常数η000是可优化的。L（Aω[X，d，W，η]−b）的句子在非空一致凸W-双曲空间（X，d，W，η）中成立的概念如定义2.1所定义，通过将新常数ηX解释为ηX（r，k）：=η（q（r），k）。定理3.9定理2.4对Aω [X，d，W，η] −b和非空一致凸W-双曲空间（X，d，W，η）也成立，其中界Φ还依赖于一致凸模η。4度量不动点理论的一个应用在最后一节中，我们给出了一致凸W-双曲空间的亚定理在度量不动点理论中的应用，更具体地说，在非扩张函数的不动点理论中的应用。设（X，d，W）是双曲空间，C∈X是X的非空凸子集.一个映射T：C→C称为非扩张映射，如果对所有x，y∈C，d（Tx，Ty）≤d（x，y）.与赋范空间[19，17]的情况一样，我们可以定义从x∈C开始的Krasnoselski-Mann迭代：x0 ： = x ，xn+1 ： = （ 1 −λn ） xn<$λnTxn ，（8）其中（λn）是[0，1]中的序列。渐近正则性由Browder和Petryshyn [5]定义：T：C→C称为渐近正则的，如果limn→∞ d（Tn（x），Tn+1（x））= 0x∈C。 根据[4]，我们说非扩张映射T：C→C是λn-渐近正则如果limn→∞ 对所有x ∈ C，d（xn，Txn）= 0. 下面的作者在[18]中证明：定理4.1设（X，d，W）是一致凸双曲空间，具有一致凸模η，使得η随r减小（对于固定ε），C∈X是非空凸子集，T：C→C非扩张，使得T至少有一个106L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）95∀δ固定点。此外，假设（λn）是[0，1]中的序列，使得λn）= ∞。则T是λn-渐近正则的。Σ∞n=0例λn（1−这个定理是Groetsch [10]证明的赋范空间的一个定理在一致凸W-双曲空间上的版本。在Groetsch定理中不过，我们必须强调，这个额外的假设是由重要的一致凸W-双曲空间类，如希尔伯特球，CAT（0）-空间或R-树满足。在接下来的文章中，我们证明了定理3.9保证了上述定理的加强的一致有效界，该定理仅假设在起点x的某个邻域中存在近似不动点。由于W-双曲空间的任何凸子集也是W-双曲空间，所以只考虑非扩张函数T：X→X。我们使用以下符号：M在（η，r）上：=<$r0，r0，k0（r1≤Qr2→η（r1，k）≥0η（r2，k）），1 2Fix（T）：={pX|T（p）= Xp}，Fixδ（T，x，b）：={yX|dX（y，T（y））≤Rδ <$dX（x，y）≤Rb}.定理3.9的下列更具体的推论可供我们应用.它的证明与[7，推论4.22]的证明相似推论4.2设P是Aω-可定义的Polish空间，K是Aω-可定义的紧致Polish空间。 让B和C像以前一样。 如果Aω [X，d，W，η] −b证明，<$z∈P<$y∈K<$xX， TX→X.Tn. e. Fix（T）/=∃则存在一个可计算泛函Φ：NN×N×NN×N→N（关于代表rz：N→N的元素z∈P）使得对所有rz∈NN，b∈N当x∈K时，X→X.Tn. e. ∧∀δ>0(Fix(T,x,b)∅)∧n≤0Φ（rz，b，η）B在任何非空一致凸W-双曲空间（X，d，W，η）中成立。和前面一样，我们可以有变量的元组和前提的有限合取，而不是单一的变量y，z和单一的前提B。利用序列（d（xn，T（xn））是非增的这一事实，我们得到T 是渐近正则的等价于<$x∈X<$k∈N <$N∈N（d（xN，T（xN））<2 −k）。定理4.1中关于（λn）的假设等价于存在见证者θ=（n）θ：N→N使得对所有n ∈ N，λi（1 −λi）≥ n。i=0时L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）95107（·）（·）⎪⎢因此，Aω[X，d，W，η]−b证明了定理4.1的以下形式化版本：<$k0<$θ1<$λ0→1<$xX，TX→X。Mon（η，r）T n. e. F ix（T）/=（n）<$$>n0（n≤R λi（1−λi））→ <$N0（dX（xN，T（xN））R2−k），i=0时其中λ0→1表示紧Polish空间[0，1]∞中具有乘积度量的元素推论4.2给出了存在一个可计算泛函Φ（k，θ，b，η）使得对所有（λn）∈[0，1]∞，x∈X，T：X→X，Mon（η，r）T n. e. ∧ ∀δ> 0(F ixδ(T, x, b)/= ∅)∧∀n (n ≤θ=（n）k=0λk（1−λk））→Σ→ <$N≤Φ（k，θ，b，η）（d（xN，T（xN））≤2−k）在任何非空一致凸W-双曲空间（X，d，W，η）中成立。再次使用（d（xn，T（xn）是非增的，可以得出Φ（k，θ，b，η）是（d（xn，T（xn）向0的收敛速度的界因此，作为推论4.2的一个应用，我们立即得到定理4.1的一个加强的以下统一形式。定理4.3设（X，d，W）是具有一致凸模η的一致凸双曲空间，使得η随r减小（对固定ε），C∈X是非空凸子集，T：C→C非扩张.设（λn）是[0，1]中的序列，θ：N→N使得对所有n∈ N，θ=（n）i=0时λi（1 −λi）≥ n。（九）设x∈C，b>0，使得对任意δ> 0，有y∈C，ρ（x，y）≤ b且ρ（y，Ty）≤ δ。（十）然后limn→∞ ρ（xn，Txn）= 0，而且。Σn≥Φ（ε，θ，b，η） ρ（xn，Txn）≤ε。在[18，定理14]中进行Φ（ε，θ，b，η）的提取：⎧⎛⎡⎪⎜⎢⎤⎞b+1你好ε <2b的平均值Φ（ε，θ，b，η）：=⎪⎪⎝⎢⎢ε·ηb+1，⎥⎠⎥b+1我不知道你在说什么。ε108L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）95此外，对于有界C，条件（10）对所有x∈C成立，其中dC代替b，因此我们得到了满足（9）的一般（λn）的渐近正则性和一个显式的L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）95109本文证明了Φ（ε，θ，dC，η）的渐近正则性速度的界，它只依赖于误差ε、一致凸模η、C的直径dC和（λn），而不依赖于非扩张映射T、迭代起点x∈C或其它与C和X有关的数据。此外，对于CAT（0）-空间（以及随后的R-树），它有一个非常“好”的一致凸模，我们得到了一个二次渐近正则性。我建议读者参阅[18]，以了解所有这些事实的详细介绍。确认我感谢Ulrich Kohlenbach，感谢他就这个问题进行了多次讨论。他的建议大大改进了结果的表述方式。引用[1] 阿尔佩林河和H.Bass，Λ-树上的长度函数和群作用，在：Gersten，S。M.，和j.R. Stallings（Eds.），“Combinatorial group theory and topology”, Annals of Mathematics Studies 265-378。[2] Bezem，M.，有限类型的强可优化泛函：包含不连续泛函的棒递归模型，J. Symbolic Logic50（1985），652-660。[3] M.布赖森，和A. Hae Zeriger，[4] Borwein，J.，S.赖克和我范文，范维空间中的Krasnoselski-Mann迭代，加拿大数学。公牛35（1992），21[5] Browder，F. E、和W. 陈文辉，李文辉[6] 奇斯韦尔岛，“Introduction to Λ-trees”, World Scientific, River Edge, NJ,[7]Gerhardy ， P. ， 和 联 合 Kohlenbach ， General logical metathormans for functional analysis ， BRICSResearch Report RS-05-21（2005），65 pp. BRICS（计算机科学基础研究），奥胡斯大学;已提交。[8] Ghys，E. ，和P. delaH arp e（Eds. ），“SurlesGroupesHyperboliquesd'apr'esMikhailGromov“，ProgresinMathematics83，Birkhéauser，Boston，1990.[9] Goebel，K.，和S.李明，“一致凸性、双曲几何与非扩张映射”，北京：清华大学出版社，纽约，1984年。[10] 格罗奇角W.，A note on segmenting Mann iterates，J. Math. Anal.和Appl.40（1972），369[11]Gromov，M.，Hyperbolic groups，in：Gersten，S. M. (Ed.)、《群论》，MSRI。Publ. 8，Springer-Verlag，1987，pp. 75-263[12] 科伦巴赫大学，证明理论和计算分析，理论计算机科学电子笔记13（1998），124[13] 科伦巴赫大学，Mann迭代的一致渐近正则性，J. Math. Anal.和Appl.279（2003），531-544。[14] 科伦巴赫大学，一些逻辑元定理及其在泛函分析中的应用，Trans. Amer. Math. Soc.357（2005），89[15] 科伦巴赫大学，从抽象泛函分析中的证明的有效界限，2006年，提交。[16] 科伦巴赫大学，“Proof Interpretations and the Computational Content证据”，2006,草案，420pp.，网址：http：//www.mathematik.tu-darmstadt.de/110L. Leus Schmidtean/Electronic Notes in Theoretical Computer Science 165（2006）95[17]克拉斯诺谢尔斯基湾一、关于逐次逼近法的两点注记。数学Nauk（N.S.）10（1955），123[18] 勒乌斯特河， 一个关于CAT（0）-s空间的等价映射的二次描述，J. M ATH。 A nal. AppL.，出版中。[19] Mann，W.R.，迭代中的平均值方法，Proc.Amer. 数学Soc. 4（1953），506[20] 摩 根 ， J. ， 和 P. Shalen ， Valuations ， trees ， and degenerations of hyperbolic structures I ， Ann.ofMath.120（1984），401-476.[21] 乳房，J，树的李-科尔钦定理，在：巴斯，H.，P. Cassidy和J. Kovacic（编辑），“贡献代数：一系列论文献给埃利斯Kolchin”，学术出版社，纽约，1977年，页。377-388.