mathlib3 documentation

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 #

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
theorem measure_theory.least_ge_le {Ω : Type u_1} {f : Ω } {i : } {r : } (ω : Ω) :
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) :
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 : ) :
theorem measure_theory.submartingale.exists_tendsto_of_abs_bdd_above_aux {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : measure_theory.filtration m0} {f : Ω } {R : nnreal} [measure_theory.is_finite_measure μ] (hf : measure_theory.submartingale f μ) (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 Ω} {ℱ : measure_theory.filtration m0} {f : Ω } {R : nnreal} [measure_theory.is_finite_measure μ] (hf : measure_theory.submartingale f μ) (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 Ω} {ℱ : measure_theory.filtration m0} {f : Ω } {R : nnreal} [measure_theory.is_finite_measure μ] (hf : measure_theory.submartingale f μ) (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 Ω} {ℱ : measure_theory.filtration m0} {f : Ω } {R : nnreal} [measure_theory.is_finite_measure μ] (hf : measure_theory.martingale f μ) (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 Ω} {ℱ : measure_theory.filtration m0} {f : Ω } {R : nnreal} [measure_theory.is_finite_measure μ] (hf : measure_theory.martingale f μ) (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 Ω} {ℱ : measure_theory.filtration m0} {f : Ω } {R : nnreal} [measure_theory.is_finite_measure μ] (hf : measure_theory.martingale f μ) (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.tendsto_sum_indicator_at_top_iff {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : measure_theory.filtration m0} {f : Ω } {R : nnreal} [measure_theory.is_finite_measure μ] (hfmono : ∀ᵐ (ω : Ω) μ, (n : ), f n ω f (n + 1) ω) (hf : measure_theory.adapted f) (hint : (n : ), measure_theory.integrable (f 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 +∞.

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) = ∞.