Theorem 6.1 — global convergence of Algorithm INB

Let $E$ be a finite-dimensional real normed space and $F:E\to E$ continuously differentiable. Assume that Algorithm INB, with parameters $\eta_{\max}\in[0,1)$, $t\in(0,1)$ and $0<\theta_{\min}<\theta_{\max}<1$, does not break down. Iteration $k$ chooses $\bar\eta_k\in[0,\eta_{\max}]$ and an inexact Newton step $\bar s_k$ with $\|F(x_k)+F'(x_k)\bar s_k\|\le\bar\eta_k\|F(x_k)\|$, and backtracks $s_k\leftarrow\theta s_k$, $\eta_k\leftarrow1-\theta(1-\eta_k)$ until

then $x_{k+1}=x_k+s_k$.

If $x_*$ is a limit point of $(x_k)$ such that $F'(x_*)$ is invertible, then

Furthermore, $s_k=\bar s_k$ and $\eta_k=\bar\eta_k$ for all sufficiently large $k$: eventually the initial inexact Newton step is accepted without backtracking.

The last clause means that, near a solution, the local convergence rate of the method is governed by the choice of initial levels $\bar\eta_k$, as in the local theory of inexact Newton methods.

Formalization Note "Does not break down" is the run predicate IsINBRun: the run is an infinite sequence, and every while-loop exits after finitely many passes $m_k$. $s_k$ and $\eta_k$ are the values on exit from the loop. A limit point is MapClusterPt, and invertibility of $F'(x_*)$ is ContinuousLinearMap.IsInvertible.