isabelle: src/HOL/Probability/Probability.thy@979cdfdf7a79 (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
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	15	begin
47694 05663f75964c reworked Probability theory hoelzl parents: 45713 diff changeset	16
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	17	end

author	hoelzl
	Thu, 13 Oct 2016 18:36:06 +0200
changeset 64283	979cdfdf7a79
parent 63716	91a0494d8a4a
child 64289	42f28160bad9
permissions	-rw-r--r--