Prove2Me

Section 4.1, Step 2 — ∥xk−y∥2\|x^k-y\|_2 converges for every fixed point yy

Proved
AndersonAccel.Safe.dist_converges

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

anderson-accelerationfejer-monotonefixed-point-iterationp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let f:Rn→Rnf:\mathbb R^n\to\mathbb R^n be nonexpansive and run Algorithm 3.1 with θˉ,τ,α∈(0,1)\bar\theta,\tau,\alpha\in(0,1), D,ϵ>0D,\epsilon>0 and max-memory m≥1m\ge1, assuming no iterate is a solution (f(xk)≠xkf(x^k)\ne x^k for all kk). Then for every fixed point y=f(y)y=f(y) the distance ∥xk−y∥2\|x^k-y\|_2 converges: there is L∈RL\in\mathbb R with

lim⁡k→∞∥xk−y∥2=L.\lim_{k\to\infty}\|x^k-y\|_2=L.

Together with the vanishing residual (4.6), this is the Opial-type ingredient from which convergence of the whole sequence follows.

Formalization Note The hypothesis f(xk)≠xkf(x^k)\ne x^k is the paper's standing simplification at the start of §4.1.

Preamble
import Mathlib
import Definitions.Def_AndersonAccel_Safe_Basic
import Definitions.Def_AndersonAccel_Safe_IsAAISRun
Formal statement
namespace AndersonAccel.Safe

open Filter Topology

/-- Section 4.1, Step 2 (p. 3181). For every fixed point `y` of `f`, `‖x^k - y‖` converges. -/
theorem dist_converges {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (hf : LipschitzWith 1 f)
    (θbar τ α D ε : ℝ) (m : ℕ)
    (hθ0 : 0 < θbar) (hθ1 : θbar < 1) (hτ0 : 0 < τ) (hτ1 : τ < 1) (hα0 : 0 < α) (hα1 : α < 1)
    (hD : 0 < D) (hε : 0 < ε) (hm : 0 < m)
    (x xt s y shat ytil : ℕ → EuclideanSpace ℝ (Fin n))
    (H : ℕ → (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))) (mem nAA : ℕ → ℕ)
    (hrun : IsAAISRun f θbar τ α D ε m x xt s y shat ytil H mem nAA)
    (hnosol : ∀ k, f (x k) ≠ x k)
    (yf : EuclideanSpace ℝ (Fin n)) (hyf : f yf = yf) :
    ∃ L : ℝ, Tendsto (fun k => ‖x k - yf‖) atTop (𝓝 L) := by sorry

end AndersonAccel.Safe
Source
Zhang, O'Donoghue, Boyd, SIAM J. Optim. 30 (2020), p. 3181, Section 4.1, Step 2
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph