Theorem 3.2 — R-linearly convergent iterates eventually satisfy the nonmonotone condition (1.4)

Proved

NonmonotoneLS.RLinear.eventual_sufficient_decrease

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

line-searchlinear-convergencenonmonotonep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1strong-convexity

Let $f : \mathbb{R}^n \to \mathbb{R}$ be continuously differentiable and let $x^*$ be a minimizer of $f$ . Let $x_k$ , $d_k$ , $\alpha_k$ ( $k = 0, 1, \dots$ ) be any sequences with $x_{k+1} = x_k + \alpha_k d_k$ (not necessarily a run of the algorithm), and write $g_k = \nabla f(x_k)$ . Assume:

$f(x_k)$ converges R-linearly to $f(x^*)$ : there are $\theta \in (0, 1)$ and $c$ with $f(x_k) - f(x^*) \le c\,\theta^k$ for all $k$ ;
the $x_k$ lie in a closed, bounded, convex set $K$ on which $f$ satisfies (3.1) with a constant $\gamma > 0$ (for all $x, y \in K$ ) and $\nabla f$ is Lipschitz continuous with constant $L$ ;
the direction assumption holds: there are $c_1, c_2 > 0$ with $g_k^{\mathsf T} d_k \le -c_1\|g_k\|^2$ and $\|d_k\| \le c_2\|g_k\|$ for all sufficiently large $k$ ;
$0 < \alpha_k \le \mu$ for all $k$ ;
$C_k$ is given by the recursion (1.6) with weights $\eta_k \in [\eta_{\min}, \eta_{\max}]$ , $0 \le \eta_{\min} \le \eta_{\max} \le 1$ , and $\eta_{\min} > \theta$ .

Then for every $\delta \in (0, 1)$ , condition (1.4),

f(x_k + \alpha_k d_k) \le C_k + \delta \alpha_k g_k^{\mathsf T} d_k,

holds for all sufficiently large $k$ .

So with averaging weights close enough to 1, the sufficient-decrease test (1.4) of the nonmonotone line search is eventually passed by the steps of any R-linearly convergent descent method of this kind.

Formalization Note. The statement follows the page. $\delta$ is the parameter of (1.4), arbitrary in $(0,1)$ . The printed proof applies (3.1) and the Lipschitz bound with $y = x^*$ , which need not lie in $K$ ; a cluster point of the $x_k$ in the compact set $K$ is also a minimizer and can take its place, so the statement is unaffected. The proof's limit $\Phi$ of $\varphi_k$ can likewise be replaced by a positive lower bound $\varphi_{k_0}$ . If $c \le 0$ the hypothesis forces $f(x_k) = f(x^*)$ for all $k$ .

Preamble

import Mathlib
import Definitions.Def_NonmonotoneLS_Shared_Params
import Definitions.Def_NonmonotoneLS_Shared_Cost
import Definitions.Def_NonmonotoneLS_Shared_Steps
import Definitions.Def_NonmonotoneLS_RLinear_Run
import Definitions.Def_NonmonotoneLS_RLinear_Regions
import Definitions.Def_NonmonotoneLS_RLinear_Constants

open scoped InnerProductSpace NNReal
open Filter

Formal statement

namespace NonmonotoneLS.RLinear

/-- Theorem 3.2 (p. 1051): let `x*` minimize `f` and let `x_{k+1} = x_k + α_k d_k` be any sequence
with `f(x_k) - f(x*) ≤ cθ^k`, `θ ∈ (0, 1)`, lying in a closed, bounded, convex set `K` on which
(3.1) holds with constant `γ` and `∇f` is `L`-Lipschitz, whose directions satisfy (2.4)–(2.5) for
all sufficiently large `k`, and whose steps satisfy `0 < α_k ≤ μ`. If `C_k` is given by (1.6) with
`η_k ∈ [η_min, η_max] ⊆ [0, 1]` and `η_min > θ`, then for every `δ ∈ (0, 1)` the condition (1.4),
`f(x_k + α_k d_k) ≤ C_k + δ α_k ∇f(x_k) d_k`, holds for all sufficiently large `k`. -/
theorem eventual_sufficient_decrease {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (hf : ContDiff ℝ 1 f) (xstar : EuclideanSpace ℝ (Fin n)) (hmin : ∀ y, f xstar ≤ f y)
    (x d : ℕ → EuclideanSpace ℝ (Fin n)) (α η : ℕ → ℝ)
    (hupd : ∀ k, x (k + 1) = x k + α k • d k)
    (θ c : ℝ) (hθ0 : 0 < θ) (hθ1 : θ < 1) (hRlin : ∀ k, f (x k) - f xstar ≤ c * θ ^ k)
    (K : Set (EuclideanSpace ℝ (Fin n))) (hKc : IsClosed K) (hKb : Bornology.IsBounded K)
    (hKconv : Convex ℝ K) (hxK : ∀ k, x k ∈ K)
    (γ : ℝ) (hγ : 0 < γ)
    (hscK : ∀ u ∈ K, ∀ v ∈ K,
      f v + ⟪gradient f v, u - v⟫_ℝ + 1 / (2 * γ) * ‖u - v‖ ^ 2 ≤ f u)
    (L : ℝ≥0) (hLip : LipschitzOnWith L (gradient f) K)
    (hdir : ∃ c₁ c₂ : ℝ, 0 < c₁ ∧ 0 < c₂ ∧ ∀ᶠ k in atTop,
      ⟪gradient f (x k), d k⟫_ℝ ≤ -c₁ * ‖gradient f (x k)‖ ^ 2 ∧
        ‖d k‖ ≤ c₂ * ‖gradient f (x k)‖)
    (μ : ℝ) (hα : ∀ k, 0 < α k ∧ α k ≤ μ)
    (ηmin ηmax : ℝ) (hηmin0 : 0 ≤ ηmin) (hηle : ηmin ≤ ηmax) (hηmax1 : ηmax ≤ 1)
    (hη : ∀ k, η k ∈ Set.Icc ηmin ηmax) (hθη : θ < ηmin)
    (δ : ℝ) (hδ0 : 0 < δ) (hδ1 : δ < 1) :
    ∀ᶠ k in atTop,
      f (x k + α k • d k) ≤ Shared.costC f x η k + δ * α k * ⟪gradient f (x k), d k⟫_ℝ := by sorry

end NonmonotoneLS.RLinear

Source

Zhang, Hager, A Nonmonotone Line Search Technique and Its Application to Unconstrained Optimization, SIAM J. Optim. 14 (2004), p. 1051, Theorem 3.2

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. $n\in\mathbb{N}$ , a $C^1$ function $f:\mathbb{R}^n\to\mathbb{R}$ with gradient $\nabla f$ , sequences $(x_k)$ and $(d_k)$ in $\mathbb{R}^n$ , and real sequences $(\alpha_k)$ and $(\eta_k)$ . This theorem does not use a parameter bundle or a run. Instead it has the following hypotheses.

Hypotheses.

$x^*$ is a global minimizer: $f(x^*)\le f(y)$ for all $y$ .
$x_{k+1}=x_k+\alpha_kd_k$ for every $k$ .
There are reals $\theta$ and $c$ with $0<\theta<1$ and $f(x_k)-f(x^*)\le c\,\theta^k$ for every $k$ . Since the left side is $\ge0$ and $\theta^k > 0$ , this forces $c\ge0$ .
$K\subseteq\mathbb{R}^n$ is closed, bounded and convex, and $x_k\in K$ for every $k$ .
$\gamma>0$ , and for all $u,v\in K$ :

f(v)+\langle\nabla f(v),u-v\rangle+\frac{1}{2\gamma}\|u-v\|^2\le f(u).

$L\ge0$ is a nonnegative real. $L=0$ is not excluded. $\nabla f$ is $L$ -Lipschitz on $K$ .
There exist $c_1>0$ and $c_2>0$ such that, for all sufficiently large $k$ (not necessarily all $k$ ):

\langle\nabla f(x_k),d_k\rangle\le -c_1\|\nabla f(x_k)\|^2\quad\text{and}\quad\|d_k\|\le c_2\|\nabla f(x_k)\|.

$\mu$ is real with $0<\alpha_k\le\mu$ for every $k$ . This forces $\mu>0$ .
Reals $\eta_{\min},\eta_{\max}$ satisfy $0\le\eta_{\min}\le\eta_{\max}\le1$ , and $\eta_k\in[\eta_{\min},\eta_{\max}]$ for every $k$ .
$\theta<\eta_{\min}$ . This forces $\eta_{\min}>0$ .
$\delta$ is real with $0<\delta<1$ .

Conclusion. For all sufficiently large $k$ :

f(x_k+\alpha_kd_k)\le C_k+\delta\,\alpha_k\,\langle\nabla f(x_k),d_k\rangle.

Here $C_k$ is Shared.costC applied to $f$ , $x$ , $\eta$ and $k$ . That definition is not shown here. By hypothesis 2, the left side equals $f(x_{k+1})$ .

Degenerate cases:

$\eta_{\max}=1$ is permitted.
$c=0$ is permitted. Then every $x_k$ is a minimizer.
For $n=0$ , all points coincide and all gradients are $0$ . The conclusion then reads $f(\text{pt})\le C_k$ for all large $k$ , which depends on the unseen definition of $C_k$ .
If $K$ is a single point, all $x_k$ equal it. Hypothesis 7 then forces $d_k=0$ eventually whenever the gradient there is $0$ .

Human review

Endorsed by Shuze Chen · Sep 28, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 28, 2026
Confirmed by the mission captain (proposal self-audit).

View graph