Commit 2023-06-18 08:20 d03610e2

View on Github →

feat: port Probability.Process.Stopping (#5213)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Process/Stopping.lean

added theorem MeasureTheory.Adapted.stoppedProcess

added theorem MeasureTheory.Adapted.stoppedProcess_of_discrete

added theorem MeasureTheory.Adapted.stronglyMeasurable_stoppedProcess

added theorem MeasureTheory.Adapted.stronglyMeasurable_stoppedProcess_of_discrete

added theorem MeasureTheory.IsStoppingTime.add

added theorem MeasureTheory.IsStoppingTime.add_const

added theorem MeasureTheory.IsStoppingTime.add_const_nat

added theorem MeasureTheory.IsStoppingTime.le_measurableSpace_of_const_le

added theorem MeasureTheory.IsStoppingTime.measurableSet_eq

added theorem MeasureTheory.IsStoppingTime.measurableSet_eq_le

added theorem MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time

added theorem MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time_of_countable

added theorem MeasureTheory.IsStoppingTime.measurableSet_ge

added theorem MeasureTheory.IsStoppingTime.measurableSet_gt

added theorem MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff

added theorem MeasureTheory.IsStoppingTime.measurableSet_inter_le

added theorem MeasureTheory.IsStoppingTime.measurableSet_inter_le_const_iff

added theorem MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff

added theorem MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time

added theorem MeasureTheory.IsStoppingTime.measurableSet_lt

added theorem MeasureTheory.IsStoppingTime.measurableSet_lt_le

added theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB

added theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_pred

added theorem MeasureTheory.IsStoppingTime.measurableSet_min_const_iff

added theorem MeasureTheory.IsStoppingTime.measurableSet_min_iff

added theorem MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le

added theorem MeasureTheory.IsStoppingTime.measurableSpace_const

added theorem MeasureTheory.IsStoppingTime.measurableSpace_le'

added theorem MeasureTheory.IsStoppingTime.measurableSpace_le

added theorem MeasureTheory.IsStoppingTime.measurableSpace_le_of_countable

added theorem MeasureTheory.IsStoppingTime.measurableSpace_le_of_le

added theorem MeasureTheory.IsStoppingTime.measurableSpace_le_of_le_const

added theorem MeasureTheory.IsStoppingTime.measurableSpace_min

added theorem MeasureTheory.IsStoppingTime.measurableSpace_min_const

added theorem MeasureTheory.IsStoppingTime.measurableSpace_mono

added theorem MeasureTheory.IsStoppingTime.piecewise_of_le

added def MeasureTheory.IsStoppingTime

added theorem MeasureTheory.ProgMeasurable.adapted_stoppedProcess

added theorem MeasureTheory.ProgMeasurable.stoppedProcess

added theorem MeasureTheory.ProgMeasurable.stronglyMeasurable_stoppedProcess

added theorem MeasureTheory.condexp_min_stopping_time_ae_eq_restrict_le

added theorem MeasureTheory.condexp_min_stopping_time_ae_eq_restrict_le_const

added theorem MeasureTheory.condexp_stopping_time_ae_eq_restrict_eq

added theorem MeasureTheory.condexp_stopping_time_ae_eq_restrict_eq_of_countable

added theorem MeasureTheory.condexp_stopping_time_ae_eq_restrict_eq_of_countable_range

added theorem MeasureTheory.integrable_stoppedProcess

added theorem MeasureTheory.integrable_stoppedProcess_of_mem_finset

added theorem MeasureTheory.integrable_stoppedValue

added theorem MeasureTheory.integrable_stoppedValue_of_mem_finset

added theorem MeasureTheory.isStoppingTime_const

added theorem MeasureTheory.isStoppingTime_of_measurableSet_eq

added theorem MeasureTheory.isStoppingTime_piecewise_const

added theorem MeasureTheory.measurable_stoppedValue

added theorem MeasureTheory.memℒp_stoppedProcess

added theorem MeasureTheory.memℒp_stoppedProcess_of_mem_finset

added theorem MeasureTheory.memℒp_stoppedValue

added theorem MeasureTheory.memℒp_stoppedValue_of_mem_finset

added theorem MeasureTheory.progMeasurable_min_stopping_time

added def MeasureTheory.stoppedProcess

added theorem MeasureTheory.stoppedProcess_eq''

added theorem MeasureTheory.stoppedProcess_eq'

added theorem MeasureTheory.stoppedProcess_eq

added theorem MeasureTheory.stoppedProcess_eq_of_ge

added theorem MeasureTheory.stoppedProcess_eq_of_le

added theorem MeasureTheory.stoppedProcess_eq_of_mem_finset

added theorem MeasureTheory.stoppedProcess_eq_stoppedValue

added def MeasureTheory.stoppedValue

added theorem MeasureTheory.stoppedValue_const

added theorem MeasureTheory.stoppedValue_eq'

added theorem MeasureTheory.stoppedValue_eq

added theorem MeasureTheory.stoppedValue_eq_of_mem_finset

added theorem MeasureTheory.stoppedValue_piecewise_const'

added theorem MeasureTheory.stoppedValue_piecewise_const

added theorem MeasureTheory.stoppedValue_stoppedProcess

added theorem MeasureTheory.stoppedValue_sub_eq_sum'

added theorem MeasureTheory.stoppedValue_sub_eq_sum

added theorem MeasureTheory.stronglyMeasurable_stoppedValue_of_le