TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05

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.

Pairwise-independent Borel-Cantelli frequency law

Statement

Let $(A_{n})_{n \geq 1}$ be pairwise independent events with $\sum_{n = 1}^{\infty} P (A_{n}) = + \infty .$ For $n \geq 1$ , put $S_{n} : = \sum_{k = 1}^{n} 1_{A_{k}}, a_{n} : = \sum_{k = 1}^{n} P (A_{k}) .$ Then $a_{n} > 0$ for all sufficiently large $n$ , and for those $n$ Then $\frac{S_{n}}{a_{n}} ⟶ 1 almost surely.$

Facts & Assumptions

Given: Pairwise independent events $(A_{n})_{n \geq 1}$ with $\sum_{n = 1}^{\infty} P (A_{n}) = + \infty$ , and the sums $S_{n}, a_{n}$ of the Statement.

[L1]

Pairwise independence means $P (A_{i} \cap A_{j}) = P (A_{i}) P (A_{j}) (i \neq j) .$ (Pairwise independence)

[L2]

An indicator of a measurable event is a real random variable, and its expectation is the probability of the event. (An indicator function is measurable exactly when its set is measurable, The expectation of an indicator is the probability of the event)

[L3]

Finite sums, products, and absolute values of measurable real-valued functions are measurable. (Arithmetic and lattice operations preserve measurability whenever they are defined)

[L4]

Expectation is linear on integrable random variables, and $Var (X) = E [X^{2}] - E [X]^{2}$ for square-integrable real random variables. (Linearity, monotonicity, and the modulus bound for expectation, Variance and covariance identities for random variables)

[L5]

Chebyshev's inequality bounds the probability of a centered deviation by variance divided by the square threshold. (Chebyshev's inequality for random variables)

[L6]

If a sum of event probabilities is finite, then the corresponding limsup event has probability zero. (First Borel-Cantelli lemma for events)

Proof

technique · direct

1.1

For each $k$ , the indicator $1_{A_{k}}$ is a real random variable by [L2]. Repeated use of [L4] and [L2] gives $E [S_{n}] = \sum_{k = 1}^{n} E [1_{A_{k}}] = \sum_{k = 1}^{n} P (A_{k}) = a_{n} .$ The divergence hypothesis makes $a_{n} \to + \infty$ . In particular, there is $N \geq 1$ with $a_{n} > 0$ for every $n \geq N$ .

givenL2L4

2.1

For $i \neq j$ , step 1.1 and [L1] give $E [1_{A_{i}} 1_{A_{j}}] = E [1_{A_{i} \cap A_{j}}] = P (A_{i} \cap A_{j}) = P (A_{i}) P (A_{j}) = E [1_{A_{i}}] E [1_{A_{j}}] .$ Also $1_{A_{k}}^{2} = 1_{A_{k}}$ for every $k$ .

step 1.1L1L2algebra

3.1

By [L3], the partial sum $S_{n}$ and its square $S_{n}^{2}$ are measurable. Expanding $S_{n}^{2}$ and using step 2.1 together with linearity from [L4] yields $E [S_{n}^{2}] = \sum_{k = 1}^{n} P (A_{k}) + 2 \sum_{1 \leq i < j \leq n} P (A_{i}) P (A_{j}) = a_{n}^{2} + \sum_{k = 1}^{n} (P (A_{k}) - P (A_{k})^{2}) \leq a_{n}^{2} + a_{n} .$ So $S_{n}$ is square-integrable, and [L4] gives $Var (S_{n}) = E [S_{n}^{2}] - E [S_{n}]^{2} \leq a_{n} .$

step 1.1step 2.1L3L4algebra

4.1

Fix $ε > 0$ and $n \geq N$ . Applying [L5] to $S_{n}$ gives $P (∣ \frac{S_{n}}{a_{n}} - 1 ∣ \geq ε) = P (∣ S_{n} - a_{n} ∣ \geq ε a_{n}) \leq \frac{Var (S_{n})}{ε^{2} a_{n}^{2}} \leq \frac{1}{ε^{2} a_{n}} .$ Hence $S_{n} / a_{n} \to 1$ in probability along the defined tail $n \geq N$ .

step 1.1step 3.1L5algebra

5.1

For each integer $m \geq 1$ , let $n_{m}$ be the least index with $a_{n_{m}} \geq a_{1} + m^{2}$ ; it exists by step 1.1. Since $a_{n_{m} - 1} < a_{1} + m^{2} \leq a_{n_{m}}$ and $a_{n_{m}} - a_{n_{m} - 1} = P (A_{n_{m}}) \leq 1$ , one has $a_{1} + m^{2} \leq a_{n_{m}} < a_{1} + m^{2} + 1.$ Therefore step 4.1 yields $P (∣ \frac{S_{n_{m}}}{a_{n_{m}}} - 1 ∣ \geq ε) \leq \frac{1}{ε^{2} (a_{1} + m^{2})},$ and the sum over $m$ is finite.

step 1.1step 4.1algebra

6.1

For each integer $r \geq 1$ , step 5.1 with $ε = 1 / r$ gives $\sum_{m = 1}^{\infty} P (∣ \frac{S_{n_{m}}}{a_{n_{m}}} - 1 ∣ \geq \frac{1}{r}) < + \infty .$ Applying [L6] to these deviation events shows that, for each $r$ , only finitely many of them occur almost surely.

step 5.1L6

7.1

Intersect the full-probability events from step 6.1 over all $r \in N_{> 0}$ . On that still full-probability event, for every $r$ there is $M_{r} (ω)$ such that $∣ \frac{S_{n_{m}} (ω)}{a_{n_{m}}} - 1 ∣ < \frac{1}{r} (m \geq M_{r} (ω)) .$ Hence $S_{n_{m}} / a_{n_{m}} \to 1$ almost surely.

step 6.1algebra

8.1

Fix $ω$ in the full-probability event from step 7.1. If $n_{m} \leq n < n_{m + 1}$ , then $S_{n_{m}} (ω) \leq S_{n} (ω) \leq S_{n_{m + 1}} (ω)$ and $a_{n_{m}} \leq a_{n} < a_{n_{m + 1}}$ , so $\frac{S_{n_{m}} (ω)}{a_{n_{m + 1}}} \leq \frac{S_{n} (ω)}{a_{n}} \leq \frac{S_{n_{m + 1}} (ω)}{a_{n_{m}}} .$ Since $a_{n_{m}} / a_{n_{m + 1}} \to 1$ and $a_{n_{m + 1}} / a_{n_{m}} \to 1$ by the bounds in step 5.1, step 7.1 squeezes $S_{n} (ω) / a_{n}$ to $1$ . Therefore $S_{n} / a_{n} \to 1$ almost surely for all sufficiently large $n$ , equivalently for all $n$ with $a_{n} > 0$ .

step 5.1step 7.1algebra

9.1

Step 8.1 is exactly the asserted frequency law.

step 8.1∎

Depends on

Used by

Second Borel-Cantelli lemma under pairwise independence Corollary

Dependency tree · two levels

25 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

Rick Durrett, Probability: Theory and Examples, 5th ed., Theorem 2.3.9 (standard reference, not scraped)