Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-15 13:13 764d7a90

View on Github →

feat(probability/stopping): first hitting time (#14630) This PR adds the first hitting time (before some time) and proves that it is a stopping time in the discrete case.

Estimated changes

Created src/probability/hitting_time.lean

added theorem measure_theory.hitting_bot_le_iff

added theorem measure_theory.hitting_eq_Inf

added theorem measure_theory.hitting_is_stopping_time

added theorem measure_theory.hitting_le

added theorem measure_theory.hitting_le_iff_of_exists

added theorem measure_theory.hitting_le_iff_of_lt

added theorem measure_theory.hitting_le_of_mem

added theorem measure_theory.hitting_lt_iff

added theorem measure_theory.hitting_mem_Icc

added theorem measure_theory.hitting_mem_set

added theorem measure_theory.hitting_of_lt

added theorem measure_theory.le_hitting

added theorem measure_theory.le_hitting_of_exists