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.52    by (simp add: pmf.rep_eq)
    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.220      by (simp add: pair_pmf_def)
   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.489    by (simp add: join_pmf_def)
   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.553 -apply(simp add: setsum_ereal_left_distrib[symmetric])
   1.554 -apply(subst ereal_divide', simp add: S_not_empty S_finite)
   1.555 -apply(simp add: ereal_times_divide_eq one_ereal_def[symmetric])
   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