TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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.

Exact gradient line search has a global objective-gap contraction

Statement

Let $U \subseteq R^{d}$ be open and convex, let $f \in C^{2} (U, R)$ have an attained global minimum $f^{*} = f (x^{*})$ at $x^{*} \in U$ , and fix $x_{0} \in U$ . Suppose the initial sublevel set $K : = {y \in U : f (y) \leq f (x_{0})}$ is compact and is contained in a convex open set $V \subseteq U$ on which

$m I ⪯ H_{f} (y) ⪯ M I (y \in V)$

for constants $0 < m \leq M$ . For every current iterate $x \in K$ , the oracle Ideal exact gradient line-search step is well-defined. If $g : = \nabla f (x) \neq 0$ and $x_{+}$ is its returned point, then

$f (x_{+}) - f^{*} \leq (1 - \frac{m}{M}) (f (x) - f^{*}) .$

If $g = 0$ , the oracle returns the unique minimizer $x = x^{*}$ . Repeated exact steps from $x_{0}$ therefore satisfy

$f (x_{k}) - f^{*} \leq {(1 - \frac{m}{M})}^{k} (f (x_{0}) - f^{*})$

for every generated $k \geq 1$ . When $m = M$ , the factor is zero for $k \geq 1$ ; no $0^{0}$ convention is used. This is an objective-gap statement and does not identify an iterate-error bound without an additional curvature estimate.

Facts & Assumptions

Given: $U, f, x^{*}, x_{0}, K, V, m, M$ as in the Statement, and a current $x \in K$ .

[F1]

Ideal exact gradient line-search step: if $g \neq 0$ , it returns the unique global minimizer of $t \mapsto f (x - t g)$ over feasible $t \geq 0$ ; if $g = 0$ , it returns the stationary point.

[F2]

The Hessian matrix and critical points of a scalar field and The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case: $H_{f}$ is the Hessian matrix and $\nabla f$ is the vector of standard-coordinate partial derivatives.

[F3]

If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative and The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : a $C^{1}$ scalar field is totally differentiable with Jacobian derivative, and its composition with a differentiable line has the chain-rule derivative.

[F4]

A $C^{2}$ function is convex exactly when its Hessian is positive semidefinite: a $C^{2}$ function with positive-semidefinite Hessian on a convex open set is convex there.

[F5]

Multivariable Taylor formula with a Lagrange remainder along a line segment: along a segment in a convex open domain, the second-order Taylor remainder is the Hessian quadratic form at a point on that segment.

[F6]

A Hessian lower bound gives strong convexity and gradient-gap bounds: applied to the restriction of $f$ to $V$ , the lower Hessian bound gives the strong-convexity inequality, uniqueness of an attained minimizer, and $∥ \nabla f (x) ∥_{2}^{2} \geq 2 m (f (x) - f^{*})$ for points of $V$ .

[F7]

A compact subset of a metric space is closed and bounded: a compact subset of a metric space is closed and bounded.

[F8]

Metric continuity characterisations, with countable choice for the sequential converse: a continuous map between metric spaces has closed preimages of closed sets; this implication uses no choice principle.

[F9]

Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line: a closed and bounded subset of Euclidean space is compact.

[F10]

A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value: a continuous real-valued function on a nonempty compact metric space attains its minimum.

[F11]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: the Euclidean norm satisfies the triangle inequality and Cauchy–Schwarz.

[F12]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : for a differentiable scalar function on an interval, its endpoint increment is its derivative at an interior point times the interval length.

Proof

1.1F2F3F6givenchoose

If $g = 0$ , [F6] gives $0 \geq 2 m (f (x) - f^{*})$ ; since $f (x) \geq f^{*}$ and $m > 0$ , $f (x) = f^{*}$ , and uniqueness gives $x = x^{*}$ . Now assume $g \neq 0$ and put $r (t) : = x - t g$ for $t \geq 0$ . [F3] gives $ϕ^{'} (0) = - ∥ g ∥_{2}^{2} < 0$ for $ϕ (t) : = f (r (t))$ . Openness of $U$ and this strict derivative provide a sufficiently small $t > 0$ with $r (t) \in U$ and $f (r (t)) < f (x) \leq f (x_{0})$ , so $S : = {t \geq 0 : r (t) \in K}$ is nonempty.

2.1F4F7F8F9F11step 1.1

By [F4], $f$ is convex on $V$ , so its sublevel set $K$ is convex because $K \subset V$ . By [F7], $K$ is closed and bounded. The affine map $r$ is continuous since $∥ r (s) - r (t) ∥_{2} = ∣ s - t ∣ ∥ g ∥_{2}$ , so [F8] makes $S = r^{- 1} (K) \cap [0, \infty)$ closed. Boundedness gives $c \in R^{d}$ and $R_{0} > 0$ with $K \subset B (c, R_{0})$ ; hence $∥ y ∥_{2} \leq ∥ c ∥_{2} + R_{0} = : R$ on $K$ . For $t \in S$ , the triangle inequality [F11] yields $t ∥ g ∥_{2} = ∥ x - r (t) ∥_{2} \leq ∥ x ∥_{2} + R$ . Thus $S$ is bounded and compact by [F9].

3.1F1F6F10givenstep 2.1algebra

The continuous restriction of $ϕ$ to the nonempty compact set $S$ attains a minimum $t_{*} \in S$ by [F10]. Since $0 \in S$ , we have $f (r (t_{*})) \leq f (x)$ . Every feasible ray parameter $t$ with $r (t) \in U$ but $t \notin S$ has $f (r (t)) > f (x_{0}) \geq f (x) \geq f (r (t_{*}))$ , so $t_{*}$ is a global feasible-ray minimizer. If two distinct parameters minimized, their endpoints $y_{1}, y_{2}$ would be distinct because $g \neq 0$ ; their midpoint $z$ lies in $K$ by step 2.1. Apply the strong-convexity inequality [F6] from $z$ to each endpoint and add: $f (z) \leq (f (y_{1}) + f (y_{2})) / 2 - m ∥ y_{1} - y_{2} ∥_{2}^{2} / 8$ , strictly below their common minimum. Thus the minimizer is unique and the output specified by [F1] is well-defined.

4.1F2F3F12givenstep 1.1step 3.1

The small step in step 1.1 strictly decreases $f$ , so the minimizer from step 3.1 has $t_{*} > 0$ . Since $r (t_{*}) \in K \subset U$ and $U$ is open, $t_{*}$ is interior to the feasible ray and $ϕ^{'} (t_{*}) = 0$ . Convexity of $V$ and step 2.1 put the segment $[x, r (t_{*})]$ in $V$ . By [F2], [F3], and the Hessian bounds, $m ∥ g ∥_{2}^{2} \leq ϕ^{''} (s) = g^{T} H_{f} (r (s)) g \leq M ∥ g ∥_{2}^{2}$ on this segment, so $ϕ^{'}$ is strictly increasing. The mean-value theorem [F12] applied to $ϕ^{'}$ on $[0, t_{*}]$ gives $∥ g ∥_{2}^{2} = ϕ^{'} (t_{*}) - ϕ^{'} (0) = t_{*} ϕ^{''} (s_{0}) \leq t_{*} M ∥ g ∥_{2}^{2}$ for some $s_{0} \in (0, t_{*})$ . Since $g \neq 0$ , division yields $t_{*} \geq 1 / M$ .

5.1F5F6givenstep 3.1step 4.1

The candidate $t_{0} : = 1 / M$ lies in $[0, t_{*}]$ by step 4.1, so $r (t_{0})$ lies on the segment from $x$ to $r (t_{*})$ and belongs to $V$ . The lower Hessian bound makes $ϕ^{''} (s) > 0$ there; since $ϕ^{'} (t_{*}) = 0$ , $ϕ^{'} (s) < 0$ for $0 \leq s < t_{*}$ . Hence $f (r (t_{0})) \leq f (x) \leq f (x_{0})$ and $r (t_{0}) \in K$ . Taylor's formula [F5] with the upper Hessian bound gives $f (r (t_{0})) \leq f (x) - M^{- 1} ∥ g ∥_{2}^{2} + (M / (2 M^{2})) ∥ g ∥_{2}^{2} = f (x) - ∥ g ∥_{2}^{2} / (2 M)$ . By the minimization proved in step 3.1, $f (x_{+}) \leq f (r (t_{0}))$ .

6.1F1F6givenstep 5.1algebradischarge-induction∎

Subtract $f^{*}$ in step 5.1 and use [F6] to get $f (x_{+}) - f^{*} \leq f (x) - f^{*} - ∥ g ∥_{2}^{2} / (2 M) \leq (1 - m / M) (f (x) - f^{*})$ . The factor is nonnegative because $m \leq M$ . Exact steps never increase the objective, so every later iterate remains in $K$ ; applying the one-step bound successively proves the stated rate for all generated iterates.

Depends on

Used by

Exact and Armijo rates on an anisotropic quadratic Example

Cited to discharge well-definedness by Ideal exact gradient line-search step.

Dependency tree · two levels

91 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

Stephen Boyd and Lieven Vandenberghe, Convex Optimization (standard reference, not scraped)
Philip E. Gill and Margaret H. Wright, Math 171B Numerical Optimization Class Notes (standard reference, not scraped)