src/HOL/Probability/Probability_Mass_Function.thy
 author nipkow Tue Feb 23 16:25:08 2016 +0100 (2016-02-23) changeset 62390 842917225d56 parent 62324 ae44f16dcea5 child 62975 1d066f6ab25d permissions -rw-r--r--
more canonical names
 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@59664 ` 25` ``` by (auto simp: emeasure_le_0_iff) } ``` 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@59494 ` 32` ```lemma ereal_divide': "b \ 0 \ ereal (a / b) = ereal a / ereal b" ``` hoelzl@59494 ` 33` ``` using ereal_divide[of a b] by simp ``` hoelzl@59494 ` 34` hoelzl@59000 ` 35` ```lemma (in finite_measure) AE_support_countable: ``` hoelzl@59000 ` 36` ``` assumes [simp]: "sets M = UNIV" ``` hoelzl@59000 ` 37` ``` shows "(AE x in M. measure M {x} \ 0) \ (\S. countable S \ (AE x in M. x \ S))" ``` hoelzl@59000 ` 38` ```proof ``` hoelzl@59000 ` 39` ``` assume "\S. countable S \ (AE x in M. x \ S)" ``` hoelzl@59000 ` 40` ``` then obtain S where S[intro]: "countable S" and ae: "AE x in M. x \ S" ``` hoelzl@59000 ` 41` ``` by auto ``` lp15@59667 ` 42` ``` then have "emeasure M (\x\{x\S. emeasure M {x} \ 0}. {x}) = ``` hoelzl@59000 ` 43` ``` (\\<^sup>+ x. emeasure M {x} * indicator {x\S. emeasure M {x} \ 0} x \count_space UNIV)" ``` hoelzl@59000 ` 44` ``` by (subst emeasure_UN_countable) ``` hoelzl@59000 ` 45` ``` (auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space) ``` hoelzl@59000 ` 46` ``` also have "\ = (\\<^sup>+ x. emeasure M {x} * indicator S x \count_space UNIV)" ``` hoelzl@59000 ` 47` ``` by (auto intro!: nn_integral_cong split: split_indicator) ``` hoelzl@59000 ` 48` ``` also have "\ = emeasure M (\x\S. {x})" ``` hoelzl@59000 ` 49` ``` by (subst emeasure_UN_countable) ``` hoelzl@59000 ` 50` ``` (auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space) ``` hoelzl@59000 ` 51` ``` also have "\ = emeasure M (space M)" ``` hoelzl@59000 ` 52` ``` using ae by (intro emeasure_eq_AE) auto ``` hoelzl@59000 ` 53` ``` finally have "emeasure M {x \ space M. x\S \ emeasure M {x} \ 0} = emeasure M (space M)" ``` hoelzl@59000 ` 54` ``` by (simp add: emeasure_single_in_space cong: rev_conj_cong) ``` hoelzl@59000 ` 55` ``` with finite_measure_compl[of "{x \ space M. x\S \ emeasure M {x} \ 0}"] ``` hoelzl@59000 ` 56` ``` have "AE x in M. x \ S \ emeasure M {x} \ 0" ``` hoelzl@59000 ` 57` ``` by (intro AE_I[OF order_refl]) (auto simp: emeasure_eq_measure set_diff_eq cong: conj_cong) ``` hoelzl@59000 ` 58` ``` then show "AE x in M. measure M {x} \ 0" ``` hoelzl@59000 ` 59` ``` by (auto simp: emeasure_eq_measure) ``` hoelzl@59000 ` 60` ```qed (auto intro!: exI[of _ "{x. measure M {x} \ 0}"] countable_support) ``` hoelzl@59000 ` 61` hoelzl@59664 ` 62` ```subsection \ PMF as measure \ ``` hoelzl@59000 ` 63` hoelzl@58587 ` 64` ```typedef 'a pmf = "{M :: 'a measure. prob_space M \ sets M = UNIV \ (AE x in M. measure M {x} \ 0)}" ``` hoelzl@58587 ` 65` ``` morphisms measure_pmf Abs_pmf ``` hoelzl@58606 ` 66` ``` by (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"]) ``` hoelzl@58606 ` 67` ``` (auto intro!: prob_space_uniform_measure AE_uniform_measureI) ``` hoelzl@58587 ` 68` hoelzl@58587 ` 69` ```declare [[coercion measure_pmf]] ``` hoelzl@58587 ` 70` hoelzl@58587 ` 71` ```lemma prob_space_measure_pmf: "prob_space (measure_pmf p)" ``` hoelzl@58587 ` 72` ``` using pmf.measure_pmf[of p] by auto ``` hoelzl@58587 ` 73` wenzelm@61605 ` 74` ```interpretation measure_pmf: prob_space "measure_pmf M" for M ``` hoelzl@58587 ` 75` ``` by (rule prob_space_measure_pmf) ``` hoelzl@58587 ` 76` wenzelm@61605 ` 77` ```interpretation measure_pmf: subprob_space "measure_pmf M" for M ``` hoelzl@59000 ` 78` ``` by (rule prob_space_imp_subprob_space) unfold_locales ``` hoelzl@59000 ` 79` hoelzl@59048 ` 80` ```lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)" ``` hoelzl@59048 ` 81` ``` by unfold_locales ``` hoelzl@59048 ` 82` hoelzl@58587 ` 83` ```locale pmf_as_measure ``` hoelzl@58587 ` 84` ```begin ``` hoelzl@58587 ` 85` hoelzl@58587 ` 86` ```setup_lifting type_definition_pmf ``` hoelzl@58587 ` 87` hoelzl@58587 ` 88` ```end ``` hoelzl@58587 ` 89` hoelzl@58587 ` 90` ```context ``` hoelzl@58587 ` 91` ```begin ``` hoelzl@58587 ` 92` hoelzl@58587 ` 93` ```interpretation pmf_as_measure . ``` hoelzl@58587 ` 94` hoelzl@58587 ` 95` ```lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV" ``` lp15@59667 ` 96` ``` by transfer blast ``` hoelzl@58587 ` 97` hoelzl@59048 ` 98` ```lemma sets_measure_pmf_count_space[measurable_cong]: ``` hoelzl@59048 ` 99` ``` "sets (measure_pmf M) = sets (count_space UNIV)" ``` hoelzl@59000 ` 100` ``` by simp ``` hoelzl@59000 ` 101` hoelzl@58587 ` 102` ```lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV" ``` hoelzl@58587 ` 103` ``` using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp ``` hoelzl@58587 ` 104` Andreas@61634 ` 105` ```lemma measure_pmf_UNIV [simp]: "measure (measure_pmf p) UNIV = 1" ``` Andreas@61634 ` 106` ```using measure_pmf.prob_space[of p] by simp ``` Andreas@61634 ` 107` hoelzl@59048 ` 108` ```lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \ space (subprob_algebra (count_space UNIV))" ``` hoelzl@59048 ` 109` ``` by (simp add: space_subprob_algebra subprob_space_measure_pmf) ``` hoelzl@59048 ` 110` hoelzl@58587 ` 111` ```lemma measurable_pmf_measure1[simp]: "measurable (M :: 'a pmf) N = UNIV \ space N" ``` hoelzl@58587 ` 112` ``` by (auto simp: measurable_def) ``` hoelzl@58587 ` 113` hoelzl@58587 ` 114` ```lemma measurable_pmf_measure2[simp]: "measurable N (M :: 'a pmf) = measurable N (count_space UNIV)" ``` hoelzl@58587 ` 115` ``` by (intro measurable_cong_sets) simp_all ``` hoelzl@58587 ` 116` hoelzl@59664 ` 117` ```lemma measurable_pair_restrict_pmf2: ``` hoelzl@59664 ` 118` ``` assumes "countable A" ``` hoelzl@59664 ` 119` ``` assumes [measurable]: "\y. y \ A \ (\x. f (x, y)) \ measurable M L" ``` hoelzl@59664 ` 120` ``` shows "f \ measurable (M \\<^sub>M restrict_space (measure_pmf N) A) L" (is "f \ measurable ?M _") ``` hoelzl@59664 ` 121` ```proof - ``` hoelzl@59664 ` 122` ``` have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)" ``` hoelzl@59664 ` 123` ``` by (simp add: restrict_count_space) ``` hoelzl@58587 ` 124` hoelzl@59664 ` 125` ``` show ?thesis ``` hoelzl@59664 ` 126` ``` by (intro measurable_compose_countable'[where f="\a b. f (fst b, a)" and g=snd and I=A, ``` haftmann@61424 ` 127` ``` unfolded prod.collapse] assms) ``` hoelzl@59664 ` 128` ``` measurable ``` hoelzl@59664 ` 129` ```qed ``` hoelzl@58587 ` 130` hoelzl@59664 ` 131` ```lemma measurable_pair_restrict_pmf1: ``` hoelzl@59664 ` 132` ``` assumes "countable A" ``` hoelzl@59664 ` 133` ``` assumes [measurable]: "\x. x \ A \ (\y. f (x, y)) \ measurable N L" ``` hoelzl@59664 ` 134` ``` shows "f \ measurable (restrict_space (measure_pmf M) A \\<^sub>M N) L" ``` hoelzl@59664 ` 135` ```proof - ``` hoelzl@59664 ` 136` ``` have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)" ``` hoelzl@59664 ` 137` ``` by (simp add: restrict_count_space) ``` hoelzl@59000 ` 138` hoelzl@59664 ` 139` ``` show ?thesis ``` hoelzl@59664 ` 140` ``` by (intro measurable_compose_countable'[where f="\a b. f (a, snd b)" and g=fst and I=A, ``` haftmann@61424 ` 141` ``` unfolded prod.collapse] assms) ``` hoelzl@59664 ` 142` ``` measurable ``` hoelzl@59664 ` 143` ```qed ``` hoelzl@59664 ` 144` hoelzl@59664 ` 145` ```lift_definition pmf :: "'a pmf \ 'a \ real" is "\M x. measure M {x}" . ``` hoelzl@59664 ` 146` hoelzl@59664 ` 147` ```lift_definition set_pmf :: "'a pmf \ 'a set" is "\M. {x. measure M {x} \ 0}" . ``` hoelzl@59664 ` 148` ```declare [[coercion set_pmf]] ``` hoelzl@58587 ` 149` hoelzl@58587 ` 150` ```lemma AE_measure_pmf: "AE x in (M::'a pmf). x \ M" ``` hoelzl@58587 ` 151` ``` by transfer simp ``` hoelzl@58587 ` 152` hoelzl@58587 ` 153` ```lemma emeasure_pmf_single_eq_zero_iff: ``` hoelzl@58587 ` 154` ``` fixes M :: "'a pmf" ``` hoelzl@58587 ` 155` ``` shows "emeasure M {y} = 0 \ y \ M" ``` hoelzl@58587 ` 156` ``` by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure]) ``` hoelzl@58587 ` 157` hoelzl@58587 ` 158` ```lemma AE_measure_pmf_iff: "(AE x in measure_pmf M. P x) \ (\y\M. P y)" ``` hoelzl@59664 ` 159` ``` using AE_measure_singleton[of M] AE_measure_pmf[of M] ``` hoelzl@59664 ` 160` ``` by (auto simp: set_pmf.rep_eq) ``` hoelzl@59664 ` 161` Andreas@61634 ` 162` ```lemma AE_pmfI: "(\y. y \ set_pmf M \ P y) \ almost_everywhere (measure_pmf M) P" ``` Andreas@61634 ` 163` ```by(simp add: AE_measure_pmf_iff) ``` Andreas@61634 ` 164` hoelzl@59664 ` 165` ```lemma countable_set_pmf [simp]: "countable (set_pmf p)" ``` hoelzl@59664 ` 166` ``` by transfer (metis prob_space.finite_measure finite_measure.countable_support) ``` hoelzl@59664 ` 167` hoelzl@59664 ` 168` ```lemma pmf_positive: "x \ set_pmf p \ 0 < pmf p x" ``` hoelzl@59664 ` 169` ``` by transfer (simp add: less_le measure_nonneg) ``` hoelzl@59664 ` 170` hoelzl@59664 ` 171` ```lemma pmf_nonneg: "0 \ pmf p x" ``` hoelzl@59664 ` 172` ``` by transfer (simp add: measure_nonneg) ``` hoelzl@59664 ` 173` hoelzl@59664 ` 174` ```lemma pmf_le_1: "pmf p x \ 1" ``` hoelzl@59664 ` 175` ``` by (simp add: pmf.rep_eq) ``` hoelzl@58587 ` 176` hoelzl@58587 ` 177` ```lemma set_pmf_not_empty: "set_pmf M \ {}" ``` hoelzl@58587 ` 178` ``` using AE_measure_pmf[of M] by (intro notI) simp ``` hoelzl@58587 ` 179` hoelzl@58587 ` 180` ```lemma set_pmf_iff: "x \ set_pmf M \ pmf M x \ 0" ``` hoelzl@58587 ` 181` ``` by transfer simp ``` hoelzl@58587 ` 182` hoelzl@59664 ` 183` ```lemma set_pmf_eq: "set_pmf M = {x. pmf M x \ 0}" ``` hoelzl@59664 ` 184` ``` by (auto simp: set_pmf_iff) ``` hoelzl@59664 ` 185` hoelzl@59664 ` 186` ```lemma emeasure_pmf_single: ``` hoelzl@59664 ` 187` ``` fixes M :: "'a pmf" ``` hoelzl@59664 ` 188` ``` shows "emeasure M {x} = pmf M x" ``` hoelzl@59664 ` 189` ``` by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure]) ``` hoelzl@59664 ` 190` Andreas@60068 ` 191` ```lemma measure_pmf_single: "measure (measure_pmf M) {x} = pmf M x" ``` Andreas@60068 ` 192` ```using emeasure_pmf_single[of M x] by(simp add: measure_pmf.emeasure_eq_measure) ``` Andreas@60068 ` 193` hoelzl@59000 ` 194` ```lemma emeasure_measure_pmf_finite: "finite S \ emeasure (measure_pmf M) S = (\s\S. pmf M s)" ``` hoelzl@59000 ` 195` ``` by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single) ``` hoelzl@59000 ` 196` Andreas@59023 ` 197` ```lemma measure_measure_pmf_finite: "finite S \ measure (measure_pmf M) S = setsum (pmf M) S" ``` hoelzl@59425 ` 198` ``` using emeasure_measure_pmf_finite[of S M] by(simp add: measure_pmf.emeasure_eq_measure) ``` Andreas@59023 ` 199` hoelzl@59000 ` 200` ```lemma nn_integral_measure_pmf_support: ``` hoelzl@59000 ` 201` ``` fixes f :: "'a \ ereal" ``` hoelzl@59000 ` 202` ``` assumes f: "finite A" and nn: "\x. x \ A \ 0 \ f x" "\x. x \ set_pmf M \ x \ A \ f x = 0" ``` hoelzl@59000 ` 203` ``` shows "(\\<^sup>+x. f x \measure_pmf M) = (\x\A. f x * pmf M x)" ``` hoelzl@59000 ` 204` ```proof - ``` hoelzl@59000 ` 205` ``` have "(\\<^sup>+x. f x \M) = (\\<^sup>+x. f x * indicator A x \M)" ``` hoelzl@59000 ` 206` ``` using nn by (intro nn_integral_cong_AE) (auto simp: AE_measure_pmf_iff split: split_indicator) ``` hoelzl@59000 ` 207` ``` also have "\ = (\x\A. f x * emeasure M {x})" ``` hoelzl@59000 ` 208` ``` using assms by (intro nn_integral_indicator_finite) auto ``` hoelzl@59000 ` 209` ``` finally show ?thesis ``` hoelzl@59000 ` 210` ``` by (simp add: emeasure_measure_pmf_finite) ``` hoelzl@59000 ` 211` ```qed ``` hoelzl@59000 ` 212` hoelzl@59000 ` 213` ```lemma nn_integral_measure_pmf_finite: ``` hoelzl@59000 ` 214` ``` fixes f :: "'a \ ereal" ``` hoelzl@59000 ` 215` ``` assumes f: "finite (set_pmf M)" and nn: "\x. x \ set_pmf M \ 0 \ f x" ``` hoelzl@59000 ` 216` ``` shows "(\\<^sup>+x. f x \measure_pmf M) = (\x\set_pmf M. f x * pmf M x)" ``` hoelzl@59000 ` 217` ``` using assms by (intro nn_integral_measure_pmf_support) auto ``` hoelzl@59000 ` 218` ```lemma integrable_measure_pmf_finite: ``` hoelzl@59000 ` 219` ``` fixes f :: "'a \ 'b::{banach, second_countable_topology}" ``` hoelzl@59000 ` 220` ``` shows "finite (set_pmf M) \ integrable M f" ``` hoelzl@59000 ` 221` ``` by (auto intro!: integrableI_bounded simp: nn_integral_measure_pmf_finite) ``` hoelzl@59000 ` 222` hoelzl@59000 ` 223` ```lemma integral_measure_pmf: ``` hoelzl@59000 ` 224` ``` assumes [simp]: "finite A" and "\a. a \ set_pmf M \ f a \ 0 \ a \ A" ``` hoelzl@59000 ` 225` ``` shows "(\x. f x \measure_pmf M) = (\a\A. f a * pmf M a)" ``` hoelzl@59000 ` 226` ```proof - ``` hoelzl@59000 ` 227` ``` have "(\x. f x \measure_pmf M) = (\x. f x * indicator A x \measure_pmf M)" ``` hoelzl@59000 ` 228` ``` using assms(2) by (intro integral_cong_AE) (auto split: split_indicator simp: AE_measure_pmf_iff) ``` hoelzl@59000 ` 229` ``` also have "\ = (\a\A. f a * pmf M a)" ``` hoelzl@59000 ` 230` ``` by (subst integral_indicator_finite_real) (auto simp: measure_def emeasure_measure_pmf_finite) ``` hoelzl@59000 ` 231` ``` finally show ?thesis . ``` hoelzl@59000 ` 232` ```qed ``` hoelzl@59000 ` 233` hoelzl@59000 ` 234` ```lemma integrable_pmf: "integrable (count_space X) (pmf M)" ``` hoelzl@59000 ` 235` ```proof - ``` hoelzl@59000 ` 236` ``` have " (\\<^sup>+ x. pmf M x \count_space X) = (\\<^sup>+ x. pmf M x \count_space (M \ X))" ``` hoelzl@59000 ` 237` ``` by (auto simp add: nn_integral_count_space_indicator set_pmf_iff intro!: nn_integral_cong split: split_indicator) ``` hoelzl@59000 ` 238` ``` then have "integrable (count_space X) (pmf M) = integrable (count_space (M \ X)) (pmf M)" ``` hoelzl@59000 ` 239` ``` by (simp add: integrable_iff_bounded pmf_nonneg) ``` hoelzl@59000 ` 240` ``` then show ?thesis ``` Andreas@59023 ` 241` ``` by (simp add: pmf.rep_eq measure_pmf.integrable_measure disjoint_family_on_def) ``` hoelzl@59000 ` 242` ```qed ``` hoelzl@59000 ` 243` hoelzl@59000 ` 244` ```lemma integral_pmf: "(\x. pmf M x \count_space X) = measure M X" ``` hoelzl@59000 ` 245` ```proof - ``` hoelzl@59000 ` 246` ``` have "(\x. pmf M x \count_space X) = (\\<^sup>+x. pmf M x \count_space X)" ``` hoelzl@59000 ` 247` ``` by (simp add: pmf_nonneg integrable_pmf nn_integral_eq_integral) ``` hoelzl@59000 ` 248` ``` also have "\ = (\\<^sup>+x. emeasure M {x} \count_space (X \ M))" ``` hoelzl@59000 ` 249` ``` by (auto intro!: nn_integral_cong_AE split: split_indicator ``` hoelzl@59000 ` 250` ``` simp: pmf.rep_eq measure_pmf.emeasure_eq_measure nn_integral_count_space_indicator ``` hoelzl@59000 ` 251` ``` AE_count_space set_pmf_iff) ``` hoelzl@59000 ` 252` ``` also have "\ = emeasure M (X \ M)" ``` hoelzl@59000 ` 253` ``` by (rule emeasure_countable_singleton[symmetric]) (auto intro: countable_set_pmf) ``` hoelzl@59000 ` 254` ``` also have "\ = emeasure M X" ``` hoelzl@59000 ` 255` ``` by (auto intro!: emeasure_eq_AE simp: AE_measure_pmf_iff) ``` hoelzl@59000 ` 256` ``` finally show ?thesis ``` hoelzl@59000 ` 257` ``` by (simp add: measure_pmf.emeasure_eq_measure) ``` hoelzl@59000 ` 258` ```qed ``` hoelzl@59000 ` 259` hoelzl@59000 ` 260` ```lemma integral_pmf_restrict: ``` hoelzl@59000 ` 261` ``` "(f::'a \ 'b::{banach, second_countable_topology}) \ borel_measurable (count_space UNIV) \ ``` hoelzl@59000 ` 262` ``` (\x. f x \measure_pmf M) = (\x. f x \restrict_space M M)" ``` hoelzl@59000 ` 263` ``` by (auto intro!: integral_cong_AE simp add: integral_restrict_space AE_measure_pmf_iff) ``` hoelzl@59000 ` 264` hoelzl@58587 ` 265` ```lemma emeasure_pmf: "emeasure (M::'a pmf) M = 1" ``` hoelzl@58587 ` 266` ```proof - ``` hoelzl@58587 ` 267` ``` have "emeasure (M::'a pmf) M = emeasure (M::'a pmf) (space M)" ``` hoelzl@58587 ` 268` ``` by (intro emeasure_eq_AE) (simp_all add: AE_measure_pmf) ``` hoelzl@58587 ` 269` ``` then show ?thesis ``` hoelzl@58587 ` 270` ``` using measure_pmf.emeasure_space_1 by simp ``` hoelzl@58587 ` 271` ```qed ``` hoelzl@58587 ` 272` Andreas@59490 ` 273` ```lemma emeasure_pmf_UNIV [simp]: "emeasure (measure_pmf M) UNIV = 1" ``` Andreas@59490 ` 274` ```using measure_pmf.emeasure_space_1[of M] by simp ``` Andreas@59490 ` 275` Andreas@59023 ` 276` ```lemma in_null_sets_measure_pmfI: ``` Andreas@59023 ` 277` ``` "A \ set_pmf p = {} \ A \ null_sets (measure_pmf p)" ``` Andreas@59023 ` 278` ```using emeasure_eq_0_AE[where ?P="\x. x \ A" and M="measure_pmf p"] ``` Andreas@59023 ` 279` ```by(auto simp add: null_sets_def AE_measure_pmf_iff) ``` Andreas@59023 ` 280` hoelzl@59664 ` 281` ```lemma measure_subprob: "measure_pmf M \ space (subprob_algebra (count_space UNIV))" ``` hoelzl@59664 ` 282` ``` by (simp add: space_subprob_algebra subprob_space_measure_pmf) ``` hoelzl@59664 ` 283` hoelzl@59664 ` 284` ```subsection \ Monad Interpretation \ ``` hoelzl@59664 ` 285` hoelzl@59664 ` 286` ```lemma measurable_measure_pmf[measurable]: ``` hoelzl@59664 ` 287` ``` "(\x. measure_pmf (M x)) \ measurable (count_space UNIV) (subprob_algebra (count_space UNIV))" ``` hoelzl@59664 ` 288` ``` by (auto simp: space_subprob_algebra intro!: prob_space_imp_subprob_space) unfold_locales ``` hoelzl@59664 ` 289` hoelzl@59664 ` 290` ```lemma bind_measure_pmf_cong: ``` hoelzl@59664 ` 291` ``` assumes "\x. A x \ space (subprob_algebra N)" "\x. B x \ space (subprob_algebra N)" ``` hoelzl@59664 ` 292` ``` assumes "\i. i \ set_pmf x \ A i = B i" ``` hoelzl@59664 ` 293` ``` shows "bind (measure_pmf x) A = bind (measure_pmf x) B" ``` hoelzl@59664 ` 294` ```proof (rule measure_eqI) ``` wenzelm@62026 ` 295` ``` show "sets (measure_pmf x \ A) = sets (measure_pmf x \ B)" ``` hoelzl@59664 ` 296` ``` using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra) ``` hoelzl@59664 ` 297` ```next ``` wenzelm@62026 ` 298` ``` fix X assume "X \ sets (measure_pmf x \ A)" ``` hoelzl@59664 ` 299` ``` then have X: "X \ sets N" ``` hoelzl@59664 ` 300` ``` using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra) ``` wenzelm@62026 ` 301` ``` show "emeasure (measure_pmf x \ A) X = emeasure (measure_pmf x \ B) X" ``` hoelzl@59664 ` 302` ``` using assms ``` hoelzl@59664 ` 303` ``` by (subst (1 2) emeasure_bind[where N=N, OF _ _ X]) ``` hoelzl@59664 ` 304` ``` (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff) ``` hoelzl@59664 ` 305` ```qed ``` hoelzl@59664 ` 306` hoelzl@59664 ` 307` ```lift_definition bind_pmf :: "'a pmf \ ('a \ 'b pmf ) \ 'b pmf" is bind ``` hoelzl@59664 ` 308` ```proof (clarify, intro conjI) ``` hoelzl@59664 ` 309` ``` fix f :: "'a measure" and g :: "'a \ 'b measure" ``` hoelzl@59664 ` 310` ``` assume "prob_space f" ``` hoelzl@59664 ` 311` ``` then interpret f: prob_space f . ``` hoelzl@59664 ` 312` ``` assume "sets f = UNIV" and ae_f: "AE x in f. measure f {x} \ 0" ``` hoelzl@59664 ` 313` ``` then have s_f[simp]: "sets f = sets (count_space UNIV)" ``` hoelzl@59664 ` 314` ``` by simp ``` hoelzl@59664 ` 315` ``` assume g: "\x. prob_space (g x) \ sets (g x) = UNIV \ (AE y in g x. measure (g x) {y} \ 0)" ``` hoelzl@59664 ` 316` ``` then have g: "\x. prob_space (g x)" and s_g[simp]: "\x. sets (g x) = sets (count_space UNIV)" ``` hoelzl@59664 ` 317` ``` and ae_g: "\x. AE y in g x. measure (g x) {y} \ 0" ``` hoelzl@59664 ` 318` ``` by auto ``` hoelzl@59664 ` 319` hoelzl@59664 ` 320` ``` have [measurable]: "g \ measurable f (subprob_algebra (count_space UNIV))" ``` hoelzl@59664 ` 321` ``` by (auto simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space g) ``` lp15@59667 ` 322` wenzelm@62026 ` 323` ``` show "prob_space (f \ g)" ``` hoelzl@59664 ` 324` ``` using g by (intro f.prob_space_bind[where S="count_space UNIV"]) auto ``` wenzelm@62026 ` 325` ``` then interpret fg: prob_space "f \ g" . ``` wenzelm@62026 ` 326` ``` show [simp]: "sets (f \ g) = UNIV" ``` hoelzl@59664 ` 327` ``` using sets_eq_imp_space_eq[OF s_f] ``` hoelzl@59664 ` 328` ``` by (subst sets_bind[where N="count_space UNIV"]) auto ``` wenzelm@62026 ` 329` ``` show "AE x in f \ g. measure (f \ g) {x} \ 0" ``` hoelzl@59664 ` 330` ``` apply (simp add: fg.prob_eq_0 AE_bind[where B="count_space UNIV"]) ``` hoelzl@59664 ` 331` ``` using ae_f ``` hoelzl@59664 ` 332` ``` apply eventually_elim ``` hoelzl@59664 ` 333` ``` using ae_g ``` hoelzl@59664 ` 334` ``` apply eventually_elim ``` hoelzl@59664 ` 335` ``` apply (auto dest: AE_measure_singleton) ``` hoelzl@59664 ` 336` ``` done ``` hoelzl@59664 ` 337` ```qed ``` hoelzl@59664 ` 338` hoelzl@59664 ` 339` ```lemma ereal_pmf_bind: "pmf (bind_pmf N f) i = (\\<^sup>+x. pmf (f x) i \measure_pmf N)" ``` hoelzl@59664 ` 340` ``` unfolding pmf.rep_eq bind_pmf.rep_eq ``` hoelzl@59664 ` 341` ``` by (auto simp: measure_pmf.measure_bind[where N="count_space UNIV"] measure_subprob measure_nonneg ``` hoelzl@59664 ` 342` ``` intro!: nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1]) ``` hoelzl@59664 ` 343` hoelzl@59664 ` 344` ```lemma pmf_bind: "pmf (bind_pmf N f) i = (\x. pmf (f x) i \measure_pmf N)" ``` hoelzl@59664 ` 345` ``` using ereal_pmf_bind[of N f i] ``` hoelzl@59664 ` 346` ``` by (subst (asm) nn_integral_eq_integral) ``` hoelzl@59664 ` 347` ``` (auto simp: pmf_nonneg pmf_le_1 ``` hoelzl@59664 ` 348` ``` intro!: nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1]) ``` hoelzl@59664 ` 349` hoelzl@59664 ` 350` ```lemma bind_pmf_const[simp]: "bind_pmf M (\x. c) = c" ``` hoelzl@59664 ` 351` ``` by transfer (simp add: bind_const' prob_space_imp_subprob_space) ``` hoelzl@59664 ` 352` hoelzl@59665 ` 353` ```lemma set_bind_pmf[simp]: "set_pmf (bind_pmf M N) = (\M\set_pmf M. set_pmf (N M))" ``` lp15@59667 ` 354` ``` unfolding set_pmf_eq ereal_eq_0(1)[symmetric] ereal_pmf_bind ``` hoelzl@59664 ` 355` ``` by (auto simp add: nn_integral_0_iff_AE AE_measure_pmf_iff set_pmf_eq not_le less_le pmf_nonneg) ``` hoelzl@59664 ` 356` hoelzl@59664 ` 357` ```lemma bind_pmf_cong: ``` hoelzl@59664 ` 358` ``` assumes "p = q" ``` hoelzl@59664 ` 359` ``` shows "(\x. x \ set_pmf q \ f x = g x) \ bind_pmf p f = bind_pmf q g" ``` wenzelm@61808 ` 360` ``` unfolding \p = q\[symmetric] measure_pmf_inject[symmetric] bind_pmf.rep_eq ``` hoelzl@59664 ` 361` ``` by (auto simp: AE_measure_pmf_iff Pi_iff space_subprob_algebra subprob_space_measure_pmf ``` hoelzl@59664 ` 362` ``` sets_bind[where N="count_space UNIV"] emeasure_bind[where N="count_space UNIV"] ``` hoelzl@59664 ` 363` ``` intro!: nn_integral_cong_AE measure_eqI) ``` hoelzl@59664 ` 364` hoelzl@59664 ` 365` ```lemma bind_pmf_cong_simp: ``` hoelzl@59664 ` 366` ``` "p = q \ (\x. x \ set_pmf q =simp=> f x = g x) \ bind_pmf p f = bind_pmf q g" ``` hoelzl@59664 ` 367` ``` by (simp add: simp_implies_def cong: bind_pmf_cong) ``` hoelzl@59664 ` 368` wenzelm@62026 ` 369` ```lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \ (\x. measure_pmf (f x)))" ``` hoelzl@59664 ` 370` ``` by transfer simp ``` hoelzl@59664 ` 371` hoelzl@59664 ` 372` ```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 ` 373` ``` using measurable_measure_pmf[of N] ``` hoelzl@59664 ` 374` ``` unfolding measure_pmf_bind ``` hoelzl@59664 ` 375` ``` apply (subst (1 3) nn_integral_max_0[symmetric]) ``` hoelzl@59664 ` 376` ``` apply (intro nn_integral_bind[where B="count_space UNIV"]) ``` hoelzl@59664 ` 377` ``` apply auto ``` hoelzl@59664 ` 378` ``` done ``` hoelzl@59664 ` 379` hoelzl@59664 ` 380` ```lemma emeasure_bind_pmf[simp]: "emeasure (bind_pmf M N) X = (\\<^sup>+x. emeasure (N x) X \M)" ``` hoelzl@59664 ` 381` ``` using measurable_measure_pmf[of N] ``` hoelzl@59664 ` 382` ``` unfolding measure_pmf_bind ``` hoelzl@59664 ` 383` ``` by (subst emeasure_bind[where N="count_space UNIV"]) auto ``` lp15@59667 ` 384` hoelzl@59664 ` 385` ```lift_definition return_pmf :: "'a \ 'a pmf" is "return (count_space UNIV)" ``` hoelzl@59664 ` 386` ``` by (auto intro!: prob_space_return simp: AE_return measure_return) ``` hoelzl@59664 ` 387` hoelzl@59664 ` 388` ```lemma bind_return_pmf: "bind_pmf (return_pmf x) f = f x" ``` hoelzl@59664 ` 389` ``` by transfer ``` hoelzl@59664 ` 390` ``` (auto intro!: prob_space_imp_subprob_space bind_return[where N="count_space UNIV"] ``` hoelzl@59664 ` 391` ``` simp: space_subprob_algebra) ``` hoelzl@59664 ` 392` hoelzl@59665 ` 393` ```lemma set_return_pmf[simp]: "set_pmf (return_pmf x) = {x}" ``` hoelzl@59664 ` 394` ``` by transfer (auto simp add: measure_return split: split_indicator) ``` hoelzl@59664 ` 395` hoelzl@59664 ` 396` ```lemma bind_return_pmf': "bind_pmf N return_pmf = N" ``` hoelzl@59664 ` 397` ```proof (transfer, clarify) ``` wenzelm@62026 ` 398` ``` fix N :: "'a measure" assume "sets N = UNIV" then show "N \ return (count_space UNIV) = N" ``` hoelzl@59664 ` 399` ``` by (subst return_sets_cong[where N=N]) (simp_all add: bind_return') ``` hoelzl@59664 ` 400` ```qed ``` hoelzl@59664 ` 401` hoelzl@59664 ` 402` ```lemma bind_assoc_pmf: "bind_pmf (bind_pmf A B) C = bind_pmf A (\x. bind_pmf (B x) C)" ``` hoelzl@59664 ` 403` ``` by transfer ``` hoelzl@59664 ` 404` ``` (auto intro!: bind_assoc[where N="count_space UNIV" and R="count_space UNIV"] ``` hoelzl@59664 ` 405` ``` simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space) ``` hoelzl@59664 ` 406` hoelzl@59664 ` 407` ```definition "map_pmf f M = bind_pmf M (\x. return_pmf (f x))" ``` hoelzl@59664 ` 408` hoelzl@59664 ` 409` ```lemma map_bind_pmf: "map_pmf f (bind_pmf M g) = bind_pmf M (\x. map_pmf f (g x))" ``` hoelzl@59664 ` 410` ``` by (simp add: map_pmf_def bind_assoc_pmf) ``` hoelzl@59664 ` 411` hoelzl@59664 ` 412` ```lemma bind_map_pmf: "bind_pmf (map_pmf f M) g = bind_pmf M (\x. g (f x))" ``` hoelzl@59664 ` 413` ``` by (simp add: map_pmf_def bind_assoc_pmf bind_return_pmf) ``` hoelzl@59664 ` 414` hoelzl@59664 ` 415` ```lemma map_pmf_transfer[transfer_rule]: ``` hoelzl@59664 ` 416` ``` "rel_fun op = (rel_fun cr_pmf cr_pmf) (\f M. distr M (count_space UNIV) f) map_pmf" ``` hoelzl@59664 ` 417` ```proof - ``` hoelzl@59664 ` 418` ``` have "rel_fun op = (rel_fun pmf_as_measure.cr_pmf pmf_as_measure.cr_pmf) ``` wenzelm@62026 ` 419` ``` (\f M. M \ (return (count_space UNIV) o f)) map_pmf" ``` lp15@59667 ` 420` ``` unfolding map_pmf_def[abs_def] comp_def by transfer_prover ``` hoelzl@59664 ` 421` ``` then show ?thesis ``` hoelzl@59664 ` 422` ``` by (force simp: rel_fun_def cr_pmf_def bind_return_distr) ``` hoelzl@59664 ` 423` ```qed ``` hoelzl@59664 ` 424` hoelzl@59664 ` 425` ```lemma map_pmf_rep_eq: ``` hoelzl@59664 ` 426` ``` "measure_pmf (map_pmf f M) = distr (measure_pmf M) (count_space UNIV) f" ``` hoelzl@59664 ` 427` ``` unfolding map_pmf_def bind_pmf.rep_eq comp_def return_pmf.rep_eq ``` hoelzl@59664 ` 428` ``` using bind_return_distr[of M f "count_space UNIV"] by (simp add: comp_def) ``` hoelzl@59664 ` 429` hoelzl@58587 ` 430` ```lemma map_pmf_id[simp]: "map_pmf id = id" ``` hoelzl@58587 ` 431` ``` by (rule, transfer) (auto simp: emeasure_distr measurable_def intro!: measure_eqI) ``` hoelzl@58587 ` 432` hoelzl@59053 ` 433` ```lemma map_pmf_ident[simp]: "map_pmf (\x. x) = (\x. x)" ``` hoelzl@59053 ` 434` ``` using map_pmf_id unfolding id_def . ``` hoelzl@59053 ` 435` hoelzl@58587 ` 436` ```lemma map_pmf_compose: "map_pmf (f \ g) = map_pmf f \ map_pmf g" ``` lp15@59667 ` 437` ``` by (rule, transfer) (simp add: distr_distr[symmetric, where N="count_space UNIV"] measurable_def) ``` hoelzl@58587 ` 438` hoelzl@59000 ` 439` ```lemma map_pmf_comp: "map_pmf f (map_pmf g M) = map_pmf (\x. f (g x)) M" ``` hoelzl@59000 ` 440` ``` using map_pmf_compose[of f g] by (simp add: comp_def) ``` hoelzl@59000 ` 441` hoelzl@59664 ` 442` ```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 ` 443` ``` unfolding map_pmf_def by (rule bind_pmf_cong) auto ``` hoelzl@59664 ` 444` hoelzl@59664 ` 445` ```lemma pmf_set_map: "set_pmf \ map_pmf f = op ` f \ set_pmf" ``` hoelzl@59665 ` 446` ``` by (auto simp add: comp_def fun_eq_iff map_pmf_def) ``` hoelzl@59664 ` 447` hoelzl@59665 ` 448` ```lemma set_map_pmf[simp]: "set_pmf (map_pmf f M) = f`set_pmf M" ``` hoelzl@59664 ` 449` ``` using pmf_set_map[of f] by (auto simp: comp_def fun_eq_iff) ``` hoelzl@58587 ` 450` hoelzl@59002 ` 451` ```lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f -` X)" ``` hoelzl@59664 ` 452` ``` unfolding map_pmf_rep_eq by (subst emeasure_distr) auto ``` hoelzl@59002 ` 453` Andreas@61634 ` 454` ```lemma measure_map_pmf[simp]: "measure (map_pmf f M) X = measure M (f -` X)" ``` Andreas@61634 ` 455` ```using emeasure_map_pmf[of f M X] by(simp add: measure_pmf.emeasure_eq_measure) ``` Andreas@61634 ` 456` hoelzl@59002 ` 457` ```lemma nn_integral_map_pmf[simp]: "(\\<^sup>+x. f x \map_pmf g M) = (\\<^sup>+x. f (g x) \M)" ``` hoelzl@59664 ` 458` ``` unfolding map_pmf_rep_eq by (intro nn_integral_distr) auto ``` hoelzl@59002 ` 459` Andreas@59023 ` 460` ```lemma ereal_pmf_map: "pmf (map_pmf f p) x = (\\<^sup>+ y. indicator (f -` {x}) y \measure_pmf p)" ``` hoelzl@59664 ` 461` ```proof (transfer fixing: f x) ``` Andreas@59023 ` 462` ``` fix p :: "'b measure" ``` Andreas@59023 ` 463` ``` presume "prob_space p" ``` Andreas@59023 ` 464` ``` then interpret prob_space p . ``` Andreas@59023 ` 465` ``` presume "sets p = UNIV" ``` Andreas@59023 ` 466` ``` then show "ereal (measure (distr p (count_space UNIV) f) {x}) = integral\<^sup>N p (indicator (f -` {x}))" ``` Andreas@59023 ` 467` ``` by(simp add: measure_distr measurable_def emeasure_eq_measure) ``` Andreas@59023 ` 468` ```qed simp_all ``` Andreas@59023 ` 469` Andreas@59023 ` 470` ```lemma nn_integral_pmf: "(\\<^sup>+ x. pmf p x \count_space A) = emeasure (measure_pmf p) A" ``` Andreas@59023 ` 471` ```proof - ``` Andreas@59023 ` 472` ``` have "(\\<^sup>+ x. pmf p x \count_space A) = (\\<^sup>+ x. pmf p x \count_space (A \ set_pmf p))" ``` Andreas@59023 ` 473` ``` by(auto simp add: nn_integral_count_space_indicator indicator_def set_pmf_iff intro: nn_integral_cong) ``` Andreas@59023 ` 474` ``` also have "\ = emeasure (measure_pmf p) (\x\A \ set_pmf p. {x})" ``` Andreas@59023 ` 475` ``` by(subst emeasure_UN_countable)(auto simp add: emeasure_pmf_single disjoint_family_on_def) ``` Andreas@59023 ` 476` ``` also have "\ = emeasure (measure_pmf p) ((\x\A \ set_pmf p. {x}) \ {x. x \ A \ x \ set_pmf p})" ``` Andreas@59023 ` 477` ``` by(rule emeasure_Un_null_set[symmetric])(auto intro: in_null_sets_measure_pmfI) ``` Andreas@59023 ` 478` ``` also have "\ = emeasure (measure_pmf p) A" ``` Andreas@59023 ` 479` ``` by(auto intro: arg_cong2[where f=emeasure]) ``` Andreas@59023 ` 480` ``` finally show ?thesis . ``` Andreas@59023 ` 481` ```qed ``` Andreas@59023 ` 482` Andreas@60068 ` 483` ```lemma map_return_pmf [simp]: "map_pmf f (return_pmf x) = return_pmf (f x)" ``` hoelzl@59664 ` 484` ``` by transfer (simp add: distr_return) ``` hoelzl@59664 ` 485` hoelzl@59664 ` 486` ```lemma map_pmf_const[simp]: "map_pmf (\_. c) M = return_pmf c" ``` hoelzl@59664 ` 487` ``` by transfer (auto simp: prob_space.distr_const) ``` hoelzl@59664 ` 488` Andreas@60068 ` 489` ```lemma pmf_return [simp]: "pmf (return_pmf x) y = indicator {y} x" ``` hoelzl@59664 ` 490` ``` by transfer (simp add: measure_return) ``` hoelzl@59664 ` 491` hoelzl@59664 ` 492` ```lemma nn_integral_return_pmf[simp]: "0 \ f x \ (\\<^sup>+x. f x \return_pmf x) = f x" ``` hoelzl@59664 ` 493` ``` unfolding return_pmf.rep_eq by (intro nn_integral_return) auto ``` hoelzl@59664 ` 494` hoelzl@59664 ` 495` ```lemma emeasure_return_pmf[simp]: "emeasure (return_pmf x) X = indicator X x" ``` hoelzl@59664 ` 496` ``` unfolding return_pmf.rep_eq by (intro emeasure_return) auto ``` hoelzl@59664 ` 497` hoelzl@59664 ` 498` ```lemma return_pmf_inj[simp]: "return_pmf x = return_pmf y \ x = y" ``` hoelzl@59664 ` 499` ``` by (metis insertI1 set_return_pmf singletonD) ``` hoelzl@59664 ` 500` hoelzl@59665 ` 501` ```lemma map_pmf_eq_return_pmf_iff: ``` hoelzl@59665 ` 502` ``` "map_pmf f p = return_pmf x \ (\y \ set_pmf p. f y = x)" ``` hoelzl@59665 ` 503` ```proof ``` hoelzl@59665 ` 504` ``` assume "map_pmf f p = return_pmf x" ``` hoelzl@59665 ` 505` ``` then have "set_pmf (map_pmf f p) = set_pmf (return_pmf x)" by simp ``` hoelzl@59665 ` 506` ``` then show "\y \ set_pmf p. f y = x" by auto ``` hoelzl@59665 ` 507` ```next ``` hoelzl@59665 ` 508` ``` assume "\y \ set_pmf p. f y = x" ``` hoelzl@59665 ` 509` ``` then show "map_pmf f p = return_pmf x" ``` hoelzl@59665 ` 510` ``` unfolding map_pmf_const[symmetric, of _ p] by (intro map_pmf_cong) auto ``` hoelzl@59665 ` 511` ```qed ``` hoelzl@59665 ` 512` hoelzl@59664 ` 513` ```definition "pair_pmf A B = bind_pmf A (\x. bind_pmf B (\y. return_pmf (x, y)))" ``` hoelzl@59664 ` 514` hoelzl@59664 ` 515` ```lemma pmf_pair: "pmf (pair_pmf M N) (a, b) = pmf M a * pmf N b" ``` hoelzl@59664 ` 516` ``` unfolding pair_pmf_def pmf_bind pmf_return ``` hoelzl@59664 ` 517` ``` apply (subst integral_measure_pmf[where A="{b}"]) ``` hoelzl@59664 ` 518` ``` apply (auto simp: indicator_eq_0_iff) ``` hoelzl@59664 ` 519` ``` apply (subst integral_measure_pmf[where A="{a}"]) ``` hoelzl@59664 ` 520` ``` apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg) ``` hoelzl@59664 ` 521` ``` done ``` hoelzl@59664 ` 522` hoelzl@59665 ` 523` ```lemma set_pair_pmf[simp]: "set_pmf (pair_pmf A B) = set_pmf A \ set_pmf B" ``` hoelzl@59664 ` 524` ``` unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto ``` hoelzl@59664 ` 525` hoelzl@59664 ` 526` ```lemma measure_pmf_in_subprob_space[measurable (raw)]: ``` hoelzl@59664 ` 527` ``` "measure_pmf M \ space (subprob_algebra (count_space UNIV))" ``` hoelzl@59664 ` 528` ``` by (simp add: space_subprob_algebra) intro_locales ``` hoelzl@59664 ` 529` hoelzl@59664 ` 530` ```lemma nn_integral_pair_pmf': "(\\<^sup>+x. f x \pair_pmf A B) = (\\<^sup>+a. \\<^sup>+b. f (a, b) \B \A)" ``` hoelzl@59664 ` 531` ```proof - ``` hoelzl@59664 ` 532` ``` have "(\\<^sup>+x. f x \pair_pmf A B) = (\\<^sup>+x. max 0 (f x) * indicator (A \ B) x \pair_pmf A B)" ``` hoelzl@59664 ` 533` ``` by (subst nn_integral_max_0[symmetric]) ``` hoelzl@59665 ` 534` ``` (auto simp: AE_measure_pmf_iff intro!: nn_integral_cong_AE) ``` hoelzl@59664 ` 535` ``` also have "\ = (\\<^sup>+a. \\<^sup>+b. max 0 (f (a, b)) * indicator (A \ B) (a, b) \B \A)" ``` hoelzl@59664 ` 536` ``` by (simp add: pair_pmf_def) ``` hoelzl@59664 ` 537` ``` also have "\ = (\\<^sup>+a. \\<^sup>+b. max 0 (f (a, b)) \B \A)" ``` hoelzl@59664 ` 538` ``` by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff) ``` hoelzl@59664 ` 539` ``` finally show ?thesis ``` hoelzl@59664 ` 540` ``` unfolding nn_integral_max_0 . ``` hoelzl@59664 ` 541` ```qed ``` hoelzl@59664 ` 542` hoelzl@59664 ` 543` ```lemma bind_pair_pmf: ``` hoelzl@59664 ` 544` ``` assumes M[measurable]: "M \ measurable (count_space UNIV \\<^sub>M count_space UNIV) (subprob_algebra N)" ``` wenzelm@62026 ` 545` ``` shows "measure_pmf (pair_pmf A B) \ M = (measure_pmf A \ (\x. measure_pmf B \ (\y. M (x, y))))" ``` hoelzl@59664 ` 546` ``` (is "?L = ?R") ``` hoelzl@59664 ` 547` ```proof (rule measure_eqI) ``` hoelzl@59664 ` 548` ``` have M'[measurable]: "M \ measurable (pair_pmf A B) (subprob_algebra N)" ``` hoelzl@59664 ` 549` ``` using M[THEN measurable_space] by (simp_all add: space_pair_measure) ``` hoelzl@59664 ` 550` hoelzl@59664 ` 551` ``` note measurable_bind[where N="count_space UNIV", measurable] ``` hoelzl@59664 ` 552` ``` note measure_pmf_in_subprob_space[simp] ``` hoelzl@59664 ` 553` hoelzl@59664 ` 554` ``` have sets_eq_N: "sets ?L = N" ``` hoelzl@59664 ` 555` ``` by (subst sets_bind[OF sets_kernel[OF M']]) auto ``` hoelzl@59664 ` 556` ``` show "sets ?L = sets ?R" ``` hoelzl@59664 ` 557` ``` using measurable_space[OF M] ``` hoelzl@59664 ` 558` ``` by (simp add: sets_eq_N space_pair_measure space_subprob_algebra) ``` hoelzl@59664 ` 559` ``` fix X assume "X \ sets ?L" ``` hoelzl@59664 ` 560` ``` then have X[measurable]: "X \ sets N" ``` hoelzl@59664 ` 561` ``` unfolding sets_eq_N . ``` hoelzl@59664 ` 562` ``` then show "emeasure ?L X = emeasure ?R X" ``` hoelzl@59664 ` 563` ``` apply (simp add: emeasure_bind[OF _ M' X]) ``` hoelzl@59664 ` 564` ``` apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A] ``` Andreas@60068 ` 565` ``` nn_integral_measure_pmf_finite emeasure_nonneg one_ereal_def[symmetric]) ``` hoelzl@59664 ` 566` ``` apply (subst emeasure_bind[OF _ _ X]) ``` hoelzl@59664 ` 567` ``` apply measurable ``` hoelzl@59664 ` 568` ``` apply (subst emeasure_bind[OF _ _ X]) ``` hoelzl@59664 ` 569` ``` apply measurable ``` hoelzl@59664 ` 570` ``` done ``` hoelzl@59664 ` 571` ```qed ``` hoelzl@59664 ` 572` hoelzl@59664 ` 573` ```lemma map_fst_pair_pmf: "map_pmf fst (pair_pmf A B) = A" ``` hoelzl@59664 ` 574` ``` by (simp add: pair_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') ``` hoelzl@59664 ` 575` hoelzl@59664 ` 576` ```lemma map_snd_pair_pmf: "map_pmf snd (pair_pmf A B) = B" ``` hoelzl@59664 ` 577` ``` by (simp add: pair_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') ``` hoelzl@59664 ` 578` hoelzl@59664 ` 579` ```lemma nn_integral_pmf': ``` hoelzl@59664 ` 580` ``` "inj_on f A \ (\\<^sup>+x. pmf p (f x) \count_space A) = emeasure p (f ` A)" ``` hoelzl@59664 ` 581` ``` by (subst nn_integral_bij_count_space[where g=f and B="f`A"]) ``` hoelzl@59664 ` 582` ``` (auto simp: bij_betw_def nn_integral_pmf) ``` hoelzl@59664 ` 583` hoelzl@59664 ` 584` ```lemma pmf_le_0_iff[simp]: "pmf M p \ 0 \ pmf M p = 0" ``` hoelzl@59664 ` 585` ``` using pmf_nonneg[of M p] by simp ``` hoelzl@59664 ` 586` hoelzl@59664 ` 587` ```lemma min_pmf_0[simp]: "min (pmf M p) 0 = 0" "min 0 (pmf M p) = 0" ``` hoelzl@59664 ` 588` ``` using pmf_nonneg[of M p] by simp_all ``` hoelzl@59664 ` 589` hoelzl@59664 ` 590` ```lemma pmf_eq_0_set_pmf: "pmf M p = 0 \ p \ set_pmf M" ``` hoelzl@59664 ` 591` ``` unfolding set_pmf_iff by simp ``` hoelzl@59664 ` 592` hoelzl@59664 ` 593` ```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 ` 594` ``` by (auto simp: pmf.rep_eq map_pmf_rep_eq measure_distr AE_measure_pmf_iff inj_onD ``` hoelzl@59664 ` 595` ``` intro!: measure_pmf.finite_measure_eq_AE) ``` hoelzl@59664 ` 596` Andreas@60068 ` 597` ```lemma pmf_map_inj': "inj f \ pmf (map_pmf f M) (f x) = pmf M x" ``` Andreas@60068 ` 598` ```apply(cases "x \ set_pmf M") ``` Andreas@60068 ` 599` ``` apply(simp add: pmf_map_inj[OF subset_inj_on]) ``` Andreas@60068 ` 600` ```apply(simp add: pmf_eq_0_set_pmf[symmetric]) ``` Andreas@60068 ` 601` ```apply(auto simp add: pmf_eq_0_set_pmf dest: injD) ``` Andreas@60068 ` 602` ```done ``` Andreas@60068 ` 603` Andreas@60068 ` 604` ```lemma pmf_map_outside: "x \ f ` set_pmf M \ pmf (map_pmf f M) x = 0" ``` Andreas@60068 ` 605` ```unfolding pmf_eq_0_set_pmf by simp ``` Andreas@60068 ` 606` hoelzl@59664 ` 607` ```subsection \ PMFs as function \ ``` hoelzl@59000 ` 608` hoelzl@58587 ` 609` ```context ``` hoelzl@58587 ` 610` ``` fixes f :: "'a \ real" ``` hoelzl@58587 ` 611` ``` assumes nonneg: "\x. 0 \ f x" ``` hoelzl@58587 ` 612` ``` assumes prob: "(\\<^sup>+x. f x \count_space UNIV) = 1" ``` hoelzl@58587 ` 613` ```begin ``` hoelzl@58587 ` 614` hoelzl@58587 ` 615` ```lift_definition embed_pmf :: "'a pmf" is "density (count_space UNIV) (ereal \ f)" ``` hoelzl@58587 ` 616` ```proof (intro conjI) ``` hoelzl@58587 ` 617` ``` have *[simp]: "\x y. ereal (f y) * indicator {x} y = ereal (f x) * indicator {x} y" ``` hoelzl@58587 ` 618` ``` by (simp split: split_indicator) ``` hoelzl@58587 ` 619` ``` show "AE x in density (count_space UNIV) (ereal \ f). ``` hoelzl@58587 ` 620` ``` measure (density (count_space UNIV) (ereal \ f)) {x} \ 0" ``` hoelzl@59092 ` 621` ``` by (simp add: AE_density nonneg measure_def emeasure_density max_def) ``` hoelzl@58587 ` 622` ``` show "prob_space (density (count_space UNIV) (ereal \ f))" ``` wenzelm@61169 ` 623` ``` by standard (simp add: emeasure_density prob) ``` hoelzl@58587 ` 624` ```qed simp ``` hoelzl@58587 ` 625` hoelzl@58587 ` 626` ```lemma pmf_embed_pmf: "pmf embed_pmf x = f x" ``` hoelzl@58587 ` 627` ```proof transfer ``` hoelzl@58587 ` 628` ``` have *[simp]: "\x y. ereal (f y) * indicator {x} y = ereal (f x) * indicator {x} y" ``` hoelzl@58587 ` 629` ``` by (simp split: split_indicator) ``` hoelzl@58587 ` 630` ``` fix x show "measure (density (count_space UNIV) (ereal \ f)) {x} = f x" ``` hoelzl@59092 ` 631` ``` by transfer (simp add: measure_def emeasure_density nonneg max_def) ``` hoelzl@58587 ` 632` ```qed ``` hoelzl@58587 ` 633` Andreas@60068 ` 634` ```lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \ 0}" ``` Andreas@60068 ` 635` ```by(auto simp add: set_pmf_eq assms pmf_embed_pmf) ``` Andreas@60068 ` 636` hoelzl@58587 ` 637` ```end ``` hoelzl@58587 ` 638` hoelzl@58587 ` 639` ```lemma embed_pmf_transfer: ``` hoelzl@58730 ` 640` ``` "rel_fun (eq_onp (\f. (\x. 0 \ f x) \ (\\<^sup>+x. ereal (f x) \count_space UNIV) = 1)) pmf_as_measure.cr_pmf (\f. density (count_space UNIV) (ereal \ f)) embed_pmf" ``` hoelzl@58587 ` 641` ``` by (auto simp: rel_fun_def eq_onp_def embed_pmf.transfer) ``` hoelzl@58587 ` 642` hoelzl@59000 ` 643` ```lemma measure_pmf_eq_density: "measure_pmf p = density (count_space UNIV) (pmf p)" ``` hoelzl@59000 ` 644` ```proof (transfer, elim conjE) ``` hoelzl@59000 ` 645` ``` fix M :: "'a measure" assume [simp]: "sets M = UNIV" and ae: "AE x in M. measure M {x} \ 0" ``` hoelzl@59000 ` 646` ``` assume "prob_space M" then interpret prob_space M . ``` hoelzl@59000 ` 647` ``` show "M = density (count_space UNIV) (\x. ereal (measure M {x}))" ``` hoelzl@59000 ` 648` ``` proof (rule measure_eqI) ``` hoelzl@59000 ` 649` ``` fix A :: "'a set" ``` lp15@59667 ` 650` ``` have "(\\<^sup>+ x. ereal (measure M {x}) * indicator A x \count_space UNIV) = ``` hoelzl@59000 ` 651` ``` (\\<^sup>+ x. emeasure M {x} * indicator (A \ {x. measure M {x} \ 0}) x \count_space UNIV)" ``` hoelzl@59000 ` 652` ``` by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator) ``` hoelzl@59000 ` 653` ``` also have "\ = (\\<^sup>+ x. emeasure M {x} \count_space (A \ {x. measure M {x} \ 0}))" ``` hoelzl@59000 ` 654` ``` by (subst nn_integral_restrict_space[symmetric]) (auto simp: restrict_count_space) ``` hoelzl@59000 ` 655` ``` also have "\ = emeasure M (\x\(A \ {x. measure M {x} \ 0}). {x})" ``` hoelzl@59000 ` 656` ``` by (intro emeasure_UN_countable[symmetric] countable_Int2 countable_support) ``` hoelzl@59000 ` 657` ``` (auto simp: disjoint_family_on_def) ``` hoelzl@59000 ` 658` ``` also have "\ = emeasure M A" ``` hoelzl@59000 ` 659` ``` using ae by (intro emeasure_eq_AE) auto ``` hoelzl@59000 ` 660` ``` finally show " emeasure M A = emeasure (density (count_space UNIV) (\x. ereal (measure M {x}))) A" ``` hoelzl@59000 ` 661` ``` using emeasure_space_1 by (simp add: emeasure_density) ``` hoelzl@59000 ` 662` ``` qed simp ``` hoelzl@59000 ` 663` ```qed ``` hoelzl@59000 ` 664` hoelzl@58587 ` 665` ```lemma td_pmf_embed_pmf: ``` hoelzl@58587 ` 666` ``` "type_definition pmf embed_pmf {f::'a \ real. (\x. 0 \ f x) \ (\\<^sup>+x. ereal (f x) \count_space UNIV) = 1}" ``` hoelzl@58587 ` 667` ``` unfolding type_definition_def ``` hoelzl@58587 ` 668` ```proof safe ``` hoelzl@58587 ` 669` ``` fix p :: "'a pmf" ``` hoelzl@58587 ` 670` ``` have "(\\<^sup>+ x. 1 \measure_pmf p) = 1" ``` hoelzl@58587 ` 671` ``` using measure_pmf.emeasure_space_1[of p] by simp ``` hoelzl@58587 ` 672` ``` then show *: "(\\<^sup>+ x. ereal (pmf p x) \count_space UNIV) = 1" ``` hoelzl@58587 ` 673` ``` by (simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg del: nn_integral_const) ``` hoelzl@58587 ` 674` hoelzl@58587 ` 675` ``` show "embed_pmf (pmf p) = p" ``` hoelzl@58587 ` 676` ``` by (intro measure_pmf_inject[THEN iffD1]) ``` hoelzl@58587 ` 677` ``` (simp add: * embed_pmf.rep_eq pmf_nonneg measure_pmf_eq_density[of p] comp_def) ``` hoelzl@58587 ` 678` ```next ``` hoelzl@58587 ` 679` ``` fix f :: "'a \ real" assume "\x. 0 \ f x" "(\\<^sup>+x. f x \count_space UNIV) = 1" ``` hoelzl@58587 ` 680` ``` then show "pmf (embed_pmf f) = f" ``` hoelzl@58587 ` 681` ``` by (auto intro!: pmf_embed_pmf) ``` hoelzl@58587 ` 682` ```qed (rule pmf_nonneg) ``` hoelzl@58587 ` 683` hoelzl@58587 ` 684` ```end ``` hoelzl@58587 ` 685` Andreas@60068 ` 686` ```lemma nn_integral_measure_pmf: "(\\<^sup>+ x. f x \measure_pmf p) = \\<^sup>+ x. ereal (pmf p x) * f x \count_space UNIV" ``` Andreas@60068 ` 687` ```by(simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg) ``` Andreas@60068 ` 688` hoelzl@58587 ` 689` ```locale pmf_as_function ``` hoelzl@58587 ` 690` ```begin ``` hoelzl@58587 ` 691` hoelzl@58587 ` 692` ```setup_lifting td_pmf_embed_pmf ``` hoelzl@58587 ` 693` lp15@59667 ` 694` ```lemma set_pmf_transfer[transfer_rule]: ``` hoelzl@58730 ` 695` ``` assumes "bi_total A" ``` lp15@59667 ` 696` ``` shows "rel_fun (pcr_pmf A) (rel_set A) (\f. {x. f x \ 0}) set_pmf" ``` wenzelm@61808 ` 697` ``` using \bi_total A\ ``` hoelzl@58730 ` 698` ``` 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 ` 699` ``` metis+ ``` hoelzl@58730 ` 700` hoelzl@59000 ` 701` ```end ``` hoelzl@59000 ` 702` hoelzl@59000 ` 703` ```context ``` hoelzl@59000 ` 704` ```begin ``` hoelzl@59000 ` 705` hoelzl@59000 ` 706` ```interpretation pmf_as_function . ``` hoelzl@59000 ` 707` hoelzl@59000 ` 708` ```lemma pmf_eqI: "(\i. pmf M i = pmf N i) \ M = N" ``` hoelzl@59000 ` 709` ``` by transfer auto ``` hoelzl@59000 ` 710` hoelzl@59000 ` 711` ```lemma pmf_eq_iff: "M = N \ (\i. pmf M i = pmf N i)" ``` hoelzl@59000 ` 712` ``` by (auto intro: pmf_eqI) ``` hoelzl@59000 ` 713` hoelzl@59664 ` 714` ```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 ` 715` ``` unfolding pmf_eq_iff pmf_bind ``` hoelzl@59664 ` 716` ```proof ``` hoelzl@59664 ` 717` ``` fix i ``` hoelzl@59664 ` 718` ``` interpret B: prob_space "restrict_space B B" ``` hoelzl@59664 ` 719` ``` by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) ``` hoelzl@59664 ` 720` ``` (auto simp: AE_measure_pmf_iff) ``` hoelzl@59664 ` 721` ``` interpret A: prob_space "restrict_space A A" ``` hoelzl@59664 ` 722` ``` by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE) ``` hoelzl@59664 ` 723` ``` (auto simp: AE_measure_pmf_iff) ``` hoelzl@59664 ` 724` hoelzl@59664 ` 725` ``` interpret AB: pair_prob_space "restrict_space A A" "restrict_space B B" ``` hoelzl@59664 ` 726` ``` by unfold_locales ``` hoelzl@59664 ` 727` hoelzl@59664 ` 728` ``` have "(\ x. \ y. pmf (C x y) i \B \A) = (\ x. (\ y. pmf (C x y) i \restrict_space B B) \A)" ``` hoelzl@59664 ` 729` ``` by (rule integral_cong) (auto intro!: integral_pmf_restrict) ``` hoelzl@59664 ` 730` ``` also have "\ = (\ x. (\ y. pmf (C x y) i \restrict_space B B) \restrict_space A A)" ``` hoelzl@59664 ` 731` ``` by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2 ``` hoelzl@59664 ` 732` ``` countable_set_pmf borel_measurable_count_space) ``` hoelzl@59664 ` 733` ``` also have "\ = (\ y. \ x. pmf (C x y) i \restrict_space A A \restrict_space B B)" ``` hoelzl@59664 ` 734` ``` by (rule AB.Fubini_integral[symmetric]) ``` hoelzl@59664 ` 735` ``` (auto intro!: AB.integrable_const_bound[where B=1] measurable_pair_restrict_pmf2 ``` hoelzl@59664 ` 736` ``` simp: pmf_nonneg pmf_le_1 measurable_restrict_space1) ``` hoelzl@59664 ` 737` ``` also have "\ = (\ y. \ x. pmf (C x y) i \restrict_space A A \B)" ``` hoelzl@59664 ` 738` ``` by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2 ``` hoelzl@59664 ` 739` ``` countable_set_pmf borel_measurable_count_space) ``` hoelzl@59664 ` 740` ``` also have "\ = (\ y. \ x. pmf (C x y) i \A \B)" ``` hoelzl@59664 ` 741` ``` by (rule integral_cong) (auto intro!: integral_pmf_restrict[symmetric]) ``` hoelzl@59664 ` 742` ``` finally show "(\ x. \ y. pmf (C x y) i \B \A) = (\ y. \ x. pmf (C x y) i \A \B)" . ``` hoelzl@59664 ` 743` ```qed ``` hoelzl@59664 ` 744` hoelzl@59664 ` 745` ```lemma pair_map_pmf1: "pair_pmf (map_pmf f A) B = map_pmf (apfst f) (pair_pmf A B)" ``` hoelzl@59664 ` 746` ```proof (safe intro!: pmf_eqI) ``` hoelzl@59664 ` 747` ``` fix a :: "'a" and b :: "'b" ``` hoelzl@59664 ` 748` ``` have [simp]: "\c d. indicator (apfst f -` {(a, b)}) (c, d) = indicator (f -` {a}) c * (indicator {b} d::ereal)" ``` hoelzl@59664 ` 749` ``` by (auto split: split_indicator) ``` hoelzl@59664 ` 750` hoelzl@59664 ` 751` ``` have "ereal (pmf (pair_pmf (map_pmf f A) B) (a, b)) = ``` hoelzl@59664 ` 752` ``` ereal (pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b))" ``` hoelzl@59664 ` 753` ``` unfolding pmf_pair ereal_pmf_map ``` hoelzl@59664 ` 754` ``` by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_multc pmf_nonneg ``` hoelzl@59664 ` 755` ``` emeasure_map_pmf[symmetric] del: emeasure_map_pmf) ``` hoelzl@59664 ` 756` ``` then show "pmf (pair_pmf (map_pmf f A) B) (a, b) = pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b)" ``` hoelzl@59664 ` 757` ``` by simp ``` hoelzl@59664 ` 758` ```qed ``` hoelzl@59664 ` 759` hoelzl@59664 ` 760` ```lemma pair_map_pmf2: "pair_pmf A (map_pmf f B) = map_pmf (apsnd f) (pair_pmf A B)" ``` hoelzl@59664 ` 761` ```proof (safe intro!: pmf_eqI) ``` hoelzl@59664 ` 762` ``` fix a :: "'a" and b :: "'b" ``` hoelzl@59664 ` 763` ``` have [simp]: "\c d. indicator (apsnd f -` {(a, b)}) (c, d) = indicator {a} c * (indicator (f -` {b}) d::ereal)" ``` hoelzl@59664 ` 764` ``` by (auto split: split_indicator) ``` hoelzl@59664 ` 765` hoelzl@59664 ` 766` ``` have "ereal (pmf (pair_pmf A (map_pmf f B)) (a, b)) = ``` hoelzl@59664 ` 767` ``` ereal (pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b))" ``` hoelzl@59664 ` 768` ``` unfolding pmf_pair ereal_pmf_map ``` hoelzl@59664 ` 769` ``` by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_cmult nn_integral_multc pmf_nonneg ``` hoelzl@59664 ` 770` ``` emeasure_map_pmf[symmetric] del: emeasure_map_pmf) ``` hoelzl@59664 ` 771` ``` then show "pmf (pair_pmf A (map_pmf f B)) (a, b) = pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b)" ``` hoelzl@59664 ` 772` ``` by simp ``` hoelzl@59664 ` 773` ```qed ``` hoelzl@59664 ` 774` hoelzl@59664 ` 775` ```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 ` 776` ``` by (simp add: pair_map_pmf2 pair_map_pmf1 map_pmf_comp split_beta') ``` hoelzl@59664 ` 777` hoelzl@59000 ` 778` ```end ``` hoelzl@59000 ` 779` Andreas@61634 ` 780` ```lemma pair_return_pmf1: "pair_pmf (return_pmf x) y = map_pmf (Pair x) y" ``` Andreas@61634 ` 781` ```by(simp add: pair_pmf_def bind_return_pmf map_pmf_def) ``` Andreas@61634 ` 782` Andreas@61634 ` 783` ```lemma pair_return_pmf2: "pair_pmf x (return_pmf y) = map_pmf (\x. (x, y)) x" ``` Andreas@61634 ` 784` ```by(simp add: pair_pmf_def bind_return_pmf map_pmf_def) ``` Andreas@61634 ` 785` Andreas@61634 ` 786` ```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 ` 787` ```by(simp add: pair_pmf_def bind_return_pmf map_pmf_def bind_assoc_pmf) ``` Andreas@61634 ` 788` Andreas@61634 ` 789` ```lemma pair_commute_pmf: "pair_pmf x y = map_pmf (\(x, y). (y, x)) (pair_pmf y x)" ``` Andreas@61634 ` 790` ```unfolding pair_pmf_def by(subst bind_commute_pmf)(simp add: map_pmf_def bind_assoc_pmf bind_return_pmf) ``` Andreas@61634 ` 791` Andreas@61634 ` 792` ```lemma set_pmf_subset_singleton: "set_pmf p \ {x} \ p = return_pmf x" ``` Andreas@61634 ` 793` ```proof(intro iffI pmf_eqI) ``` Andreas@61634 ` 794` ``` fix i ``` Andreas@61634 ` 795` ``` assume x: "set_pmf p \ {x}" ``` Andreas@61634 ` 796` ``` hence *: "set_pmf p = {x}" using set_pmf_not_empty[of p] by auto ``` Andreas@61634 ` 797` ``` have "ereal (pmf p x) = \\<^sup>+ i. indicator {x} i \p" by(simp add: emeasure_pmf_single) ``` Andreas@61634 ` 798` ``` also have "\ = \\<^sup>+ i. 1 \p" by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * ) ``` Andreas@61634 ` 799` ``` also have "\ = 1" by simp ``` Andreas@61634 ` 800` ``` finally show "pmf p i = pmf (return_pmf x) i" using x ``` Andreas@61634 ` 801` ``` by(auto split: split_indicator simp add: pmf_eq_0_set_pmf) ``` Andreas@61634 ` 802` ```qed auto ``` Andreas@61634 ` 803` Andreas@61634 ` 804` ```lemma bind_eq_return_pmf: ``` Andreas@61634 ` 805` ``` "bind_pmf p f = return_pmf x \ (\y\set_pmf p. f y = return_pmf x)" ``` Andreas@61634 ` 806` ``` (is "?lhs \ ?rhs") ``` Andreas@61634 ` 807` ```proof(intro iffI strip) ``` Andreas@61634 ` 808` ``` fix y ``` Andreas@61634 ` 809` ``` assume y: "y \ set_pmf p" ``` Andreas@61634 ` 810` ``` assume "?lhs" ``` Andreas@61634 ` 811` ``` hence "set_pmf (bind_pmf p f) = {x}" by simp ``` Andreas@61634 ` 812` ``` hence "(\y\set_pmf p. set_pmf (f y)) = {x}" by simp ``` Andreas@61634 ` 813` ``` hence "set_pmf (f y) \ {x}" using y by auto ``` Andreas@61634 ` 814` ``` thus "f y = return_pmf x" by(simp add: set_pmf_subset_singleton) ``` Andreas@61634 ` 815` ```next ``` Andreas@61634 ` 816` ``` assume *: ?rhs ``` Andreas@61634 ` 817` ``` show ?lhs ``` Andreas@61634 ` 818` ``` proof(rule pmf_eqI) ``` Andreas@61634 ` 819` ``` fix i ``` Andreas@61634 ` 820` ``` have "ereal (pmf (bind_pmf p f) i) = \\<^sup>+ y. ereal (pmf (f y) i) \p" by(simp add: ereal_pmf_bind) ``` Andreas@61634 ` 821` ``` also have "\ = \\<^sup>+ y. ereal (pmf (return_pmf x) i) \p" ``` Andreas@61634 ` 822` ``` by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * ) ``` Andreas@61634 ` 823` ``` also have "\ = ereal (pmf (return_pmf x) i)" by simp ``` Andreas@61634 ` 824` ``` finally show "pmf (bind_pmf p f) i = pmf (return_pmf x) i" by simp ``` Andreas@61634 ` 825` ``` qed ``` Andreas@61634 ` 826` ```qed ``` Andreas@61634 ` 827` Andreas@61634 ` 828` ```lemma pmf_False_conv_True: "pmf p False = 1 - pmf p True" ``` Andreas@61634 ` 829` ```proof - ``` Andreas@61634 ` 830` ``` have "pmf p False + pmf p True = measure p {False} + measure p {True}" ``` Andreas@61634 ` 831` ``` by(simp add: measure_pmf_single) ``` Andreas@61634 ` 832` ``` also have "\ = measure p ({False} \ {True})" ``` Andreas@61634 ` 833` ``` by(subst measure_pmf.finite_measure_Union) simp_all ``` Andreas@61634 ` 834` ``` also have "{False} \ {True} = space p" by auto ``` Andreas@61634 ` 835` ``` finally show ?thesis by simp ``` Andreas@61634 ` 836` ```qed ``` Andreas@61634 ` 837` Andreas@61634 ` 838` ```lemma pmf_True_conv_False: "pmf p True = 1 - pmf p False" ``` Andreas@61634 ` 839` ```by(simp add: pmf_False_conv_True) ``` Andreas@61634 ` 840` hoelzl@59664 ` 841` ```subsection \ Conditional Probabilities \ ``` hoelzl@59664 ` 842` hoelzl@59670 ` 843` ```lemma measure_pmf_zero_iff: "measure (measure_pmf p) s = 0 \ set_pmf p \ s = {}" ``` hoelzl@59670 ` 844` ``` by (subst measure_pmf.prob_eq_0) (auto simp: AE_measure_pmf_iff) ``` hoelzl@59670 ` 845` hoelzl@59664 ` 846` ```context ``` hoelzl@59664 ` 847` ``` fixes p :: "'a pmf" and s :: "'a set" ``` hoelzl@59664 ` 848` ``` assumes not_empty: "set_pmf p \ s \ {}" ``` hoelzl@59664 ` 849` ```begin ``` hoelzl@59664 ` 850` hoelzl@59664 ` 851` ```interpretation pmf_as_measure . ``` hoelzl@59664 ` 852` hoelzl@59664 ` 853` ```lemma emeasure_measure_pmf_not_zero: "emeasure (measure_pmf p) s \ 0" ``` hoelzl@59664 ` 854` ```proof ``` hoelzl@59664 ` 855` ``` assume "emeasure (measure_pmf p) s = 0" ``` hoelzl@59664 ` 856` ``` then have "AE x in measure_pmf p. x \ s" ``` hoelzl@59664 ` 857` ``` by (rule AE_I[rotated]) auto ``` hoelzl@59664 ` 858` ``` with not_empty show False ``` hoelzl@59664 ` 859` ``` by (auto simp: AE_measure_pmf_iff) ``` hoelzl@59664 ` 860` ```qed ``` hoelzl@59664 ` 861` hoelzl@59664 ` 862` ```lemma measure_measure_pmf_not_zero: "measure (measure_pmf p) s \ 0" ``` hoelzl@59664 ` 863` ``` using emeasure_measure_pmf_not_zero unfolding measure_pmf.emeasure_eq_measure by simp ``` hoelzl@59664 ` 864` hoelzl@59664 ` 865` ```lift_definition cond_pmf :: "'a pmf" is ``` hoelzl@59664 ` 866` ``` "uniform_measure (measure_pmf p) s" ``` hoelzl@59664 ` 867` ```proof (intro conjI) ``` hoelzl@59664 ` 868` ``` show "prob_space (uniform_measure (measure_pmf p) s)" ``` hoelzl@59664 ` 869` ``` by (intro prob_space_uniform_measure) (auto simp: emeasure_measure_pmf_not_zero) ``` hoelzl@59664 ` 870` ``` show "AE x in uniform_measure (measure_pmf p) s. measure (uniform_measure (measure_pmf p) s) {x} \ 0" ``` hoelzl@59664 ` 871` ``` by (simp add: emeasure_measure_pmf_not_zero measure_measure_pmf_not_zero AE_uniform_measure ``` hoelzl@59664 ` 872` ``` AE_measure_pmf_iff set_pmf.rep_eq) ``` hoelzl@59664 ` 873` ```qed simp ``` hoelzl@59664 ` 874` hoelzl@59664 ` 875` ```lemma pmf_cond: "pmf cond_pmf x = (if x \ s then pmf p x / measure p s else 0)" ``` hoelzl@59664 ` 876` ``` by transfer (simp add: emeasure_measure_pmf_not_zero pmf.rep_eq) ``` hoelzl@59664 ` 877` hoelzl@59665 ` 878` ```lemma set_cond_pmf[simp]: "set_pmf cond_pmf = set_pmf p \ s" ``` nipkow@62390 ` 879` ``` by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: if_split_asm) ``` hoelzl@59664 ` 880` hoelzl@59664 ` 881` ```end ``` hoelzl@59664 ` 882` hoelzl@59664 ` 883` ```lemma cond_map_pmf: ``` hoelzl@59664 ` 884` ``` assumes "set_pmf p \ f -` s \ {}" ``` hoelzl@59664 ` 885` ``` shows "cond_pmf (map_pmf f p) s = map_pmf f (cond_pmf p (f -` s))" ``` hoelzl@59664 ` 886` ```proof - ``` hoelzl@59664 ` 887` ``` have *: "set_pmf (map_pmf f p) \ s \ {}" ``` hoelzl@59665 ` 888` ``` using assms by auto ``` hoelzl@59664 ` 889` ``` { fix x ``` hoelzl@59664 ` 890` ``` have "ereal (pmf (map_pmf f (cond_pmf p (f -` s))) x) = ``` hoelzl@59664 ` 891` ``` emeasure p (f -` s \ f -` {x}) / emeasure p (f -` s)" ``` hoelzl@59664 ` 892` ``` unfolding ereal_pmf_map cond_pmf.rep_eq[OF assms] by (simp add: nn_integral_uniform_measure) ``` hoelzl@59664 ` 893` ``` also have "f -` s \ f -` {x} = (if x \ s then f -` {x} else {})" ``` hoelzl@59664 ` 894` ``` by auto ``` hoelzl@59664 ` 895` ``` also have "emeasure p (if x \ s then f -` {x} else {}) / emeasure p (f -` s) = ``` hoelzl@59664 ` 896` ``` ereal (pmf (cond_pmf (map_pmf f p) s) x)" ``` hoelzl@59664 ` 897` ``` using measure_measure_pmf_not_zero[OF *] ``` hoelzl@59664 ` 898` ``` by (simp add: pmf_cond[OF *] ereal_divide' ereal_pmf_map measure_pmf.emeasure_eq_measure[symmetric] ``` hoelzl@59664 ` 899` ``` del: ereal_divide) ``` hoelzl@59664 ` 900` ``` finally have "ereal (pmf (cond_pmf (map_pmf f p) s) x) = ereal (pmf (map_pmf f (cond_pmf p (f -` s))) x)" ``` hoelzl@59664 ` 901` ``` by simp } ``` hoelzl@59664 ` 902` ``` then show ?thesis ``` hoelzl@59664 ` 903` ``` by (intro pmf_eqI) simp ``` hoelzl@59664 ` 904` ```qed ``` hoelzl@59664 ` 905` hoelzl@59664 ` 906` ```lemma bind_cond_pmf_cancel: ``` hoelzl@59670 ` 907` ``` assumes [simp]: "\x. x \ set_pmf p \ set_pmf q \ {y. R x y} \ {}" ``` hoelzl@59670 ` 908` ``` assumes [simp]: "\y. y \ set_pmf q \ set_pmf p \ {x. R x y} \ {}" ``` hoelzl@59670 ` 909` ``` 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 ` 910` ``` shows "bind_pmf p (\x. cond_pmf q {y. R x y}) = q" ``` hoelzl@59664 ` 911` ```proof (rule pmf_eqI) ``` hoelzl@59670 ` 912` ``` fix i ``` hoelzl@59670 ` 913` ``` have "ereal (pmf (bind_pmf p (\x. cond_pmf q {y. R x y})) i) = ``` hoelzl@59670 ` 914` ``` (\\<^sup>+x. ereal (pmf q i / measure p {x. R x i}) * ereal (indicator {x. R x i} x) \p)" ``` hoelzl@59670 ` 915` ``` by (auto simp add: ereal_pmf_bind AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf intro!: nn_integral_cong_AE) ``` hoelzl@59670 ` 916` ``` also have "\ = (pmf q i * measure p {x. R x i}) / measure p {x. R x i}" ``` hoelzl@59670 ` 917` ``` by (simp add: pmf_nonneg measure_nonneg zero_ereal_def[symmetric] ereal_indicator ``` hoelzl@59670 ` 918` ``` nn_integral_cmult measure_pmf.emeasure_eq_measure) ``` hoelzl@59670 ` 919` ``` also have "\ = pmf q i" ``` hoelzl@59670 ` 920` ``` by (cases "pmf q i = 0") (simp_all add: pmf_eq_0_set_pmf measure_measure_pmf_not_zero) ``` hoelzl@59670 ` 921` ``` finally show "pmf (bind_pmf p (\x. cond_pmf q {y. R x y})) i = pmf q i" ``` hoelzl@59670 ` 922` ``` by simp ``` hoelzl@59664 ` 923` ```qed ``` hoelzl@59664 ` 924` hoelzl@59664 ` 925` ```subsection \ Relator \ ``` hoelzl@59664 ` 926` hoelzl@59664 ` 927` ```inductive rel_pmf :: "('a \ 'b \ bool) \ 'a pmf \ 'b pmf \ bool" ``` hoelzl@59664 ` 928` ```for R p q ``` hoelzl@59664 ` 929` ```where ``` lp15@59667 ` 930` ``` "\ \x y. (x, y) \ set_pmf pq \ R x y; ``` hoelzl@59664 ` 931` ``` map_pmf fst pq = p; map_pmf snd pq = q \ ``` hoelzl@59664 ` 932` ``` \ rel_pmf R p q" ``` hoelzl@59664 ` 933` hoelzl@59681 ` 934` ```lemma rel_pmfI: ``` hoelzl@59681 ` 935` ``` assumes R: "rel_set R (set_pmf p) (set_pmf q)" ``` hoelzl@59681 ` 936` ``` assumes eq: "\x y. x \ set_pmf p \ y \ set_pmf q \ R x y \ ``` hoelzl@59681 ` 937` ``` measure p {x. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 938` ``` shows "rel_pmf R p q" ``` hoelzl@59681 ` 939` ```proof ``` hoelzl@59681 ` 940` ``` let ?pq = "bind_pmf p (\x. bind_pmf (cond_pmf q {y. R x y}) (\y. return_pmf (x, y)))" ``` hoelzl@59681 ` 941` ``` have "\x. x \ set_pmf p \ set_pmf q \ {y. R x y} \ {}" ``` hoelzl@59681 ` 942` ``` using R by (auto simp: rel_set_def) ``` hoelzl@59681 ` 943` ``` then show "\x y. (x, y) \ set_pmf ?pq \ R x y" ``` hoelzl@59681 ` 944` ``` by auto ``` hoelzl@59681 ` 945` ``` show "map_pmf fst ?pq = p" ``` Andreas@60068 ` 946` ``` by (simp add: map_bind_pmf bind_return_pmf') ``` hoelzl@59681 ` 947` hoelzl@59681 ` 948` ``` show "map_pmf snd ?pq = q" ``` hoelzl@59681 ` 949` ``` using R eq ``` Andreas@60068 ` 950` ``` apply (simp add: bind_cond_pmf_cancel map_bind_pmf bind_return_pmf') ``` hoelzl@59681 ` 951` ``` apply (rule bind_cond_pmf_cancel) ``` hoelzl@59681 ` 952` ``` apply (auto simp: rel_set_def) ``` hoelzl@59681 ` 953` ``` done ``` hoelzl@59681 ` 954` ```qed ``` hoelzl@59681 ` 955` hoelzl@59681 ` 956` ```lemma rel_pmf_imp_rel_set: "rel_pmf R p q \ rel_set R (set_pmf p) (set_pmf q)" ``` hoelzl@59681 ` 957` ``` by (force simp add: rel_pmf.simps rel_set_def) ``` hoelzl@59681 ` 958` hoelzl@59681 ` 959` ```lemma rel_pmfD_measure: ``` hoelzl@59681 ` 960` ``` assumes rel_R: "rel_pmf R p q" and R: "\a b. R a b \ R a y \ R x b" ``` hoelzl@59681 ` 961` ``` assumes "x \ set_pmf p" "y \ set_pmf q" ``` hoelzl@59681 ` 962` ``` shows "measure p {x. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 963` ```proof - ``` hoelzl@59681 ` 964` ``` from rel_R obtain pq where pq: "\x y. (x, y) \ set_pmf pq \ R x y" ``` hoelzl@59681 ` 965` ``` and eq: "p = map_pmf fst pq" "q = map_pmf snd pq" ``` hoelzl@59681 ` 966` ``` by (auto elim: rel_pmf.cases) ``` hoelzl@59681 ` 967` ``` have "measure p {x. R x y} = measure pq {x. R (fst x) y}" ``` hoelzl@59681 ` 968` ``` by (simp add: eq map_pmf_rep_eq measure_distr) ``` hoelzl@59681 ` 969` ``` also have "\ = measure pq {y. R x (snd y)}" ``` hoelzl@59681 ` 970` ``` by (intro measure_pmf.finite_measure_eq_AE) ``` hoelzl@59681 ` 971` ``` (auto simp: AE_measure_pmf_iff R dest!: pq) ``` hoelzl@59681 ` 972` ``` also have "\ = measure q {y. R x y}" ``` hoelzl@59681 ` 973` ``` by (simp add: eq map_pmf_rep_eq measure_distr) ``` hoelzl@59681 ` 974` ``` finally show "measure p {x. R x y} = measure q {y. R x y}" . ``` hoelzl@59681 ` 975` ```qed ``` hoelzl@59681 ` 976` Andreas@61634 ` 977` ```lemma rel_pmf_measureD: ``` Andreas@61634 ` 978` ``` assumes "rel_pmf R p q" ``` Andreas@61634 ` 979` ``` shows "measure (measure_pmf p) A \ measure (measure_pmf q) {y. \x\A. R x y}" (is "?lhs \ ?rhs") ``` Andreas@61634 ` 980` ```using assms ``` Andreas@61634 ` 981` ```proof cases ``` Andreas@61634 ` 982` ``` fix pq ``` Andreas@61634 ` 983` ``` assume R: "\x y. (x, y) \ set_pmf pq \ R x y" ``` Andreas@61634 ` 984` ``` and p[symmetric]: "map_pmf fst pq = p" ``` Andreas@61634 ` 985` ``` and q[symmetric]: "map_pmf snd pq = q" ``` Andreas@61634 ` 986` ``` have "?lhs = measure (measure_pmf pq) (fst -` A)" by(simp add: p) ``` Andreas@61634 ` 987` ``` also have "\ \ measure (measure_pmf pq) {y. \x\A. R x (snd y)}" ``` Andreas@61634 ` 988` ``` by(rule measure_pmf.finite_measure_mono_AE)(auto 4 3 simp add: AE_measure_pmf_iff dest: R) ``` Andreas@61634 ` 989` ``` also have "\ = ?rhs" by(simp add: q) ``` Andreas@61634 ` 990` ``` finally show ?thesis . ``` Andreas@61634 ` 991` ```qed ``` Andreas@61634 ` 992` hoelzl@59681 ` 993` ```lemma rel_pmf_iff_measure: ``` hoelzl@59681 ` 994` ``` assumes "symp R" "transp R" ``` hoelzl@59681 ` 995` ``` shows "rel_pmf R p q \ ``` hoelzl@59681 ` 996` ``` rel_set R (set_pmf p) (set_pmf q) \ ``` hoelzl@59681 ` 997` ``` (\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 ` 998` ``` by (safe intro!: rel_pmf_imp_rel_set rel_pmfI) ``` hoelzl@59681 ` 999` ``` (auto intro!: rel_pmfD_measure dest: sympD[OF \symp R\] transpD[OF \transp R\]) ``` hoelzl@59681 ` 1000` hoelzl@59681 ` 1001` ```lemma quotient_rel_set_disjoint: ``` hoelzl@59681 ` 1002` ``` "equivp R \ C \ UNIV // {(x, y). R x y} \ rel_set R A B \ A \ C = {} \ B \ C = {}" ``` lp15@61609 ` 1003` ``` using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C] ``` hoelzl@59681 ` 1004` ``` by (auto 0 0 simp: equivp_equiv rel_set_def set_eq_iff elim: equivpE) ``` hoelzl@59681 ` 1005` ``` (blast dest: equivp_symp)+ ``` hoelzl@59681 ` 1006` hoelzl@59681 ` 1007` ```lemma quotientD: "equiv X R \ A \ X // R \ x \ A \ A = R `` {x}" ``` hoelzl@59681 ` 1008` ``` by (metis Image_singleton_iff equiv_class_eq_iff quotientE) ``` hoelzl@59681 ` 1009` hoelzl@59681 ` 1010` ```lemma rel_pmf_iff_equivp: ``` hoelzl@59681 ` 1011` ``` assumes "equivp R" ``` hoelzl@59681 ` 1012` ``` shows "rel_pmf R p q \ (\C\UNIV // {(x, y). R x y}. measure p C = measure q C)" ``` hoelzl@59681 ` 1013` ``` (is "_ \ (\C\_//?R. _)") ``` hoelzl@59681 ` 1014` ```proof (subst rel_pmf_iff_measure, safe) ``` hoelzl@59681 ` 1015` ``` show "symp R" "transp R" ``` hoelzl@59681 ` 1016` ``` using assms by (auto simp: equivp_reflp_symp_transp) ``` hoelzl@59681 ` 1017` ```next ``` hoelzl@59681 ` 1018` ``` fix C assume C: "C \ UNIV // ?R" and R: "rel_set R (set_pmf p) (set_pmf q)" ``` hoelzl@59681 ` 1019` ``` 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 ` 1020` hoelzl@59681 ` 1021` ``` show "measure p C = measure q C" ``` hoelzl@59681 ` 1022` ``` proof cases ``` hoelzl@59681 ` 1023` ``` assume "p \ C = {}" ``` lp15@61609 ` 1024` ``` moreover then have "q \ C = {}" ``` hoelzl@59681 ` 1025` ``` using quotient_rel_set_disjoint[OF assms C R] by simp ``` hoelzl@59681 ` 1026` ``` ultimately show ?thesis ``` hoelzl@59681 ` 1027` ``` unfolding measure_pmf_zero_iff[symmetric] by simp ``` hoelzl@59681 ` 1028` ``` next ``` hoelzl@59681 ` 1029` ``` assume "p \ C \ {}" ``` lp15@61609 ` 1030` ``` moreover then have "q \ C \ {}" ``` hoelzl@59681 ` 1031` ``` using quotient_rel_set_disjoint[OF assms C R] by simp ``` hoelzl@59681 ` 1032` ``` ultimately obtain x y where in_set: "x \ set_pmf p" "y \ set_pmf q" and in_C: "x \ C" "y \ C" ``` hoelzl@59681 ` 1033` ``` by auto ``` hoelzl@59681 ` 1034` ``` then have "R x y" ``` hoelzl@59681 ` 1035` ``` using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms ``` hoelzl@59681 ` 1036` ``` by (simp add: equivp_equiv) ``` hoelzl@59681 ` 1037` ``` with in_set eq have "measure p {x. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 1038` ``` by auto ``` hoelzl@59681 ` 1039` ``` moreover have "{y. R x y} = C" ``` wenzelm@61808 ` 1040` ``` using assms \x \ C\ C quotientD[of UNIV ?R C x] by (simp add: equivp_equiv) ``` hoelzl@59681 ` 1041` ``` moreover have "{x. R x y} = C" ``` wenzelm@61808 ` 1042` ``` using assms \y \ C\ C quotientD[of UNIV "?R" C y] sympD[of R] ``` hoelzl@59681 ` 1043` ``` by (auto simp add: equivp_equiv elim: equivpE) ``` hoelzl@59681 ` 1044` ``` ultimately show ?thesis ``` hoelzl@59681 ` 1045` ``` by auto ``` hoelzl@59681 ` 1046` ``` qed ``` hoelzl@59681 ` 1047` ```next ``` hoelzl@59681 ` 1048` ``` assume eq: "\C\UNIV // ?R. measure p C = measure q C" ``` hoelzl@59681 ` 1049` ``` show "rel_set R (set_pmf p) (set_pmf q)" ``` hoelzl@59681 ` 1050` ``` unfolding rel_set_def ``` hoelzl@59681 ` 1051` ``` proof safe ``` hoelzl@59681 ` 1052` ``` fix x assume x: "x \ set_pmf p" ``` hoelzl@59681 ` 1053` ``` have "{y. R x y} \ UNIV // ?R" ``` hoelzl@59681 ` 1054` ``` by (auto simp: quotient_def) ``` hoelzl@59681 ` 1055` ``` with eq have *: "measure q {y. R x y} = measure p {y. R x y}" ``` hoelzl@59681 ` 1056` ``` by auto ``` hoelzl@59681 ` 1057` ``` have "measure q {y. R x y} \ 0" ``` hoelzl@59681 ` 1058` ``` using x assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp) ``` hoelzl@59681 ` 1059` ``` then show "\y\set_pmf q. R x y" ``` hoelzl@59681 ` 1060` ``` unfolding measure_pmf_zero_iff by auto ``` hoelzl@59681 ` 1061` ``` next ``` hoelzl@59681 ` 1062` ``` fix y assume y: "y \ set_pmf q" ``` hoelzl@59681 ` 1063` ``` have "{x. R x y} \ UNIV // ?R" ``` hoelzl@59681 ` 1064` ``` using assms by (auto simp: quotient_def dest: equivp_symp) ``` hoelzl@59681 ` 1065` ``` with eq have *: "measure p {x. R x y} = measure q {x. R x y}" ``` hoelzl@59681 ` 1066` ``` by auto ``` hoelzl@59681 ` 1067` ``` have "measure p {x. R x y} \ 0" ``` hoelzl@59681 ` 1068` ``` using y assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp) ``` hoelzl@59681 ` 1069` ``` then show "\x\set_pmf p. R x y" ``` hoelzl@59681 ` 1070` ``` unfolding measure_pmf_zero_iff by auto ``` hoelzl@59681 ` 1071` ``` qed ``` hoelzl@59681 ` 1072` hoelzl@59681 ` 1073` ``` fix x y assume "x \ set_pmf p" "y \ set_pmf q" "R x y" ``` hoelzl@59681 ` 1074` ``` have "{y. R x y} \ UNIV // ?R" "{x. R x y} = {y. R x y}" ``` wenzelm@61808 ` 1075` ``` using assms \R x y\ by (auto simp: quotient_def dest: equivp_symp equivp_transp) ``` hoelzl@59681 ` 1076` ``` with eq show "measure p {x. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 1077` ``` by auto ``` hoelzl@59681 ` 1078` ```qed ``` hoelzl@59681 ` 1079` hoelzl@59664 ` 1080` ```bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf ``` hoelzl@59664 ` 1081` ```proof - ``` hoelzl@59664 ` 1082` ``` show "map_pmf id = id" by (rule map_pmf_id) ``` lp15@59667 ` 1083` ``` show "\f g. map_pmf (f \ g) = map_pmf f \ map_pmf g" by (rule map_pmf_compose) ``` hoelzl@59664 ` 1084` ``` 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 ` 1085` ``` by (intro map_pmf_cong refl) ``` hoelzl@59664 ` 1086` hoelzl@59664 ` 1087` ``` show "\f::'a \ 'b. set_pmf \ map_pmf f = op ` f \ set_pmf" ``` hoelzl@59664 ` 1088` ``` by (rule pmf_set_map) ``` hoelzl@59664 ` 1089` wenzelm@60595 ` 1090` ``` show "(card_of (set_pmf p), natLeq) \ ordLeq" for p :: "'s pmf" ``` wenzelm@60595 ` 1091` ``` proof - ``` hoelzl@59664 ` 1092` ``` have "(card_of (set_pmf p), card_of (UNIV :: nat set)) \ ordLeq" ``` hoelzl@59664 ` 1093` ``` by (rule card_of_ordLeqI[where f="to_nat_on (set_pmf p)"]) ``` hoelzl@59664 ` 1094` ``` (auto intro: countable_set_pmf) ``` hoelzl@59664 ` 1095` ``` also have "(card_of (UNIV :: nat set), natLeq) \ ordLeq" ``` hoelzl@59664 ` 1096` ``` by (metis Field_natLeq card_of_least natLeq_Well_order) ``` wenzelm@60595 ` 1097` ``` finally show ?thesis . ``` wenzelm@60595 ` 1098` ``` qed ``` hoelzl@59664 ` 1099` traytel@62324 ` 1100` ``` show "\R. rel_pmf R = (\x y. \z. set_pmf z \ {(x, y). R x y} \ ``` traytel@62324 ` 1101` ``` map_pmf fst z = x \ map_pmf snd z = y)" ``` traytel@62324 ` 1102` ``` by (auto simp add: fun_eq_iff rel_pmf.simps) ``` hoelzl@59664 ` 1103` wenzelm@60595 ` 1104` ``` show "rel_pmf R OO rel_pmf S \ rel_pmf (R OO S)" ``` wenzelm@60595 ` 1105` ``` for R :: "'a \ 'b \ bool" and S :: "'b \ 'c \ bool" ``` wenzelm@60595 ` 1106` ``` proof - ``` wenzelm@60595 ` 1107` ``` { fix p q r ``` wenzelm@60595 ` 1108` ``` assume pq: "rel_pmf R p q" ``` wenzelm@60595 ` 1109` ``` and qr:"rel_pmf S q r" ``` wenzelm@60595 ` 1110` ``` from pq obtain pq where pq: "\x y. (x, y) \ set_pmf pq \ R x y" ``` wenzelm@60595 ` 1111` ``` and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto ``` wenzelm@60595 ` 1112` ``` from qr obtain qr where qr: "\y z. (y, z) \ set_pmf qr \ S y z" ``` wenzelm@60595 ` 1113` ``` and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto ``` lp15@61609 ` 1114` wenzelm@60595 ` 1115` ``` def pr \ "bind_pmf pq (\xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\yz. return_pmf (fst xy, snd yz)))" ``` wenzelm@60595 ` 1116` ``` have pr_welldefined: "\y. y \ q \ qr \ {yz. fst yz = y} \ {}" ``` wenzelm@60595 ` 1117` ``` by (force simp: q') ``` lp15@61609 ` 1118` wenzelm@60595 ` 1119` ``` have "rel_pmf (R OO S) p r" ``` wenzelm@60595 ` 1120` ``` proof (rule rel_pmf.intros) ``` wenzelm@60595 ` 1121` ``` fix x z assume "(x, z) \ pr" ``` wenzelm@60595 ` 1122` ``` then have "\y. (x, y) \ pq \ (y, z) \ qr" ``` wenzelm@60595 ` 1123` ``` by (auto simp: q pr_welldefined pr_def split_beta) ``` wenzelm@60595 ` 1124` ``` with pq qr show "(R OO S) x z" ``` wenzelm@60595 ` 1125` ``` by blast ``` wenzelm@60595 ` 1126` ``` next ``` wenzelm@60595 ` 1127` ``` have "map_pmf snd pr = map_pmf snd (bind_pmf q (\y. cond_pmf qr {yz. fst yz = y}))" ``` wenzelm@60595 ` 1128` ``` by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_pmf_comp) ``` wenzelm@60595 ` 1129` ``` then show "map_pmf snd pr = r" ``` wenzelm@60595 ` 1130` ``` unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute) ``` wenzelm@60595 ` 1131` ``` qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp) ``` wenzelm@60595 ` 1132` ``` } ``` wenzelm@60595 ` 1133` ``` then show ?thesis ``` wenzelm@60595 ` 1134` ``` by(auto simp add: le_fun_def) ``` wenzelm@60595 ` 1135` ``` qed ``` hoelzl@59664 ` 1136` ```qed (fact natLeq_card_order natLeq_cinfinite)+ ``` hoelzl@59664 ` 1137` Andreas@61634 ` 1138` ```lemma map_pmf_idI: "(\x. x \ set_pmf p \ f x = x) \ map_pmf f p = p" ``` Andreas@61634 ` 1139` ```by(simp cong: pmf.map_cong) ``` Andreas@61634 ` 1140` hoelzl@59665 ` 1141` ```lemma rel_pmf_conj[simp]: ``` hoelzl@59665 ` 1142` ``` "rel_pmf (\x y. P \ Q x y) x y \ P \ rel_pmf Q x y" ``` hoelzl@59665 ` 1143` ``` "rel_pmf (\x y. Q x y \ P) x y \ P \ rel_pmf Q x y" ``` hoelzl@59665 ` 1144` ``` using set_pmf_not_empty by (fastforce simp: pmf.in_rel subset_eq)+ ``` hoelzl@59665 ` 1145` hoelzl@59665 ` 1146` ```lemma rel_pmf_top[simp]: "rel_pmf top = top" ``` hoelzl@59665 ` 1147` ``` by (auto simp: pmf.in_rel[abs_def] fun_eq_iff map_fst_pair_pmf map_snd_pair_pmf ``` hoelzl@59665 ` 1148` ``` intro: exI[of _ "pair_pmf x y" for x y]) ``` hoelzl@59665 ` 1149` hoelzl@59664 ` 1150` ```lemma rel_pmf_return_pmf1: "rel_pmf R (return_pmf x) M \ (\a\M. R x a)" ``` hoelzl@59664 ` 1151` ```proof safe ``` hoelzl@59664 ` 1152` ``` fix a assume "a \ M" "rel_pmf R (return_pmf x) M" ``` hoelzl@59664 ` 1153` ``` then obtain pq where *: "\a b. (a, b) \ set_pmf pq \ R a b" ``` hoelzl@59664 ` 1154` ``` and eq: "return_pmf x = map_pmf fst pq" "M = map_pmf snd pq" ``` hoelzl@59664 ` 1155` ``` by (force elim: rel_pmf.cases) ``` hoelzl@59664 ` 1156` ``` moreover have "set_pmf (return_pmf x) = {x}" ``` hoelzl@59665 ` 1157` ``` by simp ``` wenzelm@61808 ` 1158` ``` with \a \ M\ have "(x, a) \ pq" ``` hoelzl@59665 ` 1159` ``` by (force simp: eq) ``` hoelzl@59664 ` 1160` ``` with * show "R x a" ``` hoelzl@59664 ` 1161` ``` by auto ``` hoelzl@59664 ` 1162` ```qed (auto intro!: rel_pmf.intros[where pq="pair_pmf (return_pmf x) M"] ``` hoelzl@59665 ` 1163` ``` simp: map_fst_pair_pmf map_snd_pair_pmf) ``` hoelzl@59664 ` 1164` hoelzl@59664 ` 1165` ```lemma rel_pmf_return_pmf2: "rel_pmf R M (return_pmf x) \ (\a\M. R a x)" ``` hoelzl@59664 ` 1166` ``` by (subst pmf.rel_flip[symmetric]) (simp add: rel_pmf_return_pmf1) ``` hoelzl@59664 ` 1167` hoelzl@59664 ` 1168` ```lemma rel_return_pmf[simp]: "rel_pmf R (return_pmf x1) (return_pmf x2) = R x1 x2" ``` hoelzl@59664 ` 1169` ``` unfolding rel_pmf_return_pmf2 set_return_pmf by simp ``` hoelzl@59664 ` 1170` hoelzl@59664 ` 1171` ```lemma rel_pmf_False[simp]: "rel_pmf (\x y. False) x y = False" ``` hoelzl@59664 ` 1172` ``` unfolding pmf.in_rel fun_eq_iff using set_pmf_not_empty by fastforce ``` hoelzl@59664 ` 1173` hoelzl@59664 ` 1174` ```lemma rel_pmf_rel_prod: ``` hoelzl@59664 ` 1175` ``` "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 ` 1176` ```proof safe ``` hoelzl@59664 ` 1177` ``` assume "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')" ``` hoelzl@59664 ` 1178` ``` then obtain pq where pq: "\a b c d. ((a, c), (b, d)) \ set_pmf pq \ R a b \ S c d" ``` hoelzl@59664 ` 1179` ``` and eq: "map_pmf fst pq = pair_pmf A A'" "map_pmf snd pq = pair_pmf B B'" ``` hoelzl@59664 ` 1180` ``` by (force elim: rel_pmf.cases) ``` hoelzl@59664 ` 1181` ``` show "rel_pmf R A B" ``` hoelzl@59664 ` 1182` ``` proof (rule rel_pmf.intros) ``` hoelzl@59664 ` 1183` ``` let ?f = "\(a, b). (fst a, fst b)" ``` hoelzl@59664 ` 1184` ``` have [simp]: "(\x. fst (?f x)) = fst o fst" "(\x. snd (?f x)) = fst o snd" ``` hoelzl@59664 ` 1185` ``` by auto ``` hoelzl@59664 ` 1186` hoelzl@59664 ` 1187` ``` show "map_pmf fst (map_pmf ?f pq) = A" ``` hoelzl@59664 ` 1188` ``` by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_fst_pair_pmf) ``` hoelzl@59664 ` 1189` ``` show "map_pmf snd (map_pmf ?f pq) = B" ``` hoelzl@59664 ` 1190` ``` by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_fst_pair_pmf) ``` hoelzl@59664 ` 1191` hoelzl@59664 ` 1192` ``` fix a b assume "(a, b) \ set_pmf (map_pmf ?f pq)" ``` hoelzl@59664 ` 1193` ``` then obtain c d where "((a, c), (b, d)) \ set_pmf pq" ``` hoelzl@59665 ` 1194` ``` by auto ``` hoelzl@59664 ` 1195` ``` from pq[OF this] show "R a b" .. ``` hoelzl@59664 ` 1196` ``` qed ``` hoelzl@59664 ` 1197` ``` show "rel_pmf S A' B'" ``` hoelzl@59664 ` 1198` ``` proof (rule rel_pmf.intros) ``` hoelzl@59664 ` 1199` ``` let ?f = "\(a, b). (snd a, snd b)" ``` hoelzl@59664 ` 1200` ``` have [simp]: "(\x. fst (?f x)) = snd o fst" "(\x. snd (?f x)) = snd o snd" ``` hoelzl@59664 ` 1201` ``` by auto ``` hoelzl@59664 ` 1202` hoelzl@59664 ` 1203` ``` show "map_pmf fst (map_pmf ?f pq) = A'" ``` hoelzl@59664 ` 1204` ``` by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_snd_pair_pmf) ``` hoelzl@59664 ` 1205` ``` show "map_pmf snd (map_pmf ?f pq) = B'" ``` hoelzl@59664 ` 1206` ``` by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_snd_pair_pmf) ``` hoelzl@59664 ` 1207` hoelzl@59664 ` 1208` ``` fix c d assume "(c, d) \ set_pmf (map_pmf ?f pq)" ``` hoelzl@59664 ` 1209` ``` then obtain a b where "((a, c), (b, d)) \ set_pmf pq" ``` hoelzl@59665 ` 1210` ``` by auto ``` hoelzl@59664 ` 1211` ``` from pq[OF this] show "S c d" .. ``` hoelzl@59664 ` 1212` ``` qed ``` hoelzl@59664 ` 1213` ```next ``` hoelzl@59664 ` 1214` ``` assume "rel_pmf R A B" "rel_pmf S A' B'" ``` hoelzl@59664 ` 1215` ``` then obtain Rpq Spq ``` hoelzl@59664 ` 1216` ``` where Rpq: "\a b. (a, b) \ set_pmf Rpq \ R a b" ``` hoelzl@59664 ` 1217` ``` "map_pmf fst Rpq = A" "map_pmf snd Rpq = B" ``` hoelzl@59664 ` 1218` ``` and Spq: "\a b. (a, b) \ set_pmf Spq \ S a b" ``` hoelzl@59664 ` 1219` ``` "map_pmf fst Spq = A'" "map_pmf snd Spq = B'" ``` hoelzl@59664 ` 1220` ``` by (force elim: rel_pmf.cases) ``` hoelzl@59664 ` 1221` hoelzl@59664 ` 1222` ``` let ?f = "(\((a, c), (b, d)). ((a, b), (c, d)))" ``` hoelzl@59664 ` 1223` ``` let ?pq = "map_pmf ?f (pair_pmf Rpq Spq)" ``` hoelzl@59664 ` 1224` ``` have [simp]: "(\x. fst (?f x)) = (\(a, b). (fst a, fst b))" "(\x. snd (?f x)) = (\(a, b). (snd a, snd b))" ``` hoelzl@59664 ` 1225` ``` by auto ``` hoelzl@59664 ` 1226` hoelzl@59664 ` 1227` ``` show "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')" ``` hoelzl@59664 ` 1228` ``` by (rule rel_pmf.intros[where pq="?pq"]) ``` hoelzl@59665 ` 1229` ``` (auto simp: map_snd_pair_pmf map_fst_pair_pmf map_pmf_comp Rpq Spq ``` hoelzl@59664 ` 1230` ``` map_pair) ``` hoelzl@59664 ` 1231` ```qed ``` hoelzl@59664 ` 1232` lp15@59667 ` 1233` ```lemma rel_pmf_reflI: ``` hoelzl@59664 ` 1234` ``` assumes "\x. x \ set_pmf p \ P x x" ``` hoelzl@59664 ` 1235` ``` shows "rel_pmf P p p" ``` hoelzl@59665 ` 1236` ``` by (rule rel_pmf.intros[where pq="map_pmf (\x. (x, x)) p"]) ``` hoelzl@59665 ` 1237` ``` (auto simp add: pmf.map_comp o_def assms) ``` hoelzl@59664 ` 1238` Andreas@61634 ` 1239` ```lemma rel_pmf_bij_betw: ``` Andreas@61634 ` 1240` ``` assumes f: "bij_betw f (set_pmf p) (set_pmf q)" ``` Andreas@61634 ` 1241` ``` and eq: "\x. x \ set_pmf p \ pmf p x = pmf q (f x)" ``` Andreas@61634 ` 1242` ``` shows "rel_pmf (\x y. f x = y) p q" ``` Andreas@61634 ` 1243` ```proof(rule rel_pmf.intros) ``` Andreas@61634 ` 1244` ``` let ?pq = "map_pmf (\x. (x, f x)) p" ``` Andreas@61634 ` 1245` ``` show "map_pmf fst ?pq = p" by(simp add: pmf.map_comp o_def) ``` Andreas@61634 ` 1246` Andreas@61634 ` 1247` ``` have "map_pmf f p = q" ``` Andreas@61634 ` 1248` ``` proof(rule pmf_eqI) ``` Andreas@61634 ` 1249` ``` fix i ``` Andreas@61634 ` 1250` ``` show "pmf (map_pmf f p) i = pmf q i" ``` Andreas@61634 ` 1251` ``` proof(cases "i \ set_pmf q") ``` Andreas@61634 ` 1252` ``` case True ``` Andreas@61634 ` 1253` ``` with f obtain j where "i = f j" "j \ set_pmf p" ``` Andreas@61634 ` 1254` ``` by(auto simp add: bij_betw_def image_iff) ``` Andreas@61634 ` 1255` ``` thus ?thesis using f by(simp add: bij_betw_def pmf_map_inj eq) ``` Andreas@61634 ` 1256` ``` next ``` Andreas@61634 ` 1257` ``` case False thus ?thesis ``` Andreas@61634 ` 1258` ``` by(subst pmf_map_outside)(auto simp add: set_pmf_iff eq[symmetric]) ``` Andreas@61634 ` 1259` ``` qed ``` Andreas@61634 ` 1260` ``` qed ``` Andreas@61634 ` 1261` ``` then show "map_pmf snd ?pq = q" by(simp add: pmf.map_comp o_def) ``` Andreas@61634 ` 1262` ```qed auto ``` Andreas@61634 ` 1263` hoelzl@59664 ` 1264` ```context ``` hoelzl@59664 ` 1265` ```begin ``` hoelzl@59664 ` 1266` hoelzl@59664 ` 1267` ```interpretation pmf_as_measure . ``` hoelzl@59664 ` 1268` hoelzl@59664 ` 1269` ```definition "join_pmf M = bind_pmf M (\x. x)" ``` hoelzl@59664 ` 1270` hoelzl@59664 ` 1271` ```lemma bind_eq_join_pmf: "bind_pmf M f = join_pmf (map_pmf f M)" ``` hoelzl@59664 ` 1272` ``` unfolding join_pmf_def bind_map_pmf .. ``` hoelzl@59664 ` 1273` hoelzl@59664 ` 1274` ```lemma join_eq_bind_pmf: "join_pmf M = bind_pmf M id" ``` hoelzl@59664 ` 1275` ``` by (simp add: join_pmf_def id_def) ``` hoelzl@59664 ` 1276` hoelzl@59664 ` 1277` ```lemma pmf_join: "pmf (join_pmf N) i = (\M. pmf M i \measure_pmf N)" ``` hoelzl@59664 ` 1278` ``` unfolding join_pmf_def pmf_bind .. ``` hoelzl@59664 ` 1279` hoelzl@59664 ` 1280` ```lemma ereal_pmf_join: "ereal (pmf (join_pmf N) i) = (\\<^sup>+M. pmf M i \measure_pmf N)" ``` hoelzl@59664 ` 1281` ``` unfolding join_pmf_def ereal_pmf_bind .. ``` hoelzl@59664 ` 1282` hoelzl@59665 ` 1283` ```lemma set_pmf_join_pmf[simp]: "set_pmf (join_pmf f) = (\p\set_pmf f. set_pmf p)" ``` hoelzl@59665 ` 1284` ``` by (simp add: join_pmf_def) ``` hoelzl@59664 ` 1285` hoelzl@59664 ` 1286` ```lemma join_return_pmf: "join_pmf (return_pmf M) = M" ``` hoelzl@59664 ` 1287` ``` by (simp add: integral_return pmf_eq_iff pmf_join return_pmf.rep_eq) ``` hoelzl@59664 ` 1288` hoelzl@59664 ` 1289` ```lemma map_join_pmf: "map_pmf f (join_pmf AA) = join_pmf (map_pmf (map_pmf f) AA)" ``` hoelzl@59664 ` 1290` ``` by (simp add: join_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf) ``` hoelzl@59664 ` 1291` hoelzl@59664 ` 1292` ```lemma join_map_return_pmf: "join_pmf (map_pmf return_pmf A) = A" ``` hoelzl@59664 ` 1293` ``` by (simp add: join_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') ``` hoelzl@59664 ` 1294` hoelzl@59664 ` 1295` ```end ``` hoelzl@59664 ` 1296` hoelzl@59664 ` 1297` ```lemma rel_pmf_joinI: ``` hoelzl@59664 ` 1298` ``` assumes "rel_pmf (rel_pmf P) p q" ``` hoelzl@59664 ` 1299` ``` shows "rel_pmf P (join_pmf p) (join_pmf q)" ``` hoelzl@59664 ` 1300` ```proof - ``` hoelzl@59664 ` 1301` ``` from assms obtain pq where p: "p = map_pmf fst pq" ``` hoelzl@59664 ` 1302` ``` and q: "q = map_pmf snd pq" ``` hoelzl@59664 ` 1303` ``` and P: "\x y. (x, y) \ set_pmf pq \ rel_pmf P x y" ``` hoelzl@59664 ` 1304` ``` by cases auto ``` lp15@59667 ` 1305` ``` from P obtain PQ ``` hoelzl@59664 ` 1306` ``` where PQ: "\x y a b. \ (x, y) \ set_pmf pq; (a, b) \ set_pmf (PQ x y) \ \ P a b" ``` hoelzl@59664 ` 1307` ``` and x: "\x y. (x, y) \ set_pmf pq \ map_pmf fst (PQ x y) = x" ``` hoelzl@59664 ` 1308` ``` and y: "\x y. (x, y) \ set_pmf pq \ map_pmf snd (PQ x y) = y" ``` hoelzl@59664 ` 1309` ``` by(metis rel_pmf.simps) ``` hoelzl@59664 ` 1310` hoelzl@59664 ` 1311` ``` let ?r = "bind_pmf pq (\(x, y). PQ x y)" ``` hoelzl@59665 ` 1312` ``` have "\a b. (a, b) \ set_pmf ?r \ P a b" by (auto intro: PQ) ``` hoelzl@59664 ` 1313` ``` moreover have "map_pmf fst ?r = join_pmf p" "map_pmf snd ?r = join_pmf q" ``` hoelzl@59664 ` 1314` ``` 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 ` 1315` ``` ultimately show ?thesis .. ``` hoelzl@59664 ` 1316` ```qed ``` hoelzl@59664 ` 1317` hoelzl@59664 ` 1318` ```lemma rel_pmf_bindI: ``` hoelzl@59664 ` 1319` ``` assumes pq: "rel_pmf R p q" ``` hoelzl@59664 ` 1320` ``` and fg: "\x y. R x y \ rel_pmf P (f x) (g y)" ``` hoelzl@59664 ` 1321` ``` shows "rel_pmf P (bind_pmf p f) (bind_pmf q g)" ``` hoelzl@59664 ` 1322` ``` unfolding bind_eq_join_pmf ``` hoelzl@59664 ` 1323` ``` by (rule rel_pmf_joinI) ``` hoelzl@59664 ` 1324` ``` (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 ` 1325` wenzelm@61808 ` 1326` ```text \ ``` hoelzl@59664 ` 1327` ``` Proof that @{const rel_pmf} preserves orders. ``` lp15@59667 ` 1328` ``` Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism, ``` lp15@59667 ` 1329` ``` Theoretical Computer Science 12(1):19--37, 1980, ``` hoelzl@59664 ` 1330` ``` @{url "http://dx.doi.org/10.1016/0304-3975(80)90003-1"} ``` wenzelm@61808 ` 1331` ```\ ``` hoelzl@59664 ` 1332` lp15@59667 ` 1333` ```lemma ``` hoelzl@59664 ` 1334` ``` assumes *: "rel_pmf R p q" ``` hoelzl@59664 ` 1335` ``` and refl: "reflp R" and trans: "transp R" ``` hoelzl@59664 ` 1336` ``` shows measure_Ici: "measure p {y. R x y} \ measure q {y. R x y}" (is ?thesis1) ``` hoelzl@59664 ` 1337` ``` 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 ` 1338` ```proof - ``` hoelzl@59664 ` 1339` ``` from * obtain pq ``` hoelzl@59664 ` 1340` ``` where pq: "\x y. (x, y) \ set_pmf pq \ R x y" ``` hoelzl@59664 ` 1341` ``` and p: "p = map_pmf fst pq" ``` hoelzl@59664 ` 1342` ``` and q: "q = map_pmf snd pq" ``` hoelzl@59664 ` 1343` ``` by cases auto ``` hoelzl@59664 ` 1344` ``` show ?thesis1 ?thesis2 unfolding p q map_pmf_rep_eq using refl trans ``` hoelzl@59664 ` 1345` ``` 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 ` 1346` ```qed ``` hoelzl@59664 ` 1347` hoelzl@59664 ` 1348` ```lemma rel_pmf_inf: ``` hoelzl@59664 ` 1349` ``` fixes p q :: "'a pmf" ``` hoelzl@59664 ` 1350` ``` assumes 1: "rel_pmf R p q" ``` hoelzl@59664 ` 1351` ``` assumes 2: "rel_pmf R q p" ``` hoelzl@59664 ` 1352` ``` and refl: "reflp R" and trans: "transp R" ``` hoelzl@59664 ` 1353` ``` shows "rel_pmf (inf R R\\) p q" ``` hoelzl@59681 ` 1354` ```proof (subst rel_pmf_iff_equivp, safe) ``` hoelzl@59681 ` 1355` ``` show "equivp (inf R R\\)" ``` hoelzl@59681 ` 1356` ``` using trans refl by (auto simp: equivp_reflp_symp_transp intro: sympI transpI reflpI dest: transpD reflpD) ``` lp15@61609 ` 1357` hoelzl@59681 ` 1358` ``` fix C assume "C \ UNIV // {(x, y). inf R R\\ x y}" ``` hoelzl@59681 ` 1359` ``` then obtain x where C: "C = {y. R x y \ R y x}" ``` hoelzl@59681 ` 1360` ``` by (auto elim: quotientE) ``` hoelzl@59681 ` 1361` hoelzl@59670 ` 1362` ``` let ?R = "\x y. R x y \ R y x" ``` hoelzl@59670 ` 1363` ``` let ?\R = "\y. measure q {x. ?R x y}" ``` hoelzl@59681 ` 1364` ``` have "measure p {y. ?R x y} = measure p ({y. R x y} - {y. R x y \ \ R y x})" ``` hoelzl@59681 ` 1365` ``` by(auto intro!: arg_cong[where f="measure p"]) ``` hoelzl@59681 ` 1366` ``` also have "\ = measure p {y. R x y} - measure p {y. R x y \ \ R y x}" ``` hoelzl@59681 ` 1367` ``` by (rule measure_pmf.finite_measure_Diff) auto ``` hoelzl@59681 ` 1368` ``` also have "measure p {y. R x y \ \ R y x} = measure q {y. R x y \ \ R y x}" ``` hoelzl@59681 ` 1369` ``` using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi) ``` hoelzl@59681 ` 1370` ``` also have "measure p {y. R x y} = measure q {y. R x y}" ``` hoelzl@59681 ` 1371` ``` using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici) ``` hoelzl@59681 ` 1372` ``` also have "measure q {y. R x y} - measure q {y. R x y \ \ R y x} = ``` hoelzl@59681 ` 1373` ``` measure q ({y. R x y} - {y. R x y \ \ R y x})" ``` hoelzl@59681 ` 1374` ``` by(rule measure_pmf.finite_measure_Diff[symmetric]) auto ``` hoelzl@59681 ` 1375` ``` also have "\ = ?\R x" ``` hoelzl@59681 ` 1376` ``` by(auto intro!: arg_cong[where f="measure q"]) ``` hoelzl@59681 ` 1377` ``` finally show "measure p C = measure q C" ``` hoelzl@59681 ` 1378` ``` by (simp add: C conj_commute) ``` hoelzl@59664 ` 1379` ```qed ``` hoelzl@59664 ` 1380` hoelzl@59664 ` 1381` ```lemma rel_pmf_antisym: ``` hoelzl@59664 ` 1382` ``` fixes p q :: "'a pmf" ``` hoelzl@59664 ` 1383` ``` assumes 1: "rel_pmf R p q" ``` hoelzl@59664 ` 1384` ``` assumes 2: "rel_pmf R q p" ``` hoelzl@59664 ` 1385` ``` and refl: "reflp R" and trans: "transp R" and antisym: "antisymP R" ``` hoelzl@59664 ` 1386` ``` shows "p = q" ``` hoelzl@59664 ` 1387` ```proof - ``` hoelzl@59664 ` 1388` ``` from 1 2 refl trans have "rel_pmf (inf R R\\) p q" by(rule rel_pmf_inf) ``` hoelzl@59664 ` 1389` ``` also have "inf R R\\ = op =" ``` hoelzl@59665 ` 1390` ``` using refl antisym by (auto intro!: ext simp add: reflpD dest: antisymD) ``` hoelzl@59664 ` 1391` ``` finally show ?thesis unfolding pmf.rel_eq . ``` hoelzl@59664 ` 1392` ```qed ``` hoelzl@59664 ` 1393` hoelzl@59664 ` 1394` ```lemma reflp_rel_pmf: "reflp R \ reflp (rel_pmf R)" ``` hoelzl@59664 ` 1395` ```by(blast intro: reflpI rel_pmf_reflI reflpD) ``` hoelzl@59664 ` 1396` hoelzl@59664 ` 1397` ```lemma antisymP_rel_pmf: ``` hoelzl@59664 ` 1398` ``` "\ reflp R; transp R; antisymP R \ ``` hoelzl@59664 ` 1399` ``` \ antisymP (rel_pmf R)" ``` hoelzl@59664 ` 1400` ```by(rule antisymI)(blast intro: rel_pmf_antisym) ``` hoelzl@59664 ` 1401` hoelzl@59664 ` 1402` ```lemma transp_rel_pmf: ``` hoelzl@59664 ` 1403` ``` assumes "transp R" ``` hoelzl@59664 ` 1404` ``` shows "transp (rel_pmf R)" ``` hoelzl@59664 ` 1405` ```proof (rule transpI) ``` hoelzl@59664 ` 1406` ``` fix x y z ``` hoelzl@59664 ` 1407` ``` assume "rel_pmf R x y" and "rel_pmf R y z" ``` hoelzl@59664 ` 1408` ``` hence "rel_pmf (R OO R) x z" by (simp add: pmf.rel_compp relcompp.relcompI) ``` hoelzl@59664 ` 1409` ``` thus "rel_pmf R x z" ``` hoelzl@59664 ` 1410` ``` using assms by (metis (no_types) pmf.rel_mono rev_predicate2D transp_relcompp_less_eq) ``` hoelzl@59664 ` 1411` ```qed ``` hoelzl@59664 ` 1412` hoelzl@59664 ` 1413` ```subsection \ Distributions \ ``` hoelzl@59664 ` 1414` hoelzl@59000 ` 1415` ```context ``` hoelzl@59000 ` 1416` ```begin ``` hoelzl@59000 ` 1417` hoelzl@59000 ` 1418` ```interpretation pmf_as_function . ``` hoelzl@59000 ` 1419` hoelzl@59093 ` 1420` ```subsubsection \ Bernoulli Distribution \ ``` hoelzl@59093 ` 1421` hoelzl@59000 ` 1422` ```lift_definition bernoulli_pmf :: "real \ bool pmf" is ``` hoelzl@59000 ` 1423` ``` "\p b. ((\p. if b then p else 1 - p) \ min 1 \ max 0) p" ``` hoelzl@59000 ` 1424` ``` by (auto simp: nn_integral_count_space_finite[where A="{False, True}"] UNIV_bool ``` hoelzl@59000 ` 1425` ``` split: split_max split_min) ``` hoelzl@59000 ` 1426` hoelzl@59000 ` 1427` ```lemma pmf_bernoulli_True[simp]: "0 \ p \ p \ 1 \ pmf (bernoulli_pmf p) True = p" ``` hoelzl@59000 ` 1428` ``` by transfer simp ``` hoelzl@59000 ` 1429` hoelzl@59000 ` 1430` ```lemma pmf_bernoulli_False[simp]: "0 \ p \ p \ 1 \ pmf (bernoulli_pmf p) False = 1 - p" ``` hoelzl@59000 ` 1431` ``` by transfer simp ``` hoelzl@59000 ` 1432` hoelzl@59000 ` 1433` ```lemma set_pmf_bernoulli: "0 < p \ p < 1 \ set_pmf (bernoulli_pmf p) = UNIV" ``` hoelzl@59000 ` 1434` ``` by (auto simp add: set_pmf_iff UNIV_bool) ``` hoelzl@59000 ` 1435` lp15@59667 ` 1436` ```lemma nn_integral_bernoulli_pmf[simp]: ``` hoelzl@59002 ` 1437` ``` assumes [simp]: "0 \ p" "p \ 1" "\x. 0 \ f x" ``` hoelzl@59002 ` 1438` ``` shows "(\\<^sup>+x. f x \bernoulli_pmf p) = f True * p + f False * (1 - p)" ``` hoelzl@59002 ` 1439` ``` by (subst nn_integral_measure_pmf_support[of UNIV]) ``` hoelzl@59002 ` 1440` ``` (auto simp: UNIV_bool field_simps) ``` hoelzl@59002 ` 1441` lp15@59667 ` 1442` ```lemma integral_bernoulli_pmf[simp]: ``` hoelzl@59002 ` 1443` ``` assumes [simp]: "0 \ p" "p \ 1" ``` hoelzl@59002 ` 1444` ``` shows "(\x. f x \bernoulli_pmf p) = f True * p + f False * (1 - p)" ``` hoelzl@59002 ` 1445` ``` by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool) ``` hoelzl@59002 ` 1446` Andreas@59525 ` 1447` ```lemma pmf_bernoulli_half [simp]: "pmf (bernoulli_pmf (1 / 2)) x = 1 / 2" ``` Andreas@59525 ` 1448` ```by(cases x) simp_all ``` Andreas@59525 ` 1449` Andreas@59525 ` 1450` ```lemma measure_pmf_bernoulli_half: "measure_pmf (bernoulli_pmf (1 / 2)) = uniform_count_measure UNIV" ``` Andreas@59525 ` 1451` ```by(rule measure_eqI)(simp_all add: nn_integral_pmf[symmetric] emeasure_uniform_count_measure nn_integral_count_space_finite sets_uniform_count_measure) ``` Andreas@59525 ` 1452` hoelzl@59093 ` 1453` ```subsubsection \ Geometric Distribution \ ``` hoelzl@59093 ` 1454` hoelzl@60602 ` 1455` ```context ``` hoelzl@60602 ` 1456` ``` fixes p :: real assumes p[arith]: "0 < p" "p \ 1" ``` hoelzl@60602 ` 1457` ```begin ``` hoelzl@60602 ` 1458` hoelzl@60602 ` 1459` ```lift_definition geometric_pmf :: "nat pmf" is "\n. (1 - p)^n * p" ``` hoelzl@59000 ` 1460` ```proof ``` hoelzl@60602 ` 1461` ``` have "(\i. ereal (p * (1 - p) ^ i)) = ereal (p * (1 / (1 - (1 - p))))" ``` hoelzl@60602 ` 1462` ``` by (intro sums_suminf_ereal sums_mult geometric_sums) auto ``` hoelzl@60602 ` 1463` ``` then show "(\\<^sup>+ x. ereal ((1 - p)^x * p) \count_space UNIV) = 1" ``` hoelzl@59000 ` 1464` ``` by (simp add: nn_integral_count_space_nat field_simps) ``` hoelzl@59000 ` 1465` ```qed simp ``` hoelzl@59000 ` 1466` hoelzl@60602 ` 1467` ```lemma pmf_geometric[simp]: "pmf geometric_pmf n = (1 - p)^n * p" ``` hoelzl@59000 ` 1468` ``` by transfer rule ``` hoelzl@59000 ` 1469` hoelzl@60602 ` 1470` ```end ``` hoelzl@60602 ` 1471` hoelzl@60602 ` 1472` ```lemma set_pmf_geometric: "0 < p \ p < 1 \ set_pmf (geometric_pmf p) = UNIV" ``` lp15@61609 ` 1473` ``` by (auto simp: set_pmf_iff) ``` hoelzl@59000 ` 1474` hoelzl@59093 ` 1475` ```subsubsection \ Uniform Multiset Distribution \ ``` hoelzl@59093 ` 1476` hoelzl@59000 ` 1477` ```context ``` hoelzl@59000 ` 1478` ``` fixes M :: "'a multiset" assumes M_not_empty: "M \ {#}" ``` hoelzl@59000 ` 1479` ```begin ``` hoelzl@59000 ` 1480` hoelzl@59000 ` 1481` ```lift_definition pmf_of_multiset :: "'a pmf" is "\x. count M x / size M" ``` hoelzl@59000 ` 1482` ```proof ``` lp15@59667 ` 1483` ``` show "(\\<^sup>+ x. ereal (real (count M x) / real (size M)) \count_space UNIV) = 1" ``` hoelzl@59000 ` 1484` ``` using M_not_empty ``` hoelzl@59000 ` 1485` ``` by (simp add: zero_less_divide_iff nn_integral_count_space nonempty_has_size ``` hoelzl@59000 ` 1486` ``` setsum_divide_distrib[symmetric]) ``` hoelzl@59000 ` 1487` ``` (auto simp: size_multiset_overloaded_eq intro!: setsum.cong) ``` hoelzl@59000 ` 1488` ```qed simp ``` hoelzl@59000 ` 1489` hoelzl@59000 ` 1490` ```lemma pmf_of_multiset[simp]: "pmf pmf_of_multiset x = count M x / size M" ``` hoelzl@59000 ` 1491` ``` by transfer rule ``` hoelzl@59000 ` 1492` nipkow@60495 ` 1493` ```lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_mset M" ``` hoelzl@59000 ` 1494` ``` by (auto simp: set_pmf_iff) ``` hoelzl@59000 ` 1495` hoelzl@59000 ` 1496` ```end ``` hoelzl@59000 ` 1497` hoelzl@59093 ` 1498` ```subsubsection \ Uniform Distribution \ ``` hoelzl@59093 ` 1499` hoelzl@59000 ` 1500` ```context ``` hoelzl@59000 ` 1501` ``` fixes S :: "'a set" assumes S_not_empty: "S \ {}" and S_finite: "finite S" ``` hoelzl@59000 ` 1502` ```begin ``` hoelzl@59000 ` 1503` hoelzl@59000 ` 1504` ```lift_definition pmf_of_set :: "'a pmf" is "\x. indicator S x / card S" ``` hoelzl@59000 ` 1505` ```proof ``` lp15@59667 ` 1506` ``` show "(\\<^sup>+ x. ereal (indicator S x / real (card S)) \count_space UNIV) = 1" ``` hoelzl@59000 ` 1507` ``` using S_not_empty S_finite by (subst nn_integral_count_space'[of S]) auto ``` hoelzl@59000 ` 1508` ```qed simp ``` hoelzl@59000 ` 1509` hoelzl@59000 ` 1510` ```lemma pmf_of_set[simp]: "pmf pmf_of_set x = indicator S x / card S" ``` hoelzl@59000 ` 1511` ``` by transfer rule ``` hoelzl@59000 ` 1512` hoelzl@59000 ` 1513` ```lemma set_pmf_of_set[simp]: "set_pmf pmf_of_set = S" ``` hoelzl@59000 ` 1514` ``` using S_finite S_not_empty by (auto simp: set_pmf_iff) ``` hoelzl@59000 ` 1515` Andreas@61634 ` 1516` ```lemma emeasure_pmf_of_set_space[simp]: "emeasure pmf_of_set S = 1" ``` hoelzl@59002 ` 1517` ``` by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff) ``` hoelzl@59002 ` 1518` lp15@61609 ` 1519` ```lemma nn_integral_pmf_of_set': ``` Andreas@60068 ` 1520` ``` "(\x. x \ S \ f x \ 0) \ nn_integral (measure_pmf pmf_of_set) f = setsum f S / card S" ``` Andreas@60068 ` 1521` ```apply(subst nn_integral_measure_pmf_finite, simp_all add: S_finite) ``` Andreas@60068 ` 1522` ```apply(simp add: setsum_ereal_left_distrib[symmetric]) ``` Andreas@60068 ` 1523` ```apply(subst ereal_divide', simp add: S_not_empty S_finite) ``` Andreas@60068 ` 1524` ```apply(simp add: ereal_times_divide_eq one_ereal_def[symmetric]) ``` Andreas@60068 ` 1525` ```done ``` Andreas@60068 ` 1526` lp15@61609 ` 1527` ```lemma nn_integral_pmf_of_set: ``` Andreas@60068 ` 1528` ``` "nn_integral (measure_pmf pmf_of_set) f = setsum (max 0 \ f) S / card S" ``` Andreas@60068 ` 1529` ```apply(subst nn_integral_max_0[symmetric]) ``` Andreas@60068 ` 1530` ```apply(subst nn_integral_pmf_of_set') ``` Andreas@60068 ` 1531` ```apply simp_all ``` Andreas@60068 ` 1532` ```done ``` Andreas@60068 ` 1533` Andreas@60068 ` 1534` ```lemma integral_pmf_of_set: ``` Andreas@60068 ` 1535` ``` "integral\<^sup>L (measure_pmf pmf_of_set) f = setsum f S / card S" ``` Andreas@60068 ` 1536` ```apply(simp add: real_lebesgue_integral_def integrable_measure_pmf_finite nn_integral_pmf_of_set S_finite) ``` Andreas@60068 ` 1537` ```apply(subst real_of_ereal_minus') ``` Andreas@60068 ` 1538` ``` apply(simp add: ereal_max_0 S_finite del: ereal_max) ``` Andreas@60068 ` 1539` ```apply(simp add: ereal_max_0 S_finite S_not_empty del: ereal_max) ``` Andreas@60068 ` 1540` ```apply(simp add: field_simps S_finite S_not_empty) ``` Andreas@60068 ` 1541` ```apply(subst setsum.distrib[symmetric]) ``` Andreas@60068 ` 1542` ```apply(rule setsum.cong; simp_all) ``` Andreas@60068 ` 1543` ```done ``` Andreas@60068 ` 1544` Andreas@61634 ` 1545` ```lemma emeasure_pmf_of_set: ``` Andreas@61634 ` 1546` ``` "emeasure (measure_pmf pmf_of_set) A = card (S \ A) / card S" ``` Andreas@61634 ` 1547` ```apply(subst nn_integral_indicator[symmetric], simp) ``` Andreas@61634 ` 1548` ```apply(subst nn_integral_pmf_of_set) ``` Andreas@61634 ` 1549` ```apply(simp add: o_def max_def ereal_indicator[symmetric] S_not_empty S_finite real_of_nat_indicator[symmetric] of_nat_setsum[symmetric] setsum_indicator_eq_card del: of_nat_setsum) ``` Andreas@61634 ` 1550` ```done ``` Andreas@61634 ` 1551` hoelzl@59000 ` 1552` ```end ``` hoelzl@59000 ` 1553` Andreas@60068 ` 1554` ```lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x" ``` Andreas@60068 ` 1555` ```by(rule pmf_eqI)(simp add: indicator_def) ``` Andreas@60068 ` 1556` lp15@61609 ` 1557` ```lemma map_pmf_of_set_inj: ``` Andreas@60068 ` 1558` ``` assumes f: "inj_on f A" ``` Andreas@60068 ` 1559` ``` and [simp]: "A \ {}" "finite A" ``` Andreas@60068 ` 1560` ``` shows "map_pmf f (pmf_of_set A) = pmf_of_set (f ` A)" (is "?lhs = ?rhs") ``` Andreas@60068 ` 1561` ```proof(rule pmf_eqI) ``` Andreas@60068 ` 1562` ``` fix i ``` Andreas@60068 ` 1563` ``` show "pmf ?lhs i = pmf ?rhs i" ``` Andreas@60068 ` 1564` ``` proof(cases "i \ f ` A") ``` Andreas@60068 ` 1565` ``` case True ``` Andreas@60068 ` 1566` ``` then obtain i' where "i = f i'" "i' \ A" by auto ``` Andreas@60068 ` 1567` ``` thus ?thesis using f by(simp add: card_image pmf_map_inj) ``` Andreas@60068 ` 1568` ``` next ``` Andreas@60068 ` 1569` ``` case False ``` Andreas@60068 ` 1570` ``` hence "pmf ?lhs i = 0" by(simp add: pmf_eq_0_set_pmf set_map_pmf) ``` Andreas@60068 ` 1571` ``` moreover have "pmf ?rhs i = 0" using False by simp ``` Andreas@60068 ` 1572` ``` ultimately show ?thesis by simp ``` Andreas@60068 ` 1573` ``` qed ``` Andreas@60068 ` 1574` ```qed ``` Andreas@60068 ` 1575` Andreas@60068 ` 1576` ```lemma bernoulli_pmf_half_conv_pmf_of_set: "bernoulli_pmf (1 / 2) = pmf_of_set UNIV" ``` Andreas@60068 ` 1577` ```by(rule pmf_eqI) simp_all ``` Andreas@60068 ` 1578` Andreas@61634 ` 1579` Andreas@61634 ` 1580` Andreas@61634 ` 1581` ```lemma measure_pmf_of_set: ``` Andreas@61634 ` 1582` ``` assumes "S \ {}" "finite S" ``` Andreas@61634 ` 1583` ``` shows "measure (measure_pmf (pmf_of_set S)) A = card (S \ A) / card S" ``` Andreas@61634 ` 1584` ```using emeasure_pmf_of_set[OF assms, of A] ``` Andreas@61634 ` 1585` ```unfolding measure_pmf.emeasure_eq_measure by simp ``` Andreas@61634 ` 1586` hoelzl@59093 ` 1587` ```subsubsection \ Poisson Distribution \ ``` hoelzl@59093 ` 1588` hoelzl@59093 ` 1589` ```context ``` hoelzl@59093 ` 1590` ``` fixes rate :: real assumes rate_pos: "0 < rate" ``` hoelzl@59093 ` 1591` ```begin ``` hoelzl@59093 ` 1592` hoelzl@59093 ` 1593` ```lift_definition poisson_pmf :: "nat pmf" is "\k. rate ^ k / fact k * exp (-rate)" ``` lp15@59730 ` 1594` ```proof (* by Manuel Eberl *) ``` hoelzl@59093 ` 1595` ``` have summable: "summable (\x::nat. rate ^ x / fact x)" using summable_exp ``` haftmann@59557 ` 1596` ``` by (simp add: field_simps divide_inverse [symmetric]) ``` hoelzl@59093 ` 1597` ``` have "(\\<^sup>+(x::nat). rate ^ x / fact x * exp (-rate) \count_space UNIV) = ``` hoelzl@59093 ` 1598` ``` exp (-rate) * (\\<^sup>+(x::nat). rate ^ x / fact x \count_space UNIV)" ``` hoelzl@59093 ` 1599` ``` by (simp add: field_simps nn_integral_cmult[symmetric]) ``` hoelzl@59093 ` 1600` ``` also from rate_pos have "(\\<^sup>+(x::nat). rate ^ x / fact x \count_space UNIV) = (\x. rate ^ x / fact x)" ``` hoelzl@59093 ` 1601` ``` by (simp_all add: nn_integral_count_space_nat suminf_ereal summable suminf_ereal_finite) ``` hoelzl@59093 ` 1602` ``` also have "... = exp rate" unfolding exp_def ``` lp15@59730 ` 1603` ``` by (simp add: field_simps divide_inverse [symmetric]) ``` hoelzl@59093 ` 1604` ``` also have "ereal (exp (-rate)) * ereal (exp rate) = 1" ``` hoelzl@59093 ` 1605` ``` by (simp add: mult_exp_exp) ``` lp15@59730 ` 1606` ``` finally show "(\\<^sup>+ x. ereal (rate ^ x / (fact x) * exp (- rate)) \count_space UNIV) = 1" . ``` hoelzl@59093 ` 1607` ```qed (simp add: rate_pos[THEN less_imp_le]) ``` hoelzl@59093 ` 1608` hoelzl@59093 ` 1609` ```lemma pmf_poisson[simp]: "pmf poisson_pmf k = rate ^ k / fact k * exp (-rate)" ``` hoelzl@59093 ` 1610` ``` by transfer rule ``` hoelzl@59093 ` 1611` hoelzl@59093 ` 1612` ```lemma set_pmf_poisson[simp]: "set_pmf poisson_pmf = UNIV" ``` hoelzl@59093 ` 1613` ``` using rate_pos by (auto simp: set_pmf_iff) ``` hoelzl@59093 ` 1614` hoelzl@59000 ` 1615` ```end ``` hoelzl@59000 ` 1616` hoelzl@59093 ` 1617` ```subsubsection \ Binomial Distribution \ ``` hoelzl@59093 ` 1618` hoelzl@59093 ` 1619` ```context ``` hoelzl@59093 ` 1620` ``` fixes n :: nat and p :: real assumes p_nonneg: "0 \ p" and p_le_1: "p \ 1" ``` hoelzl@59093 ` 1621` ```begin ``` hoelzl@59093 ` 1622` hoelzl@59093 ` 1623` ```lift_definition binomial_pmf :: "nat pmf" is "\k. (n choose k) * p^k * (1 - p)^(n - k)" ``` hoelzl@59093 ` 1624` ```proof ``` hoelzl@59093 ` 1625` ``` have "(\\<^sup>+k. ereal (real (n choose k) * p ^ k * (1 - p) ^ (n - k)) \count_space UNIV) = ``` hoelzl@59093 ` 1626` ``` ereal (\k\n. real (n choose k) * p ^ k * (1 - p) ^ (n - k))" ``` hoelzl@59093 ` 1627` ``` using p_le_1 p_nonneg by (subst nn_integral_count_space') auto ``` hoelzl@59093 ` 1628` ``` also have "(\k\n. real (n choose k) * p ^ k * (1 - p) ^ (n - k)) = (p + (1 - p)) ^ n" ``` lp15@61609 ` 1629` ``` by (subst binomial_ring) (simp add: atLeast0AtMost) ``` hoelzl@59093 ` 1630` ``` finally show "(\\<^sup>+ x. ereal (real (n choose x) * p ^ x * (1 - p) ^ (n - x)) \count_space UNIV) = 1" ``` hoelzl@59093 ` 1631` ``` by simp ``` hoelzl@59093 ` 1632` ```qed (insert p_nonneg p_le_1, simp) ``` hoelzl@59093 ` 1633` hoelzl@59093 ` 1634` ```lemma pmf_binomial[simp]: "pmf binomial_pmf k = (n choose k) * p^k * (1 - p)^(n - k)" ``` hoelzl@59093 ` 1635` ``` by transfer rule ``` hoelzl@59093 ` 1636` hoelzl@59093 ` 1637` ```lemma set_pmf_binomial_eq: "set_pmf binomial_pmf = (if p = 0 then {0} else if p = 1 then {n} else {.. n})" ``` hoelzl@59093 ` 1638` ``` using p_nonneg p_le_1 unfolding set_eq_iff set_pmf_iff pmf_binomial by (auto simp: set_pmf_iff) ``` hoelzl@59093 ` 1639` hoelzl@59093 ` 1640` ```end ``` hoelzl@59093 ` 1641` hoelzl@59093 ` 1642` ```end ``` hoelzl@59093 ` 1643` hoelzl@59093 ` 1644` ```lemma set_pmf_binomial_0[simp]: "set_pmf (binomial_pmf n 0) = {0}" ``` hoelzl@59093 ` 1645` ``` by (simp add: set_pmf_binomial_eq) ``` hoelzl@59093 ` 1646` hoelzl@59093 ` 1647` ```lemma set_pmf_binomial_1[simp]: "set_pmf (binomial_pmf n 1) = {n}" ``` hoelzl@59093 ` 1648` ``` by (simp add: set_pmf_binomial_eq) ``` hoelzl@59093 ` 1649` hoelzl@59093 ` 1650` ```lemma set_pmf_binomial[simp]: "0 < p \ p < 1 \ set_pmf (binomial_pmf n p) = {..n}" ``` hoelzl@59093 ` 1651` ``` by (simp add: set_pmf_binomial_eq) ``` hoelzl@59093 ` 1652` Andreas@61634 ` 1653` ```context begin interpretation lifting_syntax . ``` Andreas@61634 ` 1654` Andreas@61634 ` 1655` ```lemma bind_pmf_parametric [transfer_rule]: ``` Andreas@61634 ` 1656` ``` "(rel_pmf A ===> (A ===> rel_pmf B) ===> rel_pmf B) bind_pmf bind_pmf" ``` Andreas@61634 ` 1657` ```by(blast intro: rel_pmf_bindI dest: rel_funD) ``` Andreas@61634 ` 1658` Andreas@61634 ` 1659` ```lemma return_pmf_parametric [transfer_rule]: "(A ===> rel_pmf A) return_pmf return_pmf" ``` Andreas@61634 ` 1660` ```by(rule rel_funI) simp ``` Andreas@61634 ` 1661` hoelzl@59000 ` 1662` ```end ``` Andreas@61634 ` 1663` Andreas@61634 ` 1664` ```end ```