mathlib3

ba074af8 - feat(probability/martingale): optional sampling theorem (#14065)

feat(probability/martingale): optional sampling theorem (#14065) We prove the optional sampling theorem: if `τ` is a bounded stopping time and `σ` is another stopping time, then the value of a martingale `f` at the stopping time `min τ σ` is almost everywhere equal to `μ[stopped_value f τ | hσ.measurable_space]`. Co-authored-by: RemyDegenne <remydegenne@gmail.com> Co-authored-by: Rémy Degenne <remydegenne@gmail.com>