--- a/src/HOL/Probability/Probability_Mass_Function.thy Tue Feb 10 16:08:11 2015 +0000
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Feb 10 16:09:30 2015 +0000
@@ -12,6 +12,9 @@
"~~/src/HOL/Library/Multiset"
begin
+lemma ereal_divide': "b \<noteq> 0 \<Longrightarrow> ereal (a / b) = ereal a / ereal b"
+ using ereal_divide[of a b] by simp
+
lemma (in finite_measure) countable_support:
"countable {x. measure M {x} \<noteq> 0}"
proof cases
@@ -688,6 +691,11 @@
by (intro subprob_space.measure_bind[where N="count_space UNIV", OF N]) auto
qed (auto simp: Transfer.Rel_def rel_fun_def cr_pmf_def)
+lemma ereal_pmf_join: "ereal (pmf (join_pmf N) i) = (\<integral>\<^sup>+M. pmf M i \<partial>measure_pmf N)"
+ unfolding pmf_join
+ by (intro nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1])
+ (auto simp: pmf_le_1 pmf_nonneg)
+
lemma set_pmf_join_pmf: "set_pmf (join_pmf f) = (\<Union>p\<in>set_pmf f. set_pmf p)"
apply(simp add: set_eq_iff set_pmf_iff pmf_join)
apply(subst integral_nonneg_eq_0_iff_AE)
@@ -735,6 +743,9 @@
unfolding f by (subst bind_distr[OF _ measurable_measure_pmf]) auto
qed
+lemma ereal_pmf_bind: "pmf (bind_pmf N f) i = (\<integral>\<^sup>+x. pmf (f x) i \<partial>measure_pmf N)"
+ by (auto intro!: nn_integral_distr simp: bind_pmf_def ereal_pmf_join map_pmf.rep_eq)
+
lemma pmf_bind: "pmf (bind_pmf N f) i = (\<integral>x. pmf (f x) i \<partial>measure_pmf N)"
by (auto intro!: integral_distr simp: bind_pmf_def pmf_join map_pmf.rep_eq)
@@ -857,6 +868,12 @@
end
+lemma map_bind_pmf: "map_pmf f (bind_pmf M g) = bind_pmf M (\<lambda>x. map_pmf f (g x))"
+ unfolding bind_return_pmf''[symmetric] bind_assoc_pmf[of M] ..
+
+lemma bind_map_pmf: "bind_pmf (map_pmf f M) g = bind_pmf M (\<lambda>x. g (f x))"
+ unfolding bind_return_pmf''[symmetric] bind_assoc_pmf bind_return_pmf ..
+
lemma map_join_pmf: "map_pmf f (join_pmf AA) = join_pmf (map_pmf (map_pmf f) AA)"
unfolding bind_pmf_def[symmetric]
unfolding bind_return_pmf''[symmetric] join_eq_bind_pmf bind_assoc_pmf
@@ -982,6 +999,94 @@
by (auto simp: pmf.rep_eq map_pmf.rep_eq measure_distr AE_measure_pmf_iff inj_onD
intro!: measure_pmf.finite_measure_eq_AE)
+subsection \<open> Conditional Probabilities \<close>
+
+context
+ fixes p :: "'a pmf" and s :: "'a set"
+ assumes not_empty: "set_pmf p \<inter> s \<noteq> {}"
+begin
+
+interpretation pmf_as_measure .
+
+lemma emeasure_measure_pmf_not_zero: "emeasure (measure_pmf p) s \<noteq> 0"
+proof
+ assume "emeasure (measure_pmf p) s = 0"
+ then have "AE x in measure_pmf p. x \<notin> s"
+ by (rule AE_I[rotated]) auto
+ with not_empty show False
+ by (auto simp: AE_measure_pmf_iff)
+qed
+
+lemma measure_measure_pmf_not_zero: "measure (measure_pmf p) s \<noteq> 0"
+ using emeasure_measure_pmf_not_zero unfolding measure_pmf.emeasure_eq_measure by simp
+
+lift_definition cond_pmf :: "'a pmf" is
+ "uniform_measure (measure_pmf p) s"
+proof (intro conjI)
+ show "prob_space (uniform_measure (measure_pmf p) s)"
+ by (intro prob_space_uniform_measure) (auto simp: emeasure_measure_pmf_not_zero)
+ show "AE x in uniform_measure (measure_pmf p) s. measure (uniform_measure (measure_pmf p) s) {x} \<noteq> 0"
+ by (simp add: emeasure_measure_pmf_not_zero measure_measure_pmf_not_zero AE_uniform_measure
+ AE_measure_pmf_iff set_pmf.rep_eq)
+qed simp
+
+lemma pmf_cond: "pmf cond_pmf x = (if x \<in> s then pmf p x / measure p s else 0)"
+ by transfer (simp add: emeasure_measure_pmf_not_zero pmf.rep_eq)
+
+lemma set_cond_pmf: "set_pmf cond_pmf = set_pmf p \<inter> s"
+ by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: split_if_asm)
+
+end
+
+lemma cond_map_pmf:
+ assumes "set_pmf p \<inter> f -` s \<noteq> {}"
+ shows "cond_pmf (map_pmf f p) s = map_pmf f (cond_pmf p (f -` s))"
+proof -
+ have *: "set_pmf (map_pmf f p) \<inter> s \<noteq> {}"
+ using assms by (simp add: set_map_pmf) auto
+ { fix x
+ have "ereal (pmf (map_pmf f (cond_pmf p (f -` s))) x) =
+ emeasure p (f -` s \<inter> f -` {x}) / emeasure p (f -` s)"
+ unfolding ereal_pmf_map cond_pmf.rep_eq[OF assms] by (simp add: nn_integral_uniform_measure)
+ also have "f -` s \<inter> f -` {x} = (if x \<in> s then f -` {x} else {})"
+ by auto
+ also have "emeasure p (if x \<in> s then f -` {x} else {}) / emeasure p (f -` s) =
+ ereal (pmf (cond_pmf (map_pmf f p) s) x)"
+ using measure_measure_pmf_not_zero[OF *]
+ by (simp add: pmf_cond[OF *] ereal_divide' ereal_pmf_map measure_pmf.emeasure_eq_measure[symmetric]
+ del: ereal_divide)
+ finally have "ereal (pmf (cond_pmf (map_pmf f p) s) x) = ereal (pmf (map_pmf f (cond_pmf p (f -` s))) x)"
+ by simp }
+ then show ?thesis
+ by (intro pmf_eqI) simp
+qed
+
+lemma bind_cond_pmf_cancel:
+ assumes in_S: "\<And>x. x \<in> set_pmf p \<Longrightarrow> x \<in> S x"
+ assumes S_eq: "\<And>x y. x \<in> S y \<Longrightarrow> S x = S y"
+ shows "bind_pmf p (\<lambda>x. cond_pmf p (S x)) = p"
+proof (rule pmf_eqI)
+ have [simp]: "\<And>x. x \<in> p \<Longrightarrow> p \<inter> (S x) \<noteq> {}"
+ using in_S by auto
+ fix z
+ have pmf_le: "pmf p z \<le> measure p (S z)"
+ proof cases
+ assume "z \<in> p" from in_S[OF this] show ?thesis
+ by (auto intro!: measure_pmf.finite_measure_mono simp: pmf.rep_eq)
+ qed (simp add: set_pmf_iff measure_nonneg)
+
+ have "ereal (pmf (bind_pmf p (\<lambda>x. cond_pmf p (S x))) z) =
+ (\<integral>\<^sup>+ x. ereal (pmf p z / measure p (S z)) * indicator (S z) x \<partial>p)"
+ by (subst ereal_pmf_bind)
+ (auto intro!: nn_integral_cong_AE dest!: S_eq split: split_indicator
+ simp: AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf in_S)
+ also have "\<dots> = pmf p z"
+ using pmf_le pmf_nonneg[of p z]
+ by (subst nn_integral_cmult) (simp_all add: measure_nonneg measure_pmf.emeasure_eq_measure)
+ finally show "pmf (bind_pmf p (\<lambda>x. cond_pmf p (S x))) z = pmf p z"
+ by simp
+qed
+
inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool"
for R p q
where
@@ -1026,89 +1131,23 @@
from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
- note pmf_nonneg[intro, simp]
- let ?pq = "\<lambda>y x. pmf pq (x, y)"
- let ?qr = "\<lambda>y z. pmf qr (y, z)"
-
- have nn_integral_pp2: "\<And>y. (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) = pmf q y"
- by (simp add: nn_integral_pmf' inj_on_def q)
- (auto simp add: ereal_pmf_map intro!: arg_cong2[where f=emeasure])
- have nn_integral_rr1: "\<And>y. (\<integral>\<^sup>+ x. ?qr y x \<partial>count_space UNIV) = pmf q y"
- by (simp add: nn_integral_pmf' inj_on_def q')
- (auto simp add: ereal_pmf_map intro!: arg_cong2[where f=emeasure])
- have eq: "\<And>y. (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) = (\<integral>\<^sup>+ z. ?qr y z \<partial>count_space UNIV)"
- by(simp add: nn_integral_pp2 nn_integral_rr1)
-
- def assign \<equiv> "\<lambda>(z, x, y). ?pq y x * ?qr y z / pmf q y"
- have assign_nonneg [simp]: "\<And>z x y. 0 \<le> assign (z, x, y)" by(simp add: assign_def)
- have assign_eq_0_outside: "\<And>z x y. \<lbrakk> ?pq y x = 0 \<or> ?qr y z = 0 \<rbrakk> \<Longrightarrow> assign (z, x, y) = 0"
- by(auto simp add: assign_def)
- have nn_integral_assign1: "\<And>z y. (\<integral>\<^sup>+ x. assign (z, x, y) \<partial>count_space UNIV) = ?qr y z"
- proof -
- fix y z
- have "(\<integral>\<^sup>+ x. assign (z, x, y) \<partial>count_space UNIV) =
- (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) * (?qr y z / pmf q y)"
- by(simp add: assign_def nn_integral_multc times_ereal.simps(1)[symmetric] divide_real_def mult.assoc del: times_ereal.simps(1))
- also have "\<dots> = ?qr y z" by(auto simp add: image_iff q' pmf_eq_0_set_pmf set_map_pmf nn_integral_pp2)
- finally show "?thesis z y" .
- qed
- have nn_integral_assign2: "\<And>x y. (\<integral>\<^sup>+ z. assign (z, x, y) \<partial>count_space UNIV) = ?pq y x"
- proof -
- fix x y
- have "(\<integral>\<^sup>+ z. assign (z, x, y) \<partial>count_space UNIV) = (\<integral>\<^sup>+ z. ?qr y z \<partial>count_space UNIV) * (?pq y x / pmf q y)"
- 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))
- also have "\<dots> = ?pq y x" by(auto simp add: image_iff pmf_eq_0_set_pmf set_map_pmf q nn_integral_rr1)
- finally show "?thesis x y" .
- qed
-
- def pqr \<equiv> "embed_pmf assign"
- { fix z x y
- have "assign (z, x, y) = pmf pqr (z, x, y)"
- unfolding pqr_def
- proof (subst pmf_embed_pmf)
- have "(\<integral>\<^sup>+ zxy. ereal (assign zxy) \<partial>count_space UNIV) =
- (\<integral>\<^sup>+ xy. \<integral>\<^sup>+ z. ereal (assign (z, xy)) \<partial>count_space UNIV \<partial>count_space UNIV)"
- by(subst nn_integral_snd_count_space) simp
- also have "\<dots> = (\<integral>\<^sup>+ z. ?pq (snd z) (fst z) \<partial>count_space UNIV)"
- by (subst nn_integral_assign2[symmetric]) (auto intro!: nn_integral_cong)
- finally show "(\<integral>\<^sup>+ zxy. ereal (assign zxy) \<partial>count_space UNIV) = 1"
- by (simp add: nn_integral_pmf emeasure_pmf)
- qed auto }
- note a = this
-
- def pr \<equiv> "map_pmf (\<lambda>(z, x, y). (x, z)) pqr"
+ 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)))"
+ have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {(y', z). y' = y} \<noteq> {}"
+ by (force simp: q' set_map_pmf)
have "rel_pmf (R OO S) p r"
- proof
- have pq_eq: "pq = map_pmf (\<lambda>(z, x, y). (x, y)) pqr"
- proof (rule pmf_eqI)
- fix i
- show "pmf pq i = pmf (map_pmf (\<lambda>(z, x, y). (x, y)) pqr) i"
- using nn_integral_assign2[of "fst i" "snd i", symmetric]
- by(cases i)
- (auto simp add: a nn_integral_pmf' inj_on_def ereal.inject[symmetric] ereal_pmf_map
- simp del: ereal.inject intro!: arg_cong2[where f=emeasure])
- qed
- then show "map_pmf fst pr = p"
- unfolding p pr_def by (simp add: map_pmf_comp split_beta)
-
- have qr_eq: "qr = map_pmf (\<lambda>(z, x, y). (y, z)) pqr"
- proof (rule pmf_eqI)
- fix i show "pmf qr i = pmf (map_pmf (\<lambda>(z, x, y). (y, z)) pqr) i"
- using nn_integral_assign1[of "snd i" "fst i", symmetric]
- by(cases i)
- (auto simp add: a nn_integral_pmf' inj_on_def ereal.inject[symmetric] ereal_pmf_map
- simp del: ereal.inject intro!: arg_cong2[where f=emeasure])
- qed
- then show "map_pmf snd pr = r"
- unfolding r pr_def by (simp add: map_pmf_comp split_beta)
-
- fix x z assume "(x, z) \<in> set_pmf pr"
- then have "\<exists>y. (x, y) \<in> set_pmf pq \<and> (y, z) \<in> set_pmf qr"
- unfolding pr_def pq_eq qr_eq by (force simp: set_map_pmf)
+ proof (rule rel_pmf.intros)
+ fix x z assume "(x, z) \<in> pr"
+ then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr"
+ by (auto simp: q pr_welldefined pr_def set_bind_pmf split_beta set_return_pmf set_cond_pmf set_map_pmf)
with pq qr show "(R OO S) x z"
by blast
- qed }
+ next
+ have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {(y', z). y' = y}))"
+ by (simp add: pr_def q split_beta bind_map_pmf bind_return_pmf'' map_bind_pmf map_return_pmf)
+ then show "map_pmf snd pr = r"
+ unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) auto
+ qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf bind_return_pmf'' p) }
then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
by(auto simp add: le_fun_def)
qed (fact natLeq_card_order natLeq_cinfinite)+