Commit 2025-11-03 20:48 397b110f

View on Github →

feat(Probability): predictable processes (#30997)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Probability/Martingale/Basic.lean

added theorem MeasureTheory.Martingale.eq_zero_of_predictable'

added theorem MeasureTheory.Submartingale.zero_le_of_predictable'

added theorem MeasureTheory.Supermartingale.le_zero_of_predictable'

Created Mathlib/Probability/Process/Predictable.lean

added def MeasureTheory.Filtration.predictable

added theorem MeasureTheory.IsPredictable.adapted

added theorem MeasureTheory.IsPredictable.measurableSet_prodMk_add_one_of_predictable

added theorem MeasureTheory.IsPredictable.measurable_add_one

added theorem MeasureTheory.IsPredictable.progMeasurable

added def MeasureTheory.IsPredictable

added theorem MeasureTheory.isPredictable_iff_measurable_add_one

added theorem MeasureTheory.isPredictable_of_measurable_add_one

added theorem MeasureTheory.measurableSet_predictable_Ioc_prod

added theorem MeasureTheory.measurableSet_predictable_Ioi_prod

added theorem MeasureTheory.measurableSet_predictable_singleton_bot_prod

added theorem MeasureTheory.measurableSet_predictable_singleton_prod

added theorem MeasureTheory.measurableSpace_le_predictable_of_measurableSet