isabelle: src/HOL/Probability/Probability.thy@3804a9640088 (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
66026 704e4970d703 HOL-Probability: add measurable space for trees hoelzl parents: 64320 diff changeset	14	Tree_Space
64283 979cdfdf7a79 HOL-Probability: move conditional expectation from AFP/Ergodic_Theory hoelzl parents: 63716 diff changeset	15	Conditional_Expectation
64289 42f28160bad9 HOL-Analysis: move Function Topology from AFP/Ergodict_Theory; HOL-Probability: move Essential Supremum from AFP/Lp hoelzl parents: 64283 diff changeset	16	Essential_Supremum
64320 ba194424b895 HOL-Probability: move stopping time from AFP/Markov_Models hoelzl parents: 64289 diff changeset	17	Stopping_Time
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	eberlm <eberlm@in.tum.de>
	Fri, 09 Jun 2017 18:36:25 +0200
changeset 66050	3804a9640088
parent 66026	704e4970d703
child 73253	f6bb31879698
permissions	-rw-r--r--