introduced integral syntax
authorhoelzl
Fri Jan 14 14:21:48 2011 +0100 (2011-01-14)
changeset 41544c3b977fee8a3
parent 41543 646a1399e792
child 41545 9c869baf1c66
introduced integral syntax
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Positive_Extended_Real.thy
src/HOL/Probability/Probability_Space.thy
src/HOL/Probability/Product_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
     1.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Jan 14 14:21:26 2011 +0100
     1.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Jan 14 14:21:48 2011 +0100
     1.3 @@ -489,7 +489,7 @@
     1.4  
     1.5  section "Simple integral"
     1.6  
     1.7 -definition (in measure_space)
     1.8 +definition (in measure_space) simple_integral (binder "\<integral>\<^isup>S " 10) where
     1.9    "simple_integral f = (\<Sum>x \<in> f ` space M. x * \<mu> (f -` {x} \<inter> space M))"
    1.10  
    1.11  lemma (in measure_space) simple_integral_cong:
    1.12 @@ -514,7 +514,7 @@
    1.13  qed
    1.14  
    1.15  lemma (in measure_space) simple_integral_const[simp]:
    1.16 -  "simple_integral (\<lambda>x. c) = c * \<mu> (space M)"
    1.17 +  "(\<integral>\<^isup>Sx. c) = c * \<mu> (space M)"
    1.18  proof (cases "space M = {}")
    1.19    case True thus ?thesis unfolding simple_integral_def by simp
    1.20  next
    1.21 @@ -579,7 +579,7 @@
    1.22  
    1.23  lemma (in measure_space) simple_integral_add[simp]:
    1.24    assumes "simple_function f" and "simple_function g"
    1.25 -  shows "simple_integral (\<lambda>x. f x + g x) = simple_integral f + simple_integral g"
    1.26 +  shows "(\<integral>\<^isup>Sx. f x + g x) = simple_integral f + simple_integral g"
    1.27  proof -
    1.28    { fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
    1.29      assume "x \<in> space M"
    1.30 @@ -597,7 +597,7 @@
    1.31  
    1.32  lemma (in measure_space) simple_integral_setsum[simp]:
    1.33    assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function (f i)"
    1.34 -  shows "simple_integral (\<lambda>x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. simple_integral (f i))"
    1.35 +  shows "(\<integral>\<^isup>Sx. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. simple_integral (f i))"
    1.36  proof cases
    1.37    assume "finite P"
    1.38    from this assms show ?thesis
    1.39 @@ -606,7 +606,7 @@
    1.40  
    1.41  lemma (in measure_space) simple_integral_mult[simp]:
    1.42    assumes "simple_function f"
    1.43 -  shows "simple_integral (\<lambda>x. c * f x) = c * simple_integral f"
    1.44 +  shows "(\<integral>\<^isup>Sx. c * f x) = c * simple_integral f"
    1.45  proof -
    1.46    note mult = simple_function_mult[OF simple_function_const[of c] assms]
    1.47    { fix x let ?S = "f -` {f x} \<inter> (\<lambda>x. c * f x) -` {c * f x} \<inter> space M"
    1.48 @@ -700,11 +700,11 @@
    1.49  lemma (in measure_space) simple_integral_indicator:
    1.50    assumes "A \<in> sets M"
    1.51    assumes "simple_function f"
    1.52 -  shows "simple_integral (\<lambda>x. f x * indicator A x) =
    1.53 +  shows "(\<integral>\<^isup>Sx. f x * indicator A x) =
    1.54      (\<Sum>x \<in> f ` space M. x * \<mu> (f -` {x} \<inter> space M \<inter> A))"
    1.55  proof cases
    1.56    assume "A = space M"
    1.57 -  moreover hence "simple_integral (\<lambda>x. f x * indicator A x) = simple_integral f"
    1.58 +  moreover hence "(\<integral>\<^isup>Sx. f x * indicator A x) = simple_integral f"
    1.59      by (auto intro!: simple_integral_cong)
    1.60    moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto
    1.61    ultimately show ?thesis by (simp add: simple_integral_def)
    1.62 @@ -720,7 +720,7 @@
    1.63    next
    1.64      show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x])
    1.65    qed
    1.66 -  have *: "simple_integral (\<lambda>x. f x * indicator A x) =
    1.67 +  have *: "(\<integral>\<^isup>Sx. f x * indicator A x) =
    1.68      (\<Sum>x \<in> f ` space M \<union> {0}. x * \<mu> (f -` {x} \<inter> space M \<inter> A))"
    1.69      unfolding simple_integral_def I
    1.70    proof (rule setsum_mono_zero_cong_left)
    1.71 @@ -760,18 +760,18 @@
    1.72  
    1.73  lemma (in measure_space) simple_integral_null_set:
    1.74    assumes "simple_function u" "N \<in> null_sets"
    1.75 -  shows "simple_integral (\<lambda>x. u x * indicator N x) = 0"
    1.76 +  shows "(\<integral>\<^isup>Sx. u x * indicator N x) = 0"
    1.77  proof -
    1.78    have "AE x. indicator N x = (0 :: pextreal)"
    1.79      using `N \<in> null_sets` by (auto simp: indicator_def intro!: AE_I[of _ N])
    1.80 -  then have "simple_integral (\<lambda>x. u x * indicator N x) = simple_integral (\<lambda>x. 0)"
    1.81 +  then have "(\<integral>\<^isup>Sx. u x * indicator N x) = (\<integral>\<^isup>Sx. 0)"
    1.82      using assms by (intro simple_integral_cong_AE) (auto intro!: AE_disjI2)
    1.83    then show ?thesis by simp
    1.84  qed
    1.85  
    1.86  lemma (in measure_space) simple_integral_cong_AE_mult_indicator:
    1.87    assumes sf: "simple_function f" and eq: "AE x. x \<in> S" and "S \<in> sets M"
    1.88 -  shows "simple_integral f = simple_integral (\<lambda>x. f x * indicator S x)"
    1.89 +  shows "simple_integral f = (\<integral>\<^isup>Sx. f x * indicator S x)"
    1.90  proof (rule simple_integral_cong_AE)
    1.91    show "simple_function f" by fact
    1.92    show "simple_function (\<lambda>x. f x * indicator S x)"
    1.93 @@ -783,7 +783,7 @@
    1.94  lemma (in measure_space) simple_integral_restricted:
    1.95    assumes "A \<in> sets M"
    1.96    assumes sf: "simple_function (\<lambda>x. f x * indicator A x)"
    1.97 -  shows "measure_space.simple_integral (restricted_space A) \<mu> f = simple_integral (\<lambda>x. f x * indicator A x)"
    1.98 +  shows "measure_space.simple_integral (restricted_space A) \<mu> f = (\<integral>\<^isup>Sx. f x * indicator A x)"
    1.99      (is "_ = simple_integral ?f")
   1.100    unfolding measure_space.simple_integral_def[OF restricted_measure_space[OF `A \<in> sets M`]]
   1.101    unfolding simple_integral_def
   1.102 @@ -842,7 +842,7 @@
   1.103  
   1.104  section "Continuous posititve integration"
   1.105  
   1.106 -definition (in measure_space)
   1.107 +definition (in measure_space) positive_integral (binder "\<integral>\<^isup>+ " 10) where
   1.108    "positive_integral f = SUPR {g. simple_function g \<and> g \<le> f} simple_integral"
   1.109  
   1.110  lemma (in measure_space) positive_integral_alt:
   1.111 @@ -1071,7 +1071,7 @@
   1.112    fixes g :: "'d \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
   1.113    assumes f: "bij_inv S (space M) f h"
   1.114    shows "measure_space.positive_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) g =
   1.115 -      positive_integral (\<lambda>x. g (h x))"
   1.116 +      (\<integral>\<^isup>+x. g (h x))"
   1.117  proof -
   1.118    interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
   1.119      using f by (rule measure_space_isomorphic[OF bij_inv_bij_betw(1)])
   1.120 @@ -1149,7 +1149,7 @@
   1.121      unfolding pextreal_SUP_cmult[symmetric]
   1.122    proof (safe intro!: SUP_mono bexI)
   1.123      fix i
   1.124 -    have "a * simple_integral (?uB i) = simple_integral (\<lambda>x. a * ?uB i x)"
   1.125 +    have "a * simple_integral (?uB i) = (\<integral>\<^isup>Sx. a * ?uB i x)"
   1.126        using B `simple_function u`
   1.127        by (subst simple_integral_mult[symmetric]) (auto simp: field_simps)
   1.128      also have "\<dots> \<le> positive_integral (f i)"
   1.129 @@ -1193,7 +1193,7 @@
   1.130  lemma (in measure_space) positive_integral_monotone_convergence_SUP:
   1.131    assumes "\<And>i x. x \<in> space M \<Longrightarrow> f i x \<le> f (Suc i) x"
   1.132    assumes "\<And>i. f i \<in> borel_measurable M"
   1.133 -  shows "(SUP i. positive_integral (f i)) = positive_integral (\<lambda>x. SUP i. f i x)"
   1.134 +  shows "(SUP i. positive_integral (f i)) = (\<integral>\<^isup>+ x. SUP i. f i x)"
   1.135      (is "_ = positive_integral ?u")
   1.136  proof -
   1.137    show ?thesis
   1.138 @@ -1236,7 +1236,7 @@
   1.139  qed
   1.140  
   1.141  lemma (in measure_space) positive_integral_const[simp]:
   1.142 -  "positive_integral (\<lambda>x. c) = c * \<mu> (space M)"
   1.143 +  "(\<integral>\<^isup>+ x. c) = c * \<mu> (space M)"
   1.144    by (subst positive_integral_eq_simple_integral) auto
   1.145  
   1.146  lemma (in measure_space) positive_integral_isoton_simple:
   1.147 @@ -1248,7 +1248,7 @@
   1.148  lemma (in measure_space) positive_integral_linear:
   1.149    assumes f: "f \<in> borel_measurable M"
   1.150    and g: "g \<in> borel_measurable M"
   1.151 -  shows "positive_integral (\<lambda>x. a * f x + g x) =
   1.152 +  shows "(\<integral>\<^isup>+ x. a * f x + g x) =
   1.153        a * positive_integral f + positive_integral g"
   1.154      (is "positive_integral ?L = _")
   1.155  proof -
   1.156 @@ -1276,30 +1276,32 @@
   1.157  
   1.158  lemma (in measure_space) positive_integral_cmult:
   1.159    assumes "f \<in> borel_measurable M"
   1.160 -  shows "positive_integral (\<lambda>x. c * f x) = c * positive_integral f"
   1.161 +  shows "(\<integral>\<^isup>+ x. c * f x) = c * positive_integral f"
   1.162    using positive_integral_linear[OF assms, of "\<lambda>x. 0" c] by auto
   1.163  
   1.164  lemma (in measure_space) positive_integral_multc:
   1.165    assumes "f \<in> borel_measurable M"
   1.166 -  shows "positive_integral (\<lambda>x. f x * c) = positive_integral f * c"
   1.167 +  shows "(\<integral>\<^isup>+ x. f x * c) = positive_integral f * c"
   1.168    unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp
   1.169  
   1.170  lemma (in measure_space) positive_integral_indicator[simp]:
   1.171 -  "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. indicator A x) = \<mu> A"
   1.172 -by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)
   1.173 +  "A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. indicator A x) = \<mu> A"
   1.174 +  by (subst positive_integral_eq_simple_integral)
   1.175 +     (auto simp: simple_function_indicator simple_integral_indicator)
   1.176  
   1.177  lemma (in measure_space) positive_integral_cmult_indicator:
   1.178 -  "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. c * indicator A x) = c * \<mu> A"
   1.179 -by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)
   1.180 +  "A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. c * indicator A x) = c * \<mu> A"
   1.181 +  by (subst positive_integral_eq_simple_integral)
   1.182 +     (auto simp: simple_function_indicator simple_integral_indicator)
   1.183  
   1.184  lemma (in measure_space) positive_integral_add:
   1.185    assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   1.186 -  shows "positive_integral (\<lambda>x. f x + g x) = positive_integral f + positive_integral g"
   1.187 +  shows "(\<integral>\<^isup>+ x. f x + g x) = positive_integral f + positive_integral g"
   1.188    using positive_integral_linear[OF assms, of 1] by simp
   1.189  
   1.190  lemma (in measure_space) positive_integral_setsum:
   1.191    assumes "\<And>i. i\<in>P \<Longrightarrow> f i \<in> borel_measurable M"
   1.192 -  shows "positive_integral (\<lambda>x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. positive_integral (f i))"
   1.193 +  shows "(\<integral>\<^isup>+ x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. positive_integral (f i))"
   1.194  proof cases
   1.195    assume "finite P"
   1.196    from this assms show ?thesis
   1.197 @@ -1317,11 +1319,11 @@
   1.198    assumes f: "f \<in> borel_measurable M" and g: "g \<in> borel_measurable M"
   1.199    and fin: "positive_integral g \<noteq> \<omega>"
   1.200    and mono: "\<And>x. x \<in> space M \<Longrightarrow> g x \<le> f x"
   1.201 -  shows "positive_integral (\<lambda>x. f x - g x) = positive_integral f - positive_integral g"
   1.202 +  shows "(\<integral>\<^isup>+ x. f x - g x) = positive_integral f - positive_integral g"
   1.203  proof -
   1.204    have borel: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   1.205      using f g by (rule borel_measurable_pextreal_diff)
   1.206 -  have "positive_integral (\<lambda>x. f x - g x) + positive_integral g =
   1.207 +  have "(\<integral>\<^isup>+x. f x - g x) + positive_integral g =
   1.208      positive_integral f"
   1.209      unfolding positive_integral_add[OF borel g, symmetric]
   1.210    proof (rule positive_integral_cong)
   1.211 @@ -1335,9 +1337,9 @@
   1.212  
   1.213  lemma (in measure_space) positive_integral_psuminf:
   1.214    assumes "\<And>i. f i \<in> borel_measurable M"
   1.215 -  shows "positive_integral (\<lambda>x. \<Sum>\<^isub>\<infinity> i. f i x) = (\<Sum>\<^isub>\<infinity> i. positive_integral (f i))"
   1.216 +  shows "(\<integral>\<^isup>+ x. \<Sum>\<^isub>\<infinity> i. f i x) = (\<Sum>\<^isub>\<infinity> i. positive_integral (f i))"
   1.217  proof -
   1.218 -  have "(\<lambda>i. positive_integral (\<lambda>x. \<Sum>i<i. f i x)) \<up> positive_integral (\<lambda>x. \<Sum>\<^isub>\<infinity>i. f i x)"
   1.219 +  have "(\<lambda>i. (\<integral>\<^isup>+x. \<Sum>i<i. f i x)) \<up> (\<integral>\<^isup>+x. \<Sum>\<^isub>\<infinity>i. f i x)"
   1.220      by (rule positive_integral_isoton)
   1.221         (auto intro!: borel_measurable_pextreal_setsum assms positive_integral_mono
   1.222                       arg_cong[where f=Sup]
   1.223 @@ -1350,11 +1352,11 @@
   1.224  lemma (in measure_space) positive_integral_lim_INF:
   1.225    fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> pextreal"
   1.226    assumes "\<And>i. u i \<in> borel_measurable M"
   1.227 -  shows "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x) \<le>
   1.228 +  shows "(\<integral>\<^isup>+ x. SUP n. INF m. u (m + n) x) \<le>
   1.229      (SUP n. INF m. positive_integral (u (m + n)))"
   1.230  proof -
   1.231 -  have "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x)
   1.232 -      = (SUP n. positive_integral (\<lambda>x. INF m. u (m + n) x))"
   1.233 +  have "(\<integral>\<^isup>+x. SUP n. INF m. u (m + n) x)
   1.234 +      = (SUP n. (\<integral>\<^isup>+x. INF m. u (m + n) x))"
   1.235      using assms
   1.236      by (intro positive_integral_monotone_convergence_SUP[symmetric] INF_mono)
   1.237         (auto simp del: add_Suc simp add: add_Suc[symmetric])
   1.238 @@ -1365,7 +1367,7 @@
   1.239  
   1.240  lemma (in measure_space) measure_space_density:
   1.241    assumes borel: "u \<in> borel_measurable M"
   1.242 -  shows "measure_space M (\<lambda>A. positive_integral (\<lambda>x. u x * indicator A x))" (is "measure_space M ?v")
   1.243 +  shows "measure_space M (\<lambda>A. (\<integral>\<^isup>+ x. u x * indicator A x))" (is "measure_space M ?v")
   1.244  proof
   1.245    show "?v {} = 0" by simp
   1.246    show "countably_additive M ?v"
   1.247 @@ -1384,8 +1386,8 @@
   1.248  
   1.249  lemma (in measure_space) positive_integral_translated_density:
   1.250    assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   1.251 -  shows "measure_space.positive_integral M (\<lambda>A. positive_integral (\<lambda>x. f x * indicator A x)) g =
   1.252 -    positive_integral (\<lambda>x. f x * g x)" (is "measure_space.positive_integral M ?T _ = _")
   1.253 +  shows "measure_space.positive_integral M (\<lambda>A. (\<integral>\<^isup>+ x. f x * indicator A x)) g = 
   1.254 +         (\<integral>\<^isup>+ x. f x * g x)" (is "measure_space.positive_integral M ?T _ = _")
   1.255  proof -
   1.256    from measure_space_density[OF assms(1)]
   1.257    interpret T: measure_space M ?T .
   1.258 @@ -1399,30 +1401,30 @@
   1.259        using G(1) unfolding simple_function_def by auto
   1.260      have "T.positive_integral (G i) = T.simple_integral (G i)"
   1.261        using G T.positive_integral_eq_simple_integral by simp
   1.262 -    also have "\<dots> = positive_integral (\<lambda>x. f x * (\<Sum>y\<in>G i`space M. y * indicator (G i -` {y} \<inter> space M) x))"
   1.263 +    also have "\<dots> = (\<integral>\<^isup>+x. f x * (\<Sum>y\<in>G i`space M. y * indicator (G i -` {y} \<inter> space M) x))"
   1.264        apply (simp add: T.simple_integral_def)
   1.265        apply (subst positive_integral_cmult[symmetric])
   1.266        using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage)
   1.267        apply (subst positive_integral_setsum[symmetric])
   1.268        using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage)
   1.269        by (simp add: setsum_right_distrib field_simps)
   1.270 -    also have "\<dots> = positive_integral (\<lambda>x. f x * G i x)"
   1.271 +    also have "\<dots> = (\<integral>\<^isup>+x. f x * G i x)"
   1.272        by (auto intro!: positive_integral_cong
   1.273                 simp: indicator_def if_distrib setsum_cases)
   1.274 -    finally have "T.positive_integral (G i) = positive_integral (\<lambda>x. f x * G i x)" . }
   1.275 -  with * have eq_Tg: "(\<lambda>i. positive_integral (\<lambda>x. f x * G i x)) \<up> T.positive_integral g" by simp
   1.276 +    finally have "T.positive_integral (G i) = (\<integral>\<^isup>+x. f x * G i x)" . }
   1.277 +  with * have eq_Tg: "(\<lambda>i. (\<integral>\<^isup>+x. f x * G i x)) \<up> T.positive_integral g" by simp
   1.278    from G(2) have "(\<lambda>i x. f x * G i x) \<up> (\<lambda>x. f x * g x)"
   1.279      unfolding isoton_fun_expand by (auto intro!: isoton_cmult_right)
   1.280 -  then have "(\<lambda>i. positive_integral (\<lambda>x. f x * G i x)) \<up> positive_integral (\<lambda>x. f x * g x)"
   1.281 +  then have "(\<lambda>i. (\<integral>\<^isup>+x. f x * G i x)) \<up> (\<integral>\<^isup>+x. f x * g x)"
   1.282      using assms(1) G_borel by (auto intro!: positive_integral_isoton borel_measurable_pextreal_times)
   1.283 -  with eq_Tg show "T.positive_integral g = positive_integral (\<lambda>x. f x * g x)"
   1.284 +  with eq_Tg show "T.positive_integral g = (\<integral>\<^isup>+x. f x * g x)"
   1.285      unfolding isoton_def by simp
   1.286  qed
   1.287  
   1.288  lemma (in measure_space) positive_integral_null_set:
   1.289 -  assumes "N \<in> null_sets" shows "positive_integral (\<lambda>x. u x * indicator N x) = 0"
   1.290 +  assumes "N \<in> null_sets" shows "(\<integral>\<^isup>+ x. u x * indicator N x) = 0"
   1.291  proof -
   1.292 -  have "positive_integral (\<lambda>x. u x * indicator N x) = positive_integral (\<lambda>x. 0)"
   1.293 +  have "(\<integral>\<^isup>+ x. u x * indicator N x) = (\<integral>\<^isup>+ x. 0)"
   1.294    proof (intro positive_integral_cong_AE AE_I)
   1.295      show "{x \<in> space M. u x * indicator N x \<noteq> 0} \<subseteq> N"
   1.296        by (auto simp: indicator_def)
   1.297 @@ -1434,20 +1436,20 @@
   1.298  
   1.299  lemma (in measure_space) positive_integral_Markov_inequality:
   1.300    assumes borel: "u \<in> borel_measurable M" and "A \<in> sets M" and c: "c \<noteq> \<omega>"
   1.301 -  shows "\<mu> ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * positive_integral (\<lambda>x. u x * indicator A x)"
   1.302 +  shows "\<mu> ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * (\<integral>\<^isup>+ x. u x * indicator A x)"
   1.303      (is "\<mu> ?A \<le> _ * ?PI")
   1.304  proof -
   1.305    have "?A \<in> sets M"
   1.306      using `A \<in> sets M` borel by auto
   1.307 -  hence "\<mu> ?A = positive_integral (\<lambda>x. indicator ?A x)"
   1.308 +  hence "\<mu> ?A = (\<integral>\<^isup>+ x. indicator ?A x)"
   1.309      using positive_integral_indicator by simp
   1.310 -  also have "\<dots> \<le> positive_integral (\<lambda>x. c * (u x * indicator A x))"
   1.311 +  also have "\<dots> \<le> (\<integral>\<^isup>+ x. c * (u x * indicator A x))"
   1.312    proof (rule positive_integral_mono)
   1.313      fix x assume "x \<in> space M"
   1.314      show "indicator ?A x \<le> c * (u x * indicator A x)"
   1.315        by (cases "x \<in> ?A") auto
   1.316    qed
   1.317 -  also have "\<dots> = c * positive_integral (\<lambda>x. u x * indicator A x)"
   1.318 +  also have "\<dots> = c * (\<integral>\<^isup>+ x. u x * indicator A x)"
   1.319      using assms
   1.320      by (auto intro!: positive_integral_cmult borel_measurable_indicator)
   1.321    finally show ?thesis .
   1.322 @@ -1459,7 +1461,7 @@
   1.323      (is "_ \<longleftrightarrow> \<mu> ?A = 0")
   1.324  proof -
   1.325    have A: "?A \<in> sets M" using borel by auto
   1.326 -  have u: "positive_integral (\<lambda>x. u x * indicator ?A x) = positive_integral u"
   1.327 +  have u: "(\<integral>\<^isup>+ x. u x * indicator ?A x) = positive_integral u"
   1.328      by (auto intro!: positive_integral_cong simp: indicator_def)
   1.329  
   1.330    show ?thesis
   1.331 @@ -1467,7 +1469,7 @@
   1.332      assume "\<mu> ?A = 0"
   1.333      hence "?A \<in> null_sets" using `?A \<in> sets M` by auto
   1.334      from positive_integral_null_set[OF this]
   1.335 -    have "0 = positive_integral (\<lambda>x. u x * indicator ?A x)" by simp
   1.336 +    have "0 = (\<integral>\<^isup>+ x. u x * indicator ?A x)" by simp
   1.337      thus "positive_integral u = 0" unfolding u by simp
   1.338    next
   1.339      assume *: "positive_integral u = 0"
   1.340 @@ -1507,7 +1509,7 @@
   1.341  
   1.342  lemma (in measure_space) positive_integral_restricted:
   1.343    assumes "A \<in> sets M"
   1.344 -  shows "measure_space.positive_integral (restricted_space A) \<mu> f = positive_integral (\<lambda>x. f x * indicator A x)"
   1.345 +  shows "measure_space.positive_integral (restricted_space A) \<mu> f = (\<integral>\<^isup>+ x. f x * indicator A x)"
   1.346      (is "measure_space.positive_integral ?R \<mu> f = positive_integral ?f")
   1.347  proof -
   1.348    have msR: "measure_space ?R \<mu>" by (rule restricted_measure_space[OF `A \<in> sets M`])
   1.349 @@ -1524,7 +1526,7 @@
   1.350      fix g assume "simple_function (\<lambda>x. g x * indicator A x)"
   1.351        "g \<le> f"
   1.352      then show "\<exists>x. simple_function x \<and> x \<le> (\<lambda>x. f x * indicator A x) \<and>
   1.353 -      simple_integral (\<lambda>x. g x * indicator A x) = simple_integral x"
   1.354 +      (\<integral>\<^isup>Sx. g x * indicator A x) = simple_integral x"
   1.355        apply (rule_tac exI[of _ "\<lambda>x. g x * indicator A x"])
   1.356        by (auto simp: indicator_def le_fun_def)
   1.357    next
   1.358 @@ -1560,20 +1562,18 @@
   1.359  
   1.360  definition (in measure_space) integrable where
   1.361    "integrable f \<longleftrightarrow> f \<in> borel_measurable M \<and>
   1.362 -    positive_integral (\<lambda>x. Real (f x)) \<noteq> \<omega> \<and>
   1.363 -    positive_integral (\<lambda>x. Real (- f x)) \<noteq> \<omega>"
   1.364 +    (\<integral>\<^isup>+ x. Real (f x)) \<noteq> \<omega> \<and>
   1.365 +    (\<integral>\<^isup>+ x. Real (- f x)) \<noteq> \<omega>"
   1.366  
   1.367  lemma (in measure_space) integrableD[dest]:
   1.368    assumes "integrable f"
   1.369    shows "f \<in> borel_measurable M"
   1.370 -  "positive_integral (\<lambda>x. Real (f x)) \<noteq> \<omega>"
   1.371 -  "positive_integral (\<lambda>x. Real (- f x)) \<noteq> \<omega>"
   1.372 +  "(\<integral>\<^isup>+ x. Real (f x)) \<noteq> \<omega>"
   1.373 +  "(\<integral>\<^isup>+ x. Real (- f x)) \<noteq> \<omega>"
   1.374    using assms unfolding integrable_def by auto
   1.375  
   1.376 -definition (in measure_space) integral where
   1.377 -  "integral f =
   1.378 -    real (positive_integral (\<lambda>x. Real (f x))) -
   1.379 -    real (positive_integral (\<lambda>x. Real (- f x)))"
   1.380 +definition (in measure_space) integral (binder "\<integral> " 10) where
   1.381 +  "integral f = real ((\<integral>\<^isup>+ x. Real (f x))) - real ((\<integral>\<^isup>+ x. Real (- f x)))"
   1.382  
   1.383  lemma (in measure_space) integral_cong:
   1.384    assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
   1.385 @@ -1609,7 +1609,7 @@
   1.386  
   1.387  lemma (in measure_space) integral_eq_positive_integral:
   1.388    assumes "\<And>x. 0 \<le> f x"
   1.389 -  shows "integral f = real (positive_integral (\<lambda>x. Real (f x)))"
   1.390 +  shows "integral f = real ((\<integral>\<^isup>+ x. Real (f x)))"
   1.391  proof -
   1.392    have "\<And>x. Real (- f x) = 0" using assms by simp
   1.393    thus ?thesis by (simp del: Real_eq_0 add: integral_def)
   1.394 @@ -1617,7 +1617,7 @@
   1.395  
   1.396  lemma (in measure_space) integral_vimage_inv:
   1.397    assumes f: "bij_betw f S (space M)"
   1.398 -  shows "measure_space.integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g x) = integral (\<lambda>x. g (the_inv_into S f x))"
   1.399 +  shows "measure_space.integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g x) = (\<integral>x. g (the_inv_into S f x))"
   1.400  proof -
   1.401    interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
   1.402      using f by (rule measure_space_isomorphic)
   1.403 @@ -1634,7 +1634,7 @@
   1.404  
   1.405  lemma (in measure_space) integral_minus[intro, simp]:
   1.406    assumes "integrable f"
   1.407 -  shows "integrable (\<lambda>x. - f x)" "integral (\<lambda>x. - f x) = - integral f"
   1.408 +  shows "integrable (\<lambda>x. - f x)" "(\<integral>x. - f x) = - integral f"
   1.409    using assms by (auto simp: integrable_def integral_def)
   1.410  
   1.411  lemma (in measure_space) integral_of_positive_diff:
   1.412 @@ -1685,7 +1685,7 @@
   1.413  lemma (in measure_space) integral_linear:
   1.414    assumes "integrable f" "integrable g" and "0 \<le> a"
   1.415    shows "integrable (\<lambda>t. a * f t + g t)"
   1.416 -  and "integral (\<lambda>t. a * f t + g t) = a * integral f + integral g"
   1.417 +  and "(\<integral> t. a * f t + g t) = a * integral f + integral g"
   1.418  proof -
   1.419    let ?PI = positive_integral
   1.420    let "?f x" = "Real (f x)"
   1.421 @@ -1718,7 +1718,7 @@
   1.422  
   1.423    show "integrable (\<lambda>t. a * f t + g t)" by (rule diff)
   1.424  
   1.425 -  from assms show "integral (\<lambda>t. a * f t + g t) = a * integral f + integral g"
   1.426 +  from assms show "(\<integral> t. a * f t + g t) = a * integral f + integral g"
   1.427      unfolding diff(2) unfolding integral_def * linear integrable_def
   1.428      by (cases "?PI ?f", cases "?PI ?mf", cases "?PI ?g", cases "?PI ?mg")
   1.429         (auto simp add: field_simps zero_le_mult_iff)
   1.430 @@ -1727,21 +1727,21 @@
   1.431  lemma (in measure_space) integral_add[simp, intro]:
   1.432    assumes "integrable f" "integrable g"
   1.433    shows "integrable (\<lambda>t. f t + g t)"
   1.434 -  and "integral (\<lambda>t. f t + g t) = integral f + integral g"
   1.435 +  and "(\<integral> t. f t + g t) = integral f + integral g"
   1.436    using assms integral_linear[where a=1] by auto
   1.437  
   1.438  lemma (in measure_space) integral_zero[simp, intro]:
   1.439    shows "integrable (\<lambda>x. 0)"
   1.440 -  and "integral (\<lambda>x. 0) = 0"
   1.441 +  and "(\<integral> x.0) = 0"
   1.442    unfolding integrable_def integral_def
   1.443    by (auto simp add: borel_measurable_const)
   1.444  
   1.445  lemma (in measure_space) integral_cmult[simp, intro]:
   1.446    assumes "integrable f"
   1.447    shows "integrable (\<lambda>t. a * f t)" (is ?P)
   1.448 -  and "integral (\<lambda>t. a * f t) = a * integral f" (is ?I)
   1.449 +  and "(\<integral> t. a * f t) = a * integral f" (is ?I)
   1.450  proof -
   1.451 -  have "integrable (\<lambda>t. a * f t) \<and> integral (\<lambda>t. a * f t) = a * integral f"
   1.452 +  have "integrable (\<lambda>t. a * f t) \<and> (\<integral> t. a * f t) = a * integral f"
   1.453    proof (cases rule: le_cases)
   1.454      assume "0 \<le> a" show ?thesis
   1.455        using integral_linear[OF assms integral_zero(1) `0 \<le> a`]
   1.456 @@ -1758,7 +1758,7 @@
   1.457  
   1.458  lemma (in measure_space) integral_multc:
   1.459    assumes "integrable f"
   1.460 -  shows "integral (\<lambda>x. f x * c) = integral f * c"
   1.461 +  shows "(\<integral> x. f x * c) = integral f * c"
   1.462    unfolding mult_commute[of _ c] integral_cmult[OF assms] ..
   1.463  
   1.464  lemma (in measure_space) integral_mono_AE:
   1.465 @@ -1785,7 +1785,7 @@
   1.466  lemma (in measure_space) integral_diff[simp, intro]:
   1.467    assumes f: "integrable f" and g: "integrable g"
   1.468    shows "integrable (\<lambda>t. f t - g t)"
   1.469 -  and "integral (\<lambda>t. f t - g t) = integral f - integral g"
   1.470 +  and "(\<integral> t. f t - g t) = integral f - integral g"
   1.471    using integral_add[OF f integral_minus(1)[OF g]]
   1.472    unfolding diff_minus integral_minus(2)[OF g]
   1.473    by auto
   1.474 @@ -1806,7 +1806,7 @@
   1.475  lemma (in measure_space) integral_cmul_indicator:
   1.476    assumes "A \<in> sets M" and "c \<noteq> 0 \<Longrightarrow> \<mu> A \<noteq> \<omega>"
   1.477    shows "integrable (\<lambda>x. c * indicator A x)" (is ?P)
   1.478 -  and "integral (\<lambda>x. c * indicator A x) = c * real (\<mu> A)" (is ?I)
   1.479 +  and "(\<integral>x. c * indicator A x) = c * real (\<mu> A)" (is ?I)
   1.480  proof -
   1.481    show ?P
   1.482    proof (cases "c = 0")
   1.483 @@ -1821,7 +1821,7 @@
   1.484  
   1.485  lemma (in measure_space) integral_setsum[simp, intro]:
   1.486    assumes "\<And>n. n \<in> S \<Longrightarrow> integrable (f n)"
   1.487 -  shows "integral (\<lambda>x. \<Sum> i \<in> S. f i x) = (\<Sum> i \<in> S. integral (f i))" (is "?int S")
   1.488 +  shows "(\<integral>x. \<Sum> i \<in> S. f i x) = (\<Sum> i \<in> S. integral (f i))" (is "?int S")
   1.489      and "integrable (\<lambda>x. \<Sum> i \<in> S. f i x)" (is "?I S")
   1.490  proof -
   1.491    have "?int S \<and> ?I S"
   1.492 @@ -1854,21 +1854,21 @@
   1.493    assumes borel: "g \<in> borel_measurable M"
   1.494    shows "integrable g"
   1.495  proof -
   1.496 -  have "positive_integral (\<lambda>x. Real (g x)) \<le> positive_integral (\<lambda>x. Real \<bar>g x\<bar>)"
   1.497 +  have "(\<integral>\<^isup>+ x. Real (g x)) \<le> (\<integral>\<^isup>+ x. Real \<bar>g x\<bar>)"
   1.498      by (auto intro!: positive_integral_mono)
   1.499 -  also have "\<dots> \<le> positive_integral (\<lambda>x. Real (f x))"
   1.500 +  also have "\<dots> \<le> (\<integral>\<^isup>+ x. Real (f x))"
   1.501      using f by (auto intro!: positive_integral_mono)
   1.502    also have "\<dots> < \<omega>"
   1.503      using `integrable f` unfolding integrable_def by (auto simp: pextreal_less_\<omega>)
   1.504 -  finally have pos: "positive_integral (\<lambda>x. Real (g x)) < \<omega>" .
   1.505 +  finally have pos: "(\<integral>\<^isup>+ x. Real (g x)) < \<omega>" .
   1.506  
   1.507 -  have "positive_integral (\<lambda>x. Real (- g x)) \<le> positive_integral (\<lambda>x. Real (\<bar>g x\<bar>))"
   1.508 +  have "(\<integral>\<^isup>+ x. Real (- g x)) \<le> (\<integral>\<^isup>+ x. Real (\<bar>g x\<bar>))"
   1.509      by (auto intro!: positive_integral_mono)
   1.510 -  also have "\<dots> \<le> positive_integral (\<lambda>x. Real (f x))"
   1.511 +  also have "\<dots> \<le> (\<integral>\<^isup>+ x. Real (f x))"
   1.512      using f by (auto intro!: positive_integral_mono)
   1.513    also have "\<dots> < \<omega>"
   1.514      using `integrable f` unfolding integrable_def by (auto simp: pextreal_less_\<omega>)
   1.515 -  finally have neg: "positive_integral (\<lambda>x. Real (- g x)) < \<omega>" .
   1.516 +  finally have neg: "(\<integral>\<^isup>+ x. Real (- g x)) < \<omega>" .
   1.517  
   1.518    from neg pos borel show ?thesis
   1.519      unfolding integrable_def by auto
   1.520 @@ -1908,10 +1908,10 @@
   1.521  
   1.522  lemma (in measure_space) integral_triangle_inequality:
   1.523    assumes "integrable f"
   1.524 -  shows "\<bar>integral f\<bar> \<le> integral (\<lambda>x. \<bar>f x\<bar>)"
   1.525 +  shows "\<bar>integral f\<bar> \<le> (\<integral>x. \<bar>f x\<bar>)"
   1.526  proof -
   1.527    have "\<bar>integral f\<bar> = max (integral f) (- integral f)" by auto
   1.528 -  also have "\<dots> \<le> integral (\<lambda>x. \<bar>f x\<bar>)"
   1.529 +  also have "\<dots> \<le> (\<integral>x. \<bar>f x\<bar>)"
   1.530        using assms integral_minus(2)[of f, symmetric]
   1.531        by (auto intro!: integral_mono integrable_abs simp del: integral_minus)
   1.532    finally show ?thesis .
   1.533 @@ -1921,7 +1921,7 @@
   1.534    assumes "integrable f" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
   1.535    shows "0 \<le> integral f"
   1.536  proof -
   1.537 -  have "0 = integral (\<lambda>x. 0)" by (auto simp: integral_zero)
   1.538 +  have "0 = (\<integral>x. 0)" by (auto simp: integral_zero)
   1.539    also have "\<dots> \<le> integral f"
   1.540      using assms by (rule integral_mono[OF integral_zero(1)])
   1.541    finally show ?thesis .
   1.542 @@ -1953,7 +1953,7 @@
   1.543    hence borel_u: "u \<in> borel_measurable M"
   1.544      using pos_u by (auto simp: borel_measurable_Real_eq SUP_F)
   1.545  
   1.546 -  have integral_eq: "\<And>n. positive_integral (\<lambda>x. Real (f n x)) = Real (integral (f n))"
   1.547 +  have integral_eq: "\<And>n. (\<integral>\<^isup>+ x. Real (f n x)) = Real (integral (f n))"
   1.548      using i unfolding integral_def integrable_def by (auto simp: Real_real)
   1.549  
   1.550    have pos_integral: "\<And>n. 0 \<le> integral (f n)"
   1.551 @@ -1961,14 +1961,14 @@
   1.552    hence "0 \<le> x"
   1.553      using LIMSEQ_le_const[OF ilim, of 0] by auto
   1.554  
   1.555 -  have "(\<lambda>i. positive_integral (\<lambda>x. Real (f i x))) \<up> positive_integral (\<lambda>x. Real (u x))"
   1.556 +  have "(\<lambda>i. (\<integral>\<^isup>+ x. Real (f i x))) \<up> (\<integral>\<^isup>+ x. Real (u x))"
   1.557    proof (rule positive_integral_isoton)
   1.558      from SUP_F mono pos
   1.559      show "(\<lambda>i x. Real (f i x)) \<up> (\<lambda>x. Real (u x))"
   1.560        unfolding isoton_fun_expand by (auto simp: isoton_def mono_def)
   1.561    qed (rule borel_f)
   1.562 -  hence pI: "positive_integral (\<lambda>x. Real (u x)) =
   1.563 -      (SUP n. positive_integral (\<lambda>x. Real (f n x)))"
   1.564 +  hence pI: "(\<integral>\<^isup>+ x. Real (u x)) =
   1.565 +      (SUP n. (\<integral>\<^isup>+ x. Real (f n x)))"
   1.566      unfolding isoton_def by simp
   1.567    also have "\<dots> = Real x" unfolding integral_eq
   1.568    proof (rule SUP_eq_LIMSEQ[THEN iffD2])
   1.569 @@ -1997,7 +1997,7 @@
   1.570        unfolding mono_def le_fun_def by (auto simp: field_simps)
   1.571    have 4: "\<And>x. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x"
   1.572      using lim by (auto intro!: LIMSEQ_diff)
   1.573 -  have 5: "(\<lambda>i. integral (\<lambda>x. f i x - f 0 x)) ----> x - integral (f 0)"
   1.574 +  have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x)) ----> x - integral (f 0)"
   1.575      using f ilim by (auto intro!: LIMSEQ_diff simp: integral_diff)
   1.576    note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5]
   1.577    have "integrable (\<lambda>x. (u x - f 0 x) + f 0 x)"
   1.578 @@ -2008,12 +2008,12 @@
   1.579  
   1.580  lemma (in measure_space) integral_0_iff:
   1.581    assumes "integrable f"
   1.582 -  shows "integral (\<lambda>x. \<bar>f x\<bar>) = 0 \<longleftrightarrow> \<mu> {x\<in>space M. f x \<noteq> 0} = 0"
   1.583 +  shows "(\<integral>x. \<bar>f x\<bar>) = 0 \<longleftrightarrow> \<mu> {x\<in>space M. f x \<noteq> 0} = 0"
   1.584  proof -
   1.585    have *: "\<And>x. Real (- \<bar>f x\<bar>) = 0" by auto
   1.586    have "integrable (\<lambda>x. \<bar>f x\<bar>)" using assms by (rule integrable_abs)
   1.587    hence "(\<lambda>x. Real (\<bar>f x\<bar>)) \<in> borel_measurable M"
   1.588 -    "positive_integral (\<lambda>x. Real \<bar>f x\<bar>) \<noteq> \<omega>" unfolding integrable_def by auto
   1.589 +    "(\<integral>\<^isup>+ x. Real \<bar>f x\<bar>) \<noteq> \<omega>" unfolding integrable_def by auto
   1.590    from positive_integral_0_iff[OF this(1)] this(2)
   1.591    show ?thesis unfolding integral_def *
   1.592      by (simp add: real_of_pextreal_eq_0)
   1.593 @@ -2024,7 +2024,7 @@
   1.594    and "positive_integral f \<noteq> \<omega>"
   1.595    shows "\<mu> (f -` {\<omega>} \<inter> space M) = 0"
   1.596  proof -
   1.597 -  have "\<omega> * \<mu> (f -` {\<omega>} \<inter> space M) = positive_integral (\<lambda>x. \<omega> * indicator (f -` {\<omega>} \<inter> space M) x)"
   1.598 +  have "\<omega> * \<mu> (f -` {\<omega>} \<inter> space M) = (\<integral>\<^isup>+ x. \<omega> * indicator (f -` {\<omega>} \<inter> space M) x)"
   1.599      using positive_integral_cmult_indicator[OF borel_measurable_vimage, OF assms(1), of \<omega> \<omega>] by simp
   1.600    also have "\<dots> \<le> positive_integral f"
   1.601      by (auto intro!: positive_integral_mono simp: indicator_def)
   1.602 @@ -2054,15 +2054,15 @@
   1.603  lemma (in measure_space) integral_real:
   1.604    fixes f :: "'a \<Rightarrow> pextreal"
   1.605    assumes "AE x. f x \<noteq> \<omega>"
   1.606 -  shows "integral (\<lambda>x. real (f x)) = real (positive_integral f)" (is ?plus)
   1.607 -    and "integral (\<lambda>x. - real (f x)) = - real (positive_integral f)" (is ?minus)
   1.608 +  shows "(\<integral>x. real (f x)) = real (positive_integral f)" (is ?plus)
   1.609 +    and "(\<integral>x. - real (f x)) = - real (positive_integral f)" (is ?minus)
   1.610  proof -
   1.611 -  have "positive_integral (\<lambda>x. Real (real (f x))) = positive_integral f"
   1.612 +  have "(\<integral>\<^isup>+ x. Real (real (f x))) = positive_integral f"
   1.613      apply (rule positive_integral_cong_AE)
   1.614      apply (rule AE_mp[OF assms(1)])
   1.615      by (auto intro!: AE_cong simp: Real_real)
   1.616    moreover
   1.617 -  have "positive_integral (\<lambda>x. Real (- real (f x))) = positive_integral (\<lambda>x. 0)"
   1.618 +  have "(\<integral>\<^isup>+ x. Real (- real (f x))) = (\<integral>\<^isup>+ x. 0)"
   1.619      by (intro positive_integral_cong) auto
   1.620    ultimately show ?plus ?minus
   1.621      by (auto simp: integral_def integrable_def)
   1.622 @@ -2073,7 +2073,7 @@
   1.623    and w: "integrable w" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> w x"
   1.624    and u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
   1.625    shows "integrable u'"
   1.626 -  and "(\<lambda>i. integral (\<lambda>x. \<bar>u i x - u' x\<bar>)) ----> 0" (is "?lim_diff")
   1.627 +  and "(\<lambda>i. (\<integral>x. \<bar>u i x - u' x\<bar>)) ----> 0" (is "?lim_diff")
   1.628    and "(\<lambda>i. integral (u i)) ----> integral u'" (is ?lim)
   1.629  proof -
   1.630    { fix x j assume x: "x \<in> space M"
   1.631 @@ -2108,31 +2108,31 @@
   1.632      finally have "\<bar>u j x - u' x\<bar> \<le> 2 * w x" by simp }
   1.633    note diff_less_2w = this
   1.634  
   1.635 -  have PI_diff: "\<And>m n. positive_integral (\<lambda>x. Real (?diff (m + n) x)) =
   1.636 -    positive_integral (\<lambda>x. Real (2 * w x)) - positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>)"
   1.637 +  have PI_diff: "\<And>m n. (\<integral>\<^isup>+ x. Real (?diff (m + n) x)) =
   1.638 +    (\<integral>\<^isup>+ x. Real (2 * w x)) - (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar>)"
   1.639      using diff w diff_less_2w
   1.640      by (subst positive_integral_diff[symmetric])
   1.641         (auto simp: integrable_def intro!: positive_integral_cong)
   1.642  
   1.643    have "integrable (\<lambda>x. 2 * w x)"
   1.644      using w by (auto intro: integral_cmult)
   1.645 -  hence I2w_fin: "positive_integral (\<lambda>x. Real (2 * w x)) \<noteq> \<omega>" and
   1.646 +  hence I2w_fin: "(\<integral>\<^isup>+ x. Real (2 * w x)) \<noteq> \<omega>" and
   1.647      borel_2w: "(\<lambda>x. Real (2 * w x)) \<in> borel_measurable M"
   1.648      unfolding integrable_def by auto
   1.649  
   1.650 -  have "(INF n. SUP m. positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>)) = 0" (is "?lim_SUP = 0")
   1.651 +  have "(INF n. SUP m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar>)) = 0" (is "?lim_SUP = 0")
   1.652    proof cases
   1.653 -    assume eq_0: "positive_integral (\<lambda>x. Real (2 * w x)) = 0"
   1.654 -    have "\<And>i. positive_integral (\<lambda>x. Real \<bar>u i x - u' x\<bar>) \<le> positive_integral (\<lambda>x. Real (2 * w x))"
   1.655 +    assume eq_0: "(\<integral>\<^isup>+ x. Real (2 * w x)) = 0"
   1.656 +    have "\<And>i. (\<integral>\<^isup>+ x. Real \<bar>u i x - u' x\<bar>) \<le> (\<integral>\<^isup>+ x. Real (2 * w x))"
   1.657      proof (rule positive_integral_mono)
   1.658        fix i x assume "x \<in> space M" from diff_less_2w[OF this, of i]
   1.659        show "Real \<bar>u i x - u' x\<bar> \<le> Real (2 * w x)" by auto
   1.660      qed
   1.661 -    hence "\<And>i. positive_integral (\<lambda>x. Real \<bar>u i x - u' x\<bar>) = 0" using eq_0 by auto
   1.662 +    hence "\<And>i. (\<integral>\<^isup>+ x. Real \<bar>u i x - u' x\<bar>) = 0" using eq_0 by auto
   1.663      thus ?thesis by simp
   1.664    next
   1.665 -    assume neq_0: "positive_integral (\<lambda>x. Real (2 * w x)) \<noteq> 0"
   1.666 -    have "positive_integral (\<lambda>x. Real (2 * w x)) = positive_integral (\<lambda>x. SUP n. INF m. Real (?diff (m + n) x))"
   1.667 +    assume neq_0: "(\<integral>\<^isup>+ x. Real (2 * w x)) \<noteq> 0"
   1.668 +    have "(\<integral>\<^isup>+ x. Real (2 * w x)) = (\<integral>\<^isup>+ x. SUP n. INF m. Real (?diff (m + n) x))"
   1.669      proof (rule positive_integral_cong, subst add_commute)
   1.670        fix x assume x: "x \<in> space M"
   1.671        show "Real (2 * w x) = (SUP n. INF m. Real (?diff (n + m) x))"
   1.672 @@ -2144,22 +2144,22 @@
   1.673          thus "(\<lambda>i. ?diff i x) ----> 2 * w x" by simp
   1.674        qed
   1.675      qed
   1.676 -    also have "\<dots> \<le> (SUP n. INF m. positive_integral (\<lambda>x. Real (?diff (m + n) x)))"
   1.677 +    also have "\<dots> \<le> (SUP n. INF m. (\<integral>\<^isup>+ x. Real (?diff (m + n) x)))"
   1.678        using u'_borel w u unfolding integrable_def
   1.679        by (auto intro!: positive_integral_lim_INF)
   1.680 -    also have "\<dots> = positive_integral (\<lambda>x. Real (2 * w x)) -
   1.681 -        (INF n. SUP m. positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>))"
   1.682 +    also have "\<dots> = (\<integral>\<^isup>+ x. Real (2 * w x)) -
   1.683 +        (INF n. SUP m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar>))"
   1.684        unfolding PI_diff pextreal_INF_minus[OF I2w_fin] pextreal_SUP_minus ..
   1.685      finally show ?thesis using neq_0 I2w_fin by (rule pextreal_le_minus_imp_0)
   1.686    qed
   1.687  
   1.688    have [simp]: "\<And>n m x. Real (- \<bar>u (m + n) x - u' x\<bar>) = 0" by auto
   1.689  
   1.690 -  have [simp]: "\<And>n m. positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>) =
   1.691 -    Real (integral (\<lambda>x. \<bar>u (n + m) x - u' x\<bar>))"
   1.692 +  have [simp]: "\<And>n m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar>) =
   1.693 +    Real ((\<integral>x. \<bar>u (n + m) x - u' x\<bar>))"
   1.694      using diff by (subst add_commute) (simp add: integral_def integrable_def Real_real)
   1.695  
   1.696 -  have "(SUP n. INF m. positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>)) \<le> ?lim_SUP"
   1.697 +  have "(SUP n. INF m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar>)) \<le> ?lim_SUP"
   1.698      (is "?lim_INF \<le> _") by (subst (1 2) add_commute) (rule lim_INF_le_lim_SUP)
   1.699    hence "?lim_INF = Real 0" "?lim_SUP = Real 0" using `?lim_SUP = 0` by auto
   1.700    thus ?lim_diff using diff by (auto intro!: integral_positive lim_INF_eq_lim_SUP)
   1.701 @@ -2168,15 +2168,15 @@
   1.702    proof (rule LIMSEQ_I)
   1.703      fix r :: real assume "0 < r"
   1.704      from LIMSEQ_D[OF `?lim_diff` this]
   1.705 -    obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> integral (\<lambda>x. \<bar>u n x - u' x\<bar>) < r"
   1.706 +    obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> (\<integral>x. \<bar>u n x - u' x\<bar>) < r"
   1.707        using diff by (auto simp: integral_positive)
   1.708  
   1.709      show "\<exists>N. \<forall>n\<ge>N. norm (integral (u n) - integral u') < r"
   1.710      proof (safe intro!: exI[of _ N])
   1.711        fix n assume "N \<le> n"
   1.712 -      have "\<bar>integral (u n) - integral u'\<bar> = \<bar>integral (\<lambda>x. u n x - u' x)\<bar>"
   1.713 +      have "\<bar>integral (u n) - integral u'\<bar> = \<bar>(\<integral>x. u n x - u' x)\<bar>"
   1.714          using u `integrable u'` by (auto simp: integral_diff)
   1.715 -      also have "\<dots> \<le> integral (\<lambda>x. \<bar>u n x - u' x\<bar>)" using u `integrable u'`
   1.716 +      also have "\<dots> \<le> (\<integral>x. \<bar>u n x - u' x\<bar>)" using u `integrable u'`
   1.717          by (rule_tac integral_triangle_inequality) (auto intro!: integral_diff)
   1.718        also note N[OF `N \<le> n`]
   1.719        finally show "norm (integral (u n) - integral u') < r" by simp
   1.720 @@ -2187,9 +2187,9 @@
   1.721  lemma (in measure_space) integral_sums:
   1.722    assumes borel: "\<And>i. integrable (f i)"
   1.723    and summable: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>f i x\<bar>)"
   1.724 -  and sums: "summable (\<lambda>i. integral (\<lambda>x. \<bar>f i x\<bar>))"
   1.725 +  and sums: "summable (\<lambda>i. (\<integral>x. \<bar>f i x\<bar>))"
   1.726    shows "integrable (\<lambda>x. (\<Sum>i. f i x))" (is "integrable ?S")
   1.727 -  and "(\<lambda>i. integral (f i)) sums integral (\<lambda>x. (\<Sum>i. f i x))" (is ?integral)
   1.728 +  and "(\<lambda>i. integral (f i)) sums (\<integral>x. (\<Sum>i. f i x))" (is ?integral)
   1.729  proof -
   1.730    have "\<forall>x\<in>space M. \<exists>w. (\<lambda>i. \<bar>f i x\<bar>) sums w"
   1.731      using summable unfolding summable_def by auto
   1.732 @@ -2198,7 +2198,7 @@
   1.733  
   1.734    let "?w y" = "if y \<in> space M then w y else 0"
   1.735  
   1.736 -  obtain x where abs_sum: "(\<lambda>i. integral (\<lambda>x. \<bar>f i x\<bar>)) sums x"
   1.737 +  obtain x where abs_sum: "(\<lambda>i. (\<integral>x. \<bar>f i x\<bar>)) sums x"
   1.738      using sums unfolding summable_def ..
   1.739  
   1.740    have 1: "\<And>n. integrable (\<lambda>x. \<Sum>i = 0..<n. f i x)"
   1.741 @@ -2221,7 +2221,7 @@
   1.742        by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
   1.743      { fix x show "(\<lambda>n. ?w' n x) ----> ?w x"
   1.744          using w by (cases "x \<in> space M") (simp_all add: LIMSEQ_const sums_def) }
   1.745 -    have *: "\<And>n. integral (?w' n) = (\<Sum>i = 0..< n. integral (\<lambda>x. \<bar>f i x\<bar>))"
   1.746 +    have *: "\<And>n. integral (?w' n) = (\<Sum>i = 0..< n. (\<integral>x. \<bar>f i x\<bar>))"
   1.747        using borel by (simp add: integral_setsum integrable_abs cong: integral_cong)
   1.748      from abs_sum
   1.749      show "(\<lambda>i. integral (?w' i)) ----> x" unfolding * sums_def .
   1.750 @@ -2275,15 +2275,15 @@
   1.751        by (auto intro!: sums_single simp: F F_abs) }
   1.752    note F_sums_f = this(1) and F_abs_sums_f = this(2)
   1.753  
   1.754 -  have int_f: "integral f = integral (\<lambda>x. \<Sum>r. ?F r x)" "integrable f = integrable (\<lambda>x. \<Sum>r. ?F r x)"
   1.755 +  have int_f: "integral f = (\<integral>x. \<Sum>r. ?F r x)" "integrable f = integrable (\<lambda>x. \<Sum>r. ?F r x)"
   1.756      using F_sums_f by (auto intro!: integral_cong integrable_cong simp: sums_iff)
   1.757  
   1.758    { fix r
   1.759 -    have "integral (\<lambda>x. \<bar>?F r x\<bar>) = integral (\<lambda>x. \<bar>enum r\<bar> * indicator (?A r) x)"
   1.760 +    have "(\<integral>x. \<bar>?F r x\<bar>) = (\<integral>x. \<bar>enum r\<bar> * indicator (?A r) x)"
   1.761        by (auto simp: indicator_def intro!: integral_cong)
   1.762      also have "\<dots> = \<bar>enum r\<bar> * real (\<mu> (?A r))"
   1.763        using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator)
   1.764 -    finally have "integral (\<lambda>x. \<bar>?F r x\<bar>) = \<bar>enum r * real (\<mu> (?A r))\<bar>"
   1.765 +    finally have "(\<integral>x. \<bar>?F r x\<bar>) = \<bar>enum r * real (\<mu> (?A r))\<bar>"
   1.766        by (simp add: abs_mult_pos real_pextreal_pos) }
   1.767    note int_abs_F = this
   1.768  
   1.769 @@ -2306,7 +2306,7 @@
   1.770    assumes f: "f \<in> borel_measurable M" and finite: "finite (f`space M)"
   1.771    and fin: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<omega>"
   1.772    shows "integrable f"
   1.773 -  and "integral (\<lambda>x. f x) =
   1.774 +  and "(\<integral>x. f x) =
   1.775      (\<Sum> r \<in> f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))" (is "?integral")
   1.776  proof -
   1.777    let "?A r" = "f -` {r} \<inter> space M"
   1.778 @@ -2336,7 +2336,7 @@
   1.779  lemma (in finite_measure_space) positive_integral_finite_eq_setsum:
   1.780    "positive_integral f = (\<Sum>x \<in> space M. f x * \<mu> {x})"
   1.781  proof -
   1.782 -  have *: "positive_integral f = positive_integral (\<lambda>x. \<Sum>y\<in>space M. f y * indicator {y} x)"
   1.783 +  have *: "positive_integral f = (\<integral>\<^isup>+ x. \<Sum>y\<in>space M. f y * indicator {y} x)"
   1.784      by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space])
   1.785    show ?thesis unfolding * using borel_measurable_finite[of f]
   1.786      by (simp add: positive_integral_setsum positive_integral_cmult_indicator)
   1.787 @@ -2347,8 +2347,8 @@
   1.788    and "integral f = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))" (is ?I)
   1.789  proof -
   1.790    have [simp]:
   1.791 -    "positive_integral (\<lambda>x. Real (f x)) = (\<Sum>x \<in> space M. Real (f x) * \<mu> {x})"
   1.792 -    "positive_integral (\<lambda>x. Real (- f x)) = (\<Sum>x \<in> space M. Real (- f x) * \<mu> {x})"
   1.793 +    "(\<integral>\<^isup>+ x. Real (f x)) = (\<Sum>x \<in> space M. Real (f x) * \<mu> {x})"
   1.794 +    "(\<integral>\<^isup>+ x. Real (- f x)) = (\<Sum>x \<in> space M. Real (- f x) * \<mu> {x})"
   1.795      unfolding positive_integral_finite_eq_setsum by auto
   1.796    show "integrable f" using finite_space finite_measure
   1.797      by (simp add: setsum_\<omega> integrable_def)
     2.1 --- a/src/HOL/Probability/Positive_Extended_Real.thy	Fri Jan 14 14:21:26 2011 +0100
     2.2 +++ b/src/HOL/Probability/Positive_Extended_Real.thy	Fri Jan 14 14:21:48 2011 +0100
     2.3 @@ -1603,6 +1603,136 @@
     2.4  qed
     2.5  end
     2.6  
     2.7 +lemma minus_omega[simp]: "x - \<omega> = 0" by (cases x) auto
     2.8 +
     2.9 +lemma open_pextreal_alt: "open A \<longleftrightarrow>
    2.10 +  (\<forall>x\<in>A. \<exists>e>0. {x-e <..< x+e} \<subseteq> A) \<and> (\<omega> \<in> A \<longrightarrow> (\<exists>x\<ge>0. {Real x <..} \<subseteq> A))"
    2.11 +proof -
    2.12 +  have *: "(\<exists>T. open T \<and> (Real ` (T\<inter>{0..}) = A - {\<omega>})) \<longleftrightarrow>
    2.13 +    open (real ` (A - {\<omega>}) \<union> {..<0})"
    2.14 +  proof safe
    2.15 +    fix T assume "open T" and A: "Real ` (T \<inter> {0..}) = A - {\<omega>}"
    2.16 +    have *: "(\<lambda>x. real (Real x)) ` (T \<inter> {0..}) = T \<inter> {0..}"
    2.17 +      by auto
    2.18 +    have **: "T \<inter> {0..} \<union> {..<0} = T \<union> {..<0}" by auto
    2.19 +    show "open (real ` (A - {\<omega>}) \<union> {..<0})"
    2.20 +      unfolding A[symmetric] image_image * ** using `open T` by auto
    2.21 +  next
    2.22 +    assume "open (real ` (A - {\<omega>}) \<union> {..<0})"
    2.23 +    moreover have "Real ` ((real ` (A - {\<omega>}) \<union> {..<0}) \<inter> {0..}) = A - {\<omega>}"
    2.24 +      apply auto
    2.25 +      apply (case_tac xb)
    2.26 +      apply auto
    2.27 +      apply (case_tac x)
    2.28 +      apply (auto simp: image_iff)
    2.29 +      apply (erule_tac x="Real r" in ballE)
    2.30 +      apply auto
    2.31 +      done
    2.32 +    ultimately show "\<exists>T. open T \<and> Real ` (T \<inter> {0..}) = A - {\<omega>}" by auto
    2.33 +  qed
    2.34 +  also have "\<dots> \<longleftrightarrow> (\<forall>x\<in>A. \<exists>e>0. {x-e <..< x+e} \<subseteq> A)"
    2.35 +  proof (intro iffI ballI open_subopen[THEN iffD2])
    2.36 +    fix x assume *: "\<forall>x\<in>A. \<exists>e>0. {x - e<..<x + e} \<subseteq> A" and x: "x \<in> real ` (A - {\<omega>}) \<union> {..<0}"
    2.37 +    show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}"
    2.38 +    proof (cases rule: linorder_cases)
    2.39 +      assume "x < 0" then show ?thesis by (intro exI[of _ "{..<0}"]) auto
    2.40 +    next
    2.41 +      assume "x = 0" with x
    2.42 +      have "0 \<in> A"
    2.43 +        apply auto by (case_tac x) auto
    2.44 +      with * obtain e where "e > 0" "{0 - e<..<0 + e} \<subseteq> A" by auto
    2.45 +      then have "{..<e} \<subseteq> A" using `0 \<in> A`
    2.46 +        apply auto
    2.47 +        apply (case_tac "x = 0")
    2.48 +        by (auto dest!: pextreal_zero_lessI)
    2.49 +      then have *: "{..<e} \<subseteq> A - {\<omega>}" by auto
    2.50 +      def e' \<equiv> "if e = \<omega> then 1 else real e"
    2.51 +      then have "0 < e'" using `e > 0` by (cases e) auto
    2.52 +      have "{0..<e'} \<subseteq> real ` (A - {\<omega>})"
    2.53 +      proof (cases e)
    2.54 +        case infinite
    2.55 +        then have "{..<e} = UNIV - {\<omega>}" by auto
    2.56 +        then have A: "A - {\<omega>} = UNIV - {\<omega>}" using * by auto
    2.57 +        show ?thesis unfolding e'_def infinite A
    2.58 +          apply safe
    2.59 +          apply (rule_tac x="Real x" in image_eqI)
    2.60 +          apply auto
    2.61 +          done
    2.62 +      next
    2.63 +        case (preal r)
    2.64 +        then show ?thesis unfolding e'_def using *
    2.65 +          apply safe
    2.66 +          apply (rule_tac x="Real x" in image_eqI)
    2.67 +          by (auto simp: subset_eq)
    2.68 +      qed
    2.69 +      then have "{0..<e'} \<union> {..<0} \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}" by auto
    2.70 +      moreover have "{0..<e'} \<union> {..<0} = {..<e'}" using `0 < e'` by auto
    2.71 +      ultimately have "{..<e'} \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}" by simp
    2.72 +      then show ?thesis using `0 < e'` `x = 0` by auto
    2.73 +    next
    2.74 +      assume "0 < x"
    2.75 +      with x have "Real x \<in> A" apply auto by (case_tac x) auto
    2.76 +      with * obtain e where "0 < e" and e: "{Real x - e<..<Real x + e} \<subseteq> A" by auto
    2.77 +      show ?thesis
    2.78 +      proof cases
    2.79 +        assume "e < Real x"
    2.80 +        with `0 < e` obtain r where r: "e = Real r" "0 < r" by (cases e) auto
    2.81 +        then have "r < x" using `e < Real x` `0 < e` by (auto split: split_if_asm)
    2.82 +        then have "{x - r <..< x + r} \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}"
    2.83 +          using e unfolding r
    2.84 +          apply (auto simp: subset_eq)
    2.85 +          apply (rule_tac x="Real xa" in image_eqI)
    2.86 +          by auto
    2.87 +        then show ?thesis using `0 < r` by (intro exI[of _ "{x - r <..< x + r}"]) auto
    2.88 +      next
    2.89 +        assume "\<not> e < Real x"
    2.90 +        moreover then have "Real x - e = 0" by (cases e) auto
    2.91 +        moreover have "\<And>z. 0 < z \<Longrightarrow>  z * 2 < 3 * x \<Longrightarrow> Real z < Real x + e"
    2.92 +          using `\<not> e < Real x` by (cases e) auto
    2.93 +        ultimately have "{0 <..< x + x / 2} \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}"
    2.94 +          using e
    2.95 +          apply (auto simp: subset_eq)
    2.96 +          apply (erule_tac x="Real xa" in ballE)
    2.97 +          apply (auto simp: not_less)
    2.98 +          apply (rule_tac x="Real xa" in image_eqI)
    2.99 +          apply auto
   2.100 +          done
   2.101 +        moreover have "x \<in> {0 <..< x + x / 2}" using `0 < x` by auto
   2.102 +        ultimately show ?thesis by (intro exI[of _ "{0 <..< x + x / 2}"]) auto
   2.103 +      qed
   2.104 +    qed
   2.105 +  next
   2.106 +    fix x assume x: "x \<in> A" "open (real ` (A - {\<omega>}) \<union> {..<0})"
   2.107 +    then show "\<exists>e>0. {x - e<..<x + e} \<subseteq> A"
   2.108 +    proof (cases x)
   2.109 +      case infinite then show ?thesis by (intro exI[of _ 2]) auto
   2.110 +    next
   2.111 +      case (preal r)
   2.112 +      with `x \<in> A` have r: "r \<in> real ` (A - {\<omega>}) \<union> {..<0}" by force
   2.113 +      from x(2)[unfolded open_real, THEN bspec, OF r]
   2.114 +      obtain e where e: "0 < e" "\<And>x'. \<bar>x' - r\<bar> < e \<Longrightarrow> x' \<in> real ` (A - {\<omega>}) \<union> {..<0}"
   2.115 +        by auto
   2.116 +      show ?thesis using `0 < e` preal
   2.117 +      proof (auto intro!: exI[of _ "Real e"] simp: greaterThanLessThan_iff not_less 
   2.118 +                  split: split_if_asm)
   2.119 +        fix z assume *: "Real (r - e) < z" "z < Real (r + e)"
   2.120 +        then obtain q where [simp]: "z = Real q" "0 \<le> q" by (cases z) auto
   2.121 +        with * have "r - e < q" "q < r + e" by (auto split: split_if_asm)
   2.122 +        with e(2)[of q] have "q \<in> real ` (A - {\<omega>}) \<union> {..<0}" by auto
   2.123 +        then show "z \<in> A" using `0 \<le> q` apply auto apply (case_tac x) apply auto done
   2.124 +      next
   2.125 +        fix z assume *: "0 < z" "z < Real (r + e)" "r \<le> e"
   2.126 +        then obtain q where [simp]: "z = Real q" and "0 < q" by (cases z) auto
   2.127 +        with * have "q < r + e" by (auto split: split_if_asm)
   2.128 +        moreover have "r - e < q" using `r \<le> e` `0 < q` by auto
   2.129 +        ultimately have "q \<in> real ` (A - {\<omega>}) \<union> {..<0}" using e(2)[of q] by auto
   2.130 +        then show "z \<in> A" using `0 < q` apply auto apply (case_tac x) apply auto done
   2.131 +      qed
   2.132 +    qed
   2.133 +  qed
   2.134 +  finally show ?thesis unfolding open_pextreal_def by simp
   2.135 +qed
   2.136 +
   2.137  lemma open_pextreal_lessThan[simp]:
   2.138    "open {..< a :: pextreal}"
   2.139  proof (cases a)
     3.1 --- a/src/HOL/Probability/Probability_Space.thy	Fri Jan 14 14:21:26 2011 +0100
     3.2 +++ b/src/HOL/Probability/Probability_Space.thy	Fri Jan 14 14:21:48 2011 +0100
     3.3 @@ -957,7 +957,7 @@
     3.4    assumes borel: "X \<in> borel_measurable M"
     3.5    and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
     3.6    shows "\<exists>Y\<in>borel_measurable (M\<lparr> sets := N \<rparr>). \<forall>C\<in>N.
     3.7 -      positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)"
     3.8 +      (\<integral>\<^isup>+x. Y x * indicator C x) = (\<integral>\<^isup>+x. X x * indicator C x)"
     3.9  proof -
    3.10    interpret P: prob_space "M\<lparr> sets := N \<rparr>" \<mu>
    3.11      using prob_space_subalgebra[OF N_subalgebra] .
    3.12 @@ -994,7 +994,7 @@
    3.13  
    3.14  definition (in prob_space)
    3.15    "conditional_expectation N X = (SOME Y. Y\<in>borel_measurable (M\<lparr>sets:=N\<rparr>)
    3.16 -    \<and> (\<forall>C\<in>N. positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)))"
    3.17 +    \<and> (\<forall>C\<in>N. (\<integral>\<^isup>+x. Y x * indicator C x) = (\<integral>\<^isup>+x. X x * indicator C x)))"
    3.18  
    3.19  abbreviation (in prob_space)
    3.20    "conditional_prob N A \<equiv> conditional_expectation N (indicator A)"
    3.21 @@ -1006,8 +1006,8 @@
    3.22    shows borel_measurable_conditional_expectation:
    3.23      "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)"
    3.24    and conditional_expectation: "\<And>C. C \<in> N \<Longrightarrow>
    3.25 -      positive_integral (\<lambda>x. conditional_expectation N X x * indicator C x) =
    3.26 -      positive_integral (\<lambda>x. X x * indicator C x)"
    3.27 +      (\<integral>\<^isup>+x. conditional_expectation N X x * indicator C x) =
    3.28 +      (\<integral>\<^isup>+x. X x * indicator C x)"
    3.29     (is "\<And>C. C \<in> N \<Longrightarrow> ?eq C")
    3.30  proof -
    3.31    note CE = conditional_expectation_exists[OF assms, unfolded Bex_def]
     4.1 --- a/src/HOL/Probability/Product_Measure.thy	Fri Jan 14 14:21:26 2011 +0100
     4.2 +++ b/src/HOL/Probability/Product_Measure.thy	Fri Jan 14 14:21:48 2011 +0100
     4.3 @@ -784,7 +784,7 @@
     4.4    note SUPR_C = this
     4.5    ultimately show "?C f \<in> borel_measurable M1"
     4.6      by (simp cong: measurable_cong)
     4.7 -  have "positive_integral (\<lambda>x. SUP i. F i x) = (SUP i. positive_integral (F i))"
     4.8 +  have "positive_integral (\<lambda>x. (SUP i. F i x)) = (SUP i. positive_integral (F i))"
     4.9      using F_borel F_mono
    4.10      by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric])
    4.11    also have "(SUP i. positive_integral (F i)) =
    4.12 @@ -1935,8 +1935,7 @@
    4.13    proof (unfold integrable_def, intro conjI)
    4.14      show "(\<lambda>x. abs (?f x)) \<in> borel_measurable P"
    4.15        using borel by auto
    4.16 -    have "positive_integral (\<lambda>x. Real (abs (?f x))) =
    4.17 -      positive_integral (\<lambda>x. \<Prod>i\<in>I. Real (abs (f i (x i))))"
    4.18 +    have "positive_integral (\<lambda>x. Real (abs (?f x))) = positive_integral (\<lambda>x. \<Prod>i\<in>I. Real (abs (f i (x i))))"
    4.19        by (simp add: Real_setprod abs_setprod)
    4.20      also have "\<dots> = (\<Prod>i\<in>I. M.positive_integral i (\<lambda>x. Real (abs (f i x))))"
    4.21        using f by (subst product_positive_integral_setprod) auto
     5.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Jan 14 14:21:26 2011 +0100
     5.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Jan 14 14:21:48 2011 +0100
     5.3 @@ -114,7 +114,7 @@
     5.4  qed
     5.5  
     5.6  lemma (in measure_space) density_is_absolutely_continuous:
     5.7 -  assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
     5.8 +  assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
     5.9    shows "absolutely_continuous \<nu>"
    5.10    using assms unfolding absolutely_continuous_def
    5.11    by (simp add: positive_integral_null_set)
    5.12 @@ -289,10 +289,10 @@
    5.13  lemma (in finite_measure) Radon_Nikodym_finite_measure:
    5.14    assumes "finite_measure M \<nu>"
    5.15    assumes "absolutely_continuous \<nu>"
    5.16 -  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
    5.17 +  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
    5.18  proof -
    5.19    interpret M': finite_measure M \<nu> using assms(1) .
    5.20 -  def G \<equiv> "{g \<in> borel_measurable M. \<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A}"
    5.21 +  def G \<equiv> "{g \<in> borel_measurable M. \<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x) \<le> \<nu> A}"
    5.22    have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto
    5.23    hence "G \<noteq> {}" by auto
    5.24    { fix f g assume f: "f \<in> G" and g: "g \<in> G"
    5.25 @@ -308,16 +308,16 @@
    5.26        have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
    5.27          g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
    5.28          by (auto simp: indicator_def max_def)
    5.29 -      hence "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) =
    5.30 -        positive_integral (\<lambda>x. g x * indicator (?A \<inter> A) x) +
    5.31 -        positive_integral (\<lambda>x. f x * indicator ((space M - ?A) \<inter> A) x)"
    5.32 +      hence "(\<integral>\<^isup>+x. max (g x) (f x) * indicator A x) =
    5.33 +        (\<integral>\<^isup>+x. g x * indicator (?A \<inter> A) x) +
    5.34 +        (\<integral>\<^isup>+x. f x * indicator ((space M - ?A) \<inter> A) x)"
    5.35          using f g sets unfolding G_def
    5.36          by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
    5.37        also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
    5.38          using f g sets unfolding G_def by (auto intro!: add_mono)
    5.39        also have "\<dots> = \<nu> A"
    5.40          using M'.measure_additive[OF sets] union by auto
    5.41 -      finally show "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) \<le> \<nu> A" .
    5.42 +      finally show "(\<integral>\<^isup>+x. max (g x) (f x) * indicator A x) \<le> \<nu> A" .
    5.43      qed }
    5.44    note max_in_G = this
    5.45    { fix f g assume  "f \<up> g" and f: "\<And>i. f i \<in> G"
    5.46 @@ -331,17 +331,17 @@
    5.47        hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
    5.48          using f_borel by (auto intro!: borel_measurable_indicator)
    5.49        from positive_integral_isoton[OF isoton_indicator[OF `f \<up> g`] this]
    5.50 -      have SUP: "positive_integral (\<lambda>x. g x * indicator A x) =
    5.51 -          (SUP i. positive_integral (\<lambda>x. f i x * indicator A x))"
    5.52 +      have SUP: "(\<integral>\<^isup>+x. g x * indicator A x) =
    5.53 +          (SUP i. (\<integral>\<^isup>+x. f i x * indicator A x))"
    5.54          unfolding isoton_def by simp
    5.55 -      show "positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A" unfolding SUP
    5.56 +      show "(\<integral>\<^isup>+x. g x * indicator A x) \<le> \<nu> A" unfolding SUP
    5.57          using f `A \<in> sets M` unfolding G_def by (auto intro!: SUP_leI)
    5.58      qed }
    5.59    note SUP_in_G = this
    5.60    let ?y = "SUP g : G. positive_integral g"
    5.61    have "?y \<le> \<nu> (space M)" unfolding G_def
    5.62    proof (safe intro!: SUP_leI)
    5.63 -    fix g assume "\<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A"
    5.64 +    fix g assume "\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x) \<le> \<nu> A"
    5.65      from this[THEN bspec, OF top] show "positive_integral g \<le> \<nu> (space M)"
    5.66        by (simp cong: positive_integral_cong)
    5.67    qed
    5.68 @@ -384,7 +384,7 @@
    5.69        by (auto intro!: SUP_mono positive_integral_mono Max_ge)
    5.70    qed
    5.71    finally have int_f_eq_y: "positive_integral f = ?y" .
    5.72 -  let "?t A" = "\<nu> A - positive_integral (\<lambda>x. f x * indicator A x)"
    5.73 +  let "?t A" = "\<nu> A - (\<integral>\<^isup>+x. f x * indicator A x)"
    5.74    have "finite_measure M ?t"
    5.75    proof
    5.76      show "?t {} = 0" by simp
    5.77 @@ -392,26 +392,26 @@
    5.78      show "countably_additive M ?t" unfolding countably_additive_def
    5.79      proof safe
    5.80        fix A :: "nat \<Rightarrow> 'a set"  assume A: "range A \<subseteq> sets M" "disjoint_family A"
    5.81 -      have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
    5.82 -        = positive_integral (\<lambda>x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))"
    5.83 +      have "(\<Sum>\<^isub>\<infinity> n. (\<integral>\<^isup>+x. f x * indicator (A n) x))
    5.84 +        = (\<integral>\<^isup>+x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))"
    5.85          using `range A \<subseteq> sets M`
    5.86          by (rule_tac positive_integral_psuminf[symmetric]) (auto intro!: borel_measurable_indicator)
    5.87 -      also have "\<dots> = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)"
    5.88 +      also have "\<dots> = (\<integral>\<^isup>+x. f x * indicator (\<Union>n. A n) x)"
    5.89          apply (rule positive_integral_cong)
    5.90          apply (subst psuminf_cmult_right)
    5.91          unfolding psuminf_indicator[OF `disjoint_family A`] ..
    5.92 -      finally have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
    5.93 -        = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)" .
    5.94 +      finally have "(\<Sum>\<^isub>\<infinity> n. (\<integral>\<^isup>+x. f x * indicator (A n) x))
    5.95 +        = (\<integral>\<^isup>+x. f x * indicator (\<Union>n. A n) x)" .
    5.96        moreover have "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
    5.97          using M'.measure_countably_additive A by (simp add: comp_def)
    5.98 -      moreover have "\<And>i. positive_integral (\<lambda>x. f x * indicator (A i) x) \<le> \<nu> (A i)"
    5.99 +      moreover have "\<And>i. (\<integral>\<^isup>+x. f x * indicator (A i) x) \<le> \<nu> (A i)"
   5.100            using A `f \<in> G` unfolding G_def by auto
   5.101        moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<omega>" using M'.finite_measure A by (simp add: countable_UN)
   5.102        moreover {
   5.103 -        have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
   5.104 +        have "(\<integral>\<^isup>+x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
   5.105            using A `f \<in> G` unfolding G_def by (auto simp: countable_UN)
   5.106          also have "\<nu> (\<Union>i. A i) < \<omega>" using v_fin by (simp add: pextreal_less_\<omega>)
   5.107 -        finally have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
   5.108 +        finally have "(\<integral>\<^isup>+x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
   5.109            by (simp add: pextreal_less_\<omega>) }
   5.110        ultimately
   5.111        show "(\<Sum>\<^isub>\<infinity> n. ?t (A n)) = ?t (\<Union>i. A i)"
   5.112 @@ -433,9 +433,9 @@
   5.113      hence pos_M: "0 < \<mu> (space M)"
   5.114        using ac top unfolding absolutely_continuous_def by auto
   5.115      moreover
   5.116 -    have "positive_integral (\<lambda>x. f x * indicator (space M) x) \<le> \<nu> (space M)"
   5.117 +    have "(\<integral>\<^isup>+x. f x * indicator (space M) x) \<le> \<nu> (space M)"
   5.118        using `f \<in> G` unfolding G_def by auto
   5.119 -    hence "positive_integral (\<lambda>x. f x * indicator (space M) x) \<noteq> \<omega>"
   5.120 +    hence "(\<integral>\<^isup>+x. f x * indicator (space M) x) \<noteq> \<omega>"
   5.121        using M'.finite_measure_of_space by auto
   5.122      moreover
   5.123      def b \<equiv> "?t (space M) / \<mu> (space M) / 2"
   5.124 @@ -462,30 +462,30 @@
   5.125      let "?f0 x" = "f x + b * indicator A0 x"
   5.126      { fix A assume A: "A \<in> sets M"
   5.127        hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
   5.128 -      have "positive_integral (\<lambda>x. ?f0 x  * indicator A x) =
   5.129 -        positive_integral (\<lambda>x. f x * indicator A x + b * indicator (A \<inter> A0) x)"
   5.130 +      have "(\<integral>\<^isup>+x. ?f0 x  * indicator A x) =
   5.131 +        (\<integral>\<^isup>+x. f x * indicator A x + b * indicator (A \<inter> A0) x)"
   5.132          by (auto intro!: positive_integral_cong simp: field_simps indicator_inter_arith)
   5.133 -      hence "positive_integral (\<lambda>x. ?f0 x * indicator A x) =
   5.134 -          positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0)"
   5.135 +      hence "(\<integral>\<^isup>+x. ?f0 x * indicator A x) =
   5.136 +          (\<integral>\<^isup>+x. f x * indicator A x) + b * \<mu> (A \<inter> A0)"
   5.137          using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A
   5.138          by (simp add: borel_measurable_indicator positive_integral_add positive_integral_cmult_indicator) }
   5.139      note f0_eq = this
   5.140      { fix A assume A: "A \<in> sets M"
   5.141        hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
   5.142 -      have f_le_v: "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
   5.143 +      have f_le_v: "(\<integral>\<^isup>+x. f x * indicator A x) \<le> \<nu> A"
   5.144          using `f \<in> G` A unfolding G_def by auto
   5.145        note f0_eq[OF A]
   5.146 -      also have "positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le>
   5.147 -          positive_integral (\<lambda>x. f x * indicator A x) + ?t (A \<inter> A0)"
   5.148 +      also have "(\<integral>\<^isup>+x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le>
   5.149 +          (\<integral>\<^isup>+x. f x * indicator A x) + ?t (A \<inter> A0)"
   5.150          using bM_le_t[OF `A \<inter> A0 \<in> sets M`] `A \<in> sets M` `A0 \<in> sets M`
   5.151          by (auto intro!: add_left_mono)
   5.152 -      also have "\<dots> \<le> positive_integral (\<lambda>x. f x * indicator A x) + ?t A"
   5.153 +      also have "\<dots> \<le> (\<integral>\<^isup>+x. f x * indicator A x) + ?t A"
   5.154          using M.measure_mono[simplified, OF _ `A \<inter> A0 \<in> sets M` `A \<in> sets M`]
   5.155          by (auto intro!: add_left_mono)
   5.156        also have "\<dots> \<le> \<nu> A"
   5.157          using f_le_v M'.finite_measure[simplified, OF `A \<in> sets M`]
   5.158 -        by (cases "positive_integral (\<lambda>x. f x * indicator A x)", cases "\<nu> A", auto)
   5.159 -      finally have "positive_integral (\<lambda>x. ?f0 x * indicator A x) \<le> \<nu> A" . }
   5.160 +        by (cases "(\<integral>\<^isup>+x. f x * indicator A x)", cases "\<nu> A", auto)
   5.161 +      finally have "(\<integral>\<^isup>+x. ?f0 x * indicator A x) \<le> \<nu> A" . }
   5.162      hence "?f0 \<in> G" using `A0 \<in> sets M` unfolding G_def
   5.163        by (auto intro!: borel_measurable_indicator borel_measurable_pextreal_add borel_measurable_pextreal_times)
   5.164      have real: "?t (space M) \<noteq> \<omega>" "?t A0 \<noteq> \<omega>"
   5.165 @@ -525,11 +525,11 @@
   5.166    show ?thesis
   5.167    proof (safe intro!: bexI[of _ f])
   5.168      fix A assume "A\<in>sets M"
   5.169 -    show "\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   5.170 +    show "\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   5.171      proof (rule antisym)
   5.172 -      show "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
   5.173 +      show "(\<integral>\<^isup>+x. f x * indicator A x) \<le> \<nu> A"
   5.174          using `f \<in> G` `A \<in> sets M` unfolding G_def by auto
   5.175 -      show "\<nu> A \<le> positive_integral (\<lambda>x. f x * indicator A x)"
   5.176 +      show "\<nu> A \<le> (\<integral>\<^isup>+x. f x * indicator A x)"
   5.177          using upper_bound[THEN bspec, OF `A \<in> sets M`]
   5.178           by (simp add: pextreal_zero_le_diff)
   5.179      qed
   5.180 @@ -669,7 +669,7 @@
   5.181  lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite:
   5.182    assumes "measure_space M \<nu>"
   5.183    assumes "absolutely_continuous \<nu>"
   5.184 -  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   5.185 +  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   5.186  proof -
   5.187    interpret v: measure_space M \<nu> by fact
   5.188    from split_space_into_finite_sets_and_rest[OF assms]
   5.189 @@ -680,7 +680,7 @@
   5.190      and Q_fin: "\<And>i. \<nu> (Q i) \<noteq> \<omega>" by force
   5.191    from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto
   5.192    have "\<forall>i. \<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
   5.193 -    \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
   5.194 +    \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f x * indicator (Q i \<inter> A) x))"
   5.195    proof
   5.196      fix i
   5.197      have indicator_eq: "\<And>f x A. (f x :: pextreal) * indicator (Q i \<inter> A) x * indicator (Q i) x
   5.198 @@ -702,17 +702,17 @@
   5.199        by (auto simp: R.absolutely_continuous_def absolutely_continuous_def)
   5.200      from finite_measure.Radon_Nikodym_finite_measure[OF fm fmv this]
   5.201      obtain f where f: "(\<lambda>x. f x * indicator (Q i) x) \<in> borel_measurable M"
   5.202 -      and f_int: "\<And>A. A\<in>sets M \<Longrightarrow> \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. (f x * indicator (Q i) x) * indicator A x)"
   5.203 +      and f_int: "\<And>A. A\<in>sets M \<Longrightarrow> \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. (f x * indicator (Q i) x) * indicator A x)"
   5.204        unfolding Bex_def borel_measurable_restricted[OF `Q i \<in> sets M`]
   5.205          positive_integral_restricted[OF `Q i \<in> sets M`] by (auto simp: indicator_eq)
   5.206      then show "\<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
   5.207 -      \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
   5.208 +      \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f x * indicator (Q i \<inter> A) x))"
   5.209        by (fastsimp intro!: exI[of _ "\<lambda>x. f x * indicator (Q i) x"] positive_integral_cong
   5.210            simp: indicator_def)
   5.211    qed
   5.212    from choice[OF this] obtain f where borel: "\<And>i. f i \<in> borel_measurable M"
   5.213      and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
   5.214 -      \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f i x * indicator (Q i \<inter> A) x)"
   5.215 +      \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f i x * indicator (Q i \<inter> A) x)"
   5.216      by auto
   5.217    let "?f x" =
   5.218      "(\<Sum>\<^isub>\<infinity> i. f i x * indicator (Q i) x) + \<omega> * indicator Q0 x"
   5.219 @@ -728,7 +728,7 @@
   5.220          f i x * indicator (Q i \<inter> A) x"
   5.221        "\<And>x i. (indicator A x * indicator Q0 x :: pextreal) =
   5.222          indicator (Q0 \<inter> A) x" by (auto simp: indicator_def)
   5.223 -    have "positive_integral (\<lambda>x. ?f x * indicator A x) =
   5.224 +    have "(\<integral>\<^isup>+x. ?f x * indicator A x) =
   5.225        (\<Sum>\<^isub>\<infinity> i. \<nu> (Q i \<inter> A)) + \<omega> * \<mu> (Q0 \<inter> A)"
   5.226        unfolding f[OF `A \<in> sets M`]
   5.227        apply (simp del: pextreal_times(2) add: field_simps *)
   5.228 @@ -755,7 +755,7 @@
   5.229        using Q_sets `A \<in> sets M` Q0(1) by (auto intro!: countable_UN)
   5.230      moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}"
   5.231        using `A \<in> sets M` sets_into_space Q0 by auto
   5.232 -    ultimately show "\<nu> A = positive_integral (\<lambda>x. ?f x * indicator A x)"
   5.233 +    ultimately show "\<nu> A = (\<integral>\<^isup>+x. ?f x * indicator A x)"
   5.234        using v.measure_additive[simplified, of "(\<Union>i. Q i) \<inter> A" "Q0 \<inter> A"]
   5.235        by simp
   5.236    qed
   5.237 @@ -764,14 +764,14 @@
   5.238  lemma (in sigma_finite_measure) Radon_Nikodym:
   5.239    assumes "measure_space M \<nu>"
   5.240    assumes "absolutely_continuous \<nu>"
   5.241 -  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   5.242 +  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   5.243  proof -
   5.244    from Ex_finite_integrable_function
   5.245    obtain h where finite: "positive_integral h \<noteq> \<omega>" and
   5.246      borel: "h \<in> borel_measurable M" and
   5.247      pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
   5.248      "\<And>x. x \<in> space M \<Longrightarrow> h x < \<omega>" by auto
   5.249 -  let "?T A" = "positive_integral (\<lambda>x. h x * indicator A x)"
   5.250 +  let "?T A" = "(\<integral>\<^isup>+x. h x * indicator A x)"
   5.251    from measure_space_density[OF borel] finite
   5.252    interpret T: finite_measure M ?T
   5.253      unfolding finite_measure_def finite_measure_axioms_def
   5.254 @@ -792,7 +792,7 @@
   5.255      then have "(\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
   5.256        using f_borel by (auto intro: borel_measurable_pextreal_times borel_measurable_indicator)
   5.257      from positive_integral_translated_density[OF borel this]
   5.258 -    show "\<nu> A = positive_integral (\<lambda>x. h x * f x * indicator A x)"
   5.259 +    show "\<nu> A = (\<integral>\<^isup>+x. h x * f x * indicator A x)"
   5.260        unfolding fT[OF `A \<in> sets M`] by (simp add: field_simps)
   5.261    qed
   5.262  qed
   5.263 @@ -802,7 +802,7 @@
   5.264  lemma (in measure_space) finite_density_unique:
   5.265    assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   5.266    and fin: "positive_integral f < \<omega>"
   5.267 -  shows "(\<forall>A\<in>sets M. positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. g x * indicator A x))
   5.268 +  shows "(\<forall>A\<in>sets M. (\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. g x * indicator A x))
   5.269      \<longleftrightarrow> (AE x. f x = g x)"
   5.270      (is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
   5.271  proof (intro iffI ballI)
   5.272 @@ -817,7 +817,7 @@
   5.273        and g_fin: "positive_integral g < \<omega>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
   5.274      let ?N = "{x\<in>space M. g x < f x}"
   5.275      have N: "?N \<in> sets M" using borel by simp
   5.276 -    have "?P (\<lambda>x. (f x - g x)) ?N = positive_integral (\<lambda>x. f x * indicator ?N x - g x * indicator ?N x)"
   5.277 +    have "?P (\<lambda>x. (f x - g x)) ?N = (\<integral>\<^isup>+x. f x * indicator ?N x - g x * indicator ?N x)"
   5.278        by (auto intro!: positive_integral_cong simp: indicator_def)
   5.279      also have "\<dots> = ?P f ?N - ?P g ?N"
   5.280      proof (rule positive_integral_diff)
   5.281 @@ -848,7 +848,7 @@
   5.282  
   5.283  lemma (in finite_measure) density_unique_finite_measure:
   5.284    assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
   5.285 -  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)"
   5.286 +  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. f' x * indicator A x)"
   5.287      (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
   5.288    shows "AE x. f x = f' x"
   5.289  proof -
   5.290 @@ -876,13 +876,13 @@
   5.291    have 2: "AE x. ?f Q0 x = ?f' Q0 x"
   5.292    proof (rule AE_I')
   5.293      { fix f :: "'a \<Rightarrow> pextreal" assume borel: "f \<in> borel_measurable M"
   5.294 -        and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   5.295 +        and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   5.296        let "?A i" = "Q0 \<inter> {x \<in> space M. f x < of_nat i}"
   5.297        have "(\<Union>i. ?A i) \<in> null_sets"
   5.298        proof (rule null_sets_UN)
   5.299          fix i have "?A i \<in> sets M"
   5.300            using borel Q0(1) by auto
   5.301 -        have "?\<nu> (?A i) \<le> positive_integral (\<lambda>x. of_nat i * indicator (?A i) x)"
   5.302 +        have "?\<nu> (?A i) \<le> (\<integral>\<^isup>+x. of_nat i * indicator (?A i) x)"
   5.303            unfolding eq[OF `?A i \<in> sets M`]
   5.304            by (auto intro!: positive_integral_mono simp: indicator_def)
   5.305          also have "\<dots> = of_nat i * \<mu> (?A i)"
   5.306 @@ -912,38 +912,38 @@
   5.307  
   5.308  lemma (in sigma_finite_measure) density_unique:
   5.309    assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
   5.310 -  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)"
   5.311 +  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. f' x * indicator A x)"
   5.312      (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
   5.313    shows "AE x. f x = f' x"
   5.314  proof -
   5.315    obtain h where h_borel: "h \<in> borel_measurable M"
   5.316      and fin: "positive_integral h \<noteq> \<omega>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>"
   5.317      using Ex_finite_integrable_function by auto
   5.318 -  interpret h: measure_space M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
   5.319 +  interpret h: measure_space M "\<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x)"
   5.320      using h_borel by (rule measure_space_density)
   5.321 -  interpret h: finite_measure M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
   5.322 +  interpret h: finite_measure M "\<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x)"
   5.323      by default (simp cong: positive_integral_cong add: fin)
   5.324 -  interpret f: measure_space M "\<lambda>A. positive_integral (\<lambda>x. f x * indicator A x)"
   5.325 +  interpret f: measure_space M "\<lambda>A. (\<integral>\<^isup>+x. f x * indicator A x)"
   5.326      using borel(1) by (rule measure_space_density)
   5.327 -  interpret f': measure_space M "\<lambda>A. positive_integral (\<lambda>x. f' x * indicator A x)"
   5.328 +  interpret f': measure_space M "\<lambda>A. (\<integral>\<^isup>+x. f' x * indicator A x)"
   5.329      using borel(2) by (rule measure_space_density)
   5.330    { fix A assume "A \<in> sets M"
   5.331      then have " {x \<in> space M. h x \<noteq> 0 \<and> indicator A x \<noteq> (0::pextreal)} = A"
   5.332        using pos sets_into_space by (force simp: indicator_def)
   5.333 -    then have "positive_integral (\<lambda>xa. h xa * indicator A xa) = 0 \<longleftrightarrow> A \<in> null_sets"
   5.334 +    then have "(\<integral>\<^isup>+x. h x * indicator A x) = 0 \<longleftrightarrow> A \<in> null_sets"
   5.335        using h_borel `A \<in> sets M` by (simp add: positive_integral_0_iff) }
   5.336    note h_null_sets = this
   5.337    { fix A assume "A \<in> sets M"
   5.338 -    have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) =
   5.339 +    have "(\<integral>\<^isup>+x. h x * (f x * indicator A x)) =
   5.340        f.positive_integral (\<lambda>x. h x * indicator A x)"
   5.341        using `A \<in> sets M` h_borel borel
   5.342        by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
   5.343      also have "\<dots> = f'.positive_integral (\<lambda>x. h x * indicator A x)"
   5.344        by (rule f'.positive_integral_cong_measure) (rule f)
   5.345 -    also have "\<dots> = positive_integral (\<lambda>x. h x * (f' x * indicator A x))"
   5.346 +    also have "\<dots> = (\<integral>\<^isup>+x. h x * (f' x * indicator A x))"
   5.347        using `A \<in> sets M` h_borel borel
   5.348        by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
   5.349 -    finally have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) = positive_integral (\<lambda>x. h x * (f' x * indicator A x))" . }
   5.350 +    finally have "(\<integral>\<^isup>+x. h x * (f x * indicator A x)) = (\<integral>\<^isup>+x. h x * (f' x * indicator A x))" . }
   5.351    then have "h.almost_everywhere (\<lambda>x. f x = f' x)"
   5.352      using h_borel borel
   5.353      by (intro h.density_unique_finite_measure[OF borel])
   5.354 @@ -955,7 +955,7 @@
   5.355  
   5.356  lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
   5.357    assumes \<nu>: "measure_space M \<nu>" and f: "f \<in> borel_measurable M"
   5.358 -    and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   5.359 +    and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   5.360    shows "sigma_finite_measure M \<nu> \<longleftrightarrow> (AE x. f x \<noteq> \<omega>)"
   5.361  proof
   5.362    assume "sigma_finite_measure M \<nu>"
   5.363 @@ -965,10 +965,10 @@
   5.364      and fin: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>" by auto
   5.365    have "AE x. f x * h x \<noteq> \<omega>"
   5.366    proof (rule AE_I')
   5.367 -    have "\<nu>.positive_integral h = positive_integral (\<lambda>x. f x * h x)"
   5.368 +    have "\<nu>.positive_integral h = (\<integral>\<^isup>+x. f x * h x)"
   5.369        by (simp add: \<nu>.positive_integral_cong_measure[symmetric, OF eq[symmetric]])
   5.370           (intro positive_integral_translated_density f h)
   5.371 -    then have "positive_integral (\<lambda>x. f x * h x) \<noteq> \<omega>"
   5.372 +    then have "(\<integral>\<^isup>+x. f x * h x) \<noteq> \<omega>"
   5.373        using h(2) by simp
   5.374      then show "(\<lambda>x. f x * h x) -` {\<omega>} \<inter> space M \<in> null_sets"
   5.375        using f h(1) by (auto intro!: positive_integral_omega borel_measurable_vimage)
   5.376 @@ -1018,12 +1018,12 @@
   5.377    next
   5.378      fix n obtain i j where
   5.379        [simp]: "prod_decode n = (i, j)" by (cases "prod_decode n") auto
   5.380 -    have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<noteq> \<omega>"
   5.381 +    have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x) \<noteq> \<omega>"
   5.382      proof (cases i)
   5.383        case 0
   5.384        have "AE x. f x * indicator (A i \<inter> Q j) x = 0"
   5.385          using AE by (rule AE_mp) (auto intro!: AE_cong simp: A_def `i = 0`)
   5.386 -      then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) = 0"
   5.387 +      then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x) = 0"
   5.388          using A_in_sets f
   5.389          apply (subst positive_integral_0_iff)
   5.390          apply fast
   5.391 @@ -1034,8 +1034,8 @@
   5.392        then show ?thesis by simp
   5.393      next
   5.394        case (Suc n)
   5.395 -      then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<le>
   5.396 -        positive_integral (\<lambda>x. of_nat (Suc n) * indicator (Q j) x)"
   5.397 +      then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x) \<le>
   5.398 +        (\<integral>\<^isup>+x. of_nat (Suc n) * indicator (Q j) x)"
   5.399          by (auto intro!: positive_integral_mono simp: indicator_def A_def)
   5.400        also have "\<dots> = of_nat (Suc n) * \<mu> (Q j)"
   5.401          using Q by (auto intro!: positive_integral_cmult_indicator)
   5.402 @@ -1052,7 +1052,7 @@
   5.403  
   5.404  definition (in sigma_finite_measure)
   5.405    "RN_deriv \<nu> \<equiv> SOME f. f \<in> borel_measurable M \<and>
   5.406 -    (\<forall>A \<in> sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x))"
   5.407 +    (\<forall>A \<in> sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x))"
   5.408  
   5.409  lemma (in sigma_finite_measure) RN_deriv_cong:
   5.410    assumes cong: "\<And>A. A \<in> sets M \<Longrightarrow> \<mu>' A = \<mu> A" "\<And>A. A \<in> sets M \<Longrightarrow> \<nu>' A = \<nu> A"
   5.411 @@ -1069,7 +1069,7 @@
   5.412    assumes "measure_space M \<nu>"
   5.413    assumes "absolutely_continuous \<nu>"
   5.414    shows "RN_deriv \<nu> \<in> borel_measurable M" (is ?borel)
   5.415 -  and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
   5.416 +  and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. RN_deriv \<nu> x * indicator A x)"
   5.417      (is "\<And>A. _ \<Longrightarrow> ?int A")
   5.418  proof -
   5.419    note Ex = Radon_Nikodym[OF assms, unfolded Bex_def]
   5.420 @@ -1082,13 +1082,13 @@
   5.421  lemma (in sigma_finite_measure) RN_deriv_positive_integral:
   5.422    assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
   5.423      and f: "f \<in> borel_measurable M"
   5.424 -  shows "measure_space.positive_integral M \<nu> f = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
   5.425 +  shows "measure_space.positive_integral M \<nu> f = (\<integral>\<^isup>+x. RN_deriv \<nu> x * f x)"
   5.426  proof -
   5.427    interpret \<nu>: measure_space M \<nu> by fact
   5.428    have "\<nu>.positive_integral f =
   5.429 -    measure_space.positive_integral M (\<lambda>A. positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)) f"
   5.430 +    measure_space.positive_integral M (\<lambda>A. (\<integral>\<^isup>+x. RN_deriv \<nu> x * indicator A x)) f"
   5.431      by (intro \<nu>.positive_integral_cong_measure[symmetric] RN_deriv(2)[OF \<nu>, symmetric])
   5.432 -  also have "\<dots> = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
   5.433 +  also have "\<dots> = (\<integral>\<^isup>+x. RN_deriv \<nu> x * f x)"
   5.434      by (intro positive_integral_translated_density RN_deriv[OF \<nu>] f)
   5.435    finally show ?thesis .
   5.436  qed
   5.437 @@ -1096,11 +1096,11 @@
   5.438  lemma (in sigma_finite_measure) RN_deriv_unique:
   5.439    assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
   5.440    and f: "f \<in> borel_measurable M"
   5.441 -  and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   5.442 +  and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   5.443    shows "AE x. f x = RN_deriv \<nu> x"
   5.444  proof (rule density_unique[OF f RN_deriv(1)[OF \<nu>]])
   5.445    fix A assume A: "A \<in> sets M"
   5.446 -  show "positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
   5.447 +  show "(\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. RN_deriv \<nu> x * indicator A x)"
   5.448      unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
   5.449  qed
   5.450  
   5.451 @@ -1130,10 +1130,10 @@
   5.452      using f by (auto simp: bij_inv_def indicator_def)
   5.453    have "\<nu> (f ` (f -` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f -` A \<inter> S) x)"
   5.454      using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
   5.455 -  also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
   5.456 +  also have "\<dots> = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
   5.457      unfolding positive_integral_vimage_inv[OF f]
   5.458      by (simp add: * cong: positive_integral_cong)
   5.459 -  finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
   5.460 +  finally show "\<nu> A = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
   5.461      unfolding A_f[OF `A \<in> sets M`] .
   5.462  qed
   5.463  
   5.464 @@ -1150,7 +1150,7 @@
   5.465  lemma (in sigma_finite_measure)
   5.466    assumes \<nu>: "sigma_finite_measure M \<nu>" "absolutely_continuous \<nu>"
   5.467      and f: "f \<in> borel_measurable M"
   5.468 -  shows RN_deriv_integral: "measure_space.integral M \<nu> f = integral (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integral)
   5.469 +  shows RN_deriv_integral: "measure_space.integral M \<nu> f = (\<integral>x. real (RN_deriv \<nu> x) * f x)" (is ?integral)
   5.470      and RN_deriv_integrable: "measure_space.integrable M \<nu> f \<longleftrightarrow> integrable (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integrable)
   5.471  proof -
   5.472    interpret \<nu>: sigma_finite_measure M \<nu> by fact
   5.473 @@ -1164,7 +1164,7 @@
   5.474        then have "RN_deriv \<nu> x * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)"
   5.475          using * by (simp add: Real_real) }
   5.476      note * = this
   5.477 -    have "positive_integral (\<lambda>x. RN_deriv \<nu> x * Real (f x)) = positive_integral (\<lambda>x. Real (real (RN_deriv \<nu> x) * f x))"
   5.478 +    have "(\<integral>\<^isup>+x. RN_deriv \<nu> x * Real (f x)) = (\<integral>\<^isup>+x. Real (real (RN_deriv \<nu> x) * f x))"
   5.479        apply (rule positive_integral_cong_AE)
   5.480        apply (rule AE_mp[OF RN_deriv_finite[OF \<nu>]])
   5.481        by (auto intro!: AE_cong simp: *) }
   5.482 @@ -1182,7 +1182,7 @@
   5.483  proof -
   5.484    note deriv = RN_deriv[OF assms(1, 2)]
   5.485    from deriv(2)[OF `{x} \<in> sets M`]
   5.486 -  have "\<nu> {x} = positive_integral (\<lambda>w. RN_deriv \<nu> x * indicator {x} w)"
   5.487 +  have "\<nu> {x} = (\<integral>\<^isup>+w. RN_deriv \<nu> x * indicator {x} w)"
   5.488      by (auto simp: indicator_def intro!: positive_integral_cong)
   5.489    thus ?thesis using positive_integral_cmult_indicator[OF `{x} \<in> sets M`]
   5.490      by auto