author hoelzl Tue Feb 10 12:15:05 2015 +0100 (2015-02-10) changeset 59494 054f9c9d73ea parent 59493 e088f1b2f2fc child 59495 03944a830c4a
add cond_map_pmf
```     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
```