Commit 2023-06-20 08:05 66ea1086

View on Github →

feat: port Probability.BorelCantelli (#5286)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/BorelCantelli.lean

added theorem ProbabilityTheory.iIndepFun.condexp_natural_ae_eq_of_lt

added theorem ProbabilityTheory.iIndepFun.indep_comap_natural_of_lt

added theorem ProbabilityTheory.iIndepSet.condexp_indicator_filtrationOfSet_ae_eq

added theorem ProbabilityTheory.measure_limsup_eq_one

Modified Mathlib/Probability/Process/Filtration.lean

added theorem MeasureTheory.measurableSet_filtrationOfSet'

deleted theorem MeasureTheory.measurableSet_filtration_of_set'