§6, p. 410 — Algorithm INB is Algorithm MR with the backtracking curve (6.1)

Proved

GlobalInexactNewton.Backtracking.inb_isMRRun

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

backtrackinginexact-newtonp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $E$ be a real normed space and $F:E\to E$ . Consider a run of Algorithm INB with initial levels $\bar\eta_k$ and initial inexact Newton steps $\bar s_k$ , and define the backtracking curve

\sigma_k(\eta)=\frac{1-\eta}{1-\bar\eta_k}\,\bar s_k,\qquad\bar\eta_k\le\eta\le1. \tag{6.1}

Then:

the same data, with $\sigma_k$ in place of the curves, is a run of Algorithm MR (in particular $\sigma_k$ satisfies (5.1));
every step visited by the while-loop of Algorithm INB is $\sigma_k$ at the corresponding level: if the loop has produced $s_k$ and $\eta_k$ after any number of passes, then $s_k=\sigma_k(\eta_k)$ .

This identification is how Theorem 6.1 for INB is derived from Theorem 5.2 for MR.

Formalization Note Part 2 is stated for every loop index $j$ : $s^{(j)}=\frac{1-\eta^{(j)}}{1-\bar\eta_k}\bar s_k$ . No differentiability or finite dimension is needed, so neither is assumed.

Preamble

import Mathlib
import Definitions.Def_GlobalInexactNewton_Backtracking_Method
open Filter Topology

Formal statement

namespace GlobalInexactNewton.Backtracking

/-- Eisenstat–Walker (1994), §6, after (6.1), p. 410: Algorithm INB is a special case of
Algorithm MR. With the backtracking curve (6.1) `σ_k(η) = ((1 - η)/(1 - η̄_k)) s̄_k`, every run of
Algorithm INB is a run of Algorithm MR with the same data, and every step visited by the
while-loop is `σ_k` at the corresponding level: `s_k = σ_k(η_k)` throughout the loop. -/
theorem inb_isMRRun {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (F : E → E) (ηmax t θmin θmax : ℝ) (x : ℕ → E) (ηbar : ℕ → ℝ) (sbar : ℕ → E)
    (θ : ℕ → ℕ → ℝ) (m : ℕ → ℕ) (hrun : IsINBRun F ηmax t θmin θmax x ηbar sbar θ m) :
    IsMRRun F ηmax t θmin θmax x ηbar (fun k η => ((1 - η) / (1 - ηbar k)) • sbar k) θ m ∧
      ∀ k j, trialStep (sbar k) (θ k) j =
        ((1 - trialLevel (ηbar k) (θ k) j) / (1 - ηbar k)) • sbar k := by sorry

end GlobalInexactNewton.Backtracking

Source

Eisenstat and Walker, Globally Convergent Inexact Newton Methods, SIAM J. Optim. 4(2) (1994), §6, after (6.1), p. 410

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