Prove2Me

Theorem 2.1 — the hyperplane projection method converges to a solution of VI(F,C)\mathrm{VI}(F, C)

Proved
SolodovSvaiterVI.Alg21.theorem2_1_converges_to_solution

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

global-convergencep2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1projection-methodsvariational-inequalities

Let CC be a closed convex subset of Rn\mathbb{R}^n and F:Rn→RnF : \mathbb{R}^n \to \mathbb{R}^n continuous. Suppose that the solution set SS of the variational inequality VI(F,C)\mathrm{VI}(F, C) is nonempty and that condition (1.2) holds:

⟨F(x),x−x∗⟩≥0for all x∈C and all x∗∈S.\langle F(x), x - x^* \rangle \ge 0 \qquad \text{for all } x \in C \text{ and all } x^* \in S.

Let γ,σ∈(0,1)\gamma, \sigma \in (0,1). Then every sequence (xi)(x^i) generated by Algorithm 2.1 converges to a solution of VI(F,C)\mathrm{VI}(F, C): there is x^∈S\hat x \in S with

lim⁡i→∞xi=x^.\lim_{i \to \infty} x^i = \hat x.

The theorem requires neither Lipschitz continuity nor monotonicity of FF; condition (1.2) holds for pseudomonotone maps and more generally. Each iteration of the method needs only one projection onto CC and one onto C∩HiC \cap H_i.

Formalization Note Rn\mathbb{R}^n is EuclideanSpace ℝ (Fin n); projections are projOnto, which is the true projection on the nonempty closed convex sets the algorithm uses. A run that stops at a solution (r(xi)=0r(x^i) = 0) is continued as a constant sequence (the stall encoding of IsAlg21Run), so finitely terminating runs are included and converge trivially. The whole sequence is required to converge to a single solution.

Preamble
import Mathlib
import Definitions.Def_SolodovSvaiterVI_Alg21_viSol
import Definitions.Def_SolodovSvaiterVI_Alg21_SatisfiesCond12
import Definitions.Def_SolodovSvaiterVI_Alg21_IsAlg21Run
Formal statement
namespace SolodovSvaiterVI.Alg21

/-- Theorem 2.1 of Solodov–Svaiter (p. 769): let `C ⊆ ℝⁿ` be closed and convex and `F`
continuous; suppose the solution set `S` of `VI(F, C)` is nonempty and condition (1.2) holds.
Then any sequence `{xⁱ}` generated by Algorithm 2.1 (parameters `γ, σ ∈ (0, 1)`) converges to
a solution of `VI(F, C)`.

**Formalization Note.** A run that stops at a solution is continued as a constant sequence
(stall encoding, see `IsAlg21Run`); `P_K` is `projOnto K`. -/
theorem theorem2_1_converges_to_solution {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) :
    ∃ xs ∈ viSol F C, Filter.Tendsto x Filter.atTop (nhds xs) := by sorry

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