TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Finite-time projected SGD bound for a convex objective

Statement

Assume AC. Let $C \subseteq R^{d}$ be nonempty, closed, and convex, with diameter $D = \sup_{x, y \in C} ∥ x - y ∥_{2} < \infty$ . Let $f : R^{d} \to R$ be differentiable and convex, and assume a minimizer $x^{*} \in C$ exists. Start projected SGD at deterministic $x_{0} \in C$ , with conditionally unbiased gradients, meaning $E [G_{k} ∣ F_{k}] = \nabla f (x_{k})$ as in Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates, and $E [∥ G_{k} ∥_{2}^{2} ∣ F_{k}] \leq G^{2}$ almost surely for every $k$ . For $N \geq 1$ , put ${\overset{ˉ}{x}}_{N} = N^{- 1} \sum_{k = 0}^{N - 1} x_{k}$ . If $D, G > 0$ and $α_{k} = α = D / (G \sqrt{N})$ for $0 \leq k < N$ , then $E [f ({\overset{ˉ}{x}}_{N}) - f (x^{*})] \leq \frac{D G}{\sqrt{N}} .$ If $D = 0$ or $G = 0$ , the initial point is already optimal and the displayed bound holds with right side zero.

Facts & Assumptions

Given: AC, $C, f, x^{*}, x_{0}, N$ , the projected update, conditional unbiasedness, and the moment bound in the Statement.

[A1]

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

[F1]

Projected stochastic-gradient update: $x_{k + 1} = P_{C} (x_{k} - α G_{k})$ .

[F2]

Existence, resolvent characterization, and firm nonexpansiveness of the proximal map: the proximal map is nonexpansive.

[F3]

The proximal map of an indicator is Euclidean projection: the proximal map of $ι_{C}$ is $P_{C}$ , and it fixes every point of $C$ .

[F4]

Differentiable convex functions are characterized by the gradient inequality: for differentiable convex $f$ , $f (y) \geq f (x) + ⟨ \nabla f (x), y - x ⟩$ .

[F5]

Convex and strictly convex functions on Euclidean convex sets: convexity means $f ((1 - t) x + t y) \leq (1 - t) f (x) + t f (y)$ for $t \in [0, 1]$ .

[F6]

The principle of mathematical induction: a property true at the first natural and preserved by successors holds for every natural.

[F7]

Taking out what is known and Basic algebra and order properties of conditional expectation: integrable measurable factors may be taken outside conditional expectation, which is linear and expectation-preserving.

[F8]

A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere: a nonnegative integrable random variable with zero expectation vanishes almost surely.

[F9]

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

[F10]

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

[F11]

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}$ .

[F12]

Dedekind completeness: the least-upper-bound property: every nonempty set of reals bounded above has a supremum.

[F13]

Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates: conditional unbiasedness is the almost-sure identity $E [G_{k} ∣ F_{k}] = \nabla f (x_{k})$ .

Proof

1.1A1F2F3F4F6F10F11F12F13givenalgebrainduction

First establish adaptedness of the projected iterates. The deterministic $x_{0}$ is $F_{0}$ -measurable. If $x_{k}$ is $F_{k}$ -measurable, then $x_{k}$ and $G_{k}$ are $F_{k + 1}$ -measurable because $F_{k} \subseteq F_{k + 1}$ and [F13] makes $G_{k}$ $F_{k + 1}$ -measurable. Thus $x_{k} - α G_{k}$ is $F_{k + 1}$ -measurable. By [F2]–[F3], $P_{C}$ is nonexpansive and hence continuous, so $x_{k + 1} = P_{C} (x_{k} - α G_{k})$ is $F_{k + 1}$ -measurable and lies in $C$ . Induction [F6] proves this for every $k$ . The set of pairwise distances in the nonempty set $C$ is nonempty and bounded above by the finite $D$ , so [F12] supplies its supremum. By [F10] and [F13], $∥ \nabla f (x_{k}) ∥_{2}^{2} \leq E [∥ G_{k} ∥_{2}^{2} ∣ F_{k}] \leq G^{2}$ . Since $x_{k}, x^{*} \in C$ , their distance is at most $D$ . The convex gradient inequality [F4] and [F11] give $0 \leq f (x_{k}) - f (x^{*}) \leq ⟨ \nabla f (x_{k}), x_{k} - x^{*} ⟩ \leq D G$ , so each objective value in the telescope is integrable.

2.1A1F1F2F3F4F7F9F13step 1.1givenalgebra

By [F3], $P_{C} (x^{*}) = x^{*}$ , and [F2] makes $P_{C}$ nonexpansive. Therefore $∥ x_{k + 1} - x^{*} ∥_{2}^{2} \leq ∥ x_{k} - α G_{k} - x^{*} ∥_{2}^{2}$ . Expand the square, take conditional expectation, and use [F1], [F7], [F13], and the conditional moment bound. The gradient inequality in [F4] with $x = x_{k}$ , $y = x^{*}$ gives $E [∥ x_{k + 1} - x^{*} ∥_{2}^{2} ∣ F_{k}] \leq ∥ x_{k} - x^{*} ∥_{2}^{2} - 2 α (f (x_{k}) - f (x^{*})) + α^{2} G^{2}$ .

3.1F7step 2.1givenalgebra

Take ordinary expectations in step 2.1 and sum for $k = 0, \dots, N - 1$ . The distance terms telescope, $E ∥ x_{N} - x^{*} ∥_{2}^{2} \geq 0$ , and $∥ x_{0} - x^{*} ∥_{2} \leq D$ , so $2 α \sum_{k = 0}^{N - 1} E [f (x_{k}) - f (x^{*})] \leq D^{2} + N α^{2} G^{2}$ .

4.1F5F6step 3.1givenalgebrainduction

Convexity keeps ${\overset{ˉ}{x}}_{N}$ in $C$ and gives $f ({\overset{ˉ}{x}}_{N}) \leq N^{- 1} \sum_{k < N} f (x_{k})$ . To verify this finite Jensen inequality, induction starts with equality for one point; the step writes the $m$ -point mean as $\frac{m - 1}{m}$ times the $(m - 1)$ -point mean plus $\frac{1}{m} x_{m - 1}$ , then applies [F5]. Take expectations and use step 3.1 to get $E [f ({\overset{ˉ}{x}}_{N}) - f (x^{*})] \leq \frac{D^{2}}{2 α N} + \frac{α G^{2}}{2}$ .

5.1A1F3F4F6F7F8step 4.1givenalgebrainduction∎

With $α = D / (G \sqrt{N})$ , the two terms in step 4.1 are each $D G / (2 \sqrt{N})$ , proving the stated bound. If $D = 0$ , $C$ is a singleton and $x_{0} = x^{*}$ . If $G = 0$ , [F8] applied to each conditional moment and expectation-preservation in [F7] give $G_{k} = 0$ almost surely for every fixed $k$ . For each finite horizon, induction using [F6] shows all its iterates equal $x_{0}$ almost surely. Unbiasedness at $k = 0$ gives $\nabla f (x_{0}) = 0$ , and [F4] makes $x_{0}$ a global minimizer. Thus the zero-case bound holds for every $N$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

79 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

Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, §§3.1 and 6.1, Theorem 6.1 (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), §4.1 (standard reference, not scraped)