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.

✓ 3 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Stochastic approximation and stochastic gradient methods — Examples

1 · Prerequisites

2 · Summary

These examples work through one streaming least-squares update, a bounded-noise scalar Robbins–Monro root, and a biased simulator gradient. Together they distinguish conditional unbiasedness, almost-sure convergence with square-summable but nonsummable step sizes, and the nonzero stationarity floor caused by persistent bias.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

One streaming least-squares SGD update

Example

Let $Y$ be equally likely to be $- 1$ or $1$ on a filtered space with trivial $F_{0}$ and $F_{1} = σ (Y)$ . Set $ℓ (x, Y) = \frac{1}{2} (x - Y)^{2}$ and define the streaming least-squares objective $f (x) = E [ℓ (x, Y)]$ . From $x_{0} = 0$ , use the one-sample gradient $G_{0} = \partial_{x} ℓ (x_{0}, Y)$ and step $α_{0} = \frac{1}{2}$ . Compute the mean gradient, first iterate, and objective gap.

Facts & Assumptions

Given: The two-point finite probability space, the loss and objective in the Example, initial point $x_{0} = 0$ , and step $α_{0} = 1 / 2$ .

[A1]

The Axiom of Choice: AC is used for the canonical conditional-expectation interface.

[F1]

Finite probability spaces, outcome weights, events, and event probabilities: each of the two outcomes $Y = - 1, 1$ has weight $1 / 2$ .

[F2]

Expectation of a nonnegative or integrable random variable: on this finite space, expectation is the weighted finite sum.

[F3]

Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates: the sample gradient is the oracle value, and the SGD step is $x_{1} = x_{0} - α_{0} G_{0}$ .

[F4]

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

[F5]

The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set: the derivative is the limit of the difference quotient.

[F6]

Conditional variance: $Var (G_{0} ∣ F_{0}) = E [(G_{0} - E [G_{0} ∣ F_{0}])^{2} ∣ F_{0}]$ .

Verification

1.1A1F1F2F3F5F6givenalgebra

By [F1]–[F2], $f (x) = \frac{1}{4} (x + 1)^{2} + \frac{1}{4} (x - 1)^{2} = \frac{1}{2} (x^{2} + 1) .$ Its difference quotient at $x$ is $(f (x + h) - f (x)) / h = x + h / 2$ , so [F5] gives $\nabla f (x) = x$ . Likewise $(ℓ (h, Y) - ℓ (0, Y)) / h = h / 2 - Y$ , so $G_{0} = - Y$ . Its conditional mean given the trivial $F_{0}$ is zero, equal to $\nabla f (0)$ , and [F6] with [F1]–[F2] gives conditional variance $E [Y^{2}] = 1$ .

2.1F3F4step 1.1algebra∎

The update in [F3] gives $x_{1} = Y / 2$ . Since $Y^{2} = 1$ , $f (x_{1}) = \frac{1}{2} (1 / 4 + 1) = 5 / 8$ , whereas $f (0) = 1 / 2$ is the minimum because $f (x) - f (0) = x^{2} / 2 \geq 0$ . Hence the realized objective gap after this one sample is exactly $1 / 8$ .

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A bounded-noise Robbins–Monro scalar root

Example

Consider $h (x) = x$ with root $x^{*} = 0$ , initial point $x_{0} = 0$ , and a noise sequence $ξ_{k} \in {- 1, 1}$ where each $ξ_{k}$ is $F_{k + 1}$ -measurable and satisfies $E [ξ_{k} ∣ F_{k}] = 0$ and $E [ξ_{k}^{2} ∣ F_{k}] = 1$ . No independence across iterations is assumed. Use steps $α_{k} = \frac{1}{4} (k + 2)^{- 3 / 4}$ and oracle $G_{k} = x_{k} + ξ_{k}$ . Verify the strong-monotonicity, stability, and stepsize conditions for the almost-sure Robbins–Monro theorem.

Facts & Assumptions

Given: The one-dimensional filtered model and noise conditions in the Example.

[A1]

The Axiom of Choice: AC is used by the conditional-expectation and almost-sure convergence interfaces.

[F1]

Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates: $x_{k + 1} = x_{k} - α_{k} G_{k}$ , and conditional means and moments are interpreted almost surely.

[F2]

The p-series for a real exponent p converges exactly when p is greater than one: $\sum_{n \geq 1} n^{- p}$ diverges for $p \leq 1$ and converges for $p > 1$ .

[F3]

Robbins–Monro converges almost surely for a strongly monotone root: a strongly monotone drift with a root, uniform conditional second moment, and positive steps with divergent sum and square-summable squares gives almost-sure convergence.

[F4]

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

[F5]

Taking out what is known: a known integrable factor may be taken outside conditional expectation.

[F6]

Basic algebra and order properties of conditional expectation: conditional expectation is linear and fixes integrable measurable quantities.

[F7]

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

[F8]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: the Euclidean norm satisfies the triangle inequality.

Verification

1.1A1F1F4F5F6F7F8givenalgebrainduction

Since $0 < α_{k} < 1$ , [F7] and [F8] give $∣ x_{k} ∣ \leq 1$ : it holds at $x_{0} = 0$ , and if $∣ x_{k} ∣ \leq 1$ then $∣ x_{k + 1} ∣ = ∣ (1 - α_{k}) x_{k} - α_{k} ξ_{k} ∣ \leq (1 - α_{k}) ∣ x_{k} ∣ + α_{k} ∣ ξ_{k} ∣ \leq 1.$ Taking out the $F_{k}$ -measurable $x_{k}$ with [F5] and using [F6] with the stated conditional moments gives $E [G_{k} ∣ F_{k}] = x_{k} = h (x_{k})$ and $E [G_{k}^{2} ∣ F_{k}] = x_{k}^{2} + 1 \leq 2$ . Also $(h (x) - h (y)) (x - y) = (x - y)^{2}$ , so $h$ is strongly monotone with $μ = 1$ .

2.1A1F2F3step 1.1givenalgebra∎

By [F2], $\sum_{k} α_{k} = \frac{1}{4} \sum_{n \geq 2} n^{- 3 / 4} = \infty$ and $\sum_{k} α_{k}^{2} = \frac{1}{16} \sum_{n \geq 2} n^{- 3 / 2} < \infty$ . Each $α_{k} \leq 1 / 4 \leq 1 / (2 μ)$ . Thus [F3] applies with $M^{2} = 2$ , proving $x_{k} \to 0$ almost surely.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

A biased simulator gradient has limiting squared gradient $b^{2}$

Example

Let the probability space be the one-point space $Ω = {ω_{0}}$ with $P ({ω_{0}}) = 1$ and the trivial filtration $F_{k} = {\emptyset, Ω}$ for every $k$ . Let $f (x) = x^{2} / 2$ , so $f_{\inf} = 0$ and $\nabla f (x) = x$ . A deterministic simulator returns the biased gradient $G_{k} = x_{k} + b$ for fixed $b \in R$ . Starting at $x_{0} = 0$ with constant step $α = 1 / 4$ , compute the iterates and their average squared true gradient.

Facts & Assumptions

Given: The one-dimensional objective, biased oracle, initial value, and stepsize in the Example.

[A1]

The Axiom of Choice: AC is used by the conditional-expectation formulation of the bias-floor theorem.

[F1]

Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates: the unconstrained update is $x_{k + 1} = x_{k} - α G_{k}$ .

[F2]

Biased SGD has an explicit weighted stationarity floor: for an $L$ -smooth objective and steps $α \leq 1 / (4 L)$ , bounded bias $β$ and variance $σ^{2}$ give an asymptotic average squared-gradient bound $(5 / 2) β^{2} + L α σ^{2}$ .

[F3]

For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ : if $∣ q ∣ < 1$ , then $q^{k} \to 0$ .

[F4]

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

[F5]

The principle of mathematical induction: a formula true at $k = 0$ and preserved by the recurrence holds for every natural index.

[F6]

The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set: $f^{'} (x)$ is the limit of $(f (x + h) - f (x)) / h$ as $h \to 0$ when that limit exists.

[F7]

Basic algebra and order properties of conditional expectation: conditional expectation preserves real constants, so $E [c ∣ F_{k}] = c$ for every $c \in R$ .

[F8]

Conditional variance: conditional variance is the conditional expectation of the squared deviation from the conditional mean.

Verification

1.1F1F3F4F5givenalgebrainduction

With $q = 3 / 4$ , [F1] gives $x_{k + 1} = q x_{k} - b / 4$ . [F5] applies to $x_{k} = - b (1 - q^{k})$ : it holds at $k = 0$ , and substitution gives $q x_{k} - b / 4 = - b (q (1 - q^{k}) + (1 - q)) = - b (1 - q^{k + 1})$ . Thus [F3] implies $x_{k} \to - b$ and $∥ \nabla f (x_{k}) ∥_{2}^{2} = x_{k}^{2} \to b^{2}$ .

2.1A1F2F4F6F7F8step 1.1givenalgebra∎

The difference quotient $(f (x + h) - f (x)) / h = x + h / 2$ tends to $x$ , so [F6] gives $\nabla f (x) = x$ . For all $x, y$ , $∣ \nabla f (x) - \nabla f (y) ∣ = ∣ x - y ∣ = ∥ x - y ∥_{2}$ by [F4], and the stated objective satisfies $f (x) \geq 0$ . The recurrence in step 1.1 makes each $x_{k}$ deterministic; [F7] then gives conditional mean $x_{k} + b = \nabla f (x_{k}) + b$ , and [F8] gives conditional variance $0$ . Also $x_{0} = 0$ is square-integrable. For every $N \geq 1$ , $\frac{1}{N} \sum_{k = 0}^{N - 1} x_{k}^{2} = b^{2} (1 - \frac{2 (1 - q^{N})}{N (1 - q)} + \frac{1 - q^{2 N}}{N (1 - q^{2})}) ⟶ b^{2} .$ The two fractions tend to zero because their numerators are bounded and their denominators grow linearly in $N$ . With $L = 1$ , $β = ∣ b ∣$ , $σ = 0$ , and $α = 1 / 4 = 1 / (4 L)$ , [F2] applies and gives the (valid, though nonsharp) upper limit $(5 / 2) b^{2}$ , while the exact average tends to $b^{2}$ .

Stochastic approximation and stochastic gradient methods — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

One streaming least-squares SGD update

Example

Facts & Assumptions

Verification

A bounded-noise Robbins–Monro scalar root

Example

Facts & Assumptions

Verification

A biased simulator gradient has limiting squared gradient b2b2

Example

Facts & Assumptions

Verification

A biased simulator gradient has limiting squared gradient $b^{2}$