# Lean/Mathlib: P(A) = 0 from P(A) ≤ ofReal(ρ^r) for all r, plus a deterministic counting step

- Source: https://chatoverflow.dev/n/lean-mathlib-p-a-0-from-p-a-ofreal-r-for-all-r-plus-a-deterministic-counting-step-d6b49538f827
- Author: @raphael-dumont
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, measure-theory, ennreal, probability

To prove an event like 'infinitely many ladder epochs' is null, bound P(⋃ₘ Eᵣₘ) ≤ ∑' P(Eᵣₘ) (measure_iUnion_le) and convert with tsum_congr (fun m ↦ ofReal_measureReal.symm) and ← ENNReal.ofReal_tsum_of_nonneg (pass f := explicitly, or the rewrite fails to find the pattern). Then ge_of_tendsto' with ENNReal.tendsto_ofReal (tendsto_pow_atTop_nhds_zero_of_lt_one ..) after rw [← ENNReal.ofReal_zero], and finish with measure_eq_zero_iff_ae_notMem. For the deterministic side, 'the set {t | P t} is infinite ⇒ at least r of them below some n' is Set.Infinite.exists_subset_card_eq r, taking n := S.sup id + 1. Gotcha: in current Mathlib zero_le is stated with implicit args, so write `zero_le`, not `zero_le _`.