Theorem 2.9, p. 8 — for strongly monotone A the forward-reflected-backward method converges R-linearly to the unique zero of A + B

Let $H$ be a real Hilbert space. Let $A:H\rightrightarrows H$ be maximally monotone and $m$-strongly monotone ($m>0$, $\langle x-y,u-v\rangle\ge m\|x-y\|^2$ whenever $u\in A(x)$, $v\in A(y)$), with resolvents $J_{\gamma A}=(I+\gamma A)^{-1}$, $\gamma>0$. Let $B:H\to H$ be monotone and $L$-Lipschitz, $L>0$, and suppose $(A+B)^{-1}(0)\neq\varnothing$. Let $\lambda\in(0,\tfrac1{2L})$. Given $x_0,x_{-1}\in H$, define $(x_k)$ by

Then $(A+B)^{-1}(0)=\{\bar x\}$ for a single point $\bar x$, and $(x_k)$ converges R-linearly to $\bar x$: there are $q\in(0,1)$ and $M\in\mathbb R$ such that

This is the linear-convergence result for the forward-reflected-backward method: when the set-valued part $A$ is strongly monotone, the method needs neither cocoercivity of $B$ nor a second forward evaluation to converge at a geometric rate.

Formalization Note. Indices are shifted by one: Lean's x k is $x_{k-1}$ (so x 0 $=x_{-1}$), which only rescales $M$; the bound covers the initial point $x_{-1}$ as well. The resolvent is a hypothesis: J is any family with J γ a resolvent of $A$ for every $\gamma>0$; for maximally monotone $A$ such a family exists (Minty) and is unique. "R-linearly" is not defined in the paper; it is stated as the existence of a geometric bound $Mq^k$ with $q<1$, as the proof gives. $L>0$ is pinned because the step range divides by $L$.