Commit 2023-06-02 15:12 7f6ce653

View on Github →

feat: port Probability.Independence.Basic (#4557) The names of many definitions and lemmas in the Mathlib3 file contained Indep so Mathport added Cat at a bunch of places that had to be removed. The Mathlib4 equivalent is iIndep see this thread

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Independence/Basic.lean

added theorem ProbabilityTheory.Indep.indepSet_of_measurableSet

added theorem ProbabilityTheory.Indep.indepSets

added theorem ProbabilityTheory.Indep.symm

added def ProbabilityTheory.Indep

added theorem ProbabilityTheory.IndepFun.ae_eq

added theorem ProbabilityTheory.IndepFun.comp

added def ProbabilityTheory.IndepFun

added def ProbabilityTheory.IndepSet

added theorem ProbabilityTheory.IndepSets.bInter

added theorem ProbabilityTheory.IndepSets.bUnion

added theorem ProbabilityTheory.IndepSets.iInter

added theorem ProbabilityTheory.IndepSets.iUnion

added theorem ProbabilityTheory.IndepSets.indep'

added theorem ProbabilityTheory.IndepSets.indep

added theorem ProbabilityTheory.IndepSets.indepSet_of_mem

added theorem ProbabilityTheory.IndepSets.inter

added theorem ProbabilityTheory.IndepSets.symm

added theorem ProbabilityTheory.IndepSets.union

added theorem ProbabilityTheory.IndepSets.union_iff

added def ProbabilityTheory.IndepSets

added theorem ProbabilityTheory.iIndep.iIndepSets

added theorem ProbabilityTheory.iIndep.indep

added def ProbabilityTheory.iIndep

added theorem ProbabilityTheory.iIndepFun.indepFun

added theorem ProbabilityTheory.iIndepFun.indepFun_finset

added theorem ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_not_mem

added theorem ProbabilityTheory.iIndepFun.indepFun_prod

added theorem ProbabilityTheory.iIndepFun.indepFun_prod_range_succ

added theorem ProbabilityTheory.iIndepFun.mul

added def ProbabilityTheory.iIndepFun

added theorem ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul

added theorem ProbabilityTheory.iIndepSet.iIndepFun_indicator

added theorem ProbabilityTheory.iIndepSet.indep_generateFrom_le

added theorem ProbabilityTheory.iIndepSet.indep_generateFrom_le_nat

added theorem ProbabilityTheory.iIndepSet.indep_generateFrom_lt

added theorem ProbabilityTheory.iIndepSet.indep_generateFrom_of_disjoint

added def ProbabilityTheory.iIndepSet

added theorem ProbabilityTheory.iIndepSets.iIndep

added theorem ProbabilityTheory.iIndepSets.indepSets

added theorem ProbabilityTheory.iIndepSets.piiUnionInter_of_not_mem

added def ProbabilityTheory.iIndepSets

added theorem ProbabilityTheory.indepFun_iff_indepSet_preimage

added theorem ProbabilityTheory.indepFun_iff_measure_inter_preimage_eq_mul

added theorem ProbabilityTheory.indepSet_empty_left

added theorem ProbabilityTheory.indepSet_empty_right

added theorem ProbabilityTheory.indepSet_iff_indepSets_singleton

added theorem ProbabilityTheory.indepSet_iff_measure_inter_eq_mul

added theorem ProbabilityTheory.indepSets_of_indepSets_of_le_left

added theorem ProbabilityTheory.indepSets_of_indepSets_of_le_right

added theorem ProbabilityTheory.indepSets_piiUnionInter_of_disjoint

added theorem ProbabilityTheory.indepSets_singleton_iff

added theorem ProbabilityTheory.indep_bot_left

added theorem ProbabilityTheory.indep_bot_right

added theorem ProbabilityTheory.indep_iSup_of_antitone

added theorem ProbabilityTheory.indep_iSup_of_directed_le

added theorem ProbabilityTheory.indep_iSup_of_disjoint

added theorem ProbabilityTheory.indep_iSup_of_monotone

added theorem ProbabilityTheory.indep_iff_forall_indepSet

added theorem ProbabilityTheory.indep_of_indep_of_le_left

added theorem ProbabilityTheory.indep_of_indep_of_le_right