Theorem MeasureTheory.IsPredictable.martingalePart_eq

Modification history

2026-06-25 07:54

Mathlib/Probability/Martingale/Centering.lean

chore: remove unused instances (#41013) …

Modified MeasureTheory.IsPredictable.martingalePart_eq View on Github →

2026-04-24 08:11

Mathlib/Probability/Martingale/Centering.lean

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

Added MeasureTheory.IsPredictable.martingalePart_eq View on Github →