Commit 2022-09-10 10:02 7fd4a0bf

View on Github →

feat(probability/stopping): generalize mem_ℒp_stopped_value (#16369) Also rename many lemmas which had names *_of_encodable but took countable arguments since a recent PR which replaced all encodable by countable but did not touch the names.

Estimated changes

Modified src/probability/martingale/basic.lean

Modified src/probability/stopping.lean

modified theorem measure_theory.integrable_stopped_value

added theorem measure_theory.integrable_stopped_value_of_mem_finset

added theorem measure_theory.is_stopping_time.measurable_set_inter_le_const_iff

added theorem measure_theory.is_stopping_time.measurable_space_le_of_countable

deleted theorem measure_theory.is_stopping_time.measurable_space_le_of_encodable

added theorem measure_theory.is_stopping_time.measurable_space_le_of_le

modified theorem measure_theory.mem_ℒp_stopped_value

added theorem measure_theory.mem_ℒp_stopped_value_of_mem_finset

added theorem measure_theory.stopped_value_eq'

added theorem measure_theory.stopped_value_eq_of_mem_finset