1.22. ForMathlib.Probability.Independence.IndepFun🔗

Lemmas about independence

Module LeanMachineLearning.ForMathlib.Probability.Independence.IndepFun contains 16 exposed declarations.

• ProbabilityTheory.indepFun_zero_measureLemma · 0 deps
• ProbabilityTheory.indepFun_cond_of_indepFunLemma · 0 deps
• ProbabilityTheory.indepFun_cond_compLemma · 0 deps
• ProbabilityTheory.indepFun_cond_preimage_singleton_leftLemma · 0 deps
• ProbabilityTheory.indepFun_cond_preimage_singleton_rightLemma · 0 deps
• ProbabilityTheory.iIndepFun_nat_iff_forall_indepFunLemma · 0 deps
• ProbabilityTheory.IndepFun_map_iffLemma · 0 deps
• ProbabilityTheory.iIndepFun_map_iffLemma · 0 deps
• ProbabilityTheory.identDistrib_map_right_iffLemma · 0 deps
• ProbabilityTheory.identDistrib_commLemma · 0 deps
• ProbabilityTheory.identDistrib_map_left_iffLemma · 0 deps
• ProbabilityTheory.hasLaw_fst_prodLemma · 0 deps
• ProbabilityTheory.hasLaw_snd_prodLemma · 0 deps
• ProbabilityTheory.IndepFun.snd_prodLemma · 0 deps
• ProbabilityTheory.IndepFun.fst_prodLemma · 0 deps
• ProbabilityTheory.iIndepFun.indepFun_of_measurable_iSup_comapLemma · 0 deps