src/HOL/Probability/Probability_Mass_Function.thy
 author Lars Hupel Mon Jan 22 15:50:29 2018 +0100 (19 months ago) changeset 67486 d617e84bb2b1 parent 67399 eab6ce8368fa child 67489 f1ba59ddd9a6 permissions -rw-r--r--
tuned
 hoelzl@58606 ` 1` ```(* Title: HOL/Probability/Probability_Mass_Function.thy ``` lp15@59667 ` 2` ``` Author: Johannes Hölzl, TU München ``` Andreas@59023 ` 3` ``` Author: Andreas Lochbihler, ETH Zurich ``` Andreas@59023 ` 4` ```*) ``` hoelzl@58606 ` 5` hoelzl@59000 ` 6` ```section \ Probability mass function \ ``` hoelzl@59000 ` 7` hoelzl@58587 ` 8` ```theory Probability_Mass_Function ``` hoelzl@59000 ` 9` ```imports ``` hoelzl@59000 ` 10` ``` Giry_Monad ``` wenzelm@66453 ` 11` ``` "HOL-Library.Multiset" ``` hoelzl@58587 ` 12` ```begin ``` hoelzl@58587 ` 13` hoelzl@59664 ` 14` ```lemma AE_emeasure_singleton: ``` hoelzl@59664 ` 15` ``` assumes x: "emeasure M {x} \ 0" and ae: "AE x in M. P x" shows "P x" ``` hoelzl@59664 ` 16` ```proof - ``` hoelzl@59664 ` 17` ``` from x have x_M: "{x} \ sets M" ``` hoelzl@59664 ` 18` ``` by (auto intro: emeasure_notin_sets) ``` hoelzl@59664 ` 19` ``` from ae obtain N where N: "{x\space M. \ P x} \ N" "emeasure M N = 0" "N \ sets M" ``` hoelzl@59664 ` 20` ``` by (auto elim: AE_E) ``` hoelzl@59664 ` 21` ``` { assume "\ P x" ``` hoelzl@59664 ` 22` ``` with x_M[THEN sets.sets_into_space] N have "emeasure M {x} \ emeasure M N" ``` hoelzl@59664 ` 23` ``` by (intro emeasure_mono) auto ``` hoelzl@59664 ` 24` ``` with x N have False ``` hoelzl@62975 ` 25` ``` by (auto simp:) } ``` hoelzl@59664 ` 26` ``` then show "P x" by auto ``` hoelzl@59664 ` 27` ```qed ``` hoelzl@59664 ` 28` hoelzl@59664 ` 29` ```lemma AE_measure_singleton: "measure M {x} \ 0 \ AE x in M. P x \ P x" ``` hoelzl@59664 ` 30` ``` by (metis AE_emeasure_singleton measure_def emeasure_empty measure_empty) ``` hoelzl@59664 ` 31` hoelzl@59000 ` 32` ```lemma (in finite_measure) AE_support_countable: ``` hoelzl@59000 ` 33` ``` assumes [simp]: "sets M = UNIV" ``` hoelzl@59000 ` 34` ``` shows "(AE x in M. measure M {x} \ 0) \ (\S. countable S \ (AE x in M. x \ S))" ``` hoelzl@59000 ` 35` ```proof ``` hoelzl@59000 ` 36` ``` assume "\S. countable S \ (AE x in M. x \ S)" ``` hoelzl@59000 ` 37` ``` then obtain S where S[intro]: "countable S" and ae: "AE x in M. x \ S" ``` hoelzl@59000 ` 38` ``` by auto ``` lp15@59667 ` 39` ``` then have "emeasure M (\x\{x\S. emeasure M {x} \ 0}. {x}) = ``` hoelzl@59000 ` 40` ``` (\\<^sup>+ x. emeasure M {x} * indicator {x\S. emeasure M {x} \ 0} x \count_space UNIV)" ``` hoelzl@59000 ` 41` ``` by (subst emeasure_UN_countable) ``` hoelzl@59000 ` 42` ``` (auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space) ``` hoelzl@59000 ` 43` ``` also have "\ = (\\<^sup>+ x. emeasure M {x} * indicator S x \count_space UNIV)" ``` hoelzl@59000 ` 44` ``` by (auto intro!: nn_integral_cong split: split_indicator) ``` hoelzl@59000 ` 45` ``` also have "\ = emeasure M (\x\S. {x})" ``` hoelzl@59000 ` 46` ``` by (subst emeasure_UN_countable) ``` hoelzl@59000 ` 47` ``` (auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space) ``` hoelzl@59000 ` 48` ``` also have "\ = emeasure M (space M)" ``` hoelzl@59000 ` 49` ``` using ae by (intro emeasure_eq_AE) auto ``` hoelzl@59000 ` 50` ``` finally have "emeasure M {x \ space M. x\S \ emeasure M {x} \ 0} = emeasure M (space M)" ``` hoelzl@59000 ` 51` ``` by (simp add: emeasure_single_in_space cong: rev_conj_cong) ``` hoelzl@59000 ` 52` ``` with finite_measure_compl[of "{x \ space M. x\S \ emeasure M {x} \ 0}"] ``` hoelzl@59000 ` 53` ``` have "AE x in M. x \ S \ emeasure M {x} \ 0" ``` hoelzl@62975 ` 54` ``` by (intro AE_I[OF order_refl]) (auto simp: emeasure_eq_measure measure_nonneg set_diff_eq cong: conj_cong) ``` hoelzl@59000 ` 55` ``` then show "AE x in M. measure M {x} \ 0" ``` hoelzl@59000 ` 56` ``` by (auto simp: emeasure_eq_measure) ``` hoelzl@59000 ` 57` ```qed (auto intro!: exI[of _ "{x. measure M {x} \ 0}"] countable_support) ``` hoelzl@59000 ` 58` hoelzl@59664 ` 59` ```subsection \ PMF as measure \ ``` hoelzl@59000 ` 60` hoelzl@58587 ` 61` ```typedef 'a pmf = "{M :: 'a measure. prob_space M \ sets M = UNIV \ (AE x in M. measure M {x} \ 0)}" ``` hoelzl@58587 ` 62` ``` morphisms measure_pmf Abs_pmf ``` hoelzl@58606 ` 63` ``` by (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"]) ``` hoelzl@58606 ` 64` ``` (auto intro!: prob_space_uniform_measure AE_uniform_measureI) ``` hoelzl@58587 ` 65` hoelzl@58587 ` 66` ```declare [[coercion measure_pmf]] ``` hoelzl@58587 ` 67` hoelzl@58587 ` 68` ```lemma prob_space_measure_pmf: "prob_space (measure_pmf p)" ``` hoelzl@58587 ` 69` ``` using pmf.measure_pmf[of p] by auto ``` hoelzl@58587 ` 70` wenzelm@61605 ` 71` ```interpretation measure_pmf: prob_space "measure_pmf M" for M ``` hoelzl@58587 ` 72` ``` by (rule prob_space_measure_pmf) ``` hoelzl@58587 ` 73` wenzelm@61605 ` 74` ```interpretation measure_pmf: subprob_space "measure_pmf M" for M ``` hoelzl@59000 ` 75` ``` by (rule prob_space_imp_subprob_space) unfold_locales ``` hoelzl@59000 ` 76` hoelzl@59048 ` 77` ```lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)" ``` hoelzl@59048 ` 78` ``` by unfold_locales ``` hoelzl@59048 ` 79` hoelzl@58587 ` 80` ```locale pmf_as_measure ``` hoelzl@58587 ` 81` ```begin ``` hoelzl@58587 ` 82` hoelzl@58587 ` 83` ```setup_lifting type_definition_pmf ``` hoelzl@58587 ` 84` hoelzl@58587 ` 85` ```end ``` hoelzl@58587 ` 86` hoelzl@58587 ` 87` ```context ``` hoelzl@58587 ` 88` ```begin ``` hoelzl@58587 ` 89` hoelzl@58587 ` 90` ```interpretation pmf_as_measure . ``` hoelzl@58587 ` 91` hoelzl@58587 ` 92` ```lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV" ``` lp15@59667 ` 93` ``` by transfer blast ``` hoelzl@58587 ` 94` hoelzl@59048 ` 95` ```lemma sets_measure_pmf_count_space[measurable_cong]: ``` hoelzl@59048 ` 96` ``` "sets (measure_pmf M) = sets (count_space UNIV)" ``` hoelzl@59000 ` 97` ``` by simp ``` hoelzl@59000 ` 98` hoelzl@58587 ` 99` ```lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV" ``` hoelzl@58587 ` 100` ``` using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp ``` hoelzl@58587 ` 101` Andreas@61634 ` 102` ```lemma measure_pmf_UNIV [simp]: "measure (measure_pmf p) UNIV = 1" ``` Andreas@61634 ` 103` ```using measure_pmf.prob_space[of p] by simp ``` Andreas@61634 ` 104` hoelzl@59048 ` 105` ```lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \ space (subprob_algebra (count_space UNIV))" ``` hoelzl@59048 ` 106` ``` by (simp add: space_subprob_algebra subprob_space_measure_pmf) ``` hoelzl@59048 ` 107` hoelzl@58587 ` 108` ```lemma measurable_pmf_measure1[simp]: "measurable (M :: 'a pmf) N = UNIV \ space N" ``` hoelzl@58587 ` 109` ``` by (auto simp: measurable_def) ``` hoelzl@58587 ` 110` hoelzl@58587 ` 111` ```lemma measurable_pmf_measure2[simp]: "measurable N (M :: 'a pmf) = measurable N (count_space UNIV)" ``` hoelzl@58587 ` 112` ``` by (intro measurable_cong_sets) simp_all ``` hoelzl@58587 ` 113` hoelzl@59664 ` 114` ```lemma measurable_pair_restrict_pmf2: ``` hoelzl@59664 ` 115` ``` assumes "countable A" ``` hoelzl@59664 ` 116` ``` assumes [measurable]: "\y. y \ A \ (\x. f (x, y)) \ measurable M L" ``` hoelzl@59664 ` 117` ``` shows "f \ measurable (M \\<^sub>M restrict_space (measure_pmf N) A) L" (is "f \ measurable ?M _") ``` hoelzl@59664 ` 118` ```proof - ``` hoelzl@59664 ` 119` ``` have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)" ``` hoelzl@59664 ` 120` ``` by (simp add: restrict_count_space) ``` hoelzl@58587 ` 121` hoelzl@59664 ` 122` ``` show ?thesis ``` hoelzl@59664 ` 123` ``` by (intro measurable_compose_countable'[where f="\a b. f (fst b, a)" and g=snd and I=A, ``` haftmann@61424 ` 124` ``` unfolded prod.collapse] assms) ``` hoelzl@59664 ` 125` ``` measurable ``` hoelzl@59664 ` 126` ```qed ``` hoelzl@58587 ` 127` hoelzl@59664 ` 128` ```lemma measurable_pair_restrict_pmf1: ``` hoelzl@59664 ` 129` ``` assumes "countable A" ``` hoelzl@59664 ` 130` ``` assumes [measurable]: "\x. x \ A \ (\y. f (x, y)) \ measurable N L" ``` hoelzl@59664 ` 131` ``` shows "f \ measurable (restrict_space (measure_pmf M) A \\<^sub>M N) L" ``` hoelzl@59664 ` 132` ```proof - ``` hoelzl@59664 ` 133` ``` have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)" ``` hoelzl@59664 ` 134` ``` by (simp add: restrict_count_space) ``` hoelzl@59000 ` 135` hoelzl@59664 ` 136` ``` show ?thesis ``` hoelzl@59664 ` 137` ``` by (intro measurable_compose_countable'[where f="\a b. f (a, snd b)" and g=fst and I=A, ``` haftmann@61424 ` 138` ``` unfolded prod.collapse] assms) ``` hoelzl@59664 ` 139` ``` measurable ``` hoelzl@59664 ` 140` ```qed ``` hoelzl@59664 ` 141` hoelzl@59664 ` 142` ```lift_definition pmf :: "'a pmf \ 'a \ real" is "\M x. measure M {x}" . ``` hoelzl@59664 ` 143` hoelzl@59664 ` 144` ```lift_definition set_pmf :: "'a pmf \ 'a set" is "\M. {x. measure M {x} \ 0}" . ``` hoelzl@59664 ` 145` ```declare [[coercion set_pmf]] ``` hoelzl@58587 ` 146` hoelzl@58587 ` 147` ```lemma AE_measure_pmf: "AE x in (M::'a pmf). x \ M" ``` hoelzl@58587 ` 148` ``` by transfer simp ``` hoelzl@58587 ` 149` hoelzl@58587 ` 150` ```lemma emeasure_pmf_single_eq_zero_iff: ``` hoelzl@58587 ` 151` ``` fixes M :: "'a pmf" ``` hoelzl@58587 ` 152` ``` shows "emeasure M {y} = 0 \ y \ M" ``` hoelzl@62975 ` 153` ``` unfolding set_pmf.rep_eq by (simp add: measure_pmf.emeasure_eq_measure) ``` hoelzl@58587 ` 154` hoelzl@58587 ` 155` ```lemma AE_measure_pmf_iff: "(AE x in measure_pmf M. P x) \ (\y\M. P y)" ``` hoelzl@59664 ` 156` ``` using AE_measure_singleton[of M] AE_measure_pmf[of M] ``` hoelzl@59664 ` 157` ``` by (auto simp: set_pmf.rep_eq) ``` hoelzl@59664 ` 158` Andreas@61634 ` 159` ```lemma AE_pmfI: "(\y. y \ set_pmf M \ P y) \ almost_everywhere (measure_pmf M) P" ``` Andreas@61634 ` 160` ```by(simp add: AE_measure_pmf_iff) ``` Andreas@61634 ` 161` hoelzl@59664 ` 162` ```lemma countable_set_pmf [simp]: "countable (set_pmf p)" ``` hoelzl@59664 ` 163` ``` by transfer (metis prob_space.finite_measure finite_measure.countable_support) ``` hoelzl@59664 ` 164` hoelzl@59664 ` 165` ```lemma pmf_positive: "x \ set_pmf p \ 0 < pmf p x" ``` hoelzl@62975 ` 166` ``` by transfer (simp add: less_le) ``` hoelzl@59664 ` 167` hoelzl@62975 ` 168` ```lemma pmf_nonneg[simp]: "0 \ pmf p x" ``` hoelzl@62975 ` 169` ``` by transfer simp ``` hoelzl@63886 ` 170` eberlm@63099 ` 171` ```lemma pmf_not_neg [simp]: "\pmf p x < 0" ``` eberlm@63099 ` 172` ``` by (simp add: not_less pmf_nonneg) ``` eberlm@63099 ` 173` eberlm@63099 ` 174` ```lemma pmf_pos [simp]: "pmf p x \ 0 \ pmf p x > 0" ``` eberlm@63099 ` 175` ``` using pmf_nonneg[of p x] by linarith ``` hoelzl@59664 ` 176` hoelzl@59664 ` 177` ```lemma pmf_le_1: "pmf p x \ 1" ``` hoelzl@59664 ` 178` ``` by (simp add: pmf.rep_eq) ``` hoelzl@58587 ` 179` hoelzl@58587 ` 180` ```lemma set_pmf_not_empty: "set_pmf M \ {}" ``` hoelzl@58587 ` 181` ``` using AE_measure_pmf[of M] by (intro notI) simp ``` hoelzl@58587 ` 182` hoelzl@58587 ` 183` ```lemma set_pmf_iff: "x \ set_pmf M \ pmf M x \ 0" ``` hoelzl@58587 ` 184` ``` by transfer simp ``` hoelzl@58587 ` 185` hoelzl@62975 ` 186` ```lemma pmf_positive_iff: "0 < pmf p x \ x \ set_pmf p" ``` hoelzl@62975 ` 187` ``` unfolding less_le by (simp add: set_pmf_iff) ``` hoelzl@62975 ` 188` hoelzl@59664 ` 189` ```lemma set_pmf_eq: "set_pmf M = {x. pmf M x \ 0}" ``` hoelzl@59664 ` 190` ``` by (auto simp: set_pmf_iff) ``` hoelzl@59664 ` 191` eberlm@63099 ` 192` ```lemma set_pmf_eq': "set_pmf p = {x. pmf p x > 0}" ``` eberlm@63099 ` 193` ```proof safe ``` eberlm@63099 ` 194` ``` fix x assume "x \ set_pmf p" ``` eberlm@63099 ` 195` ``` hence "pmf p x \ 0" by (auto simp: set_pmf_eq) ``` eberlm@63099 ` 196` ``` with pmf_nonneg[of p x] show "pmf p x > 0" by simp ``` eberlm@63099 ` 197` ```qed (auto simp: set_pmf_eq) ``` eberlm@63099 ` 198` hoelzl@59664 ` 199` ```lemma emeasure_pmf_single: ``` hoelzl@59664 ` 200` ``` fixes M :: "'a pmf" ``` hoelzl@59664 ` 201` ``` shows "emeasure M {x} = pmf M x" ``` hoelzl@59664 ` 202` ``` by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure]) ``` hoelzl@59664 ` 203` Andreas@60068 ` 204` ```lemma measure_pmf_single: "measure (measure_pmf M) {x} = pmf M x" ``` hoelzl@62975 ` 205` ``` using emeasure_pmf_single[of M x] by(simp add: measure_pmf.emeasure_eq_measure pmf_nonneg measure_nonneg) ``` Andreas@60068 ` 206` hoelzl@59000 ` 207` ```lemma emeasure_measure_pmf_finite: "finite S \ emeasure (measure_pmf M) S = (\s\S. pmf M s)" ``` nipkow@64267 ` 208` ``` by (subst emeasure_eq_sum_singleton) (auto simp: emeasure_pmf_single pmf_nonneg) ``` hoelzl@59000 ` 209` nipkow@64267 ` 210` ```lemma measure_measure_pmf_finite: "finite S \ measure (measure_pmf M) S = sum (pmf M) S" ``` hoelzl@62975 ` 211` ``` using emeasure_measure_pmf_finite[of S M] ``` nipkow@64267 ` 212` ``` by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg sum_nonneg pmf_nonneg) ``` Andreas@59023 ` 213` nipkow@64267 ` 214` ```lemma sum_pmf_eq_1: ``` eberlm@63099 ` 215` ``` assumes "finite A" "set_pmf p \ A" ``` eberlm@63099 ` 216` ``` shows "(\x\A. pmf p x) = 1" ``` eberlm@63099 ` 217` ```proof - ``` eberlm@63099 ` 218` ``` have "(\x\A. pmf p x) = measure_pmf.prob p A" ``` eberlm@63099 ` 219` ``` by (simp add: measure_measure_pmf_finite assms) ``` eberlm@63099 ` 220` ``` also from assms have "\ = 1" ``` eberlm@63099 ` 221` ``` by (subst measure_pmf.prob_eq_1) (auto simp: AE_measure_pmf_iff) ``` eberlm@63099 ` 222` ``` finally show ?thesis . ``` eberlm@63099 ` 223` ```qed ``` eberlm@63099 ` 224` hoelzl@59000 ` 225` ```lemma nn_integral_measure_pmf_support: ``` hoelzl@62975 ` 226` ``` fixes f :: "'a \ ennreal" ``` hoelzl@59000 ` 227` ``` assumes f: "finite A" and nn: "\x. x \ A \ 0 \ f x" "\x. x \ set_pmf M \ x \ A \ f x = 0" ``` hoelzl@59000 ` 228` ``` shows "(\\<^sup>+x. f x \measure_pmf M) = (\x\A. f x * pmf M x)" ``` hoelzl@59000 ` 229` ```proof - ``` hoelzl@59000 ` 230` ``` have "(\\<^sup>+x. f x \M) = (\\<^sup>+x. f x * indicator A x \M)" ``` hoelzl@59000 ` 231` ``` using nn by (intro nn_integral_cong_AE) (auto simp: AE_measure_pmf_iff split: split_indicator) ``` hoelzl@59000 ` 232` ``` also have "\ = (\x\A. f x * emeasure M {x})" ``` hoelzl@59000 ` 233` ``` using assms by (intro nn_integral_indicator_finite) auto ``` hoelzl@59000 ` 234` ``` finally show ?thesis ``` hoelzl@59000 ` 235` ``` by (simp add: emeasure_measure_pmf_finite) ``` hoelzl@59000 ` 236` ```qed ``` hoelzl@59000 ` 237` hoelzl@59000 ` 238` ```lemma nn_integral_measure_pmf_finite: ``` hoelzl@62975 ` 239` ``` fixes f :: "'a \ ennreal" ``` hoelzl@59000 ` 240` ``` assumes f: "finite (set_pmf M)" and nn: "\x. x \ set_pmf M \ 0 \ f x" ``` hoelzl@59000 ` 241` ``` shows "(\\<^sup>+x. f x \measure_pmf M) = (\x\set_pmf M. f x * pmf M x)" ``` hoelzl@59000 ` 242` ``` using assms by (intro nn_integral_measure_pmf_support) auto ``` hoelzl@62975 ` 243` hoelzl@59000 ` 244` ```lemma integrable_measure_pmf_finite: ``` hoelzl@59000 ` 245` ``` fixes f :: "'a \ 'b::{banach, second_countable_topology}" ``` hoelzl@59000 ` 246` ``` shows "finite (set_pmf M) \ integrable M f" ``` hoelzl@62975 ` 247` ``` by (auto intro!: integrableI_bounded simp: nn_integral_measure_pmf_finite ennreal_mult_less_top) ``` hoelzl@59000 ` 248` hoelzl@64008 ` 249` ```lemma integral_measure_pmf_real: ``` hoelzl@59000 ` 250` ``` assumes [simp]: "finite A" and "\a. a \ set_pmf M \ f a \ 0 \ a \ A" ``` hoelzl@59000 ` 251` ``` shows "(\x. f x \measure_pmf M) = (\a\A. f a * pmf M a)" ``` hoelzl@59000 ` 252` ```proof - ``` hoelzl@59000 ` 253` ``` have "(\x. f x \measure_pmf M) = (\x. f x * indicator A x \measure_pmf M)" ``` hoelzl@59000 ` 254` ``` using assms(2) by (intro integral_cong_AE) (auto split: split_indicator simp: AE_measure_pmf_iff) ``` hoelzl@59000 ` 255` ``` also have "\ = (\a\A. f a * pmf M a)" ``` hoelzl@62975 ` 256` ``` by (subst integral_indicator_finite_real) ``` hoelzl@62975 ` 257` ``` (auto simp: measure_def emeasure_measure_pmf_finite pmf_nonneg) ``` hoelzl@59000 ` 258` ``` finally show ?thesis . ``` hoelzl@59000 ` 259` ```qed ``` hoelzl@59000 ` 260` hoelzl@59000 ` 261` ```lemma integrable_pmf: "integrable (count_space X) (pmf M)" ``` hoelzl@59000 ` 262` ```proof - ``` hoelzl@59000 ` 263` ``` have " (\\<^sup>+ x. pmf M x \count_space X) = (\\<^sup>+ x. pmf M x \count_space (M \ X))" ``` hoelzl@59000 ` 264` ``` by (auto simp add: nn_integral_count_space_indicator set_pmf_iff intro!: nn_integral_cong split: split_indicator) ``` hoelzl@59000 ` 265` ``` then have "integrable (count_space X) (pmf M) = integrable (count_space (M \ X)) (pmf M)" ``` hoelzl@59000 ` 266` ``` by (simp add: integrable_iff_bounded pmf_nonneg) ``` hoelzl@59000 ` 267` ``` then show ?thesis ``` Andreas@59023 ` 268` ``` by (simp add: pmf.rep_eq measure_pmf.integrable_measure disjoint_family_on_def) ``` hoelzl@59000 ` 269` ```qed ``` hoelzl@59000 ` 270` hoelzl@59000 ` 271` ```lemma integral_pmf: "(\x. pmf M x \count_space X) = measure M X" ``` hoelzl@59000 ` 272` ```proof - ``` hoelzl@59000 ` 273` ``` have "(\x. pmf M x \count_space X) = (\\<^sup>+x. pmf M x \count_space X)" ``` hoelzl@59000 ` 274` ``` by (simp add: pmf_nonneg integrable_pmf nn_integral_eq_integral) ``` hoelzl@59000 ` 275` ``` also have "\ = (\\<^sup>+x. emeasure M {x} \count_space (X \ M))" ``` hoelzl@59000 ` 276` ``` by (auto intro!: nn_integral_cong_AE split: split_indicator ``` hoelzl@59000 ` 277` ``` simp: pmf.rep_eq measure_pmf.emeasure_eq_measure nn_integral_count_space_indicator ``` hoelzl@59000 ` 278` ``` AE_count_space set_pmf_iff) ``` hoelzl@59000 ` 279` ``` also have "\ = emeasure M (X \ M)" ``` hoelzl@59000 ` 280` ``` by (rule emeasure_countable_singleton[symmetric]) (auto intro: countable_set_pmf) ``` hoelzl@59000 ` 281` ``` also have "\ = emeasure M X" ``` hoelzl@59000 ` 282` ``` by (auto intro!: emeasure_eq_AE simp: AE_measure_pmf_iff) ``` hoelzl@59000 ` 283` ``` finally show ?thesis ``` hoelzl@62975 ` 284` ``` by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg integral_nonneg pmf_nonneg) ``` hoelzl@59000 ` 285` ```qed ``` hoelzl@59000 ` 286` hoelzl@59000 ` 287` ```lemma integral_pmf_restrict: ``` hoelzl@59000 ` 288` ``` "(f::'a \ 'b::{banach, second_countable_topology}) \ borel_measurable (count_space UNIV) \ ``` hoelzl@59000 ` 289` ``` (\x. f x \measure_pmf M) = (\x. f x \restrict_space M M)" ``` hoelzl@59000 ` 290` ``` by (auto intro!: integral_cong_AE simp add: integral_restrict_space AE_measure_pmf_iff) ``` hoelzl@59000 ` 291` hoelzl@58587 ` 292` ```lemma emeasure_pmf: "emeasure (M::'a pmf) M = 1" ``` hoelzl@58587 ` 293` ```proof - ``` hoelzl@58587 ` 294` ``` have "emeasure (M::'a pmf) M = emeasure (M::'a pmf) (space M)" ``` hoelzl@58587 ` 295` ``` by (intro emeasure_eq_AE) (simp_all add: AE_measure_pmf) ``` hoelzl@58587 ` 296` ``` then show ?thesis ``` hoelzl@58587 ` 297` ``` using measure_pmf.emeasure_space_1 by simp ``` hoelzl@58587 ` 298` ```qed ``` hoelzl@58587 ` 299` Andreas@59490 ` 300` ```lemma emeasure_pmf_UNIV [simp]: "emeasure (measure_pmf M) UNIV = 1" ``` Andreas@59490 ` 301` ```using measure_pmf.emeasure_space_1[of M] by simp ``` Andreas@59490 ` 302` Andreas@59023 ` 303` ```lemma in_null_sets_measure_pmfI: ``` Andreas@59023 ` 304` ``` "A \ set_pmf p = {} \ A \ null_sets (measure_pmf p)" ``` Andreas@59023 ` 305` ```using emeasure_eq_0_AE[where ?P="\x. x \ A" and M="measure_pmf p"] ``` Andreas@59023 ` 306` ```by(auto simp add: null_sets_def AE_measure_pmf_iff) ``` Andreas@59023 ` 307` hoelzl@59664 ` 308` ```lemma measure_subprob: "measure_pmf M \ space (subprob_algebra (count_space UNIV))" ``` hoelzl@59664 ` 309` ``` by (simp add: space_subprob_algebra subprob_space_measure_pmf) ``` hoelzl@59664 ` 310` hoelzl@59664 ` 311` ```subsection \ Monad Interpretation \ ``` hoelzl@59664 ` 312` hoelzl@59664 ` 313` ```lemma measurable_measure_pmf[measurable]: ``` hoelzl@59664 ` 314` ``` "(\x. measure_pmf (M x)) \ measurable (count_space UNIV) (subprob_algebra (count_space UNIV))" ``` hoelzl@59664 ` 315` ``` by (auto simp: space_subprob_algebra intro!: prob_space_imp_subprob_space) unfold_locales ``` hoelzl@59664 ` 316` hoelzl@59664 ` 317` ```lemma bind_measure_pmf_cong: ``` hoelzl@59664 ` 318` ``` assumes "\x. A x \ space (subprob_algebra N)" "\x. B x \ space (subprob_algebra N)" ``` hoelzl@59664 ` 319` ``` assumes "\i. i \ set_pmf x \ A i = B i" ``` hoelzl@59664 ` 320` ``` shows "bind (measure_pmf x) A = bind (measure_pmf x) B" ``` hoelzl@59664 ` 321` ```proof (rule measure_eqI) ``` wenzelm@62026 ` 322` ``` show "sets (measure_pmf x \ A) = sets (measure_pmf x \ B)" ``` hoelzl@59664 ` 323` ``` using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra) ``` hoelzl@59664 ` 324` ```next ``` wenzelm@62026 ` 325` ``` fix X assume "X \ sets (measure_pmf x \ A)" ``` hoelzl@59664 ` 326` ``` then have X: "X \ sets N" ``` hoelzl@59664 ` 327` ``` using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra) ``` wenzelm@62026 ` 328` ``` show "emeasure (measure_pmf x \ A) X = emeasure (measure_pmf x \ B) X" ``` hoelzl@59664 ` 329` ``` using assms ``` hoelzl@59664 ` 330` ``` by (subst (1 2) emeasure_bind[where N=N, OF _ _ X]) ``` hoelzl@59664 ` 331` ``` (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff) ``` hoelzl@59664 ` 332` ```qed ``` hoelzl@59664 ` 333` hoelzl@59664 ` 334` ```lift_definition bind_pmf :: "'a pmf \ ('a \ 'b pmf ) \ 'b pmf" is bind ``` hoelzl@59664 ` 335` ```proof (clarify, intro conjI) ``` hoelzl@59664 ` 336` ``` fix f :: "'a measure" and g :: "'a \ 'b measure" ``` hoelzl@59664 ` 337` ``` assume "prob_space f" ``` hoelzl@59664 ` 338` ``` then interpret f: prob_space f . ``` hoelzl@59664 ` 339` ``` assume "sets f = UNIV" and ae_f: "AE x in f. measure f {x} \ 0" ``` hoelzl@59664 ` 340` ``` then have s_f[simp]: "sets f = sets (count_space UNIV)" ``` hoelzl@59664 ` 341` ``` by simp ``` hoelzl@59664 ` 342` ``` assume g: "\x. prob_space (g x) \ sets (g x) = UNIV \ (AE y in g x. measure (g x) {y} \ 0)" ``` hoelzl@59664 ` 343` ``` then have g: "\x. prob_space (g x)" and s_g[simp]: "\x. sets (g x) = sets (count_space UNIV)" ``` hoelzl@59664 ` 344` ``` and ae_g: "\x. AE y in g x. measure (g x) {y} \ 0" ``` hoelzl@59664 ` 345` ``` by auto ``` hoelzl@59664 ` 346` hoelzl@59664 ` 347` ``` have [measurable]: "g \ measurable f (subprob_algebra (count_space UNIV))" ``` hoelzl@59664 ` 348` ``` by (auto simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space g) ``` lp15@59667 ` 349` wenzelm@62026 ` 350` ``` show "prob_space (f \ g)" ``` hoelzl@59664 ` 351` ``` using g by (intro f.prob_space_bind[where S="count_space UNIV"]) auto ``` wenzelm@62026 ` 352` ``` then interpret fg: prob_space "f \ g" . ``` wenzelm@62026 ` 353` ``` show [simp]: "sets (f \ g) = UNIV" ``` hoelzl@59664 ` 354` ``` using sets_eq_imp_space_eq[OF s_f] ``` hoelzl@59664 ` 355` ``` by (subst sets_bind[where N="count_space UNIV"]) auto ``` wenzelm@62026 ` 356` ``` show "AE x in f \ g. measure (f \ g) {x} \ 0" ``` hoelzl@59664 ` 357` ``` apply (simp add: fg.prob_eq_0 AE_bind[where B="count_space UNIV"]) ``` hoelzl@59664 ` 358` ``` using ae_f ``` hoelzl@59664 ` 359` ``` apply eventually_elim ``` hoelzl@59664 ` 360` ``` using ae_g ``` hoelzl@59664 ` 361` ``` apply eventually_elim ``` hoelzl@59664 ` 362` ``` apply (auto dest: AE_measure_singleton) ``` hoelzl@59664 ` 363` ``` done ``` hoelzl@59664 ` 364` ```qed ``` hoelzl@59664 ` 365` eberlm@63099 ` 366` ```adhoc_overloading Monad_Syntax.bind bind_pmf ``` eberlm@63099 ` 367` hoelzl@62975 ` 368` ```lemma ennreal_pmf_bind: "pmf (bind_pmf N f) i = (\\<^sup>+x. pmf (f x) i \measure_pmf N)" ``` hoelzl@59664 ` 369` ``` unfolding pmf.rep_eq bind_pmf.rep_eq ``` hoelzl@59664 ` 370` ``` by (auto simp: measure_pmf.measure_bind[where N="count_space UNIV"] measure_subprob measure_nonneg ``` hoelzl@59664 ` 371` ``` intro!: nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1]) ``` hoelzl@59664 ` 372` hoelzl@59664 ` 373` ```lemma pmf_bind: "pmf (bind_pmf N f) i = (\x. pmf (f x) i \measure_pmf N)" ``` hoelzl@62975 ` 374` ``` using ennreal_pmf_bind[of N f i] ``` hoelzl@59664 ` 375` ``` by (subst (asm) nn_integral_eq_integral) ``` hoelzl@62975 ` 376` ``` (auto simp: pmf_nonneg pmf_le_1 pmf_nonneg integral_nonneg ``` hoelzl@59664 ` 377` ``` intro!: nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1]) ``` hoelzl@59664 ` 378` hoelzl@59664 ` 379` ```lemma bind_pmf_const[simp]: "bind_pmf M (\x. c) = c" ``` hoelzl@59664 ` 380` ``` by transfer (simp add: bind_const' prob_space_imp_subprob_space) ``` hoelzl@59664 ` 381` hoelzl@59665 ` 382` ```lemma set_bind_pmf[simp]: "set_pmf (bind_pmf M N) = (\M\set_pmf M. set_pmf (N M))" ``` hoelzl@62975 ` 383` ```proof - ``` hoelzl@62975 ` 384` ``` have "set_pmf (bind_pmf M N) = {x. ennreal (pmf (bind_pmf M N) x) \ 0}" ``` hoelzl@62975 ` 385` ``` by (simp add: set_pmf_eq pmf_nonneg) ``` hoelzl@62975 ` 386` ``` also have "\ = (\M\set_pmf M. set_pmf (N M))" ``` hoelzl@62975 ` 387` ``` unfolding ennreal_pmf_bind ``` hoelzl@62975 ` 388` ``` by (subst nn_integral_0_iff_AE) (auto simp: AE_measure_pmf_iff pmf_nonneg set_pmf_eq) ``` hoelzl@62975 ` 389` ``` finally show ?thesis . ``` hoelzl@62975 ` 390` ```qed ``` hoelzl@59664 ` 391` eberlm@63099 ` 392` ```lemma bind_pmf_cong [fundef_cong]: ``` hoelzl@59664 ` 393` ``` assumes "p = q" ``` hoelzl@59664 ` 394` ``` shows "(\x. x \ set_pmf q \ f x = g x) \ bind_pmf p f = bind_pmf q g" ``` wenzelm@61808 ` 395` ``` unfolding \p = q\[symmetric] measure_pmf_inject[symmetric] bind_pmf.rep_eq ``` hoelzl@59664 ` 396` ``` by (auto simp: AE_measure_pmf_iff Pi_iff space_subprob_algebra subprob_space_measure_pmf ``` hoelzl@59664 ` 397` ``` sets_bind[where N="count_space UNIV"] emeasure_bind[where N="count_space UNIV"] ``` hoelzl@59664 ` 398` ``` intro!: nn_integral_cong_AE measure_eqI) ``` hoelzl@59664 ` 399` hoelzl@59664 ` 400` ```lemma bind_pmf_cong_simp: ``` hoelzl@59664 ` 401` ``` "p = q \ (\x. x \ set_pmf q =simp=> f x = g x) \ bind_pmf p f = bind_pmf q g" ``` hoelzl@59664 ` 402` ``` by (simp add: simp_implies_def cong: bind_pmf_cong) ``` hoelzl@59664 ` 403` wenzelm@62026 ` 404` ```lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \ (\x. measure_pmf (f x)))" ``` hoelzl@59664 ` 405` ``` by transfer simp ``` hoelzl@59664 ` 406` hoelzl@59664 ` 407` ```lemma nn_integral_bind_pmf[simp]: "(\\<^sup>+x. f x \bind_pmf M N) = (\\<^sup>+x. \\<^sup>+y. f y \N x \M)" ``` hoelzl@59664 ` 408` ``` using measurable_measure_pmf[of N] ``` hoelzl@59664 ` 409` ``` unfolding measure_pmf_bind ``` hoelzl@59664 ` 410` ``` apply (intro nn_integral_bind[where B="count_space UNIV"]) ``` hoelzl@59664 ` 411` ``` apply auto ``` hoelzl@59664 ` 412` ``` done ``` hoelzl@59664 ` 413` hoelzl@59664 ` 414` ```lemma emeasure_bind_pmf[simp]: "emeasure (bind_pmf M N) X = (\\<^sup>+x. emeasure (N x) X \M)" ``` hoelzl@59664 ` 415` ``` using measurable_measure_pmf[of N] ``` hoelzl@59664 ` 416` ``` unfolding measure_pmf_bind ``` hoelzl@59664 ` 417` ``` by (subst emeasure_bind[where N="count_space UNIV"]) auto ``` lp15@59667 ` 418` hoelzl@59664 ` 419` ```lift_definition return_pmf :: "'a \ 'a pmf" is "return (count_space UNIV)" ``` hoelzl@59664 ` 420` ``` by (auto intro!: prob_space_return simp: AE_return measure_return) ``` hoelzl@59664 ` 421` hoelzl@59664 ` 422` ```lemma bind_return_pmf: "bind_pmf (return_pmf x) f = f x" ``` hoelzl@59664 ` 423` ``` by transfer ``` hoelzl@59664 ` 424` ``` (auto intro!: prob_space_imp_subprob_space bind_return[where N="count_space UNIV"] ``` hoelzl@59664 ` 425` ``` simp: space_subprob_algebra) ``` hoelzl@59664 ` 426` hoelzl@59665 ` 427` ```lemma set_return_pmf[simp]: "set_pmf (return_pmf x) = {x}" ``` hoelzl@59664 ` 428` ``` by transfer (auto simp add: measure_return split: split_indicator) ``` hoelzl@59664 ` 429` hoelzl@59664 ` 430` ```lemma bind_return_pmf': "bind_pmf N return_pmf = N" ``` hoelzl@59664 ` 431` ```proof (transfer, clarify) ``` wenzelm@62026 ` 432` ``` fix N :: "'a measure" assume "sets N = UNIV" then show "N \ return (count_space UNIV) = N" ``` hoelzl@59664 ` 433` ``` by (subst return_sets_cong[where N=N]) (simp_all add: bind_return') ``` hoelzl@59664 ` 434` ```qed ``` hoelzl@59664 ` 435` hoelzl@59664 ` 436` ```lemma bind_assoc_pmf: "bind_pmf (bind_pmf A B) C = bind_pmf A (\x. bind_pmf (B x) C)" ``` hoelzl@59664 ` 437` ``` by transfer ``` hoelzl@59664 ` 438` ``` (auto intro!: bind_assoc[where N="count_space UNIV" and R="count_space UNIV"] ``` hoelzl@59664 ` 439` ``` simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space) ``` hoelzl@59664 ` 440` hoelzl@59664 ` 441` ```definition "map_pmf f M = bind_pmf M (\x. return_pmf (f x))" ``` hoelzl@59664 ` 442` hoelzl@59664 ` 443` ```lemma map_bind_pmf: "map_pmf f (bind_pmf M g) = bind_pmf M (\x. map_pmf f (g x))" ``` hoelzl@59664 ` 444` ``` by (simp add: map_pmf_def bind_assoc_pmf) ``` hoelzl@59664 ` 445` hoelzl@59664 ` 446` ```lemma bind_map_pmf: "bind_pmf (map_pmf f M) g = bind_pmf M (\x. g (f x))" ``` hoelzl@59664 ` 447` ``` by (simp add: map_pmf_def bind_assoc_pmf bind_return_pmf) ``` hoelzl@59664 ` 448` hoelzl@59664 ` 449` ```lemma map_pmf_transfer[transfer_rule]: ``` nipkow@67399 ` 450` ``` "rel_fun (=) (rel_fun cr_pmf cr_pmf) (\f M. distr M (count_space UNIV) f) map_pmf" ``` hoelzl@59664 ` 451` ```proof - ``` nipkow@67399 ` 452` ``` have "rel_fun (=) (rel_fun pmf_as_measure.cr_pmf pmf_as_measure.cr_pmf) ``` wenzelm@62026 ` 453` ``` (\f M. M \ (return (count_space UNIV) o f)) map_pmf" ``` lp15@59667 ` 454` ``` unfolding map_pmf_def[abs_def] comp_def by transfer_prover ``` hoelzl@59664 ` 455` ``` then show ?thesis ``` hoelzl@59664 ` 456` ``` by (force simp: rel_fun_def cr_pmf_def bind_return_distr) ``` hoelzl@59664 ` 457` ```qed ``` hoelzl@59664 ` 458` hoelzl@59664 ` 459` ```lemma map_pmf_rep_eq: ``` hoelzl@59664 ` 460` ``` "measure_pmf (map_pmf f M) = distr (measure_pmf M) (count_space UNIV) f" ``` hoelzl@59664 ` 461` ``` unfolding map_pmf_def bind_pmf.rep_eq comp_def return_pmf.rep_eq ``` hoelzl@59664 ` 462` ``` using bind_return_distr[of M f "count_space UNIV"] by (simp add: comp_def) ``` hoelzl@59664 ` 463` hoelzl@58587 ` 464` ```lemma map_pmf_id[simp]: "map_pmf id = id" ``` hoelzl@58587 ` 465` ``` by (rule, transfer) (auto simp: emeasure_distr measurable_def intro!: measure_eqI) ``` hoelzl@58587 ` 466` hoelzl@59053 ` 467` ```lemma map_pmf_ident[simp]: "map_pmf (\x. x) = (\x. x)" ``` hoelzl@59053 ` 468` ``` using map_pmf_id unfolding id_def . ``` hoelzl@59053 ` 469` hoelzl@58587 ` 470` ```lemma map_pmf_compose: "map_pmf (f \ g) = map_pmf f \ map_pmf g" ``` lp15@59667 ` 471` ``` by (rule, transfer) (simp add: distr_distr[symmetric, where N="count_space UNIV"] measurable_def) ``` hoelzl@58587 ` 472` hoelzl@59000 ` 473` ```lemma map_pmf_comp: "map_pmf f (map_pmf g M) = map_pmf (\x. f (g x)) M" ``` hoelzl@59000 ` 474` ``` using map_pmf_compose[of f g] by (simp add: comp_def) ``` hoelzl@59000 ` 475` hoelzl@59664 ` 476` ```lemma map_pmf_cong: "p = q \ (\x. x \ set_pmf q \ f x = g x) \ map_pmf f p = map_pmf g q" ``` hoelzl@59664 ` 477` ``` unfolding map_pmf_def by (rule bind_pmf_cong) auto ``` hoelzl@59664 ` 478` nipkow@67399 ` 479` ```lemma pmf_set_map: "set_pmf \ map_pmf f = (`) f \ set_pmf" ``` hoelzl@59665 ` 480` ``` by (auto simp add: comp_def fun_eq_iff map_pmf_def) ``` hoelzl@59664 ` 481` hoelzl@59665 ` 482` ```lemma set_map_pmf[simp]: "set_pmf (map_pmf f M) = f`set_pmf M" ``` hoelzl@59664 ` 483` ``` using pmf_set_map[of f] by (auto simp: comp_def fun_eq_iff) ``` hoelzl@58587 ` 484` hoelzl@59002 ` 485` ```lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f -` X)" ``` hoelzl@59664 ` 486` ``` unfolding map_pmf_rep_eq by (subst emeasure_distr) auto ``` hoelzl@59002 ` 487` Andreas@61634 ` 488` ```lemma measure_map_pmf[simp]: "measure (map_pmf f M) X = measure M (f -` X)" ``` hoelzl@62975 ` 489` ```using emeasure_map_pmf[of f M X] by(simp add: measure_pmf.emeasure_eq_measure measure_nonneg) ``` Andreas@61634 ` 490` hoelzl@59002 ` 491` ```lemma nn_integral_map_pmf[simp]: "(\\<^sup>+x. f x \map_pmf g M) = (\\<^sup>+x. f (g x) \M)" ``` hoelzl@59664 ` 492` ``` unfolding map_pmf_rep_eq by (intro nn_integral_distr) auto ``` hoelzl@59002 ` 493` hoelzl@62975 ` 494` ```lemma ennreal_pmf_map: "pmf (map_pmf f p) x = (\\<^sup>+ y. indicator (f -` {x}) y \measure_pmf p)" ``` hoelzl@59664 ` 495` ```proof (transfer fixing: f x) ``` Andreas@59023 ` 496` ``` fix p :: "'b measure" ``` Andreas@59023 ` 497` ``` presume "prob_space p" ``` Andreas@59023 ` 498` ``` then interpret prob_space p . ``` Andreas@59023 ` 499` ``` presume "sets p = UNIV" ``` hoelzl@62975 ` 500` ``` then show "ennreal (measure (distr p (count_space UNIV) f) {x}) = integral\<^sup>N p (indicator (f -` {x}))" ``` hoelzl@62975 ` 501` ``` by(simp add: measure_distr measurable_def emeasure_eq_measure) ``` hoelzl@62975 ` 502` ```qed simp_all ``` hoelzl@62975 ` 503` hoelzl@62975 ` 504` ```lemma pmf_map: "pmf (map_pmf f p) x = measure p (f -` {x})" ``` hoelzl@62975 ` 505` ```proof (transfer fixing: f x) ``` hoelzl@62975 ` 506` ``` fix p :: "'b measure" ``` hoelzl@62975 ` 507` ``` presume "prob_space p" ``` hoelzl@62975 ` 508` ``` then interpret prob_space p . ``` hoelzl@62975 ` 509` ``` presume "sets p = UNIV" ``` hoelzl@62975 ` 510` ``` then show "measure (distr p (count_space UNIV) f) {x} = measure p (f -` {x})" ``` Andreas@59023 ` 511` ``` by(simp add: measure_distr measurable_def emeasure_eq_measure) ``` Andreas@59023 ` 512` ```qed simp_all ``` Andreas@59023 ` 513` Andreas@59023 ` 514` ```lemma nn_integral_pmf: "(\\<^sup>+ x. pmf p x \count_space A) = emeasure (measure_pmf p) A" ``` Andreas@59023 ` 515` ```proof - ``` Andreas@59023 ` 516` ``` have "(\\<^sup>+ x. pmf p x \count_space A) = (\\<^sup>+ x. pmf p x \count_space (A \ set_pmf p))" ``` Andreas@59023 ` 517` ``` by(auto simp add: nn_integral_count_space_indicator indicator_def set_pmf_iff intro: nn_integral_cong) ``` Andreas@59023 ` 518` ``` also have "\ = emeasure (measure_pmf p) (\x\A \ set_pmf p. {x})" ``` Andreas@59023 ` 519` ``` by(subst emeasure_UN_countable)(auto simp add: emeasure_pmf_single disjoint_family_on_def) ``` Andreas@59023 ` 520` ``` also have "\ = emeasure (measure_pmf p) ((\x\A \ set_pmf p. {x}) \ {x. x \ A \ x \ set_pmf p})" ``` Andreas@59023 ` 521` ``` by(rule emeasure_Un_null_set[symmetric])(auto intro: in_null_sets_measure_pmfI) ``` Andreas@59023 ` 522` ``` also have "\ = emeasure (measure_pmf p) A" ``` Andreas@59023 ` 523` ``` by(auto intro: arg_cong2[where f=emeasure]) ``` Andreas@59023 ` 524` ``` finally show ?thesis . ``` Andreas@59023 ` 525` ```qed ``` Andreas@59023 ` 526` hoelzl@62975 ` 527` ```lemma integral_map_pmf[simp]: ``` hoelzl@62975 ` 528` ``` fixes f :: "'a \ 'b::{banach, second_countable_topology}" ``` hoelzl@62975 ` 529` ``` shows "integral\<^sup>L (map_pmf g p) f = integral\<^sup>L p (\x. f (g x))" ``` hoelzl@62975 ` 530` ``` by (simp add: integral_distr map_pmf_rep_eq) ``` hoelzl@62975 ` 531` eberlm@66568 ` 532` ```lemma pmf_abs_summable [intro]: "pmf p abs_summable_on A" ``` lars@67486 ` 533` ``` by (rule abs_summable_on_subset[OF _ subset_UNIV]) ``` eberlm@66568 ` 534` ``` (auto simp: abs_summable_on_def integrable_iff_bounded nn_integral_pmf) ``` eberlm@66568 ` 535` eberlm@66568 ` 536` ```lemma measure_pmf_conv_infsetsum: "measure (measure_pmf p) A = infsetsum (pmf p) A" ``` lars@67486 ` 537` ``` unfolding infsetsum_def by (simp add: integral_eq_nn_integral nn_integral_pmf measure_def) ``` eberlm@66568 ` 538` eberlm@66568 ` 539` ```lemma infsetsum_pmf_eq_1: ``` eberlm@66568 ` 540` ``` assumes "set_pmf p \ A" ``` eberlm@66568 ` 541` ``` shows "infsetsum (pmf p) A = 1" ``` eberlm@66568 ` 542` ```proof - ``` eberlm@66568 ` 543` ``` have "infsetsum (pmf p) A = lebesgue_integral (count_space UNIV) (pmf p)" ``` eberlm@66568 ` 544` ``` using assms unfolding infsetsum_altdef ``` eberlm@66568 ` 545` ``` by (intro Bochner_Integration.integral_cong) (auto simp: indicator_def set_pmf_eq) ``` eberlm@66568 ` 546` ``` also have "\ = 1" ``` eberlm@66568 ` 547` ``` by (subst integral_eq_nn_integral) (auto simp: nn_integral_pmf) ``` eberlm@66568 ` 548` ``` finally show ?thesis . ``` eberlm@66568 ` 549` ```qed ``` eberlm@66568 ` 550` Andreas@60068 ` 551` ```lemma map_return_pmf [simp]: "map_pmf f (return_pmf x) = return_pmf (f x)" ``` hoelzl@59664 ` 552` ``` by transfer (simp add: distr_return) ``` hoelzl@59664 ` 553` hoelzl@59664 ` 554` ```lemma map_pmf_const[simp]: "map_pmf (\_. c) M = return_pmf c" ``` hoelzl@59664 ` 555` ``` by transfer (auto simp: prob_space.distr_const) ``` hoelzl@59664 ` 556` Andreas@60068 ` 557` ```lemma pmf_return [simp]: "pmf (return_pmf x) y = indicator {y} x" ``` hoelzl@59664 ` 558` ``` by transfer (simp add: measure_return) ``` hoelzl@59664 ` 559` hoelzl@59664 ` 560` ```lemma nn_integral_return_pmf[simp]: "0 \ f x \ (\\<^sup>+x. f x \return_pmf x) = f x" ``` hoelzl@59664 ` 561` ``` unfolding return_pmf.rep_eq by (intro nn_integral_return) auto ``` hoelzl@59664 ` 562` hoelzl@59664 ` 563` ```lemma emeasure_return_pmf[simp]: "emeasure (return_pmf x) X = indicator X x" ``` hoelzl@59664 ` 564` ``` unfolding return_pmf.rep_eq by (intro emeasure_return) auto ``` hoelzl@59664 ` 565` eberlm@63099 ` 566` ```lemma measure_return_pmf [simp]: "measure_pmf.prob (return_pmf x) A = indicator A x" ``` eberlm@63099 ` 567` ```proof - ``` hoelzl@63886 ` 568` ``` have "ennreal (measure_pmf.prob (return_pmf x) A) = ``` eberlm@63099 ` 569` ``` emeasure (measure_pmf (return_pmf x)) A" ``` eberlm@63099 ` 570` ``` by (simp add: measure_pmf.emeasure_eq_measure) ``` eberlm@63099 ` 571` ``` also have "\ = ennreal (indicator A x)" by (simp add: ennreal_indicator) ``` eberlm@63099 ` 572` ``` finally show ?thesis by simp ``` eberlm@63099 ` 573` ```qed ``` eberlm@63099 ` 574` hoelzl@59664 ` 575` ```lemma return_pmf_inj[simp]: "return_pmf x = return_pmf y \ x = y" ``` hoelzl@59664 ` 576` ``` by (metis insertI1 set_return_pmf singletonD) ``` hoelzl@59664 ` 577` hoelzl@59665 ` 578` ```lemma map_pmf_eq_return_pmf_iff: ``` hoelzl@59665 ` 579` ``` "map_pmf f p = return_pmf x \ (\y \ set_pmf p. f y = x)" ``` hoelzl@59665 ` 580` ```proof ``` hoelzl@59665 ` 581` ``` assume "map_pmf f p = return_pmf x" ``` hoelzl@59665 ` 582` ``` then have "set_pmf (map_pmf f p) = set_pmf (return_pmf x)" by simp ``` hoelzl@59665 ` 583` ``` then show "\y \ set_pmf p. f y = x" by auto ``` hoelzl@59665 ` 584` ```next ``` hoelzl@59665 ` 585` ``` assume "\y \ set_pmf p. f y = x" ``` hoelzl@59665 ` 586` ``` then show "map_pmf f p = return_pmf x" ``` hoelzl@59665 ` 587` ``` unfolding map_pmf_const[symmetric, of _ p] by (intro map_pmf_cong) auto ``` hoelzl@59665 ` 588` ```qed ``` hoelzl@59665 ` 589` hoelzl@59664 ` 590` ```definition "pair_pmf A B = bind_pmf A (\x. bind_pmf B (\y. return_pmf (x, y)))" ``` hoelzl@59664 ` 591` hoelzl@59664 ` 592` ```lemma pmf_pair: "pmf (pair_pmf M N) (a, b) = pmf M a * pmf N b" ``` hoelzl@59664 ` 593` ``` unfolding pair_pmf_def pmf_bind pmf_return ``` hoelzl@64008 ` 594` ``` apply (subst integral_measure_pmf_real[where A="{b}"]) ``` hoelzl@59664 ` 595` ``` apply (auto simp: indicator_eq_0_iff) ``` hoelzl@64008 ` 596` ``` apply (subst integral_measure_pmf_real[where A="{a}"]) ``` nipkow@64267 ` 597` ``` apply (auto simp: indicator_eq_0_iff sum_nonneg_eq_0_iff pmf_nonneg) ``` hoelzl@59664 ` 598` ``` done ``` hoelzl@59664 ` 599` hoelzl@59665 ` 600` ```lemma set_pair_pmf[simp]: "set_pmf (pair_pmf A B) = set_pmf A \ set_pmf B" ``` hoelzl@59664 ` 601` ``` unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto ``` hoelzl@59664 ` 602` hoelzl@59664 ` 603` ```lemma measure_pmf_in_subprob_space[measurable (raw)]: ``` hoelzl@59664 ` 604` ``` "measure_pmf M \ space (subprob_algebra (count_space UNIV))" ``` hoelzl@59664 ` 605` ``` by (simp add: space_subprob_algebra) intro_locales ``` hoelzl@59664 ` 606` hoelzl@59664 ` 607` ```lemma nn_integral_pair_pmf': "(\\<^sup>+x. f x \pair_pmf A B) = (\\<^sup>+a. \\<^sup>+b. f (a, b) \B \A)" ``` hoelzl@59664 ` 608` ```proof - ``` hoelzl@62975 ` 609` ``` have "(\\<^sup>+x. f x \pair_pmf A B) = (\\<^sup>+x. f x * indicator (A \ B) x \pair_pmf A B)" ``` hoelzl@62975 ` 610` ``` by (auto simp: AE_measure_pmf_iff intro!: nn_integral_cong_AE) ``` hoelzl@62975 ` 611` ``` also have "\ = (\\<^sup>+a. \\<^sup>+b. f (a, b) * indicator (A \ B) (a, b) \B \A)" ``` hoelzl@59664 ` 612` ``` by (simp add: pair_pmf_def) ``` hoelzl@62975 ` 613` ``` also have "\ = (\\<^sup>+a. \\<^sup>+b. f (a, b) \B \A)" ``` hoelzl@59664 ` 614` ``` by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff) ``` hoelzl@62975 ` 615` ``` finally show ?thesis . ``` hoelzl@59664 ` 616` ```qed ``` hoelzl@59664 ` 617` hoelzl@59664 ` 618` ```lemma bind_pair_pmf: ``` hoelzl@59664 ` 619` ``` assumes M[measurable]: "M \ measurable (count_space UNIV \\<^sub>M count_space UNIV) (subprob_algebra N)" ``` wenzelm@62026 ` 620` ``` shows "measure_pmf (pair_pmf A B) \ M = (measure_pmf A \ (\x. measure_pmf B \ (\y. M (x, y))))" ``` hoelzl@59664 ` 621` ``` (is "?L = ?R") ``` hoelzl@59664 ` 622` ```proof (rule measure_eqI) ``` hoelzl@59664 ` 623` ``` have M'[measurable]: "M \ measurable (pair_pmf A B) (subprob_algebra N)" ``` hoelzl@59664 ` 624` ``` using M[THEN measurable_space] by (simp_all add: space_pair_measure) ``` hoelzl@59664 ` 625` hoelzl@59664 ` 626` ``` note measurable_bind[where N="count_space UNIV", measurable] ``` hoelzl@59664 ` 627` ``` note measure_pmf_in_subprob_space[simp] ``` hoelzl@59664 ` 628` hoelzl@59664 ` 629` ``` have sets_eq_N: "sets ?L = N" ``` hoelzl@59664 ` 630` ``` by (subst sets_bind[OF sets_kernel[OF M']]) auto ``` hoelzl@59664 ` 631` ``` show "sets ?L = sets ?R" ``` hoelzl@59664 ` 632` ``` using measurable_space[OF M] ``` hoelzl@59664 ` 633` ``` by (simp add: sets_eq_N space_pair_measure space_subprob_algebra) ``` hoelzl@59664 ` 634` ``` fix X assume "X \ sets ?L" ``` hoelzl@59664 ` 635` ``` then have X[measurable]: "X \ sets N" ``` hoelzl@59664 ` 636` ``` unfolding sets_eq_N . ``` hoelzl@59664 ` 637` ``` then show "emeasure ?L X = emeasure ?R X" ``` hoelzl@59664 ` 638` ``` apply (simp add: emeasure_bind[OF _ M' X]) ``` hoelzl@59664 ` 639` ``` apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A] ``` hoelzl@62975 ` 640` ``` nn_integral_measure_pmf_finite) ``` hoelzl@59664 ` 641` ``` apply (subst emeasure_bind[OF _ _ X]) ``` hoelzl@59664 ` 642` ``` apply measurable ``` hoelzl@59664 ` 643` ``` apply (subst emeasure_bind[OF _ _ X]) ``` hoelzl@59664 ` 644` ``` apply measurable ``` hoelzl@59664 ` 645` ``` done ``` hoelzl@59664 ` 646` ```qed ``` hoelzl@59664 ` 647` hoelzl@59664 ` 648` ```lemma map_fst_pair_pmf: "map_pmf fst (pair_pmf A B) = A" ``` hoelzl@59664 ` 649` ``` by (simp add: pair_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') ``` hoelzl@59664 ` 650` hoelzl@59664 ` 651` ```lemma map_snd_pair_pmf: "map_pmf snd (pair_pmf A B) = B" ``` hoelzl@59664 ` 652` ``` by (simp add: pair_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') ``` hoelzl@59664 ` 653` hoelzl@59664 ` 654` ```lemma nn_integral_pmf': ``` hoelzl@59664 ` 655` ``` "inj_on f A \ (\\<^sup>+x. pmf p (f x) \count_space A) = emeasure p (f ` A)" ``` hoelzl@59664 ` 656` ``` by (subst nn_integral_bij_count_space[where g=f and B="f`A"]) ``` hoelzl@59664 ` 657` ``` (auto simp: bij_betw_def nn_integral_pmf) ``` hoelzl@59664 ` 658` hoelzl@59664 ` 659` ```lemma pmf_le_0_iff[simp]: "pmf M p \ 0 \ pmf M p = 0" ``` hoelzl@62975 ` 660` ``` using pmf_nonneg[of M p] by arith ``` hoelzl@59664 ` 661` hoelzl@59664 ` 662` ```lemma min_pmf_0[simp]: "min (pmf M p) 0 = 0" "min 0 (pmf M p) = 0" ``` hoelzl@62975 ` 663` ``` using pmf_nonneg[of M p] by arith+ ``` hoelzl@59664 ` 664` hoelzl@59664 ` 665` ```lemma pmf_eq_0_set_pmf: "pmf M p = 0 \ p \ set_pmf M" ``` hoelzl@59664 ` 666` ``` unfolding set_pmf_iff by simp ``` hoelzl@59664 ` 667` hoelzl@59664 ` 668` ```lemma pmf_map_inj: "inj_on f (set_pmf M) \ x \ set_pmf M \ pmf (map_pmf f M) (f x) = pmf M x" ``` hoelzl@59664 ` 669` ``` by (auto simp: pmf.rep_eq map_pmf_rep_eq measure_distr AE_measure_pmf_iff inj_onD ``` hoelzl@59664 ` 670` ``` intro!: measure_pmf.finite_measure_eq_AE) ``` hoelzl@59664 ` 671` Andreas@60068 ` 672` ```lemma pmf_map_inj': "inj f \ pmf (map_pmf f M) (f x) = pmf M x" ``` Andreas@60068 ` 673` ```apply(cases "x \ set_pmf M") ``` Andreas@60068 ` 674` ``` apply(simp add: pmf_map_inj[OF subset_inj_on]) ``` Andreas@60068 ` 675` ```apply(simp add: pmf_eq_0_set_pmf[symmetric]) ``` Andreas@60068 ` 676` ```apply(auto simp add: pmf_eq_0_set_pmf dest: injD) ``` Andreas@60068 ` 677` ```done ``` Andreas@60068 ` 678` Andreas@60068 ` 679` ```lemma pmf_map_outside: "x \ f ` set_pmf M \ pmf (map_pmf f M) x = 0" ``` hoelzl@64008 ` 680` ``` unfolding pmf_eq_0_set_pmf by simp ``` hoelzl@64008 ` 681` hoelzl@64008 ` 682` ```lemma measurable_set_pmf[measurable]: "Measurable.pred (count_space UNIV) (\x. x \ set_pmf M)" ``` hoelzl@64008 ` 683` ``` by simp ``` Andreas@60068 ` 684` eberlm@65395 ` 685` hoelzl@59664 ` 686` ```subsection \ PMFs as function \ ``` hoelzl@59000 ` 687` hoelzl@58587 ` 688` ```context ``` hoelzl@58587 ` 689` ``` fixes f :: "'a \ real" ``` hoelzl@58587 ` 690` ``` assumes nonneg: "\x. 0 \ f x" ``` hoelzl@58587 ` 691` ``` assumes prob: "(\\<^sup>+x. f x \count_space UNIV) = 1" ``` hoelzl@58587 ` 692` ```begin ``` hoelzl@58587 ` 693` hoelzl@62975 ` 694` ```lift_definition embed_pmf :: "'a pmf" is "density (count_space UNIV) (ennreal \ f)" ``` hoelzl@58587 ` 695` ```proof (intro conjI) ``` hoelzl@62975 ` 696` ``` have *[simp]: "\x y. ennreal (f y) * indicator {x} y = ennreal (f x) * indicator {x} y" ``` hoelzl@58587 ` 697` ``` by (simp split: split_indicator) ``` hoelzl@62975 ` 698` ``` show "AE x in density (count_space UNIV) (ennreal \ f). ``` hoelzl@62975 ` 699` ``` measure (density (count_space UNIV) (ennreal \ f)) {x} \ 0" ``` hoelzl@59092 ` 700` ``` by (simp add: AE_density nonneg measure_def emeasure_density max_def) ``` hoelzl@62975 ` 701` ``` show "prob_space (density (count_space UNIV) (ennreal \ f))" ``` wenzelm@61169 ` 702` ``` by standard (simp add: emeasure_density prob) ``` hoelzl@58587 ` 703` ```qed simp ``` hoelzl@58587 ` 704` hoelzl@58587 ` 705` ```lemma pmf_embed_pmf: "pmf embed_pmf x = f x" ``` hoelzl@58587 ` 706` ```proof transfer ``` hoelzl@62975 ` 707` ``` have *[simp]: "\x y. ennreal (f y) * indicator {x} y = ennreal (f x) * indicator {x} y" ``` hoelzl@58587 ` 708` ``` by (simp split: split_indicator) ``` hoelzl@62975 ` 709` ``` fix x show "measure (density (count_space UNIV) (ennreal \ f)) {x} = f x" ``` hoelzl@59092 ` 710` ``` by transfer (simp add: measure_def emeasure_density nonneg max_def) ``` hoelzl@58587 ` 711` ```qed ``` hoelzl@58587 ` 712` Andreas@60068 ` 713` ```lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \ 0}" ``` wenzelm@63092 ` 714` ```by(auto simp add: set_pmf_eq pmf_embed_pmf) ``` Andreas@60068 ` 715` hoelzl@58587 ` 716` ```end ``` hoelzl@58587 ` 717` hoelzl@58587 ` 718` ```lemma embed_pmf_transfer: ``` hoelzl@62975 ` 719` ``` "rel_fun (eq_onp (\f. (\x. 0 \ f x) \ (\\<^sup>+x. ennreal (f x) \count_space UNIV) = 1)) pmf_as_measure.cr_pmf (\f. density (count_space UNIV) (ennreal \ f)) embed_pmf" ``` hoelzl@58587 ` 720` ``` by (auto simp: rel_fun_def eq_onp_def embed_pmf.transfer) ``` hoelzl@58587 ` 721` hoelzl@59000 ` 722` ```lemma measure_pmf_eq_density: "measure_pmf p = density (count_space UNIV) (pmf p)" ``` hoelzl@59000 ` 723` ```proof (transfer, elim conjE) ``` hoelzl@59000 ` 724` ``` fix M :: "'a measure" assume [simp]: "sets M = UNIV" and ae: "AE x in M. measure M {x} \ 0" ``` hoelzl@59000 ` 725` ``` assume "prob_space M" then interpret prob_space M . ``` hoelzl@62975 ` 726` ``` show "M = density (count_space UNIV) (\x. ennreal (measure M {x}))" ``` hoelzl@59000 ` 727` ``` proof (rule measure_eqI) ``` hoelzl@59000 ` 728` ``` fix A :: "'a set" ``` hoelzl@62975 ` 729` ``` have "(\\<^sup>+ x. ennreal (measure M {x}) * indicator A x \count_space UNIV) = ``` hoelzl@59000 ` 730` ``` (\\<^sup>+ x. emeasure M {x} * indicator (A \ {x. measure M {x} \ 0}) x \count_space UNIV)" ``` hoelzl@59000 ` 731` ``` by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator) ``` hoelzl@59000 ` 732` ``` also have "\ = (\\<^sup>+ x. emeasure M {x} \count_space (A \ {x. measure M {x} \ 0}))" ``` hoelzl@59000 ` 733` ``` by (subst nn_integral_restrict_space[symmetric]) (auto simp: restrict_count_space) ``` hoelzl@59000 ` 734` ``` also have "\ = emeasure M (\x\(A \ {x. measure M {x} \ 0}). {x})" ``` hoelzl@59000 ` 735` ``` by (intro emeasure_UN_countable[symmetric] countable_Int2 countable_support) ``` hoelzl@59000 ` 736` ``` (auto simp: disjoint_family_on_def) ``` hoelzl@59000 ` 737` ``` also have "\ = emeasure M A" ``` hoelzl@59000 ` 738` ``` using ae by (intro emeasure_eq_AE) auto ``` hoelzl@62975 ` 739` ``` finally show " emeasure M A = emeasure (density (count_space UNIV) (\x. ennreal (measure M {x}))) A" ``` hoelzl@59000 ` 740` ``` using emeasure_space_1 by (simp add: emeasure_density) ``` hoelzl@59000 ` 741` ``` qed simp ``` hoelzl@59000 ` 742` ```qed ``` hoelzl@59000 ` 743` hoelzl@58587 ` 744` ```lemma td_pmf_embed_pmf: ``` hoelzl@62975 ` 745` ``` "type_definition pmf embed_pmf {f::'a \ real. (\x. 0 \ f x) \ (\\<^sup>+x. ennreal (f x) \count_space UNIV) = 1}" ``` hoelzl@58587 ` 746` ``` unfolding type_definition_def ``` hoelzl@58587 ` 747` ```proof safe ``` hoelzl@58587 ` 748` ``` fix p :: "'a pmf" ``` hoelzl@58587 ` 749` ``` have "(\\<^sup>+ x. 1 \measure_pmf p) = 1" ``` hoelzl@58587 ` 750` ``` using measure_pmf.emeasure_space_1[of p] by simp ``` hoelzl@62975 ` 751` ``` then show *: "(\\<^sup>+ x. ennreal (pmf p x) \count_space UNIV) = 1" ``` hoelzl@58587 ` 752` ``` by (simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg del: nn_integral_const) ``` hoelzl@58587 ` 753` hoelzl@58587 ` 754` ``` show "embed_pmf (pmf p) = p" ``` hoelzl@58587 ` 755` ``` by (intro measure_pmf_inject[THEN iffD1]) ``` hoelzl@58587 ` 756` ``` (simp add: * embed_pmf.rep_eq pmf_nonneg measure_pmf_eq_density[of p] comp_def) ``` hoelzl@58587 ` 757` ```next ``` hoelzl@58587 ` 758` ``` fix f :: "'a \ real" assume "\x. 0 \ f x" "(\\<^sup>+x. f x \count_space UNIV) = 1" ``` hoelzl@58587 ` 759` ``` then show "pmf (embed_pmf f) = f" ``` hoelzl@58587 ` 760` ``` by (auto intro!: pmf_embed_pmf) ``` hoelzl@58587 ` 761` ```qed (rule pmf_nonneg) ``` hoelzl@58587 ` 762` hoelzl@58587 ` 763` ```end ``` hoelzl@58587 ` 764` hoelzl@62975 ` 765` ```lemma nn_integral_measure_pmf: "(\\<^sup>+ x. f x \measure_pmf p) = \\<^sup>+ x. ennreal (pmf p x) * f x \count_space UNIV" ``` Andreas@60068 ` 766` ```by(simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg) ``` Andreas@60068 ` 767` hoelzl@64008 ` 768` ```lemma integral_measure_pmf: ``` hoelzl@64008 ` 769` ``` fixes f :: "'a \ 'b::{banach, second_countable_topology}" ``` hoelzl@64008 ` 770` ``` assumes A: "finite A" ``` hoelzl@64008 ` 771` ``` shows "(\a. a \ set_pmf M \ f a \ 0 \ a \ A) \ (LINT x|M. f x) = (\a\A. pmf M a *\<^sub>R f a)" ``` hoelzl@64008 ` 772` ``` unfolding measure_pmf_eq_density ``` hoelzl@64008 ` 773` ``` apply (simp add: integral_density) ``` hoelzl@64008 ` 774` ``` apply (subst lebesgue_integral_count_space_finite_support) ``` nipkow@64267 ` 775` ``` apply (auto intro!: finite_subset[OF _ \finite A\] sum.mono_neutral_left simp: pmf_eq_0_set_pmf) ``` hoelzl@64008 ` 776` ``` done ``` lars@67486 ` 777` eberlm@65395 ` 778` ```lemma expectation_return_pmf [simp]: ``` eberlm@65395 ` 779` ``` fixes f :: "'a \ 'b::{banach, second_countable_topology}" ``` eberlm@65395 ` 780` ``` shows "measure_pmf.expectation (return_pmf x) f = f x" ``` eberlm@65395 ` 781` ``` by (subst integral_measure_pmf[of "{x}"]) simp_all ``` eberlm@65395 ` 782` eberlm@65395 ` 783` ```lemma pmf_expectation_bind: ``` eberlm@65395 ` 784` ``` fixes p :: "'a pmf" and f :: "'a \ 'b pmf" ``` eberlm@65395 ` 785` ``` and h :: "'b \ 'c::{banach, second_countable_topology}" ``` eberlm@65395 ` 786` ``` assumes "finite A" "\x. x \ A \ finite (set_pmf (f x))" "set_pmf p \ A" ``` eberlm@65395 ` 787` ``` shows "measure_pmf.expectation (p \ f) h = ``` eberlm@65395 ` 788` ``` (\a\A. pmf p a *\<^sub>R measure_pmf.expectation (f a) h)" ``` eberlm@65395 ` 789` ```proof - ``` eberlm@65395 ` 790` ``` have "measure_pmf.expectation (p \ f) h = (\a\(\x\A. set_pmf (f x)). pmf (p \ f) a *\<^sub>R h a)" ``` eberlm@65395 ` 791` ``` using assms by (intro integral_measure_pmf) auto ``` eberlm@65395 ` 792` ``` also have "\ = (\x\(\x\A. set_pmf (f x)). (\a\A. (pmf p a * pmf (f a) x) *\<^sub>R h x))" ``` eberlm@65395 ` 793` ``` proof (intro sum.cong refl, goal_cases) ``` eberlm@65395 ` 794` ``` case (1 x) ``` eberlm@65395 ` 795` ``` thus ?case ``` lars@67486 ` 796` ``` by (subst pmf_bind, subst integral_measure_pmf[of A]) ``` eberlm@65395 ` 797` ``` (insert assms, auto simp: scaleR_sum_left) ``` eberlm@65395 ` 798` ``` qed ``` eberlm@65395 ` 799` ``` also have "\ = (\j\A. pmf p j *\<^sub>R (\i\(\x\A. set_pmf (f x)). pmf (f j) i *\<^sub>R h i))" ``` haftmann@66804 ` 800` ``` by (subst sum.swap) (simp add: scaleR_sum_right) ``` eberlm@65395 ` 801` ``` also have "\ = (\j\A. pmf p j *\<^sub>R measure_pmf.expectation (f j) h)" ``` eberlm@65395 ` 802` ``` proof (intro sum.cong refl, goal_cases) ``` eberlm@65395 ` 803` ``` case (1 x) ``` eberlm@65395 ` 804` ``` thus ?case ``` lars@67486 ` 805` ``` by (subst integral_measure_pmf[of "(\x\A. set_pmf (f x))"]) ``` eberlm@65395 ` 806` ``` (insert assms, auto simp: scaleR_sum_left) ``` eberlm@65395 ` 807` ``` qed ``` eberlm@65395 ` 808` ``` finally show ?thesis . ``` eberlm@65395 ` 809` ```qed ``` hoelzl@64008 ` 810` wenzelm@67226 ` 811` ```lemma continuous_on_LINT_pmf: \ \This is dominated convergence!?\ ``` hoelzl@64008 ` 812` ``` fixes f :: "'i \ 'a::topological_space \ 'b::{banach, second_countable_topology}" ``` hoelzl@64008 ` 813` ``` assumes f: "\i. i \ set_pmf M \ continuous_on A (f i)" ``` hoelzl@64008 ` 814` ``` and bnd: "\a i. a \ A \ i \ set_pmf M \ norm (f i a) \ B" ``` hoelzl@64008 ` 815` ``` shows "continuous_on A (\a. LINT i|M. f i a)" ``` hoelzl@64008 ` 816` ```proof cases ``` hoelzl@64008 ` 817` ``` assume "finite M" with f show ?thesis ``` hoelzl@64008 ` 818` ``` using integral_measure_pmf[OF \finite M\] ``` hoelzl@64008 ` 819` ``` by (subst integral_measure_pmf[OF \finite M\]) ``` nipkow@64267 ` 820` ``` (auto intro!: continuous_on_sum continuous_on_scaleR continuous_on_const) ``` hoelzl@64008 ` 821` ```next ``` hoelzl@64008 ` 822` ``` assume "infinite M" ``` hoelzl@64008 ` 823` ``` let ?f = "\i x. pmf (map_pmf (to_nat_on M) M) i *\<^sub>R f (from_nat_into M i) x" ``` hoelzl@64008 ` 824` hoelzl@64008 ` 825` ``` show ?thesis ``` hoelzl@64008 ` 826` ``` proof (rule uniform_limit_theorem) ``` hoelzl@64008 ` 827` ``` show "\\<^sub>F n in sequentially. continuous_on A (\a. \in a. \ia. LINT i|M. f i a) sequentially" ``` hoelzl@64008 ` 831` ``` proof (subst uniform_limit_cong[where g="\n a. \i A" ``` hoelzl@64008 ` 833` ``` have 1: "(LINT i|M. f i a) = (LINT i|map_pmf (to_nat_on M) M. f (from_nat_into M i) a)" ``` hoelzl@64008 ` 834` ``` by (auto intro!: integral_cong_AE AE_pmfI) ``` hoelzl@64008 ` 835` ``` have 2: "\ = (LINT i|count_space UNIV. pmf (map_pmf (to_nat_on M) M) i *\<^sub>R f (from_nat_into M i) a)" ``` hoelzl@64008 ` 836` ``` by (simp add: measure_pmf_eq_density integral_density) ``` hoelzl@64008 ` 837` ``` have "(\n. ?f n a) sums (LINT i|M. f i a)" ``` hoelzl@64008 ` 838` ``` unfolding 1 2 ``` hoelzl@64008 ` 839` ``` proof (intro sums_integral_count_space_nat) ``` hoelzl@64008 ` 840` ``` have A: "integrable M (\i. f i a)" ``` hoelzl@64008 ` 841` ``` using \a\A\ by (auto intro!: measure_pmf.integrable_const_bound AE_pmfI bnd) ``` hoelzl@64008 ` 842` ``` have "integrable (map_pmf (to_nat_on M) M) (\i. f (from_nat_into M i) a)" ``` hoelzl@64008 ` 843` ``` by (auto simp add: map_pmf_rep_eq integrable_distr_eq intro!: AE_pmfI integrable_cong_AE_imp[OF A]) ``` hoelzl@64008 ` 844` ``` then show "integrable (count_space UNIV) (\n. ?f n a)" ``` hoelzl@64008 ` 845` ``` by (simp add: measure_pmf_eq_density integrable_density) ``` hoelzl@64008 ` 846` ``` qed ``` hoelzl@64008 ` 847` ``` then show "(LINT i|M. f i a) = (\ n. ?f n a)" ``` hoelzl@64008 ` 848` ``` by (simp add: sums_unique) ``` hoelzl@64008 ` 849` ``` next ``` hoelzl@64008 ` 850` ``` show "uniform_limit A (\n a. \ia. (\ n. ?f n a)) sequentially" ``` hoelzl@64008 ` 851` ``` proof (rule weierstrass_m_test) ``` hoelzl@64008 ` 852` ``` fix n a assume "a\A" ``` hoelzl@64008 ` 853` ``` then show "norm (?f n a) \ pmf (map_pmf (to_nat_on M) M) n * B" ``` hoelzl@64008 ` 854` ``` using bnd by (auto intro!: mult_mono simp: from_nat_into set_pmf_not_empty) ``` hoelzl@64008 ` 855` ``` next ``` hoelzl@64008 ` 856` ``` have "integrable (map_pmf (to_nat_on M) M) (\n. B)" ``` hoelzl@64008 ` 857` ``` by auto ``` hoelzl@64008 ` 858` ``` then show "summable (\n. pmf (map_pmf (to_nat_on (set_pmf M)) M) n * B)" ``` hoelzl@64008 ` 859` ``` by (simp add: measure_pmf_eq_density integrable_density integrable_count_space_nat_iff summable_rabs_cancel) ``` hoelzl@64008 ` 860` ``` qed ``` hoelzl@64008 ` 861` ``` qed simp ``` hoelzl@64008 ` 862` ``` qed simp ``` hoelzl@64008 ` 863` ```qed ``` hoelzl@64008 ` 864` hoelzl@64008 ` 865` ```lemma continuous_on_LBINT: ``` hoelzl@64008 ` 866` ``` fixes f :: "real \ real" ``` hoelzl@64008 ` 867` ``` assumes f: "\b. a \ b \ set_integrable lborel {a..b} f" ``` hoelzl@64008 ` 868` ``` shows "continuous_on UNIV (\b. LBINT x:{a..b}. f x)" ``` hoelzl@64008 ` 869` ```proof (subst set_borel_integral_eq_integral) ``` hoelzl@64008 ` 870` ``` { fix b :: real assume "a \ b" ``` hoelzl@64008 ` 871` ``` from f[OF this] have "continuous_on {a..b} (\b. integral {a..b} f)" ``` lp15@66192 ` 872` ``` by (intro indefinite_integral_continuous_1 set_borel_integral_eq_integral) } ``` hoelzl@64008 ` 873` ``` note * = this ``` hoelzl@64008 ` 874` hoelzl@64008 ` 875` ``` have "continuous_on (\b\{a..}. {a <..< b}) (\b. integral {a..b} f)" ``` hoelzl@64008 ` 876` ``` proof (intro continuous_on_open_UN) ``` hoelzl@64008 ` 877` ``` show "b \ {a..} \ continuous_on {a<..b. integral {a..b} f)" for b ``` hoelzl@64008 ` 878` ``` using *[of b] by (rule continuous_on_subset) auto ``` hoelzl@64008 ` 879` ``` qed simp ``` hoelzl@64008 ` 880` ``` also have "(\b\{a..}. {a <..< b}) = {a <..}" ``` hoelzl@64008 ` 881` ``` by (auto simp: lt_ex gt_ex less_imp_le) (simp add: Bex_def less_imp_le gt_ex cong: rev_conj_cong) ``` hoelzl@64008 ` 882` ``` finally have "continuous_on {a+1 ..} (\b. integral {a..b} f)" ``` hoelzl@64008 ` 883` ``` by (rule continuous_on_subset) auto ``` hoelzl@64008 ` 884` ``` moreover have "continuous_on {a..a+1} (\b. integral {a..b} f)" ``` hoelzl@64008 ` 885` ``` by (rule *) simp ``` hoelzl@64008 ` 886` ``` moreover ``` hoelzl@64008 ` 887` ``` have "x \ a \ {a..x} = (if a = x then {a} else {})" for x ``` hoelzl@64008 ` 888` ``` by auto ``` hoelzl@64008 ` 889` ``` then have "continuous_on {..a} (\b. integral {a..b} f)" ``` hoelzl@64008 ` 890` ``` by (subst continuous_on_cong[OF refl, where g="\x. 0"]) (auto intro!: continuous_on_const) ``` hoelzl@64008 ` 891` ``` ultimately have "continuous_on ({..a} \ {a..a+1} \ {a+1 ..}) (\b. integral {a..b} f)" ``` hoelzl@64008 ` 892` ``` by (intro continuous_on_closed_Un) auto ``` hoelzl@64008 ` 893` ``` also have "{..a} \ {a..a+1} \ {a+1 ..} = UNIV" ``` hoelzl@64008 ` 894` ``` by auto ``` hoelzl@64008 ` 895` ``` finally show "continuous_on UNIV (\b. integral {a..b} f)" ``` hoelzl@64008 ` 896` ``` by auto ``` hoelzl@64008 ` 897` ```next ``` hoelzl@64008 ` 898` ``` show "set_integrable lborel {a..b} f" for b ``` hoelzl@64008 ` 899` ``` using f by (cases "a \ b") auto ``` hoelzl@64008 ` 900` ```qed ``` hoelzl@64008 ` 901` hoelzl@58587 ` 902` ```locale pmf_as_function ``` hoelzl@58587 ` 903` ```begin ``` hoelzl@58587 ` 904` hoelzl@58587 ` 905` ```setup_lifting td_pmf_embed_pmf ``` hoelzl@58587 ` 906` lp15@59667 ` 907` ```lemma set_pmf_transfer[transfer_rule]: ``` hoelzl@58730 ` 908` ``` assumes "bi_total A" ``` lp15@59667 ` 909` ``` shows "rel_fun (pcr_pmf A) (rel_set A) (\f. {x. f x \ 0}) set_pmf" ``` wenzelm@61808 ` 910` ``` using \bi_total A\ ``` hoelzl@58730 ` 911` ``` by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff) ``` hoelzl@58730 ` 912` ``` metis+ ``` hoelzl@58730 ` 913` hoelzl@59000 ` 914` ```end ``` hoelzl@59000 ` 915` hoelzl@59000 ` 916` ```context ``` hoelzl@59000 ` 917` ```begin ``` hoelzl@59000 ` 918` hoelzl@59000 ` 919` ```interpretation pmf_as_function . ``` hoelzl@59000 ` 920` hoelzl@59000 ` 921` ```lemma pmf_eqI: "(\i. pmf M i = pmf N i) \ M = N" ``` hoelzl@59000 ` 922` ``` by transfer auto ``` hoelzl@59000 ` 923` hoelzl@59000 ` 924` ```lemma pmf_eq_iff: "M = N \ (\i. pmf M i = pmf N i)" ``` hoelzl@59000 ` 925` ``` by (auto intro: pmf_eqI) ``` hoelzl@59000 ` 926` eberlm@63099 ` 927` ```lemma pmf_neq_exists_less: ``` eberlm@63099 ` 928` ``` assumes "M \ N" ``` eberlm@63099 ` 929` ``` shows "\x. pmf M x < pmf N x" ``` eberlm@63099 ` 930` ```proof (rule ccontr) ``` eberlm@63099 ` 931` ``` assume "\(\x. pmf M x < pmf N x)" ``` eberlm@63099 ` 932` ``` hence ge: "pmf M x \ pmf N x" for x by (auto simp: not_less) ``` eberlm@63099 ` 933` ``` from assms obtain x where "pmf M x \ pmf N x" by (auto simp: pmf_eq_iff) ``` eberlm@63099 ` 934` ``` with ge[of x] have gt: "pmf M x > pmf N x" by simp ``` eberlm@63099 ` 935` ``` have "1 = measure (measure_pmf M) UNIV" by simp ``` eberlm@63099 ` 936` ``` also have "\ = measure (measure_pmf N) {x} + measure (measure_pmf N) (UNIV - {x})" ``` eberlm@63099 ` 937` ``` by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all ``` hoelzl@63886 ` 938` ``` also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}" ``` eberlm@63099 ` 939` ``` by (simp add: measure_pmf_single) ``` eberlm@63099 ` 940` ``` also have "measure (measure_pmf N) (UNIV - {x}) \ measure (measure_pmf M) (UNIV - {x})" ``` hoelzl@63886 ` 941` ``` by (subst (1 2) integral_pmf [symmetric]) ``` eberlm@63099 ` 942` ``` (intro integral_mono integrable_pmf, simp_all add: ge) ``` eberlm@63099 ` 943` ``` also have "measure (measure_pmf M) {x} + \ = 1" ``` eberlm@63099 ` 944` ``` by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all ``` eberlm@63099 ` 945` ``` finally show False by simp_all ``` eberlm@63099 ` 946` ```qed ``` eberlm@63099 ` 947` hoelzl@59664 ` 948` ```lemma bind_commute_pmf: "bind_pmf A (\x. bind_pmf B (C x)) = bind_pmf B (\y. bind_pmf A (\x. C x y))" ``` hoelzl@59664 ` 949` ``` unfolding pmf_eq_iff pmf_bind ``` hoelzl@59664 ` 950` ```proof ``` hoelzl@59664 ` 951` ``` fix i ``` hoelzl@59664 ` 952` ``` interpret B: prob_space "restrict_space B B" ``` hoelzl@59664 ` 953` ``` by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) ``` hoelzl@59664 ` 954` ``` (auto simp: AE_measure_pmf_iff) ``` hoelzl@59664 ` 955` ``` interpret A: prob_space "restrict_space A A" ``` hoelzl@59664 ` 956` ``` by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) ``` hoelzl@59664 ` 957` ``` (auto simp: AE_measure_pmf_iff) ``` hoelzl@59664 ` 958` hoelzl@59664 ` 959` ``` interpret AB: pair_prob_space "restrict_space A A" "restrict_space B B" ``` hoelzl@59664 ` 960` ``` by unfold_locales ``` hoelzl@59664 ` 961` hoelzl@59664 ` 962` ``` have "(\ x. \ y. pmf (C x y) i \B \A) = (\ x. (\ y. pmf (C x y) i \restrict_space B B) \A)" ``` hoelzl@63886 ` 963` ``` by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict) ``` hoelzl@59664 ` 964` ``` also have "\ = (\ x. (\ y. pmf (C x y) i \restrict_space B B) \restrict_space A A)" ``` hoelzl@59664 ` 965` ``` by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2 ``` hoelzl@59664 ` 966` ``` countable_set_pmf borel_measurable_count_space) ``` hoelzl@59664 ` 967` ``` also have "\ = (\ y. \ x. pmf (C x y) i \restrict_space A A \restrict_space B B)" ``` hoelzl@59664 ` 968` ``` by (rule AB.Fubini_integral[symmetric]) ``` hoelzl@59664 ` 969` ``` (auto intro!: AB.integrable_const_bound[where B=1] measurable_pair_restrict_pmf2 ``` hoelzl@59664 ` 970` ``` simp: pmf_nonneg pmf_le_1 measurable_restrict_space1) ``` hoelzl@59664 ` 971` ``` also have "\ = (\ y. \ x. pmf (C x y) i \restrict_space A A \B)" ``` hoelzl@59664 ` 972` ``` by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2 ``` hoelzl@59664 ` 973` ``` countable_set_pmf borel_measurable_count_space) ``` hoelzl@59664 ` 974` ``` also have "\ = (\ y. \ x. pmf (C x y) i \A \B)" ``` hoelzl@63886 ` 975` ``` by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict[symmetric]) ``` hoelzl@59664 ` 976` ``` finally show "(\ x. \ y. pmf (C x y) i \B \A) = (\ y. \ x. pmf (C x y) i \A \B)" . ``` hoelzl@59664 ` 977` ```qed ``` hoelzl@59664 ` 978` hoelzl@59664 ` 979` ```lemma pair_map_pmf1: "pair_pmf (map_pmf f A) B = map_pmf (apfst f) (pair_pmf A B)" ``` hoelzl@59664 ` 980` ```proof (safe intro!: pmf_eqI) ``` hoelzl@59664 ` 981` ``` fix a :: "'a" and b :: "'b" ``` hoelzl@62975 ` 982` ``` have [simp]: "\c d. indicator (apfst f -` {(a, b)}) (c, d) = indicator (f -` {a}) c * (indicator {b} d::ennreal)" ``` hoelzl@59664 ` 983` ``` by (auto split: split_indicator) ``` hoelzl@59664 ` 984` hoelzl@62975 ` 985` ``` have "ennreal (pmf (pair_pmf (map_pmf f A) B) (a, b)) = ``` hoelzl@62975 ` 986` ``` ennreal (pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b))" ``` hoelzl@62975 ` 987` ``` unfolding pmf_pair ennreal_pmf_map ``` hoelzl@59664 ` 988` ``` by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_multc pmf_nonneg ``` hoelzl@62975 ` 989` ``` emeasure_map_pmf[symmetric] ennreal_mult del: emeasure_map_pmf) ``` hoelzl@59664 ` 990` ``` then show "pmf (pair_pmf (map_pmf f A) B) (a, b) = pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b)" ``` hoelzl@62975 ` 991` ``` by (simp add: pmf_nonneg) ``` hoelzl@59664 ` 992` ```qed ``` hoelzl@59664 ` 993` hoelzl@59664 ` 994` ```lemma pair_map_pmf2: "pair_pmf A (map_pmf f B) = map_pmf (apsnd f) (pair_pmf A B)" ``` hoelzl@59664 ` 995` ```proof (safe intro!: pmf_eqI) ``` hoelzl@59664 ` 996` ``` fix a :: "'a" and b :: "'b" ``` hoelzl@62975 ` 997` ``` have [simp]: "\c d. indicator (apsnd f -` {(a, b)}) (c, d) = indicator {a} c * (indicator (f -` {b}) d::ennreal)" ``` hoelzl@59664 ` 998` ``` by (auto split: split_indicator) ``` hoelzl@59664 ` 999` hoelzl@62975 ` 1000` ``` have "ennreal (pmf (pair_pmf A (map_pmf f B)) (a, b)) = ``` hoelzl@62975 ` 1001` ``` ennreal (pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b))" ``` hoelzl@62975 ` 1002` ``` unfolding pmf_pair ennreal_pmf_map ``` hoelzl@59664 ` 1003` ``` by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_cmult nn_integral_multc pmf_nonneg ``` hoelzl@62975 ` 1004` ``` emeasure_map_pmf[symmetric] ennreal_mult del: emeasure_map_pmf) ``` hoelzl@59664 ` 1005` ``` then show "pmf (pair_pmf A (map_pmf f B)) (a, b) = pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b)" ``` hoelzl@62975 ` 1006` ``` by (simp add: pmf_nonneg) ``` hoelzl@59664 ` 1007` ```qed ``` hoelzl@59664 ` 1008` hoelzl@59664 ` 1009` ```lemma map_pair: "map_pmf (\(a, b). (f a, g b)) (pair_pmf A B) = pair_pmf (map_pmf f A) (map_pmf g B)" ``` hoelzl@59664 ` 1010` ``` by (simp add: pair_map_pmf2 pair_map_pmf1 map_pmf_comp split_beta') ``` hoelzl@59664 ` 1011` hoelzl@59000 ` 1012` ```end ``` hoelzl@59000 ` 1013` Andreas@61634 ` 1014` ```lemma pair_return_pmf1: "pair_pmf (return_pmf x) y = map_pmf (Pair x) y" ``` Andreas@61634 ` 1015` ```by(simp add: pair_pmf_def bind_return_pmf map_pmf_def) ``` Andreas@61634 ` 1016` Andreas@61634 ` 1017` ```lemma pair_return_pmf2: "pair_pmf x (return_pmf y) = map_pmf (\x. (x, y)) x" ``` Andreas@61634 ` 1018` ```by(simp add: pair_pmf_def bind_return_pmf map_pmf_def) ``` Andreas@61634 ` 1019` Andreas@61634 ` 1020` ```lemma pair_pair_pmf: "pair_pmf (pair_pmf u v) w = map_pmf (\(x, (y, z)). ((x, y), z)) (pair_pmf u (pair_pmf v w))" ``` Andreas@61634 ` 1021` ```by(simp add: pair_pmf_def bind_return_pmf map_pmf_def bind_assoc_pmf) ``` Andreas@61634 ` 1022` Andreas@61634 ` 1023` ```lemma pair_commute_pmf: "pair_pmf x y = map_pmf (\(x, y). (y, x)) (pair_pmf y x)" ``` Andreas@61634 ` 1024` ```unfolding pair_pmf_def by(subst bind_commute_pmf)(simp add: map_pmf_def bind_assoc_pmf bind_return_pmf) ``` Andreas@61634 ` 1025` Andreas@61634 ` 1026` ```lemma set_pmf_subset_singleton: "set_pmf p \ {x} \ p = return_pmf x" ``` Andreas@61634 ` 1027` ```proof(intro iffI pmf_eqI) ``` Andreas@61634 ` 1028` ``` fix i ``` Andreas@61634 ` 1029` ``` assume x: "set_pmf p \ {x}" ``` Andreas@61634 ` 1030` ``` hence *: "set_pmf p = {x}" using set_pmf_not_empty[of p] by auto ``` hoelzl@62975 ` 1031` ``` have "ennreal (pmf p x) = \\<^sup>+ i. indicator {x} i \p" by(simp add: emeasure_pmf_single) ``` Andreas@61634 ` 1032` ``` also have "\ = \\<^sup>+ i. 1 \p" by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * ) ``` Andreas@61634 ` 1033` ``` also have "\ = 1" by simp ``` Andreas@61634 ` 1034` ``` finally show "pmf p i = pmf (return_pmf x) i" using x ``` Andreas@61634 ` 1035` ``` by(auto split: split_indicator simp add: pmf_eq_0_set_pmf) ``` Andreas@61634 ` 1036` ```qed auto ``` Andreas@61634 ` 1037` Andreas@61634 ` 1038` ```lemma bind_eq_return_pmf: ``` Andreas@61634 ` 1039` ``` "bind_pmf p f = return_pmf x \ (\y\set_pmf p. f y = return_pmf x)" ``` Andreas@61634 ` 1040` ``` (is "?lhs \ ?rhs") ``` Andreas@61634 ` 1041` ```proof(intro iffI strip) ``` Andreas@61634 ` 1042` ``` fix y ``` Andreas@61634 ` 1043` ``` assume y: "y \ set_pmf p" ``` Andreas@61634 ` 1044` ``` assume "?lhs" ``` Andreas@61634 ` 1045` ``` hence "set_pmf (bind_pmf p f) = {x}" by simp ``` Andreas@61634 ` 1046` ``` hence "(\y\set_pmf p. set_pmf (f y)) = {x}" by simp ``` Andreas@61634 ` 1047` ``` hence "set_pmf (f y) \ {x}" using y by auto ``` Andreas@61634 ` 1048` ``` thus "f y = return_pmf x" by(simp add: set_pmf_subset_singleton) ``` Andreas@61634 ` 1049` ```next ``` Andreas@61634 ` 1050` ``` assume *: ?rhs ``` Andreas@61634 ` 1051` ``` show ?lhs ``` Andreas@61634 ` 1052` ``` proof(rule pmf_eqI) ``` Andreas@61634 ` 1053` ``` fix i ``` hoelzl@62975 ` 1054` ``` have "ennreal (pmf (bind_pmf p f) i) = \\<^sup>+ y. ennreal (pmf (f y) i) \p" ``` hoelzl@62975 ` 1055` ``` by (simp add: ennreal_pmf_bind) ``` hoelzl@62975 ` 1056` ``` also have "\ = \\<^sup>+ y. ennreal (pmf (return_pmf x) i) \p" ``` Andreas@61634 ` 1057` ``` by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * ) ``` hoelzl@62975 ` 1058` ``` also have "\ = ennreal (pmf (return_pmf x) i)" ``` hoelzl@62975 ` 1059` ``` by simp ``` hoelzl@62975 ` 1060` ``` finally show "pmf (bind_pmf p f) i = pmf (return_pmf x) i" ``` hoelzl@62975 ` 1061` ``` by (simp add: pmf_nonneg) ``` Andreas@61634 ` 1062` ``` qed ``` Andreas@61634 ` 1063` ```qed ``` Andreas@61634 ` 1064` Andreas@61634 ` 1065` ```lemma pmf_False_conv_True: "pmf p False = 1 - pmf p True" ``` Andreas@61634 ` 1066` ```proof - ``` Andreas@61634 ` 1067` ``` have "pmf p False + pmf p True = measure p {False} + measure p {True}" ``` Andreas@61634 ` 1068` ``` by(simp add: measure_pmf_single) ``` Andreas@61634 ` 1069` ``` also have "\ = measure p ({False} \ {True})" ``` Andreas@61634 ` 1070` ``` by(subst measure_pmf.finite_measure_Union) simp_all ``` Andreas@61634 ` 1071` ``` also have "{False} \ {True} = space p" by auto ``` Andreas@61634 ` 1072` ``` finally show ?thesis by simp ``` Andreas@61634 ` 1073` ```qed ``` Andreas@61634 ` 1074` Andreas@61634 ` 1075` ```lemma pmf_True_conv_False: "pmf p True = 1 - pmf p False" ``` Andreas@61634 ` 1076` ```by(simp add: pmf_False_conv_True) ``` Andreas@61634 ` 1077` hoelzl@59664 ` 1078` ```subsection \ Conditional Probabilities \ ``` hoelzl@59664 ` 1079` hoelzl@59670 ` 1080` ```lemma measure_pmf_zero_iff: "measure (measure_pmf p) s = 0 \ set_pmf p \ s = {}" ``` hoelzl@59670 ` 1081` ``` by (subst measure_pmf.prob_eq_0) (auto simp: AE_measure_pmf_iff) ``` hoelzl@59670 ` 1082` hoelzl@59664 ` 1083` ```context ``` hoelzl@59664 ` 1084` ``` fixes p :: "'a pmf" and s :: "'a set" ``` hoelzl@59664 ` 1085` ``` assumes not_empty: "set_pmf p \ s \ {}" ``` hoelzl@59664 ` 1086` ```begin ``` hoelzl@59664 ` 1087` hoelzl@59664 ` 1088` ```interpretation pmf_as_measure . ``` hoelzl@59664 ` 1089` hoelzl@59664 ` 1090` ```lemma emeasure_measure_pmf_not_zero: "emeasure (measure_pmf p) s \ 0" ``` hoelzl@59664 ` 1091` ```proof ``` hoelzl@59664 ` 1092` ``` assume "emeasure (measure_pmf p) s = 0" ``` hoelzl@59664 ` 1093` ``` then have "AE x in measure_pmf p. x \ s" ``` hoelzl@59664 ` 1094` ``` by (rule AE_I[rotated]) auto ``` hoelzl@59664 ` 1095` ``` with not_empty show False ``` hoelzl@59664 ` 1096` ``` by (auto simp: AE_measure_pmf_iff) ``` hoelzl@59664 ` 1097` ```qed ``` hoelzl@59664 ` 1098` hoelzl@59664 ` 1099` ```lemma measure_measure_pmf_not_zero: "measure (measure_pmf p) s \ 0" ``` hoelzl@62975 ` 1100` ``` using emeasure_measure_pmf_not_zero by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg) ``` hoelzl@59664 ` 1101` hoelzl@59664 ` 1102` ```lift_definition cond_pmf :: "'a pmf" is ``` hoelzl@59664 ` 1103` ``` "uniform_measure (measure_pmf p) s" ``` hoelzl@59664 ` 1104` ```proof (intro conjI) ``` hoelzl@59664 ` 1105` ``` show "prob_space (uniform_measure (measure_pmf p) s)" ``` hoelzl@59664 ` 1106` ``` by (intro prob_space_uniform_measure) (auto simp: emeasure_measure_pmf_not_zero) ``` hoelzl@59664 ` 1107` ``` show "AE x in uniform_measure (measure_pmf p) s. measure (uniform_measure (measure_pmf p) s) {x} \ 0" ``` hoelzl@59664 ` 1108` ``` by (simp add: emeasure_measure_pmf_not_zero measure_measure_pmf_not_zero AE_uniform_measure ``` hoelzl@62975 ` 1109` ``` AE_measure_pmf_iff set_pmf.rep_eq less_top[symmetric]) ``` hoelzl@59664 ` 1110` ```qed simp ``` hoelzl@59664 ` 1111` hoelzl@59664 ` 1112` ```lemma pmf_cond: "pmf cond_pmf x = (if x \ s then pmf p x / measure p s else 0)" ``` hoelzl@59664 ` 1113` ``` by transfer (simp add: emeasure_measure_pmf_not_zero pmf.rep_eq) ``` hoelzl@59664 ` 1114` hoelzl@59665 ` 1115` ```lemma set_cond_pmf[simp]: "set_pmf cond_pmf = set_pmf p \ s" ``` nipkow@62390 ` 1116` ``` by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: if_split_asm) ``` hoelzl@59664 ` 1117` hoelzl@59664 ` 1118` ```end ``` hoelzl@59664 ` 1119` eberlm@63099 ` 1120` ```lemma measure_pmf_posI: "x \ set_pmf p \ x \ A \ measure_pmf.prob p A > 0" ``` eberlm@63099 ` 1121` ``` using measure_measure_pmf_not_zero[of p A] by (subst zero_less_measure_iff) blast ``` eberlm@63099 ` 1122` hoelzl@59664 ` 1123` ```lemma cond_map_pmf: ``` hoelzl@59664 ` 1124` ``` assumes "set_pmf p \ f -` s \ {}" ``` hoelzl@59664 ` 1125` ``` shows "cond_pmf (map_pmf f p) s = map_pmf f (cond_pmf p (f -` s))" ``` hoelzl@59664 ` 1126` ```proof - ``` hoelzl@59664 ` 1127` ``` have *: "set_pmf (map_pmf f p) \ s \ {}" ``` hoelzl@59665 ` 1128` ``` using assms by auto ``` hoelzl@59664 ` 1129` ``` { fix x ``` hoelzl@62975 ` 1130` ``` have "ennreal (pmf (map_pmf f (cond_pmf p (f -` s))) x) = ``` hoelzl@59664 ` 1131` ``` emeasure p (f -` s \ f -` {x}) / emeasure p (f -` s)" ``` hoelzl@62975 ` 1132` ``` unfolding ennreal_pmf_map cond_pmf.rep_eq[OF assms] by (simp add: nn_integral_uniform_measure) ``` hoelzl@59664 ` 1133` ``` also have "f -` s \ f -` {x} = (if x \ s then f -` {x} else {})" ``` hoelzl@59664 ` 1134` ``` by auto ``` hoelzl@59664 ` 1135` ``` also have "emeasure p (if x \ s then f -` {x} else {}) / emeasure p (f -` s) = ``` hoelzl@62975 ` 1136` ``` ennreal (pmf (cond_pmf (map_pmf f p) s) x)" ``` hoelzl@59664 ` 1137` ``` using measure_measure_pmf_not_zero[OF *] ``` hoelzl@62975 ` 1138` ``` by (simp add: pmf_cond[OF *] ennreal_pmf_map measure_pmf.emeasure_eq_measure ``` hoelzl@62975 ` 1139` ``` divide_ennreal pmf_nonneg measure_nonneg zero_less_measure_iff pmf_map) ``` hoelzl@62975 ` 1140` ``` finally have "ennreal (pmf (cond_pmf (map_pmf f p) s) x) = ennreal (pmf (map_pmf f (cond_pmf p (f -` s))) x)" ``` hoelzl@59664 ` 1141` ``` by simp } ``` hoelzl@59664 ` 1142` ``` then show ?thesis ``` hoelzl@62975 ` 1143` ``` by (intro pmf_eqI) (simp add: pmf_nonneg) ``` hoelzl@59664 ` 1144` ```qed ``` hoelzl@59664 ` 1145` hoelzl@59664 ` 1146` ```lemma bind_cond_pmf_cancel: ``` hoelzl@59670 ` 1147` ``` assumes [simp]: "\x. x \ set_pmf p \ set_pmf q \ {y. R x y} \ {}" ``` hoelzl@59670 ` 1148` ``` assumes [simp]: "\y. y \ set_pmf q \ set_pmf p \ {x. R x y} \ {}" ``` hoelzl@59670 ` 1149` ``` assumes [simp]: "\x y. x \ set_pmf p \ y \ set_pmf q \ R x y \ measure q {y. R x y} = measure p {x. R x y}" ``` hoelzl@59670 ` 1150` ``` shows "bind_pmf p (\x. cond_pmf q {y. R x y}) = q" ``` hoelzl@59664 ` 1151` ```proof (rule pmf_eqI) ``` hoelzl@59670 ` 1152` ``` fix i ``` hoelzl@62975 ` 1153` ``` have "ennreal (pmf (bind_pmf p (\x. cond_pmf q {y. R x y})) i) = ``` hoelzl@62975 ` 1154` ``` (\\<^sup>+x. ennreal (pmf q i / measure p {x. R x i}) * ennreal (indicator {x. R x i} x) \p)" ``` hoelzl@62975 ` 1155` ``` by (auto simp add: ennreal_pmf_bind AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf pmf_nonneg measure_nonneg ``` hoelzl@62975 ` 1156` ``` intro!: nn_integral_cong_AE) ``` hoelzl@59670 ` 1157` ``` also have "\ = (pmf q i * measure p {x. R x i}) / measure p {x. R x i}" ``` hoelzl@62975 ` 1158` ``` by (simp add: pmf_nonneg measure_nonneg zero_ennreal_def[symmetric] ennreal_indicator ``` hoelzl@62975 ` 1159` ``` nn_integral_cmult measure_pmf.emeasure_eq_measure ennreal_mult[symmetric]) ``` hoelzl@59670 ` 1160` ``` also have "\ = pmf q i" ``` hoelzl@62975 ` 1161` ``` by (cases "pmf q i = 0") ``` hoelzl@62975 ` 1162` ``` (simp_all add: pmf_eq_0_set_pmf measure_measure_pmf_not_zero pmf_nonneg) ``` hoelzl@59670 ` 1163` ``` finally show "pmf (bind_pmf p (\x. cond_pmf q {y. R x y})) i = pmf q i" ``` hoelzl@62975 ` 1164` ``` by (simp add: pmf_nonneg) ``` hoelzl@59664 ` 1165` ```qed ``` hoelzl@59664 ` 1166` hoelzl@59664 ` 1167` ```subsection \ Relator \ ``` hoelzl@59664 ` 1168` hoelzl@59664 ` 1169` ```inductive rel_pmf :: "('a \ 'b \ bool) \ 'a pmf \ 'b pmf \ bool" ``` hoelzl@59664 ` 1170` ```for R p q ``` hoelzl@59664 ` 1171` ```where ``` lp15@59667 ` 1172` ``` "\ \x y. (x, y) \ set_pmf pq \ R x y; ``` hoelzl@59664 ` 1173` ``` map_pmf fst pq = p; map_pmf snd pq = q \ ``` hoelzl@59664 ` 1174` ``` \ rel_pmf R p q" ``` hoelzl@59664 ` 1175` hoelzl@59681 ` 1176` ```lemma rel_pmfI: ``` hoelzl@59681 ` 1177` ``` assumes R: "rel_set R (set_pmf p) (set_pmf q)" ``` hoelzl@59681 ` 1178` ``` assumes eq: "\x y. x \ set_pmf p \ y \ set_pmf q \ R x y \ ``` hoelzl@59681 ` 1179` ``` measure p {x. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 1180` ``` shows "rel_pmf R p q" ``` hoelzl@59681 ` 1181` ```proof ``` hoelzl@59681 ` 1182` ``` let ?pq = "bind_pmf p (\x. bind_pmf (cond_pmf q {y. R x y}) (\y. return_pmf (x, y)))" ``` hoelzl@59681 ` 1183` ``` have "\x. x \ set_pmf p \ set_pmf q \ {y. R x y} \ {}" ``` hoelzl@59681 ` 1184` ``` using R by (auto simp: rel_set_def) ``` hoelzl@59681 ` 1185` ``` then show "\x y. (x, y) \ set_pmf ?pq \ R x y" ``` hoelzl@59681 ` 1186` ``` by auto ``` hoelzl@59681 ` 1187` ``` show "map_pmf fst ?pq = p" ``` Andreas@60068 ` 1188` ``` by (simp add: map_bind_pmf bind_return_pmf') ``` hoelzl@59681 ` 1189` hoelzl@59681 ` 1190` ``` show "map_pmf snd ?pq = q" ``` hoelzl@59681 ` 1191` ``` using R eq ``` Andreas@60068 ` 1192` ``` apply (simp add: bind_cond_pmf_cancel map_bind_pmf bind_return_pmf') ``` hoelzl@59681 ` 1193` ``` apply (rule bind_cond_pmf_cancel) ``` hoelzl@59681 ` 1194` ``` apply (auto simp: rel_set_def) ``` hoelzl@59681 ` 1195` ``` done ``` hoelzl@59681 ` 1196` ```qed ``` hoelzl@59681 ` 1197` hoelzl@59681 ` 1198` ```lemma rel_pmf_imp_rel_set: "rel_pmf R p q \ rel_set R (set_pmf p) (set_pmf q)" ``` hoelzl@59681 ` 1199` ``` by (force simp add: rel_pmf.simps rel_set_def) ``` hoelzl@59681 ` 1200` hoelzl@59681 ` 1201` ```lemma rel_pmfD_measure: ``` hoelzl@59681 ` 1202` ``` assumes rel_R: "rel_pmf R p q" and R: "\a b. R a b \ R a y \ R x b" ``` hoelzl@59681 ` 1203` ``` assumes "x \ set_pmf p" "y \ set_pmf q" ``` hoelzl@59681 ` 1204` ``` shows "measure p {x. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 1205` ```proof - ``` hoelzl@59681 ` 1206` ``` from rel_R obtain pq where pq: "\x y. (x, y) \ set_pmf pq \ R x y" ``` hoelzl@59681 ` 1207` ``` and eq: "p = map_pmf fst pq" "q = map_pmf snd pq" ``` hoelzl@59681 ` 1208` ``` by (auto elim: rel_pmf.cases) ``` hoelzl@59681 ` 1209` ``` have "measure p {x. R x y} = measure pq {x. R (fst x) y}" ``` hoelzl@59681 ` 1210` ``` by (simp add: eq map_pmf_rep_eq measure_distr) ``` hoelzl@59681 ` 1211` ``` also have "\ = measure pq {y. R x (snd y)}" ``` hoelzl@59681 ` 1212` ``` by (intro measure_pmf.finite_measure_eq_AE) ``` hoelzl@59681 ` 1213` ``` (auto simp: AE_measure_pmf_iff R dest!: pq) ``` hoelzl@59681 ` 1214` ``` also have "\ = measure q {y. R x y}" ``` hoelzl@59681 ` 1215` ``` by (simp add: eq map_pmf_rep_eq measure_distr) ``` hoelzl@59681 ` 1216` ``` finally show "measure p {x. R x y} = measure q {y. R x y}" . ``` hoelzl@59681 ` 1217` ```qed ``` hoelzl@59681 ` 1218` Andreas@61634 ` 1219` ```lemma rel_pmf_measureD: ``` Andreas@61634 ` 1220` ``` assumes "rel_pmf R p q" ``` Andreas@61634 ` 1221` ``` shows "measure (measure_pmf p) A \ measure (measure_pmf q) {y. \x\A. R x y}" (is "?lhs \ ?rhs") ``` Andreas@61634 ` 1222` ```using assms ``` Andreas@61634 ` 1223` ```proof cases ``` Andreas@61634 ` 1224` ``` fix pq ``` Andreas@61634 ` 1225` ``` assume R: "\x y. (x, y) \ set_pmf pq \ R x y" ``` Andreas@61634 ` 1226` ``` and p[symmetric]: "map_pmf fst pq = p" ``` Andreas@61634 ` 1227` ``` and q[symmetric]: "map_pmf snd pq = q" ``` Andreas@61634 ` 1228` ``` have "?lhs = measure (measure_pmf pq) (fst -` A)" by(simp add: p) ``` Andreas@61634 ` 1229` ``` also have "\ \ measure (measure_pmf pq) {y. \x\A. R x (snd y)}" ``` Andreas@61634 ` 1230` ``` by(rule measure_pmf.finite_measure_mono_AE)(auto 4 3 simp add: AE_measure_pmf_iff dest: R) ``` Andreas@61634 ` 1231` ``` also have "\ = ?rhs" by(simp add: q) ``` Andreas@61634 ` 1232` ``` finally show ?thesis . ``` Andreas@61634 ` 1233` ```qed ``` Andreas@61634 ` 1234` hoelzl@59681 ` 1235` ```lemma rel_pmf_iff_measure: ``` hoelzl@59681 ` 1236` ``` assumes "symp R" "transp R" ``` hoelzl@59681 ` 1237` ``` shows "rel_pmf R p q \ ``` hoelzl@59681 ` 1238` ``` rel_set R (set_pmf p) (set_pmf q) \ ``` hoelzl@59681 ` 1239` ``` (\x\set_pmf p. \y\set_pmf q. R x y \ measure p {x. R x y} = measure q {y. R x y})" ``` hoelzl@59681 ` 1240` ``` by (safe intro!: rel_pmf_imp_rel_set rel_pmfI) ``` hoelzl@59681 ` 1241` ``` (auto intro!: rel_pmfD_measure dest: sympD[OF \symp R\] transpD[OF \transp R\]) ``` hoelzl@59681 ` 1242` hoelzl@59681 ` 1243` ```lemma quotient_rel_set_disjoint: ``` hoelzl@59681 ` 1244` ``` "equivp R \ C \ UNIV // {(x, y). R x y} \ rel_set R A B \ A \ C = {} \ B \ C = {}" ``` lp15@61609 ` 1245` ``` using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C] ``` hoelzl@59681 ` 1246` ``` by (auto 0 0 simp: equivp_equiv rel_set_def set_eq_iff elim: equivpE) ``` hoelzl@59681 ` 1247` ``` (blast dest: equivp_symp)+ ``` hoelzl@59681 ` 1248` hoelzl@59681 ` 1249` ```lemma quotientD: "equiv X R \ A \ X // R \ x \ A \ A = R `` {x}" ``` hoelzl@59681 ` 1250` ``` by (metis Image_singleton_iff equiv_class_eq_iff quotientE) ``` hoelzl@59681 ` 1251` hoelzl@59681 ` 1252` ```lemma rel_pmf_iff_equivp: ``` hoelzl@59681 ` 1253` ``` assumes "equivp R" ``` hoelzl@59681 ` 1254` ``` shows "rel_pmf R p q \ (\C\UNIV // {(x, y). R x y}. measure p C = measure q C)" ``` hoelzl@59681 ` 1255` ``` (is "_ \ (\C\_//?R. _)") ``` hoelzl@59681 ` 1256` ```proof (subst rel_pmf_iff_measure, safe) ``` hoelzl@59681 ` 1257` ``` show "symp R" "transp R" ``` hoelzl@59681 ` 1258` ``` using assms by (auto simp: equivp_reflp_symp_transp) ``` hoelzl@59681 ` 1259` ```next ``` hoelzl@59681 ` 1260` ``` fix C assume C: "C \ UNIV // ?R" and R: "rel_set R (set_pmf p) (set_pmf q)" ``` hoelzl@59681 ` 1261` ``` assume eq: "\x\set_pmf p. \y\set_pmf q. R x y \ measure p {x. R x y} = measure q {y. R x y}" ``` lp15@61609 ` 1262` hoelzl@59681 ` 1263` ``` show "measure p C = measure q C" ``` wenzelm@63540 ` 1264` ``` proof (cases "p \ C = {}") ``` wenzelm@63540 ` 1265` ``` case True ``` wenzelm@63540 ` 1266` ``` then have "q \ C = {}" ``` hoelzl@59681 ` 1267` ``` using quotient_rel_set_disjoint[OF assms C R] by simp ``` wenzelm@63540 ` 1268` ``` with True show ?thesis ``` hoelzl@59681 ` 1269` ``` unfolding measure_pmf_zero_iff[symmetric] by simp ``` hoelzl@59681 ` 1270` ``` next ``` wenzelm@63540 ` 1271` ``` case False ``` wenzelm@63540 ` 1272` ``` then have "q \ C \ {}" ``` hoelzl@59681 ` 1273` ``` using quotient_rel_set_disjoint[OF assms C R] by simp ``` wenzelm@63540 ` 1274` ``` with False obtain x y where in_set: "x \ set_pmf p" "y \ set_pmf q" and in_C: "x \ C" "y \ C" ``` hoelzl@59681 ` 1275` ``` by auto ``` hoelzl@59681 ` 1276` ``` then have "R x y" ``` hoelzl@59681 ` 1277` ``` using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms ``` hoelzl@59681 ` 1278` ``` by (simp add: equivp_equiv) ``` hoelzl@59681 ` 1279` ``` with in_set eq have "measure p {x. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 1280` ``` by auto ``` hoelzl@59681 ` 1281` ``` moreover have "{y. R x y} = C" ``` wenzelm@61808 ` 1282` ``` using assms \x \ C\ C quotientD[of UNIV ?R C x] by (simp add: equivp_equiv) ``` hoelzl@59681 ` 1283` ``` moreover have "{x. R x y} = C" ``` wenzelm@61808 ` 1284` ``` using assms \y \ C\ C quotientD[of UNIV "?R" C y] sympD[of R] ``` hoelzl@59681 ` 1285` ``` by (auto simp add: equivp_equiv elim: equivpE) ``` hoelzl@59681 ` 1286` ``` ultimately show ?thesis ``` hoelzl@59681 ` 1287` ``` by auto ``` hoelzl@59681 ` 1288` ``` qed ``` hoelzl@59681 ` 1289` ```next ``` hoelzl@59681 ` 1290` ``` assume eq: "\C\UNIV // ?R. measure p C = measure q C" ``` hoelzl@59681 ` 1291` ``` show "rel_set R (set_pmf p) (set_pmf q)" ``` hoelzl@59681 ` 1292` ``` unfolding rel_set_def ``` hoelzl@59681 ` 1293` ``` proof safe ``` hoelzl@59681 ` 1294` ``` fix x assume x: "x \ set_pmf p" ``` hoelzl@59681 ` 1295` ``` have "{y. R x y} \ UNIV // ?R" ``` hoelzl@59681 ` 1296` ``` by (auto simp: quotient_def) ``` hoelzl@59681 ` 1297` ``` with eq have *: "measure q {y. R x y} = measure p {y. R x y}" ``` hoelzl@59681 ` 1298` ``` by auto ``` hoelzl@59681 ` 1299` ``` have "measure q {y. R x y} \ 0" ``` hoelzl@59681 ` 1300` ``` using x assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp) ``` hoelzl@59681 ` 1301` ``` then show "\y\set_pmf q. R x y" ``` hoelzl@59681 ` 1302` ``` unfolding measure_pmf_zero_iff by auto ``` hoelzl@59681 ` 1303` ``` next ``` hoelzl@59681 ` 1304` ``` fix y assume y: "y \ set_pmf q" ``` hoelzl@59681 ` 1305` ``` have "{x. R x y} \ UNIV // ?R" ``` hoelzl@59681 ` 1306` ``` using assms by (auto simp: quotient_def dest: equivp_symp) ``` hoelzl@59681 ` 1307` ``` with eq have *: "measure p {x. R x y} = measure q {x. R x y}" ``` hoelzl@59681 ` 1308` ``` by auto ``` hoelzl@59681 ` 1309` ``` have "measure p {x. R x y} \ 0" ``` hoelzl@59681 ` 1310` ``` using y assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp) ``` hoelzl@59681 ` 1311` ``` then show "\x\set_pmf p. R x y" ``` hoelzl@59681 ` 1312` ``` unfolding measure_pmf_zero_iff by auto ``` hoelzl@59681 ` 1313` ``` qed ``` hoelzl@59681 ` 1314` hoelzl@59681 ` 1315` ``` fix x y assume "x \ set_pmf p" "y \ set_pmf q" "R x y" ``` hoelzl@59681 ` 1316` ``` have "{y. R x y} \ UNIV // ?R" "{x. R x y} = {y. R x y}" ``` wenzelm@61808 ` 1317` ``` using assms \R x y\ by (auto simp: quotient_def dest: equivp_symp equivp_transp) ``` hoelzl@59681 ` 1318` ``` with eq show "measure p {x. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 1319` ``` by auto ``` hoelzl@59681 ` 1320` ```qed ``` hoelzl@59681 ` 1321` hoelzl@59664 ` 1322` ```bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf ``` hoelzl@59664 ` 1323` ```proof - ``` hoelzl@59664 ` 1324` ``` show "map_pmf id = id" by (rule map_pmf_id) ``` lp15@59667 ` 1325` ``` show "\f g. map_pmf (f \ g) = map_pmf f \ map_pmf g" by (rule map_pmf_compose) ``` hoelzl@59664 ` 1326` ``` show "\f g::'a \ 'b. \p. (\x. x \ set_pmf p \ f x = g x) \ map_pmf f p = map_pmf g p" ``` hoelzl@59664 ` 1327` ``` by (intro map_pmf_cong refl) ``` hoelzl@59664 ` 1328` nipkow@67399 ` 1329` ``` show "\f::'a \ 'b. set_pmf \ map_pmf f = (`) f \ set_pmf" ``` hoelzl@59664 ` 1330` ``` by (rule pmf_set_map) ``` hoelzl@59664 ` 1331` wenzelm@60595 ` 1332` ``` show "(card_of (set_pmf p), natLeq) \ ordLeq" for p :: "'s pmf" ``` wenzelm@60595 ` 1333` ``` proof - ``` hoelzl@59664 ` 1334` ``` have "(card_of (set_pmf p), card_of (UNIV :: nat set)) \ ordLeq" ``` hoelzl@59664 ` 1335` ``` by (rule card_of_ordLeqI[where f="to_nat_on (set_pmf p)"]) ``` hoelzl@59664 ` 1336` ``` (auto intro: countable_set_pmf) ``` hoelzl@59664 ` 1337` ``` also have "(card_of (UNIV :: nat set), natLeq) \ ordLeq" ``` hoelzl@59664 ` 1338` ``` by (metis Field_natLeq card_of_least natLeq_Well_order) ``` wenzelm@60595 ` 1339` ``` finally show ?thesis . ``` wenzelm@60595 ` 1340` ``` qed ``` hoelzl@59664 ` 1341` traytel@62324 ` 1342` ``` show "\R. rel_pmf R = (\x y. \z. set_pmf z \ {(x, y). R x y} \ ``` traytel@62324 ` 1343` ``` map_pmf fst z = x \ map_pmf snd z = y)" ``` traytel@62324 ` 1344` ``` by (auto simp add: fun_eq_iff rel_pmf.simps) ``` hoelzl@59664 ` 1345` wenzelm@60595 ` 1346` ``` show "rel_pmf R OO rel_pmf S \ rel_pmf (R OO S)" ``` wenzelm@60595 ` 1347` ``` for R :: "'a \ 'b \ bool" and S :: "'b \ 'c \ bool" ``` wenzelm@60595 ` 1348` ``` proof - ``` wenzelm@60595 ` 1349` ``` { fix p q r ``` wenzelm@60595 ` 1350` ``` assume pq: "rel_pmf R p q" ``` wenzelm@60595 ` 1351` ``` and qr:"rel_pmf S q r" ``` wenzelm@60595 ` 1352` ``` from pq obtain pq where pq: "\x y. (x, y) \ set_pmf pq \ R x y" ``` wenzelm@60595 ` 1353` ``` and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto ``` wenzelm@60595 ` 1354` ``` from qr obtain qr where qr: "\y z. (y, z) \ set_pmf qr \ S y z" ``` wenzelm@60595 ` 1355` ``` and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto ``` lp15@61609 ` 1356` wenzelm@63040 ` 1357` ``` define pr where "pr = ``` wenzelm@63040 ` 1358` ``` bind_pmf pq (\xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) ``` wenzelm@63040 ` 1359` ``` (\yz. return_pmf (fst xy, snd yz)))" ``` wenzelm@60595 ` 1360` ``` have pr_welldefined: "\y. y \ q \ qr \ {yz. fst yz = y} \ {}" ``` wenzelm@60595 ` 1361` ``` by (force simp: q') ``` lp15@61609 ` 1362` wenzelm@60595 ` 1363` ``` have "rel_pmf (R OO S) p r" ``` wenzelm@60595 ` 1364` ``` proof (rule rel_pmf.intros) ``` wenzelm@60595 ` 1365` ``` fix x z assume "(x, z) \ pr" ``` wenzelm@60595 ` 1366` ``` then have "\y. (x, y) \ pq \ (y, z) \ qr" ``` wenzelm@60595 ` 1367` ``` by (auto simp: q pr_welldefined pr_def split_beta) ``` wenzelm@60595 ` 1368` ``` with pq qr show "(R OO S) x z" ``` wenzelm@60595 ` 1369` ``` by blast ``` wenzelm@60595 ` 1370` ``` next ``` wenzelm@60595 ` 1371` ``` have "map_pmf snd pr = map_pmf snd (bind_pmf q (\y. cond_pmf qr {yz. fst yz = y}))" ``` wenzelm@60595 ` 1372` ``` by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_pmf_comp) ``` wenzelm@60595 ` 1373` ``` then show "map_pmf snd pr = r" ``` wenzelm@60595 ` 1374` ``` unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute) ``` wenzelm@60595 ` 1375` ``` qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp) ``` wenzelm@60595 ` 1376` ``` } ``` wenzelm@60595 ` 1377` ``` then show ?thesis ``` wenzelm@60595 ` 1378` ``` by(auto simp add: le_fun_def) ``` wenzelm@60595 ` 1379` ``` qed ``` hoelzl@59664 ` 1380` ```qed (fact natLeq_card_order natLeq_cinfinite)+ ``` hoelzl@59664 ` 1381` Andreas@61634 ` 1382` ```lemma map_pmf_idI: "(\x. x \ set_pmf p \ f x = x) \ map_pmf f p = p" ``` Andreas@61634 ` 1383` ```by(simp cong: pmf.map_cong) ``` Andreas@61634 ` 1384` hoelzl@59665 ` 1385` ```lemma rel_pmf_conj[simp]: ``` hoelzl@59665 ` 1386` ``` "rel_pmf (\x y. P \ Q x y) x y \ P \ rel_pmf Q x y" ``` hoelzl@59665 ` 1387` ``` "rel_pmf (\x y. Q x y \ P) x y \ P \ rel_pmf Q x y" ``` hoelzl@59665 ` 1388` ``` using set_pmf_not_empty by (fastforce simp: pmf.in_rel subset_eq)+ ``` hoelzl@59665 ` 1389` hoelzl@59665 ` 1390` ```lemma rel_pmf_top[simp]: "rel_pmf top = top" ``` hoelzl@59665 ` 1391` ``` by (auto simp: pmf.in_rel[abs_def] fun_eq_iff map_fst_pair_pmf map_snd_pair_pmf ``` hoelzl@59665 ` 1392` ``` intro: exI[of _ "pair_pmf x y" for x y]) ``` hoelzl@59665 ` 1393` hoelzl@59664 ` 1394` ```lemma rel_pmf_return_pmf1: "rel_pmf R (return_pmf x) M \ (\a\M. R x a)" ``` hoelzl@59664 ` 1395` ```proof safe ``` hoelzl@59664 ` 1396` ``` fix a assume "a \ M" "rel_pmf R (return_pmf x) M" ``` hoelzl@59664 ` 1397` ``` then obtain pq where *: "\a b. (a, b) \ set_pmf pq \ R a b" ``` hoelzl@59664 ` 1398` ``` and eq: "return_pmf x = map_pmf fst pq" "M = map_pmf snd pq" ``` hoelzl@59664 ` 1399` ``` by (force elim: rel_pmf.cases) ``` hoelzl@59664 ` 1400` ``` moreover have "set_pmf (return_pmf x) = {x}" ``` hoelzl@59665 ` 1401` ``` by simp ``` wenzelm@61808 ` 1402` ``` with \a \ M\ have "(x, a) \ pq" ``` hoelzl@59665 ` 1403` ``` by (force simp: eq) ``` hoelzl@59664 ` 1404` ``` with * show "R x a" ``` hoelzl@59664 ` 1405` ``` by auto ``` hoelzl@59664 ` 1406` ```qed (auto intro!: rel_pmf.intros[where pq="pair_pmf (return_pmf x) M"] ``` hoelzl@59665 ` 1407` ``` simp: map_fst_pair_pmf map_snd_pair_pmf) ``` hoelzl@59664 ` 1408` hoelzl@59664 ` 1409` ```lemma rel_pmf_return_pmf2: "rel_pmf R M (return_pmf x) \ (\a\M. R a x)" ``` hoelzl@59664 ` 1410` ``` by (subst pmf.rel_flip[symmetric]) (simp add: rel_pmf_return_pmf1) ``` hoelzl@59664 ` 1411` hoelzl@59664 ` 1412` ```lemma rel_return_pmf[simp]: "rel_pmf R (return_pmf x1) (return_pmf x2) = R x1 x2" ``` hoelzl@59664 ` 1413` ``` unfolding rel_pmf_return_pmf2 set_return_pmf by simp ``` hoelzl@59664 ` 1414` hoelzl@59664 ` 1415` ```lemma rel_pmf_False[simp]: "rel_pmf (\x y. False) x y = False" ``` hoelzl@59664 ` 1416` ``` unfolding pmf.in_rel fun_eq_iff using set_pmf_not_empty by fastforce ``` hoelzl@59664 ` 1417` hoelzl@59664 ` 1418` ```lemma rel_pmf_rel_prod: ``` hoelzl@59664 ` 1419` ``` "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B') \ rel_pmf R A B \ rel_pmf S A' B'" ``` hoelzl@59664 ` 1420` ```proof safe ``` hoelzl@59664 ` 1421` ``` assume "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')" ``` hoelzl@59664 ` 1422` ``` then obtain pq where pq: "\a b c d. ((a, c), (b, d)) \ set_pmf pq \ R a b \ S c d" ``` hoelzl@59664 ` 1423` ``` and eq: "map_pmf fst pq = pair_pmf A A'" "map_pmf snd pq = pair_pmf B B'" ``` hoelzl@59664 ` 1424` ``` by (force elim: rel_pmf.cases) ``` hoelzl@59664 ` 1425` ``` show "rel_pmf R A B" ``` hoelzl@59664 ` 1426` ``` proof (rule rel_pmf.intros) ``` hoelzl@59664 ` 1427` ``` let ?f = "\(a, b). (fst a, fst b)" ``` hoelzl@59664 ` 1428` ``` have [simp]: "(\x. fst (?f x)) = fst o fst" "(\x. snd (?f x)) = fst o snd" ``` hoelzl@59664 ` 1429` ``` by auto ``` hoelzl@59664 ` 1430` hoelzl@59664 ` 1431` ``` show "map_pmf fst (map_pmf ?f pq) = A" ``` hoelzl@59664 ` 1432` ``` by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_fst_pair_pmf) ``` hoelzl@59664 ` 1433` ``` show "map_pmf snd (map_pmf ?f pq) = B" ``` hoelzl@59664 ` 1434` ``` by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_fst_pair_pmf) ``` hoelzl@59664 ` 1435` hoelzl@59664 ` 1436` ``` fix a b assume "(a, b) \ set_pmf (map_pmf ?f pq)" ``` hoelzl@59664 ` 1437` ``` then obtain c d where "((a, c), (b, d)) \ set_pmf pq" ``` hoelzl@59665 ` 1438` ``` by auto ``` hoelzl@59664 ` 1439` ``` from pq[OF this] show "R a b" .. ``` hoelzl@59664 ` 1440` ``` qed ``` hoelzl@59664 ` 1441` ``` show "rel_pmf S A' B'" ``` hoelzl@59664 ` 1442` ``` proof (rule rel_pmf.intros) ``` hoelzl@59664 ` 1443` ``` let ?f = "\(a, b). (snd a, snd b)" ``` hoelzl@59664 ` 1444` ``` have [simp]: "(\x. fst (?f x)) = snd o fst" "(\x. snd (?f x)) = snd o snd" ``` hoelzl@59664 ` 1445` ``` by auto ``` hoelzl@59664 ` 1446` hoelzl@59664 ` 1447` ``` show "map_pmf fst (map_pmf ?f pq) = A'" ``` hoelzl@59664 ` 1448` ``` by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_snd_pair_pmf) ``` hoelzl@59664 ` 1449` ``` show "map_pmf snd (map_pmf ?f pq) = B'" ``` hoelzl@59664 ` 1450` ``` by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_snd_pair_pmf) ``` hoelzl@59664 ` 1451` hoelzl@59664 ` 1452` ``` fix c d assume "(c, d) \ set_pmf (map_pmf ?f pq)" ``` hoelzl@59664 ` 1453` ``` then obtain a b where "((a, c), (b, d)) \ set_pmf pq" ``` hoelzl@59665 ` 1454` ``` by auto ``` hoelzl@59664 ` 1455` ``` from pq[OF this] show "S c d" .. ``` hoelzl@59664 ` 1456` ``` qed ``` hoelzl@59664 ` 1457` ```next ``` hoelzl@59664 ` 1458` ``` assume "rel_pmf R A B" "rel_pmf S A' B'" ``` hoelzl@59664 ` 1459` ``` then obtain Rpq Spq ``` hoelzl@59664 ` 1460` ``` where Rpq: "\a b. (a, b) \ set_pmf Rpq \ R a b" ``` hoelzl@59664 ` 1461` ``` "map_pmf fst Rpq = A" "map_pmf snd Rpq = B" ``` hoelzl@59664 ` 1462` ``` and Spq: "\a b. (a, b) \ set_pmf Spq \ S a b" ``` hoelzl@59664 ` 1463` ``` "map_pmf fst Spq = A'" "map_pmf snd Spq = B'" ``` hoelzl@59664 ` 1464` ``` by (force elim: rel_pmf.cases) ``` hoelzl@59664 ` 1465` hoelzl@59664 ` 1466` ``` let ?f = "(\((a, c), (b, d)). ((a, b), (c, d)))" ``` hoelzl@59664 ` 1467` ``` let ?pq = "map_pmf ?f (pair_pmf Rpq Spq)" ``` hoelzl@59664 ` 1468` ``` have [simp]: "(\x. fst (?f x)) = (\(a, b). (fst a, fst b))" "(\x. snd (?f x)) = (\(a, b). (snd a, snd b))" ``` hoelzl@59664 ` 1469` ``` by auto ``` hoelzl@59664 ` 1470` hoelzl@59664 ` 1471` ``` show "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')" ``` hoelzl@59664 ` 1472` ``` by (rule rel_pmf.intros[where pq="?pq"]) ``` hoelzl@59665 ` 1473` ``` (auto simp: map_snd_pair_pmf map_fst_pair_pmf map_pmf_comp Rpq Spq ``` hoelzl@59664 ` 1474` ``` map_pair) ``` hoelzl@59664 ` 1475` ```qed ``` hoelzl@59664 ` 1476` lp15@59667 ` 1477` ```lemma rel_pmf_reflI: ``` hoelzl@59664 ` 1478` ``` assumes "\x. x \ set_pmf p \ P x x" ``` hoelzl@59664 ` 1479` ``` shows "rel_pmf P p p" ``` hoelzl@59665 ` 1480` ``` by (rule rel_pmf.intros[where pq="map_pmf (\x. (x, x)) p"]) ``` hoelzl@59665 ` 1481` ``` (auto simp add: pmf.map_comp o_def assms) ``` hoelzl@59664 ` 1482` Andreas@61634 ` 1483` ```lemma rel_pmf_bij_betw: ``` Andreas@61634 ` 1484` ``` assumes f: "bij_betw f (set_pmf p) (set_pmf q)" ``` Andreas@61634 ` 1485` ``` and eq: "\x. x \ set_pmf p \ pmf p x = pmf q (f x)" ``` Andreas@61634 ` 1486` ``` shows "rel_pmf (\x y. f x = y) p q" ``` Andreas@61634 ` 1487` ```proof(rule rel_pmf.intros) ``` Andreas@61634 ` 1488` ``` let ?pq = "map_pmf (\x. (x, f x)) p" ``` Andreas@61634 ` 1489` ``` show "map_pmf fst ?pq = p" by(simp add: pmf.map_comp o_def) ``` Andreas@61634 ` 1490` Andreas@61634 ` 1491` ``` have "map_pmf f p = q" ``` Andreas@61634 ` 1492` ``` proof(rule pmf_eqI) ``` Andreas@61634 ` 1493` ``` fix i ``` Andreas@61634 ` 1494` ``` show "pmf (map_pmf f p) i = pmf q i" ``` Andreas@61634 ` 1495` ``` proof(cases "i \ set_pmf q") ``` Andreas@61634 ` 1496` ``` case True ``` Andreas@61634 ` 1497` ``` with f obtain j where "i = f j" "j \ set_pmf p" ``` Andreas@61634 ` 1498` ``` by(auto simp add: bij_betw_def image_iff) ``` Andreas@61634 ` 1499` ``` thus ?thesis using f by(simp add: bij_betw_def pmf_map_inj eq) ``` Andreas@61634 ` 1500` ``` next ``` Andreas@61634 ` 1501` ``` case False thus ?thesis ``` Andreas@61634 ` 1502` ``` by(subst pmf_map_outside)(auto simp add: set_pmf_iff eq[symmetric]) ``` Andreas@61634 ` 1503` ``` qed ``` Andreas@61634 ` 1504` ``` qed ``` Andreas@61634 ` 1505` ``` then show "map_pmf snd ?pq = q" by(simp add: pmf.map_comp o_def) ``` Andreas@61634 ` 1506` ```qed auto ``` Andreas@61634 ` 1507` hoelzl@59664 ` 1508` ```context ``` hoelzl@59664 ` 1509` ```begin ``` hoelzl@59664 ` 1510` hoelzl@59664 ` 1511` ```interpretation pmf_as_measure . ``` hoelzl@59664 ` 1512` hoelzl@59664 ` 1513` ```definition "join_pmf M = bind_pmf M (\x. x)" ``` hoelzl@59664 ` 1514` hoelzl@59664 ` 1515` ```lemma bind_eq_join_pmf: "bind_pmf M f = join_pmf (map_pmf f M)" ``` hoelzl@59664 ` 1516` ``` unfolding join_pmf_def bind_map_pmf .. ``` hoelzl@59664 ` 1517` hoelzl@59664 ` 1518` ```lemma join_eq_bind_pmf: "join_pmf M = bind_pmf M id" ``` hoelzl@59664 ` 1519` ``` by (simp add: join_pmf_def id_def) ``` hoelzl@59664 ` 1520` hoelzl@59664 ` 1521` ```lemma pmf_join: "pmf (join_pmf N) i = (\M. pmf M i \measure_pmf N)" ``` hoelzl@59664 ` 1522` ``` unfolding join_pmf_def pmf_bind .. ``` hoelzl@59664 ` 1523` hoelzl@62975 ` 1524` ```lemma ennreal_pmf_join: "ennreal (pmf (join_pmf N) i) = (\\<^sup>+M. pmf M i \measure_pmf N)" ``` hoelzl@62975 ` 1525` ``` unfolding join_pmf_def ennreal_pmf_bind .. ``` hoelzl@59664 ` 1526` hoelzl@59665 ` 1527` ```lemma set_pmf_join_pmf[simp]: "set_pmf (join_pmf f) = (\p\set_pmf f. set_pmf p)" ``` hoelzl@59665 ` 1528` ``` by (simp add: join_pmf_def) ``` hoelzl@59664 ` 1529` hoelzl@59664 ` 1530` ```lemma join_return_pmf: "join_pmf (return_pmf M) = M" ``` hoelzl@59664 ` 1531` ``` by (simp add: integral_return pmf_eq_iff pmf_join return_pmf.rep_eq) ``` hoelzl@59664 ` 1532` hoelzl@59664 ` 1533` ```lemma map_join_pmf: "map_pmf f (join_pmf AA) = join_pmf (map_pmf (map_pmf f) AA)" ``` hoelzl@59664 ` 1534` ``` by (simp add: join_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf) ``` hoelzl@59664 ` 1535` hoelzl@59664 ` 1536` ```lemma join_map_return_pmf: "join_pmf (map_pmf return_pmf A) = A" ``` hoelzl@59664 ` 1537` ``` by (simp add: join_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') ``` hoelzl@59664 ` 1538` hoelzl@59664 ` 1539` ```end ``` hoelzl@59664 ` 1540` hoelzl@59664 ` 1541` ```lemma rel_pmf_joinI: ``` hoelzl@59664 ` 1542` ``` assumes "rel_pmf (rel_pmf P) p q" ``` hoelzl@59664 ` 1543` ``` shows "rel_pmf P (join_pmf p) (join_pmf q)" ``` hoelzl@59664 ` 1544` ```proof - ``` hoelzl@59664 ` 1545` ``` from assms obtain pq where p: "p = map_pmf fst pq" ``` hoelzl@59664 ` 1546` ``` and q: "q = map_pmf snd pq" ``` hoelzl@59664 ` 1547` ``` and P: "\x y. (x, y) \ set_pmf pq \ rel_pmf P x y" ``` hoelzl@59664 ` 1548` ``` by cases auto ``` lp15@59667 ` 1549` ``` from P obtain PQ ``` hoelzl@59664 ` 1550` ``` where PQ: "\x y a b. \ (x, y) \ set_pmf pq; (a, b) \ set_pmf (PQ x y) \ \ P a b" ``` hoelzl@59664 ` 1551` ``` and x: "\x y. (x, y) \ set_pmf pq \ map_pmf fst (PQ x y) = x" ``` hoelzl@59664 ` 1552` ``` and y: "\x y. (x, y) \ set_pmf pq \ map_pmf snd (PQ x y) = y" ``` hoelzl@59664 ` 1553` ``` by(metis rel_pmf.simps) ``` hoelzl@59664 ` 1554` hoelzl@59664 ` 1555` ``` let ?r = "bind_pmf pq (\(x, y). PQ x y)" ``` hoelzl@59665 ` 1556` ``` have "\a b. (a, b) \ set_pmf ?r \ P a b" by (auto intro: PQ) ``` hoelzl@59664 ` 1557` ``` moreover have "map_pmf fst ?r = join_pmf p" "map_pmf snd ?r = join_pmf q" ``` hoelzl@59664 ` 1558` ``` by (simp_all add: p q x y join_pmf_def map_bind_pmf bind_map_pmf split_def cong: bind_pmf_cong) ``` hoelzl@59664 ` 1559` ``` ultimately show ?thesis .. ``` hoelzl@59664 ` 1560` ```qed ``` hoelzl@59664 ` 1561` hoelzl@59664 ` 1562` ```lemma rel_pmf_bindI: ``` hoelzl@59664 ` 1563` ``` assumes pq: "rel_pmf R p q" ``` hoelzl@59664 ` 1564` ``` and fg: "\x y. R x y \ rel_pmf P (f x) (g y)" ``` hoelzl@59664 ` 1565` ``` shows "rel_pmf P (bind_pmf p f) (bind_pmf q g)" ``` hoelzl@59664 ` 1566` ``` unfolding bind_eq_join_pmf ``` hoelzl@59664 ` 1567` ``` by (rule rel_pmf_joinI) ``` hoelzl@59664 ` 1568` ``` (auto simp add: pmf.rel_map intro: pmf.rel_mono[THEN le_funD, THEN le_funD, THEN le_boolD, THEN mp, OF _ pq] fg) ``` hoelzl@59664 ` 1569` wenzelm@61808 ` 1570` ```text \ ``` hoelzl@59664 ` 1571` ``` Proof that @{const rel_pmf} preserves orders. ``` lp15@59667 ` 1572` ``` Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism, ``` lp15@59667 ` 1573` ``` Theoretical Computer Science 12(1):19--37, 1980, ``` wenzelm@63680 ` 1574` ``` \<^url>\http://dx.doi.org/10.1016/0304-3975(80)90003-1\ ``` wenzelm@61808 ` 1575` ```\ ``` hoelzl@59664 ` 1576` lp15@59667 ` 1577` ```lemma ``` hoelzl@59664 ` 1578` ``` assumes *: "rel_pmf R p q" ``` hoelzl@59664 ` 1579` ``` and refl: "reflp R" and trans: "transp R" ``` hoelzl@59664 ` 1580` ``` shows measure_Ici: "measure p {y. R x y} \ measure q {y. R x y}" (is ?thesis1) ``` hoelzl@59664 ` 1581` ``` and measure_Ioi: "measure p {y. R x y \ \ R y x} \ measure q {y. R x y \ \ R y x}" (is ?thesis2) ``` hoelzl@59664 ` 1582` ```proof - ``` hoelzl@59664 ` 1583` ``` from * obtain pq ``` hoelzl@59664 ` 1584` ``` where pq: "\x y. (x, y) \ set_pmf pq \ R x y" ``` hoelzl@59664 ` 1585` ``` and p: "p = map_pmf fst pq" ``` hoelzl@59664 ` 1586` ``` and q: "q = map_pmf snd pq" ``` hoelzl@59664 ` 1587` ``` by cases auto ``` hoelzl@59664 ` 1588` ``` show ?thesis1 ?thesis2 unfolding p q map_pmf_rep_eq using refl trans ``` hoelzl@59664 ` 1589` ``` by(auto 4 3 simp add: measure_distr reflpD AE_measure_pmf_iff intro!: measure_pmf.finite_measure_mono_AE dest!: pq elim: transpE) ``` hoelzl@59664 ` 1590` ```qed ``` hoelzl@59664 ` 1591` hoelzl@59664 ` 1592` ```lemma rel_pmf_inf: ``` hoelzl@59664 ` 1593` ``` fixes p q :: "'a pmf" ``` hoelzl@59664 ` 1594` ``` assumes 1: "rel_pmf R p q" ``` hoelzl@59664 ` 1595` ``` assumes 2: "rel_pmf R q p" ``` hoelzl@59664 ` 1596` ``` and refl: "reflp R" and trans: "transp R" ``` hoelzl@59664 ` 1597` ``` shows "rel_pmf (inf R R\\) p q" ``` hoelzl@59681 ` 1598` ```proof (subst rel_pmf_iff_equivp, safe) ``` hoelzl@59681 ` 1599` ``` show "equivp (inf R R\\)" ``` hoelzl@59681 ` 1600` ``` using trans refl by (auto simp: equivp_reflp_symp_transp intro: sympI transpI reflpI dest: transpD reflpD) ``` lp15@61609 ` 1601` hoelzl@59681 ` 1602` ``` fix C assume "C \ UNIV // {(x, y). inf R R\\ x y}" ``` hoelzl@59681 ` 1603` ``` then obtain x where C: "C = {y. R x y \ R y x}" ``` hoelzl@59681 ` 1604` ``` by (auto elim: quotientE) ``` hoelzl@59681 ` 1605` hoelzl@59670 ` 1606` ``` let ?R = "\x y. R x y \ R y x" ``` hoelzl@59670 ` 1607` ``` let ?\R = "\y. measure q {x. ?R x y}" ``` hoelzl@59681 ` 1608` ``` have "measure p {y. ?R x y} = measure p ({y. R x y} - {y. R x y \ \ R y x})" ``` hoelzl@59681 ` 1609` ``` by(auto intro!: arg_cong[where f="measure p"]) ``` hoelzl@59681 ` 1610` ``` also have "\ = measure p {y. R x y} - measure p {y. R x y \ \ R y x}" ``` hoelzl@59681 ` 1611` ``` by (rule measure_pmf.finite_measure_Diff) auto ``` hoelzl@59681 ` 1612` ``` also have "measure p {y. R x y \ \ R y x} = measure q {y. R x y \ \ R y x}" ``` hoelzl@59681 ` 1613` ``` using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi) ``` hoelzl@59681 ` 1614` ``` also have "measure p {y. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 1615` ``` using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici) ``` hoelzl@59681 ` 1616` ``` also have "measure q {y. R x y} - measure q {y. R x y \ \ R y x} = ``` hoelzl@59681 ` 1617` ``` measure q ({y. R x y} - {y. R x y \ \ R y x})" ``` hoelzl@59681 ` 1618` ``` by(rule measure_pmf.finite_measure_Diff[symmetric]) auto ``` hoelzl@59681 ` 1619` ``` also have "\ = ?\R x" ``` hoelzl@59681 ` 1620` ``` by(auto intro!: arg_cong[where f="measure q"]) ``` hoelzl@59681 ` 1621` ``` finally show "measure p C = measure q C" ``` hoelzl@59681 ` 1622` ``` by (simp add: C conj_commute) ``` hoelzl@59664 ` 1623` ```qed ``` hoelzl@59664 ` 1624` hoelzl@59664 ` 1625` ```lemma rel_pmf_antisym: ``` hoelzl@59664 ` 1626` ``` fixes p q :: "'a pmf" ``` hoelzl@59664 ` 1627` ``` assumes 1: "rel_pmf R p q" ``` hoelzl@59664 ` 1628` ``` assumes 2: "rel_pmf R q p" ``` haftmann@64634 ` 1629` ``` and refl: "reflp R" and trans: "transp R" and antisym: "antisymp R" ``` hoelzl@59664 ` 1630` ``` shows "p = q" ``` hoelzl@59664 ` 1631` ```proof - ``` hoelzl@59664 ` 1632` ``` from 1 2 refl trans have "rel_pmf (inf R R\\) p q" by(rule rel_pmf_inf) ``` nipkow@67399 ` 1633` ``` also have "inf R R\\ = (=)" ``` haftmann@64634 ` 1634` ``` using refl antisym by (auto intro!: ext simp add: reflpD dest: antisympD) ``` hoelzl@59664 ` 1635` ``` finally show ?thesis unfolding pmf.rel_eq . ``` hoelzl@59664 ` 1636` ```qed ``` hoelzl@59664 ` 1637` hoelzl@59664 ` 1638` ```lemma reflp_rel_pmf: "reflp R \ reflp (rel_pmf R)" ``` haftmann@64634 ` 1639` ``` by (fact pmf.rel_reflp) ``` hoelzl@59664 ` 1640` haftmann@64634 ` 1641` ```lemma antisymp_rel_pmf: ``` haftmann@64634 ` 1642` ``` "\ reflp R; transp R; antisymp R \ ``` haftmann@64634 ` 1643` ``` \ antisymp (rel_pmf R)" ``` haftmann@64634 ` 1644` ```by(rule antisympI)(blast intro: rel_pmf_antisym) ``` hoelzl@59664 ` 1645` hoelzl@59664 ` 1646` ```lemma transp_rel_pmf: ``` hoelzl@59664 ` 1647` ``` assumes "transp R" ``` hoelzl@59664 ` 1648` ``` shows "transp (rel_pmf R)" ``` haftmann@64634 ` 1649` ``` using assms by (fact pmf.rel_transp) ``` hoelzl@59664 ` 1650` lars@67486 ` 1651` hoelzl@59664 ` 1652` ```subsection \ Distributions \ ``` hoelzl@59664 ` 1653` hoelzl@59000 ` 1654` ```context ``` hoelzl@59000 ` 1655` ```begin ``` hoelzl@59000 ` 1656` hoelzl@59000 ` 1657` ```interpretation pmf_as_function . ``` hoelzl@59000 ` 1658` hoelzl@59093 ` 1659` ```subsubsection \ Bernoulli Distribution \ ``` hoelzl@59093 ` 1660` hoelzl@59000 ` 1661` ```lift_definition bernoulli_pmf :: "real \ bool pmf" is ``` hoelzl@59000 ` 1662` ``` "\p b. ((\p. if b then p else 1 - p) \ min 1 \ max 0) p" ``` hoelzl@59000 ` 1663` ``` by (auto simp: nn_integral_count_space_finite[where A="{False, True}"] UNIV_bool ``` hoelzl@59000 ` 1664` ``` split: split_max split_min) ``` hoelzl@59000 ` 1665` hoelzl@59000 ` 1666` ```lemma pmf_bernoulli_True[simp]: "0 \ p \ p \ 1 \ pmf (bernoulli_pmf p) True = p" ``` hoelzl@59000 ` 1667` ``` by transfer simp ``` hoelzl@59000 ` 1668` hoelzl@59000 ` 1669` ```lemma pmf_bernoulli_False[simp]: "0 \ p \ p \ 1 \ pmf (bernoulli_pmf p) False = 1 - p" ``` hoelzl@59000 ` 1670` ``` by transfer simp ``` hoelzl@59000 ` 1671` hoelzl@62975 ` 1672` ```lemma set_pmf_bernoulli[simp]: "0 < p \ p < 1 \ set_pmf (bernoulli_pmf p) = UNIV" ``` hoelzl@59000 ` 1673` ``` by (auto simp add: set_pmf_iff UNIV_bool) ``` hoelzl@59000 ` 1674` lp15@59667 ` 1675` ```lemma nn_integral_bernoulli_pmf[simp]: ``` hoelzl@59002 ` 1676` ``` assumes [simp]: "0 \ p" "p \ 1" "\x. 0 \ f x" ``` hoelzl@59002 ` 1677` ``` shows "(\\<^sup>+x. f x \bernoulli_pmf p) = f True * p + f False * (1 - p)" ``` hoelzl@59002 ` 1678` ``` by (subst nn_integral_measure_pmf_support[of UNIV]) ``` hoelzl@59002 ` 1679` ``` (auto simp: UNIV_bool field_simps) ``` hoelzl@59002 ` 1680` lp15@59667 ` 1681` ```lemma integral_bernoulli_pmf[simp]: ``` hoelzl@59002 ` 1682` ``` assumes [simp]: "0 \ p" "p \ 1" ``` hoelzl@59002 ` 1683` ``` shows "(\x. f x \bernoulli_pmf p) = f True * p + f False * (1 - p)" ``` hoelzl@59002 ` 1684` ``` by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool) ``` hoelzl@59002 ` 1685` Andreas@59525 ` 1686` ```lemma pmf_bernoulli_half [simp]: "pmf (bernoulli_pmf (1 / 2)) x = 1 / 2" ``` Andreas@59525 ` 1687` ```by(cases x) simp_all ``` Andreas@59525 ` 1688` Andreas@59525 ` 1689` ```lemma measure_pmf_bernoulli_half: "measure_pmf (bernoulli_pmf (1 / 2)) = uniform_count_measure UNIV" ``` hoelzl@62975 ` 1690` ``` by (rule measure_eqI) ``` hoelzl@62975 ` 1691` ``` (simp_all add: nn_integral_pmf[symmetric] emeasure_uniform_count_measure ennreal_divide_numeral[symmetric] ``` hoelzl@62975 ` 1692` ``` nn_integral_count_space_finite sets_uniform_count_measure divide_ennreal_def mult_ac ``` hoelzl@62975 ` 1693` ``` ennreal_of_nat_eq_real_of_nat) ``` Andreas@59525 ` 1694` hoelzl@59093 ` 1695` ```subsubsection \ Geometric Distribution \ ``` hoelzl@59093 ` 1696` hoelzl@60602 ` 1697` ```context ``` hoelzl@60602 ` 1698` ``` fixes p :: real assumes p[arith]: "0 < p" "p \ 1" ``` hoelzl@60602 ` 1699` ```begin ``` hoelzl@60602 ` 1700` hoelzl@60602 ` 1701` ```lift_definition geometric_pmf :: "nat pmf" is "\n. (1 - p)^n * p" ``` hoelzl@59000 ` 1702` ```proof ``` hoelzl@62975 ` 1703` ``` have "(\i. ennreal (p * (1 - p) ^ i)) = ennreal (p * (1 / (1 - (1 - p))))" ``` hoelzl@62975 ` 1704` ``` by (intro suminf_ennreal_eq sums_mult geometric_sums) auto ``` hoelzl@62975 ` 1705` ``` then show "(\\<^sup>+ x. ennreal ((1 - p)^x * p) \count_space UNIV) = 1" ``` hoelzl@59000 ` 1706` ``` by (simp add: nn_integral_count_space_nat field_simps) ``` hoelzl@59000 ` 1707` ```qed simp ``` hoelzl@59000 ` 1708` hoelzl@60602 ` 1709` ```lemma pmf_geometric[simp]: "pmf geometric_pmf n = (1 - p)^n * p" ``` hoelzl@59000 ` 1710` ``` by transfer rule ``` hoelzl@59000 ` 1711` hoelzl@60602 ` 1712` ```end ``` hoelzl@60602 ` 1713` hoelzl@60602 ` 1714` ```lemma set_pmf_geometric: "0 < p \ p < 1 \ set_pmf (geometric_pmf p) = UNIV" ``` lp15@61609 ` 1715` ``` by (auto simp: set_pmf_iff) ``` hoelzl@59000 ` 1716` hoelzl@59093 ` 1717` ```subsubsection \ Uniform Multiset Distribution \ ``` hoelzl@59093 ` 1718` hoelzl@59000 ` 1719` ```context ``` hoelzl@59000 ` 1720` ``` fixes M :: "'a multiset" assumes M_not_empty: "M \ {#}" ``` hoelzl@59000 ` 1721` ```begin ``` hoelzl@59000 ` 1722` hoelzl@59000 ` 1723` ```lift_definition pmf_of_multiset :: "'a pmf" is "\x. count M x / size M" ``` hoelzl@59000 ` 1724` ```proof ``` hoelzl@62975 ` 1725` ``` show "(\\<^sup>+ x. ennreal (real (count M x) / real (size M)) \count_space UNIV) = 1" ``` hoelzl@59000 ` 1726` ``` using M_not_empty ``` hoelzl@59000 ` 1727` ``` by (simp add: zero_less_divide_iff nn_integral_count_space nonempty_has_size ``` nipkow@64267 ` 1728` ``` sum_divide_distrib[symmetric]) ``` nipkow@64267 ` 1729` ``` (auto simp: size_multiset_overloaded_eq intro!: sum.cong) ``` hoelzl@59000 ` 1730` ```qed simp ``` hoelzl@59000 ` 1731` hoelzl@59000 ` 1732` ```lemma pmf_of_multiset[simp]: "pmf pmf_of_multiset x = count M x / size M" ``` hoelzl@59000 ` 1733` ``` by transfer rule ``` hoelzl@59000 ` 1734` nipkow@60495 ` 1735` ```lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_mset M" ``` hoelzl@59000 ` 1736` ``` by (auto simp: set_pmf_iff) ``` hoelzl@59000 ` 1737` hoelzl@59000 ` 1738` ```end ``` hoelzl@59000 ` 1739` hoelzl@59093 ` 1740` ```subsubsection \ Uniform Distribution \ ``` hoelzl@59093 ` 1741` hoelzl@59000 ` 1742` ```context ``` hoelzl@59000 ` 1743` ``` fixes S :: "'a set" assumes S_not_empty: "S \ {}" and S_finite: "finite S" ``` hoelzl@59000 ` 1744` ```begin ``` hoelzl@59000 ` 1745` hoelzl@59000 ` 1746` ```lift_definition pmf_of_set :: "'a pmf" is "\x. indicator S x / card S" ``` hoelzl@59000 ` 1747` ```proof ``` hoelzl@62975 ` 1748` ``` show "(\\<^sup>+ x. ennreal (indicator S x / real (card S)) \count_space UNIV) = 1" ``` hoelzl@62975 ` 1749` ``` using S_not_empty S_finite ``` hoelzl@62975 ` 1750` ``` by (subst nn_integral_count_space'[of S]) ``` hoelzl@62975 ` 1751` ``` (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_mult[symmetric]) ``` hoelzl@59000 ` 1752` ```qed simp ``` hoelzl@59000 ` 1753` hoelzl@59000 ` 1754` ```lemma pmf_of_set[simp]: "pmf pmf_of_set x = indicator S x / card S" ``` hoelzl@59000 ` 1755` ``` by transfer rule ``` hoelzl@59000 ` 1756` hoelzl@59000 ` 1757` ```lemma set_pmf_of_set[simp]: "set_pmf pmf_of_set = S" ``` hoelzl@59000 ` 1758` ``` using S_finite S_not_empty by (auto simp: set_pmf_iff) ``` hoelzl@59000 ` 1759` Andreas@61634 ` 1760` ```lemma emeasure_pmf_of_set_space[simp]: "emeasure pmf_of_set S = 1" ``` hoelzl@59002 ` 1761` ``` by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff) ``` hoelzl@59002 ` 1762` nipkow@64267 ` 1763` ```lemma nn_integral_pmf_of_set: "nn_integral (measure_pmf pmf_of_set) f = sum f S / card S" ``` hoelzl@62975 ` 1764` ``` by (subst nn_integral_measure_pmf_finite) ``` nipkow@64267 ` 1765` ``` (simp_all add: sum_distrib_right[symmetric] card_gt_0_iff S_not_empty S_finite divide_ennreal_def ``` hoelzl@62975 ` 1766` ``` divide_ennreal[symmetric] ennreal_of_nat_eq_real_of_nat[symmetric] ennreal_times_divide) ``` Andreas@60068 ` 1767` nipkow@64267 ` 1768` ```lemma integral_pmf_of_set: "integral\<^sup>L (measure_pmf pmf_of_set) f = sum f S / card S" ``` nipkow@64267 ` 1769` ``` by (subst integral_measure_pmf[of S]) (auto simp: S_finite sum_divide_distrib) ``` Andreas@60068 ` 1770` hoelzl@62975 ` 1771` ```lemma emeasure_pmf_of_set: "emeasure (measure_pmf pmf_of_set) A = card (S \ A) / card S" ``` hoelzl@62975 ` 1772` ``` by (subst nn_integral_indicator[symmetric], simp) ``` nipkow@64267 ` 1773` ``` (simp add: S_finite S_not_empty card_gt_0_iff indicator_def sum.If_cases divide_ennreal ``` hoelzl@62975 ` 1774` ``` ennreal_of_nat_eq_real_of_nat nn_integral_pmf_of_set) ``` Andreas@60068 ` 1775` hoelzl@62975 ` 1776` ```lemma measure_pmf_of_set: "measure (measure_pmf pmf_of_set) A = card (S \ A) / card S" ``` wenzelm@63092 ` 1777` ``` using emeasure_pmf_of_set[of A] ``` hoelzl@62975 ` 1778` ``` by (simp add: measure_nonneg measure_pmf.emeasure_eq_measure) ``` Andreas@61634 ` 1779` hoelzl@59000 ` 1780` ```end ``` lars@67486 ` 1781` eberlm@65395 ` 1782` ```lemma pmf_expectation_bind_pmf_of_set: ``` eberlm@65395 ` 1783` ``` fixes A :: "'a set" and f :: "'a \ 'b pmf" ``` eberlm@65395 ` 1784` ``` and h :: "'b \ 'c::{banach, second_countable_topology}" ``` eberlm@65395 ` 1785` ``` assumes "A \ {}" "finite A" "\x. x \ A \ finite (set_pmf (f x))" ``` eberlm@65395 ` 1786` ``` shows "measure_pmf.expectation (pmf_of_set A \ f) h = ``` eberlm@65395 ` 1787` ``` (\a\A. measure_pmf.expectation (f a) h /\<^sub>R real (card A))" ``` eberlm@65395 ` 1788` ``` using assms by (subst pmf_expectation_bind[of A]) (auto simp: divide_simps) ``` hoelzl@59000 ` 1789` eberlm@63099 ` 1790` ```lemma map_pmf_of_set: ``` eberlm@63099 ` 1791` ``` assumes "finite A" "A \ {}" ``` hoelzl@63886 ` 1792` ``` shows "map_pmf f (pmf_of_set A) = pmf_of_multiset (image_mset f (mset_set A))" ``` eberlm@63099 ` 1793` ``` (is "?lhs = ?rhs") ``` eberlm@63099 ` 1794` ```proof (intro pmf_eqI) ``` eberlm@63099 ` 1795` ``` fix x ``` eberlm@63099 ` 1796` ``` from assms have "ennreal (pmf ?lhs x) = ennreal (pmf ?rhs x)" ``` eberlm@63099 ` 1797` ``` by (subst ennreal_pmf_map) ``` eberlm@63099 ` 1798` ``` (simp_all add: emeasure_pmf_of_set mset_set_empty_iff count_image_mset Int_commute) ``` eberlm@63099 ` 1799` ``` thus "pmf ?lhs x = pmf ?rhs x" by simp ``` eberlm@63099 ` 1800` ```qed ``` eberlm@63099 ` 1801` eberlm@63099 ` 1802` ```lemma pmf_bind_pmf_of_set: ``` eberlm@63099 ` 1803` ``` assumes "A \ {}" "finite A" ``` hoelzl@63886 ` 1804` ``` shows "pmf (bind_pmf (pmf_of_set A) f) x = ``` eberlm@63099 ` 1805` ``` (\xa\A. pmf (f xa) x) / real_of_nat (card A)" (is "?lhs = ?rhs") ``` eberlm@63099 ` 1806` ```proof - ``` eberlm@63099 ` 1807` ``` from assms have "card A > 0" by auto ``` eberlm@63099 ` 1808` ``` with assms have "ennreal ?lhs = ennreal ?rhs" ``` hoelzl@63886 ` 1809` ``` by (subst ennreal_pmf_bind) ``` hoelzl@63886 ` 1810` ``` (simp_all add: nn_integral_pmf_of_set max_def pmf_nonneg divide_ennreal [symmetric] ``` nipkow@64267 ` 1811` ``` sum_nonneg ennreal_of_nat_eq_real_of_nat) ``` nipkow@64267 ` 1812` ``` thus ?thesis by (subst (asm) ennreal_inj) (auto intro!: sum_nonneg divide_nonneg_nonneg) ``` eberlm@63099 ` 1813` ```qed ``` eberlm@63099 ` 1814` Andreas@60068 ` 1815` ```lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x" ``` Andreas@60068 ` 1816` ```by(rule pmf_eqI)(simp add: indicator_def) ``` Andreas@60068 ` 1817` lp15@61609 ` 1818` ```lemma map_pmf_of_set_inj: ``` Andreas@60068 ` 1819` ``` assumes f: "inj_on f A" ``` Andreas@60068 ` 1820` ``` and [simp]: "A \ {}" "finite A" ``` Andreas@60068 ` 1821` ``` shows "map_pmf f (pmf_of_set A) = pmf_of_set (f ` A)" (is "?lhs = ?rhs") ``` Andreas@60068 ` 1822` ```proof(rule pmf_eqI) ``` Andreas@60068 ` 1823` ``` fix i ``` Andreas@60068 ` 1824` ``` show "pmf ?lhs i = pmf ?rhs i" ``` Andreas@60068 ` 1825` ``` proof(cases "i \ f ` A") ``` Andreas@60068 ` 1826` ``` case True ``` Andreas@60068 ` 1827` ``` then obtain i' where "i = f i'" "i' \ A" by auto ``` Andreas@60068 ` 1828` ``` thus ?thesis using f by(simp add: card_image pmf_map_inj) ``` Andreas@60068 ` 1829` ``` next ``` Andreas@60068 ` 1830` ``` case False ``` Andreas@60068 ` 1831` ``` hence "pmf ?lhs i = 0" by(simp add: pmf_eq_0_set_pmf set_map_pmf) ``` Andreas@60068 ` 1832` ``` moreover have "pmf ?rhs i = 0" using False by simp ``` Andreas@60068 ` 1833` ``` ultimately show ?thesis by simp ``` Andreas@60068 ` 1834` ``` qed ``` Andreas@60068 ` 1835` ```qed ``` Andreas@60068 ` 1836` eberlm@65395 ` 1837` ```lemma map_pmf_of_set_bij_betw: ``` eberlm@65395 ` 1838` ``` assumes "bij_betw f A B" "A \ {}" "finite A" ``` eberlm@65395 ` 1839` ``` shows "map_pmf f (pmf_of_set A) = pmf_of_set B" ``` eberlm@65395 ` 1840` ```proof - ``` eberlm@65395 ` 1841` ``` have "map_pmf f (pmf_of_set A) = pmf_of_set (f ` A)" ``` eberlm@65395 ` 1842` ``` by (intro map_pmf_of_set_inj assms bij_betw_imp_inj_on[OF assms(1)]) ``` eberlm@65395 ` 1843` ``` also from assms have "f ` A = B" by (simp add: bij_betw_def) ``` eberlm@65395 ` 1844` ``` finally show ?thesis . ``` eberlm@65395 ` 1845` ```qed ``` eberlm@65395 ` 1846` eberlm@63099 ` 1847` ```text \ ``` hoelzl@63886 ` 1848` ``` Choosing an element uniformly at random from the union of a disjoint family ``` hoelzl@63886 ` 1849` ``` of finite non-empty sets with the same size is the same as first choosing a set ``` hoelzl@63886 ` 1850` ``` from the family uniformly at random and then choosing an element from the chosen set ``` hoelzl@63886 ` 1851` ``` uniformly at random. ``` eberlm@63099 ` 1852` ```\ ``` eberlm@63099 ` 1853` ```lemma pmf_of_set_UN: ``` eberlm@63099 ` 1854` ``` assumes "finite (UNION A f)" "A \ {}" "\x. x \ A \ f x \ {}" ``` eberlm@63099 ` 1855` ``` "\x. x \ A \ card (f x) = n" "disjoint_family_on f A" ``` eberlm@63099 ` 1856` ``` shows "pmf_of_set (UNION A f) = do {x \ pmf_of_set A; pmf_of_set (f x)}" ``` eberlm@63099 ` 1857` ``` (is "?lhs = ?rhs") ``` eberlm@63099 ` 1858` ```proof (intro pmf_eqI) ``` eberlm@63099 ` 1859` ``` fix x ``` eberlm@63099 ` 1860` ``` from assms have [simp]: "finite A" ``` eberlm@63099 ` 1861` ``` using infinite_disjoint_family_imp_infinite_UNION[of A f] by blast ``` eberlm@63099 ` 1862` ``` from assms have "ereal (pmf (pmf_of_set (UNION A f)) x) = ``` eberlm@63099 ` 1863` ``` ereal (indicator (\x\A. f x) x / real (card (\x\A. f x)))" ``` eberlm@63099 ` 1864` ``` by (subst pmf_of_set) auto ``` eberlm@63099 ` 1865` ``` also from assms have "card (\x\A. f x) = card A * n" ``` eberlm@63099 ` 1866` ``` by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def) ``` hoelzl@63886 ` 1867` ``` also from assms ``` hoelzl@63886 ` 1868` ``` have "indicator (\x\A. f x) x / real \ = ``` eberlm@63099 ` 1869` ``` indicator (\x\A. f x) x / (n * real (card A))" ``` nipkow@64267 ` 1870` ``` by (simp add: sum_divide_distrib [symmetric] mult_ac) ``` eberlm@63099 ` 1871` ``` also from assms have "indicator (\x\A. f x) x = (\y\A. indicator (f y) x)" ``` eberlm@63099 ` 1872` ``` by (intro indicator_UN_disjoint) simp_all ``` eberlm@63099 ` 1873` ``` also from assms have "ereal ((\y\A. indicator (f y) x) / (real n * real (card A))) = ``` eberlm@63099 ` 1874` ``` ereal (pmf ?rhs x)" ``` nipkow@64267 ` 1875` ``` by (subst pmf_bind_pmf_of_set) (simp_all add: sum_divide_distrib) ``` eberlm@63099 ` 1876` ``` finally show "pmf ?lhs x = pmf ?rhs x" by simp ``` eberlm@63099 ` 1877` ```qed ``` eberlm@63099 ` 1878` Andreas@60068 ` 1879` ```lemma bernoulli_pmf_half_conv_pmf_of_set: "bernoulli_pmf (1 / 2) = pmf_of_set UNIV" ``` hoelzl@62975 ` 1880` ``` by (rule pmf_eqI) simp_all ``` Andreas@61634 ` 1881` hoelzl@59093 ` 1882` ```subsubsection \ Poisson Distribution \ ``` hoelzl@59093 ` 1883` hoelzl@59093 ` 1884` ```context ``` hoelzl@59093 ` 1885` ``` fixes rate :: real assumes rate_pos: "0 < rate" ``` hoelzl@59093 ` 1886` ```begin ``` hoelzl@59093 ` 1887` hoelzl@59093 ` 1888` ```lift_definition poisson_pmf :: "nat pmf" is "\k. rate ^ k / fact k * exp (-rate)" ``` lp15@59730 ` 1889` ```proof (* by Manuel Eberl *) ``` hoelzl@59093 ` 1890` ``` have summable: "summable (\x::nat. rate ^ x / fact x)" using summable_exp ``` haftmann@59557 ` 1891` ``` by (simp add: field_simps divide_inverse [symmetric]) ``` hoelzl@59093 ` 1892` ``` have "(\\<^sup>+(x::nat). rate ^ x / fact x * exp (-rate) \count_space UNIV) = ``` hoelzl@59093 ` 1893` ``` exp (-rate) * (\\<^sup>+(x::nat). rate ^ x / fact x \count_space UNIV)" ``` hoelzl@62975 ` 1894` ``` by (simp add: field_simps nn_integral_cmult[symmetric] ennreal_mult'[symmetric]) ``` hoelzl@59093 ` 1895` ``` also from rate_pos have "(\\<^sup>+(x::nat). rate ^ x / fact x \count_space UNIV) = (\x. rate ^ x / fact x)" ``` hoelzl@62975 ` 1896` ``` by (simp_all add: nn_integral_count_space_nat suminf_ennreal summable ennreal_suminf_neq_top) ``` hoelzl@59093 ` 1897` ``` also have "... = exp rate" unfolding exp_def ``` lp15@59730 ` 1898` ``` by (simp add: field_simps divide_inverse [symmetric]) ``` hoelzl@62975 ` 1899` ``` also have "ennreal (exp (-rate)) * ennreal (exp rate) = 1" ``` hoelzl@62975 ` 1900` ``` by (simp add: mult_exp_exp ennreal_mult[symmetric]) ``` hoelzl@62975 ` 1901` ``` finally show "(\\<^sup>+ x. ennreal (rate ^ x / (fact x) * exp (- rate)) \count_space UNIV) = 1" . ``` hoelzl@59093 ` 1902` ```qed (simp add: rate_pos[THEN less_imp_le]) ``` hoelzl@59093 ` 1903` hoelzl@59093 ` 1904` ```lemma pmf_poisson[simp]: "pmf poisson_pmf k = rate ^ k / fact k * exp (-rate)" ``` hoelzl@59093 ` 1905` ``` by transfer rule ``` hoelzl@59093 ` 1906` hoelzl@59093 ` 1907` ```lemma set_pmf_poisson[simp]: "set_pmf poisson_pmf = UNIV" ``` hoelzl@59093 ` 1908` ``` using rate_pos by (auto simp: set_pmf_iff) ``` hoelzl@59093 ` 1909` hoelzl@59000 ` 1910` ```end ``` hoelzl@59000 ` 1911` hoelzl@59093 ` 1912` ```subsubsection \ Binomial Distribution \ ``` hoelzl@59093 ` 1913` hoelzl@59093 ` 1914` ```context ``` hoelzl@59093 ` 1915` ``` fixes n :: nat and p :: real assumes p_nonneg: "0 \ p" and p_le_1: "p \ 1" ``` hoelzl@59093 ` 1916` ```begin ``` hoelzl@59093 ` 1917` hoelzl@59093 ` 1918` ```lift_definition binomial_pmf :: "nat pmf" is "\k. (n choose k) * p^k * (1 - p)^(n - k)" ``` hoelzl@59093 ` 1919` ```proof ``` hoelzl@62975 ` 1920` ``` have "(\\<^sup>+k. ennreal (real (n choose k) * p ^ k * (1 - p) ^ (n - k)) \count_space UNIV) = ``` hoelzl@62975 ` 1921` ``` ennreal (\k\n. real (n choose k) * p ^ k * (1 - p) ^ (n - k))" ``` hoelzl@59093 ` 1922` ``` using p_le_1 p_nonneg by (subst nn_integral_count_space') auto ``` hoelzl@59093 ` 1923` ``` also have "(\k\n. real (n choose k) * p ^ k * (1 - p) ^ (n - k)) = (p + (1 - p)) ^ n" ``` lp15@61609 ` 1924` ``` by (subst binomial_ring) (simp add: atLeast0AtMost) ``` hoelzl@62975 ` 1925` ``` finally show "(\\<^sup>+ x. ennreal (real (n choose x) * p ^ x * (1 - p) ^ (n - x)) \count_space UNIV) = 1" ``` hoelzl@59093 ` 1926` ``` by simp ``` hoelzl@59093 ` 1927` ```qed (insert p_nonneg p_le_1, simp) ``` hoelzl@59093 ` 1928` hoelzl@59093 ` 1929` ```lemma pmf_binomial[simp]: "pmf binomial_pmf k = (n choose k) * p^k * (1 - p)^(n - k)" ``` hoelzl@59093 ` 1930` ``` by transfer rule ``` hoelzl@59093 ` 1931` hoelzl@59093 ` 1932` ```lemma set_pmf_binomial_eq: "set_pmf binomial_pmf = (if p = 0 then {0} else if p = 1 then {n} else {.. n})" ``` hoelzl@59093 ` 1933` ``` using p_nonneg p_le_1 unfolding set_eq_iff set_pmf_iff pmf_binomial by (auto simp: set_pmf_iff) ``` hoelzl@59093 ` 1934` hoelzl@59093 ` 1935` ```end ``` hoelzl@59093 ` 1936` hoelzl@59093 ` 1937` ```end ``` hoelzl@59093 ` 1938` hoelzl@59093 ` 1939` ```lemma set_pmf_binomial_0[simp]: "set_pmf (binomial_pmf n 0) = {0}" ``` hoelzl@59093 ` 1940` ``` by (simp add: set_pmf_binomial_eq) ``` hoelzl@59093 ` 1941` hoelzl@59093 ` 1942` ```lemma set_pmf_binomial_1[simp]: "set_pmf (binomial_pmf n 1) = {n}" ``` hoelzl@59093 ` 1943` ``` by (simp add: set_pmf_binomial_eq) ``` hoelzl@59093 ` 1944` hoelzl@59093 ` 1945` ```lemma set_pmf_binomial[simp]: "0 < p \ p < 1 \ set_pmf (binomial_pmf n p) = {..n}" ``` hoelzl@59093 ` 1946` ``` by (simp add: set_pmf_binomial_eq) ``` hoelzl@59093 ` 1947` wenzelm@63343 ` 1948` ```context includes lifting_syntax ``` wenzelm@63343 ` 1949` ```begin ``` Andreas@61634 ` 1950` Andreas@61634 ` 1951` ```lemma bind_pmf_parametric [transfer_rule]: ``` Andreas@61634 ` 1952` ``` "(rel_pmf A ===> (A ===> rel_pmf B) ===> rel_pmf B) bind_pmf bind_pmf" ``` Andreas@61634 ` 1953` ```by(blast intro: rel_pmf_bindI dest: rel_funD) ``` Andreas@61634 ` 1954` Andreas@61634 ` 1955` ```lemma return_pmf_parametric [transfer_rule]: "(A ===> rel_pmf A) return_pmf return_pmf" ``` Andreas@61634 ` 1956` ```by(rule rel_funI) simp ``` Andreas@61634 ` 1957` hoelzl@59000 ` 1958` ```end ``` Andreas@61634 ` 1959` eberlm@63099 ` 1960` eberlm@63194 ` 1961` ```primrec replicate_pmf :: "nat \ 'a pmf \ 'a list pmf" where ``` eberlm@63194 ` 1962` ``` "replicate_pmf 0 _ = return_pmf []" ``` eberlm@63194 ` 1963` ```| "replicate_pmf (Suc n) p = do {x \ p; xs \ replicate_pmf n p; return_pmf (x#xs)}" ``` eberlm@63194 ` 1964` eberlm@63194 ` 1965` ```lemma replicate_pmf_1: "replicate_pmf 1 p = map_pmf (\x. [x]) p" ``` eberlm@63194 ` 1966` ``` by (simp add: map_pmf_def bind_return_pmf) ``` hoelzl@63886 ` 1967` hoelzl@63886 ` 1968` ```lemma set_replicate_pmf: ``` eberlm@63194 ` 1969` ``` "set_pmf (replicate_pmf n p) = {xs\lists (set_pmf p). length xs = n}" ``` eberlm@63194 ` 1970` ``` by (induction n) (auto simp: length_Suc_conv) ``` eberlm@63194 ` 1971` eberlm@63194 ` 1972` ```lemma replicate_pmf_distrib: ``` hoelzl@63886 ` 1973` ``` "replicate_pmf (m + n) p = ``` eberlm@63194 ` 1974` ``` do {xs \ replicate_pmf m p; ys \ replicate_pmf n p; return_pmf (xs @ ys)}" ``` eberlm@63194 ` 1975` ``` by (induction m) (simp_all add: bind_return_pmf bind_return_pmf' bind_assoc_pmf) ``` eberlm@63194 ` 1976` hoelzl@63886 ` 1977` ```lemma power_diff': ``` eberlm@63194 ` 1978` ``` assumes "b \ a" ``` eberlm@63194 ` 1979` ``` shows "x ^ (a - b) = (if x = 0 \ a = b then 1 else x ^ a / (x::'a::field) ^ b)" ``` eberlm@63194 ` 1980` ```proof (cases "x = 0") ``` eberlm@63194 ` 1981` ``` case True ``` eberlm@63194 ` 1982` ``` with assms show ?thesis by (cases "a - b") simp_all ``` eberlm@63194 ` 1983` ```qed (insert assms, simp_all add: power_diff) ``` eberlm@63194 ` 1984` hoelzl@63886 ` 1985` eberlm@63194 ` 1986` ```lemma binomial_pmf_Suc: ``` eberlm@63194 ` 1987` ``` assumes "p \ {0..1}" ``` hoelzl@63886 ` 1988` ``` shows "binomial_pmf (Suc n) p = ``` hoelzl@63886 ` 1989` ``` do {b \ bernoulli_pmf p; ``` hoelzl@63886 ` 1990` ``` k \ binomial_pmf n p; ``` eberlm@63194 ` 1991` ``` return_pmf ((if b then 1 else 0) + k)}" (is "_ = ?rhs") ``` eberlm@63194 ` 1992` ```proof (intro pmf_eqI) ``` eberlm@63194 ` 1993` ``` fix k ``` eberlm@63194 ` 1994` ``` have A: "indicator {Suc a} (Suc b) = indicator {a} b" for a b ``` eberlm@63194 ` 1995` ``` by (simp add: indicator_def) ``` eberlm@63194 ` 1996` ``` show "pmf (binomial_pmf (Suc n) p) k = pmf ?rhs k" ``` eberlm@63194 ` 1997` ``` by (cases k; cases "k > n") ``` eberlm@63194 ` 1998` ``` (insert assms, auto simp: pmf_bind measure_pmf_single A divide_simps algebra_simps ``` eberlm@63194 ` 1999` ``` not_less less_eq_Suc_le [symmetric] power_diff') ``` eberlm@63194 ` 2000` ```qed ``` eberlm@63194 ` 2001` eberlm@63194 ` 2002` ```lemma binomial_pmf_0: "p \ {0..1} \ binomial_pmf 0 p = return_pmf 0" ``` eberlm@63194 ` 2003` ``` by (rule pmf_eqI) (simp_all add: indicator_def) ``` eberlm@63194 ` 2004` eberlm@63194 ` 2005` ```lemma binomial_pmf_altdef: ``` eberlm@63194 ` 2006` ``` assumes "p \ {0..1}" ``` eberlm@63194 ` 2007` ``` shows "binomial_pmf n p = map_pmf (length \ filter id) (replicate_pmf n (bernoulli_pmf p))" ``` hoelzl@63886 ` 2008` ``` by (induction n) ``` hoelzl@63886 ` 2009` ``` (insert assms, auto simp: binomial_pmf_Suc map_pmf_def bind_return_pmf bind_assoc_pmf ``` eberlm@63194 ` 2010` ``` bind_return_pmf' binomial_pmf_0 intro!: bind_pmf_cong) ``` eberlm@63194 ` 2011` eberlm@63194 ` 2012` lars@67486 ` 2013` ```subsection \PMFs from association lists\ ``` eberlm@63099 ` 2014` hoelzl@63886 ` 2015` ```definition pmf_of_list ::" ('a \ real) list \ 'a pmf" where ``` nipkow@63882 ` 2016` ``` "pmf_of_list xs = embed_pmf (\x. sum_list (map snd (filter (\z. fst z = x) xs)))" ``` eberlm@63099 ` 2017` eberlm@63099 ` 2018` ```definition pmf_of_list_wf where ``` nipkow@63882 ` 2019` ``` "pmf_of_list_wf xs \ (\x\set (map snd xs) . x \ 0) \ sum_list (map snd xs) = 1" ``` eberlm@63099 ` 2020` eberlm@63099 ` 2021` ```lemma pmf_of_list_wfI: ``` nipkow@63882 ` 2022` ``` "(\x. x \ set (map snd xs) \ x \ 0) \ sum_list (map snd xs) = 1 \ pmf_of_list_wf xs" ``` eberlm@63099 ` 2023` ``` unfolding pmf_of_list_wf_def by simp ``` eberlm@63099 ` 2024` eberlm@63099 ` 2025` ```context ``` eberlm@63099 ` 2026` ```begin ``` eberlm@63099 ` 2027` eberlm@63099 ` 2028` ```private lemma pmf_of_list_aux: ``` eberlm@63099 ` 2029` ``` assumes "\x. x \ set (map snd xs) \ x \ 0" ``` nipkow@63882 ` 2030` ``` assumes "sum_list (map snd xs) = 1" ``` nipkow@63882 ` 2031` ``` shows "(\\<^sup>+ x. ennreal (sum_list (map snd [z\xs . fst z = x])) \count_space UNIV) = 1" ``` eberlm@63099 ` 2032` ```proof - ``` nipkow@63882 ` 2033` ``` have "(\\<^sup>+ x. ennreal (sum_list (map snd (filter (\z. fst z = x) xs))) \count_space UNIV) = ``` nipkow@63882 ` 2034` ``` (\\<^sup>+ x. ennreal (sum_list (map (\(x',p). indicator {x'} x * p) xs)) \count_space UNIV)" ``` lars@67486 ` 2035` ``` apply (intro nn_integral_cong ennreal_cong, subst sum_list_map_filter') ``` lars@67486 ` 2036` ``` apply (rule arg_cong[where f = sum_list]) ``` lars@67486 ` 2037` ``` apply (auto cong: map_cong) ``` lars@67486 ` 2038` ``` done ``` eberlm@63099 ` 2039` ``` also have "\ = (\(x',p)\xs. (\\<^sup>+ x. ennreal (indicator {x'} x * p) \count_space UNIV))" ``` eberlm@63099 ` 2040` ``` using assms(1) ``` eberlm@63099 ` 2041` ``` proof (induction xs) ``` eberlm@63099 ` 2042` ``` case (Cons x xs) ``` eberlm@63099 ` 2043` ``` from Cons.prems have "snd x \ 0" by simp ``` eberlm@63099 ` 2044` ``` moreover have "b \ 0" if "(a,b) \ set xs" for a b ``` eberlm@63099 ` 2045` ``` using Cons.prems[of b] that by force ``` hoelzl@63886 ` 2046` ``` ultimately have "(\\<^sup>+ y. ennreal (\(x', p)\x # xs. indicator {x'} y * p) \count_space UNIV) = ``` hoelzl@63886 ` 2047` ``` (\\<^sup>+ y. ennreal (indicator {fst x} y * snd x) + ``` eberlm@63099 ` 2048` ``` ennreal (\(x', p)\xs. indicator {x'} y * p) \count_space UNIV)" ``` hoelzl@63886 ` 2049` ``` by (intro nn_integral_cong, subst ennreal_plus [symmetric]) ``` nipkow@63882 ` 2050` ``` (auto simp: case_prod_unfold indicator_def intro!: sum_list_nonneg) ``` hoelzl@63886 ` 2051` ``` also have "\ = (\\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \count_space UNIV) + ``` eberlm@63099 ` 2052` ``` (\\<^sup>+ y. ennreal (\(x', p)\xs. indicator {x'} y * p) \count_space UNIV)" ``` eberlm@63099 ` 2053` ``` by (intro nn_integral_add) ``` nipkow@63882 ` 2054` ``` (force intro!: sum_list_nonneg AE_I2 intro: Cons simp: indicator_def)+ ``` eberlm@63099 ` 2055` ``` also have "(\\<^sup>+ y. ennreal (\(x', p)\xs. indicator {x'} y * p) \count_space UNIV) = ``` eberlm@63099 ` 2056` ``` (\(x', p)\xs. (\\<^sup>+ y. ennreal (indicator {x'} y * p) \count_space UNIV))" ``` eberlm@63099 ` 2057` ``` using Cons(1) by (intro Cons) simp_all ``` eberlm@63099 ` 2058` ``` finally show ?case by (simp add: case_prod_unfold) ``` eberlm@63099 ` 2059` ``` qed simp ``` eberlm@63099 ` 2060` ``` also have "\ = (\(x',p)\xs. ennreal p * (\\<^sup>+ x. indicator {x'} x \count_space UNIV))" ``` eberlm@63099 ` 2061` ``` using assms(1) ``` nipkow@63882 ` 2062` ``` by (intro sum_list_cong, simp only: case_prod_unfold, subst nn_integral_cmult [symmetric]) ``` eberlm@63099 ` 2063` ``` (auto intro!: assms(1) simp: max_def times_ereal.simps [symmetric] mult_ac ereal_indicator ``` eberlm@63099 ` 2064` ``` simp del: times_ereal.simps)+ ``` nipkow@63882 ` 2065` ``` also from assms have "\ = sum_list (map snd xs)" by (simp add: case_prod_unfold sum_list_ennreal) ``` eberlm@63099 ` 2066` ``` also have "\ = 1" using assms(2) by simp ``` eberlm@63099 ` 2067` ``` finally show ?thesis . ``` eberlm@63099 ` 2068` ```qed ``` eberlm@63099 ` 2069` eberlm@63099 ` 2070` ```lemma pmf_pmf_of_list: ``` eberlm@63099 ` 2071` ``` assumes "pmf_of_list_wf xs" ``` nipkow@63882 ` 2072` ``` shows "pmf (pmf_of_list xs) x = sum_list (map snd (filter (\z. fst z = x) xs))" ``` eberlm@63099 ` 2073` ``` using assms pmf_of_list_aux[of xs] unfolding pmf_of_list_def pmf_of_list_wf_def ``` nipkow@63882 ` 2074` ``` by (subst pmf_embed_pmf) (auto intro!: sum_list_nonneg) ``` eberlm@63099 ` 2075` Andreas@61634 ` 2076` ```end ``` eberlm@63099 ` 2077` eberlm@63099 ` 2078` ```lemma set_pmf_of_list: ``` eberlm@63099 ` 2079` ``` assumes "pmf_of_list_wf xs" ``` eberlm@63099 ` 2080` ``` shows "set_pmf (pmf_of_list xs) \ set (map fst xs)" ``` eberlm@63099 ` 2081` ```proof clarify ``` eberlm@63099 ` 2082` ``` fix x assume A: "x \ set_pmf (pmf_of_list xs)" ``` eberlm@63099 ` 2083` ``` show "x \ set (map fst xs)" ``` eberlm@63099 ` 2084` ``` proof (rule ccontr) ``` eberlm@63099 ` 2085` ``` assume "x \ set (map fst xs)" ``` eberlm@63099 ` 2086` ``` hence "[z\xs . fst z = x] = []" by (auto simp: filter_empty_conv) ``` eberlm@63099 ` 2087` ``` with A assms show False by (simp add: pmf_pmf_of_list set_pmf_eq) ``` eberlm@63099 ` 2088` ``` qed ``` eberlm@63099 ` 2089` ```qed ``` eberlm@63099 ` 2090` eberlm@63099 ` 2091` ```lemma finite_set_pmf_of_list: ``` eberlm@63099 ` 2092` ``` assumes "pmf_of_list_wf xs" ``` eberlm@63099 ` 2093` ``` shows "finite (set_pmf (pmf_of_list xs))" ``` eberlm@63099 ` 2094` ``` using assms by (rule finite_subset[OF set_pmf_of_list]) simp_all ``` eberlm@63099 ` 2095` eberlm@63099 ` 2096` ```lemma emeasure_Int_set_pmf: ``` eberlm@63099 ` 2097` ``` "emeasure (measure_pmf p) (A \ set_pmf p) = emeasure (measure_pmf p) A" ``` eberlm@63099 ` 2098` ``` by (rule emeasure_eq_AE) (auto simp: AE_measure_pmf_iff) ``` eberlm@63099 ` 2099` eberlm@63099 ` 2100` ```lemma measure_Int_set_pmf: ``` eberlm@63099 ` 2101` ``` "measure (measure_pmf p) (A \ set_pmf p) = measure (measure_pmf p) A" ``` eberlm@63099 ` 2102` ``` using emeasure_Int_set_pmf[of p A] by (simp add: Sigma_Algebra.measure_def) ``` eberlm@63099 ` 2103` eberlm@66568 ` 2104` ```lemma measure_prob_cong_0: ``` eberlm@66568 ` 2105` ``` assumes "\x. x \ A - B \ pmf p x = 0" ``` eberlm@66568 ` 2106` ``` assumes "\x. x \ B - A \ pmf p x = 0" ``` eberlm@66568 ` 2107` ``` shows "measure (measure_pmf p) A = measure (measure_pmf p) B" ``` eberlm@66568 ` 2108` ```proof - ``` eberlm@66568 ` 2109` ``` have "measure_pmf.prob p A = measure_pmf.prob p (A \ set_pmf p)" ``` eberlm@66568 ` 2110` ``` by (simp add: measure_Int_set_pmf) ``` eberlm@66568 ` 2111` ``` also have "A \ set_pmf p = B \ set_pmf p" ``` eberlm@66568 ` 2112` ``` using assms by (auto simp: set_pmf_eq) ``` eberlm@66568 ` 2113` ``` also have "measure_pmf.prob p \ = measure_pmf.prob p B" ``` eberlm@66568 ` 2114` ``` by (simp add: measure_Int_set_pmf) ``` eberlm@66568 ` 2115` ``` finally show ?thesis . ``` eberlm@66568 ` 2116` ```qed ``` eberlm@66568 ` 2117` eberlm@63099 ` 2118` ```lemma emeasure_pmf_of_list: ``` eberlm@63099 ` 2119` ``` assumes "pmf_of_list_wf xs" ``` nipkow@63882 ` 2120` ``` shows "emeasure (pmf_of_list xs) A = ennreal (sum_list (map snd (filter (\x. fst x \ A) xs)))" ``` eberlm@63099 ` 2121` ```proof - ``` eberlm@63099 ` 2122` ``` have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)" ``` eberlm@63099 ` 2123` ``` by simp ``` hoelzl@63886 ` 2124` ``` also from assms ``` nipkow@63882 ` 2125` ``` have "\ = (\x\set_pmf (pmf_of_list xs) \ A. ennreal (sum_list (map snd [z\xs . fst z = x])))" ``` hoelzl@63973 ` 2126` ``` by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list Int_def) ``` hoelzl@63886 ` 2127` ``` also from assms ``` nipkow@63882 ` 2128` ``` have "\ = ennreal (\x\set_pmf (pmf_of_list xs) \ A. sum_list (map snd [z\xs . fst z = x]))" ``` nipkow@64267 ` 2129` ``` by (subst sum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg) ``` hoelzl@63886 ` 2130` ``` also have "\ = ennreal (\x\set_pmf (pmf_of_list xs) \ A. ``` eberlm@63099 ` 2131` ``` indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S") ``` nipkow@64267 ` 2132` ``` using assms by (intro ennreal_cong sum.cong) (auto simp: pmf_pmf_of_list) ``` eberlm@63099 ` 2133` ``` also have "?S = (\x\set_pmf (pmf_of_list xs). indicator A x * pmf (pmf_of_list xs) x)" ``` nipkow@64267 ` 2134` ``` using assms by (intro sum.mono_neutral_left set_pmf_of_list finite_set_pmf_of_list) auto ``` eberlm@63099 ` 2135` ``` also have "\ = (\x\set (map fst xs). indicator A x * pmf (pmf_of_list xs) x)" ``` nipkow@64267 ` 2136` ``` using assms by (intro sum.mono_neutral_left set_pmf_of_list) (auto simp: set_pmf_eq) ``` hoelzl@63886 ` 2137` ``` also have "\ = (\x\set (map fst xs). indicator A x * ``` nipkow@63882 ` 2138` ``` sum_list (map snd (filter (\z. fst z = x) xs)))" ``` eberlm@63099 ` 2139` ``` using assms by (simp add: pmf_pmf_of_list) ``` nipkow@63882 ` 2140` ``` also have "\ = (\x\set (map fst xs). sum_list (map snd (filter (\z. fst z = x \ x \ A) xs)))" ``` nipkow@64267 ` 2141` ``` by (intro sum.cong) (auto simp: indicator_def) ``` eberlm@63099 ` 2142` ``` also have "\ = (\x\set (map fst xs). (\xa = 0.. x \ A then snd (xs ! xa) else 0))" ``` nipkow@64267 ` 2144` ``` by (intro sum.cong refl, subst sum_list_map_filter', subst sum_list_sum_nth) simp ``` hoelzl@63886 ` 2145` ``` also have "\ = (\xa = 0..x\set (map fst xs). ``` eberlm@63099 ` 2146` ``` if fst (xs ! xa) = x \ x \ A then snd (xs ! xa) else 0))" ``` haftmann@66804 ` 2147` ``` by (rule sum.swap) ``` hoelzl@63886 ` 2148` ``` also have "\ = (\xa = 0.. A then ``` eberlm@63099 ` 2149` ``` (\x\set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)" ``` lp15@66089 ` 2150` ``` by (auto intro!: sum.cong sum.neutral simp del: sum.delta) ``` eberlm@63099 ` 2151` ``` also have "\ = (\xa = 0.. A then snd (xs ! xa) else 0)" ``` nipkow@64267 ` 2152` ``` by (intro sum.cong refl) (simp_all add: sum.delta) ``` nipkow@63882 ` 2153` ``` also have "\ = sum_list (map snd (filter (\x. fst x \ A) xs))" ``` nipkow@64267 ` 2154` ``` by (subst sum_list_map_filter', subst sum_list_sum_nth) simp_all ``` hoelzl@63886 ` 2155` ``` finally show ?thesis . ``` eberlm@63099 ` 2156` ```qed ``` eberlm@63099 ` 2157` eberlm@63099 ` 2158` ```lemma measure_pmf_of_list: ``` eberlm@63099 ` 2159` ``` assumes "pmf_of_list_wf xs" ``` nipkow@63882 ` 2160` ``` shows "measure (pmf_of_list xs) A = sum_list (map snd (filter (\x. fst x \ A) xs))" ``` eberlm@63099 ` 2161` ``` using assms unfolding pmf_of_list_wf_def Sigma_Algebra.measure_def ``` nipkow@63882 ` 2162` ``` by (subst emeasure_pmf_of_list [OF assms], subst enn2real_ennreal) (auto intro!: sum_list_nonneg) ``` eberlm@63099 ` 2163` eberlm@63194 ` 2164` ```(* TODO Move? *) ``` nipkow@63882 ` 2165` ```lemma sum_list_nonneg_eq_zero_iff: ``` eberlm@63194 ` 2166` ``` fixes xs :: "'a :: linordered_ab_group_add list" ``` nipkow@63882 ` 2167` ``` shows "(\x. x \ set xs \ x \ 0) \ sum_list xs = 0 \ set xs \ {0}" ``` eberlm@63194 ` 2168` ```proof (induction xs) ``` eberlm@63194 ` 2169` ``` case (Cons x xs) ``` nipkow@63882 ` 2170` ``` from Cons.prems have "sum_list (x#xs) = 0 \ x = 0 \ sum_list xs = 0" ``` nipkow@63882 ` 2171` ``` unfolding sum_list_simps by (subst add_nonneg_eq_0_iff) (auto intro: sum_list_nonneg) ``` eberlm@63194 ` 2172` ``` with Cons.IH Cons.prems show ?case by simp ``` eberlm@63194 ` 2173` ```qed simp_all ``` eberlm@63194 ` 2174` nipkow@63882 ` 2175` ```lemma sum_list_filter_nonzero: ``` nipkow@63882 ` 2176` ``` "sum_list (filter (\x. x \ 0) xs) = sum_list xs" ``` eberlm@63194 ` 2177` ``` by (induction xs) simp_all ``` eberlm@63194 ` 2178` ```(* END MOVE *) ``` hoelzl@63886 ` 2179` eberlm@63194 ` 2180` ```lemma set_pmf_of_list_eq: ``` eberlm@63194 ` 2181` ``` assumes "pmf_of_list_wf xs" "\x. x \ snd ` set xs \ x > 0" ``` eberlm@63194 ` 2182` ``` shows "set_pmf (pmf_of_list xs) = fst ` set xs" ``` eberlm@63194 ` 2183` ```proof ``` eberlm@63194 ` 2184` ``` { ``` eberlm@63194 ` 2185` ``` fix x assume A: "x \ fst ` set xs" and B: "x \ set_pmf (pmf_of_list xs)" ``` eberlm@63194 ` 2186` ``` then obtain y where y: "(x, y) \ set xs" by auto ``` nipkow@63882 ` 2187` ``` from B have "sum_list (map snd [z\xs. fst z = x]) = 0" ``` eberlm@63194 ` 2188` ``` by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq) ``` eberlm@63194 ` 2189` ``` moreover from y have "y \ snd ` {xa \ set xs. fst xa = x}" by force ``` hoelzl@63886 ` 2190` ``` ultimately have "y = 0" using assms(1) ``` nipkow@63882 ` 2191` ``` by (subst (asm) sum_list_nonneg_eq_zero_iff) (auto simp: pmf_of_list_wf_def) ``` eberlm@63194 ` 2192` ``` with assms(2) y have False by force ``` eberlm@63194 ` 2193` ``` } ``` eberlm@63194 ` 2194` ``` thus "fst ` set xs \ set_pmf (pmf_of_list xs)" by blast ``` eberlm@63194 ` 2195` ```qed (insert set_pmf_of_list[OF assms(1)], simp_all) ``` hoelzl@63886 ` 2196` eberlm@63194 ` 2197` ```lemma pmf_of_list_remove_zeros: ``` eberlm@63194 ` 2198` ``` assumes "pmf_of_list_wf xs" ``` eberlm@63194 ` 2199` ``` defines "xs' \ filter (\z. snd z \ 0) xs" ``` eberlm@63194 ` 2200` ``` shows "pmf_of_list_wf xs'" "pmf_of_list xs' = pmf_of_list xs" ``` eberlm@63194 ` 2201` ```proof - ``` eberlm@63194 ` 2202` ``` have "map snd [z\xs . snd z \ 0] = filter (\x. x \ 0) (map snd xs)" ``` eberlm@63194 ` 2203` ``` by (induction xs) simp_all ``` eberlm@63194 ` 2204` ``` with assms(1) show wf: "pmf_of_list_wf xs'" ``` nipkow@63882 ` 2205` ``` by (auto simp: pmf_of_list_wf_def xs'_def sum_list_filter_nonzero) ``` nipkow@63882 ` 2206` ``` have "sum_list (map snd [z\xs' . fst z = i]) = sum_list (map snd [z\xs . fst z = i])" for i ``` eberlm@63194 ` 2207` ``` unfolding xs'_def by (induction xs) simp_all ``` eberlm@63194 ` 2208` ``` with assms(1) wf show "pmf_of_list xs' = pmf_of_list xs" ``` eberlm@63194 ` 2209` ``` by (intro pmf_eqI) (simp_all add: pmf_pmf_of_list) ``` eberlm@63194 ` 2210` ```qed ``` eberlm@63194 ` 2211` eberlm@63099 ` 2212` ```end ```