Prove2Me

Solutions of VI(F,C)\mathrm{VI}(F, C) are exactly the zeros of the projected residual

Proved
SolodovSvaiterVI.Alg21.mem_viSol_iff_residual_eq_zero

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

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

Let CC be a nonempty closed convex subset of Rn\mathbb{R}^n and F:Rn→RnF : \mathbb{R}^n \to \mathbb{R}^n any map. Let SS be the solution set of VI(F,C)\mathrm{VI}(F, C) and r(x)=x−PC[x−F(x)]r(x) = x - P_C[x - F(x)] the projected residual. Then for every x∈Rnx \in \mathbb{R}^n,

x∈S  ⟺  r(x)=0.x \in S \iff r(x) = 0.

This is what makes r(xi)=0r(x^i) = 0 a valid stopping test in Algorithm 2.1, and it is how the convergence proof certifies that a limit point is a solution.

Formalization Note The paper assumes SS nonempty throughout; here only C≠∅C \neq \emptyset is assumed (it follows from S≠∅S \ne \emptyset and is what makes PCP_C well defined). No continuity of FF is needed.

Preamble
import Mathlib
import Definitions.Def_SolodovSvaiterVI_Alg21_viSol
import Definitions.Def_SolodovSvaiterVI_Alg21_residual
Formal statement
namespace SolodovSvaiterVI.Alg21

/-- Solodov–Svaiter, Section 2, p. 767: solutions of `VI(F, C)` coincide with the zeros of the
projected residual `r(x) = x − P_C[x − F(x)]`, i.e. `x ∈ S ⟺ r(x) = 0`. -/
theorem mem_viSol_iff_residual_eq_zero {n : ℕ}
    (F : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (C : Set (EuclideanSpace ℝ (Fin n))) (hCne : C.Nonempty) (hCc : IsClosed C)
    (hCcv : Convex ℝ C) (x : EuclideanSpace ℝ (Fin n)) :
    x ∈ viSol F C ↔ residual F C x = 0 := by sorry

end SolodovSvaiterVI.Alg21
Source
Solodov & Svaiter, A New Projection Method for Variational Inequality Problems, SIAM J. Control Optim. 37 (1999), p. 767, Section 2 (first paragraph)
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