Commit 2023-06-20 02:30 51aa827c

View on Github →

feat: port Probability.Martingale.OptionalStopping (#5274)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Martingale/OptionalStopping.lean

added theorem MeasureTheory.Submartingale.expected_stoppedValue_mono

added theorem MeasureTheory.maximal_ineq

added theorem MeasureTheory.smul_le_stoppedValue_hitting

added theorem MeasureTheory.submartingale_iff_expected_stoppedValue_mono

added theorem MeasureTheory.submartingale_of_expected_stoppedValue_mono