Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-12 21:16 43e859a0

View on Github →

feat(probability/martingale/convergence): a.e. martingale convergence theorem (#15904) This PR proves the a.e. martingale convergence while a later PR will show the L¹ version. I've also added a new martingale folder in the probability folder as there are a few files regarding martingales now.

Estimated changes

Modified src/measure_theory/function/lp_space.lean

added theorem measure_theory.ae_bdd_liminf_at_top_of_snorm_bdd

added theorem measure_theory.ae_bdd_liminf_at_top_rpow_of_snorm_bdd

Renamed src/probability/martingale.lean to src/probability/martingale/basic.lean

Created src/probability/martingale/convergence.lean

added theorem measure_theory.not_frequently_of_upcrossings_lt_top

added theorem measure_theory.submartingale.ae_tendsto_limit_process

added theorem measure_theory.submartingale.exists_ae_tendsto_of_bdd

added theorem measure_theory.submartingale.exists_ae_trim_tendsto_of_bdd

added theorem measure_theory.submartingale.mem_ℒp_limit_process

added theorem measure_theory.submartingale.upcrossings_ae_lt_top'

added theorem measure_theory.submartingale.upcrossings_ae_lt_top

added theorem measure_theory.tendsto_of_uncrossing_lt_top

added theorem measure_theory.upcrossings_eq_top_of_frequently_lt

Renamed src/probability/upcrossing.lean to src/probability/martingale/upcrossing.lean

Modified src/probability/stopping.lean

added def measure_theory.filtration.limit_process

added theorem measure_theory.filtration.mem_ℒp_limit_process_of_snorm_bdd

added theorem measure_theory.filtration.strongly_measurable_limit_process'

added theorem measure_theory.filtration.strongly_measurable_limit_process

Modified src/topology/instances/ennreal.lean

added theorem ennreal.exists_frequently_lt_of_liminf_ne_top'

added theorem ennreal.exists_frequently_lt_of_liminf_ne_top

added theorem ennreal.exists_upcrossings_of_not_bounded_under