Commit 2022-08-07 07:29 e2333f32

View on Github →

feat(probability/upcrossing): Doob's upcrossing estimate (#14933) This PR proves Doob's upcrossing estimate which is central for the martingale convergence theorems.

Estimated changes

Modified docs/references.bib

Modified src/algebra/order/lattice_group.lean

added theorem lattice_ordered_comm_group.pos_eq_self_of_one_lt_pos

Modified src/probability/hitting_time.lean

added theorem measure_theory.hitting_eq_hitting_of_exists

added theorem measure_theory.is_stopping_time_hitting_is_stopping_time

Modified src/probability/martingale.lean

added theorem measure_theory.martingale_const

Modified src/probability/stopping.lean

added theorem measure_theory.adapted_const

Created src/probability/upcrossing.lean

added theorem measure_theory.adapted.integrable_upcrossings_before

added theorem measure_theory.adapted.is_stopping_time_crossing

added theorem measure_theory.adapted.is_stopping_time_lower_crossing_time

added theorem measure_theory.adapted.is_stopping_time_upper_crossing_time

added theorem measure_theory.adapted.measurable_upcrossings

added theorem measure_theory.adapted.measurable_upcrossings_before

added theorem measure_theory.adapted.upcrossing_strat_adapted

added theorem measure_theory.crossing_eq_crossing_of_lower_crossing_time_lt

added theorem measure_theory.crossing_eq_crossing_of_upper_crossing_time_lt

added theorem measure_theory.crossing_pos_eq

added theorem measure_theory.exists_upper_crossing_time_eq

added theorem measure_theory.integral_mul_upcrossings_before_le_integral

added theorem measure_theory.le_sub_of_le_upcrossings_before

added def measure_theory.lower_crossing_time

added def measure_theory.lower_crossing_time_aux

added theorem measure_theory.lower_crossing_time_le

added theorem measure_theory.lower_crossing_time_le_upper_crossing_time_succ

added theorem measure_theory.lower_crossing_time_lt_of_lt_upcrossings_before

added theorem measure_theory.lower_crossing_time_lt_upper_crossing_time

added theorem measure_theory.lower_crossing_time_mono

added theorem measure_theory.lower_crossing_time_stabilize'

added theorem measure_theory.lower_crossing_time_stabilize

added theorem measure_theory.lower_crossing_time_zero

added theorem measure_theory.mul_integral_upcrossings_before_le_integral_pos_part_aux1

added theorem measure_theory.mul_integral_upcrossings_before_le_integral_pos_part_aux2

added theorem measure_theory.mul_upcrossings_before_le

added theorem measure_theory.stopped_value_lower_crossing_time

added theorem measure_theory.stopped_value_upper_crossing_time

added theorem measure_theory.sub_eq_zero_of_upcrossings_before_lt

added theorem measure_theory.submartingale.mul_integral_upcrossings_before_le_integral_pos_part

added theorem measure_theory.submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part

added theorem measure_theory.submartingale.sum_mul_upcrossing_strat_le

added theorem measure_theory.submartingale.sum_sub_upcrossing_strat_mul

added theorem measure_theory.submartingale.sum_upcrossing_strat_mul

added def measure_theory.upcrossing_strat

added theorem measure_theory.upcrossing_strat_le_one

added theorem measure_theory.upcrossing_strat_nonneg

added def measure_theory.upcrossings_before

added theorem measure_theory.upcrossings_before_bot

added theorem measure_theory.upcrossings_before_eq_sum

added theorem measure_theory.upcrossings_before_le

added theorem measure_theory.upcrossings_before_lt_of_exists_upcrossing

added theorem measure_theory.upcrossings_before_mono

added theorem measure_theory.upcrossings_before_pos_eq

added theorem measure_theory.upcrossings_before_zero'

added theorem measure_theory.upcrossings_before_zero

added theorem measure_theory.upcrossings_lt_top_iff

added def measure_theory.upper_crossing_time

added theorem measure_theory.upper_crossing_time_bound_eq

added theorem measure_theory.upper_crossing_time_eq_of_bound_le

added theorem measure_theory.upper_crossing_time_eq_of_upcrossings_before_lt

added theorem measure_theory.upper_crossing_time_eq_upper_crossing_time_of_lt

added theorem measure_theory.upper_crossing_time_le

added theorem measure_theory.upper_crossing_time_le_lower_crossing_time

added theorem measure_theory.upper_crossing_time_lt_bdd_above

added theorem measure_theory.upper_crossing_time_lt_lower_crossing_time

added theorem measure_theory.upper_crossing_time_lt_nonempty

added theorem measure_theory.upper_crossing_time_lt_of_le_upcrossings_before

added theorem measure_theory.upper_crossing_time_lt_succ

added theorem measure_theory.upper_crossing_time_mono

added theorem measure_theory.upper_crossing_time_stabilize'

added theorem measure_theory.upper_crossing_time_stabilize

added theorem measure_theory.upper_crossing_time_succ

added theorem measure_theory.upper_crossing_time_succ_eq

added theorem measure_theory.upper_crossing_time_zero'

added theorem measure_theory.upper_crossing_time_zero