renamed positive_integral to nn_integral
authorhoelzl
Mon May 19 14:26:58 2014 +0200 (2014-05-19)
changeset 56996891e992e510f
parent 56995 61855ade6c7e
child 57001 db2e51a80ab5
renamed positive_integral to nn_integral
NEWS
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Distributions.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
     1.1 --- a/NEWS	Mon May 19 13:53:58 2014 +0200
     1.2 +++ b/NEWS	Mon May 19 14:26:58 2014 +0200
     1.3 @@ -733,6 +733,13 @@
     1.4      integral_cmul_indicator
     1.5      integral_real
     1.6  
     1.7 +  - Renamed positive_integral to nn_integral:
     1.8 +
     1.9 +    * Renamed all lemmas "*positive_integral*" to *nn_integral*"
    1.10 +      positive_integral_positive ~> nn_integral_nonneg
    1.11 +
    1.12 +    * Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
    1.13 +
    1.14  *** Scala ***
    1.15  
    1.16  * The signature and semantics of Document.Snapshot.cumulate_markup /
     2.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Mon May 19 13:53:58 2014 +0200
     2.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Mon May 19 14:26:58 2014 +0200
     2.3 @@ -239,7 +239,7 @@
     2.4    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")
     2.5  proof (rule emeasure_measure_of[OF pair_measure_def])
     2.6    show "positive (sets (N \<Otimes>\<^sub>M M)) ?\<mu>"
     2.7 -    by (auto simp: positive_def positive_integral_positive)
     2.8 +    by (auto simp: positive_def nn_integral_nonneg)
     2.9    have eq[simp]: "\<And>A x y. indicator A (x, y) = indicator (Pair x -` A) y"
    2.10      by (auto simp: indicator_def)
    2.11    show "countably_additive (sets (N \<Otimes>\<^sub>M M)) ?\<mu>"
    2.12 @@ -253,8 +253,8 @@
    2.13      moreover have "\<And>x. range (\<lambda>i. Pair x -` F i) \<subseteq> sets M"
    2.14        using F by (auto simp: sets_Pair1)
    2.15      ultimately show "(\<Sum>n. ?\<mu> (F n)) = ?\<mu> (\<Union>i. F i)"
    2.16 -      by (auto simp add: vimage_UN positive_integral_suminf[symmetric] suminf_emeasure subset_eq emeasure_nonneg sets_Pair1
    2.17 -               intro!: positive_integral_cong positive_integral_indicator[symmetric])
    2.18 +      by (auto simp add: vimage_UN nn_integral_suminf[symmetric] suminf_emeasure subset_eq emeasure_nonneg sets_Pair1
    2.19 +               intro!: nn_integral_cong nn_integral_indicator[symmetric])
    2.20    qed
    2.21    show "{a \<times> b |a b. a \<in> sets N \<and> b \<in> sets M} \<subseteq> Pow (space N \<times> space M)"
    2.22      using sets.space_closed[of N] sets.space_closed[of M] by auto
    2.23 @@ -267,7 +267,7 @@
    2.24    have [simp]: "\<And>x y. indicator X (x, y) = indicator (Pair x -` X) y"
    2.25      by (auto simp: indicator_def)
    2.26    show ?thesis
    2.27 -    using X by (auto intro!: positive_integral_cong simp: emeasure_pair_measure sets_Pair1)
    2.28 +    using X by (auto intro!: nn_integral_cong simp: emeasure_pair_measure sets_Pair1)
    2.29  qed
    2.30  
    2.31  lemma (in sigma_finite_measure) emeasure_pair_measure_Times:
    2.32 @@ -275,9 +275,9 @@
    2.33    shows "emeasure (N \<Otimes>\<^sub>M M) (A \<times> B) = emeasure N A * emeasure M B"
    2.34  proof -
    2.35    have "emeasure (N \<Otimes>\<^sub>M M) (A \<times> B) = (\<integral>\<^sup>+x. emeasure M B * indicator A x \<partial>N)"
    2.36 -    using A B by (auto intro!: positive_integral_cong simp: emeasure_pair_measure_alt)
    2.37 +    using A B by (auto intro!: nn_integral_cong simp: emeasure_pair_measure_alt)
    2.38    also have "\<dots> = emeasure M B * emeasure N A"
    2.39 -    using A by (simp add: emeasure_nonneg positive_integral_cmult_indicator)
    2.40 +    using A by (simp add: emeasure_nonneg nn_integral_cmult_indicator)
    2.41    finally show ?thesis
    2.42      by (simp add: ac_simps)
    2.43  qed
    2.44 @@ -418,7 +418,7 @@
    2.45    proof (rule AE_I)
    2.46      from N measurable_emeasure_Pair1[OF `N \<in> sets (M1 \<Otimes>\<^sub>M M2)`]
    2.47      show "emeasure M1 {x\<in>space M1. emeasure M2 (Pair x -` N) \<noteq> 0} = 0"
    2.48 -      by (auto simp: M2.emeasure_pair_measure_alt positive_integral_0_iff emeasure_nonneg)
    2.49 +      by (auto simp: M2.emeasure_pair_measure_alt nn_integral_0_iff emeasure_nonneg)
    2.50      show "{x \<in> space M1. emeasure M2 (Pair x -` N) \<noteq> 0} \<in> sets M1"
    2.51        by (intro borel_measurable_ereal_neq_const measurable_emeasure_Pair1 N)
    2.52      { fix x assume "x \<in> space M1" "emeasure M2 (Pair x -` N) = 0"
    2.53 @@ -446,9 +446,9 @@
    2.54      by (simp add: M2.emeasure_pair_measure)
    2.55    also have "\<dots> = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. 0 \<partial>M2 \<partial>M1)"
    2.56      using ae
    2.57 -    apply (safe intro!: positive_integral_cong_AE)
    2.58 +    apply (safe intro!: nn_integral_cong_AE)
    2.59      apply (intro AE_I2)
    2.60 -    apply (safe intro!: positive_integral_cong_AE)
    2.61 +    apply (safe intro!: nn_integral_cong_AE)
    2.62      apply auto
    2.63      done
    2.64    finally show "emeasure (M1 \<Otimes>\<^sub>M M2) {x \<in> space (M1 \<Otimes>\<^sub>M M2). \<not> P x} = 0" by simp
    2.65 @@ -486,7 +486,7 @@
    2.66    "x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^sub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L"
    2.67    by simp
    2.68  
    2.69 -lemma (in sigma_finite_measure) borel_measurable_positive_integral_fst':
    2.70 +lemma (in sigma_finite_measure) borel_measurable_nn_integral_fst':
    2.71    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)" "\<And>x. 0 \<le> f x"
    2.72    shows "(\<lambda>x. \<integral>\<^sup>+ y. f (x, y) \<partial>M) \<in> borel_measurable M1"
    2.73  using f proof induct
    2.74 @@ -495,7 +495,7 @@
    2.75      by (auto simp: space_pair_measure)
    2.76    show ?case
    2.77      apply (subst measurable_cong)
    2.78 -    apply (rule positive_integral_cong)
    2.79 +    apply (rule nn_integral_cong)
    2.80      apply fact+
    2.81      done
    2.82  next
    2.83 @@ -506,56 +506,56 @@
    2.84      by (simp add: sets_Pair1[OF set])
    2.85    from this measurable_emeasure_Pair[OF set] show ?case
    2.86      by (rule measurable_cong[THEN iffD1])
    2.87 -qed (simp_all add: positive_integral_add positive_integral_cmult measurable_compose_Pair1
    2.88 -                   positive_integral_monotone_convergence_SUP incseq_def le_fun_def
    2.89 +qed (simp_all add: nn_integral_add nn_integral_cmult measurable_compose_Pair1
    2.90 +                   nn_integral_monotone_convergence_SUP incseq_def le_fun_def
    2.91                cong: measurable_cong)
    2.92  
    2.93 -lemma (in sigma_finite_measure) positive_integral_fst':
    2.94 +lemma (in sigma_finite_measure) nn_integral_fst':
    2.95    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)" "\<And>x. 0 \<le> f x"
    2.96 -  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 = _")
    2.97 +  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 = _")
    2.98  using f proof induct
    2.99    case (cong u v)
   2.100    then have "?I u = ?I v"
   2.101 -    by (intro positive_integral_cong) (auto simp: space_pair_measure)
   2.102 +    by (intro nn_integral_cong) (auto simp: space_pair_measure)
   2.103    with cong show ?case
   2.104 -    by (simp cong: positive_integral_cong)
   2.105 -qed (simp_all add: emeasure_pair_measure positive_integral_cmult positive_integral_add
   2.106 -                   positive_integral_monotone_convergence_SUP
   2.107 -                   measurable_compose_Pair1 positive_integral_positive
   2.108 -                   borel_measurable_positive_integral_fst' positive_integral_mono incseq_def le_fun_def
   2.109 -              cong: positive_integral_cong)
   2.110 +    by (simp cong: nn_integral_cong)
   2.111 +qed (simp_all add: emeasure_pair_measure nn_integral_cmult nn_integral_add
   2.112 +                   nn_integral_monotone_convergence_SUP
   2.113 +                   measurable_compose_Pair1 nn_integral_nonneg
   2.114 +                   borel_measurable_nn_integral_fst' nn_integral_mono incseq_def le_fun_def
   2.115 +              cong: nn_integral_cong)
   2.116  
   2.117 -lemma (in sigma_finite_measure) positive_integral_fst:
   2.118 +lemma (in sigma_finite_measure) nn_integral_fst:
   2.119    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)"
   2.120 -  shows "(\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x, y) \<partial>M) \<partial>M1) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M) f"
   2.121 +  shows "(\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x, y) \<partial>M) \<partial>M1) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M) f"
   2.122    using f
   2.123 -    borel_measurable_positive_integral_fst'[of "\<lambda>x. max 0 (f x)"]
   2.124 -    positive_integral_fst'[of "\<lambda>x. max 0 (f x)"]
   2.125 -  unfolding positive_integral_max_0 by auto
   2.126 +    borel_measurable_nn_integral_fst'[of "\<lambda>x. max 0 (f x)"]
   2.127 +    nn_integral_fst'[of "\<lambda>x. max 0 (f x)"]
   2.128 +  unfolding nn_integral_max_0 by auto
   2.129  
   2.130 -lemma (in sigma_finite_measure) borel_measurable_positive_integral[measurable (raw)]:
   2.131 +lemma (in sigma_finite_measure) borel_measurable_nn_integral[measurable (raw)]:
   2.132    "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"
   2.133 -  using borel_measurable_positive_integral_fst'[of "\<lambda>x. max 0 (split f x)" N]
   2.134 -  by (simp add: positive_integral_max_0)
   2.135 +  using borel_measurable_nn_integral_fst'[of "\<lambda>x. max 0 (split f x)" N]
   2.136 +  by (simp add: nn_integral_max_0)
   2.137  
   2.138 -lemma (in pair_sigma_finite) positive_integral_snd:
   2.139 +lemma (in pair_sigma_finite) nn_integral_snd:
   2.140    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
   2.141 -  shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M2) f"
   2.142 +  shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M2) f"
   2.143  proof -
   2.144    note measurable_pair_swap[OF f]
   2.145 -  from M1.positive_integral_fst[OF this]
   2.146 +  from M1.nn_integral_fst[OF this]
   2.147    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))"
   2.148      by simp
   2.149 -  also have "(\<integral>\<^sup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^sub>M M1)) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M2) f"
   2.150 +  also have "(\<integral>\<^sup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^sub>M M1)) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M2) f"
   2.151      by (subst distr_pair_swap)
   2.152 -       (auto simp: positive_integral_distr[OF measurable_pair_swap' f] intro!: positive_integral_cong)
   2.153 +       (auto simp: nn_integral_distr[OF measurable_pair_swap' f] intro!: nn_integral_cong)
   2.154    finally show ?thesis .
   2.155  qed
   2.156  
   2.157  lemma (in pair_sigma_finite) Fubini:
   2.158    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
   2.159    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)"
   2.160 -  unfolding positive_integral_snd[OF assms] M2.positive_integral_fst[OF assms] ..
   2.161 +  unfolding nn_integral_snd[OF assms] M2.nn_integral_fst[OF assms] ..
   2.162  
   2.163  subsection {* Products on counting spaces, densities and distributions *}
   2.164  
   2.165 @@ -602,7 +602,7 @@
   2.166      apply (subst emeasure_count_space)
   2.167      using X_subset apply auto []
   2.168      apply (simp add: fin_Pair emeasure_count_space X_subset fin_X)
   2.169 -    apply (subst positive_integral_count_space)
   2.170 +    apply (subst nn_integral_count_space)
   2.171      using A apply simp
   2.172      apply (simp del: real_of_nat_setsum add: real_of_nat_setsum[symmetric])
   2.173      apply (subst card_gt_0_iff)
   2.174 @@ -626,12 +626,12 @@
   2.175    fix A assume A: "A \<in> sets ?L"
   2.176    with f g have "(\<integral>\<^sup>+ x. f x * \<integral>\<^sup>+ y. g y * indicator A (x, y) \<partial>M2 \<partial>M1) =
   2.177      (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f x * g y * indicator A (x, y) \<partial>M2 \<partial>M1)"
   2.178 -    by (intro positive_integral_cong_AE)
   2.179 -       (auto simp add: positive_integral_cmult[symmetric] ac_simps)
   2.180 +    by (intro nn_integral_cong_AE)
   2.181 +       (auto simp add: nn_integral_cmult[symmetric] ac_simps)
   2.182    with A f g show "emeasure ?L A = emeasure ?R A"
   2.183 -    by (simp add: D2.emeasure_pair_measure emeasure_density positive_integral_density
   2.184 -                  M2.positive_integral_fst[symmetric]
   2.185 -             cong: positive_integral_cong)
   2.186 +    by (simp add: D2.emeasure_pair_measure emeasure_density nn_integral_density
   2.187 +                  M2.nn_integral_fst[symmetric]
   2.188 +             cong: nn_integral_cong)
   2.189  qed simp
   2.190  
   2.191  lemma sigma_finite_measure_distr:
   2.192 @@ -662,8 +662,8 @@
   2.193    fix A assume A: "A \<in> sets ?P"
   2.194    with f g show "emeasure ?P A = emeasure ?D A"
   2.195      by (auto simp add: N.emeasure_pair_measure_alt space_pair_measure emeasure_distr
   2.196 -                       T.emeasure_pair_measure_alt positive_integral_distr
   2.197 -             intro!: positive_integral_cong arg_cong[where f="emeasure N"])
   2.198 +                       T.emeasure_pair_measure_alt nn_integral_distr
   2.199 +             intro!: nn_integral_cong arg_cong[where f="emeasure N"])
   2.200  qed simp
   2.201  
   2.202  lemma pair_measure_eqI:
     3.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Mon May 19 13:53:58 2014 +0200
     3.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Mon May 19 14:26:58 2014 +0200
     3.3 @@ -284,10 +284,10 @@
     3.4  
     3.5    from m have "m * emeasure M {x\<in>space M. 0 \<noteq> f x} = 
     3.6      (\<integral>\<^sup>+x. m * indicator {x\<in>space M. 0 \<noteq> f x} x \<partial>M)"
     3.7 -    using f by (intro positive_integral_cmult_indicator[symmetric]) auto
     3.8 +    using f by (intro nn_integral_cmult_indicator[symmetric]) auto
     3.9    also have "\<dots> \<le> (\<integral>\<^sup>+x. f x \<partial>M)"
    3.10      using AE_space
    3.11 -  proof (intro positive_integral_mono_AE, eventually_elim)
    3.12 +  proof (intro nn_integral_mono_AE, eventually_elim)
    3.13      fix x assume "x \<in> space M"
    3.14      with nn show "m * indicator {x \<in> space M. 0 \<noteq> f x} x \<le> f x"
    3.15        using f by (auto split: split_indicator simp: simple_function_def m_def)
    3.16 @@ -447,7 +447,7 @@
    3.17    finally show ?thesis .
    3.18  qed
    3.19  
    3.20 -lemma simple_bochner_integral_eq_positive_integral:
    3.21 +lemma simple_bochner_integral_eq_nn_integral:
    3.22    assumes f: "simple_bochner_integrable M f" "\<And>x. 0 \<le> f x"
    3.23    shows "simple_bochner_integral M f = (\<integral>\<^sup>+x. f x \<partial>M)"
    3.24  proof -
    3.25 @@ -479,7 +479,7 @@
    3.26               simp del: setsum_ereal times_ereal.simps(1))
    3.27    also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)"
    3.28      using f
    3.29 -    by (intro positive_integral_eq_simple_integral[symmetric])
    3.30 +    by (intro nn_integral_eq_simple_integral[symmetric])
    3.31         (auto simp: simple_function_compose1 simple_bochner_integrable.simps)
    3.32    finally show ?thesis .
    3.33  qed
    3.34 @@ -502,13 +502,13 @@
    3.35      by (auto intro!: simple_bochner_integral_norm_bound)
    3.36    also have "\<dots> = (\<integral>\<^sup>+x. norm (s x - t x) \<partial>M)"
    3.37      using simple_bochner_integrable_compose2[of "\<lambda>x y. norm (x - y)" M "s" "t"] s t
    3.38 -    by (auto intro!: simple_bochner_integral_eq_positive_integral)
    3.39 +    by (auto intro!: simple_bochner_integral_eq_nn_integral)
    3.40    also have "\<dots> \<le> (\<integral>\<^sup>+x. ereal (norm (f x - s x)) + ereal (norm (f x - t x)) \<partial>M)"
    3.41 -    by (auto intro!: positive_integral_mono)
    3.42 +    by (auto intro!: nn_integral_mono)
    3.43         (metis (erased, hide_lams) add_diff_cancel_left add_diff_eq diff_add_eq order_trans
    3.44                norm_minus_commute norm_triangle_ineq4 order_refl)
    3.45    also have "\<dots> = ?S + ?T"
    3.46 -   by (rule positive_integral_add) auto
    3.47 +   by (rule nn_integral_add) auto
    3.48    finally show ?thesis .
    3.49  qed
    3.50  
    3.51 @@ -524,14 +524,14 @@
    3.52    assumes "M = N" "\<And>x. x \<in> space N \<Longrightarrow> f x = g x" "x = y"
    3.53    shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral N g y"
    3.54    unfolding has_bochner_integral.simps assms(1,3)
    3.55 -  using assms(2) by (simp cong: measurable_cong_strong positive_integral_cong_strong)
    3.56 +  using assms(2) by (simp cong: measurable_cong_strong nn_integral_cong_strong)
    3.57  
    3.58  lemma has_bochner_integral_cong_AE:
    3.59    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow>
    3.60      has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
    3.61    unfolding has_bochner_integral.simps
    3.62    by (intro arg_cong[where f=Ex] ext conj_cong rev_conj_cong refl arg_cong[where f="\<lambda>x. x ----> 0"]
    3.63 -            positive_integral_cong_AE)
    3.64 +            nn_integral_cong_AE)
    3.65       auto
    3.66  
    3.67  lemma borel_measurable_has_bochner_integral[measurable_dest]:
    3.68 @@ -557,7 +557,7 @@
    3.69        using A by auto
    3.70    qed (rule simple_function_indicator assms)+
    3.71    moreover have "simple_bochner_integral M (indicator A) = measure M A"
    3.72 -    using simple_bochner_integral_eq_positive_integral[OF sbi] A
    3.73 +    using simple_bochner_integral_eq_nn_integral[OF sbi] A
    3.74      by (simp add: ereal_indicator emeasure_eq_ereal_measure)
    3.75    ultimately show ?thesis
    3.76      by (metis has_bochner_integral_simple_bochner_integrable)
    3.77 @@ -584,14 +584,14 @@
    3.78      (is "?f ----> 0")
    3.79    proof (rule tendsto_sandwich)
    3.80      show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) ----> 0"
    3.81 -      by (auto simp: positive_integral_positive)
    3.82 +      by (auto simp: nn_integral_nonneg)
    3.83      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"
    3.84        (is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
    3.85      proof (intro always_eventually allI)
    3.86        fix i have "?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) + ereal (norm (g x - sg i x)) \<partial>M)"
    3.87 -        by (auto intro!: positive_integral_mono norm_diff_triangle_ineq)
    3.88 +        by (auto intro!: nn_integral_mono norm_diff_triangle_ineq)
    3.89        also have "\<dots> = ?g i"
    3.90 -        by (intro positive_integral_add) auto
    3.91 +        by (intro nn_integral_add) auto
    3.92        finally show "?f i \<le> ?g i" .
    3.93      qed
    3.94      show "?g ----> 0"
    3.95 @@ -625,15 +625,15 @@
    3.96      (is "?f ----> 0")
    3.97    proof (rule tendsto_sandwich)
    3.98      show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) ----> 0"
    3.99 -      by (auto simp: positive_integral_positive)
   3.100 +      by (auto simp: nn_integral_nonneg)
   3.101  
   3.102      show "eventually (\<lambda>i. ?f i \<le> K * (\<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M)) sequentially"
   3.103        (is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
   3.104      proof (intro always_eventually allI)
   3.105        fix i have "?f i \<le> (\<integral>\<^sup>+ x. ereal K * norm (f x - s i x) \<partial>M)"
   3.106 -        using K by (intro positive_integral_mono) (auto simp: mult_ac)
   3.107 +        using K by (intro nn_integral_mono) (auto simp: mult_ac)
   3.108        also have "\<dots> = ?g i"
   3.109 -        using K by (intro positive_integral_cmult) auto
   3.110 +        using K by (intro nn_integral_cmult) auto
   3.111        finally show "?f i \<le> ?g i" .
   3.112      qed
   3.113      show "?g ----> 0"
   3.114 @@ -738,15 +738,15 @@
   3.115    then have "\<And>x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> m" "0 \<le> m"
   3.116      by (auto simp: m_def image_comp comp_def Max_ge_iff)
   3.117    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)"
   3.118 -    by (auto split: split_indicator intro!: Max_ge positive_integral_mono simp:)
   3.119 +    by (auto split: split_indicator intro!: Max_ge nn_integral_mono simp:)
   3.120    also have "\<dots> < \<infinity>"
   3.121 -    using s by (subst positive_integral_cmult_indicator) (auto simp: `0 \<le> m` simple_bochner_integrable.simps)
   3.122 +    using s by (subst nn_integral_cmult_indicator) (auto simp: `0 \<le> m` simple_bochner_integrable.simps)
   3.123    finally have s_fin: "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>" .
   3.124  
   3.125    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)"
   3.126 -    by (auto intro!: positive_integral_mono) (metis add_commute norm_triangle_sub)
   3.127 +    by (auto intro!: nn_integral_mono) (metis add_commute norm_triangle_sub)
   3.128    also have "\<dots> = (\<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) + (\<integral>\<^sup>+x. norm (s i x) \<partial>M)"
   3.129 -    by (rule positive_integral_add) auto
   3.130 +    by (rule nn_integral_add) auto
   3.131    also have "\<dots> < \<infinity>"
   3.132      using s_fin f_s_fin by auto
   3.133    finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" .
   3.134 @@ -776,13 +776,13 @@
   3.135        have "ereal (norm (?s n)) \<le> simple_bochner_integral M (\<lambda>x. norm (s n x))"
   3.136          by (auto intro!: simple_bochner_integral_norm_bound)
   3.137        also have "\<dots> = (\<integral>\<^sup>+x. norm (s n x) \<partial>M)"
   3.138 -        by (intro simple_bochner_integral_eq_positive_integral)
   3.139 +        by (intro simple_bochner_integral_eq_nn_integral)
   3.140             (auto intro: s simple_bochner_integrable_compose2)
   3.141        also have "\<dots> \<le> (\<integral>\<^sup>+x. ereal (norm (f x - s n x)) + norm (f x) \<partial>M)"
   3.142 -        by (auto intro!: positive_integral_mono)
   3.143 +        by (auto intro!: nn_integral_mono)
   3.144             (metis add_commute norm_minus_commute norm_triangle_sub)
   3.145        also have "\<dots> = ?t n" 
   3.146 -        by (rule positive_integral_add) auto
   3.147 +        by (rule nn_integral_add) auto
   3.148        finally show "norm (?s n) \<le> ?t n" .
   3.149      qed
   3.150      have "?t ----> 0 + (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
   3.151 @@ -816,7 +816,7 @@
   3.152    have "(\<lambda>i. ereal (norm (?s i - ?t i))) ----> ereal 0"
   3.153    proof (rule tendsto_sandwich)
   3.154      show "eventually (\<lambda>i. 0 \<le> ereal (norm (?s i - ?t i))) sequentially" "(\<lambda>_. 0) ----> ereal 0"
   3.155 -      by (auto simp: positive_integral_positive zero_ereal_def[symmetric])
   3.156 +      by (auto simp: nn_integral_nonneg zero_ereal_def[symmetric])
   3.157  
   3.158      show "eventually (\<lambda>i. norm (?s i - ?t i) \<le> ?S i + ?T i) sequentially"
   3.159        by (intro always_eventually allI simple_bochner_integral_bounded s t f)
   3.160 @@ -841,7 +841,7 @@
   3.161    fix s assume "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
   3.162    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)"
   3.163      using ae
   3.164 -    by (intro ext positive_integral_cong_AE, eventually_elim) simp
   3.165 +    by (intro ext nn_integral_cong_AE, eventually_elim) simp
   3.166    finally show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x - s i x)) \<partial>M) ----> 0" .
   3.167  qed (auto intro: g)
   3.168  
   3.169 @@ -1087,7 +1087,7 @@
   3.170          by (intro simple_bochner_integral_bounded s f)
   3.171        also have "\<dots> < ereal (e / 2) + e / 2"
   3.172          using ereal_add_strict_mono[OF less_imp_le[OF M[OF n]] _ `?S n \<noteq> \<infinity>` M[OF m]]
   3.173 -        by (auto simp: positive_integral_positive)
   3.174 +        by (auto simp: nn_integral_nonneg)
   3.175        also have "\<dots> = e" by simp
   3.176        finally show "dist (?s n) (?s m) < e"
   3.177          by (simp add: dist_norm)
   3.178 @@ -1098,7 +1098,7 @@
   3.179      by (rule, rule) fact+
   3.180  qed
   3.181  
   3.182 -lemma positive_integral_dominated_convergence_norm:
   3.183 +lemma nn_integral_dominated_convergence_norm:
   3.184    fixes u' :: "_ \<Rightarrow> _::{real_normed_vector, second_countable_topology}"
   3.185    assumes [measurable]:
   3.186         "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
   3.187 @@ -1122,9 +1122,9 @@
   3.188    qed
   3.189    
   3.190    have "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) ----> (\<integral>\<^sup>+x. 0 \<partial>M)"
   3.191 -  proof (rule positive_integral_dominated_convergence)  
   3.192 +  proof (rule nn_integral_dominated_convergence)  
   3.193      show "(\<integral>\<^sup>+x. 2 * w x \<partial>M) < \<infinity>"
   3.194 -      by (rule positive_integral_mult_bounded_inf[OF _ w, of 2]) auto
   3.195 +      by (rule nn_integral_mult_bounded_inf[OF _ w, of 2]) auto
   3.196      show "AE x in M. (\<lambda>i. ereal (norm (u' x - u i x))) ----> 0"
   3.197        using u' 
   3.198      proof eventually_elim
   3.199 @@ -1152,9 +1152,9 @@
   3.200    proof (rule integrableI_sequence)
   3.201      { fix i
   3.202        have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. 2 * ereal (norm (f x)) \<partial>M)"
   3.203 -        by (intro positive_integral_mono) (simp add: bound)
   3.204 +        by (intro nn_integral_mono) (simp add: bound)
   3.205        also have "\<dots> = 2 * (\<integral>\<^sup>+x. ereal (norm (f x)) \<partial>M)"
   3.206 -        by (rule positive_integral_cmult) auto
   3.207 +        by (rule nn_integral_cmult) auto
   3.208        finally have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>"
   3.209          using fin by auto }
   3.210      note fin_s = this
   3.211 @@ -1163,13 +1163,13 @@
   3.212        by (rule simple_bochner_integrableI_bounded) fact+
   3.213  
   3.214      show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
   3.215 -    proof (rule positive_integral_dominated_convergence_norm)
   3.216 +    proof (rule nn_integral_dominated_convergence_norm)
   3.217        show "\<And>j. AE x in M. norm (s j x) \<le> 2 * norm (f x)"
   3.218          using bound by auto
   3.219        show "\<And>i. s i \<in> borel_measurable M" "(\<lambda>x. 2 * norm (f x)) \<in> borel_measurable M"
   3.220          using s by (auto intro: borel_measurable_simple_function)
   3.221        show "(\<integral>\<^sup>+ x. ereal (2 * norm (f x)) \<partial>M) < \<infinity>"
   3.222 -        using fin unfolding times_ereal.simps(1)[symmetric] by (subst positive_integral_cmult) auto
   3.223 +        using fin unfolding times_ereal.simps(1)[symmetric] by (subst nn_integral_cmult) auto
   3.224        show "AE x in M. (\<lambda>i. s i x) ----> f x"
   3.225          using pointwise by auto
   3.226      qed fact
   3.227 @@ -1182,7 +1182,7 @@
   3.228    shows "integrable M f"
   3.229  proof -
   3.230    have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
   3.231 -    using assms by (intro positive_integral_cong_AE) auto
   3.232 +    using assms by (intro nn_integral_cong_AE) auto
   3.233    then show ?thesis
   3.234      using assms by (intro integrableI_bounded) auto
   3.235  qed
   3.236 @@ -1203,7 +1203,7 @@
   3.237    assume "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   3.238    assume "AE x in M. norm (g x) \<le> norm (f x)"
   3.239    then have "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
   3.240 -    by  (intro positive_integral_mono_AE) auto
   3.241 +    by  (intro nn_integral_mono_AE) auto
   3.242    also assume "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
   3.243    finally show "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) < \<infinity>" .
   3.244  qed 
   3.245 @@ -1249,7 +1249,7 @@
   3.246  
   3.247  lemma integrable_indicator_iff:
   3.248    "integrable M (indicator A::_ \<Rightarrow> real) \<longleftrightarrow> A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
   3.249 -  by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ereal_indicator positive_integral_indicator'
   3.250 +  by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ereal_indicator nn_integral_indicator'
   3.251             cong: conj_cong)
   3.252  
   3.253  lemma integral_dominated_convergence:
   3.254 @@ -1264,7 +1264,7 @@
   3.255    have "AE x in M. 0 \<le> w x"
   3.256      using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans)
   3.257    then have "(\<integral>\<^sup>+x. w x \<partial>M) = (\<integral>\<^sup>+x. norm (w x) \<partial>M)"
   3.258 -    by (intro positive_integral_cong_AE) auto
   3.259 +    by (intro nn_integral_cong_AE) auto
   3.260    with `integrable M w` have w: "w \<in> borel_measurable M" "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
   3.261      unfolding integrable_iff_bounded by auto
   3.262  
   3.263 @@ -1273,7 +1273,7 @@
   3.264    proof
   3.265      fix i 
   3.266      have "(\<integral>\<^sup>+ x. ereal (norm (s i x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
   3.267 -      using bound by (intro positive_integral_mono_AE) auto
   3.268 +      using bound by (intro nn_integral_mono_AE) auto
   3.269      with w show "(\<integral>\<^sup>+ x. ereal (norm (s i x)) \<partial>M) < \<infinity>" by auto
   3.270    qed fact
   3.271  
   3.272 @@ -1285,7 +1285,7 @@
   3.273    proof
   3.274      have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
   3.275        using all_bound lim
   3.276 -    proof (intro positive_integral_mono_AE, eventually_elim)
   3.277 +    proof (intro nn_integral_mono_AE, eventually_elim)
   3.278        fix x assume "\<forall>i. norm (s i x) \<le> w x" "(\<lambda>i. s i x) ----> f x"
   3.279        then show "ereal (norm (f x)) \<le> ereal (w x)"
   3.280          by (intro LIMSEQ_le_const2[where X="\<lambda>i. ereal (norm (s i x))"] tendsto_intros lim_ereal[THEN iffD2]) auto
   3.281 @@ -1308,7 +1308,7 @@
   3.282      show "(\<lambda>n. \<integral>\<^sup>+x. norm (s n x - f x) \<partial>M) ----> ereal 0"
   3.283        unfolding zero_ereal_def[symmetric]
   3.284        apply (subst norm_minus_commute)
   3.285 -    proof (rule positive_integral_dominated_convergence_norm[where w=w])
   3.286 +    proof (rule nn_integral_dominated_convergence_norm[where w=w])
   3.287        show "\<And>n. s n \<in> borel_measurable M"
   3.288          using int_s unfolding integrable_iff_bounded by auto
   3.289      qed fact+
   3.290 @@ -1325,7 +1325,7 @@
   3.291    using integrable_mult_left[of c M f] integrable_mult_left[of "1 / c" M "\<lambda>x. c * f x"]
   3.292    by (cases "c = 0") auto
   3.293  
   3.294 -lemma positive_integral_eq_integral:
   3.295 +lemma nn_integral_eq_integral:
   3.296    assumes f: "integrable M f"
   3.297    assumes nonneg: "AE x in M. 0 \<le> f x" 
   3.298    shows "(\<integral>\<^sup>+ x. f x \<partial>M) = integral\<^sup>L M f"
   3.299 @@ -1338,7 +1338,7 @@
   3.300      next
   3.301        case (mult f c) then show ?case
   3.302          unfolding times_ereal.simps(1)[symmetric]
   3.303 -        by (subst positive_integral_cmult)
   3.304 +        by (subst nn_integral_cmult)
   3.305             (auto simp add: integrable_mult_left_iff zero_ereal_def[symmetric])
   3.306      next
   3.307        case (add g f)
   3.308 @@ -1346,7 +1346,7 @@
   3.309          by (auto intro!: integrable_bound[OF add(8)])
   3.310        with add show ?case
   3.311          unfolding plus_ereal.simps(1)[symmetric]
   3.312 -        by (subst positive_integral_add) auto
   3.313 +        by (subst nn_integral_add) auto
   3.314      next
   3.315        case (seq s)
   3.316        { fix i x assume "x \<in> space M" with seq(4) have "s i x \<le> f x"
   3.317 @@ -1366,7 +1366,7 @@
   3.318            using seq f s_le_f by (intro integrable_bound[OF f(3)]) auto
   3.319          have "(\<lambda>i. \<integral>\<^sup>+ x. s i x \<partial>M) ----> \<integral>\<^sup>+ x. f x \<partial>M"
   3.320            using seq s_le_f f
   3.321 -          by (intro positive_integral_dominated_convergence[where w=f])
   3.322 +          by (intro nn_integral_dominated_convergence[where w=f])
   3.323               (auto simp: integrable_iff_bounded)
   3.324          also have "(\<lambda>i. \<integral>\<^sup>+x. s i x \<partial>M) = (\<lambda>i. \<integral>x. s i x \<partial>M)"
   3.325            using seq int_s by simp
   3.326 @@ -1379,19 +1379,19 @@
   3.327    also have "\<dots> = integral\<^sup>L M f"
   3.328      using assms by (auto intro!: integral_cong_AE)
   3.329    also have "(\<integral>\<^sup>+ x. max 0 (f x) \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M)"
   3.330 -    using assms by (auto intro!: positive_integral_cong_AE simp: max_def)
   3.331 +    using assms by (auto intro!: nn_integral_cong_AE simp: max_def)
   3.332    finally show ?thesis .
   3.333  qed
   3.334  
   3.335  lemma integral_norm_bound:
   3.336    fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   3.337    shows "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
   3.338 -  using positive_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
   3.339 +  using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
   3.340    using integral_norm_bound_ereal[of M f] by simp
   3.341    
   3.342 -lemma integral_eq_positive_integral:
   3.343 +lemma integral_eq_nn_integral:
   3.344    "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)"
   3.345 -  by (subst positive_integral_eq_integral) auto
   3.346 +  by (subst nn_integral_eq_integral) auto
   3.347    
   3.348  lemma integrableI_simple_bochner_integrable:
   3.349    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   3.350 @@ -1445,9 +1445,9 @@
   3.351      fix i
   3.352  
   3.353      have "(\<integral>\<^sup>+x. norm (s' i x) \<partial>M) \<le> (\<integral>\<^sup>+x. 2 * ereal (norm (f x)) \<partial>M)"
   3.354 -      using s by (intro positive_integral_mono) (auto simp: s'_eq_s)
   3.355 +      using s by (intro nn_integral_mono) (auto simp: s'_eq_s)
   3.356      also have "\<dots> < \<infinity>"
   3.357 -      using f by (subst positive_integral_cmult) auto
   3.358 +      using f by (subst nn_integral_cmult) auto
   3.359      finally have sbi: "simple_bochner_integrable M (s' i)"
   3.360        using sf by (intro simple_bochner_integrableI_bounded) auto
   3.361      then show "integrable M (s' i)"
   3.362 @@ -1475,8 +1475,8 @@
   3.363    shows "0 \<le> integral\<^sup>L M f"
   3.364  proof -
   3.365    have "0 \<le> ereal (integral\<^sup>L M (\<lambda>x. max 0 (f x)))"
   3.366 -    by (subst integral_eq_positive_integral)
   3.367 -       (auto intro: real_of_ereal_pos positive_integral_positive integrable_max assms)
   3.368 +    by (subst integral_eq_nn_integral)
   3.369 +       (auto intro: real_of_ereal_pos nn_integral_nonneg integrable_max assms)
   3.370    also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = integral\<^sup>L M f"
   3.371      using assms(2) by (intro integral_cong_AE assms integrable_max) auto
   3.372    finally show ?thesis
   3.373 @@ -1493,10 +1493,10 @@
   3.374    shows "integral\<^sup>L M f = 0 \<longleftrightarrow> (AE x in M. f x = 0)"
   3.375  proof
   3.376    assume "integral\<^sup>L M f = 0"
   3.377 -  then have "integral\<^sup>P M f = 0"
   3.378 -    using positive_integral_eq_integral[OF f nonneg] by simp
   3.379 +  then have "integral\<^sup>N M f = 0"
   3.380 +    using nn_integral_eq_integral[OF f nonneg] by simp
   3.381    then have "AE x in M. ereal (f x) \<le> 0"
   3.382 -    by (simp add: positive_integral_0_iff_AE)
   3.383 +    by (simp add: nn_integral_0_iff_AE)
   3.384    with nonneg show "AE x in M. f x = 0"
   3.385      by auto
   3.386  qed (auto simp add: integral_eq_zero_AE)
   3.387 @@ -1527,8 +1527,8 @@
   3.388      and nn: "AE x in M. 0 \<le> g x"
   3.389    shows "integrable (density M g) f \<longleftrightarrow> integrable M (\<lambda>x. g x *\<^sub>R f x)"
   3.390    unfolding integrable_iff_bounded using nn
   3.391 -  apply (simp add: positive_integral_density )
   3.392 -  apply (intro arg_cong2[where f="op ="] refl positive_integral_cong_AE)
   3.393 +  apply (simp add: nn_integral_density )
   3.394 +  apply (intro arg_cong2[where f="op ="] refl nn_integral_cong_AE)
   3.395    apply auto
   3.396    done
   3.397  
   3.398 @@ -1547,9 +1547,9 @@
   3.399      have int: "integrable M (\<lambda>x. g x * indicator A x)"
   3.400        using g base integrable_density[of "indicator A :: 'a \<Rightarrow> real" M g] by simp
   3.401      then have "integral\<^sup>L M (\<lambda>x. g x * indicator A x) = (\<integral>\<^sup>+ x. ereal (g x * indicator A x) \<partial>M)"
   3.402 -      using g by (subst positive_integral_eq_integral) auto
   3.403 +      using g by (subst nn_integral_eq_integral) auto
   3.404      also have "\<dots> = (\<integral>\<^sup>+ x. ereal (g x) * indicator A x \<partial>M)"
   3.405 -      by (intro positive_integral_cong) (auto split: split_indicator)
   3.406 +      by (intro nn_integral_cong) (auto split: split_indicator)
   3.407      also have "\<dots> = emeasure (density M g) A"
   3.408        by (rule emeasure_density[symmetric]) auto
   3.409      also have "\<dots> = ereal (measure (density M g) A)"
   3.410 @@ -1607,7 +1607,7 @@
   3.411    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   3.412    assumes [measurable]: "g \<in> measurable M N" "f \<in> borel_measurable N"
   3.413    shows "integrable (distr M N g) f \<longleftrightarrow> integrable M (\<lambda>x. f (g x))"
   3.414 -  unfolding integrable_iff_bounded by (simp_all add: positive_integral_distr)
   3.415 +  unfolding integrable_iff_bounded by (simp_all add: nn_integral_distr)
   3.416  
   3.417  lemma integrable_distr:
   3.418    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   3.419 @@ -1678,7 +1678,7 @@
   3.420  lemma integrable_count_space:
   3.421    fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
   3.422    shows "finite X \<Longrightarrow> integrable (count_space X) f"
   3.423 -  by (auto simp: positive_integral_count_space integrable_iff_bounded)
   3.424 +  by (auto simp: nn_integral_count_space integrable_iff_bounded)
   3.425  
   3.426  lemma measure_count_space[simp]:
   3.427    "B \<subseteq> A \<Longrightarrow> finite B \<Longrightarrow> measure (count_space A) B = card B"
   3.428 @@ -1731,15 +1731,15 @@
   3.429    also have "\<dots> = integral\<^sup>L M (\<lambda>x. max 0 (f x)) - integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
   3.430      by (intro integral_diff integrable_max integrable_minus integrable_zero f)
   3.431    also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = real (\<integral>\<^sup>+x. max 0 (f x) \<partial>M)"
   3.432 -    by (subst integral_eq_positive_integral[symmetric]) (auto intro!: integrable_max f)
   3.433 +    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: integrable_max f)
   3.434    also have "integral\<^sup>L M (\<lambda>x. max 0 (- f x)) = real (\<integral>\<^sup>+x. max 0 (- f x) \<partial>M)"
   3.435 -    by (subst integral_eq_positive_integral[symmetric]) (auto intro!: integrable_max f)
   3.436 +    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: integrable_max f)
   3.437    also have "(\<lambda>x. ereal (max 0 (f x))) = (\<lambda>x. max 0 (ereal (f x)))"
   3.438      by (auto simp: max_def)
   3.439    also have "(\<lambda>x. ereal (max 0 (- f x))) = (\<lambda>x. max 0 (- ereal (f x)))"
   3.440      by (auto simp: max_def)
   3.441    finally show ?thesis
   3.442 -    unfolding positive_integral_max_0 .
   3.443 +    unfolding nn_integral_max_0 .
   3.444  qed
   3.445  
   3.446  lemma real_integrable_def:
   3.447 @@ -1749,12 +1749,12 @@
   3.448  proof (safe del: notI)
   3.449    assume *: "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
   3.450    have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
   3.451 -    by (intro positive_integral_mono) auto
   3.452 +    by (intro nn_integral_mono) auto
   3.453    also note *
   3.454    finally show "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>"
   3.455      by simp
   3.456    have "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
   3.457 -    by (intro positive_integral_mono) auto
   3.458 +    by (intro nn_integral_mono) auto
   3.459    also note *
   3.460    finally show "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
   3.461      by simp
   3.462 @@ -1762,11 +1762,11 @@
   3.463    assume [measurable]: "f \<in> borel_measurable M"
   3.464    assume fin: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
   3.465    have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. max 0 (ereal (f x)) + max 0 (ereal (- f x)) \<partial>M)"
   3.466 -    by (intro positive_integral_cong) (auto simp: max_def)
   3.467 +    by (intro nn_integral_cong) (auto simp: max_def)
   3.468    also have"\<dots> = (\<integral>\<^sup>+ x. max 0 (ereal (f x)) \<partial>M) + (\<integral>\<^sup>+ x. max 0 (ereal (- f x)) \<partial>M)"
   3.469 -    by (intro positive_integral_add) auto
   3.470 +    by (intro nn_integral_add) auto
   3.471    also have "\<dots> < \<infinity>"
   3.472 -    using fin by (auto simp: positive_integral_max_0)
   3.473 +    using fin by (auto simp: nn_integral_max_0)
   3.474    finally show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity>" .
   3.475  qed
   3.476  
   3.477 @@ -1782,8 +1782,8 @@
   3.478      "(\<integral>\<^sup>+x. ereal (-f x)\<partial>M) = ereal q"
   3.479      "f \<in> borel_measurable M" "integral\<^sup>L M f = r - q"
   3.480    using assms unfolding real_integrable_def real_lebesgue_integral_def[OF assms]
   3.481 -  using positive_integral_positive[of M "\<lambda>x. ereal (f x)"]
   3.482 -  using positive_integral_positive[of M "\<lambda>x. ereal (-f x)"]
   3.483 +  using nn_integral_nonneg[of M "\<lambda>x. ereal (f x)"]
   3.484 +  using nn_integral_nonneg[of M "\<lambda>x. ereal (-f x)"]
   3.485    by (cases rule: ereal2_cases[of "(\<integral>\<^sup>+x. ereal (-f x)\<partial>M)" "(\<integral>\<^sup>+x. ereal (f x)\<partial>M)"]) auto
   3.486  
   3.487  lemma integral_monotone_convergence_nonneg:
   3.488 @@ -1797,7 +1797,7 @@
   3.489    and "integral\<^sup>L M u = x"
   3.490  proof -
   3.491    have "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = (SUP n. (\<integral>\<^sup>+ x. ereal (f n x) \<partial>M))"
   3.492 -  proof (subst positive_integral_monotone_convergence_SUP_AE[symmetric])
   3.493 +  proof (subst nn_integral_monotone_convergence_SUP_AE[symmetric])
   3.494      fix i
   3.495      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)"
   3.496        by eventually_elim (auto simp: mono_def)
   3.497 @@ -1805,16 +1805,16 @@
   3.498        using i by auto
   3.499    next
   3.500      show "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = \<integral>\<^sup>+ x. (SUP i. ereal (f i x)) \<partial>M"
   3.501 -      apply (rule positive_integral_cong_AE)
   3.502 +      apply (rule nn_integral_cong_AE)
   3.503        using lim mono
   3.504        by eventually_elim (simp add: SUP_eq_LIMSEQ[THEN iffD2])
   3.505    qed
   3.506    also have "\<dots> = ereal x"
   3.507 -    using mono i unfolding positive_integral_eq_integral[OF i pos]
   3.508 +    using mono i unfolding nn_integral_eq_integral[OF i pos]
   3.509      by (subst SUP_eq_LIMSEQ) (auto simp: mono_def intro!: integral_mono_AE ilim)
   3.510    finally have "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = ereal x" .
   3.511    moreover have "(\<integral>\<^sup>+ x. ereal (- u x) \<partial>M) = 0"
   3.512 -  proof (subst positive_integral_0_iff_AE)
   3.513 +  proof (subst nn_integral_0_iff_AE)
   3.514      show "(\<lambda>x. ereal (- u x)) \<in> borel_measurable M"
   3.515        using u by auto
   3.516      from mono pos[of 0] lim show "AE x in M. ereal (- u x) \<le> 0"
   3.517 @@ -1865,11 +1865,11 @@
   3.518    shows "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
   3.519  proof -
   3.520    have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>x. norm (f x) \<partial>M)"
   3.521 -    using f by (intro positive_integral_eq_integral integrable_norm) auto
   3.522 +    using f by (intro nn_integral_eq_integral integrable_norm) auto
   3.523    then have "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) = 0"
   3.524      by simp
   3.525    also have "\<dots> \<longleftrightarrow> emeasure M {x\<in>space M. ereal (norm (f x)) \<noteq> 0} = 0"
   3.526 -    by (intro positive_integral_0_iff) auto
   3.527 +    by (intro nn_integral_0_iff) auto
   3.528    finally show ?thesis
   3.529      by simp
   3.530  qed
   3.531 @@ -1917,7 +1917,7 @@
   3.532        using int by (simp add: integral_0_iff)
   3.533      moreover
   3.534      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)"
   3.535 -      using A by (intro positive_integral_mono_AE) auto
   3.536 +      using A by (intro nn_integral_mono_AE) auto
   3.537      then have "(emeasure M) A \<le> (emeasure M) {x \<in> space M. Y x - X x \<noteq> 0}"
   3.538        using int A by (simp add: integrable_def)
   3.539      ultimately have "emeasure M A = 0"
   3.540 @@ -2221,7 +2221,7 @@
   3.541              by (intro simple_function_borel_measurable)
   3.542                 (auto simp: space_pair_measure dest: finite_subset)
   3.543            have "(\<integral>\<^sup>+ y. ereal (norm (s i (x, y))) \<partial>M) \<le> (\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M)"
   3.544 -            using x s by (intro positive_integral_mono) auto
   3.545 +            using x s by (intro nn_integral_mono) auto
   3.546            also have "(\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M) < \<infinity>"
   3.547              using int_2f by (simp add: integrable_iff_bounded)
   3.548            finally show "(\<integral>\<^sup>+ xa. ereal (norm (s i (x, xa))) \<partial>M) < \<infinity>" .
   3.549 @@ -2276,7 +2276,7 @@
   3.550    have "(\<integral>\<^sup>+ x. emeasure M2 (Pair x -` A) \<partial>M1) \<noteq> \<infinity>"
   3.551      by simp
   3.552    then have "AE x in M1. emeasure M2 (Pair x -` A) \<noteq> \<infinity>"
   3.553 -    by (rule positive_integral_PInf_AE[rotated]) (intro M2.measurable_emeasure_Pair A)
   3.554 +    by (rule nn_integral_PInf_AE[rotated]) (intro M2.measurable_emeasure_Pair A)
   3.555    moreover have "\<And>x. x \<in> space M1 \<Longrightarrow> Pair x -` A = {y\<in>space M2. (x, y) \<in> A}"
   3.556      using sets.sets_into_space[OF A] by (auto simp: space_pair_measure)
   3.557    ultimately show ?thesis by auto
   3.558 @@ -2288,11 +2288,11 @@
   3.559    shows "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
   3.560  proof -
   3.561    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))"
   3.562 -    by (rule M2.positive_integral_fst) simp
   3.563 +    by (rule M2.nn_integral_fst) simp
   3.564    also have "(\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2)) \<noteq> \<infinity>"
   3.565      using f unfolding integrable_iff_bounded by simp
   3.566    finally have "AE x in M1. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<noteq> \<infinity>"
   3.567 -    by (intro positive_integral_PInf_AE M2.borel_measurable_positive_integral )
   3.568 +    by (intro nn_integral_PInf_AE M2.borel_measurable_nn_integral )
   3.569         (auto simp: measurable_split_conv)
   3.570    with AE_space show ?thesis
   3.571      by eventually_elim
   3.572 @@ -2308,9 +2308,9 @@
   3.573    show "(\<lambda>x. \<integral> y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
   3.574      by (rule M2.borel_measurable_lebesgue_integral) simp
   3.575    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)"
   3.576 -    using AE_integrable_fst'[OF f] by (auto intro!: positive_integral_mono_AE integral_norm_bound_ereal)
   3.577 +    using AE_integrable_fst'[OF f] by (auto intro!: nn_integral_mono_AE integral_norm_bound_ereal)
   3.578    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))"
   3.579 -    by (rule M2.positive_integral_fst) simp
   3.580 +    by (rule M2.nn_integral_fst) simp
   3.581    also have "(\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2)) < \<infinity>"
   3.582      using f unfolding integrable_iff_bounded by simp
   3.583    finally show "(\<integral>\<^sup>+ x. ereal (norm (\<integral> y. f (x, y) \<partial>M2)) \<partial>M1) < \<infinity>" .
   3.584 @@ -2341,18 +2341,18 @@
   3.585      have "(\<integral>\<^sup>+x. ereal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1) =
   3.586        (\<integral>\<^sup>+x. emeasure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1)"
   3.587        using emeasure_pair_measure_finite[OF base]
   3.588 -      by (intro positive_integral_cong_AE, eventually_elim) (simp add: emeasure_eq_ereal_measure)
   3.589 +      by (intro nn_integral_cong_AE, eventually_elim) (simp add: emeasure_eq_ereal_measure)
   3.590      also have "\<dots> = emeasure (M1 \<Otimes>\<^sub>M M2) A"
   3.591        using sets.sets_into_space[OF A]
   3.592        by (subst M2.emeasure_pair_measure_alt)
   3.593 -         (auto intro!: positive_integral_cong arg_cong[where f="emeasure M2"] simp: space_pair_measure)
   3.594 +         (auto intro!: nn_integral_cong arg_cong[where f="emeasure M2"] simp: space_pair_measure)
   3.595      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" .
   3.596  
   3.597      from base * show "integrable M1 (\<lambda>x. measure M2 {y \<in> space M2. (x, y) \<in> A})"
   3.598        by (simp add: measure_nonneg integrable_iff_bounded)
   3.599      then have "(\<integral>x. measure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1) = 
   3.600        (\<integral>\<^sup>+x. ereal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1)"
   3.601 -      by (rule positive_integral_eq_integral[symmetric]) (simp add: measure_nonneg)
   3.602 +      by (rule nn_integral_eq_integral[symmetric]) (simp add: measure_nonneg)
   3.603      also note *
   3.604      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"
   3.605        using base by (simp add: emeasure_eq_ereal_measure)
   3.606 @@ -2417,9 +2417,9 @@
   3.607          from s have "norm (\<integral> y. s i (x, y) \<partial>M2) \<le> (\<integral>\<^sup>+y. norm (s i (x, y)) \<partial>M2)"
   3.608            by (rule integral_norm_bound_ereal)
   3.609          also have "\<dots> \<le> (\<integral>\<^sup>+y. 2 * norm (f (x, y)) \<partial>M2)"
   3.610 -          using x lim by (auto intro!: positive_integral_mono simp: space_pair_measure)
   3.611 +          using x lim by (auto intro!: nn_integral_mono simp: space_pair_measure)
   3.612          also have "\<dots> = (\<integral>y. 2 * norm (f (x, y)) \<partial>M2)"
   3.613 -          using f by (intro positive_integral_eq_integral) auto
   3.614 +          using f by (intro nn_integral_eq_integral) auto
   3.615          finally show "norm (\<integral> y. s i (x, y) \<partial>M2) \<le> (\<integral> y. 2 * norm (f (x, y)) \<partial>M2)"
   3.616            by simp
   3.617        qed
   3.618 @@ -2530,9 +2530,9 @@
   3.619        (\<integral>\<^sup>+ x. (\<Prod>i\<in>I. ereal (norm (f i (x i)))) \<partial>Pi\<^sub>M I M)"
   3.620      by (simp add: setprod_norm setprod_ereal)
   3.621    also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+ x. ereal (norm (f i x)) \<partial>M i)"
   3.622 -    using assms by (intro product_positive_integral_setprod) auto
   3.623 +    using assms by (intro product_nn_integral_setprod) auto
   3.624    also have "\<dots> < \<infinity>"
   3.625 -    using integrable by (simp add: setprod_PInf positive_integral_positive integrable_iff_bounded)
   3.626 +    using integrable by (simp add: setprod_PInf nn_integral_nonneg integrable_iff_bounded)
   3.627    finally show "(\<integral>\<^sup>+ x. ereal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) < \<infinity>" .
   3.628  qed
   3.629  
   3.630 @@ -2568,7 +2568,7 @@
   3.631    have "f \<in> borel_measurable M"
   3.632      using assms by (auto simp: measurable_def)
   3.633    with assms show ?thesis
   3.634 -    using assms by (auto simp: integrable_iff_bounded positive_integral_subalgebra)
   3.635 +    using assms by (auto simp: integrable_iff_bounded nn_integral_subalgebra)
   3.636  qed
   3.637  
   3.638  lemma integral_subalgebra:
     4.1 --- a/src/HOL/Probability/Distributions.thy	Mon May 19 13:53:58 2014 +0200
     4.2 +++ b/src/HOL/Probability/Distributions.thy	Mon May 19 14:26:58 2014 +0200
     4.3 @@ -56,9 +56,9 @@
     4.4  
     4.5    have "emeasure ?D (space ?D) = (\<integral>\<^sup>+ x. ereal (?f x) * indicator {0..} x \<partial>lborel)"
     4.6      by (auto simp: emeasure_density exponential_density_def
     4.7 -             intro!: positive_integral_cong split: split_indicator)
     4.8 +             intro!: nn_integral_cong split: split_indicator)
     4.9    also have "\<dots> = ereal (0 - ?F 0)"
    4.10 -  proof (rule positive_integral_FTC_atLeast)
    4.11 +  proof (rule nn_integral_FTC_atLeast)
    4.12      have "((\<lambda>x. exp (l * x)) ---> 0) at_bot"
    4.13        by (rule filterlim_compose[OF exp_at_bot filterlim_tendsto_pos_mult_at_bot[of _ l]])
    4.14           (simp_all add: tendsto_const filterlim_ident)
    4.15 @@ -72,10 +72,10 @@
    4.16  
    4.17    assume "0 \<le> a"
    4.18    have "emeasure ?D {..a} = (\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel)"
    4.19 -    by (auto simp add: emeasure_density intro!: positive_integral_cong split: split_indicator)
    4.20 +    by (auto simp add: emeasure_density intro!: nn_integral_cong split: split_indicator)
    4.21         (auto simp: exponential_density_def)
    4.22    also have "(\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel) = ereal (?F a) - ereal (?F 0)"
    4.23 -    using `0 \<le> a` deriv by (intro positive_integral_FTC_atLeastAtMost) auto
    4.24 +    using `0 \<le> a` deriv by (intro nn_integral_FTC_atLeastAtMost) auto
    4.25    also have "\<dots> = 1 - exp (- a * l)"
    4.26      by simp
    4.27    finally show "emeasure ?D {.. a} = 1 - exp (- a * l)" .
    4.28 @@ -241,9 +241,9 @@
    4.29       by simp
    4.30    also have "\<dots> = (\<integral>\<^sup>+ x. (1 / emeasure M' A) * indicator (A \<inter> B) x \<partial>M')"
    4.31      using A B
    4.32 -    by (intro positive_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal)
    4.33 +    by (intro nn_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal)
    4.34    also have "\<dots> = (\<integral>\<^sup>+ x. ?f x * indicator B x \<partial>M')"
    4.35 -    by (rule positive_integral_cong) (auto split: split_indicator)
    4.36 +    by (rule nn_integral_cong) (auto split: split_indicator)
    4.37    finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B"
    4.38      using A B X by (auto simp add: emeasure_distr emeasure_density)
    4.39  qed simp
    4.40 @@ -271,10 +271,10 @@
    4.41   
    4.42    have "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) =
    4.43      (\<integral>\<^sup>+ x. ereal (1 / measure lborel A) * indicator (A \<inter> {..a}) x \<partial>lborel)"
    4.44 -    by (auto intro!: positive_integral_cong split: split_indicator)
    4.45 +    by (auto intro!: nn_integral_cong split: split_indicator)
    4.46    also have "\<dots> = ereal (1 / measure lborel A) * emeasure lborel (A \<inter> {..a})"
    4.47      using `A \<in> sets borel`
    4.48 -    by (intro positive_integral_cmult_indicator) (auto simp: measure_nonneg)
    4.49 +    by (intro nn_integral_cmult_indicator) (auto simp: measure_nonneg)
    4.50    also have "\<dots> = ereal (measure lborel (A \<inter> {..a}) / r)"
    4.51      unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def)
    4.52    finally show "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) =
    4.53 @@ -331,10 +331,10 @@
    4.54      using distributed_borel_measurable[OF D] `a \<le> t` `t \<le> b`
    4.55      unfolding distributed_distr_eq_density[OF D]
    4.56      by (subst emeasure_density)
    4.57 -       (auto intro!: positive_integral_cong simp: measure_def split: split_indicator)
    4.58 +       (auto intro!: nn_integral_cong simp: measure_def split: split_indicator)
    4.59    also have "\<dots> = ereal (1 / (b - a)) * (t - a)"
    4.60      using `a \<le> t` `t \<le> b`
    4.61 -    by (subst positive_integral_cmult_indicator) auto
    4.62 +    by (subst nn_integral_cmult_indicator) auto
    4.63    finally show ?thesis
    4.64      by (simp add: measure_def)
    4.65  qed
     5.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Mon May 19 13:53:58 2014 +0200
     5.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Mon May 19 14:26:58 2014 +0200
     5.3 @@ -688,15 +688,15 @@
     5.4    "(\<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))"
     5.5    using emeasure_PiM[OF finite_index] by auto
     5.6  
     5.7 -lemma (in product_sigma_finite) positive_integral_empty:
     5.8 +lemma (in product_sigma_finite) nn_integral_empty:
     5.9    assumes pos: "0 \<le> f (\<lambda>k. undefined)"
    5.10 -  shows "integral\<^sup>P (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
    5.11 +  shows "integral\<^sup>N (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
    5.12  proof -
    5.13    interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI)
    5.14    have "\<And>A. emeasure (Pi\<^sub>M {} M) (Pi\<^sub>E {} A) = 1"
    5.15      using assms by (subst measure_times) auto
    5.16    then show ?thesis
    5.17 -    unfolding positive_integral_def simple_function_def simple_integral_def[abs_def]
    5.18 +    unfolding nn_integral_def simple_function_def simple_integral_def[abs_def]
    5.19    proof (simp add: space_PiM_empty sets_PiM_empty, intro antisym)
    5.20      show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
    5.21        by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
    5.22 @@ -768,10 +768,10 @@
    5.23    qed
    5.24  qed
    5.25  
    5.26 -lemma (in product_sigma_finite) product_positive_integral_fold:
    5.27 +lemma (in product_sigma_finite) product_nn_integral_fold:
    5.28    assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
    5.29    and f: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
    5.30 -  shows "integral\<^sup>P (Pi\<^sub>M (I \<union> J) M) f =
    5.31 +  shows "integral\<^sup>N (Pi\<^sub>M (I \<union> J) M) f =
    5.32      (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^sub>M J M)) \<partial>(Pi\<^sub>M I M))"
    5.33  proof -
    5.34    interpret I: finite_product_sigma_finite M I by default fact
    5.35 @@ -781,8 +781,8 @@
    5.36      using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
    5.37    show ?thesis
    5.38      apply (subst distr_merge[OF IJ, symmetric])
    5.39 -    apply (subst positive_integral_distr[OF measurable_merge f])
    5.40 -    apply (subst J.positive_integral_fst[symmetric, OF P_borel])
    5.41 +    apply (subst nn_integral_distr[OF measurable_merge f])
    5.42 +    apply (subst J.nn_integral_fst[symmetric, OF P_borel])
    5.43      apply simp
    5.44      done
    5.45  qed
    5.46 @@ -799,30 +799,30 @@
    5.47      by (simp add: emeasure_distr measurable_component_singleton)
    5.48  qed simp
    5.49  
    5.50 -lemma (in product_sigma_finite) product_positive_integral_singleton:
    5.51 +lemma (in product_sigma_finite) product_nn_integral_singleton:
    5.52    assumes f: "f \<in> borel_measurable (M i)"
    5.53 -  shows "integral\<^sup>P (Pi\<^sub>M {i} M) (\<lambda>x. f (x i)) = integral\<^sup>P (M i) f"
    5.54 +  shows "integral\<^sup>N (Pi\<^sub>M {i} M) (\<lambda>x. f (x i)) = integral\<^sup>N (M i) f"
    5.55  proof -
    5.56    interpret I: finite_product_sigma_finite M "{i}" by default simp
    5.57    from f show ?thesis
    5.58      apply (subst distr_singleton[symmetric])
    5.59 -    apply (subst positive_integral_distr[OF measurable_component_singleton])
    5.60 +    apply (subst nn_integral_distr[OF measurable_component_singleton])
    5.61      apply simp_all
    5.62      done
    5.63  qed
    5.64  
    5.65 -lemma (in product_sigma_finite) product_positive_integral_insert:
    5.66 +lemma (in product_sigma_finite) product_nn_integral_insert:
    5.67    assumes I[simp]: "finite I" "i \<notin> I"
    5.68      and f: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
    5.69 -  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))"
    5.70 +  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))"
    5.71  proof -
    5.72    interpret I: finite_product_sigma_finite M I by default auto
    5.73    interpret i: finite_product_sigma_finite M "{i}" by default auto
    5.74    have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
    5.75      using f by auto
    5.76    show ?thesis
    5.77 -    unfolding product_positive_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f]
    5.78 -  proof (rule positive_integral_cong, subst product_positive_integral_singleton[symmetric])
    5.79 +    unfolding product_nn_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f]
    5.80 +  proof (rule nn_integral_cong, subst product_nn_integral_singleton[symmetric])
    5.81      fix x assume x: "x \<in> space (Pi\<^sub>M I M)"
    5.82      let ?f = "\<lambda>y. f (x(i := y))"
    5.83      show "?f \<in> borel_measurable (M i)"
    5.84 @@ -830,16 +830,16 @@
    5.85        unfolding comp_def .
    5.86      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)"
    5.87        using x
    5.88 -      by (auto intro!: positive_integral_cong arg_cong[where f=f]
    5.89 +      by (auto intro!: nn_integral_cong arg_cong[where f=f]
    5.90                 simp add: space_PiM extensional_def PiE_def)
    5.91    qed
    5.92  qed
    5.93  
    5.94 -lemma (in product_sigma_finite) product_positive_integral_setprod:
    5.95 +lemma (in product_sigma_finite) product_nn_integral_setprod:
    5.96    fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> ereal"
    5.97    assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
    5.98    and pos: "\<And>i x. i \<in> I \<Longrightarrow> 0 \<le> f i x"
    5.99 -  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))"
   5.100 +  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))"
   5.101  using assms proof induct
   5.102    case (insert i I)
   5.103    note `finite I`[intro, simp]
   5.104 @@ -852,10 +852,10 @@
   5.105                measurable_comp[OF measurable_component_singleton, unfolded comp_def])
   5.106         auto
   5.107    then show ?case
   5.108 -    apply (simp add: product_positive_integral_insert[OF insert(1,2) prod])
   5.109 -    apply (simp add: insert(2-) * pos borel setprod_ereal_pos positive_integral_multc)
   5.110 -    apply (subst positive_integral_cmult)
   5.111 -    apply (auto simp add: pos borel insert(2-) setprod_ereal_pos positive_integral_positive)
   5.112 +    apply (simp add: product_nn_integral_insert[OF insert(1,2) prod])
   5.113 +    apply (simp add: insert(2-) * pos borel setprod_ereal_pos nn_integral_multc)
   5.114 +    apply (subst nn_integral_cmult)
   5.115 +    apply (auto simp add: pos borel insert(2-) setprod_ereal_pos nn_integral_nonneg)
   5.116      done
   5.117  qed (simp add: space_PiM)
   5.118  
   5.119 @@ -871,9 +871,9 @@
   5.120    then have "emeasure ?P A = (\<integral>\<^sup>+x. indicator A x \<partial>?P)" 
   5.121      by simp
   5.122    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)" 
   5.123 -    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def PiE_def eq)
   5.124 +    by (intro nn_integral_cong) (auto simp: space_PiM indicator_def PiE_def eq)
   5.125    also have "\<dots> = emeasure ?D A"
   5.126 -    using A by (simp add: product_positive_integral_singleton emeasure_distr)
   5.127 +    using A by (simp add: product_nn_integral_singleton emeasure_distr)
   5.128    finally show "emeasure (Pi\<^sub>M {i} M) A = emeasure ?D A" .
   5.129  qed simp
   5.130  
   5.131 @@ -894,7 +894,7 @@
   5.132      apply (subst distr_merge[symmetric, OF IJ])
   5.133      apply (subst emeasure_distr[OF measurable_merge A])
   5.134      apply (subst J.emeasure_pair_measure_alt[OF merge])
   5.135 -    apply (auto intro!: positive_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
   5.136 +    apply (auto intro!: nn_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
   5.137      done
   5.138  
   5.139    show ?B
     6.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Mon May 19 13:53:58 2014 +0200
     6.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Mon May 19 14:26:58 2014 +0200
     6.3 @@ -59,7 +59,7 @@
     6.4        using K J by (subst emeasure_fold_integral) auto
     6.5      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)"
     6.6        (is "_ = (\<integral>\<^sup>+x. \<mu>G (?MZ x) \<partial>Pi\<^sub>M J M)")
     6.7 -    proof (intro positive_integral_cong)
     6.8 +    proof (intro nn_integral_cong)
     6.9        fix x assume x: "x \<in> space (Pi\<^sub>M J M)"
    6.10        with K merge_in_G(2)[OF this]
    6.11        show "emeasure (Pi\<^sub>M (K - J) M) (?M x) = \<mu>G (?MZ x)"
    6.12 @@ -141,7 +141,7 @@
    6.13            have "?a / 2^k \<le> \<mu>G (Z n)" using Z by auto
    6.14            also have "\<dots> \<le> (\<integral>\<^sup>+ x. indicator (?Q n) x + ?a / 2^(k+1) \<partial>Pi\<^sub>M J' M)"
    6.15              unfolding fold(2)[OF J' `Z n \<in> ?G`]
    6.16 -          proof (intro positive_integral_mono)
    6.17 +          proof (intro nn_integral_mono)
    6.18              fix x assume x: "x \<in> space (Pi\<^sub>M J' M)"
    6.19              then have "?q n x \<le> 1 + 0"
    6.20                using J' Z fold(3) Z_sets by auto
    6.21 @@ -153,7 +153,7 @@
    6.22            qed
    6.23            also have "\<dots> = emeasure (Pi\<^sub>M J' M) (?Q n) + ?a / 2^(k+1)"
    6.24              using `0 \<le> ?a` Q_sets J'.emeasure_space_1
    6.25 -            by (subst positive_integral_add) auto
    6.26 +            by (subst nn_integral_add) auto
    6.27            finally show "?a / 2^(k+1) \<le> emeasure (Pi\<^sub>M J' M) (?Q n)" using `?a \<le> 1`
    6.28              by (cases rule: ereal2_cases[of ?a "emeasure (Pi\<^sub>M J' M) (?Q n)"])
    6.29                 (auto simp: field_simps)
     7.1 --- a/src/HOL/Probability/Information.thy	Mon May 19 13:53:58 2014 +0200
     7.2 +++ b/src/HOL/Probability/Information.thy	Mon May 19 14:26:58 2014 +0200
     7.3 @@ -143,10 +143,10 @@
     7.4      using D by auto
     7.5  
     7.6    have D_neg: "(\<integral>\<^sup>+ x. ereal (- D x) \<partial>M) = 0"
     7.7 -    using D by (subst positive_integral_0_iff_AE) auto
     7.8 +    using D by (subst nn_integral_0_iff_AE) auto
     7.9  
    7.10    have "(\<integral>\<^sup>+ x. ereal (D x) \<partial>M) = emeasure (density M D) (space M)"
    7.11 -    using D by (simp add: emeasure_density cong: positive_integral_cong)
    7.12 +    using D by (simp add: emeasure_density cong: nn_integral_cong)
    7.13    then have D_pos: "(\<integral>\<^sup>+ x. ereal (D x) \<partial>M) = 1"
    7.14      using N.emeasure_space_1 by simp
    7.15  
    7.16 @@ -178,11 +178,11 @@
    7.17        have "emeasure M {x\<in>space M. D x = 1} = (\<integral>\<^sup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"
    7.18          using D(1) by auto
    7.19        also have "\<dots> = (\<integral>\<^sup>+ x. ereal (D x) \<partial>M)"
    7.20 -        using disj by (auto intro!: positive_integral_cong_AE simp: indicator_def one_ereal_def)
    7.21 +        using disj by (auto intro!: nn_integral_cong_AE simp: indicator_def one_ereal_def)
    7.22        finally have "AE x in M. D x = 1"
    7.23          using D D_pos by (intro AE_I_eq_1) auto
    7.24        then have "(\<integral>\<^sup>+x. indicator A x\<partial>M) = (\<integral>\<^sup>+x. ereal (D x) * indicator A x\<partial>M)"
    7.25 -        by (intro positive_integral_cong_AE) (auto simp: one_ereal_def[symmetric])
    7.26 +        by (intro nn_integral_cong_AE) (auto simp: one_ereal_def[symmetric])
    7.27        also have "\<dots> = density M D A"
    7.28          using `A \<in> sets M` D by (simp add: emeasure_density)
    7.29        finally show False using `A \<in> sets M` `emeasure (density M D) A \<noteq> emeasure M A` by simp
    7.30 @@ -844,9 +844,9 @@
    7.31    from X.emeasure_space_1 have "(\<integral>\<^sup>+x. Px x \<partial>MX) = 1"
    7.32      unfolding distributed_distr_eq_density[OF X] using Px
    7.33      by (subst (asm) emeasure_density)
    7.34 -       (auto simp: borel_measurable_ereal_iff intro!: integral_cong cong: positive_integral_cong)
    7.35 +       (auto simp: borel_measurable_ereal_iff intro!: integral_cong cong: nn_integral_cong)
    7.36    ultimately show False
    7.37 -    by (simp add: positive_integral_cong_AE)
    7.38 +    by (simp add: nn_integral_cong_AE)
    7.39  qed
    7.40  
    7.41  lemma (in information_space) entropy_le:
    7.42 @@ -876,11 +876,11 @@
    7.43      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"
    7.44        by (auto simp: one_ereal_def)
    7.45      have "(\<integral>\<^sup>+ x. max 0 (ereal (- (if Px x = 0 then 0 else 1))) \<partial>MX) = (\<integral>\<^sup>+ x. 0 \<partial>MX)"
    7.46 -      by (intro positive_integral_cong) (auto split: split_max)
    7.47 +      by (intro nn_integral_cong) (auto split: split_max)
    7.48      then show "integrable (distr M MX X) (\<lambda>x. 1 / Px x)"
    7.49        unfolding distributed_distr_eq_density[OF X] using Px
    7.50 -      by (auto simp: positive_integral_density real_integrable_def borel_measurable_ereal_iff fin positive_integral_max_0
    7.51 -              cong: positive_integral_cong)
    7.52 +      by (auto simp: nn_integral_density real_integrable_def borel_measurable_ereal_iff fin nn_integral_max_0
    7.53 +              cong: nn_integral_cong)
    7.54      have "integrable MX (\<lambda>x. Px x * log b (1 / Px x)) =
    7.55        integrable MX (\<lambda>x. - Px x * log b (Px x))"
    7.56        using Px
    7.57 @@ -1084,37 +1084,37 @@
    7.58      by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
    7.59  
    7.60    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))"
    7.61 -    apply (subst positive_integral_density)
    7.62 +    apply (subst nn_integral_density)
    7.63      apply simp
    7.64      apply (rule distributed_AE[OF Pxyz])
    7.65      apply auto []
    7.66 -    apply (rule positive_integral_mono_AE)
    7.67 +    apply (rule nn_integral_mono_AE)
    7.68      using ae5 ae6 ae7 ae8
    7.69      apply eventually_elim
    7.70      apply auto
    7.71      done
    7.72    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)"
    7.73 -    by (subst STP.positive_integral_snd[symmetric]) (auto simp add: split_beta')
    7.74 +    by (subst STP.nn_integral_snd[symmetric]) (auto simp add: split_beta')
    7.75    also have "\<dots> = (\<integral>\<^sup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^sub>M P)"
    7.76 -    apply (rule positive_integral_cong_AE)
    7.77 +    apply (rule nn_integral_cong_AE)
    7.78      using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
    7.79      apply eventually_elim
    7.80    proof (case_tac x, simp del: times_ereal.simps add: space_pair_measure)
    7.81      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"
    7.82        "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
    7.83      then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
    7.84 -      by (subst positive_integral_multc)
    7.85 +      by (subst nn_integral_multc)
    7.86           (auto split: prod.split)
    7.87    qed
    7.88    also have "\<dots> = 1"
    7.89      using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
    7.90 -    by (subst positive_integral_density[symmetric]) auto
    7.91 +    by (subst nn_integral_density[symmetric]) auto
    7.92    finally have le1: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> 1" .
    7.93    also have "\<dots> < \<infinity>" by simp
    7.94    finally have fin: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
    7.95  
    7.96    have pos: "(\<integral>\<^sup>+x. ?f x \<partial>?P) \<noteq> 0"
    7.97 -    apply (subst positive_integral_density)
    7.98 +    apply (subst nn_integral_density)
    7.99      apply simp
   7.100      apply (rule distributed_AE[OF Pxyz])
   7.101      apply auto []
   7.102 @@ -1123,18 +1123,18 @@
   7.103      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)))"
   7.104      assume "(\<integral>\<^sup>+x. ?g x \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)) = 0"
   7.105      then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. ?g x \<le> 0"
   7.106 -      by (intro positive_integral_0_iff_AE[THEN iffD1]) auto
   7.107 +      by (intro nn_integral_0_iff_AE[THEN iffD1]) auto
   7.108      then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pxyz x = 0"
   7.109        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   7.110        by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
   7.111      then have "(\<integral>\<^sup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) = 0"
   7.112 -      by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
   7.113 +      by (subst nn_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
   7.114      with P.emeasure_space_1 show False
   7.115 -      by (subst (asm) emeasure_density) (auto cong: positive_integral_cong)
   7.116 +      by (subst (asm) emeasure_density) (auto cong: nn_integral_cong)
   7.117    qed
   7.118  
   7.119    have neg: "(\<integral>\<^sup>+ x. - ?f x \<partial>?P) = 0"
   7.120 -    apply (rule positive_integral_0_iff_AE[THEN iffD2])
   7.121 +    apply (rule nn_integral_0_iff_AE[THEN iffD2])
   7.122      apply simp
   7.123      apply (subst AE_density)
   7.124      apply simp
   7.125 @@ -1160,14 +1160,14 @@
   7.126          by simp
   7.127      qed simp
   7.128      then have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) = (\<integral>x. ?f x \<partial>?P)"
   7.129 -      apply (rule positive_integral_eq_integral)
   7.130 +      apply (rule nn_integral_eq_integral)
   7.131        apply (subst AE_density)
   7.132        apply simp
   7.133        using ae5 ae6 ae7 ae8
   7.134        apply eventually_elim
   7.135        apply auto
   7.136        done
   7.137 -    with positive_integral_positive[of ?P ?f] pos le1
   7.138 +    with nn_integral_nonneg[of ?P ?f] pos le1
   7.139      show "0 < (\<integral>x. ?f x \<partial>?P)" "(\<integral>x. ?f x \<partial>?P) \<le> 1"
   7.140        by (simp_all add: one_ereal_def)
   7.141    qed
   7.142 @@ -1341,36 +1341,36 @@
   7.143      using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
   7.144      by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
   7.145    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))"
   7.146 -    apply (subst positive_integral_density)
   7.147 +    apply (subst nn_integral_density)
   7.148      apply (rule distributed_borel_measurable[OF Pxyz])
   7.149      apply (rule distributed_AE[OF Pxyz])
   7.150      apply simp
   7.151 -    apply (rule positive_integral_mono_AE)
   7.152 +    apply (rule nn_integral_mono_AE)
   7.153      using ae5 ae6 ae7 ae8
   7.154      apply eventually_elim
   7.155      apply auto
   7.156      done
   7.157    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)"
   7.158 -    by (subst STP.positive_integral_snd[symmetric]) (auto simp add: split_beta')
   7.159 +    by (subst STP.nn_integral_snd[symmetric]) (auto simp add: split_beta')
   7.160    also have "\<dots> = (\<integral>\<^sup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^sub>M P)"
   7.161 -    apply (rule positive_integral_cong_AE)
   7.162 +    apply (rule nn_integral_cong_AE)
   7.163      using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
   7.164      apply eventually_elim
   7.165    proof (case_tac x, simp del: times_ereal.simps add: space_pair_measure)
   7.166      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"
   7.167        "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
   7.168      then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
   7.169 -      by (subst positive_integral_multc) auto
   7.170 +      by (subst nn_integral_multc) auto
   7.171    qed
   7.172    also have "\<dots> = 1"
   7.173      using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
   7.174 -    by (subst positive_integral_density[symmetric]) auto
   7.175 +    by (subst nn_integral_density[symmetric]) auto
   7.176    finally have le1: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> 1" .
   7.177    also have "\<dots> < \<infinity>" by simp
   7.178    finally have fin: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
   7.179  
   7.180    have pos: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> 0"
   7.181 -    apply (subst positive_integral_density)
   7.182 +    apply (subst nn_integral_density)
   7.183      apply simp
   7.184      apply (rule distributed_AE[OF Pxyz])
   7.185      apply simp
   7.186 @@ -1379,18 +1379,18 @@
   7.187      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)))"
   7.188      assume "(\<integral>\<^sup>+ x. ?g x \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)) = 0"
   7.189      then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. ?g x \<le> 0"
   7.190 -      by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: borel_measurable_ereal measurable_If)
   7.191 +      by (intro nn_integral_0_iff_AE[THEN iffD1]) (auto intro!: borel_measurable_ereal measurable_If)
   7.192      then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pxyz x = 0"
   7.193        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   7.194        by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
   7.195      then have "(\<integral>\<^sup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) = 0"
   7.196 -      by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
   7.197 +      by (subst nn_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
   7.198      with P.emeasure_space_1 show False
   7.199 -      by (subst (asm) emeasure_density) (auto cong: positive_integral_cong)
   7.200 +      by (subst (asm) emeasure_density) (auto cong: nn_integral_cong)
   7.201    qed
   7.202  
   7.203    have neg: "(\<integral>\<^sup>+ x. - ?f x \<partial>?P) = 0"
   7.204 -    apply (rule positive_integral_0_iff_AE[THEN iffD2])
   7.205 +    apply (rule nn_integral_0_iff_AE[THEN iffD2])
   7.206      apply (auto simp: split_beta') []
   7.207      apply (subst AE_density)
   7.208      apply (auto simp: split_beta') []
   7.209 @@ -1416,14 +1416,14 @@
   7.210          by simp
   7.211      qed simp
   7.212      then have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) = (\<integral>x. ?f x \<partial>?P)"
   7.213 -      apply (rule positive_integral_eq_integral)
   7.214 +      apply (rule nn_integral_eq_integral)
   7.215        apply (subst AE_density)
   7.216        apply simp
   7.217        using ae5 ae6 ae7 ae8
   7.218        apply eventually_elim
   7.219        apply auto
   7.220        done
   7.221 -    with positive_integral_positive[of ?P ?f] pos le1
   7.222 +    with nn_integral_nonneg[of ?P ?f] pos le1
   7.223      show "0 < (\<integral>x. ?f x \<partial>?P)" "(\<integral>x. ?f x \<partial>?P) \<le> 1"
   7.224        by (simp_all add: one_ereal_def)
   7.225    qed
     8.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon May 19 13:53:58 2014 +0200
     8.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon May 19 14:26:58 2014 +0200
     8.3 @@ -544,7 +544,7 @@
     8.4        by (auto simp: field_simps)
     8.5      with `0 < c` show ?thesis
     8.6        by (cases "a \<le> b")
     8.7 -         (auto simp: field_simps emeasure_density positive_integral_distr positive_integral_cmult
     8.8 +         (auto simp: field_simps emeasure_density nn_integral_distr nn_integral_cmult
     8.9                       borel_measurable_indicator' emeasure_distr)
    8.10    next
    8.11      assume "\<not> 0 < c" with `c \<noteq> 0` have "c < 0" by auto
    8.12 @@ -552,23 +552,23 @@
    8.13        by (auto simp: field_simps)
    8.14      with `c < 0` show ?thesis
    8.15        by (cases "a \<le> b")
    8.16 -         (auto simp: field_simps emeasure_density positive_integral_distr
    8.17 -                     positive_integral_cmult borel_measurable_indicator' emeasure_distr)
    8.18 +         (auto simp: field_simps emeasure_density nn_integral_distr
    8.19 +                     nn_integral_cmult borel_measurable_indicator' emeasure_distr)
    8.20    qed
    8.21  qed simp
    8.22  
    8.23 -lemma positive_integral_real_affine:
    8.24 +lemma nn_integral_real_affine:
    8.25    fixes c :: real assumes [measurable]: "f \<in> borel_measurable borel" and c: "c \<noteq> 0"
    8.26    shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = \<bar>c\<bar> * (\<integral>\<^sup>+x. f (t + c * x) \<partial>lborel)"
    8.27    by (subst lborel_real_affine[OF c, of t])
    8.28 -     (simp add: positive_integral_density positive_integral_distr positive_integral_cmult)
    8.29 +     (simp add: nn_integral_density nn_integral_distr nn_integral_cmult)
    8.30  
    8.31  lemma lborel_integrable_real_affine:
    8.32    fixes f :: "real \<Rightarrow> _ :: {banach, second_countable_topology}"
    8.33    assumes f: "integrable lborel f"
    8.34    shows "c \<noteq> 0 \<Longrightarrow> integrable lborel (\<lambda>x. f (t + c * x))"
    8.35    using f f[THEN borel_measurable_integrable] unfolding integrable_iff_bounded
    8.36 -  by (subst (asm) positive_integral_real_affine[where c=c and t=t]) auto
    8.37 +  by (subst (asm) nn_integral_real_affine[where c=c and t=t]) auto
    8.38  
    8.39  lemma lborel_integrable_real_affine_iff:
    8.40    fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
    8.41 @@ -638,7 +638,7 @@
    8.42      by simp
    8.43  qed
    8.44  
    8.45 -lemma positive_integral_has_integral:
    8.46 +lemma nn_integral_has_integral:
    8.47    fixes f::"'a::ordered_euclidean_space \<Rightarrow> real"
    8.48    assumes f: "f \<in> borel_measurable lebesgue" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lebesgue) = ereal r"
    8.49    shows "(f has_integral r) UNIV"
    8.50 @@ -648,7 +648,7 @@
    8.51  next
    8.52    case (mult g c)
    8.53    then have "ereal c * (\<integral>\<^sup>+ x. g x \<partial>lebesgue) = ereal r"
    8.54 -    by (subst positive_integral_cmult[symmetric]) auto
    8.55 +    by (subst nn_integral_cmult[symmetric]) auto
    8.56    then obtain r' where "(c = 0 \<and> r = 0) \<or> ((\<integral>\<^sup>+ x. ereal (g x) \<partial>lebesgue) = ereal r' \<and> r = c * r')"
    8.57      by (cases "\<integral>\<^sup>+ x. ereal (g x) \<partial>lebesgue") (auto split: split_if_asm)
    8.58    with mult show ?case
    8.59 @@ -657,7 +657,7 @@
    8.60    case (add g h)
    8.61    moreover
    8.62    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)"
    8.63 -    unfolding plus_ereal.simps[symmetric] by (subst positive_integral_add) auto
    8.64 +    unfolding plus_ereal.simps[symmetric] by (subst nn_integral_add) auto
    8.65    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"
    8.66      by (cases "\<integral>\<^sup>+ x. h x \<partial>lebesgue" "\<integral>\<^sup>+ x. g x \<partial>lebesgue" rule: ereal2_cases) auto
    8.67    ultimately show ?case
    8.68 @@ -677,11 +677,11 @@
    8.69    
    8.70    { fix i
    8.71      have "(\<integral>\<^sup>+x. ereal (U i x) \<partial>lebesgue) \<le> (\<integral>\<^sup>+x. ereal (f x) \<partial>lebesgue)"
    8.72 -      using U_le_f by (intro positive_integral_mono) simp
    8.73 +      using U_le_f by (intro nn_integral_mono) simp
    8.74      then obtain p where "(\<integral>\<^sup>+x. U i x \<partial>lebesgue) = ereal p" "p \<le> r"
    8.75        using seq(6) by (cases "\<integral>\<^sup>+x. U i x \<partial>lebesgue") auto
    8.76      moreover then have "0 \<le> p"
    8.77 -      by (metis ereal_less_eq(5) positive_integral_positive)
    8.78 +      by (metis ereal_less_eq(5) nn_integral_nonneg)
    8.79      moreover note seq
    8.80      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"
    8.81        by auto }
    8.82 @@ -701,7 +701,7 @@
    8.83        using seq by auto
    8.84    qed
    8.85    moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lebesgue)) ----> (\<integral>\<^sup>+x. f x \<partial>lebesgue)"
    8.86 -    using seq U_le_f by (intro positive_integral_dominated_convergence[where w=f]) auto
    8.87 +    using seq U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto
    8.88    ultimately have "integral UNIV f = r"
    8.89      by (auto simp add: int_eq p seq intro: LIMSEQ_unique)
    8.90    with * show ?case
    8.91 @@ -712,9 +712,9 @@
    8.92    fixes f::"'a::ordered_euclidean_space \<Rightarrow> real"
    8.93    assumes f: "integrable lebesgue f" "\<And>x. 0 \<le> f x"
    8.94    shows "(f has_integral integral\<^sup>L lebesgue f) UNIV"
    8.95 -proof (rule positive_integral_has_integral)
    8.96 +proof (rule nn_integral_has_integral)
    8.97    show "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lebesgue) = ereal (integral\<^sup>L lebesgue f)"
    8.98 -    using f by (intro positive_integral_eq_integral) auto
    8.99 +    using f by (intro nn_integral_eq_integral) auto
   8.100  qed (insert f, auto)
   8.101  
   8.102  lemma has_integral_lebesgue_integral_lebesgue:
   8.103 @@ -744,13 +744,13 @@
   8.104    qed
   8.105  qed
   8.106  
   8.107 -lemma lebesgue_positive_integral_eq_borel:
   8.108 +lemma lebesgue_nn_integral_eq_borel:
   8.109    assumes f: "f \<in> borel_measurable borel"
   8.110 -  shows "integral\<^sup>P lebesgue f = integral\<^sup>P lborel f"
   8.111 +  shows "integral\<^sup>N lebesgue f = integral\<^sup>N lborel f"
   8.112  proof -
   8.113 -  from f have "integral\<^sup>P lebesgue (\<lambda>x. max 0 (f x)) = integral\<^sup>P lborel (\<lambda>x. max 0 (f x))"
   8.114 -    by (auto intro!: positive_integral_subalgebra[symmetric])
   8.115 -  then show ?thesis unfolding positive_integral_max_0 .
   8.116 +  from f have "integral\<^sup>N lebesgue (\<lambda>x. max 0 (f x)) = integral\<^sup>N lborel (\<lambda>x. max 0 (f x))"
   8.117 +    by (auto intro!: nn_integral_subalgebra[symmetric])
   8.118 +  then show ?thesis unfolding nn_integral_max_0 .
   8.119  qed
   8.120  
   8.121  lemma lebesgue_integral_eq_borel:
   8.122 @@ -777,29 +777,29 @@
   8.123      unfolding lebesgue_integral_eq_borel[OF borel] by simp
   8.124  qed
   8.125  
   8.126 -lemma positive_integral_bound_simple_function:
   8.127 +lemma nn_integral_bound_simple_function:
   8.128    assumes bnd: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x" "\<And>x. x \<in> space M \<Longrightarrow> f x < \<infinity>"
   8.129    assumes f[measurable]: "simple_function M f"
   8.130    assumes supp: "emeasure M {x\<in>space M. f x \<noteq> 0} < \<infinity>"
   8.131 -  shows "positive_integral M f < \<infinity>"
   8.132 +  shows "nn_integral M f < \<infinity>"
   8.133  proof cases
   8.134    assume "space M = {}"
   8.135 -  then have "positive_integral M f = (\<integral>\<^sup>+x. 0 \<partial>M)"
   8.136 -    by (intro positive_integral_cong) auto
   8.137 +  then have "nn_integral M f = (\<integral>\<^sup>+x. 0 \<partial>M)"
   8.138 +    by (intro nn_integral_cong) auto
   8.139    then show ?thesis by simp
   8.140  next
   8.141    assume "space M \<noteq> {}"
   8.142    with simple_functionD(1)[OF f] bnd have bnd: "0 \<le> Max (f`space M) \<and> Max (f`space M) < \<infinity>"
   8.143      by (subst Max_less_iff) (auto simp: Max_ge_iff)
   8.144    
   8.145 -  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)"
   8.146 -  proof (rule positive_integral_mono)
   8.147 +  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)"
   8.148 +  proof (rule nn_integral_mono)
   8.149      fix x assume "x \<in> space M"
   8.150      with f show "f x \<le> Max (f ` space M) * indicator {x \<in> space M. f x \<noteq> 0} x"
   8.151        by (auto split: split_indicator intro!: Max_ge simple_functionD)
   8.152    qed
   8.153    also have "\<dots> < \<infinity>"
   8.154 -    using bnd supp by (subst positive_integral_cmult) auto
   8.155 +    using bnd supp by (subst nn_integral_cmult) auto
   8.156    finally show ?thesis .
   8.157  qed
   8.158  
   8.159 @@ -814,10 +814,10 @@
   8.160    from f_borel have "(\<lambda>x. ereal (f x)) \<in> borel_measurable lebesgue" by auto
   8.161    from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
   8.162  
   8.163 -  have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lebesgue) = (SUP i. integral\<^sup>P lebesgue (F i))"
   8.164 +  have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lebesgue) = (SUP i. integral\<^sup>N lebesgue (F i))"
   8.165      using F
   8.166 -    by (subst positive_integral_monotone_convergence_SUP[symmetric])
   8.167 -       (simp_all add: positive_integral_max_0 borel_measurable_simple_function)
   8.168 +    by (subst nn_integral_monotone_convergence_SUP[symmetric])
   8.169 +       (simp_all add: nn_integral_max_0 borel_measurable_simple_function)
   8.170    also have "\<dots> \<le> ereal I"
   8.171    proof (rule SUP_least)
   8.172      fix i :: nat
   8.173 @@ -873,7 +873,7 @@
   8.174        unfolding integrable_iff_bounded
   8.175      proof
   8.176        have "(\<integral>\<^sup>+x. F i x \<partial>lebesgue) < \<infinity>"
   8.177 -      proof (rule positive_integral_bound_simple_function)
   8.178 +      proof (rule nn_integral_bound_simple_function)
   8.179          fix x::'a assume "x \<in> space lebesgue" then show "0 \<le> F i x" "F i x < \<infinity>"
   8.180            using F by (auto simp: image_iff eq_commute)
   8.181        next
   8.182 @@ -890,9 +890,9 @@
   8.183        by (rule has_integral_lebesgue_integral_lebesgue)
   8.184      from this I have "integral\<^sup>L lebesgue (\<lambda>x. real (F i x)) \<le> I"
   8.185        by (rule has_integral_le) (intro ballI F_bound)
   8.186 -    moreover have "integral\<^sup>P lebesgue (F i) = integral\<^sup>L lebesgue (\<lambda>x. real (F i x))"
   8.187 -      using int F by (subst positive_integral_eq_integral[symmetric])  (auto simp: F_eq2[symmetric] real_of_ereal_pos)
   8.188 -    ultimately show "integral\<^sup>P lebesgue (F i) \<le> ereal I"
   8.189 +    moreover have "integral\<^sup>N lebesgue (F i) = integral\<^sup>L lebesgue (\<lambda>x. real (F i x))"
   8.190 +      using int F by (subst nn_integral_eq_integral[symmetric])  (auto simp: F_eq2[symmetric] real_of_ereal_pos)
   8.191 +    ultimately show "integral\<^sup>N lebesgue (F i) \<le> ereal I"
   8.192        by simp
   8.193    qed
   8.194    finally show "integrable lebesgue f"
   8.195 @@ -1003,8 +1003,8 @@
   8.196  lemma borel_fubini_positiv_integral:
   8.197    fixes f :: "'a::ordered_euclidean_space \<Rightarrow> ereal"
   8.198    assumes f: "f \<in> borel_measurable borel"
   8.199 -  shows "integral\<^sup>P lborel f = \<integral>\<^sup>+x. f (p2e x) \<partial>(\<Pi>\<^sub>M (i::'a)\<in>Basis. lborel)"
   8.200 -  by (subst lborel_eq_lborel_space) (simp add: positive_integral_distr measurable_p2e f)
   8.201 +  shows "integral\<^sup>N lborel f = \<integral>\<^sup>+x. f (p2e x) \<partial>(\<Pi>\<^sub>M (i::'a)\<in>Basis. lborel)"
   8.202 +  by (subst lborel_eq_lborel_space) (simp add: nn_integral_distr measurable_p2e f)
   8.203  
   8.204  lemma borel_fubini_integrable:
   8.205    fixes f :: "'a::ordered_euclidean_space \<Rightarrow> _::{banach, second_countable_topology}"
   8.206 @@ -1125,21 +1125,21 @@
   8.207      by (intro integrable_has_integral_nonneg) (auto split: split_indicator)
   8.208  qed
   8.209  
   8.210 -lemma positive_integral_FTC_atLeastAtMost:
   8.211 +lemma nn_integral_FTC_atLeastAtMost:
   8.212    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"
   8.213    shows "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
   8.214  proof -
   8.215    have "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)"
   8.216      by (rule integrable_FTC_Icc_nonneg) fact+
   8.217    then have "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = (\<integral>x. f x * indicator {a .. b} x \<partial>lborel)"
   8.218 -    using assms by (intro positive_integral_eq_integral) (auto simp: indicator_def)
   8.219 +    using assms by (intro nn_integral_eq_integral) (auto simp: indicator_def)
   8.220    also have "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
   8.221      by (rule integral_FTC_Icc_nonneg) fact+
   8.222    finally show ?thesis
   8.223      unfolding ereal_indicator[symmetric] by simp
   8.224  qed
   8.225  
   8.226 -lemma positive_integral_FTC_atLeast:
   8.227 +lemma nn_integral_FTC_atLeast:
   8.228    fixes f :: "real \<Rightarrow> real"
   8.229    assumes f_borel: "f \<in> borel_measurable borel"
   8.230    assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x" 
   8.231 @@ -1161,10 +1161,10 @@
   8.232      then show "(\<lambda>n. ?f n x) ----> ?fR x"
   8.233        by (rule Lim_eventually)
   8.234    qed
   8.235 -  then have "integral\<^sup>P lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
   8.236 +  then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
   8.237      by simp
   8.238    also have "\<dots> = (SUP i::nat. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))"
   8.239 -  proof (rule positive_integral_monotone_convergence_SUP)
   8.240 +  proof (rule nn_integral_monotone_convergence_SUP)
   8.241      show "incseq ?f"
   8.242        using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
   8.243      show "\<And>i. (?f i) \<in> borel_measurable lborel"
   8.244 @@ -1173,7 +1173,7 @@
   8.245        using nonneg by (auto split: split_indicator)
   8.246    qed
   8.247    also have "\<dots> = (SUP i::nat. ereal (F (a + real i) - F a))"
   8.248 -    by (subst positive_integral_FTC_atLeastAtMost[OF f_borel f nonneg]) auto
   8.249 +    by (subst nn_integral_FTC_atLeastAtMost[OF f_borel f nonneg]) auto
   8.250    also have "\<dots> = T - F a"
   8.251    proof (rule SUP_Lim_ereal)
   8.252      show "incseq (\<lambda>n. ereal (F (a + real n) - F a))"
     9.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon May 19 13:53:58 2014 +0200
     9.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon May 19 14:26:58 2014 +0200
     9.3 @@ -17,7 +17,7 @@
     9.4  
     9.5  text {*
     9.6  
     9.7 -Our simple functions are not restricted to positive real numbers. Instead
     9.8 +Our simple functions are not restricted to nonnegative real numbers. Instead
     9.9  they are just functions with a finite range and are measurable when singleton
    9.10  sets are measurable.
    9.11  
    9.12 @@ -725,7 +725,7 @@
    9.13    using simple_integral_mult[OF simple_function_indicator[OF A]]
    9.14    unfolding simple_integral_indicator_only[OF A] by simp
    9.15  
    9.16 -lemma simple_integral_positive:
    9.17 +lemma simple_integral_nonneg:
    9.18    assumes f: "simple_function M f" and ae: "AE x in M. 0 \<le> f x"
    9.19    shows "0 \<le> integral\<^sup>S M f"
    9.20  proof -
    9.21 @@ -736,26 +736,26 @@
    9.22  
    9.23  subsection {* Integral on nonnegative functions *}
    9.24  
    9.25 -definition positive_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>P") where
    9.26 -  "integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^sup>S M g)"
    9.27 +definition nn_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>N") where
    9.28 +  "integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^sup>S M g)"
    9.29  
    9.30  syntax
    9.31 -  "_positive_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>+ _. _ \<partial>_" [60,61] 110)
    9.32 +  "_nn_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>+ _. _ \<partial>_" [60,61] 110)
    9.33  
    9.34  translations
    9.35 -  "\<integral>\<^sup>+ x. f \<partial>M" == "CONST positive_integral M (%x. f)"
    9.36 +  "\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)"
    9.37  
    9.38 -lemma positive_integral_positive:
    9.39 -  "0 \<le> integral\<^sup>P M f"
    9.40 -  by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: positive_integral_def le_fun_def)
    9.41 +lemma nn_integral_nonneg:
    9.42 +  "0 \<le> integral\<^sup>N M f"
    9.43 +  by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: nn_integral_def le_fun_def)
    9.44  
    9.45 -lemma positive_integral_not_MInfty[simp]: "integral\<^sup>P M f \<noteq> -\<infinity>"
    9.46 -  using positive_integral_positive[of M f] by auto
    9.47 +lemma nn_integral_not_MInfty[simp]: "integral\<^sup>N M f \<noteq> -\<infinity>"
    9.48 +  using nn_integral_nonneg[of M f] by auto
    9.49  
    9.50 -lemma positive_integral_def_finite:
    9.51 -  "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)"
    9.52 +lemma nn_integral_def_finite:
    9.53 +  "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)"
    9.54      (is "_ = SUPREMUM ?A ?f")
    9.55 -  unfolding positive_integral_def
    9.56 +  unfolding nn_integral_def
    9.57  proof (safe intro!: antisym SUP_least)
    9.58    fix g assume g: "simple_function M g" "g \<le> max 0 \<circ> f"
    9.59    let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}"
    9.60 @@ -797,9 +797,9 @@
    9.61    qed
    9.62  qed (auto intro: SUP_upper)
    9.63  
    9.64 -lemma positive_integral_mono_AE:
    9.65 -  assumes ae: "AE x in M. u x \<le> v x" shows "integral\<^sup>P M u \<le> integral\<^sup>P M v"
    9.66 -  unfolding positive_integral_def
    9.67 +lemma nn_integral_mono_AE:
    9.68 +  assumes ae: "AE x in M. u x \<le> v x" shows "integral\<^sup>N M u \<le> integral\<^sup>N M v"
    9.69 +  unfolding nn_integral_def
    9.70  proof (safe intro!: SUP_mono)
    9.71    fix n assume n: "simple_function M n" "n \<le> max 0 \<circ> u"
    9.72    from ae[THEN AE_E] guess N . note N = this
    9.73 @@ -822,57 +822,57 @@
    9.74      by force
    9.75  qed
    9.76  
    9.77 -lemma positive_integral_mono:
    9.78 -  "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^sup>P M u \<le> integral\<^sup>P M v"
    9.79 -  by (auto intro: positive_integral_mono_AE)
    9.80 +lemma nn_integral_mono:
    9.81 +  "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^sup>N M u \<le> integral\<^sup>N M v"
    9.82 +  by (auto intro: nn_integral_mono_AE)
    9.83  
    9.84 -lemma positive_integral_cong_AE:
    9.85 -  "AE x in M. u x = v x \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P M v"
    9.86 -  by (auto simp: eq_iff intro!: positive_integral_mono_AE)
    9.87 +lemma nn_integral_cong_AE:
    9.88 +  "AE x in M. u x = v x \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v"
    9.89 +  by (auto simp: eq_iff intro!: nn_integral_mono_AE)
    9.90  
    9.91 -lemma positive_integral_cong:
    9.92 -  "(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P M v"
    9.93 -  by (auto intro: positive_integral_cong_AE)
    9.94 +lemma nn_integral_cong:
    9.95 +  "(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v"
    9.96 +  by (auto intro: nn_integral_cong_AE)
    9.97  
    9.98 -lemma positive_integral_cong_strong:
    9.99 -  "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"
   9.100 -  by (auto intro: positive_integral_cong)
   9.101 +lemma nn_integral_cong_strong:
   9.102 +  "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"
   9.103 +  by (auto intro: nn_integral_cong)
   9.104  
   9.105 -lemma positive_integral_eq_simple_integral:
   9.106 -  assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^sup>P M f = integral\<^sup>S M f"
   9.107 +lemma nn_integral_eq_simple_integral:
   9.108 +  assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^sup>N M f = integral\<^sup>S M f"
   9.109  proof -
   9.110    let ?f = "\<lambda>x. f x * indicator (space M) x"
   9.111    have f': "simple_function M ?f" using f by auto
   9.112    with f(2) have [simp]: "max 0 \<circ> ?f = ?f"
   9.113      by (auto simp: fun_eq_iff max_def split: split_indicator)
   9.114 -  have "integral\<^sup>P M ?f \<le> integral\<^sup>S M ?f" using f'
   9.115 -    by (force intro!: SUP_least simple_integral_mono simp: le_fun_def positive_integral_def)
   9.116 -  moreover have "integral\<^sup>S M ?f \<le> integral\<^sup>P M ?f"
   9.117 -    unfolding positive_integral_def
   9.118 +  have "integral\<^sup>N M ?f \<le> integral\<^sup>S M ?f" using f'
   9.119 +    by (force intro!: SUP_least simple_integral_mono simp: le_fun_def nn_integral_def)
   9.120 +  moreover have "integral\<^sup>S M ?f \<le> integral\<^sup>N M ?f"
   9.121 +    unfolding nn_integral_def
   9.122      using f' by (auto intro!: SUP_upper)
   9.123    ultimately show ?thesis
   9.124 -    by (simp cong: positive_integral_cong simple_integral_cong)
   9.125 +    by (simp cong: nn_integral_cong simple_integral_cong)
   9.126  qed
   9.127  
   9.128 -lemma positive_integral_eq_simple_integral_AE:
   9.129 -  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"
   9.130 +lemma nn_integral_eq_simple_integral_AE:
   9.131 +  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"
   9.132  proof -
   9.133    have "AE x in M. f x = max 0 (f x)" using f by (auto split: split_max)
   9.134 -  with f have "integral\<^sup>P M f = integral\<^sup>S M (\<lambda>x. max 0 (f x))"
   9.135 -    by (simp cong: positive_integral_cong_AE simple_integral_cong_AE
   9.136 -             add: positive_integral_eq_simple_integral)
   9.137 +  with f have "integral\<^sup>N M f = integral\<^sup>S M (\<lambda>x. max 0 (f x))"
   9.138 +    by (simp cong: nn_integral_cong_AE simple_integral_cong_AE
   9.139 +             add: nn_integral_eq_simple_integral)
   9.140    with assms show ?thesis
   9.141      by (auto intro!: simple_integral_cong_AE split: split_max)
   9.142  qed
   9.143  
   9.144 -lemma positive_integral_SUP_approx:
   9.145 +lemma nn_integral_SUP_approx:
   9.146    assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
   9.147    and u: "simple_function M u" "u \<le> (SUP i. f i)" "u`space M \<subseteq> {0..<\<infinity>}"
   9.148 -  shows "integral\<^sup>S M u \<le> (SUP i. integral\<^sup>P M (f i))" (is "_ \<le> ?S")
   9.149 +  shows "integral\<^sup>S M u \<le> (SUP i. integral\<^sup>N M (f i))" (is "_ \<le> ?S")
   9.150  proof (rule ereal_le_mult_one_interval)
   9.151 -  have "0 \<le> (SUP i. integral\<^sup>P M (f i))"
   9.152 -    using f(3) by (auto intro!: SUP_upper2 positive_integral_positive)
   9.153 -  then show "(SUP i. integral\<^sup>P M (f i)) \<noteq> -\<infinity>" by auto
   9.154 +  have "0 \<le> (SUP i. integral\<^sup>N M (f i))"
   9.155 +    using f(3) by (auto intro!: SUP_upper2 nn_integral_nonneg)
   9.156 +  then show "(SUP i. integral\<^sup>N M (f i)) \<noteq> -\<infinity>" by auto
   9.157    have u_range: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> u x \<and> u x \<noteq> \<infinity>"
   9.158      using u(3) by auto
   9.159    fix a :: ereal assume "0 < a" "a < 1"
   9.160 @@ -940,55 +940,55 @@
   9.161      have "a * integral\<^sup>S M (?uB i) = (\<integral>\<^sup>Sx. a * ?uB i x \<partial>M)"
   9.162        using B `simple_function M u` u_range
   9.163        by (subst simple_integral_mult) (auto split: split_indicator)
   9.164 -    also have "\<dots> \<le> integral\<^sup>P M (f i)"
   9.165 +    also have "\<dots> \<le> integral\<^sup>N M (f i)"
   9.166      proof -
   9.167        have *: "simple_function M (\<lambda>x. a * ?uB i x)" using B `0 < a` u(1) by auto
   9.168        show ?thesis using f(3) * u_range `0 < a`
   9.169 -        by (subst positive_integral_eq_simple_integral[symmetric])
   9.170 -           (auto intro!: positive_integral_mono split: split_indicator)
   9.171 +        by (subst nn_integral_eq_simple_integral[symmetric])
   9.172 +           (auto intro!: nn_integral_mono split: split_indicator)
   9.173      qed
   9.174 -    finally show "a * integral\<^sup>S M (?uB i) \<le> integral\<^sup>P M (f i)"
   9.175 +    finally show "a * integral\<^sup>S M (?uB i) \<le> integral\<^sup>N M (f i)"
   9.176        by auto
   9.177    next
   9.178      fix i show "0 \<le> \<integral>\<^sup>S x. ?uB i x \<partial>M" using B `0 < a` u(1) u_range
   9.179 -      by (intro simple_integral_positive) (auto split: split_indicator)
   9.180 +      by (intro simple_integral_nonneg) (auto split: split_indicator)
   9.181    qed (insert `0 < a`, auto)
   9.182    ultimately show "a * integral\<^sup>S M u \<le> ?S" by simp
   9.183  qed
   9.184  
   9.185 -lemma incseq_positive_integral:
   9.186 -  assumes "incseq f" shows "incseq (\<lambda>i. integral\<^sup>P M (f i))"
   9.187 +lemma incseq_nn_integral:
   9.188 +  assumes "incseq f" shows "incseq (\<lambda>i. integral\<^sup>N M (f i))"
   9.189  proof -
   9.190    have "\<And>i x. f i x \<le> f (Suc i) x"
   9.191      using assms by (auto dest!: incseq_SucD simp: le_fun_def)
   9.192    then show ?thesis
   9.193 -    by (auto intro!: incseq_SucI positive_integral_mono)
   9.194 +    by (auto intro!: incseq_SucI nn_integral_mono)
   9.195  qed
   9.196  
   9.197  text {* Beppo-Levi monotone convergence theorem *}
   9.198 -lemma positive_integral_monotone_convergence_SUP:
   9.199 +lemma nn_integral_monotone_convergence_SUP:
   9.200    assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
   9.201 -  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"
   9.202 +  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))"
   9.203  proof (rule antisym)
   9.204 -  show "(SUP j. integral\<^sup>P M (f j)) \<le> (\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M)"
   9.205 -    by (auto intro!: SUP_least SUP_upper positive_integral_mono)
   9.206 +  show "(SUP j. integral\<^sup>N M (f j)) \<le> (\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M)"
   9.207 +    by (auto intro!: SUP_least SUP_upper nn_integral_mono)
   9.208  next
   9.209 -  show "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^sup>P M (f j))"
   9.210 -    unfolding positive_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"]
   9.211 +  show "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^sup>N M (f j))"
   9.212 +    unfolding nn_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"]
   9.213    proof (safe intro!: SUP_least)
   9.214      fix g assume g: "simple_function M g"
   9.215        and *: "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
   9.216      then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
   9.217        using f by (auto intro!: SUP_upper2)
   9.218 -    with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>P M (f j))"
   9.219 -      by (intro  positive_integral_SUP_approx[OF f g _ g'])
   9.220 +    with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>N M (f j))"
   9.221 +      by (intro  nn_integral_SUP_approx[OF f g _ g'])
   9.222           (auto simp: le_fun_def max_def)
   9.223    qed
   9.224  qed
   9.225  
   9.226 -lemma positive_integral_monotone_convergence_SUP_AE:
   9.227 +lemma nn_integral_monotone_convergence_SUP_AE:
   9.228    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"
   9.229 -  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"
   9.230 +  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))"
   9.231  proof -
   9.232    from f have "AE x in M. \<forall>i. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x"
   9.233      by (simp add: AE_all_countable)
   9.234 @@ -996,9 +996,9 @@
   9.235    let ?f = "\<lambda>i x. if x \<in> space M - N then f i x else 0"
   9.236    have f_eq: "AE x in M. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ _ N])
   9.237    then have "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>M)"
   9.238 -    by (auto intro!: positive_integral_cong_AE)
   9.239 +    by (auto intro!: nn_integral_cong_AE)
   9.240    also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. ?f i x \<partial>M))"
   9.241 -  proof (rule positive_integral_monotone_convergence_SUP)
   9.242 +  proof (rule nn_integral_monotone_convergence_SUP)
   9.243      show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI)
   9.244      { fix i show "(\<lambda>x. if x \<in> space M - N then f i x else 0) \<in> borel_measurable M"
   9.245          using f N(3) by (intro measurable_If_set) auto
   9.246 @@ -1006,39 +1006,39 @@
   9.247          using N(1) by auto }
   9.248    qed
   9.249    also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))"
   9.250 -    using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] positive_integral_cong_AE ext)
   9.251 +    using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] nn_integral_cong_AE ext)
   9.252    finally show ?thesis .
   9.253  qed
   9.254  
   9.255 -lemma positive_integral_monotone_convergence_SUP_AE_incseq:
   9.256 +lemma nn_integral_monotone_convergence_SUP_AE_incseq:
   9.257    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"
   9.258 -  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"
   9.259 +  shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))"
   9.260    using f[unfolded incseq_Suc_iff le_fun_def]
   9.261 -  by (intro positive_integral_monotone_convergence_SUP_AE[OF _ borel])
   9.262 +  by (intro nn_integral_monotone_convergence_SUP_AE[OF _ borel])
   9.263       auto
   9.264  
   9.265 -lemma positive_integral_monotone_convergence_simple:
   9.266 +lemma nn_integral_monotone_convergence_simple:
   9.267    assumes f: "incseq f" "\<And>i x. 0 \<le> f i x" "\<And>i. simple_function M (f i)"
   9.268    shows "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
   9.269 -  using assms unfolding positive_integral_monotone_convergence_SUP[OF f(1)
   9.270 +  using assms unfolding nn_integral_monotone_convergence_SUP[OF f(1)
   9.271      f(3)[THEN borel_measurable_simple_function] f(2)]
   9.272 -  by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPREMUM UNIV"] ext)
   9.273 +  by (auto intro!: nn_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPREMUM UNIV"] ext)
   9.274  
   9.275 -lemma positive_integral_max_0:
   9.276 -  "(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>P M f"
   9.277 -  by (simp add: le_fun_def positive_integral_def)
   9.278 +lemma nn_integral_max_0:
   9.279 +  "(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>N M f"
   9.280 +  by (simp add: le_fun_def nn_integral_def)
   9.281  
   9.282 -lemma positive_integral_cong_pos:
   9.283 +lemma nn_integral_cong_pos:
   9.284    assumes "\<And>x. x \<in> space M \<Longrightarrow> f x \<le> 0 \<and> g x \<le> 0 \<or> f x = g x"
   9.285 -  shows "integral\<^sup>P M f = integral\<^sup>P M g"
   9.286 +  shows "integral\<^sup>N M f = integral\<^sup>N M g"
   9.287  proof -
   9.288 -  have "integral\<^sup>P M (\<lambda>x. max 0 (f x)) = integral\<^sup>P M (\<lambda>x. max 0 (g x))"
   9.289 -  proof (intro positive_integral_cong)
   9.290 +  have "integral\<^sup>N M (\<lambda>x. max 0 (f x)) = integral\<^sup>N M (\<lambda>x. max 0 (g x))"
   9.291 +  proof (intro nn_integral_cong)
   9.292      fix x assume "x \<in> space M"
   9.293      from assms[OF this] show "max 0 (f x) = max 0 (g x)"
   9.294        by (auto split: split_max)
   9.295    qed
   9.296 -  then show ?thesis by (simp add: positive_integral_max_0)
   9.297 +  then show ?thesis by (simp add: nn_integral_max_0)
   9.298  qed
   9.299  
   9.300  lemma SUP_simple_integral_sequences:
   9.301 @@ -1049,40 +1049,40 @@
   9.302      (is "SUPREMUM _ ?F = SUPREMUM _ ?G")
   9.303  proof -
   9.304    have "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
   9.305 -    using f by (rule positive_integral_monotone_convergence_simple)
   9.306 +    using f by (rule nn_integral_monotone_convergence_simple)
   9.307    also have "\<dots> = (\<integral>\<^sup>+x. (SUP i. g i x) \<partial>M)"
   9.308 -    unfolding eq[THEN positive_integral_cong_AE] ..
   9.309 +    unfolding eq[THEN nn_integral_cong_AE] ..
   9.310    also have "\<dots> = (SUP i. ?G i)"
   9.311 -    using g by (rule positive_integral_monotone_convergence_simple[symmetric])
   9.312 +    using g by (rule nn_integral_monotone_convergence_simple[symmetric])
   9.313    finally show ?thesis by simp
   9.314  qed
   9.315  
   9.316 -lemma positive_integral_const[simp]:
   9.317 +lemma nn_integral_const[simp]:
   9.318    "0 \<le> c \<Longrightarrow> (\<integral>\<^sup>+ x. c \<partial>M) = c * (emeasure M) (space M)"
   9.319 -  by (subst positive_integral_eq_simple_integral) auto
   9.320 +  by (subst nn_integral_eq_simple_integral) auto
   9.321  
   9.322 -lemma positive_integral_linear:
   9.323 +lemma nn_integral_linear:
   9.324    assumes f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" and "0 \<le> a"
   9.325    and g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x"
   9.326 -  shows "(\<integral>\<^sup>+ x. a * f x + g x \<partial>M) = a * integral\<^sup>P M f + integral\<^sup>P M g"
   9.327 -    (is "integral\<^sup>P M ?L = _")
   9.328 +  shows "(\<integral>\<^sup>+ x. a * f x + g x \<partial>M) = a * integral\<^sup>N M f + integral\<^sup>N M g"
   9.329 +    (is "integral\<^sup>N M ?L = _")
   9.330  proof -
   9.331    from borel_measurable_implies_simple_function_sequence'[OF f(1)] guess u .
   9.332 -  note u = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
   9.333 +  note u = nn_integral_monotone_convergence_simple[OF this(2,5,1)] this
   9.334    from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v .
   9.335 -  note v = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
   9.336 +  note v = nn_integral_monotone_convergence_simple[OF this(2,5,1)] this
   9.337    let ?L' = "\<lambda>i x. a * u i x + v i x"
   9.338  
   9.339    have "?L \<in> borel_measurable M" using assms by auto
   9.340    from borel_measurable_implies_simple_function_sequence'[OF this] guess l .
   9.341 -  note l = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
   9.342 +  note l = nn_integral_monotone_convergence_simple[OF this(2,5,1)] this
   9.343  
   9.344    have inc: "incseq (\<lambda>i. a * integral\<^sup>S M (u i))" "incseq (\<lambda>i. integral\<^sup>S M (v i))"
   9.345      using u v `0 \<le> a`
   9.346      by (auto simp: incseq_Suc_iff le_fun_def
   9.347               intro!: add_mono ereal_mult_left_mono simple_integral_mono)
   9.348    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)"
   9.349 -    using u v `0 \<le> a` by (auto simp: simple_integral_positive)
   9.350 +    using u v `0 \<le> a` by (auto simp: simple_integral_nonneg)
   9.351    { fix i from pos[of i] have "a * integral\<^sup>S M (u i) \<noteq> -\<infinity>" "integral\<^sup>S M (v i) \<noteq> -\<infinity>"
   9.352        by (auto split: split_if_asm) }
   9.353    note not_MInf = this
   9.354 @@ -1111,69 +1111,69 @@
   9.355      unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
   9.356      apply (subst SUP_ereal_cmult [symmetric, OF pos(1) `0 \<le> a`])
   9.357      apply (subst SUP_ereal_add [symmetric, OF inc not_MInf]) .
   9.358 -  then show ?thesis by (simp add: positive_integral_max_0)
   9.359 +  then show ?thesis by (simp add: nn_integral_max_0)
   9.360  qed
   9.361  
   9.362 -lemma positive_integral_cmult:
   9.363 +lemma nn_integral_cmult:
   9.364    assumes f: "f \<in> borel_measurable M" "0 \<le> c"
   9.365 -  shows "(\<integral>\<^sup>+ x. c * f x \<partial>M) = c * integral\<^sup>P M f"
   9.366 +  shows "(\<integral>\<^sup>+ x. c * f x \<partial>M) = c * integral\<^sup>N M f"
   9.367  proof -
   9.368    have [simp]: "\<And>x. c * max 0 (f x) = max 0 (c * f x)" using `0 \<le> c`
   9.369      by (auto split: split_max simp: ereal_zero_le_0_iff)
   9.370    have "(\<integral>\<^sup>+ x. c * f x \<partial>M) = (\<integral>\<^sup>+ x. c * max 0 (f x) \<partial>M)"
   9.371 -    by (simp add: positive_integral_max_0)
   9.372 +    by (simp add: nn_integral_max_0)
   9.373    then show ?thesis
   9.374 -    using positive_integral_linear[OF _ _ `0 \<le> c`, of "\<lambda>x. max 0 (f x)" _ "\<lambda>x. 0"] f
   9.375 -    by (auto simp: positive_integral_max_0)
   9.376 +    using nn_integral_linear[OF _ _ `0 \<le> c`, of "\<lambda>x. max 0 (f x)" _ "\<lambda>x. 0"] f
   9.377 +    by (auto simp: nn_integral_max_0)
   9.378  qed
   9.379  
   9.380 -lemma positive_integral_multc:
   9.381 +lemma nn_integral_multc:
   9.382    assumes "f \<in> borel_measurable M" "0 \<le> c"
   9.383 -  shows "(\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>P M f * c"
   9.384 -  unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp
   9.385 +  shows "(\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>N M f * c"
   9.386 +  unfolding mult_commute[of _ c] nn_integral_cmult[OF assms] by simp
   9.387  
   9.388 -lemma positive_integral_indicator[simp]:
   9.389 +lemma nn_integral_indicator[simp]:
   9.390    "A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. indicator A x\<partial>M) = (emeasure M) A"
   9.391 -  by (subst positive_integral_eq_simple_integral)
   9.392 +  by (subst nn_integral_eq_simple_integral)
   9.393       (auto simp: simple_integral_indicator)
   9.394  
   9.395 -lemma positive_integral_cmult_indicator:
   9.396 +lemma nn_integral_cmult_indicator:
   9.397    "0 \<le> c \<Longrightarrow> A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. c * indicator A x \<partial>M) = c * (emeasure M) A"
   9.398 -  by (subst positive_integral_eq_simple_integral)
   9.399 +  by (subst nn_integral_eq_simple_integral)
   9.400       (auto simp: simple_function_indicator simple_integral_indicator)
   9.401  
   9.402 -lemma positive_integral_indicator':
   9.403 +lemma nn_integral_indicator':
   9.404    assumes [measurable]: "A \<inter> space M \<in> sets M"
   9.405    shows "(\<integral>\<^sup>+ x. indicator A x \<partial>M) = emeasure M (A \<inter> space M)"
   9.406  proof -
   9.407    have "(\<integral>\<^sup>+ x. indicator A x \<partial>M) = (\<integral>\<^sup>+ x. indicator (A \<inter> space M) x \<partial>M)"
   9.408 -    by (intro positive_integral_cong) (simp split: split_indicator)
   9.409 +    by (intro nn_integral_cong) (simp split: split_indicator)
   9.410    also have "\<dots> = emeasure M (A \<inter> space M)"
   9.411      by simp
   9.412    finally show ?thesis .
   9.413  qed
   9.414  
   9.415 -lemma positive_integral_add:
   9.416 +lemma nn_integral_add:
   9.417    assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
   9.418    and g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
   9.419 -  shows "(\<integral>\<^sup>+ x. f x + g x \<partial>M) = integral\<^sup>P M f + integral\<^sup>P M g"
   9.420 +  shows "(\<integral>\<^sup>+ x. f x + g x \<partial>M) = integral\<^sup>N M f + integral\<^sup>N M g"
   9.421  proof -
   9.422    have ae: "AE x in M. max 0 (f x) + max 0 (g x) = max 0 (f x + g x)"
   9.423      using assms by (auto split: split_max)
   9.424    have "(\<integral>\<^sup>+ x. f x + g x \<partial>M) = (\<integral>\<^sup>+ x. max 0 (f x + g x) \<partial>M)"
   9.425 -    by (simp add: positive_integral_max_0)
   9.426 +    by (simp add: nn_integral_max_0)
   9.427    also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) + max 0 (g x) \<partial>M)"
   9.428 -    unfolding ae[THEN positive_integral_cong_AE] ..
   9.429 +    unfolding ae[THEN nn_integral_cong_AE] ..
   9.430    also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) \<partial>M) + (\<integral>\<^sup>+ x. max 0 (g x) \<partial>M)"
   9.431 -    using positive_integral_linear[of "\<lambda>x. max 0 (f x)" _ 1 "\<lambda>x. max 0 (g x)"] f g
   9.432 +    using nn_integral_linear[of "\<lambda>x. max 0 (f x)" _ 1 "\<lambda>x. max 0 (g x)"] f g
   9.433      by auto
   9.434    finally show ?thesis
   9.435 -    by (simp add: positive_integral_max_0)
   9.436 +    by (simp add: nn_integral_max_0)
   9.437  qed
   9.438  
   9.439 -lemma positive_integral_setsum:
   9.440 +lemma nn_integral_setsum:
   9.441    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"
   9.442 -  shows "(\<integral>\<^sup>+ x. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^sup>P M (f i))"
   9.443 +  shows "(\<integral>\<^sup>+ x. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^sup>N M (f i))"
   9.444  proof cases
   9.445    assume f: "finite P"
   9.446    from assms have "AE x in M. \<forall>i\<in>P. 0 \<le> f i x" unfolding AE_finite_all[OF f] by auto
   9.447 @@ -1183,12 +1183,12 @@
   9.448      then have "f i \<in> borel_measurable M" "AE x in M. 0 \<le> f i x"
   9.449        "(\<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)"
   9.450        by (auto intro!: setsum_nonneg)
   9.451 -    from positive_integral_add[OF this]
   9.452 +    from nn_integral_add[OF this]
   9.453      show ?case using insert by auto
   9.454    qed simp
   9.455  qed simp
   9.456  
   9.457 -lemma positive_integral_Markov_inequality:
   9.458 +lemma nn_integral_Markov_inequality:
   9.459    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"
   9.460    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)"
   9.461      (is "(emeasure M) ?A \<le> _ * ?PI")
   9.462 @@ -1196,19 +1196,19 @@
   9.463    have "?A \<in> sets M"
   9.464      using `A \<in> sets M` u by auto
   9.465    hence "(emeasure M) ?A = (\<integral>\<^sup>+ x. indicator ?A x \<partial>M)"
   9.466 -    using positive_integral_indicator by simp
   9.467 +    using nn_integral_indicator by simp
   9.468    also have "\<dots> \<le> (\<integral>\<^sup>+ x. c * (u x * indicator A x) \<partial>M)" using u c
   9.469 -    by (auto intro!: positive_integral_mono_AE
   9.470 +    by (auto intro!: nn_integral_mono_AE
   9.471        simp: indicator_def ereal_zero_le_0_iff)
   9.472    also have "\<dots> = c * (\<integral>\<^sup>+ x. u x * indicator A x \<partial>M)"
   9.473      using assms
   9.474 -    by (auto intro!: positive_integral_cmult simp: ereal_zero_le_0_iff)
   9.475 +    by (auto intro!: nn_integral_cmult simp: ereal_zero_le_0_iff)
   9.476    finally show ?thesis .
   9.477  qed
   9.478  
   9.479 -lemma positive_integral_noteq_infinite:
   9.480 +lemma nn_integral_noteq_infinite:
   9.481    assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
   9.482 -  and "integral\<^sup>P M g \<noteq> \<infinity>"
   9.483 +  and "integral\<^sup>N M g \<noteq> \<infinity>"
   9.484    shows "AE x in M. g x \<noteq> \<infinity>"
   9.485  proof (rule ccontr)
   9.486    assume c: "\<not> (AE x in M. g x \<noteq> \<infinity>)"
   9.487 @@ -1218,34 +1218,34 @@
   9.488    ultimately have "0 < (emeasure M) {x\<in>space M. g x = \<infinity>}" by auto
   9.489    then have "\<infinity> = \<infinity> * (emeasure M) {x\<in>space M. g x = \<infinity>}" by auto
   9.490    also have "\<dots> \<le> (\<integral>\<^sup>+x. \<infinity> * indicator {x\<in>space M. g x = \<infinity>} x \<partial>M)"
   9.491 -    using g by (subst positive_integral_cmult_indicator) auto
   9.492 -  also have "\<dots> \<le> integral\<^sup>P M g"
   9.493 -    using assms by (auto intro!: positive_integral_mono_AE simp: indicator_def)
   9.494 -  finally show False using `integral\<^sup>P M g \<noteq> \<infinity>` by auto
   9.495 +    using g by (subst nn_integral_cmult_indicator) auto
   9.496 +  also have "\<dots> \<le> integral\<^sup>N M g"
   9.497 +    using assms by (auto intro!: nn_integral_mono_AE simp: indicator_def)
   9.498 +  finally show False using `integral\<^sup>N M g \<noteq> \<infinity>` by auto
   9.499  qed
   9.500  
   9.501 -lemma positive_integral_PInf:
   9.502 +lemma nn_integral_PInf:
   9.503    assumes f: "f \<in> borel_measurable M"
   9.504 -  and not_Inf: "integral\<^sup>P M f \<noteq> \<infinity>"
   9.505 +  and not_Inf: "integral\<^sup>N M f \<noteq> \<infinity>"
   9.506    shows "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
   9.507  proof -
   9.508    have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) = (\<integral>\<^sup>+ x. \<infinity> * indicator (f -` {\<infinity>} \<inter> space M) x \<partial>M)"
   9.509 -    using f by (subst positive_integral_cmult_indicator) (auto simp: measurable_sets)
   9.510 -  also have "\<dots> \<le> integral\<^sup>P M (\<lambda>x. max 0 (f x))"
   9.511 -    by (auto intro!: positive_integral_mono simp: indicator_def max_def)
   9.512 -  finally have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) \<le> integral\<^sup>P M f"
   9.513 -    by (simp add: positive_integral_max_0)
   9.514 +    using f by (subst nn_integral_cmult_indicator) (auto simp: measurable_sets)
   9.515 +  also have "\<dots> \<le> integral\<^sup>N M (\<lambda>x. max 0 (f x))"
   9.516 +    by (auto intro!: nn_integral_mono simp: indicator_def max_def)
   9.517 +  finally have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) \<le> integral\<^sup>N M f"
   9.518 +    by (simp add: nn_integral_max_0)
   9.519    moreover have "0 \<le> (emeasure M) (f -` {\<infinity>} \<inter> space M)"
   9.520      by (rule emeasure_nonneg)
   9.521    ultimately show ?thesis
   9.522      using assms by (auto split: split_if_asm)
   9.523  qed
   9.524  
   9.525 -lemma positive_integral_PInf_AE:
   9.526 -  assumes "f \<in> borel_measurable M" "integral\<^sup>P M f \<noteq> \<infinity>" shows "AE x in M. f x \<noteq> \<infinity>"
   9.527 +lemma nn_integral_PInf_AE:
   9.528 +  assumes "f \<in> borel_measurable M" "integral\<^sup>N M f \<noteq> \<infinity>" shows "AE x in M. f x \<noteq> \<infinity>"
   9.529  proof (rule AE_I)
   9.530    show "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
   9.531 -    by (rule positive_integral_PInf[OF assms])
   9.532 +    by (rule nn_integral_PInf[OF assms])
   9.533    show "f -` {\<infinity>} \<inter> space M \<in> sets M"
   9.534      using assms by (auto intro: borel_measurable_vimage)
   9.535  qed auto
   9.536 @@ -1254,18 +1254,18 @@
   9.537    assumes "simple_function M f" "\<And>x. 0 \<le> f x"
   9.538    and "integral\<^sup>S M f \<noteq> \<infinity>"
   9.539    shows "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
   9.540 -proof (rule positive_integral_PInf)
   9.541 +proof (rule nn_integral_PInf)
   9.542    show "f \<in> borel_measurable M" using assms by (auto intro: borel_measurable_simple_function)
   9.543 -  show "integral\<^sup>P M f \<noteq> \<infinity>"
   9.544 -    using assms by (simp add: positive_integral_eq_simple_integral)
   9.545 +  show "integral\<^sup>N M f \<noteq> \<infinity>"
   9.546 +    using assms by (simp add: nn_integral_eq_simple_integral)
   9.547  qed
   9.548  
   9.549 -lemma positive_integral_diff:
   9.550 +lemma nn_integral_diff:
   9.551    assumes f: "f \<in> borel_measurable M"
   9.552    and g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
   9.553 -  and fin: "integral\<^sup>P M g \<noteq> \<infinity>"
   9.554 +  and fin: "integral\<^sup>N M g \<noteq> \<infinity>"
   9.555    and mono: "AE x in M. g x \<le> f x"
   9.556 -  shows "(\<integral>\<^sup>+ x. f x - g x \<partial>M) = integral\<^sup>P M f - integral\<^sup>P M g"
   9.557 +  shows "(\<integral>\<^sup>+ x. f x - g x \<partial>M) = integral\<^sup>N M f - integral\<^sup>N M g"
   9.558  proof -
   9.559    have diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M" "AE x in M. 0 \<le> f x - g x"
   9.560      using assms by (auto intro: ereal_diff_positive)
   9.561 @@ -1274,61 +1274,61 @@
   9.562        by (cases rule: ereal2_cases[of a b]) auto }
   9.563    note * = this
   9.564    then have "AE x in M. f x = f x - g x + g x"
   9.565 -    using mono positive_integral_noteq_infinite[OF g fin] assms by auto
   9.566 -  then have **: "integral\<^sup>P M f = (\<integral>\<^sup>+x. f x - g x \<partial>M) + integral\<^sup>P M g"
   9.567 -    unfolding positive_integral_add[OF diff g, symmetric]
   9.568 -    by (rule positive_integral_cong_AE)
   9.569 +    using mono nn_integral_noteq_infinite[OF g fin] assms by auto
   9.570 +  then have **: "integral\<^sup>N M f = (\<integral>\<^sup>+x. f x - g x \<partial>M) + integral\<^sup>N M g"
   9.571 +    unfolding nn_integral_add[OF diff g, symmetric]
   9.572 +    by (rule nn_integral_cong_AE)
   9.573    show ?thesis unfolding **
   9.574 -    using fin positive_integral_positive[of M g]
   9.575 -    by (cases rule: ereal2_cases[of "\<integral>\<^sup>+ x. f x - g x \<partial>M" "integral\<^sup>P M g"]) auto
   9.576 +    using fin nn_integral_nonneg[of M g]
   9.577 +    by (cases rule: ereal2_cases[of "\<integral>\<^sup>+ x. f x - g x \<partial>M" "integral\<^sup>N M g"]) auto
   9.578  qed
   9.579  
   9.580 -lemma positive_integral_suminf:
   9.581 +lemma nn_integral_suminf:
   9.582    assumes f: "\<And>i. f i \<in> borel_measurable M" "\<And>i. AE x in M. 0 \<le> f i x"
   9.583 -  shows "(\<integral>\<^sup>+ x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>P M (f i))"
   9.584 +  shows "(\<integral>\<^sup>+ x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>N M (f i))"
   9.585  proof -
   9.586    have all_pos: "AE x in M. \<forall>i. 0 \<le> f i x"
   9.587      using assms by (auto simp: AE_all_countable)
   9.588 -  have "(\<Sum>i. integral\<^sup>P M (f i)) = (SUP n. \<Sum>i<n. integral\<^sup>P M (f i))"
   9.589 -    using positive_integral_positive by (rule suminf_ereal_eq_SUP)
   9.590 +  have "(\<Sum>i. integral\<^sup>N M (f i)) = (SUP n. \<Sum>i<n. integral\<^sup>N M (f i))"
   9.591 +    using nn_integral_nonneg by (rule suminf_ereal_eq_SUP)
   9.592    also have "\<dots> = (SUP n. \<integral>\<^sup>+x. (\<Sum>i<n. f i x) \<partial>M)"
   9.593 -    unfolding positive_integral_setsum[OF f] ..
   9.594 +    unfolding nn_integral_setsum[OF f] ..
   9.595    also have "\<dots> = \<integral>\<^sup>+x. (SUP n. \<Sum>i<n. f i x) \<partial>M" using f all_pos
   9.596 -    by (intro positive_integral_monotone_convergence_SUP_AE[symmetric])
   9.597 +    by (intro nn_integral_monotone_convergence_SUP_AE[symmetric])
   9.598         (elim AE_mp, auto simp: setsum_nonneg simp del: setsum_lessThan_Suc intro!: AE_I2 setsum_mono3)
   9.599    also have "\<dots> = \<integral>\<^sup>+x. (\<Sum>i. f i x) \<partial>M" using all_pos
   9.600 -    by (intro positive_integral_cong_AE) (auto simp: suminf_ereal_eq_SUP)
   9.601 +    by (intro nn_integral_cong_AE) (auto simp: suminf_ereal_eq_SUP)
   9.602    finally show ?thesis by simp
   9.603  qed
   9.604  
   9.605 -lemma positive_integral_mult_bounded_inf:
   9.606 +lemma nn_integral_mult_bounded_inf:
   9.607    assumes f: "f \<in> borel_measurable M" "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>"
   9.608      and c: "0 \<le> c" "c \<noteq> \<infinity>" and ae: "AE x in M. g x \<le> c * f x"
   9.609    shows "(\<integral>\<^sup>+x. g x \<partial>M) < \<infinity>"
   9.610  proof -
   9.611    have "(\<integral>\<^sup>+x. g x \<partial>M) \<le> (\<integral>\<^sup>+x. c * f x \<partial>M)"
   9.612 -    by (intro positive_integral_mono_AE ae)
   9.613 +    by (intro nn_integral_mono_AE ae)
   9.614    also have "(\<integral>\<^sup>+x. c * f x \<partial>M) < \<infinity>"
   9.615 -    using c f by (subst positive_integral_cmult) auto
   9.616 +    using c f by (subst nn_integral_cmult) auto
   9.617    finally show ?thesis .
   9.618  qed
   9.619  
   9.620  text {* Fatou's lemma: convergence theorem on limes inferior *}
   9.621  
   9.622 -lemma positive_integral_liminf:
   9.623 +lemma nn_integral_liminf:
   9.624    fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   9.625    assumes u: "\<And>i. u i \<in> borel_measurable M" "\<And>i. AE x in M. 0 \<le> u i x"
   9.626 -  shows "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>P M (u n))"
   9.627 +  shows "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))"
   9.628  proof -
   9.629    have pos: "AE x in M. \<forall>i. 0 \<le> u i x" using u by (auto simp: AE_all_countable)
   9.630    have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) =
   9.631      (SUP n. \<integral>\<^sup>+ x. (INF i:{n..}. u i x) \<partial>M)"
   9.632      unfolding liminf_SUP_INF using pos u
   9.633 -    by (intro positive_integral_monotone_convergence_SUP_AE)
   9.634 +    by (intro nn_integral_monotone_convergence_SUP_AE)
   9.635         (elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_superset_mono)
   9.636 -  also have "\<dots> \<le> liminf (\<lambda>n. integral\<^sup>P M (u n))"
   9.637 +  also have "\<dots> \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))"
   9.638      unfolding liminf_SUP_INF
   9.639 -    by (auto intro!: SUP_mono exI INF_greatest positive_integral_mono INF_lower)
   9.640 +    by (auto intro!: SUP_mono exI INF_greatest nn_integral_mono INF_lower)
   9.641    finally show ?thesis .
   9.642  qed
   9.643  
   9.644 @@ -1345,11 +1345,11 @@
   9.645    shows "c - a \<le> c - b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c < \<infinity> \<Longrightarrow> b \<le> a"
   9.646    by (cases a b c rule: ereal3_cases) auto
   9.647  
   9.648 -lemma positive_integral_limsup:
   9.649 +lemma nn_integral_limsup:
   9.650    fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   9.651    assumes [measurable]: "\<And>i. u i \<in> borel_measurable M" "w \<in> borel_measurable M"
   9.652    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>"
   9.653 -  shows "limsup (\<lambda>n. integral\<^sup>P M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)"
   9.654 +  shows "limsup (\<lambda>n. integral\<^sup>N M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)"
   9.655  proof -
   9.656    have bnd: "AE x in M. \<forall>i. 0 \<le> u i x \<and> u i x \<le> w x"
   9.657      using bounds by (auto simp: AE_all_countable)
   9.658 @@ -1358,38 +1358,38 @@
   9.659      by auto
   9.660  
   9.661    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)"
   9.662 -  proof (intro positive_integral_diff[symmetric])
   9.663 +  proof (intro nn_integral_diff[symmetric])
   9.664      show "AE x in M. 0 \<le> limsup (\<lambda>n. u n x)"
   9.665        using bnd by (auto intro!: le_Limsup)
   9.666      show "AE x in M. limsup (\<lambda>n. u n x) \<le> w x"
   9.667        using bnd by (auto intro!: Limsup_le)
   9.668      then have "(\<integral>\<^sup>+x. limsup (\<lambda>n. u n x) \<partial>M) < \<infinity>"
   9.669 -      by (intro positive_integral_mult_bounded_inf[OF _ w, of 1]) auto
   9.670 +      by (intro nn_integral_mult_bounded_inf[OF _ w, of 1]) auto
   9.671      then show "(\<integral>\<^sup>+x. limsup (\<lambda>n. u n x) \<partial>M) \<noteq> \<infinity>"
   9.672        by simp
   9.673    qed auto
   9.674    also have "\<dots> = (\<integral>\<^sup>+x. liminf (\<lambda>n. w x - u n x) \<partial>M)"
   9.675      using w_nonneg
   9.676 -    by (intro positive_integral_cong_AE, eventually_elim)
   9.677 +    by (intro nn_integral_cong_AE, eventually_elim)
   9.678         (auto intro!: liminf_ereal_cminus[symmetric])
   9.679    also have "\<dots> \<le> liminf (\<lambda>n. \<integral>\<^sup>+x. w x - u n x \<partial>M)"
   9.680 -  proof (rule positive_integral_liminf)
   9.681 +  proof (rule nn_integral_liminf)
   9.682      fix i show "AE x in M. 0 \<le> w x - u i x"
   9.683        using bounds[of i] by eventually_elim (auto intro: ereal_diff_positive)
   9.684    qed simp
   9.685    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))"
   9.686 -  proof (intro ext positive_integral_diff)
   9.687 +  proof (intro ext nn_integral_diff)
   9.688      fix i have "(\<integral>\<^sup>+x. u i x \<partial>M) < \<infinity>"
   9.689 -      using bounds by (intro positive_integral_mult_bounded_inf[OF _ w, of 1]) auto
   9.690 +      using bounds by (intro nn_integral_mult_bounded_inf[OF _ w, of 1]) auto
   9.691      then show "(\<integral>\<^sup>+x. u i x \<partial>M) \<noteq> \<infinity>" by simp
   9.692    qed (insert bounds, auto)
   9.693    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)"
   9.694      using w by (intro liminf_ereal_cminus) auto
   9.695    finally show ?thesis
   9.696 -    by (rule ereal_mono_minus_cancel) (intro w positive_integral_positive)+
   9.697 +    by (rule ereal_mono_minus_cancel) (intro w nn_integral_nonneg)+
   9.698  qed
   9.699  
   9.700 -lemma positive_integral_dominated_convergence:
   9.701 +lemma nn_integral_dominated_convergence:
   9.702    assumes [measurable]:
   9.703         "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
   9.704      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"
   9.705 @@ -1397,25 +1397,25 @@
   9.706      and u': "AE x in M. (\<lambda>i. u i x) ----> u' x"
   9.707    shows "(\<lambda>i. (\<integral>\<^sup>+x. u i x \<partial>M)) ----> (\<integral>\<^sup>+x. u' x \<partial>M)"
   9.708  proof -
   9.709 -  have "limsup (\<lambda>n. integral\<^sup>P M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)"
   9.710 -    by (intro positive_integral_limsup[OF _ _ bound w]) auto
   9.711 +  have "limsup (\<lambda>n. integral\<^sup>N M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)"
   9.712 +    by (intro nn_integral_limsup[OF _ _ bound w]) auto
   9.713    moreover have "(\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M) = (\<integral>\<^sup>+ x. u' x \<partial>M)"
   9.714 -    using u' by (intro positive_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot)
   9.715 +    using u' by (intro nn_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot)
   9.716    moreover have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) = (\<integral>\<^sup>+ x. u' x \<partial>M)"
   9.717 -    using u' by (intro positive_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot)
   9.718 -  moreover have "(\<integral>\<^sup>+x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>P M (u n))"
   9.719 -    by (intro positive_integral_liminf[OF _ bound(1)]) auto
   9.720 -  moreover have "liminf (\<lambda>n. integral\<^sup>P M (u n)) \<le> limsup (\<lambda>n. integral\<^sup>P M (u n))"
   9.721 +    using u' by (intro nn_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot)
   9.722 +  moreover have "(\<integral>\<^sup>+x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))"
   9.723 +    by (intro nn_integral_liminf[OF _ bound(1)]) auto
   9.724 +  moreover have "liminf (\<lambda>n. integral\<^sup>N M (u n)) \<le> limsup (\<lambda>n. integral\<^sup>N M (u n))"
   9.725      by (intro Liminf_le_Limsup sequentially_bot)
   9.726    ultimately show ?thesis
   9.727      by (intro Liminf_eq_Limsup) auto
   9.728  qed
   9.729  
   9.730 -lemma positive_integral_null_set:
   9.731 +lemma nn_integral_null_set:
   9.732    assumes "N \<in> null_sets M" shows "(\<integral>\<^sup>+ x. u x * indicator N x \<partial>M) = 0"
   9.733  proof -
   9.734    have "(\<integral>\<^sup>+ x. u x * indicator N x \<partial>M) = (\<integral>\<^sup>+ x. 0 \<partial>M)"
   9.735 -  proof (intro positive_integral_cong_AE AE_I)
   9.736 +  proof (intro nn_integral_cong_AE AE_I)
   9.737      show "{x \<in> space M. u x * indicator N x \<noteq> 0} \<subseteq> N"
   9.738        by (auto simp: indicator_def)
   9.739      show "(emeasure M) N = 0" "N \<in> sets M"
   9.740 @@ -1424,29 +1424,29 @@
   9.741    then show ?thesis by simp
   9.742  qed
   9.743  
   9.744 -lemma positive_integral_0_iff:
   9.745 +lemma nn_integral_0_iff:
   9.746    assumes u: "u \<in> borel_measurable M" and pos: "AE x in M. 0 \<le> u x"
   9.747 -  shows "integral\<^sup>P M u = 0 \<longleftrightarrow> emeasure M {x\<in>space M. u x \<noteq> 0} = 0"
   9.748 +  shows "integral\<^sup>N M u = 0 \<longleftrightarrow> emeasure M {x\<in>space M. u x \<noteq> 0} = 0"
   9.749      (is "_ \<longleftrightarrow> (emeasure M) ?A = 0")
   9.750  proof -
   9.751 -  have u_eq: "(\<integral>\<^sup>+ x. u x * indicator ?A x \<partial>M) = integral\<^sup>P M u"
   9.752 -    by (auto intro!: positive_integral_cong simp: indicator_def)
   9.753 +  have u_eq: "(\<integral>\<^sup>+ x. u x * indicator ?A x \<partial>M) = integral\<^sup>N M u"
   9.754 +    by (auto intro!: nn_integral_cong simp: indicator_def)
   9.755    show ?thesis
   9.756    proof
   9.757      assume "(emeasure M) ?A = 0"
   9.758 -    with positive_integral_null_set[of ?A M u] u
   9.759 -    show "integral\<^sup>P M u = 0" by (simp add: u_eq null_sets_def)
   9.760 +    with nn_integral_null_set[of ?A M u] u
   9.761 +    show "integral\<^sup>N M u = 0" by (simp add: u_eq null_sets_def)
   9.762    next
   9.763      { fix r :: ereal and n :: nat assume gt_1: "1 \<le> real n * r"
   9.764        then have "0 < real n * r" by (cases r) (auto split: split_if_asm simp: one_ereal_def)
   9.765        then have "0 \<le> r" by (auto simp add: ereal_zero_less_0_iff) }
   9.766      note gt_1 = this
   9.767 -    assume *: "integral\<^sup>P M u = 0"
   9.768 +    assume *: "integral\<^sup>N M u = 0"
   9.769      let ?M = "\<lambda>n. {x \<in> space M. 1 \<le> real (n::nat) * u x}"
   9.770      have "0 = (SUP n. (emeasure M) (?M n \<inter> ?A))"
   9.771      proof -
   9.772        { fix n :: nat
   9.773 -        from positive_integral_Markov_inequality[OF u pos, of ?A "ereal (real n)"]
   9.774 +        from nn_integral_Markov_inequality[OF u pos, of ?A "ereal (real n)"]
   9.775          have "(emeasure M) (?M n \<inter> ?A) \<le> 0" unfolding u_eq * using u by simp
   9.776          moreover have "0 \<le> (emeasure M) (?M n \<inter> ?A)" using u by auto
   9.777          ultimately have "(emeasure M) (?M n \<inter> ?A) = 0" by auto }
   9.778 @@ -1489,33 +1489,33 @@
   9.779    qed
   9.780  qed
   9.781  
   9.782 -lemma positive_integral_0_iff_AE:
   9.783 +lemma nn_integral_0_iff_AE:
   9.784    assumes u: "u \<in> borel_measurable M"
   9.785 -  shows "integral\<^sup>P M u = 0 \<longleftrightarrow> (AE x in M. u x \<le> 0)"
   9.786 +  shows "integral\<^sup>N M u = 0 \<longleftrightarrow> (AE x in M. u x \<le> 0)"
   9.787  proof -
   9.788    have sets: "{x\<in>space M. max 0 (u x) \<noteq> 0} \<in> sets M"
   9.789      using u by auto
   9.790 -  from positive_integral_0_iff[of "\<lambda>x. max 0 (u x)"]
   9.791 -  have "integral\<^sup>P M u = 0 \<longleftrightarrow> (AE x in M. max 0 (u x) = 0)"
   9.792 -    unfolding positive_integral_max_0
   9.793 +  from nn_integral_0_iff[of "\<lambda>x. max 0 (u x)"]
   9.794 +  have "integral\<^sup>N M u = 0 \<longleftrightarrow> (AE x in M. max 0 (u x) = 0)"
   9.795 +    unfolding nn_integral_max_0
   9.796      using AE_iff_null[OF sets] u by auto
   9.797    also have "\<dots> \<longleftrightarrow> (AE x in M. u x \<le> 0)" by (auto split: split_max)
   9.798    finally show ?thesis .
   9.799  qed
   9.800  
   9.801 -lemma AE_iff_positive_integral: 
   9.802 -  "{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"
   9.803 -  by (subst positive_integral_0_iff_AE) (auto simp: one_ereal_def zero_ereal_def
   9.804 +lemma AE_iff_nn_integral: 
   9.805 +  "{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"
   9.806 +  by (subst nn_integral_0_iff_AE) (auto simp: one_ereal_def zero_ereal_def
   9.807      sets.sets_Collect_neg indicator_def[abs_def] measurable_If)
   9.808  
   9.809 -lemma positive_integral_const_If:
   9.810 +lemma nn_integral_const_If:
   9.811    "(\<integral>\<^sup>+x. a \<partial>M) = (if 0 \<le> a then a * (emeasure M) (space M) else 0)"
   9.812 -  by (auto intro!: positive_integral_0_iff_AE[THEN iffD2])
   9.813 +  by (auto intro!: nn_integral_0_iff_AE[THEN iffD2])
   9.814  
   9.815 -lemma positive_integral_subalgebra:
   9.816 +lemma nn_integral_subalgebra:
   9.817    assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
   9.818    and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> emeasure N A = emeasure M A"
   9.819 -  shows "integral\<^sup>P N f = integral\<^sup>P M f"
   9.820 +  shows "integral\<^sup>N N f = integral\<^sup>N M f"
   9.821  proof -
   9.822    have [simp]: "\<And>f :: 'a \<Rightarrow> ereal. f \<in> borel_measurable N \<Longrightarrow> f \<in> borel_measurable M"
   9.823      using N by (auto simp: measurable_def)
   9.824 @@ -1525,12 +1525,12 @@
   9.825      using N by auto
   9.826    from f show ?thesis
   9.827      apply induct
   9.828 -    apply (simp_all add: positive_integral_add positive_integral_cmult positive_integral_monotone_convergence_SUP N)
   9.829 -    apply (auto intro!: positive_integral_cong cong: positive_integral_cong simp: N(2)[symmetric])
   9.830 +    apply (simp_all add: nn_integral_add nn_integral_cmult nn_integral_monotone_convergence_SUP N)
   9.831 +    apply (auto intro!: nn_integral_cong cong: nn_integral_cong simp: N(2)[symmetric])
   9.832      done
   9.833  qed
   9.834  
   9.835 -lemma positive_integral_nat_function:
   9.836 +lemma nn_integral_nat_function:
   9.837    fixes f :: "'a \<Rightarrow> nat"
   9.838    assumes "f \<in> measurable M (count_space UNIV)"
   9.839    shows "(\<integral>\<^sup>+x. ereal (of_nat (f x)) \<partial>M) = (\<Sum>t. emeasure M {x\<in>space M. t < f x})"
   9.840 @@ -1549,9 +1549,9 @@
   9.841      ultimately have "ereal(of_nat(f x)) = (\<Sum>i. indicator (F i) x)"
   9.842        by (simp add: sums_iff) }
   9.843    then have "(\<integral>\<^sup>+x. ereal (of_nat (f x)) \<partial>M) = (\<integral>\<^sup>+x. (\<Sum>i. indicator (F i) x) \<partial>M)"
   9.844 -    by (simp cong: positive_integral_cong)
   9.845 +    by (simp cong: nn_integral_cong)
   9.846    also have "\<dots> = (\<Sum>i. emeasure M (F i))"
   9.847 -    by (simp add: positive_integral_suminf)
   9.848 +    by (simp add: nn_integral_suminf)
   9.849    finally show ?thesis
   9.850      by (simp add: F_def)
   9.851  qed
   9.852 @@ -1560,17 +1560,17 @@
   9.853  
   9.854  subsubsection {* Distributions *}
   9.855  
   9.856 -lemma positive_integral_distr':
   9.857 +lemma nn_integral_distr':
   9.858    assumes T: "T \<in> measurable M M'"
   9.859    and f: "f \<in> borel_measurable (distr M M' T)" "\<And>x. 0 \<le> f x"
   9.860 -  shows "integral\<^sup>P (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)"
   9.861 +  shows "integral\<^sup>N (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)"
   9.862    using f 
   9.863  proof induct
   9.864    case (cong f g)
   9.865    with T show ?case
   9.866 -    apply (subst positive_integral_cong[of _ f g])
   9.867 +    apply (subst nn_integral_cong[of _ f g])
   9.868      apply simp
   9.869 -    apply (subst positive_integral_cong[of _ "\<lambda>x. f (T x)" "\<lambda>x. g (T x)"])
   9.870 +    apply (subst nn_integral_cong[of _ "\<lambda>x. f (T x)" "\<lambda>x. g (T x)"])
   9.871      apply (simp add: measurable_def Pi_iff)
   9.872      apply simp
   9.873      done
   9.874 @@ -1579,15 +1579,15 @@
   9.875    then have eq: "\<And>x. x \<in> space M \<Longrightarrow> indicator A (T x) = indicator (T -` A \<inter> space M) x"
   9.876      by (auto simp: indicator_def)
   9.877    from set T show ?case
   9.878 -    by (subst positive_integral_cong[OF eq])
   9.879 -       (auto simp add: emeasure_distr intro!: positive_integral_indicator[symmetric] measurable_sets)
   9.880 -qed (simp_all add: measurable_compose[OF T] T positive_integral_cmult positive_integral_add
   9.881 -                   positive_integral_monotone_convergence_SUP le_fun_def incseq_def)
   9.882 +    by (subst nn_integral_cong[OF eq])
   9.883 +       (auto simp add: emeasure_distr intro!: nn_integral_indicator[symmetric] measurable_sets)
   9.884 +qed (simp_all add: measurable_compose[OF T] T nn_integral_cmult nn_integral_add
   9.885 +                   nn_integral_monotone_convergence_SUP le_fun_def incseq_def)
   9.886  
   9.887 -lemma positive_integral_distr:
   9.888 -  "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)"
   9.889 -  by (subst (1 2) positive_integral_max_0[symmetric])
   9.890 -     (simp add: positive_integral_distr')
   9.891 +lemma nn_integral_distr:
   9.892 +  "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)"
   9.893 +  by (subst (1 2) nn_integral_max_0[symmetric])
   9.894 +     (simp add: nn_integral_distr')
   9.895  
   9.896  subsubsection {* Counting space *}
   9.897  
   9.898 @@ -1595,26 +1595,26 @@
   9.899    "simple_function (count_space A) f \<longleftrightarrow> finite (f ` A)"
   9.900    unfolding simple_function_def by simp
   9.901  
   9.902 -lemma positive_integral_count_space:
   9.903 +lemma nn_integral_count_space:
   9.904    assumes A: "finite {a\<in>A. 0 < f a}"
   9.905 -  shows "integral\<^sup>P (count_space A) f = (\<Sum>a|a\<in>A \<and> 0 < f a. f a)"
   9.906 +  shows "integral\<^sup>N (count_space A) f = (\<Sum>a|a\<in>A \<and> 0 < f a. f a)"
   9.907  proof -
   9.908    have *: "(\<integral>\<^sup>+x. max 0 (f x) \<partial>count_space A) =
   9.909      (\<integral>\<^sup>+ x. (\<Sum>a|a\<in>A \<and> 0 < f a. f a * indicator {a} x) \<partial>count_space A)"
   9.910 -    by (auto intro!: positive_integral_cong
   9.911 +    by (auto intro!: nn_integral_cong
   9.912               simp add: indicator_def if_distrib setsum_cases[OF A] max_def le_less)
   9.913    also have "\<dots> = (\<Sum>a|a\<in>A \<and> 0 < f a. \<integral>\<^sup>+ x. f a * indicator {a} x \<partial>count_space A)"
   9.914 -    by (subst positive_integral_setsum)
   9.915 +    by (subst nn_integral_setsum)
   9.916         (simp_all add: AE_count_space ereal_zero_le_0_iff less_imp_le)
   9.917    also have "\<dots> = (\<Sum>a|a\<in>A \<and> 0 < f a. f a)"
   9.918 -    by (auto intro!: setsum_cong simp: positive_integral_cmult_indicator one_ereal_def[symmetric])
   9.919 -  finally show ?thesis by (simp add: positive_integral_max_0)
   9.920 +    by (auto intro!: setsum_cong simp: nn_integral_cmult_indicator one_ereal_def[symmetric])
   9.921 +  finally show ?thesis by (simp add: nn_integral_max_0)
   9.922  qed
   9.923  
   9.924 -lemma positive_integral_count_space_finite:
   9.925 +lemma nn_integral_count_space_finite:
   9.926      "finite A \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>count_space A) = (\<Sum>a\<in>A. max 0 (f a))"
   9.927 -  by (subst positive_integral_max_0[symmetric])
   9.928 -     (auto intro!: setsum_mono_zero_left simp: positive_integral_count_space less_le)
   9.929 +  by (subst nn_integral_max_0[symmetric])
   9.930 +     (auto intro!: setsum_mono_zero_left simp: nn_integral_count_space less_le)
   9.931  
   9.932  lemma emeasure_UN_countable:
   9.933    assumes sets: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" and I: "countable I" 
   9.934 @@ -1623,7 +1623,7 @@
   9.935  proof cases
   9.936    assume "finite I" with sets disj show ?thesis
   9.937      by (subst setsum_emeasure[symmetric])
   9.938 -       (auto intro!: setsum_cong simp add: max_def subset_eq positive_integral_count_space_finite emeasure_nonneg)
   9.939 +       (auto intro!: setsum_cong simp add: max_def subset_eq nn_integral_count_space_finite emeasure_nonneg)
   9.940  next
   9.941    assume f: "\<not> finite I"
   9.942    then have [intro]: "I \<noteq> {}" by auto
   9.943 @@ -1648,15 +1648,15 @@
   9.944       by (auto simp: ereal_zero_less_0_iff indicator_def from_nat_into `I \<noteq> {}` simp del: ereal_0_less_1)
   9.945      have "(\<integral>\<^sup>+ ia. emeasure M (X ia) * indicator {from_nat_into I i} ia \<partial>count_space I) =
   9.946        (if 0 < emeasure M (X (from_nat_into I i)) then emeasure M (X (from_nat_into I i)) else 0)"
   9.947 -      by (subst positive_integral_count_space) (simp_all add: eq)
   9.948 +      by (subst nn_integral_count_space) (simp_all add: eq)
   9.949      also have "\<dots> = emeasure M (X (from_nat_into I i))"
   9.950        by (simp add: less_le emeasure_nonneg)
   9.951      finally show "emeasure M (X (from_nat_into I i)) =
   9.952           \<integral>\<^sup>+ ia. emeasure M (X ia) * indicator {from_nat_into I i} ia \<partial>count_space I" ..
   9.953    qed
   9.954    also have "\<dots> = (\<integral>\<^sup>+i. emeasure M (X i) \<partial>count_space I)"
   9.955 -    apply (subst positive_integral_suminf[symmetric])
   9.956 -    apply (auto simp: emeasure_nonneg intro!: positive_integral_cong)
   9.957 +    apply (subst nn_integral_suminf[symmetric])
   9.958 +    apply (auto simp: emeasure_nonneg intro!: nn_integral_cong)
   9.959    proof -
   9.960      fix x assume "x \<in> I"
   9.961      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)"
   9.962 @@ -1670,12 +1670,12 @@
   9.963  
   9.964  subsubsection {* Measures with Restricted Space *}
   9.965  
   9.966 -lemma positive_integral_restrict_space:
   9.967 +lemma nn_integral_restrict_space:
   9.968    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"
   9.969 -  shows "positive_integral (restrict_space M \<Omega>) f = positive_integral M f"
   9.970 +  shows "nn_integral (restrict_space M \<Omega>) f = nn_integral M f"
   9.971  using f proof (induct rule: borel_measurable_induct)
   9.972    case (cong f g) then show ?case
   9.973 -    using positive_integral_cong[of M f g] positive_integral_cong[of "restrict_space M \<Omega>" f g]
   9.974 +    using nn_integral_cong[of M f g] nn_integral_cong[of "restrict_space M \<Omega>" f g]
   9.975        sets.sets_into_space[OF `\<Omega> \<in> sets M`]
   9.976      by (simp add: subset_eq space_restrict_space)
   9.977  next
   9.978 @@ -1683,19 +1683,19 @@
   9.979    then have "A \<subseteq> \<Omega>"
   9.980      unfolding indicator_eq_0_iff by (auto dest: sets.sets_into_space)
   9.981    with set `\<Omega> \<in> sets M` sets.sets_into_space[OF `\<Omega> \<in> sets M`] show ?case
   9.982 -    by (subst positive_integral_indicator')
   9.983 +    by (subst nn_integral_indicator')
   9.984         (auto simp add: sets_restrict_space_iff space_restrict_space
   9.985                    emeasure_restrict_space Int_absorb2
   9.986                  dest: sets.sets_into_space)
   9.987  next
   9.988    case (mult f c) then show ?case
   9.989 -    by (cases "c = 0") (simp_all add: measurable_restrict_space1 \<Omega> positive_integral_cmult)
   9.990 +    by (cases "c = 0") (simp_all add: measurable_restrict_space1 \<Omega> nn_integral_cmult)
   9.991  next
   9.992    case (add f g) then show ?case
   9.993 -    by (simp add: measurable_restrict_space1 \<Omega> positive_integral_add ereal_add_nonneg_eq_0_iff)
   9.994 +    by (simp add: measurable_restrict_space1 \<Omega> nn_integral_add ereal_add_nonneg_eq_0_iff)
   9.995  next
   9.996    case (seq F) then show ?case
   9.997 -    by (auto simp add: SUP_eq_iff measurable_restrict_space1 \<Omega> positive_integral_monotone_convergence_SUP)
   9.998 +    by (auto simp add: SUP_eq_iff measurable_restrict_space1 \<Omega> nn_integral_monotone_convergence_SUP)
   9.999  qed
  9.1000  
  9.1001  subsubsection {* Measure spaces with an associated density *}
  9.1002 @@ -1720,14 +1720,14 @@
  9.1003  
  9.1004  lemma density_cong: "f \<in> borel_measurable M \<Longrightarrow> f' \<in> borel_measurable M \<Longrightarrow>
  9.1005    (AE x in M. f x = f' x) \<Longrightarrow> density M f = density M f'"
  9.1006 -  unfolding density_def by (auto intro!: measure_of_eq positive_integral_cong_AE sets.space_closed)
  9.1007 +  unfolding density_def by (auto intro!: measure_of_eq nn_integral_cong_AE sets.space_closed)
  9.1008  
  9.1009  lemma density_max_0: "density M f = density M (\<lambda>x. max 0 (f x))"
  9.1010  proof -
  9.1011    have "\<And>x A. max 0 (f x) * indicator A x = max 0 (f x * indicator A x)"
  9.1012      by (auto simp: indicator_def)
  9.1013    then show ?thesis
  9.1014 -    unfolding density_def by (simp add: positive_integral_max_0)
  9.1015 +    unfolding density_def by (simp add: nn_integral_max_0)
  9.1016  qed
  9.1017  
  9.1018  lemma density_ereal_max_0: "density M (\<lambda>x. ereal (f x)) = density M (\<lambda>x. ereal (max 0 (f x)))"
  9.1019 @@ -1741,10 +1741,10 @@
  9.1020  proof (rule emeasure_measure_of_sigma)
  9.1021    show "sigma_algebra (space M) (sets M)" ..
  9.1022    show "positive (sets M) ?\<mu>"
  9.1023 -    using f by (auto simp: positive_def intro!: positive_integral_positive)
  9.1024 +    using f by (auto simp: positive_def intro!: nn_integral_nonneg)
  9.1025    have \<mu>_eq: "?\<mu> = (\<lambda>A. \<integral>\<^sup>+ x. max 0 (f x) * indicator A x \<partial>M)" (is "?\<mu> = ?\<mu>'")
  9.1026 -    apply (subst positive_integral_max_0[symmetric])
  9.1027 -    apply (intro ext positive_integral_cong_AE AE_I2)
  9.1028 +    apply (subst nn_integral_max_0[symmetric])
  9.1029 +    apply (intro ext nn_integral_cong_AE AE_I2)
  9.1030      apply (auto simp: indicator_def)
  9.1031      done
  9.1032    show "countably_additive (sets M) ?\<mu>"
  9.1033 @@ -1756,9 +1756,9 @@
  9.1034        by (auto simp: set_eq_iff)
  9.1035      assume disj: "disjoint_family A"
  9.1036      have "(\<Sum>n. ?\<mu>' (A n)) = (\<integral>\<^sup>+ x. (\<Sum>n. max 0 (f x) * indicator (A n) x) \<partial>M)"
  9.1037 -      using f * by (simp add: positive_integral_suminf)
  9.1038 +      using f * by (simp add: nn_integral_suminf)
  9.1039      also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) * (\<Sum>n. indicator (A n) x) \<partial>M)" using f
  9.1040 -      by (auto intro!: suminf_cmult_ereal positive_integral_cong_AE)
  9.1041 +      by (auto intro!: suminf_cmult_ereal nn_integral_cong_AE)
  9.1042      also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) * indicator (\<Union>n. A n) x \<partial>M)"
  9.1043        unfolding suminf_indicator[OF disj] ..
  9.1044      finally show "(\<Sum>n. ?\<mu>' (A n)) = ?\<mu>' (\<Union>x. A x)" by simp
  9.1045 @@ -1771,15 +1771,15 @@
  9.1046  proof -
  9.1047    { assume "A \<in> sets M"
  9.1048      have eq: "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^sup>+x. max 0 (f x) * indicator A x \<partial>M)"
  9.1049 -      apply (subst positive_integral_max_0[symmetric])
  9.1050 -      apply (intro positive_integral_cong)
  9.1051 +      apply (subst nn_integral_max_0[symmetric])
  9.1052 +      apply (intro nn_integral_cong)
  9.1053        apply (auto simp: indicator_def)
  9.1054        done
  9.1055      have "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = 0 \<longleftrightarrow> 
  9.1056        emeasure M {x \<in> space M. max 0 (f x) * indicator A x \<noteq> 0} = 0"
  9.1057        unfolding eq
  9.1058        using f `A \<in> sets M`
  9.1059 -      by (intro positive_integral_0_iff) auto
  9.1060 +      by (intro nn_integral_0_iff) auto
  9.1061      also have "\<dots> \<longleftrightarrow> (AE x in M. max 0 (f x) * indicator A x = 0)"
  9.1062        using f `A \<in> sets M`
  9.1063        by (intro AE_iff_measurable[OF _ refl, symmetric]) auto
  9.1064 @@ -1814,15 +1814,15 @@
  9.1065         (auto elim: eventually_elim2)
  9.1066  qed
  9.1067  
  9.1068 -lemma positive_integral_density':
  9.1069 +lemma nn_integral_density':
  9.1070    assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
  9.1071    assumes g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x"
  9.1072 -  shows "integral\<^sup>P (density M f) g = (\<integral>\<^sup>+ x. f x * g x \<partial>M)"
  9.1073 +  shows "integral\<^sup>N (density M f) g = (\<integral>\<^sup>+ x. f x * g x \<partial>M)"
  9.1074  using g proof induct
  9.1075    case (cong u v)
  9.1076    then show ?case
  9.1077 -    apply (subst positive_integral_cong[OF cong(3)])
  9.1078 -    apply (simp_all cong: positive_integral_cong)
  9.1079 +    apply (subst nn_integral_cong[OF cong(3)])
  9.1080 +    apply (simp_all cong: nn_integral_cong)
  9.1081      done
  9.1082  next
  9.1083    case (set A) then show ?case
  9.1084 @@ -1831,31 +1831,31 @@
  9.1085    case (mult u c)
  9.1086    moreover have "\<And>x. f x * (c * u x) = c * (f x * u x)" by (simp add: field_simps)
  9.1087    ultimately show ?case
  9.1088 -    using f by (simp add: positive_integral_cmult)
  9.1089 +    using f by (simp add: nn_integral_cmult)
  9.1090  next
  9.1091    case (add u v)
  9.1092    then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x"
  9.1093      by (simp add: ereal_right_distrib)
  9.1094    with add f show ?case
  9.1095 -    by (auto simp add: positive_integral_add ereal_zero_le_0_iff intro!: positive_integral_add[symmetric])
  9.1096 +    by (auto simp add: nn_integral_add ereal_zero_le_0_iff intro!: nn_integral_add[symmetric])
  9.1097  next
  9.1098    case (seq U)
  9.1099    from f(2) have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)"
  9.1100      by eventually_elim (simp add: SUP_ereal_cmult seq)
  9.1101    from seq f show ?case
  9.1102 -    apply (simp add: positive_integral_monotone_convergence_SUP)
  9.1103 -    apply (subst positive_integral_cong_AE[OF eq])
  9.1104 -    apply (subst positive_integral_monotone_convergence_SUP_AE)
  9.1105 +    apply (simp add: nn_integral_monotone_convergence_SUP)
  9.1106 +    apply (subst nn_integral_cong_AE[OF eq])
  9.1107 +    apply (subst nn_integral_monotone_convergence_SUP_AE)
  9.1108      apply (auto simp: incseq_def le_fun_def intro!: ereal_mult_left_mono)
  9.1109      done
  9.1110  qed
  9.1111  
  9.1112 -lemma positive_integral_density:
  9.1113 +lemma nn_integral_density:
  9.1114    "f \<in> borel_measurable M \<Longrightarrow> AE x in M. 0 \<le> f x \<Longrightarrow> g' \<in> borel_measurable M \<Longrightarrow> 
  9.1115 -    integral\<^sup>P (density M f) g' = (\<integral>\<^sup>+ x. f x * g' x \<partial>M)"
  9.1116 -  by (subst (1 2) positive_integral_max_0[symmetric])
  9.1117 -     (auto intro!: positive_integral_cong_AE
  9.1118 -           simp: measurable_If max_def ereal_zero_le_0_iff positive_integral_density')
  9.1119 +    integral\<^sup>N (density M f) g' = (\<integral>\<^sup>+ x. f x * g' x \<partial>M)"
  9.1120 +  by (subst (1 2) nn_integral_max_0[symmetric])
  9.1121 +     (auto intro!: nn_integral_cong_AE
  9.1122 +           simp: measurable_If max_def ereal_zero_le_0_iff nn_integral_density')
  9.1123  
  9.1124  lemma emeasure_restricted:
  9.1125    assumes S: "S \<in> sets M" and X: "X \<in> sets M"
  9.1126 @@ -1864,7 +1864,7 @@
  9.1127    have "emeasure (density M (indicator S)) X = (\<integral>\<^sup>+x. indicator S x * indicator X x \<partial>M)"
  9.1128      using S X by (simp add: emeasure_density)
  9.1129    also have "\<dots> = (\<integral>\<^sup>+x. indicator (S \<inter> X) x \<partial>M)"
  9.1130 -    by (auto intro!: positive_integral_cong simp: indicator_def)
  9.1131 +    by (auto intro!: nn_integral_cong simp: indicator_def)
  9.1132    also have "\<dots> = emeasure M (S \<inter> X)"
  9.1133      using S X by (simp add: sets.Int)
  9.1134    finally show ?thesis .
  9.1135 @@ -1880,7 +1880,7 @@
  9.1136  
  9.1137  lemma emeasure_density_const:
  9.1138    "A \<in> sets M \<Longrightarrow> 0 \<le> c \<Longrightarrow> emeasure (density M (\<lambda>_. c)) A = c * emeasure M A"
  9.1139 -  by (auto simp: positive_integral_cmult_indicator emeasure_density)
  9.1140 +  by (auto simp: nn_integral_cmult_indicator emeasure_density)
  9.1141  
  9.1142  lemma measure_density_const:
  9.1143    "A \<in> sets M \<Longrightarrow> 0 < c \<Longrightarrow> c \<noteq> \<infinity> \<Longrightarrow> measure (density M (\<lambda>_. c)) A = real c * measure M A"
  9.1144 @@ -1889,7 +1889,7 @@
  9.1145  lemma density_density_eq:
  9.1146     "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. 0 \<le> f x \<Longrightarrow>
  9.1147     density (density M f) g = density M (\<lambda>x. f x * g x)"
  9.1148 -  by (auto intro!: measure_eqI simp: emeasure_density positive_integral_density ac_simps)
  9.1149 +  by (auto intro!: measure_eqI simp: emeasure_density nn_integral_density ac_simps)
  9.1150  
  9.1151  lemma distr_density_distr:
  9.1152    assumes T: "T \<in> measurable M M'" and T': "T' \<in> measurable M' M"
  9.1153 @@ -1904,7 +1904,7 @@
  9.1154        using T inv by (auto simp: indicator_def measurable_space) }
  9.1155    with A T T' f show "emeasure ?R A = emeasure ?L A"
  9.1156      by (simp add: measurable_comp emeasure_density emeasure_distr
  9.1157 -                  positive_integral_distr measurable_sets cong: positive_integral_cong)
  9.1158 +                  nn_integral_distr measurable_sets cong: nn_integral_cong)
  9.1159  qed simp
  9.1160  
  9.1161  lemma density_density_divide:
  9.1162 @@ -1951,7 +1951,7 @@
  9.1163    have "{a. (a \<in> X \<longrightarrow> a \<in> A \<and> 0 < f a) \<and> a \<in> X} = {a\<in>X. 0 < f a}"
  9.1164      using `X \<subseteq> A` by auto
  9.1165    with A show ?thesis
  9.1166 -    by (simp add: emeasure_density positive_integral_count_space ereal_zero_le_0_iff
  9.1167 +    by (simp add: emeasure_density nn_integral_count_space ereal_zero_le_0_iff
  9.1168                    point_measure_def indicator_def)
  9.1169  qed
  9.1170  
  9.1171 @@ -1973,14 +1973,14 @@
  9.1172    unfolding point_measure_def
  9.1173    by (subst AE_density) (auto simp: AE_density AE_count_space point_measure_def)
  9.1174  
  9.1175 -lemma positive_integral_point_measure:
  9.1176 +lemma nn_integral_point_measure:
  9.1177    "finite {a\<in>A. 0 < f a \<and> 0 < g a} \<Longrightarrow>
  9.1178 -    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)"
  9.1179 +    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)"
  9.1180    unfolding point_measure_def
  9.1181    apply (subst density_max_0)
  9.1182 -  apply (subst positive_integral_density)
  9.1183 -  apply (simp_all add: AE_count_space positive_integral_density)
  9.1184 -  apply (subst positive_integral_count_space )
  9.1185 +  apply (subst nn_integral_density)
  9.1186 +  apply (simp_all add: AE_count_space nn_integral_density)
  9.1187 +  apply (subst nn_integral_count_space )
  9.1188    apply (auto intro!: setsum_cong simp: max_def ereal_zero_less_0_iff)
  9.1189    apply (rule finite_subset)
  9.1190    prefer 2
  9.1191 @@ -1988,10 +1988,10 @@
  9.1192    apply auto
  9.1193    done
  9.1194  
  9.1195 -lemma positive_integral_point_measure_finite:
  9.1196 +lemma nn_integral_point_measure_finite:
  9.1197    "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>
  9.1198 -    integral\<^sup>P (point_measure A f) g = (\<Sum>a\<in>A. f a * g a)"
  9.1199 -  by (subst positive_integral_point_measure) (auto intro!: setsum_mono_zero_left simp: less_le)
  9.1200 +    integral\<^sup>N (point_measure A f) g = (\<Sum>a\<in>A. f a * g a)"
  9.1201 +  by (subst nn_integral_point_measure) (auto intro!: setsum_mono_zero_left simp: less_le)
  9.1202  
  9.1203  subsubsection {* Uniform measure *}
  9.1204  
  9.1205 @@ -2008,10 +2008,10 @@
  9.1206  proof -
  9.1207    from A B have "emeasure (uniform_measure M A) B = (\<integral>\<^sup>+x. (1 / emeasure M A) * indicator (A \<inter> B) x \<partial>M)"
  9.1208      by (auto simp add: uniform_measure_def emeasure_density split: split_indicator
  9.1209 -             intro!: positive_integral_cong)
  9.1210 +             intro!: nn_integral_cong)
  9.1211    also have "\<dots> = emeasure M (A \<inter> B) / emeasure M A"
  9.1212      using A B
  9.1213 -    by (subst positive_integral_cmult_indicator) (simp_all add: sets.Int emeasure_nonneg)
  9.1214 +    by (subst nn_integral_cmult_indicator) (simp_all add: sets.Int emeasure_nonneg)
  9.1215    finally show ?thesis .
  9.1216  qed
  9.1217  
    10.1 --- a/src/HOL/Probability/Probability_Measure.thy	Mon May 19 13:53:58 2014 +0200
    10.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Mon May 19 14:26:58 2014 +0200
    10.3 @@ -290,7 +290,7 @@
    10.4               simp: disjoint_family_on_def)
    10.5    also have "\<dots> = (\<integral>\<^sup>+i. \<P>(x in M. P i x) \<partial>count_space I)"
    10.6      unfolding emeasure_eq_measure using disj
    10.7 -    by (intro positive_integral_cong ereal.inject[THEN iffD2] prob_eq_AE)
    10.8 +    by (intro nn_integral_cong ereal.inject[THEN iffD2] prob_eq_AE)
    10.9         (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+
   10.10    finally show ?thesis .
   10.11  qed
   10.12 @@ -402,9 +402,9 @@
   10.13    also have "\<dots> = emeasure (density (count_space A) P) {a}"
   10.14      using X by (simp add: distributed_distr_eq_density)
   10.15    also have "\<dots> = (\<integral>\<^sup>+x. P a * indicator {a} x \<partial>count_space A)"
   10.16 -    using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: positive_integral_cong)
   10.17 +    using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: nn_integral_cong)
   10.18    also have "\<dots> = P a"
   10.19 -    using X a by (subst positive_integral_cmult_indicator) (auto simp: distributed_def one_ereal_def[symmetric] AE_count_space)
   10.20 +    using X a by (subst nn_integral_cmult_indicator) (auto simp: distributed_def one_ereal_def[symmetric] AE_count_space)
   10.21    finally show ?thesis ..
   10.22  qed
   10.23  
   10.24 @@ -446,10 +446,10 @@
   10.25    by (auto simp: distributed_AE
   10.26                   distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr)
   10.27  
   10.28 -lemma distributed_positive_integral:
   10.29 +lemma distributed_nn_integral:
   10.30    "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)"
   10.31    by (auto simp: distributed_AE
   10.32 -                 distributed_distr_eq_density[symmetric] positive_integral_density[symmetric] positive_integral_distr)
   10.33 +                 distributed_distr_eq_density[symmetric] nn_integral_density[symmetric] nn_integral_distr)
   10.34  
   10.35  lemma distributed_integral:
   10.36    "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)"
   10.37 @@ -520,10 +520,10 @@
   10.38      have "emeasure ?L E = emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B}"
   10.39        by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair)
   10.40      also have "\<dots> = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)"
   10.41 -      using f by (auto simp add: eq positive_integral_multc intro!: positive_integral_cong)
   10.42 +      using f by (auto simp add: eq nn_integral_multc intro!: nn_integral_cong)
   10.43      also have "\<dots> = emeasure ?R E"
   10.44 -      by (auto simp add: emeasure_density T.positive_integral_fst[symmetric]
   10.45 -               intro!: positive_integral_cong split: split_indicator)
   10.46 +      by (auto simp add: emeasure_density T.nn_integral_fst[symmetric]
   10.47 +               intro!: nn_integral_cong split: split_indicator)
   10.48      finally show "emeasure ?L E = emeasure ?R E" .
   10.49    qed
   10.50  qed (auto simp: f)
   10.51 @@ -564,12 +564,12 @@
   10.52          using Pxy A by (intro distributed_emeasure) auto
   10.53        finally have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
   10.54          (\<integral>\<^sup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^sub>M T))"
   10.55 -        by (auto intro!: positive_integral_cong split: split_indicator) }
   10.56 +        by (auto intro!: nn_integral_cong split: split_indicator) }
   10.57      note * = this
   10.58      show "distr M ?D (\<lambda>x. (Y x, X x)) = density ?D (\<lambda>(x, y). Pxy (y, x))"
   10.59        apply (intro measure_eqI)
   10.60        apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1])
   10.61 -      apply (subst positive_integral_distr)
   10.62 +      apply (subst nn_integral_distr)
   10.63        apply (auto intro!: * simp: comp_def split_beta)
   10.64        done
   10.65    qed
   10.66 @@ -590,13 +590,13 @@
   10.67    show X: "X \<in> measurable M S" by simp
   10.68  
   10.69    show borel: "Px \<in> borel_measurable S"
   10.70 -    by (auto intro!: T.positive_integral_fst simp: Px_def)
   10.71 +    by (auto intro!: T.nn_integral_fst simp: Px_def)
   10.72  
   10.73    interpret Pxy: prob_space "distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))"
   10.74      by (intro prob_space_distr) simp
   10.75    have "(\<integral>\<^sup>+ x. max 0 (- Pxy x) \<partial>(S \<Otimes>\<^sub>M T)) = (\<integral>\<^sup>+ x. 0 \<partial>(S \<Otimes>\<^sub>M T))"
   10.76      using Pxy
   10.77 -    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_AE)
   10.78 +    by (intro nn_integral_cong_AE) (auto simp: max_def dest: distributed_AE)
   10.79  
   10.80    show "distr M S X = density S Px"
   10.81    proof (rule measure_eqI)
   10.82 @@ -608,18 +608,18 @@
   10.83        using Pxy by (simp add: distributed_def)
   10.84      also have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
   10.85        using A borel Pxy
   10.86 -      by (simp add: emeasure_density T.positive_integral_fst[symmetric])
   10.87 +      by (simp add: emeasure_density T.nn_integral_fst[symmetric])
   10.88      also have "\<dots> = \<integral>\<^sup>+ x. Px x * indicator A x \<partial>S"
   10.89 -      apply (rule positive_integral_cong_AE)
   10.90 +      apply (rule nn_integral_cong_AE)
   10.91        using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space
   10.92      proof eventually_elim
   10.93        fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)"
   10.94        moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x"
   10.95          by (auto simp: indicator_def)
   10.96        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"
   10.97 -        by (simp add: eq positive_integral_multc cong: positive_integral_cong)
   10.98 +        by (simp add: eq nn_integral_multc cong: nn_integral_cong)
   10.99        also have "(\<integral>\<^sup>+ y. Pxy (x, y) \<partial>T) = Px x"
  10.100 -        by (simp add: Px_def ereal_real positive_integral_positive)
  10.101 +        by (simp add: Px_def ereal_real nn_integral_nonneg)
  10.102        finally show "(\<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" .
  10.103      qed
  10.104      finally show "emeasure (distr M S X) A = emeasure (density S Px) A"
  10.105 @@ -627,7 +627,7 @@
  10.106    qed simp
  10.107    
  10.108    show "AE x in S. 0 \<le> Px x"
  10.109 -    by (simp add: Px_def positive_integral_positive real_of_ereal_pos)
  10.110 +    by (simp add: Px_def nn_integral_nonneg real_of_ereal_pos)
  10.111  qed
  10.112  
  10.113  lemma (in prob_space) distr_marginal2:
  10.114 @@ -727,10 +727,10 @@
  10.115                 intro!: arg_cong[where f=prob])
  10.116      also have "\<dots> = (\<integral>\<^sup>+x. ereal (P' a) * indicator {a} x \<partial>S)"
  10.117        using A X a
  10.118 -      by (subst positive_integral_cmult_indicator)
  10.119 +      by (subst nn_integral_cmult_indicator)
  10.120           (auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg)
  10.121      also have "\<dots> = (\<integral>\<^sup>+x. ereal (P' x) * indicator {a} x \<partial>S)"
  10.122 -      by (auto simp: indicator_def intro!: positive_integral_cong)
  10.123 +      by (auto simp: indicator_def intro!: nn_integral_cong)
  10.124      also have "\<dots> = emeasure (density S P') {a}"
  10.125        using a A by (intro emeasure_density[symmetric]) (auto simp: S_def)
  10.126      finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" .
  10.127 @@ -866,7 +866,7 @@
  10.128      Pxy[THEN simple_distributed, THEN distributed_real_AE]
  10.129    show ?thesis
  10.130      unfolding AE_count_space
  10.131 -    apply (auto simp add: positive_integral_count_space_finite * intro!: setsum_cong split: split_max)
  10.132 +    apply (auto simp add: nn_integral_count_space_finite * intro!: setsum_cong split: split_max)
  10.133      done
  10.134  qed
  10.135  
    11.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Mon May 19 13:53:58 2014 +0200
    11.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon May 19 14:26:58 2014 +0200
    11.3 @@ -44,7 +44,7 @@
    11.4  qed fact
    11.5  
    11.6  lemma (in sigma_finite_measure) Ex_finite_integrable_function:
    11.7 -  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)"
    11.8 +  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)"
    11.9  proof -
   11.10    obtain A :: "nat \<Rightarrow> 'a set" where
   11.11      range[measurable]: "range A \<subseteq> sets M" and
   11.12 @@ -67,8 +67,8 @@
   11.13    proof (safe intro!: bexI[of _ ?h] del: notI)
   11.14      have "\<And>i. A i \<in> sets M"
   11.15        using range by fastforce+
   11.16 -    then have "integral\<^sup>P M ?h = (\<Sum>i. n i * emeasure M (A i))" using pos
   11.17 -      by (simp add: positive_integral_suminf positive_integral_cmult_indicator)
   11.18 +    then have "integral\<^sup>N M ?h = (\<Sum>i. n i * emeasure M (A i))" using pos
   11.19 +      by (simp add: nn_integral_suminf nn_integral_cmult_indicator)
   11.20      also have "\<dots> \<le> (\<Sum>i. (1 / 2)^Suc i)"
   11.21      proof (rule suminf_le_pos)
   11.22        fix N
   11.23 @@ -82,7 +82,7 @@
   11.24        finally show "n N * emeasure M (A N) \<le> (1 / 2) ^ Suc N" .
   11.25        show "0 \<le> n N * emeasure M (A N)" using n[of N] `A N \<in> sets M` by (simp add: emeasure_nonneg)
   11.26      qed
   11.27 -    finally show "integral\<^sup>P M ?h \<noteq> \<infinity>" unfolding suminf_half_series_ereal by auto
   11.28 +    finally show "integral\<^sup>N M ?h \<noteq> \<infinity>" unfolding suminf_half_series_ereal by auto
   11.29    next
   11.30      { fix x assume "x \<in> space M"
   11.31        then obtain i where "x \<in> A i" using space[symmetric] by auto
   11.32 @@ -317,7 +317,7 @@
   11.33          (\<integral>\<^sup>+x. g x * indicator (?A \<inter> A) x \<partial>M) +
   11.34          (\<integral>\<^sup>+x. f x * indicator ((space M - ?A) \<inter> A) x \<partial>M)"
   11.35          using f g sets unfolding G_def
   11.36 -        by (auto cong: positive_integral_cong intro!: positive_integral_add)
   11.37 +        by (auto cong: nn_integral_cong intro!: nn_integral_add)
   11.38        also have "\<dots> \<le> N (?A \<inter> A) + N ((space M - ?A) \<inter> A)"
   11.39          using f g sets unfolding G_def by (auto intro!: add_mono)
   11.40        also have "\<dots> = N A"
   11.41 @@ -338,31 +338,31 @@
   11.42        fix A assume "A \<in> sets M"
   11.43        have "(\<integral>\<^sup>+x. (SUP i. f i x) * indicator A x \<partial>M) =
   11.44          (\<integral>\<^sup>+x. (SUP i. f i x * indicator A x) \<partial>M)"
   11.45 -        by (intro positive_integral_cong) (simp split: split_indicator)
   11.46 +        by (intro nn_integral_cong) (simp split: split_indicator)
   11.47        also have "\<dots> = (SUP i. (\<integral>\<^sup>+x. f i x * indicator A x \<partial>M))"
   11.48          using `incseq f` f `A \<in> sets M`
   11.49 -        by (intro positive_integral_monotone_convergence_SUP)
   11.50 +        by (intro nn_integral_monotone_convergence_SUP)
   11.51             (auto simp: G_def incseq_Suc_iff le_fun_def split: split_indicator)
   11.52        finally show "(\<integral>\<^sup>+x. (SUP i. f i x) * indicator A x \<partial>M) \<le> N A"
   11.53          using f `A \<in> sets M` by (auto intro!: SUP_least simp: G_def)
   11.54      qed }
   11.55    note SUP_in_G = this
   11.56 -  let ?y = "SUP g : G. integral\<^sup>P M g"
   11.57 +  let ?y = "SUP g : G. integral\<^sup>N M g"
   11.58    have y_le: "?y \<le> N (space M)" unfolding G_def
   11.59    proof (safe intro!: SUP_least)
   11.60      fix g assume "\<forall>A\<in>sets M. (\<integral>\<^sup>+x. g x * indicator A x \<partial>M) \<le> N A"
   11.61 -    from this[THEN bspec, OF sets.top] show "integral\<^sup>P M g \<le> N (space M)"
   11.62 -      by (simp cong: positive_integral_cong)
   11.63 +    from this[THEN bspec, OF sets.top] show "integral\<^sup>N M g \<le> N (space M)"
   11.64 +      by (simp cong: nn_integral_cong)
   11.65    qed
   11.66 -  from SUP_countable_SUP [OF `G \<noteq> {}`, of "integral\<^sup>P M"] guess ys .. note ys = this
   11.67 -  then have "\<forall>n. \<exists>g. g\<in>G \<and> integral\<^sup>P M g = ys n"
   11.68 +  from SUP_countable_SUP [OF `G \<noteq> {}`, of "integral\<^sup>N M"] guess ys .. note ys = this
   11.69 +  then have "\<forall>n. \<exists>g. g\<in>G \<and> integral\<^sup>N M g = ys n"
   11.70    proof safe
   11.71 -    fix n assume "range ys \<subseteq> integral\<^sup>P M ` G"
   11.72 -    hence "ys n \<in> integral\<^sup>P M ` G" by auto
   11.73 -    thus "\<exists>g. g\<in>G \<and> integral\<^sup>P M g = ys n" by auto
   11.74 +    fix n assume "range ys \<subseteq> integral\<^sup>N M ` G"
   11.75 +    hence "ys n \<in> integral\<^sup>N M ` G" by auto
   11.76 +    thus "\<exists>g. g\<in>G \<and> integral\<^sup>N M g = ys n" by auto
   11.77    qed
   11.78 -  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
   11.79 -  hence y_eq: "?y = (SUP i. integral\<^sup>P M (gs i))" using ys by auto
   11.80 +  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
   11.81 +  hence y_eq: "?y = (SUP i. integral\<^sup>N M (gs i))" using ys by auto
   11.82    let ?g = "\<lambda>i x. Max ((\<lambda>n. gs n x) ` {..i})"
   11.83    def f \<equiv> "\<lambda>x. SUP i. ?g i x"
   11.84    let ?F = "\<lambda>A x. f x * indicator A x"
   11.85 @@ -380,17 +380,17 @@
   11.86      by (auto intro!: incseq_SucI le_funI simp add: atMost_Suc)
   11.87    from SUP_in_G[OF this g_in_G] have [measurable]: "f \<in> G" unfolding f_def .
   11.88    then have [simp, intro]: "f \<in> borel_measurable M" unfolding G_def by auto
   11.89 -  have "integral\<^sup>P M f = (SUP i. integral\<^sup>P M (?g i))" unfolding f_def
   11.90 +  have "integral\<^sup>N M f = (SUP i. integral\<^sup>N M (?g i))" unfolding f_def
   11.91      using g_in_G `incseq ?g`
   11.92 -    by (auto intro!: positive_integral_monotone_convergence_SUP simp: G_def)
   11.93 +    by (auto intro!: nn_integral_monotone_convergence_SUP simp: G_def)
   11.94    also have "\<dots> = ?y"
   11.95    proof (rule antisym)
   11.96 -    show "(SUP i. integral\<^sup>P M (?g i)) \<le> ?y"
   11.97 +    show "(SUP i. integral\<^sup>N M (?g i)) \<le> ?y"
   11.98        using g_in_G by (auto intro: SUP_mono)
   11.99 -    show "?y \<le> (SUP i. integral\<^sup>P M (?g i))" unfolding y_eq
  11.100 -      by (auto intro!: SUP_mono positive_integral_mono Max_ge)
  11.101 +    show "?y \<le> (SUP i. integral\<^sup>N M (?g i))" unfolding y_eq
  11.102 +      by (auto intro!: SUP_mono nn_integral_mono Max_ge)
  11.103    qed
  11.104 -  finally have int_f_eq_y: "integral\<^sup>P M f = ?y" .
  11.105 +  finally have int_f_eq_y: "integral\<^sup>N M f = ?y" .
  11.106    have "\<And>x. 0 \<le> f x"
  11.107      unfolding f_def using `\<And>i. gs i \<in> G`
  11.108      by (auto intro!: SUP_upper2 Max_ge_iff[THEN iffD2] simp: G_def)
  11.109 @@ -401,12 +401,12 @@
  11.110    have emeasure_M: "\<And>A. A \<in> sets M \<Longrightarrow> emeasure ?M A = ?t A"
  11.111    proof (subst emeasure_diff_measure)
  11.112      from f_le_N[of "space M"] show "finite_measure N" "finite_measure (density M f)"
  11.113 -      by (auto intro!: finite_measureI simp: emeasure_density cong: positive_integral_cong)
  11.114 +      by (auto intro!: finite_measureI simp: emeasure_density cong: nn_integral_cong)
  11.115    next
  11.116      fix B assume "B \<in> sets N" with f_le_N[of B] show "emeasure (density M f) B \<le> emeasure N B"
  11.117 -      by (auto simp: sets_eq emeasure_density cong: positive_integral_cong)
  11.118 +      by (auto simp: sets_eq emeasure_density cong: nn_integral_cong)
  11.119    qed (auto simp: sets_eq emeasure_density)
  11.120 -  from emeasure_M[of "space M"] N.finite_emeasure_space positive_integral_positive[of M "?F (space M)"]
  11.121 +  from emeasure_M[of "space M"] N.finite_emeasure_space nn_integral_nonneg[of M "?F (space M)"]
  11.122    interpret M': finite_measure ?M
  11.123      by (auto intro!: finite_measureI simp: sets_eq_imp_space_eq[OF sets_eq] N.emeasure_eq_measure ereal_minus_eq_PInfty_iff)
  11.124  
  11.125 @@ -417,7 +417,7 @@
  11.126        unfolding absolutely_continuous_def by auto
  11.127      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)
  11.128      ultimately have "N A - (\<integral>\<^sup>+ x. ?F A x \<partial>M) = 0"
  11.129 -      using positive_integral_positive[of M] by (auto intro!: antisym)
  11.130 +      using nn_integral_nonneg[of M] by (auto intro!: antisym)
  11.131      then show "A \<in> null_sets ?M"
  11.132        using A_M by (simp add: emeasure_M null_sets_def sets_eq)
  11.133    qed
  11.134 @@ -462,11 +462,11 @@
  11.135        hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
  11.136        have "(\<integral>\<^sup>+x. ?f0 x  * indicator A x \<partial>M) =
  11.137          (\<integral>\<^sup>+x. f x * indicator A x + b * indicator (A \<inter> A0) x \<partial>M)"
  11.138 -        by (auto intro!: positive_integral_cong split: split_indicator)
  11.139 +        by (auto intro!: nn_integral_cong split: split_indicator)
  11.140        hence "(\<integral>\<^sup>+x. ?f0 x * indicator A x \<partial>M) =
  11.141            (\<integral>\<^sup>+x. f x * indicator A x \<partial>M) + b * emeasure M (A \<inter> A0)"
  11.142          using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A b `f \<in> G`
  11.143 -        by (simp add: positive_integral_add positive_integral_cmult_indicator G_def) }
  11.144 +        by (simp add: nn_integral_add nn_integral_cmult_indicator G_def) }
  11.145      note f0_eq = this
  11.146      { fix A assume A: "A \<in> sets M"
  11.147        hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
  11.148 @@ -480,11 +480,11 @@
  11.149          by (auto intro!: add_left_mono simp: sets_eq)
  11.150        also have "\<dots> \<le> N A"
  11.151          unfolding emeasure_M[OF `A \<in> sets M`]
  11.152 -        using f_le_v N.emeasure_eq_measure[of A] positive_integral_positive[of M "?F A"]
  11.153 +        using f_le_v N.emeasure_eq_measure[of A] nn_integral_nonneg[of M "?F A"]
  11.154          by (cases "\<integral>\<^sup>+x. ?F A x \<partial>M", cases "N A") auto
  11.155        finally have "(\<integral>\<^sup>+x. ?f0 x * indicator A x \<partial>M) \<le> N A" . }
  11.156      hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G` by (auto simp: G_def)
  11.157 -    have int_f_finite: "integral\<^sup>P M f \<noteq> \<infinity>"
  11.158 +    have int_f_finite: "integral\<^sup>N M f \<noteq> \<infinity>"
  11.159        by (metis N.emeasure_finite ereal_infty_less_eq2(1) int_f_eq_y y_le)
  11.160      have  "0 < ?M (space M) - emeasure ?Mb (space M)"
  11.161        using pos_t
  11.162 @@ -503,13 +503,13 @@
  11.163        by (auto simp: absolutely_continuous_def null_sets_def)
  11.164      then have "0 < emeasure M A0" using emeasure_nonneg[of M A0] by auto
  11.165      hence "0 < b * emeasure M A0" using b by (auto simp: ereal_zero_less_0_iff)
  11.166 -    with int_f_finite have "?y + 0 < integral\<^sup>P M f + b * emeasure M A0" unfolding int_f_eq_y
  11.167 +    with int_f_finite have "?y + 0 < integral\<^sup>N M f + b * emeasure M A0" unfolding int_f_eq_y
  11.168        using `f \<in> G`
  11.169 -      by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 positive_integral_positive)
  11.170 -    also have "\<dots> = integral\<^sup>P M ?f0" using f0_eq[OF sets.top] `A0 \<in> sets M` sets.sets_into_space
  11.171 -      by (simp cong: positive_integral_cong)
  11.172 -    finally have "?y < integral\<^sup>P M ?f0" by simp
  11.173 -    moreover from `?f0 \<in> G` have "integral\<^sup>P M ?f0 \<le> ?y" by (auto intro!: SUP_upper)
  11.174 +      by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 nn_integral_nonneg)
  11.175 +    also have "\<dots> = integral\<^sup>N M ?f0" using f0_eq[OF sets.top] `A0 \<in> sets M` sets.sets_into_space
  11.176 +      by (simp cong: nn_integral_cong)
  11.177 +    finally have "?y < integral\<^sup>N M ?f0" by simp
  11.178 +    moreover from `?f0 \<in> G` have "integral\<^sup>N M ?f0 \<le> ?y" by (auto intro!: SUP_upper)
  11.179      ultimately show False by auto
  11.180    qed
  11.181    let ?f = "\<lambda>x. max 0 (f x)"
  11.182 @@ -520,7 +520,7 @@
  11.183      fix A assume A: "A\<in>sets (density M ?f)"
  11.184      then show "emeasure (density M ?f) A = emeasure N A"
  11.185        using `f \<in> G` A upper_bound[THEN bspec, of A] N.emeasure_eq_measure[of A]
  11.186 -      by (cases "integral\<^sup>P M (?F A)")
  11.187 +      by (cases "integral\<^sup>N M (?F A)")
  11.188           (auto intro!: antisym simp add: emeasure_density G_def emeasure_M density_max_0[symmetric])
  11.189    qed auto
  11.190  qed
  11.191 @@ -669,10 +669,10 @@
  11.192    proof (intro allI finite_measure.Radon_Nikodym_finite_measure)
  11.193      fix i
  11.194      from Q show "finite_measure (?M i)"
  11.195 -      by (auto intro!: finite_measureI cong: positive_integral_cong
  11.196 +      by (auto intro!: finite_measureI cong: nn_integral_cong
  11.197                 simp add: emeasure_density subset_eq sets_eq)
  11.198      from Q have "emeasure (?N i) (space N) = emeasure N (Q i)"
  11.199 -      by (simp add: sets_eq[symmetric] emeasure_density subset_eq cong: positive_integral_cong)
  11.200 +      by (simp add: sets_eq[symmetric] emeasure_density subset_eq cong: nn_integral_cong)
  11.201      with Q_fin show "finite_measure (?N i)"
  11.202        by (auto intro!: finite_measureI)
  11.203      show "sets (?N i) = sets (?M i)" by (simp add: sets_eq)
  11.204 @@ -688,8 +688,8 @@
  11.205      by force
  11.206    { fix A i assume A: "A \<in> sets M"
  11.207      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"
  11.208 -      by (auto simp add: emeasure_density positive_integral_density subset_eq
  11.209 -               intro!: positive_integral_cong split: split_indicator)
  11.210 +      by (auto simp add: emeasure_density nn_integral_density subset_eq
  11.211 +               intro!: nn_integral_cong split: split_indicator)
  11.212      also have "\<dots> = emeasure N (Q i \<inter> A)"
  11.213        using A Q by (simp add: f_density emeasure_restricted subset_eq sets_eq)
  11.214      finally have "emeasure N (Q i \<inter> A) = (\<integral>\<^sup>+x. f i x * indicator (Q i \<inter> A) x \<partial>M)" .. }
  11.215 @@ -709,13 +709,13 @@
  11.216          "\<And>i. AE x in M. 0 \<le> f i x * indicator (Q i \<inter> A) x"
  11.217          using borel Qi Q0(1) `A \<in> sets M` by (auto intro!: borel_measurable_ereal_times)
  11.218        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)"
  11.219 -        using borel by (intro positive_integral_cong) (auto simp: indicator_def)
  11.220 +        using borel by (intro nn_integral_cong) (auto simp: indicator_def)
  11.221        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)"
  11.222          using borel Qi Q0(1) `A \<in> sets M`
  11.223 -        by (subst positive_integral_add) (auto simp del: ereal_infty_mult
  11.224 -            simp add: positive_integral_cmult_indicator sets.Int intro!: suminf_0_le)
  11.225 +        by (subst nn_integral_add) (auto simp del: ereal_infty_mult
  11.226 +            simp add: nn_integral_cmult_indicator sets.Int intro!: suminf_0_le)
  11.227        also have "\<dots> = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)"
  11.228 -        by (subst integral_eq[OF `A \<in> sets M`], subst positive_integral_suminf) auto
  11.229 +        by (subst integral_eq[OF `A \<in> sets M`], subst nn_integral_suminf) auto
  11.230        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)" .
  11.231        moreover have "(\<Sum>i. N (Q i \<inter> A)) = N ((\<Union>i. Q i) \<inter> A)"
  11.232          using Q Q_sets `A \<in> sets M`
  11.233 @@ -742,7 +742,7 @@
  11.234    shows "\<exists>f \<in> borel_measurable M. (\<forall>x. 0 \<le> f x) \<and> density M f = N"
  11.235  proof -
  11.236    from Ex_finite_integrable_function
  11.237 -  obtain h where finite: "integral\<^sup>P M h \<noteq> \<infinity>" and
  11.238 +  obtain h where finite: "integral\<^sup>N M h \<noteq> \<infinity>" and
  11.239      borel: "h \<in> borel_measurable M" and
  11.240      nn: "\<And>x. 0 \<le> h x" and
  11.241      pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
  11.242 @@ -750,7 +750,7 @@
  11.243    let ?T = "\<lambda>A. (\<integral>\<^sup>+x. h x * indicator A x \<partial>M)"
  11.244    let ?MT = "density M h"
  11.245    from borel finite nn interpret T: finite_measure ?MT
  11.246 -    by (auto intro!: finite_measureI cong: positive_integral_cong simp: emeasure_density)
  11.247 +    by (auto intro!: finite_measureI cong: nn_integral_cong simp: emeasure_density)
  11.248    have "absolutely_continuous ?MT N" "sets N = sets ?MT"
  11.249    proof (unfold absolutely_continuous_def, safe)
  11.250      fix A assume "A \<in> null_sets ?MT"
  11.251 @@ -774,7 +774,7 @@
  11.252  lemma finite_density_unique:
  11.253    assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  11.254    assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
  11.255 -  and fin: "integral\<^sup>P M f \<noteq> \<infinity>"
  11.256 +  and fin: "integral\<^sup>N M f \<noteq> \<infinity>"
  11.257    shows "density M f = density M g \<longleftrightarrow> (AE x in M. f x = g x)"
  11.258  proof (intro iffI ballI)
  11.259    fix A assume eq: "AE x in M. f x = g x"
  11.260 @@ -786,19 +786,19 @@
  11.261    with borel have eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
  11.262      by (simp add: emeasure_density[symmetric])
  11.263    from this[THEN bspec, OF sets.top] fin
  11.264 -  have g_fin: "integral\<^sup>P M g \<noteq> \<infinity>" by (simp cong: positive_integral_cong)
  11.265 +  have g_fin: "integral\<^sup>N M g \<noteq> \<infinity>" by (simp cong: nn_integral_cong)
  11.266    { fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  11.267        and pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
  11.268 -      and g_fin: "integral\<^sup>P M g \<noteq> \<infinity>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
  11.269 +      and g_fin: "integral\<^sup>N M g \<noteq> \<infinity>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
  11.270      let ?N = "{x\<in>space M. g x < f x}"
  11.271      have N: "?N \<in> sets M" using borel by simp
  11.272 -    have "?P g ?N \<le> integral\<^sup>P M g" using pos
  11.273 -      by (intro positive_integral_mono_AE) (auto split: split_indicator)
  11.274 +    have "?P g ?N \<le> integral\<^sup>N M g" using pos
  11.275 +      by (intro nn_integral_mono_AE) (auto split: split_indicator)
  11.276      then have Pg_fin: "?P g ?N \<noteq> \<infinity>" using g_fin by auto
  11.277      have "?P (\<lambda>x. (f x - g x)) ?N = (\<integral>\<^sup>+x. f x * indicator ?N x - g x * indicator ?N x \<partial>M)"
  11.278 -      by (auto intro!: positive_integral_cong simp: indicator_def)
  11.279 +      by (auto intro!: nn_integral_cong simp: indicator_def)
  11.280      also have "\<dots> = ?P f ?N - ?P g ?N"
  11.281 -    proof (rule positive_integral_diff)
  11.282 +    proof (rule nn_integral_diff)
  11.283        show "(\<lambda>x. f x * indicator ?N x) \<in> borel_measurable M" "(\<lambda>x. g x * indicator ?N x) \<in> borel_measurable M"
  11.284          using borel N by auto
  11.285        show "AE x in M. g x * indicator ?N x \<le> f x * indicator ?N x"
  11.286 @@ -806,10 +806,10 @@
  11.287          using pos by (auto split: split_indicator)
  11.288      qed fact
  11.289      also have "\<dots> = 0"
  11.290 -      unfolding eq[THEN bspec, OF N] using positive_integral_positive[of M] Pg_fin by auto
  11.291 +      unfolding eq[THEN bspec, OF N] using nn_integral_nonneg[of M] Pg_fin by auto
  11.292      finally have "AE x in M. f x \<le> g x"
  11.293 -      using pos borel positive_integral_PInf_AE[OF borel(2) g_fin]
  11.294 -      by (subst (asm) positive_integral_0_iff_AE)
  11.295 +      using pos borel nn_integral_PInf_AE[OF borel(2) g_fin]
  11.296 +      by (subst (asm) nn_integral_0_iff_AE)
  11.297           (auto split: split_indicator simp: not_less ereal_minus_le_iff) }
  11.298    from this[OF borel pos g_fin eq] this[OF borel(2,1) pos(2,1) fin] eq
  11.299    show "AE x in M. f x = g x" by auto
  11.300 @@ -856,9 +856,9 @@
  11.301            using borel Q0(1) by auto
  11.302          have "?N (?A i) \<le> (\<integral>\<^sup>+x. (i::ereal) * indicator (?A i) x \<partial>M)"
  11.303            unfolding eq[OF `?A i \<in> sets M`]
  11.304 -          by (auto intro!: positive_integral_mono simp: indicator_def)
  11.305 +          by (auto intro!: nn_integral_mono simp: indicator_def)
  11.306          also have "\<dots> = i * emeasure M (?A i)"
  11.307 -          using `?A i \<in> sets M` by (auto intro!: positive_integral_cmult_indicator)
  11.308 +          using `?A i \<in> sets M` by (auto intro!: nn_integral_cmult_indicator)
  11.309          also have "\<dots> < \<infinity>" using emeasure_real[of "?A i"] by simp
  11.310          finally have "?N (?A i) \<noteq> \<infinity>" by simp
  11.311          then show "?A i \<in> null_sets M" using in_Q0[OF `?A i \<in> sets M`] `?A i \<in> sets M` by auto
  11.312 @@ -888,35 +888,35 @@
  11.313    shows "AE x in M. f x = f' x"
  11.314  proof -
  11.315    obtain h where h_borel: "h \<in> borel_measurable M"
  11.316 -    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"
  11.317 +    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"
  11.318      using Ex_finite_integrable_function by auto
  11.319    then have h_nn: "AE x in M. 0 \<le> h x" by auto
  11.320    let ?H = "density M h"
  11.321    interpret h: finite_measure ?H
  11.322      using fin h_borel pos
  11.323 -    by (intro finite_measureI) (simp cong: positive_integral_cong emeasure_density add: fin)
  11.324 +    by (intro finite_measureI) (simp cong: nn_integral_cong emeasure_density add: fin)
  11.325    let ?fM = "density M f"
  11.326    let ?f'M = "density M f'"
  11.327    { fix A assume "A \<in> sets M"
  11.328      then have "{x \<in> space M. h x * indicator A x \<noteq> 0} = A"
  11.329        using pos(1) sets.sets_into_space by (force simp: indicator_def)
  11.330      then have "(\<integral>\<^sup>+x. h x * indicator A x \<partial>M) = 0 \<longleftrightarrow> A \<in> null_sets M"
  11.331 -      using h_borel `A \<in> sets M` h_nn by (subst positive_integral_0_iff) auto }
  11.332 +      using h_borel `A \<in> sets M` h_nn by (subst nn_integral_0_iff) auto }
  11.333    note h_null_sets = this
  11.334    { fix A assume "A \<in> sets M"
  11.335      have "(\<integral>\<^sup>+x. f x * (h x * indicator A x) \<partial>M) = (\<integral>\<^sup>+x. h x * indicator A x \<partial>?fM)"
  11.336        using `A \<in> sets M` h_borel h_nn f f'
  11.337 -      by (intro positive_integral_density[symmetric]) auto
  11.338 +      by (intro nn_integral_density[symmetric]) auto
  11.339      also have "\<dots> = (\<integral>\<^sup>+x. h x * indicator A x \<partial>?f'M)"
  11.340        by (simp_all add: density_eq)
  11.341      also have "\<dots> = (\<integral>\<^sup>+x. f' x * (h x * indicator A x) \<partial>M)"
  11.342        using `A \<in> sets M` h_borel h_nn f f'
  11.343 -      by (intro positive_integral_density) auto
  11.344 +      by (intro nn_integral_density) auto
  11.345      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)"
  11.346        by (simp add: ac_simps)
  11.347      then have "(\<integral>\<^sup>+x. (f x * indicator A x) \<partial>?H) = (\<integral>\<^sup>+x. (f' x * indicator A x) \<partial>?H)"
  11.348        using `A \<in> sets M` h_borel h_nn f f'
  11.349 -      by (subst (asm) (1 2) positive_integral_density[symmetric]) auto }
  11.350 +      by (subst (asm) (1 2) nn_integral_density[symmetric]) auto }
  11.351    then have "AE x in ?H. f x = f' x" using h_borel h_nn f f'
  11.352      by (intro h.density_unique_finite_measure absolutely_continuous_AE[of M])
  11.353         (auto simp add: AE_density)
  11.354 @@ -975,17 +975,17 @@
  11.355    assume "sigma_finite_measure ?N"
  11.356    then interpret N: sigma_finite_measure ?N .
  11.357    from N.Ex_finite_integrable_function obtain h where
  11.358 -    h: "h \<in> borel_measurable M" "integral\<^sup>P ?N h \<noteq> \<infinity>" and
  11.359 +    h: "h \<in> borel_measurable M" "integral\<^sup>N ?N h \<noteq> \<infinity>" and
  11.360      h_nn: "\<And>x. 0 \<le> h x" and
  11.361      fin: "\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>" by auto
  11.362    have "AE x in M. f x * h x \<noteq> \<infinity>"
  11.363    proof (rule AE_I')
  11.364 -    have "integral\<^sup>P ?N h = (\<integral>\<^sup>+x. f x * h x \<partial>M)" using f h h_nn
  11.365 -      by (auto intro!: positive_integral_density)
  11.366 +    have "integral\<^sup>N ?N h = (\<integral>\<^sup>+x. f x * h x \<partial>M)" using f h h_nn
  11.367 +      by (auto intro!: nn_integral_density)
  11.368      then have "(\<integral>\<^sup>+x. f x * h x \<partial>M) \<noteq> \<infinity>"
  11.369        using h(2) by simp
  11.370      then show "(\<lambda>x. f x * h x) -` {\<infinity>} \<inter> space M \<in> null_sets M"
  11.371 -      using f h(1) by (auto intro!: positive_integral_PInf borel_measurable_vimage)
  11.372 +      using f h(1) by (auto intro!: nn_integral_PInf borel_measurable_vimage)
  11.373    qed auto
  11.374    then show "AE x in M. f x \<noteq> \<infinity>"
  11.375      using fin by (auto elim!: AE_Ball_mp)
  11.376 @@ -1036,14 +1036,14 @@
  11.377        case 0
  11.378        have "AE x in M. f x * indicator (A i \<inter> Q j) x = 0"
  11.379          using AE by (auto simp: A_def `i = 0`)
  11.380 -      from positive_integral_cong_AE[OF this] show ?thesis by simp
  11.381 +      from nn_integral_cong_AE[OF this] show ?thesis by simp
  11.382      next
  11.383        case (Suc n)
  11.384        then have "(\<integral>\<^sup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<le>
  11.385          (\<integral>\<^sup>+x. (Suc n :: ereal) * indicator (Q j) x \<partial>M)"
  11.386 -        by (auto intro!: positive_integral_mono simp: indicator_def A_def real_eq_of_nat)
  11.387 +        by (auto intro!: nn_integral_mono simp: indicator_def A_def real_eq_of_nat)
  11.388        also have "\<dots> = Suc n * emeasure M (Q j)"
  11.389 -        using Q by (auto intro!: positive_integral_cmult_indicator)
  11.390 +        using Q by (auto intro!: nn_integral_cmult_indicator)
  11.391        also have "\<dots> < \<infinity>"
  11.392          using Q by (auto simp: real_eq_of_nat[symmetric])
  11.393        finally show ?thesis by simp
  11.394 @@ -1109,15 +1109,15 @@
  11.395    "absolutely_continuous M N \<Longrightarrow> sets N = sets M \<Longrightarrow> density M (RN_deriv M N) = N"
  11.396    by (metis RN_derivI Radon_Nikodym)
  11.397  
  11.398 -lemma (in sigma_finite_measure) RN_deriv_positive_integral:
  11.399 +lemma (in sigma_finite_measure) RN_deriv_nn_integral:
  11.400    assumes N: "absolutely_continuous M N" "sets N = sets M"
  11.401      and f: "f \<in> borel_measurable M"
  11.402 -  shows "integral\<^sup>P N f = (\<integral>\<^sup>+x. RN_deriv M N x * f x \<partial>M)"
  11.403 +  shows "integral\<^sup>N N f = (\<integral>\<^sup>+x. RN_deriv M N x * f x \<partial>M)"
  11.404  proof -
  11.405 -  have "integral\<^sup>P N f = integral\<^sup>P (density M (RN_deriv M N)) f"
  11.406 +  have "integral\<^sup>N N f = integral\<^sup>N (density M (RN_deriv M N)) f"
  11.407      using N by (simp add: density_RN_deriv)
  11.408    also have "\<dots> = (\<integral>\<^sup>+x. RN_deriv M N x * f x \<partial>M)"
  11.409 -    using f by (simp add: positive_integral_density RN_deriv_nonneg)
  11.410 +    using f by (simp add: nn_integral_density RN_deriv_nonneg)
  11.411    finally show ?thesis by simp
  11.412  qed
  11.413  
  11.414 @@ -1261,9 +1261,9 @@
  11.415    have "N (?RN \<infinity>) = (\<integral>\<^sup>+ x. RN_deriv M N x * indicator (?RN \<infinity>) x \<partial>M)"
  11.416      using RN(1,3) by (subst RN(2)[symmetric]) (auto simp: emeasure_density)
  11.417    also have "\<dots> = (\<integral>\<^sup>+ x. \<infinity> * indicator (?RN \<infinity>) x \<partial>M)"
  11.418 -    by (intro positive_integral_cong) (auto simp: indicator_def)
  11.419 +    by (intro nn_integral_cong) (auto simp: indicator_def)
  11.420    also have "\<dots> = \<infinity> * emeasure M (?RN \<infinity>)"
  11.421 -    using RN by (intro positive_integral_cmult_indicator) auto
  11.422 +    using RN by (intro nn_integral_cmult_indicator) auto
  11.423    finally have eq: "N (?RN \<infinity>) = \<infinity> * emeasure M (?RN \<infinity>)" .
  11.424    moreover
  11.425    have "emeasure M (?RN \<infinity>) = 0"
  11.426 @@ -1287,7 +1287,7 @@
  11.427    have "N (?RN 0) = (\<integral>\<^sup>+ x. RN_deriv M N x * indicator (?RN 0) x \<partial>M)"
  11.428      using RN(1,3) by (subst RN(2)[symmetric]) (auto simp: emeasure_density)
  11.429    also have "\<dots> = (\<integral>\<^sup>+ x. 0 \<partial>M)"
  11.430 -    by (intro positive_integral_cong) (auto simp: indicator_def)
  11.431 +    by (intro nn_integral_cong) (auto simp: indicator_def)
  11.432    finally have "AE x in N. RN_deriv M N x \<noteq> 0"
  11.433      using RN by (subst AE_iff_measurable[OF _ refl]) (auto simp: ac cong: sets_eq_imp_space_eq)
  11.434    with RN(3) eq show "AE x in N. 0 < real (RN_deriv M N x)"
  11.435 @@ -1301,9 +1301,9 @@
  11.436  proof -
  11.437    from `{x} \<in> sets M`
  11.438    have "density M (RN_deriv M N) {x} = (\<integral>\<^sup>+w. RN_deriv M N x * indicator {x} w \<partial>M)"
  11.439 -    by (auto simp: indicator_def emeasure_density intro!: positive_integral_cong)
  11.440 +    by (auto simp: indicator_def emeasure_density intro!: nn_integral_cong)
  11.441    with x density_RN_deriv[OF ac] RN_deriv_nonneg[of M N] show ?thesis
  11.442 -    by (auto simp: positive_integral_cmult_indicator)
  11.443 +    by (auto simp: nn_integral_cmult_indicator)
  11.444  qed
  11.445  
  11.446  end