author | haftmann |
Thu, 13 Oct 2011 23:27:46 +0200 | |
changeset 45140 | 339a8b3c4791 |
parent 43556 | 0d78c8d31d0d |
child 45713 | badee348c5fb |
permissions | -rw-r--r-- |
33536 | 1 |
theory Probability |
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
35833
diff
changeset
|
2 |
imports |
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
|
3 |
Complete_Measure |
42148 | 4 |
Probability_Measure |
42147 | 5 |
Infinite_Product_Measure |
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
42148
diff
changeset
|
6 |
Independent_Family |
43556
0d78c8d31d0d
move conditional expectation to its own theory file
hoelzl
parents:
42902
diff
changeset
|
7 |
Conditional_Probability |
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
35833
diff
changeset
|
8 |
Information |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
35833
diff
changeset
|
9 |
"ex/Dining_Cryptographers" |
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
|
10 |
"ex/Koepf_Duermuth_Countermeasure" |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
11 |
begin |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
12 |
end |