CAT(0)空间中Halpern迭代的有效元稳定性
泛函分析
2012-06-11 v4 逻辑
摘要
本文给出了CAT(0)空间中非扩张映射Halpern迭代强收敛的一个有效一致元稳定性速率（在Tao的意义下）。从Saejung的一个非有效证明中提取该速率，是通用证明挖掘程序的一个实例，该程序利用数理逻辑工具揭示证明中隐藏的计算内容。本文首次将此方法应用于一个使用了Banach极限的证明，该证明因此实质性地涉及了选择公理。
引用
@article{arxiv.1107.3215,
title = {Effective metastability of Halpern iterates in CAT(0) spaces},
author = {Ulrich Kohlenbach and Laurentiu Leustean},
journal= {arXiv preprint arXiv:1107.3215},
year = {2012}
}
备注
some typos corrected