Prove2Me

Theorem 3.2, p. 5 — every run of the projected reflected gradient method converges weakly to a solution of the monotone VI

Proved
ProjReflGrad.Weak.theorem_3_2

by mikedeng1 · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1projection-methodvariational-inequalityweak-convergence

Let HH be a real Hilbert space, C⊆HC\subseteq H closed and convex, and F:H→HF:H\to H a mapping such that

  1. (C1) the solution set SS of the variational inequality ⟨F(x∗),x−x∗⟩≥0\langle F(x^*),x-x^*\rangle\ge0 for all x∈Cx\in C is nonempty;
  2. (C2) FF is monotone on HH;
  3. (C3) FF is Lipschitz continuous on HH with a constant L>0L>0.

Let 0<λ<(2−1)/L0<\lambda<(\sqrt2-1)/L and let (xn),(yn)(x_n),(y_n) be generated by the projected reflected gradient method (Algorithm 3.1): x0=y0∈Hx_0=y_0\in H arbitrary and

xn+1=PC(xn−λF(yn)),yn+1=2xn+1−xn.x_{n+1}=P_C\big(x_n-\lambda F(y_n)\big),\qquad y_{n+1}=2x_{n+1}-x_n .

Then there is x∗∈Sx^*\in S with

xn⇀x∗(n→∞).x_n\rightharpoonup x^*\qquad(n\to\infty).

This is the main convergence result of the paper: the method needs one projection and one evaluation of FF per iteration, and still converges under the same assumptions as the extragradient method.

Formalization Note. Weak convergence is stated as ⟨xn,v⟩→⟨x∗,v⟩\langle x_n,v\rangle\to\langle x^*,v\rangle for every v∈Hv\in H. The run predicate has no stopping rule (a stopped run continues as a constant sequence). x0x_0 is not required to lie in CC.

Preamble
import Mathlib
import Definitions.Def_ProjReflGrad_Weak_Setting
Formal statement
namespace ProjReflGrad.Weak

/-- Theorem 3.2 (Malitsky 2015, p. 5): under (C1)–(C3) and `0 < λ < (√2 - 1)/L`, every sequence
`(x_n)` generated by Algorithm 3.1 converges weakly to a solution of (1.1). -/
theorem theorem_3_2 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (C : Set H) (hCcl : IsClosed C) (hCcv : Convex ℝ C) (F : H → H) (L lam : ℝ)
    (hC1 : (solSet C F).Nonempty) (hC2 : IsMonotoneMap F) (hL : 0 < L) (hC3 : IsLipschitzMap F L)
    (hlam0 : 0 < lam) (hlam1 : lam < (Real.sqrt 2 - 1) / L)
    (x y : ℕ → H) (hrun : IsPRGRun C F lam x y) :
    ∃ xs ∈ solSet C F, IsWeakLimit x xs := by sorry

end ProjReflGrad.Weak
Source
Malitsky, Projected Reflected Gradient Methods for Monotone Variational Inequalities, arXiv:1502.04968v1, p. 5, Theorem 3.2
Human review

  • Endorsed by Shuze Chen · Oct 9, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 9, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph