src/HOL/Probability/Probability_Measure.thy
2014-06-12 hoelzl 2014-06-12 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
2014-05-20 hoelzl 2014-05-20 add various lemmas
2014-05-19 hoelzl 2014-05-19 renamed positive_integral to nn_integral
2014-05-19 hoelzl 2014-05-19 fixed document generation for HOL-Probability
2014-05-19 hoelzl 2014-05-19 introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2013-11-12 hoelzl 2013-11-12 measure of a countable union
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-04-10 hoelzl 2013-04-10 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
2013-03-22 hoelzl 2013-03-22 introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
2012-12-07 hoelzl 2012-12-07 add exponential and uniform distributions
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-11-16 hoelzl 2012-11-16 rules for AE and prob
2012-11-02 hoelzl 2012-11-02 use measurability prover
2012-11-02 hoelzl 2012-11-02 add measurability prover; add support for Borel sets
2012-11-02 hoelzl 2012-11-02 add syntax and a.e.-rules for (conditional) probability on predicates
2012-10-10 hoelzl 2012-10-10 joint distribution of independent variables
2012-10-10 hoelzl 2012-10-10 show and use distributed_swap and distributed_jointI
2012-10-10 hoelzl 2012-10-10 continuous version of entropy_le
2012-10-10 hoelzl 2012-10-10 generalize from prob_space to finite_measure
2012-10-10 hoelzl 2012-10-10 tuned product measurability
2012-04-23 hoelzl 2012-04-23 reworked Probability theory
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2012-03-13 wenzelm 2012-03-13 tuned proofs -- eliminated pointless chaining of facts after 'interpret';
2012-02-28 wenzelm 2012-02-28 avoid undeclared variables in let bindings; tuned proofs;
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