TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Projected subgradient best-iterate and weighted-average bound

Statement

Let $C \subseteq R^{n}$ be nonempty, closed, and convex, let $f : C \to R$ be convex, and run Projected subgradient method with finite budget for $N \geq 1$ steps with positive $α_{k}$ . Assume all $N$ oracle calls return valid pairs. Suppose a global minimizer $x^{*} \in C$ exists and the oracle vectors obey $∥ g_{k} ∥_{2} \leq G$ ; let $R \geq ∥ x_{0} - x^{*} ∥_{2}$ . Set $A_{N} = \sum_{k < N} α_{k} > 0$ and ${\overset{ˉ}{x}}_{N} = A_{N}^{- 1} \sum_{k < N} α_{k} x_{k}$ . Then $\max {\min_{0 \leq k < N} (f (x_{k}) - f (x^{*})), f ({\overset{ˉ}{x}}_{N}) - f (x^{*})} \leq \frac{R^{2} + G^{2} \sum_{k < N} α_{k}^{2}}{2 A_{N}} .$

Facts & Assumptions

Given: The finite algorithm Projected subgradient method with finite budget, its one-step estimate One-step estimate for projected subgradient descent, convexity Convex and strictly convex functions on Euclidean convex sets, and finite Jensen Finite Jensen inequality for convex functions on $R^{n}$ .

[F1]

For each $k$ , $∥ x_{k + 1} - x^{*} ∥_{2}^{2} \leq ∥ x_{k} - x^{*} ∥_{2}^{2} - 2 α_{k} (f (x_{k}) - f (x^{*})) + α_{k}^{2} ∥ g_{k} ∥_{2}^{2}$ (One-step estimate for projected subgradient descent).

[F2]

For a convex function and nonnegative weights summing to one, its value at the weighted average is at most the weighted average of its values (Finite Jensen inequality for convex functions on $R^{n}$ ).

[F3]

Starting from $x_{0} \in C$ , each successful update is the unique projection onto $C$ and remains feasible; the finite-budget result also establishes that the returned average is defined and feasible (Projected subgradient method with finite budget, Every point has a unique nearest point in a nonempty closed Euclidean convex set, The projected subgradient method returns within its finite budget).

[F4]

Since the stepsizes are positive, $A_{N} = \sum_{k < N} α_{k} > 0$ , and the weights $α_{k} / A_{N}$ are positive and sum to one by the scaling law for finite sums (Laws of finite sums and finite products).

[F5]

The nonempty finite list of objective gaps has a minimum attained by one of its indices (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

Proof

1.1F1F4givenalgebra

Rearrange [F1] and sum over $k = 0, \dots, N - 1$ . The squared-distance terms telescope, giving $2 \sum_{k < N} α_{k} (f (x_{k}) - f (x^{*})) \leq ∥ x_{0} - x^{*} ∥_{2}^{2} - ∥ x_{N} - x^{*} ∥_{2}^{2} + \sum_{k < N} α_{k}^{2} ∥ g_{k} ∥_{2}^{2} \leq R^{2} + G^{2} \sum_{k < N} α_{k}^{2}$ , since the last squared distance is nonnegative. Divide by $2 A_{N} > 0$ using [F4] to bound the weighted average of the objective gaps.

2.1F2F3F4F5step 1.1algebra∎

By [F3] the iterates lie in $C$ , and by [F4] the normalized positive weights sum to one. Apply [F2] to get $f ({\overset{ˉ}{x}}_{N}) - f (x^{*}) \leq A_{N}^{- 1} \sum_{k < N} α_{k} (f (x_{k}) - f (x^{*}))$ . By [F5], the minimum gap is attained; since a positive weighted average with weights summing to one is at least the minimum term, both the minimum gap and the gap at ${\overset{ˉ}{x}}_{N}$ are bounded above by the weighted average of the gaps. Step 1.1 therefore bounds their maximum as asserted.

Depends on

Used by

The fixed-step projected subgradient rate is O(1/√N) Corollary

Dependency tree · two levels

34 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

Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, §3.1 (standard reference, not scraped)
Dimitri Bertsekas, MIT 6.253 Complete Lecture Notes, Lecture 15 (standard reference, not scraped)