src/HOL/Probability/Probability_Mass_Function.thy
 author hoelzl Fri Sep 30 16:08:38 2016 +0200 (2016-09-30) changeset 64008 17a20ca86d62 parent 63973 b09f16aeb694 child 64267 b9a1486e79be permissions -rw-r--r--
HOL-Probability: more about probability, prepare for Markov processes in the AFP
 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 ``` hoelzl@59000 ` 11` ``` "~~/src/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)" ``` hoelzl@62975 ` 208` ``` by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single pmf_nonneg) ``` hoelzl@59000 ` 209` Andreas@59023 ` 210` ```lemma measure_measure_pmf_finite: "finite S \ measure (measure_pmf M) S = setsum (pmf M) S" ``` hoelzl@62975 ` 211` ``` using emeasure_measure_pmf_finite[of S M] ``` hoelzl@62975 ` 212` ``` by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg setsum_nonneg pmf_nonneg) ``` Andreas@59023 ` 213` eberlm@63099 ` 214` ```lemma setsum_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]: ``` hoelzl@59664 ` 450` ``` "rel_fun op = (rel_fun cr_pmf cr_pmf) (\f M. distr M (count_space UNIV) f) map_pmf" ``` hoelzl@59664 ` 451` ```proof - ``` hoelzl@59664 ` 452` ``` have "rel_fun op = (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` hoelzl@59664 ` 479` ```lemma pmf_set_map: "set_pmf \ map_pmf f = op ` 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` Andreas@60068 ` 532` ```lemma map_return_pmf [simp]: "map_pmf f (return_pmf x) = return_pmf (f x)" ``` hoelzl@59664 ` 533` ``` by transfer (simp add: distr_return) ``` hoelzl@59664 ` 534` hoelzl@59664 ` 535` ```lemma map_pmf_const[simp]: "map_pmf (\_. c) M = return_pmf c" ``` hoelzl@59664 ` 536` ``` by transfer (auto simp: prob_space.distr_const) ``` hoelzl@59664 ` 537` Andreas@60068 ` 538` ```lemma pmf_return [simp]: "pmf (return_pmf x) y = indicator {y} x" ``` hoelzl@59664 ` 539` ``` by transfer (simp add: measure_return) ``` hoelzl@59664 ` 540` hoelzl@59664 ` 541` ```lemma nn_integral_return_pmf[simp]: "0 \ f x \ (\\<^sup>+x. f x \return_pmf x) = f x" ``` hoelzl@59664 ` 542` ``` unfolding return_pmf.rep_eq by (intro nn_integral_return) auto ``` hoelzl@59664 ` 543` hoelzl@59664 ` 544` ```lemma emeasure_return_pmf[simp]: "emeasure (return_pmf x) X = indicator X x" ``` hoelzl@59664 ` 545` ``` unfolding return_pmf.rep_eq by (intro emeasure_return) auto ``` hoelzl@59664 ` 546` eberlm@63099 ` 547` ```lemma measure_return_pmf [simp]: "measure_pmf.prob (return_pmf x) A = indicator A x" ``` eberlm@63099 ` 548` ```proof - ``` hoelzl@63886 ` 549` ``` have "ennreal (measure_pmf.prob (return_pmf x) A) = ``` eberlm@63099 ` 550` ``` emeasure (measure_pmf (return_pmf x)) A" ``` eberlm@63099 ` 551` ``` by (simp add: measure_pmf.emeasure_eq_measure) ``` eberlm@63099 ` 552` ``` also have "\ = ennreal (indicator A x)" by (simp add: ennreal_indicator) ``` eberlm@63099 ` 553` ``` finally show ?thesis by simp ``` eberlm@63099 ` 554` ```qed ``` eberlm@63099 ` 555` hoelzl@59664 ` 556` ```lemma return_pmf_inj[simp]: "return_pmf x = return_pmf y \ x = y" ``` hoelzl@59664 ` 557` ``` by (metis insertI1 set_return_pmf singletonD) ``` hoelzl@59664 ` 558` hoelzl@59665 ` 559` ```lemma map_pmf_eq_return_pmf_iff: ``` hoelzl@59665 ` 560` ``` "map_pmf f p = return_pmf x \ (\y \ set_pmf p. f y = x)" ``` hoelzl@59665 ` 561` ```proof ``` hoelzl@59665 ` 562` ``` assume "map_pmf f p = return_pmf x" ``` hoelzl@59665 ` 563` ``` then have "set_pmf (map_pmf f p) = set_pmf (return_pmf x)" by simp ``` hoelzl@59665 ` 564` ``` then show "\y \ set_pmf p. f y = x" by auto ``` hoelzl@59665 ` 565` ```next ``` hoelzl@59665 ` 566` ``` assume "\y \ set_pmf p. f y = x" ``` hoelzl@59665 ` 567` ``` then show "map_pmf f p = return_pmf x" ``` hoelzl@59665 ` 568` ``` unfolding map_pmf_const[symmetric, of _ p] by (intro map_pmf_cong) auto ``` hoelzl@59665 ` 569` ```qed ``` hoelzl@59665 ` 570` hoelzl@59664 ` 571` ```definition "pair_pmf A B = bind_pmf A (\x. bind_pmf B (\y. return_pmf (x, y)))" ``` hoelzl@59664 ` 572` hoelzl@59664 ` 573` ```lemma pmf_pair: "pmf (pair_pmf M N) (a, b) = pmf M a * pmf N b" ``` hoelzl@59664 ` 574` ``` unfolding pair_pmf_def pmf_bind pmf_return ``` hoelzl@64008 ` 575` ``` apply (subst integral_measure_pmf_real[where A="{b}"]) ``` hoelzl@59664 ` 576` ``` apply (auto simp: indicator_eq_0_iff) ``` hoelzl@64008 ` 577` ``` apply (subst integral_measure_pmf_real[where A="{a}"]) ``` hoelzl@59664 ` 578` ``` apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg) ``` hoelzl@59664 ` 579` ``` done ``` hoelzl@59664 ` 580` hoelzl@59665 ` 581` ```lemma set_pair_pmf[simp]: "set_pmf (pair_pmf A B) = set_pmf A \ set_pmf B" ``` hoelzl@59664 ` 582` ``` unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto ``` hoelzl@59664 ` 583` hoelzl@59664 ` 584` ```lemma measure_pmf_in_subprob_space[measurable (raw)]: ``` hoelzl@59664 ` 585` ``` "measure_pmf M \ space (subprob_algebra (count_space UNIV))" ``` hoelzl@59664 ` 586` ``` by (simp add: space_subprob_algebra) intro_locales ``` hoelzl@59664 ` 587` hoelzl@59664 ` 588` ```lemma nn_integral_pair_pmf': "(\\<^sup>+x. f x \pair_pmf A B) = (\\<^sup>+a. \\<^sup>+b. f (a, b) \B \A)" ``` hoelzl@59664 ` 589` ```proof - ``` hoelzl@62975 ` 590` ``` have "(\\<^sup>+x. f x \pair_pmf A B) = (\\<^sup>+x. f x * indicator (A \ B) x \pair_pmf A B)" ``` hoelzl@62975 ` 591` ``` by (auto simp: AE_measure_pmf_iff intro!: nn_integral_cong_AE) ``` hoelzl@62975 ` 592` ``` also have "\ = (\\<^sup>+a. \\<^sup>+b. f (a, b) * indicator (A \ B) (a, b) \B \A)" ``` hoelzl@59664 ` 593` ``` by (simp add: pair_pmf_def) ``` hoelzl@62975 ` 594` ``` also have "\ = (\\<^sup>+a. \\<^sup>+b. f (a, b) \B \A)" ``` hoelzl@59664 ` 595` ``` by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff) ``` hoelzl@62975 ` 596` ``` finally show ?thesis . ``` hoelzl@59664 ` 597` ```qed ``` hoelzl@59664 ` 598` hoelzl@59664 ` 599` ```lemma bind_pair_pmf: ``` hoelzl@59664 ` 600` ``` assumes M[measurable]: "M \ measurable (count_space UNIV \\<^sub>M count_space UNIV) (subprob_algebra N)" ``` wenzelm@62026 ` 601` ``` shows "measure_pmf (pair_pmf A B) \ M = (measure_pmf A \ (\x. measure_pmf B \ (\y. M (x, y))))" ``` hoelzl@59664 ` 602` ``` (is "?L = ?R") ``` hoelzl@59664 ` 603` ```proof (rule measure_eqI) ``` hoelzl@59664 ` 604` ``` have M'[measurable]: "M \ measurable (pair_pmf A B) (subprob_algebra N)" ``` hoelzl@59664 ` 605` ``` using M[THEN measurable_space] by (simp_all add: space_pair_measure) ``` hoelzl@59664 ` 606` hoelzl@59664 ` 607` ``` note measurable_bind[where N="count_space UNIV", measurable] ``` hoelzl@59664 ` 608` ``` note measure_pmf_in_subprob_space[simp] ``` hoelzl@59664 ` 609` hoelzl@59664 ` 610` ``` have sets_eq_N: "sets ?L = N" ``` hoelzl@59664 ` 611` ``` by (subst sets_bind[OF sets_kernel[OF M']]) auto ``` hoelzl@59664 ` 612` ``` show "sets ?L = sets ?R" ``` hoelzl@59664 ` 613` ``` using measurable_space[OF M] ``` hoelzl@59664 ` 614` ``` by (simp add: sets_eq_N space_pair_measure space_subprob_algebra) ``` hoelzl@59664 ` 615` ``` fix X assume "X \ sets ?L" ``` hoelzl@59664 ` 616` ``` then have X[measurable]: "X \ sets N" ``` hoelzl@59664 ` 617` ``` unfolding sets_eq_N . ``` hoelzl@59664 ` 618` ``` then show "emeasure ?L X = emeasure ?R X" ``` hoelzl@59664 ` 619` ``` apply (simp add: emeasure_bind[OF _ M' X]) ``` hoelzl@59664 ` 620` ``` apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A] ``` hoelzl@62975 ` 621` ``` nn_integral_measure_pmf_finite) ``` hoelzl@59664 ` 622` ``` apply (subst emeasure_bind[OF _ _ X]) ``` hoelzl@59664 ` 623` ``` apply measurable ``` hoelzl@59664 ` 624` ``` apply (subst emeasure_bind[OF _ _ X]) ``` hoelzl@59664 ` 625` ``` apply measurable ``` hoelzl@59664 ` 626` ``` done ``` hoelzl@59664 ` 627` ```qed ``` hoelzl@59664 ` 628` hoelzl@59664 ` 629` ```lemma map_fst_pair_pmf: "map_pmf fst (pair_pmf A B) = A" ``` hoelzl@59664 ` 630` ``` by (simp add: pair_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') ``` hoelzl@59664 ` 631` hoelzl@59664 ` 632` ```lemma map_snd_pair_pmf: "map_pmf snd (pair_pmf A B) = B" ``` hoelzl@59664 ` 633` ``` by (simp add: pair_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') ``` hoelzl@59664 ` 634` hoelzl@59664 ` 635` ```lemma nn_integral_pmf': ``` hoelzl@59664 ` 636` ``` "inj_on f A \ (\\<^sup>+x. pmf p (f x) \count_space A) = emeasure p (f ` A)" ``` hoelzl@59664 ` 637` ``` by (subst nn_integral_bij_count_space[where g=f and B="f`A"]) ``` hoelzl@59664 ` 638` ``` (auto simp: bij_betw_def nn_integral_pmf) ``` hoelzl@59664 ` 639` hoelzl@59664 ` 640` ```lemma pmf_le_0_iff[simp]: "pmf M p \ 0 \ pmf M p = 0" ``` hoelzl@62975 ` 641` ``` using pmf_nonneg[of M p] by arith ``` hoelzl@59664 ` 642` hoelzl@59664 ` 643` ```lemma min_pmf_0[simp]: "min (pmf M p) 0 = 0" "min 0 (pmf M p) = 0" ``` hoelzl@62975 ` 644` ``` using pmf_nonneg[of M p] by arith+ ``` hoelzl@59664 ` 645` hoelzl@59664 ` 646` ```lemma pmf_eq_0_set_pmf: "pmf M p = 0 \ p \ set_pmf M" ``` hoelzl@59664 ` 647` ``` unfolding set_pmf_iff by simp ``` hoelzl@59664 ` 648` hoelzl@59664 ` 649` ```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 ` 650` ``` by (auto simp: pmf.rep_eq map_pmf_rep_eq measure_distr AE_measure_pmf_iff inj_onD ``` hoelzl@59664 ` 651` ``` intro!: measure_pmf.finite_measure_eq_AE) ``` hoelzl@59664 ` 652` Andreas@60068 ` 653` ```lemma pmf_map_inj': "inj f \ pmf (map_pmf f M) (f x) = pmf M x" ``` Andreas@60068 ` 654` ```apply(cases "x \ set_pmf M") ``` Andreas@60068 ` 655` ``` apply(simp add: pmf_map_inj[OF subset_inj_on]) ``` Andreas@60068 ` 656` ```apply(simp add: pmf_eq_0_set_pmf[symmetric]) ``` Andreas@60068 ` 657` ```apply(auto simp add: pmf_eq_0_set_pmf dest: injD) ``` Andreas@60068 ` 658` ```done ``` Andreas@60068 ` 659` Andreas@60068 ` 660` ```lemma pmf_map_outside: "x \ f ` set_pmf M \ pmf (map_pmf f M) x = 0" ``` hoelzl@64008 ` 661` ``` unfolding pmf_eq_0_set_pmf by simp ``` hoelzl@64008 ` 662` hoelzl@64008 ` 663` ```lemma measurable_set_pmf[measurable]: "Measurable.pred (count_space UNIV) (\x. x \ set_pmf M)" ``` hoelzl@64008 ` 664` ``` by simp ``` Andreas@60068 ` 665` hoelzl@59664 ` 666` ```subsection \ PMFs as function \ ``` hoelzl@59000 ` 667` hoelzl@58587 ` 668` ```context ``` hoelzl@58587 ` 669` ``` fixes f :: "'a \ real" ``` hoelzl@58587 ` 670` ``` assumes nonneg: "\x. 0 \ f x" ``` hoelzl@58587 ` 671` ``` assumes prob: "(\\<^sup>+x. f x \count_space UNIV) = 1" ``` hoelzl@58587 ` 672` ```begin ``` hoelzl@58587 ` 673` hoelzl@62975 ` 674` ```lift_definition embed_pmf :: "'a pmf" is "density (count_space UNIV) (ennreal \ f)" ``` hoelzl@58587 ` 675` ```proof (intro conjI) ``` hoelzl@62975 ` 676` ``` have *[simp]: "\x y. ennreal (f y) * indicator {x} y = ennreal (f x) * indicator {x} y" ``` hoelzl@58587 ` 677` ``` by (simp split: split_indicator) ``` hoelzl@62975 ` 678` ``` show "AE x in density (count_space UNIV) (ennreal \ f). ``` hoelzl@62975 ` 679` ``` measure (density (count_space UNIV) (ennreal \ f)) {x} \ 0" ``` hoelzl@59092 ` 680` ``` by (simp add: AE_density nonneg measure_def emeasure_density max_def) ``` hoelzl@62975 ` 681` ``` show "prob_space (density (count_space UNIV) (ennreal \ f))" ``` wenzelm@61169 ` 682` ``` by standard (simp add: emeasure_density prob) ``` hoelzl@58587 ` 683` ```qed simp ``` hoelzl@58587 ` 684` hoelzl@58587 ` 685` ```lemma pmf_embed_pmf: "pmf embed_pmf x = f x" ``` hoelzl@58587 ` 686` ```proof transfer ``` hoelzl@62975 ` 687` ``` have *[simp]: "\x y. ennreal (f y) * indicator {x} y = ennreal (f x) * indicator {x} y" ``` hoelzl@58587 ` 688` ``` by (simp split: split_indicator) ``` hoelzl@62975 ` 689` ``` fix x show "measure (density (count_space UNIV) (ennreal \ f)) {x} = f x" ``` hoelzl@59092 ` 690` ``` by transfer (simp add: measure_def emeasure_density nonneg max_def) ``` hoelzl@58587 ` 691` ```qed ``` hoelzl@58587 ` 692` Andreas@60068 ` 693` ```lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \ 0}" ``` wenzelm@63092 ` 694` ```by(auto simp add: set_pmf_eq pmf_embed_pmf) ``` Andreas@60068 ` 695` hoelzl@58587 ` 696` ```end ``` hoelzl@58587 ` 697` hoelzl@58587 ` 698` ```lemma embed_pmf_transfer: ``` hoelzl@62975 ` 699` ``` "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 ` 700` ``` by (auto simp: rel_fun_def eq_onp_def embed_pmf.transfer) ``` hoelzl@58587 ` 701` hoelzl@59000 ` 702` ```lemma measure_pmf_eq_density: "measure_pmf p = density (count_space UNIV) (pmf p)" ``` hoelzl@59000 ` 703` ```proof (transfer, elim conjE) ``` hoelzl@59000 ` 704` ``` fix M :: "'a measure" assume [simp]: "sets M = UNIV" and ae: "AE x in M. measure M {x} \ 0" ``` hoelzl@59000 ` 705` ``` assume "prob_space M" then interpret prob_space M . ``` hoelzl@62975 ` 706` ``` show "M = density (count_space UNIV) (\x. ennreal (measure M {x}))" ``` hoelzl@59000 ` 707` ``` proof (rule measure_eqI) ``` hoelzl@59000 ` 708` ``` fix A :: "'a set" ``` hoelzl@62975 ` 709` ``` have "(\\<^sup>+ x. ennreal (measure M {x}) * indicator A x \count_space UNIV) = ``` hoelzl@59000 ` 710` ``` (\\<^sup>+ x. emeasure M {x} * indicator (A \ {x. measure M {x} \ 0}) x \count_space UNIV)" ``` hoelzl@59000 ` 711` ``` by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator) ``` hoelzl@59000 ` 712` ``` also have "\ = (\\<^sup>+ x. emeasure M {x} \count_space (A \ {x. measure M {x} \ 0}))" ``` hoelzl@59000 ` 713` ``` by (subst nn_integral_restrict_space[symmetric]) (auto simp: restrict_count_space) ``` hoelzl@59000 ` 714` ``` also have "\ = emeasure M (\x\(A \ {x. measure M {x} \ 0}). {x})" ``` hoelzl@59000 ` 715` ``` by (intro emeasure_UN_countable[symmetric] countable_Int2 countable_support) ``` hoelzl@59000 ` 716` ``` (auto simp: disjoint_family_on_def) ``` hoelzl@59000 ` 717` ``` also have "\ = emeasure M A" ``` hoelzl@59000 ` 718` ``` using ae by (intro emeasure_eq_AE) auto ``` hoelzl@62975 ` 719` ``` finally show " emeasure M A = emeasure (density (count_space UNIV) (\x. ennreal (measure M {x}))) A" ``` hoelzl@59000 ` 720` ``` using emeasure_space_1 by (simp add: emeasure_density) ``` hoelzl@59000 ` 721` ``` qed simp ``` hoelzl@59000 ` 722` ```qed ``` hoelzl@59000 ` 723` hoelzl@58587 ` 724` ```lemma td_pmf_embed_pmf: ``` hoelzl@62975 ` 725` ``` "type_definition pmf embed_pmf {f::'a \ real. (\x. 0 \ f x) \ (\\<^sup>+x. ennreal (f x) \count_space UNIV) = 1}" ``` hoelzl@58587 ` 726` ``` unfolding type_definition_def ``` hoelzl@58587 ` 727` ```proof safe ``` hoelzl@58587 ` 728` ``` fix p :: "'a pmf" ``` hoelzl@58587 ` 729` ``` have "(\\<^sup>+ x. 1 \measure_pmf p) = 1" ``` hoelzl@58587 ` 730` ``` using measure_pmf.emeasure_space_1[of p] by simp ``` hoelzl@62975 ` 731` ``` then show *: "(\\<^sup>+ x. ennreal (pmf p x) \count_space UNIV) = 1" ``` hoelzl@58587 ` 732` ``` by (simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg del: nn_integral_const) ``` hoelzl@58587 ` 733` hoelzl@58587 ` 734` ``` show "embed_pmf (pmf p) = p" ``` hoelzl@58587 ` 735` ``` by (intro measure_pmf_inject[THEN iffD1]) ``` hoelzl@58587 ` 736` ``` (simp add: * embed_pmf.rep_eq pmf_nonneg measure_pmf_eq_density[of p] comp_def) ``` hoelzl@58587 ` 737` ```next ``` hoelzl@58587 ` 738` ``` fix f :: "'a \ real" assume "\x. 0 \ f x" "(\\<^sup>+x. f x \count_space UNIV) = 1" ``` hoelzl@58587 ` 739` ``` then show "pmf (embed_pmf f) = f" ``` hoelzl@58587 ` 740` ``` by (auto intro!: pmf_embed_pmf) ``` hoelzl@58587 ` 741` ```qed (rule pmf_nonneg) ``` hoelzl@58587 ` 742` hoelzl@58587 ` 743` ```end ``` hoelzl@58587 ` 744` hoelzl@62975 ` 745` ```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 ` 746` ```by(simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg) ``` Andreas@60068 ` 747` hoelzl@64008 ` 748` ```lemma integral_measure_pmf: ``` hoelzl@64008 ` 749` ``` fixes f :: "'a \ 'b::{banach, second_countable_topology}" ``` hoelzl@64008 ` 750` ``` assumes A: "finite A" ``` hoelzl@64008 ` 751` ``` 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 ` 752` ``` unfolding measure_pmf_eq_density ``` hoelzl@64008 ` 753` ``` apply (simp add: integral_density) ``` hoelzl@64008 ` 754` ``` apply (subst lebesgue_integral_count_space_finite_support) ``` hoelzl@64008 ` 755` ``` apply (auto intro!: finite_subset[OF _ \finite A\] setsum.mono_neutral_left simp: pmf_eq_0_set_pmf) ``` hoelzl@64008 ` 756` ``` done ``` hoelzl@64008 ` 757` hoelzl@64008 ` 758` ```lemma continuous_on_LINT_pmf: -- \This is dominated convergence!?\ ``` hoelzl@64008 ` 759` ``` fixes f :: "'i \ 'a::topological_space \ 'b::{banach, second_countable_topology}" ``` hoelzl@64008 ` 760` ``` assumes f: "\i. i \ set_pmf M \ continuous_on A (f i)" ``` hoelzl@64008 ` 761` ``` and bnd: "\a i. a \ A \ i \ set_pmf M \ norm (f i a) \ B" ``` hoelzl@64008 ` 762` ``` shows "continuous_on A (\a. LINT i|M. f i a)" ``` hoelzl@64008 ` 763` ```proof cases ``` hoelzl@64008 ` 764` ``` assume "finite M" with f show ?thesis ``` hoelzl@64008 ` 765` ``` using integral_measure_pmf[OF \finite M\] ``` hoelzl@64008 ` 766` ``` by (subst integral_measure_pmf[OF \finite M\]) ``` hoelzl@64008 ` 767` ``` (auto intro!: continuous_on_setsum continuous_on_scaleR continuous_on_const) ``` hoelzl@64008 ` 768` ```next ``` hoelzl@64008 ` 769` ``` assume "infinite M" ``` hoelzl@64008 ` 770` ``` let ?f = "\i x. pmf (map_pmf (to_nat_on M) M) i *\<^sub>R f (from_nat_into M i) x" ``` hoelzl@64008 ` 771` hoelzl@64008 ` 772` ``` show ?thesis ``` hoelzl@64008 ` 773` ``` proof (rule uniform_limit_theorem) ``` hoelzl@64008 ` 774` ``` show "\\<^sub>F n in sequentially. continuous_on A (\a. \in a. \ia. LINT i|M. f i a) sequentially" ``` hoelzl@64008 ` 778` ``` proof (subst uniform_limit_cong[where g="\n a. \i A" ``` hoelzl@64008 ` 780` ``` 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 ` 781` ``` by (auto intro!: integral_cong_AE AE_pmfI) ``` hoelzl@64008 ` 782` ``` 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 ` 783` ``` by (simp add: measure_pmf_eq_density integral_density) ``` hoelzl@64008 ` 784` ``` have "(\n. ?f n a) sums (LINT i|M. f i a)" ``` hoelzl@64008 ` 785` ``` unfolding 1 2 ``` hoelzl@64008 ` 786` ``` proof (intro sums_integral_count_space_nat) ``` hoelzl@64008 ` 787` ``` have A: "integrable M (\i. f i a)" ``` hoelzl@64008 ` 788` ``` using \a\A\ by (auto intro!: measure_pmf.integrable_const_bound AE_pmfI bnd) ``` hoelzl@64008 ` 789` ``` have "integrable (map_pmf (to_nat_on M) M) (\i. f (from_nat_into M i) a)" ``` hoelzl@64008 ` 790` ``` by (auto simp add: map_pmf_rep_eq integrable_distr_eq intro!: AE_pmfI integrable_cong_AE_imp[OF A]) ``` hoelzl@64008 ` 791` ``` then show "integrable (count_space UNIV) (\n. ?f n a)" ``` hoelzl@64008 ` 792` ``` by (simp add: measure_pmf_eq_density integrable_density) ``` hoelzl@64008 ` 793` ``` qed ``` hoelzl@64008 ` 794` ``` then show "(LINT i|M. f i a) = (\ n. ?f n a)" ``` hoelzl@64008 ` 795` ``` by (simp add: sums_unique) ``` hoelzl@64008 ` 796` ``` next ``` hoelzl@64008 ` 797` ``` show "uniform_limit A (\n a. \ia. (\ n. ?f n a)) sequentially" ``` hoelzl@64008 ` 798` ``` proof (rule weierstrass_m_test) ``` hoelzl@64008 ` 799` ``` fix n a assume "a\A" ``` hoelzl@64008 ` 800` ``` then show "norm (?f n a) \ pmf (map_pmf (to_nat_on M) M) n * B" ``` hoelzl@64008 ` 801` ``` using bnd by (auto intro!: mult_mono simp: from_nat_into set_pmf_not_empty) ``` hoelzl@64008 ` 802` ``` next ``` hoelzl@64008 ` 803` ``` have "integrable (map_pmf (to_nat_on M) M) (\n. B)" ``` hoelzl@64008 ` 804` ``` by auto ``` hoelzl@64008 ` 805` ``` then show "summable (\n. pmf (map_pmf (to_nat_on (set_pmf M)) M) n * B)" ``` hoelzl@64008 ` 806` ``` by (simp add: measure_pmf_eq_density integrable_density integrable_count_space_nat_iff summable_rabs_cancel) ``` hoelzl@64008 ` 807` ``` qed ``` hoelzl@64008 ` 808` ``` qed simp ``` hoelzl@64008 ` 809` ``` qed simp ``` hoelzl@64008 ` 810` ```qed ``` hoelzl@64008 ` 811` hoelzl@64008 ` 812` ```lemma continuous_on_LBINT: ``` hoelzl@64008 ` 813` ``` fixes f :: "real \ real" ``` hoelzl@64008 ` 814` ``` assumes f: "\b. a \ b \ set_integrable lborel {a..b} f" ``` hoelzl@64008 ` 815` ``` shows "continuous_on UNIV (\b. LBINT x:{a..b}. f x)" ``` hoelzl@64008 ` 816` ```proof (subst set_borel_integral_eq_integral) ``` hoelzl@64008 ` 817` ``` { fix b :: real assume "a \ b" ``` hoelzl@64008 ` 818` ``` from f[OF this] have "continuous_on {a..b} (\b. integral {a..b} f)" ``` hoelzl@64008 ` 819` ``` by (intro indefinite_integral_continuous set_borel_integral_eq_integral) } ``` hoelzl@64008 ` 820` ``` note * = this ``` hoelzl@64008 ` 821` hoelzl@64008 ` 822` ``` have "continuous_on (\b\{a..}. {a <..< b}) (\b. integral {a..b} f)" ``` hoelzl@64008 ` 823` ``` proof (intro continuous_on_open_UN) ``` hoelzl@64008 ` 824` ``` show "b \ {a..} \ continuous_on {a<..b. integral {a..b} f)" for b ``` hoelzl@64008 ` 825` ``` using *[of b] by (rule continuous_on_subset) auto ``` hoelzl@64008 ` 826` ``` qed simp ``` hoelzl@64008 ` 827` ``` also have "(\b\{a..}. {a <..< b}) = {a <..}" ``` hoelzl@64008 ` 828` ``` 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 ` 829` ``` finally have "continuous_on {a+1 ..} (\b. integral {a..b} f)" ``` hoelzl@64008 ` 830` ``` by (rule continuous_on_subset) auto ``` hoelzl@64008 ` 831` ``` moreover have "continuous_on {a..a+1} (\b. integral {a..b} f)" ``` hoelzl@64008 ` 832` ``` by (rule *) simp ``` hoelzl@64008 ` 833` ``` moreover ``` hoelzl@64008 ` 834` ``` have "x \ a \ {a..x} = (if a = x then {a} else {})" for x ``` hoelzl@64008 ` 835` ``` by auto ``` hoelzl@64008 ` 836` ``` then have "continuous_on {..a} (\b. integral {a..b} f)" ``` hoelzl@64008 ` 837` ``` by (subst continuous_on_cong[OF refl, where g="\x. 0"]) (auto intro!: continuous_on_const) ``` hoelzl@64008 ` 838` ``` ultimately have "continuous_on ({..a} \ {a..a+1} \ {a+1 ..}) (\b. integral {a..b} f)" ``` hoelzl@64008 ` 839` ``` by (intro continuous_on_closed_Un) auto ``` hoelzl@64008 ` 840` ``` also have "{..a} \ {a..a+1} \ {a+1 ..} = UNIV" ``` hoelzl@64008 ` 841` ``` by auto ``` hoelzl@64008 ` 842` ``` finally show "continuous_on UNIV (\b. integral {a..b} f)" ``` hoelzl@64008 ` 843` ``` by auto ``` hoelzl@64008 ` 844` ```next ``` hoelzl@64008 ` 845` ``` show "set_integrable lborel {a..b} f" for b ``` hoelzl@64008 ` 846` ``` using f by (cases "a \ b") auto ``` hoelzl@64008 ` 847` ```qed ``` hoelzl@64008 ` 848` hoelzl@58587 ` 849` ```locale pmf_as_function ``` hoelzl@58587 ` 850` ```begin ``` hoelzl@58587 ` 851` hoelzl@58587 ` 852` ```setup_lifting td_pmf_embed_pmf ``` hoelzl@58587 ` 853` lp15@59667 ` 854` ```lemma set_pmf_transfer[transfer_rule]: ``` hoelzl@58730 ` 855` ``` assumes "bi_total A" ``` lp15@59667 ` 856` ``` shows "rel_fun (pcr_pmf A) (rel_set A) (\f. {x. f x \ 0}) set_pmf" ``` wenzelm@61808 ` 857` ``` using \bi_total A\ ``` hoelzl@58730 ` 858` ``` 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 ` 859` ``` metis+ ``` hoelzl@58730 ` 860` hoelzl@59000 ` 861` ```end ``` hoelzl@59000 ` 862` hoelzl@59000 ` 863` ```context ``` hoelzl@59000 ` 864` ```begin ``` hoelzl@59000 ` 865` hoelzl@59000 ` 866` ```interpretation pmf_as_function . ``` hoelzl@59000 ` 867` hoelzl@59000 ` 868` ```lemma pmf_eqI: "(\i. pmf M i = pmf N i) \ M = N" ``` hoelzl@59000 ` 869` ``` by transfer auto ``` hoelzl@59000 ` 870` hoelzl@59000 ` 871` ```lemma pmf_eq_iff: "M = N \ (\i. pmf M i = pmf N i)" ``` hoelzl@59000 ` 872` ``` by (auto intro: pmf_eqI) ``` hoelzl@59000 ` 873` eberlm@63099 ` 874` ```lemma pmf_neq_exists_less: ``` eberlm@63099 ` 875` ``` assumes "M \ N" ``` eberlm@63099 ` 876` ``` shows "\x. pmf M x < pmf N x" ``` eberlm@63099 ` 877` ```proof (rule ccontr) ``` eberlm@63099 ` 878` ``` assume "\(\x. pmf M x < pmf N x)" ``` eberlm@63099 ` 879` ``` hence ge: "pmf M x \ pmf N x" for x by (auto simp: not_less) ``` eberlm@63099 ` 880` ``` from assms obtain x where "pmf M x \ pmf N x" by (auto simp: pmf_eq_iff) ``` eberlm@63099 ` 881` ``` with ge[of x] have gt: "pmf M x > pmf N x" by simp ``` eberlm@63099 ` 882` ``` have "1 = measure (measure_pmf M) UNIV" by simp ``` eberlm@63099 ` 883` ``` also have "\ = measure (measure_pmf N) {x} + measure (measure_pmf N) (UNIV - {x})" ``` eberlm@63099 ` 884` ``` by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all ``` hoelzl@63886 ` 885` ``` also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}" ``` eberlm@63099 ` 886` ``` by (simp add: measure_pmf_single) ``` eberlm@63099 ` 887` ``` also have "measure (measure_pmf N) (UNIV - {x}) \ measure (measure_pmf M) (UNIV - {x})" ``` hoelzl@63886 ` 888` ``` by (subst (1 2) integral_pmf [symmetric]) ``` eberlm@63099 ` 889` ``` (intro integral_mono integrable_pmf, simp_all add: ge) ``` eberlm@63099 ` 890` ``` also have "measure (measure_pmf M) {x} + \ = 1" ``` eberlm@63099 ` 891` ``` by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all ``` eberlm@63099 ` 892` ``` finally show False by simp_all ``` eberlm@63099 ` 893` ```qed ``` eberlm@63099 ` 894` hoelzl@59664 ` 895` ```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 ` 896` ``` unfolding pmf_eq_iff pmf_bind ``` hoelzl@59664 ` 897` ```proof ``` hoelzl@59664 ` 898` ``` fix i ``` hoelzl@59664 ` 899` ``` interpret B: prob_space "restrict_space B B" ``` hoelzl@59664 ` 900` ``` by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) ``` hoelzl@59664 ` 901` ``` (auto simp: AE_measure_pmf_iff) ``` hoelzl@59664 ` 902` ``` interpret A: prob_space "restrict_space A A" ``` hoelzl@59664 ` 903` ``` by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) ``` hoelzl@59664 ` 904` ``` (auto simp: AE_measure_pmf_iff) ``` hoelzl@59664 ` 905` hoelzl@59664 ` 906` ``` interpret AB: pair_prob_space "restrict_space A A" "restrict_space B B" ``` hoelzl@59664 ` 907` ``` by unfold_locales ``` hoelzl@59664 ` 908` hoelzl@59664 ` 909` ``` have "(\ x. \ y. pmf (C x y) i \B \A) = (\ x. (\ y. pmf (C x y) i \restrict_space B B) \A)" ``` hoelzl@63886 ` 910` ``` by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict) ``` hoelzl@59664 ` 911` ``` also have "\ = (\ x. (\ y. pmf (C x y) i \restrict_space B B) \restrict_space A A)" ``` hoelzl@59664 ` 912` ``` by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2 ``` hoelzl@59664 ` 913` ``` countable_set_pmf borel_measurable_count_space) ``` hoelzl@59664 ` 914` ``` also have "\ = (\ y. \ x. pmf (C x y) i \restrict_space A A \restrict_space B B)" ``` hoelzl@59664 ` 915` ``` by (rule AB.Fubini_integral[symmetric]) ``` hoelzl@59664 ` 916` ``` (auto intro!: AB.integrable_const_bound[where B=1] measurable_pair_restrict_pmf2 ``` hoelzl@59664 ` 917` ``` simp: pmf_nonneg pmf_le_1 measurable_restrict_space1) ``` hoelzl@59664 ` 918` ``` also have "\ = (\ y. \ x. pmf (C x y) i \restrict_space A A \B)" ``` hoelzl@59664 ` 919` ``` by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2 ``` hoelzl@59664 ` 920` ``` countable_set_pmf borel_measurable_count_space) ``` hoelzl@59664 ` 921` ``` also have "\ = (\ y. \ x. pmf (C x y) i \A \B)" ``` hoelzl@63886 ` 922` ``` by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict[symmetric]) ``` hoelzl@59664 ` 923` ``` finally show "(\ x. \ y. pmf (C x y) i \B \A) = (\ y. \ x. pmf (C x y) i \A \B)" . ``` hoelzl@59664 ` 924` ```qed ``` hoelzl@59664 ` 925` hoelzl@59664 ` 926` ```lemma pair_map_pmf1: "pair_pmf (map_pmf f A) B = map_pmf (apfst f) (pair_pmf A B)" ``` hoelzl@59664 ` 927` ```proof (safe intro!: pmf_eqI) ``` hoelzl@59664 ` 928` ``` fix a :: "'a" and b :: "'b" ``` hoelzl@62975 ` 929` ``` have [simp]: "\c d. indicator (apfst f -` {(a, b)}) (c, d) = indicator (f -` {a}) c * (indicator {b} d::ennreal)" ``` hoelzl@59664 ` 930` ``` by (auto split: split_indicator) ``` hoelzl@59664 ` 931` hoelzl@62975 ` 932` ``` have "ennreal (pmf (pair_pmf (map_pmf f A) B) (a, b)) = ``` hoelzl@62975 ` 933` ``` ennreal (pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b))" ``` hoelzl@62975 ` 934` ``` unfolding pmf_pair ennreal_pmf_map ``` hoelzl@59664 ` 935` ``` by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_multc pmf_nonneg ``` hoelzl@62975 ` 936` ``` emeasure_map_pmf[symmetric] ennreal_mult del: emeasure_map_pmf) ``` hoelzl@59664 ` 937` ``` 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 ` 938` ``` by (simp add: pmf_nonneg) ``` hoelzl@59664 ` 939` ```qed ``` hoelzl@59664 ` 940` hoelzl@59664 ` 941` ```lemma pair_map_pmf2: "pair_pmf A (map_pmf f B) = map_pmf (apsnd f) (pair_pmf A B)" ``` hoelzl@59664 ` 942` ```proof (safe intro!: pmf_eqI) ``` hoelzl@59664 ` 943` ``` fix a :: "'a" and b :: "'b" ``` hoelzl@62975 ` 944` ``` have [simp]: "\c d. indicator (apsnd f -` {(a, b)}) (c, d) = indicator {a} c * (indicator (f -` {b}) d::ennreal)" ``` hoelzl@59664 ` 945` ``` by (auto split: split_indicator) ``` hoelzl@59664 ` 946` hoelzl@62975 ` 947` ``` have "ennreal (pmf (pair_pmf A (map_pmf f B)) (a, b)) = ``` hoelzl@62975 ` 948` ``` ennreal (pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b))" ``` hoelzl@62975 ` 949` ``` unfolding pmf_pair ennreal_pmf_map ``` hoelzl@59664 ` 950` ``` by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_cmult nn_integral_multc pmf_nonneg ``` hoelzl@62975 ` 951` ``` emeasure_map_pmf[symmetric] ennreal_mult del: emeasure_map_pmf) ``` hoelzl@59664 ` 952` ``` 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 ` 953` ``` by (simp add: pmf_nonneg) ``` hoelzl@59664 ` 954` ```qed ``` hoelzl@59664 ` 955` hoelzl@59664 ` 956` ```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 ` 957` ``` by (simp add: pair_map_pmf2 pair_map_pmf1 map_pmf_comp split_beta') ``` hoelzl@59664 ` 958` hoelzl@59000 ` 959` ```end ``` hoelzl@59000 ` 960` Andreas@61634 ` 961` ```lemma pair_return_pmf1: "pair_pmf (return_pmf x) y = map_pmf (Pair x) y" ``` Andreas@61634 ` 962` ```by(simp add: pair_pmf_def bind_return_pmf map_pmf_def) ``` Andreas@61634 ` 963` Andreas@61634 ` 964` ```lemma pair_return_pmf2: "pair_pmf x (return_pmf y) = map_pmf (\x. (x, y)) x" ``` Andreas@61634 ` 965` ```by(simp add: pair_pmf_def bind_return_pmf map_pmf_def) ``` Andreas@61634 ` 966` Andreas@61634 ` 967` ```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 ` 968` ```by(simp add: pair_pmf_def bind_return_pmf map_pmf_def bind_assoc_pmf) ``` Andreas@61634 ` 969` Andreas@61634 ` 970` ```lemma pair_commute_pmf: "pair_pmf x y = map_pmf (\(x, y). (y, x)) (pair_pmf y x)" ``` Andreas@61634 ` 971` ```unfolding pair_pmf_def by(subst bind_commute_pmf)(simp add: map_pmf_def bind_assoc_pmf bind_return_pmf) ``` Andreas@61634 ` 972` Andreas@61634 ` 973` ```lemma set_pmf_subset_singleton: "set_pmf p \ {x} \ p = return_pmf x" ``` Andreas@61634 ` 974` ```proof(intro iffI pmf_eqI) ``` Andreas@61634 ` 975` ``` fix i ``` Andreas@61634 ` 976` ``` assume x: "set_pmf p \ {x}" ``` Andreas@61634 ` 977` ``` hence *: "set_pmf p = {x}" using set_pmf_not_empty[of p] by auto ``` hoelzl@62975 ` 978` ``` have "ennreal (pmf p x) = \\<^sup>+ i. indicator {x} i \p" by(simp add: emeasure_pmf_single) ``` Andreas@61634 ` 979` ``` also have "\ = \\<^sup>+ i. 1 \p" by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * ) ``` Andreas@61634 ` 980` ``` also have "\ = 1" by simp ``` Andreas@61634 ` 981` ``` finally show "pmf p i = pmf (return_pmf x) i" using x ``` Andreas@61634 ` 982` ``` by(auto split: split_indicator simp add: pmf_eq_0_set_pmf) ``` Andreas@61634 ` 983` ```qed auto ``` Andreas@61634 ` 984` Andreas@61634 ` 985` ```lemma bind_eq_return_pmf: ``` Andreas@61634 ` 986` ``` "bind_pmf p f = return_pmf x \ (\y\set_pmf p. f y = return_pmf x)" ``` Andreas@61634 ` 987` ``` (is "?lhs \ ?rhs") ``` Andreas@61634 ` 988` ```proof(intro iffI strip) ``` Andreas@61634 ` 989` ``` fix y ``` Andreas@61634 ` 990` ``` assume y: "y \ set_pmf p" ``` Andreas@61634 ` 991` ``` assume "?lhs" ``` Andreas@61634 ` 992` ``` hence "set_pmf (bind_pmf p f) = {x}" by simp ``` Andreas@61634 ` 993` ``` hence "(\y\set_pmf p. set_pmf (f y)) = {x}" by simp ``` Andreas@61634 ` 994` ``` hence "set_pmf (f y) \ {x}" using y by auto ``` Andreas@61634 ` 995` ``` thus "f y = return_pmf x" by(simp add: set_pmf_subset_singleton) ``` Andreas@61634 ` 996` ```next ``` Andreas@61634 ` 997` ``` assume *: ?rhs ``` Andreas@61634 ` 998` ``` show ?lhs ``` Andreas@61634 ` 999` ``` proof(rule pmf_eqI) ``` Andreas@61634 ` 1000` ``` fix i ``` hoelzl@62975 ` 1001` ``` have "ennreal (pmf (bind_pmf p f) i) = \\<^sup>+ y. ennreal (pmf (f y) i) \p" ``` hoelzl@62975 ` 1002` ``` by (simp add: ennreal_pmf_bind) ``` hoelzl@62975 ` 1003` ``` also have "\ = \\<^sup>+ y. ennreal (pmf (return_pmf x) i) \p" ``` Andreas@61634 ` 1004` ``` by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * ) ``` hoelzl@62975 ` 1005` ``` also have "\ = ennreal (pmf (return_pmf x) i)" ``` hoelzl@62975 ` 1006` ``` by simp ``` hoelzl@62975 ` 1007` ``` finally show "pmf (bind_pmf p f) i = pmf (return_pmf x) i" ``` hoelzl@62975 ` 1008` ``` by (simp add: pmf_nonneg) ``` Andreas@61634 ` 1009` ``` qed ``` Andreas@61634 ` 1010` ```qed ``` Andreas@61634 ` 1011` Andreas@61634 ` 1012` ```lemma pmf_False_conv_True: "pmf p False = 1 - pmf p True" ``` Andreas@61634 ` 1013` ```proof - ``` Andreas@61634 ` 1014` ``` have "pmf p False + pmf p True = measure p {False} + measure p {True}" ``` Andreas@61634 ` 1015` ``` by(simp add: measure_pmf_single) ``` Andreas@61634 ` 1016` ``` also have "\ = measure p ({False} \ {True})" ``` Andreas@61634 ` 1017` ``` by(subst measure_pmf.finite_measure_Union) simp_all ``` Andreas@61634 ` 1018` ``` also have "{False} \ {True} = space p" by auto ``` Andreas@61634 ` 1019` ``` finally show ?thesis by simp ``` Andreas@61634 ` 1020` ```qed ``` Andreas@61634 ` 1021` Andreas@61634 ` 1022` ```lemma pmf_True_conv_False: "pmf p True = 1 - pmf p False" ``` Andreas@61634 ` 1023` ```by(simp add: pmf_False_conv_True) ``` Andreas@61634 ` 1024` hoelzl@59664 ` 1025` ```subsection \ Conditional Probabilities \ ``` hoelzl@59664 ` 1026` hoelzl@59670 ` 1027` ```lemma measure_pmf_zero_iff: "measure (measure_pmf p) s = 0 \ set_pmf p \ s = {}" ``` hoelzl@59670 ` 1028` ``` by (subst measure_pmf.prob_eq_0) (auto simp: AE_measure_pmf_iff) ``` hoelzl@59670 ` 1029` hoelzl@59664 ` 1030` ```context ``` hoelzl@59664 ` 1031` ``` fixes p :: "'a pmf" and s :: "'a set" ``` hoelzl@59664 ` 1032` ``` assumes not_empty: "set_pmf p \ s \ {}" ``` hoelzl@59664 ` 1033` ```begin ``` hoelzl@59664 ` 1034` hoelzl@59664 ` 1035` ```interpretation pmf_as_measure . ``` hoelzl@59664 ` 1036` hoelzl@59664 ` 1037` ```lemma emeasure_measure_pmf_not_zero: "emeasure (measure_pmf p) s \ 0" ``` hoelzl@59664 ` 1038` ```proof ``` hoelzl@59664 ` 1039` ``` assume "emeasure (measure_pmf p) s = 0" ``` hoelzl@59664 ` 1040` ``` then have "AE x in measure_pmf p. x \ s" ``` hoelzl@59664 ` 1041` ``` by (rule AE_I[rotated]) auto ``` hoelzl@59664 ` 1042` ``` with not_empty show False ``` hoelzl@59664 ` 1043` ``` by (auto simp: AE_measure_pmf_iff) ``` hoelzl@59664 ` 1044` ```qed ``` hoelzl@59664 ` 1045` hoelzl@59664 ` 1046` ```lemma measure_measure_pmf_not_zero: "measure (measure_pmf p) s \ 0" ``` hoelzl@62975 ` 1047` ``` using emeasure_measure_pmf_not_zero by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg) ``` hoelzl@59664 ` 1048` hoelzl@59664 ` 1049` ```lift_definition cond_pmf :: "'a pmf" is ``` hoelzl@59664 ` 1050` ``` "uniform_measure (measure_pmf p) s" ``` hoelzl@59664 ` 1051` ```proof (intro conjI) ``` hoelzl@59664 ` 1052` ``` show "prob_space (uniform_measure (measure_pmf p) s)" ``` hoelzl@59664 ` 1053` ``` by (intro prob_space_uniform_measure) (auto simp: emeasure_measure_pmf_not_zero) ``` hoelzl@59664 ` 1054` ``` show "AE x in uniform_measure (measure_pmf p) s. measure (uniform_measure (measure_pmf p) s) {x} \ 0" ``` hoelzl@59664 ` 1055` ``` by (simp add: emeasure_measure_pmf_not_zero measure_measure_pmf_not_zero AE_uniform_measure ``` hoelzl@62975 ` 1056` ``` AE_measure_pmf_iff set_pmf.rep_eq less_top[symmetric]) ``` hoelzl@59664 ` 1057` ```qed simp ``` hoelzl@59664 ` 1058` hoelzl@59664 ` 1059` ```lemma pmf_cond: "pmf cond_pmf x = (if x \ s then pmf p x / measure p s else 0)" ``` hoelzl@59664 ` 1060` ``` by transfer (simp add: emeasure_measure_pmf_not_zero pmf.rep_eq) ``` hoelzl@59664 ` 1061` hoelzl@59665 ` 1062` ```lemma set_cond_pmf[simp]: "set_pmf cond_pmf = set_pmf p \ s" ``` nipkow@62390 ` 1063` ``` by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: if_split_asm) ``` hoelzl@59664 ` 1064` hoelzl@59664 ` 1065` ```end ``` hoelzl@59664 ` 1066` eberlm@63099 ` 1067` ```lemma measure_pmf_posI: "x \ set_pmf p \ x \ A \ measure_pmf.prob p A > 0" ``` eberlm@63099 ` 1068` ``` using measure_measure_pmf_not_zero[of p A] by (subst zero_less_measure_iff) blast ``` eberlm@63099 ` 1069` hoelzl@59664 ` 1070` ```lemma cond_map_pmf: ``` hoelzl@59664 ` 1071` ``` assumes "set_pmf p \ f -` s \ {}" ``` hoelzl@59664 ` 1072` ``` shows "cond_pmf (map_pmf f p) s = map_pmf f (cond_pmf p (f -` s))" ``` hoelzl@59664 ` 1073` ```proof - ``` hoelzl@59664 ` 1074` ``` have *: "set_pmf (map_pmf f p) \ s \ {}" ``` hoelzl@59665 ` 1075` ``` using assms by auto ``` hoelzl@59664 ` 1076` ``` { fix x ``` hoelzl@62975 ` 1077` ``` have "ennreal (pmf (map_pmf f (cond_pmf p (f -` s))) x) = ``` hoelzl@59664 ` 1078` ``` emeasure p (f -` s \ f -` {x}) / emeasure p (f -` s)" ``` hoelzl@62975 ` 1079` ``` unfolding ennreal_pmf_map cond_pmf.rep_eq[OF assms] by (simp add: nn_integral_uniform_measure) ``` hoelzl@59664 ` 1080` ``` also have "f -` s \ f -` {x} = (if x \ s then f -` {x} else {})" ``` hoelzl@59664 ` 1081` ``` by auto ``` hoelzl@59664 ` 1082` ``` also have "emeasure p (if x \ s then f -` {x} else {}) / emeasure p (f -` s) = ``` hoelzl@62975 ` 1083` ``` ennreal (pmf (cond_pmf (map_pmf f p) s) x)" ``` hoelzl@59664 ` 1084` ``` using measure_measure_pmf_not_zero[OF *] ``` hoelzl@62975 ` 1085` ``` by (simp add: pmf_cond[OF *] ennreal_pmf_map measure_pmf.emeasure_eq_measure ``` hoelzl@62975 ` 1086` ``` divide_ennreal pmf_nonneg measure_nonneg zero_less_measure_iff pmf_map) ``` hoelzl@62975 ` 1087` ``` 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 ` 1088` ``` by simp } ``` hoelzl@59664 ` 1089` ``` then show ?thesis ``` hoelzl@62975 ` 1090` ``` by (intro pmf_eqI) (simp add: pmf_nonneg) ``` hoelzl@59664 ` 1091` ```qed ``` hoelzl@59664 ` 1092` hoelzl@59664 ` 1093` ```lemma bind_cond_pmf_cancel: ``` hoelzl@59670 ` 1094` ``` assumes [simp]: "\x. x \ set_pmf p \ set_pmf q \ {y. R x y} \ {}" ``` hoelzl@59670 ` 1095` ``` assumes [simp]: "\y. y \ set_pmf q \ set_pmf p \ {x. R x y} \ {}" ``` hoelzl@59670 ` 1096` ``` 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 ` 1097` ``` shows "bind_pmf p (\x. cond_pmf q {y. R x y}) = q" ``` hoelzl@59664 ` 1098` ```proof (rule pmf_eqI) ``` hoelzl@59670 ` 1099` ``` fix i ``` hoelzl@62975 ` 1100` ``` have "ennreal (pmf (bind_pmf p (\x. cond_pmf q {y. R x y})) i) = ``` hoelzl@62975 ` 1101` ``` (\\<^sup>+x. ennreal (pmf q i / measure p {x. R x i}) * ennreal (indicator {x. R x i} x) \p)" ``` hoelzl@62975 ` 1102` ``` by (auto simp add: ennreal_pmf_bind AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf pmf_nonneg measure_nonneg ``` hoelzl@62975 ` 1103` ``` intro!: nn_integral_cong_AE) ``` hoelzl@59670 ` 1104` ``` also have "\ = (pmf q i * measure p {x. R x i}) / measure p {x. R x i}" ``` hoelzl@62975 ` 1105` ``` by (simp add: pmf_nonneg measure_nonneg zero_ennreal_def[symmetric] ennreal_indicator ``` hoelzl@62975 ` 1106` ``` nn_integral_cmult measure_pmf.emeasure_eq_measure ennreal_mult[symmetric]) ``` hoelzl@59670 ` 1107` ``` also have "\ = pmf q i" ``` hoelzl@62975 ` 1108` ``` by (cases "pmf q i = 0") ``` hoelzl@62975 ` 1109` ``` (simp_all add: pmf_eq_0_set_pmf measure_measure_pmf_not_zero pmf_nonneg) ``` hoelzl@59670 ` 1110` ``` finally show "pmf (bind_pmf p (\x. cond_pmf q {y. R x y})) i = pmf q i" ``` hoelzl@62975 ` 1111` ``` by (simp add: pmf_nonneg) ``` hoelzl@59664 ` 1112` ```qed ``` hoelzl@59664 ` 1113` hoelzl@59664 ` 1114` ```subsection \ Relator \ ``` hoelzl@59664 ` 1115` hoelzl@59664 ` 1116` ```inductive rel_pmf :: "('a \ 'b \ bool) \ 'a pmf \ 'b pmf \ bool" ``` hoelzl@59664 ` 1117` ```for R p q ``` hoelzl@59664 ` 1118` ```where ``` lp15@59667 ` 1119` ``` "\ \x y. (x, y) \ set_pmf pq \ R x y; ``` hoelzl@59664 ` 1120` ``` map_pmf fst pq = p; map_pmf snd pq = q \ ``` hoelzl@59664 ` 1121` ``` \ rel_pmf R p q" ``` hoelzl@59664 ` 1122` hoelzl@59681 ` 1123` ```lemma rel_pmfI: ``` hoelzl@59681 ` 1124` ``` assumes R: "rel_set R (set_pmf p) (set_pmf q)" ``` hoelzl@59681 ` 1125` ``` assumes eq: "\x y. x \ set_pmf p \ y \ set_pmf q \ R x y \ ``` hoelzl@59681 ` 1126` ``` measure p {x. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 1127` ``` shows "rel_pmf R p q" ``` hoelzl@59681 ` 1128` ```proof ``` hoelzl@59681 ` 1129` ``` let ?pq = "bind_pmf p (\x. bind_pmf (cond_pmf q {y. R x y}) (\y. return_pmf (x, y)))" ``` hoelzl@59681 ` 1130` ``` have "\x. x \ set_pmf p \ set_pmf q \ {y. R x y} \ {}" ``` hoelzl@59681 ` 1131` ``` using R by (auto simp: rel_set_def) ``` hoelzl@59681 ` 1132` ``` then show "\x y. (x, y) \ set_pmf ?pq \ R x y" ``` hoelzl@59681 ` 1133` ``` by auto ``` hoelzl@59681 ` 1134` ``` show "map_pmf fst ?pq = p" ``` Andreas@60068 ` 1135` ``` by (simp add: map_bind_pmf bind_return_pmf') ``` hoelzl@59681 ` 1136` hoelzl@59681 ` 1137` ``` show "map_pmf snd ?pq = q" ``` hoelzl@59681 ` 1138` ``` using R eq ``` Andreas@60068 ` 1139` ``` apply (simp add: bind_cond_pmf_cancel map_bind_pmf bind_return_pmf') ``` hoelzl@59681 ` 1140` ``` apply (rule bind_cond_pmf_cancel) ``` hoelzl@59681 ` 1141` ``` apply (auto simp: rel_set_def) ``` hoelzl@59681 ` 1142` ``` done ``` hoelzl@59681 ` 1143` ```qed ``` hoelzl@59681 ` 1144` hoelzl@59681 ` 1145` ```lemma rel_pmf_imp_rel_set: "rel_pmf R p q \ rel_set R (set_pmf p) (set_pmf q)" ``` hoelzl@59681 ` 1146` ``` by (force simp add: rel_pmf.simps rel_set_def) ``` hoelzl@59681 ` 1147` hoelzl@59681 ` 1148` ```lemma rel_pmfD_measure: ``` hoelzl@59681 ` 1149` ``` assumes rel_R: "rel_pmf R p q" and R: "\a b. R a b \ R a y \ R x b" ``` hoelzl@59681 ` 1150` ``` assumes "x \ set_pmf p" "y \ set_pmf q" ``` hoelzl@59681 ` 1151` ``` shows "measure p {x. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 1152` ```proof - ``` hoelzl@59681 ` 1153` ``` from rel_R obtain pq where pq: "\x y. (x, y) \ set_pmf pq \ R x y" ``` hoelzl@59681 ` 1154` ``` and eq: "p = map_pmf fst pq" "q = map_pmf snd pq" ``` hoelzl@59681 ` 1155` ``` by (auto elim: rel_pmf.cases) ``` hoelzl@59681 ` 1156` ``` have "measure p {x. R x y} = measure pq {x. R (fst x) y}" ``` hoelzl@59681 ` 1157` ``` by (simp add: eq map_pmf_rep_eq measure_distr) ``` hoelzl@59681 ` 1158` ``` also have "\ = measure pq {y. R x (snd y)}" ``` hoelzl@59681 ` 1159` ``` by (intro measure_pmf.finite_measure_eq_AE) ``` hoelzl@59681 ` 1160` ``` (auto simp: AE_measure_pmf_iff R dest!: pq) ``` hoelzl@59681 ` 1161` ``` also have "\ = measure q {y. R x y}" ``` hoelzl@59681 ` 1162` ``` by (simp add: eq map_pmf_rep_eq measure_distr) ``` hoelzl@59681 ` 1163` ``` finally show "measure p {x. R x y} = measure q {y. R x y}" . ``` hoelzl@59681 ` 1164` ```qed ``` hoelzl@59681 ` 1165` Andreas@61634 ` 1166` ```lemma rel_pmf_measureD: ``` Andreas@61634 ` 1167` ``` assumes "rel_pmf R p q" ``` Andreas@61634 ` 1168` ``` shows "measure (measure_pmf p) A \ measure (measure_pmf q) {y. \x\A. R x y}" (is "?lhs \ ?rhs") ``` Andreas@61634 ` 1169` ```using assms ``` Andreas@61634 ` 1170` ```proof cases ``` Andreas@61634 ` 1171` ``` fix pq ``` Andreas@61634 ` 1172` ``` assume R: "\x y. (x, y) \ set_pmf pq \ R x y" ``` Andreas@61634 ` 1173` ``` and p[symmetric]: "map_pmf fst pq = p" ``` Andreas@61634 ` 1174` ``` and q[symmetric]: "map_pmf snd pq = q" ``` Andreas@61634 ` 1175` ``` have "?lhs = measure (measure_pmf pq) (fst -` A)" by(simp add: p) ``` Andreas@61634 ` 1176` ``` also have "\ \ measure (measure_pmf pq) {y. \x\A. R x (snd y)}" ``` Andreas@61634 ` 1177` ``` by(rule measure_pmf.finite_measure_mono_AE)(auto 4 3 simp add: AE_measure_pmf_iff dest: R) ``` Andreas@61634 ` 1178` ``` also have "\ = ?rhs" by(simp add: q) ``` Andreas@61634 ` 1179` ``` finally show ?thesis . ``` Andreas@61634 ` 1180` ```qed ``` Andreas@61634 ` 1181` hoelzl@59681 ` 1182` ```lemma rel_pmf_iff_measure: ``` hoelzl@59681 ` 1183` ``` assumes "symp R" "transp R" ``` hoelzl@59681 ` 1184` ``` shows "rel_pmf R p q \ ``` hoelzl@59681 ` 1185` ``` rel_set R (set_pmf p) (set_pmf q) \ ``` hoelzl@59681 ` 1186` ``` (\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 ` 1187` ``` by (safe intro!: rel_pmf_imp_rel_set rel_pmfI) ``` hoelzl@59681 ` 1188` ``` (auto intro!: rel_pmfD_measure dest: sympD[OF \symp R\] transpD[OF \transp R\]) ``` hoelzl@59681 ` 1189` hoelzl@59681 ` 1190` ```lemma quotient_rel_set_disjoint: ``` hoelzl@59681 ` 1191` ``` "equivp R \ C \ UNIV // {(x, y). R x y} \ rel_set R A B \ A \ C = {} \ B \ C = {}" ``` lp15@61609 ` 1192` ``` using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C] ``` hoelzl@59681 ` 1193` ``` by (auto 0 0 simp: equivp_equiv rel_set_def set_eq_iff elim: equivpE) ``` hoelzl@59681 ` 1194` ``` (blast dest: equivp_symp)+ ``` hoelzl@59681 ` 1195` hoelzl@59681 ` 1196` ```lemma quotientD: "equiv X R \ A \ X // R \ x \ A \ A = R `` {x}" ``` hoelzl@59681 ` 1197` ``` by (metis Image_singleton_iff equiv_class_eq_iff quotientE) ``` hoelzl@59681 ` 1198` hoelzl@59681 ` 1199` ```lemma rel_pmf_iff_equivp: ``` hoelzl@59681 ` 1200` ``` assumes "equivp R" ``` hoelzl@59681 ` 1201` ``` shows "rel_pmf R p q \ (\C\UNIV // {(x, y). R x y}. measure p C = measure q C)" ``` hoelzl@59681 ` 1202` ``` (is "_ \ (\C\_//?R. _)") ``` hoelzl@59681 ` 1203` ```proof (subst rel_pmf_iff_measure, safe) ``` hoelzl@59681 ` 1204` ``` show "symp R" "transp R" ``` hoelzl@59681 ` 1205` ``` using assms by (auto simp: equivp_reflp_symp_transp) ``` hoelzl@59681 ` 1206` ```next ``` hoelzl@59681 ` 1207` ``` fix C assume C: "C \ UNIV // ?R" and R: "rel_set R (set_pmf p) (set_pmf q)" ``` hoelzl@59681 ` 1208` ``` 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 ` 1209` hoelzl@59681 ` 1210` ``` show "measure p C = measure q C" ``` wenzelm@63540 ` 1211` ``` proof (cases "p \ C = {}") ``` wenzelm@63540 ` 1212` ``` case True ``` wenzelm@63540 ` 1213` ``` then have "q \ C = {}" ``` hoelzl@59681 ` 1214` ``` using quotient_rel_set_disjoint[OF assms C R] by simp ``` wenzelm@63540 ` 1215` ``` with True show ?thesis ``` hoelzl@59681 ` 1216` ``` unfolding measure_pmf_zero_iff[symmetric] by simp ``` hoelzl@59681 ` 1217` ``` next ``` wenzelm@63540 ` 1218` ``` case False ``` wenzelm@63540 ` 1219` ``` then have "q \ C \ {}" ``` hoelzl@59681 ` 1220` ``` using quotient_rel_set_disjoint[OF assms C R] by simp ``` wenzelm@63540 ` 1221` ``` 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 ` 1222` ``` by auto ``` hoelzl@59681 ` 1223` ``` then have "R x y" ``` hoelzl@59681 ` 1224` ``` using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms ``` hoelzl@59681 ` 1225` ``` by (simp add: equivp_equiv) ``` hoelzl@59681 ` 1226` ``` with in_set eq have "measure p {x. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 1227` ``` by auto ``` hoelzl@59681 ` 1228` ``` moreover have "{y. R x y} = C" ``` wenzelm@61808 ` 1229` ``` using assms \x \ C\ C quotientD[of UNIV ?R C x] by (simp add: equivp_equiv) ``` hoelzl@59681 ` 1230` ``` moreover have "{x. R x y} = C" ``` wenzelm@61808 ` 1231` ``` using assms \y \ C\ C quotientD[of UNIV "?R" C y] sympD[of R] ``` hoelzl@59681 ` 1232` ``` by (auto simp add: equivp_equiv elim: equivpE) ``` hoelzl@59681 ` 1233` ``` ultimately show ?thesis ``` hoelzl@59681 ` 1234` ``` by auto ``` hoelzl@59681 ` 1235` ``` qed ``` hoelzl@59681 ` 1236` ```next ``` hoelzl@59681 ` 1237` ``` assume eq: "\C\UNIV // ?R. measure p C = measure q C" ``` hoelzl@59681 ` 1238` ``` show "rel_set R (set_pmf p) (set_pmf q)" ``` hoelzl@59681 ` 1239` ``` unfolding rel_set_def ``` hoelzl@59681 ` 1240` ``` proof safe ``` hoelzl@59681 ` 1241` ``` fix x assume x: "x \ set_pmf p" ``` hoelzl@59681 ` 1242` ``` have "{y. R x y} \ UNIV // ?R" ``` hoelzl@59681 ` 1243` ``` by (auto simp: quotient_def) ``` hoelzl@59681 ` 1244` ``` with eq have *: "measure q {y. R x y} = measure p {y. R x y}" ``` hoelzl@59681 ` 1245` ``` by auto ``` hoelzl@59681 ` 1246` ``` have "measure q {y. R x y} \ 0" ``` hoelzl@59681 ` 1247` ``` using x assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp) ``` hoelzl@59681 ` 1248` ``` then show "\y\set_pmf q. R x y" ``` hoelzl@59681 ` 1249` ``` unfolding measure_pmf_zero_iff by auto ``` hoelzl@59681 ` 1250` ``` next ``` hoelzl@59681 ` 1251` ``` fix y assume y: "y \ set_pmf q" ``` hoelzl@59681 ` 1252` ``` have "{x. R x y} \ UNIV // ?R" ``` hoelzl@59681 ` 1253` ``` using assms by (auto simp: quotient_def dest: equivp_symp) ``` hoelzl@59681 ` 1254` ``` with eq have *: "measure p {x. R x y} = measure q {x. R x y}" ``` hoelzl@59681 ` 1255` ``` by auto ``` hoelzl@59681 ` 1256` ``` have "measure p {x. R x y} \ 0" ``` hoelzl@59681 ` 1257` ``` using y assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp) ``` hoelzl@59681 ` 1258` ``` then show "\x\set_pmf p. R x y" ``` hoelzl@59681 ` 1259` ``` unfolding measure_pmf_zero_iff by auto ``` hoelzl@59681 ` 1260` ``` qed ``` hoelzl@59681 ` 1261` hoelzl@59681 ` 1262` ``` fix x y assume "x \ set_pmf p" "y \ set_pmf q" "R x y" ``` hoelzl@59681 ` 1263` ``` have "{y. R x y} \ UNIV // ?R" "{x. R x y} = {y. R x y}" ``` wenzelm@61808 ` 1264` ``` using assms \R x y\ by (auto simp: quotient_def dest: equivp_symp equivp_transp) ``` hoelzl@59681 ` 1265` ``` with eq show "measure p {x. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 1266` ``` by auto ``` hoelzl@59681 ` 1267` ```qed ``` hoelzl@59681 ` 1268` hoelzl@59664 ` 1269` ```bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf ``` hoelzl@59664 ` 1270` ```proof - ``` hoelzl@59664 ` 1271` ``` show "map_pmf id = id" by (rule map_pmf_id) ``` lp15@59667 ` 1272` ``` show "\f g. map_pmf (f \ g) = map_pmf f \ map_pmf g" by (rule map_pmf_compose) ``` hoelzl@59664 ` 1273` ``` 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 ` 1274` ``` by (intro map_pmf_cong refl) ``` hoelzl@59664 ` 1275` hoelzl@59664 ` 1276` ``` show "\f::'a \ 'b. set_pmf \ map_pmf f = op ` f \ set_pmf" ``` hoelzl@59664 ` 1277` ``` by (rule pmf_set_map) ``` hoelzl@59664 ` 1278` wenzelm@60595 ` 1279` ``` show "(card_of (set_pmf p), natLeq) \ ordLeq" for p :: "'s pmf" ``` wenzelm@60595 ` 1280` ``` proof - ``` hoelzl@59664 ` 1281` ``` have "(card_of (set_pmf p), card_of (UNIV :: nat set)) \ ordLeq" ``` hoelzl@59664 ` 1282` ``` by (rule card_of_ordLeqI[where f="to_nat_on (set_pmf p)"]) ``` hoelzl@59664 ` 1283` ``` (auto intro: countable_set_pmf) ``` hoelzl@59664 ` 1284` ``` also have "(card_of (UNIV :: nat set), natLeq) \ ordLeq" ``` hoelzl@59664 ` 1285` ``` by (metis Field_natLeq card_of_least natLeq_Well_order) ``` wenzelm@60595 ` 1286` ``` finally show ?thesis . ``` wenzelm@60595 ` 1287` ``` qed ``` hoelzl@59664 ` 1288` traytel@62324 ` 1289` ``` show "\R. rel_pmf R = (\x y. \z. set_pmf z \ {(x, y). R x y} \ ``` traytel@62324 ` 1290` ``` map_pmf fst z = x \ map_pmf snd z = y)" ``` traytel@62324 ` 1291` ``` by (auto simp add: fun_eq_iff rel_pmf.simps) ``` hoelzl@59664 ` 1292` wenzelm@60595 ` 1293` ``` show "rel_pmf R OO rel_pmf S \ rel_pmf (R OO S)" ``` wenzelm@60595 ` 1294` ``` for R :: "'a \ 'b \ bool" and S :: "'b \ 'c \ bool" ``` wenzelm@60595 ` 1295` ``` proof - ``` wenzelm@60595 ` 1296` ``` { fix p q r ``` wenzelm@60595 ` 1297` ``` assume pq: "rel_pmf R p q" ``` wenzelm@60595 ` 1298` ``` and qr:"rel_pmf S q r" ``` wenzelm@60595 ` 1299` ``` from pq obtain pq where pq: "\x y. (x, y) \ set_pmf pq \ R x y" ``` wenzelm@60595 ` 1300` ``` and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto ``` wenzelm@60595 ` 1301` ``` from qr obtain qr where qr: "\y z. (y, z) \ set_pmf qr \ S y z" ``` wenzelm@60595 ` 1302` ``` and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto ``` lp15@61609 ` 1303` wenzelm@63040 ` 1304` ``` define pr where "pr = ``` wenzelm@63040 ` 1305` ``` bind_pmf pq (\xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) ``` wenzelm@63040 ` 1306` ``` (\yz. return_pmf (fst xy, snd yz)))" ``` wenzelm@60595 ` 1307` ``` have pr_welldefined: "\y. y \ q \ qr \ {yz. fst yz = y} \ {}" ``` wenzelm@60595 ` 1308` ``` by (force simp: q') ``` lp15@61609 ` 1309` wenzelm@60595 ` 1310` ``` have "rel_pmf (R OO S) p r" ``` wenzelm@60595 ` 1311` ``` proof (rule rel_pmf.intros) ``` wenzelm@60595 ` 1312` ``` fix x z assume "(x, z) \ pr" ``` wenzelm@60595 ` 1313` ``` then have "\y. (x, y) \ pq \ (y, z) \ qr" ``` wenzelm@60595 ` 1314` ``` by (auto simp: q pr_welldefined pr_def split_beta) ``` wenzelm@60595 ` 1315` ``` with pq qr show "(R OO S) x z" ``` wenzelm@60595 ` 1316` ``` by blast ``` wenzelm@60595 ` 1317` ``` next ``` wenzelm@60595 ` 1318` ``` have "map_pmf snd pr = map_pmf snd (bind_pmf q (\y. cond_pmf qr {yz. fst yz = y}))" ``` wenzelm@60595 ` 1319` ``` by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_pmf_comp) ``` wenzelm@60595 ` 1320` ``` then show "map_pmf snd pr = r" ``` wenzelm@60595 ` 1321` ``` unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute) ``` wenzelm@60595 ` 1322` ``` qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp) ``` wenzelm@60595 ` 1323` ``` } ``` wenzelm@60595 ` 1324` ``` then show ?thesis ``` wenzelm@60595 ` 1325` ``` by(auto simp add: le_fun_def) ``` wenzelm@60595 ` 1326` ``` qed ``` hoelzl@59664 ` 1327` ```qed (fact natLeq_card_order natLeq_cinfinite)+ ``` hoelzl@59664 ` 1328` Andreas@61634 ` 1329` ```lemma map_pmf_idI: "(\x. x \ set_pmf p \ f x = x) \ map_pmf f p = p" ``` Andreas@61634 ` 1330` ```by(simp cong: pmf.map_cong) ``` Andreas@61634 ` 1331` hoelzl@59665 ` 1332` ```lemma rel_pmf_conj[simp]: ``` hoelzl@59665 ` 1333` ``` "rel_pmf (\x y. P \ Q x y) x y \ P \ rel_pmf Q x y" ``` hoelzl@59665 ` 1334` ``` "rel_pmf (\x y. Q x y \ P) x y \ P \ rel_pmf Q x y" ``` hoelzl@59665 ` 1335` ``` using set_pmf_not_empty by (fastforce simp: pmf.in_rel subset_eq)+ ``` hoelzl@59665 ` 1336` hoelzl@59665 ` 1337` ```lemma rel_pmf_top[simp]: "rel_pmf top = top" ``` hoelzl@59665 ` 1338` ``` by (auto simp: pmf.in_rel[abs_def] fun_eq_iff map_fst_pair_pmf map_snd_pair_pmf ``` hoelzl@59665 ` 1339` ``` intro: exI[of _ "pair_pmf x y" for x y]) ``` hoelzl@59665 ` 1340` hoelzl@59664 ` 1341` ```lemma rel_pmf_return_pmf1: "rel_pmf R (return_pmf x) M \ (\a\M. R x a)" ``` hoelzl@59664 ` 1342` ```proof safe ``` hoelzl@59664 ` 1343` ``` fix a assume "a \ M" "rel_pmf R (return_pmf x) M" ``` hoelzl@59664 ` 1344` ``` then obtain pq where *: "\a b. (a, b) \ set_pmf pq \ R a b" ``` hoelzl@59664 ` 1345` ``` and eq: "return_pmf x = map_pmf fst pq" "M = map_pmf snd pq" ``` hoelzl@59664 ` 1346` ``` by (force elim: rel_pmf.cases) ``` hoelzl@59664 ` 1347` ``` moreover have "set_pmf (return_pmf x) = {x}" ``` hoelzl@59665 ` 1348` ``` by simp ``` wenzelm@61808 ` 1349` ``` with \a \ M\ have "(x, a) \ pq" ``` hoelzl@59665 ` 1350` ``` by (force simp: eq) ``` hoelzl@59664 ` 1351` ``` with * show "R x a" ``` hoelzl@59664 ` 1352` ``` by auto ``` hoelzl@59664 ` 1353` ```qed (auto intro!: rel_pmf.intros[where pq="pair_pmf (return_pmf x) M"] ``` hoelzl@59665 ` 1354` ``` simp: map_fst_pair_pmf map_snd_pair_pmf) ``` hoelzl@59664 ` 1355` hoelzl@59664 ` 1356` ```lemma rel_pmf_return_pmf2: "rel_pmf R M (return_pmf x) \ (\a\M. R a x)" ``` hoelzl@59664 ` 1357` ``` by (subst pmf.rel_flip[symmetric]) (simp add: rel_pmf_return_pmf1) ``` hoelzl@59664 ` 1358` hoelzl@59664 ` 1359` ```lemma rel_return_pmf[simp]: "rel_pmf R (return_pmf x1) (return_pmf x2) = R x1 x2" ``` hoelzl@59664 ` 1360` ``` unfolding rel_pmf_return_pmf2 set_return_pmf by simp ``` hoelzl@59664 ` 1361` hoelzl@59664 ` 1362` ```lemma rel_pmf_False[simp]: "rel_pmf (\x y. False) x y = False" ``` hoelzl@59664 ` 1363` ``` unfolding pmf.in_rel fun_eq_iff using set_pmf_not_empty by fastforce ``` hoelzl@59664 ` 1364` hoelzl@59664 ` 1365` ```lemma rel_pmf_rel_prod: ``` hoelzl@59664 ` 1366` ``` "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 ` 1367` ```proof safe ``` hoelzl@59664 ` 1368` ``` assume "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')" ``` hoelzl@59664 ` 1369` ``` then obtain pq where pq: "\a b c d. ((a, c), (b, d)) \ set_pmf pq \ R a b \ S c d" ``` hoelzl@59664 ` 1370` ``` and eq: "map_pmf fst pq = pair_pmf A A'" "map_pmf snd pq = pair_pmf B B'" ``` hoelzl@59664 ` 1371` ``` by (force elim: rel_pmf.cases) ``` hoelzl@59664 ` 1372` ``` show "rel_pmf R A B" ``` hoelzl@59664 ` 1373` ``` proof (rule rel_pmf.intros) ``` hoelzl@59664 ` 1374` ``` let ?f = "\(a, b). (fst a, fst b)" ``` hoelzl@59664 ` 1375` ``` have [simp]: "(\x. fst (?f x)) = fst o fst" "(\x. snd (?f x)) = fst o snd" ``` hoelzl@59664 ` 1376` ``` by auto ``` hoelzl@59664 ` 1377` hoelzl@59664 ` 1378` ``` show "map_pmf fst (map_pmf ?f pq) = A" ``` hoelzl@59664 ` 1379` ``` by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_fst_pair_pmf) ``` hoelzl@59664 ` 1380` ``` show "map_pmf snd (map_pmf ?f pq) = B" ``` hoelzl@59664 ` 1381` ``` by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_fst_pair_pmf) ``` hoelzl@59664 ` 1382` hoelzl@59664 ` 1383` ``` fix a b assume "(a, b) \ set_pmf (map_pmf ?f pq)" ``` hoelzl@59664 ` 1384` ``` then obtain c d where "((a, c), (b, d)) \ set_pmf pq" ``` hoelzl@59665 ` 1385` ``` by auto ``` hoelzl@59664 ` 1386` ``` from pq[OF this] show "R a b" .. ``` hoelzl@59664 ` 1387` ``` qed ``` hoelzl@59664 ` 1388` ``` show "rel_pmf S A' B'" ``` hoelzl@59664 ` 1389` ``` proof (rule rel_pmf.intros) ``` hoelzl@59664 ` 1390` ``` let ?f = "\(a, b). (snd a, snd b)" ``` hoelzl@59664 ` 1391` ``` have [simp]: "(\x. fst (?f x)) = snd o fst" "(\x. snd (?f x)) = snd o snd" ``` hoelzl@59664 ` 1392` ``` by auto ``` hoelzl@59664 ` 1393` hoelzl@59664 ` 1394` ``` show "map_pmf fst (map_pmf ?f pq) = A'" ``` hoelzl@59664 ` 1395` ``` by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_snd_pair_pmf) ``` hoelzl@59664 ` 1396` ``` show "map_pmf snd (map_pmf ?f pq) = B'" ``` hoelzl@59664 ` 1397` ``` by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_snd_pair_pmf) ``` hoelzl@59664 ` 1398` hoelzl@59664 ` 1399` ``` fix c d assume "(c, d) \ set_pmf (map_pmf ?f pq)" ``` hoelzl@59664 ` 1400` ``` then obtain a b where "((a, c), (b, d)) \ set_pmf pq" ``` hoelzl@59665 ` 1401` ``` by auto ``` hoelzl@59664 ` 1402` ``` from pq[OF this] show "S c d" .. ``` hoelzl@59664 ` 1403` ``` qed ``` hoelzl@59664 ` 1404` ```next ``` hoelzl@59664 ` 1405` ``` assume "rel_pmf R A B" "rel_pmf S A' B'" ``` hoelzl@59664 ` 1406` ``` then obtain Rpq Spq ``` hoelzl@59664 ` 1407` ``` where Rpq: "\a b. (a, b) \ set_pmf Rpq \ R a b" ``` hoelzl@59664 ` 1408` ``` "map_pmf fst Rpq = A" "map_pmf snd Rpq = B" ``` hoelzl@59664 ` 1409` ``` and Spq: "\a b. (a, b) \ set_pmf Spq \ S a b" ``` hoelzl@59664 ` 1410` ``` "map_pmf fst Spq = A'" "map_pmf snd Spq = B'" ``` hoelzl@59664 ` 1411` ``` by (force elim: rel_pmf.cases) ``` hoelzl@59664 ` 1412` hoelzl@59664 ` 1413` ``` let ?f = "(\((a, c), (b, d)). ((a, b), (c, d)))" ``` hoelzl@59664 ` 1414` ``` let ?pq = "map_pmf ?f (pair_pmf Rpq Spq)" ``` hoelzl@59664 ` 1415` ``` have [simp]: "(\x. fst (?f x)) = (\(a, b). (fst a, fst b))" "(\x. snd (?f x)) = (\(a, b). (snd a, snd b))" ``` hoelzl@59664 ` 1416` ``` by auto ``` hoelzl@59664 ` 1417` hoelzl@59664 ` 1418` ``` show "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')" ``` hoelzl@59664 ` 1419` ``` by (rule rel_pmf.intros[where pq="?pq"]) ``` hoelzl@59665 ` 1420` ``` (auto simp: map_snd_pair_pmf map_fst_pair_pmf map_pmf_comp Rpq Spq ``` hoelzl@59664 ` 1421` ``` map_pair) ``` hoelzl@59664 ` 1422` ```qed ``` hoelzl@59664 ` 1423` lp15@59667 ` 1424` ```lemma rel_pmf_reflI: ``` hoelzl@59664 ` 1425` ``` assumes "\x. x \ set_pmf p \ P x x" ``` hoelzl@59664 ` 1426` ``` shows "rel_pmf P p p" ``` hoelzl@59665 ` 1427` ``` by (rule rel_pmf.intros[where pq="map_pmf (\x. (x, x)) p"]) ``` hoelzl@59665 ` 1428` ``` (auto simp add: pmf.map_comp o_def assms) ``` hoelzl@59664 ` 1429` Andreas@61634 ` 1430` ```lemma rel_pmf_bij_betw: ``` Andreas@61634 ` 1431` ``` assumes f: "bij_betw f (set_pmf p) (set_pmf q)" ``` Andreas@61634 ` 1432` ``` and eq: "\x. x \ set_pmf p \ pmf p x = pmf q (f x)" ``` Andreas@61634 ` 1433` ``` shows "rel_pmf (\x y. f x = y) p q" ``` Andreas@61634 ` 1434` ```proof(rule rel_pmf.intros) ``` Andreas@61634 ` 1435` ``` let ?pq = "map_pmf (\x. (x, f x)) p" ``` Andreas@61634 ` 1436` ``` show "map_pmf fst ?pq = p" by(simp add: pmf.map_comp o_def) ``` Andreas@61634 ` 1437` Andreas@61634 ` 1438` ``` have "map_pmf f p = q" ``` Andreas@61634 ` 1439` ``` proof(rule pmf_eqI) ``` Andreas@61634 ` 1440` ``` fix i ``` Andreas@61634 ` 1441` ``` show "pmf (map_pmf f p) i = pmf q i" ``` Andreas@61634 ` 1442` ``` proof(cases "i \ set_pmf q") ``` Andreas@61634 ` 1443` ``` case True ``` Andreas@61634 ` 1444` ``` with f obtain j where "i = f j" "j \ set_pmf p" ``` Andreas@61634 ` 1445` ``` by(auto simp add: bij_betw_def image_iff) ``` Andreas@61634 ` 1446` ``` thus ?thesis using f by(simp add: bij_betw_def pmf_map_inj eq) ``` Andreas@61634 ` 1447` ``` next ``` Andreas@61634 ` 1448` ``` case False thus ?thesis ``` Andreas@61634 ` 1449` ``` by(subst pmf_map_outside)(auto simp add: set_pmf_iff eq[symmetric]) ``` Andreas@61634 ` 1450` ``` qed ``` Andreas@61634 ` 1451` ``` qed ``` Andreas@61634 ` 1452` ``` then show "map_pmf snd ?pq = q" by(simp add: pmf.map_comp o_def) ``` Andreas@61634 ` 1453` ```qed auto ``` Andreas@61634 ` 1454` hoelzl@59664 ` 1455` ```context ``` hoelzl@59664 ` 1456` ```begin ``` hoelzl@59664 ` 1457` hoelzl@59664 ` 1458` ```interpretation pmf_as_measure . ``` hoelzl@59664 ` 1459` hoelzl@59664 ` 1460` ```definition "join_pmf M = bind_pmf M (\x. x)" ``` hoelzl@59664 ` 1461` hoelzl@59664 ` 1462` ```lemma bind_eq_join_pmf: "bind_pmf M f = join_pmf (map_pmf f M)" ``` hoelzl@59664 ` 1463` ``` unfolding join_pmf_def bind_map_pmf .. ``` hoelzl@59664 ` 1464` hoelzl@59664 ` 1465` ```lemma join_eq_bind_pmf: "join_pmf M = bind_pmf M id" ``` hoelzl@59664 ` 1466` ``` by (simp add: join_pmf_def id_def) ``` hoelzl@59664 ` 1467` hoelzl@59664 ` 1468` ```lemma pmf_join: "pmf (join_pmf N) i = (\M. pmf M i \measure_pmf N)" ``` hoelzl@59664 ` 1469` ``` unfolding join_pmf_def pmf_bind .. ``` hoelzl@59664 ` 1470` hoelzl@62975 ` 1471` ```lemma ennreal_pmf_join: "ennreal (pmf (join_pmf N) i) = (\\<^sup>+M. pmf M i \measure_pmf N)" ``` hoelzl@62975 ` 1472` ``` unfolding join_pmf_def ennreal_pmf_bind .. ``` hoelzl@59664 ` 1473` hoelzl@59665 ` 1474` ```lemma set_pmf_join_pmf[simp]: "set_pmf (join_pmf f) = (\p\set_pmf f. set_pmf p)" ``` hoelzl@59665 ` 1475` ``` by (simp add: join_pmf_def) ``` hoelzl@59664 ` 1476` hoelzl@59664 ` 1477` ```lemma join_return_pmf: "join_pmf (return_pmf M) = M" ``` hoelzl@59664 ` 1478` ``` by (simp add: integral_return pmf_eq_iff pmf_join return_pmf.rep_eq) ``` hoelzl@59664 ` 1479` hoelzl@59664 ` 1480` ```lemma map_join_pmf: "map_pmf f (join_pmf AA) = join_pmf (map_pmf (map_pmf f) AA)" ``` hoelzl@59664 ` 1481` ``` by (simp add: join_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf) ``` hoelzl@59664 ` 1482` hoelzl@59664 ` 1483` ```lemma join_map_return_pmf: "join_pmf (map_pmf return_pmf A) = A" ``` hoelzl@59664 ` 1484` ``` by (simp add: join_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') ``` hoelzl@59664 ` 1485` hoelzl@59664 ` 1486` ```end ``` hoelzl@59664 ` 1487` hoelzl@59664 ` 1488` ```lemma rel_pmf_joinI: ``` hoelzl@59664 ` 1489` ``` assumes "rel_pmf (rel_pmf P) p q" ``` hoelzl@59664 ` 1490` ``` shows "rel_pmf P (join_pmf p) (join_pmf q)" ``` hoelzl@59664 ` 1491` ```proof - ``` hoelzl@59664 ` 1492` ``` from assms obtain pq where p: "p = map_pmf fst pq" ``` hoelzl@59664 ` 1493` ``` and q: "q = map_pmf snd pq" ``` hoelzl@59664 ` 1494` ``` and P: "\x y. (x, y) \ set_pmf pq \ rel_pmf P x y" ``` hoelzl@59664 ` 1495` ``` by cases auto ``` lp15@59667 ` 1496` ``` from P obtain PQ ``` hoelzl@59664 ` 1497` ``` where PQ: "\x y a b. \ (x, y) \ set_pmf pq; (a, b) \ set_pmf (PQ x y) \ \ P a b" ``` hoelzl@59664 ` 1498` ``` and x: "\x y. (x, y) \ set_pmf pq \ map_pmf fst (PQ x y) = x" ``` hoelzl@59664 ` 1499` ``` and y: "\x y. (x, y) \ set_pmf pq \ map_pmf snd (PQ x y) = y" ``` hoelzl@59664 ` 1500` ``` by(metis rel_pmf.simps) ``` hoelzl@59664 ` 1501` hoelzl@59664 ` 1502` ``` let ?r = "bind_pmf pq (\(x, y). PQ x y)" ``` hoelzl@59665 ` 1503` ``` have "\a b. (a, b) \ set_pmf ?r \ P a b" by (auto intro: PQ) ``` hoelzl@59664 ` 1504` ``` moreover have "map_pmf fst ?r = join_pmf p" "map_pmf snd ?r = join_pmf q" ``` hoelzl@59664 ` 1505` ``` 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 ` 1506` ``` ultimately show ?thesis .. ``` hoelzl@59664 ` 1507` ```qed ``` hoelzl@59664 ` 1508` hoelzl@59664 ` 1509` ```lemma rel_pmf_bindI: ``` hoelzl@59664 ` 1510` ``` assumes pq: "rel_pmf R p q" ``` hoelzl@59664 ` 1511` ``` and fg: "\x y. R x y \ rel_pmf P (f x) (g y)" ``` hoelzl@59664 ` 1512` ``` shows "rel_pmf P (bind_pmf p f) (bind_pmf q g)" ``` hoelzl@59664 ` 1513` ``` unfolding bind_eq_join_pmf ``` hoelzl@59664 ` 1514` ``` by (rule rel_pmf_joinI) ``` hoelzl@59664 ` 1515` ``` (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 ` 1516` wenzelm@61808 ` 1517` ```text \ ``` hoelzl@59664 ` 1518` ``` Proof that @{const rel_pmf} preserves orders. ``` lp15@59667 ` 1519` ``` Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism, ``` lp15@59667 ` 1520` ``` Theoretical Computer Science 12(1):19--37, 1980, ``` wenzelm@63680 ` 1521` ``` \<^url>\http://dx.doi.org/10.1016/0304-3975(80)90003-1\ ``` wenzelm@61808 ` 1522` ```\ ``` hoelzl@59664 ` 1523` lp15@59667 ` 1524` ```lemma ``` hoelzl@59664 ` 1525` ``` assumes *: "rel_pmf R p q" ``` hoelzl@59664 ` 1526` ``` and refl: "reflp R" and trans: "transp R" ``` hoelzl@59664 ` 1527` ``` shows measure_Ici: "measure p {y. R x y} \ measure q {y. R x y}" (is ?thesis1) ``` hoelzl@59664 ` 1528` ``` 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 ` 1529` ```proof - ``` hoelzl@59664 ` 1530` ``` from * obtain pq ``` hoelzl@59664 ` 1531` ``` where pq: "\x y. (x, y) \ set_pmf pq \ R x y" ``` hoelzl@59664 ` 1532` ``` and p: "p = map_pmf fst pq" ``` hoelzl@59664 ` 1533` ``` and q: "q = map_pmf snd pq" ``` hoelzl@59664 ` 1534` ``` by cases auto ``` hoelzl@59664 ` 1535` ``` show ?thesis1 ?thesis2 unfolding p q map_pmf_rep_eq using refl trans ``` hoelzl@59664 ` 1536` ``` 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 ` 1537` ```qed ``` hoelzl@59664 ` 1538` hoelzl@59664 ` 1539` ```lemma rel_pmf_inf: ``` hoelzl@59664 ` 1540` ``` fixes p q :: "'a pmf" ``` hoelzl@59664 ` 1541` ``` assumes 1: "rel_pmf R p q" ``` hoelzl@59664 ` 1542` ``` assumes 2: "rel_pmf R q p" ``` hoelzl@59664 ` 1543` ``` and refl: "reflp R" and trans: "transp R" ``` hoelzl@59664 ` 1544` ``` shows "rel_pmf (inf R R\\) p q" ``` hoelzl@59681 ` 1545` ```proof (subst rel_pmf_iff_equivp, safe) ``` hoelzl@59681 ` 1546` ``` show "equivp (inf R R\\)" ``` hoelzl@59681 ` 1547` ``` using trans refl by (auto simp: equivp_reflp_symp_transp intro: sympI transpI reflpI dest: transpD reflpD) ``` lp15@61609 ` 1548` hoelzl@59681 ` 1549` ``` fix C assume "C \ UNIV // {(x, y). inf R R\\ x y}" ``` hoelzl@59681 ` 1550` ``` then obtain x where C: "C = {y. R x y \ R y x}" ``` hoelzl@59681 ` 1551` ``` by (auto elim: quotientE) ``` hoelzl@59681 ` 1552` hoelzl@59670 ` 1553` ``` let ?R = "\x y. R x y \ R y x" ``` hoelzl@59670 ` 1554` ``` let ?\R = "\y. measure q {x. ?R x y}" ``` hoelzl@59681 ` 1555` ``` have "measure p {y. ?R x y} = measure p ({y. R x y} - {y. R x y \ \ R y x})" ``` hoelzl@59681 ` 1556` ``` by(auto intro!: arg_cong[where f="measure p"]) ``` hoelzl@59681 ` 1557` ``` also have "\ = measure p {y. R x y} - measure p {y. R x y \ \ R y x}" ``` hoelzl@59681 ` 1558` ``` by (rule measure_pmf.finite_measure_Diff) auto ``` hoelzl@59681 ` 1559` ``` also have "measure p {y. R x y \ \ R y x} = measure q {y. R x y \ \ R y x}" ``` hoelzl@59681 ` 1560` ``` using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi) ``` hoelzl@59681 ` 1561` ``` also have "measure p {y. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 1562` ``` using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici) ``` hoelzl@59681 ` 1563` ``` also have "measure q {y. R x y} - measure q {y. R x y \ \ R y x} = ``` hoelzl@59681 ` 1564` ``` measure q ({y. R x y} - {y. R x y \ \ R y x})" ``` hoelzl@59681 ` 1565` ``` by(rule measure_pmf.finite_measure_Diff[symmetric]) auto ``` hoelzl@59681 ` 1566` ``` also have "\ = ?\R x" ``` hoelzl@59681 ` 1567` ``` by(auto intro!: arg_cong[where f="measure q"]) ``` hoelzl@59681 ` 1568` ``` finally show "measure p C = measure q C" ``` hoelzl@59681 ` 1569` ``` by (simp add: C conj_commute) ``` hoelzl@59664 ` 1570` ```qed ``` hoelzl@59664 ` 1571` hoelzl@59664 ` 1572` ```lemma rel_pmf_antisym: ``` hoelzl@59664 ` 1573` ``` fixes p q :: "'a pmf" ``` hoelzl@59664 ` 1574` ``` assumes 1: "rel_pmf R p q" ``` hoelzl@59664 ` 1575` ``` assumes 2: "rel_pmf R q p" ``` hoelzl@59664 ` 1576` ``` and refl: "reflp R" and trans: "transp R" and antisym: "antisymP R" ``` hoelzl@59664 ` 1577` ``` shows "p = q" ``` hoelzl@59664 ` 1578` ```proof - ``` hoelzl@59664 ` 1579` ``` from 1 2 refl trans have "rel_pmf (inf R R\\) p q" by(rule rel_pmf_inf) ``` hoelzl@59664 ` 1580` ``` also have "inf R R\\ = op =" ``` hoelzl@59665 ` 1581` ``` using refl antisym by (auto intro!: ext simp add: reflpD dest: antisymD) ``` hoelzl@59664 ` 1582` ``` finally show ?thesis unfolding pmf.rel_eq . ``` hoelzl@59664 ` 1583` ```qed ``` hoelzl@59664 ` 1584` hoelzl@59664 ` 1585` ```lemma reflp_rel_pmf: "reflp R \ reflp (rel_pmf R)" ``` hoelzl@59664 ` 1586` ```by(blast intro: reflpI rel_pmf_reflI reflpD) ``` hoelzl@59664 ` 1587` hoelzl@59664 ` 1588` ```lemma antisymP_rel_pmf: ``` hoelzl@59664 ` 1589` ``` "\ reflp R; transp R; antisymP R \ ``` hoelzl@59664 ` 1590` ``` \ antisymP (rel_pmf R)" ``` hoelzl@59664 ` 1591` ```by(rule antisymI)(blast intro: rel_pmf_antisym) ``` hoelzl@59664 ` 1592` hoelzl@59664 ` 1593` ```lemma transp_rel_pmf: ``` hoelzl@59664 ` 1594` ``` assumes "transp R" ``` hoelzl@59664 ` 1595` ``` shows "transp (rel_pmf R)" ``` hoelzl@59664 ` 1596` ```proof (rule transpI) ``` hoelzl@59664 ` 1597` ``` fix x y z ``` hoelzl@59664 ` 1598` ``` assume "rel_pmf R x y" and "rel_pmf R y z" ``` hoelzl@59664 ` 1599` ``` hence "rel_pmf (R OO R) x z" by (simp add: pmf.rel_compp relcompp.relcompI) ``` hoelzl@59664 ` 1600` ``` thus "rel_pmf R x z" ``` hoelzl@59664 ` 1601` ``` using assms by (metis (no_types) pmf.rel_mono rev_predicate2D transp_relcompp_less_eq) ``` hoelzl@59664 ` 1602` ```qed ``` hoelzl@59664 ` 1603` hoelzl@59664 ` 1604` ```subsection \ Distributions \ ``` hoelzl@59664 ` 1605` hoelzl@59000 ` 1606` ```context ``` hoelzl@59000 ` 1607` ```begin ``` hoelzl@59000 ` 1608` hoelzl@59000 ` 1609` ```interpretation pmf_as_function . ``` hoelzl@59000 ` 1610` hoelzl@59093 ` 1611` ```subsubsection \ Bernoulli Distribution \ ``` hoelzl@59093 ` 1612` hoelzl@59000 ` 1613` ```lift_definition bernoulli_pmf :: "real \ bool pmf" is ``` hoelzl@59000 ` 1614` ``` "\p b. ((\p. if b then p else 1 - p) \ min 1 \ max 0) p" ``` hoelzl@59000 ` 1615` ``` by (auto simp: nn_integral_count_space_finite[where A="{False, True}"] UNIV_bool ``` hoelzl@59000 ` 1616` ``` split: split_max split_min) ``` hoelzl@59000 ` 1617` hoelzl@59000 ` 1618` ```lemma pmf_bernoulli_True[simp]: "0 \ p \ p \ 1 \ pmf (bernoulli_pmf p) True = p" ``` hoelzl@59000 ` 1619` ``` by transfer simp ``` hoelzl@59000 ` 1620` hoelzl@59000 ` 1621` ```lemma pmf_bernoulli_False[simp]: "0 \ p \ p \ 1 \ pmf (bernoulli_pmf p) False = 1 - p" ``` hoelzl@59000 ` 1622` ``` by transfer simp ``` hoelzl@59000 ` 1623` hoelzl@62975 ` 1624` ```lemma set_pmf_bernoulli[simp]: "0 < p \ p < 1 \ set_pmf (bernoulli_pmf p) = UNIV" ``` hoelzl@59000 ` 1625` ``` by (auto simp add: set_pmf_iff UNIV_bool) ``` hoelzl@59000 ` 1626` lp15@59667 ` 1627` ```lemma nn_integral_bernoulli_pmf[simp]: ``` hoelzl@59002 ` 1628` ``` assumes [simp]: "0 \ p" "p \ 1" "\x. 0 \ f x" ``` hoelzl@59002 ` 1629` ``` shows "(\\<^sup>+x. f x \bernoulli_pmf p) = f True * p + f False * (1 - p)" ``` hoelzl@59002 ` 1630` ``` by (subst nn_integral_measure_pmf_support[of UNIV]) ``` hoelzl@59002 ` 1631` ``` (auto simp: UNIV_bool field_simps) ``` hoelzl@59002 ` 1632` lp15@59667 ` 1633` ```lemma integral_bernoulli_pmf[simp]: ``` hoelzl@59002 ` 1634` ``` assumes [simp]: "0 \ p" "p \ 1" ``` hoelzl@59002 ` 1635` ``` shows "(\x. f x \bernoulli_pmf p) = f True * p + f False * (1 - p)" ``` hoelzl@59002 ` 1636` ``` by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool) ``` hoelzl@59002 ` 1637` Andreas@59525 ` 1638` ```lemma pmf_bernoulli_half [simp]: "pmf (bernoulli_pmf (1 / 2)) x = 1 / 2" ``` Andreas@59525 ` 1639` ```by(cases x) simp_all ``` Andreas@59525 ` 1640` Andreas@59525 ` 1641` ```lemma measure_pmf_bernoulli_half: "measure_pmf (bernoulli_pmf (1 / 2)) = uniform_count_measure UNIV" ``` hoelzl@62975 ` 1642` ``` by (rule measure_eqI) ``` hoelzl@62975 ` 1643` ``` (simp_all add: nn_integral_pmf[symmetric] emeasure_uniform_count_measure ennreal_divide_numeral[symmetric] ``` hoelzl@62975 ` 1644` ``` nn_integral_count_space_finite sets_uniform_count_measure divide_ennreal_def mult_ac ``` hoelzl@62975 ` 1645` ``` ennreal_of_nat_eq_real_of_nat) ``` Andreas@59525 ` 1646` hoelzl@59093 ` 1647` ```subsubsection \ Geometric Distribution \ ``` hoelzl@59093 ` 1648` hoelzl@60602 ` 1649` ```context ``` hoelzl@60602 ` 1650` ``` fixes p :: real assumes p[arith]: "0 < p" "p \ 1" ``` hoelzl@60602 ` 1651` ```begin ``` hoelzl@60602 ` 1652` hoelzl@60602 ` 1653` ```lift_definition geometric_pmf :: "nat pmf" is "\n. (1 - p)^n * p" ``` hoelzl@59000 ` 1654` ```proof ``` hoelzl@62975 ` 1655` ``` have "(\i. ennreal (p * (1 - p) ^ i)) = ennreal (p * (1 / (1 - (1 - p))))" ``` hoelzl@62975 ` 1656` ``` by (intro suminf_ennreal_eq sums_mult geometric_sums) auto ``` hoelzl@62975 ` 1657` ``` then show "(\\<^sup>+ x. ennreal ((1 - p)^x * p) \count_space UNIV) = 1" ``` hoelzl@59000 ` 1658` ``` by (simp add: nn_integral_count_space_nat field_simps) ``` hoelzl@59000 ` 1659` ```qed simp ``` hoelzl@59000 ` 1660` hoelzl@60602 ` 1661` ```lemma pmf_geometric[simp]: "pmf geometric_pmf n = (1 - p)^n * p" ``` hoelzl@59000 ` 1662` ``` by transfer rule ``` hoelzl@59000 ` 1663` hoelzl@60602 ` 1664` ```end ``` hoelzl@60602 ` 1665` hoelzl@60602 ` 1666` ```lemma set_pmf_geometric: "0 < p \ p < 1 \ set_pmf (geometric_pmf p) = UNIV" ``` lp15@61609 ` 1667` ``` by (auto simp: set_pmf_iff) ``` hoelzl@59000 ` 1668` hoelzl@59093 ` 1669` ```subsubsection \ Uniform Multiset Distribution \ ``` hoelzl@59093 ` 1670` hoelzl@59000 ` 1671` ```context ``` hoelzl@59000 ` 1672` ``` fixes M :: "'a multiset" assumes M_not_empty: "M \ {#}" ``` hoelzl@59000 ` 1673` ```begin ``` hoelzl@59000 ` 1674` hoelzl@59000 ` 1675` ```lift_definition pmf_of_multiset :: "'a pmf" is "\x. count M x / size M" ``` hoelzl@59000 ` 1676` ```proof ``` hoelzl@62975 ` 1677` ``` show "(\\<^sup>+ x. ennreal (real (count M x) / real (size M)) \count_space UNIV) = 1" ``` hoelzl@59000 ` 1678` ``` using M_not_empty ``` hoelzl@59000 ` 1679` ``` by (simp add: zero_less_divide_iff nn_integral_count_space nonempty_has_size ``` hoelzl@59000 ` 1680` ``` setsum_divide_distrib[symmetric]) ``` hoelzl@59000 ` 1681` ``` (auto simp: size_multiset_overloaded_eq intro!: setsum.cong) ``` hoelzl@59000 ` 1682` ```qed simp ``` hoelzl@59000 ` 1683` hoelzl@59000 ` 1684` ```lemma pmf_of_multiset[simp]: "pmf pmf_of_multiset x = count M x / size M" ``` hoelzl@59000 ` 1685` ``` by transfer rule ``` hoelzl@59000 ` 1686` nipkow@60495 ` 1687` ```lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_mset M" ``` hoelzl@59000 ` 1688` ``` by (auto simp: set_pmf_iff) ``` hoelzl@59000 ` 1689` hoelzl@59000 ` 1690` ```end ``` hoelzl@59000 ` 1691` hoelzl@59093 ` 1692` ```subsubsection \ Uniform Distribution \ ``` hoelzl@59093 ` 1693` hoelzl@59000 ` 1694` ```context ``` hoelzl@59000 ` 1695` ``` fixes S :: "'a set" assumes S_not_empty: "S \ {}" and S_finite: "finite S" ``` hoelzl@59000 ` 1696` ```begin ``` hoelzl@59000 ` 1697` hoelzl@59000 ` 1698` ```lift_definition pmf_of_set :: "'a pmf" is "\x. indicator S x / card S" ``` hoelzl@59000 ` 1699` ```proof ``` hoelzl@62975 ` 1700` ``` show "(\\<^sup>+ x. ennreal (indicator S x / real (card S)) \count_space UNIV) = 1" ``` hoelzl@62975 ` 1701` ``` using S_not_empty S_finite ``` hoelzl@62975 ` 1702` ``` by (subst nn_integral_count_space'[of S]) ``` hoelzl@62975 ` 1703` ``` (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_mult[symmetric]) ``` hoelzl@59000 ` 1704` ```qed simp ``` hoelzl@59000 ` 1705` hoelzl@59000 ` 1706` ```lemma pmf_of_set[simp]: "pmf pmf_of_set x = indicator S x / card S" ``` hoelzl@59000 ` 1707` ``` by transfer rule ``` hoelzl@59000 ` 1708` hoelzl@59000 ` 1709` ```lemma set_pmf_of_set[simp]: "set_pmf pmf_of_set = S" ``` hoelzl@59000 ` 1710` ``` using S_finite S_not_empty by (auto simp: set_pmf_iff) ``` hoelzl@59000 ` 1711` Andreas@61634 ` 1712` ```lemma emeasure_pmf_of_set_space[simp]: "emeasure pmf_of_set S = 1" ``` hoelzl@59002 ` 1713` ``` by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff) ``` hoelzl@59002 ` 1714` hoelzl@62975 ` 1715` ```lemma nn_integral_pmf_of_set: "nn_integral (measure_pmf pmf_of_set) f = setsum f S / card S" ``` hoelzl@62975 ` 1716` ``` by (subst nn_integral_measure_pmf_finite) ``` Mathias@63918 ` 1717` ``` (simp_all add: setsum_distrib_right[symmetric] card_gt_0_iff S_not_empty S_finite divide_ennreal_def ``` hoelzl@62975 ` 1718` ``` divide_ennreal[symmetric] ennreal_of_nat_eq_real_of_nat[symmetric] ennreal_times_divide) ``` Andreas@60068 ` 1719` hoelzl@62975 ` 1720` ```lemma integral_pmf_of_set: "integral\<^sup>L (measure_pmf pmf_of_set) f = setsum f S / card S" ``` hoelzl@62975 ` 1721` ``` by (subst integral_measure_pmf[of S]) (auto simp: S_finite setsum_divide_distrib) ``` Andreas@60068 ` 1722` hoelzl@62975 ` 1723` ```lemma emeasure_pmf_of_set: "emeasure (measure_pmf pmf_of_set) A = card (S \ A) / card S" ``` hoelzl@62975 ` 1724` ``` by (subst nn_integral_indicator[symmetric], simp) ``` hoelzl@62975 ` 1725` ``` (simp add: S_finite S_not_empty card_gt_0_iff indicator_def setsum.If_cases divide_ennreal ``` hoelzl@62975 ` 1726` ``` ennreal_of_nat_eq_real_of_nat nn_integral_pmf_of_set) ``` Andreas@60068 ` 1727` hoelzl@62975 ` 1728` ```lemma measure_pmf_of_set: "measure (measure_pmf pmf_of_set) A = card (S \ A) / card S" ``` wenzelm@63092 ` 1729` ``` using emeasure_pmf_of_set[of A] ``` hoelzl@62975 ` 1730` ``` by (simp add: measure_nonneg measure_pmf.emeasure_eq_measure) ``` Andreas@61634 ` 1731` hoelzl@59000 ` 1732` ```end ``` hoelzl@59000 ` 1733` eberlm@63099 ` 1734` ```lemma map_pmf_of_set: ``` eberlm@63099 ` 1735` ``` assumes "finite A" "A \ {}" ``` hoelzl@63886 ` 1736` ``` shows "map_pmf f (pmf_of_set A) = pmf_of_multiset (image_mset f (mset_set A))" ``` eberlm@63099 ` 1737` ``` (is "?lhs = ?rhs") ``` eberlm@63099 ` 1738` ```proof (intro pmf_eqI) ``` eberlm@63099 ` 1739` ``` fix x ``` eberlm@63099 ` 1740` ``` from assms have "ennreal (pmf ?lhs x) = ennreal (pmf ?rhs x)" ``` eberlm@63099 ` 1741` ``` by (subst ennreal_pmf_map) ``` eberlm@63099 ` 1742` ``` (simp_all add: emeasure_pmf_of_set mset_set_empty_iff count_image_mset Int_commute) ``` eberlm@63099 ` 1743` ``` thus "pmf ?lhs x = pmf ?rhs x" by simp ``` eberlm@63099 ` 1744` ```qed ``` eberlm@63099 ` 1745` eberlm@63099 ` 1746` ```lemma pmf_bind_pmf_of_set: ``` eberlm@63099 ` 1747` ``` assumes "A \ {}" "finite A" ``` hoelzl@63886 ` 1748` ``` shows "pmf (bind_pmf (pmf_of_set A) f) x = ``` eberlm@63099 ` 1749` ``` (\xa\A. pmf (f xa) x) / real_of_nat (card A)" (is "?lhs = ?rhs") ``` eberlm@63099 ` 1750` ```proof - ``` eberlm@63099 ` 1751` ``` from assms have "card A > 0" by auto ``` eberlm@63099 ` 1752` ``` with assms have "ennreal ?lhs = ennreal ?rhs" ``` hoelzl@63886 ` 1753` ``` by (subst ennreal_pmf_bind) ``` hoelzl@63886 ` 1754` ``` (simp_all add: nn_integral_pmf_of_set max_def pmf_nonneg divide_ennreal [symmetric] ``` eberlm@63099 ` 1755` ``` setsum_nonneg ennreal_of_nat_eq_real_of_nat) ``` eberlm@63099 ` 1756` ``` thus ?thesis by (subst (asm) ennreal_inj) (auto intro!: setsum_nonneg divide_nonneg_nonneg) ``` eberlm@63099 ` 1757` ```qed ``` eberlm@63099 ` 1758` Andreas@60068 ` 1759` ```lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x" ``` Andreas@60068 ` 1760` ```by(rule pmf_eqI)(simp add: indicator_def) ``` Andreas@60068 ` 1761` lp15@61609 ` 1762` ```lemma map_pmf_of_set_inj: ``` Andreas@60068 ` 1763` ``` assumes f: "inj_on f A" ``` Andreas@60068 ` 1764` ``` and [simp]: "A \ {}" "finite A" ``` Andreas@60068 ` 1765` ``` shows "map_pmf f (pmf_of_set A) = pmf_of_set (f ` A)" (is "?lhs = ?rhs") ``` Andreas@60068 ` 1766` ```proof(rule pmf_eqI) ``` Andreas@60068 ` 1767` ``` fix i ``` Andreas@60068 ` 1768` ``` show "pmf ?lhs i = pmf ?rhs i" ``` Andreas@60068 ` 1769` ``` proof(cases "i \ f ` A") ``` Andreas@60068 ` 1770` ``` case True ``` Andreas@60068 ` 1771` ``` then obtain i' where "i = f i'" "i' \ A" by auto ``` Andreas@60068 ` 1772` ``` thus ?thesis using f by(simp add: card_image pmf_map_inj) ``` Andreas@60068 ` 1773` ``` next ``` Andreas@60068 ` 1774` ``` case False ``` Andreas@60068 ` 1775` ``` hence "pmf ?lhs i = 0" by(simp add: pmf_eq_0_set_pmf set_map_pmf) ``` Andreas@60068 ` 1776` ``` moreover have "pmf ?rhs i = 0" using False by simp ``` Andreas@60068 ` 1777` ``` ultimately show ?thesis by simp ``` Andreas@60068 ` 1778` ``` qed ``` Andreas@60068 ` 1779` ```qed ``` Andreas@60068 ` 1780` eberlm@63099 ` 1781` ```text \ ``` hoelzl@63886 ` 1782` ``` Choosing an element uniformly at random from the union of a disjoint family ``` hoelzl@63886 ` 1783` ``` of finite non-empty sets with the same size is the same as first choosing a set ``` hoelzl@63886 ` 1784` ``` from the family uniformly at random and then choosing an element from the chosen set ``` hoelzl@63886 ` 1785` ``` uniformly at random. ``` eberlm@63099 ` 1786` ```\ ``` eberlm@63099 ` 1787` ```lemma pmf_of_set_UN: ``` eberlm@63099 ` 1788` ``` assumes "finite (UNION A f)" "A \ {}" "\x. x \ A \ f x \ {}" ``` eberlm@63099 ` 1789` ``` "\x. x \ A \ card (f x) = n" "disjoint_family_on f A" ``` eberlm@63099 ` 1790` ``` shows "pmf_of_set (UNION A f) = do {x \ pmf_of_set A; pmf_of_set (f x)}" ``` eberlm@63099 ` 1791` ``` (is "?lhs = ?rhs") ``` eberlm@63099 ` 1792` ```proof (intro pmf_eqI) ``` eberlm@63099 ` 1793` ``` fix x ``` eberlm@63099 ` 1794` ``` from assms have [simp]: "finite A" ``` eberlm@63099 ` 1795` ``` using infinite_disjoint_family_imp_infinite_UNION[of A f] by blast ``` eberlm@63099 ` 1796` ``` from assms have "ereal (pmf (pmf_of_set (UNION A f)) x) = ``` eberlm@63099 ` 1797` ``` ereal (indicator (\x\A. f x) x / real (card (\x\A. f x)))" ``` eberlm@63099 ` 1798` ``` by (subst pmf_of_set) auto ``` eberlm@63099 ` 1799` ``` also from assms have "card (\x\A. f x) = card A * n" ``` eberlm@63099 ` 1800` ``` by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def) ``` hoelzl@63886 ` 1801` ``` also from assms ``` hoelzl@63886 ` 1802` ``` have "indicator (\x\A. f x) x / real \ = ``` eberlm@63099 ` 1803` ``` indicator (\x\A. f x) x / (n * real (card A))" ``` eberlm@63099 ` 1804` ``` by (simp add: setsum_divide_distrib [symmetric] mult_ac) ``` eberlm@63099 ` 1805` ``` also from assms have "indicator (\x\A. f x) x = (\y\A. indicator (f y) x)" ``` eberlm@63099 ` 1806` ``` by (intro indicator_UN_disjoint) simp_all ``` eberlm@63099 ` 1807` ``` also from assms have "ereal ((\y\A. indicator (f y) x) / (real n * real (card A))) = ``` eberlm@63099 ` 1808` ``` ereal (pmf ?rhs x)" ``` eberlm@63099 ` 1809` ``` by (subst pmf_bind_pmf_of_set) (simp_all add: setsum_divide_distrib) ``` eberlm@63099 ` 1810` ``` finally show "pmf ?lhs x = pmf ?rhs x" by simp ``` eberlm@63099 ` 1811` ```qed ``` eberlm@63099 ` 1812` Andreas@60068 ` 1813` ```lemma bernoulli_pmf_half_conv_pmf_of_set: "bernoulli_pmf (1 / 2) = pmf_of_set UNIV" ``` hoelzl@62975 ` 1814` ``` by (rule pmf_eqI) simp_all ``` Andreas@61634 ` 1815` hoelzl@59093 ` 1816` ```subsubsection \ Poisson Distribution \ ``` hoelzl@59093 ` 1817` hoelzl@59093 ` 1818` ```context ``` hoelzl@59093 ` 1819` ``` fixes rate :: real assumes rate_pos: "0 < rate" ``` hoelzl@59093 ` 1820` ```begin ``` hoelzl@59093 ` 1821` hoelzl@59093 ` 1822` ```lift_definition poisson_pmf :: "nat pmf" is "\k. rate ^ k / fact k * exp (-rate)" ``` lp15@59730 ` 1823` ```proof (* by Manuel Eberl *) ``` hoelzl@59093 ` 1824` ``` have summable: "summable (\x::nat. rate ^ x / fact x)" using summable_exp ``` haftmann@59557 ` 1825` ``` by (simp add: field_simps divide_inverse [symmetric]) ``` hoelzl@59093 ` 1826` ``` have "(\\<^sup>+(x::nat). rate ^ x / fact x * exp (-rate) \count_space UNIV) = ``` hoelzl@59093 ` 1827` ``` exp (-rate) * (\\<^sup>+(x::nat). rate ^ x / fact x \count_space UNIV)" ``` hoelzl@62975 ` 1828` ``` by (simp add: field_simps nn_integral_cmult[symmetric] ennreal_mult'[symmetric]) ``` hoelzl@59093 ` 1829` ``` also from rate_pos have "(\\<^sup>+(x::nat). rate ^ x / fact x \count_space UNIV) = (\x. rate ^ x / fact x)" ``` hoelzl@62975 ` 1830` ``` by (simp_all add: nn_integral_count_space_nat suminf_ennreal summable ennreal_suminf_neq_top) ``` hoelzl@59093 ` 1831` ``` also have "... = exp rate" unfolding exp_def ``` lp15@59730 ` 1832` ``` by (simp add: field_simps divide_inverse [symmetric]) ``` hoelzl@62975 ` 1833` ``` also have "ennreal (exp (-rate)) * ennreal (exp rate) = 1" ``` hoelzl@62975 ` 1834` ``` by (simp add: mult_exp_exp ennreal_mult[symmetric]) ``` hoelzl@62975 ` 1835` ``` finally show "(\\<^sup>+ x. ennreal (rate ^ x / (fact x) * exp (- rate)) \count_space UNIV) = 1" . ``` hoelzl@59093 ` 1836` ```qed (simp add: rate_pos[THEN less_imp_le]) ``` hoelzl@59093 ` 1837` hoelzl@59093 ` 1838` ```lemma pmf_poisson[simp]: "pmf poisson_pmf k = rate ^ k / fact k * exp (-rate)" ``` hoelzl@59093 ` 1839` ``` by transfer rule ``` hoelzl@59093 ` 1840` hoelzl@59093 ` 1841` ```lemma set_pmf_poisson[simp]: "set_pmf poisson_pmf = UNIV" ``` hoelzl@59093 ` 1842` ``` using rate_pos by (auto simp: set_pmf_iff) ``` hoelzl@59093 ` 1843` hoelzl@59000 ` 1844` ```end ``` hoelzl@59000 ` 1845` hoelzl@59093 ` 1846` ```subsubsection \ Binomial Distribution \ ``` hoelzl@59093 ` 1847` hoelzl@59093 ` 1848` ```context ``` hoelzl@59093 ` 1849` ``` fixes n :: nat and p :: real assumes p_nonneg: "0 \ p" and p_le_1: "p \ 1" ``` hoelzl@59093 ` 1850` ```begin ``` hoelzl@59093 ` 1851` hoelzl@59093 ` 1852` ```lift_definition binomial_pmf :: "nat pmf" is "\k. (n choose k) * p^k * (1 - p)^(n - k)" ``` hoelzl@59093 ` 1853` ```proof ``` hoelzl@62975 ` 1854` ``` have "(\\<^sup>+k. ennreal (real (n choose k) * p ^ k * (1 - p) ^ (n - k)) \count_space UNIV) = ``` hoelzl@62975 ` 1855` ``` ennreal (\k\n. real (n choose k) * p ^ k * (1 - p) ^ (n - k))" ``` hoelzl@59093 ` 1856` ``` using p_le_1 p_nonneg by (subst nn_integral_count_space') auto ``` hoelzl@59093 ` 1857` ``` also have "(\k\n. real (n choose k) * p ^ k * (1 - p) ^ (n - k)) = (p + (1 - p)) ^ n" ``` lp15@61609 ` 1858` ``` by (subst binomial_ring) (simp add: atLeast0AtMost) ``` hoelzl@62975 ` 1859` ``` finally show "(\\<^sup>+ x. ennreal (real (n choose x) * p ^ x * (1 - p) ^ (n - x)) \count_space UNIV) = 1" ``` hoelzl@59093 ` 1860` ``` by simp ``` hoelzl@59093 ` 1861` ```qed (insert p_nonneg p_le_1, simp) ``` hoelzl@59093 ` 1862` hoelzl@59093 ` 1863` ```lemma pmf_binomial[simp]: "pmf binomial_pmf k = (n choose k) * p^k * (1 - p)^(n - k)" ``` hoelzl@59093 ` 1864` ``` by transfer rule ``` hoelzl@59093 ` 1865` hoelzl@59093 ` 1866` ```lemma set_pmf_binomial_eq: "set_pmf binomial_pmf = (if p = 0 then {0} else if p = 1 then {n} else {.. n})" ``` hoelzl@59093 ` 1867` ``` using p_nonneg p_le_1 unfolding set_eq_iff set_pmf_iff pmf_binomial by (auto simp: set_pmf_iff) ``` hoelzl@59093 ` 1868` hoelzl@59093 ` 1869` ```end ``` hoelzl@59093 ` 1870` hoelzl@59093 ` 1871` ```end ``` hoelzl@59093 ` 1872` hoelzl@59093 ` 1873` ```lemma set_pmf_binomial_0[simp]: "set_pmf (binomial_pmf n 0) = {0}" ``` hoelzl@59093 ` 1874` ``` by (simp add: set_pmf_binomial_eq) ``` hoelzl@59093 ` 1875` hoelzl@59093 ` 1876` ```lemma set_pmf_binomial_1[simp]: "set_pmf (binomial_pmf n 1) = {n}" ``` hoelzl@59093 ` 1877` ``` by (simp add: set_pmf_binomial_eq) ``` hoelzl@59093 ` 1878` hoelzl@59093 ` 1879` ```lemma set_pmf_binomial[simp]: "0 < p \ p < 1 \ set_pmf (binomial_pmf n p) = {..n}" ``` hoelzl@59093 ` 1880` ``` by (simp add: set_pmf_binomial_eq) ``` hoelzl@59093 ` 1881` wenzelm@63343 ` 1882` ```context includes lifting_syntax ``` wenzelm@63343 ` 1883` ```begin ``` Andreas@61634 ` 1884` Andreas@61634 ` 1885` ```lemma bind_pmf_parametric [transfer_rule]: ``` Andreas@61634 ` 1886` ``` "(rel_pmf A ===> (A ===> rel_pmf B) ===> rel_pmf B) bind_pmf bind_pmf" ``` Andreas@61634 ` 1887` ```by(blast intro: rel_pmf_bindI dest: rel_funD) ``` Andreas@61634 ` 1888` Andreas@61634 ` 1889` ```lemma return_pmf_parametric [transfer_rule]: "(A ===> rel_pmf A) return_pmf return_pmf" ``` Andreas@61634 ` 1890` ```by(rule rel_funI) simp ``` Andreas@61634 ` 1891` hoelzl@59000 ` 1892` ```end ``` Andreas@61634 ` 1893` eberlm@63099 ` 1894` eberlm@63194 ` 1895` ```primrec replicate_pmf :: "nat \ 'a pmf \ 'a list pmf" where ``` eberlm@63194 ` 1896` ``` "replicate_pmf 0 _ = return_pmf []" ``` eberlm@63194 ` 1897` ```| "replicate_pmf (Suc n) p = do {x \ p; xs \ replicate_pmf n p; return_pmf (x#xs)}" ``` eberlm@63194 ` 1898` eberlm@63194 ` 1899` ```lemma replicate_pmf_1: "replicate_pmf 1 p = map_pmf (\x. [x]) p" ``` eberlm@63194 ` 1900` ``` by (simp add: map_pmf_def bind_return_pmf) ``` hoelzl@63886 ` 1901` hoelzl@63886 ` 1902` ```lemma set_replicate_pmf: ``` eberlm@63194 ` 1903` ``` "set_pmf (replicate_pmf n p) = {xs\lists (set_pmf p). length xs = n}" ``` eberlm@63194 ` 1904` ``` by (induction n) (auto simp: length_Suc_conv) ``` eberlm@63194 ` 1905` eberlm@63194 ` 1906` ```lemma replicate_pmf_distrib: ``` hoelzl@63886 ` 1907` ``` "replicate_pmf (m + n) p = ``` eberlm@63194 ` 1908` ``` do {xs \ replicate_pmf m p; ys \ replicate_pmf n p; return_pmf (xs @ ys)}" ``` eberlm@63194 ` 1909` ``` by (induction m) (simp_all add: bind_return_pmf bind_return_pmf' bind_assoc_pmf) ``` eberlm@63194 ` 1910` hoelzl@63886 ` 1911` ```lemma power_diff': ``` eberlm@63194 ` 1912` ``` assumes "b \ a" ``` eberlm@63194 ` 1913` ``` shows "x ^ (a - b) = (if x = 0 \ a = b then 1 else x ^ a / (x::'a::field) ^ b)" ``` eberlm@63194 ` 1914` ```proof (cases "x = 0") ``` eberlm@63194 ` 1915` ``` case True ``` eberlm@63194 ` 1916` ``` with assms show ?thesis by (cases "a - b") simp_all ``` eberlm@63194 ` 1917` ```qed (insert assms, simp_all add: power_diff) ``` eberlm@63194 ` 1918` hoelzl@63886 ` 1919` eberlm@63194 ` 1920` ```lemma binomial_pmf_Suc: ``` eberlm@63194 ` 1921` ``` assumes "p \ {0..1}" ``` hoelzl@63886 ` 1922` ``` shows "binomial_pmf (Suc n) p = ``` hoelzl@63886 ` 1923` ``` do {b \ bernoulli_pmf p; ``` hoelzl@63886 ` 1924` ``` k \ binomial_pmf n p; ``` eberlm@63194 ` 1925` ``` return_pmf ((if b then 1 else 0) + k)}" (is "_ = ?rhs") ``` eberlm@63194 ` 1926` ```proof (intro pmf_eqI) ``` eberlm@63194 ` 1927` ``` fix k ``` eberlm@63194 ` 1928` ``` have A: "indicator {Suc a} (Suc b) = indicator {a} b" for a b ``` eberlm@63194 ` 1929` ``` by (simp add: indicator_def) ``` eberlm@63194 ` 1930` ``` show "pmf (binomial_pmf (Suc n) p) k = pmf ?rhs k" ``` eberlm@63194 ` 1931` ``` by (cases k; cases "k > n") ``` eberlm@63194 ` 1932` ``` (insert assms, auto simp: pmf_bind measure_pmf_single A divide_simps algebra_simps ``` eberlm@63194 ` 1933` ``` not_less less_eq_Suc_le [symmetric] power_diff') ``` eberlm@63194 ` 1934` ```qed ``` eberlm@63194 ` 1935` eberlm@63194 ` 1936` ```lemma binomial_pmf_0: "p \ {0..1} \ binomial_pmf 0 p = return_pmf 0" ``` eberlm@63194 ` 1937` ``` by (rule pmf_eqI) (simp_all add: indicator_def) ``` eberlm@63194 ` 1938` eberlm@63194 ` 1939` ```lemma binomial_pmf_altdef: ``` eberlm@63194 ` 1940` ``` assumes "p \ {0..1}" ``` eberlm@63194 ` 1941` ``` shows "binomial_pmf n p = map_pmf (length \ filter id) (replicate_pmf n (bernoulli_pmf p))" ``` hoelzl@63886 ` 1942` ``` by (induction n) ``` hoelzl@63886 ` 1943` ``` (insert assms, auto simp: binomial_pmf_Suc map_pmf_def bind_return_pmf bind_assoc_pmf ``` eberlm@63194 ` 1944` ``` bind_return_pmf' binomial_pmf_0 intro!: bind_pmf_cong) ``` eberlm@63194 ` 1945` eberlm@63194 ` 1946` eberlm@63099 ` 1947` ```subsection \PMFs from assiciation lists\ ``` eberlm@63099 ` 1948` hoelzl@63886 ` 1949` ```definition pmf_of_list ::" ('a \ real) list \ 'a pmf" where ``` nipkow@63882 ` 1950` ``` "pmf_of_list xs = embed_pmf (\x. sum_list (map snd (filter (\z. fst z = x) xs)))" ``` eberlm@63099 ` 1951` eberlm@63099 ` 1952` ```definition pmf_of_list_wf where ``` nipkow@63882 ` 1953` ``` "pmf_of_list_wf xs \ (\x\set (map snd xs) . x \ 0) \ sum_list (map snd xs) = 1" ``` eberlm@63099 ` 1954` eberlm@63099 ` 1955` ```lemma pmf_of_list_wfI: ``` nipkow@63882 ` 1956` ``` "(\x. x \ set (map snd xs) \ x \ 0) \ sum_list (map snd xs) = 1 \ pmf_of_list_wf xs" ``` eberlm@63099 ` 1957` ``` unfolding pmf_of_list_wf_def by simp ``` eberlm@63099 ` 1958` eberlm@63099 ` 1959` ```context ``` eberlm@63099 ` 1960` ```begin ``` eberlm@63099 ` 1961` eberlm@63099 ` 1962` ```private lemma pmf_of_list_aux: ``` eberlm@63099 ` 1963` ``` assumes "\x. x \ set (map snd xs) \ x \ 0" ``` nipkow@63882 ` 1964` ``` assumes "sum_list (map snd xs) = 1" ``` nipkow@63882 ` 1965` ``` shows "(\\<^sup>+ x. ennreal (sum_list (map snd [z\xs . fst z = x])) \count_space UNIV) = 1" ``` eberlm@63099 ` 1966` ```proof - ``` nipkow@63882 ` 1967` ``` have "(\\<^sup>+ x. ennreal (sum_list (map snd (filter (\z. fst z = x) xs))) \count_space UNIV) = ``` nipkow@63882 ` 1968` ``` (\\<^sup>+ x. ennreal (sum_list (map (\(x',p). indicator {x'} x * p) xs)) \count_space UNIV)" ``` nipkow@63882 ` 1969` ``` by (intro nn_integral_cong ennreal_cong, subst sum_list_map_filter') (auto intro: sum_list_cong) ``` eberlm@63099 ` 1970` ``` also have "\ = (\(x',p)\xs. (\\<^sup>+ x. ennreal (indicator {x'} x * p) \count_space UNIV))" ``` eberlm@63099 ` 1971` ``` using assms(1) ``` eberlm@63099 ` 1972` ``` proof (induction xs) ``` eberlm@63099 ` 1973` ``` case (Cons x xs) ``` eberlm@63099 ` 1974` ``` from Cons.prems have "snd x \ 0" by simp ``` eberlm@63099 ` 1975` ``` moreover have "b \ 0" if "(a,b) \ set xs" for a b ``` eberlm@63099 ` 1976` ``` using Cons.prems[of b] that by force ``` hoelzl@63886 ` 1977` ``` ultimately have "(\\<^sup>+ y. ennreal (\(x', p)\x # xs. indicator {x'} y * p) \count_space UNIV) = ``` hoelzl@63886 ` 1978` ``` (\\<^sup>+ y. ennreal (indicator {fst x} y * snd x) + ``` eberlm@63099 ` 1979` ``` ennreal (\(x', p)\xs. indicator {x'} y * p) \count_space UNIV)" ``` hoelzl@63886 ` 1980` ``` by (intro nn_integral_cong, subst ennreal_plus [symmetric]) ``` nipkow@63882 ` 1981` ``` (auto simp: case_prod_unfold indicator_def intro!: sum_list_nonneg) ``` hoelzl@63886 ` 1982` ``` also have "\ = (\\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \count_space UNIV) + ``` eberlm@63099 ` 1983` ``` (\\<^sup>+ y. ennreal (\(x', p)\xs. indicator {x'} y * p) \count_space UNIV)" ``` eberlm@63099 ` 1984` ``` by (intro nn_integral_add) ``` nipkow@63882 ` 1985` ``` (force intro!: sum_list_nonneg AE_I2 intro: Cons simp: indicator_def)+ ``` eberlm@63099 ` 1986` ``` also have "(\\<^sup>+ y. ennreal (\(x', p)\xs. indicator {x'} y * p) \count_space UNIV) = ``` eberlm@63099 ` 1987` ``` (\(x', p)\xs. (\\<^sup>+ y. ennreal (indicator {x'} y * p) \count_space UNIV))" ``` eberlm@63099 ` 1988` ``` using Cons(1) by (intro Cons) simp_all ``` eberlm@63099 ` 1989` ``` finally show ?case by (simp add: case_prod_unfold) ``` eberlm@63099 ` 1990` ``` qed simp ``` eberlm@63099 ` 1991` ``` also have "\ = (\(x',p)\xs. ennreal p * (\\<^sup>+ x. indicator {x'} x \count_space UNIV))" ``` eberlm@63099 ` 1992` ``` using assms(1) ``` nipkow@63882 ` 1993` ``` by (intro sum_list_cong, simp only: case_prod_unfold, subst nn_integral_cmult [symmetric]) ``` eberlm@63099 ` 1994` ``` (auto intro!: assms(1) simp: max_def times_ereal.simps [symmetric] mult_ac ereal_indicator ``` eberlm@63099 ` 1995` ``` simp del: times_ereal.simps)+ ``` nipkow@63882 ` 1996` ``` also from assms have "\ = sum_list (map snd xs)" by (simp add: case_prod_unfold sum_list_ennreal) ``` eberlm@63099 ` 1997` ``` also have "\ = 1" using assms(2) by simp ``` eberlm@63099 ` 1998` ``` finally show ?thesis . ``` eberlm@63099 ` 1999` ```qed ``` eberlm@63099 ` 2000` eberlm@63099 ` 2001` ```lemma pmf_pmf_of_list: ``` eberlm@63099 ` 2002` ``` assumes "pmf_of_list_wf xs" ``` nipkow@63882 ` 2003` ``` shows "pmf (pmf_of_list xs) x = sum_list (map snd (filter (\z. fst z = x) xs))" ``` eberlm@63099 ` 2004` ``` using assms pmf_of_list_aux[of xs] unfolding pmf_of_list_def pmf_of_list_wf_def ``` nipkow@63882 ` 2005` ``` by (subst pmf_embed_pmf) (auto intro!: sum_list_nonneg) ``` eberlm@63099 ` 2006` Andreas@61634 ` 2007` ```end ``` eberlm@63099 ` 2008` eberlm@63099 ` 2009` ```lemma set_pmf_of_list: ``` eberlm@63099 ` 2010` ``` assumes "pmf_of_list_wf xs" ``` eberlm@63099 ` 2011` ``` shows "set_pmf (pmf_of_list xs) \ set (map fst xs)" ``` eberlm@63099 ` 2012` ```proof clarify ``` eberlm@63099 ` 2013` ``` fix x assume A: "x \ set_pmf (pmf_of_list xs)" ``` eberlm@63099 ` 2014` ``` show "x \ set (map fst xs)" ``` eberlm@63099 ` 2015` ``` proof (rule ccontr) ``` eberlm@63099 ` 2016` ``` assume "x \ set (map fst xs)" ``` eberlm@63099 ` 2017` ``` hence "[z\xs . fst z = x] = []" by (auto simp: filter_empty_conv) ``` eberlm@63099 ` 2018` ``` with A assms show False by (simp add: pmf_pmf_of_list set_pmf_eq) ``` eberlm@63099 ` 2019` ``` qed ``` eberlm@63099 ` 2020` ```qed ``` eberlm@63099 ` 2021` eberlm@63099 ` 2022` ```lemma finite_set_pmf_of_list: ``` eberlm@63099 ` 2023` ``` assumes "pmf_of_list_wf xs" ``` eberlm@63099 ` 2024` ``` shows "finite (set_pmf (pmf_of_list xs))" ``` eberlm@63099 ` 2025` ``` using assms by (rule finite_subset[OF set_pmf_of_list]) simp_all ``` eberlm@63099 ` 2026` eberlm@63099 ` 2027` ```lemma emeasure_Int_set_pmf: ``` eberlm@63099 ` 2028` ``` "emeasure (measure_pmf p) (A \ set_pmf p) = emeasure (measure_pmf p) A" ``` eberlm@63099 ` 2029` ``` by (rule emeasure_eq_AE) (auto simp: AE_measure_pmf_iff) ``` eberlm@63099 ` 2030` eberlm@63099 ` 2031` ```lemma measure_Int_set_pmf: ``` eberlm@63099 ` 2032` ``` "measure (measure_pmf p) (A \ set_pmf p) = measure (measure_pmf p) A" ``` eberlm@63099 ` 2033` ``` using emeasure_Int_set_pmf[of p A] by (simp add: Sigma_Algebra.measure_def) ``` eberlm@63099 ` 2034` eberlm@63099 ` 2035` ```lemma emeasure_pmf_of_list: ``` eberlm@63099 ` 2036` ``` assumes "pmf_of_list_wf xs" ``` nipkow@63882 ` 2037` ``` shows "emeasure (pmf_of_list xs) A = ennreal (sum_list (map snd (filter (\x. fst x \ A) xs)))" ``` eberlm@63099 ` 2038` ```proof - ``` eberlm@63099 ` 2039` ``` have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)" ``` eberlm@63099 ` 2040` ``` by simp ``` hoelzl@63886 ` 2041` ``` also from assms ``` nipkow@63882 ` 2042` ``` have "\ = (\x\set_pmf (pmf_of_list xs) \ A. ennreal (sum_list (map snd [z\xs . fst z = x])))" ``` hoelzl@63973 ` 2043` ``` by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list Int_def) ``` hoelzl@63886 ` 2044` ``` also from assms ``` nipkow@63882 ` 2045` ``` have "\ = ennreal (\x\set_pmf (pmf_of_list xs) \ A. sum_list (map snd [z\xs . fst z = x]))" ``` nipkow@63882 ` 2046` ``` by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg) ``` hoelzl@63886 ` 2047` ``` also have "\ = ennreal (\x\set_pmf (pmf_of_list xs) \ A. ``` eberlm@63099 ` 2048` ``` indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S") ``` eberlm@63099 ` 2049` ``` using assms by (intro ennreal_cong setsum.cong) (auto simp: pmf_pmf_of_list) ``` eberlm@63099 ` 2050` ``` also have "?S = (\x\set_pmf (pmf_of_list xs). indicator A x * pmf (pmf_of_list xs) x)" ``` eberlm@63099 ` 2051` ``` using assms by (intro setsum.mono_neutral_left set_pmf_of_list finite_set_pmf_of_list) auto ``` eberlm@63099 ` 2052` ``` also have "\ = (\x\set (map fst xs). indicator A x * pmf (pmf_of_list xs) x)" ``` eberlm@63099 ` 2053` ``` using assms by (intro setsum.mono_neutral_left set_pmf_of_list) (auto simp: set_pmf_eq) ``` hoelzl@63886 ` 2054` ``` also have "\ = (\x\set (map fst xs). indicator A x * ``` nipkow@63882 ` 2055` ``` sum_list (map snd (filter (\z. fst z = x) xs)))" ``` eberlm@63099 ` 2056` ``` using assms by (simp add: pmf_pmf_of_list) ``` nipkow@63882 ` 2057` ``` also have "\ = (\x\set (map fst xs). sum_list (map snd (filter (\z. fst z = x \ x \ A) xs)))" ``` eberlm@63099 ` 2058` ``` by (intro setsum.cong) (auto simp: indicator_def) ``` eberlm@63099 ` 2059` ``` also have "\ = (\x\set (map fst xs). (\xa = 0.. x \ A then snd (xs ! xa) else 0))" ``` nipkow@63882 ` 2061` ``` by (intro setsum.cong refl, subst sum_list_map_filter', subst sum_list_setsum_nth) simp ``` hoelzl@63886 ` 2062` ``` also have "\ = (\xa = 0..x\set (map fst xs). ``` eberlm@63099 ` 2063` ``` if fst (xs ! xa) = x \ x \ A then snd (xs ! xa) else 0))" ``` eberlm@63099 ` 2064` ``` by (rule setsum.commute) ``` hoelzl@63886 ` 2065` ``` also have "\ = (\xa = 0.. A then ``` eberlm@63099 ` 2066` ``` (\x\set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)" ``` eberlm@63099 ` 2067` ``` by (auto intro!: setsum.cong setsum.neutral) ``` eberlm@63099 ` 2068` ``` also have "\ = (\xa = 0.. A then snd (xs ! xa) else 0)" ``` eberlm@63099 ` 2069` ``` by (intro setsum.cong refl) (simp_all add: setsum.delta) ``` nipkow@63882 ` 2070` ``` also have "\ = sum_list (map snd (filter (\x. fst x \ A) xs))" ``` nipkow@63882 ` 2071` ``` by (subst sum_list_map_filter', subst sum_list_setsum_nth) simp_all ``` hoelzl@63886 ` 2072` ``` finally show ?thesis . ``` eberlm@63099 ` 2073` ```qed ``` eberlm@63099 ` 2074` eberlm@63099 ` 2075` ```lemma measure_pmf_of_list: ``` eberlm@63099 ` 2076` ``` assumes "pmf_of_list_wf xs" ``` nipkow@63882 ` 2077` ``` shows "measure (pmf_of_list xs) A = sum_list (map snd (filter (\x. fst x \ A) xs))" ``` eberlm@63099 ` 2078` ``` using assms unfolding pmf_of_list_wf_def Sigma_Algebra.measure_def ``` nipkow@63882 ` 2079` ``` by (subst emeasure_pmf_of_list [OF assms], subst enn2real_ennreal) (auto intro!: sum_list_nonneg) ``` eberlm@63099 ` 2080` eberlm@63194 ` 2081` ```(* TODO Move? *) ``` nipkow@63882 ` 2082` ```lemma sum_list_nonneg_eq_zero_iff: ``` eberlm@63194 ` 2083` ``` fixes xs :: "'a :: linordered_ab_group_add list" ``` nipkow@63882 ` 2084` ``` shows "(\x. x \ set xs \ x \ 0) \ sum_list xs = 0 \ set xs \ {0}" ``` eberlm@63194 ` 2085` ```proof (induction xs) ``` eberlm@63194 ` 2086` ``` case (Cons x xs) ``` nipkow@63882 ` 2087` ``` from Cons.prems have "sum_list (x#xs) = 0 \ x = 0 \ sum_list xs = 0" ``` nipkow@63882 ` 2088` ``` unfolding sum_list_simps by (subst add_nonneg_eq_0_iff) (auto intro: sum_list_nonneg) ``` eberlm@63194 ` 2089` ``` with Cons.IH Cons.prems show ?case by simp ``` eberlm@63194 ` 2090` ```qed simp_all ``` eberlm@63194 ` 2091` nipkow@63882 ` 2092` ```lemma sum_list_filter_nonzero: ``` nipkow@63882 ` 2093` ``` "sum_list (filter (\x. x \ 0) xs) = sum_list xs" ``` eberlm@63194 ` 2094` ``` by (induction xs) simp_all ``` eberlm@63194 ` 2095` ```(* END MOVE *) ``` hoelzl@63886 ` 2096` eberlm@63194 ` 2097` ```lemma set_pmf_of_list_eq: ``` eberlm@63194 ` 2098` ``` assumes "pmf_of_list_wf xs" "\x. x \ snd ` set xs \ x > 0" ``` eberlm@63194 ` 2099` ``` shows "set_pmf (pmf_of_list xs) = fst ` set xs" ``` eberlm@63194 ` 2100` ```proof ``` eberlm@63194 ` 2101` ``` { ``` eberlm@63194 ` 2102` ``` fix x assume A: "x \ fst ` set xs" and B: "x \ set_pmf (pmf_of_list xs)" ``` eberlm@63194 ` 2103` ``` then obtain y where y: "(x, y) \ set xs" by auto ``` nipkow@63882 ` 2104` ``` from B have "sum_list (map snd [z\xs. fst z = x]) = 0" ``` eberlm@63194 ` 2105` ``` by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq) ``` eberlm@63194 ` 2106` ``` moreover from y have "y \ snd ` {xa \ set xs. fst xa = x}" by force ``` hoelzl@63886 ` 2107` ``` ultimately have "y = 0" using assms(1) ``` nipkow@63882 ` 2108` ``` by (subst (asm) sum_list_nonneg_eq_zero_iff) (auto simp: pmf_of_list_wf_def) ``` eberlm@63194 ` 2109` ``` with assms(2) y have False by force ``` eberlm@63194 ` 2110` ``` } ``` eberlm@63194 ` 2111` ``` thus "fst ` set xs \ set_pmf (pmf_of_list xs)" by blast ``` eberlm@63194 ` 2112` ```qed (insert set_pmf_of_list[OF assms(1)], simp_all) ``` hoelzl@63886 ` 2113` eberlm@63194 ` 2114` ```lemma pmf_of_list_remove_zeros: ``` eberlm@63194 ` 2115` ``` assumes "pmf_of_list_wf xs" ``` eberlm@63194 ` 2116` ``` defines "xs' \ filter (\z. snd z \ 0) xs" ``` eberlm@63194 ` 2117` ``` shows "pmf_of_list_wf xs'" "pmf_of_list xs' = pmf_of_list xs" ``` eberlm@63194 ` 2118` ```proof - ``` eberlm@63194 ` 2119` ``` have "map snd [z\xs . snd z \ 0] = filter (\x. x \ 0) (map snd xs)" ``` eberlm@63194 ` 2120` ``` by (induction xs) simp_all ``` eberlm@63194 ` 2121` ``` with assms(1) show wf: "pmf_of_list_wf xs'" ``` nipkow@63882 ` 2122` ``` by (auto simp: pmf_of_list_wf_def xs'_def sum_list_filter_nonzero) ``` nipkow@63882 ` 2123` ``` have "sum_list (map snd [z\xs' . fst z = i]) = sum_list (map snd [z\xs . fst z = i])" for i ``` eberlm@63194 ` 2124` ``` unfolding xs'_def by (induction xs) simp_all ``` eberlm@63194 ` 2125` ``` with assms(1) wf show "pmf_of_list xs' = pmf_of_list xs" ``` eberlm@63194 ` 2126` ``` by (intro pmf_eqI) (simp_all add: pmf_pmf_of_list) ``` eberlm@63194 ` 2127` ```qed ``` eberlm@63194 ` 2128` eberlm@63099 ` 2129` ```end ```