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.57      by(auto simp add: le_fun_def)
    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