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.
Bounded centered convergent series have summable variances
Statement
Let be independent centered real random variables with almost surely for one finite constant . If converges almost surely, then . The bound is two-sided and uniform in .
Facts & Assumptions
Almost-sure convergence of a random series: 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 def-almost-sure-convergence-of-random-variables. With from def-partial-sums-and-sample-means, its convergence event is This is exactly the real Cauchy condition, with the indexing of thm-series-cauchy-criterion 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, cor-almost-sure-convergence-of-an-independent-series-is-a-zero-one-event gives . Set on and off . The functions converge everywhere to , so thm-sequential-suprema-infima-limsup-liminf-and-pointwise-limits-are-measurable and thm-arithmetic-and-lattice-operations-preserve-measurability 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 .
Disjoint groups of an independent sigma-algebra family remain independent: Let be an independent family of sigma-algebras on a probability space, and let be pairwise disjoint index sets. For each , define Then the sigma-algebras are independent.
Expectations factor over finite products of independent random variables: Let , let be independent real random variables on a common probability space, and let be Borel measurable for each . 1. If every is nonnegative, then in . 2. If every is integrable, then is integrable and the same factorization holds in .
Variance and covariance identities for random variables: Let be square-integrable real random variables on one probability space. Then Moreover, covariance is symmetric and bilinear on finite linear combinations. On finite full-power-set probability spaces these formulas reduce to the published finite identities.
Continuity from below for measures: Let be an increasing sequence of measurable sets for a measure , so . Then No finiteness hypothesis is required.
Linearity, monotonicity, and the modulus bound for expectation: Let be integrable real or complex random variables on one probability space. 1. For scalars , 2. If and are real-valued and almost surely, then 3.
Proof
Given: The objects and hypotheses of the statement.
Put and . Almost every convergent path is bounded. The measurable events for positive integers increase to a probability-one event. Continuity from below supplies one integer with probability . Set and ; thus .
The past event and are independent of by grouping. All moments below are finite by boundedness. Expanding and factoring the cross term and the square term gives . This also holds at , where the past sum is zero.
On , the triangle inequality and give almost surely. Split the expectation in the previous identity over and . Monotonicity yields .
Sum from to . The expectation differences telescope, the exit events are disjoint, and on . Thus for every . The increasing nonnegative partial sums are bounded, so their series is finite. No division by or a variance is used, and is included.
Depends on
- Almost-sure convergence of a random series
- Partial sums, row sums and sample means
- Independent random elements
- Disjoint groups of an independent sigma-algebra family remain independent
- Expectations factor over finite products of independent random variables
- Variance and covariance identities for random variables
- Continuity from below for measures
- Linearity, monotonicity, and the modulus bound for expectation
Used by
Dependency tree · two levels
34 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
- Lemma 3.13 and complete proof, pp. 67–68 (standard reference, not scraped)