src/HOL/Probability/Projective_Family.thy
8 months ago haftmann 2018-11-18 removed legacy input syntax
8 months ago haftmann 2018-11-08 removed relics of ASCII syntax for indexed big operators
2016-08-05 hoelzl 2016-08-05 move measure theory from HOL-Probability to HOL-Multivariate_Analysis
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-04-14 hoelzl 2016-04-14 Probability: move emeasure and nn_integral from ereal to ennreal
2016-01-01 wenzelm 2016-01-01 more symbols;
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-10-07 hoelzl 2015-10-07 cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
2014-11-02 wenzelm 2014-11-02 modernized header;
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
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2012-11-28 wenzelm 2012-11-28 eliminated slightly odd identifiers;
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-19 hoelzl 2012-11-19 tuned FinMap
2012-11-19 hoelzl 2012-11-19 merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
2012-11-16 hoelzl 2012-11-16 renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space
2012-11-16 immler 2012-11-16 renamed to more appropriate lim_P for projective limit
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-09 immler 2012-11-09 moved lemmas into projective_family; added header for theory Projective_Family
2012-11-09 immler 2012-11-09 removed redundant/unnecessary assumptions from projective_family
2012-11-07 immler 2012-11-07 assume probability spaces; allow empty index set
2012-11-07 immler 2012-11-07 added projective_family; generalized generator in product_prob_space to projective_family