TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Biased SGD has an explicit weighted stationarity floor

Statement

Assume AC. Let $f : R^{d} \to R$ have $L$ -Lipschitz gradient for $L > 0$ and satisfy $f (x) \geq f_{\inf}$ for a real lower bound $f_{\inf}$ . Run the unconstrained update of Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates from square-integrable $x_{0}$ with deterministic steps $0 < α_{k} \leq 1 / (4 L)$ . Suppose $E [G_{k} ∣ F_{k}] = \nabla f (x_{k}) + b_{k}, ∥ b_{k} ∥_{2} \leq β_{k}, Var (G_{k} ∣ F_{k}) \leq σ_{k}^{2}$ almost surely, where $b_{k}$ is $F_{k}$ -measurable and $β_{k}, σ_{k}$ are deterministic nonnegative bounds. For $N \geq 1$ and $Δ = E f (x_{0}) - f_{\inf} < \infty$ , $\frac{\sum_{k = 0}^{N - 1} α_{k} E ∥ \nabla f (x_{k}) ∥_{2}^{2}}{\sum_{k = 0}^{N - 1} α_{k}} \leq \frac{2 Δ + 2 \sum_{k < N} α_{k} β_{k}^{2} + 2 L \sum_{k < N} α_{k}^{2} β_{k}^{2} + L \sum_{k < N} α_{k}^{2} σ_{k}^{2}}{\sum_{k < N} α_{k}} .$ In particular, for constant $α, β, σ$ the uniform average is at most $\frac{2 Δ}{α N} + \frac{5}{2} β^{2} + L α σ^{2},$ and therefore ${lim sup}_{N \to \infty} \frac{1}{N} \sum_{k = 0}^{N - 1} E ∥ \nabla f (x_{k}) ∥_{2}^{2} \leq \frac{5}{2} β^{2} + L α σ^{2} .$ Decreasing steps retain the displayed weighted bias and noise sums.

Facts & Assumptions

Given: AC; the smooth objective, lower bound, update, conditional mean and variance conditions in the Statement.

[A1]

The Axiom of Choice: AC supplies the conditional-expectation classes.

[F1]

Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates: the update is $x_{k + 1} = x_{k} - α_{k} G_{k}$ , with conditional mean and vector variance defined coordinatewise.

[F2]

Descent inequality for a Lipschitz gradient: $f (y) \leq f (x) + ⟨ \nabla f (x), y - x ⟩ + (L / 2) ∥ y - x ∥_{2}^{2}$ .

[F3]

Conditional variance and Conditional variance is well-defined and has the second-moment formula: vector second moment equals squared conditional mean plus the sum of coordinate conditional variances.

[F4]

Taking out what is known: an integrable finite measurable factor may be taken outside conditional expectation when the products are integrable.

[F5]

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

[F6]

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

[F7]

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 ⟩ ∣ \leq ∥ u ∥_{2} ∥ v ∥_{2}$ , and the Euclidean norm satisfies the triangle inequality.

[F8]

The principle of mathematical induction: a property true at the first index and inherited by each successor holds at every natural index.

Proof

1.1A1F1F2F3F4F5F6F7F8givenalgebrainduction

By the oracle definition [F1], each $G_{k}$ used in the conditional variance is square-integrable. Since $x_{0}$ is square-integrable and each deterministic step is finite, the update and [F8] give square-integrable $x_{k}$ for every finite $k$ by induction. The Lipschitz gradient and the triangle inequality in [F7] make $g_{k} = \nabla f (x_{k})$ square-integrable. Applying [F2] at $0, x_{k}$ , and using [F7] and $2 a b \leq a^{2} + b^{2}$ , gives $∣ f (x_{k}) ∣ \leq C (1 + ∥ x_{k} ∥_{2}^{2})$ for a finite constant $C$ depending on $f (0), \nabla f (0), L, f_{\inf}$ ; thus the objective values are integrable. Write ${\overset{ˉ}{G}}_{k} = E [G_{k} ∣ F_{k}] = g_{k} + b_{k}$ . By [F3] and the bias bound, $E [∥ G_{k} ∥_{2}^{2} ∣ F_{k}] = ∥ {\overset{ˉ}{G}}_{k} ∥_{2}^{2} + Var (G_{k} ∣ F_{k}) \leq ∥ g_{k} + b_{k} ∥_{2}^{2} + σ_{k}^{2} .$ The conditional products are integrable by the square-integrable oracle and the stated moment hypotheses.

2.1A1F1F2F3F4F5F6step 1.1algebra

Apply [F2] to $x_{k + 1} = x_{k} - α_{k} G_{k}$ , condition on $F_{k}$ , and use step 1.1. Expanding $∥ g_{k} + b_{k} ∥_{2}^{2}$ gives $E [f (x_{k + 1}) ∣ F_{k}] \leq f (x_{k}) - α_{k} (1 - L α_{k} / 2) ∥ g_{k} ∥_{2}^{2} - α_{k} (1 - L α_{k}) ⟨ g_{k}, b_{k} ⟩ + \frac{L α_{k}^{2}}{2} (β_{k}^{2} + σ_{k}^{2}) .$

3.1F7step 2.1givenalgebra

Put $q = L α_{k} \leq 1 / 4$ . By [F7] and $(∥ g_{k} ∥_{2} / 2 - (1 - q) β_{k})^{2} \geq 0$ , $(1 - q) ∥ g_{k} ∥_{2} β_{k} \leq \frac{1}{4} ∥ g_{k} ∥_{2}^{2} + (1 - q)^{2} β_{k}^{2} .$ Use this to bound the possibly positive cross term in step 2.1. Its gradient coefficient is at most $- α_{k} (3 / 4 - q / 2) \leq - α_{k} / 2$ , and the bias terms are at most $α_{k} β_{k}^{2} + L α_{k}^{2} β_{k}^{2}$ . Hence $E [f (x_{k + 1}) ∣ F_{k}] \leq f (x_{k}) - \frac{α_{k}}{2} ∥ g_{k} ∥_{2}^{2} + α_{k} β_{k}^{2} + L α_{k}^{2} β_{k}^{2} + \frac{L α_{k}^{2}}{2} σ_{k}^{2} .$

4.1F5step 3.1givenalgebra

Take ordinary expectations and sum step 3.1 from $k = 0$ to $N - 1$ . The objective terms telescope and $E f (x_{N}) \geq f_{\inf}$ , giving $\frac{1}{2} \sum_{k < N} α_{k} E ∥ g_{k} ∥_{2}^{2} \leq Δ + \sum_{k < N} α_{k} β_{k}^{2} + L \sum_{k < N} α_{k}^{2} β_{k}^{2} + \frac{L}{2} \sum_{k < N} α_{k}^{2} σ_{k}^{2} .$ Multiply by $2$ and divide by $\sum_{k < N} α_{k} > 0$ to obtain the weighted bound.

5.1step 4.1givenalgebra∎

For constant $α, β, σ$ , divide the numerator in step 4.1 by $N α$ ; the result is $2 Δ / (α N) + 2 β^{2} + 2 L α β^{2} + L α σ^{2}$ . Since $L α \leq 1 / 4$ , this is at most $2 Δ / (α N) + (5 / 2) β^{2} + L α σ^{2}$ . Taking the upper limit as $N \to \infty$ proves the displayed limit-superior bound.

Depends on

Used by

A biased simulator gradient has limiting squared gradient b² Example

Dependency tree · two levels

52 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

Léon Bottou, Frank E. Curtis, and Jorge Nocedal, Optimization Methods for Large-Scale Machine Learning, SIAM Review 60(2) (2018), §§4.1 and 4.3 (standard reference, not scraped)