Commit 2026-04-24 08:11 e1f3ae32

View on Github →

feat(ProbabilityTheory): add APIs for predicationPart and martingalePart (#38267) Upstream results from https://github.com/RemyDegenne/brownian-motion/pull/422

Estimated changes

Modified Mathlib/Probability/Martingale/Centering.lean

added theorem MeasureTheory.IsPredictable.martingalePart_eq

added theorem MeasureTheory.IsPredictable.predictablePart_eq

added theorem MeasureTheory.Martingale.martingalePart_eq

added theorem MeasureTheory.Martingale.predictablePart_eq_zero

added theorem MeasureTheory.Submartingale.monotone_predictablePart

added theorem MeasureTheory.Submartingale.predictablePart_nonneg

added theorem MeasureTheory.isPredictable_predictablePart

added theorem MeasureTheory.martingalePart_add

added theorem MeasureTheory.martingalePart_smul

added theorem MeasureTheory.martingalePart_zero

added theorem MeasureTheory.predictablePart_add

added theorem MeasureTheory.predictablePart_add_one

added theorem MeasureTheory.predictablePart_smul