author | eberlm |
Tue, 31 May 2016 13:02:44 +0200 | |
changeset 63194 | 0b7bdb75f451 |
parent 63122 | dd651e3f7413 |
child 63243 | 1bc6816fd525 |
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 |
63194 | 11 |
PMF_Impl |
58588 | 12 |
Stream_Space |
63122 | 13 |
Random_Permutations |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
58606
diff
changeset
|
14 |
Embed_Measure |
62083 | 15 |
Central_Limit_Theorem |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
16 |
begin |
47694 | 17 |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
18 |
end |