Theorem 3.11 — forcing terms (2.25) give q-superlinear convergence

Assume the standing assumptions of §3.4 ($g$ twice continuously differentiable and strongly convex with constant $m>0$, $\nabla g$ $L_1$-Lipschitz, $\nabla^2 g$ $L_2$-Lipschitz, $h$ proper closed convex with domain $D$), let $x^\star$ be the optimal solution of $\min_x g(x)+h(x)$, and let $M>0$ satisfy $\nabla^2 g(x)\preceq MI$ for all $x$. There is $\delta>0$ with the following property. Consider any run of the inexact proximal Newton method with unit step lengths under the stopping condition (2.24), whose forcing terms are chosen by

with any first forcing term $\eta_0\in[0, m/2]$. If $\|x_0 - x^\star\| < \delta$, then $x_k\to x^\star$ q-superlinearly: $x_k\to x^\star$ and, for every $\varepsilon>0$, $\|x_{k+1}-x^\star\|\le\varepsilon\|x_k-x^\star\|$ for all sufficiently large $k$.

The forcing terms (2.25) need no tuning: they measure how well the previous model predicted the composite gradient step, and they make the subproblems be solved more accurately exactly when the iterates approach $x^\star$.

Formalization Note (2.25) does not define $\eta_0$; the theorem allows any $\eta_0 \in [0, m/2]$, the range (2.25) gives the later terms, and $\delta$ does not depend on $\eta_0$ or on the run. The forcing terms depend on the iterates, unlike in Theorem 3.10. When $G_{f/M}(x_{k-1}) = 0$ the quotient is $0$ in Lean; this happens only at $x_{k-1} = x^\star$.