isabelle: src/HOL/Probability/Probability.thy@087d81f5213e (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
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav hoelzl parents: 58606 diff changeset	15	Interval_Integral
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav hoelzl parents: 58606 diff changeset	16	Set_Integral
58606 9c66f7c541fb add Giry monad hoelzl parents: 58588 diff changeset	17	Giry_Monad
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	18	begin
47694 05663f75964c reworked Probability theory hoelzl parents: 45713 diff changeset	19
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	20	end

author	wenzelm
	Mon, 06 Apr 2015 23:14:05 +0200
changeset 59940	087d81f5213e
parent 59092	d469103c0737
child 61359	e985b52c3eb3
permissions	-rw-r--r--