(26)–(27), p. 403 — for positive a_n, (26) implies Σ a_n = ∞

Proved

RobbinsMonroSA.Conv.eq_27

by mikedeng1 · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1seriesstochastic-approximation

Let $\{a_n\}$ be positive constants satisfying

\sum_{n=2}^{\infty} \frac{a_n}{a_1 + \cdots + a_{n-1}} = \infty. \tag{26}

Then

\sum_{n=1}^{\infty} a_n = \infty. \tag{27}

This is used to show that $A_n \to \infty$ , so that the linear growth (28) of $A_n$ in the partial sums of $a_n$ holds for large $n$ .

Formalization Note Indices are 0-based. Both " $=\infty$ " are divergence of the partial sums to $+\infty$ .

Preamble

import Mathlib
import Definitions.Def_RobbinsMonroSA_Conv_Setting

open MeasureTheory ProbabilityTheory Filter Topology

Formal statement

namespace RobbinsMonroSA.Conv

/-- (26)–(27), p. 403. For positive `a_n`, (26) implies `Σ a_n = ∞`. -/
theorem eq_27 (a : ℕ → ℝ) (hpos : ∀ n, 0 < a n) (h26 : StepCond26 a) :
    Tendsto (fun N => ∑ n ∈ Finset.range N, a n) atTop atTop := by sorry

end RobbinsMonroSA.Conv

Source

Robbins and Monro, A stochastic approximation method, Ann. Math. Statist. 22 (1951), p. 403, (26)–(27)

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph