Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-24 14:38 34cfcd02

View on Github →

feat(probability/stopping): generalize is_stopping_time.measurable_set_lt and variants beyond ℕ (#12240) The lemma is_stopping_time.measurable_set_lt and the similar results for gt, ge and eq were written for stopping times with value in nat. We generalize those results to linear orders with the order topology.

Estimated changes

Modified src/order/bounds.lean

added theorem exists_glb_Ioi

added theorem exists_lub_Iio

added theorem glb_Ioi_eq_self_or_Ioi_eq_Ici

added theorem le_glb_Ioi

added theorem lub_Iio_eq_self_or_Iio_eq_Iic

added theorem lub_Iio_le

Modified src/probability/stopping.lean

added theorem measure_theory.filtration.const_apply

modified theorem measure_theory.is_stopping_time.add_const

modified theorem measure_theory.is_stopping_time.measurable_set_eq

modified theorem measure_theory.is_stopping_time.measurable_set_eq_le

modified theorem measure_theory.is_stopping_time.measurable_set_ge

added theorem measure_theory.is_stopping_time.measurable_set_gt

modified theorem measure_theory.is_stopping_time.measurable_set_le

modified theorem measure_theory.is_stopping_time.measurable_set_lt

modified theorem measure_theory.is_stopping_time.measurable_set_lt_le

added theorem measure_theory.is_stopping_time.measurable_set_lt_of_is_lub

added theorem measure_theory.is_stopping_time.measurable_set_lt_of_pred

modified def measure_theory.is_stopping_time

modified theorem measure_theory.is_stopping_time_const

modified theorem measure_theory.is_stopping_time_of_measurable_set_eq

modified theorem measure_theory.measurable_set_of_filtration