cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
authorhoelzl
Fri Nov 14 13:18:33 2014 +0100 (2014-11-14)
changeset 590022c8b2fb54b88
parent 59001 44afb337bb92
child 59003 16d92d37a8a1
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Indicator_Function.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability_Mass_Function.thy
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Nov 14 08:18:58 2014 +0100
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Nov 14 13:18:33 2014 +0100
     1.3 @@ -863,13 +863,13 @@
     1.4  
     1.5  lemma ereal_left_mult_cong:
     1.6    fixes a b c :: ereal
     1.7 -  shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = c * b"
     1.8 +  shows  "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * d"
     1.9    by (cases "c = 0") simp_all
    1.10  
    1.11  lemma ereal_right_mult_cong: 
    1.12 -  fixes a b c d :: ereal
    1.13 +  fixes a b c :: ereal
    1.14    shows "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = d * b"
    1.15 -  by (cases "d = 0") simp_all
    1.16 +  by (cases "c = 0") simp_all
    1.17  
    1.18  lemma ereal_distrib:
    1.19    fixes a b c :: ereal
    1.20 @@ -891,6 +891,10 @@
    1.21    shows "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> r * setsum f A = (\<Sum>n\<in>A. r * f n)"
    1.22    by (induct A rule: infinite_finite_induct)  (auto simp: ereal_right_distrib setsum_nonneg)
    1.23  
    1.24 +lemma setsum_ereal_left_distrib:
    1.25 +  "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> setsum f A * r = (\<Sum>n\<in>A. f n * r :: ereal)"
    1.26 +  using setsum_ereal_right_distrib[of A f r] by (simp add: mult_ac)
    1.27 +
    1.28  lemma ereal_le_epsilon:
    1.29    fixes x y :: ereal
    1.30    assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + e"
     2.1 --- a/src/HOL/Library/Indicator_Function.thy	Fri Nov 14 08:18:58 2014 +0100
     2.2 +++ b/src/HOL/Library/Indicator_Function.thy	Fri Nov 14 13:18:33 2014 +0100
     2.3 @@ -57,6 +57,9 @@
     2.4  lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
     2.5    unfolding indicator_def by (cases x) auto
     2.6  
     2.7 +lemma indicator_image: "inj f \<Longrightarrow> indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)"
     2.8 +  by (auto simp: indicator_def inj_on_def)
     2.9 +
    2.10  lemma
    2.11    fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
    2.12    shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
     3.1 --- a/src/HOL/Probability/Giry_Monad.thy	Fri Nov 14 08:18:58 2014 +0100
     3.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Fri Nov 14 13:18:33 2014 +0100
     3.3 @@ -785,7 +785,7 @@
     3.4        \<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
     3.5    by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)
     3.6  
     3.7 -lemma nn_integral_bind:
     3.8 +lemma nn_integral_bind':
     3.9    assumes f: "f \<in> borel_measurable B" "\<And>x. 0 \<le> f x"
    3.10    assumes N: "N \<in> measurable M (subprob_algebra B)"
    3.11    shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
    3.12 @@ -795,6 +795,15 @@
    3.13      by (rule nn_integral_distr[OF N nn_integral_measurable_subprob_algebra[OF f]])
    3.14  qed (simp add: bind_empty space_empty[of M] nn_integral_count_space)
    3.15  
    3.16 +lemma nn_integral_bind:
    3.17 +  assumes [measurable]: "f \<in> borel_measurable B"
    3.18 +  assumes N: "N \<in> measurable M (subprob_algebra B)"
    3.19 +  shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
    3.20 +  apply (subst (1 3) nn_integral_max_0[symmetric])
    3.21 +  apply (rule nn_integral_bind'[OF _ _ N])
    3.22 +  apply auto
    3.23 +  done
    3.24 +
    3.25  lemma AE_bind:
    3.26    assumes P[measurable]: "Measurable.pred B P"
    3.27    assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)"
     4.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri Nov 14 08:18:58 2014 +0100
     4.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri Nov 14 13:18:33 2014 +0100
     4.3 @@ -552,7 +552,7 @@
     4.4      (\<Sum>y\<in>f`space M. y * (\<Sum>z\<in>g`space M. 
     4.5        if \<exists>x\<in>space M. y = f x \<and> z = g x then emeasure M {x\<in>space M. g x = z} else 0))"
     4.6      unfolding simple_integral_def
     4.7 -  proof (safe intro!: setsum.cong ereal_left_mult_cong)
     4.8 +  proof (safe intro!: setsum.cong ereal_right_mult_cong)
     4.9      fix y assume y: "y \<in> space M" "f y \<noteq> 0"
    4.10      have [simp]: "g ` space M \<inter> {z. \<exists>x\<in>space M. f y = f x \<and> z = g x} = 
    4.11          {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"
    4.12 @@ -1894,7 +1894,7 @@
    4.13    using simple_function_restrict_space_ereal[THEN iffD1, OF \<Omega>, THEN simple_functionD(1)]
    4.14    by (auto simp add: space_restrict_space emeasure_restrict_space[OF \<Omega>(1)] le_infI2 simple_integral_def
    4.15             split: split_indicator split_indicator_asm
    4.16 -           intro!: setsum.mono_neutral_cong_left ereal_left_mult_cong arg_cong2[where f=emeasure])
    4.17 +           intro!: setsum.mono_neutral_cong_left ereal_right_mult_cong[OF refl] arg_cong2[where f=emeasure])
    4.18  
    4.19  lemma one_not_less_zero[simp]: "\<not> 1 < (0::ereal)"
    4.20    by (simp add: zero_ereal_def one_ereal_def) 
     5.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Nov 14 08:18:58 2014 +0100
     5.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Nov 14 13:18:33 2014 +0100
     5.3 @@ -281,6 +281,12 @@
     5.4    unfolding `p = q`[symmetric] measure_pmf_inject[symmetric] map_pmf.rep_eq
     5.5    by (auto simp add: emeasure_distr AE_measure_pmf_iff intro!: emeasure_eq_AE measure_eqI)
     5.6  
     5.7 +lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f -` X)"
     5.8 +  unfolding map_pmf.rep_eq by (subst emeasure_distr) auto
     5.9 +
    5.10 +lemma nn_integral_map_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>map_pmf g M) = (\<integral>\<^sup>+x. f (g x) \<partial>M)"
    5.11 +  unfolding map_pmf.rep_eq by (intro nn_integral_distr) auto
    5.12 +
    5.13  lemma pmf_set_map: 
    5.14    fixes f :: "'a \<Rightarrow> 'b"
    5.15    shows "set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf"
    5.16 @@ -433,6 +439,17 @@
    5.17  lemma set_pmf_bernoulli: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (bernoulli_pmf p) = UNIV"
    5.18    by (auto simp add: set_pmf_iff UNIV_bool)
    5.19  
    5.20 +lemma nn_integral_bernoulli_pmf[simp]: 
    5.21 +  assumes [simp]: "0 \<le> p" "p \<le> 1" "\<And>x. 0 \<le> f x"
    5.22 +  shows "(\<integral>\<^sup>+x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
    5.23 +  by (subst nn_integral_measure_pmf_support[of UNIV])
    5.24 +     (auto simp: UNIV_bool field_simps)
    5.25 +
    5.26 +lemma integral_bernoulli_pmf[simp]: 
    5.27 +  assumes [simp]: "0 \<le> p" "p \<le> 1"
    5.28 +  shows "(\<integral>x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
    5.29 +  by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool)
    5.30 +
    5.31  lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. 1 / 2^Suc n"
    5.32  proof
    5.33    note geometric_sums[of "1 / 2"]
    5.34 @@ -445,7 +462,7 @@
    5.35  lemma pmf_geometric[simp]: "pmf geometric_pmf n = 1 / 2^Suc n"
    5.36    by transfer rule
    5.37  
    5.38 -lemma set_pmf_geometric: "set_pmf geometric_pmf = UNIV"
    5.39 +lemma set_pmf_geometric[simp]: "set_pmf geometric_pmf = UNIV"
    5.40    by (auto simp: set_pmf_iff)
    5.41  
    5.42  context
    5.43 @@ -485,6 +502,9 @@
    5.44  lemma set_pmf_of_set[simp]: "set_pmf pmf_of_set = S"
    5.45    using S_finite S_not_empty by (auto simp: set_pmf_iff)
    5.46  
    5.47 +lemma emeasure_pmf_of_set[simp]: "emeasure pmf_of_set S = 1"
    5.48 +  by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff)
    5.49 +
    5.50  end
    5.51  
    5.52  end
    5.53 @@ -558,12 +578,18 @@
    5.54  lemma map_return_pmf: "map_pmf f (return_pmf x) = return_pmf (f x)"
    5.55    by transfer (simp add: distr_return)
    5.56  
    5.57 -lemma set_pmf_return: "set_pmf (return_pmf x) = {x}"
    5.58 +lemma set_return_pmf: "set_pmf (return_pmf x) = {x}"
    5.59    by transfer (auto simp add: measure_return split: split_indicator)
    5.60  
    5.61  lemma pmf_return: "pmf (return_pmf x) y = indicator {y} x"
    5.62    by transfer (simp add: measure_return)
    5.63  
    5.64 +lemma nn_integral_return_pmf[simp]: "0 \<le> f x \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>return_pmf x) = f x"
    5.65 +  unfolding return_pmf.rep_eq by (intro nn_integral_return) auto
    5.66 +
    5.67 +lemma emeasure_return_pmf[simp]: "emeasure (return_pmf x) X = indicator X x"
    5.68 +  unfolding return_pmf.rep_eq by (intro emeasure_return) auto
    5.69 +
    5.70  end
    5.71  
    5.72  definition "bind_pmf M f = join_pmf (map_pmf f M)"
    5.73 @@ -584,6 +610,41 @@
    5.74  lemma bind_return_pmf: "bind_pmf (return_pmf x) f = f x"
    5.75    unfolding bind_pmf_def map_return_pmf join_return_pmf ..
    5.76  
    5.77 +lemma set_bind_pmf: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
    5.78 +  apply (simp add: set_eq_iff set_pmf_iff pmf_bind)
    5.79 +  apply (subst integral_nonneg_eq_0_iff_AE)
    5.80 +  apply (auto simp: pmf_nonneg pmf_le_1 AE_measure_pmf_iff
    5.81 +              intro!: measure_pmf.integrable_const_bound[where B=1])
    5.82 +  done
    5.83 +
    5.84 +lemma measurable_pair_restrict_pmf2:
    5.85 +  assumes "countable A"
    5.86 +  assumes "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L"
    5.87 +  shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L"
    5.88 +  apply (subst measurable_cong_sets)
    5.89 +  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
    5.90 +  apply (simp_all add: restrict_count_space)
    5.91 +  apply (subst split_eta[symmetric])
    5.92 +  unfolding measurable_split_conv
    5.93 +  apply (rule measurable_compose_countable'[OF _ measurable_snd `countable A`])
    5.94 +  apply (rule measurable_compose[OF measurable_fst])
    5.95 +  apply fact
    5.96 +  done
    5.97 +
    5.98 +lemma measurable_pair_restrict_pmf1:
    5.99 +  assumes "countable A"
   5.100 +  assumes "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L"
   5.101 +  shows "f \<in> measurable (restrict_space (measure_pmf M) A \<Otimes>\<^sub>M N) L"
   5.102 +  apply (subst measurable_cong_sets)
   5.103 +  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
   5.104 +  apply (simp_all add: restrict_count_space)
   5.105 +  apply (subst split_eta[symmetric])
   5.106 +  unfolding measurable_split_conv
   5.107 +  apply (rule measurable_compose_countable'[OF _ measurable_fst `countable A`])
   5.108 +  apply (rule measurable_compose[OF measurable_snd])
   5.109 +  apply fact
   5.110 +  done
   5.111 +                                
   5.112  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))"
   5.113    unfolding pmf_eq_iff pmf_bind
   5.114  proof
   5.115 @@ -601,36 +662,15 @@
   5.116    have "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>A)"
   5.117      by (rule integral_cong) (auto intro!: integral_pmf_restrict)
   5.118    also have "\<dots> = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>restrict_space A A)"
   5.119 -    apply (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral)
   5.120 -    apply (auto simp: measurable_split_conv)
   5.121 -    apply (subst measurable_cong_sets)
   5.122 -    apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
   5.123 -    apply (simp add: restrict_count_space)
   5.124 -    apply (rule measurable_compose_countable'[OF _ measurable_snd])
   5.125 -    apply (rule measurable_compose[OF measurable_fst])
   5.126 -    apply (auto intro: countable_set_pmf)
   5.127 -    done
   5.128 +    by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
   5.129 +              countable_set_pmf borel_measurable_count_space)
   5.130    also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>restrict_space A A \<partial>restrict_space B B)"
   5.131 -    apply (rule AB.Fubini_integral[symmetric])
   5.132 -    apply (auto intro!: AB.integrable_const_bound[where B=1] simp: pmf_nonneg pmf_le_1)
   5.133 -    apply (auto simp: measurable_split_conv)
   5.134 -    apply (subst measurable_cong_sets)
   5.135 -    apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
   5.136 -    apply (simp add: restrict_count_space)
   5.137 -    apply (rule measurable_compose_countable'[OF _ measurable_snd])
   5.138 -    apply (rule measurable_compose[OF measurable_fst])
   5.139 -    apply (auto intro: countable_set_pmf)
   5.140 -    done
   5.141 +    by (rule AB.Fubini_integral[symmetric])
   5.142 +       (auto intro!: AB.integrable_const_bound[where B=1] measurable_pair_restrict_pmf2
   5.143 +             simp: pmf_nonneg pmf_le_1 countable_set_pmf measurable_restrict_space1)
   5.144    also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>restrict_space A A \<partial>B)"
   5.145 -    apply (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral)
   5.146 -    apply (auto simp: measurable_split_conv)
   5.147 -    apply (subst measurable_cong_sets)
   5.148 -    apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
   5.149 -    apply (simp add: restrict_count_space)
   5.150 -    apply (rule measurable_compose_countable'[OF _ measurable_snd])
   5.151 -    apply (rule measurable_compose[OF measurable_fst])
   5.152 -    apply (auto intro: countable_set_pmf)
   5.153 -    done
   5.154 +    by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
   5.155 +              countable_set_pmf borel_measurable_count_space)
   5.156    also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)"
   5.157      by (rule integral_cong) (auto intro!: integral_pmf_restrict[symmetric])
   5.158    finally show "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)" .
   5.159 @@ -642,6 +682,22 @@
   5.160  
   5.161  interpretation pmf_as_measure .
   5.162  
   5.163 +lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<guillemotright>= (\<lambda>x. measure_pmf (f x)))"
   5.164 +  by transfer simp
   5.165 +
   5.166 +lemma nn_integral_bind_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>bind_pmf M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
   5.167 +  using measurable_measure_pmf[of N]
   5.168 +  unfolding measure_pmf_bind
   5.169 +  apply (subst (1 3) nn_integral_max_0[symmetric])
   5.170 +  apply (intro nn_integral_bind[where B="count_space UNIV"])
   5.171 +  apply auto
   5.172 +  done
   5.173 +
   5.174 +lemma emeasure_bind_pmf[simp]: "emeasure (bind_pmf M N) X = (\<integral>\<^sup>+x. emeasure (N x) X \<partial>M)"
   5.175 +  using measurable_measure_pmf[of N]
   5.176 +  unfolding measure_pmf_bind
   5.177 +  by (subst emeasure_bind[where N="count_space UNIV"]) auto
   5.178 +
   5.179  lemma bind_return_pmf': "bind_pmf N return_pmf = N"
   5.180  proof (transfer, clarify)
   5.181    fix N :: "'a measure" assume "sets N = UNIV" then show "N \<guillemotright>= return (count_space UNIV) = N"
   5.182 @@ -661,9 +717,6 @@
   5.183       (auto intro!: bind_assoc[where N="count_space UNIV" and R="count_space UNIV"]
   5.184             simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space)
   5.185  
   5.186 -lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<guillemotright>= (\<lambda>x. measure_pmf (f x)))"
   5.187 -  by transfer simp
   5.188 -
   5.189  end
   5.190  
   5.191  definition "pair_pmf A B = bind_pmf A (\<lambda>x. bind_pmf B (\<lambda>y. return_pmf (x, y)))"
   5.192 @@ -676,6 +729,9 @@
   5.193    apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg)
   5.194    done
   5.195  
   5.196 +lemma set_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
   5.197 +  unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto
   5.198 +
   5.199  lemma bind_pair_pmf:
   5.200    assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)"
   5.201    shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))"
   5.202 @@ -700,18 +756,18 @@
   5.203    then show "emeasure ?L X = emeasure ?R X"
   5.204      apply (simp add: emeasure_bind[OF _ M' X])
   5.205      unfolding pair_pmf_def measure_pmf_bind[of A]
   5.206 -    apply (subst nn_integral_bind[OF _ emeasure_nonneg])
   5.207 +    apply (subst nn_integral_bind)
   5.208      apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
   5.209      apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
   5.210      apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
   5.211      apply measurable
   5.212      unfolding measure_pmf_bind
   5.213 -    apply (subst nn_integral_bind[OF _ emeasure_nonneg])
   5.214 +    apply (subst nn_integral_bind)
   5.215      apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
   5.216      apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
   5.217      apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
   5.218      apply measurable
   5.219 -    apply (simp add: nn_integral_measure_pmf_finite set_pmf_return emeasure_nonneg pmf_return one_ereal_def[symmetric])
   5.220 +    apply (simp add: nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric])
   5.221      apply (subst emeasure_bind[OF _ _ X])
   5.222      apply simp
   5.223      apply (rule measurable_bind[where N="count_space UNIV"])
   5.224 @@ -727,15 +783,6 @@
   5.225      done
   5.226  qed
   5.227  
   5.228 -lemma set_pmf_bind: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
   5.229 -  apply (simp add: set_eq_iff set_pmf_iff pmf_bind)
   5.230 -  apply (subst integral_nonneg_eq_0_iff_AE)
   5.231 -  apply (auto simp: pmf_nonneg pmf_le_1 AE_measure_pmf_iff
   5.232 -              intro!: measure_pmf.integrable_const_bound[where B=1])
   5.233 -  done
   5.234 -
   5.235 -lemma set_pmf_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
   5.236 -  unfolding pair_pmf_def set_pmf_bind set_pmf_return by auto
   5.237  
   5.238  (*
   5.239