Generalized Borel-Cantelli lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves Lévy's generalized Borel-Cantelli lemma which is a generalization of the Borel-Cantelli lemmas. With this generalization, one can easily deduce the Borel-Cantelli lemmas by choosing appropriate filtrations. This file also contains the one sided martingale bound which is required to prove the generalized Borel-Cantelli.

Main results #

• measure_theory.submartingale.bdd_above_iff_exists_tendsto: the one sided martingale bound: given a submartingale f with uniformly bounded differences, the set for which f converges is almost everywhere equal to the set for which it is bounded.
• measure_theory.ae_mem_limsup_at_top_iff: Lévy's generalized Borel-Cantelli: given a filtration ℱ and a sequence of sets s such that s n ∈ ℱ n for all n, limsup at_top s is almost everywhere equal to the set for which ∑ ℙ[s (n + 1)∣ℱ n] = ∞.

One sided martingale bound #

Lévy's generalization of the Borel-Cantelli lemma #

Lévy's generalization of the Borel-Cantelli lemma states that: given a natural number indexed filtration $(\mathcal{F}_n)$, and a sequence of sets $(s_n)$ such that for all $n$, $s_n \in \mathcal{F}_n$, $limsup_n s_n$ is almost everywhere equal to the set for which $\sum_n \mathbb{P}[s_n \mid \mathcal{F}_n] = \infty$.

The proof strategy follows by constructing a martingale satisfying the one sided martingale bound. In particular, we define $$ f_n := \sum_{k < n} \mathbf{1}_{s_{n + 1}} - \mathbb{P}[s_{n + 1} \mid \mathcal{F}_n]. $$ Then, as a martingale is both a sub and a super-martingale, the set for which it is unbounded from above must agree with the set for which it is unbounded from below almost everywhere. Thus, it can only converge to $\pm \infty$ with probability 0. Thus, by considering $$ \limsup_n s_n = \{\sum_n \mathbf{1}_{s_n} = \infty\} $$ almost everywhere, the result follows.