Commit 2023-06-19 07:36 09f32cc7

View on Github →

feat: port Probability.Martingale.OptionalSampling (#5247)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

deleted theorem MeasureTheory.condexp_of_aEStronglyMeasurable'

added theorem MeasureTheory.condexp_of_aestronglyMeasurable'

Created Mathlib/Probability/Martingale/OptionalSampling.lean

added theorem MeasureTheory.Martingale.condexp_stoppedValue_stopping_time_ae_eq_restrict_le

added theorem MeasureTheory.Martingale.condexp_stopping_time_ae_eq_restrict_eq_const

added theorem MeasureTheory.Martingale.condexp_stopping_time_ae_eq_restrict_eq_const_of_le_const

added theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le

added theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_const

added theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_const_of_countable_range

added theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_of_countable_range

added theorem MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq

added theorem MeasureTheory.Martingale.stoppedValue_min_ae_eq_condexp