Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 19:31 ad88a836

View on Github →

feat(probability_theory/martingale): add super/sub-martingales (#10710)

Estimated changes

Modified src/measure_theory/function/conditional_expectation.lean

Modified src/probability_theory/martingale.lean

added theorem measure_theory.martingale.set_integral_eq

added theorem measure_theory.martingale.submartingale

added theorem measure_theory.martingale.supermartingale

added theorem measure_theory.martingale_iff

added theorem measure_theory.submartingale.adapted

added theorem measure_theory.submartingale.add

added theorem measure_theory.submartingale.add_martingale

added theorem measure_theory.submartingale.ae_le_condexp

added theorem measure_theory.submartingale.integrable

added theorem measure_theory.submartingale.measurable

added theorem measure_theory.submartingale.neg

added theorem measure_theory.submartingale.set_integral_le

added theorem measure_theory.submartingale.smul_nonneg

added theorem measure_theory.submartingale.smul_nonpos

added theorem measure_theory.submartingale.sub_martingale

added theorem measure_theory.submartingale.sub_supermartingale

added def measure_theory.submartingale

added theorem measure_theory.supermartingale.adapted

added theorem measure_theory.supermartingale.add

added theorem measure_theory.supermartingale.add_martingale

added theorem measure_theory.supermartingale.condexp_ae_le

added theorem measure_theory.supermartingale.integrable

added theorem measure_theory.supermartingale.measurable

added theorem measure_theory.supermartingale.neg

added theorem measure_theory.supermartingale.set_integral_le

added theorem measure_theory.supermartingale.smul_nonneg

added theorem measure_theory.supermartingale.smul_nonpos

added theorem measure_theory.supermartingale.sub_martingale

added theorem measure_theory.supermartingale.sub_submartingale

added def measure_theory.supermartingale