src/HOL/Probability/Probability_Mass_Function.thy
changeset 59425 c5e79df8cc21
parent 59327 8a779359df67
child 59475 8300c4ddf493
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Jan 22 13:21:45 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Jan 22 14:51:08 2015 +0100
     1.3 @@ -12,16 +12,6 @@
     1.4    "~~/src/HOL/Library/Multiset"
     1.5  begin
     1.6  
     1.7 -lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M"
     1.8 -   by (cases "space M = {}")
     1.9 -      (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'
    1.10 -                cong: subprob_algebra_cong)
    1.11 -
    1.12 -
    1.13 -lemma (in prob_space) distr_const[simp]:
    1.14 -  "c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c"
    1.15 -  by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1)
    1.16 -
    1.17  lemma (in finite_measure) countable_support:
    1.18    "countable {x. measure M {x} \<noteq> 0}"
    1.19  proof cases
    1.20 @@ -214,8 +204,7 @@
    1.21    by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single)
    1.22  
    1.23  lemma measure_measure_pmf_finite: "finite S \<Longrightarrow> measure (measure_pmf M) S = setsum (pmf M) S"
    1.24 -using emeasure_measure_pmf_finite[of S M]
    1.25 -by(simp add: measure_pmf.emeasure_eq_measure)
    1.26 +  using emeasure_measure_pmf_finite[of S M] by(simp add: measure_pmf.emeasure_eq_measure)
    1.27  
    1.28  lemma nn_integral_measure_pmf_support:
    1.29    fixes f :: "'a \<Rightarrow> ereal"
    1.30 @@ -759,33 +748,34 @@
    1.31                intro!: measure_pmf.integrable_const_bound[where B=1])
    1.32    done
    1.33  
    1.34 +
    1.35  lemma measurable_pair_restrict_pmf2:
    1.36    assumes "countable A"
    1.37 -  assumes "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L"
    1.38 -  shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L"
    1.39 -  apply (subst measurable_cong_sets)
    1.40 -  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
    1.41 -  apply (simp_all add: restrict_count_space)
    1.42 -  apply (subst split_eta[symmetric])
    1.43 -  unfolding measurable_split_conv
    1.44 -  apply (rule measurable_compose_countable'[OF _ measurable_snd `countable A`])
    1.45 -  apply (rule measurable_compose[OF measurable_fst])
    1.46 -  apply fact
    1.47 -  done
    1.48 +  assumes [measurable]: "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L"
    1.49 +  shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L" (is "f \<in> measurable ?M _")
    1.50 +proof -
    1.51 +  have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)"
    1.52 +    by (simp add: restrict_count_space)
    1.53 +
    1.54 +  show ?thesis
    1.55 +    by (intro measurable_compose_countable'[where f="\<lambda>a b. f (fst b, a)" and g=snd and I=A,
    1.56 +                                            unfolded pair_collapse] assms)
    1.57 +        measurable
    1.58 +qed
    1.59  
    1.60  lemma measurable_pair_restrict_pmf1:
    1.61    assumes "countable A"
    1.62 -  assumes "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L"
    1.63 +  assumes [measurable]: "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L"
    1.64    shows "f \<in> measurable (restrict_space (measure_pmf M) A \<Otimes>\<^sub>M N) L"
    1.65 -  apply (subst measurable_cong_sets)
    1.66 -  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
    1.67 -  apply (simp_all add: restrict_count_space)
    1.68 -  apply (subst split_eta[symmetric])
    1.69 -  unfolding measurable_split_conv
    1.70 -  apply (rule measurable_compose_countable'[OF _ measurable_fst `countable A`])
    1.71 -  apply (rule measurable_compose[OF measurable_snd])
    1.72 -  apply fact
    1.73 -  done
    1.74 +proof -
    1.75 +  have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)"
    1.76 +    by (simp add: restrict_count_space)
    1.77 +
    1.78 +  show ?thesis
    1.79 +    by (intro measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A,
    1.80 +                                            unfolded pair_collapse] assms)
    1.81 +        measurable
    1.82 +qed
    1.83                                  
    1.84  lemma bind_commute_pmf: "bind_pmf A (\<lambda>x. bind_pmf B (C x)) = bind_pmf B (\<lambda>y. bind_pmf A (\<lambda>x. C x y))"
    1.85    unfolding pmf_eq_iff pmf_bind
    1.86 @@ -993,11 +983,6 @@
    1.87       map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk>
    1.88    \<Longrightarrow> rel_pmf R p q"
    1.89  
    1.90 -lemma nn_integral_count_space_eq:
    1.91 -  "(\<And>x. x \<in> A - B \<Longrightarrow> f x = 0) \<Longrightarrow> (\<And>x. x \<in> B - A \<Longrightarrow> f x = 0) \<Longrightarrow>
    1.92 -    (\<integral>\<^sup>+x. f x \<partial>count_space A) = (\<integral>\<^sup>+x. f x \<partial>count_space B)"
    1.93 -  by (auto simp: nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
    1.94 -
    1.95  bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf
    1.96  proof -
    1.97    show "map_pmf id = id" by (rule map_pmf_id)