Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-22 10:57 e18fa7b9

View on Github →

feat(probability/martingale/centering): uniqueness of Doob's decomposition (#16532)

Estimated changes

Modified src/probability/martingale/basic.lean

added theorem measure_theory.martingale.eq_zero_of_predicatable

added theorem measure_theory.submartingale.zero_le_of_predictable

added theorem measure_theory.supermartingale.le_zero_of_predictable

Modified src/probability/martingale/centering.lean

added theorem measure_theory.martingale_part_add_ae_eq

added theorem measure_theory.predictable_part_add_ae_eq

Modified src/probability/process/adapted.lean

added theorem measure_theory.predictable.adapted