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.

Robbins–Monro converges almost surely for a strongly monotone root

Statement

Assume the Axiom of Choice. Let $h : R^{d} \to R^{d}$ have a root $x^{*}$ , so $h (x^{*}) = 0$ , and suppose that for some $μ > 0$ , $⟨ h (x) - h (y), x - y ⟩ \geq μ ∥ x - y ∥_{2}^{2} (x, y \in R^{d}) .$ On a filtered probability space, let $x_{0}$ be square-integrable and let $x_{k}, G_{k}$ follow Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates. Assume each $h (x_{k})$ is $F_{k}$ -measurable, and suppose $E [G_{k} ∣ F_{k}] = h (x_{k}), E [∥ G_{k} ∥_{2}^{2} ∣ F_{k}] \leq M^{2}$ almost surely for a finite constant $M$ . If the deterministic stepsizes satisfy $α_{k} > 0$ , $\sum_{k} α_{k} = \infty$ , and $\sum_{k} α_{k}^{2} < \infty$ , then $x_{k} \to x^{*}$ almost surely. Strong monotonicity also makes the root unique.

Facts & Assumptions

Given: AC, the update and filtration in the Statement, a root $x^{*}$ , the strong-monotonicity inequality, square-integrable $x_{0}$ , and the stated conditional oracle bounds.

[A1]

The Axiom of Choice: AC is assumed for the conditional-expectation and Doob interfaces.

[F1]

Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates: $x_{k + 1} = x_{k} - α_{k} G_{k}$ , $x_{k}$ is $F_{k}$ -measurable, $G_{k}$ is $F_{k + 1}$ -measurable, vector conditional expectations are coordinatewise almost-sure classes, and $E [∥ G_{k} ∥_{2}^{2} ∣ F_{k}] = ∥ E [G_{k} ∣ F_{k}] ∥_{2}^{2} + Var (G_{k} ∣ F_{k})$ with nonnegative conditional variance.

[F2]

Robbins–Siegmund almost-supermartingale convergence: if $V_{k}$ is nonnegative adapted integrable and $E [V_{k + 1} ∣ F_{k}] \leq V_{k} - b_{k} + c_{k}$ with $b_{k} \geq 0$ predictable and $\sum c_{k} < \infty$ , then $V_{k}$ converges almost surely and $\sum b_{k} < \infty$ almost surely.

[F3]

Taking out what is known: a finite $F_{k}$ -measurable factor may be taken outside conditional expectation when the input and products are integrable.

[F4]

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

[F5]

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

[F6]

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

[F7]

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

Proof

1.1F1F4F5F6F7givenalgebrainduction

Write $V_{k} = ∥ x_{k} - x^{*} ∥_{2}^{2}$ . By [F6] and $(\sqrt{μ} ∥ u ∥_{2} - ∥ v ∥_{2} / \sqrt{μ})^{2} \geq 0$ , $2 ∣ ⟨ u, v ⟩ ∣ \leq μ ∥ u ∥_{2}^{2} + μ^{- 1} ∥ v ∥_{2}^{2}$ . The update therefore gives $V_{k + 1} \leq (1 + μ α_{k}) V_{k} + (α_{k} / μ + α_{k}^{2}) ∥ G_{k} ∥_{2}^{2} .$ By [F4], the conditional moment bound implies $E ∥ G_{k} ∥_{2}^{2} \leq M^{2}$ . Using [F1] and nonnegativity of conditional variance gives $E [∥ h (x_{k}) ∥_{2}^{2}] \leq M^{2}$ . Thus [F7] and induction from square-integrable $x_{0}$ show every $V_{k}$ is integrable; Cauchy–Schwarz makes the products of $x_{k} - x^{*}$ with both $G_{k}$ and $h (x_{k})$ integrable.

2.1A1F1F3F4F5givenstep 1.1algebra

Strong monotonicity with $y = x^{*}$ gives $⟨ h (x_{k}), x_{k} - x^{*} ⟩ \geq μ V_{k}$ . Expanding the update and using [F3] to take out $x_{k} - x^{*}$ , then [F4] for the conditional mean and moment, yields $E [V_{k + 1} ∣ F_{k}] \leq V_{k} - 2 μ α_{k} V_{k} + M^{2} α_{k}^{2} .$ The products are integrable by step 1.1.

3.1A1F2step 1.1step 2.1given

Step 2.1 supplies the conditional inequality required by [F2]. Apply it with $a_{k} = 0$ , $b_{k} = 2 μ α_{k} V_{k}$ , and $c_{k} = M^{2} α_{k}^{2}$ . Step 1.1 gives the required integrability, and the stepsize hypotheses make $b_{k}$ predictable and $c_{k}$ summable. Hence $V_{k}$ converges almost surely and $\sum_{k} α_{k} V_{k} < \infty$ almost surely.

4.1F2step 3.1givenalgebra∎

If the almost-sure limit of $V_{k}$ were positive, then eventually $V_{k}$ would be bounded below by half that limit, contradicting $\sum_{k} α_{k} V_{k} < \infty$ and $\sum_{k} α_{k} = \infty$ . Thus $V_{k} \to 0$ and $x_{k} \to x^{*}$ almost surely. If $x^{'}$ were another root, the strong-monotonicity inequality at $(x^{*}, x^{'})$ would give $0 \geq μ ∥ x^{*} - x^{'} ∥_{2}^{2}$ , hence $x^{'} = x^{*}$ .

Depends on

Used by

A bounded-noise Robbins–Monro scalar root 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.2 (standard reference, not scraped)
Dimitri P. Bertsekas, Convex Optimization Algorithms, Appendix A, Proposition A.4.5 (standard reference, not scraped)