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.

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 #

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
Instances For
    theorem MeasureTheory.leastGE_le {Ω : Type u_1} {f : Ω} {i : } {r : } (ω : Ω) :
    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 (π ω) (MeasureTheory.leastGE f r n ω)
    theorem MeasureTheory.stoppedValue_stoppedValue_leastGE {Ω : Type u_1} (f : Ω) (π : Ω) (r : ) {n : } (hπn : ∀ (ω : Ω), π ω n) :
    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 : ) :
    @[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 : ) :

    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
    Instances For
      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 = kFinset.range n, ((s (k + 1)).indicator 1 - MeasureTheory.condexp ( k) μ ((s (k + 1)).indicator 1))
      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 : ) => kFinset.range n, (s (k + 1)).indicator 1 ω) Filter.atTop Filter.atTop Filter.Tendsto (fun (n : ) => kFinset.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 : ) => kFinset.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) = ∞.