src/HOL/Probability/Independent_Family.thy
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Fri, 05 Aug 2016 18:34:57 +0200 hoelzl move measure theory from HOL-Probability to HOL-Multivariate_Analysis
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Thu, 14 Apr 2016 15:48:11 +0200 hoelzl Probability: move emeasure and nn_integral from ereal to ennreal
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Mon, 07 Dec 2015 20:19:59 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 07 Oct 2015 17:11:16 +0200 hoelzl cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Sun, 02 Nov 2014 17:06:05 +0100 wenzelm modernized header;
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Mon, 30 Jun 2014 15:45:21 +0200 hoelzl import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Thu, 12 Jun 2014 15:47:36 +0200 hoelzl properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
Sat, 15 Mar 2014 08:31:33 +0100 haftmann more complete set of lemmas wrt. image and composition
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Tue, 27 Nov 2012 11:29:47 +0100 immler qualified interpretation of sigma_algebra, to avoid name clashes
Mon, 19 Nov 2012 12:29:02 +0100 hoelzl merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
Fri, 16 Nov 2012 18:45:57 +0100 hoelzl move theorems to be more generally useable
Thu, 15 Nov 2012 10:49:58 +0100 immler regularity of measures, therefore:
Tue, 06 Nov 2012 19:18:35 +0100 hoelzl add support for function application to measurability prover
Fri, 02 Nov 2012 14:23:54 +0100 hoelzl use measurability prover
Wed, 10 Oct 2012 12:12:31 +0200 hoelzl joint distribution of independent variables
Wed, 10 Oct 2012 12:12:30 +0200 hoelzl indep_vars does not need sigma-sets
Wed, 10 Oct 2012 12:12:23 +0200 hoelzl remove incseq assumption from measure_eqI_generator_eq
Wed, 10 Oct 2012 12:12:21 +0200 hoelzl simplified assumptions for kolmogorov_0_1_law
Wed, 10 Oct 2012 12:12:18 +0200 hoelzl tuned product measurability
Wed, 10 Oct 2012 12:12:14 +0200 hoelzl rename terminal_events to tail_event
Mon, 23 Apr 2012 12:14:35 +0200 hoelzl reworked Probability theory
Tue, 28 Feb 2012 21:53:36 +0100 wenzelm avoid undeclared variables in let bindings;
Wed, 07 Dec 2011 15:10:29 +0100 hoelzl 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
Thu, 18 Aug 2011 13:36:58 -0700 huffman remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
Tue, 19 Jul 2011 14:36:12 +0200 hoelzl Rename extreal => ereal
Thu, 09 Jun 2011 14:04:34 +0200 hoelzl lemma: independence is equal to mutual information = 0
Thu, 26 May 2011 17:59:39 +0200 hoelzl introduce independence of two random variables
Thu, 26 May 2011 17:40:01 +0200 hoelzl add lemma indep_distribution_eq_measure
Thu, 26 May 2011 14:12:06 +0200 hoelzl add lemma indep_rv_finite
Thu, 26 May 2011 14:12:02 +0200 hoelzl add lemma borel_0_1_law
Thu, 26 May 2011 14:12:00 +0200 hoelzl use abbrevitation events == sets M
Thu, 26 May 2011 14:11:58 +0200 hoelzl add lemma kolmogorov_0_1_law
Thu, 26 May 2011 14:11:57 +0200 hoelzl add lemma indep_sets_collect_sigma
Tue, 17 May 2011 11:47:36 +0200 hoelzl Add formalization of probabilistic independence for families of sets
less more (0) tip