Alphabeta Math
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.

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

Statement

Assume the exact algorithm hypotheses of Proximal-gradient, FISTA, and fixed-period restarted FISTA, that F=f+g is μ-strongly convex for μ>0 under Strong convexity for an extended-real objective, that a minimizer x∗ exists, and that F(x0)<+∞. For each mode, let (xk)k≥0 denote the sequence whose finite prefixes are its executions with arbitrary finite budgets, using the same initial point and, for restart, the same period. Exact proximal points are unique, so these prefixes agree whenever their budgets overlap. A run with budget N satisfies the bounds below for 0≤k≤N and 0≤jm≤N, respectively. Exact proximal gradient satisfies F(xk)−F(x∗)≤qk(F(x0)−F(x∗)),q=11+μ/(4L)<1. For fixed-period restarted FISTA with m=⌈8L/μ⌉ updates per full block, the restart-point gaps obey F(xjm)−F(x∗)≤2−j(F(x0)−F(x∗)),j≥0.

Facts & Assumptions

Given: The exact algorithms, μ-strongly convex objective, minimizer and finite starting objective in the Statement.

[F1]

Strong convexity for an extended-real objective: for finite-domain points, F((1−θ)x+θy)≤(1−θ)F(x)+θF(y)−(μ/2)θ(1−θ)∥x−y∥22.

[F2]

Existence, resolvent characterization, and firm nonexpansiveness of the proximal map: an exact step x+=TL(x) has p=L(x−x+)−∇f(x)∈∂g(x+).

[F3]

Differentiable convex functions are characterized by the gradient inequality: ∇f(x+)∈∂f(x+) and convexity gives the gradient lower bound.

[F4]

One-step proximal-gradient estimate: at a finite iterate x with z=x, exact proximal gradient gives F(x)≥F(x+)+L∥x+−x∥22/2; both objective values are finite.

[F5]

FISTA has an O(1/k^2) objective bound: m exact FISTA updates from a point w have gap at most 2L∥w−x∗∥22/(m+1)2.

[F6]

Subdifferentials of proper extended-real convex functions: r∈∂F(x) means F(z)≥F(x)+⟨r,z−x⟩ for every z.

Proof

1.1F1F6givenalgebra

If r∈∂F(x) and z∈dom⁡F, [F6] gives the subgradient lower bound at (1−θ)x+θz, while [F1] gives the strong-convexity upper bound there. Combine them, divide by θ>0, and let θ↓0. This gives F(z)≥F(x)+⟨r,z−x⟩+μ2∥z−x∥22. Taking z=x∗ and maximizing the right-hand upper bound ⟨r,x−x∗⟩−(μ/2)∥x−x∗∥2 by completing the square yields F(x)−F(x∗)≤∥r∥22/(2μ).

1.2F1givenalgebra

Strong convexity and minimality imply F(w)−F(x∗)≥(μ/2)∥w−x∗∥22 for every finite w: apply [F1] to (x∗,w), use F(x∗)≤F((1−θ)x∗+θw), divide by θ, and let θ↓0.

2.1F2F3F6F7step 1.1givenalgebra

For an exact step x+=TL(x), [F2] gives p=L(x−x+)−∇f(x)∈∂g(x+). Adding the gradient inequality [F3] shows r=p+∇f(x+)∈∂F(x+) by [F6]. If d=x+−x, [F7] and Lipschitz continuity give ∥r∥2≤L∥d∥2+L∥d∥2=2L∥d∥2. Step 1.1 therefore yields F(x+)−F(x∗)≤(2L2/μ)∥d∥22.

3.1F4step 2.1giveninductionalgebra

By [F4], F(x)−F(x+)≥(L/2)∥d∥22. Combining with step 2.1 gives F(x)−F(x∗)≥(1+μ/(4L))(F(x+)−F(x∗)). Apply this at every proximal-gradient step and induct to obtain the stated factor qk.

4.1F5step 1.2giveninductionalgebra∎

Apply [F5] to one FISTA block starting at a restart point w. Step 1.2 gives ∥w−x∗∥22≤2(F(w)−F(x∗))/μ, so the block-end gap is at most 4L(F(w)−F(x∗))/(μ(m+1)2). Since m+1≥8L/μ, this factor is at most 1/2. Each completed restart starts the next block at its last iterate; induction over blocks proves the stated restart-point bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

43 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