src/HOL/Probability/Measure_Space.thy
2015-05-04 hoelzl 2015-05-04 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
2015-04-22 paulson 2015-04-22 fixes for limits
2015-04-21 paulson 2015-04-21 New material, mostly about limits. Consolidation.
2015-04-14 Andreas Lochbihler 2015-04-14 add lemmas about restrict_space
2015-03-05 hoelzl 2015-03-05 fix import path
2015-01-22 hoelzl 2015-01-22 import general thms from Density_Compiler
2014-11-24 hoelzl 2014-11-24 add congruence solver to measurability prover
2014-11-17 hoelzl 2014-11-17 add reindex rules for distr and nn_integral on count_space
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-07 hoelzl 2014-10-07 add Giry monad
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-30 hoelzl 2014-06-30 some lemmas about the indicator function; removed lemma sums_def2
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-06-18 hoelzl 2014-06-18 filters are easier to define with INF on filters.
2014-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-06-12 hoelzl 2014-06-12 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
2014-05-30 hoelzl 2014-05-30 better support for restrict_space
2014-05-20 hoelzl 2014-05-20 add various lemmas
2014-05-19 hoelzl 2014-05-19 fixed document generation for HOL-Probability
2014-03-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-18 hoelzl 2014-03-18 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2013-11-12 hoelzl 2013-11-12 add restrict_space measure
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-03-05 hoelzl 2013-03-05 generalized lemmas in Extended_Real_Limits
2013-01-31 hoelzl 2013-01-31 use order topology for extended reals
2012-12-07 hoelzl 2012-12-07 add exponential and uniform distributions
2012-12-05 hoelzl 2012-12-05 Move the measurability prover to its own file
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-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-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 add induction rule for intersection-stable sigma-sets
2012-10-10 hoelzl 2012-10-10 remove incseq assumption from measure_eqI_generator_eq
2012-10-10 hoelzl 2012-10-10 tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
2012-04-25 hoelzl 2012-04-25 add Caratheodories theorem for semi-rings of sets
2012-04-25 hoelzl 2012-04-25 moved lemmas to appropriate places
2012-04-23 hoelzl 2012-04-23 reworked Probability theory