Formalization of Two Fixed-Point Algorithms in Hilbert Spaces

Yifan Bai, Yantao Li, Jian Yu +1

Iterative algorithms are fundamental tools for approximating fixed-points of nonexpansive operators in real Hilbert spaces. Among them, Krasnosel'ski\uı--Mann iteration and Halper…