author | hoelzl |
Wed, 06 Jan 2016 12:18:53 +0100 | |
changeset 62083 | 7582b39f51ed |
parent 61359 | e985b52c3eb3 |
child 63122 | dd651e3f7413 |
permissions | -rw-r--r-- |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
58606
diff
changeset
|
1 |
(* Title: HOL/Probability/Probability.thy |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
58606
diff
changeset
|
2 |
Author: Johannes Hölzl, TU München |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
58606
diff
changeset
|
3 |
*) |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
58606
diff
changeset
|
4 |
|
33536 | 5 |
theory Probability |
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
35833
diff
changeset
|
6 |
imports |
50089
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
50088
diff
changeset
|
7 |
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
|
8 |
Complete_Measure |
50088 | 9 |
Projective_Limit |
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
57252
diff
changeset
|
10 |
Probability_Mass_Function |
58588 | 11 |
Stream_Space |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
58606
diff
changeset
|
12 |
Embed_Measure |
62083 | 13 |
Central_Limit_Theorem |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
14 |
begin |
47694 | 15 |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
16 |
end |