Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalization of Two Fixed-Point Algorithms in Hilbert Spaces

Yifan Bai, Yantao Li, Jian Yu, Jingwei Liang

TL;DR

This work formalizes the convergence of Krasnosel'ski--Mann iteration and Halpern iteration in the interactive theorem prover Lean4 based on type dependent theory and provides reusable components for machine-checked convergence analysis of fixed-point iterations and theories of convex analysis in real Hilbert spaces.

Abstract

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

Formalization of Two Fixed-Point Algorithms in Hilbert Spaces

TL;DR

This work formalizes the convergence of Krasnosel'ski--Mann iteration and Halpern iteration in the interactive theorem prover Lean4 based on type dependent theory and provides reusable components for machine-checked convergence analysis of fixed-point iterations and theories of convex analysis in real Hilbert spaces.

Abstract

Iterative algorithms are fundamental tools for approximating fixed-points of nonexpansive operators in real Hilbert spaces. Among them, Krasnosel'skiĭ--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.
Paper Structure (20 sections, 15 theorems, 19 equations, 2 figures)

This paper contains 20 sections, 15 theorems, 19 equations, 2 figures.

Table of Contents

  1. Key words
  2. Introduction
  3. Iterative schemes
  4. Motivation and main contributions
  5. Main contributions
  6. Paper organization
  7. Weak topology of Hilbert spaces
  8. Existing results in mathlib
  9. Weak convergence
  10. Closedness
  11. Compactness
  12. Nonexpansive operator and fixed-point iteration
  13. Nonexpansive operators
  14. Fixed-point iterations
  15. Convergence analysis
  16. ...and 5 more sections

Key Result

Theorem 2.2

Let $\{x_n\}$ be a sequence in a real Hilbert space $\mathcal{H}$ and let $p \in \mathcal{H}$. Sequence $\{x_n\}$converges weakly to $p$ if and only if

Figures (2)

  • Figure 1: Dependency graph of part of the formalized theorems.
  • Figure 2: Type coercion between weak and strong topologies of a Hilbert space.

Theorems & Definitions (20)

  • Definition 2.1: Weak topology
  • Theorem 2.2: Weak convergence
  • Theorem 2.3: Boundedness of weak convergence sequence
  • Theorem 2.4: bauschke2011convex
  • Theorem 2.5: bauschke2011convex
  • Theorem 2.6: bauschke2011convex
  • Theorem 2.7: bauschke2011convex
  • Theorem 2.8: Banach--Alaoglu theorem, bauschke2011convex
  • Theorem 2.9: bauschke2011convex
  • Corollary 2.10: bauschke2011convex
  • ...and 10 more