Commit 2023-10-31 11:24 2d242e7f

View on Github →

feat: Independence of singletons (#7251) Port a bit of https://github.com/leanprover-community/mathlib/pull/18506, but it's mostly handmade.

Estimated changes

Modified Mathlib/Probability/Independence/Basic.lean

added theorem ProbabilityTheory.IndepFun.meas_inter

added theorem ProbabilityTheory.iIndep.iIndepSets'

added theorem ProbabilityTheory.iIndep.meas_biInter

added theorem ProbabilityTheory.iIndep.meas_iInter

added theorem ProbabilityTheory.iIndepFun.meas_biInter

added theorem ProbabilityTheory.iIndepFun.meas_iInter

added theorem ProbabilityTheory.iIndepSet_iff_iIndepSets_singleton

added theorem ProbabilityTheory.iIndepSet_iff_meas_biInter

added theorem ProbabilityTheory.iIndepSets.iIndepSet_of_mem

added theorem ProbabilityTheory.iIndepSets.meas_biInter

added theorem ProbabilityTheory.iIndepSets.meas_iInter

added theorem ProbabilityTheory.iIndepSets_singleton_iff

added theorem ProbabilityTheory.iIndep_comap_mem_iff

Modified Mathlib/Probability/Independence/Kernel.lean

added theorem ProbabilityTheory.kernel.IndepFun.meas_inter

added theorem ProbabilityTheory.kernel.iIndep.iIndepSets'

added theorem ProbabilityTheory.kernel.iIndep.meas_biInter

added theorem ProbabilityTheory.kernel.iIndep.meas_iInter

added theorem ProbabilityTheory.kernel.iIndepFun.meas_biInter

added theorem ProbabilityTheory.kernel.iIndepFun.meas_iInter

added theorem ProbabilityTheory.kernel.iIndepSet_iff_iIndepSets_singleton

added theorem ProbabilityTheory.kernel.iIndepSet_iff_meas_biInter

added theorem ProbabilityTheory.kernel.iIndepSets.iIndepSet_of_mem

added theorem ProbabilityTheory.kernel.iIndepSets.meas_biInter

added theorem ProbabilityTheory.kernel.iIndepSets.meas_iInter

added theorem ProbabilityTheory.kernel.iIndepSets_singleton_iff

added theorem ProbabilityTheory.kernel.iIndep_comap_mem_iff