Theorem MeasureTheory.predictablePart_add_one

Modification history

2026-04-24 08:11

Mathlib/Probability/Martingale/Centering.lean

feat(ProbabilityTheory): add APIs for predicationPart and martingalePart (#38267) …

Added MeasureTheory.predictablePart_add_one View on Github →