Theorem 2.5, p. 6 — the forward-reflected-backward iterates converge weakly to a zero of A + B

Let $H$ be a real Hilbert space, $A:H\rightrightarrows H$ maximally monotone, and $B:H\to H$ monotone and $L$-Lipschitz with $L>0$, and suppose $(A+B)^{-1}(0)\ne\varnothing$. Fix $\varepsilon>0$ and step sizes $(\lambda_k)_{k\ge -1}\subseteq[\varepsilon,\tfrac{1-2\varepsilon}{2L}]$, and let $(x_k)_{k\ge-1}$ be generated from arbitrary $x_0,x_{-1}\in H$ by

Then $(x_k)$ converges weakly to a point of $(A+B)^{-1}(0)$: there is $\bar x$ with $0\in A(\bar x)+B(\bar x)$ and

This is the main convergence result for the forward-reflected-backward method: one forward evaluation of $B$ and one resolvent of $A$ per iteration suffice, with $B$ only monotone and Lipschitz (not cocoercive).

Formalization Note. The resolvent is not constructed: the iteration is driven by a family $J$ with $J(\gamma)=J_{\gamma A}$ for every $\gamma>0$, given as the hypothesis that $\gamma^{-1}(w-J(\gamma)w)\in A(J(\gamma)w)$ for all $w$. The paper's sequences start at $x_{-1}$ and $\lambda_{-1}$; in Lean x j is $x_{j-1}$ and lam j is $\lambda_{j-1}$, so a statement about $x_{k+1},x_k,x_{k-1},\lambda_k,\lambda_{k-1}$ is stated about x (k+2), x (k+1), x k, lam (k+1), lam k. Maximal monotonicity of $A$ is kept as a hypothesis alongside the resolvent family. $L>0$ is assumed because the step range divides by $L$. The step range constrains every $\lambda_j$, $j\ge-1$.