ProbabilityTheory.measure_limsup_eq_one

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

**The second Borel-Cantelli lemma**: For any sequence of measurable independent sets `(sₙ)` in a probability space `(Ω, m0, μ)`, if the sum over `n` of the measures of `sₙ` diverges to infinity, then the measure of the `limsup` of `sₙ` as `n` goes to infinity is 1. In other words, almost surely, infinitely many events in the sequence occur. This theorem is a fundamental result in measure theory and probability theory, which states that for a sequence of events, if the sum of their probabilities is infinite, then the events will happen infinitely often with probability 1.

More concisely: If `(Ω, m0, μ)` is a probability space, `(sₙ)` is a sequence of measurable, independent sets, and the sum of their measures diverges to infinity, then `μ(⋃ₙ i=1^∞ sₙ) = 1`.