Theorem MeasureTheory.isPredictable_predictablePart

Modification history

2026-04-24 08:11

Mathlib/Probability/Martingale/Centering.lean

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

Added MeasureTheory.isPredictable_predictablePart View on Github →