| author | sultana | 
| Sat, 14 Apr 2012 23:52:17 +0100 | |
| changeset 47477 | 3fabf352243e | 
| parent 45713 | badee348c5fb | 
| child 47694 | 05663f75964c | 
| permissions | -rw-r--r-- | 
| 33536 | 1 | theory Probability | 
| 36080 
0d9affa4e73c
Added Information theory and Example: dining cryptographers
 hoelzl parents: 
35833diff
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: 
40859diff
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: 
42148diff
changeset | 6 | Independent_Family | 
| 43556 
0d78c8d31d0d
move conditional expectation to its own theory file
 hoelzl parents: 
42902diff
changeset | 7 | Conditional_Probability | 
| 36080 
0d9affa4e73c
Added Information theory and Example: dining cryptographers
 hoelzl parents: 
35833diff
changeset | 8 | Information | 
| 33271 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
 paulson parents: diff
changeset | 9 | begin | 
| 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
 paulson parents: diff
changeset | 10 | end |