TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Fletcher–Reeves has vanishing gradient liminf under strong Wolfe

Statement

Let $D \subseteq R^{n}$ be open, $f : D \to R$ be $C^{1}$ , and $x_{0} \in D$ . Let $L_{0} = {x \in D : f (x) \leq f (x_{0})}$ , and suppose $f$ is bounded below on $L_{0}$ . Suppose an open set $N \subseteq D$ contains every trial segment $x_{k} + [0, t_{k}] d_{k}$ and, for one $L > 0$ , $∥ \nabla f (u) - \nabla f (v) ∥_{2} \leq L ∥ u - v ∥_{2} (u, v \in N) .$ Consider an infinite sequence following the FR recurrence $d_{0} = - g_{0}$ , $d_{k} = - g_{k} + (∥ g_{k} ∥_{2}^{2} / ∥ g_{k - 1} ∥_{2}^{2}) d_{k - 1}$ from Fletcher–Reeves and safeguarded Polak–Ribière nonlinear conjugate gradients, with $g_{k} = \nabla f (x_{k}) \neq 0$ , feasible updates $x_{k + 1} = x_{k} + t_{k} d_{k}$ , and every $t_{k}$ a strong Wolfe step for constants $0 < c_{1} < c_{2} < 1 / 2$ . Then ${lim inf}_{k \to \infty} ∥ g_{k} ∥_{2} = 0.$ This is a theorem about the infinite recurrence and successful updates, not an infinite execution of the finite- $K$ algorithm. The conclusion is a liminf statement; it does not assert $∥ g_{k} ∥_{2} \to 0$ .

Facts & Assumptions

Given: The domain, objective, lower bound, uniform Lipschitz-gradient neighborhood, FR recurrence, and successful strong Wolfe steps in the Statement.

[F1]

Fletcher–Reeves descent and direction-growth bound: with $δ = (1 - 2 c_{2}) / (1 - c_{2})$ and $C_{3} = (1 + c_{2}) / (1 - c_{2})$ , $q_{k} = - g_{k}^{T} d_{k} / ∥ g_{k} ∥_{2}^{2}$ satisfies $q_{k} \geq δ > 0$ and $∥ d_{k} ∥_{2}^{2} \leq C_{3} ∥ g_{k} ∥_{2}^{4} \sum_{j = 0}^{k} ∥ g_{j} ∥_{2}^{- 2}$ .

[F2]

Wolfe and strong Wolfe line-search conditions: every strong Wolfe step is a Wolfe step.

[F3]

Wolfe steps imply the Zoutendijk summability condition: under the stated lower-bound, smoothness, feasibility, descent, and Wolfe hypotheses, $\sum_{k \geq 0} \cos^{2} θ_{k} ∥ g_{k} ∥_{2}^{2} < \infty$ .

Proof

Given: The hypotheses and notation in the Statement.

1.1givenF1F2F3

By [F1], every $d_{k}$ is a strict descent direction. By [F2], the accepted strong Wolfe steps are Wolfe steps. The hypotheses therefore match [F3], so $\sum_{k = 0}^{\infty} \cos^{2} θ_{k} ∥ g_{k} ∥_{2}^{2} < \infty .$

1.2givenchoosealgebra

Suppose instead that ${lim inf}_{k} ∥ g_{k} ∥_{2} > 0$ . Choose $γ > 0$ and an integer $K \geq 1$ such that $∥ g_{j} ∥_{2} \geq γ$ for every $j \geq K$ . Then for $k \geq K$ , $S_{k} : = \sum_{j = 0}^{k} \frac{1}{∥ g_{j} ∥_{2}^{2}} \leq k (\sum_{j = 0}^{K - 1} \frac{1}{∥ g_{j} ∥_{2}^{2}} + γ^{- 2}) = : A_{0} k,$ where $A_{0} > 0$ .

2.1F1step 1.1step 1.2algebracontradiction∎

From [F1], $∥ d_{k} ∥_{2}^{2} \leq C_{3} A_{0} k ∥ g_{k} ∥_{2}^{4}$ . Since $q_{k} = - g_{k}^{T} d_{k} / ∥ g_{k} ∥_{2}^{2}$ and $\cos θ_{k} = - g_{k}^{T} d_{k} / (∥ g_{k} ∥_{2} ∥ d_{k} ∥_{2})$ , $\cos^{2} θ_{k} ∥ g_{k} ∥_{2}^{2} = \frac{(g_{k}^{T} d_{k})^{2}}{∥ d_{k} ∥_{2}^{2}} = \frac{q_{k}^{2} ∥ g_{k} ∥_{2}^{4}}{∥ d_{k} ∥_{2}^{2}} \geq \frac{δ^{2}}{C_{3} A_{0} k} .$ The harmonic series diverges, contradicting step 1.1. Thus the supposition is false and ${lim inf}_{k} ∥ g_{k} ∥_{2} = 0$ .

Remarks

The source proofs use bounded initial level sets to obtain bounded gradients. The argument here does not: the local direction-growth estimate in [F1] is normalized by the current gradient and leads directly to the harmonic contradiction under the hypotheses stated above.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jorge Nocedal and Stephen J. Wright, Numerical Optimization, second edition (standard reference, not scraped)
Jean Charles Gilbert and Jorge Nocedal, Global Convergence Properties of Conjugate Gradient Methods for Optimization, SIAM Journal on Optimization 2(1), 21–42 (1992), DOI 10.1137/0802003 (standard reference, not scraped)