Commit 2023-06-20 07:33 eff781e4

View on Github →

feat: port Probability.Martingale.Convergence (#5283)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Martingale/Convergence.lean

added theorem MeasureTheory.Integrable.tendsto_ae_condexp

added theorem MeasureTheory.Integrable.tendsto_snorm_condexp

added theorem MeasureTheory.Martingale.ae_eq_condexp_limitProcess

added theorem MeasureTheory.Martingale.eq_condexp_of_tendsto_snorm

added theorem MeasureTheory.Submartingale.ae_tendsto_limitProcess

added theorem MeasureTheory.Submartingale.ae_tendsto_limitProcess_of_uniformIntegrable

added theorem MeasureTheory.Submartingale.exists_ae_tendsto_of_bdd

added theorem MeasureTheory.Submartingale.exists_ae_trim_tendsto_of_bdd

added theorem MeasureTheory.Submartingale.memℒp_limitProcess

added theorem MeasureTheory.Submartingale.tendsto_snorm_one_limitProcess

added theorem MeasureTheory.Submartingale.upcrossings_ae_lt_top'

added theorem MeasureTheory.Submartingale.upcrossings_ae_lt_top

added theorem MeasureTheory.not_frequently_of_upcrossings_lt_top

added theorem MeasureTheory.tendsto_ae_condexp

added theorem MeasureTheory.tendsto_of_uncrossing_lt_top

added theorem MeasureTheory.tendsto_snorm_condexp

added theorem MeasureTheory.upcrossings_eq_top_of_frequently_lt