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.
Almost-sure convergence of a random series
Definition
For real random variables , the series converges almost surely if its partial sums converge to a finite real limit on an event of probability one, as in Almost-sure convergence of real random variables. With from Partial sums, row sums and sample means, its convergence event is This is exactly the real Cauchy condition, with the indexing of A series converges iff for every there is with for all shifted by one. Measurable arithmetic makes every event in this countable expression measurable. For any fixed , the union over may be restricted to ; then each difference uses only . Thus is in the tail sigma-algebra, without assuming independence. Under independence, Almost-sure convergence of an independent series is a zero-one event gives .
Set on and off . The functions converge everywhere to , so Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable and Arithmetic and lattice operations preserve measurability whenever they are defined make measurable.
For Borel sets , the event is likewise tail measurable. Changing finitely many summands adds an eventually constant finite difference to ; divided by deterministic tending to infinity that difference tends to zero, so the normalized limsup is unchanged. The sign of the unnormalized limsup need not be unchanged: the all-zero sequence has limsup zero, while changing its first term to makes the limsup of partial sums equal to .
Depends on
- Partial sums, row sums and sample means
- Almost-sure convergence of real random variables
- A series converges iff for every $\varepsilon > 0$ there is $N$ with $|a_{m+1} + \dots + a_n| < \varepsilon$ for all $n > m \ge N$
- Arithmetic and lattice operations preserve measurability whenever they are defined
- Almost-sure convergence of an independent series is a zero-one event
- Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable
Used by
- Kolmogorov two-series sufficiency Corollary
- Summable untruncated variances are not necessary Counterexample
- Bounded centered convergent series have summable variances Lemma
- Independent-copy symmetrization of random series Lemma
- Convergence in probability and almost surely agree for independent series Theorem
- Kolmogorov convergence criterion Theorem
- Kolmogorov three-series theorem Theorem
Dependency tree · two levels
22 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
- Section 2.5, Example 2.5.2 p. 81 and series convention p. 84 (standard reference, not scraped)
- Section 3.4 opening, p. 61 (standard reference, not scraped)