977 |
991 |
978 lemma pmf_map_inj: "inj_on f (set_pmf M) \<Longrightarrow> x \<in> set_pmf M \<Longrightarrow> pmf (map_pmf f M) (f x) = pmf M x" |
992 lemma pmf_map_inj: "inj_on f (set_pmf M) \<Longrightarrow> x \<in> set_pmf M \<Longrightarrow> pmf (map_pmf f M) (f x) = pmf M x" |
979 by (auto simp: pmf.rep_eq map_pmf.rep_eq measure_distr AE_measure_pmf_iff inj_onD |
993 by (auto simp: pmf.rep_eq map_pmf.rep_eq measure_distr AE_measure_pmf_iff inj_onD |
980 intro!: measure_pmf.finite_measure_eq_AE) |
994 intro!: measure_pmf.finite_measure_eq_AE) |
981 |
995 |
|
996 subsection \<open> Conditional Probabilities \<close> |
|
997 |
|
998 context |
|
999 fixes p :: "'a pmf" and s :: "'a set" |
|
1000 assumes not_empty: "set_pmf p \<inter> s \<noteq> {}" |
|
1001 begin |
|
1002 |
|
1003 interpretation pmf_as_measure . |
|
1004 |
|
1005 lemma emeasure_measure_pmf_not_zero: "emeasure (measure_pmf p) s \<noteq> 0" |
|
1006 proof |
|
1007 assume "emeasure (measure_pmf p) s = 0" |
|
1008 then have "AE x in measure_pmf p. x \<notin> s" |
|
1009 by (rule AE_I[rotated]) auto |
|
1010 with not_empty show False |
|
1011 by (auto simp: AE_measure_pmf_iff) |
|
1012 qed |
|
1013 |
|
1014 lemma measure_measure_pmf_not_zero: "measure (measure_pmf p) s \<noteq> 0" |
|
1015 using emeasure_measure_pmf_not_zero unfolding measure_pmf.emeasure_eq_measure by simp |
|
1016 |
|
1017 lift_definition cond_pmf :: "'a pmf" is |
|
1018 "uniform_measure (measure_pmf p) s" |
|
1019 proof (intro conjI) |
|
1020 show "prob_space (uniform_measure (measure_pmf p) s)" |
|
1021 by (intro prob_space_uniform_measure) (auto simp: emeasure_measure_pmf_not_zero) |
|
1022 show "AE x in uniform_measure (measure_pmf p) s. measure (uniform_measure (measure_pmf p) s) {x} \<noteq> 0" |
|
1023 by (simp add: emeasure_measure_pmf_not_zero measure_measure_pmf_not_zero AE_uniform_measure |
|
1024 AE_measure_pmf_iff set_pmf.rep_eq) |
|
1025 qed simp |
|
1026 |
|
1027 lemma pmf_cond: "pmf cond_pmf x = (if x \<in> s then pmf p x / measure p s else 0)" |
|
1028 by transfer (simp add: emeasure_measure_pmf_not_zero pmf.rep_eq) |
|
1029 |
|
1030 lemma set_cond_pmf: "set_pmf cond_pmf = set_pmf p \<inter> s" |
|
1031 by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: split_if_asm) |
|
1032 |
|
1033 end |
|
1034 |
982 inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool" |
1035 inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool" |
983 for R p q |
1036 for R p q |
984 where |
1037 where |
985 "\<lbrakk> \<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y; |
1038 "\<lbrakk> \<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y; |
986 map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk> |
1039 map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk> |
1021 from pq obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y" |
1074 from pq obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y" |
1022 and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto |
1075 and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto |
1023 from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z" |
1076 from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z" |
1024 and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto |
1077 and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto |
1025 |
1078 |
1026 note pmf_nonneg[intro, simp] |
1079 def pr \<equiv> "bind_pmf pq (\<lambda>(x, y). bind_pmf (cond_pmf qr {(y', z). y' = y}) (\<lambda>(y', z). return_pmf (x, z)))" |
1027 let ?pq = "\<lambda>y x. pmf pq (x, y)" |
1080 have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {(y', z). y' = y} \<noteq> {}" |
1028 let ?qr = "\<lambda>y z. pmf qr (y, z)" |
1081 by (force simp: q' set_map_pmf) |
1029 |
|
1030 have nn_integral_pp2: "\<And>y. (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) = pmf q y" |
|
1031 by (simp add: nn_integral_pmf' inj_on_def q) |
|
1032 (auto simp add: ereal_pmf_map intro!: arg_cong2[where f=emeasure]) |
|
1033 have nn_integral_rr1: "\<And>y. (\<integral>\<^sup>+ x. ?qr y x \<partial>count_space UNIV) = pmf q y" |
|
1034 by (simp add: nn_integral_pmf' inj_on_def q') |
|
1035 (auto simp add: ereal_pmf_map intro!: arg_cong2[where f=emeasure]) |
|
1036 have eq: "\<And>y. (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) = (\<integral>\<^sup>+ z. ?qr y z \<partial>count_space UNIV)" |
|
1037 by(simp add: nn_integral_pp2 nn_integral_rr1) |
|
1038 |
|
1039 def assign \<equiv> "\<lambda>y x z. ?pq y x * ?qr y z / pmf q y" |
|
1040 have assign_nonneg [simp]: "\<And>y x z. 0 \<le> assign y x z" by(simp add: assign_def) |
|
1041 have assign_eq_0_outside: "\<And>y x z. \<lbrakk> ?pq y x = 0 \<or> ?qr y z = 0 \<rbrakk> \<Longrightarrow> assign y x z = 0" |
|
1042 by(auto simp add: assign_def) |
|
1043 have nn_integral_assign1: "\<And>y z. (\<integral>\<^sup>+ x. assign y x z \<partial>count_space UNIV) = ?qr y z" |
|
1044 proof - |
|
1045 fix y z |
|
1046 have "(\<integral>\<^sup>+ x. assign y x z \<partial>count_space UNIV) = |
|
1047 (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) * (?qr y z / pmf q y)" |
|
1048 by(simp add: assign_def nn_integral_multc times_ereal.simps(1)[symmetric] divide_real_def mult.assoc del: times_ereal.simps(1)) |
|
1049 also have "\<dots> = ?qr y z" by(auto simp add: image_iff q' pmf_eq_0_set_pmf set_map_pmf nn_integral_pp2) |
|
1050 finally show "?thesis y z" . |
|
1051 qed |
|
1052 have nn_integral_assign2: "\<And>y x. (\<integral>\<^sup>+ z. assign y x z \<partial>count_space UNIV) = ?pq y x" |
|
1053 proof - |
|
1054 fix x y |
|
1055 have "(\<integral>\<^sup>+ z. assign y x z \<partial>count_space UNIV) = (\<integral>\<^sup>+ z. ?qr y z \<partial>count_space UNIV) * (?pq y x / pmf q y)" |
|
1056 by(simp add: assign_def divide_real_def mult.commute[where a="?pq y x"] mult.assoc nn_integral_multc times_ereal.simps(1)[symmetric] del: times_ereal.simps(1)) |
|
1057 also have "\<dots> = ?pq y x" by(auto simp add: image_iff pmf_eq_0_set_pmf set_map_pmf q nn_integral_rr1) |
|
1058 finally show "?thesis y x" . |
|
1059 qed |
|
1060 |
|
1061 def pqr \<equiv> "embed_pmf (\<lambda>(y, x, z). assign y x z)" |
|
1062 { fix y x z |
|
1063 have "assign y x z = pmf pqr (y, x, z)" |
|
1064 unfolding pqr_def |
|
1065 proof (subst pmf_embed_pmf) |
|
1066 have "(\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space UNIV) = |
|
1067 (\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>(count_space ((\<lambda>((x, y), z). (y, x, z)) ` (pq \<times> r))))" |
|
1068 by (force simp add: pmf_eq_0_set_pmf r set_map_pmf split: split_indicator |
|
1069 intro!: nn_integral_count_space_eq assign_eq_0_outside) |
|
1070 also have "\<dots> = (\<integral>\<^sup>+ x. ereal ((\<lambda>((x, y), z). assign y x z) x) \<partial>(count_space (pq \<times> r)))" |
|
1071 by (subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric]) |
|
1072 (auto simp: inj_on_def intro!: nn_integral_cong) |
|
1073 also have "\<dots> = (\<integral>\<^sup>+ xy. \<integral>\<^sup>+z. ereal ((\<lambda>((x, y), z). assign y x z) (xy, z)) \<partial>count_space r \<partial>count_space pq)" |
|
1074 by (subst sigma_finite_measure.nn_integral_fst) |
|
1075 (auto simp: pair_measure_countable sigma_finite_measure_count_space_countable) |
|
1076 also have "\<dots> = (\<integral>\<^sup>+ xy. \<integral>\<^sup>+z. ereal ((\<lambda>((x, y), z). assign y x z) (xy, z)) \<partial>count_space UNIV \<partial>count_space pq)" |
|
1077 by (intro nn_integral_cong nn_integral_count_space_eq) |
|
1078 (force simp: r set_map_pmf pmf_eq_0_set_pmf intro!: assign_eq_0_outside)+ |
|
1079 also have "\<dots> = (\<integral>\<^sup>+ z. ?pq (snd z) (fst z) \<partial>count_space pq)" |
|
1080 by (subst nn_integral_assign2[symmetric]) (auto intro!: nn_integral_cong) |
|
1081 finally show "(\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space UNIV) = 1" |
|
1082 by (simp add: nn_integral_pmf emeasure_pmf) |
|
1083 qed auto } |
|
1084 note a = this |
|
1085 |
|
1086 def pr \<equiv> "map_pmf (\<lambda>(y, x, z). (x, z)) pqr" |
|
1087 |
1082 |
1088 have "rel_pmf (R OO S) p r" |
1083 have "rel_pmf (R OO S) p r" |
1089 proof |
1084 proof (rule rel_pmf.intros) |
1090 have pq_eq: "pq = map_pmf (\<lambda>(y, x, z). (x, y)) pqr" |
1085 fix x z assume "(x, z) \<in> pr" |
1091 proof (rule pmf_eqI) |
1086 then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr" |
1092 fix i |
1087 by (auto simp: q pr_welldefined pr_def set_bind_pmf split_beta set_return_pmf set_cond_pmf set_map_pmf) |
1093 show "pmf pq i = pmf (map_pmf (\<lambda>(y, x, z). (x, y)) pqr) i" |
|
1094 using nn_integral_assign2[of "snd i" "fst i", symmetric] |
|
1095 by (auto simp add: a nn_integral_pmf' inj_on_def ereal.inject[symmetric] ereal_pmf_map |
|
1096 simp del: ereal.inject intro!: arg_cong2[where f=emeasure]) |
|
1097 qed |
|
1098 then show "map_pmf fst pr = p" |
|
1099 unfolding p pr_def by (simp add: map_pmf_comp split_beta) |
|
1100 |
|
1101 have qr_eq: "qr = map_pmf (\<lambda>(y, x, z). (y, z)) pqr" |
|
1102 proof (rule pmf_eqI) |
|
1103 fix i show "pmf qr i = pmf (map_pmf (\<lambda>(y, x, z). (y, z)) pqr) i" |
|
1104 using nn_integral_assign1[of "fst i" "snd i", symmetric] |
|
1105 by (auto simp add: a nn_integral_pmf' inj_on_def ereal.inject[symmetric] ereal_pmf_map |
|
1106 simp del: ereal.inject intro!: arg_cong2[where f=emeasure]) |
|
1107 qed |
|
1108 then show "map_pmf snd pr = r" |
|
1109 unfolding r pr_def by (simp add: map_pmf_comp split_beta) |
|
1110 |
|
1111 fix x z assume "(x, z) \<in> set_pmf pr" |
|
1112 then have "\<exists>y. (x, y) \<in> set_pmf pq \<and> (y, z) \<in> set_pmf qr" |
|
1113 unfolding pr_def pq_eq qr_eq by (force simp: set_map_pmf) |
|
1114 with pq qr show "(R OO S) x z" |
1088 with pq qr show "(R OO S) x z" |
1115 by blast |
1089 by blast |
1116 qed } |
1090 next |
|
1091 { fix z |
|
1092 have "ereal (pmf (map_pmf snd pr) z) = |
|
1093 (\<integral>\<^sup>+y. \<integral>\<^sup>+x. indicator (snd -` {z}) x \<partial>cond_pmf qr {(y', z). y' = y} \<partial>q)" |
|
1094 by (simp add: q pr_def map_bind_pmf split_beta map_return_pmf bind_return_pmf'' bind_map_pmf |
|
1095 ereal_pmf_bind ereal_pmf_map) |
|
1096 also have "\<dots> = (\<integral>\<^sup>+y. \<integral>\<^sup>+x. indicator (snd -` {z}) x \<partial>uniform_measure qr {(y', z). y' = y} \<partial>q)" |
|
1097 by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff cond_pmf.rep_eq pr_welldefined |
|
1098 simp del: emeasure_uniform_measure) |
|
1099 also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. indicator {(y, z)} x \<partial>qr) / emeasure q {y} \<partial>q)" |
|
1100 by (auto simp: nn_integral_uniform_measure q' simp del: nn_integral_indicator split: split_indicator |
|
1101 intro!: nn_integral_cong arg_cong2[where f="op /"] arg_cong2[where f=emeasure]) |
|
1102 also have "\<dots> = (\<integral>\<^sup>+y. pmf qr (y, z) \<partial>count_space UNIV)" |
|
1103 by (subst measure_pmf_eq_density) |
|
1104 (force simp: q' emeasure_pmf_single nn_integral_density pmf_nonneg pmf_eq_0_set_pmf set_map_pmf |
|
1105 intro!: nn_integral_cong split: split_indicator) |
|
1106 also have "\<dots> = ereal (pmf r z)" |
|
1107 by (subst nn_integral_pmf') |
|
1108 (auto simp add: inj_on_def r ereal_pmf_map intro!: arg_cong2[where f=emeasure]) |
|
1109 finally have "pmf (map_pmf snd pr) z = pmf r z" |
|
1110 by simp } |
|
1111 then show "map_pmf snd pr = r" |
|
1112 by (rule pmf_eqI) |
|
1113 qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf bind_return_pmf'' p) } |
1117 then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)" |
1114 then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)" |
1118 by(auto simp add: le_fun_def) |
1115 by(auto simp add: le_fun_def) |
1119 qed (fact natLeq_card_order natLeq_cinfinite)+ |
1116 qed (fact natLeq_card_order natLeq_cinfinite)+ |
1120 |
1117 |
1121 lemma rel_pmf_return_pmf1: "rel_pmf R (return_pmf x) M \<longleftrightarrow> (\<forall>a\<in>M. R x a)" |
1118 lemma rel_pmf_return_pmf1: "rel_pmf R (return_pmf x) M \<longleftrightarrow> (\<forall>a\<in>M. R x a)" |