Theorem MeasureTheory.martingalePart_add_predictablePart

Modification history

2023-06-19 09:58

Mathlib/Probability/Martingale/Centering.lean

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

Added MeasureTheory.martingalePart_add_predictablePart View on Github →