Commit 2023-06-19 09:58 9e48670a

View on Github →

feat: port Probability.Martingale.Centering (#5252)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Martingale/Centering.lean

added theorem MeasureTheory.adapted_martingalePart

added theorem MeasureTheory.adapted_predictablePart'

added theorem MeasureTheory.adapted_predictablePart

added theorem MeasureTheory.integrable_martingalePart

added theorem MeasureTheory.martingalePart_add_ae_eq

added theorem MeasureTheory.martingalePart_add_predictablePart

added theorem MeasureTheory.martingalePart_bdd_difference

added theorem MeasureTheory.martingalePart_eq_sum

added theorem MeasureTheory.martingale_martingalePart

added theorem MeasureTheory.predictablePart_add_ae_eq

added theorem MeasureTheory.predictablePart_bdd_difference

added theorem MeasureTheory.predictablePart_zero