1.11. ForMathlib.Probability.Independence.IndepFun
Lemmas about independence
Module LeanMachineLearning.ForMathlib.Probability.Independence.IndepFun contains 8 exposed declarations.
-
ProbabilityTheory.indepFun_zero_measure -
ProbabilityTheory.indepFun_cond_of_indepFun -
ProbabilityTheory.iIndepFun_nat_iff_forall_indepFun -
ProbabilityTheory.IndepFun_map_iff -
ProbabilityTheory.iIndepFun_map_iff -
ProbabilityTheory.identDistrib_map_right_iff -
ProbabilityTheory.identDistrib_comm -
ProbabilityTheory.identDistrib_map_left_iff