Commit 2023-08-02 15:54 a3b98ba0

View on Github →

refactor(Probability/Independence): define independence using kernel independence (#6294) Independence is the special case of independence with respect to a kernel and a measure where the kernel is constant.

Estimated changes

Modified Mathlib/Probability/ConditionalExpectation.lean

Modified Mathlib/Probability/Independence/Basic.lean

modified theorem ProbabilityTheory.Indep.indepSet_of_measurableSet

modified def ProbabilityTheory.Indep

modified theorem ProbabilityTheory.IndepFun.comp

modified def ProbabilityTheory.IndepFun

added theorem ProbabilityTheory.IndepFun_iff

added theorem ProbabilityTheory.IndepFun_iff_Indep

added theorem ProbabilityTheory.IndepSet_iff

added theorem ProbabilityTheory.IndepSet_iff_Indep

modified def ProbabilityTheory.IndepSets

added theorem ProbabilityTheory.IndepSets_iff

added theorem ProbabilityTheory.Indep_iff

added theorem ProbabilityTheory.Indep_iff_IndepSets

added theorem ProbabilityTheory.iIndepFun_iff

added theorem ProbabilityTheory.iIndepFun_iff_iIndep

added theorem ProbabilityTheory.iIndepSet_iff

added theorem ProbabilityTheory.iIndepSet_iff_iIndep

added theorem ProbabilityTheory.iIndepSets_iff

added theorem ProbabilityTheory.iIndep_iff

added theorem ProbabilityTheory.iIndep_iff_iIndepSets

modified theorem ProbabilityTheory.indepSet_empty_right

modified theorem ProbabilityTheory.indepSet_iff_indepSets_singleton

modified theorem ProbabilityTheory.indep_bot_right

Modified Mathlib/Probability/Independence/ZeroOne.lean

Modified Mathlib/Probability/Integration.lean