mathlib

fe445767 - feat(probability/martingale): the optional stopping theorem (#13630)

feat(probability/martingale): the optional stopping theorem (#13630) We prove the optional stopping theorem (also known as the fair game theorem). This is number 62 on Freek 100 theorems. Co-authored-by: RemyDegenne <Remydegenne@gmail.com> Co-authored-by: Rémy Degenne <remydegenne@gmail.com>