Commit 2023-06-20 07:43 6533094a

View on Github →

feat: port Probability.Martingale.BorelCantelli (#5285)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Martingale/BorelCantelli.lean

added theorem MeasureTheory.Adapted.isStoppingTime_leastGE

added theorem MeasureTheory.BorelCantelli.adapted_process

added theorem MeasureTheory.BorelCantelli.integrable_process

added theorem MeasureTheory.BorelCantelli.martingalePart_process_ae_eq

added theorem MeasureTheory.BorelCantelli.predictablePart_process_ae_eq

added theorem MeasureTheory.BorelCantelli.process_difference_le

added theorem MeasureTheory.BorelCantelli.process_zero

added theorem MeasureTheory.Martingale.ae_not_tendsto_atTop_atBot

added theorem MeasureTheory.Martingale.ae_not_tendsto_atTop_atTop

added theorem MeasureTheory.Martingale.bddAbove_range_iff_bddBelow_range

added theorem MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto

added theorem MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto_aux

added theorem MeasureTheory.Submartingale.exists_tendsto_of_abs_bddAbove_aux

added theorem MeasureTheory.Submartingale.stoppedValue_leastGE

added theorem MeasureTheory.Submartingale.stoppedValue_leastGE_snorm_le'

added theorem MeasureTheory.Submartingale.stoppedValue_leastGE_snorm_le

added theorem MeasureTheory.ae_mem_limsup_atTop_iff

added theorem MeasureTheory.leastGE_eq_min

added theorem MeasureTheory.leastGE_le

added theorem MeasureTheory.leastGE_mono

added theorem MeasureTheory.norm_stoppedValue_leastGE_le

added theorem MeasureTheory.stoppedValue_stoppedValue_leastGE

added theorem MeasureTheory.tendsto_sum_indicator_atTop_iff'

added theorem MeasureTheory.tendsto_sum_indicator_atTop_iff