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

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 _.