TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21

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.

The first Borel-Cantelli lemma for measures

Statement

Let $(E_{k})_{k \in N}$ be measurable sets in a measure space. If the nonnegative extended sum satisfies

$\sum_{k = 0}^{\infty} μ (E_{k}) < + \infty,$

then

$μ ({lim sup}_{k \to \infty} E_{k}) = 0.$

No independence hypothesis and no finiteness hypothesis on the whole space are required.

Facts & Assumptions

Given: Measurable sets $(E_{k})$ with $S : = \sum_{k} μ (E_{k}) < + \infty$ .

[L1]

Measures are monotone (Measures are monotone) and countably subadditive (Finite and countable subadditivity of measures).

[L2]

The set limsup is $⋂_{N} ⋃_{k \geq N} E_{k}$ (Limit superior and limit inferior of a sequence of sets).

[L3]

A nonnegative extended sum is the supremum of its partial sums (Series in the nonnegative extended real line), while a convergent real series is the limit of its real partial sums (Series, partial sums, convergence and the sum, divergence, and the tail series).

[L4]

A convergent real series and each of its tails converge, with total sum equal to the initial partial sum plus the tail sum (A series converges iff each of its tail series converges, and the sum splits as $s_{N}$ plus the $N$ -th tail).

[L5]

Limits of real sequences respect addition and subtraction (Algebra of limits: sums, scalar multiples, products and quotients).

Proof

technique · direct

1.1

Since $S$ is finite, every $μ (E_{k})$ and every partial sum $s_{n}$ is real. The $s_{n}$ increase and have supremum $S$ ; given $ε > 0$ , the defining property of the supremum supplies $N$ with $S - ε < s_{N} \leq S$ , and then $S - ε < s_{n} \leq S$ for every $n \geq N$ . Thus the real series $\sum_{k} μ (E_{k})$ converges to $S$ , and its tail sums $T_{N} : = \sum_{k \geq N} μ (E_{k})$ are real.

givenL3

1.2

For every $N$ , [L2] gives ${lim sup}_{k} E_{k} \subseteq ⋃_{k \geq N} E_{k}$ , so monotonicity and subadditivity give $μ ({lim sup}_{k} E_{k}) \leq T_{N}$ .

givenL1L2

2.1

If $s_{N} = \sum_{k < N} μ (E_{k})$ , then $T_{N} = S - s_{N}$ by tail invariance, and $s_{N} \to S$ ; hence $T_{N} \to 0$ by the algebra of limits.

step 1.1L4L5

3.1

The nonnegative number $μ ({lim sup}_{k} E_{k})$ is at most every $T_{N}$ by step 1.2, while step 2.1 makes those tails arbitrarily small; therefore it is $0$ .

step 1.2step 2.1∎

Depends on

Used by

Borel-Cantelli for the shrinking intervals (0,2⁻ᵏ) under a dyadic atomic measure Example

Dependency tree · two levels

36 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

S. Axler, Measure, Integration & Real Analysis, Theorem 12.6 (standard reference, not scraped)
T. Tao, An Introduction to Measure Theory, Exercise 1.4.44 (standard reference, not scraped)