# HG changeset patch
# User hoelzl
# Date 1400502418 -7200
# Node ID 891e992e510fd111b2d08a0beb2eba0d52bbb037
# Parent  61855ade6c7e55694b7569ec01584a0585835376
renamed positive_integral to nn_integral

diff -r 61855ade6c7e -r 891e992e510f NEWS
--- a/NEWS	Mon May 19 13:53:58 2014 +0200
+++ b/NEWS	Mon May 19 14:26:58 2014 +0200
@@ -733,6 +733,13 @@
     integral_cmul_indicator
     integral_real
 
+  - Renamed positive_integral to nn_integral:
+
+    * Renamed all lemmas "*positive_integral*" to *nn_integral*"
+      positive_integral_positive ~> nn_integral_nonneg
+
+    * Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
+
 *** Scala ***
 
 * The signature and semantics of Document.Snapshot.cumulate_markup /
diff -r 61855ade6c7e -r 891e992e510f src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Mon May 19 13:53:58 2014 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Mon May 19 14:26:58 2014 +0200
@@ -239,7 +239,7 @@
   shows "emeasure (N \<Otimes>\<^sub>M M) X = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. indicator X (x, y) \<partial>M \<partial>N)" (is "_ = ?\<mu> X")
 proof (rule emeasure_measure_of[OF pair_measure_def])
   show "positive (sets (N \<Otimes>\<^sub>M M)) ?\<mu>"
-    by (auto simp: positive_def positive_integral_positive)
+    by (auto simp: positive_def nn_integral_nonneg)
   have eq[simp]: "\<And>A x y. indicator A (x, y) = indicator (Pair x -` A) y"
     by (auto simp: indicator_def)
   show "countably_additive (sets (N \<Otimes>\<^sub>M M)) ?\<mu>"
@@ -253,8 +253,8 @@
     moreover have "\<And>x. range (\<lambda>i. Pair x -` F i) \<subseteq> sets M"
       using F by (auto simp: sets_Pair1)
     ultimately show "(\<Sum>n. ?\<mu> (F n)) = ?\<mu> (\<Union>i. F i)"
-      by (auto simp add: vimage_UN positive_integral_suminf[symmetric] suminf_emeasure subset_eq emeasure_nonneg sets_Pair1
-               intro!: positive_integral_cong positive_integral_indicator[symmetric])
+      by (auto simp add: vimage_UN nn_integral_suminf[symmetric] suminf_emeasure subset_eq emeasure_nonneg sets_Pair1
+               intro!: nn_integral_cong nn_integral_indicator[symmetric])
   qed
   show "{a \<times> b |a b. a \<in> sets N \<and> b \<in> sets M} \<subseteq> Pow (space N \<times> space M)"
     using sets.space_closed[of N] sets.space_closed[of M] by auto
@@ -267,7 +267,7 @@
   have [simp]: "\<And>x y. indicator X (x, y) = indicator (Pair x -` X) y"
     by (auto simp: indicator_def)
   show ?thesis
-    using X by (auto intro!: positive_integral_cong simp: emeasure_pair_measure sets_Pair1)
+    using X by (auto intro!: nn_integral_cong simp: emeasure_pair_measure sets_Pair1)
 qed
 
 lemma (in sigma_finite_measure) emeasure_pair_measure_Times:
@@ -275,9 +275,9 @@
   shows "emeasure (N \<Otimes>\<^sub>M M) (A \<times> B) = emeasure N A * emeasure M B"
 proof -
   have "emeasure (N \<Otimes>\<^sub>M M) (A \<times> B) = (\<integral>\<^sup>+x. emeasure M B * indicator A x \<partial>N)"
-    using A B by (auto intro!: positive_integral_cong simp: emeasure_pair_measure_alt)
+    using A B by (auto intro!: nn_integral_cong simp: emeasure_pair_measure_alt)
   also have "\<dots> = emeasure M B * emeasure N A"
-    using A by (simp add: emeasure_nonneg positive_integral_cmult_indicator)
+    using A by (simp add: emeasure_nonneg nn_integral_cmult_indicator)
   finally show ?thesis
     by (simp add: ac_simps)
 qed
@@ -418,7 +418,7 @@
   proof (rule AE_I)
     from N measurable_emeasure_Pair1[OF `N \<in> sets (M1 \<Otimes>\<^sub>M M2)`]
     show "emeasure M1 {x\<in>space M1. emeasure M2 (Pair x -` N) \<noteq> 0} = 0"
-      by (auto simp: M2.emeasure_pair_measure_alt positive_integral_0_iff emeasure_nonneg)
+      by (auto simp: M2.emeasure_pair_measure_alt nn_integral_0_iff emeasure_nonneg)
     show "{x \<in> space M1. emeasure M2 (Pair x -` N) \<noteq> 0} \<in> sets M1"
       by (intro borel_measurable_ereal_neq_const measurable_emeasure_Pair1 N)
     { fix x assume "x \<in> space M1" "emeasure M2 (Pair x -` N) = 0"
@@ -446,9 +446,9 @@
     by (simp add: M2.emeasure_pair_measure)
   also have "\<dots> = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. 0 \<partial>M2 \<partial>M1)"
     using ae
-    apply (safe intro!: positive_integral_cong_AE)
+    apply (safe intro!: nn_integral_cong_AE)
     apply (intro AE_I2)
-    apply (safe intro!: positive_integral_cong_AE)
+    apply (safe intro!: nn_integral_cong_AE)
     apply auto
     done
   finally show "emeasure (M1 \<Otimes>\<^sub>M M2) {x \<in> space (M1 \<Otimes>\<^sub>M M2). \<not> P x} = 0" by simp
@@ -486,7 +486,7 @@
   "x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^sub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L"
   by simp
 
-lemma (in sigma_finite_measure) borel_measurable_positive_integral_fst':
+lemma (in sigma_finite_measure) borel_measurable_nn_integral_fst':
   assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)" "\<And>x. 0 \<le> f x"
   shows "(\<lambda>x. \<integral>\<^sup>+ y. f (x, y) \<partial>M) \<in> borel_measurable M1"
 using f proof induct
@@ -495,7 +495,7 @@
     by (auto simp: space_pair_measure)
   show ?case
     apply (subst measurable_cong)
-    apply (rule positive_integral_cong)
+    apply (rule nn_integral_cong)
     apply fact+
     done
 next
@@ -506,56 +506,56 @@
     by (simp add: sets_Pair1[OF set])
   from this measurable_emeasure_Pair[OF set] show ?case
     by (rule measurable_cong[THEN iffD1])
-qed (simp_all add: positive_integral_add positive_integral_cmult measurable_compose_Pair1
-                   positive_integral_monotone_convergence_SUP incseq_def le_fun_def
+qed (simp_all add: nn_integral_add nn_integral_cmult measurable_compose_Pair1
+                   nn_integral_monotone_convergence_SUP incseq_def le_fun_def
               cong: measurable_cong)
 
-lemma (in sigma_finite_measure) positive_integral_fst':
+lemma (in sigma_finite_measure) nn_integral_fst':
   assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)" "\<And>x. 0 \<le> f x"
-  shows "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>M \<partial>M1) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M) f" (is "?I f = _")
+  shows "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>M \<partial>M1) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M) f" (is "?I f = _")
 using f proof induct
   case (cong u v)
   then have "?I u = ?I v"
-    by (intro positive_integral_cong) (auto simp: space_pair_measure)
+    by (intro nn_integral_cong) (auto simp: space_pair_measure)
   with cong show ?case
-    by (simp cong: positive_integral_cong)
-qed (simp_all add: emeasure_pair_measure positive_integral_cmult positive_integral_add
-                   positive_integral_monotone_convergence_SUP
-                   measurable_compose_Pair1 positive_integral_positive
-                   borel_measurable_positive_integral_fst' positive_integral_mono incseq_def le_fun_def
-              cong: positive_integral_cong)
+    by (simp cong: nn_integral_cong)
+qed (simp_all add: emeasure_pair_measure nn_integral_cmult nn_integral_add
+                   nn_integral_monotone_convergence_SUP
+                   measurable_compose_Pair1 nn_integral_nonneg
+                   borel_measurable_nn_integral_fst' nn_integral_mono incseq_def le_fun_def
+              cong: nn_integral_cong)
 
-lemma (in sigma_finite_measure) positive_integral_fst:
+lemma (in sigma_finite_measure) nn_integral_fst:
   assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)"
-  shows "(\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x, y) \<partial>M) \<partial>M1) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M) f"
+  shows "(\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x, y) \<partial>M) \<partial>M1) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M) f"
   using f
-    borel_measurable_positive_integral_fst'[of "\<lambda>x. max 0 (f x)"]
-    positive_integral_fst'[of "\<lambda>x. max 0 (f x)"]
-  unfolding positive_integral_max_0 by auto
+    borel_measurable_nn_integral_fst'[of "\<lambda>x. max 0 (f x)"]
+    nn_integral_fst'[of "\<lambda>x. max 0 (f x)"]
+  unfolding nn_integral_max_0 by auto
 
-lemma (in sigma_finite_measure) borel_measurable_positive_integral[measurable (raw)]:
+lemma (in sigma_finite_measure) borel_measurable_nn_integral[measurable (raw)]:
   "split f \<in> borel_measurable (N \<Otimes>\<^sub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^sup>+ y. f x y \<partial>M) \<in> borel_measurable N"
-  using borel_measurable_positive_integral_fst'[of "\<lambda>x. max 0 (split f x)" N]
-  by (simp add: positive_integral_max_0)
+  using borel_measurable_nn_integral_fst'[of "\<lambda>x. max 0 (split f x)" N]
+  by (simp add: nn_integral_max_0)
 
-lemma (in pair_sigma_finite) positive_integral_snd:
+lemma (in pair_sigma_finite) nn_integral_snd:
   assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
-  shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M2) f"
+  shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M2) f"
 proof -
   note measurable_pair_swap[OF f]
-  from M1.positive_integral_fst[OF this]
+  from M1.nn_integral_fst[OF this]
   have "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^sub>M M1))"
     by simp
-  also have "(\<integral>\<^sup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^sub>M M1)) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M2) f"
+  also have "(\<integral>\<^sup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^sub>M M1)) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M2) f"
     by (subst distr_pair_swap)
-       (auto simp: positive_integral_distr[OF measurable_pair_swap' f] intro!: positive_integral_cong)
+       (auto simp: nn_integral_distr[OF measurable_pair_swap' f] intro!: nn_integral_cong)
   finally show ?thesis .
 qed
 
 lemma (in pair_sigma_finite) Fubini:
   assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
   shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x, y) \<partial>M2) \<partial>M1)"
-  unfolding positive_integral_snd[OF assms] M2.positive_integral_fst[OF assms] ..
+  unfolding nn_integral_snd[OF assms] M2.nn_integral_fst[OF assms] ..
 
 subsection {* Products on counting spaces, densities and distributions *}
 
@@ -602,7 +602,7 @@
     apply (subst emeasure_count_space)
     using X_subset apply auto []
     apply (simp add: fin_Pair emeasure_count_space X_subset fin_X)
-    apply (subst positive_integral_count_space)
+    apply (subst nn_integral_count_space)
     using A apply simp
     apply (simp del: real_of_nat_setsum add: real_of_nat_setsum[symmetric])
     apply (subst card_gt_0_iff)
@@ -626,12 +626,12 @@
   fix A assume A: "A \<in> sets ?L"
   with f g have "(\<integral>\<^sup>+ x. f x * \<integral>\<^sup>+ y. g y * indicator A (x, y) \<partial>M2 \<partial>M1) =
     (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f x * g y * indicator A (x, y) \<partial>M2 \<partial>M1)"
-    by (intro positive_integral_cong_AE)
-       (auto simp add: positive_integral_cmult[symmetric] ac_simps)
+    by (intro nn_integral_cong_AE)
+       (auto simp add: nn_integral_cmult[symmetric] ac_simps)
   with A f g show "emeasure ?L A = emeasure ?R A"
-    by (simp add: D2.emeasure_pair_measure emeasure_density positive_integral_density
-                  M2.positive_integral_fst[symmetric]
-             cong: positive_integral_cong)
+    by (simp add: D2.emeasure_pair_measure emeasure_density nn_integral_density
+                  M2.nn_integral_fst[symmetric]
+             cong: nn_integral_cong)
 qed simp
 
 lemma sigma_finite_measure_distr:
@@ -662,8 +662,8 @@
   fix A assume A: "A \<in> sets ?P"
   with f g show "emeasure ?P A = emeasure ?D A"
     by (auto simp add: N.emeasure_pair_measure_alt space_pair_measure emeasure_distr
-                       T.emeasure_pair_measure_alt positive_integral_distr
-             intro!: positive_integral_cong arg_cong[where f="emeasure N"])
+                       T.emeasure_pair_measure_alt nn_integral_distr
+             intro!: nn_integral_cong arg_cong[where f="emeasure N"])
 qed simp
 
 lemma pair_measure_eqI:
diff -r 61855ade6c7e -r 891e992e510f src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Mon May 19 13:53:58 2014 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy	Mon May 19 14:26:58 2014 +0200
@@ -284,10 +284,10 @@
 
   from m have "m * emeasure M {x\<in>space M. 0 \<noteq> f x} = 
     (\<integral>\<^sup>+x. m * indicator {x\<in>space M. 0 \<noteq> f x} x \<partial>M)"
-    using f by (intro positive_integral_cmult_indicator[symmetric]) auto
+    using f by (intro nn_integral_cmult_indicator[symmetric]) auto
   also have "\<dots> \<le> (\<integral>\<^sup>+x. f x \<partial>M)"
     using AE_space
-  proof (intro positive_integral_mono_AE, eventually_elim)
+  proof (intro nn_integral_mono_AE, eventually_elim)
     fix x assume "x \<in> space M"
     with nn show "m * indicator {x \<in> space M. 0 \<noteq> f x} x \<le> f x"
       using f by (auto split: split_indicator simp: simple_function_def m_def)
@@ -447,7 +447,7 @@
   finally show ?thesis .
 qed
 
-lemma simple_bochner_integral_eq_positive_integral:
+lemma simple_bochner_integral_eq_nn_integral:
   assumes f: "simple_bochner_integrable M f" "\<And>x. 0 \<le> f x"
   shows "simple_bochner_integral M f = (\<integral>\<^sup>+x. f x \<partial>M)"
 proof -
@@ -479,7 +479,7 @@
              simp del: setsum_ereal times_ereal.simps(1))
   also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)"
     using f
-    by (intro positive_integral_eq_simple_integral[symmetric])
+    by (intro nn_integral_eq_simple_integral[symmetric])
        (auto simp: simple_function_compose1 simple_bochner_integrable.simps)
   finally show ?thesis .
 qed
@@ -502,13 +502,13 @@
     by (auto intro!: simple_bochner_integral_norm_bound)
   also have "\<dots> = (\<integral>\<^sup>+x. norm (s x - t x) \<partial>M)"
     using simple_bochner_integrable_compose2[of "\<lambda>x y. norm (x - y)" M "s" "t"] s t
-    by (auto intro!: simple_bochner_integral_eq_positive_integral)
+    by (auto intro!: simple_bochner_integral_eq_nn_integral)
   also have "\<dots> \<le> (\<integral>\<^sup>+x. ereal (norm (f x - s x)) + ereal (norm (f x - t x)) \<partial>M)"
-    by (auto intro!: positive_integral_mono)
+    by (auto intro!: nn_integral_mono)
        (metis (erased, hide_lams) add_diff_cancel_left add_diff_eq diff_add_eq order_trans
               norm_minus_commute norm_triangle_ineq4 order_refl)
   also have "\<dots> = ?S + ?T"
-   by (rule positive_integral_add) auto
+   by (rule nn_integral_add) auto
   finally show ?thesis .
 qed
 
@@ -524,14 +524,14 @@
   assumes "M = N" "\<And>x. x \<in> space N \<Longrightarrow> f x = g x" "x = y"
   shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral N g y"
   unfolding has_bochner_integral.simps assms(1,3)
-  using assms(2) by (simp cong: measurable_cong_strong positive_integral_cong_strong)
+  using assms(2) by (simp cong: measurable_cong_strong nn_integral_cong_strong)
 
 lemma has_bochner_integral_cong_AE:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow>
     has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
   unfolding has_bochner_integral.simps
   by (intro arg_cong[where f=Ex] ext conj_cong rev_conj_cong refl arg_cong[where f="\<lambda>x. x ----> 0"]
-            positive_integral_cong_AE)
+            nn_integral_cong_AE)
      auto
 
 lemma borel_measurable_has_bochner_integral[measurable_dest]:
@@ -557,7 +557,7 @@
       using A by auto
   qed (rule simple_function_indicator assms)+
   moreover have "simple_bochner_integral M (indicator A) = measure M A"
-    using simple_bochner_integral_eq_positive_integral[OF sbi] A
+    using simple_bochner_integral_eq_nn_integral[OF sbi] A
     by (simp add: ereal_indicator emeasure_eq_ereal_measure)
   ultimately show ?thesis
     by (metis has_bochner_integral_simple_bochner_integrable)
@@ -584,14 +584,14 @@
     (is "?f ----> 0")
   proof (rule tendsto_sandwich)
     show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) ----> 0"
-      by (auto simp: positive_integral_positive)
+      by (auto simp: nn_integral_nonneg)
     show "eventually (\<lambda>i. ?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) \<partial>M) + \<integral>\<^sup>+ x. (norm (g x - sg i x)) \<partial>M) sequentially"
       (is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
     proof (intro always_eventually allI)
       fix i have "?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) + ereal (norm (g x - sg i x)) \<partial>M)"
-        by (auto intro!: positive_integral_mono norm_diff_triangle_ineq)
+        by (auto intro!: nn_integral_mono norm_diff_triangle_ineq)
       also have "\<dots> = ?g i"
-        by (intro positive_integral_add) auto
+        by (intro nn_integral_add) auto
       finally show "?f i \<le> ?g i" .
     qed
     show "?g ----> 0"
@@ -625,15 +625,15 @@
     (is "?f ----> 0")
   proof (rule tendsto_sandwich)
     show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) ----> 0"
-      by (auto simp: positive_integral_positive)
+      by (auto simp: nn_integral_nonneg)
 
     show "eventually (\<lambda>i. ?f i \<le> K * (\<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M)) sequentially"
       (is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
     proof (intro always_eventually allI)
       fix i have "?f i \<le> (\<integral>\<^sup>+ x. ereal K * norm (f x - s i x) \<partial>M)"
-        using K by (intro positive_integral_mono) (auto simp: mult_ac)
+        using K by (intro nn_integral_mono) (auto simp: mult_ac)
       also have "\<dots> = ?g i"
-        using K by (intro positive_integral_cmult) auto
+        using K by (intro nn_integral_cmult) auto
       finally show "?f i \<le> ?g i" .
     qed
     show "?g ----> 0"
@@ -738,15 +738,15 @@
   then have "\<And>x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> m" "0 \<le> m"
     by (auto simp: m_def image_comp comp_def Max_ge_iff)
   then have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. ereal m * indicator {x\<in>space M. s i x \<noteq> 0} x \<partial>M)"
-    by (auto split: split_indicator intro!: Max_ge positive_integral_mono simp:)
+    by (auto split: split_indicator intro!: Max_ge nn_integral_mono simp:)
   also have "\<dots> < \<infinity>"
-    using s by (subst positive_integral_cmult_indicator) (auto simp: `0 \<le> m` simple_bochner_integrable.simps)
+    using s by (subst nn_integral_cmult_indicator) (auto simp: `0 \<le> m` simple_bochner_integrable.simps)
   finally have s_fin: "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>" .
 
   have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x - s i x)) + ereal (norm (s i x)) \<partial>M)"
-    by (auto intro!: positive_integral_mono) (metis add_commute norm_triangle_sub)
+    by (auto intro!: nn_integral_mono) (metis add_commute norm_triangle_sub)
   also have "\<dots> = (\<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) + (\<integral>\<^sup>+x. norm (s i x) \<partial>M)"
-    by (rule positive_integral_add) auto
+    by (rule nn_integral_add) auto
   also have "\<dots> < \<infinity>"
     using s_fin f_s_fin by auto
   finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" .
@@ -776,13 +776,13 @@
       have "ereal (norm (?s n)) \<le> simple_bochner_integral M (\<lambda>x. norm (s n x))"
         by (auto intro!: simple_bochner_integral_norm_bound)
       also have "\<dots> = (\<integral>\<^sup>+x. norm (s n x) \<partial>M)"
-        by (intro simple_bochner_integral_eq_positive_integral)
+        by (intro simple_bochner_integral_eq_nn_integral)
            (auto intro: s simple_bochner_integrable_compose2)
       also have "\<dots> \<le> (\<integral>\<^sup>+x. ereal (norm (f x - s n x)) + norm (f x) \<partial>M)"
-        by (auto intro!: positive_integral_mono)
+        by (auto intro!: nn_integral_mono)
            (metis add_commute norm_minus_commute norm_triangle_sub)
       also have "\<dots> = ?t n" 
-        by (rule positive_integral_add) auto
+        by (rule nn_integral_add) auto
       finally show "norm (?s n) \<le> ?t n" .
     qed
     have "?t ----> 0 + (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
@@ -816,7 +816,7 @@
   have "(\<lambda>i. ereal (norm (?s i - ?t i))) ----> ereal 0"
   proof (rule tendsto_sandwich)
     show "eventually (\<lambda>i. 0 \<le> ereal (norm (?s i - ?t i))) sequentially" "(\<lambda>_. 0) ----> ereal 0"
-      by (auto simp: positive_integral_positive zero_ereal_def[symmetric])
+      by (auto simp: nn_integral_nonneg zero_ereal_def[symmetric])
 
     show "eventually (\<lambda>i. norm (?s i - ?t i) \<le> ?S i + ?T i) sequentially"
       by (intro always_eventually allI simple_bochner_integral_bounded s t f)
@@ -841,7 +841,7 @@
   fix s assume "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
   also have "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) = (\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x - s i x)) \<partial>M)"
     using ae
-    by (intro ext positive_integral_cong_AE, eventually_elim) simp
+    by (intro ext nn_integral_cong_AE, eventually_elim) simp
   finally show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x - s i x)) \<partial>M) ----> 0" .
 qed (auto intro: g)
 
@@ -1087,7 +1087,7 @@
         by (intro simple_bochner_integral_bounded s f)
       also have "\<dots> < ereal (e / 2) + e / 2"
         using ereal_add_strict_mono[OF less_imp_le[OF M[OF n]] _ `?S n \<noteq> \<infinity>` M[OF m]]
-        by (auto simp: positive_integral_positive)
+        by (auto simp: nn_integral_nonneg)
       also have "\<dots> = e" by simp
       finally show "dist (?s n) (?s m) < e"
         by (simp add: dist_norm)
@@ -1098,7 +1098,7 @@
     by (rule, rule) fact+
 qed
 
-lemma positive_integral_dominated_convergence_norm:
+lemma nn_integral_dominated_convergence_norm:
   fixes u' :: "_ \<Rightarrow> _::{real_normed_vector, second_countable_topology}"
   assumes [measurable]:
        "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
@@ -1122,9 +1122,9 @@
   qed
   
   have "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) ----> (\<integral>\<^sup>+x. 0 \<partial>M)"
-  proof (rule positive_integral_dominated_convergence)  
+  proof (rule nn_integral_dominated_convergence)  
     show "(\<integral>\<^sup>+x. 2 * w x \<partial>M) < \<infinity>"
-      by (rule positive_integral_mult_bounded_inf[OF _ w, of 2]) auto
+      by (rule nn_integral_mult_bounded_inf[OF _ w, of 2]) auto
     show "AE x in M. (\<lambda>i. ereal (norm (u' x - u i x))) ----> 0"
       using u' 
     proof eventually_elim
@@ -1152,9 +1152,9 @@
   proof (rule integrableI_sequence)
     { fix i
       have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. 2 * ereal (norm (f x)) \<partial>M)"
-        by (intro positive_integral_mono) (simp add: bound)
+        by (intro nn_integral_mono) (simp add: bound)
       also have "\<dots> = 2 * (\<integral>\<^sup>+x. ereal (norm (f x)) \<partial>M)"
-        by (rule positive_integral_cmult) auto
+        by (rule nn_integral_cmult) auto
       finally have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>"
         using fin by auto }
     note fin_s = this
@@ -1163,13 +1163,13 @@
       by (rule simple_bochner_integrableI_bounded) fact+
 
     show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
-    proof (rule positive_integral_dominated_convergence_norm)
+    proof (rule nn_integral_dominated_convergence_norm)
       show "\<And>j. AE x in M. norm (s j x) \<le> 2 * norm (f x)"
         using bound by auto
       show "\<And>i. s i \<in> borel_measurable M" "(\<lambda>x. 2 * norm (f x)) \<in> borel_measurable M"
         using s by (auto intro: borel_measurable_simple_function)
       show "(\<integral>\<^sup>+ x. ereal (2 * norm (f x)) \<partial>M) < \<infinity>"
-        using fin unfolding times_ereal.simps(1)[symmetric] by (subst positive_integral_cmult) auto
+        using fin unfolding times_ereal.simps(1)[symmetric] by (subst nn_integral_cmult) auto
       show "AE x in M. (\<lambda>i. s i x) ----> f x"
         using pointwise by auto
     qed fact
@@ -1182,7 +1182,7 @@
   shows "integrable M f"
 proof -
   have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
-    using assms by (intro positive_integral_cong_AE) auto
+    using assms by (intro nn_integral_cong_AE) auto
   then show ?thesis
     using assms by (intro integrableI_bounded) auto
 qed
@@ -1203,7 +1203,7 @@
   assume "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   assume "AE x in M. norm (g x) \<le> norm (f x)"
   then have "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
-    by  (intro positive_integral_mono_AE) auto
+    by  (intro nn_integral_mono_AE) auto
   also assume "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
   finally show "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) < \<infinity>" .
 qed 
@@ -1249,7 +1249,7 @@
 
 lemma integrable_indicator_iff:
   "integrable M (indicator A::_ \<Rightarrow> real) \<longleftrightarrow> A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
-  by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ereal_indicator positive_integral_indicator'
+  by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ereal_indicator nn_integral_indicator'
            cong: conj_cong)
 
 lemma integral_dominated_convergence:
@@ -1264,7 +1264,7 @@
   have "AE x in M. 0 \<le> w x"
     using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans)
   then have "(\<integral>\<^sup>+x. w x \<partial>M) = (\<integral>\<^sup>+x. norm (w x) \<partial>M)"
-    by (intro positive_integral_cong_AE) auto
+    by (intro nn_integral_cong_AE) auto
   with `integrable M w` have w: "w \<in> borel_measurable M" "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
     unfolding integrable_iff_bounded by auto
 
@@ -1273,7 +1273,7 @@
   proof
     fix i 
     have "(\<integral>\<^sup>+ x. ereal (norm (s i x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
-      using bound by (intro positive_integral_mono_AE) auto
+      using bound by (intro nn_integral_mono_AE) auto
     with w show "(\<integral>\<^sup>+ x. ereal (norm (s i x)) \<partial>M) < \<infinity>" by auto
   qed fact
 
@@ -1285,7 +1285,7 @@
   proof
     have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
       using all_bound lim
-    proof (intro positive_integral_mono_AE, eventually_elim)
+    proof (intro nn_integral_mono_AE, eventually_elim)
       fix x assume "\<forall>i. norm (s i x) \<le> w x" "(\<lambda>i. s i x) ----> f x"
       then show "ereal (norm (f x)) \<le> ereal (w x)"
         by (intro LIMSEQ_le_const2[where X="\<lambda>i. ereal (norm (s i x))"] tendsto_intros lim_ereal[THEN iffD2]) auto
@@ -1308,7 +1308,7 @@
     show "(\<lambda>n. \<integral>\<^sup>+x. norm (s n x - f x) \<partial>M) ----> ereal 0"
       unfolding zero_ereal_def[symmetric]
       apply (subst norm_minus_commute)
-    proof (rule positive_integral_dominated_convergence_norm[where w=w])
+    proof (rule nn_integral_dominated_convergence_norm[where w=w])
       show "\<And>n. s n \<in> borel_measurable M"
         using int_s unfolding integrable_iff_bounded by auto
     qed fact+
@@ -1325,7 +1325,7 @@
   using integrable_mult_left[of c M f] integrable_mult_left[of "1 / c" M "\<lambda>x. c * f x"]
   by (cases "c = 0") auto
 
-lemma positive_integral_eq_integral:
+lemma nn_integral_eq_integral:
   assumes f: "integrable M f"
   assumes nonneg: "AE x in M. 0 \<le> f x" 
   shows "(\<integral>\<^sup>+ x. f x \<partial>M) = integral\<^sup>L M f"
@@ -1338,7 +1338,7 @@
     next
       case (mult f c) then show ?case
         unfolding times_ereal.simps(1)[symmetric]
-        by (subst positive_integral_cmult)
+        by (subst nn_integral_cmult)
            (auto simp add: integrable_mult_left_iff zero_ereal_def[symmetric])
     next
       case (add g f)
@@ -1346,7 +1346,7 @@
         by (auto intro!: integrable_bound[OF add(8)])
       with add show ?case
         unfolding plus_ereal.simps(1)[symmetric]
-        by (subst positive_integral_add) auto
+        by (subst nn_integral_add) auto
     next
       case (seq s)
       { fix i x assume "x \<in> space M" with seq(4) have "s i x \<le> f x"
@@ -1366,7 +1366,7 @@
           using seq f s_le_f by (intro integrable_bound[OF f(3)]) auto
         have "(\<lambda>i. \<integral>\<^sup>+ x. s i x \<partial>M) ----> \<integral>\<^sup>+ x. f x \<partial>M"
           using seq s_le_f f
-          by (intro positive_integral_dominated_convergence[where w=f])
+          by (intro nn_integral_dominated_convergence[where w=f])
              (auto simp: integrable_iff_bounded)
         also have "(\<lambda>i. \<integral>\<^sup>+x. s i x \<partial>M) = (\<lambda>i. \<integral>x. s i x \<partial>M)"
           using seq int_s by simp
@@ -1379,19 +1379,19 @@
   also have "\<dots> = integral\<^sup>L M f"
     using assms by (auto intro!: integral_cong_AE)
   also have "(\<integral>\<^sup>+ x. max 0 (f x) \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M)"
-    using assms by (auto intro!: positive_integral_cong_AE simp: max_def)
+    using assms by (auto intro!: nn_integral_cong_AE simp: max_def)
   finally show ?thesis .
 qed
 
 lemma integral_norm_bound:
   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   shows "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
-  using positive_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
+  using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
   using integral_norm_bound_ereal[of M f] by simp
   
-lemma integral_eq_positive_integral:
+lemma integral_eq_nn_integral:
   "integrable M f \<Longrightarrow> (\<And>x. 0 \<le> f x) \<Longrightarrow> integral\<^sup>L M f = real (\<integral>\<^sup>+ x. ereal (f x) \<partial>M)"
-  by (subst positive_integral_eq_integral) auto
+  by (subst nn_integral_eq_integral) auto
   
 lemma integrableI_simple_bochner_integrable:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
@@ -1445,9 +1445,9 @@
     fix i
 
     have "(\<integral>\<^sup>+x. norm (s' i x) \<partial>M) \<le> (\<integral>\<^sup>+x. 2 * ereal (norm (f x)) \<partial>M)"
-      using s by (intro positive_integral_mono) (auto simp: s'_eq_s)
+      using s by (intro nn_integral_mono) (auto simp: s'_eq_s)
     also have "\<dots> < \<infinity>"
-      using f by (subst positive_integral_cmult) auto
+      using f by (subst nn_integral_cmult) auto
     finally have sbi: "simple_bochner_integrable M (s' i)"
       using sf by (intro simple_bochner_integrableI_bounded) auto
     then show "integrable M (s' i)"
@@ -1475,8 +1475,8 @@
   shows "0 \<le> integral\<^sup>L M f"
 proof -
   have "0 \<le> ereal (integral\<^sup>L M (\<lambda>x. max 0 (f x)))"
-    by (subst integral_eq_positive_integral)
-       (auto intro: real_of_ereal_pos positive_integral_positive integrable_max assms)
+    by (subst integral_eq_nn_integral)
+       (auto intro: real_of_ereal_pos nn_integral_nonneg integrable_max assms)
   also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = integral\<^sup>L M f"
     using assms(2) by (intro integral_cong_AE assms integrable_max) auto
   finally show ?thesis
@@ -1493,10 +1493,10 @@
   shows "integral\<^sup>L M f = 0 \<longleftrightarrow> (AE x in M. f x = 0)"
 proof
   assume "integral\<^sup>L M f = 0"
-  then have "integral\<^sup>P M f = 0"
-    using positive_integral_eq_integral[OF f nonneg] by simp
+  then have "integral\<^sup>N M f = 0"
+    using nn_integral_eq_integral[OF f nonneg] by simp
   then have "AE x in M. ereal (f x) \<le> 0"
-    by (simp add: positive_integral_0_iff_AE)
+    by (simp add: nn_integral_0_iff_AE)
   with nonneg show "AE x in M. f x = 0"
     by auto
 qed (auto simp add: integral_eq_zero_AE)
@@ -1527,8 +1527,8 @@
     and nn: "AE x in M. 0 \<le> g x"
   shows "integrable (density M g) f \<longleftrightarrow> integrable M (\<lambda>x. g x *\<^sub>R f x)"
   unfolding integrable_iff_bounded using nn
-  apply (simp add: positive_integral_density )
-  apply (intro arg_cong2[where f="op ="] refl positive_integral_cong_AE)
+  apply (simp add: nn_integral_density )
+  apply (intro arg_cong2[where f="op ="] refl nn_integral_cong_AE)
   apply auto
   done
 
@@ -1547,9 +1547,9 @@
     have int: "integrable M (\<lambda>x. g x * indicator A x)"
       using g base integrable_density[of "indicator A :: 'a \<Rightarrow> real" M g] by simp
     then have "integral\<^sup>L M (\<lambda>x. g x * indicator A x) = (\<integral>\<^sup>+ x. ereal (g x * indicator A x) \<partial>M)"
-      using g by (subst positive_integral_eq_integral) auto
+      using g by (subst nn_integral_eq_integral) auto
     also have "\<dots> = (\<integral>\<^sup>+ x. ereal (g x) * indicator A x \<partial>M)"
-      by (intro positive_integral_cong) (auto split: split_indicator)
+      by (intro nn_integral_cong) (auto split: split_indicator)
     also have "\<dots> = emeasure (density M g) A"
       by (rule emeasure_density[symmetric]) auto
     also have "\<dots> = ereal (measure (density M g) A)"
@@ -1607,7 +1607,7 @@
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes [measurable]: "g \<in> measurable M N" "f \<in> borel_measurable N"
   shows "integrable (distr M N g) f \<longleftrightarrow> integrable M (\<lambda>x. f (g x))"
-  unfolding integrable_iff_bounded by (simp_all add: positive_integral_distr)
+  unfolding integrable_iff_bounded by (simp_all add: nn_integral_distr)
 
 lemma integrable_distr:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
@@ -1678,7 +1678,7 @@
 lemma integrable_count_space:
   fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
   shows "finite X \<Longrightarrow> integrable (count_space X) f"
-  by (auto simp: positive_integral_count_space integrable_iff_bounded)
+  by (auto simp: nn_integral_count_space integrable_iff_bounded)
 
 lemma measure_count_space[simp]:
   "B \<subseteq> A \<Longrightarrow> finite B \<Longrightarrow> measure (count_space A) B = card B"
@@ -1731,15 +1731,15 @@
   also have "\<dots> = integral\<^sup>L M (\<lambda>x. max 0 (f x)) - integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
     by (intro integral_diff integrable_max integrable_minus integrable_zero f)
   also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = real (\<integral>\<^sup>+x. max 0 (f x) \<partial>M)"
-    by (subst integral_eq_positive_integral[symmetric]) (auto intro!: integrable_max f)
+    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: integrable_max f)
   also have "integral\<^sup>L M (\<lambda>x. max 0 (- f x)) = real (\<integral>\<^sup>+x. max 0 (- f x) \<partial>M)"
-    by (subst integral_eq_positive_integral[symmetric]) (auto intro!: integrable_max f)
+    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: integrable_max f)
   also have "(\<lambda>x. ereal (max 0 (f x))) = (\<lambda>x. max 0 (ereal (f x)))"
     by (auto simp: max_def)
   also have "(\<lambda>x. ereal (max 0 (- f x))) = (\<lambda>x. max 0 (- ereal (f x)))"
     by (auto simp: max_def)
   finally show ?thesis
-    unfolding positive_integral_max_0 .
+    unfolding nn_integral_max_0 .
 qed
 
 lemma real_integrable_def:
@@ -1749,12 +1749,12 @@
 proof (safe del: notI)
   assume *: "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
   have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
-    by (intro positive_integral_mono) auto
+    by (intro nn_integral_mono) auto
   also note *
   finally show "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>"
     by simp
   have "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
-    by (intro positive_integral_mono) auto
+    by (intro nn_integral_mono) auto
   also note *
   finally show "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
     by simp
@@ -1762,11 +1762,11 @@
   assume [measurable]: "f \<in> borel_measurable M"
   assume fin: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
   have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. max 0 (ereal (f x)) + max 0 (ereal (- f x)) \<partial>M)"
-    by (intro positive_integral_cong) (auto simp: max_def)
+    by (intro nn_integral_cong) (auto simp: max_def)
   also have"\<dots> = (\<integral>\<^sup>+ x. max 0 (ereal (f x)) \<partial>M) + (\<integral>\<^sup>+ x. max 0 (ereal (- f x)) \<partial>M)"
-    by (intro positive_integral_add) auto
+    by (intro nn_integral_add) auto
   also have "\<dots> < \<infinity>"
-    using fin by (auto simp: positive_integral_max_0)
+    using fin by (auto simp: nn_integral_max_0)
   finally show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity>" .
 qed
 
@@ -1782,8 +1782,8 @@
     "(\<integral>\<^sup>+x. ereal (-f x)\<partial>M) = ereal q"
     "f \<in> borel_measurable M" "integral\<^sup>L M f = r - q"
   using assms unfolding real_integrable_def real_lebesgue_integral_def[OF assms]
-  using positive_integral_positive[of M "\<lambda>x. ereal (f x)"]
-  using positive_integral_positive[of M "\<lambda>x. ereal (-f x)"]
+  using nn_integral_nonneg[of M "\<lambda>x. ereal (f x)"]
+  using nn_integral_nonneg[of M "\<lambda>x. ereal (-f x)"]
   by (cases rule: ereal2_cases[of "(\<integral>\<^sup>+x. ereal (-f x)\<partial>M)" "(\<integral>\<^sup>+x. ereal (f x)\<partial>M)"]) auto
 
 lemma integral_monotone_convergence_nonneg:
@@ -1797,7 +1797,7 @@
   and "integral\<^sup>L M u = x"
 proof -
   have "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = (SUP n. (\<integral>\<^sup>+ x. ereal (f n x) \<partial>M))"
-  proof (subst positive_integral_monotone_convergence_SUP_AE[symmetric])
+  proof (subst nn_integral_monotone_convergence_SUP_AE[symmetric])
     fix i
     from mono pos show "AE x in M. ereal (f i x) \<le> ereal (f (Suc i) x) \<and> 0 \<le> ereal (f i x)"
       by eventually_elim (auto simp: mono_def)
@@ -1805,16 +1805,16 @@
       using i by auto
   next
     show "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = \<integral>\<^sup>+ x. (SUP i. ereal (f i x)) \<partial>M"
-      apply (rule positive_integral_cong_AE)
+      apply (rule nn_integral_cong_AE)
       using lim mono
       by eventually_elim (simp add: SUP_eq_LIMSEQ[THEN iffD2])
   qed
   also have "\<dots> = ereal x"
-    using mono i unfolding positive_integral_eq_integral[OF i pos]
+    using mono i unfolding nn_integral_eq_integral[OF i pos]
     by (subst SUP_eq_LIMSEQ) (auto simp: mono_def intro!: integral_mono_AE ilim)
   finally have "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = ereal x" .
   moreover have "(\<integral>\<^sup>+ x. ereal (- u x) \<partial>M) = 0"
-  proof (subst positive_integral_0_iff_AE)
+  proof (subst nn_integral_0_iff_AE)
     show "(\<lambda>x. ereal (- u x)) \<in> borel_measurable M"
       using u by auto
     from mono pos[of 0] lim show "AE x in M. ereal (- u x) \<le> 0"
@@ -1865,11 +1865,11 @@
   shows "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
 proof -
   have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>x. norm (f x) \<partial>M)"
-    using f by (intro positive_integral_eq_integral integrable_norm) auto
+    using f by (intro nn_integral_eq_integral integrable_norm) auto
   then have "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) = 0"
     by simp
   also have "\<dots> \<longleftrightarrow> emeasure M {x\<in>space M. ereal (norm (f x)) \<noteq> 0} = 0"
-    by (intro positive_integral_0_iff) auto
+    by (intro nn_integral_0_iff) auto
   finally show ?thesis
     by simp
 qed
@@ -1917,7 +1917,7 @@
       using int by (simp add: integral_0_iff)
     moreover
     have "(\<integral>\<^sup>+x. indicator A x \<partial>M) \<le> (\<integral>\<^sup>+x. indicator {x \<in> space M. Y x - X x \<noteq> 0} x \<partial>M)"
-      using A by (intro positive_integral_mono_AE) auto
+      using A by (intro nn_integral_mono_AE) auto
     then have "(emeasure M) A \<le> (emeasure M) {x \<in> space M. Y x - X x \<noteq> 0}"
       using int A by (simp add: integrable_def)
     ultimately have "emeasure M A = 0"
@@ -2221,7 +2221,7 @@
             by (intro simple_function_borel_measurable)
                (auto simp: space_pair_measure dest: finite_subset)
           have "(\<integral>\<^sup>+ y. ereal (norm (s i (x, y))) \<partial>M) \<le> (\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M)"
-            using x s by (intro positive_integral_mono) auto
+            using x s by (intro nn_integral_mono) auto
           also have "(\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M) < \<infinity>"
             using int_2f by (simp add: integrable_iff_bounded)
           finally show "(\<integral>\<^sup>+ xa. ereal (norm (s i (x, xa))) \<partial>M) < \<infinity>" .
@@ -2276,7 +2276,7 @@
   have "(\<integral>\<^sup>+ x. emeasure M2 (Pair x -` A) \<partial>M1) \<noteq> \<infinity>"
     by simp
   then have "AE x in M1. emeasure M2 (Pair x -` A) \<noteq> \<infinity>"
-    by (rule positive_integral_PInf_AE[rotated]) (intro M2.measurable_emeasure_Pair A)
+    by (rule nn_integral_PInf_AE[rotated]) (intro M2.measurable_emeasure_Pair A)
   moreover have "\<And>x. x \<in> space M1 \<Longrightarrow> Pair x -` A = {y\<in>space M2. (x, y) \<in> A}"
     using sets.sets_into_space[OF A] by (auto simp: space_pair_measure)
   ultimately show ?thesis by auto
@@ -2288,11 +2288,11 @@
   shows "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
 proof -
   have "(\<integral>\<^sup>+x. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<partial>M1) = (\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2))"
-    by (rule M2.positive_integral_fst) simp
+    by (rule M2.nn_integral_fst) simp
   also have "(\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2)) \<noteq> \<infinity>"
     using f unfolding integrable_iff_bounded by simp
   finally have "AE x in M1. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<noteq> \<infinity>"
-    by (intro positive_integral_PInf_AE M2.borel_measurable_positive_integral )
+    by (intro nn_integral_PInf_AE M2.borel_measurable_nn_integral )
        (auto simp: measurable_split_conv)
   with AE_space show ?thesis
     by eventually_elim
@@ -2308,9 +2308,9 @@
   show "(\<lambda>x. \<integral> y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
     by (rule M2.borel_measurable_lebesgue_integral) simp
   have "(\<integral>\<^sup>+ x. ereal (norm (\<integral> y. f (x, y) \<partial>M2)) \<partial>M1) \<le> (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<partial>M1)"
-    using AE_integrable_fst'[OF f] by (auto intro!: positive_integral_mono_AE integral_norm_bound_ereal)
+    using AE_integrable_fst'[OF f] by (auto intro!: nn_integral_mono_AE integral_norm_bound_ereal)
   also have "(\<integral>\<^sup>+x. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<partial>M1) = (\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2))"
-    by (rule M2.positive_integral_fst) simp
+    by (rule M2.nn_integral_fst) simp
   also have "(\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2)) < \<infinity>"
     using f unfolding integrable_iff_bounded by simp
   finally show "(\<integral>\<^sup>+ x. ereal (norm (\<integral> y. f (x, y) \<partial>M2)) \<partial>M1) < \<infinity>" .
@@ -2341,18 +2341,18 @@
     have "(\<integral>\<^sup>+x. ereal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1) =
       (\<integral>\<^sup>+x. emeasure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1)"
       using emeasure_pair_measure_finite[OF base]
-      by (intro positive_integral_cong_AE, eventually_elim) (simp add: emeasure_eq_ereal_measure)
+      by (intro nn_integral_cong_AE, eventually_elim) (simp add: emeasure_eq_ereal_measure)
     also have "\<dots> = emeasure (M1 \<Otimes>\<^sub>M M2) A"
       using sets.sets_into_space[OF A]
       by (subst M2.emeasure_pair_measure_alt)
-         (auto intro!: positive_integral_cong arg_cong[where f="emeasure M2"] simp: space_pair_measure)
+         (auto intro!: nn_integral_cong arg_cong[where f="emeasure M2"] simp: space_pair_measure)
     finally have *: "(\<integral>\<^sup>+x. ereal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1) = emeasure (M1 \<Otimes>\<^sub>M M2) A" .
 
     from base * show "integrable M1 (\<lambda>x. measure M2 {y \<in> space M2. (x, y) \<in> A})"
       by (simp add: measure_nonneg integrable_iff_bounded)
     then have "(\<integral>x. measure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1) = 
       (\<integral>\<^sup>+x. ereal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1)"
-      by (rule positive_integral_eq_integral[symmetric]) (simp add: measure_nonneg)
+      by (rule nn_integral_eq_integral[symmetric]) (simp add: measure_nonneg)
     also note *
     finally show "(\<integral>x. measure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1) *\<^sub>R c = measure (M1 \<Otimes>\<^sub>M M2) A *\<^sub>R c"
       using base by (simp add: emeasure_eq_ereal_measure)
@@ -2417,9 +2417,9 @@
         from s have "norm (\<integral> y. s i (x, y) \<partial>M2) \<le> (\<integral>\<^sup>+y. norm (s i (x, y)) \<partial>M2)"
           by (rule integral_norm_bound_ereal)
         also have "\<dots> \<le> (\<integral>\<^sup>+y. 2 * norm (f (x, y)) \<partial>M2)"
-          using x lim by (auto intro!: positive_integral_mono simp: space_pair_measure)
+          using x lim by (auto intro!: nn_integral_mono simp: space_pair_measure)
         also have "\<dots> = (\<integral>y. 2 * norm (f (x, y)) \<partial>M2)"
-          using f by (intro positive_integral_eq_integral) auto
+          using f by (intro nn_integral_eq_integral) auto
         finally show "norm (\<integral> y. s i (x, y) \<partial>M2) \<le> (\<integral> y. 2 * norm (f (x, y)) \<partial>M2)"
           by simp
       qed
@@ -2530,9 +2530,9 @@
       (\<integral>\<^sup>+ x. (\<Prod>i\<in>I. ereal (norm (f i (x i)))) \<partial>Pi\<^sub>M I M)"
     by (simp add: setprod_norm setprod_ereal)
   also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+ x. ereal (norm (f i x)) \<partial>M i)"
-    using assms by (intro product_positive_integral_setprod) auto
+    using assms by (intro product_nn_integral_setprod) auto
   also have "\<dots> < \<infinity>"
-    using integrable by (simp add: setprod_PInf positive_integral_positive integrable_iff_bounded)
+    using integrable by (simp add: setprod_PInf nn_integral_nonneg integrable_iff_bounded)
   finally show "(\<integral>\<^sup>+ x. ereal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) < \<infinity>" .
 qed
 
@@ -2568,7 +2568,7 @@
   have "f \<in> borel_measurable M"
     using assms by (auto simp: measurable_def)
   with assms show ?thesis
-    using assms by (auto simp: integrable_iff_bounded positive_integral_subalgebra)
+    using assms by (auto simp: integrable_iff_bounded nn_integral_subalgebra)
 qed
 
 lemma integral_subalgebra:
diff -r 61855ade6c7e -r 891e992e510f src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Mon May 19 13:53:58 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy	Mon May 19 14:26:58 2014 +0200
@@ -56,9 +56,9 @@
 
   have "emeasure ?D (space ?D) = (\<integral>\<^sup>+ x. ereal (?f x) * indicator {0..} x \<partial>lborel)"
     by (auto simp: emeasure_density exponential_density_def
-             intro!: positive_integral_cong split: split_indicator)
+             intro!: nn_integral_cong split: split_indicator)
   also have "\<dots> = ereal (0 - ?F 0)"
-  proof (rule positive_integral_FTC_atLeast)
+  proof (rule nn_integral_FTC_atLeast)
     have "((\<lambda>x. exp (l * x)) ---> 0) at_bot"
       by (rule filterlim_compose[OF exp_at_bot filterlim_tendsto_pos_mult_at_bot[of _ l]])
          (simp_all add: tendsto_const filterlim_ident)
@@ -72,10 +72,10 @@
 
   assume "0 \<le> a"
   have "emeasure ?D {..a} = (\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel)"
-    by (auto simp add: emeasure_density intro!: positive_integral_cong split: split_indicator)
+    by (auto simp add: emeasure_density intro!: nn_integral_cong split: split_indicator)
        (auto simp: exponential_density_def)
   also have "(\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel) = ereal (?F a) - ereal (?F 0)"
-    using `0 \<le> a` deriv by (intro positive_integral_FTC_atLeastAtMost) auto
+    using `0 \<le> a` deriv by (intro nn_integral_FTC_atLeastAtMost) auto
   also have "\<dots> = 1 - exp (- a * l)"
     by simp
   finally show "emeasure ?D {.. a} = 1 - exp (- a * l)" .
@@ -241,9 +241,9 @@
      by simp
   also have "\<dots> = (\<integral>\<^sup>+ x. (1 / emeasure M' A) * indicator (A \<inter> B) x \<partial>M')"
     using A B
-    by (intro positive_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal)
+    by (intro nn_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal)
   also have "\<dots> = (\<integral>\<^sup>+ x. ?f x * indicator B x \<partial>M')"
-    by (rule positive_integral_cong) (auto split: split_indicator)
+    by (rule nn_integral_cong) (auto split: split_indicator)
   finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B"
     using A B X by (auto simp add: emeasure_distr emeasure_density)
 qed simp
@@ -271,10 +271,10 @@
  
   have "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) =
     (\<integral>\<^sup>+ x. ereal (1 / measure lborel A) * indicator (A \<inter> {..a}) x \<partial>lborel)"
-    by (auto intro!: positive_integral_cong split: split_indicator)
+    by (auto intro!: nn_integral_cong split: split_indicator)
   also have "\<dots> = ereal (1 / measure lborel A) * emeasure lborel (A \<inter> {..a})"
     using `A \<in> sets borel`
-    by (intro positive_integral_cmult_indicator) (auto simp: measure_nonneg)
+    by (intro nn_integral_cmult_indicator) (auto simp: measure_nonneg)
   also have "\<dots> = ereal (measure lborel (A \<inter> {..a}) / r)"
     unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def)
   finally show "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) =
@@ -331,10 +331,10 @@
     using distributed_borel_measurable[OF D] `a \<le> t` `t \<le> b`
     unfolding distributed_distr_eq_density[OF D]
     by (subst emeasure_density)
-       (auto intro!: positive_integral_cong simp: measure_def split: split_indicator)
+       (auto intro!: nn_integral_cong simp: measure_def split: split_indicator)
   also have "\<dots> = ereal (1 / (b - a)) * (t - a)"
     using `a \<le> t` `t \<le> b`
-    by (subst positive_integral_cmult_indicator) auto
+    by (subst nn_integral_cmult_indicator) auto
   finally show ?thesis
     by (simp add: measure_def)
 qed
diff -r 61855ade6c7e -r 891e992e510f src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Mon May 19 13:53:58 2014 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Mon May 19 14:26:58 2014 +0200
@@ -688,15 +688,15 @@
   "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (Pi\<^sub>M I M) (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
   using emeasure_PiM[OF finite_index] by auto
 
-lemma (in product_sigma_finite) positive_integral_empty:
+lemma (in product_sigma_finite) nn_integral_empty:
   assumes pos: "0 \<le> f (\<lambda>k. undefined)"
-  shows "integral\<^sup>P (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
+  shows "integral\<^sup>N (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
 proof -
   interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI)
   have "\<And>A. emeasure (Pi\<^sub>M {} M) (Pi\<^sub>E {} A) = 1"
     using assms by (subst measure_times) auto
   then show ?thesis
-    unfolding positive_integral_def simple_function_def simple_integral_def[abs_def]
+    unfolding nn_integral_def simple_function_def simple_integral_def[abs_def]
   proof (simp add: space_PiM_empty sets_PiM_empty, intro antisym)
     show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
       by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
@@ -768,10 +768,10 @@
   qed
 qed
 
-lemma (in product_sigma_finite) product_positive_integral_fold:
+lemma (in product_sigma_finite) product_nn_integral_fold:
   assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
   and f: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
-  shows "integral\<^sup>P (Pi\<^sub>M (I \<union> J) M) f =
+  shows "integral\<^sup>N (Pi\<^sub>M (I \<union> J) M) f =
     (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^sub>M J M)) \<partial>(Pi\<^sub>M I M))"
 proof -
   interpret I: finite_product_sigma_finite M I by default fact
@@ -781,8 +781,8 @@
     using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
   show ?thesis
     apply (subst distr_merge[OF IJ, symmetric])
-    apply (subst positive_integral_distr[OF measurable_merge f])
-    apply (subst J.positive_integral_fst[symmetric, OF P_borel])
+    apply (subst nn_integral_distr[OF measurable_merge f])
+    apply (subst J.nn_integral_fst[symmetric, OF P_borel])
     apply simp
     done
 qed
@@ -799,30 +799,30 @@
     by (simp add: emeasure_distr measurable_component_singleton)
 qed simp
 
-lemma (in product_sigma_finite) product_positive_integral_singleton:
+lemma (in product_sigma_finite) product_nn_integral_singleton:
   assumes f: "f \<in> borel_measurable (M i)"
-  shows "integral\<^sup>P (Pi\<^sub>M {i} M) (\<lambda>x. f (x i)) = integral\<^sup>P (M i) f"
+  shows "integral\<^sup>N (Pi\<^sub>M {i} M) (\<lambda>x. f (x i)) = integral\<^sup>N (M i) f"
 proof -
   interpret I: finite_product_sigma_finite M "{i}" by default simp
   from f show ?thesis
     apply (subst distr_singleton[symmetric])
-    apply (subst positive_integral_distr[OF measurable_component_singleton])
+    apply (subst nn_integral_distr[OF measurable_component_singleton])
     apply simp_all
     done
 qed
 
-lemma (in product_sigma_finite) product_positive_integral_insert:
+lemma (in product_sigma_finite) product_nn_integral_insert:
   assumes I[simp]: "finite I" "i \<notin> I"
     and f: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
-  shows "integral\<^sup>P (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x(i := y)) \<partial>(M i)) \<partial>(Pi\<^sub>M I M))"
+  shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x(i := y)) \<partial>(M i)) \<partial>(Pi\<^sub>M I M))"
 proof -
   interpret I: finite_product_sigma_finite M I by default auto
   interpret i: finite_product_sigma_finite M "{i}" by default auto
   have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
     using f by auto
   show ?thesis
-    unfolding product_positive_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f]
-  proof (rule positive_integral_cong, subst product_positive_integral_singleton[symmetric])
+    unfolding product_nn_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f]
+  proof (rule nn_integral_cong, subst product_nn_integral_singleton[symmetric])
     fix x assume x: "x \<in> space (Pi\<^sub>M I M)"
     let ?f = "\<lambda>y. f (x(i := y))"
     show "?f \<in> borel_measurable (M i)"
@@ -830,16 +830,16 @@
       unfolding comp_def .
     show "(\<integral>\<^sup>+ y. f (merge I {i} (x, y)) \<partial>Pi\<^sub>M {i} M) = (\<integral>\<^sup>+ y. f (x(i := y i)) \<partial>Pi\<^sub>M {i} M)"
       using x
-      by (auto intro!: positive_integral_cong arg_cong[where f=f]
+      by (auto intro!: nn_integral_cong arg_cong[where f=f]
                simp add: space_PiM extensional_def PiE_def)
   qed
 qed
 
-lemma (in product_sigma_finite) product_positive_integral_setprod:
+lemma (in product_sigma_finite) product_nn_integral_setprod:
   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
   and pos: "\<And>i x. i \<in> I \<Longrightarrow> 0 \<le> f i x"
-  shows "(\<integral>\<^sup>+ x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^sub>M I M) = (\<Prod>i\<in>I. integral\<^sup>P (M i) (f i))"
+  shows "(\<integral>\<^sup>+ x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^sub>M I M) = (\<Prod>i\<in>I. integral\<^sup>N (M i) (f i))"
 using assms proof induct
   case (insert i I)
   note `finite I`[intro, simp]
@@ -852,10 +852,10 @@
               measurable_comp[OF measurable_component_singleton, unfolded comp_def])
        auto
   then show ?case
-    apply (simp add: product_positive_integral_insert[OF insert(1,2) prod])
-    apply (simp add: insert(2-) * pos borel setprod_ereal_pos positive_integral_multc)
-    apply (subst positive_integral_cmult)
-    apply (auto simp add: pos borel insert(2-) setprod_ereal_pos positive_integral_positive)
+    apply (simp add: product_nn_integral_insert[OF insert(1,2) prod])
+    apply (simp add: insert(2-) * pos borel setprod_ereal_pos nn_integral_multc)
+    apply (subst nn_integral_cmult)
+    apply (auto simp add: pos borel insert(2-) setprod_ereal_pos nn_integral_nonneg)
     done
 qed (simp add: space_PiM)
 
@@ -871,9 +871,9 @@
   then have "emeasure ?P A = (\<integral>\<^sup>+x. indicator A x \<partial>?P)" 
     by simp
   also have "\<dots> = (\<integral>\<^sup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)" 
-    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def PiE_def eq)
+    by (intro nn_integral_cong) (auto simp: space_PiM indicator_def PiE_def eq)
   also have "\<dots> = emeasure ?D A"
-    using A by (simp add: product_positive_integral_singleton emeasure_distr)
+    using A by (simp add: product_nn_integral_singleton emeasure_distr)
   finally show "emeasure (Pi\<^sub>M {i} M) A = emeasure ?D A" .
 qed simp
 
@@ -894,7 +894,7 @@
     apply (subst distr_merge[symmetric, OF IJ])
     apply (subst emeasure_distr[OF measurable_merge A])
     apply (subst J.emeasure_pair_measure_alt[OF merge])
-    apply (auto intro!: positive_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
+    apply (auto intro!: nn_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
     done
 
   show ?B
diff -r 61855ade6c7e -r 891e992e510f src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Mon May 19 13:53:58 2014 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Mon May 19 14:26:58 2014 +0200
@@ -59,7 +59,7 @@
       using K J by (subst emeasure_fold_integral) auto
     also have "\<dots> = (\<integral>\<^sup>+ y. \<mu>G ((\<lambda>x. merge J (I - J) (y, x)) -` Z \<inter> space (Pi\<^sub>M I M)) \<partial>Pi\<^sub>M J M)"
       (is "_ = (\<integral>\<^sup>+x. \<mu>G (?MZ x) \<partial>Pi\<^sub>M J M)")
-    proof (intro positive_integral_cong)
+    proof (intro nn_integral_cong)
       fix x assume x: "x \<in> space (Pi\<^sub>M J M)"
       with K merge_in_G(2)[OF this]
       show "emeasure (Pi\<^sub>M (K - J) M) (?M x) = \<mu>G (?MZ x)"
@@ -141,7 +141,7 @@
           have "?a / 2^k \<le> \<mu>G (Z n)" using Z by auto
           also have "\<dots> \<le> (\<integral>\<^sup>+ x. indicator (?Q n) x + ?a / 2^(k+1) \<partial>Pi\<^sub>M J' M)"
             unfolding fold(2)[OF J' `Z n \<in> ?G`]
-          proof (intro positive_integral_mono)
+          proof (intro nn_integral_mono)
             fix x assume x: "x \<in> space (Pi\<^sub>M J' M)"
             then have "?q n x \<le> 1 + 0"
               using J' Z fold(3) Z_sets by auto
@@ -153,7 +153,7 @@
           qed
           also have "\<dots> = emeasure (Pi\<^sub>M J' M) (?Q n) + ?a / 2^(k+1)"
             using `0 \<le> ?a` Q_sets J'.emeasure_space_1
-            by (subst positive_integral_add) auto
+            by (subst nn_integral_add) auto
           finally show "?a / 2^(k+1) \<le> emeasure (Pi\<^sub>M J' M) (?Q n)" using `?a \<le> 1`
             by (cases rule: ereal2_cases[of ?a "emeasure (Pi\<^sub>M J' M) (?Q n)"])
                (auto simp: field_simps)
diff -r 61855ade6c7e -r 891e992e510f src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Mon May 19 13:53:58 2014 +0200
+++ b/src/HOL/Probability/Information.thy	Mon May 19 14:26:58 2014 +0200
@@ -143,10 +143,10 @@
     using D by auto
 
   have D_neg: "(\<integral>\<^sup>+ x. ereal (- D x) \<partial>M) = 0"
-    using D by (subst positive_integral_0_iff_AE) auto
+    using D by (subst nn_integral_0_iff_AE) auto
 
   have "(\<integral>\<^sup>+ x. ereal (D x) \<partial>M) = emeasure (density M D) (space M)"
-    using D by (simp add: emeasure_density cong: positive_integral_cong)
+    using D by (simp add: emeasure_density cong: nn_integral_cong)
   then have D_pos: "(\<integral>\<^sup>+ x. ereal (D x) \<partial>M) = 1"
     using N.emeasure_space_1 by simp
 
@@ -178,11 +178,11 @@
       have "emeasure M {x\<in>space M. D x = 1} = (\<integral>\<^sup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"
         using D(1) by auto
       also have "\<dots> = (\<integral>\<^sup>+ x. ereal (D x) \<partial>M)"
-        using disj by (auto intro!: positive_integral_cong_AE simp: indicator_def one_ereal_def)
+        using disj by (auto intro!: nn_integral_cong_AE simp: indicator_def one_ereal_def)
       finally have "AE x in M. D x = 1"
         using D D_pos by (intro AE_I_eq_1) auto
       then have "(\<integral>\<^sup>+x. indicator A x\<partial>M) = (\<integral>\<^sup>+x. ereal (D x) * indicator A x\<partial>M)"
-        by (intro positive_integral_cong_AE) (auto simp: one_ereal_def[symmetric])
+        by (intro nn_integral_cong_AE) (auto simp: one_ereal_def[symmetric])
       also have "\<dots> = density M D A"
         using `A \<in> sets M` D by (simp add: emeasure_density)
       finally show False using `A \<in> sets M` `emeasure (density M D) A \<noteq> emeasure M A` by simp
@@ -844,9 +844,9 @@
   from X.emeasure_space_1 have "(\<integral>\<^sup>+x. Px x \<partial>MX) = 1"
     unfolding distributed_distr_eq_density[OF X] using Px
     by (subst (asm) emeasure_density)
-       (auto simp: borel_measurable_ereal_iff intro!: integral_cong cong: positive_integral_cong)
+       (auto simp: borel_measurable_ereal_iff intro!: integral_cong cong: nn_integral_cong)
   ultimately show False
-    by (simp add: positive_integral_cong_AE)
+    by (simp add: nn_integral_cong_AE)
 qed
 
 lemma (in information_space) entropy_le:
@@ -876,11 +876,11 @@
     have [simp]: "\<And>x. x \<in> space MX \<Longrightarrow> ereal (if Px x = 0 then 0 else 1) = indicator {x \<in> space MX. Px x \<noteq> 0} x"
       by (auto simp: one_ereal_def)
     have "(\<integral>\<^sup>+ x. max 0 (ereal (- (if Px x = 0 then 0 else 1))) \<partial>MX) = (\<integral>\<^sup>+ x. 0 \<partial>MX)"
-      by (intro positive_integral_cong) (auto split: split_max)
+      by (intro nn_integral_cong) (auto split: split_max)
     then show "integrable (distr M MX X) (\<lambda>x. 1 / Px x)"
       unfolding distributed_distr_eq_density[OF X] using Px
-      by (auto simp: positive_integral_density real_integrable_def borel_measurable_ereal_iff fin positive_integral_max_0
-              cong: positive_integral_cong)
+      by (auto simp: nn_integral_density real_integrable_def borel_measurable_ereal_iff fin nn_integral_max_0
+              cong: nn_integral_cong)
     have "integrable MX (\<lambda>x. Px x * log b (1 / Px x)) =
       integrable MX (\<lambda>x. - Px x * log b (Px x))"
       using Px
@@ -1084,37 +1084,37 @@
     by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
 
   have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^sup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P))"
-    apply (subst positive_integral_density)
+    apply (subst nn_integral_density)
     apply simp
     apply (rule distributed_AE[OF Pxyz])
     apply auto []
-    apply (rule positive_integral_mono_AE)
+    apply (rule nn_integral_mono_AE)
     using ae5 ae6 ae7 ae8
     apply eventually_elim
     apply auto
     done
   also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
-    by (subst STP.positive_integral_snd[symmetric]) (auto simp add: split_beta')
+    by (subst STP.nn_integral_snd[symmetric]) (auto simp add: split_beta')
   also have "\<dots> = (\<integral>\<^sup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^sub>M P)"
-    apply (rule positive_integral_cong_AE)
+    apply (rule nn_integral_cong_AE)
     using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
     apply eventually_elim
   proof (case_tac x, simp del: times_ereal.simps add: space_pair_measure)
     fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
       "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
     then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
-      by (subst positive_integral_multc)
+      by (subst nn_integral_multc)
          (auto split: prod.split)
   qed
   also have "\<dots> = 1"
     using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
-    by (subst positive_integral_density[symmetric]) auto
+    by (subst nn_integral_density[symmetric]) auto
   finally have le1: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> 1" .
   also have "\<dots> < \<infinity>" by simp
   finally have fin: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
 
   have pos: "(\<integral>\<^sup>+x. ?f x \<partial>?P) \<noteq> 0"
-    apply (subst positive_integral_density)
+    apply (subst nn_integral_density)
     apply simp
     apply (rule distributed_AE[OF Pxyz])
     apply auto []
@@ -1123,18 +1123,18 @@
     let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
     assume "(\<integral>\<^sup>+x. ?g x \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)) = 0"
     then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. ?g x \<le> 0"
-      by (intro positive_integral_0_iff_AE[THEN iffD1]) auto
+      by (intro nn_integral_0_iff_AE[THEN iffD1]) auto
     then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pxyz x = 0"
       using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
       by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
     then have "(\<integral>\<^sup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) = 0"
-      by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
+      by (subst nn_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
     with P.emeasure_space_1 show False
-      by (subst (asm) emeasure_density) (auto cong: positive_integral_cong)
+      by (subst (asm) emeasure_density) (auto cong: nn_integral_cong)
   qed
 
   have neg: "(\<integral>\<^sup>+ x. - ?f x \<partial>?P) = 0"
-    apply (rule positive_integral_0_iff_AE[THEN iffD2])
+    apply (rule nn_integral_0_iff_AE[THEN iffD2])
     apply simp
     apply (subst AE_density)
     apply simp
@@ -1160,14 +1160,14 @@
         by simp
     qed simp
     then have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) = (\<integral>x. ?f x \<partial>?P)"
-      apply (rule positive_integral_eq_integral)
+      apply (rule nn_integral_eq_integral)
       apply (subst AE_density)
       apply simp
       using ae5 ae6 ae7 ae8
       apply eventually_elim
       apply auto
       done
-    with positive_integral_positive[of ?P ?f] pos le1
+    with nn_integral_nonneg[of ?P ?f] pos le1
     show "0 < (\<integral>x. ?f x \<partial>?P)" "(\<integral>x. ?f x \<partial>?P) \<le> 1"
       by (simp_all add: one_ereal_def)
   qed
@@ -1341,36 +1341,36 @@
     using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
     by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
   have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^sup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P))"
-    apply (subst positive_integral_density)
+    apply (subst nn_integral_density)
     apply (rule distributed_borel_measurable[OF Pxyz])
     apply (rule distributed_AE[OF Pxyz])
     apply simp
-    apply (rule positive_integral_mono_AE)
+    apply (rule nn_integral_mono_AE)
     using ae5 ae6 ae7 ae8
     apply eventually_elim
     apply auto
     done
   also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
-    by (subst STP.positive_integral_snd[symmetric]) (auto simp add: split_beta')
+    by (subst STP.nn_integral_snd[symmetric]) (auto simp add: split_beta')
   also have "\<dots> = (\<integral>\<^sup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^sub>M P)"
-    apply (rule positive_integral_cong_AE)
+    apply (rule nn_integral_cong_AE)
     using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
     apply eventually_elim
   proof (case_tac x, simp del: times_ereal.simps add: space_pair_measure)
     fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
       "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
     then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
-      by (subst positive_integral_multc) auto
+      by (subst nn_integral_multc) auto
   qed
   also have "\<dots> = 1"
     using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
-    by (subst positive_integral_density[symmetric]) auto
+    by (subst nn_integral_density[symmetric]) auto
   finally have le1: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> 1" .
   also have "\<dots> < \<infinity>" by simp
   finally have fin: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
 
   have pos: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> 0"
-    apply (subst positive_integral_density)
+    apply (subst nn_integral_density)
     apply simp
     apply (rule distributed_AE[OF Pxyz])
     apply simp
@@ -1379,18 +1379,18 @@
     let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
     assume "(\<integral>\<^sup>+ x. ?g x \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)) = 0"
     then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. ?g x \<le> 0"
-      by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: borel_measurable_ereal measurable_If)
+      by (intro nn_integral_0_iff_AE[THEN iffD1]) (auto intro!: borel_measurable_ereal measurable_If)
     then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pxyz x = 0"
       using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
       by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
     then have "(\<integral>\<^sup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) = 0"
-      by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
+      by (subst nn_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
     with P.emeasure_space_1 show False
-      by (subst (asm) emeasure_density) (auto cong: positive_integral_cong)
+      by (subst (asm) emeasure_density) (auto cong: nn_integral_cong)
   qed
 
   have neg: "(\<integral>\<^sup>+ x. - ?f x \<partial>?P) = 0"
-    apply (rule positive_integral_0_iff_AE[THEN iffD2])
+    apply (rule nn_integral_0_iff_AE[THEN iffD2])
     apply (auto simp: split_beta') []
     apply (subst AE_density)
     apply (auto simp: split_beta') []
@@ -1416,14 +1416,14 @@
         by simp
     qed simp
     then have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) = (\<integral>x. ?f x \<partial>?P)"
-      apply (rule positive_integral_eq_integral)
+      apply (rule nn_integral_eq_integral)
       apply (subst AE_density)
       apply simp
       using ae5 ae6 ae7 ae8
       apply eventually_elim
       apply auto
       done
-    with positive_integral_positive[of ?P ?f] pos le1
+    with nn_integral_nonneg[of ?P ?f] pos le1
     show "0 < (\<integral>x. ?f x \<partial>?P)" "(\<integral>x. ?f x \<partial>?P) \<le> 1"
       by (simp_all add: one_ereal_def)
   qed
diff -r 61855ade6c7e -r 891e992e510f src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon May 19 13:53:58 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon May 19 14:26:58 2014 +0200
@@ -544,7 +544,7 @@
       by (auto simp: field_simps)
     with `0 < c` show ?thesis
       by (cases "a \<le> b")
-         (auto simp: field_simps emeasure_density positive_integral_distr positive_integral_cmult
+         (auto simp: field_simps emeasure_density nn_integral_distr nn_integral_cmult
                      borel_measurable_indicator' emeasure_distr)
   next
     assume "\<not> 0 < c" with `c \<noteq> 0` have "c < 0" by auto
@@ -552,23 +552,23 @@
       by (auto simp: field_simps)
     with `c < 0` show ?thesis
       by (cases "a \<le> b")
-         (auto simp: field_simps emeasure_density positive_integral_distr
-                     positive_integral_cmult borel_measurable_indicator' emeasure_distr)
+         (auto simp: field_simps emeasure_density nn_integral_distr
+                     nn_integral_cmult borel_measurable_indicator' emeasure_distr)
   qed
 qed simp
 
-lemma positive_integral_real_affine:
+lemma nn_integral_real_affine:
   fixes c :: real assumes [measurable]: "f \<in> borel_measurable borel" and c: "c \<noteq> 0"
   shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = \<bar>c\<bar> * (\<integral>\<^sup>+x. f (t + c * x) \<partial>lborel)"
   by (subst lborel_real_affine[OF c, of t])
-     (simp add: positive_integral_density positive_integral_distr positive_integral_cmult)
+     (simp add: nn_integral_density nn_integral_distr nn_integral_cmult)
 
 lemma lborel_integrable_real_affine:
   fixes f :: "real \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes f: "integrable lborel f"
   shows "c \<noteq> 0 \<Longrightarrow> integrable lborel (\<lambda>x. f (t + c * x))"
   using f f[THEN borel_measurable_integrable] unfolding integrable_iff_bounded
-  by (subst (asm) positive_integral_real_affine[where c=c and t=t]) auto
+  by (subst (asm) nn_integral_real_affine[where c=c and t=t]) auto
 
 lemma lborel_integrable_real_affine_iff:
   fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
@@ -638,7 +638,7 @@
     by simp
 qed
 
-lemma positive_integral_has_integral:
+lemma nn_integral_has_integral:
   fixes f::"'a::ordered_euclidean_space \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable lebesgue" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lebesgue) = ereal r"
   shows "(f has_integral r) UNIV"
@@ -648,7 +648,7 @@
 next
   case (mult g c)
   then have "ereal c * (\<integral>\<^sup>+ x. g x \<partial>lebesgue) = ereal r"
-    by (subst positive_integral_cmult[symmetric]) auto
+    by (subst nn_integral_cmult[symmetric]) auto
   then obtain r' where "(c = 0 \<and> r = 0) \<or> ((\<integral>\<^sup>+ x. ereal (g x) \<partial>lebesgue) = ereal r' \<and> r = c * r')"
     by (cases "\<integral>\<^sup>+ x. ereal (g x) \<partial>lebesgue") (auto split: split_if_asm)
   with mult show ?case
@@ -657,7 +657,7 @@
   case (add g h)
   moreover
   then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lebesgue) = (\<integral>\<^sup>+ x. h x \<partial>lebesgue) + (\<integral>\<^sup>+ x. g x \<partial>lebesgue)"
-    unfolding plus_ereal.simps[symmetric] by (subst positive_integral_add) auto
+    unfolding plus_ereal.simps[symmetric] by (subst nn_integral_add) auto
   with add obtain a b where "(\<integral>\<^sup>+ x. h x \<partial>lebesgue) = ereal a" "(\<integral>\<^sup>+ x. g x \<partial>lebesgue) = ereal b" "r = a + b"
     by (cases "\<integral>\<^sup>+ x. h x \<partial>lebesgue" "\<integral>\<^sup>+ x. g x \<partial>lebesgue" rule: ereal2_cases) auto
   ultimately show ?case
@@ -677,11 +677,11 @@
   
   { fix i
     have "(\<integral>\<^sup>+x. ereal (U i x) \<partial>lebesgue) \<le> (\<integral>\<^sup>+x. ereal (f x) \<partial>lebesgue)"
-      using U_le_f by (intro positive_integral_mono) simp
+      using U_le_f by (intro nn_integral_mono) simp
     then obtain p where "(\<integral>\<^sup>+x. U i x \<partial>lebesgue) = ereal p" "p \<le> r"
       using seq(6) by (cases "\<integral>\<^sup>+x. U i x \<partial>lebesgue") auto
     moreover then have "0 \<le> p"
-      by (metis ereal_less_eq(5) positive_integral_positive)
+      by (metis ereal_less_eq(5) nn_integral_nonneg)
     moreover note seq
     ultimately have "\<exists>p. (\<integral>\<^sup>+x. U i x \<partial>lebesgue) = ereal p \<and> 0 \<le> p \<and> p \<le> r \<and> (U i has_integral p) UNIV"
       by auto }
@@ -701,7 +701,7 @@
       using seq by auto
   qed
   moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lebesgue)) ----> (\<integral>\<^sup>+x. f x \<partial>lebesgue)"
-    using seq U_le_f by (intro positive_integral_dominated_convergence[where w=f]) auto
+    using seq U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto
   ultimately have "integral UNIV f = r"
     by (auto simp add: int_eq p seq intro: LIMSEQ_unique)
   with * show ?case
@@ -712,9 +712,9 @@
   fixes f::"'a::ordered_euclidean_space \<Rightarrow> real"
   assumes f: "integrable lebesgue f" "\<And>x. 0 \<le> f x"
   shows "(f has_integral integral\<^sup>L lebesgue f) UNIV"
-proof (rule positive_integral_has_integral)
+proof (rule nn_integral_has_integral)
   show "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lebesgue) = ereal (integral\<^sup>L lebesgue f)"
-    using f by (intro positive_integral_eq_integral) auto
+    using f by (intro nn_integral_eq_integral) auto
 qed (insert f, auto)
 
 lemma has_integral_lebesgue_integral_lebesgue:
@@ -744,13 +744,13 @@
   qed
 qed
 
-lemma lebesgue_positive_integral_eq_borel:
+lemma lebesgue_nn_integral_eq_borel:
   assumes f: "f \<in> borel_measurable borel"
-  shows "integral\<^sup>P lebesgue f = integral\<^sup>P lborel f"
+  shows "integral\<^sup>N lebesgue f = integral\<^sup>N lborel f"
 proof -
-  from f have "integral\<^sup>P lebesgue (\<lambda>x. max 0 (f x)) = integral\<^sup>P lborel (\<lambda>x. max 0 (f x))"
-    by (auto intro!: positive_integral_subalgebra[symmetric])
-  then show ?thesis unfolding positive_integral_max_0 .
+  from f have "integral\<^sup>N lebesgue (\<lambda>x. max 0 (f x)) = integral\<^sup>N lborel (\<lambda>x. max 0 (f x))"
+    by (auto intro!: nn_integral_subalgebra[symmetric])
+  then show ?thesis unfolding nn_integral_max_0 .
 qed
 
 lemma lebesgue_integral_eq_borel:
@@ -777,29 +777,29 @@
     unfolding lebesgue_integral_eq_borel[OF borel] by simp
 qed
 
-lemma positive_integral_bound_simple_function:
+lemma nn_integral_bound_simple_function:
   assumes bnd: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x" "\<And>x. x \<in> space M \<Longrightarrow> f x < \<infinity>"
   assumes f[measurable]: "simple_function M f"
   assumes supp: "emeasure M {x\<in>space M. f x \<noteq> 0} < \<infinity>"
-  shows "positive_integral M f < \<infinity>"
+  shows "nn_integral M f < \<infinity>"
 proof cases
   assume "space M = {}"
-  then have "positive_integral M f = (\<integral>\<^sup>+x. 0 \<partial>M)"
-    by (intro positive_integral_cong) auto
+  then have "nn_integral M f = (\<integral>\<^sup>+x. 0 \<partial>M)"
+    by (intro nn_integral_cong) auto
   then show ?thesis by simp
 next
   assume "space M \<noteq> {}"
   with simple_functionD(1)[OF f] bnd have bnd: "0 \<le> Max (f`space M) \<and> Max (f`space M) < \<infinity>"
     by (subst Max_less_iff) (auto simp: Max_ge_iff)
   
-  have "positive_integral M f \<le> (\<integral>\<^sup>+x. Max (f`space M) * indicator {x\<in>space M. f x \<noteq> 0} x \<partial>M)"
-  proof (rule positive_integral_mono)
+  have "nn_integral M f \<le> (\<integral>\<^sup>+x. Max (f`space M) * indicator {x\<in>space M. f x \<noteq> 0} x \<partial>M)"
+  proof (rule nn_integral_mono)
     fix x assume "x \<in> space M"
     with f show "f x \<le> Max (f ` space M) * indicator {x \<in> space M. f x \<noteq> 0} x"
       by (auto split: split_indicator intro!: Max_ge simple_functionD)
   qed
   also have "\<dots> < \<infinity>"
-    using bnd supp by (subst positive_integral_cmult) auto
+    using bnd supp by (subst nn_integral_cmult) auto
   finally show ?thesis .
 qed
 
@@ -814,10 +814,10 @@
   from f_borel have "(\<lambda>x. ereal (f x)) \<in> borel_measurable lebesgue" by auto
   from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
 
-  have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lebesgue) = (SUP i. integral\<^sup>P lebesgue (F i))"
+  have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lebesgue) = (SUP i. integral\<^sup>N lebesgue (F i))"
     using F
-    by (subst positive_integral_monotone_convergence_SUP[symmetric])
-       (simp_all add: positive_integral_max_0 borel_measurable_simple_function)
+    by (subst nn_integral_monotone_convergence_SUP[symmetric])
+       (simp_all add: nn_integral_max_0 borel_measurable_simple_function)
   also have "\<dots> \<le> ereal I"
   proof (rule SUP_least)
     fix i :: nat
@@ -873,7 +873,7 @@
       unfolding integrable_iff_bounded
     proof
       have "(\<integral>\<^sup>+x. F i x \<partial>lebesgue) < \<infinity>"
-      proof (rule positive_integral_bound_simple_function)
+      proof (rule nn_integral_bound_simple_function)
         fix x::'a assume "x \<in> space lebesgue" then show "0 \<le> F i x" "F i x < \<infinity>"
           using F by (auto simp: image_iff eq_commute)
       next
@@ -890,9 +890,9 @@
       by (rule has_integral_lebesgue_integral_lebesgue)
     from this I have "integral\<^sup>L lebesgue (\<lambda>x. real (F i x)) \<le> I"
       by (rule has_integral_le) (intro ballI F_bound)
-    moreover have "integral\<^sup>P lebesgue (F i) = integral\<^sup>L lebesgue (\<lambda>x. real (F i x))"
-      using int F by (subst positive_integral_eq_integral[symmetric])  (auto simp: F_eq2[symmetric] real_of_ereal_pos)
-    ultimately show "integral\<^sup>P lebesgue (F i) \<le> ereal I"
+    moreover have "integral\<^sup>N lebesgue (F i) = integral\<^sup>L lebesgue (\<lambda>x. real (F i x))"
+      using int F by (subst nn_integral_eq_integral[symmetric])  (auto simp: F_eq2[symmetric] real_of_ereal_pos)
+    ultimately show "integral\<^sup>N lebesgue (F i) \<le> ereal I"
       by simp
   qed
   finally show "integrable lebesgue f"
@@ -1003,8 +1003,8 @@
 lemma borel_fubini_positiv_integral:
   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> ereal"
   assumes f: "f \<in> borel_measurable borel"
-  shows "integral\<^sup>P lborel f = \<integral>\<^sup>+x. f (p2e x) \<partial>(\<Pi>\<^sub>M (i::'a)\<in>Basis. lborel)"
-  by (subst lborel_eq_lborel_space) (simp add: positive_integral_distr measurable_p2e f)
+  shows "integral\<^sup>N lborel f = \<integral>\<^sup>+x. f (p2e x) \<partial>(\<Pi>\<^sub>M (i::'a)\<in>Basis. lborel)"
+  by (subst lborel_eq_lborel_space) (simp add: nn_integral_distr measurable_p2e f)
 
 lemma borel_fubini_integrable:
   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> _::{banach, second_countable_topology}"
@@ -1125,21 +1125,21 @@
     by (intro integrable_has_integral_nonneg) (auto split: split_indicator)
 qed
 
-lemma positive_integral_FTC_atLeastAtMost:
+lemma nn_integral_FTC_atLeastAtMost:
   assumes "f \<in> borel_measurable borel" "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" "a \<le> b"
   shows "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
 proof -
   have "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)"
     by (rule integrable_FTC_Icc_nonneg) fact+
   then have "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = (\<integral>x. f x * indicator {a .. b} x \<partial>lborel)"
-    using assms by (intro positive_integral_eq_integral) (auto simp: indicator_def)
+    using assms by (intro nn_integral_eq_integral) (auto simp: indicator_def)
   also have "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
     by (rule integral_FTC_Icc_nonneg) fact+
   finally show ?thesis
     unfolding ereal_indicator[symmetric] by simp
 qed
 
-lemma positive_integral_FTC_atLeast:
+lemma nn_integral_FTC_atLeast:
   fixes f :: "real \<Rightarrow> real"
   assumes f_borel: "f \<in> borel_measurable borel"
   assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x" 
@@ -1161,10 +1161,10 @@
     then show "(\<lambda>n. ?f n x) ----> ?fR x"
       by (rule Lim_eventually)
   qed
-  then have "integral\<^sup>P lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
+  then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
     by simp
   also have "\<dots> = (SUP i::nat. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))"
-  proof (rule positive_integral_monotone_convergence_SUP)
+  proof (rule nn_integral_monotone_convergence_SUP)
     show "incseq ?f"
       using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
     show "\<And>i. (?f i) \<in> borel_measurable lborel"
@@ -1173,7 +1173,7 @@
       using nonneg by (auto split: split_indicator)
   qed
   also have "\<dots> = (SUP i::nat. ereal (F (a + real i) - F a))"
-    by (subst positive_integral_FTC_atLeastAtMost[OF f_borel f nonneg]) auto
+    by (subst nn_integral_FTC_atLeastAtMost[OF f_borel f nonneg]) auto
   also have "\<dots> = T - F a"
   proof (rule SUP_Lim_ereal)
     show "incseq (\<lambda>n. ereal (F (a + real n) - F a))"
diff -r 61855ade6c7e -r 891e992e510f src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon May 19 13:53:58 2014 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon May 19 14:26:58 2014 +0200
@@ -17,7 +17,7 @@
 
 text {*
 
-Our simple functions are not restricted to positive real numbers. Instead
+Our simple functions are not restricted to nonnegative real numbers. Instead
 they are just functions with a finite range and are measurable when singleton
 sets are measurable.
 
@@ -725,7 +725,7 @@
   using simple_integral_mult[OF simple_function_indicator[OF A]]
   unfolding simple_integral_indicator_only[OF A] by simp
 
-lemma simple_integral_positive:
+lemma simple_integral_nonneg:
   assumes f: "simple_function M f" and ae: "AE x in M. 0 \<le> f x"
   shows "0 \<le> integral\<^sup>S M f"
 proof -
@@ -736,26 +736,26 @@
 
 subsection {* Integral on nonnegative functions *}
 
-definition positive_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>P") where
-  "integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^sup>S M g)"
+definition nn_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>N") where
+  "integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^sup>S M g)"
 
 syntax
-  "_positive_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>+ _. _ \<partial>_" [60,61] 110)
+  "_nn_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>+ _. _ \<partial>_" [60,61] 110)
 
 translations
-  "\<integral>\<^sup>+ x. f \<partial>M" == "CONST positive_integral M (%x. f)"
+  "\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)"
 
-lemma positive_integral_positive:
-  "0 \<le> integral\<^sup>P M f"
-  by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: positive_integral_def le_fun_def)
+lemma nn_integral_nonneg:
+  "0 \<le> integral\<^sup>N M f"
+  by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: nn_integral_def le_fun_def)
 
-lemma positive_integral_not_MInfty[simp]: "integral\<^sup>P M f \<noteq> -\<infinity>"
-  using positive_integral_positive[of M f] by auto
+lemma nn_integral_not_MInfty[simp]: "integral\<^sup>N M f \<noteq> -\<infinity>"
+  using nn_integral_nonneg[of M f] by auto
 
-lemma positive_integral_def_finite:
-  "integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f \<and> range g \<subseteq> {0 ..< \<infinity>}}. integral\<^sup>S M g)"
+lemma nn_integral_def_finite:
+  "integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f \<and> range g \<subseteq> {0 ..< \<infinity>}}. integral\<^sup>S M g)"
     (is "_ = SUPREMUM ?A ?f")
-  unfolding positive_integral_def
+  unfolding nn_integral_def
 proof (safe intro!: antisym SUP_least)
   fix g assume g: "simple_function M g" "g \<le> max 0 \<circ> f"
   let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}"
@@ -797,9 +797,9 @@
   qed
 qed (auto intro: SUP_upper)
 
-lemma positive_integral_mono_AE:
-  assumes ae: "AE x in M. u x \<le> v x" shows "integral\<^sup>P M u \<le> integral\<^sup>P M v"
-  unfolding positive_integral_def
+lemma nn_integral_mono_AE:
+  assumes ae: "AE x in M. u x \<le> v x" shows "integral\<^sup>N M u \<le> integral\<^sup>N M v"
+  unfolding nn_integral_def
 proof (safe intro!: SUP_mono)
   fix n assume n: "simple_function M n" "n \<le> max 0 \<circ> u"
   from ae[THEN AE_E] guess N . note N = this
@@ -822,57 +822,57 @@
     by force
 qed
 
-lemma positive_integral_mono:
-  "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^sup>P M u \<le> integral\<^sup>P M v"
-  by (auto intro: positive_integral_mono_AE)
+lemma nn_integral_mono:
+  "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^sup>N M u \<le> integral\<^sup>N M v"
+  by (auto intro: nn_integral_mono_AE)
 
-lemma positive_integral_cong_AE:
-  "AE x in M. u x = v x \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P M v"
-  by (auto simp: eq_iff intro!: positive_integral_mono_AE)
+lemma nn_integral_cong_AE:
+  "AE x in M. u x = v x \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v"
+  by (auto simp: eq_iff intro!: nn_integral_mono_AE)
 
-lemma positive_integral_cong:
-  "(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P M v"
-  by (auto intro: positive_integral_cong_AE)
+lemma nn_integral_cong:
+  "(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v"
+  by (auto intro: nn_integral_cong_AE)
 
-lemma positive_integral_cong_strong:
-  "M = N \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P N v"
-  by (auto intro: positive_integral_cong)
+lemma nn_integral_cong_strong:
+  "M = N \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N N v"
+  by (auto intro: nn_integral_cong)
 
-lemma positive_integral_eq_simple_integral:
-  assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^sup>P M f = integral\<^sup>S M f"
+lemma nn_integral_eq_simple_integral:
+  assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^sup>N M f = integral\<^sup>S M f"
 proof -
   let ?f = "\<lambda>x. f x * indicator (space M) x"
   have f': "simple_function M ?f" using f by auto
   with f(2) have [simp]: "max 0 \<circ> ?f = ?f"
     by (auto simp: fun_eq_iff max_def split: split_indicator)
-  have "integral\<^sup>P M ?f \<le> integral\<^sup>S M ?f" using f'
-    by (force intro!: SUP_least simple_integral_mono simp: le_fun_def positive_integral_def)
-  moreover have "integral\<^sup>S M ?f \<le> integral\<^sup>P M ?f"
-    unfolding positive_integral_def
+  have "integral\<^sup>N M ?f \<le> integral\<^sup>S M ?f" using f'
+    by (force intro!: SUP_least simple_integral_mono simp: le_fun_def nn_integral_def)
+  moreover have "integral\<^sup>S M ?f \<le> integral\<^sup>N M ?f"
+    unfolding nn_integral_def
     using f' by (auto intro!: SUP_upper)
   ultimately show ?thesis
-    by (simp cong: positive_integral_cong simple_integral_cong)
+    by (simp cong: nn_integral_cong simple_integral_cong)
 qed
 
-lemma positive_integral_eq_simple_integral_AE:
-  assumes f: "simple_function M f" "AE x in M. 0 \<le> f x" shows "integral\<^sup>P M f = integral\<^sup>S M f"
+lemma nn_integral_eq_simple_integral_AE:
+  assumes f: "simple_function M f" "AE x in M. 0 \<le> f x" shows "integral\<^sup>N M f = integral\<^sup>S M f"
 proof -
   have "AE x in M. f x = max 0 (f x)" using f by (auto split: split_max)
-  with f have "integral\<^sup>P M f = integral\<^sup>S M (\<lambda>x. max 0 (f x))"
-    by (simp cong: positive_integral_cong_AE simple_integral_cong_AE
-             add: positive_integral_eq_simple_integral)
+  with f have "integral\<^sup>N M f = integral\<^sup>S M (\<lambda>x. max 0 (f x))"
+    by (simp cong: nn_integral_cong_AE simple_integral_cong_AE
+             add: nn_integral_eq_simple_integral)
   with assms show ?thesis
     by (auto intro!: simple_integral_cong_AE split: split_max)
 qed
 
-lemma positive_integral_SUP_approx:
+lemma nn_integral_SUP_approx:
   assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
   and u: "simple_function M u" "u \<le> (SUP i. f i)" "u`space M \<subseteq> {0..<\<infinity>}"
-  shows "integral\<^sup>S M u \<le> (SUP i. integral\<^sup>P M (f i))" (is "_ \<le> ?S")
+  shows "integral\<^sup>S M u \<le> (SUP i. integral\<^sup>N M (f i))" (is "_ \<le> ?S")
 proof (rule ereal_le_mult_one_interval)
-  have "0 \<le> (SUP i. integral\<^sup>P M (f i))"
-    using f(3) by (auto intro!: SUP_upper2 positive_integral_positive)
-  then show "(SUP i. integral\<^sup>P M (f i)) \<noteq> -\<infinity>" by auto
+  have "0 \<le> (SUP i. integral\<^sup>N M (f i))"
+    using f(3) by (auto intro!: SUP_upper2 nn_integral_nonneg)
+  then show "(SUP i. integral\<^sup>N M (f i)) \<noteq> -\<infinity>" by auto
   have u_range: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> u x \<and> u x \<noteq> \<infinity>"
     using u(3) by auto
   fix a :: ereal assume "0 < a" "a < 1"
@@ -940,55 +940,55 @@
     have "a * integral\<^sup>S M (?uB i) = (\<integral>\<^sup>Sx. a * ?uB i x \<partial>M)"
       using B `simple_function M u` u_range
       by (subst simple_integral_mult) (auto split: split_indicator)
-    also have "\<dots> \<le> integral\<^sup>P M (f i)"
+    also have "\<dots> \<le> integral\<^sup>N M (f i)"
     proof -
       have *: "simple_function M (\<lambda>x. a * ?uB i x)" using B `0 < a` u(1) by auto
       show ?thesis using f(3) * u_range `0 < a`
-        by (subst positive_integral_eq_simple_integral[symmetric])
-           (auto intro!: positive_integral_mono split: split_indicator)
+        by (subst nn_integral_eq_simple_integral[symmetric])
+           (auto intro!: nn_integral_mono split: split_indicator)
     qed
-    finally show "a * integral\<^sup>S M (?uB i) \<le> integral\<^sup>P M (f i)"
+    finally show "a * integral\<^sup>S M (?uB i) \<le> integral\<^sup>N M (f i)"
       by auto
   next
     fix i show "0 \<le> \<integral>\<^sup>S x. ?uB i x \<partial>M" using B `0 < a` u(1) u_range
-      by (intro simple_integral_positive) (auto split: split_indicator)
+      by (intro simple_integral_nonneg) (auto split: split_indicator)
   qed (insert `0 < a`, auto)
   ultimately show "a * integral\<^sup>S M u \<le> ?S" by simp
 qed
 
-lemma incseq_positive_integral:
-  assumes "incseq f" shows "incseq (\<lambda>i. integral\<^sup>P M (f i))"
+lemma incseq_nn_integral:
+  assumes "incseq f" shows "incseq (\<lambda>i. integral\<^sup>N M (f i))"
 proof -
   have "\<And>i x. f i x \<le> f (Suc i) x"
     using assms by (auto dest!: incseq_SucD simp: le_fun_def)
   then show ?thesis
-    by (auto intro!: incseq_SucI positive_integral_mono)
+    by (auto intro!: incseq_SucI nn_integral_mono)
 qed
 
 text {* Beppo-Levi monotone convergence theorem *}
-lemma positive_integral_monotone_convergence_SUP:
+lemma nn_integral_monotone_convergence_SUP:
   assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
-  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"
+  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))"
 proof (rule antisym)
-  show "(SUP j. integral\<^sup>P M (f j)) \<le> (\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M)"
-    by (auto intro!: SUP_least SUP_upper positive_integral_mono)
+  show "(SUP j. integral\<^sup>N M (f j)) \<le> (\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M)"
+    by (auto intro!: SUP_least SUP_upper nn_integral_mono)
 next
-  show "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^sup>P M (f j))"
-    unfolding positive_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"]
+  show "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^sup>N M (f j))"
+    unfolding nn_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"]
   proof (safe intro!: SUP_least)
     fix g assume g: "simple_function M g"
       and *: "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
     then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
       using f by (auto intro!: SUP_upper2)
-    with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>P M (f j))"
-      by (intro  positive_integral_SUP_approx[OF f g _ g'])
+    with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>N M (f j))"
+      by (intro  nn_integral_SUP_approx[OF f g _ g'])
          (auto simp: le_fun_def max_def)
   qed
 qed
 
-lemma positive_integral_monotone_convergence_SUP_AE:
+lemma nn_integral_monotone_convergence_SUP_AE:
   assumes f: "\<And>i. AE x in M. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x" "\<And>i. f i \<in> borel_measurable M"
-  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"
+  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))"
 proof -
   from f have "AE x in M. \<forall>i. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x"
     by (simp add: AE_all_countable)
@@ -996,9 +996,9 @@
   let ?f = "\<lambda>i x. if x \<in> space M - N then f i x else 0"
   have f_eq: "AE x in M. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ _ N])
   then have "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>M)"
-    by (auto intro!: positive_integral_cong_AE)
+    by (auto intro!: nn_integral_cong_AE)
   also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. ?f i x \<partial>M))"
-  proof (rule positive_integral_monotone_convergence_SUP)
+  proof (rule nn_integral_monotone_convergence_SUP)
     show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI)
     { fix i show "(\<lambda>x. if x \<in> space M - N then f i x else 0) \<in> borel_measurable M"
         using f N(3) by (intro measurable_If_set) auto
@@ -1006,39 +1006,39 @@
         using N(1) by auto }
   qed
   also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))"
-    using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] positive_integral_cong_AE ext)
+    using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] nn_integral_cong_AE ext)
   finally show ?thesis .
 qed
 
-lemma positive_integral_monotone_convergence_SUP_AE_incseq:
+lemma nn_integral_monotone_convergence_SUP_AE_incseq:
   assumes f: "incseq f" "\<And>i. AE x in M. 0 \<le> f i x" and borel: "\<And>i. f i \<in> borel_measurable M"
-  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"
+  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))"
   using f[unfolded incseq_Suc_iff le_fun_def]
-  by (intro positive_integral_monotone_convergence_SUP_AE[OF _ borel])
+  by (intro nn_integral_monotone_convergence_SUP_AE[OF _ borel])
      auto
 
-lemma positive_integral_monotone_convergence_simple:
+lemma nn_integral_monotone_convergence_simple:
   assumes f: "incseq f" "\<And>i x. 0 \<le> f i x" "\<And>i. simple_function M (f i)"
   shows "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
-  using assms unfolding positive_integral_monotone_convergence_SUP[OF f(1)
+  using assms unfolding nn_integral_monotone_convergence_SUP[OF f(1)
     f(3)[THEN borel_measurable_simple_function] f(2)]
-  by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPREMUM UNIV"] ext)
+  by (auto intro!: nn_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPREMUM UNIV"] ext)
 
-lemma positive_integral_max_0:
-  "(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>P M f"
-  by (simp add: le_fun_def positive_integral_def)
+lemma nn_integral_max_0:
+  "(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>N M f"
+  by (simp add: le_fun_def nn_integral_def)
 
-lemma positive_integral_cong_pos:
+lemma nn_integral_cong_pos:
   assumes "\<And>x. x \<in> space M \<Longrightarrow> f x \<le> 0 \<and> g x \<le> 0 \<or> f x = g x"
-  shows "integral\<^sup>P M f = integral\<^sup>P M g"
+  shows "integral\<^sup>N M f = integral\<^sup>N M g"
 proof -
-  have "integral\<^sup>P M (\<lambda>x. max 0 (f x)) = integral\<^sup>P M (\<lambda>x. max 0 (g x))"
-  proof (intro positive_integral_cong)
+  have "integral\<^sup>N M (\<lambda>x. max 0 (f x)) = integral\<^sup>N M (\<lambda>x. max 0 (g x))"
+  proof (intro nn_integral_cong)
     fix x assume "x \<in> space M"
     from assms[OF this] show "max 0 (f x) = max 0 (g x)"
       by (auto split: split_max)
   qed
-  then show ?thesis by (simp add: positive_integral_max_0)
+  then show ?thesis by (simp add: nn_integral_max_0)
 qed
 
 lemma SUP_simple_integral_sequences:
@@ -1049,40 +1049,40 @@
     (is "SUPREMUM _ ?F = SUPREMUM _ ?G")
 proof -
   have "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
-    using f by (rule positive_integral_monotone_convergence_simple)
+    using f by (rule nn_integral_monotone_convergence_simple)
   also have "\<dots> = (\<integral>\<^sup>+x. (SUP i. g i x) \<partial>M)"
-    unfolding eq[THEN positive_integral_cong_AE] ..
+    unfolding eq[THEN nn_integral_cong_AE] ..
   also have "\<dots> = (SUP i. ?G i)"
-    using g by (rule positive_integral_monotone_convergence_simple[symmetric])
+    using g by (rule nn_integral_monotone_convergence_simple[symmetric])
   finally show ?thesis by simp
 qed
 
-lemma positive_integral_const[simp]:
+lemma nn_integral_const[simp]:
   "0 \<le> c \<Longrightarrow> (\<integral>\<^sup>+ x. c \<partial>M) = c * (emeasure M) (space M)"
-  by (subst positive_integral_eq_simple_integral) auto
+  by (subst nn_integral_eq_simple_integral) auto
 
-lemma positive_integral_linear:
+lemma nn_integral_linear:
   assumes f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" and "0 \<le> a"
   and g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x"
-  shows "(\<integral>\<^sup>+ x. a * f x + g x \<partial>M) = a * integral\<^sup>P M f + integral\<^sup>P M g"
-    (is "integral\<^sup>P M ?L = _")
+  shows "(\<integral>\<^sup>+ x. a * f x + g x \<partial>M) = a * integral\<^sup>N M f + integral\<^sup>N M g"
+    (is "integral\<^sup>N M ?L = _")
 proof -
   from borel_measurable_implies_simple_function_sequence'[OF f(1)] guess u .
-  note u = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
+  note u = nn_integral_monotone_convergence_simple[OF this(2,5,1)] this
   from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v .
-  note v = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
+  note v = nn_integral_monotone_convergence_simple[OF this(2,5,1)] this
   let ?L' = "\<lambda>i x. a * u i x + v i x"
 
   have "?L \<in> borel_measurable M" using assms by auto
   from borel_measurable_implies_simple_function_sequence'[OF this] guess l .
-  note l = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
+  note l = nn_integral_monotone_convergence_simple[OF this(2,5,1)] this
 
   have inc: "incseq (\<lambda>i. a * integral\<^sup>S M (u i))" "incseq (\<lambda>i. integral\<^sup>S M (v i))"
     using u v `0 \<le> a`
     by (auto simp: incseq_Suc_iff le_fun_def
              intro!: add_mono ereal_mult_left_mono simple_integral_mono)
   have pos: "\<And>i. 0 \<le> integral\<^sup>S M (u i)" "\<And>i. 0 \<le> integral\<^sup>S M (v i)" "\<And>i. 0 \<le> a * integral\<^sup>S M (u i)"
-    using u v `0 \<le> a` by (auto simp: simple_integral_positive)
+    using u v `0 \<le> a` by (auto simp: simple_integral_nonneg)
   { fix i from pos[of i] have "a * integral\<^sup>S M (u i) \<noteq> -\<infinity>" "integral\<^sup>S M (v i) \<noteq> -\<infinity>"
       by (auto split: split_if_asm) }
   note not_MInf = this
@@ -1111,69 +1111,69 @@
     unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
     apply (subst SUP_ereal_cmult [symmetric, OF pos(1) `0 \<le> a`])
     apply (subst SUP_ereal_add [symmetric, OF inc not_MInf]) .
-  then show ?thesis by (simp add: positive_integral_max_0)
+  then show ?thesis by (simp add: nn_integral_max_0)
 qed
 
-lemma positive_integral_cmult:
+lemma nn_integral_cmult:
   assumes f: "f \<in> borel_measurable M" "0 \<le> c"
-  shows "(\<integral>\<^sup>+ x. c * f x \<partial>M) = c * integral\<^sup>P M f"
+  shows "(\<integral>\<^sup>+ x. c * f x \<partial>M) = c * integral\<^sup>N M f"
 proof -
   have [simp]: "\<And>x. c * max 0 (f x) = max 0 (c * f x)" using `0 \<le> c`
     by (auto split: split_max simp: ereal_zero_le_0_iff)
   have "(\<integral>\<^sup>+ x. c * f x \<partial>M) = (\<integral>\<^sup>+ x. c * max 0 (f x) \<partial>M)"
-    by (simp add: positive_integral_max_0)
+    by (simp add: nn_integral_max_0)
   then show ?thesis
-    using positive_integral_linear[OF _ _ `0 \<le> c`, of "\<lambda>x. max 0 (f x)" _ "\<lambda>x. 0"] f
-    by (auto simp: positive_integral_max_0)
+    using nn_integral_linear[OF _ _ `0 \<le> c`, of "\<lambda>x. max 0 (f x)" _ "\<lambda>x. 0"] f
+    by (auto simp: nn_integral_max_0)
 qed
 
-lemma positive_integral_multc:
+lemma nn_integral_multc:
   assumes "f \<in> borel_measurable M" "0 \<le> c"
-  shows "(\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>P M f * c"
-  unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp
+  shows "(\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>N M f * c"
+  unfolding mult_commute[of _ c] nn_integral_cmult[OF assms] by simp
 
-lemma positive_integral_indicator[simp]:
+lemma nn_integral_indicator[simp]:
   "A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. indicator A x\<partial>M) = (emeasure M) A"
-  by (subst positive_integral_eq_simple_integral)
+  by (subst nn_integral_eq_simple_integral)
      (auto simp: simple_integral_indicator)
 
-lemma positive_integral_cmult_indicator:
+lemma nn_integral_cmult_indicator:
   "0 \<le> c \<Longrightarrow> A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. c * indicator A x \<partial>M) = c * (emeasure M) A"
-  by (subst positive_integral_eq_simple_integral)
+  by (subst nn_integral_eq_simple_integral)
      (auto simp: simple_function_indicator simple_integral_indicator)
 
-lemma positive_integral_indicator':
+lemma nn_integral_indicator':
   assumes [measurable]: "A \<inter> space M \<in> sets M"
   shows "(\<integral>\<^sup>+ x. indicator A x \<partial>M) = emeasure M (A \<inter> space M)"
 proof -
   have "(\<integral>\<^sup>+ x. indicator A x \<partial>M) = (\<integral>\<^sup>+ x. indicator (A \<inter> space M) x \<partial>M)"
-    by (intro positive_integral_cong) (simp split: split_indicator)
+    by (intro nn_integral_cong) (simp split: split_indicator)
   also have "\<dots> = emeasure M (A \<inter> space M)"
     by simp
   finally show ?thesis .
 qed
 
-lemma positive_integral_add:
+lemma nn_integral_add:
   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
   and g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
-  shows "(\<integral>\<^sup>+ x. f x + g x \<partial>M) = integral\<^sup>P M f + integral\<^sup>P M g"
+  shows "(\<integral>\<^sup>+ x. f x + g x \<partial>M) = integral\<^sup>N M f + integral\<^sup>N M g"
 proof -
   have ae: "AE x in M. max 0 (f x) + max 0 (g x) = max 0 (f x + g x)"
     using assms by (auto split: split_max)
   have "(\<integral>\<^sup>+ x. f x + g x \<partial>M) = (\<integral>\<^sup>+ x. max 0 (f x + g x) \<partial>M)"
-    by (simp add: positive_integral_max_0)
+    by (simp add: nn_integral_max_0)
   also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) + max 0 (g x) \<partial>M)"
-    unfolding ae[THEN positive_integral_cong_AE] ..
+    unfolding ae[THEN nn_integral_cong_AE] ..
   also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) \<partial>M) + (\<integral>\<^sup>+ x. max 0 (g x) \<partial>M)"
-    using positive_integral_linear[of "\<lambda>x. max 0 (f x)" _ 1 "\<lambda>x. max 0 (g x)"] f g
+    using nn_integral_linear[of "\<lambda>x. max 0 (f x)" _ 1 "\<lambda>x. max 0 (g x)"] f g
     by auto
   finally show ?thesis
-    by (simp add: positive_integral_max_0)
+    by (simp add: nn_integral_max_0)
 qed
 
-lemma positive_integral_setsum:
+lemma nn_integral_setsum:
   assumes "\<And>i. i\<in>P \<Longrightarrow> f i \<in> borel_measurable M" "\<And>i. i\<in>P \<Longrightarrow> AE x in M. 0 \<le> f i x"
-  shows "(\<integral>\<^sup>+ x. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^sup>P M (f i))"
+  shows "(\<integral>\<^sup>+ x. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^sup>N M (f i))"
 proof cases
   assume f: "finite P"
   from assms have "AE x in M. \<forall>i\<in>P. 0 \<le> f i x" unfolding AE_finite_all[OF f] by auto
@@ -1183,12 +1183,12 @@
     then have "f i \<in> borel_measurable M" "AE x in M. 0 \<le> f i x"
       "(\<lambda>x. \<Sum>i\<in>P. f i x) \<in> borel_measurable M" "AE x in M. 0 \<le> (\<Sum>i\<in>P. f i x)"
       by (auto intro!: setsum_nonneg)
-    from positive_integral_add[OF this]
+    from nn_integral_add[OF this]
     show ?case using insert by auto
   qed simp
 qed simp
 
-lemma positive_integral_Markov_inequality:
+lemma nn_integral_Markov_inequality:
   assumes u: "u \<in> borel_measurable M" "AE x in M. 0 \<le> u x" and "A \<in> sets M" and c: "0 \<le> c"
   shows "(emeasure M) ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * (\<integral>\<^sup>+ x. u x * indicator A x \<partial>M)"
     (is "(emeasure M) ?A \<le> _ * ?PI")
@@ -1196,19 +1196,19 @@
   have "?A \<in> sets M"
     using `A \<in> sets M` u by auto
   hence "(emeasure M) ?A = (\<integral>\<^sup>+ x. indicator ?A x \<partial>M)"
-    using positive_integral_indicator by simp
+    using nn_integral_indicator by simp
   also have "\<dots> \<le> (\<integral>\<^sup>+ x. c * (u x * indicator A x) \<partial>M)" using u c
-    by (auto intro!: positive_integral_mono_AE
+    by (auto intro!: nn_integral_mono_AE
       simp: indicator_def ereal_zero_le_0_iff)
   also have "\<dots> = c * (\<integral>\<^sup>+ x. u x * indicator A x \<partial>M)"
     using assms
-    by (auto intro!: positive_integral_cmult simp: ereal_zero_le_0_iff)
+    by (auto intro!: nn_integral_cmult simp: ereal_zero_le_0_iff)
   finally show ?thesis .
 qed
 
-lemma positive_integral_noteq_infinite:
+lemma nn_integral_noteq_infinite:
   assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
-  and "integral\<^sup>P M g \<noteq> \<infinity>"
+  and "integral\<^sup>N M g \<noteq> \<infinity>"
   shows "AE x in M. g x \<noteq> \<infinity>"
 proof (rule ccontr)
   assume c: "\<not> (AE x in M. g x \<noteq> \<infinity>)"
@@ -1218,34 +1218,34 @@
   ultimately have "0 < (emeasure M) {x\<in>space M. g x = \<infinity>}" by auto
   then have "\<infinity> = \<infinity> * (emeasure M) {x\<in>space M. g x = \<infinity>}" by auto
   also have "\<dots> \<le> (\<integral>\<^sup>+x. \<infinity> * indicator {x\<in>space M. g x = \<infinity>} x \<partial>M)"
-    using g by (subst positive_integral_cmult_indicator) auto
-  also have "\<dots> \<le> integral\<^sup>P M g"
-    using assms by (auto intro!: positive_integral_mono_AE simp: indicator_def)
-  finally show False using `integral\<^sup>P M g \<noteq> \<infinity>` by auto
+    using g by (subst nn_integral_cmult_indicator) auto
+  also have "\<dots> \<le> integral\<^sup>N M g"
+    using assms by (auto intro!: nn_integral_mono_AE simp: indicator_def)
+  finally show False using `integral\<^sup>N M g \<noteq> \<infinity>` by auto
 qed
 
-lemma positive_integral_PInf:
+lemma nn_integral_PInf:
   assumes f: "f \<in> borel_measurable M"
-  and not_Inf: "integral\<^sup>P M f \<noteq> \<infinity>"
+  and not_Inf: "integral\<^sup>N M f \<noteq> \<infinity>"
   shows "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
 proof -
   have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) = (\<integral>\<^sup>+ x. \<infinity> * indicator (f -` {\<infinity>} \<inter> space M) x \<partial>M)"
-    using f by (subst positive_integral_cmult_indicator) (auto simp: measurable_sets)
-  also have "\<dots> \<le> integral\<^sup>P M (\<lambda>x. max 0 (f x))"
-    by (auto intro!: positive_integral_mono simp: indicator_def max_def)
-  finally have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) \<le> integral\<^sup>P M f"
-    by (simp add: positive_integral_max_0)
+    using f by (subst nn_integral_cmult_indicator) (auto simp: measurable_sets)
+  also have "\<dots> \<le> integral\<^sup>N M (\<lambda>x. max 0 (f x))"
+    by (auto intro!: nn_integral_mono simp: indicator_def max_def)
+  finally have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) \<le> integral\<^sup>N M f"
+    by (simp add: nn_integral_max_0)
   moreover have "0 \<le> (emeasure M) (f -` {\<infinity>} \<inter> space M)"
     by (rule emeasure_nonneg)
   ultimately show ?thesis
     using assms by (auto split: split_if_asm)
 qed
 
-lemma positive_integral_PInf_AE:
-  assumes "f \<in> borel_measurable M" "integral\<^sup>P M f \<noteq> \<infinity>" shows "AE x in M. f x \<noteq> \<infinity>"
+lemma nn_integral_PInf_AE:
+  assumes "f \<in> borel_measurable M" "integral\<^sup>N M f \<noteq> \<infinity>" shows "AE x in M. f x \<noteq> \<infinity>"
 proof (rule AE_I)
   show "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
-    by (rule positive_integral_PInf[OF assms])
+    by (rule nn_integral_PInf[OF assms])
   show "f -` {\<infinity>} \<inter> space M \<in> sets M"
     using assms by (auto intro: borel_measurable_vimage)
 qed auto
@@ -1254,18 +1254,18 @@
   assumes "simple_function M f" "\<And>x. 0 \<le> f x"
   and "integral\<^sup>S M f \<noteq> \<infinity>"
   shows "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
-proof (rule positive_integral_PInf)
+proof (rule nn_integral_PInf)
   show "f \<in> borel_measurable M" using assms by (auto intro: borel_measurable_simple_function)
-  show "integral\<^sup>P M f \<noteq> \<infinity>"
-    using assms by (simp add: positive_integral_eq_simple_integral)
+  show "integral\<^sup>N M f \<noteq> \<infinity>"
+    using assms by (simp add: nn_integral_eq_simple_integral)
 qed
 
-lemma positive_integral_diff:
+lemma nn_integral_diff:
   assumes f: "f \<in> borel_measurable M"
   and g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
-  and fin: "integral\<^sup>P M g \<noteq> \<infinity>"
+  and fin: "integral\<^sup>N M g \<noteq> \<infinity>"
   and mono: "AE x in M. g x \<le> f x"
-  shows "(\<integral>\<^sup>+ x. f x - g x \<partial>M) = integral\<^sup>P M f - integral\<^sup>P M g"
+  shows "(\<integral>\<^sup>+ x. f x - g x \<partial>M) = integral\<^sup>N M f - integral\<^sup>N M g"
 proof -
   have diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M" "AE x in M. 0 \<le> f x - g x"
     using assms by (auto intro: ereal_diff_positive)
@@ -1274,61 +1274,61 @@
       by (cases rule: ereal2_cases[of a b]) auto }
   note * = this
   then have "AE x in M. f x = f x - g x + g x"
-    using mono positive_integral_noteq_infinite[OF g fin] assms by auto
-  then have **: "integral\<^sup>P M f = (\<integral>\<^sup>+x. f x - g x \<partial>M) + integral\<^sup>P M g"
-    unfolding positive_integral_add[OF diff g, symmetric]
-    by (rule positive_integral_cong_AE)
+    using mono nn_integral_noteq_infinite[OF g fin] assms by auto
+  then have **: "integral\<^sup>N M f = (\<integral>\<^sup>+x. f x - g x \<partial>M) + integral\<^sup>N M g"
+    unfolding nn_integral_add[OF diff g, symmetric]
+    by (rule nn_integral_cong_AE)
   show ?thesis unfolding **
-    using fin positive_integral_positive[of M g]
-    by (cases rule: ereal2_cases[of "\<integral>\<^sup>+ x. f x - g x \<partial>M" "integral\<^sup>P M g"]) auto
+    using fin nn_integral_nonneg[of M g]
+    by (cases rule: ereal2_cases[of "\<integral>\<^sup>+ x. f x - g x \<partial>M" "integral\<^sup>N M g"]) auto
 qed
 
-lemma positive_integral_suminf:
+lemma nn_integral_suminf:
   assumes f: "\<And>i. f i \<in> borel_measurable M" "\<And>i. AE x in M. 0 \<le> f i x"
-  shows "(\<integral>\<^sup>+ x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>P M (f i))"
+  shows "(\<integral>\<^sup>+ x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>N M (f i))"
 proof -
   have all_pos: "AE x in M. \<forall>i. 0 \<le> f i x"
     using assms by (auto simp: AE_all_countable)
-  have "(\<Sum>i. integral\<^sup>P M (f i)) = (SUP n. \<Sum>i<n. integral\<^sup>P M (f i))"
-    using positive_integral_positive by (rule suminf_ereal_eq_SUP)
+  have "(\<Sum>i. integral\<^sup>N M (f i)) = (SUP n. \<Sum>i<n. integral\<^sup>N M (f i))"
+    using nn_integral_nonneg by (rule suminf_ereal_eq_SUP)
   also have "\<dots> = (SUP n. \<integral>\<^sup>+x. (\<Sum>i<n. f i x) \<partial>M)"
-    unfolding positive_integral_setsum[OF f] ..
+    unfolding nn_integral_setsum[OF f] ..
   also have "\<dots> = \<integral>\<^sup>+x. (SUP n. \<Sum>i<n. f i x) \<partial>M" using f all_pos
-    by (intro positive_integral_monotone_convergence_SUP_AE[symmetric])
+    by (intro nn_integral_monotone_convergence_SUP_AE[symmetric])
        (elim AE_mp, auto simp: setsum_nonneg simp del: setsum_lessThan_Suc intro!: AE_I2 setsum_mono3)
   also have "\<dots> = \<integral>\<^sup>+x. (\<Sum>i. f i x) \<partial>M" using all_pos
-    by (intro positive_integral_cong_AE) (auto simp: suminf_ereal_eq_SUP)
+    by (intro nn_integral_cong_AE) (auto simp: suminf_ereal_eq_SUP)
   finally show ?thesis by simp
 qed
 
-lemma positive_integral_mult_bounded_inf:
+lemma nn_integral_mult_bounded_inf:
   assumes f: "f \<in> borel_measurable M" "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>"
     and c: "0 \<le> c" "c \<noteq> \<infinity>" and ae: "AE x in M. g x \<le> c * f x"
   shows "(\<integral>\<^sup>+x. g x \<partial>M) < \<infinity>"
 proof -
   have "(\<integral>\<^sup>+x. g x \<partial>M) \<le> (\<integral>\<^sup>+x. c * f x \<partial>M)"
-    by (intro positive_integral_mono_AE ae)
+    by (intro nn_integral_mono_AE ae)
   also have "(\<integral>\<^sup>+x. c * f x \<partial>M) < \<infinity>"
-    using c f by (subst positive_integral_cmult) auto
+    using c f by (subst nn_integral_cmult) auto
   finally show ?thesis .
 qed
 
 text {* Fatou's lemma: convergence theorem on limes inferior *}
 
-lemma positive_integral_liminf:
+lemma nn_integral_liminf:
   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes u: "\<And>i. u i \<in> borel_measurable M" "\<And>i. AE x in M. 0 \<le> u i x"
-  shows "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>P M (u n))"
+  shows "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))"
 proof -
   have pos: "AE x in M. \<forall>i. 0 \<le> u i x" using u by (auto simp: AE_all_countable)
   have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) =
     (SUP n. \<integral>\<^sup>+ x. (INF i:{n..}. u i x) \<partial>M)"
     unfolding liminf_SUP_INF using pos u
-    by (intro positive_integral_monotone_convergence_SUP_AE)
+    by (intro nn_integral_monotone_convergence_SUP_AE)
        (elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_superset_mono)
-  also have "\<dots> \<le> liminf (\<lambda>n. integral\<^sup>P M (u n))"
+  also have "\<dots> \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))"
     unfolding liminf_SUP_INF
-    by (auto intro!: SUP_mono exI INF_greatest positive_integral_mono INF_lower)
+    by (auto intro!: SUP_mono exI INF_greatest nn_integral_mono INF_lower)
   finally show ?thesis .
 qed
 
@@ -1345,11 +1345,11 @@
   shows "c - a \<le> c - b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c < \<infinity> \<Longrightarrow> b \<le> a"
   by (cases a b c rule: ereal3_cases) auto
 
-lemma positive_integral_limsup:
+lemma nn_integral_limsup:
   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes [measurable]: "\<And>i. u i \<in> borel_measurable M" "w \<in> borel_measurable M"
   assumes bounds: "\<And>i. AE x in M. 0 \<le> u i x" "\<And>i. AE x in M. u i x \<le> w x" and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
-  shows "limsup (\<lambda>n. integral\<^sup>P M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)"
+  shows "limsup (\<lambda>n. integral\<^sup>N M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)"
 proof -
   have bnd: "AE x in M. \<forall>i. 0 \<le> u i x \<and> u i x \<le> w x"
     using bounds by (auto simp: AE_all_countable)
@@ -1358,38 +1358,38 @@
     by auto
 
   have "(\<integral>\<^sup>+x. w x \<partial>M) - (\<integral>\<^sup>+x. limsup (\<lambda>n. u n x) \<partial>M) = (\<integral>\<^sup>+x. w x - limsup (\<lambda>n. u n x) \<partial>M)"
-  proof (intro positive_integral_diff[symmetric])
+  proof (intro nn_integral_diff[symmetric])
     show "AE x in M. 0 \<le> limsup (\<lambda>n. u n x)"
       using bnd by (auto intro!: le_Limsup)
     show "AE x in M. limsup (\<lambda>n. u n x) \<le> w x"
       using bnd by (auto intro!: Limsup_le)
     then have "(\<integral>\<^sup>+x. limsup (\<lambda>n. u n x) \<partial>M) < \<infinity>"
-      by (intro positive_integral_mult_bounded_inf[OF _ w, of 1]) auto
+      by (intro nn_integral_mult_bounded_inf[OF _ w, of 1]) auto
     then show "(\<integral>\<^sup>+x. limsup (\<lambda>n. u n x) \<partial>M) \<noteq> \<infinity>"
       by simp
   qed auto
   also have "\<dots> = (\<integral>\<^sup>+x. liminf (\<lambda>n. w x - u n x) \<partial>M)"
     using w_nonneg
-    by (intro positive_integral_cong_AE, eventually_elim)
+    by (intro nn_integral_cong_AE, eventually_elim)
        (auto intro!: liminf_ereal_cminus[symmetric])
   also have "\<dots> \<le> liminf (\<lambda>n. \<integral>\<^sup>+x. w x - u n x \<partial>M)"
-  proof (rule positive_integral_liminf)
+  proof (rule nn_integral_liminf)
     fix i show "AE x in M. 0 \<le> w x - u i x"
       using bounds[of i] by eventually_elim (auto intro: ereal_diff_positive)
   qed simp
   also have "(\<lambda>n. \<integral>\<^sup>+x. w x - u n x \<partial>M) = (\<lambda>n. (\<integral>\<^sup>+x. w x \<partial>M) - (\<integral>\<^sup>+x. u n x \<partial>M))"
-  proof (intro ext positive_integral_diff)
+  proof (intro ext nn_integral_diff)
     fix i have "(\<integral>\<^sup>+x. u i x \<partial>M) < \<infinity>"
-      using bounds by (intro positive_integral_mult_bounded_inf[OF _ w, of 1]) auto
+      using bounds by (intro nn_integral_mult_bounded_inf[OF _ w, of 1]) auto
     then show "(\<integral>\<^sup>+x. u i x \<partial>M) \<noteq> \<infinity>" by simp
   qed (insert bounds, auto)
   also have "liminf (\<lambda>n. (\<integral>\<^sup>+x. w x \<partial>M) - (\<integral>\<^sup>+x. u n x \<partial>M)) = (\<integral>\<^sup>+x. w x \<partial>M) - limsup (\<lambda>n. \<integral>\<^sup>+x. u n x \<partial>M)"
     using w by (intro liminf_ereal_cminus) auto
   finally show ?thesis
-    by (rule ereal_mono_minus_cancel) (intro w positive_integral_positive)+
+    by (rule ereal_mono_minus_cancel) (intro w nn_integral_nonneg)+
 qed
 
-lemma positive_integral_dominated_convergence:
+lemma nn_integral_dominated_convergence:
   assumes [measurable]:
        "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
     and bound: "\<And>j. AE x in M. 0 \<le> u j x" "\<And>j. AE x in M. u j x \<le> w x"
@@ -1397,25 +1397,25 @@
     and u': "AE x in M. (\<lambda>i. u i x) ----> u' x"
   shows "(\<lambda>i. (\<integral>\<^sup>+x. u i x \<partial>M)) ----> (\<integral>\<^sup>+x. u' x \<partial>M)"
 proof -
-  have "limsup (\<lambda>n. integral\<^sup>P M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)"
-    by (intro positive_integral_limsup[OF _ _ bound w]) auto
+  have "limsup (\<lambda>n. integral\<^sup>N M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)"
+    by (intro nn_integral_limsup[OF _ _ bound w]) auto
   moreover have "(\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M) = (\<integral>\<^sup>+ x. u' x \<partial>M)"
-    using u' by (intro positive_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot)
+    using u' by (intro nn_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot)
   moreover have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) = (\<integral>\<^sup>+ x. u' x \<partial>M)"
-    using u' by (intro positive_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot)
-  moreover have "(\<integral>\<^sup>+x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>P M (u n))"
-    by (intro positive_integral_liminf[OF _ bound(1)]) auto
-  moreover have "liminf (\<lambda>n. integral\<^sup>P M (u n)) \<le> limsup (\<lambda>n. integral\<^sup>P M (u n))"
+    using u' by (intro nn_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot)
+  moreover have "(\<integral>\<^sup>+x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))"
+    by (intro nn_integral_liminf[OF _ bound(1)]) auto
+  moreover have "liminf (\<lambda>n. integral\<^sup>N M (u n)) \<le> limsup (\<lambda>n. integral\<^sup>N M (u n))"
     by (intro Liminf_le_Limsup sequentially_bot)
   ultimately show ?thesis
     by (intro Liminf_eq_Limsup) auto
 qed
 
-lemma positive_integral_null_set:
+lemma nn_integral_null_set:
   assumes "N \<in> null_sets M" shows "(\<integral>\<^sup>+ x. u x * indicator N x \<partial>M) = 0"
 proof -
   have "(\<integral>\<^sup>+ x. u x * indicator N x \<partial>M) = (\<integral>\<^sup>+ x. 0 \<partial>M)"
-  proof (intro positive_integral_cong_AE AE_I)
+  proof (intro nn_integral_cong_AE AE_I)
     show "{x \<in> space M. u x * indicator N x \<noteq> 0} \<subseteq> N"
       by (auto simp: indicator_def)
     show "(emeasure M) N = 0" "N \<in> sets M"
@@ -1424,29 +1424,29 @@
   then show ?thesis by simp
 qed
 
-lemma positive_integral_0_iff:
+lemma nn_integral_0_iff:
   assumes u: "u \<in> borel_measurable M" and pos: "AE x in M. 0 \<le> u x"
-  shows "integral\<^sup>P M u = 0 \<longleftrightarrow> emeasure M {x\<in>space M. u x \<noteq> 0} = 0"
+  shows "integral\<^sup>N M u = 0 \<longleftrightarrow> emeasure M {x\<in>space M. u x \<noteq> 0} = 0"
     (is "_ \<longleftrightarrow> (emeasure M) ?A = 0")
 proof -
-  have u_eq: "(\<integral>\<^sup>+ x. u x * indicator ?A x \<partial>M) = integral\<^sup>P M u"
-    by (auto intro!: positive_integral_cong simp: indicator_def)
+  have u_eq: "(\<integral>\<^sup>+ x. u x * indicator ?A x \<partial>M) = integral\<^sup>N M u"
+    by (auto intro!: nn_integral_cong simp: indicator_def)
   show ?thesis
   proof
     assume "(emeasure M) ?A = 0"
-    with positive_integral_null_set[of ?A M u] u
-    show "integral\<^sup>P M u = 0" by (simp add: u_eq null_sets_def)
+    with nn_integral_null_set[of ?A M u] u
+    show "integral\<^sup>N M u = 0" by (simp add: u_eq null_sets_def)
   next
     { fix r :: ereal and n :: nat assume gt_1: "1 \<le> real n * r"
       then have "0 < real n * r" by (cases r) (auto split: split_if_asm simp: one_ereal_def)
       then have "0 \<le> r" by (auto simp add: ereal_zero_less_0_iff) }
     note gt_1 = this
-    assume *: "integral\<^sup>P M u = 0"
+    assume *: "integral\<^sup>N M u = 0"
     let ?M = "\<lambda>n. {x \<in> space M. 1 \<le> real (n::nat) * u x}"
     have "0 = (SUP n. (emeasure M) (?M n \<inter> ?A))"
     proof -
       { fix n :: nat
-        from positive_integral_Markov_inequality[OF u pos, of ?A "ereal (real n)"]
+        from nn_integral_Markov_inequality[OF u pos, of ?A "ereal (real n)"]
         have "(emeasure M) (?M n \<inter> ?A) \<le> 0" unfolding u_eq * using u by simp
         moreover have "0 \<le> (emeasure M) (?M n \<inter> ?A)" using u by auto
         ultimately have "(emeasure M) (?M n \<inter> ?A) = 0" by auto }
@@ -1489,33 +1489,33 @@
   qed
 qed
 
-lemma positive_integral_0_iff_AE:
+lemma nn_integral_0_iff_AE:
   assumes u: "u \<in> borel_measurable M"
-  shows "integral\<^sup>P M u = 0 \<longleftrightarrow> (AE x in M. u x \<le> 0)"
+  shows "integral\<^sup>N M u = 0 \<longleftrightarrow> (AE x in M. u x \<le> 0)"
 proof -
   have sets: "{x\<in>space M. max 0 (u x) \<noteq> 0} \<in> sets M"
     using u by auto
-  from positive_integral_0_iff[of "\<lambda>x. max 0 (u x)"]
-  have "integral\<^sup>P M u = 0 \<longleftrightarrow> (AE x in M. max 0 (u x) = 0)"
-    unfolding positive_integral_max_0
+  from nn_integral_0_iff[of "\<lambda>x. max 0 (u x)"]
+  have "integral\<^sup>N M u = 0 \<longleftrightarrow> (AE x in M. max 0 (u x) = 0)"
+    unfolding nn_integral_max_0
     using AE_iff_null[OF sets] u by auto
   also have "\<dots> \<longleftrightarrow> (AE x in M. u x \<le> 0)" by (auto split: split_max)
   finally show ?thesis .
 qed
 
-lemma AE_iff_positive_integral: 
-  "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> integral\<^sup>P M (indicator {x. \<not> P x}) = 0"
-  by (subst positive_integral_0_iff_AE) (auto simp: one_ereal_def zero_ereal_def
+lemma AE_iff_nn_integral: 
+  "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> integral\<^sup>N M (indicator {x. \<not> P x}) = 0"
+  by (subst nn_integral_0_iff_AE) (auto simp: one_ereal_def zero_ereal_def
     sets.sets_Collect_neg indicator_def[abs_def] measurable_If)
 
-lemma positive_integral_const_If:
+lemma nn_integral_const_If:
   "(\<integral>\<^sup>+x. a \<partial>M) = (if 0 \<le> a then a * (emeasure M) (space M) else 0)"
-  by (auto intro!: positive_integral_0_iff_AE[THEN iffD2])
+  by (auto intro!: nn_integral_0_iff_AE[THEN iffD2])
 
-lemma positive_integral_subalgebra:
+lemma nn_integral_subalgebra:
   assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
   and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> emeasure N A = emeasure M A"
-  shows "integral\<^sup>P N f = integral\<^sup>P M f"
+  shows "integral\<^sup>N N f = integral\<^sup>N M f"
 proof -
   have [simp]: "\<And>f :: 'a \<Rightarrow> ereal. f \<in> borel_measurable N \<Longrightarrow> f \<in> borel_measurable M"
     using N by (auto simp: measurable_def)
@@ -1525,12 +1525,12 @@
     using N by auto
   from f show ?thesis
     apply induct
-    apply (simp_all add: positive_integral_add positive_integral_cmult positive_integral_monotone_convergence_SUP N)
-    apply (auto intro!: positive_integral_cong cong: positive_integral_cong simp: N(2)[symmetric])
+    apply (simp_all add: nn_integral_add nn_integral_cmult nn_integral_monotone_convergence_SUP N)
+    apply (auto intro!: nn_integral_cong cong: nn_integral_cong simp: N(2)[symmetric])
     done
 qed
 
-lemma positive_integral_nat_function:
+lemma nn_integral_nat_function:
   fixes f :: "'a \<Rightarrow> nat"
   assumes "f \<in> measurable M (count_space UNIV)"
   shows "(\<integral>\<^sup>+x. ereal (of_nat (f x)) \<partial>M) = (\<Sum>t. emeasure M {x\<in>space M. t < f x})"
@@ -1549,9 +1549,9 @@
     ultimately have "ereal(of_nat(f x)) = (\<Sum>i. indicator (F i) x)"
       by (simp add: sums_iff) }
   then have "(\<integral>\<^sup>+x. ereal (of_nat (f x)) \<partial>M) = (\<integral>\<^sup>+x. (\<Sum>i. indicator (F i) x) \<partial>M)"
-    by (simp cong: positive_integral_cong)
+    by (simp cong: nn_integral_cong)
   also have "\<dots> = (\<Sum>i. emeasure M (F i))"
-    by (simp add: positive_integral_suminf)
+    by (simp add: nn_integral_suminf)
   finally show ?thesis
     by (simp add: F_def)
 qed
@@ -1560,17 +1560,17 @@
 
 subsubsection {* Distributions *}
 
-lemma positive_integral_distr':
+lemma nn_integral_distr':
   assumes T: "T \<in> measurable M M'"
   and f: "f \<in> borel_measurable (distr M M' T)" "\<And>x. 0 \<le> f x"
-  shows "integral\<^sup>P (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)"
+  shows "integral\<^sup>N (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)"
   using f 
 proof induct
   case (cong f g)
   with T show ?case
-    apply (subst positive_integral_cong[of _ f g])
+    apply (subst nn_integral_cong[of _ f g])
     apply simp
-    apply (subst positive_integral_cong[of _ "\<lambda>x. f (T x)" "\<lambda>x. g (T x)"])
+    apply (subst nn_integral_cong[of _ "\<lambda>x. f (T x)" "\<lambda>x. g (T x)"])
     apply (simp add: measurable_def Pi_iff)
     apply simp
     done
@@ -1579,15 +1579,15 @@
   then have eq: "\<And>x. x \<in> space M \<Longrightarrow> indicator A (T x) = indicator (T -` A \<inter> space M) x"
     by (auto simp: indicator_def)
   from set T show ?case
-    by (subst positive_integral_cong[OF eq])
-       (auto simp add: emeasure_distr intro!: positive_integral_indicator[symmetric] measurable_sets)
-qed (simp_all add: measurable_compose[OF T] T positive_integral_cmult positive_integral_add
-                   positive_integral_monotone_convergence_SUP le_fun_def incseq_def)
+    by (subst nn_integral_cong[OF eq])
+       (auto simp add: emeasure_distr intro!: nn_integral_indicator[symmetric] measurable_sets)
+qed (simp_all add: measurable_compose[OF T] T nn_integral_cmult nn_integral_add
+                   nn_integral_monotone_convergence_SUP le_fun_def incseq_def)
 
-lemma positive_integral_distr:
-  "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integral\<^sup>P (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)"
-  by (subst (1 2) positive_integral_max_0[symmetric])
-     (simp add: positive_integral_distr')
+lemma nn_integral_distr:
+  "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integral\<^sup>N (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)"
+  by (subst (1 2) nn_integral_max_0[symmetric])
+     (simp add: nn_integral_distr')
 
 subsubsection {* Counting space *}
 
@@ -1595,26 +1595,26 @@
   "simple_function (count_space A) f \<longleftrightarrow> finite (f ` A)"
   unfolding simple_function_def by simp
 
-lemma positive_integral_count_space:
+lemma nn_integral_count_space:
   assumes A: "finite {a\<in>A. 0 < f a}"
-  shows "integral\<^sup>P (count_space A) f = (\<Sum>a|a\<in>A \<and> 0 < f a. f a)"
+  shows "integral\<^sup>N (count_space A) f = (\<Sum>a|a\<in>A \<and> 0 < f a. f a)"
 proof -
   have *: "(\<integral>\<^sup>+x. max 0 (f x) \<partial>count_space A) =
     (\<integral>\<^sup>+ x. (\<Sum>a|a\<in>A \<and> 0 < f a. f a * indicator {a} x) \<partial>count_space A)"
-    by (auto intro!: positive_integral_cong
+    by (auto intro!: nn_integral_cong
              simp add: indicator_def if_distrib setsum_cases[OF A] max_def le_less)
   also have "\<dots> = (\<Sum>a|a\<in>A \<and> 0 < f a. \<integral>\<^sup>+ x. f a * indicator {a} x \<partial>count_space A)"
-    by (subst positive_integral_setsum)
+    by (subst nn_integral_setsum)
        (simp_all add: AE_count_space ereal_zero_le_0_iff less_imp_le)
   also have "\<dots> = (\<Sum>a|a\<in>A \<and> 0 < f a. f a)"
-    by (auto intro!: setsum_cong simp: positive_integral_cmult_indicator one_ereal_def[symmetric])
-  finally show ?thesis by (simp add: positive_integral_max_0)
+    by (auto intro!: setsum_cong simp: nn_integral_cmult_indicator one_ereal_def[symmetric])
+  finally show ?thesis by (simp add: nn_integral_max_0)
 qed
 
-lemma positive_integral_count_space_finite:
+lemma nn_integral_count_space_finite:
     "finite A \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>count_space A) = (\<Sum>a\<in>A. max 0 (f a))"
-  by (subst positive_integral_max_0[symmetric])
-     (auto intro!: setsum_mono_zero_left simp: positive_integral_count_space less_le)
+  by (subst nn_integral_max_0[symmetric])
+     (auto intro!: setsum_mono_zero_left simp: nn_integral_count_space less_le)
 
 lemma emeasure_UN_countable:
   assumes sets: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" and I: "countable I" 
@@ -1623,7 +1623,7 @@
 proof cases
   assume "finite I" with sets disj show ?thesis
     by (subst setsum_emeasure[symmetric])
-       (auto intro!: setsum_cong simp add: max_def subset_eq positive_integral_count_space_finite emeasure_nonneg)
+       (auto intro!: setsum_cong simp add: max_def subset_eq nn_integral_count_space_finite emeasure_nonneg)
 next
   assume f: "\<not> finite I"
   then have [intro]: "I \<noteq> {}" by auto
@@ -1648,15 +1648,15 @@
      by (auto simp: ereal_zero_less_0_iff indicator_def from_nat_into `I \<noteq> {}` simp del: ereal_0_less_1)
     have "(\<integral>\<^sup>+ ia. emeasure M (X ia) * indicator {from_nat_into I i} ia \<partial>count_space I) =
       (if 0 < emeasure M (X (from_nat_into I i)) then emeasure M (X (from_nat_into I i)) else 0)"
-      by (subst positive_integral_count_space) (simp_all add: eq)
+      by (subst nn_integral_count_space) (simp_all add: eq)
     also have "\<dots> = emeasure M (X (from_nat_into I i))"
       by (simp add: less_le emeasure_nonneg)
     finally show "emeasure M (X (from_nat_into I i)) =
          \<integral>\<^sup>+ ia. emeasure M (X ia) * indicator {from_nat_into I i} ia \<partial>count_space I" ..
   qed
   also have "\<dots> = (\<integral>\<^sup>+i. emeasure M (X i) \<partial>count_space I)"
-    apply (subst positive_integral_suminf[symmetric])
-    apply (auto simp: emeasure_nonneg intro!: positive_integral_cong)
+    apply (subst nn_integral_suminf[symmetric])
+    apply (auto simp: emeasure_nonneg intro!: nn_integral_cong)
   proof -
     fix x assume "x \<in> I"
     then have "(\<Sum>i. emeasure M (X x) * indicator {from_nat_into I i} x) = (\<Sum>i\<in>{to_nat_on I x}. emeasure M (X x) * indicator {from_nat_into I i} x)"
@@ -1670,12 +1670,12 @@
 
 subsubsection {* Measures with Restricted Space *}
 
-lemma positive_integral_restrict_space:
+lemma nn_integral_restrict_space:
   assumes \<Omega>: "\<Omega> \<in> sets M" and f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" "\<And>x. x \<in> space M - \<Omega> \<Longrightarrow> f x = 0"
-  shows "positive_integral (restrict_space M \<Omega>) f = positive_integral M f"
+  shows "nn_integral (restrict_space M \<Omega>) f = nn_integral M f"
 using f proof (induct rule: borel_measurable_induct)
   case (cong f g) then show ?case
-    using positive_integral_cong[of M f g] positive_integral_cong[of "restrict_space M \<Omega>" f g]
+    using nn_integral_cong[of M f g] nn_integral_cong[of "restrict_space M \<Omega>" f g]
       sets.sets_into_space[OF `\<Omega> \<in> sets M`]
     by (simp add: subset_eq space_restrict_space)
 next
@@ -1683,19 +1683,19 @@
   then have "A \<subseteq> \<Omega>"
     unfolding indicator_eq_0_iff by (auto dest: sets.sets_into_space)
   with set `\<Omega> \<in> sets M` sets.sets_into_space[OF `\<Omega> \<in> sets M`] show ?case
-    by (subst positive_integral_indicator')
+    by (subst nn_integral_indicator')
        (auto simp add: sets_restrict_space_iff space_restrict_space
                   emeasure_restrict_space Int_absorb2
                 dest: sets.sets_into_space)
 next
   case (mult f c) then show ?case
-    by (cases "c = 0") (simp_all add: measurable_restrict_space1 \<Omega> positive_integral_cmult)
+    by (cases "c = 0") (simp_all add: measurable_restrict_space1 \<Omega> nn_integral_cmult)
 next
   case (add f g) then show ?case
-    by (simp add: measurable_restrict_space1 \<Omega> positive_integral_add ereal_add_nonneg_eq_0_iff)
+    by (simp add: measurable_restrict_space1 \<Omega> nn_integral_add ereal_add_nonneg_eq_0_iff)
 next
   case (seq F) then show ?case
-    by (auto simp add: SUP_eq_iff measurable_restrict_space1 \<Omega> positive_integral_monotone_convergence_SUP)
+    by (auto simp add: SUP_eq_iff measurable_restrict_space1 \<Omega> nn_integral_monotone_convergence_SUP)
 qed
 
 subsubsection {* Measure spaces with an associated density *}
@@ -1720,14 +1720,14 @@
 
 lemma density_cong: "f \<in> borel_measurable M \<Longrightarrow> f' \<in> borel_measurable M \<Longrightarrow>
   (AE x in M. f x = f' x) \<Longrightarrow> density M f = density M f'"
-  unfolding density_def by (auto intro!: measure_of_eq positive_integral_cong_AE sets.space_closed)
+  unfolding density_def by (auto intro!: measure_of_eq nn_integral_cong_AE sets.space_closed)
 
 lemma density_max_0: "density M f = density M (\<lambda>x. max 0 (f x))"
 proof -
   have "\<And>x A. max 0 (f x) * indicator A x = max 0 (f x * indicator A x)"
     by (auto simp: indicator_def)
   then show ?thesis
-    unfolding density_def by (simp add: positive_integral_max_0)
+    unfolding density_def by (simp add: nn_integral_max_0)
 qed
 
 lemma density_ereal_max_0: "density M (\<lambda>x. ereal (f x)) = density M (\<lambda>x. ereal (max 0 (f x)))"
@@ -1741,10 +1741,10 @@
 proof (rule emeasure_measure_of_sigma)
   show "sigma_algebra (space M) (sets M)" ..
   show "positive (sets M) ?\<mu>"
-    using f by (auto simp: positive_def intro!: positive_integral_positive)
+    using f by (auto simp: positive_def intro!: nn_integral_nonneg)
   have \<mu>_eq: "?\<mu> = (\<lambda>A. \<integral>\<^sup>+ x. max 0 (f x) * indicator A x \<partial>M)" (is "?\<mu> = ?\<mu>'")
-    apply (subst positive_integral_max_0[symmetric])
-    apply (intro ext positive_integral_cong_AE AE_I2)
+    apply (subst nn_integral_max_0[symmetric])
+    apply (intro ext nn_integral_cong_AE AE_I2)
     apply (auto simp: indicator_def)
     done
   show "countably_additive (sets M) ?\<mu>"
@@ -1756,9 +1756,9 @@
       by (auto simp: set_eq_iff)
     assume disj: "disjoint_family A"
     have "(\<Sum>n. ?\<mu>' (A n)) = (\<integral>\<^sup>+ x. (\<Sum>n. max 0 (f x) * indicator (A n) x) \<partial>M)"
-      using f * by (simp add: positive_integral_suminf)
+      using f * by (simp add: nn_integral_suminf)
     also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) * (\<Sum>n. indicator (A n) x) \<partial>M)" using f
-      by (auto intro!: suminf_cmult_ereal positive_integral_cong_AE)
+      by (auto intro!: suminf_cmult_ereal nn_integral_cong_AE)
     also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) * indicator (\<Union>n. A n) x \<partial>M)"
       unfolding suminf_indicator[OF disj] ..
     finally show "(\<Sum>n. ?\<mu>' (A n)) = ?\<mu>' (\<Union>x. A x)" by simp
@@ -1771,15 +1771,15 @@
 proof -
   { assume "A \<in> sets M"
     have eq: "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^sup>+x. max 0 (f x) * indicator A x \<partial>M)"
-      apply (subst positive_integral_max_0[symmetric])
-      apply (intro positive_integral_cong)
+      apply (subst nn_integral_max_0[symmetric])
+      apply (intro nn_integral_cong)
       apply (auto simp: indicator_def)
       done
     have "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = 0 \<longleftrightarrow> 
       emeasure M {x \<in> space M. max 0 (f x) * indicator A x \<noteq> 0} = 0"
       unfolding eq
       using f `A \<in> sets M`
-      by (intro positive_integral_0_iff) auto
+      by (intro nn_integral_0_iff) auto
     also have "\<dots> \<longleftrightarrow> (AE x in M. max 0 (f x) * indicator A x = 0)"
       using f `A \<in> sets M`
       by (intro AE_iff_measurable[OF _ refl, symmetric]) auto
@@ -1814,15 +1814,15 @@
        (auto elim: eventually_elim2)
 qed
 
-lemma positive_integral_density':
+lemma nn_integral_density':
   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
   assumes g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x"
-  shows "integral\<^sup>P (density M f) g = (\<integral>\<^sup>+ x. f x * g x \<partial>M)"
+  shows "integral\<^sup>N (density M f) g = (\<integral>\<^sup>+ x. f x * g x \<partial>M)"
 using g proof induct
   case (cong u v)
   then show ?case
-    apply (subst positive_integral_cong[OF cong(3)])
-    apply (simp_all cong: positive_integral_cong)
+    apply (subst nn_integral_cong[OF cong(3)])
+    apply (simp_all cong: nn_integral_cong)
     done
 next
   case (set A) then show ?case
@@ -1831,31 +1831,31 @@
   case (mult u c)
   moreover have "\<And>x. f x * (c * u x) = c * (f x * u x)" by (simp add: field_simps)
   ultimately show ?case
-    using f by (simp add: positive_integral_cmult)
+    using f by (simp add: nn_integral_cmult)
 next
   case (add u v)
   then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x"
     by (simp add: ereal_right_distrib)
   with add f show ?case
-    by (auto simp add: positive_integral_add ereal_zero_le_0_iff intro!: positive_integral_add[symmetric])
+    by (auto simp add: nn_integral_add ereal_zero_le_0_iff intro!: nn_integral_add[symmetric])
 next
   case (seq U)
   from f(2) have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)"
     by eventually_elim (simp add: SUP_ereal_cmult seq)
   from seq f show ?case
-    apply (simp add: positive_integral_monotone_convergence_SUP)
-    apply (subst positive_integral_cong_AE[OF eq])
-    apply (subst positive_integral_monotone_convergence_SUP_AE)
+    apply (simp add: nn_integral_monotone_convergence_SUP)
+    apply (subst nn_integral_cong_AE[OF eq])
+    apply (subst nn_integral_monotone_convergence_SUP_AE)
     apply (auto simp: incseq_def le_fun_def intro!: ereal_mult_left_mono)
     done
 qed
 
-lemma positive_integral_density:
+lemma nn_integral_density:
   "f \<in> borel_measurable M \<Longrightarrow> AE x in M. 0 \<le> f x \<Longrightarrow> g' \<in> borel_measurable M \<Longrightarrow> 
-    integral\<^sup>P (density M f) g' = (\<integral>\<^sup>+ x. f x * g' x \<partial>M)"
-  by (subst (1 2) positive_integral_max_0[symmetric])
-     (auto intro!: positive_integral_cong_AE
-           simp: measurable_If max_def ereal_zero_le_0_iff positive_integral_density')
+    integral\<^sup>N (density M f) g' = (\<integral>\<^sup>+ x. f x * g' x \<partial>M)"
+  by (subst (1 2) nn_integral_max_0[symmetric])
+     (auto intro!: nn_integral_cong_AE
+           simp: measurable_If max_def ereal_zero_le_0_iff nn_integral_density')
 
 lemma emeasure_restricted:
   assumes S: "S \<in> sets M" and X: "X \<in> sets M"
@@ -1864,7 +1864,7 @@
   have "emeasure (density M (indicator S)) X = (\<integral>\<^sup>+x. indicator S x * indicator X x \<partial>M)"
     using S X by (simp add: emeasure_density)
   also have "\<dots> = (\<integral>\<^sup>+x. indicator (S \<inter> X) x \<partial>M)"
-    by (auto intro!: positive_integral_cong simp: indicator_def)
+    by (auto intro!: nn_integral_cong simp: indicator_def)
   also have "\<dots> = emeasure M (S \<inter> X)"
     using S X by (simp add: sets.Int)
   finally show ?thesis .
@@ -1880,7 +1880,7 @@
 
 lemma emeasure_density_const:
   "A \<in> sets M \<Longrightarrow> 0 \<le> c \<Longrightarrow> emeasure (density M (\<lambda>_. c)) A = c * emeasure M A"
-  by (auto simp: positive_integral_cmult_indicator emeasure_density)
+  by (auto simp: nn_integral_cmult_indicator emeasure_density)
 
 lemma measure_density_const:
   "A \<in> sets M \<Longrightarrow> 0 < c \<Longrightarrow> c \<noteq> \<infinity> \<Longrightarrow> measure (density M (\<lambda>_. c)) A = real c * measure M A"
@@ -1889,7 +1889,7 @@
 lemma density_density_eq:
    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. 0 \<le> f x \<Longrightarrow>
    density (density M f) g = density M (\<lambda>x. f x * g x)"
-  by (auto intro!: measure_eqI simp: emeasure_density positive_integral_density ac_simps)
+  by (auto intro!: measure_eqI simp: emeasure_density nn_integral_density ac_simps)
 
 lemma distr_density_distr:
   assumes T: "T \<in> measurable M M'" and T': "T' \<in> measurable M' M"
@@ -1904,7 +1904,7 @@
       using T inv by (auto simp: indicator_def measurable_space) }
   with A T T' f show "emeasure ?R A = emeasure ?L A"
     by (simp add: measurable_comp emeasure_density emeasure_distr
-                  positive_integral_distr measurable_sets cong: positive_integral_cong)
+                  nn_integral_distr measurable_sets cong: nn_integral_cong)
 qed simp
 
 lemma density_density_divide:
@@ -1951,7 +1951,7 @@
   have "{a. (a \<in> X \<longrightarrow> a \<in> A \<and> 0 < f a) \<and> a \<in> X} = {a\<in>X. 0 < f a}"
     using `X \<subseteq> A` by auto
   with A show ?thesis
-    by (simp add: emeasure_density positive_integral_count_space ereal_zero_le_0_iff
+    by (simp add: emeasure_density nn_integral_count_space ereal_zero_le_0_iff
                   point_measure_def indicator_def)
 qed
 
@@ -1973,14 +1973,14 @@
   unfolding point_measure_def
   by (subst AE_density) (auto simp: AE_density AE_count_space point_measure_def)
 
-lemma positive_integral_point_measure:
+lemma nn_integral_point_measure:
   "finite {a\<in>A. 0 < f a \<and> 0 < g a} \<Longrightarrow>
-    integral\<^sup>P (point_measure A f) g = (\<Sum>a|a\<in>A \<and> 0 < f a \<and> 0 < g a. f a * g a)"
+    integral\<^sup>N (point_measure A f) g = (\<Sum>a|a\<in>A \<and> 0 < f a \<and> 0 < g a. f a * g a)"
   unfolding point_measure_def
   apply (subst density_max_0)
-  apply (subst positive_integral_density)
-  apply (simp_all add: AE_count_space positive_integral_density)
-  apply (subst positive_integral_count_space )
+  apply (subst nn_integral_density)
+  apply (simp_all add: AE_count_space nn_integral_density)
+  apply (subst nn_integral_count_space )
   apply (auto intro!: setsum_cong simp: max_def ereal_zero_less_0_iff)
   apply (rule finite_subset)
   prefer 2
@@ -1988,10 +1988,10 @@
   apply auto
   done
 
-lemma positive_integral_point_measure_finite:
+lemma nn_integral_point_measure_finite:
   "finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> 0 \<le> f a) \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> 0 \<le> g a) \<Longrightarrow>
-    integral\<^sup>P (point_measure A f) g = (\<Sum>a\<in>A. f a * g a)"
-  by (subst positive_integral_point_measure) (auto intro!: setsum_mono_zero_left simp: less_le)
+    integral\<^sup>N (point_measure A f) g = (\<Sum>a\<in>A. f a * g a)"
+  by (subst nn_integral_point_measure) (auto intro!: setsum_mono_zero_left simp: less_le)
 
 subsubsection {* Uniform measure *}
 
@@ -2008,10 +2008,10 @@
 proof -
   from A B have "emeasure (uniform_measure M A) B = (\<integral>\<^sup>+x. (1 / emeasure M A) * indicator (A \<inter> B) x \<partial>M)"
     by (auto simp add: uniform_measure_def emeasure_density split: split_indicator
-             intro!: positive_integral_cong)
+             intro!: nn_integral_cong)
   also have "\<dots> = emeasure M (A \<inter> B) / emeasure M A"
     using A B
-    by (subst positive_integral_cmult_indicator) (simp_all add: sets.Int emeasure_nonneg)
+    by (subst nn_integral_cmult_indicator) (simp_all add: sets.Int emeasure_nonneg)
   finally show ?thesis .
 qed
 
diff -r 61855ade6c7e -r 891e992e510f src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Mon May 19 13:53:58 2014 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Mon May 19 14:26:58 2014 +0200
@@ -290,7 +290,7 @@
              simp: disjoint_family_on_def)
   also have "\<dots> = (\<integral>\<^sup>+i. \<P>(x in M. P i x) \<partial>count_space I)"
     unfolding emeasure_eq_measure using disj
-    by (intro positive_integral_cong ereal.inject[THEN iffD2] prob_eq_AE)
+    by (intro nn_integral_cong ereal.inject[THEN iffD2] prob_eq_AE)
        (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+
   finally show ?thesis .
 qed
@@ -402,9 +402,9 @@
   also have "\<dots> = emeasure (density (count_space A) P) {a}"
     using X by (simp add: distributed_distr_eq_density)
   also have "\<dots> = (\<integral>\<^sup>+x. P a * indicator {a} x \<partial>count_space A)"
-    using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: positive_integral_cong)
+    using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: nn_integral_cong)
   also have "\<dots> = P a"
-    using X a by (subst positive_integral_cmult_indicator) (auto simp: distributed_def one_ereal_def[symmetric] AE_count_space)
+    using X a by (subst nn_integral_cmult_indicator) (auto simp: distributed_def one_ereal_def[symmetric] AE_count_space)
   finally show ?thesis ..
 qed
 
@@ -446,10 +446,10 @@
   by (auto simp: distributed_AE
                  distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr)
 
-lemma distributed_positive_integral:
+lemma distributed_nn_integral:
   "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^sup>+x. f x * g x \<partial>N) = (\<integral>\<^sup>+x. g (X x) \<partial>M)"
   by (auto simp: distributed_AE
-                 distributed_distr_eq_density[symmetric] positive_integral_density[symmetric] positive_integral_distr)
+                 distributed_distr_eq_density[symmetric] nn_integral_density[symmetric] nn_integral_distr)
 
 lemma distributed_integral:
   "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>x. f x * g x \<partial>N) = (\<integral>x. g (X x) \<partial>M)"
@@ -520,10 +520,10 @@
     have "emeasure ?L E = emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B}"
       by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair)
     also have "\<dots> = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)"
-      using f by (auto simp add: eq positive_integral_multc intro!: positive_integral_cong)
+      using f by (auto simp add: eq nn_integral_multc intro!: nn_integral_cong)
     also have "\<dots> = emeasure ?R E"
-      by (auto simp add: emeasure_density T.positive_integral_fst[symmetric]
-               intro!: positive_integral_cong split: split_indicator)
+      by (auto simp add: emeasure_density T.nn_integral_fst[symmetric]
+               intro!: nn_integral_cong split: split_indicator)
     finally show "emeasure ?L E = emeasure ?R E" .
   qed
 qed (auto simp: f)
@@ -564,12 +564,12 @@
         using Pxy A by (intro distributed_emeasure) auto
       finally have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
         (\<integral>\<^sup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^sub>M T))"
-        by (auto intro!: positive_integral_cong split: split_indicator) }
+        by (auto intro!: nn_integral_cong split: split_indicator) }
     note * = this
     show "distr M ?D (\<lambda>x. (Y x, X x)) = density ?D (\<lambda>(x, y). Pxy (y, x))"
       apply (intro measure_eqI)
       apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1])
-      apply (subst positive_integral_distr)
+      apply (subst nn_integral_distr)
       apply (auto intro!: * simp: comp_def split_beta)
       done
   qed
@@ -590,13 +590,13 @@
   show X: "X \<in> measurable M S" by simp
 
   show borel: "Px \<in> borel_measurable S"
-    by (auto intro!: T.positive_integral_fst simp: Px_def)
+    by (auto intro!: T.nn_integral_fst simp: Px_def)
 
   interpret Pxy: prob_space "distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))"
     by (intro prob_space_distr) simp
   have "(\<integral>\<^sup>+ x. max 0 (- Pxy x) \<partial>(S \<Otimes>\<^sub>M T)) = (\<integral>\<^sup>+ x. 0 \<partial>(S \<Otimes>\<^sub>M T))"
     using Pxy
-    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_AE)
+    by (intro nn_integral_cong_AE) (auto simp: max_def dest: distributed_AE)
 
   show "distr M S X = density S Px"
   proof (rule measure_eqI)
@@ -608,18 +608,18 @@
       using Pxy by (simp add: distributed_def)
     also have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
       using A borel Pxy
-      by (simp add: emeasure_density T.positive_integral_fst[symmetric])
+      by (simp add: emeasure_density T.nn_integral_fst[symmetric])
     also have "\<dots> = \<integral>\<^sup>+ x. Px x * indicator A x \<partial>S"
-      apply (rule positive_integral_cong_AE)
+      apply (rule nn_integral_cong_AE)
       using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space
     proof eventually_elim
       fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)"
       moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x"
         by (auto simp: indicator_def)
       ultimately have "(\<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = (\<integral>\<^sup>+ y. Pxy (x, y) \<partial>T) * indicator A x"
-        by (simp add: eq positive_integral_multc cong: positive_integral_cong)
+        by (simp add: eq nn_integral_multc cong: nn_integral_cong)
       also have "(\<integral>\<^sup>+ y. Pxy (x, y) \<partial>T) = Px x"
-        by (simp add: Px_def ereal_real positive_integral_positive)
+        by (simp add: Px_def ereal_real nn_integral_nonneg)
       finally show "(\<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" .
     qed
     finally show "emeasure (distr M S X) A = emeasure (density S Px) A"
@@ -627,7 +627,7 @@
   qed simp
   
   show "AE x in S. 0 \<le> Px x"
-    by (simp add: Px_def positive_integral_positive real_of_ereal_pos)
+    by (simp add: Px_def nn_integral_nonneg real_of_ereal_pos)
 qed
 
 lemma (in prob_space) distr_marginal2:
@@ -727,10 +727,10 @@
                intro!: arg_cong[where f=prob])
     also have "\<dots> = (\<integral>\<^sup>+x. ereal (P' a) * indicator {a} x \<partial>S)"
       using A X a
-      by (subst positive_integral_cmult_indicator)
+      by (subst nn_integral_cmult_indicator)
          (auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg)
     also have "\<dots> = (\<integral>\<^sup>+x. ereal (P' x) * indicator {a} x \<partial>S)"
-      by (auto simp: indicator_def intro!: positive_integral_cong)
+      by (auto simp: indicator_def intro!: nn_integral_cong)
     also have "\<dots> = emeasure (density S P') {a}"
       using a A by (intro emeasure_density[symmetric]) (auto simp: S_def)
     finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" .
@@ -866,7 +866,7 @@
     Pxy[THEN simple_distributed, THEN distributed_real_AE]
   show ?thesis
     unfolding AE_count_space
-    apply (auto simp add: positive_integral_count_space_finite * intro!: setsum_cong split: split_max)
+    apply (auto simp add: nn_integral_count_space_finite * intro!: setsum_cong split: split_max)
     done
 qed
 
diff -r 61855ade6c7e -r 891e992e510f src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Mon May 19 13:53:58 2014 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon May 19 14:26:58 2014 +0200
@@ -44,7 +44,7 @@
 qed fact
 
 lemma (in sigma_finite_measure) Ex_finite_integrable_function:
-  shows "\<exists>h\<in>borel_measurable M. integral\<^sup>P M h \<noteq> \<infinity> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>) \<and> (\<forall>x. 0 \<le> h x)"
+  shows "\<exists>h\<in>borel_measurable M. integral\<^sup>N M h \<noteq> \<infinity> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>) \<and> (\<forall>x. 0 \<le> h x)"
 proof -
   obtain A :: "nat \<Rightarrow> 'a set" where
     range[measurable]: "range A \<subseteq> sets M" and
@@ -67,8 +67,8 @@
   proof (safe intro!: bexI[of _ ?h] del: notI)
     have "\<And>i. A i \<in> sets M"
       using range by fastforce+
-    then have "integral\<^sup>P M ?h = (\<Sum>i. n i * emeasure M (A i))" using pos
-      by (simp add: positive_integral_suminf positive_integral_cmult_indicator)
+    then have "integral\<^sup>N M ?h = (\<Sum>i. n i * emeasure M (A i))" using pos
+      by (simp add: nn_integral_suminf nn_integral_cmult_indicator)
     also have "\<dots> \<le> (\<Sum>i. (1 / 2)^Suc i)"
     proof (rule suminf_le_pos)
       fix N
@@ -82,7 +82,7 @@
       finally show "n N * emeasure M (A N) \<le> (1 / 2) ^ Suc N" .
       show "0 \<le> n N * emeasure M (A N)" using n[of N] `A N \<in> sets M` by (simp add: emeasure_nonneg)
     qed
-    finally show "integral\<^sup>P M ?h \<noteq> \<infinity>" unfolding suminf_half_series_ereal by auto
+    finally show "integral\<^sup>N M ?h \<noteq> \<infinity>" unfolding suminf_half_series_ereal by auto
   next
     { fix x assume "x \<in> space M"
       then obtain i where "x \<in> A i" using space[symmetric] by auto
@@ -317,7 +317,7 @@
         (\<integral>\<^sup>+x. g x * indicator (?A \<inter> A) x \<partial>M) +
         (\<integral>\<^sup>+x. f x * indicator ((space M - ?A) \<inter> A) x \<partial>M)"
         using f g sets unfolding G_def
-        by (auto cong: positive_integral_cong intro!: positive_integral_add)
+        by (auto cong: nn_integral_cong intro!: nn_integral_add)
       also have "\<dots> \<le> N (?A \<inter> A) + N ((space M - ?A) \<inter> A)"
         using f g sets unfolding G_def by (auto intro!: add_mono)
       also have "\<dots> = N A"
@@ -338,31 +338,31 @@
       fix A assume "A \<in> sets M"
       have "(\<integral>\<^sup>+x. (SUP i. f i x) * indicator A x \<partial>M) =
         (\<integral>\<^sup>+x. (SUP i. f i x * indicator A x) \<partial>M)"
-        by (intro positive_integral_cong) (simp split: split_indicator)
+        by (intro nn_integral_cong) (simp split: split_indicator)
       also have "\<dots> = (SUP i. (\<integral>\<^sup>+x. f i x * indicator A x \<partial>M))"
         using `incseq f` f `A \<in> sets M`
-        by (intro positive_integral_monotone_convergence_SUP)
+        by (intro nn_integral_monotone_convergence_SUP)
            (auto simp: G_def incseq_Suc_iff le_fun_def split: split_indicator)
       finally show "(\<integral>\<^sup>+x. (SUP i. f i x) * indicator A x \<partial>M) \<le> N A"
         using f `A \<in> sets M` by (auto intro!: SUP_least simp: G_def)
     qed }
   note SUP_in_G = this
-  let ?y = "SUP g : G. integral\<^sup>P M g"
+  let ?y = "SUP g : G. integral\<^sup>N M g"
   have y_le: "?y \<le> N (space M)" unfolding G_def
   proof (safe intro!: SUP_least)
     fix g assume "\<forall>A\<in>sets M. (\<integral>\<^sup>+x. g x * indicator A x \<partial>M) \<le> N A"
-    from this[THEN bspec, OF sets.top] show "integral\<^sup>P M g \<le> N (space M)"
-      by (simp cong: positive_integral_cong)
+    from this[THEN bspec, OF sets.top] show "integral\<^sup>N M g \<le> N (space M)"
+      by (simp cong: nn_integral_cong)
   qed
-  from SUP_countable_SUP [OF `G \<noteq> {}`, of "integral\<^sup>P M"] guess ys .. note ys = this
-  then have "\<forall>n. \<exists>g. g\<in>G \<and> integral\<^sup>P M g = ys n"
+  from SUP_countable_SUP [OF `G \<noteq> {}`, of "integral\<^sup>N M"] guess ys .. note ys = this
+  then have "\<forall>n. \<exists>g. g\<in>G \<and> integral\<^sup>N M g = ys n"
   proof safe
-    fix n assume "range ys \<subseteq> integral\<^sup>P M ` G"
-    hence "ys n \<in> integral\<^sup>P M ` G" by auto
-    thus "\<exists>g. g\<in>G \<and> integral\<^sup>P M g = ys n" by auto
+    fix n assume "range ys \<subseteq> integral\<^sup>N M ` G"
+    hence "ys n \<in> integral\<^sup>N M ` G" by auto
+    thus "\<exists>g. g\<in>G \<and> integral\<^sup>N M g = ys n" by auto
   qed
-  from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. integral\<^sup>P M (gs n) = ys n" by auto
-  hence y_eq: "?y = (SUP i. integral\<^sup>P M (gs i))" using ys by auto
+  from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. integral\<^sup>N M (gs n) = ys n" by auto
+  hence y_eq: "?y = (SUP i. integral\<^sup>N M (gs i))" using ys by auto
   let ?g = "\<lambda>i x. Max ((\<lambda>n. gs n x) ` {..i})"
   def f \<equiv> "\<lambda>x. SUP i. ?g i x"
   let ?F = "\<lambda>A x. f x * indicator A x"
@@ -380,17 +380,17 @@
     by (auto intro!: incseq_SucI le_funI simp add: atMost_Suc)
   from SUP_in_G[OF this g_in_G] have [measurable]: "f \<in> G" unfolding f_def .
   then have [simp, intro]: "f \<in> borel_measurable M" unfolding G_def by auto
-  have "integral\<^sup>P M f = (SUP i. integral\<^sup>P M (?g i))" unfolding f_def
+  have "integral\<^sup>N M f = (SUP i. integral\<^sup>N M (?g i))" unfolding f_def
     using g_in_G `incseq ?g`
-    by (auto intro!: positive_integral_monotone_convergence_SUP simp: G_def)
+    by (auto intro!: nn_integral_monotone_convergence_SUP simp: G_def)
   also have "\<dots> = ?y"
   proof (rule antisym)
-    show "(SUP i. integral\<^sup>P M (?g i)) \<le> ?y"
+    show "(SUP i. integral\<^sup>N M (?g i)) \<le> ?y"
       using g_in_G by (auto intro: SUP_mono)
-    show "?y \<le> (SUP i. integral\<^sup>P M (?g i))" unfolding y_eq
-      by (auto intro!: SUP_mono positive_integral_mono Max_ge)
+    show "?y \<le> (SUP i. integral\<^sup>N M (?g i))" unfolding y_eq
+      by (auto intro!: SUP_mono nn_integral_mono Max_ge)
   qed
-  finally have int_f_eq_y: "integral\<^sup>P M f = ?y" .
+  finally have int_f_eq_y: "integral\<^sup>N M f = ?y" .
   have "\<And>x. 0 \<le> f x"
     unfolding f_def using `\<And>i. gs i \<in> G`
     by (auto intro!: SUP_upper2 Max_ge_iff[THEN iffD2] simp: G_def)
@@ -401,12 +401,12 @@
   have emeasure_M: "\<And>A. A \<in> sets M \<Longrightarrow> emeasure ?M A = ?t A"
   proof (subst emeasure_diff_measure)
     from f_le_N[of "space M"] show "finite_measure N" "finite_measure (density M f)"
-      by (auto intro!: finite_measureI simp: emeasure_density cong: positive_integral_cong)
+      by (auto intro!: finite_measureI simp: emeasure_density cong: nn_integral_cong)
   next
     fix B assume "B \<in> sets N" with f_le_N[of B] show "emeasure (density M f) B \<le> emeasure N B"
-      by (auto simp: sets_eq emeasure_density cong: positive_integral_cong)
+      by (auto simp: sets_eq emeasure_density cong: nn_integral_cong)
   qed (auto simp: sets_eq emeasure_density)
-  from emeasure_M[of "space M"] N.finite_emeasure_space positive_integral_positive[of M "?F (space M)"]
+  from emeasure_M[of "space M"] N.finite_emeasure_space nn_integral_nonneg[of M "?F (space M)"]
   interpret M': finite_measure ?M
     by (auto intro!: finite_measureI simp: sets_eq_imp_space_eq[OF sets_eq] N.emeasure_eq_measure ereal_minus_eq_PInfty_iff)
 
@@ -417,7 +417,7 @@
       unfolding absolutely_continuous_def by auto
     moreover from A_M A_N have "(\<integral>\<^sup>+ x. ?F A x \<partial>M) \<le> N A" using `f \<in> G` by (auto simp: G_def)
     ultimately have "N A - (\<integral>\<^sup>+ x. ?F A x \<partial>M) = 0"
-      using positive_integral_positive[of M] by (auto intro!: antisym)
+      using nn_integral_nonneg[of M] by (auto intro!: antisym)
     then show "A \<in> null_sets ?M"
       using A_M by (simp add: emeasure_M null_sets_def sets_eq)
   qed
@@ -462,11 +462,11 @@
       hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
       have "(\<integral>\<^sup>+x. ?f0 x  * indicator A x \<partial>M) =
         (\<integral>\<^sup>+x. f x * indicator A x + b * indicator (A \<inter> A0) x \<partial>M)"
-        by (auto intro!: positive_integral_cong split: split_indicator)
+        by (auto intro!: nn_integral_cong split: split_indicator)
       hence "(\<integral>\<^sup>+x. ?f0 x * indicator A x \<partial>M) =
           (\<integral>\<^sup>+x. f x * indicator A x \<partial>M) + b * emeasure M (A \<inter> A0)"
         using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A b `f \<in> G`
-        by (simp add: positive_integral_add positive_integral_cmult_indicator G_def) }
+        by (simp add: nn_integral_add nn_integral_cmult_indicator G_def) }
     note f0_eq = this
     { fix A assume A: "A \<in> sets M"
       hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
@@ -480,11 +480,11 @@
         by (auto intro!: add_left_mono simp: sets_eq)
       also have "\<dots> \<le> N A"
         unfolding emeasure_M[OF `A \<in> sets M`]
-        using f_le_v N.emeasure_eq_measure[of A] positive_integral_positive[of M "?F A"]
+        using f_le_v N.emeasure_eq_measure[of A] nn_integral_nonneg[of M "?F A"]
         by (cases "\<integral>\<^sup>+x. ?F A x \<partial>M", cases "N A") auto
       finally have "(\<integral>\<^sup>+x. ?f0 x * indicator A x \<partial>M) \<le> N A" . }
     hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G` by (auto simp: G_def)
-    have int_f_finite: "integral\<^sup>P M f \<noteq> \<infinity>"
+    have int_f_finite: "integral\<^sup>N M f \<noteq> \<infinity>"
       by (metis N.emeasure_finite ereal_infty_less_eq2(1) int_f_eq_y y_le)
     have  "0 < ?M (space M) - emeasure ?Mb (space M)"
       using pos_t
@@ -503,13 +503,13 @@
       by (auto simp: absolutely_continuous_def null_sets_def)
     then have "0 < emeasure M A0" using emeasure_nonneg[of M A0] by auto
     hence "0 < b * emeasure M A0" using b by (auto simp: ereal_zero_less_0_iff)
-    with int_f_finite have "?y + 0 < integral\<^sup>P M f + b * emeasure M A0" unfolding int_f_eq_y
+    with int_f_finite have "?y + 0 < integral\<^sup>N M f + b * emeasure M A0" unfolding int_f_eq_y
       using `f \<in> G`
-      by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 positive_integral_positive)
-    also have "\<dots> = integral\<^sup>P M ?f0" using f0_eq[OF sets.top] `A0 \<in> sets M` sets.sets_into_space
-      by (simp cong: positive_integral_cong)
-    finally have "?y < integral\<^sup>P M ?f0" by simp
-    moreover from `?f0 \<in> G` have "integral\<^sup>P M ?f0 \<le> ?y" by (auto intro!: SUP_upper)
+      by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 nn_integral_nonneg)
+    also have "\<dots> = integral\<^sup>N M ?f0" using f0_eq[OF sets.top] `A0 \<in> sets M` sets.sets_into_space
+      by (simp cong: nn_integral_cong)
+    finally have "?y < integral\<^sup>N M ?f0" by simp
+    moreover from `?f0 \<in> G` have "integral\<^sup>N M ?f0 \<le> ?y" by (auto intro!: SUP_upper)
     ultimately show False by auto
   qed
   let ?f = "\<lambda>x. max 0 (f x)"
@@ -520,7 +520,7 @@
     fix A assume A: "A\<in>sets (density M ?f)"
     then show "emeasure (density M ?f) A = emeasure N A"
       using `f \<in> G` A upper_bound[THEN bspec, of A] N.emeasure_eq_measure[of A]
-      by (cases "integral\<^sup>P M (?F A)")
+      by (cases "integral\<^sup>N M (?F A)")
          (auto intro!: antisym simp add: emeasure_density G_def emeasure_M density_max_0[symmetric])
   qed auto
 qed
@@ -669,10 +669,10 @@
   proof (intro allI finite_measure.Radon_Nikodym_finite_measure)
     fix i
     from Q show "finite_measure (?M i)"
-      by (auto intro!: finite_measureI cong: positive_integral_cong
+      by (auto intro!: finite_measureI cong: nn_integral_cong
                simp add: emeasure_density subset_eq sets_eq)
     from Q have "emeasure (?N i) (space N) = emeasure N (Q i)"
-      by (simp add: sets_eq[symmetric] emeasure_density subset_eq cong: positive_integral_cong)
+      by (simp add: sets_eq[symmetric] emeasure_density subset_eq cong: nn_integral_cong)
     with Q_fin show "finite_measure (?N i)"
       by (auto intro!: finite_measureI)
     show "sets (?N i) = sets (?M i)" by (simp add: sets_eq)
@@ -688,8 +688,8 @@
     by force
   { fix A i assume A: "A \<in> sets M"
     with Q borel have "(\<integral>\<^sup>+x. f i x * indicator (Q i \<inter> A) x \<partial>M) = emeasure (density (?M i) (f i)) A"
-      by (auto simp add: emeasure_density positive_integral_density subset_eq
-               intro!: positive_integral_cong split: split_indicator)
+      by (auto simp add: emeasure_density nn_integral_density subset_eq
+               intro!: nn_integral_cong split: split_indicator)
     also have "\<dots> = emeasure N (Q i \<inter> A)"
       using A Q by (simp add: f_density emeasure_restricted subset_eq sets_eq)
     finally have "emeasure N (Q i \<inter> A) = (\<integral>\<^sup>+x. f i x * indicator (Q i \<inter> A) x \<partial>M)" .. }
@@ -709,13 +709,13 @@
         "\<And>i. AE x in M. 0 \<le> f i x * indicator (Q i \<inter> A) x"
         using borel Qi Q0(1) `A \<in> sets M` by (auto intro!: borel_measurable_ereal_times)
       have "(\<integral>\<^sup>+x. ?f x * indicator A x \<partial>M) = (\<integral>\<^sup>+x. (\<Sum>i. f i x * indicator (Q i \<inter> A) x) + \<infinity> * indicator (Q0 \<inter> A) x \<partial>M)"
-        using borel by (intro positive_integral_cong) (auto simp: indicator_def)
+        using borel by (intro nn_integral_cong) (auto simp: indicator_def)
       also have "\<dots> = (\<integral>\<^sup>+x. (\<Sum>i. f i x * indicator (Q i \<inter> A) x) \<partial>M) + \<infinity> * emeasure M (Q0 \<inter> A)"
         using borel Qi Q0(1) `A \<in> sets M`
-        by (subst positive_integral_add) (auto simp del: ereal_infty_mult
-            simp add: positive_integral_cmult_indicator sets.Int intro!: suminf_0_le)
+        by (subst nn_integral_add) (auto simp del: ereal_infty_mult
+            simp add: nn_integral_cmult_indicator sets.Int intro!: suminf_0_le)
       also have "\<dots> = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)"
-        by (subst integral_eq[OF `A \<in> sets M`], subst positive_integral_suminf) auto
+        by (subst integral_eq[OF `A \<in> sets M`], subst nn_integral_suminf) auto
       finally have "(\<integral>\<^sup>+x. ?f x * indicator A x \<partial>M) = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)" .
       moreover have "(\<Sum>i. N (Q i \<inter> A)) = N ((\<Union>i. Q i) \<inter> A)"
         using Q Q_sets `A \<in> sets M`
@@ -742,7 +742,7 @@
   shows "\<exists>f \<in> borel_measurable M. (\<forall>x. 0 \<le> f x) \<and> density M f = N"
 proof -
   from Ex_finite_integrable_function
-  obtain h where finite: "integral\<^sup>P M h \<noteq> \<infinity>" and
+  obtain h where finite: "integral\<^sup>N M h \<noteq> \<infinity>" and
     borel: "h \<in> borel_measurable M" and
     nn: "\<And>x. 0 \<le> h x" and
     pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
@@ -750,7 +750,7 @@
   let ?T = "\<lambda>A. (\<integral>\<^sup>+x. h x * indicator A x \<partial>M)"
   let ?MT = "density M h"
   from borel finite nn interpret T: finite_measure ?MT
-    by (auto intro!: finite_measureI cong: positive_integral_cong simp: emeasure_density)
+    by (auto intro!: finite_measureI cong: nn_integral_cong simp: emeasure_density)
   have "absolutely_continuous ?MT N" "sets N = sets ?MT"
   proof (unfold absolutely_continuous_def, safe)
     fix A assume "A \<in> null_sets ?MT"
@@ -774,7 +774,7 @@
 lemma finite_density_unique:
   assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
-  and fin: "integral\<^sup>P M f \<noteq> \<infinity>"
+  and fin: "integral\<^sup>N M f \<noteq> \<infinity>"
   shows "density M f = density M g \<longleftrightarrow> (AE x in M. f x = g x)"
 proof (intro iffI ballI)
   fix A assume eq: "AE x in M. f x = g x"
@@ -786,19 +786,19 @@
   with borel have eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
     by (simp add: emeasure_density[symmetric])
   from this[THEN bspec, OF sets.top] fin
-  have g_fin: "integral\<^sup>P M g \<noteq> \<infinity>" by (simp cong: positive_integral_cong)
+  have g_fin: "integral\<^sup>N M g \<noteq> \<infinity>" by (simp cong: nn_integral_cong)
   { fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
       and pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
-      and g_fin: "integral\<^sup>P M g \<noteq> \<infinity>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
+      and g_fin: "integral\<^sup>N M g \<noteq> \<infinity>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
     let ?N = "{x\<in>space M. g x < f x}"
     have N: "?N \<in> sets M" using borel by simp
-    have "?P g ?N \<le> integral\<^sup>P M g" using pos
-      by (intro positive_integral_mono_AE) (auto split: split_indicator)
+    have "?P g ?N \<le> integral\<^sup>N M g" using pos
+      by (intro nn_integral_mono_AE) (auto split: split_indicator)
     then have Pg_fin: "?P g ?N \<noteq> \<infinity>" using g_fin by auto
     have "?P (\<lambda>x. (f x - g x)) ?N = (\<integral>\<^sup>+x. f x * indicator ?N x - g x * indicator ?N x \<partial>M)"
-      by (auto intro!: positive_integral_cong simp: indicator_def)
+      by (auto intro!: nn_integral_cong simp: indicator_def)
     also have "\<dots> = ?P f ?N - ?P g ?N"
-    proof (rule positive_integral_diff)
+    proof (rule nn_integral_diff)
       show "(\<lambda>x. f x * indicator ?N x) \<in> borel_measurable M" "(\<lambda>x. g x * indicator ?N x) \<in> borel_measurable M"
         using borel N by auto
       show "AE x in M. g x * indicator ?N x \<le> f x * indicator ?N x"
@@ -806,10 +806,10 @@
         using pos by (auto split: split_indicator)
     qed fact
     also have "\<dots> = 0"
-      unfolding eq[THEN bspec, OF N] using positive_integral_positive[of M] Pg_fin by auto
+      unfolding eq[THEN bspec, OF N] using nn_integral_nonneg[of M] Pg_fin by auto
     finally have "AE x in M. f x \<le> g x"
-      using pos borel positive_integral_PInf_AE[OF borel(2) g_fin]
-      by (subst (asm) positive_integral_0_iff_AE)
+      using pos borel nn_integral_PInf_AE[OF borel(2) g_fin]
+      by (subst (asm) nn_integral_0_iff_AE)
          (auto split: split_indicator simp: not_less ereal_minus_le_iff) }
   from this[OF borel pos g_fin eq] this[OF borel(2,1) pos(2,1) fin] eq
   show "AE x in M. f x = g x" by auto
@@ -856,9 +856,9 @@
           using borel Q0(1) by auto
         have "?N (?A i) \<le> (\<integral>\<^sup>+x. (i::ereal) * indicator (?A i) x \<partial>M)"
           unfolding eq[OF `?A i \<in> sets M`]
-          by (auto intro!: positive_integral_mono simp: indicator_def)
+          by (auto intro!: nn_integral_mono simp: indicator_def)
         also have "\<dots> = i * emeasure M (?A i)"
-          using `?A i \<in> sets M` by (auto intro!: positive_integral_cmult_indicator)
+          using `?A i \<in> sets M` by (auto intro!: nn_integral_cmult_indicator)
         also have "\<dots> < \<infinity>" using emeasure_real[of "?A i"] by simp
         finally have "?N (?A i) \<noteq> \<infinity>" by simp
         then show "?A i \<in> null_sets M" using in_Q0[OF `?A i \<in> sets M`] `?A i \<in> sets M` by auto
@@ -888,35 +888,35 @@
   shows "AE x in M. f x = f' x"
 proof -
   obtain h where h_borel: "h \<in> borel_measurable M"
-    and fin: "integral\<^sup>P M h \<noteq> \<infinity>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<infinity>" "\<And>x. 0 \<le> h x"
+    and fin: "integral\<^sup>N M h \<noteq> \<infinity>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<infinity>" "\<And>x. 0 \<le> h x"
     using Ex_finite_integrable_function by auto
   then have h_nn: "AE x in M. 0 \<le> h x" by auto
   let ?H = "density M h"
   interpret h: finite_measure ?H
     using fin h_borel pos
-    by (intro finite_measureI) (simp cong: positive_integral_cong emeasure_density add: fin)
+    by (intro finite_measureI) (simp cong: nn_integral_cong emeasure_density add: fin)
   let ?fM = "density M f"
   let ?f'M = "density M f'"
   { fix A assume "A \<in> sets M"
     then have "{x \<in> space M. h x * indicator A x \<noteq> 0} = A"
       using pos(1) sets.sets_into_space by (force simp: indicator_def)
     then have "(\<integral>\<^sup>+x. h x * indicator A x \<partial>M) = 0 \<longleftrightarrow> A \<in> null_sets M"
-      using h_borel `A \<in> sets M` h_nn by (subst positive_integral_0_iff) auto }
+      using h_borel `A \<in> sets M` h_nn by (subst nn_integral_0_iff) auto }
   note h_null_sets = this
   { fix A assume "A \<in> sets M"
     have "(\<integral>\<^sup>+x. f x * (h x * indicator A x) \<partial>M) = (\<integral>\<^sup>+x. h x * indicator A x \<partial>?fM)"
       using `A \<in> sets M` h_borel h_nn f f'
-      by (intro positive_integral_density[symmetric]) auto
+      by (intro nn_integral_density[symmetric]) auto
     also have "\<dots> = (\<integral>\<^sup>+x. h x * indicator A x \<partial>?f'M)"
       by (simp_all add: density_eq)
     also have "\<dots> = (\<integral>\<^sup>+x. f' x * (h x * indicator A x) \<partial>M)"
       using `A \<in> sets M` h_borel h_nn f f'
-      by (intro positive_integral_density) auto
+      by (intro nn_integral_density) auto
     finally have "(\<integral>\<^sup>+x. h x * (f x * indicator A x) \<partial>M) = (\<integral>\<^sup>+x. h x * (f' x * indicator A x) \<partial>M)"
       by (simp add: ac_simps)
     then have "(\<integral>\<^sup>+x. (f x * indicator A x) \<partial>?H) = (\<integral>\<^sup>+x. (f' x * indicator A x) \<partial>?H)"
       using `A \<in> sets M` h_borel h_nn f f'
-      by (subst (asm) (1 2) positive_integral_density[symmetric]) auto }
+      by (subst (asm) (1 2) nn_integral_density[symmetric]) auto }
   then have "AE x in ?H. f x = f' x" using h_borel h_nn f f'
     by (intro h.density_unique_finite_measure absolutely_continuous_AE[of M])
        (auto simp add: AE_density)
@@ -975,17 +975,17 @@
   assume "sigma_finite_measure ?N"
   then interpret N: sigma_finite_measure ?N .
   from N.Ex_finite_integrable_function obtain h where
-    h: "h \<in> borel_measurable M" "integral\<^sup>P ?N h \<noteq> \<infinity>" and
+    h: "h \<in> borel_measurable M" "integral\<^sup>N ?N h \<noteq> \<infinity>" and
     h_nn: "\<And>x. 0 \<le> h x" and
     fin: "\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>" by auto
   have "AE x in M. f x * h x \<noteq> \<infinity>"
   proof (rule AE_I')
-    have "integral\<^sup>P ?N h = (\<integral>\<^sup>+x. f x * h x \<partial>M)" using f h h_nn
-      by (auto intro!: positive_integral_density)
+    have "integral\<^sup>N ?N h = (\<integral>\<^sup>+x. f x * h x \<partial>M)" using f h h_nn
+      by (auto intro!: nn_integral_density)
     then have "(\<integral>\<^sup>+x. f x * h x \<partial>M) \<noteq> \<infinity>"
       using h(2) by simp
     then show "(\<lambda>x. f x * h x) -` {\<infinity>} \<inter> space M \<in> null_sets M"
-      using f h(1) by (auto intro!: positive_integral_PInf borel_measurable_vimage)
+      using f h(1) by (auto intro!: nn_integral_PInf borel_measurable_vimage)
   qed auto
   then show "AE x in M. f x \<noteq> \<infinity>"
     using fin by (auto elim!: AE_Ball_mp)
@@ -1036,14 +1036,14 @@
       case 0
       have "AE x in M. f x * indicator (A i \<inter> Q j) x = 0"
         using AE by (auto simp: A_def `i = 0`)
-      from positive_integral_cong_AE[OF this] show ?thesis by simp
+      from nn_integral_cong_AE[OF this] show ?thesis by simp
     next
       case (Suc n)
       then have "(\<integral>\<^sup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<le>
         (\<integral>\<^sup>+x. (Suc n :: ereal) * indicator (Q j) x \<partial>M)"
-        by (auto intro!: positive_integral_mono simp: indicator_def A_def real_eq_of_nat)
+        by (auto intro!: nn_integral_mono simp: indicator_def A_def real_eq_of_nat)
       also have "\<dots> = Suc n * emeasure M (Q j)"
-        using Q by (auto intro!: positive_integral_cmult_indicator)
+        using Q by (auto intro!: nn_integral_cmult_indicator)
       also have "\<dots> < \<infinity>"
         using Q by (auto simp: real_eq_of_nat[symmetric])
       finally show ?thesis by simp
@@ -1109,15 +1109,15 @@
   "absolutely_continuous M N \<Longrightarrow> sets N = sets M \<Longrightarrow> density M (RN_deriv M N) = N"
   by (metis RN_derivI Radon_Nikodym)
 
-lemma (in sigma_finite_measure) RN_deriv_positive_integral:
+lemma (in sigma_finite_measure) RN_deriv_nn_integral:
   assumes N: "absolutely_continuous M N" "sets N = sets M"
     and f: "f \<in> borel_measurable M"
-  shows "integral\<^sup>P N f = (\<integral>\<^sup>+x. RN_deriv M N x * f x \<partial>M)"
+  shows "integral\<^sup>N N f = (\<integral>\<^sup>+x. RN_deriv M N x * f x \<partial>M)"
 proof -
-  have "integral\<^sup>P N f = integral\<^sup>P (density M (RN_deriv M N)) f"
+  have "integral\<^sup>N N f = integral\<^sup>N (density M (RN_deriv M N)) f"
     using N by (simp add: density_RN_deriv)
   also have "\<dots> = (\<integral>\<^sup>+x. RN_deriv M N x * f x \<partial>M)"
-    using f by (simp add: positive_integral_density RN_deriv_nonneg)
+    using f by (simp add: nn_integral_density RN_deriv_nonneg)
   finally show ?thesis by simp
 qed
 
@@ -1261,9 +1261,9 @@
   have "N (?RN \<infinity>) = (\<integral>\<^sup>+ x. RN_deriv M N x * indicator (?RN \<infinity>) x \<partial>M)"
     using RN(1,3) by (subst RN(2)[symmetric]) (auto simp: emeasure_density)
   also have "\<dots> = (\<integral>\<^sup>+ x. \<infinity> * indicator (?RN \<infinity>) x \<partial>M)"
-    by (intro positive_integral_cong) (auto simp: indicator_def)
+    by (intro nn_integral_cong) (auto simp: indicator_def)
   also have "\<dots> = \<infinity> * emeasure M (?RN \<infinity>)"
-    using RN by (intro positive_integral_cmult_indicator) auto
+    using RN by (intro nn_integral_cmult_indicator) auto
   finally have eq: "N (?RN \<infinity>) = \<infinity> * emeasure M (?RN \<infinity>)" .
   moreover
   have "emeasure M (?RN \<infinity>) = 0"
@@ -1287,7 +1287,7 @@
   have "N (?RN 0) = (\<integral>\<^sup>+ x. RN_deriv M N x * indicator (?RN 0) x \<partial>M)"
     using RN(1,3) by (subst RN(2)[symmetric]) (auto simp: emeasure_density)
   also have "\<dots> = (\<integral>\<^sup>+ x. 0 \<partial>M)"
-    by (intro positive_integral_cong) (auto simp: indicator_def)
+    by (intro nn_integral_cong) (auto simp: indicator_def)
   finally have "AE x in N. RN_deriv M N x \<noteq> 0"
     using RN by (subst AE_iff_measurable[OF _ refl]) (auto simp: ac cong: sets_eq_imp_space_eq)
   with RN(3) eq show "AE x in N. 0 < real (RN_deriv M N x)"
@@ -1301,9 +1301,9 @@
 proof -
   from `{x} \<in> sets M`
   have "density M (RN_deriv M N) {x} = (\<integral>\<^sup>+w. RN_deriv M N x * indicator {x} w \<partial>M)"
-    by (auto simp: indicator_def emeasure_density intro!: positive_integral_cong)
+    by (auto simp: indicator_def emeasure_density intro!: nn_integral_cong)
   with x density_RN_deriv[OF ac] RN_deriv_nonneg[of M N] show ?thesis
-    by (auto simp: positive_integral_cmult_indicator)
+    by (auto simp: nn_integral_cmult_indicator)
 qed
 
 end