Prove2Me

Lemma 3.3 — ∥Bk∥2≤3((1+θˉ+τ)/τ)m−2\|B_k\|_2\le 3((1+\bar\theta+\tau)/\tau)^m-2

Proved
AndersonAccel.Safe.norm_windowB_le

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

anderson-accelerationoperator-normp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1rank-one-update

Let θˉ,τ∈(0,1)\bar\theta,\tau\in(0,1) and let m≥1m\ge1 be the max-memory. Let s0,…,smk−1s_0,\dots,s_{m_k-1} and y0,…,ymk−1y_0,\dots,y_{m_k-1} be vectors in Rn\mathbb R^n with mk≤mm_k\le m, and let Bk=BmkB_k=B^{m_k} be the Powell-regularized matrix of (3.5). Assume

  1. every update is well-defined: s^iTsi≠0\hat s_i^Ts_i\ne0;
  2. ∥yi∥2≤2∥si∥2\|y_i\|_2\le2\|s_i\|_2;
  3. ∥s^i∥2≥τ∥si∥2\|\hat s_i\|_2\ge\tau\|s_i\|_2,

for i=0,…,mk−1i=0,\dots,m_k-1. Then, in the induced ℓ2\ell_2 operator norm,

∥Bk∥2 ≤ 3(1+θˉ+ττ)m−2.\|B_k\|_2\ \le\ 3\Bigl(\frac{1+\bar\theta+\tau}{\tau}\Bigr)^{m}-2.

The bound is uniform in the iteration and depends only on θˉ\bar\theta, τ\tau and the max-memory mm; together with Lemma 3.2 it controls the inverse matrices used by the algorithm.

Formalization Note The paper assumes "mkm_k is chosen by rule (3.7)" and uses it, in the first line of its proof, only through ∥s^i∥2≥τ∥si∥2\|\hat s_i\|_2\ge\tau\|s_i\|_2 and mk≤mm_k\le m; these two consequences are the hypotheses here. The connection with rule (3.7) along the algorithm is Corollary 3.5. The exponent is the max-memory mm, not mkm_k.

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

/-- Lemma 3.3 (p. 3178). Under the hypotheses of Lemma 3.2, if `‖y_i‖ ≤ 2‖s_i‖` on the window and
the window satisfies what rule (3.7) guarantees (`‖ŝ_i‖ ≥ τ‖s_i‖` and `m_k ≤ m`), then
`‖B‖ ≤ 3((1 + θ̄ + τ)/τ)^m - 2` in the operator 2-norm. -/
theorem norm_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‖) :
    ‖windowB θbar s y mk‖ ≤ 3 * ((1 + θbar + τ) / τ) ^ m - 2 := by sorry

end AndersonAccel.Safe
Source
Zhang, O'Donoghue, Boyd, SIAM J. Optim. 30 (2020), p. 3178, Lemma 3.3 (rule (3.7), p. 3177)
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