src/HOL/Probability/Probability_Measure.thy
2011-06-09 hoelzl 2011-06-09 lemma: independence is equal to mutual information = 0
2011-06-09 hoelzl 2011-06-09 jensens inequality
2011-05-26 hoelzl 2011-05-26 integral strong monotone; finite subadditivity for measure
2011-05-26 hoelzl 2011-05-26 add lemma indep_distribution_eq_measure
2011-05-26 hoelzl 2011-05-26 add lemma indep_sets_collect_sigma
2011-05-23 hoelzl 2011-05-23 move lemmas to Extended_Reals and Extended_Real_Limits
2011-05-20 hoelzl 2011-05-20 Add restricted borel measure to {0 .. 1}
2011-05-20 hoelzl 2011-05-20 add lemma prob_finite_product
2011-05-19 hoelzl 2011-05-19 add Bernoulli space
2011-05-19 hoelzl 2011-05-19 add product of probability spaces with finite cardinality
2011-05-19 hoelzl 2011-05-19 remove double sum_over_space_real_distribution
2011-04-01 hoelzl 2011-04-01 remove unnecessary prob_preserving
2011-04-01 hoelzl 2011-04-01 add prob_space_vimage
2011-03-29 hoelzl 2011-03-29 rename Probability_Space to Probability_Measure