/-- **First Borel–Cantelli lemma.** If `∑ μ(Aₙ) < ∞` then `μ(limsup Aₙ) = 0`.
Hint: show `limsup A atTop ⊆ ⋃ k, A (k + n)` for every `n` (rewrite with
`limsup_eq_iInf_iSup_of_nat'` and use `iInf_le`), bound by `measure_iUnion_le`, and let `n → ∞`
with `ENNReal.tendsto_sum_nat_add` and `ge_of_tendsto'`. -/
theorem borel_cantelli_first {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) {A : ℕ → Set Ω}
(hA : ∑' n, μ (A n) ≠ ∞) : μ (limsup A atTop) = 0 := by
sorryShow the compiled solution
/-- **First Borel–Cantelli lemma.** If `∑ P(Aₙ) < ∞`, then almost surely only finitely many of
the events `Aₙ` occur: `P(limsup Aₙ) = 0`. No independence is needed. Proof (as in the lesson):
for every `n`, the event "infinitely many `Aₖ` occur" lies inside `⋃ₖ A_{k+n}`, whose probability
is at most the tail `∑ₖ P(A_{k+n})` of a convergent series, and the tails tend to `0`
(`ENNReal.tendsto_sum_nat_add`). Mathlib's version is `measure_limsup_atTop_eq_zero`. -/
theorem borel_cantelli_first {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) {A : ℕ → Set Ω}
(hA : ∑' n, μ (A n) ≠ ∞) : μ (limsup A atTop) = 0 := by
-- `limsup A = ⋂ n, ⋃ k, A (k + n)`, so it lies in each tail union.
have hsub : ∀ n, limsup A atTop ⊆ ⋃ k, A (k + n) := fun n => by
rw [limsup_eq_iInf_iSup_of_nat']
exact iInf_le (fun n => ⋃ k, A (k + n)) n
-- Each tail union has probability at most the tail of the series.
have hle : ∀ n, μ (limsup A atTop) ≤ ∑' k, μ (A (k + n)) := fun n =>
(measure_mono (hsub n)).trans (measure_iUnion_le _)
-- The tails of a convergent series tend to zero.
exact le_antisymm (ge_of_tendsto' (ENNReal.tendsto_sum_nat_add _ hA) hle) (by simp)Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/MeasureTheoreticProbability.leanTry it in the Lean web editor