author  wenzelm 
Thu, 18 Apr 2013 17:07:01 +0200  
changeset 51717  9e7d1c139569 
parent 50419  3177d0374701 
child 57252  19b7ace1c5da 
permissions  rwrr 
33536  1 
theory Probability 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
35833
diff
changeset

2 
imports 
50089
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
50088
diff
changeset

3 
Discrete_Topology 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
40859
diff
changeset

4 
Complete_Measure 
42148  5 
Probability_Measure 
42147  6 
Infinite_Product_Measure 
50088  7 
Projective_Limit 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
42148
diff
changeset

8 
Independent_Family 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
35833
diff
changeset

9 
Information 
50419  10 
Distributions 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

11 
begin 
47694  12 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

13 
end 