Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-23 16:11 7a6d8505

View on Github →

feat(probability/stopping): measurability of comparisons of stopping times (#14061) Among other related results, prove that {x | τ x ≤ π x} is measurable with respect to the sigma algebras generated by each of the two stopping times involved.

Estimated changes

Modified src/measure_theory/group/arithmetic.lean

added theorem measurable_set_eq_fun_of_encodable

Modified src/probability/stopping.lean

added theorem measure_theory.is_stopping_time.measurable_set_eq_stopping_time

added theorem measure_theory.is_stopping_time.measurable_set_eq_stopping_time_of_encodable

added theorem measure_theory.is_stopping_time.measurable_set_inter_le_iff

added theorem measure_theory.is_stopping_time.measurable_set_le_stopping_time

added theorem measure_theory.is_stopping_time.measurable_set_min_const_iff

added theorem measure_theory.is_stopping_time.measurable_set_stopping_time_le

added theorem measure_theory.is_stopping_time.measurable_space_le'

modified theorem measure_theory.is_stopping_time.measurable_space_le

added theorem measure_theory.is_stopping_time.measurable_space_le_of_encodable

added theorem measure_theory.is_stopping_time.measurable_space_min_const