Commit 2023-11-30 16:55 ab3f6972

View on Github →

feat(Probability/Independence): add conditional independence (#6098) Define conditional independence of sigma-algebras, sets and functions. This is a special case of independence with respect to a kernel and a measure. Conditional independence is obtained by using the conditional expectation kernel condexpKernel.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Independence/Conditional.lean

added theorem ProbabilityTheory.CondIndep.condIndepSet_of_measurableSet

added theorem ProbabilityTheory.CondIndep.condIndepSets

added theorem ProbabilityTheory.CondIndep.symm

added def ProbabilityTheory.CondIndep

added theorem ProbabilityTheory.CondIndepFun.comp

added def ProbabilityTheory.CondIndepFun

added def ProbabilityTheory.CondIndepSet

added theorem ProbabilityTheory.CondIndepSets.bInter

added theorem ProbabilityTheory.CondIndepSets.bUnion

added theorem ProbabilityTheory.CondIndepSets.condIndep'

added theorem ProbabilityTheory.CondIndepSets.condIndep

added theorem ProbabilityTheory.CondIndepSets.condIndepSet_of_mem

added theorem ProbabilityTheory.CondIndepSets.iInter

added theorem ProbabilityTheory.CondIndepSets.iUnion

added theorem ProbabilityTheory.CondIndepSets.inter

added theorem ProbabilityTheory.CondIndepSets.symm

added theorem ProbabilityTheory.CondIndepSets.union

added theorem ProbabilityTheory.CondIndepSets.union_iff

added def ProbabilityTheory.CondIndepSets

added theorem ProbabilityTheory.condIndepFun_iff

added theorem ProbabilityTheory.condIndepFun_iff_condIndep

added theorem ProbabilityTheory.condIndepFun_iff_condIndepSet_preimage

added theorem ProbabilityTheory.condIndepFun_iff_condexp_inter_preimage_eq_mul

added theorem ProbabilityTheory.condIndepSet_empty_left

added theorem ProbabilityTheory.condIndepSet_empty_right

added theorem ProbabilityTheory.condIndepSet_iff

added theorem ProbabilityTheory.condIndepSet_iff_condIndep

added theorem ProbabilityTheory.condIndepSet_iff_condIndepSets_singleton

added theorem ProbabilityTheory.condIndepSets_iff

added theorem ProbabilityTheory.condIndepSets_of_condIndepSets_of_le_left

added theorem ProbabilityTheory.condIndepSets_of_condIndepSets_of_le_right

added theorem ProbabilityTheory.condIndepSets_piiUnionInter_of_disjoint

added theorem ProbabilityTheory.condIndepSets_singleton_iff

added theorem ProbabilityTheory.condIndep_bot_left

added theorem ProbabilityTheory.condIndep_bot_right

added theorem ProbabilityTheory.condIndep_iSup_of_antitone

added theorem ProbabilityTheory.condIndep_iSup_of_directed_le

added theorem ProbabilityTheory.condIndep_iSup_of_disjoint

added theorem ProbabilityTheory.condIndep_iSup_of_monotone

added theorem ProbabilityTheory.condIndep_iff

added theorem ProbabilityTheory.condIndep_iff_condIndepSets

added theorem ProbabilityTheory.condIndep_iff_forall_condIndepSet

added theorem ProbabilityTheory.condIndep_of_condIndep_of_le_left

added theorem ProbabilityTheory.condIndep_of_condIndep_of_le_right

added theorem ProbabilityTheory.iCondIndep.condIndep

added theorem ProbabilityTheory.iCondIndep.iCondIndepSets

added def ProbabilityTheory.iCondIndep

added theorem ProbabilityTheory.iCondIndepFun.condIndepFun

added theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset

added theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset_prod_of_not_mem

added theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prod

added theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prod_range_succ

added theorem ProbabilityTheory.iCondIndepFun.mul

added def ProbabilityTheory.iCondIndepFun

added theorem ProbabilityTheory.iCondIndepFun_iff

added theorem ProbabilityTheory.iCondIndepFun_iff_condexp_inter_preimage_eq_mul

added theorem ProbabilityTheory.iCondIndepFun_iff_iCondIndep

added theorem ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_le

added theorem ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_le_nat

added theorem ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_lt

added theorem ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_of_disjoint

added theorem ProbabilityTheory.iCondIndepSet.iCondIndepFun_indicator

added def ProbabilityTheory.iCondIndepSet

added theorem ProbabilityTheory.iCondIndepSet_iff

added theorem ProbabilityTheory.iCondIndepSet_iff_iCondIndep

added theorem ProbabilityTheory.iCondIndepSet_iff_iCondIndepSets_singleton

added theorem ProbabilityTheory.iCondIndepSets.condIndepSets

added theorem ProbabilityTheory.iCondIndepSets.iCondIndep

added theorem ProbabilityTheory.iCondIndepSets.piiUnionInter_of_not_mem

added def ProbabilityTheory.iCondIndepSets

added theorem ProbabilityTheory.iCondIndepSets_iff

added theorem ProbabilityTheory.iCondIndepSets_singleton_iff

added theorem ProbabilityTheory.iCondIndep_iff

added theorem ProbabilityTheory.iCondIndep_iff_iCondIndepSets

Modified Mathlib/Probability/Independence/ZeroOne.lean

added theorem ProbabilityTheory.condIndep_biSup_compl

added theorem ProbabilityTheory.condIndep_biSup_limsup

added theorem ProbabilityTheory.condIndep_iSup_directed_limsup

added theorem ProbabilityTheory.condIndep_iSup_limsup

added theorem ProbabilityTheory.condIndep_limsup_atBot_self

added theorem ProbabilityTheory.condIndep_limsup_atTop_self

added theorem ProbabilityTheory.condIndep_limsup_self

added theorem ProbabilityTheory.condexp_eq_zero_or_one_of_condIndepSet_self

added theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup

added theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup_atBot

added theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup_atTop

added theorem ProbabilityTheory.kernel.indep_biSup_compl

added theorem ProbabilityTheory.kernel.indep_biSup_limsup

added theorem ProbabilityTheory.kernel.indep_iSup_directed_limsup

added theorem ProbabilityTheory.kernel.indep_iSup_limsup

added theorem ProbabilityTheory.kernel.indep_limsup_atBot_self

added theorem ProbabilityTheory.kernel.indep_limsup_atTop_self

added theorem ProbabilityTheory.kernel.indep_limsup_self

added theorem ProbabilityTheory.kernel.measure_eq_zero_or_one_of_indepSet_self

added theorem ProbabilityTheory.kernel.measure_eq_zero_or_one_or_top_of_indepSet_self

added theorem ProbabilityTheory.kernel.measure_zero_or_one_of_measurableSet_limsup

added theorem ProbabilityTheory.kernel.measure_zero_or_one_of_measurableSet_limsup_atBot

added theorem ProbabilityTheory.kernel.measure_zero_or_one_of_measurableSet_limsup_atTop