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.

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

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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

A biased simulator gradient has limiting squared gradient b2b2