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.

SVRG conditional unbiasedness and variance bound

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 a filtration \mathcal F_t, suppose x_t and the snapshot \tilde x are measurable, the uniform index I_t is independent of \mathcal F_t, and the relevant second moments are finite. For

v_{t} = \nabla f_{I_{t}} (x_{t}) - \nabla f_{I_{t}} (\tilde{x}) + \nabla F (\tilde{x}),

one has

$E [v_{t} ∣ F_{t}] = \nabla F (x_{t}), E [∥ v_{t} ∥_{2}^{2} ∣ F_{t}] \leq 4 L (F (x_{t}) - F (x^{*})) + 4 L (F (\tilde{x}) - F (x^{*})) .$

Facts & Assumptions

Given: The finite-sum hypotheses and filtration in the Statement, AC for conditional-expectation classes, and the SVRG estimator definition.

[F1]

Finite-sum SVRG: v_t=grad f_{I_t}(x_t)-grad f_{I_t}(\tilde x)+grad F(\tilde x), with I_t uniform and independent of the past.

[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: filtration-measurable iterates and conditional expectations use the stated oracle convention; AC is assumed for the conditional-expectation classes.

[F4]

Conditional expectation as an ae class: conditional expectations are almost-sure classes whose existence is supplied under AC.

[F5]

Conditioning a known variable and an independent variable: an integrable real variable independent of the conditioning sigma-algebra has conditional expectation equal to its mean.

[F6]

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

[F7]

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

[F8]

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

[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: the gradient of F is the finite average of the component gradients.

[F11]

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

[A1]

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

Proof

Given: The objects, hypotheses, and finite second moments in the Statement.

1.1A1F1F3F4F5F6F7F10F11givenalgebra

Condition on \mathcal F_t. Each component gradient at x_t or \tilde x is known given \mathcal F_t, while the indicators 1_{I_t=i} have conditional expectation 1/n by [F5]. Taking the known component gradients outside with [F6], summing by [F7] and [F11], and using [F10] gives E[v_t|\mathcal F_t]=n^{-1}sum_i(grad f_i(x_t)-grad f_i(\tilde x))+grad F(\tilde x)=grad F(x_t).

2.1A1F1F3F5F6F7F8F9F10F11step 1.1givenalgebra

Write $a_{i} = \nabla f_{i} (x_{t}) - \nabla f_{i} (x^{*})$ and $b_{i} = \nabla f_{i} (\tilde{x}) - \nabla f_{i} (x^{*})$ . Since $\nabla F (x^{*}) = 0$ , [F1] gives $v_{t} = a_{I_{t}} - (b_{I_{t}} - \overset{ˉ}{b})$ with $\overset{ˉ}{b} = n^{- 1} \sum_{i} b_{i} = \nabla F (\tilde{x})$ by [F10]–[F11]. The centered term has conditional mean zero by [F5]–[F7], and $E [∥ b_{I_{t}} - \overset{ˉ}{b} ∥_{2}^{2} ∣ F_{t}] = n^{- 1} \sum_{i} ∥ b_{i} - \overset{ˉ}{b} ∥_{2}^{2} = n^{- 1} \sum_{i} ∥ b_{i} ∥_{2}^{2} - ∥ \overset{ˉ}{b} ∥_{2}^{2} \leq n^{- 1} \sum_{i} ∥ b_{i} ∥_{2}^{2}$ , by expansion and $n^{- 1} \sum_{i} b_{i} = \overset{ˉ}{b}$ .

3.1A1F2F8F9F11step 2.1givenalgebra∎

Expanding the square and applying [F9] together with 2ab<=a^2+b^2 gives ||a_{I_t}-(b_{I_t}-\bar b)||2^2<=2||a{I_t}||2^2+2||b{I_t}-\bar b||_2^2. Apply [F2] with y=x* to the first finite average and to the second; grad F(x*)=0 makes the linear term vanish, so the two averages are at most 2L(F(x_t)-F(x*)) and 2L(F(\tilde x)-F(x*)) by finite-sum algebra [F11]. Multiplying their sum by 2 proves the displayed second-moment bound.

Depends on

Used by

Expected linear contraction of an SVRG epoch Theorem

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

Rie Johnson and Tong Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, NeurIPS 2013 (standard reference, not scraped)
Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, complete monograph (standard reference, not scraped)