Prove2Me

Theorem 3.5 — Algorithm GIN converges to a limit point near which ∥sk∥≤Γ(1−ηk)∥F(xk)∥\|s_k\|\le\Gamma(1-\eta_k)\|F(x_k)\|

Proved
GlobalInexactNewton.Backtracking.theorem_3_5

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

global-convergenceinexact-newtonp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let EE be a finite-dimensional real normed space and F:E→EF:E\to E continuously differentiable. Assume that Algorithm GIN with parameter t∈(0,1)t\in(0,1) does not break down, with iterates xkx_k, levels ηk\eta_k and steps sk=xk+1−xks_k=x_{k+1}-x_k. Let x∗x_* be a limit point of (xk)(x_k) for which there is a constant Γ\Gamma, independent of kk, with

∥sk∥≤Γ(1−ηk) ∥F(xk)∥(3.2)\|s_k\|\le\Gamma(1-\eta_k)\,\|F(x_k)\| \tag{3.2}

whenever xkx_k is sufficiently near x∗x_* and kk is sufficiently large. Then xk→x∗x_k\to x_*.

No invertibility of F′(x∗)F'(x_*) is assumed, and the theorem does not claim F(x∗)=0F(x_*)=0. It complements Theorem 3.3 and gives the convergence part of Theorem 5.2.

Formalization Note The paper says "sufficiently near" and "sufficiently large"; we state: there exist Γ∈R\Gamma\in\mathbb R, δ>0\delta>0 and KK such that (3.2) holds for every k≥Kk\ge K with ∥xk−x∗∥<δ\|x_k-x_*\|<\delta. Γ\Gamma is chosen before kk ("independent of kk").

Preamble
import Mathlib
import Definitions.Def_GlobalInexactNewton_Backtracking_Method
open Filter Topology
Formal statement
namespace GlobalInexactNewton.Backtracking

/-- Eisenstat–Walker (1994), p. 401, Theorem 3.5: assume Algorithm GIN does not break down. If
`x_*` is a limit point of `{x_k}` such that there is a `Γ` independent of `k` for which (3.2)
`‖s_k‖ ≤ Γ (1 - η_k) ‖F(x_k)‖` whenever `x_k` is sufficiently near `x_*` and `k` is sufficiently
large, then `x_k → x_*`. "Sufficiently near / large" is `∃ δ > 0, ∃ K`, after `∃ Γ`. No invertibility
of `F'(x_*)` is assumed. -/
theorem theorem_3_5 {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (F : E → E) (hF : ContDiff ℝ 1 F) (t : ℝ) (x : ℕ → E) (η : ℕ → ℝ)
    (hrun : IsGINRun F t x η) (xstar : E) (hlim : MapClusterPt xstar atTop x)
    (hΓ : ∃ Γ : ℝ, ∃ δ > 0, ∃ K : ℕ, ∀ k ≥ K, x k ∈ Metric.ball xstar δ →
      ‖x (k + 1) - x k‖ ≤ Γ * (1 - η k) * ‖F (x k)‖) :
    Tendsto x atTop (𝓝 xstar) := by sorry

end GlobalInexactNewton.Backtracking
Source
Eisenstat and Walker, Globally Convergent Inexact Newton Methods, SIAM J. Optim. 4(2) (1994), p. 401, Theorem 3.5
Human review

  • Endorsed by Shuze Chen · Oct 6, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 6, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph