Eq. (2.8): $\eta_i \|r(x^i)\| \to 0$ along Algorithm 2.1

Proved

SolodovSvaiterVI.Alg21.eq2_8_tendsto_eta_residual

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

p2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1projection-methodsvariational-inequalities

Let $C$ be a closed convex subset of $\mathbb{R}^n$ and $F : \mathbb{R}^n \to \mathbb{R}^n$ continuous. Assume the solution set $S$ of $\mathrm{VI}(F, C)$ is nonempty and condition (1.2) holds, and let $\gamma, \sigma \in (0,1)$ . Then for every sequence $(x^i)$ generated by Algorithm 2.1, with stepsizes $\eta_i = \gamma^{k_i}$ ,

\lim_{i \to \infty} \eta_i \|r(x^i)\| = 0. \tag{2.8}

This limit drives the final case analysis of the convergence proof: either the stepsizes stay away from zero along a subsequence, and then the residual vanishes along it, or the stepsizes tend to zero.

Formalization Note A run that stops at a solution is continued as a constant sequence (see IsAlg21Run); at such indices $r(x^i) = 0$ , so the term is $0$ whatever $k_i$ is, and the stall encoding does not change the content.

Preamble

import Mathlib
import Definitions.Def_SolodovSvaiterVI_Alg21_viSol
import Definitions.Def_SolodovSvaiterVI_Alg21_SatisfiesCond12
import Definitions.Def_SolodovSvaiterVI_Alg21_residual
import Definitions.Def_SolodovSvaiterVI_Alg21_IsAlg21Run

Formal statement

namespace SolodovSvaiterVI.Alg21

/-- Solodov–Svaiter, proof of Theorem 2.1, (2.8) (p. 770): along any sequence generated by
Algorithm 2.1, `lim_{i→∞} ηᵢ ‖r(xⁱ)‖ = 0` with `ηᵢ = γ^{kᵢ}`.

**Formalization Note.** At stalled indices (`r(xⁱ) = 0`) the term is `0`, so the stall
encoding of termination does not change the content. -/
theorem eq2_8_tendsto_eta_residual {n : ℕ}
    (F : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (C : Set (EuclideanSpace ℝ (Fin n))) (hCc : IsClosed C) (hCcv : Convex ℝ C)
    (hF : Continuous F) (hS : (viSol F C).Nonempty) (h12 : SatisfiesCond12 F C)
    (gamma sigma : ℝ) (hγ0 : 0 < gamma) (hγ1 : gamma < 1) (hσ0 : 0 < sigma) (hσ1 : sigma < 1)
    (x : ℕ → EuclideanSpace ℝ (Fin n)) (k : ℕ → ℕ) (hrun : IsAlg21Run F C gamma sigma x k) :
    Filter.Tendsto (fun i => gamma ^ (k i) * ‖residual F C (x i)‖) Filter.atTop (nhds 0) := by sorry

end SolodovSvaiterVI.Alg21

Source

Solodov & Svaiter, A New Projection Method for Variational Inequality Problems, SIAM J. Control Optim. 37 (1999), p. 770, proof of Theorem 2.1, Eq. (2.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

Eq. (2.8): ηi∥r(xi)∥→0\eta_i \|r(x^i)\| \to 0ηi​∥r(xi)∥→0 along Algorithm 2.1

Eq. (2.8): $\eta_i \|r(x^i)\| \to 0$ along Algorithm 2.1