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.
Kolmogorov iid l1 strong law
Statement
For IID real with , almost surely.
Facts & Assumptions
Measurable coordinatewise functions preserve independence: Let be an independent family of random elements . For each , let be measurable. Then the family is independent.
Summability of truncated normalized variances: For identically distributed integrable real and , . No independence is required.
Strong law under summable normalized variances: Let be independent square-integrable real random variables. Let be deterministic and nondecreasing with . If then In particular, for IID centered square-integrable variables and any , almost surely (the displayed normalization is used for ).
Cesaro limit of truncated means: For identically distributed integrable real , with , one has .
Iid linear truncation occurs only finitely often: For identically distributed integrable real , put . Almost surely for all sufficiently large . Consequently . Independence is unnecessary.
Proof
Given: The objects, hypotheses and definitions in the statement. Its conclusions are to be established below.
Set . The truncation maps are Borel, so F1 makes mutually independent. They are bounded by n and hence square-integrable.
F2 gives . With , F3 applies to step 1.1 and yields almost surely.
By F4, . By F5, almost surely. Intersecting the two conull events with step 2.1 and adding these three terms gives .
Depends on
Used by
- Iid strong law implies the weak law Corollary
- Strong law estimator of an integrable mean Example
- Strong law for empirical indicator averages Example
- Strong law does not assert a rate Remark
- Empirical measures of iid euclidean samples converge weakly Theorem
- Integrability is necessary for an iid finite mean strong law Theorem
Dependency tree · two levels
29 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
- Durrett, §§2.4–2.5, pp. 76–87 (standard reference, not scraped)
- Roch, Note 5, Theorems 5.8–5.9, printed pp. 5–6 (mutual independence specialization only) (standard reference, not scraped)