Borel_Cantelli_Lemma
Provedborel-cantellimeasure-theoryprobability-theoryproofwiki
If the sum of the measures of a countable collection of measurable sets converges, then the measure of the lim sup is zero.
Preamble
import Mathlib.MeasureTheory.Measure.MeasureSpace
Formal statement
theorem Borel_Cantelli_Lemma {α : Type _} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : ℕ → Set α} (hE : ∀ n, MeasurableSet (E n)) (hsum : ∑' n, μ (E n) < ⊤) : μ (Filter.limsup E Filter.atTop) = 0 := by sorrySource