src/HOL/Probability/Sigma_Algebra.thy
2015-01-16 hoelzl 2015-01-16 tuned measurability proofs
2015-01-15 hoelzl 2015-01-15 piecewise measurability using restrict_space; cleanup Borel_Space
2014-12-05 hoelzl 2014-12-05 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
2014-12-04 hoelzl 2014-12-04 generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
2014-11-24 hoelzl 2014-11-24 add congruence solver to measurability prover
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 fix document generation for HOL-Probability
2014-10-07 hoelzl 2014-10-07 add Giry monad
2014-10-06 hoelzl 2014-10-06 add measure space for (coinductive) streams
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-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-05-30 hoelzl 2014-05-30 generalizd measurability on restricted space; rule for integrability on compact sets
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-05-19 hoelzl 2014-05-19 introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
2014-05-13 hoelzl 2014-05-13 clean up Lebesgue integration
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2013-11-13 hoelzl 2013-11-13 fix document generation for HOL-Probability
2013-11-12 hoelzl 2013-11-12 measure of a countable union
2013-11-12 hoelzl 2013-11-12 add restrict_space measure
2013-09-24 Andreas Lochbihler 2013-09-24 make measure_of total
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-04-10 hoelzl 2013-04-10 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
2012-12-14 hoelzl 2012-12-14 Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
2012-12-05 hoelzl 2012-12-05 Move the measurability prover to its own file
2012-12-05 hoelzl 2012-12-05 Show search depth in the debug output of the measurability prover
2012-11-29 hoelzl 2012-11-29 make SML/NJ happy (give names for all fields in a record)
2012-11-28 wenzelm 2012-11-28 eliminated slightly odd identifiers;
2012-11-27 immler 2012-11-27 based countable topological basis on Countable_Set
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-16 hoelzl 2012-11-16 more measurability rules
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-11-02 hoelzl 2012-11-02 add measurability prover; add support for Borel sets
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-10-10 hoelzl 2012-10-10 add induction rule for intersection-stable sigma-sets
2012-10-10 hoelzl 2012-10-10 add measurable_compose
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 correct lemma name
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-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-26 huffman 2011-08-26 make HOL-Probability respect set/pred distinction
2011-08-09 haftmann 2011-08-09 tuned proofs
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 sigma_sets_singleton
2011-05-26 hoelzl 2011-05-26 add lemma indep_sets_collect_sigma
2011-05-17 hoelzl 2011-05-17 Collect intro-rules for sigma-algebras * * * sets_Collect shouldn't be intro rules
2011-05-17 hoelzl 2011-05-17 add measurable_Least
2011-05-17 hoelzl 2011-05-17 add restrict_sigma
2011-03-29 hoelzl 2011-03-29 proved caratheodory_empty_continuous
2011-03-22 hoelzl 2011-03-22 standardized headers
2011-03-22 hoelzl 2011-03-22 add ring_of_sets and subset_class as basis for algebra
2011-03-14 wenzelm 2011-03-14 standardized headers;