src/HOL/Probability/Borel_Space.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
2015-01-13 hoelzl 2015-01-13 measurability prover: removed app splitting, replaced by more powerful destruction rules
2014-12-04 hoelzl 2014-12-04 generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
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-13 immler 2014-10-13 relaxed class constraints for exp
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add 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-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-06-16 hoelzl 2014-06-16 add more derivative and continuity rules for complex-values functions
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 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-21 hoelzl 2014-05-21 generalized Bochner integral over infinite sums
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-04-02 hoelzl 2014-04-02 extend continuous_intros; remove continuous_on_intros and isCont_intros
2014-03-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2013-12-16 immler 2013-12-16 prefer box over greaterThanLessThan on euclidean_space
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-08-27 hoelzl 2013-08-27 renamed inner_dense_linorder to dense_linorder
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 move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
2013-03-05 hoelzl 2013-03-05 generalized lemmas in Extended_Real_Limits
2013-02-13 immler 2013-02-13 eliminated union_closed_basis; cleanup Fin_Map
2013-01-14 hoelzl 2013-01-14 move prod instantiation of second_countable_topology to its definition
2013-01-14 hoelzl 2013-01-14 renamed countable_basis_space to second_countable_topology
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-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 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 move theorems to be more generally useable
2012-11-16 hoelzl 2012-11-16 more measurability rules
2012-11-16 immler 2012-11-16 allow arbitrary enumerations of basis in locale for generation of borel sets
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-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 use continuity to show Borel-measurability
2012-04-25 hoelzl 2012-04-25 moved lemmas to appropriate places
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-12 noschinl 2012-03-12 tuned proofs
2012-02-28 wenzelm 2012-02-28 avoid undeclared variables in let bindings; tuned proofs;
2011-10-28 hoelzl 2011-10-28 correct import path
2011-10-28 hoelzl 2011-10-28 allow to build Probability and MV-Analysis with one ROOT.ML
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-02 huffman 2011-09-02 remove more duplicate lemmas
2011-08-26 huffman 2011-08-26 make HOL-Probability respect set/pred distinction
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 add ereal to typeclass infinity
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal
2011-05-26 hoelzl 2011-05-26 composition of convex and measurable function is measurable
2011-05-23 hoelzl 2011-05-23 move lemmas to Extended_Reals and Extended_Real_Limits
2011-05-17 hoelzl 2011-05-17 add borel_eq_atLeastLessThan
2011-03-29 wenzelm 2011-03-29 tuned headers;