src/HOL/Probability/Probability_Mass_Function.thy
changeset 59048 7dc8ac6f0895
parent 59024 5fcfeae84b96
child 59052 a05c8305781e
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 24 12:20:35 2014 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 24 12:20:14 2014 +0100
     1.3 @@ -98,6 +98,9 @@
     1.4  interpretation measure_pmf!: subprob_space "measure_pmf M" for M
     1.5    by (rule prob_space_imp_subprob_space) unfold_locales
     1.6  
     1.7 +lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)"
     1.8 +  by unfold_locales
     1.9 +
    1.10  locale pmf_as_measure
    1.11  begin
    1.12  
    1.13 @@ -141,12 +144,16 @@
    1.14  lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV"
    1.15    by transfer metis
    1.16  
    1.17 -lemma sets_measure_pmf_count_space: "sets (measure_pmf M) = sets (count_space UNIV)"
    1.18 +lemma sets_measure_pmf_count_space[measurable_cong]:
    1.19 +  "sets (measure_pmf M) = sets (count_space UNIV)"
    1.20    by simp
    1.21  
    1.22  lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV"
    1.23    using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp
    1.24  
    1.25 +lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \<in> space (subprob_algebra (count_space UNIV))"
    1.26 +  by (simp add: space_subprob_algebra subprob_space_measure_pmf)
    1.27 +
    1.28  lemma measurable_pmf_measure1[simp]: "measurable (M :: 'a pmf) N = UNIV \<rightarrow> space N"
    1.29    by (auto simp: measurable_def)
    1.30  
    1.31 @@ -555,11 +562,11 @@
    1.32    shows "bind (measure_pmf x) A = bind (measure_pmf x) B"
    1.33  proof (rule measure_eqI)
    1.34    show "sets (measure_pmf x \<guillemotright>= A) = sets (measure_pmf x \<guillemotright>= B)"
    1.35 -    using assms by (subst (1 2) sets_bind) auto
    1.36 +    using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra)
    1.37  next
    1.38    fix X assume "X \<in> sets (measure_pmf x \<guillemotright>= A)"
    1.39    then have X: "X \<in> sets N"
    1.40 -    using assms by (subst (asm) sets_bind) auto
    1.41 +    using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra)
    1.42    show "emeasure (measure_pmf x \<guillemotright>= A) X = emeasure (measure_pmf x \<guillemotright>= B) X"
    1.43      using assms
    1.44      by (subst (1 2) emeasure_bind[where N=N, OF _ _ X])
    1.45 @@ -575,21 +582,19 @@
    1.46  proof (intro conjI)
    1.47    fix M :: "'a pmf pmf"
    1.48  
    1.49 -  have *: "measure_pmf \<in> measurable (measure_pmf M) (subprob_algebra (count_space UNIV))"
    1.50 -    using measurable_measure_pmf[of "\<lambda>x. x"] by simp
    1.51 -  
    1.52    interpret bind: prob_space "measure_pmf M \<guillemotright>= measure_pmf"
    1.53 -    apply (rule measure_pmf.prob_space_bind[OF _ *])
    1.54 -    apply (auto intro!: AE_I2)
    1.55 +    apply (intro measure_pmf.prob_space_bind[where S="count_space UNIV"] AE_I2)
    1.56 +    apply (auto intro!: subprob_space_measure_pmf simp: space_subprob_algebra)
    1.57      apply unfold_locales
    1.58      done
    1.59    show "prob_space (measure_pmf M \<guillemotright>= measure_pmf)"
    1.60      by intro_locales
    1.61    show "sets (measure_pmf M \<guillemotright>= measure_pmf) = UNIV"
    1.62 -    by (subst sets_bind[OF *]) auto
    1.63 +    by (subst sets_bind) auto
    1.64    have "AE x in measure_pmf M \<guillemotright>= measure_pmf. emeasure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0"
    1.65 -    by (auto simp add: AE_bind[OF _ *] AE_measure_pmf_iff emeasure_bind[OF _ *]
    1.66 -        nn_integral_0_iff_AE measure_pmf.emeasure_eq_measure measure_le_0_iff set_pmf_iff pmf.rep_eq)
    1.67 +    by (auto simp: AE_bind[where B="count_space UNIV"] measure_pmf_in_subprob_algebra
    1.68 +                   emeasure_bind[where N="count_space UNIV"] AE_measure_pmf_iff nn_integral_0_iff_AE
    1.69 +                   measure_pmf.emeasure_eq_measure measure_le_0_iff set_pmf_iff pmf.rep_eq)
    1.70    then show "AE x in measure_pmf M \<guillemotright>= measure_pmf. measure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0"
    1.71      unfolding bind.emeasure_eq_measure by simp
    1.72  qed
    1.73 @@ -772,6 +777,10 @@
    1.74  lemma set_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
    1.75    unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto
    1.76  
    1.77 +lemma measure_pmf_in_subprob_space[measurable (raw)]:
    1.78 +  "measure_pmf M \<in> space (subprob_algebra (count_space UNIV))"
    1.79 +  by (simp add: space_subprob_algebra) intro_locales
    1.80 +
    1.81  lemma bind_pair_pmf:
    1.82    assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)"
    1.83    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.84 @@ -780,46 +789,25 @@
    1.85    have M'[measurable]: "M \<in> measurable (pair_pmf A B) (subprob_algebra N)"
    1.86      using M[THEN measurable_space] by (simp_all add: space_pair_measure)
    1.87  
    1.88 +  note measurable_bind[where N="count_space UNIV", measurable]
    1.89 +  note measure_pmf_in_subprob_space[simp]
    1.90 +
    1.91    have sets_eq_N: "sets ?L = N"
    1.92 -    by (simp add: sets_bind[OF M'])
    1.93 +    by (subst sets_bind[OF sets_kernel[OF M']]) auto
    1.94    show "sets ?L = sets ?R"
    1.95 -    unfolding sets_eq_N
    1.96 -    apply (subst sets_bind[where N=N])
    1.97 -    apply (rule measurable_bind)
    1.98 -    apply (rule measurable_compose[OF _ measurable_measure_pmf])
    1.99 -    apply measurable
   1.100 -    apply (auto intro!: sets_pair_measure_cong sets_measure_pmf_count_space)
   1.101 -    done
   1.102 +    using measurable_space[OF M]
   1.103 +    by (simp add: sets_eq_N space_pair_measure space_subprob_algebra)
   1.104    fix X assume "X \<in> sets ?L"
   1.105    then have X[measurable]: "X \<in> sets N"
   1.106      unfolding sets_eq_N .
   1.107    then show "emeasure ?L X = emeasure ?R X"
   1.108      apply (simp add: emeasure_bind[OF _ M' X])
   1.109 -    unfolding pair_pmf_def measure_pmf_bind[of A]
   1.110 -    apply (subst nn_integral_bind)
   1.111 -    apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
   1.112 -    apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
   1.113 -    apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
   1.114 -    apply measurable
   1.115 -    unfolding measure_pmf_bind
   1.116 -    apply (subst nn_integral_bind)
   1.117 -    apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
   1.118 -    apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
   1.119 -    apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
   1.120 +    apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A]
   1.121 +      nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric])
   1.122 +    apply (subst emeasure_bind[OF _ _ X])
   1.123      apply measurable
   1.124 -    apply (simp add: nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric])
   1.125      apply (subst emeasure_bind[OF _ _ X])
   1.126 -    apply simp
   1.127 -    apply (rule measurable_bind[where N="count_space UNIV"])
   1.128 -    apply (rule measurable_compose[OF _ measurable_measure_pmf])
   1.129      apply measurable
   1.130 -    apply (rule sets_pair_measure_cong sets_measure_pmf_count_space refl)+
   1.131 -    apply (subst measurable_cong_sets[OF sets_pair_measure_cong[OF sets_measure_pmf_count_space refl] refl])
   1.132 -    apply simp
   1.133 -    apply (subst emeasure_bind[OF _ _ X])
   1.134 -    apply simp
   1.135 -    apply (rule measurable_compose[OF _ M])
   1.136 -    apply (auto simp: space_pair_measure)
   1.137      done
   1.138  qed
   1.139