src/HOL/Probability/Independent_Family.thy
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