mathlib

8c9342fd - feat(probability/martingale/borel_cantelli): Lévy's generalized Borel-Cantelli (#16358)

feat(probability/martingale/borel_cantelli): Lévy's generalized Borel-Cantelli (#16358) This PR proves the one sided martingale bound and uses it to prove the Lévy's generalized Borel-Cantelli lemma. With the generalized Borel-Cantelli, the still missing second Borel-Cantelli lemma follows by choosing an appropriate filtration. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>