Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-18 13:45 8c9342fd

View on Github →

feat(probability/martingale/borel_cantelli): Lévy's generalized Borel-Cantelli (#16358) This PR proves the one sided martingale bound and uses it to prove the Lévy's generalized Borel-Cantelli lemma. With the generalized Borel-Cantelli, the still missing second Borel-Cantelli lemma follows by choosing an appropriate filtration.

Estimated changes

Modified src/measure_theory/function/conditional_expectation/real.lean

added theorem measure_theory.ae_bdd_condexp_of_ae_bdd

added theorem measure_theory.integral_abs_condexp_le

added theorem measure_theory.set_integral_abs_condexp_le

Modified src/measure_theory/integral/bochner.lean

added theorem measure_theory.snorm_one_le_of_le'

added theorem measure_theory.snorm_one_le_of_le

Modified src/measure_theory/integral/set_integral.lean

added theorem measure_theory.set_integral_gt_gt

Modified src/probability/martingale/basic.lean

added theorem measure_theory.martingale_const_fun

Created src/probability/martingale/borel_cantelli.lean

added theorem measure_theory.adapted.is_stopping_time_least_ge

added theorem measure_theory.ae_mem_limsup_at_top_iff

added theorem measure_theory.borel_cantelli.adapted_process

added theorem measure_theory.borel_cantelli.integrable_process

added theorem measure_theory.borel_cantelli.martingale_part_process_ae_eq

added theorem measure_theory.borel_cantelli.predictable_part_process_ae_eq

added def measure_theory.borel_cantelli.process

added theorem measure_theory.borel_cantelli.process_difference_le

added theorem measure_theory.borel_cantelli.process_zero

added def measure_theory.least_ge

added theorem measure_theory.least_ge_eq_min

added theorem measure_theory.least_ge_le

added theorem measure_theory.least_ge_mono

added theorem measure_theory.martingale.ae_not_tendsto_at_top_at_bot

added theorem measure_theory.martingale.ae_not_tendsto_at_top_at_top

added theorem measure_theory.martingale.bdd_above_range_iff_bdd_below_range

added theorem measure_theory.norm_stopped_value_least_ge_le

added theorem measure_theory.stopped_value_stopped_value_least_ge

added theorem measure_theory.submartingale.bdd_above_iff_exists_tendsto

added theorem measure_theory.submartingale.bdd_above_iff_exists_tendsto_aux

added theorem measure_theory.submartingale.exists_tendsto_of_abs_bdd_above_aux

added theorem measure_theory.submartingale.stopped_value_least_ge

added theorem measure_theory.submartingale.stopped_value_least_ge_snorm_le'

added theorem measure_theory.submartingale.stopped_value_least_ge_snorm_le

added theorem measure_theory.tendsto_sum_indicator_at_top_iff'

added theorem measure_theory.tendsto_sum_indicator_at_top_iff

Modified src/probability/martingale/centering.lean

modified theorem measure_theory.martingale_part_add_predictable_part

added theorem measure_theory.martingale_part_bdd_difference

added theorem measure_theory.predictable_part_bdd_difference

Modified src/topology/algebra/order/liminf_limsup.lean

added theorem bdd_above_range_of_tendsto_at_top_at_bot

added theorem bdd_below_range_of_tendsto_at_top_at_top

added theorem filter.tendsto.is_bounded_under_ge_at_top

added theorem filter.tendsto.is_bounded_under_le_at_bot

added theorem is_bounded_ge_at_top

added theorem is_bounded_le_at_bot

added theorem limsup_eq_tendsto_sum_indicator_at_top

added theorem limsup_eq_tendsto_sum_indicator_nat_at_top