Alphabeta MathHow 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.
First Borel-Cantelli lemma for events
Statement
Let be events in a probability space. If then
No independence hypothesis is needed.
Facts & Assumptions
Given: Events with .
The infinitely-often event is the set limsup. (Limsup and the infinitely often event)
If the sum of the measures is finite, then the measure of the set limsup is zero. (The first Borel-Cantelli lemma for measures)
Proof
By [L1], the event is exactly .
Applying [L2] to the probability measure and the measurable sets gives
Depends on
Used by
- Brownian paths have infinite total variation Corollary
- Summable untruncated variances are not necessary Counterexample
- Weak tests against likelihood tilts do not ensure almost-sure posterior consistency Counterexample
- A square-integrable linear shift with nonsummable physical dependence Example
- A summable tail bound becomes an almost-sure eventual bound Example
- Cauchy sequences in probability have a measurable limit Lemma
- Exponential tests and KL mass force posterior exclusion Lemma
- Finite moments control increments over short moving windows Lemma
- Iid linear truncation occurs only finitely often Lemma
- Independent Brownian motion straightens a Poisson clock Lemma
- Necessity of the truncated mean and variance conditions Lemma
- Zero-variance geometric Markov sums have a uniform strong rate Lemma
- An almost-surely convergent subsequence from convergence in probability Theorem
- Brownian law of the iterated logarithm at infinity Theorem
- Brownian paths are nowhere differentiable Theorem
- Brownian quadratic variation on dyadic partitions Theorem
- Etemadi strong law for pairwise independent iid variables Theorem
- Functional central limit theorem by bracketing entropy Theorem
- Kolmogorov continuity criterion in one parameter Theorem
- Kolmogorov three-series theorem Theorem
- Pairwise-independent Borel-Cantelli frequency law Theorem
- Posterior consistency from KL support and uniformly summable tests Theorem
- Strong invariance principle for geometrically ergodic chains Theorem
- Tang's conditional recommendation sampler Theorem
- Uniform dyadic Brownian quadratic variation process Theorem
Dependency tree · two levels
10 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.1 (standard reference, not scraped)