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

Expected linear contraction of an SVRG epoch

Statement

Let n,d≥1, and let fi:Rd→R be convex, continuously differentiable, with L-Lipschitz gradients for a common L>0. Put F=n−1∑i=1nfi, assume F is μ-strongly convex for μ>0, and let x∗ satisfy ∇F(x∗)=0. In one SVRG epoch Finite-sum SVRG, take a deterministic snapshot x~, set x0=x~, choose

η=110L,m=2n,

and choose each uniform inner index independently of the past. Assume n≥10L/μ. Choose the output index J independently and uniformly from {0,…,m−1}. Then

E[F(xJ)−F(x∗)]≤q(F(x~)−F(x∗)),q=1μη(1−2Lη)m+2Lη1−2Lη≤78.

The expectation is over the inner indices and J; this is an epoch expectation bound and asserts no almost-sure convergence.

Facts & Assumptions

Given: The functions, smoothness, strong convexity, stationary minimizer, snapshot, inner iteration, and independent uniform output index in the Statement. All finite-time moments exist because a finite horizon has only finitely many index histories and each update evaluates finite gradients at finite points.

[F1]

Finite-sum SVRG: xt+1=xt−ηvt, with vt=∇fIt(xt)−∇fIt(x~)+∇F(x~) and independent uniform It.

[F2]

SVRG conditional unbiasedness and variance bound: conditionally on the history, E[vt]=∇F(xt) and E∥vt∥22≤4L(F(xt)−F(x∗))+4L(F(x~)−F(x∗)).

[F3]

Descent inequality for a Lipschitz gradient: an L-Lipschitz gradient gives fi(z)≤fi(w)+⟨∇fi(w),z−w⟩+(L/2)∥z−w∥22.

[F4]

Gradient of a finite sum is the finite sum of gradients: ∇F(w)=n−1∑i∇fi(w).

[F5]

Strong convexity makes a differentiable gradient strongly monotone: F(y)≥F(x)+⟨∇F(x),y−x⟩+(μ/2)∥y−x∥22.

[F6]

Differentiable convex functions are characterized by the gradient inequality: convex differentiable F satisfies F(y)≥F(x)+⟨∇F(x),y−x⟩.

[F7]

The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn: ∥z∥22=⟨z,z⟩ and the inner product is bilinear.

[F8]

Laws of finite sums and finite products: finite sums are additive, obey scaling, and telescope.

[A1]

The Axiom of Choice: AC is assumed for the conditional-expectation interfaces used in [F2].

Proof

Given: The objects and assumptions in the Statement.

1.1A1F1F2F3F4F6F7F8givenalgebra

Write Δt=F(xt)−F(x∗) and Δ~=F(x~)−F(x∗). Averaging [F3] and using [F4], [F8] gives the L-smooth descent inequality for F. By [F1], [F2], [F6], and [F7], expansion of the squared distance and the convex gradient inequality yield E[∥xt+1−x∗∥22∣Ft]≤∥xt−x∗∥22−2ηΔt+η2E[∥vt∥22∣Ft]≤∥xt−x∗∥22−2η(1−2Lη)Δt+4η2LΔ~.

2.1A1F5F8step 1.1givenalgebra

Average the conditional inequality in step 1.1 over the finite index histories and sum for t=0,…,m−1. By [F8] the finite sum telescopes; the terminal squared distance is nonnegative and x0=x~, hence m−1∑t=0m−1E[Δt]≤∥x~−x∗∥22/[2η(1−2Lη)m]+[2ηL/(1−2Lη)]Δ~. By [F5] and ∇F(x∗)=0, ∥x~−x∗∥22≤2Δ~/μ; the independent uniform J makes its expected gap the average on the left, giving the stated q.

3.1step 2.1givenalgebra∎

With η=1/(10L) and m=2n, 1−2Lη=4/5, so q=25L/(4μn)+1/4≤5/8+1/4=7/8 by n≥10L/μ. This proves the Statement.

Depends on

Used by

Dependency tree · two levels

56 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