LemmaStatement: 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 conditional estimator, variance, and table recurrence

Statement

Let f_i:R^d->R be convex and continuously differentiable with L-Lipschitz gradients, set F=n^{-1}sum_i f_i, and let x* satisfy grad F(x*)=0. Conditional on the current iterate x_k and table alpha_i^k, assume an independent uniform index I_k and finite second moments. Put

$S_{k} = \frac{1}{n} \sum_{i = 1}^{n} ∥ α_{i}^{k} - \nabla f_{i} (x^{*}) ∥_{2}^{2}, {\overset{ˉ}{α}}_{k} = \frac{1}{n} \sum_{i} α_{i}^{k}, v_{k} = \nabla f_{I_{k}} (x_{k}) - α_{I_{k}}^{k} + {\overset{ˉ}{α}}_{k} .$

Then

$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, for the SAGA table replacement in Finite-sum SAGA,

E [S_{k + 1} ∣ F_{k}] \leq (1 - 1 / n) S_{k} + \frac{2 L}{n} (F (x_{k}) - F (x^{*})) .

Facts & Assumptions

Given: The finite-sum assumptions, x*, AC, and the SAGA update order. As stipulated by conditioning on the current iterate and table, $F_{k}$ is the history before drawing $I_{k}$ and contains the current state: $x_{k}$ and every $α_{i}^{k}$ are $F_{k}$ -measurable. For the initialized SAGA process this is the history generated by the past indices $I_{0}, \dots, I_{k - 1}$ , or any larger history containing that state from which $I_{k}$ is independent.

[F1]

Finite-sum SAGA: v_k uses the old table; after the step, only alpha_{I_k} is replaced by grad f_{I_k}(x_k).

[F2]

Cocoercive gradient bound for a convex smooth finite sum: n^{-1}sum_i||grad f_i(x)-grad f_i(y)||_2^2<=2L(F(x)-F(y)-<grad F(y),x-y>).

[F3]

Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates: an iterate process is coordinatewise measurable with respect to the current sigma-algebra; an oracle output is measurable at the next time. Table measurability here is part of the current-state conditioning above, not an assertion of this oracle definition.

[F4]

Conditional expectation as an ae class: conditional expectations are almost-sure classes and assume AC for existence.

[F5]

Conditioning a known variable and an independent variable: an independent integrable index indicator has conditional expectation equal to its mean.

[F6]

Taking out what is known: measurable integrable factors can be taken outside conditional expectation.

[F7]

Basic algebra and order properties of conditional expectation: conditional expectation is linear and preserves finite sums.

[F8]

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

[F9]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: |<u,v>|<=||u||_2||v||_2.

[F10]

Gradient of a finite sum is the finite sum of gradients: grad F is the finite average of component gradients.

[F11]

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

[A1]

The Axiom of Choice: assume AC for existence of the conditional-expectation classes used below.

Proof

Given: The objects and hypotheses in the Statement.

1.1F1F11givenalgebrainduction

At initialization the algorithm sets ${\overset{ˉ}{α}}_{0} = n^{- 1} \sum_{i} α_{i}^{0}$ . If ${\overset{ˉ}{α}}_{k} = n^{- 1} \sum_{i} α_{i}^{k}$ and the sampled index is $i$ , its one evaluation $g_{k} = \nabla f_{i} (x_{k})$ and table-mean update give ${\overset{ˉ}{α}}_{k + 1} = {\overset{ˉ}{α}}_{k} + \frac{1}{n} (\nabla f_{i} (x_{k}) - α_{i}^{k}) = \frac{1}{n} \sum_{j \neq i} α_{j}^{k} + \frac{1}{n} \nabla f_{i} (x_{k}) = \frac{1}{n} \sum_{j} α_{j}^{k + 1},$ by the recursion and finite-sum algebra [F11]. Induction proves this maintained-mean identity pathwise at every finite $k$ .

2.1A1F1F3F4F5F6F7F10F11givenalgebra

By [F1], $v_{k} = \nabla f_{I_{k}} (x_{k}) - α_{I_{k}}^{k} + {\overset{ˉ}{α}}_{k}$ . Conditioned on $F_{k}$ , $x_{k}$ and every $α_{i}^{k}$ are known, while each event ${I_{k} = i}$ has conditional probability $1 / n$ by [F5]; taking known vectors out by [F6], linearity [F7], the maintained-mean identity [step 1.1], [F10] and [F11] give $E [v_{k} ∣ F_{k}] = \nabla F (x_{k})$ .

2.2A1F1F3F5F6F7F8F9F10F11givenalgebra

Let $g_{i} = \nabla f_{i} (x_{k}) - \nabla f_{i} (x^{*})$ and $h_{i} = α_{i}^{k} - \nabla f_{i} (x^{*})$ , so $\overset{ˉ}{h} = n^{- 1} \sum_{i} h_{i} = {\overset{ˉ}{α}}_{k}$ by [F10], [F11], [step 1.1], and $\nabla F (x^{*}) = 0$ . Then $v_{k} = g_{I_{k}} - h_{I_{k}} + \overset{ˉ}{h}$ . Expanding its square and applying [F9] and $2 a b \leq a^{2} + b^{2}$ gives $∥ a + b + c ∥_{2}^{2} \leq 3 (∥ a ∥_{2}^{2} + ∥ b ∥_{2}^{2} + ∥ c ∥_{2}^{2})$ ; averaging yields $E [∥ v_{k} ∥_{2}^{2} ∣ F_{k}] \leq 3 (n^{- 1} \sum_{i} ∥ g_{i} ∥_{2}^{2} + S_{k} + ∥ \overset{ˉ}{h} ∥_{2}^{2})$ . Also, expanding the finite average and applying vector and scalar Cauchy–Schwarz from [F9] gives $∥ \overset{ˉ}{h} ∥_{2}^{2} = n^{- 2} \sum_{i, j} ⟨ h_{i}, h_{j} ⟩ \leq n^{- 2} (\sum_{i} ∥ h_{i} ∥_{2})^{2} \leq n^{- 1} \sum_{i} ∥ h_{i} ∥_{2}^{2} = S_{k}$ . The finite-sum expansions use [F11].

3.1A1F2F11step 2.2givenalgebra

Apply [F2] with $y = x^{*}$ to obtain $n^{- 1} \sum_{i} ∥ g_{i} ∥_{2}^{2} \leq 2 L (F (x_{k}) - F (x^{*}))$ . Substitution in step 2.2 proves $E [∥ v_{k} ∥_{2}^{2} ∣ F_{k}] \leq 6 L (F (x_{k}) - F (x^{*})) + 6 S_{k}$ .

4.1A1F1F2F3F5F6F7F11step 3.1givenalgebra∎

If $I_{k} = i$ , the table update [F1] changes $S$ by $n^{- 1} (∥ g_{i} ∥_{2}^{2} - ∥ h_{i} ∥_{2}^{2})$ . Averaging over the $n$ equally likely indices gives $E [S_{k + 1} ∣ F_{k}] = (1 - 1 / n) S_{k} + n^{- 2} \sum_{i} ∥ g_{i} ∥_{2}^{2}$ ; [F2] bounds the last term by $(2 L / n) (F (x_{k}) - F (x^{*}))$ .

Depends on

Used by

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)
Léon Bottou, Frank E. Curtis, and Jorge Nocedal, Optimization Methods for Large-Scale Machine Learning, SIAM Review 60(2) (2018) (standard reference, not scraped)