src/HOL/Probability/Probability_Mass_Function.thy
changeset 59493 e088f1b2f2fc
parent 59475 8300c4ddf493
child 59494 054f9c9d73ea
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Feb 06 17:57:03 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 10 12:09:32 2015 +0100
     1.3 @@ -685,6 +685,11 @@
     1.4      by (intro subprob_space.measure_bind[where N="count_space UNIV", OF N]) auto
     1.5  qed (auto simp: Transfer.Rel_def rel_fun_def cr_pmf_def)
     1.6  
     1.7 +lemma ereal_pmf_join: "ereal (pmf (join_pmf N) i) = (\<integral>\<^sup>+M. pmf M i \<partial>measure_pmf N)"
     1.8 +  unfolding pmf_join
     1.9 +  by (intro nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1])
    1.10 +     (auto simp: pmf_le_1 pmf_nonneg)
    1.11 +
    1.12  lemma set_pmf_join_pmf: "set_pmf (join_pmf f) = (\<Union>p\<in>set_pmf f. set_pmf p)"
    1.13  apply(simp add: set_eq_iff set_pmf_iff pmf_join)
    1.14  apply(subst integral_nonneg_eq_0_iff_AE)
    1.15 @@ -732,6 +737,9 @@
    1.16      unfolding f by (subst bind_distr[OF _ measurable_measure_pmf]) auto
    1.17  qed
    1.18  
    1.19 +lemma ereal_pmf_bind: "pmf (bind_pmf N f) i = (\<integral>\<^sup>+x. pmf (f x) i \<partial>measure_pmf N)"
    1.20 +  by (auto intro!: nn_integral_distr simp: bind_pmf_def ereal_pmf_join map_pmf.rep_eq)
    1.21 +
    1.22  lemma pmf_bind: "pmf (bind_pmf N f) i = (\<integral>x. pmf (f x) i \<partial>measure_pmf N)"
    1.23    by (auto intro!: integral_distr simp: bind_pmf_def pmf_join map_pmf.rep_eq)
    1.24  
    1.25 @@ -854,6 +862,12 @@
    1.26  
    1.27  end
    1.28  
    1.29 +lemma map_bind_pmf: "map_pmf f (bind_pmf M g) = bind_pmf M (\<lambda>x. map_pmf f (g x))"
    1.30 +  unfolding bind_return_pmf''[symmetric] bind_assoc_pmf[of M] ..
    1.31 +
    1.32 +lemma bind_map_pmf: "bind_pmf (map_pmf f M) g = bind_pmf M (\<lambda>x. g (f x))"
    1.33 +  unfolding bind_return_pmf''[symmetric] bind_assoc_pmf bind_return_pmf ..
    1.34 +
    1.35  lemma map_join_pmf: "map_pmf f (join_pmf AA) = join_pmf (map_pmf (map_pmf f) AA)"
    1.36    unfolding bind_pmf_def[symmetric]
    1.37    unfolding bind_return_pmf''[symmetric] join_eq_bind_pmf bind_assoc_pmf
    1.38 @@ -979,6 +993,45 @@
    1.39    by (auto simp: pmf.rep_eq map_pmf.rep_eq measure_distr AE_measure_pmf_iff inj_onD
    1.40             intro!: measure_pmf.finite_measure_eq_AE)
    1.41  
    1.42 +subsection \<open> Conditional Probabilities \<close>
    1.43 +
    1.44 +context
    1.45 +  fixes p :: "'a pmf" and s :: "'a set"
    1.46 +  assumes not_empty: "set_pmf p \<inter> s \<noteq> {}"
    1.47 +begin
    1.48 +
    1.49 +interpretation pmf_as_measure .
    1.50 +
    1.51 +lemma emeasure_measure_pmf_not_zero: "emeasure (measure_pmf p) s \<noteq> 0"
    1.52 +proof
    1.53 +  assume "emeasure (measure_pmf p) s = 0"
    1.54 +  then have "AE x in measure_pmf p. x \<notin> s"
    1.55 +    by (rule AE_I[rotated]) auto
    1.56 +  with not_empty show False
    1.57 +    by (auto simp: AE_measure_pmf_iff)
    1.58 +qed
    1.59 +
    1.60 +lemma measure_measure_pmf_not_zero: "measure (measure_pmf p) s \<noteq> 0"
    1.61 +  using emeasure_measure_pmf_not_zero unfolding measure_pmf.emeasure_eq_measure by simp
    1.62 +
    1.63 +lift_definition cond_pmf :: "'a pmf" is
    1.64 +  "uniform_measure (measure_pmf p) s"
    1.65 +proof (intro conjI)
    1.66 +  show "prob_space (uniform_measure (measure_pmf p) s)"
    1.67 +    by (intro prob_space_uniform_measure) (auto simp: emeasure_measure_pmf_not_zero)
    1.68 +  show "AE x in uniform_measure (measure_pmf p) s. measure (uniform_measure (measure_pmf p) s) {x} \<noteq> 0"
    1.69 +    by (simp add: emeasure_measure_pmf_not_zero measure_measure_pmf_not_zero AE_uniform_measure
    1.70 +                  AE_measure_pmf_iff set_pmf.rep_eq)
    1.71 +qed simp
    1.72 +
    1.73 +lemma pmf_cond: "pmf cond_pmf x = (if x \<in> s then pmf p x / measure p s else 0)"
    1.74 +  by transfer (simp add: emeasure_measure_pmf_not_zero pmf.rep_eq)
    1.75 +
    1.76 +lemma set_cond_pmf: "set_pmf cond_pmf = set_pmf p \<inter> s"
    1.77 +  by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: split_if_asm)
    1.78 +
    1.79 +end
    1.80 +
    1.81  inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool"
    1.82  for R p q
    1.83  where
    1.84 @@ -1023,97 +1076,41 @@
    1.85      from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
    1.86        and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
    1.87  
    1.88 -    note pmf_nonneg[intro, simp]
    1.89 -    let ?pq = "\<lambda>y x. pmf pq (x, y)"
    1.90 -    let ?qr = "\<lambda>y z. pmf qr (y, z)"
    1.91 -
    1.92 -    have nn_integral_pp2: "\<And>y. (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) = pmf q y"
    1.93 -      by (simp add: nn_integral_pmf' inj_on_def q)
    1.94 -         (auto simp add: ereal_pmf_map intro!: arg_cong2[where f=emeasure])
    1.95 -    have nn_integral_rr1: "\<And>y. (\<integral>\<^sup>+ x. ?qr y x \<partial>count_space UNIV) = pmf q y"
    1.96 -      by (simp add: nn_integral_pmf' inj_on_def q')
    1.97 -         (auto simp add: ereal_pmf_map intro!: arg_cong2[where f=emeasure])
    1.98 -    have eq: "\<And>y. (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) = (\<integral>\<^sup>+ z. ?qr y z \<partial>count_space UNIV)"
    1.99 -      by(simp add: nn_integral_pp2 nn_integral_rr1)
   1.100 -
   1.101 -    def assign \<equiv> "\<lambda>y x z. ?pq y x * ?qr y z / pmf q y"
   1.102 -    have assign_nonneg [simp]: "\<And>y x z. 0 \<le> assign y x z" by(simp add: assign_def)
   1.103 -    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"
   1.104 -      by(auto simp add: assign_def)
   1.105 -    have nn_integral_assign1: "\<And>y z. (\<integral>\<^sup>+ x. assign y x z \<partial>count_space UNIV) = ?qr y z"
   1.106 -    proof -
   1.107 -      fix y z
   1.108 -      have "(\<integral>\<^sup>+ x. assign y x z \<partial>count_space UNIV) = 
   1.109 -            (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) * (?qr y z / pmf q y)"
   1.110 -        by(simp add: assign_def nn_integral_multc times_ereal.simps(1)[symmetric] divide_real_def mult.assoc del: times_ereal.simps(1))
   1.111 -      also have "\<dots> = ?qr y z" by(auto simp add: image_iff q' pmf_eq_0_set_pmf set_map_pmf nn_integral_pp2)
   1.112 -      finally show "?thesis y z" .
   1.113 -    qed
   1.114 -    have nn_integral_assign2: "\<And>y x. (\<integral>\<^sup>+ z. assign y x z \<partial>count_space UNIV) = ?pq y x"
   1.115 -    proof -
   1.116 -      fix x y
   1.117 -      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)"
   1.118 -        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))
   1.119 -      also have "\<dots> = ?pq y x" by(auto simp add: image_iff pmf_eq_0_set_pmf set_map_pmf q nn_integral_rr1)
   1.120 -      finally show "?thesis y x" .
   1.121 -    qed
   1.122 -
   1.123 -    def pqr \<equiv> "embed_pmf (\<lambda>(y, x, z). assign y x z)"
   1.124 -    { fix y x z
   1.125 -      have "assign y x z = pmf pqr (y, x, z)"
   1.126 -        unfolding pqr_def
   1.127 -      proof (subst pmf_embed_pmf)
   1.128 -        have "(\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space UNIV) =
   1.129 -          (\<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))))"
   1.130 -          by (force simp add: pmf_eq_0_set_pmf r set_map_pmf split: split_indicator
   1.131 -                    intro!: nn_integral_count_space_eq assign_eq_0_outside)
   1.132 -        also have "\<dots> = (\<integral>\<^sup>+ x. ereal ((\<lambda>((x, y), z). assign y x z) x) \<partial>(count_space (pq \<times> r)))"
   1.133 -          by (subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric])
   1.134 -             (auto simp: inj_on_def intro!: nn_integral_cong)
   1.135 -        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)"
   1.136 -          by (subst sigma_finite_measure.nn_integral_fst)
   1.137 -             (auto simp: pair_measure_countable sigma_finite_measure_count_space_countable)
   1.138 -        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)"
   1.139 -          by (intro nn_integral_cong nn_integral_count_space_eq)
   1.140 -             (force simp: r set_map_pmf pmf_eq_0_set_pmf intro!: assign_eq_0_outside)+
   1.141 -        also have "\<dots> = (\<integral>\<^sup>+ z. ?pq (snd z) (fst z) \<partial>count_space pq)"
   1.142 -          by (subst nn_integral_assign2[symmetric]) (auto intro!: nn_integral_cong)
   1.143 -        finally show "(\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space UNIV) = 1"
   1.144 -          by (simp add: nn_integral_pmf emeasure_pmf)
   1.145 -      qed auto }
   1.146 -    note a = this
   1.147 -
   1.148 -    def pr \<equiv> "map_pmf (\<lambda>(y, x, z). (x, z)) pqr"
   1.149 +    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)))"
   1.150 +    have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {(y', z). y' = y} \<noteq> {}"
   1.151 +      by (force simp: q' set_map_pmf)
   1.152  
   1.153      have "rel_pmf (R OO S) p r"
   1.154 -    proof
   1.155 -      have pq_eq: "pq = map_pmf (\<lambda>(y, x, z). (x, y)) pqr"
   1.156 -      proof (rule pmf_eqI)
   1.157 -        fix i
   1.158 -        show "pmf pq i = pmf (map_pmf (\<lambda>(y, x, z). (x, y)) pqr) i"
   1.159 -          using nn_integral_assign2[of "snd i" "fst i", symmetric]
   1.160 -          by (auto simp add: a nn_integral_pmf' inj_on_def ereal.inject[symmetric] ereal_pmf_map 
   1.161 -                   simp del: ereal.inject intro!: arg_cong2[where f=emeasure])
   1.162 -      qed
   1.163 -      then show "map_pmf fst pr = p"
   1.164 -        unfolding p pr_def by (simp add: map_pmf_comp split_beta)
   1.165 -
   1.166 -      have qr_eq: "qr = map_pmf (\<lambda>(y, x, z). (y, z)) pqr"
   1.167 -      proof (rule pmf_eqI)
   1.168 -        fix i show "pmf qr i = pmf (map_pmf (\<lambda>(y, x, z). (y, z)) pqr) i"
   1.169 -          using nn_integral_assign1[of "fst i" "snd i", symmetric]
   1.170 -          by (auto simp add: a nn_integral_pmf' inj_on_def ereal.inject[symmetric] ereal_pmf_map 
   1.171 -                   simp del: ereal.inject intro!: arg_cong2[where f=emeasure])
   1.172 -      qed
   1.173 -      then show "map_pmf snd pr = r"
   1.174 -        unfolding r pr_def by (simp add: map_pmf_comp split_beta)
   1.175 -
   1.176 -      fix x z assume "(x, z) \<in> set_pmf pr"
   1.177 -      then have "\<exists>y. (x, y) \<in> set_pmf pq \<and> (y, z) \<in> set_pmf qr"
   1.178 -        unfolding pr_def pq_eq qr_eq by (force simp: set_map_pmf)
   1.179 +    proof (rule rel_pmf.intros)
   1.180 +      fix x z assume "(x, z) \<in> pr"
   1.181 +      then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr"
   1.182 +        by (auto simp: q pr_welldefined pr_def set_bind_pmf split_beta set_return_pmf set_cond_pmf set_map_pmf)
   1.183        with pq qr show "(R OO S) x z"
   1.184          by blast
   1.185 -    qed }
   1.186 +    next
   1.187 +      { fix z
   1.188 +        have "ereal (pmf (map_pmf snd pr) z) =
   1.189 +            (\<integral>\<^sup>+y. \<integral>\<^sup>+x. indicator (snd -` {z}) x \<partial>cond_pmf qr {(y', z). y' = y} \<partial>q)"
   1.190 +          by (simp add: q pr_def map_bind_pmf split_beta map_return_pmf bind_return_pmf'' bind_map_pmf
   1.191 +                   ereal_pmf_bind ereal_pmf_map)
   1.192 +        also have "\<dots> = (\<integral>\<^sup>+y. \<integral>\<^sup>+x. indicator (snd -` {z}) x \<partial>uniform_measure qr {(y', z). y' = y} \<partial>q)"
   1.193 +          by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff cond_pmf.rep_eq pr_welldefined
   1.194 +                   simp del: emeasure_uniform_measure)
   1.195 +        also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. indicator {(y, z)} x \<partial>qr) / emeasure q {y} \<partial>q)"
   1.196 +          by (auto simp: nn_integral_uniform_measure q' simp del: nn_integral_indicator split: split_indicator
   1.197 +                   intro!: nn_integral_cong arg_cong2[where f="op /"] arg_cong2[where f=emeasure])
   1.198 +        also have "\<dots> = (\<integral>\<^sup>+y. pmf qr (y, z) \<partial>count_space UNIV)"
   1.199 +          by (subst measure_pmf_eq_density)
   1.200 +             (force simp: q' emeasure_pmf_single nn_integral_density pmf_nonneg pmf_eq_0_set_pmf set_map_pmf
   1.201 +                    intro!: nn_integral_cong split: split_indicator)
   1.202 +        also have "\<dots> = ereal (pmf r z)"
   1.203 +          by (subst nn_integral_pmf')
   1.204 +             (auto simp add: inj_on_def r ereal_pmf_map intro!: arg_cong2[where f=emeasure])
   1.205 +        finally have "pmf (map_pmf snd pr) z = pmf r z"
   1.206 +          by simp }
   1.207 +      then show "map_pmf snd pr = r"
   1.208 +        by (rule pmf_eqI)
   1.209 +    qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf bind_return_pmf'' p) }
   1.210    then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
   1.211      by(auto simp add: le_fun_def)
   1.212  qed (fact natLeq_card_order natLeq_cinfinite)+