author | hoelzl |
Tue, 07 Oct 2014 10:34:24 +0200 | |
changeset 58606 | 9c66f7c541fb |
parent 58588 | 93d87fd1583d |
child 59092 | d469103c0737 |
permissions | -rw-r--r-- |
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 |
50088 | 5 |
Projective_Limit |
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
42148
diff
changeset
|
6 |
Independent_Family |
50419 | 7 |
Distributions |
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
57252
diff
changeset
|
8 |
Probability_Mass_Function |
58588 | 9 |
Stream_Space |
58606 | 10 |
Giry_Monad |
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 |