Commit 2023-06-19 04:18 ab4ba6c4

View on Github →

feat: port Probability.Process.HittingTime (#5222)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Process/HittingTime.lean

added theorem MeasureTheory.hitting_bot_le_iff

added theorem MeasureTheory.hitting_eq_end_iff

added theorem MeasureTheory.hitting_eq_hitting_of_exists

added theorem MeasureTheory.hitting_eq_sInf

added theorem MeasureTheory.hitting_isStoppingTime

added theorem MeasureTheory.hitting_le

added theorem MeasureTheory.hitting_le_iff_of_exists

added theorem MeasureTheory.hitting_le_iff_of_lt

added theorem MeasureTheory.hitting_le_of_mem

added theorem MeasureTheory.hitting_lt_iff

added theorem MeasureTheory.hitting_mem_Icc

added theorem MeasureTheory.hitting_mem_set

added theorem MeasureTheory.hitting_mem_set_of_hitting_lt

added theorem MeasureTheory.hitting_mono

added theorem MeasureTheory.hitting_of_le

added theorem MeasureTheory.hitting_of_lt

added theorem MeasureTheory.isStoppingTime_hitting_isStoppingTime

added theorem MeasureTheory.le_hitting

added theorem MeasureTheory.le_hitting_of_exists

added theorem MeasureTheory.not_mem_of_lt_hitting

added theorem MeasureTheory.stoppedValue_hitting_mem