2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-07 hoelzl 2015-10-07 cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-06-12 hoelzl 2014-06-12 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-19 hoelzl 2012-11-19 merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-11-15 immler 2012-11-15 regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards
2012-11-06 hoelzl 2012-11-06 add support for function application to measurability prover
2012-11-02 hoelzl 2012-11-02 use measurability prover
2012-10-10 hoelzl 2012-10-10 joint distribution of independent variables
2012-10-10 hoelzl 2012-10-10 indep_vars does not need sigma-sets
2012-10-10 hoelzl 2012-10-10 remove incseq assumption from measure_eqI_generator_eq
2012-10-10 hoelzl 2012-10-10 simplified assumptions for kolmogorov_0_1_law
2012-10-10 hoelzl 2012-10-10 tuned product measurability
2012-10-10 hoelzl 2012-10-10 rename terminal_events to tail_event
2012-04-23 hoelzl 2012-04-23 reworked Probability theory
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