Commit 2025-10-27 13:29 0c8813a6

refactor(Probability): change stopping times to take values in WithTop (#29430) This PR changes stopping times to have type Ω → WithTop ι instead of Ω → ι. Previously, a stopping time for a filtration indexed by Nat had to have value in Nat. That's not representative of the way stopping times are used in probability. A typical stopping time is the first time at which we see a head in an infinite sequence of coin flips. That time could be infinite (although it is almost surely finite). We can't represent it with a Ω → Nat stopping time: if we choose an arbitrary value in Nat for the event that it is infinite, we destroy the stopping time property. We faced that issue in the BorelCantelli file, in which we avoided such a possibly infinite stopping time by introducing a sequence of bounded stopping times. We had to prove additional lemmas about them since we could not directly use the API for stopped processes. With the new type, that file is greatly simplified as the API is directly usable, and we can write the proof as we would on paper. The issue with the previous stopping time implementation was noted in [Ying and Degenne, A Formalization of Doob’s Martingale Convergence Theorems in mathlib, CPP 2023, https://dl.acm.org/doi/pdf/10.1145/3573105.3575675]. Other changes:

• the sigma-algebra generated by a stopping time is now a sub-sigma algebra by definition
• measurableSet_eq_stopping_time is generalized and the now useless measurableSet_eq_stopping_time_of_countable is removed
• hitting is renamed to hittingBtwn
• a new hittingAfter is introduced and used in the Borel-Cantelli proof. That proof is now much simpler since we can use a stopped process as intended instead of going around the limitations of the previous stopping time implementation.