Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-31 15:55 1e7dab97

View on Github →

feat(probability/borel_cantelli): the second Borel-Cantelli lemma (#16882)

Estimated changes

Modified docs/undergrad.yaml

Modified src/measure_theory/measurable_space.lean

added theorem comap_measurable

Created src/probability/borel_cantelli.lean

added theorem probability_theory.Indep_fun.condexp_natrual_ae_eq_of_lt

added theorem probability_theory.Indep_fun.indep_comap_natural_of_lt

added theorem probability_theory.Indep_set.condexp_indicator_filtration_of_set_ae_eq

added theorem probability_theory.measure_limsup_eq_one

Modified src/probability/independence.lean

added theorem probability_theory.Indep_set.Indep_fun_indicator

added theorem probability_theory.Indep_set.indep_generate_from_le

added theorem probability_theory.Indep_set.indep_generate_from_le_nat

added theorem probability_theory.Indep_set.indep_generate_from_lt

Modified src/probability/martingale/borel_cantelli.lean

modified theorem measure_theory.ae_mem_limsup_at_top_iff

Modified src/probability/process/filtration.lean

added theorem measure_theory.filtration.filtration_of_set_eq_natural

added def measure_theory.filtration_of_set

added theorem measure_theory.measurable_set_filtration_of_set'

added theorem measure_theory.measurable_set_filtration_of_set

Modified src/topology/algebra/infinite_sum.lean

added theorem tsum_singleton

Modified src/topology/instances/ennreal.lean

added theorem ennreal.tsum_add_one_eq_top