# mathlib3documentation

probability.martingale.borel_cantelli

# 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 #

noncomputable def measure_theory.least_ge {Ω : Type u_1} (f : Ω ) (r : ) (n : ) :
Ω

least_ge f r n is the stopping time corresponding to the first time f ≥ r.

Equations
• = 0 n
theorem measure_theory.adapted.is_stopping_time_least_ge {Ω : Type u_1} {m0 : measurable_space Ω} {ℱ : m0} {f : Ω } (r : ) (n : ) (hf : f) :
theorem measure_theory.least_ge_le {Ω : Type u_1} {f : Ω } {i : } {r : } (ω : Ω) :
ω i
theorem measure_theory.least_ge_mono {Ω : Type u_1} {f : Ω } {n m : } (hnm : n m) (r : ) (ω : Ω) :
ω ω
theorem measure_theory.least_ge_eq_min {Ω : Type u_1} {f : Ω } (π : Ω ) (r : ) (ω : Ω) {n : } (hπn : (ω : Ω), π ω n) :
(π ω) ω = linear_order.min (π ω) n ω)
theorem measure_theory.stopped_value_stopped_value_least_ge {Ω : Type u_1} (f : Ω ) (π : Ω ) (r : ) {n : } (hπn : (ω : Ω), π ω n) :
theorem measure_theory.submartingale.stopped_value_least_ge {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } (hf : μ) (r : ) :
theorem measure_theory.norm_stopped_value_least_ge_le {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {f : Ω } {r : } {R : nnreal} (hr : 0 r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) μ, (i : ), |f (i + 1) ω - f i ω| R) (i : ) :
∀ᵐ (ω : Ω) μ, r + R
theorem measure_theory.submartingale.stopped_value_least_ge_snorm_le {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {r : } {R : nnreal} (hf : μ) (hr : 0 r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) μ, (i : ), |f (i + 1) ω - f i ω| R) (i : ) :
theorem measure_theory.submartingale.stopped_value_least_ge_snorm_le' {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {r : } {R : nnreal} (hf : μ) (hr : 0 r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) μ, (i : ), |f (i + 1) ω - f i ω| R) (i : ) :
theorem measure_theory.submartingale.exists_tendsto_of_abs_bdd_above_aux {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {R : nnreal} (hf : μ) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) μ, (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) μ, bdd_above (set.range (λ (n : ), f n ω)) ( (c : ), filter.tendsto (λ (n : ), f n ω) filter.at_top (nhds c))

This lemma is superceded by submartingale.bdd_above_iff_exists_tendsto.

theorem measure_theory.submartingale.bdd_above_iff_exists_tendsto_aux {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {R : nnreal} (hf : μ) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) μ, (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) μ, bdd_above (set.range (λ (n : ), f n ω)) (c : ), filter.tendsto (λ (n : ), f n ω) filter.at_top (nhds c)
theorem measure_theory.submartingale.bdd_above_iff_exists_tendsto {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {R : nnreal} (hf : μ) (hbdd : ∀ᵐ (ω : Ω) μ, (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) μ, bdd_above (set.range (λ (n : ), f n ω)) (c : ), filter.tendsto (λ (n : ), f n ω) filter.at_top (nhds c)

One sided martingale bound: If f is a submartingale which has uniformly bounded differences, then for almost every ω, f n ω is bounded above (in n) if and only if it converges.

### 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.

theorem measure_theory.martingale.bdd_above_range_iff_bdd_below_range {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {R : nnreal} (hf : μ) (hbdd : ∀ᵐ (ω : Ω) μ, (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) μ, bdd_above (set.range (λ (n : ), f n ω)) bdd_below (set.range (λ (n : ), f n ω))
theorem measure_theory.martingale.ae_not_tendsto_at_top_at_top {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {R : nnreal} (hf : μ) (hbdd : ∀ᵐ (ω : Ω) μ, (i : ), |f (i + 1) ω - f i ω| R) :
theorem measure_theory.martingale.ae_not_tendsto_at_top_at_bot {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {R : nnreal} (hf : μ) (hbdd : ∀ᵐ (ω : Ω) μ, (i : ), |f (i + 1) ω - f i ω| R) :
noncomputable def measure_theory.borel_cantelli.process {Ω : Type u_1} (s : set Ω) (n : ) :
Ω

Auxiliary definition required to prove Lévy's generalization of the Borel-Cantelli lemmas for which we will take the martingale part.

Equations
theorem measure_theory.borel_cantelli.adapted_process {Ω : Type u_1} {m0 : measurable_space Ω} {ℱ : m0} {s : set Ω} (hs : (n : ), measurable_set (s n)) :
theorem measure_theory.borel_cantelli.martingale_part_process_ae_eq {Ω : Type u_1} {m0 : measurable_space Ω} (ℱ : m0) (μ : measure_theory.measure Ω) (s : set Ω) (n : ) :
= (finset.range n).sum (λ (k : ), (s (k + 1)).indicator 1 - μ ((s (k + 1)).indicator 1))
theorem measure_theory.borel_cantelli.predictable_part_process_ae_eq {Ω : Type u_1} {m0 : measurable_space Ω} (ℱ : m0) (μ : measure_theory.measure Ω) (s : set Ω) (n : ) :
= (finset.range n).sum (λ (k : ), μ ((s (k + 1)).indicator 1))
theorem measure_theory.borel_cantelli.process_difference_le {Ω : Type u_1} (s : set Ω) (ω : Ω) (n : ) :
theorem measure_theory.borel_cantelli.integrable_process {Ω : Type u_1} {m0 : measurable_space Ω} {ℱ : m0} {s : set Ω} (μ : measure_theory.measure Ω) (hs : (n : ), measurable_set (s n)) (n : ) :
theorem measure_theory.tendsto_sum_indicator_at_top_iff {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {R : nnreal} (hfmono : ∀ᵐ (ω : Ω) μ, (n : ), f n ω f (n + 1) ω) (hf : f) (hint : (n : ), μ) (hbdd : ∀ᵐ (ω : Ω) μ, (n : ), |f (n + 1) ω - f n ω| R) :

An a.e. monotone adapted process f with uniformly bounded differences converges to +∞ if and only if its predictable part also converges to +∞.

theorem measure_theory.tendsto_sum_indicator_at_top_iff' {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {s : set Ω} (hs : (n : ), measurable_set (s n)) :
∀ᵐ (ω : Ω) μ, filter.tendsto (λ (n : ), (finset.range n).sum (λ (k : ), (s (k + 1)).indicator 1 ω)) filter.at_top filter.at_top filter.tendsto (λ (n : ), (finset.range n).sum (λ (k : ), μ ((s (k + 1)).indicator 1) ω)) filter.at_top filter.at_top
theorem measure_theory.ae_mem_limsup_at_top_iff {Ω : Type u_1} {m0 : measurable_space Ω} {ℱ : m0} (μ : measure_theory.measure Ω) {s : set Ω} (hs : (n : ), measurable_set (s n)) :
∀ᵐ (ω : Ω) μ, filter.tendsto (λ (n : ), (finset.range n).sum (λ (k : ), μ ((s (k + 1)).indicator 1) ω)) filter.at_top filter.at_top

Lévy's generalization of the Borel-Cantelli lemma: given a sequence of sets s and a filtration ℱ such that for all n, s n is ℱ n-measurable, at_top.limsup s is almost everywhere equal to the set for which ∑ k, ℙ(s (k + 1) | ℱ k) = ∞.