TheoremStatement: Literature-sourcedProof: 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.

FISTA has an O(1/k^2) objective bound

Statement

Under the exact FISTA hypotheses of Proximal-gradient, FISTA, and fixed-period restarted FISTA, suppose $F = f + g$ has a minimizer $x_{*}$ . For every $x_{0} \in R^{n}$ and $k \geq 1$ , $0 \leq F (x_{k}) - F (x_{*}) \leq \frac{2 L ∥ x_{0} - x_{*} ∥_{2}^{2}}{(k + 1)^{2}} .$

Facts & Assumptions

Given: The FISTA recurrence, its objective and minimizer in the Statement.

[F1]

FISTA energy estimate-sequence recurrence: $2 t_{k}^{2} (F (x_{k}) - F (x_{*})) / L + ∥ u_{k} ∥_{2}^{2} \leq ∥ x_{0} - x_{*} ∥_{2}^{2}$ after telescoping the energy recurrence.

[F2]

Proximal-gradient, FISTA, and fixed-period restarted FISTA: $t_{1} = 1$ and $t_{k + 1} = (1 + \sqrt{1 + 4 t_{k}^{2}}) / 2$ .

[F3]

Proximal-gradient, FISTA, and fixed-period restarted FISTA: each FISTA proximal output is in $dom g$ and has finite $F$ .

Proof

1.1F1givenalgebra

Summing the energy recurrence of [F1] from $1$ to $k$ cancels all intermediate potentials. The $k = 1$ base term is $∥ u_{0} ∥_{2}^{2} = ∥ x_{0} - x_{*} ∥_{2}^{2}$ , and every later objective coefficient is nonnegative; dropping $∥ u_{k} ∥_{2}^{2}$ gives $F (x_{k}) - F (x_{*}) \leq \frac{L ∥ x_{0} - x_{*} ∥_{2}^{2}}{2 t_{k}^{2}} .$ The gap is nonnegative because $x_{*}$ minimizes $F$ .

2.1F2F3step 1.1giveninductionalgebra∎

Since $\sqrt{1 + 4 t_{k}^{2}} \geq 2 t_{k}$ , [F2] gives $t_{k + 1} \geq t_{k} + 1 / 2$ . Starting from $t_{1} = 1$ , induction yields $t_{k} \geq (k + 1) / 2$ . Substitution into step 1.1 gives the stated bound. Finite objective values for the iterates follow from [F3].

Depends on

Used by

Strong convexity gives linear proximal-gradient and restarted-FISTA rates Theorem

Dependency tree · two levels

6 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

Amir Beck and Marc Teboulle, A Fast Iterative Shrinkage-Thresholding Algorithm for Linear Inverse Problems, Theorem 4.4 (standard reference, not scraped)
Neal Parikh and Stephen Boyd, Proximal Algorithms, §4.3 (standard reference, not scraped)