add bind_cond_pmf_cancel
authorhoelzl
Tue Feb 10 13:50:30 2015 +0100 (2015-02-10)
changeset 5949503944a830c4a
parent 59494 054f9c9d73ea
child 59496 6faf024a1893
add bind_cond_pmf_cancel
src/HOL/Probability/Probability_Mass_Function.thy
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 10 12:15:05 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 10 13:50:30 2015 +0100
     1.3 @@ -1058,6 +1058,32 @@
     1.4      by (intro pmf_eqI) simp
     1.5  qed
     1.6  
     1.7 +lemma bind_cond_pmf_cancel:
     1.8 +  assumes in_S: "\<And>x. x \<in> set_pmf p \<Longrightarrow> x \<in> S x"
     1.9 +  assumes S_eq: "\<And>x y. x \<in> S y \<Longrightarrow> S x = S y"
    1.10 +  shows "bind_pmf p (\<lambda>x. cond_pmf p (S x)) = p"
    1.11 +proof (rule pmf_eqI)
    1.12 +  have [simp]: "\<And>x. x \<in> p \<Longrightarrow> p \<inter> (S x) \<noteq> {}"
    1.13 +    using in_S by auto
    1.14 +  fix z
    1.15 +  have pmf_le: "pmf p z \<le> measure p (S z)"
    1.16 +  proof cases
    1.17 +    assume "z \<in> p" from in_S[OF this] show ?thesis
    1.18 +      by (auto intro!: measure_pmf.finite_measure_mono simp: pmf.rep_eq)
    1.19 +  qed (simp add: set_pmf_iff measure_nonneg)
    1.20 +
    1.21 +  have "ereal (pmf (bind_pmf p (\<lambda>x. cond_pmf p (S x))) z) =
    1.22 +    (\<integral>\<^sup>+ x. ereal (pmf p z / measure p (S z)) * indicator (S z) x \<partial>p)"
    1.23 +    by (subst ereal_pmf_bind)
    1.24 +       (auto intro!: nn_integral_cong_AE dest!: S_eq split: split_indicator
    1.25 +             simp: AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf in_S)
    1.26 +  also have "\<dots> = pmf p z"
    1.27 +    using pmf_le pmf_nonneg[of p z]
    1.28 +    by (subst nn_integral_cmult) (simp_all add: measure_nonneg measure_pmf.emeasure_eq_measure)
    1.29 +  finally show "pmf (bind_pmf p (\<lambda>x. cond_pmf p (S x))) z = pmf p z"
    1.30 +    by simp
    1.31 +qed
    1.32 +
    1.33  inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool"
    1.34  for R p q
    1.35  where
    1.36 @@ -1114,28 +1140,10 @@
    1.37        with pq qr show "(R OO S) x z"
    1.38          by blast
    1.39      next
    1.40 -      { fix z
    1.41 -        have "ereal (pmf (map_pmf snd pr) z) =
    1.42 -            (\<integral>\<^sup>+y. \<integral>\<^sup>+x. indicator (snd -` {z}) x \<partial>cond_pmf qr {(y', z). y' = y} \<partial>q)"
    1.43 -          by (simp add: q pr_def map_bind_pmf split_beta map_return_pmf bind_return_pmf'' bind_map_pmf
    1.44 -                   ereal_pmf_bind ereal_pmf_map)
    1.45 -        also have "\<dots> = (\<integral>\<^sup>+y. \<integral>\<^sup>+x. indicator (snd -` {z}) x \<partial>uniform_measure qr {(y', z). y' = y} \<partial>q)"
    1.46 -          by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff cond_pmf.rep_eq pr_welldefined
    1.47 -                   simp del: emeasure_uniform_measure)
    1.48 -        also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. indicator {(y, z)} x \<partial>qr) / emeasure q {y} \<partial>q)"
    1.49 -          by (auto simp: nn_integral_uniform_measure q' simp del: nn_integral_indicator split: split_indicator
    1.50 -                   intro!: nn_integral_cong arg_cong2[where f="op /"] arg_cong2[where f=emeasure])
    1.51 -        also have "\<dots> = (\<integral>\<^sup>+y. pmf qr (y, z) \<partial>count_space UNIV)"
    1.52 -          by (subst measure_pmf_eq_density)
    1.53 -             (force simp: q' emeasure_pmf_single nn_integral_density pmf_nonneg pmf_eq_0_set_pmf set_map_pmf
    1.54 -                    intro!: nn_integral_cong split: split_indicator)
    1.55 -        also have "\<dots> = ereal (pmf r z)"
    1.56 -          by (subst nn_integral_pmf')
    1.57 -             (auto simp add: inj_on_def r ereal_pmf_map intro!: arg_cong2[where f=emeasure])
    1.58 -        finally have "pmf (map_pmf snd pr) z = pmf r z"
    1.59 -          by simp }
    1.60 +      have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {(y', z). y' = y}))"
    1.61 +        by (simp add: pr_def q split_beta bind_map_pmf bind_return_pmf'' map_bind_pmf map_return_pmf)
    1.62        then show "map_pmf snd pr = r"
    1.63 -        by (rule pmf_eqI)
    1.64 +        unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) auto
    1.65      qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf bind_return_pmf'' p) }
    1.66    then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
    1.67      by(auto simp add: le_fun_def)