Commit 2022-07-27 19:44 3086d342

View on Github →

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.

Estimated changes

Modified src/probability/martingale.lean

added theorem measure_theory.submartingale.sum_mul_sub'

added theorem measure_theory.submartingale.sum_mul_sub

Modified src/probability/stopping.lean

deleted theorem measure_theory.adapted.add

added theorem measure_theory.adapted.inv

added theorem measure_theory.adapted.mul

deleted theorem measure_theory.adapted.neg

modified theorem measure_theory.adapted.smul

added theorem measure_theory.adapted.strongly_measurable

added theorem measure_theory.adapted.strongly_measurable_le