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.

SAGA expected linear contraction with a memory-scaled step size

Statement

Let $n, d \geq 1$ , and let $f_{i} : R^{d} \to R$ be convex, continuously differentiable, with $L$ -Lipschitz gradients for a common $L > 0$ . Put $F = n^{- 1} \sum_{i} f_{i}$ , assume $F$ is $μ$ -strongly convex with $μ > 0$ , and let $x^{*}$ satisfy $\nabla F (x^{*}) = 0$ . Run SAGA Finite-sum SAGA from a deterministic $x_{0}$ and its stated initialized gradient table. For

$0 < η \leq \min {\frac{1}{3 L}, \frac{μ}{13 L^{2}}, \frac{1}{7 μ n}},$

define $V_{k} = ∥ x_{k} - x^{*} ∥_{2}^{2}$ , $S_{k} = n^{- 1} \sum_{i} ∥ α_{i}^{k} - \nabla f_{i} (x^{*}) ∥_{2}^{2}$ , and $L_{k} = V_{k} + 7 η^{2} n S_{k}$ . Then for every $k \geq 0$ ,

$E [L_{k + 1}] \leq (1 - μ η) E [L_{k}] .$

Scope note: This is the retained memory-scaled sufficient branch. The controlling STO2 contract separately proves the factor $1 - \min {μ η, 1 / (7 n)}$ for every $0 < η \leq 1 / (10 L)$ , with the faster factor $1 - μ η$ when $μ η \leq 1 / (7 n)$ . The restriction $η \leq 1 / (7 μ n)$ here is sufficient for this branch's faster factor; it is not claimed necessary or optimal. The standard-initialization counterexample refutes removing that rate cap from this faster factor.

Facts & Assumptions

Given: The functions, $x^{*}$ , SAGA initialization and independent uniform sampling in the Statement, with AC for conditional-expectation classes. Finite-time moments exist because for each finite $k$ the algorithm has finitely many index histories and each gradient evaluation is finite.

[F1]

Finite-sum SAGA: $x_{k + 1} = x_{k} - η v_{k}$ , then the sampled table entry is replaced by $\nabla f_{I_{k}} (x_{k})$ using the pre-update iterate.

[F2]

SAGA conditional estimator, variance, and table recurrence: conditionally on the history, $E [v_{k} ∣ F_{k}] = \nabla F (x_{k})$ , $E [∥ v_{k} ∥_{2}^{2} ∣ F_{k}] \leq 6 L (F (x_{k}) - F (x^{*})) + 6 S_{k}$ , and $E [S_{k + 1} ∣ F_{k}] \leq (1 - 1 / n) S_{k} + (2 L / n) (F (x_{k}) - F (x^{*}))$ .

[F3]

Gradient of a finite sum is the finite sum of gradients: $\nabla F (w) = n^{- 1} \sum_{i} \nabla f_{i} (w)$ .

[F4]

Descent inequality for a Lipschitz gradient: each $f_{i}$ satisfies its $L$ -smooth upper descent inequality.

[F5]

Strong convexity makes a differentiable gradient strongly monotone: $F (y) \geq F (x) + ⟨ \nabla F (x), y - x ⟩ + (μ / 2) ∥ y - x ∥_{2}^{2}$ .

[F6]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the Euclidean inner product is bilinear and $∥ z ∥_{2}^{2} = ⟨ z, z ⟩$ .

[F7]

Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction: an $L$ -Lipschitz gradient satisfies $∥ \nabla f_{i} (x) - \nabla f_{i} (y) ∥_{2} \leq L ∥ x - y ∥_{2}$ .

[F8]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: $∣ ⟨ z, w ⟩ ∣ \leq ∥ z ∥_{2} ∥ w ∥_{2}$ ; applying Cauchy–Schwarz to the finite vector of component norms bounds an average by its root-mean-square norm.

[F9]

Basic algebra and order properties of conditional expectation: conditional expectation preserves order and $E [E [X ∣ F_{k}]] = E [X]$ for integrable $X$ .

[F10]

Finite sums and finite products, by recursion: the finite average is the recursively defined finite sum scaled by $1 / n$ .

[F11]

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

[A1]

The Axiom of Choice: AC is assumed by the conditional-expectation interface [F2].

Proof

Given: The objects and assumptions in the Statement.

1.1F3F4F5F11givenalgebra

Put $Δ_{k} = F (x_{k}) - F (x^{*})$ . Averaging [F4] from $x^{*}$ to $x_{k}$ , and using [F3], [F11] and $\nabla F (x^{*}) = 0$ , gives $Δ_{k} \leq (L / 2) V_{k}$ . Applying [F5] from $x^{*}$ to $x_{k}$ also gives $Δ_{k} \geq (μ / 2) V_{k} \geq 0$ .

2.1A1F1F2F5F6step 1.1givenalgebra

Expand [F1] and condition on the current history. The unbiased part of [F2] gives cross term $- 2 η ⟨ \nabla F (x_{k}), x_{k} - x^{*} ⟩ \leq - 2 μ η V_{k}$ by [F5]. The second-moment bound in [F2] and step 1.1 then give $E [V_{k + 1} ∣ F_{k}] \leq (1 - 2 μ η + 3 η^{2} L^{2}) V_{k} + 6 η^{2} S_{k}$ .

2.2A1F2step 1.1givenalgebra

The table recurrence in [F2], followed by step 1.1, gives $E [S_{k + 1} ∣ F_{k}] \leq (1 - 1 / n) S_{k} + (L^{2} / n) V_{k}$ .

3.1A1step 2.1step 2.2givenalgebra

Multiply step 2.2 by $7 η^{2} n$ and add step 2.1. The coefficient of $V_{k}$ is $1 - 2 μ η + 10 η^{2} L^{2}$ , and the coefficient of $S_{k}$ is $(7 n - 1) η^{2}$ . Since $η \leq μ / (13 L^{2})$ , the first coefficient is at most $1 - μ η$ ; since $η \leq 1 / (7 μ n)$ , the second is at most $7 η^{2} n (1 - μ η)$ . Thus $E [L_{k + 1} ∣ F_{k}] \leq (1 - μ η) L_{k}$ .

4.1A1F3F5F7F8F9F10F11step 3.1givenalgebra∎

By [F3], [F7], [F8], [F10], [F11], and finite Cauchy–Schwarz, $∥ \nabla F (x) - \nabla F (y) ∥_{2}^{2} \leq n^{- 1} \sum_{i} ∥ \nabla f_{i} (x) - \nabla f_{i} (y) ∥_{2}^{2} \leq L^{2} ∥ x - y ∥_{2}^{2}$ . For $x \neq y$ , [F5] and [F8] now give $μ ∥ x - y ∥_{2}^{2} \leq ⟨ \nabla F (x) - \nabla F (y), x - y ⟩ \leq L ∥ x - y ∥_{2}^{2}$ , so $μ \leq L$ . Thus $1 - μ η \geq 2 / 3 > 0$ by the step-size bound. Apply [F9] to take expectations in the conditional inequality from step 3.1; this proves the stated contraction.

Remarks

The refutation of the unamended SAGA factor from the standard initialization is proved in The assigned SAGA Lyapunov factor fails under standard initialization. This theorem proves the corrected sufficient-step-size statement above.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

70 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

Aaron Defazio, Francis Bach, and Simon Lacoste-Julien, SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives, NeurIPS 2014 (standard reference, not scraped)
Robert M. Gower and Alexandre Gramfort, Optimization for Data Science: Stochastic Variance Reduced Gradient Methods, complete lecture-note deck (standard reference, not scraped)