src/HOL/Probability/Borel_Space.thy
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;
2011-03-22 hoelzl 2011-03-22 standardized headers
2011-03-14 hoelzl 2011-03-14 reworked Probability theory: measures are not type restricted to positive extended reals
2011-03-14 hoelzl 2011-03-14 moved t2_spaces to HOL image
2011-02-23 hoelzl 2011-02-23 log is borel measurable
2011-01-14 hoelzl 2011-01-14 tuned formalization of subalgebra
2010-12-08 hoelzl 2010-12-08 use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
2010-12-08 hoelzl 2010-12-08 integral over setprod
2010-12-08 haftmann 2010-12-08 work around problems with eta-expansion of equations
2010-12-08 haftmann 2010-12-08 nice syntax for lattice INFI, SUPR; various *_apply rules for lattice operations on fun; more default simplification rules
2010-12-06 hoelzl 2010-12-06 folding on arbitrary Lebesgue integrable functions
2010-12-06 hoelzl 2010-12-06 fixed spelling errors
2010-12-03 hoelzl 2010-12-03 it is known as the extended reals, not the infinite reals
2010-12-01 hoelzl 2010-12-01 Tuned setup for borel_measurable with min, max and psuminf.
2010-12-01 hoelzl 2010-12-01 Replace algebra_eqI by algebra.equality; Move sets_sigma_subset to Sigma_Algebra;
2010-12-01 hoelzl 2010-12-01 Support product spaces on sigma finite measures. Introduce the almost everywhere quantifier. Introduce 'morphism' theorems for most constants. Prove uniqueness of measures on cut stable generators. Prove uniqueness of the Radon-Nikodym derivative. Removed misleading suffix from borel_space and lebesgue_space. Use product spaces to introduce Fubini on the Lebesgue integral. Combine Euclidean_Lebesgue and Lebesgue_Measure. Generalize theorems about mutual information and entropy to arbitrary probability spaces. Remove simproc mult_log as it does not work with interpretations. Introduce completion of measure spaces. Change type of sigma. Introduce dynkin systems.