LemmaStatement: 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–Siegmund almost-supermartingale convergence

Statement

Assume the Axiom of Choice. Let $(Ω, F, (F_{k})_{k \geq 0}, P)$ be a discrete filtered probability space. Let $X_{k}$ be nonnegative, adapted, and integrable for every $k$ . Let $a_{k}, c_{k}$ be deterministic nonnegative sequences with finite sums, and let $b_{k}$ be nonnegative, $F_{k}$ -measurable, and integrable. If $E [X_{k + 1} ∣ F_{k}] \leq (1 + a_{k}) X_{k} - b_{k} + c_{k} almost surely for every k,$ then $X_{k}$ converges almost surely to a finite nonnegative random variable and $\sum_{k \geq 0} b_{k} < \infty$ almost surely.

Facts & Assumptions

Given: The filtered probability space, processes, summable sequences, conditional inequality, and the Axiom of Choice in the Statement. A sequence of nonnegative reals is summable when its partial sums have a finite supremum.

[A1]

The Axiom of Choice: every family of nonempty sets has a choice function. It is assumed for the conditional-expectation and Doob interfaces used here.

[F1]

Filtration and filtered probability space: $F_{k} \subseteq F_{k + 1} \subseteq F$ .

[F2]

Adapted and integrable stochastic process: adaptedness means $F_{k}$ -measurability at time $k$ , and integrability means finite expectation of the absolute value at every fixed time.

[F3]

Conditional expectation as an ae class: under AC, conditional expectations exist as almost-sure classes; inequalities and equalities between them are interpreted almost surely.

[F4]

Doob submartingale convergence theorem: under AC, a submartingale $Y_{k}$ with $\sup_{k} E [Y_{k}^{+}] < \infty$ has a finite integrable almost-sure limit.

[F5]

The real exponential function and the number $e$ by a power series: $\exp (t) = \sum_{n \geq 0} t^{n} / n!$ , so $\exp (0) = 1$ .

[F6]

The exponential function is smooth and $(\exp)^{'} = \exp$ : $\exp^{'} (t) = \exp (t)$ .

[F7]

The exponential function is strictly increasing: $\exp$ is increasing on $R$ .

[F8]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : for a function continuous on $[u, v]$ and differentiable on $(u, v)$ , some $w \in (u, v)$ satisfies $g (v) - g (u) = g^{'} (w) (v - u)$ .

[F9]

The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ : $\exp (s + t) = \exp (s) \exp (t)$ .

[F10]

Complete ordered field (least-upper-bound property): every nonempty set of reals bounded above has a least upper bound.

[F11]

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

[F12]

Basic algebra and order properties of conditional expectation: conditional expectation is linear and fixes constants; Taking out what is known: an integrable measurable factor can be taken outside when the products are integrable.

Proof

1.1A1F5F6F7F8F9F10F11givenchoosealgebrainduction

Define $A_{0} = 1$ , $A_{k + 1} = A_{k} (1 + a_{k})$ , and $T_{k} = \sum_{j \geq k} c_{j} / A_{j + 1}$ . Then $A_{k} \geq 1$ . For $t > 0$ , [F8] applied to $\exp$ on $[0, t]$ gives $\exp (t) - 1 = t \exp (w)$ for some $w \in (0, t)$ ; by [F5] and [F7], $\exp (w) \geq 1$ , so $1 + t \leq \exp (t)$ , with equality at $t = 0$ . Repeated use of [F9] now gives $A_{k} \leq \exp (\sum_{j < k} a_{j}) \leq \exp (\sum_{j \geq 0} a_{j})$ . Thus $A_{k}$ is nondecreasing and bounded. Let $A_{\infty} = \sup_{k} A_{k}$ , which exists by [F10]; for every $ε > 0$ , some $n$ has $A_{n} > A_{\infty} - ε$ , and then $A_{\infty} - ε < A_{n} \leq A_{k} \leq A_{\infty}$ for all $k \geq n$ , so $A_{k} \to A_{\infty} \geq 1$ . If $C_{m} = \sum_{j < m} c_{j}$ and $C_{\infty} = \sup_{m} C_{m}$ , then for every $ε > 0$ some $m$ has $C_{m} > C_{\infty} - ε$ ; for $k \geq m$ , $0 \leq T_{k} \leq C_{\infty} - C_{k} \leq C_{\infty} - C_{m} < ε$ . Thus $T_{k} \to 0$ .

2.1A1F1F2F3F4F12step 1.1givenalgebra

Put $Z_{k} = X_{k} / A_{k} + T_{k}$ . Each $Z_{k}$ is nonnegative, adapted, and integrable by [F1]–[F3]. By [F12], division by the positive deterministic $A_{k + 1}$ and addition of the deterministic $T_{k + 1}$ commute with conditional expectation. Since $A_{k + 1} = A_{k} (1 + a_{k})$ and $T_{k} = c_{k} / A_{k + 1} + T_{k + 1}$ , the given conditional inequality yields $E [Z_{k + 1} ∣ F_{k}] \leq \frac{(1 + a_{k}) X_{k} - b_{k} + c_{k}}{A_{k + 1}} + T_{k + 1} = Z_{k} - \frac{b_{k}}{A_{k + 1}} .$ Hence $- Z_{k}$ is an integrable adapted submartingale and $\sup_{k} E [(- Z_{k})^{+}] = 0$ . By [F4], $Z_{k}$ converges almost surely to a finite limit.

3.1A1F1F2F3F4F12step 2.1algebra

Define $S_{k} = \sum_{j < k} b_{j} / A_{j + 1}$ and $W_{k} = Z_{k} + S_{k}$ . For each $k$ , $S_{k + 1} = S_{k} + b_{k} / A_{k + 1}$ is $F_{k}$ -measurable: each earlier $b_{j}$ is $F_{j}$ -measurable with $F_{j} \subseteq F_{k}$ , the new term $b_{k}$ is $F_{k}$ -measurable by hypothesis, and the denominators are deterministic. The finite sums $S_{k}, S_{k + 1}$ are nonnegative and integrable by [F2]–[F3]. Hence [F12] gives $E [S_{k + 1} ∣ F_{k}] = S_{k + 1} = S_{k} + b_{k} / A_{k + 1}$ . Combining this with step 2.1 by linearity yields $E [W_{k + 1} ∣ F_{k}] \leq Z_{k} - b_{k} / A_{k + 1} + S_{k} + b_{k} / A_{k + 1} = W_{k}$ . Thus $- W_{k}$ is an integrable adapted submartingale with $\sup_{k} E [(- W_{k})^{+}] = 0$ ; [F4] gives a finite almost-sure limit for $W_{k}$ . Since the increasing partial sums $S_{k}$ are bounded above by $W_{k}$ , their limit is finite almost surely.

4.1step 1.1step 2.1step 3.1algebra∎

From $1 \leq A_{j + 1} \leq A_{\infty}$ , step 3.1 implies $\sum_{j} b_{j} \leq A_{\infty} \sum_{j} b_{j} / A_{j + 1} < \infty$ almost surely. By definition, $X_{k} = A_{k} (Z_{k} - T_{k})$ ; step 1.1 gives $A_{k} \to A_{\infty}$ and $T_{k} \to 0$ , and step 2.1 gives convergence of $Z_{k}$ . Therefore $X_{k}$ converges to a finite nonnegative limit and the asserted decrement sum is finite.

Source notes

The author-hosted Bertsekas appendix states a generalized Robbins–Siegmund theorem but provides no proof of it; the preceding note describes a proof route without giving its argument. It is recorded as statement-level comparison only; the proof above derives the required result from the complete current Doob submartingale supplier.

Depends on

Used by

Dependency tree · two levels

64 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

Dimitri P. Bertsekas, Convex Optimization Algorithms, Appendix A, Proposition A.4.5 (standard reference, not scraped)