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