Commit 2025-01-21 18:51 8e7550d9

refactor(Probability.Martingale.BorelCantelli): move and simplify lemmas about indicators (#19039) Two lemmas about indicators (limsup_eq_tendsto_sum_indicator_nat_atTop, limsup_eq_tendsto_sum_indicator_atTop) are moved from Mathlib.Topology.Algebra.Order.LiminfLimsup to a new file Mathlib.Topology.Algebra.IndicatorCard . Mathlib.Probability.Martingale.BorelCantelli. I'm not completely sure this is the right place for them, but it simplifies significantly the imports and these lemmas weren't used anywhere else, so... Their proofs are also significantly simplified. There are two new lemma Set.sum_indicator_eventually_eq_card and Set.infinite_iff_tendsto_sum_indicator_atTop which seem more versatile and concentrate most of the difficulty, limsup_eq_tendsto_sum_indicator_nat_atTop is removed (it is less general than the last result), and limsup_eq_tendsto_sum_indicator_atTop is deduced very quickly from Set.infinite_iff_tendsto_sum_indicator_atTop. The statement of Set.infinite_iff_tendsto_sum_indicator_atTop is also slightly generalized.