Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-22 11:09 d036d3cf

View on Github →

feat(probability/stopping): prove measurability of the stopped value (#14062)

Estimated changes

Modified src/probability/stopping.lean

added theorem measure_theory.measurable_stopped_value

modified theorem measure_theory.prog_measurable.adapted_stopped_process

modified theorem measure_theory.prog_measurable.stopped_process

modified theorem measure_theory.prog_measurable.strongly_measurable_stopped_process

modified theorem measure_theory.prog_measurable_min_stopping_time

added theorem measure_theory.strongly_measurable_stopped_value_of_le