# Documentation

Mathlib.Probability.Martingale.BorelCantelli

# Generalized Borel-Cantelli lemma #

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 #

• MeasureTheory.Submartingale.bddAbove_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.
• MeasureTheory.ae_mem_limsup_atTop_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 atTop s is almost everywhere equal to the set for which ∑ ℙ[s (n + 1)∣ℱ n] = ∞.

### One sided martingale bound #

noncomputable def MeasureTheory.leastGE {Ω : Type u_1} (f : Ω) (r : ) (n : ) :
Ω

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

Instances For
theorem MeasureTheory.Adapted.isStoppingTime_leastGE {Ω : Type u_1} {m0 : } {ℱ : } {f : Ω} (r : ) (n : ) (hf : ) :
theorem MeasureTheory.leastGE_le {Ω : Type u_1} {f : Ω} {i : } {r : } (ω : Ω) :
i
theorem MeasureTheory.leastGE_mono {Ω : Type u_1} {f : Ω} {n : } {m : } (hnm : n m) (r : ) (ω : Ω) :
theorem MeasureTheory.leastGE_eq_min {Ω : Type u_1} {f : Ω} (π : Ω) (r : ) (ω : Ω) {n : } (hπn : ∀ (ω : Ω), π ω n) :
MeasureTheory.leastGE f r (π ω) ω = min (π ω) ()
theorem MeasureTheory.stoppedValue_stoppedValue_leastGE {Ω : Type u_1} (f : Ω) (π : Ω) (r : ) {n : } (hπn : ∀ (ω : Ω), π ω n) :
theorem MeasureTheory.Submartingale.stoppedValue_leastGE {Ω : Type u_1} {m0 : } {μ : } {ℱ : } {f : Ω} (hf : ) (r : ) :
MeasureTheory.Submartingale (fun i => ) μ
theorem MeasureTheory.norm_stoppedValue_leastGE_le {Ω : Type u_1} {m0 : } {μ : } {f : Ω} {r : } {R : NNReal} (hr : 0 r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |f (i + 1) ω - f i ω| R) (i : ) :
∀ᵐ (ω : Ω) ∂μ, r + R
theorem MeasureTheory.Submartingale.stoppedValue_leastGE_snorm_le {Ω : Type u_1} {m0 : } {μ : } {ℱ : } {f : Ω} {r : } {R : NNReal} (hf : ) (hr : 0 r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |f (i + 1) ω - f i ω| R) (i : ) :
2 * μ Set.univ * ENNReal.ofReal (r + R)
theorem MeasureTheory.Submartingale.stoppedValue_leastGE_snorm_le' {Ω : Type u_1} {m0 : } {μ : } {ℱ : } {f : Ω} {r : } {R : NNReal} (hf : ) (hr : 0 r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |f (i + 1) ω - f i ω| R) (i : ) :
↑(ENNReal.toNNReal (2 * μ Set.univ * ENNReal.ofReal (r + R)))
theorem MeasureTheory.Submartingale.exists_tendsto_of_abs_bddAbove_aux {Ω : Type u_1} {m0 : } {μ : } {ℱ : } {f : Ω} {R : NNReal} (hf : ) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω)c, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds c)

This lemma is superseded by Submartingale.bddAbove_iff_exists_tendsto.

theorem MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto_aux {Ω : Type u_1} {m0 : } {μ : } {ℱ : } {f : Ω} {R : NNReal} (hf : ) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) c, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds c)
theorem MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto {Ω : Type u_1} {m0 : } {μ : } {ℱ : } {f : Ω} {R : NNReal} (hf : ) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) c, Filter.Tendsto (fun n => f n ω) Filter.atTop (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 MeasureTheory.Martingale.bddAbove_range_iff_bddBelow_range {Ω : Type u_1} {m0 : } {μ : } {ℱ : } {f : Ω} {R : NNReal} (hf : ) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) BddBelow (Set.range fun n => f n ω)
theorem MeasureTheory.Martingale.ae_not_tendsto_atTop_atTop {Ω : Type u_1} {m0 : } {μ : } {ℱ : } {f : Ω} {R : NNReal} (hf : ) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) ∂μ, ¬Filter.Tendsto (fun n => f n ω) Filter.atTop Filter.atTop
theorem MeasureTheory.Martingale.ae_not_tendsto_atTop_atBot {Ω : Type u_1} {m0 : } {μ : } {ℱ : } {f : Ω} {R : NNReal} (hf : ) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) ∂μ, ¬Filter.Tendsto (fun n => f n ω) Filter.atTop Filter.atBot
noncomputable def MeasureTheory.BorelCantelli.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.

Instances For
theorem MeasureTheory.BorelCantelli.adapted_process {Ω : Type u_1} {m0 : } {ℱ : } {s : Set Ω} (hs : ∀ (n : ), MeasurableSet (s n)) :
theorem MeasureTheory.BorelCantelli.martingalePart_process_ae_eq {Ω : Type u_1} {m0 : } (ℱ : ) (μ : ) (s : Set Ω) (n : ) :
= Finset.sum () fun k => Set.indicator (s (k + 1)) 1 - MeasureTheory.condexp ( k) μ (Set.indicator (s (k + 1)) 1)
theorem MeasureTheory.BorelCantelli.predictablePart_process_ae_eq {Ω : Type u_1} {m0 : } (ℱ : ) (μ : ) (s : Set Ω) (n : ) :
= Finset.sum () fun k => MeasureTheory.condexp ( k) μ (Set.indicator (s (k + 1)) 1)
theorem MeasureTheory.BorelCantelli.process_difference_le {Ω : Type u_1} (s : Set Ω) (ω : Ω) (n : ) :
|| 1
theorem MeasureTheory.BorelCantelli.integrable_process {Ω : Type u_1} {m0 : } {ℱ : } {s : Set Ω} (μ : ) (hs : ∀ (n : ), MeasurableSet (s n)) (n : ) :
theorem MeasureTheory.tendsto_sum_indicator_atTop_iff {Ω : Type u_1} {m0 : } {μ : } {ℱ : } {f : Ω} {R : NNReal} (hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ), f n ω f (n + 1) ω) (hf : ) (hint : ∀ (n : ), ) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ), |f (n + 1) ω - f n ω| R) :
∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun n => f n ω) Filter.atTop Filter.atTop Filter.Tendsto (fun n => ) Filter.atTop Filter.atTop

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

theorem MeasureTheory.tendsto_sum_indicator_atTop_iff' {Ω : Type u_1} {m0 : } {μ : } {ℱ : } {s : Set Ω} (hs : ∀ (n : ), MeasurableSet (s n)) :
∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun n => Finset.sum () fun k => Set.indicator (s (k + 1)) 1 ω) Filter.atTop Filter.atTop Filter.Tendsto (fun n => Finset.sum () fun k => MeasureTheory.condexp ( k) μ (Set.indicator (s (k + 1)) 1) ω) Filter.atTop Filter.atTop
theorem MeasureTheory.ae_mem_limsup_atTop_iff {Ω : Type u_1} {m0 : } {ℱ : } (μ : ) {s : Set Ω} (hs : ∀ (n : ), MeasurableSet (s n)) :
∀ᵐ (ω : Ω) ∂μ, ω Filter.limsup s Filter.atTop Filter.Tendsto (fun n => Finset.sum () fun k => MeasureTheory.condexp ( k) μ (Set.indicator (s (k + 1)) 1) ω) Filter.atTop Filter.atTop

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, limsup s atTop is almost everywhere equal to the set for which ∑ k, ℙ(s (k + 1) | ℱ k) = ∞.