1056 by simp } |
1056 by simp } |
1057 then show ?thesis |
1057 then show ?thesis |
1058 by (intro pmf_eqI) simp |
1058 by (intro pmf_eqI) simp |
1059 qed |
1059 qed |
1060 |
1060 |
|
1061 lemma bind_cond_pmf_cancel: |
|
1062 assumes in_S: "\<And>x. x \<in> set_pmf p \<Longrightarrow> x \<in> S x" |
|
1063 assumes S_eq: "\<And>x y. x \<in> S y \<Longrightarrow> S x = S y" |
|
1064 shows "bind_pmf p (\<lambda>x. cond_pmf p (S x)) = p" |
|
1065 proof (rule pmf_eqI) |
|
1066 have [simp]: "\<And>x. x \<in> p \<Longrightarrow> p \<inter> (S x) \<noteq> {}" |
|
1067 using in_S by auto |
|
1068 fix z |
|
1069 have pmf_le: "pmf p z \<le> measure p (S z)" |
|
1070 proof cases |
|
1071 assume "z \<in> p" from in_S[OF this] show ?thesis |
|
1072 by (auto intro!: measure_pmf.finite_measure_mono simp: pmf.rep_eq) |
|
1073 qed (simp add: set_pmf_iff measure_nonneg) |
|
1074 |
|
1075 have "ereal (pmf (bind_pmf p (\<lambda>x. cond_pmf p (S x))) z) = |
|
1076 (\<integral>\<^sup>+ x. ereal (pmf p z / measure p (S z)) * indicator (S z) x \<partial>p)" |
|
1077 by (subst ereal_pmf_bind) |
|
1078 (auto intro!: nn_integral_cong_AE dest!: S_eq split: split_indicator |
|
1079 simp: AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf in_S) |
|
1080 also have "\<dots> = pmf p z" |
|
1081 using pmf_le pmf_nonneg[of p z] |
|
1082 by (subst nn_integral_cmult) (simp_all add: measure_nonneg measure_pmf.emeasure_eq_measure) |
|
1083 finally show "pmf (bind_pmf p (\<lambda>x. cond_pmf p (S x))) z = pmf p z" |
|
1084 by simp |
|
1085 qed |
|
1086 |
1061 inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool" |
1087 inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool" |
1062 for R p q |
1088 for R p q |
1063 where |
1089 where |
1064 "\<lbrakk> \<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y; |
1090 "\<lbrakk> \<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y; |
1065 map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk> |
1091 map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk> |
1112 then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr" |
1138 then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr" |
1113 by (auto simp: q pr_welldefined pr_def set_bind_pmf split_beta set_return_pmf set_cond_pmf set_map_pmf) |
1139 by (auto simp: q pr_welldefined pr_def set_bind_pmf split_beta set_return_pmf set_cond_pmf set_map_pmf) |
1114 with pq qr show "(R OO S) x z" |
1140 with pq qr show "(R OO S) x z" |
1115 by blast |
1141 by blast |
1116 next |
1142 next |
1117 { fix z |
1143 have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {(y', z). y' = y}))" |
1118 have "ereal (pmf (map_pmf snd pr) z) = |
1144 by (simp add: pr_def q split_beta bind_map_pmf bind_return_pmf'' map_bind_pmf map_return_pmf) |
1119 (\<integral>\<^sup>+y. \<integral>\<^sup>+x. indicator (snd -` {z}) x \<partial>cond_pmf qr {(y', z). y' = y} \<partial>q)" |
|
1120 by (simp add: q pr_def map_bind_pmf split_beta map_return_pmf bind_return_pmf'' bind_map_pmf |
|
1121 ereal_pmf_bind ereal_pmf_map) |
|
1122 also have "\<dots> = (\<integral>\<^sup>+y. \<integral>\<^sup>+x. indicator (snd -` {z}) x \<partial>uniform_measure qr {(y', z). y' = y} \<partial>q)" |
|
1123 by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff cond_pmf.rep_eq pr_welldefined |
|
1124 simp del: emeasure_uniform_measure) |
|
1125 also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. indicator {(y, z)} x \<partial>qr) / emeasure q {y} \<partial>q)" |
|
1126 by (auto simp: nn_integral_uniform_measure q' simp del: nn_integral_indicator split: split_indicator |
|
1127 intro!: nn_integral_cong arg_cong2[where f="op /"] arg_cong2[where f=emeasure]) |
|
1128 also have "\<dots> = (\<integral>\<^sup>+y. pmf qr (y, z) \<partial>count_space UNIV)" |
|
1129 by (subst measure_pmf_eq_density) |
|
1130 (force simp: q' emeasure_pmf_single nn_integral_density pmf_nonneg pmf_eq_0_set_pmf set_map_pmf |
|
1131 intro!: nn_integral_cong split: split_indicator) |
|
1132 also have "\<dots> = ereal (pmf r z)" |
|
1133 by (subst nn_integral_pmf') |
|
1134 (auto simp add: inj_on_def r ereal_pmf_map intro!: arg_cong2[where f=emeasure]) |
|
1135 finally have "pmf (map_pmf snd pr) z = pmf r z" |
|
1136 by simp } |
|
1137 then show "map_pmf snd pr = r" |
1145 then show "map_pmf snd pr = r" |
1138 by (rule pmf_eqI) |
1146 unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) auto |
1139 qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf bind_return_pmf'' p) } |
1147 qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf bind_return_pmf'' p) } |
1140 then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)" |
1148 then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)" |
1141 by(auto simp add: le_fun_def) |
1149 by(auto simp add: le_fun_def) |
1142 qed (fact natLeq_card_order natLeq_cinfinite)+ |
1150 qed (fact natLeq_card_order natLeq_cinfinite)+ |
1143 |
1151 |