Theorem 3.3, p. 6 — under strong monotonicity every run of the projected reflected gradient method converges R-linearly to the solution

Proved

ProjReflGrad.Linear.theorem_3_3

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

linear-convergencep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1projection-methodstrongly-monotonevariational-inequality

Let $H$ be a real Hilbert space, $C\subseteq H$ closed and convex, and $F:H\to H$ . Assume

(C1) the variational inequality (1.1) — find $x^*\in C$ with $\langle F(x^*),x-x^*\rangle\ge0$ for all $x\in C$ — has a solution;
(C2*) $F$ is strongly monotone: $\langle F(x)-F(y),x-y\rangle\ge m\|x-y\|^2$ for all $x,y\in H$ , with $m>0$ ;
(C3) $F$ is $L$ -Lipschitz on $H$ with $L>0$ .

Let $0<\lambda<(\sqrt2-1)/L$ and let $(x_n),(y_n)$ be generated by Algorithm 3.1 from any $x_0=y_0\in H$ :

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

Then $(x_n)$ converges to the solution $z$ of (1.1) at least R-linearly: there exist $\gamma\in(0,1)$ and $M>0$ such that

\|x_n-z\|\ \le\ M\gamma^n\qquad\text{for every } n\ge0 .

The solution is unique under (C2*), so the conclusion is about the solution. The rate matches the R-linear rate known for the extragradient method, while the projected reflected gradient method needs only one projection and one evaluation of $F$ per iteration.

Formalization Note. The paper's "converges at least R-linearly" is made explicit by the last display of its proof, $\|x_n-z\|^2\le\gamma^nM$ for $n>0$ ; the Lean statement takes square roots and enlarges $M$ to cover $n=0$ , giving domination of $\|x_n-z\|$ by a geometric sequence with ratio strictly between $0$ and $1$ . The conclusion is stated for every $z\in S$ , which by uniqueness is the solution. The starting point $x_0$ need not lie in $C$ . The projection $P_C$ is the metric projection (closed, convex, nonempty $C$ in a complete space).

Preamble

import Mathlib
import Definitions.Def_ProjReflGrad_Linear_Setting

Formal statement

namespace ProjReflGrad.Linear

/-- Theorem 3.3 (Malitsky 2015, p. 6): assume (C1), (C2*) with modulus `m > 0` and (C3) with
`L > 0`, and `0 < λ < (√2 - 1)/L`. Then every run `(x_n)` of Algorithm 3.1 converges to the
solution `z` of (1.1) at least R-linearly: there are `γ ∈ (0, 1)` and `M > 0` with
`‖x_n - z‖ ≤ Mγⁿ` for every `n`. -/
theorem theorem_3_3 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (C : Set H) (hCcl : IsClosed C) (hCcv : Convex ℝ C) (F : H → H) (L lam m : ℝ)
    (hC1 : (ProjReflGrad.Weak.solSet C F).Nonempty) (hm : 0 < m) (hC2s : IsStronglyMonotoneMap F m)
    (hL : 0 < L) (hC3 : ProjReflGrad.Weak.IsLipschitzMap F L)
    (hlam0 : 0 < lam) (hlam1 : lam < (Real.sqrt 2 - 1) / L)
    (x y : ℕ → H) (hrun : ProjReflGrad.Weak.IsPRGRun C F lam x y) :
    ∀ z ∈ ProjReflGrad.Weak.solSet C F, ∃ γ M : ℝ, 0 < γ ∧ γ < 1 ∧ 0 < M ∧ ∀ n : ℕ, ‖x n - z‖ ≤ M * γ ^ n := by sorry

end ProjReflGrad.Linear

Source

Malitsky, Projected Reflected Gradient Methods for Monotone Variational Inequalities, arXiv:1502.04968v1, p. 6, Theorem 3.3 (proof pp. 6–7)

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