在Hilbert空间中形式化两种不动点算法
Formalization of Two Fixed-Point Algorithms in Hilbert Spaces
AI总结：
本文在Lean4中形式化了两种固定点算法在Hilbert空间中的收敛性，提供了非扩张算子和Fejér单调序列的定义，并验证了两种迭代方案的收敛性。
摘要：
迭代算法是近似非扩张算子在实Hilbert空间中不动点的基本工具。其中，Krasnosel'ski\uı--Mann迭代和Halpern迭代是两种广泛应用的方案。在本文中，我们基于类型依赖理论，在交互定理证明器Lean4中形式化了这两种固定点算法的收敛性。为此，我们形式化了无限维实Hilbert空间中的弱收敛性和拓扑性质。还提供了非扩张算子的定义和性质。作为凸分析中的有用工具，我们随后形式化了Fejér单调序列。在这些基础上，我们验证了这两种迭代方案的收敛性。我们的形式化为在实Hilbert空间中固定点迭代和凸分析理论的机检查收敛性分析提供了可重用的组件。我们的代码可在https://github.com/TTony2019/fixed-point-iterations-in-lean上获取。
英文摘要：
Iterative algorithms are fundamental tools for approximating fixed-points of nonexpansive operators in real Hilbert spaces. Among them, Krasnosel'ski\uı--Mann iteration and Halpern iteration are two widely used schemes. In this work, we formalize the convergence of these two fixed-point algorithms in the interactive theorem prover Lean4 based on type dependent theory. To this end, weak convergence and topological properties in the infinite-dimensional real Hilbert space are formalized. Definition and properties of nonexpansive operators are also provided. As a useful tool in convex analysis, we then formalize the Fejér monotone sequence. Building on these foundations, we verify the convergence of both the iteration schemes. Our formalization provides reusable components for machine-checked convergence analysis of fixed-point iterations and theories of convex analysis in real Hilbert spaces. Our code is available at https://github.com/TTony2019/fixed-point-iterations-in-lean.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
