add cond_map_pmf
authorhoelzl
Tue Feb 10 12:15:05 2015 +0100 (2015-02-10)
changeset 59494054f9c9d73ea
parent 59493 e088f1b2f2fc
child 59495 03944a830c4a
add cond_map_pmf
src/HOL/Probability/Probability_Mass_Function.thy
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 10 12:09:32 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 10 12:15:05 2015 +0100
     1.3 @@ -12,6 +12,9 @@
     1.4    "~~/src/HOL/Library/Multiset"
     1.5  begin
     1.6  
     1.7 +lemma ereal_divide': "b \<noteq> 0 \<Longrightarrow> ereal (a / b) = ereal a / ereal b"
     1.8 +  using ereal_divide[of a b] by simp
     1.9 +
    1.10  lemma (in finite_measure) countable_support:
    1.11    "countable {x. measure M {x} \<noteq> 0}"
    1.12  proof cases
    1.13 @@ -1032,6 +1035,29 @@
    1.14  
    1.15  end
    1.16  
    1.17 +lemma cond_map_pmf:
    1.18 +  assumes "set_pmf p \<inter> f -` s \<noteq> {}"
    1.19 +  shows "cond_pmf (map_pmf f p) s = map_pmf f (cond_pmf p (f -` s))"
    1.20 +proof -
    1.21 +  have *: "set_pmf (map_pmf f p) \<inter> s \<noteq> {}"
    1.22 +    using assms by (simp add: set_map_pmf) auto
    1.23 +  { fix x
    1.24 +    have "ereal (pmf (map_pmf f (cond_pmf p (f -` s))) x) =
    1.25 +      emeasure p (f -` s \<inter> f -` {x}) / emeasure p (f -` s)"
    1.26 +      unfolding ereal_pmf_map cond_pmf.rep_eq[OF assms] by (simp add: nn_integral_uniform_measure)
    1.27 +    also have "f -` s \<inter> f -` {x} = (if x \<in> s then f -` {x} else {})"
    1.28 +      by auto
    1.29 +    also have "emeasure p (if x \<in> s then f -` {x} else {}) / emeasure p (f -` s) =
    1.30 +      ereal (pmf (cond_pmf (map_pmf f p) s) x)"
    1.31 +      using measure_measure_pmf_not_zero[OF *]
    1.32 +      by (simp add: pmf_cond[OF *] ereal_divide' ereal_pmf_map measure_pmf.emeasure_eq_measure[symmetric]
    1.33 +               del: ereal_divide)
    1.34 +    finally have "ereal (pmf (cond_pmf (map_pmf f p) s) x) = ereal (pmf (map_pmf f (cond_pmf p (f -` s))) x)"
    1.35 +      by simp }
    1.36 +  then show ?thesis
    1.37 +    by (intro pmf_eqI) simp
    1.38 +qed
    1.39 +
    1.40  inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool"
    1.41  for R p q
    1.42  where