isabelle: src/HOL/Probability/Probability.thy@0b7bdb75f451 (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
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 32d1795cc77a added projective limit; immler parents: 50087 diff changeset	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 0b7bdb75f451 Added code generation for PMFs eberlm parents: 63122 diff changeset	11	PMF_Impl
58588 93d87fd1583d add measure space for (coinductive) streams hoelzl parents: 58587 diff changeset	12	Stream_Space
63122 dd651e3f7413 Added set permutations/random permutations eberlm parents: 62083 diff changeset	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 7582b39f51ed add the proof of the central limit theorem hoelzl parents: 61359 diff changeset	15	Central_Limit_Theorem
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	16	begin
47694 05663f75964c reworked Probability theory hoelzl parents: 45713 diff changeset	17
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	18	end

author	eberlm
	Tue, 31 May 2016 13:02:44 +0200
changeset 63194	0b7bdb75f451
parent 63122	dd651e3f7413
child 63243	1bc6816fd525
permissions	-rw-r--r--