isabelle: src/HOL/Probability/Probability.thy@412140038d3c (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
58588 93d87fd1583d add measure space for (coinductive) streams hoelzl parents: 58587 diff changeset	11	Stream_Space
59092 d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav hoelzl parents: 58606 diff changeset	12	Embed_Measure
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: 61359 diff changeset	13	Central_Limit_Theorem
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	14	begin
47694 05663f75964c reworked Probability theory hoelzl parents: 45713 diff changeset	15
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	16	end

author	nipkow
	Sat, 21 May 2016 07:08:46 +0200
changeset 63106	412140038d3c
parent 62083	7582b39f51ed
child 63122	dd651e3f7413
permissions	-rw-r--r--