isabelle: src/HOL/Probability/Probability.thy@9a28fc03c3fe (annotated)

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 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset	5	theory Probability
36080 0d9affa4e73c Added Information theory and Example: dining cryptographers hoelzl parents: 35833 diff changeset	6	imports
63716 91a0494d8a4a HOL-Probability: Projective_Limit was missing (cf. 44ce6b524ff3); tuned hoelzl parents: 63626 diff changeset	7	Central_Limit_Theorem
50089 1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: 50088 diff changeset	8	Discrete_Topology
63194 0b7bdb75f451 Added code generation for PMFs eberlm parents: 63122 diff changeset	9	PMF_Impl
63716 91a0494d8a4a HOL-Probability: Projective_Limit was missing (cf. 44ce6b524ff3); tuned hoelzl parents: 63626 diff changeset	10	Projective_Limit
63122 dd651e3f7413 Added set permutations/random permutations eberlm parents: 62083 diff changeset	11	Random_Permutations
63716 91a0494d8a4a HOL-Probability: Projective_Limit was missing (cf. 44ce6b524ff3); tuned hoelzl parents: 63626 diff changeset	12	SPMF
91a0494d8a4a HOL-Probability: Projective_Limit was missing (cf. 44ce6b524ff3); tuned hoelzl parents: 63626 diff changeset	13	Stream_Space
64283 979cdfdf7a79 HOL-Probability: move conditional expectation from AFP/Ergodic_Theory hoelzl parents: 63716 diff changeset	14	Conditional_Expectation
64289 42f28160bad9 HOL-Analysis: move Function Topology from AFP/Ergodict_Theory; HOL-Probability: move Essential Supremum from AFP/Lp hoelzl parents: 64283 diff changeset	15	Essential_Supremum
64320 ba194424b895 HOL-Probability: move stopping time from AFP/Markov_Models hoelzl parents: 64289 diff changeset	16	Stopping_Time
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	17	begin
47694 05663f75964c reworked Probability theory hoelzl parents: 45713 diff changeset	18
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	19	end

author	wenzelm
	Fri, 26 May 2017 11:09:16 +0200
changeset 65930	9a28fc03c3fe
parent 64320	ba194424b895
child 66026	704e4970d703
permissions	-rw-r--r--