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.
Etemadi strong law for pairwise independent iid variables
Statement
Pairwise independent, identically distributed integrable real satisfy 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.
Independence forces covariance to vanish: If and are independent square-integrable real random variables, then
Thus independence implies zero covariance. The converse is false in general.
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.
Integer part: for every real there is exactly one integer with : Identify with its canonical copy inside , along the embeddings (lem-nat-embeds-int, lem-int-embeds-rat, lem-rat-embeds-dense, def-integers). Then for every real there is exactly one integer with
It is written and called the integer part, or floor, of .
Two independent ingredients are needed and neither may be dropped. Existence is the Archimedean property (thm-of-archimedean) together with the well-ordering of (thm-well-ordering-principle): the first says that is caught between two integers at all, the second picks the least integer above . Uniqueness is the discreteness of : no integer lies strictly between and .
This lemma is stated once here and reused. It is what turns "the nearest integer to " from a picture into an object, and the companion page's oscillator is computed from it in one line.
Integer powers : Let , where is the ambient ordered field (def-ordered-field, def-field).
Natural exponents. By the recursion theorem (thm-recursion) applied to the set , the starting element and the function , there is a unique function , written , with
Thus , , and so on. Note that this is defined for every , including .
Negative exponents. If and with , set
Why that is legitimate. The right-hand side presupposes that is
invertible, that is, that . This is a proof obligation and not an
observation, and it is discharged by claim 2 of lem-power-laws: for
in a field, for every , proved there by induction on
from the fact that a field has no zero divisors (lem-of-no-zero-divisors).
That lemma is a statement about the operation introduced here, so it depends on
this definition and is recorded in this item's justified_by rather than in its
deps (SCHEMA §3). Given , the value is a single
well-determined element, because multiplicative inverses in a field are unique
(lem-of-inverse-unique).
Integer exponents. Every integer (def-integers) is either or for a unique natural , where is the embedding (lem-nat-embeds-int, def-int-operations). This too is a citation and not a slogan: the order on is total (thm-int-ordered-ring), so or ; the image of is exactly the set of nonnegative integers, and each of them is for a unique natural (lem-nat-embeds-int); and if then , by compatibility of the order with addition (thm-int-ordered-ring), so and , with unique because is injective. The two clauses above therefore define for every whenever , and for every for arbitrary . The clauses are consistent where they overlap: the only overlap is , where and .
For , , and for the series diverges: Let and let be the integer power (def-integer-power), so that for every , including .
- If then the series converges (def-series) and
- If then diverges.
The series starts at and its first term is ; in particular , while the series starting at sums to . Which starting index is meant has to be said, and it is said here.
Summability of truncated normalized variances: For identically distributed integrable real and , . No independence is required.
Chebyshev's inequality for random variables: If is a square-integrable real random variable and , then
First Borel-Cantelli lemma for events: Let be events in a probability space. If then
No independence hypothesis is needed.
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.
First suppose . Put , , and . Pairwise independence survives these coordinatewise Borel maps by applying F1 separately to each independent pair. F2 and F3 give .
Fix an integer and . By F4 set for , using F5. For large j, and ; this follows on dividing by . The sequence is eventually strictly increasing, since tends to infinity.
For each m, let be the first nonnegative j with . Apart from finitely many small j, by F6. The omitted finitely many j affect only m<=max , so increasing the constant gives for every m.
Interchanging finite nonnegative double sums and then taking suprema, step 1.1 and step 1.3 give , the last inequality by F7. For each positive integer l, F8 bounds by . F9 and a countable intersection over l imply almost surely.
F10 gives . For , nonnegativity makes . Consequently step 1.2 and step 2.1 give on a conull event.
Intersect these events over . Since and is finite and nonnegative, step 3.1 gives . F11 removes the truncation error. For general real variables, apply this nonnegative result separately to and ; their integrability and pairwise independence follow from the given hypotheses and coordinatewise measurability. Subtracting the two finite limits proves the assertion.
Depends on
- Pairwise independence
- Iid linear truncation occurs only finitely often
- Summability of truncated normalized variances
- Cesaro limit of truncated means
- Chebyshev's inequality for random variables
- Independence forces covariance to vanish
- Variance and covariance identities for random variables
- Measurable coordinatewise functions preserve independence
- First Borel-Cantelli lemma for events
- A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum
- Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$
- Integer powers $a^m$
- For $|r| < 1$, $\sum_{k \ge 0} r^k = 1/(1-r)$, and for $|r| \ge 1$ the series diverges
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
68 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, Theorem 2.4.1, Lemmas 2.4.2–2.4.4 and complete proof, pp. 76–78 (standard reference, not scraped)