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

Weighted prox-error summability preserves an O(1/k^2) FISTA bound

Statement

Under the certified inexact FISTA model of Certified inexact proximal-gradient and FISTA updates, suppose $F = f + g$ has a minimizer $x_{*}$ . For each $k \geq 1$ , $F (x_{k}) - F (x_{*}) \leq \frac{2 L}{(k + 1)^{2}} (∥ x_{0} - x_{*} ∥_{2}^{2} + \frac{2}{L} \sum_{j = 1}^{k} j^{2} η_{j}) .$ In particular, weighted summability $\sum_{j \geq 1} j^{2} η_{j} < \infty$ preserves an $O (1 / k^{2})$ objective bound under this certificate model.

Facts & Assumptions

Given: The certified inexact FISTA sequence, its errors, and a minimizer.

[F1]

FISTA energy recurrence with certified proximal errors: the potential after $k$ calls is at most $∥ x_{0} - x_{*} ∥_{2}^{2} + (2 / L) \sum_{j = 1}^{k} t_{j}^{2} η_{j}$ .

[F2]

Certified inexact proximal-gradient and FISTA updates: $t_{1} = 1$ and $t_{j + 1} = (1 + \sqrt{1 + 4 t_{j}^{2}}) / 2$ .

Proof

1.1F1givenalgebra

Sum the recurrence [F1] through step $k$ and discard the nonnegative squared potential. This gives $F (x_{k}) - F (x_{*}) \leq \frac{L}{2 t_{k}^{2}} (∥ x_{0} - x_{*} ∥_{2}^{2} + \frac{2}{L} \sum_{j = 1}^{k} t_{j}^{2} η_{j}) .$

2.1F2step 1.1giveninductionalgebra∎

Since $\sqrt{1 + 4 t_{j}^{2}} \leq 2 t_{j} + 1$ for $t_{j} \geq 0$ , [F2] gives $t_{j + 1} \leq t_{j} + 1$ and induction yields $t_{j} \leq j$ . The lower bound $\sqrt{1 + 4 t_{j}^{2}} \geq 2 t_{j}$ gives $t_{k} \geq (k + 1) / 2$ . Therefore $t_{j}^{2} η_{j} \leq j^{2} η_{j}$ and $1 / (2 t_{k}^{2}) \leq 2 / (k + 1)^{2}$ ; substitution into step 1.1 proves the displayed estimate.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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

Mark Schmidt, Nicolas Le Roux, and Francis Bach, Convergence Rates of Inexact Proximal-Gradient Methods for Convex Optimization, §3 and Appendix §6.2 (standard reference, not scraped)