src/HOL/Probability/Probability_Mass_Function.thy
 changeset 59134 a71f2e256ee2 parent 59093 2b106e58a177 child 59325 922d31f5c3f5
```     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Dec 11 14:14:39 2014 +0100
1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Dec 12 10:58:40 2014 +0100
1.3 @@ -883,6 +883,52 @@
1.4    "measure_pmf M \<in> space (subprob_algebra (count_space UNIV))"
1.5    by (simp add: space_subprob_algebra) intro_locales
1.6
1.7 +lemma nn_integral_pair_pmf': "(\<integral>\<^sup>+x. f x \<partial>pair_pmf A B) = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. f (a, b) \<partial>B \<partial>A)"
1.8 +proof -
1.9 +  have "(\<integral>\<^sup>+x. f x \<partial>pair_pmf A B) = (\<integral>\<^sup>+x. max 0 (f x) * indicator (A \<times> B) x \<partial>pair_pmf A B)"
1.10 +    by (subst nn_integral_max_0[symmetric])
1.11 +       (auto simp: AE_measure_pmf_iff set_pair_pmf intro!: nn_integral_cong_AE)
1.12 +  also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. max 0 (f (a, b)) * indicator (A \<times> B) (a, b) \<partial>B \<partial>A)"
1.13 +    by (simp add: pair_pmf_def)
1.14 +  also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. max 0 (f (a, b)) \<partial>B \<partial>A)"
1.15 +    by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff)
1.16 +  finally show ?thesis
1.17 +    unfolding nn_integral_max_0 .
1.18 +qed
1.19 +
1.20 +lemma pair_map_pmf1: "pair_pmf (map_pmf f A) B = map_pmf (apfst f) (pair_pmf A B)"
1.21 +proof (safe intro!: pmf_eqI)
1.22 +  fix a :: "'a" and b :: "'b"
1.23 +  have [simp]: "\<And>c d. indicator (apfst f -` {(a, b)}) (c, d) = indicator (f -` {a}) c * (indicator {b} d::ereal)"
1.24 +    by (auto split: split_indicator)
1.25 +
1.26 +  have "ereal (pmf (pair_pmf (map_pmf f A) B) (a, b)) =
1.27 +         ereal (pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b))"
1.28 +    unfolding pmf_pair ereal_pmf_map
1.29 +    by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_multc pmf_nonneg
1.30 +                  emeasure_map_pmf[symmetric] del: emeasure_map_pmf)
1.31 +  then show "pmf (pair_pmf (map_pmf f A) B) (a, b) = pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b)"
1.32 +    by simp
1.33 +qed
1.34 +
1.35 +lemma pair_map_pmf2: "pair_pmf A (map_pmf f B) = map_pmf (apsnd f) (pair_pmf A B)"
1.36 +proof (safe intro!: pmf_eqI)
1.37 +  fix a :: "'a" and b :: "'b"
1.38 +  have [simp]: "\<And>c d. indicator (apsnd f -` {(a, b)}) (c, d) = indicator {a} c * (indicator (f -` {b}) d::ereal)"
1.39 +    by (auto split: split_indicator)
1.40 +
1.41 +  have "ereal (pmf (pair_pmf A (map_pmf f B)) (a, b)) =
1.42 +         ereal (pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b))"
1.43 +    unfolding pmf_pair ereal_pmf_map
1.44 +    by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_cmult nn_integral_multc pmf_nonneg
1.45 +                  emeasure_map_pmf[symmetric] del: emeasure_map_pmf)
1.46 +  then show "pmf (pair_pmf A (map_pmf f B)) (a, b) = pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b)"
1.47 +    by simp
1.48 +qed
1.49 +
1.50 +lemma map_pair: "map_pmf (\<lambda>(a, b). (f a, g b)) (pair_pmf A B) = pair_pmf (map_pmf f A) (map_pmf g B)"
1.51 +  by (simp add: pair_map_pmf2 pair_map_pmf1 map_pmf_comp split_beta')
1.52 +
1.53  lemma bind_pair_pmf:
1.54    assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)"
1.55    shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))"
1.56 @@ -1384,5 +1430,82 @@
1.58  qed (fact natLeq_card_order natLeq_cinfinite)+
1.59
1.60 +lemma rel_pmf_return_pmf1: "rel_pmf R (return_pmf x) M \<longleftrightarrow> (\<forall>a\<in>M. R x a)"
1.61 +proof safe
1.62 +  fix a assume "a \<in> M" "rel_pmf R (return_pmf x) M"
1.63 +  then obtain pq where *: "\<And>a b. (a, b) \<in> set_pmf pq \<Longrightarrow> R a b"
1.64 +    and eq: "return_pmf x = map_pmf fst pq" "M = map_pmf snd pq"
1.65 +    by (force elim: rel_pmf.cases)
1.66 +  moreover have "set_pmf (return_pmf x) = {x}"
1.67 +    by (simp add: set_return_pmf)
1.68 +  with `a \<in> M` have "(x, a) \<in> pq"
1.69 +    by (force simp: eq set_map_pmf)
1.70 +  with * show "R x a"
1.71 +    by auto
1.72 +qed (auto intro!: rel_pmf.intros[where pq="pair_pmf (return_pmf x) M"]
1.73 +          simp: map_fst_pair_pmf map_snd_pair_pmf set_pair_pmf set_return_pmf)
1.74 +
1.75 +lemma rel_pmf_return_pmf2: "rel_pmf R M (return_pmf x) \<longleftrightarrow> (\<forall>a\<in>M. R a x)"
1.76 +  by (subst pmf.rel_flip[symmetric]) (simp add: rel_pmf_return_pmf1)
1.77 +
1.78 +lemma rel_pmf_rel_prod:
1.79 +  "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B') \<longleftrightarrow> rel_pmf R A B \<and> rel_pmf S A' B'"
1.80 +proof safe
1.81 +  assume "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')"
1.82 +  then obtain pq where pq: "\<And>a b c d. ((a, c), (b, d)) \<in> set_pmf pq \<Longrightarrow> R a b \<and> S c d"
1.83 +    and eq: "map_pmf fst pq = pair_pmf A A'" "map_pmf snd pq = pair_pmf B B'"
1.84 +    by (force elim: rel_pmf.cases)
1.85 +  show "rel_pmf R A B"
1.86 +  proof (rule rel_pmf.intros)
1.87 +    let ?f = "\<lambda>(a, b). (fst a, fst b)"
1.88 +    have [simp]: "(\<lambda>x. fst (?f x)) = fst o fst" "(\<lambda>x. snd (?f x)) = fst o snd"
1.89 +      by auto
1.90 +
1.91 +    show "map_pmf fst (map_pmf ?f pq) = A"
1.92 +      by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_fst_pair_pmf)
1.93 +    show "map_pmf snd (map_pmf ?f pq) = B"
1.94 +      by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_fst_pair_pmf)
1.95 +
1.96 +    fix a b assume "(a, b) \<in> set_pmf (map_pmf ?f pq)"
1.97 +    then obtain c d where "((a, c), (b, d)) \<in> set_pmf pq"
1.98 +      by (auto simp: set_map_pmf)
1.99 +    from pq[OF this] show "R a b" ..
1.100 +  qed
1.101 +  show "rel_pmf S A' B'"
1.102 +  proof (rule rel_pmf.intros)
1.103 +    let ?f = "\<lambda>(a, b). (snd a, snd b)"
1.104 +    have [simp]: "(\<lambda>x. fst (?f x)) = snd o fst" "(\<lambda>x. snd (?f x)) = snd o snd"
1.105 +      by auto
1.106 +
1.107 +    show "map_pmf fst (map_pmf ?f pq) = A'"
1.108 +      by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_snd_pair_pmf)
1.109 +    show "map_pmf snd (map_pmf ?f pq) = B'"
1.110 +      by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_snd_pair_pmf)
1.111 +
1.112 +    fix c d assume "(c, d) \<in> set_pmf (map_pmf ?f pq)"
1.113 +    then obtain a b where "((a, c), (b, d)) \<in> set_pmf pq"
1.114 +      by (auto simp: set_map_pmf)
1.115 +    from pq[OF this] show "S c d" ..
1.116 +  qed
1.117 +next
1.118 +  assume "rel_pmf R A B" "rel_pmf S A' B'"
1.119 +  then obtain Rpq Spq
1.120 +    where Rpq: "\<And>a b. (a, b) \<in> set_pmf Rpq \<Longrightarrow> R a b"
1.121 +        "map_pmf fst Rpq = A" "map_pmf snd Rpq = B"
1.122 +      and Spq: "\<And>a b. (a, b) \<in> set_pmf Spq \<Longrightarrow> S a b"
1.123 +        "map_pmf fst Spq = A'" "map_pmf snd Spq = B'"
1.124 +    by (force elim: rel_pmf.cases)
1.125 +
1.126 +  let ?f = "(\<lambda>((a, c), (b, d)). ((a, b), (c, d)))"
1.127 +  let ?pq = "map_pmf ?f (pair_pmf Rpq Spq)"
1.128 +  have [simp]: "(\<lambda>x. fst (?f x)) = (\<lambda>(a, b). (fst a, fst b))" "(\<lambda>x. snd (?f x)) = (\<lambda>(a, b). (snd a, snd b))"
1.129 +    by auto
1.130 +
1.131 +  show "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')"
1.132 +    by (rule rel_pmf.intros[where pq="?pq"])
1.133 +       (auto simp: map_snd_pair_pmf map_fst_pair_pmf set_pair_pmf set_map_pmf map_pmf_comp Rpq Spq
1.134 +                   map_pair)
1.135 +qed
1.136 +
1.137  end
1.138
```