ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

Constant-step SGD can have a nonzero noise floor

Example

Fix $0 < α \leq 1 / 4$ , $b \in R$ , $σ \geq 0$ , and $x_{0} \in R$ . For every integer horizon $N \geq 1$ , take the finite probability space ${- 1, 1}^{N}$ with each sign vector assigned mass $2^{- N}$ , let $ξ_{0}, \dots, ξ_{N - 1}$ be its coordinate signs, set $f (x) = x^{2} / 2$ , and run $x_{t + 1} = x_{t} - α (x_{t} + b + σ ξ_{t})$ . Write $q = 1 - α$ . For every $0 \leq t \leq N$ , the horizon-consistent moment is $E [x_{t}^{2}] = (q^{t} x_{0} - b (1 - q^{t}))^{2} + \frac{α σ^{2}}{2 - α} (1 - q^{2 t}),$ so these moments converge as $t \to \infty$ to $b^{2} + α σ^{2} / (2 - α)$ . In the unbiased case $b = 0$ with $σ > 0$ , the fixed-step expected squared gradient therefore has a positive noise floor.

Under AC, two published finite-horizon bounds also apply. For $b = 0$ , if $R_{N}$ is chosen independently and uniformly from ${0, \dots, N - 1}$ on a finite extension, then $E ∣ x_{R_{N}} ∣^{2} \leq x_{0}^{2} / (α N) + α σ^{2}$ . For general $b$ , the uniform average satisfies $N^{- 1} \sum_{t = 0}^{N - 1} E [x_{t}^{2}] \leq x_{0}^{2} / (α N) + (5 / 2) b^{2} + α σ^{2}$ .

Example references

Stochastic-gradient-descent procedure: fixes the unconstrained update applied in this example.

Independent finite random-index extension: constructs the independent uniform output index.

Published uniform-random-iterate theorem: supplies the unbiased constant-step bound under its exact hypotheses.

Published biased-noise-floor theorem: supplies the bounded-bias average bound under its exact hypotheses.

Facts & Assumptions

Given: The finite product sample space and recurrence in the Example; AC is used only for the two conditional-expectation theorem comparisons at the end of the verification.

[A1]

The Axiom of Choice: AC supplies the conditional-expectation classes required by the published theorem comparisons.

[F1]

Stochastic gradient descent: for $s = 1, \dots, N$ , the update is $y_{s + 1} = y_{s} - α H_{s}$ , starting at $y_{1}$ .

[F2]

Probability measures and probability spaces and Measures on sigma-algebras: a probability measure has total mass one and is countably additive.

[F3]

Random elements and real random variables: each coordinate sign is a measurable real random variable.

[F4]

Filtration and filtered probability space and Adapted and integrable stochastic process: $F_{t}$ records the first $t$ signs and $x_{t}$ is measurable with respect to it.

[F5]

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

[F6]

Conditional variance and Conditional variance is well-defined and has the second-moment formula: conditional variance is the conditional second moment of the centered direction.

[F7]

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

[F8]

An independent finite random index has the weighted expectation formula: a finite uniform index can be added independently and its output expectation is the arithmetic mean of the iterate expectations.

[F9]

Nonconvex SGD stationarity bound for a uniform randomized iterate: assume AC, $f : R^{d} \to R$ continuously differentiable with $L$ -Lipschitz gradient for $L > 0$ , a real global lower bound $f_{\inf}$ , deterministic $x_{0}$ , and the filtration-adapted update with square-integrable directions, conditional mean $\nabla f (x_{t})$ and conditional variance at most $σ^{2}$ . For constant $0 < α \leq 1 / L$ , $N \geq 1$ , and $Δ = f (x_{0}) - f_{\inf}$ , the independent uniform output from ${0, \dots, N - 1}$ obeys $E ∥ \nabla f (x_{R}) ∥_{2}^{2} \leq 2 Δ / (α N) + L α σ^{2}$ .

[F10]

Biased SGD has an explicit weighted stationarity floor: assume AC, $f : R^{d} \to R$ with $L$ -Lipschitz gradient for $L > 0$ , a real global lower bound $f_{\inf}$ , square-integrable $x_{0}$ , and the filtration-adapted update with square-integrable directions, conditional mean $\nabla f (x_{t}) + b_{t}$ , measurable conditional bias $b_{t}$ of norm at most a deterministic $β \geq 0$ , and conditional variance at most a deterministic $σ^{2} \geq 0$ . For constant $0 < α \leq 1 / (4 L)$ , $N \geq 1$ , and finite $Δ = E f (x_{0}) - f_{\inf}$ , the uniform average of $E ∥ \nabla f (x_{t}) ∥_{2}^{2}$ over $0 \leq t < N$ is at most $2 Δ / (α N) + (5 / 2) β^{2} + L α σ^{2}$ .

[F11]

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

Verification

1.1F1F2F3F4F11givenconstructalgebra

For a fixed horizon $N$ , let $F_{t}$ be generated by $ξ_{0}, \dots, ξ_{t - 1}$ , with $F_{0}$ trivial and $F_{t} = F_{N}$ for $t > N$ . Apply [F1] with $y_{s} = x_{s - 1}$ , $H_{s} = G_{s - 1}$ , and $H_{s} = F_{s - 1}$ for $s \geq 1$ , setting $H_{0} = F_{0}$ ; this gives exactly the zero-based recurrence in the Example. For $0 \leq t < N$ and each prefix atom $A$ , define $C_{t} H$ on $A$ as the average of $H$ over its $2^{N - t}$ extensions. This is an explicit $F_{t}$ -measurable function, and finite summation gives $\int_{B} C_{t} H d P = \int_{B} H d P$ for every $B \in F_{t}$ , since $B$ is a union of prefix atoms. Half the extensions of each prefix have each next sign, so $C_{t} ξ_{t} = 0$ and $C_{t} (ξ_{t}^{2}) = 1$ . The recurrence makes $x_{t}$ constant on each prefix, hence $C_{t} G_{t} = x_{t} + b$ and $C_{t} [(G_{t} - (x_{t} + b))^{2}] = σ^{2}$ for $G_{t} = x_{t} + b + σ ξ_{t}$ . All variables have finite moments on the finite space; these averages and identities require no AC.

1.2F1giveninductionalgebra

Put $m_{t} = E [x_{t}]$ . The update is $x_{t + 1} = q x_{t} - α b - α σ ξ_{t}$ , hence $m_{t + 1} = q m_{t} - α b$ with $m_{0} = x_{0}$ . Induction gives $m_{t} = q^{t} x_{0} - b (1 - q^{t})$ for every $t \leq N$ .

2.1F2F4F11step 1.1step 1.2givenalgebra

Let $V_{t} = E [(x_{t} - m_{t})^{2}]$ . Averaging first over each prefix atom as in step 1.1 gives $E [(x_{t} - m_{t}) ξ_{t}] = 0$ and $E [ξ_{t}^{2}] = 1$ , so the cross term vanishes and $V_{t + 1} = q^{2} V_{t} + α^{2} σ^{2}$ , with $V_{0} = 0$ . Thus $V_{t} = α^{2} σ^{2} \sum_{j = 0}^{t - 1} q^{2 j} = \frac{α σ^{2}}{2 - α} (1 - q^{2 t})$ , since $1 - q^{2} = α (2 - α)$ . Adding $m_{t}^{2}$ proves the displayed moment formula, and it is independent of the chosen horizon whenever $N \geq t$ .

2.2A1F5F6F8F9step 1.1givenalgebra

Now assume AC for the published bounds. The event-integral identities in step 1.1 identify its finite averages with the conditional-expectation classes [F5] and their conditional variances [F6]. Here $f^{'} (x) = x$ and $∣ f^{'} (u) - f^{'} (v) ∣ = ∣ u - v ∣$ , so the gradient is $1$ -Lipschitz. The deterministic start and all directions are square-integrable by step 1.1, and $f (x) \geq 0$ . In the unbiased case, $L = 1$ , $f_{\inf} = 0$ , $Δ = x_{0}^{2} / 2$ , and step 1.1 verifies conditional unbiasedness and variance $σ^{2}$ ; $α \leq 1 / 4 \leq 1 / L$ . Use [F8] with $p_{k} = 1 / N$ and apply [F9] to obtain $E ∣ x_{R_{N}} ∣^{2} \leq x_{0}^{2} / (α N) + α σ^{2}$ .

3.1F7step 2.1givenalgebra

Here $q = 1 - α \in [3 / 4, 1)$ , so [F7] gives $q^{t} \to 0$ . The formula in step 2.1 therefore yields $E [x_{t}^{2}] \to b^{2} + α σ^{2} / (2 - α)$ ; if $b = 0 < σ$ , this limit is strictly positive. This proves the exact constant-step noise-floor claim without using AC.

4.1A1F5F6F10step 1.1step 2.2step 3.1givenalgebra∎

For general $b$ , step 1.1 verifies conditional mean $f^{'} (x_{t}) + b$ , bias bound $β = ∣ b ∣$ , variance bound $σ^{2}$ , and $f (x) \geq 0$ . The step restriction is $α \leq 1 / (4 L)$ because $L = 1$ . Apply [F10] with $Δ = x_{0}^{2} / 2$ to obtain $N^{- 1} \sum_{t = 0}^{N - 1} E [x_{t}^{2}] \leq x_{0}^{2} / (α N) + (5 / 2) b^{2} + α σ^{2}$ . The exact limiting floor from step 3.1 is at most $b^{2} + α σ^{2}$ , since $2 - α \geq 1$ , and is therefore consistent with this bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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