Commit 2023-06-20 07:23 33347eff

View on Github →

feat: port Probability.Martingale.Upcrossing (#5281)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Martingale/Upcrossing.lean

added theorem MeasureTheory.Adapted.integrable_upcrossingsBefore

added theorem MeasureTheory.Adapted.isStoppingTime_crossing

added theorem MeasureTheory.Adapted.isStoppingTime_lowerCrossingTime

added theorem MeasureTheory.Adapted.isStoppingTime_upperCrossingTime

added theorem MeasureTheory.Adapted.measurable_upcrossings

added theorem MeasureTheory.Adapted.measurable_upcrossingsBefore

added theorem MeasureTheory.Adapted.upcrossingStrat_adapted

added theorem MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part

added theorem MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part

added theorem MeasureTheory.Submartingale.sum_mul_upcrossingStrat_le

added theorem MeasureTheory.Submartingale.sum_sub_upcrossingStrat_mul

added theorem MeasureTheory.Submartingale.sum_upcrossingStrat_mul

added theorem MeasureTheory.crossing_eq_crossing_of_lowerCrossingTime_lt

added theorem MeasureTheory.crossing_eq_crossing_of_upperCrossingTime_lt

added theorem MeasureTheory.crossing_pos_eq

added theorem MeasureTheory.exists_upperCrossingTime_eq

added theorem MeasureTheory.integral_mul_upcrossingsBefore_le_integral

added theorem MeasureTheory.le_sub_of_le_upcrossingsBefore

added theorem MeasureTheory.lowerCrossingTime_le

added theorem MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ

added theorem MeasureTheory.lowerCrossingTime_lt_of_lt_upcrossingsBefore

added theorem MeasureTheory.lowerCrossingTime_lt_upperCrossingTime

added theorem MeasureTheory.lowerCrossingTime_mono

added theorem MeasureTheory.lowerCrossingTime_stabilize'

added theorem MeasureTheory.lowerCrossingTime_stabilize

added theorem MeasureTheory.lowerCrossingTime_zero

added theorem MeasureTheory.mul_integral_upcrossingsBefore_le_integral_pos_part_aux

added theorem MeasureTheory.mul_upcrossingsBefore_le

added theorem MeasureTheory.stoppedValue_lowerCrossingTime

added theorem MeasureTheory.stoppedValue_upperCrossingTime

added theorem MeasureTheory.sub_eq_zero_of_upcrossingsBefore_lt

added theorem MeasureTheory.upcrossingStrat_le_one

added theorem MeasureTheory.upcrossingStrat_nonneg

added theorem MeasureTheory.upcrossingsBefore_bot

added theorem MeasureTheory.upcrossingsBefore_eq_sum

added theorem MeasureTheory.upcrossingsBefore_le

added theorem MeasureTheory.upcrossingsBefore_lt_of_exists_upcrossing

added theorem MeasureTheory.upcrossingsBefore_mono

added theorem MeasureTheory.upcrossingsBefore_pos_eq

added theorem MeasureTheory.upcrossingsBefore_zero'

added theorem MeasureTheory.upcrossingsBefore_zero

added theorem MeasureTheory.upcrossings_lt_top_iff

added theorem MeasureTheory.upperCrossingTime_bound_eq

added theorem MeasureTheory.upperCrossingTime_eq_of_bound_le

added theorem MeasureTheory.upperCrossingTime_eq_of_upcrossingsBefore_lt

added theorem MeasureTheory.upperCrossingTime_eq_upperCrossingTime_of_lt

added theorem MeasureTheory.upperCrossingTime_le

added theorem MeasureTheory.upperCrossingTime_le_lowerCrossingTime

added theorem MeasureTheory.upperCrossingTime_lt_bddAbove

added theorem MeasureTheory.upperCrossingTime_lt_lowerCrossingTime

added theorem MeasureTheory.upperCrossingTime_lt_nonempty

added theorem MeasureTheory.upperCrossingTime_lt_of_le_upcrossingsBefore

added theorem MeasureTheory.upperCrossingTime_lt_succ

added theorem MeasureTheory.upperCrossingTime_mono

added theorem MeasureTheory.upperCrossingTime_stabilize'

added theorem MeasureTheory.upperCrossingTime_stabilize

added theorem MeasureTheory.upperCrossingTime_succ

added theorem MeasureTheory.upperCrossingTime_succ_eq

added theorem MeasureTheory.upperCrossingTime_zero'

added theorem MeasureTheory.upperCrossingTime_zero

Modified Mathlib/Probability/Notation.lean