isabelle: src/HOL/Probability/Probability.thy@604653cc39cb (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
73253 f6bb31879698 HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc. Manuel Eberl <eberlm@in.tum.de> parents: 66026 diff changeset	13	Product_PMF
f6bb31879698 HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc. Manuel Eberl <eberlm@in.tum.de> parents: 66026 diff changeset	14	Hoeffding
63716 91a0494d8a4a HOL-Probability: Projective_Limit was missing (cf. 44ce6b524ff3); tuned hoelzl parents: 63626 diff changeset	15	Stream_Space
66026 704e4970d703 HOL-Probability: add measurable space for trees hoelzl parents: 64320 diff changeset	16	Tree_Space
64283 979cdfdf7a79 HOL-Probability: move conditional expectation from AFP/Ergodic_Theory hoelzl parents: 63716 diff changeset	17	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	18	Essential_Supremum
64320 ba194424b895 HOL-Probability: move stopping time from AFP/Markov_Models hoelzl parents: 64289 diff changeset	19	Stopping_Time
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	20	begin
47694 05663f75964c reworked Probability theory hoelzl parents: 45713 diff changeset	21
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	22	end

author	paulson
	Sat, 27 Jul 2024 11:41:17 +0100
changeset 80619	604653cc39cb
parent 73253	f6bb31879698
permissions	-rw-r--r--