mathlib

3086d342 - feat(probability/martingale): the discrete stochastic integral of a submartingale is a submartingale (#14909)

feat(probability/martingale): the discrete stochastic integral of a submartingale is a submartingale (#14909) This PR proves that the discrete stochastic integral of a predictable process with a submartingale is a submartingale. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>