Commit 2022-09-11 21:08 87714908
View on Github →chore(probability/martingale): move the optional stopping theorem to its own file (#16464) The idea is to reserve martingale/basic.lean to really basic API about (sub/super)martingales.
chore(probability/martingale): move the optional stopping theorem to its own file (#16464) The idea is to reserve martingale/basic.lean to really basic API about (sub/super)martingales.