src/HOL/Probability/Independent_Family.thy
2012-02-28 wenzelm 2012-02-28 avoid undeclared variables in let bindings; tuned proofs;
2011-12-07 hoelzl 2011-12-07 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal
2011-06-09 hoelzl 2011-06-09 lemma: independence is equal to mutual information = 0
2011-05-26 hoelzl 2011-05-26 introduce independence of two random variables
2011-05-26 hoelzl 2011-05-26 add lemma indep_distribution_eq_measure
2011-05-26 hoelzl 2011-05-26 add lemma indep_rv_finite
2011-05-26 hoelzl 2011-05-26 add lemma borel_0_1_law
2011-05-26 hoelzl 2011-05-26 use abbrevitation events == sets M
2011-05-26 hoelzl 2011-05-26 add lemma kolmogorov_0_1_law
2011-05-26 hoelzl 2011-05-26 add lemma indep_sets_collect_sigma
2011-05-17 hoelzl 2011-05-17 Add formalization of probabilistic independence for families of sets