Pipeline-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.

Variance reduced finite sum and adaptive gradient optimization — Examples

1 · Prerequisites

2 · Summary

The balanced 14-example logistic fit has a unique minimizer at zero and meets the smooth, strongly convex hypotheses for the exact SVRG epoch bound. The work ledger compares equal 2000-step SVRG and SAGA blocks, including SAGA's table initialization. The final example instantiates the periodic bounded-gradient Adam divergence calculation and its explicit positive cycle drift.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedOpen item page →

A regularized logistic finite sum with an exact minimizer

Statement

Consider $n = 14$ one-dimensional examples, seven with feature $a_{i} = 1$ and label $y_{i} = 1$ , and seven with $a_{i} = 1$ and $y_{i} = - 1$ . With unit $ℓ_{2}$ regularization, define

$f_{i} (w) = \log (1 + \exp (- y_{i} w)) + \frac{1}{2} w^{2}, F (w) = \frac{1}{14} \sum_{i = 1}^{14} f_{i} (w) .$ Here $\log$ denotes the natural logarithm.

Then each component is convex with $5 / 4$ -Lipschitz gradient, $F$ is $1$ -strongly convex, and its unique minimizer is $w^{*} = 0$ . An SVRG epoch from snapshot $\tilde{w} = 1$ with $η = 2 / 25$ and $m = 28$ therefore satisfies

$E [F (w_{J}) - F (0)] \leq \frac{181}{224} [F (1) - F (0)], F (1) - F (0) = \frac{1}{2} \log (2 + e + e^{- 1}) + \frac{1}{2} - \log 2.$

Facts & Assumptions

Given: The finite data set and objective in the Statement.

[F1]

Finite-sum SVRG: SVRG returns an independent uniform inner iterate and uses a full gradient plus two component gradients per inner update.

[F2]

Expected linear contraction of an SVRG epoch: if all components are convex, continuously differentiable and $L$ -smooth, the average is $μ$ -strongly convex with a stationary point $x^{*}$ , $n \geq 10 L / μ$ , $η = 1 / (10 L)$ , and $m = 2 n$ , then from a deterministic snapshot with the theorem's independent uniform component draws and output index the expected gap relative to $x^{*}$ contracts by its stated $q$ .

[F3]

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

[F4]

Strong convexity for an extended-real objective: $μ$ -strong convexity is the strong-Jensen inequality with decrement $(μ / 2) θ (1 - θ) ∣ x - y ∣^{2}$ .

[F5]

Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction: an $L$ -Lipschitz gradient obeys $∣ f_{i}^{'} (u) - f_{i}^{'} (v) ∣ \leq L ∣ u - v ∣$ in one dimension.

[F6]

The exponential function is smooth and $(\exp)^{'} = \exp$ : $(e^{w})^{'} = e^{w}$ .

[F7]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: $(\log u)^{'} = 1 / u$ for $u > 0$ .

[F8]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : the derivative of a composition is the derivative of the outer function applied to the derivative of the inner function.

[F9]

Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives: sums and scalar multiples differentiate termwise.

[F10]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : a differentiable scalar function's difference over an interval equals its derivative at an intermediate point times the interval length.

[F11]

Multivariable Taylor formula with a Lagrange remainder along a line segment: a $C^{2}$ scalar function on a segment has a second-order Taylor formula with Hessian remainder at an intermediate point.

[F12]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : in one dimension the Euclidean norm is absolute value.

[F13]

The real exponential function and the number $e$ by a power series: $\exp (w)$ is the real exponential and $e = \exp (1)$ .

[F14]

Finite sums and finite products, by recursion: $F$ is the finite average of its fourteen component losses.

[F15]

The natural logarithm as the inverse of the exponential function: for $x > 0$ , $\log x$ is the unique real $y$ with $\exp (y) = x$ .

[F16]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\log$ is strictly increasing on $(0, \infty)$ and $\log (a b) = \log a + \log b$ for $a, b > 0$ .

[F17]

The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : $\exp (w) > 0$ and $\exp (- w) = 1 / \exp (w)$ .

[F18]

Convex and strictly convex functions on Euclidean convex sets: convexity is the segment inequality for function values.

[F19]

Sign rules for products and monotonicity of multiplication: multiplication by a positive denominator preserves order. Squares of nonzero elements are positive makes a nonzero real square positive, and Multiplication by zero: $0 \cdot a = 0$ gives square zero in the zero case; thus every real square is nonnegative.

[F20]

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

[A1]

The Axiom of Choice: assume AC for the conditional-expectation interfaces inherited from the SVRG theorem [F2].

Proof

Given: The data, loss, and regularizer in the Statement.

1.1F6F7F8F9F13F17F19givenalgebra

Write $r = \exp (w) > 0$ by [F13] and [F17]. By [F6]–[F9], $f_{+}^{'} (w) = - 1 / (1 + r) + w$ , $f_{-}^{'} (w) = r / (1 + r) + w$ , and $f_{+}^{''} (w) = f_{-}^{''} (w) = 1 + r / (1 + r)^{2}$ . Since $(1 + r)^{2} - 4 r = (r - 1)^{2} \geq 0$ by [F19], $1 \leq f_{i}^{''} (w) \leq 5 / 4$ for every component and $w$ .

2.1F4F5F10F11F12F14F18F20step 1.1givenalgebra

Apply [F10] to $f_{i}^{'}$ and [F12]; step 1.1 gives $∣ f_{i}^{'} (u) - f_{i}^{'} (v) ∣ \leq (5 / 4) ∣ u - v ∣$ , so every component is $5 / 4$ -smooth. For any $u, v$ , [F11] gives $f_{i} (v) \geq f_{i} (u) + f_{i}^{'} (u) (v - u) + (v - u)^{2} / 2$ . For $0 \leq θ \leq 1$ , put $z = (1 - θ) u + θ v$ , apply this inequality from $z$ to $u, v$ , weight by $1 - θ, θ$ , and add; the gradient terms cancel and $(1 - θ) (u - z)^{2} + θ (v - z)^{2} = θ (1 - θ) (v - u)^{2}$ . Hence $(1 - θ) f_{i} (u) + θ f_{i} (v) \geq f_{i} (z) + \frac{1}{2} θ (1 - θ) (v - u)^{2}$ . Since the subtracted term is nonnegative, this gives ordinary convexity by [F18] and verifies the strong Jensen inequality in [F4]. Averaging these inequalities with [F20] proves that F is convex and 1-strongly convex.

3.1A1F1F2F3F13F14F15F16F17F20step 1.1step 2.1givenalgebra∎

At $w = 0$ , the two component derivatives in step 1.1 are $- 1 / 2$ and $1 / 2$ , so [F3], [F14] and [F20] give $F^{'} (0) = 0$ . Averaging the lower Taylor inequality from step 2.1 gives $F (w) \geq F (0) + F^{'} (0) w + w^{2} / 2 = F (0) + w^{2} / 2$ , so $0$ is the unique minimizer. Substitution gives $F (0) = \log 2$ . The product law [F16] and $e = \exp (1)$ from [F13], with $e^{- 1} = 1 / e$ from [F17], give $F (1) - F (0) = \frac{1}{2} \log (2 + e + e^{- 1}) + \frac{1}{2} - \log 2$ . Since $n = 14 \geq 10 (5 / 4) / 1$ , $η = 2 / 25 = 1 / (10 L)$ , and $m = 28 = 2 n$ , [F1] and [F2] give the claimed SVRG guarantee with $q = \frac{25 L}{4 μ n} + \frac{1}{4} = \frac{125}{224} + \frac{56}{224} = \frac{181}{224}$ .

ExampleConstruction: Literature-sourcedVerification: AI-adaptedOpen item page →

SVRG and SAGA gradient-work and storage ledger

Statement

Let a finite sum have $n, d \geq 1$ components and dimension, and let an SVRG epoch and SAGA block each have $m \geq 1$ inner updates. Count component-gradient evaluations separately from scalar coordinate arithmetic, and do not cache SVRG snapshot gradients. SVRG uses $n + 2 m$ component-gradient evaluations per epoch, $O (n d)$ arithmetic to assemble its full gradient, $O (d)$ arithmetic per inner update, and $O (d)$ working storage. SAGA uses $n + m$ component-gradient evaluations during its initialized block and $m$ new evaluations in each later equally long block; initializing its mean takes $O (n d)$ arithmetic, each later update takes $O (d)$ arithmetic, and its table plus auxiliary vectors use $O (n d)$ storage. The cost of evaluating a component gradient is not bounded here. For $n = 1000$ , $d = 20$ , and $m = 2 n = 2000$ , the gradient counts are 5000 SVRG evaluations per epoch, 3000 SAGA evaluations in the initial block, and 2000 in a later block; the SAGA table has 20,000 scalar coordinates.

Facts & Assumptions

Given: The component count, dimension, horizon, and algorithms in the Statement.

[F1]

Finite-sum SVRG: the procedure computes the full finite-sum gradient, evaluates both displayed component gradients at every inner update without caching snapshot values, and uses a fixed number of vector additions, scalings, and temporaries per update.

[F2]

Finite-sum SAGA: initialization evaluates one component gradient for each table entry and forms their running mean; each later update evaluates one sampled component gradient once and reuses it for the estimator and replacement, with a fixed number of vector operations and temporary $d$ -vectors.

[F3]

Finite sums and finite products, by recursion: the finite objective contains exactly $n$ component functions.

Proof

Given: $n, d \geq 1$ , an epoch and blocks of length $m \geq 1$ , and the displayed finite-sum algorithms. The numerical instance is $n = 1000$ , $d = 20$ , and $m = 2 n = 2000$ .

1.1F1F2F3givenalgebra

By [F1] and [F3], one full gradient evaluates each of the $n$ component gradients once, and each of the $m$ inner updates evaluates two component gradients, so SVRG uses $n + 2 m$ evaluations. By [F2], SAGA initializes all $n$ table entries and evaluates one sampled component per update, so its initialized block uses $n + m$ evaluations and a later block uses $m$ . Substitution of $n = 1000$ and $m = 2000$ gives 5000, 3000, and 2000, respectively.

1.2F1F2F3givenalgebra

A full gradient sums and scales $n$ vectors with $d$ coordinates, using $O (n d)$ coordinate operations; each update in [F1] has a fixed number of vector operations and therefore costs $O (d)$ . SAGA's initialization forms the table mean from $n$ vectors for $O (n d)$ coordinate operations, and each update in [F2] uses a fixed number of vector operations for $O (d)$ .

2.1F1F2givenalgebra∎

For SVRG, sample the independent uniform output index $J$ before the epoch and save $x_{J}$ when that index is reached, including $x_{0}$ if $J = 0$ . The inner updates do not use $J$ , so independence gives the same joint law of $J$ and the trajectory, and hence the same returned-snapshot law as sampling $J$ after the updates. This implementation needs one saved $d$ -vector in addition to the fixed update buffers in [F1], uses no extra gradient evaluations, and therefore has $O (d)$ working storage. By [F2], SAGA stores $n$ table vectors and a constant number of additional $d$ -vectors, giving $n d + O (d) = O (n d)$ scalars because $n \geq 1$ . At the numerical instance the table itself contains $1000 \cdot 20 = 20,000$ coordinates. The accounting excludes arithmetic within each component-gradient evaluation and makes no total-runtime claim.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedOpen item page →

A bounded periodic gradient sequence with divergent Adam iterates

Statement

For Adam with $β_{1} = 0$ , $β_{2} = 1 / 2$ , $η = 1$ , and $ϵ = 1 / 100$ , feed the repeated affine losses $5 x / 2, - x, - x$ from $x_{1} = 0$ . Every gradient has magnitude at most $5 / 2$ , but the terminal subsequence $x_{3 k + 1}$ tends to $+ \infty$ ; for every $k \geq 2$ , its cycle drift is at least $7295 / 90804$ .

Facts & Assumptions

Given: The update and loss sequence in the Statement.

[F1]

Bias-corrected Adam update: Adam's bias-corrected moments and coordinate update are defined for the fixed parameters in the Statement.

[F2]

Adam diverges on a periodic bounded-gradient loss sequence: this exact loss sequence and parameter choice give cycle drift at least $7295 / 90804 > 0$ for every cycle $k \geq 2$ and hence an unbounded terminal subsequence.

[F3]

Convex and strictly convex functions on Euclidean convex sets: affine losses satisfy the convex segment inequality.

[F4]

Every complete ordered field is Archimedean: for every real $R$ there is a natural integer $N \geq 1$ with $R < N$ .

[F5]

Sign rules for products and monotonicity of multiplication: multiplication by a positive real preserves strict order.

Proof

Given: The finite-prefix online loss sequence in the Statement.

1.1F1F3givenalgebra

Each loss is affine, so direct substitution in [F3] verifies convexity. Its derivative is respectively $5 / 2, - 1, - 1$ , all of magnitude at most $5 / 2$ ; the updates are the bias-corrected Adam updates [F1].

2.1F2F4F5step 1.1givenalgebrainduction∎

The gradients and parameters in step 1.1 are the specified inputs of [F2]. Let $δ = 7295 / 90804 > 0$ ; its cycle calculation gives $x_{3 (k + 1) + 1} - x_{3 k + 1} \geq δ$ for every $k \geq 2$ . With $X_{k} = x_{3 k + 1}$ , induction gives $X_{2 + r} \geq X_{2} + r δ$ for every natural $r \geq 0$ . For any real $M$ , [F4] supplies a natural $N \geq 1$ with $(M - X_{2}) / δ < N$ . Since $δ > 0$ , [F5] gives $X_{2} + N δ > M$ , and then every $r \geq N$ satisfies $X_{2 + r} \geq X_{2} + N δ > M$ . This is exactly convergence of the terminal subsequence to $+ \infty$ , after its first two cycles.

Variance reduced finite sum and adaptive gradient optimization — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A regularized logistic finite sum with an exact minimizer

Statement

Facts & Assumptions

Proof

SVRG and SAGA gradient-work and storage ledger

Statement

Facts & Assumptions

Proof

A bounded periodic gradient sequence with divergent Adam iterates

Statement

Facts & Assumptions

Proof

Sources