mathlib3

e2333f32 - feat(probability/upcrossing): Doob's upcrossing estimate (#14933)

feat(probability/upcrossing): Doob's upcrossing estimate (#14933) This PR proves Doob's upcrossing estimate which is central for the martingale convergence theorems. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>