Formalization of Two Fixed-Point Algorithms in Hilbert Spaces

TL;DR

This paper formalizes the convergence proofs of Krasnosel'ski--Mann and Halpern fixed-point algorithms in Hilbert spaces using the Lean4 theorem prover, enhancing machine-checked analysis in convex optimization.

Contribution

It provides a formalization of key fixed-point algorithms and their convergence in Hilbert spaces within Lean4, including properties of nonexpansive operators and Fejér monotone sequences.

Findings

Formalized convergence of Krasnosel'ski--Mann iteration

Formalized convergence of Halpern iteration

Developed reusable components for convex analysis in Lean4

Abstract

Iterative algorithms are fundamental tools for approximating fixed-points of nonexpansive operators in real Hilbert spaces. Among them, Krasnosel'ski\u{\i}--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\'{e}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.