src/HOL/Probability/Finite_Product_Measure.thy
2015-12-30 wenzelm 2015-12-30 clarified print modes;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-04 ballarin 2015-11-04 Qualifiers in locale expressions default to mandatory regardless of the command.
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-10-08 hoelzl 2015-10-08 measurable sets on product spaces are embeddings of countable products
2015-10-08 hoelzl 2015-10-08 generalize eqI theorems for product measures
2015-10-07 hoelzl 2015-10-07 cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-13 wenzelm 2015-09-13 renamed method "goals" to "goal_cases" to emphasize its meaning;
2015-06-25 wenzelm 2015-06-25 tuned proofs;
2015-01-22 hoelzl 2015-01-22 import general thms from Density_Compiler
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-24 hoelzl 2014-11-24 add congruence solver to measurability prover
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-07 hoelzl 2014-10-07 add Giry monad
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-05-20 hoelzl 2014-05-20 add various lemmas
2014-05-19 hoelzl 2014-05-19 renamed positive_integral to nn_integral
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-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
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-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 move theorems to be more generally useable
2012-11-16 hoelzl 2012-11-16 measurability for nat_case and comb_seq
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-06 immler 2012-11-06 moved lemmas further up
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 for the product measure it is enough if only one measure is sigma-finite
2012-10-10 hoelzl 2012-10-10 remove incseq assumption from measure_eqI_generator_eq
2012-10-10 hoelzl 2012-10-10 merge should operate on pairs
2012-10-10 hoelzl 2012-10-10 remove incseq assumption from sigma_prod_algebra_sigma_eq
2012-10-10 hoelzl 2012-10-10 tuned product 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-13 wenzelm 2012-03-13 tuned proofs -- eliminated pointless chaining of facts after 'interpret';
2012-02-28 wenzelm 2012-02-28 avoid undeclared variables in let bindings; tuned proofs;
2011-12-07 hoelzl 2011-12-07 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
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-07-19 hoelzl 2011-07-19 Rename extreal => ereal
2011-05-26 hoelzl 2011-05-26 add lemma indep_distribution_eq_measure
2011-05-23 hoelzl 2011-05-23 move lemmas to Extended_Reals and Extended_Real_Limits
2011-03-29 hoelzl 2011-03-29 split Product_Measure into Binary_Product_Measure and Finite_Product_Measure