Commit 2023-06-19 04:18 04d2fe96

View on Github →

feat: port Probability.Martingale.Basic (#5215)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Martingale/Basic.lean

added theorem MeasureTheory.Martingale.add

added theorem MeasureTheory.Martingale.condexp_ae_eq

added theorem MeasureTheory.Martingale.eq_zero_of_predictable

added theorem MeasureTheory.Martingale.neg

added theorem MeasureTheory.Martingale.set_integral_eq

added theorem MeasureTheory.Martingale.smul

added theorem MeasureTheory.Martingale.sub

added theorem MeasureTheory.Martingale.submartingale

added theorem MeasureTheory.Martingale.supermartingale

added def MeasureTheory.Martingale

added theorem MeasureTheory.Submartingale.add

added theorem MeasureTheory.Submartingale.add_martingale

added theorem MeasureTheory.Submartingale.ae_le_condexp

added theorem MeasureTheory.Submartingale.condexp_sub_nonneg

added theorem MeasureTheory.Submartingale.neg

added theorem MeasureTheory.Submartingale.set_integral_le

added theorem MeasureTheory.Submartingale.smul_nonneg

added theorem MeasureTheory.Submartingale.smul_nonpos

added theorem MeasureTheory.Submartingale.sub_martingale

added theorem MeasureTheory.Submartingale.sub_supermartingale

added theorem MeasureTheory.Submartingale.sum_mul_sub'

added theorem MeasureTheory.Submartingale.sum_mul_sub

added theorem MeasureTheory.Submartingale.zero_le_of_predictable

added def MeasureTheory.Submartingale

added theorem MeasureTheory.Supermartingale.add

added theorem MeasureTheory.Supermartingale.add_martingale

added theorem MeasureTheory.Supermartingale.condexp_ae_le

added theorem MeasureTheory.Supermartingale.le_zero_of_predictable

added theorem MeasureTheory.Supermartingale.neg

added theorem MeasureTheory.Supermartingale.set_integral_le

added theorem MeasureTheory.Supermartingale.smul_nonneg

added theorem MeasureTheory.Supermartingale.smul_nonpos

added theorem MeasureTheory.Supermartingale.sub_martingale

added theorem MeasureTheory.Supermartingale.sub_submartingale

added def MeasureTheory.Supermartingale

added theorem MeasureTheory.martingale_condexp

added theorem MeasureTheory.martingale_const

added theorem MeasureTheory.martingale_const_fun

added theorem MeasureTheory.martingale_iff

added theorem MeasureTheory.martingale_nat

added theorem MeasureTheory.martingale_of_condexp_sub_eq_zero_nat

added theorem MeasureTheory.martingale_of_set_integral_eq_succ

added theorem MeasureTheory.martingale_zero

added theorem MeasureTheory.submartingale_iff_condexp_sub_nonneg

added theorem MeasureTheory.submartingale_nat

added theorem MeasureTheory.submartingale_of_condexp_sub_nonneg

added theorem MeasureTheory.submartingale_of_condexp_sub_nonneg_nat

added theorem MeasureTheory.submartingale_of_set_integral_le

added theorem MeasureTheory.submartingale_of_set_integral_le_succ

added theorem MeasureTheory.supermartingale_nat

added theorem MeasureTheory.supermartingale_of_condexp_sub_nonneg_nat

added theorem MeasureTheory.supermartingale_of_set_integral_succ_le