author | hoelzl |
Fri, 05 Dec 2014 12:06:18 +0100 | |
changeset 59092 | d469103c0737 |
parent 58606 | 9c66f7c541fb |
child 61359 | e985b52c3eb3 |
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 |
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
42148
diff
changeset
|
10 |
Independent_Family |
50419 | 11 |
Distributions |
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
57252
diff
changeset
|
12 |
Probability_Mass_Function |
58588 | 13 |
Stream_Space |
59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
58606
diff
changeset
|
14 |
Embed_Measure |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
58606
diff
changeset
|
15 |
Interval_Integral |
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
58606
diff
changeset
|
16 |
Set_Integral |
58606 | 17 |
Giry_Monad |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
18 |
begin |
47694 | 19 |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
20 |
end |