src/HOL/Probability/Probability_Measure.thy
2011-12-20 noschinl 2011-12-20 add simp rules for enat and ereal
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-12-01 hoelzl 2011-12-01 moved theorems about distribution to the definition; removed oopsed-lemma
2011-12-01 hoelzl 2011-12-01 rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal
2011-07-04 hoelzl 2011-07-04 the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})
2011-06-27 hoelzl 2011-06-27 move conditional expectation to its own theory file
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