Commit 2024-09-03 08:22 d48a1f22

View on Github →

feat: remove many IsMarkovKernel and IsProbabilityMeasure assumptions (#16399) These follow from independence assumptions that are made in the statements.

Estimated changes

Modified Mathlib/Probability/BorelCantelli.lean

Modified Mathlib/Probability/Independence/Basic.lean

added theorem ProbabilityTheory.iIndep.isProbabilityMeasure

modified theorem ProbabilityTheory.iIndepSet.indep_generateFrom_le

modified theorem ProbabilityTheory.iIndepSet.indep_generateFrom_le_nat

modified theorem ProbabilityTheory.iIndepSet.indep_generateFrom_lt

modified theorem ProbabilityTheory.iIndepSet.indep_generateFrom_of_disjoint

added theorem ProbabilityTheory.iIndepSet.isProbabilityMeasure

modified theorem ProbabilityTheory.iIndepSets.iIndep

added theorem ProbabilityTheory.iIndepSets.isProbabilityMeasure

modified theorem ProbabilityTheory.indepSets_piiUnionInter_of_disjoint

modified theorem ProbabilityTheory.indep_iSup_of_disjoint

Modified Mathlib/Probability/Independence/Kernel.lean

added theorem ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure

modified theorem ProbabilityTheory.Kernel.iIndepFun.ae_isProbabilityMeasure

modified theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finset

modified theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_mk

modified theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_mk_prod_mk

added theorem ProbabilityTheory.Kernel.iIndepFun_congr

added theorem ProbabilityTheory.Kernel.iIndepFun_zero_right

modified theorem ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le

modified theorem ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le_nat

modified theorem ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_lt

modified theorem ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_of_disjoint

added theorem ProbabilityTheory.Kernel.iIndepSet_congr

added theorem ProbabilityTheory.Kernel.iIndepSet_zero_right

added theorem ProbabilityTheory.Kernel.iIndepSets.ae_isProbabilityMeasure

modified theorem ProbabilityTheory.Kernel.iIndepSets.iIndep

added theorem ProbabilityTheory.Kernel.iIndepSets_congr

added theorem ProbabilityTheory.Kernel.iIndepSets_zero_right

added theorem ProbabilityTheory.Kernel.iIndep_congr

added theorem ProbabilityTheory.Kernel.iIndep_zero_right

added theorem ProbabilityTheory.Kernel.indepFun_congr

added theorem ProbabilityTheory.Kernel.indepFun_zero_left

added theorem ProbabilityTheory.Kernel.indepFun_zero_right

added theorem ProbabilityTheory.Kernel.indepSet_congr

added theorem ProbabilityTheory.Kernel.indepSet_zero_left

added theorem ProbabilityTheory.Kernel.indepSet_zero_right

added theorem ProbabilityTheory.Kernel.indepSets_congr

modified theorem ProbabilityTheory.Kernel.indepSets_piiUnionInter_of_disjoint

added theorem ProbabilityTheory.Kernel.indepSets_zero_left

added theorem ProbabilityTheory.Kernel.indepSets_zero_right

added theorem ProbabilityTheory.Kernel.indep_congr

modified theorem ProbabilityTheory.Kernel.indep_iSup_of_disjoint

added theorem ProbabilityTheory.Kernel.indep_zero_left

added theorem ProbabilityTheory.Kernel.indep_zero_right

Modified Mathlib/Probability/Independence/ZeroOne.lean

added theorem ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self'

modified theorem ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self

modified theorem ProbabilityTheory.indep_biSup_compl

modified theorem ProbabilityTheory.indep_biSup_limsup

modified theorem ProbabilityTheory.indep_iSup_directed_limsup

modified theorem ProbabilityTheory.indep_iSup_limsup

modified theorem ProbabilityTheory.indep_limsup_atBot_self

modified theorem ProbabilityTheory.indep_limsup_atTop_self

modified theorem ProbabilityTheory.indep_limsup_self

modified theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup

modified theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atBot

modified theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop

Modified Mathlib/Probability/Kernel/Basic.lean

added theorem ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel