Prove2Me

Eq. (4.3) — the iterates stay within ∥x0−y∥2+CDUˉ∑i(i+1)−(1+ϵ)\|x^0-y\|_2+CD\bar U\sum_i(i+1)^{-(1+\epsilon)} of every fixed point

Proved
AndersonAccel.Safe.dist_bounded

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

anderson-accelerationboundednessfixed-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). Let yy be any fixed point of ff, Uˉ=∥g(x0)∥2\bar U=\|g(x^0)\|_2, and

C=(3(1+θˉ+ττ)m−2)n−1/θˉ mC=\Bigl(3\Bigl(\frac{1+\bar\theta+\tau}{\tau}\Bigr)^m-2\Bigr)^{n-1}\Big/\bar\theta^{\,m}

the bound (3.8). Then for every k≥0k\ge0

∥xk−y∥2 ≤ ∥x0−y∥2+CDUˉ∑i=0∞(i+1)−(1+ϵ).\|x^k-y\|_2\ \le\ \|x^0-y\|_2+CD\bar U\sum_{i=0}^\infty(i+1)^{-(1+\epsilon)}.

In particular the iterates are bounded. The right-hand side is the constant EE of the paper.

Formalization Note The paper writes "some constant CC independent of the iteration count" with ∥Hki∥2≤C\|H_{k_i}\|_2\le C by Corollary 3.5; the explicit bound (3.8) is used for CC. The series is the tsum of (i+1)−(1+ϵ)(i+1)^{-(1+\epsilon)} (real power), which converges since ϵ>0\epsilon>0. 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

/-- Eq. (4.3) (p. 3180). For every fixed point `y`,
`‖x^k - y‖ ≤ ‖x^0 - y‖ + C D Ū ∑_{i ≥ 0} (i + 1)^{-(1+ε)}` for all `k`, where `C` is the bound (3.8). -/
theorem dist_bounded {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) :
    ∀ k, ‖x k - yf‖ ≤ ‖x 0 - yf‖ +
      (3 * ((1 + θbar + τ) / τ) ^ m - 2) ^ (n - 1) / θbar ^ m * D * ‖residual f (x 0)‖ *
        ∑' i : ℕ, ((i : ℝ) + 1) ^ (-(1 + ε)) := by sorry

end AndersonAccel.Safe
Source
Zhang, O'Donoghue, Boyd, SIAM J. Optim. 30 (2020), p. 3180, Section 4.1, Step 1, Eq. (4.3)
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