src/HOL/Probability/Probability_Mass_Function.thy
 changeset 62975 1d066f6ab25d parent 62390 842917225d56 child 63040 eb4ddd18d635
```     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Apr 14 12:17:44 2016 +0200
1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Apr 14 15:48:11 2016 +0200
1.3 @@ -22,16 +22,13 @@
1.4      with x_M[THEN sets.sets_into_space] N have "emeasure M {x} \<le> emeasure M N"
1.5        by (intro emeasure_mono) auto
1.6      with x N have False
1.7 -      by (auto simp: emeasure_le_0_iff) }
1.8 +      by (auto simp:) }
1.9    then show "P x" by auto
1.10  qed
1.11
1.12  lemma AE_measure_singleton: "measure M {x} \<noteq> 0 \<Longrightarrow> AE x in M. P x \<Longrightarrow> P x"
1.13    by (metis AE_emeasure_singleton measure_def emeasure_empty measure_empty)
1.14
1.15 -lemma ereal_divide': "b \<noteq> 0 \<Longrightarrow> ereal (a / b) = ereal a / ereal b"
1.16 -  using ereal_divide[of a b] by simp
1.17 -
1.18  lemma (in finite_measure) AE_support_countable:
1.19    assumes [simp]: "sets M = UNIV"
1.20    shows "(AE x in M. measure M {x} \<noteq> 0) \<longleftrightarrow> (\<exists>S. countable S \<and> (AE x in M. x \<in> S))"
1.21 @@ -54,7 +51,7 @@
1.22      by (simp add: emeasure_single_in_space cong: rev_conj_cong)
1.23    with finite_measure_compl[of "{x \<in> space M. x\<in>S \<and> emeasure M {x} \<noteq> 0}"]
1.24    have "AE x in M. x \<in> S \<and> emeasure M {x} \<noteq> 0"
1.25 -    by (intro AE_I[OF order_refl]) (auto simp: emeasure_eq_measure set_diff_eq cong: conj_cong)
1.26 +    by (intro AE_I[OF order_refl]) (auto simp: emeasure_eq_measure measure_nonneg set_diff_eq cong: conj_cong)
1.27    then show "AE x in M. measure M {x} \<noteq> 0"
1.28      by (auto simp: emeasure_eq_measure)
1.29  qed (auto intro!: exI[of _ "{x. measure M {x} \<noteq> 0}"] countable_support)
1.30 @@ -153,7 +150,7 @@
1.31  lemma emeasure_pmf_single_eq_zero_iff:
1.32    fixes M :: "'a pmf"
1.33    shows "emeasure M {y} = 0 \<longleftrightarrow> y \<notin> M"
1.34 -  by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure])
1.35 +  unfolding set_pmf.rep_eq by (simp add: measure_pmf.emeasure_eq_measure)
1.36
1.37  lemma AE_measure_pmf_iff: "(AE x in measure_pmf M. P x) \<longleftrightarrow> (\<forall>y\<in>M. P y)"
1.38    using AE_measure_singleton[of M] AE_measure_pmf[of M]
1.39 @@ -166,10 +163,10 @@
1.40    by transfer (metis prob_space.finite_measure finite_measure.countable_support)
1.41
1.42  lemma pmf_positive: "x \<in> set_pmf p \<Longrightarrow> 0 < pmf p x"
1.43 -  by transfer (simp add: less_le measure_nonneg)
1.44 +  by transfer (simp add: less_le)
1.45
1.46 -lemma pmf_nonneg: "0 \<le> pmf p x"
1.47 -  by transfer (simp add: measure_nonneg)
1.48 +lemma pmf_nonneg[simp]: "0 \<le> pmf p x"
1.49 +  by transfer simp
1.50
1.51  lemma pmf_le_1: "pmf p x \<le> 1"
1.53 @@ -180,6 +177,9 @@
1.54  lemma set_pmf_iff: "x \<in> set_pmf M \<longleftrightarrow> pmf M x \<noteq> 0"
1.55    by transfer simp
1.56
1.57 +lemma pmf_positive_iff: "0 < pmf p x \<longleftrightarrow> x \<in> set_pmf p"
1.58 +  unfolding less_le by (simp add: set_pmf_iff)
1.59 +
1.60  lemma set_pmf_eq: "set_pmf M = {x. pmf M x \<noteq> 0}"
1.61    by (auto simp: set_pmf_iff)
1.62
1.63 @@ -189,16 +189,17 @@
1.64    by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure])
1.65
1.66  lemma measure_pmf_single: "measure (measure_pmf M) {x} = pmf M x"
1.67 -using emeasure_pmf_single[of M x] by(simp add: measure_pmf.emeasure_eq_measure)
1.68 +  using emeasure_pmf_single[of M x] by(simp add: measure_pmf.emeasure_eq_measure pmf_nonneg measure_nonneg)
1.69
1.70  lemma emeasure_measure_pmf_finite: "finite S \<Longrightarrow> emeasure (measure_pmf M) S = (\<Sum>s\<in>S. pmf M s)"
1.71 -  by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single)
1.72 +  by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single pmf_nonneg)
1.73
1.74  lemma measure_measure_pmf_finite: "finite S \<Longrightarrow> measure (measure_pmf M) S = setsum (pmf M) S"
1.75 -  using emeasure_measure_pmf_finite[of S M] by(simp add: measure_pmf.emeasure_eq_measure)
1.76 +  using emeasure_measure_pmf_finite[of S M]
1.77 +  by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg setsum_nonneg pmf_nonneg)
1.78
1.79  lemma nn_integral_measure_pmf_support:
1.80 -  fixes f :: "'a \<Rightarrow> ereal"
1.81 +  fixes f :: "'a \<Rightarrow> ennreal"
1.82    assumes f: "finite A" and nn: "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x" "\<And>x. x \<in> set_pmf M \<Longrightarrow> x \<notin> A \<Longrightarrow> f x = 0"
1.83    shows "(\<integral>\<^sup>+x. f x \<partial>measure_pmf M) = (\<Sum>x\<in>A. f x * pmf M x)"
1.84  proof -
1.85 @@ -211,14 +212,15 @@
1.86  qed
1.87
1.88  lemma nn_integral_measure_pmf_finite:
1.89 -  fixes f :: "'a \<Rightarrow> ereal"
1.90 +  fixes f :: "'a \<Rightarrow> ennreal"
1.91    assumes f: "finite (set_pmf M)" and nn: "\<And>x. x \<in> set_pmf M \<Longrightarrow> 0 \<le> f x"
1.92    shows "(\<integral>\<^sup>+x. f x \<partial>measure_pmf M) = (\<Sum>x\<in>set_pmf M. f x * pmf M x)"
1.93    using assms by (intro nn_integral_measure_pmf_support) auto
1.94 +
1.95  lemma integrable_measure_pmf_finite:
1.96    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
1.97    shows "finite (set_pmf M) \<Longrightarrow> integrable M f"
1.98 -  by (auto intro!: integrableI_bounded simp: nn_integral_measure_pmf_finite)
1.99 +  by (auto intro!: integrableI_bounded simp: nn_integral_measure_pmf_finite ennreal_mult_less_top)
1.100
1.101  lemma integral_measure_pmf:
1.102    assumes [simp]: "finite A" and "\<And>a. a \<in> set_pmf M \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow> a \<in> A"
1.103 @@ -227,7 +229,8 @@
1.104    have "(\<integral>x. f x \<partial>measure_pmf M) = (\<integral>x. f x * indicator A x \<partial>measure_pmf M)"
1.105      using assms(2) by (intro integral_cong_AE) (auto split: split_indicator simp: AE_measure_pmf_iff)
1.106    also have "\<dots> = (\<Sum>a\<in>A. f a * pmf M a)"
1.107 -    by (subst integral_indicator_finite_real) (auto simp: measure_def emeasure_measure_pmf_finite)
1.108 +    by (subst integral_indicator_finite_real)
1.109 +       (auto simp: measure_def emeasure_measure_pmf_finite pmf_nonneg)
1.110    finally show ?thesis .
1.111  qed
1.112
1.113 @@ -254,7 +257,7 @@
1.114    also have "\<dots> = emeasure M X"
1.115      by (auto intro!: emeasure_eq_AE simp: AE_measure_pmf_iff)
1.116    finally show ?thesis
1.117 -    by (simp add: measure_pmf.emeasure_eq_measure)
1.118 +    by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg integral_nonneg pmf_nonneg)
1.119  qed
1.120
1.121  lemma integral_pmf_restrict:
1.122 @@ -336,23 +339,29 @@
1.123      done
1.124  qed
1.125
1.126 -lemma ereal_pmf_bind: "pmf (bind_pmf N f) i = (\<integral>\<^sup>+x. pmf (f x) i \<partial>measure_pmf N)"
1.127 +lemma ennreal_pmf_bind: "pmf (bind_pmf N f) i = (\<integral>\<^sup>+x. pmf (f x) i \<partial>measure_pmf N)"
1.128    unfolding pmf.rep_eq bind_pmf.rep_eq
1.129    by (auto simp: measure_pmf.measure_bind[where N="count_space UNIV"] measure_subprob measure_nonneg
1.130             intro!: nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1])
1.131
1.132  lemma pmf_bind: "pmf (bind_pmf N f) i = (\<integral>x. pmf (f x) i \<partial>measure_pmf N)"
1.133 -  using ereal_pmf_bind[of N f i]
1.134 +  using ennreal_pmf_bind[of N f i]
1.135    by (subst (asm) nn_integral_eq_integral)
1.136 -     (auto simp: pmf_nonneg pmf_le_1
1.137 +     (auto simp: pmf_nonneg pmf_le_1 pmf_nonneg integral_nonneg
1.138             intro!: nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1])
1.139
1.140  lemma bind_pmf_const[simp]: "bind_pmf M (\<lambda>x. c) = c"
1.141    by transfer (simp add: bind_const' prob_space_imp_subprob_space)
1.142
1.143  lemma set_bind_pmf[simp]: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
1.144 -  unfolding set_pmf_eq ereal_eq_0(1)[symmetric] ereal_pmf_bind
1.145 -  by (auto simp add: nn_integral_0_iff_AE AE_measure_pmf_iff set_pmf_eq not_le less_le pmf_nonneg)
1.146 +proof -
1.147 +  have "set_pmf (bind_pmf M N) = {x. ennreal (pmf (bind_pmf M N) x) \<noteq> 0}"
1.148 +    by (simp add: set_pmf_eq pmf_nonneg)
1.149 +  also have "\<dots> = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
1.150 +    unfolding ennreal_pmf_bind
1.151 +    by (subst nn_integral_0_iff_AE) (auto simp: AE_measure_pmf_iff pmf_nonneg set_pmf_eq)
1.152 +  finally show ?thesis .
1.153 +qed
1.154
1.155  lemma bind_pmf_cong:
1.156    assumes "p = q"
1.157 @@ -372,7 +381,6 @@
1.158  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)"
1.159    using measurable_measure_pmf[of N]
1.160    unfolding measure_pmf_bind
1.161 -  apply (subst (1 3) nn_integral_max_0[symmetric])
1.162    apply (intro nn_integral_bind[where B="count_space UNIV"])
1.163    apply auto
1.164    done
1.165 @@ -452,18 +460,28 @@
1.166    unfolding map_pmf_rep_eq by (subst emeasure_distr) auto
1.167
1.168  lemma measure_map_pmf[simp]: "measure (map_pmf f M) X = measure M (f -` X)"
1.169 -using emeasure_map_pmf[of f M X] by(simp add: measure_pmf.emeasure_eq_measure)
1.170 +using emeasure_map_pmf[of f M X] by(simp add: measure_pmf.emeasure_eq_measure measure_nonneg)
1.171
1.172  lemma nn_integral_map_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>map_pmf g M) = (\<integral>\<^sup>+x. f (g x) \<partial>M)"
1.173    unfolding map_pmf_rep_eq by (intro nn_integral_distr) auto
1.174
1.175 -lemma ereal_pmf_map: "pmf (map_pmf f p) x = (\<integral>\<^sup>+ y. indicator (f -` {x}) y \<partial>measure_pmf p)"
1.176 +lemma ennreal_pmf_map: "pmf (map_pmf f p) x = (\<integral>\<^sup>+ y. indicator (f -` {x}) y \<partial>measure_pmf p)"
1.177  proof (transfer fixing: f x)
1.178    fix p :: "'b measure"
1.179    presume "prob_space p"
1.180    then interpret prob_space p .
1.181    presume "sets p = UNIV"
1.182 -  then show "ereal (measure (distr p (count_space UNIV) f) {x}) = integral\<^sup>N p (indicator (f -` {x}))"
1.183 +  then show "ennreal (measure (distr p (count_space UNIV) f) {x}) = integral\<^sup>N p (indicator (f -` {x}))"
1.184 +    by(simp add: measure_distr measurable_def emeasure_eq_measure)
1.185 +qed simp_all
1.186 +
1.187 +lemma pmf_map: "pmf (map_pmf f p) x = measure p (f -` {x})"
1.188 +proof (transfer fixing: f x)
1.189 +  fix p :: "'b measure"
1.190 +  presume "prob_space p"
1.191 +  then interpret prob_space p .
1.192 +  presume "sets p = UNIV"
1.193 +  then show "measure (distr p (count_space UNIV) f) {x} = measure p (f -` {x})"
1.194      by(simp add: measure_distr measurable_def emeasure_eq_measure)
1.195  qed simp_all
1.196
1.197 @@ -480,6 +498,11 @@
1.198    finally show ?thesis .
1.199  qed
1.200
1.201 +lemma integral_map_pmf[simp]:
1.202 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
1.203 +  shows "integral\<^sup>L (map_pmf g p) f = integral\<^sup>L p (\<lambda>x. f (g x))"
1.204 +  by (simp add: integral_distr map_pmf_rep_eq)
1.205 +
1.206  lemma map_return_pmf [simp]: "map_pmf f (return_pmf x) = return_pmf (f x)"
1.207    by transfer (simp add: distr_return)
1.208
1.209 @@ -529,15 +552,13 @@
1.210
1.211  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.212  proof -
1.213 -  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.214 -    by (subst nn_integral_max_0[symmetric])
1.215 -       (auto simp: AE_measure_pmf_iff intro!: nn_integral_cong_AE)
1.216 -  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.217 +  have "(\<integral>\<^sup>+x. f x \<partial>pair_pmf A B) = (\<integral>\<^sup>+x. f x * indicator (A \<times> B) x \<partial>pair_pmf A B)"
1.218 +    by (auto simp: AE_measure_pmf_iff intro!: nn_integral_cong_AE)
1.219 +  also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. f (a, b) * indicator (A \<times> B) (a, b) \<partial>B \<partial>A)"
1.221 -  also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. max 0 (f (a, b)) \<partial>B \<partial>A)"
1.222 +  also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. f (a, b) \<partial>B \<partial>A)"
1.223      by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff)
1.224 -  finally show ?thesis
1.225 -    unfolding nn_integral_max_0 .
1.226 +  finally show ?thesis .
1.227  qed
1.228
1.229  lemma bind_pair_pmf:
1.230 @@ -562,7 +583,7 @@
1.231    then show "emeasure ?L X = emeasure ?R X"
1.232      apply (simp add: emeasure_bind[OF _ M' X])
1.233      apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A]
1.234 -                     nn_integral_measure_pmf_finite emeasure_nonneg one_ereal_def[symmetric])
1.235 +                     nn_integral_measure_pmf_finite)
1.236      apply (subst emeasure_bind[OF _ _ X])
1.237      apply measurable
1.238      apply (subst emeasure_bind[OF _ _ X])
1.239 @@ -582,10 +603,10 @@
1.240       (auto simp: bij_betw_def nn_integral_pmf)
1.241
1.242  lemma pmf_le_0_iff[simp]: "pmf M p \<le> 0 \<longleftrightarrow> pmf M p = 0"
1.243 -  using pmf_nonneg[of M p] by simp
1.244 +  using pmf_nonneg[of M p] by arith
1.245
1.246  lemma min_pmf_0[simp]: "min (pmf M p) 0 = 0" "min 0 (pmf M p) = 0"
1.247 -  using pmf_nonneg[of M p] by simp_all
1.248 +  using pmf_nonneg[of M p] by arith+
1.249
1.250  lemma pmf_eq_0_set_pmf: "pmf M p = 0 \<longleftrightarrow> p \<notin> set_pmf M"
1.251    unfolding set_pmf_iff by simp
1.252 @@ -612,22 +633,22 @@
1.253    assumes prob: "(\<integral>\<^sup>+x. f x \<partial>count_space UNIV) = 1"
1.254  begin
1.255
1.256 -lift_definition embed_pmf :: "'a pmf" is "density (count_space UNIV) (ereal \<circ> f)"
1.257 +lift_definition embed_pmf :: "'a pmf" is "density (count_space UNIV) (ennreal \<circ> f)"
1.258  proof (intro conjI)
1.259 -  have *[simp]: "\<And>x y. ereal (f y) * indicator {x} y = ereal (f x) * indicator {x} y"
1.260 +  have *[simp]: "\<And>x y. ennreal (f y) * indicator {x} y = ennreal (f x) * indicator {x} y"
1.261      by (simp split: split_indicator)
1.262 -  show "AE x in density (count_space UNIV) (ereal \<circ> f).
1.263 -    measure (density (count_space UNIV) (ereal \<circ> f)) {x} \<noteq> 0"
1.264 +  show "AE x in density (count_space UNIV) (ennreal \<circ> f).
1.265 +    measure (density (count_space UNIV) (ennreal \<circ> f)) {x} \<noteq> 0"
1.266      by (simp add: AE_density nonneg measure_def emeasure_density max_def)
1.267 -  show "prob_space (density (count_space UNIV) (ereal \<circ> f))"
1.268 +  show "prob_space (density (count_space UNIV) (ennreal \<circ> f))"
1.269      by standard (simp add: emeasure_density prob)
1.270  qed simp
1.271
1.272  lemma pmf_embed_pmf: "pmf embed_pmf x = f x"
1.273  proof transfer
1.274 -  have *[simp]: "\<And>x y. ereal (f y) * indicator {x} y = ereal (f x) * indicator {x} y"
1.275 +  have *[simp]: "\<And>x y. ennreal (f y) * indicator {x} y = ennreal (f x) * indicator {x} y"
1.276      by (simp split: split_indicator)
1.277 -  fix x show "measure (density (count_space UNIV) (ereal \<circ> f)) {x} = f x"
1.278 +  fix x show "measure (density (count_space UNIV) (ennreal \<circ> f)) {x} = f x"
1.279      by transfer (simp add: measure_def emeasure_density nonneg max_def)
1.280  qed
1.281
1.282 @@ -637,17 +658,17 @@
1.283  end
1.284
1.285  lemma embed_pmf_transfer:
1.286 -  "rel_fun (eq_onp (\<lambda>f. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ereal (f x) \<partial>count_space UNIV) = 1)) pmf_as_measure.cr_pmf (\<lambda>f. density (count_space UNIV) (ereal \<circ> f)) embed_pmf"
1.287 +  "rel_fun (eq_onp (\<lambda>f. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ennreal (f x) \<partial>count_space UNIV) = 1)) pmf_as_measure.cr_pmf (\<lambda>f. density (count_space UNIV) (ennreal \<circ> f)) embed_pmf"
1.288    by (auto simp: rel_fun_def eq_onp_def embed_pmf.transfer)
1.289
1.290  lemma measure_pmf_eq_density: "measure_pmf p = density (count_space UNIV) (pmf p)"
1.291  proof (transfer, elim conjE)
1.292    fix M :: "'a measure" assume [simp]: "sets M = UNIV" and ae: "AE x in M. measure M {x} \<noteq> 0"
1.293    assume "prob_space M" then interpret prob_space M .
1.294 -  show "M = density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))"
1.295 +  show "M = density (count_space UNIV) (\<lambda>x. ennreal (measure M {x}))"
1.296    proof (rule measure_eqI)
1.297      fix A :: "'a set"
1.298 -    have "(\<integral>\<^sup>+ x. ereal (measure M {x}) * indicator A x \<partial>count_space UNIV) =
1.299 +    have "(\<integral>\<^sup>+ x. ennreal (measure M {x}) * indicator A x \<partial>count_space UNIV) =
1.300        (\<integral>\<^sup>+ x. emeasure M {x} * indicator (A \<inter> {x. measure M {x} \<noteq> 0}) x \<partial>count_space UNIV)"
1.301        by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator)
1.302      also have "\<dots> = (\<integral>\<^sup>+ x. emeasure M {x} \<partial>count_space (A \<inter> {x. measure M {x} \<noteq> 0}))"
1.303 @@ -657,19 +678,19 @@
1.304           (auto simp: disjoint_family_on_def)
1.305      also have "\<dots> = emeasure M A"
1.306        using ae by (intro emeasure_eq_AE) auto
1.307 -    finally show " emeasure M A = emeasure (density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))) A"
1.308 +    finally show " emeasure M A = emeasure (density (count_space UNIV) (\<lambda>x. ennreal (measure M {x}))) A"
1.309        using emeasure_space_1 by (simp add: emeasure_density)
1.310    qed simp
1.311  qed
1.312
1.313  lemma td_pmf_embed_pmf:
1.314 -  "type_definition pmf embed_pmf {f::'a \<Rightarrow> real. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ereal (f x) \<partial>count_space UNIV) = 1}"
1.315 +  "type_definition pmf embed_pmf {f::'a \<Rightarrow> real. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ennreal (f x) \<partial>count_space UNIV) = 1}"
1.316    unfolding type_definition_def
1.317  proof safe
1.318    fix p :: "'a pmf"
1.319    have "(\<integral>\<^sup>+ x. 1 \<partial>measure_pmf p) = 1"
1.320      using measure_pmf.emeasure_space_1[of p] by simp
1.321 -  then show *: "(\<integral>\<^sup>+ x. ereal (pmf p x) \<partial>count_space UNIV) = 1"
1.322 +  then show *: "(\<integral>\<^sup>+ x. ennreal (pmf p x) \<partial>count_space UNIV) = 1"
1.323      by (simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg del: nn_integral_const)
1.324
1.325    show "embed_pmf (pmf p) = p"
1.326 @@ -683,7 +704,7 @@
1.327
1.328  end
1.329
1.330 -lemma nn_integral_measure_pmf: "(\<integral>\<^sup>+ x. f x \<partial>measure_pmf p) = \<integral>\<^sup>+ x. ereal (pmf p x) * f x \<partial>count_space UNIV"
1.331 +lemma nn_integral_measure_pmf: "(\<integral>\<^sup>+ x. f x \<partial>measure_pmf p) = \<integral>\<^sup>+ x. ennreal (pmf p x) * f x \<partial>count_space UNIV"
1.332  by(simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg)
1.333
1.334  locale pmf_as_function
1.335 @@ -745,31 +766,31 @@
1.336  lemma pair_map_pmf1: "pair_pmf (map_pmf f A) B = map_pmf (apfst f) (pair_pmf A B)"
1.337  proof (safe intro!: pmf_eqI)
1.338    fix a :: "'a" and b :: "'b"
1.339 -  have [simp]: "\<And>c d. indicator (apfst f -` {(a, b)}) (c, d) = indicator (f -` {a}) c * (indicator {b} d::ereal)"
1.340 +  have [simp]: "\<And>c d. indicator (apfst f -` {(a, b)}) (c, d) = indicator (f -` {a}) c * (indicator {b} d::ennreal)"
1.341      by (auto split: split_indicator)
1.342
1.343 -  have "ereal (pmf (pair_pmf (map_pmf f A) B) (a, b)) =
1.344 -         ereal (pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b))"
1.345 -    unfolding pmf_pair ereal_pmf_map
1.346 +  have "ennreal (pmf (pair_pmf (map_pmf f A) B) (a, b)) =
1.347 +         ennreal (pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b))"
1.348 +    unfolding pmf_pair ennreal_pmf_map
1.349      by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_multc pmf_nonneg
1.350 -                  emeasure_map_pmf[symmetric] del: emeasure_map_pmf)
1.351 +                  emeasure_map_pmf[symmetric] ennreal_mult del: emeasure_map_pmf)
1.352    then show "pmf (pair_pmf (map_pmf f A) B) (a, b) = pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b)"
1.353 -    by simp
1.354 +    by (simp add: pmf_nonneg)
1.355  qed
1.356
1.357  lemma pair_map_pmf2: "pair_pmf A (map_pmf f B) = map_pmf (apsnd f) (pair_pmf A B)"
1.358  proof (safe intro!: pmf_eqI)
1.359    fix a :: "'a" and b :: "'b"
1.360 -  have [simp]: "\<And>c d. indicator (apsnd f -` {(a, b)}) (c, d) = indicator {a} c * (indicator (f -` {b}) d::ereal)"
1.361 +  have [simp]: "\<And>c d. indicator (apsnd f -` {(a, b)}) (c, d) = indicator {a} c * (indicator (f -` {b}) d::ennreal)"
1.362      by (auto split: split_indicator)
1.363
1.364 -  have "ereal (pmf (pair_pmf A (map_pmf f B)) (a, b)) =
1.365 -         ereal (pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b))"
1.366 -    unfolding pmf_pair ereal_pmf_map
1.367 +  have "ennreal (pmf (pair_pmf A (map_pmf f B)) (a, b)) =
1.368 +         ennreal (pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b))"
1.369 +    unfolding pmf_pair ennreal_pmf_map
1.370      by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_cmult nn_integral_multc pmf_nonneg
1.371 -                  emeasure_map_pmf[symmetric] del: emeasure_map_pmf)
1.372 +                  emeasure_map_pmf[symmetric] ennreal_mult del: emeasure_map_pmf)
1.373    then show "pmf (pair_pmf A (map_pmf f B)) (a, b) = pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b)"
1.374 -    by simp
1.375 +    by (simp add: pmf_nonneg)
1.376  qed
1.377
1.378  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.379 @@ -794,7 +815,7 @@
1.380    fix i
1.381    assume x: "set_pmf p \<subseteq> {x}"
1.382    hence *: "set_pmf p = {x}" using set_pmf_not_empty[of p] by auto
1.383 -  have "ereal (pmf p x) = \<integral>\<^sup>+ i. indicator {x} i \<partial>p" by(simp add: emeasure_pmf_single)
1.384 +  have "ennreal (pmf p x) = \<integral>\<^sup>+ i. indicator {x} i \<partial>p" by(simp add: emeasure_pmf_single)
1.385    also have "\<dots> = \<integral>\<^sup>+ i. 1 \<partial>p" by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * )
1.386    also have "\<dots> = 1" by simp
1.387    finally show "pmf p i = pmf (return_pmf x) i" using x
1.388 @@ -817,11 +838,14 @@
1.389    show ?lhs
1.390    proof(rule pmf_eqI)
1.391      fix i
1.392 -    have "ereal (pmf (bind_pmf p f) i) = \<integral>\<^sup>+ y. ereal (pmf (f y) i) \<partial>p" by(simp add: ereal_pmf_bind)
1.393 -    also have "\<dots> = \<integral>\<^sup>+ y. ereal (pmf (return_pmf x) i) \<partial>p"
1.394 +    have "ennreal (pmf (bind_pmf p f) i) = \<integral>\<^sup>+ y. ennreal (pmf (f y) i) \<partial>p"
1.395 +      by (simp add: ennreal_pmf_bind)
1.396 +    also have "\<dots> = \<integral>\<^sup>+ y. ennreal (pmf (return_pmf x) i) \<partial>p"
1.397        by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * )
1.398 -    also have "\<dots> = ereal (pmf (return_pmf x) i)" by simp
1.399 -    finally show "pmf (bind_pmf p f) i = pmf (return_pmf x) i" by simp
1.400 +    also have "\<dots> = ennreal (pmf (return_pmf x) i)"
1.401 +      by simp
1.402 +    finally show "pmf (bind_pmf p f) i = pmf (return_pmf x) i"
1.403 +      by (simp add: pmf_nonneg)
1.404    qed
1.405  qed
1.406
1.407 @@ -860,7 +884,7 @@
1.408  qed
1.409
1.410  lemma measure_measure_pmf_not_zero: "measure (measure_pmf p) s \<noteq> 0"
1.411 -  using emeasure_measure_pmf_not_zero unfolding measure_pmf.emeasure_eq_measure by simp
1.412 +  using emeasure_measure_pmf_not_zero by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg)
1.413
1.414  lift_definition cond_pmf :: "'a pmf" is
1.415    "uniform_measure (measure_pmf p) s"
1.416 @@ -869,7 +893,7 @@
1.417      by (intro prob_space_uniform_measure) (auto simp: emeasure_measure_pmf_not_zero)
1.418    show "AE x in uniform_measure (measure_pmf p) s. measure (uniform_measure (measure_pmf p) s) {x} \<noteq> 0"
1.419      by (simp add: emeasure_measure_pmf_not_zero measure_measure_pmf_not_zero AE_uniform_measure
1.420 -                  AE_measure_pmf_iff set_pmf.rep_eq)
1.421 +                  AE_measure_pmf_iff set_pmf.rep_eq less_top[symmetric])
1.422  qed simp
1.423
1.424  lemma pmf_cond: "pmf cond_pmf x = (if x \<in> s then pmf p x / measure p s else 0)"
1.425 @@ -887,20 +911,20 @@
1.426    have *: "set_pmf (map_pmf f p) \<inter> s \<noteq> {}"
1.427      using assms by auto
1.428    { fix x
1.429 -    have "ereal (pmf (map_pmf f (cond_pmf p (f -` s))) x) =
1.430 +    have "ennreal (pmf (map_pmf f (cond_pmf p (f -` s))) x) =
1.431        emeasure p (f -` s \<inter> f -` {x}) / emeasure p (f -` s)"
1.432 -      unfolding ereal_pmf_map cond_pmf.rep_eq[OF assms] by (simp add: nn_integral_uniform_measure)
1.433 +      unfolding ennreal_pmf_map cond_pmf.rep_eq[OF assms] by (simp add: nn_integral_uniform_measure)
1.434      also have "f -` s \<inter> f -` {x} = (if x \<in> s then f -` {x} else {})"
1.435        by auto
1.436      also have "emeasure p (if x \<in> s then f -` {x} else {}) / emeasure p (f -` s) =
1.437 -      ereal (pmf (cond_pmf (map_pmf f p) s) x)"
1.438 +      ennreal (pmf (cond_pmf (map_pmf f p) s) x)"
1.439        using measure_measure_pmf_not_zero[OF *]
1.440 -      by (simp add: pmf_cond[OF *] ereal_divide' ereal_pmf_map measure_pmf.emeasure_eq_measure[symmetric]
1.441 -               del: ereal_divide)
1.442 -    finally have "ereal (pmf (cond_pmf (map_pmf f p) s) x) = ereal (pmf (map_pmf f (cond_pmf p (f -` s))) x)"
1.443 +      by (simp add: pmf_cond[OF *] ennreal_pmf_map measure_pmf.emeasure_eq_measure
1.444 +                    divide_ennreal pmf_nonneg measure_nonneg zero_less_measure_iff pmf_map)
1.445 +    finally have "ennreal (pmf (cond_pmf (map_pmf f p) s) x) = ennreal (pmf (map_pmf f (cond_pmf p (f -` s))) x)"
1.446        by simp }
1.447    then show ?thesis
1.448 -    by (intro pmf_eqI) simp
1.449 +    by (intro pmf_eqI) (simp add: pmf_nonneg)
1.450  qed
1.451
1.452  lemma bind_cond_pmf_cancel:
1.453 @@ -910,16 +934,18 @@
1.454    shows "bind_pmf p (\<lambda>x. cond_pmf q {y. R x y}) = q"
1.455  proof (rule pmf_eqI)
1.456    fix i
1.457 -  have "ereal (pmf (bind_pmf p (\<lambda>x. cond_pmf q {y. R x y})) i) =
1.458 -    (\<integral>\<^sup>+x. ereal (pmf q i / measure p {x. R x i}) * ereal (indicator {x. R x i} x) \<partial>p)"
1.459 -    by (auto simp add: ereal_pmf_bind AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf intro!: nn_integral_cong_AE)
1.460 +  have "ennreal (pmf (bind_pmf p (\<lambda>x. cond_pmf q {y. R x y})) i) =
1.461 +    (\<integral>\<^sup>+x. ennreal (pmf q i / measure p {x. R x i}) * ennreal (indicator {x. R x i} x) \<partial>p)"
1.462 +    by (auto simp add: ennreal_pmf_bind AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf pmf_nonneg measure_nonneg
1.463 +             intro!: nn_integral_cong_AE)
1.464    also have "\<dots> = (pmf q i * measure p {x. R x i}) / measure p {x. R x i}"
1.465 -    by (simp add: pmf_nonneg measure_nonneg zero_ereal_def[symmetric] ereal_indicator
1.466 -                  nn_integral_cmult measure_pmf.emeasure_eq_measure)
1.467 +    by (simp add: pmf_nonneg measure_nonneg zero_ennreal_def[symmetric] ennreal_indicator
1.468 +                  nn_integral_cmult measure_pmf.emeasure_eq_measure ennreal_mult[symmetric])
1.469    also have "\<dots> = pmf q i"
1.470 -    by (cases "pmf q i = 0") (simp_all add: pmf_eq_0_set_pmf measure_measure_pmf_not_zero)
1.471 +    by (cases "pmf q i = 0")
1.472 +       (simp_all add: pmf_eq_0_set_pmf measure_measure_pmf_not_zero pmf_nonneg)
1.473    finally show "pmf (bind_pmf p (\<lambda>x. cond_pmf q {y. R x y})) i = pmf q i"
1.474 -    by simp
1.475 +    by (simp add: pmf_nonneg)
1.476  qed
1.477
1.478  subsection \<open> Relator \<close>
1.479 @@ -1277,8 +1303,8 @@
1.480  lemma pmf_join: "pmf (join_pmf N) i = (\<integral>M. pmf M i \<partial>measure_pmf N)"
1.481    unfolding join_pmf_def pmf_bind ..
1.482
1.483 -lemma ereal_pmf_join: "ereal (pmf (join_pmf N) i) = (\<integral>\<^sup>+M. pmf M i \<partial>measure_pmf N)"
1.484 -  unfolding join_pmf_def ereal_pmf_bind ..
1.485 +lemma ennreal_pmf_join: "ennreal (pmf (join_pmf N) i) = (\<integral>\<^sup>+M. pmf M i \<partial>measure_pmf N)"
1.486 +  unfolding join_pmf_def ennreal_pmf_bind ..
1.487
1.488  lemma set_pmf_join_pmf[simp]: "set_pmf (join_pmf f) = (\<Union>p\<in>set_pmf f. set_pmf p)"
1.490 @@ -1430,7 +1456,7 @@
1.491  lemma pmf_bernoulli_False[simp]: "0 \<le> p \<Longrightarrow> p \<le> 1 \<Longrightarrow> pmf (bernoulli_pmf p) False = 1 - p"
1.492    by transfer simp
1.493
1.494 -lemma set_pmf_bernoulli: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (bernoulli_pmf p) = UNIV"
1.495 +lemma set_pmf_bernoulli[simp]: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (bernoulli_pmf p) = UNIV"
1.496    by (auto simp add: set_pmf_iff UNIV_bool)
1.497
1.498  lemma nn_integral_bernoulli_pmf[simp]:
1.499 @@ -1448,7 +1474,10 @@
1.500  by(cases x) simp_all
1.501
1.502  lemma measure_pmf_bernoulli_half: "measure_pmf (bernoulli_pmf (1 / 2)) = uniform_count_measure UNIV"
1.503 -by(rule measure_eqI)(simp_all add: nn_integral_pmf[symmetric] emeasure_uniform_count_measure nn_integral_count_space_finite sets_uniform_count_measure)
1.504 +  by (rule measure_eqI)
1.505 +     (simp_all add: nn_integral_pmf[symmetric] emeasure_uniform_count_measure ennreal_divide_numeral[symmetric]
1.506 +                    nn_integral_count_space_finite sets_uniform_count_measure divide_ennreal_def mult_ac
1.507 +                    ennreal_of_nat_eq_real_of_nat)
1.508
1.509  subsubsection \<open> Geometric Distribution \<close>
1.510
1.511 @@ -1458,9 +1487,9 @@
1.512
1.513  lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. (1 - p)^n * p"
1.514  proof
1.515 -  have "(\<Sum>i. ereal (p * (1 - p) ^ i)) = ereal (p * (1 / (1 - (1 - p))))"
1.516 -    by (intro sums_suminf_ereal sums_mult geometric_sums) auto
1.517 -  then show "(\<integral>\<^sup>+ x. ereal ((1 - p)^x * p) \<partial>count_space UNIV) = 1"
1.518 +  have "(\<Sum>i. ennreal (p * (1 - p) ^ i)) = ennreal (p * (1 / (1 - (1 - p))))"
1.519 +    by (intro suminf_ennreal_eq sums_mult geometric_sums) auto
1.520 +  then show "(\<integral>\<^sup>+ x. ennreal ((1 - p)^x * p) \<partial>count_space UNIV) = 1"
1.521      by (simp add: nn_integral_count_space_nat field_simps)
1.522  qed simp
1.523
1.524 @@ -1480,7 +1509,7 @@
1.525
1.526  lift_definition pmf_of_multiset :: "'a pmf" is "\<lambda>x. count M x / size M"
1.527  proof
1.528 -  show "(\<integral>\<^sup>+ x. ereal (real (count M x) / real (size M)) \<partial>count_space UNIV) = 1"
1.529 +  show "(\<integral>\<^sup>+ x. ennreal (real (count M x) / real (size M)) \<partial>count_space UNIV) = 1"
1.530      using M_not_empty
1.531      by (simp add: zero_less_divide_iff nn_integral_count_space nonempty_has_size
1.532                    setsum_divide_distrib[symmetric])
1.533 @@ -1503,8 +1532,10 @@
1.534
1.535  lift_definition pmf_of_set :: "'a pmf" is "\<lambda>x. indicator S x / card S"
1.536  proof
1.537 -  show "(\<integral>\<^sup>+ x. ereal (indicator S x / real (card S)) \<partial>count_space UNIV) = 1"
1.538 -    using S_not_empty S_finite by (subst nn_integral_count_space'[of S]) auto
1.539 +  show "(\<integral>\<^sup>+ x. ennreal (indicator S x / real (card S)) \<partial>count_space UNIV) = 1"
1.540 +    using S_not_empty S_finite
1.541 +    by (subst nn_integral_count_space'[of S])
1.542 +       (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_mult[symmetric])
1.543  qed simp
1.544
1.545  lemma pmf_of_set[simp]: "pmf pmf_of_set x = indicator S x / card S"
1.546 @@ -1516,38 +1547,22 @@
1.547  lemma emeasure_pmf_of_set_space[simp]: "emeasure pmf_of_set S = 1"
1.548    by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff)
1.549
1.550 -lemma nn_integral_pmf_of_set':
1.551 -  "(\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0) \<Longrightarrow> nn_integral (measure_pmf pmf_of_set) f = setsum f S / card S"
1.552 -apply(subst nn_integral_measure_pmf_finite, simp_all add: S_finite)
1.554 -apply(subst ereal_divide', simp add: S_not_empty S_finite)
1.556 -done
1.557 +lemma nn_integral_pmf_of_set: "nn_integral (measure_pmf pmf_of_set) f = setsum f S / card S"
1.558 +  by (subst nn_integral_measure_pmf_finite)
1.559 +     (simp_all add: setsum_left_distrib[symmetric] card_gt_0_iff S_not_empty S_finite divide_ennreal_def
1.560 +                divide_ennreal[symmetric] ennreal_of_nat_eq_real_of_nat[symmetric] ennreal_times_divide)
1.561
1.562 -lemma nn_integral_pmf_of_set:
1.563 -  "nn_integral (measure_pmf pmf_of_set) f = setsum (max 0 \<circ> f) S / card S"
1.564 -apply(subst nn_integral_max_0[symmetric])
1.565 -apply(subst nn_integral_pmf_of_set')
1.566 -apply simp_all
1.567 -done
1.568 +lemma integral_pmf_of_set: "integral\<^sup>L (measure_pmf pmf_of_set) f = setsum f S / card S"
1.569 +  by (subst integral_measure_pmf[of S]) (auto simp: S_finite setsum_divide_distrib)
1.570
1.571 -lemma integral_pmf_of_set:
1.572 -  "integral\<^sup>L (measure_pmf pmf_of_set) f = setsum f S / card S"
1.573 -apply(simp add: real_lebesgue_integral_def integrable_measure_pmf_finite nn_integral_pmf_of_set S_finite)
1.574 -apply(subst real_of_ereal_minus')
1.575 - apply(simp add: ereal_max_0 S_finite del: ereal_max)
1.576 -apply(simp add: ereal_max_0 S_finite S_not_empty del: ereal_max)
1.577 -apply(simp add: field_simps S_finite S_not_empty)
1.578 -apply(subst setsum.distrib[symmetric])
1.579 -apply(rule setsum.cong; simp_all)
1.580 -done
1.581 +lemma emeasure_pmf_of_set: "emeasure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
1.582 +  by (subst nn_integral_indicator[symmetric], simp)
1.583 +     (simp add: S_finite S_not_empty card_gt_0_iff indicator_def setsum.If_cases divide_ennreal
1.584 +                ennreal_of_nat_eq_real_of_nat nn_integral_pmf_of_set)
1.585
1.586 -lemma emeasure_pmf_of_set:
1.587 -  "emeasure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
1.588 -apply(subst nn_integral_indicator[symmetric], simp)
1.589 -apply(subst nn_integral_pmf_of_set)
1.590 -apply(simp add: o_def max_def ereal_indicator[symmetric] S_not_empty S_finite real_of_nat_indicator[symmetric] of_nat_setsum[symmetric] setsum_indicator_eq_card del: of_nat_setsum)
1.591 -done
1.592 +lemma measure_pmf_of_set: "measure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
1.593 +  using emeasure_pmf_of_set[OF assms, of A]
1.594 +  by (simp add: measure_nonneg measure_pmf.emeasure_eq_measure)
1.595
1.596  end
1.597
1.598 @@ -1574,15 +1589,7 @@
1.599  qed
1.600
1.601  lemma bernoulli_pmf_half_conv_pmf_of_set: "bernoulli_pmf (1 / 2) = pmf_of_set UNIV"
1.602 -by(rule pmf_eqI) simp_all
1.603 -
1.604 -
1.605 -
1.606 -lemma measure_pmf_of_set:
1.607 -  assumes "S \<noteq> {}" "finite S"
1.608 -  shows "measure (measure_pmf (pmf_of_set S)) A = card (S \<inter> A) / card S"
1.609 -using emeasure_pmf_of_set[OF assms, of A]
1.610 -unfolding measure_pmf.emeasure_eq_measure by simp
1.611 +  by (rule pmf_eqI) simp_all
1.612
1.613  subsubsection \<open> Poisson Distribution \<close>
1.614
1.615 @@ -1596,14 +1603,14 @@
1.616      by (simp add: field_simps divide_inverse [symmetric])
1.617    have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x * exp (-rate) \<partial>count_space UNIV) =
1.618            exp (-rate) * (\<integral>\<^sup>+(x::nat). rate ^ x / fact x \<partial>count_space UNIV)"
1.619 -    by (simp add: field_simps nn_integral_cmult[symmetric])
1.620 +    by (simp add: field_simps nn_integral_cmult[symmetric] ennreal_mult'[symmetric])
1.621    also from rate_pos have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x \<partial>count_space UNIV) = (\<Sum>x. rate ^ x / fact x)"
1.622 -    by (simp_all add: nn_integral_count_space_nat suminf_ereal summable suminf_ereal_finite)
1.623 +    by (simp_all add: nn_integral_count_space_nat suminf_ennreal summable ennreal_suminf_neq_top)
1.624    also have "... = exp rate" unfolding exp_def
1.625      by (simp add: field_simps divide_inverse [symmetric])
1.626 -  also have "ereal (exp (-rate)) * ereal (exp rate) = 1"
1.627 -    by (simp add: mult_exp_exp)
1.628 -  finally show "(\<integral>\<^sup>+ x. ereal (rate ^ x / (fact x) * exp (- rate)) \<partial>count_space UNIV) = 1" .
1.629 +  also have "ennreal (exp (-rate)) * ennreal (exp rate) = 1"
1.630 +    by (simp add: mult_exp_exp ennreal_mult[symmetric])
1.631 +  finally show "(\<integral>\<^sup>+ x. ennreal (rate ^ x / (fact x) * exp (- rate)) \<partial>count_space UNIV) = 1" .
1.632  qed (simp add: rate_pos[THEN less_imp_le])
1.633
1.634  lemma pmf_poisson[simp]: "pmf poisson_pmf k = rate ^ k / fact k * exp (-rate)"
1.635 @@ -1622,12 +1629,12 @@
1.636
1.637  lift_definition binomial_pmf :: "nat pmf" is "\<lambda>k. (n choose k) * p^k * (1 - p)^(n - k)"
1.638  proof
1.639 -  have "(\<integral>\<^sup>+k. ereal (real (n choose k) * p ^ k * (1 - p) ^ (n - k)) \<partial>count_space UNIV) =
1.640 -    ereal (\<Sum>k\<le>n. real (n choose k) * p ^ k * (1 - p) ^ (n - k))"
1.641 +  have "(\<integral>\<^sup>+k. ennreal (real (n choose k) * p ^ k * (1 - p) ^ (n - k)) \<partial>count_space UNIV) =
1.642 +    ennreal (\<Sum>k\<le>n. real (n choose k) * p ^ k * (1 - p) ^ (n - k))"
1.643      using p_le_1 p_nonneg by (subst nn_integral_count_space') auto
1.644    also have "(\<Sum>k\<le>n. real (n choose k) * p ^ k * (1 - p) ^ (n - k)) = (p + (1 - p)) ^ n"
1.645      by (subst binomial_ring) (simp add: atLeast0AtMost)
1.646 -  finally show "(\<integral>\<^sup>+ x. ereal (real (n choose x) * p ^ x * (1 - p) ^ (n - x)) \<partial>count_space UNIV) = 1"
1.647 +  finally show "(\<integral>\<^sup>+ x. ennreal (real (n choose x) * p ^ x * (1 - p) ^ (n - x)) \<partial>count_space UNIV) = 1"
1.648      by simp
1.649  qed (insert p_nonneg p_le_1, simp)
1.650
```