author | hoelzl |
Mon, 06 Oct 2014 16:27:07 +0200 | |
changeset 58587 | 5484f6079bcd |
parent 57252 | 19b7ace1c5da |
child 58588 | 93d87fd1583d |
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 |
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 |
50419 | 9 |
Distributions |
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
57252
diff
changeset
|
10 |
Probability_Mass_Function |
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 |