Theorems · Theorem · probability

ProbabilityTheory.measure_limsup_eq_one

∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ℕ → Set Ω},
  (∀ (n : ℕ), MeasurableSet (s n)) →
    ProbabilityTheory.iIndepSet s μ → ∑' (n : ℕ), μ (s n) = ⊤ → μ (Filter.limsup s Filter.atTop) = 1

The second Borel-Cantelli lemma: Given a sequence of independent sets (sₙ) such that ∑ n, μ sₙ = ∞, limsup sₙ has measure 1.

Defined in

Mathlib.Probability.BorelCantelli

Cited by

0 results in Mathlib

Foundations

Depth 325 from the axioms · uses propext, Classical.choice, Quot.sound