Theorem MeasureTheory.Submartingale.predictablePart_nonneg

Modification history

2026-05-26 07:57

Mathlib/Probability/Martingale/Centering.lean

chore: drop completeness from the definition of conditional expectation (#39862) …

Modified MeasureTheory.Submartingale.predictablePart_nonneg View on Github →

2026-04-24 08:11

Mathlib/Probability/Martingale/Centering.lean

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

Added MeasureTheory.Submartingale.predictablePart_nonneg View on Github →