Prove2Me

Corollary 3.4 — ∥Hk∥2≤(3((1+θˉ+τ)/τ)m−2)n−1/θˉm\|H_k\|_2\le(3((1+\bar\theta+\tau)/\tau)^m-2)^{n-1}/\bar\theta^m (3.8)

Proved
AndersonAccel.Safe.norm_inverse_windowB_le

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

anderson-accelerationmatrix-inverseoperator-normp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Under the assumptions of Lemma 3.3 (θˉ,τ∈(0,1)\bar\theta,\tau\in(0,1), max-memory m≥1m\ge1, mk≤mm_k\le m, well-defined updates, ∥yi∥2≤2∥si∥2\|y_i\|_2\le2\|s_i\|_2 and ∥s^i∥2≥τ∥si∥2\|\hat s_i\|_2\ge\tau\|s_i\|_2 on the window), the inverse Hk=Bk−1H_k=B_k^{-1} of the Powell-regularized matrix satisfies

∥Hk∥2 ≤ (3(1+θˉ+ττ)m−2)n−1/θˉ m.(3.8)\|H_k\|_2\ \le\ \Bigl(3\Bigl(\frac{1+\bar\theta+\tau}{\tau}\Bigr)^m-2\Bigr)^{n-1}\Big/\bar\theta^{\,m}.\qquad(3.8)

This is the uniform bound on the approximate inverse Jacobians that the global convergence proof needs for every accelerated step.

Formalization Note HkH_k is Ring.inverse of the window matrix, which is its true inverse by Lemma 3.2. nn is the dimension; for n=0n=0 the natural-number subtraction gives n−1=0n-1=0, which is harmless since then Hk=0H_k=0.

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

/-- Corollary 3.4, Eq. (3.8) (p. 3178). Under the hypotheses of Lemma 3.3,
`‖H‖ = ‖B⁻¹‖ ≤ (3((1 + θ̄ + τ)/τ)^m - 2)^{n-1} / θ̄^m`. -/
theorem norm_inverse_windowB_le {n : ℕ} (θbar τ : ℝ) (m : ℕ) (hθ0 : 0 < θbar) (hθ1 : θbar < 1)
    (hτ0 : 0 < τ) (hτ1 : τ < 1) (hm : 1 ≤ m)
    (s y : ℕ → EuclideanSpace ℝ (Fin n)) (mk : ℕ) (hmk : mk ≤ m)
    (hwd : ∀ i < mk, inner ℝ (windowShat s i) (s i) ≠ 0)
    (hy : ∀ i < mk, ‖y i‖ ≤ 2 * ‖s i‖)
    (hτs : ∀ i < mk, τ * ‖s i‖ ≤ ‖windowShat s i‖) :
    ‖Ring.inverse (windowB θbar s y mk)‖ ≤
      (3 * ((1 + θbar + τ) / τ) ^ m - 2) ^ (n - 1) / θbar ^ m := by sorry

end AndersonAccel.Safe
Source
Zhang, O'Donoghue, Boyd, SIAM J. Optim. 30 (2020), p. 3178, Corollary 3.4, Eq. (3.8)
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