isabelle: src/HOL/Probability/Probability.thy@1546a042e87b (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
42861 16375b493b64 Add formalization of probabilistic independence for families of sets hoelzl parents: 42148 diff changeset	10	Independent_Family
50419 3177d0374701 add exponential and uniform distributions hoelzl parents: 50089 diff changeset	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 93d87fd1583d add measure space for (coinductive) streams hoelzl parents: 58587 diff changeset	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
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
61359 e985b52c3eb3 cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution hoelzl parents: 59092 diff changeset	18

author	eberlm
	Tue, 05 Jan 2016 17:54:10 +0100
changeset 62065	1546a042e87b
parent 61359	e985b52c3eb3
child 62083	7582b39f51ed
permissions	-rw-r--r--