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.

Note: the usual Borel-Cantelli lemmas are not in this file. See MeasureTheory.measure_limsup_eq_zero for the first (which does not depend on the results here), and ProbabilityTheory.measure_limsup_eq_one for the second (which does).

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.

Equations

• MeasureTheory.leastGE f r n = MeasureTheory.hitting f (Set.Ici r) 0 n

theorem MeasureTheory.Adapted.isStoppingTime_leastGE {Ω : Type u_1} {m0 : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} (r : ℝ) (n : ℕ) (hf : MeasureTheory.Adapted ℱ f) : MeasureTheory.IsStoppingTime ℱ (MeasureTheory.leastGE f r n)

theorem MeasureTheory.leastGE_le {Ω : Type u_1} {f : ℕ → Ω → ℝ} {i : ℕ} {r : ℝ} (ω : Ω) : MeasureTheory.leastGE f r i ω ≤ i

theorem MeasureTheory.leastGE_mono {Ω : Type u_1} {f : ℕ → Ω → ℝ} {n m : ℕ} (hnm : n ≤ m) (r : ℝ) (ω : Ω) : MeasureTheory.leastGE f r n ω ≤ MeasureTheory.leastGE f r m ω

theorem MeasureTheory.leastGE_eq_min {Ω : Type u_1} {f : ℕ → Ω → ℝ} (π : Ω → ℕ) (r : ℝ) (ω : Ω) {n : ℕ} (hπn : ∀ (ω : Ω), π ω ≤ n) : MeasureTheory.leastGE f r (π ω) ω = π ω ⊓ MeasureTheory.leastGE f r n ω

theorem MeasureTheory.stoppedValue_stoppedValue_leastGE {Ω : Type u_1} (f : ℕ → Ω → ℝ) (π : Ω → ℕ) (r : ℝ) {n : ℕ} (hπn : ∀ (ω : Ω), π ω ≤ n) : MeasureTheory.stoppedValue (fun (i : ℕ) => MeasureTheory.stoppedValue f (MeasureTheory.leastGE f r i)) π = MeasureTheory.stoppedValue (MeasureTheory.stoppedProcess f (MeasureTheory.leastGE f r n)) π

theorem MeasureTheory.Submartingale.stoppedValue_leastGE {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f ℱ μ) (r : ℝ) : MeasureTheory.Submartingale (fun (i : ℕ) => MeasureTheory.stoppedValue f (MeasureTheory.leastGE f r i)) ℱ μ

theorem MeasureTheory.norm_stoppedValue_leastGE_le {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ℕ → Ω → ℝ} {r : ℝ} {R : NNReal} (hr : 0 ≤ r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) (i : ℕ) : ∀ᵐ (ω : Ω) ∂μ, MeasureTheory.stoppedValue f (MeasureTheory.leastGE f r i) ω ≤ r + ↑R

theorem MeasureTheory.Submartingale.stoppedValue_leastGE_eLpNorm_le {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} {r : ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f ℱ μ) (hr : 0 ≤ r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) (i : ℕ) : MeasureTheory.eLpNorm (MeasureTheory.stoppedValue f (MeasureTheory.leastGE f r i)) 1 μ ≤ 2 * μ Set.univ * ENNReal.ofReal (r + ↑R)

@[deprecated MeasureTheory.Submartingale.stoppedValue_leastGE_eLpNorm_le]

theorem MeasureTheory.Submartingale.stoppedValue_leastGE_snorm_le {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} {r : ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f ℱ μ) (hr : 0 ≤ r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) (i : ℕ) : MeasureTheory.eLpNorm (MeasureTheory.stoppedValue f (MeasureTheory.leastGE f r i)) 1 μ ≤ 2 * μ Set.univ * ENNReal.ofReal (r + ↑R)

Alias of MeasureTheory.Submartingale.stoppedValue_leastGE_eLpNorm_le.

theorem MeasureTheory.Submartingale.stoppedValue_leastGE_eLpNorm_le' {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} {r : ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f ℱ μ) (hr : 0 ≤ r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) (i : ℕ) : MeasureTheory.eLpNorm (MeasureTheory.stoppedValue f (MeasureTheory.leastGE f r i)) 1 μ ≤ ↑(2 * μ Set.univ * ENNReal.ofReal (r + ↑R)).toNNReal

@[deprecated MeasureTheory.Submartingale.stoppedValue_leastGE_eLpNorm_le']

theorem MeasureTheory.Submartingale.stoppedValue_leastGE_snorm_le' {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} {r : ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f ℱ μ) (hr : 0 ≤ r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) (i : ℕ) : MeasureTheory.eLpNorm (MeasureTheory.stoppedValue f (MeasureTheory.leastGE f r i)) 1 μ ≤ ↑(2 * μ Set.univ * ENNReal.ofReal (r + ↑R)).toNNReal

Alias of MeasureTheory.Submartingale.stoppedValue_leastGE_eLpNorm_le'.

theorem MeasureTheory.Submartingale.exists_tendsto_of_abs_bddAbove_aux {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f ℱ μ) (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 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f ℱ μ) (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 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f ℱ μ) (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 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Martingale f ℱ μ) (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 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Martingale f ℱ μ) (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 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Martingale f ℱ μ) (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.

Equations

• MeasureTheory.BorelCantelli.process s n = ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1

theorem MeasureTheory.BorelCantelli.process_zero {Ω : Type u_1} {s : ℕ → Set Ω} : MeasureTheory.BorelCantelli.process s 0 = 0

theorem MeasureTheory.BorelCantelli.adapted_process {Ω : Type u_1} {m0 : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {s : ℕ → Set Ω} (hs : ∀ (n : ℕ), MeasurableSet (s n)) : MeasureTheory.Adapted ℱ (MeasureTheory.BorelCantelli.process s)

theorem MeasureTheory.BorelCantelli.martingalePart_process_ae_eq {Ω : Type u_1} {m0 : MeasurableSpace Ω} (ℱ : MeasureTheory.Filtration ℕ m0) (μ : MeasureTheory.Measure Ω) (s : ℕ → Set Ω) (n : ℕ) : MeasureTheory.martingalePart (MeasureTheory.BorelCantelli.process s) ℱ μ n = ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - MeasureTheory.condexp (↑ℱ k) μ ((s (k + 1)).indicator 1))

theorem MeasureTheory.BorelCantelli.predictablePart_process_ae_eq {Ω : Type u_1} {m0 : MeasurableSpace Ω} (ℱ : MeasureTheory.Filtration ℕ m0) (μ : MeasureTheory.Measure Ω) (s : ℕ → Set Ω) (n : ℕ) : MeasureTheory.predictablePart (MeasureTheory.BorelCantelli.process s) ℱ μ n = ∑ k ∈ Finset.range n, MeasureTheory.condexp (↑ℱ k) μ ((s (k + 1)).indicator 1)

theorem MeasureTheory.BorelCantelli.process_difference_le {Ω : Type u_1} (s : ℕ → Set Ω) (ω : Ω) (n : ℕ) : |MeasureTheory.BorelCantelli.process s (n + 1) ω - MeasureTheory.BorelCantelli.process s n ω| ≤ ↑1

theorem MeasureTheory.BorelCantelli.integrable_process {Ω : Type u_1} {m0 : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {s : ℕ → Set Ω} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (hs : ∀ (n : ℕ), MeasurableSet (s n)) (n : ℕ) : MeasureTheory.Integrable (MeasureTheory.BorelCantelli.process s n) μ

theorem MeasureTheory.tendsto_sum_indicator_atTop_iff {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω) (hf : MeasureTheory.Adapted ℱ f) (hint : ∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n ω) Filter.atTop Filter.atTop ↔ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.predictablePart f ℱ μ 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 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ] {s : ℕ → Set Ω} (hs : ∀ (n : ℕ), MeasurableSet (s n)) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) Filter.atTop Filter.atTop ↔ Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range n, MeasureTheory.condexp (↑ℱ k) μ ((s (k + 1)).indicator 1) ω) Filter.atTop Filter.atTop

theorem MeasureTheory.ae_mem_limsup_atTop_iff {Ω : Type u_1} {m0 : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ m0} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {s : ℕ → Set Ω} (hs : ∀ (n : ℕ), MeasurableSet (s n)) : ∀ᵐ (ω : Ω) ∂μ, ω ∈ Filter.limsup s Filter.atTop ↔ Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range n, MeasureTheory.condexp (↑ℱ k) μ ((s (k + 1)).indicator 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) = ∞.