src/HOL/Probability/Lebesgue_Integration.thy

     apply (subst SUPR_ereal_add[symmetric, OF inc not_MInf]) .
   then show ?thesis by (simp add: positive_integral_max_0)
 qed
 
 lemma positive_integral_cmult:
-  assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "0 \<le> c"
+  assumes f: "f \<in> borel_measurable M" "0 \<le> c"
   shows "(\<integral>\<^isup>+ x. c * f x \<partial>M) = c * integral\<^isup>P M f"
 proof -
   have [simp]: "\<And>x. c * max 0 (f x) = max 0 (c * f x)" using `0 \<le> c`
     by (auto split: split_max simp: ereal_zero_le_0_iff)
   have "(\<integral>\<^isup>+ x. c * f x \<partial>M) = (\<integral>\<^isup>+ x. c * max 0 (f x) \<partial>M)"

     using positive_integral_linear[OF _ _ `0 \<le> c`, of "\<lambda>x. max 0 (f x)" _ "\<lambda>x. 0"] f
     by (auto simp: positive_integral_max_0)
 qed
 
 lemma positive_integral_multc:
-  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "0 \<le> c"
+  assumes "f \<in> borel_measurable M" "0 \<le> c"
   shows "(\<integral>\<^isup>+ x. f x * c \<partial>M) = integral\<^isup>P M f * c"
   unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp
 
 lemma positive_integral_indicator[simp]:
   "A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. indicator A x\<partial>M) = (emeasure M) A"
   by (subst positive_integral_eq_simple_integral)
-     (auto simp: simple_function_indicator simple_integral_indicator)
+     (auto simp: simple_integral_indicator)
 
 lemma positive_integral_cmult_indicator:
   "0 \<le> c \<Longrightarrow> A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. c * indicator A x \<partial>M) = c * (emeasure M) A"
   by (subst positive_integral_eq_simple_integral)
      (auto simp: simple_function_indicator simple_integral_indicator)

     show ?case using insert by auto
   qed simp
 qed simp
 
 lemma positive_integral_Markov_inequality:
-  assumes u: "u \<in> borel_measurable M" "AE x in M. 0 \<le> u x" and "A \<in> sets M" and c: "0 \<le> c" "c \<noteq> \<infinity>"
+  assumes u: "u \<in> borel_measurable M" "AE x in M. 0 \<le> u x" and "A \<in> sets M" and c: "0 \<le> c"
   shows "(emeasure M) ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * (\<integral>\<^isup>+ x. u x * indicator A x \<partial>M)"
     (is "(emeasure M) ?A \<le> _ * ?PI")
 proof -
   have "?A \<in> sets M"
     using `A \<in> sets M` u by auto

 
 lemma integrable_cong:
   "(\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable M g"
   by (simp cong: positive_integral_cong measurable_cong add: integrable_def)
 
+lemma integral_mono_AE:
+  assumes fg: "integrable M f" "integrable M g"
+  and mono: "AE t in M. f t \<le> g t"
+  shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
+proof -
+  have "AE x in M. ereal (f x) \<le> ereal (g x)"
+    using mono by auto
+  moreover have "AE x in M. ereal (- g x) \<le> ereal (- f x)"
+    using mono by auto
+  ultimately show ?thesis using fg
+    by (auto intro!: add_mono positive_integral_mono_AE real_of_ereal_positive_mono
+             simp: positive_integral_positive lebesgue_integral_def diff_minus)
+qed
+
+lemma integral_mono:
+  assumes "integrable M f" "integrable M g" "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
+  shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
+  using assms by (auto intro: integral_mono_AE)
+
 lemma positive_integral_eq_integral:
   assumes f: "integrable M f"
   assumes nonneg: "AE x in M. 0 \<le> f x" 
   shows "(\<integral>\<^isup>+ x. ereal (f x) \<partial>M) = integral\<^isup>L M f"
 proof -

 
 lemma lebesgue_integral_cmult_nonneg:
   assumes f: "f \<in> borel_measurable M" and "0 \<le> c"
   shows "(\<integral>x. c * f x \<partial>M) = c * integral\<^isup>L M f"
 proof -
-  { have "c * real (integral\<^isup>P M (\<lambda>x. max 0 (ereal (f x)))) =
-      real (ereal c * integral\<^isup>P M (\<lambda>x. max 0 (ereal (f x))))"
-      by simp
-    also have "\<dots> = real (integral\<^isup>P M (\<lambda>x. ereal c * max 0 (ereal (f x))))"
+  { have "real (ereal c * integral\<^isup>P M (\<lambda>x. max 0 (ereal (f x)))) =
+      real (integral\<^isup>P M (\<lambda>x. ereal c * max 0 (ereal (f x))))"
       using f `0 \<le> c` by (subst positive_integral_cmult) auto
     also have "\<dots> = real (integral\<^isup>P M (\<lambda>x. max 0 (ereal (c * f x))))"
       using `0 \<le> c` by (auto intro!: arg_cong[where f=real] positive_integral_cong simp: max_def zero_le_mult_iff)
     finally have "real (integral\<^isup>P M (\<lambda>x. ereal (c * f x))) = c * real (integral\<^isup>P M (\<lambda>x. ereal (f x)))"
       by (simp add: positive_integral_max_0) }
   moreover
-  { have "c * real (integral\<^isup>P M (\<lambda>x. max 0 (ereal (- f x)))) =
-      real (ereal c * integral\<^isup>P M (\<lambda>x. max 0 (ereal (- f x))))"
-      by simp
-    also have "\<dots> = real (integral\<^isup>P M (\<lambda>x. ereal c * max 0 (ereal (- f x))))"
+  { have "real (ereal c * integral\<^isup>P M (\<lambda>x. max 0 (ereal (- f x)))) =
+      real (integral\<^isup>P M (\<lambda>x. ereal c * max 0 (ereal (- f x))))"
       using f `0 \<le> c` by (subst positive_integral_cmult) auto
     also have "\<dots> = real (integral\<^isup>P M (\<lambda>x. max 0 (ereal (- c * f x))))"
       using `0 \<le> c` by (auto intro!: arg_cong[where f=real] positive_integral_cong simp: max_def mult_le_0_iff)
     finally have "real (integral\<^isup>P M (\<lambda>x. ereal (- c * f x))) = c * real (integral\<^isup>P M (\<lambda>x. ereal (- f x)))"
       by (simp add: positive_integral_max_0) }

 lemma integral_multc:
   assumes "integrable M f"
   shows "(\<integral> x. f x * c \<partial>M) = integral\<^isup>L M f * c"
   unfolding mult_commute[of _ c] integral_cmult[OF assms] ..
 
-lemma integral_mono_AE:
-  assumes fg: "integrable M f" "integrable M g"
-  and mono: "AE t in M. f t \<le> g t"
-  shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
-proof -
-  have "AE x in M. ereal (f x) \<le> ereal (g x)"
-    using mono by auto
-  moreover have "AE x in M. ereal (- g x) \<le> ereal (- f x)"
-    using mono by auto
-  ultimately show ?thesis using fg
-    by (auto intro!: add_mono positive_integral_mono_AE real_of_ereal_positive_mono
-             simp: positive_integral_positive lebesgue_integral_def diff_minus)
-qed
-
-lemma integral_mono:
-  assumes "integrable M f" "integrable M g" "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
-  shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
-  using assms by (auto intro: integral_mono_AE)
-
 lemma integral_diff[simp, intro]:
   assumes f: "integrable M f" and g: "integrable M g"
   shows "integrable M (\<lambda>t. f t - g t)"
   and "(\<integral> t. f t - g t \<partial>M) = integral\<^isup>L M f - integral\<^isup>L M g"
   using integral_add[OF f integral_minus(1)[OF g]]

     from this assms show ?thesis by (induct S) simp_all
   qed simp
   thus "?int S" and "?I S" by auto
 qed
 
+lemma integrable_bound:
+  assumes "integrable M f" and f: "AE x in M. \<bar>g x\<bar> \<le> f x"
+  assumes borel: "g \<in> borel_measurable M"
+  shows "integrable M g"
+proof -
+  have "(\<integral>\<^isup>+ x. ereal (g x) \<partial>M) \<le> (\<integral>\<^isup>+ x. ereal \<bar>g x\<bar> \<partial>M)"
+    by (auto intro!: positive_integral_mono)
+  also have "\<dots> \<le> (\<integral>\<^isup>+ x. ereal (f x) \<partial>M)"
+    using f by (auto intro!: positive_integral_mono_AE)
+  also have "\<dots> < \<infinity>"
+    using `integrable M f` unfolding integrable_def by auto
+  finally have pos: "(\<integral>\<^isup>+ x. ereal (g x) \<partial>M) < \<infinity>" .
+
+  have "(\<integral>\<^isup>+ x. ereal (- g x) \<partial>M) \<le> (\<integral>\<^isup>+ x. ereal (\<bar>g x\<bar>) \<partial>M)"
+    by (auto intro!: positive_integral_mono)
+  also have "\<dots> \<le> (\<integral>\<^isup>+ x. ereal (f x) \<partial>M)"
+    using f by (auto intro!: positive_integral_mono_AE)
+  also have "\<dots> < \<infinity>"
+    using `integrable M f` unfolding integrable_def by auto
+  finally have neg: "(\<integral>\<^isup>+ x. ereal (- g x) \<partial>M) < \<infinity>" .
+
+  from neg pos borel show ?thesis
+    unfolding integrable_def by auto
+qed
+
 lemma integrable_abs:
-  assumes "integrable M f"
+  assumes f: "integrable M f"
   shows "integrable M (\<lambda> x. \<bar>f x\<bar>)"
 proof -
   from assms have *: "(\<integral>\<^isup>+x. ereal (- \<bar>f x\<bar>)\<partial>M) = 0"
     "\<And>x. ereal \<bar>f x\<bar> = max 0 (ereal (f x)) + max 0 (ereal (- f x))"
     by (auto simp: integrable_def positive_integral_0_iff_AE split: split_max)

     using borel by (auto intro!: positive_integral_subalgebra N)
   moreover have "f \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable N"
     using assms unfolding measurable_def by auto
   ultimately show ?P ?I
     by (auto simp: integrable_def lebesgue_integral_def positive_integral_max_0)
-qed
-
-lemma integrable_bound:
-  assumes "integrable M f"
-  and f: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
-    "\<And>x. x \<in> space M \<Longrightarrow> \<bar>g x\<bar> \<le> f x"
-  assumes borel: "g \<in> borel_measurable M"
-  shows "integrable M g"
-proof -
-  have "(\<integral>\<^isup>+ x. ereal (g x) \<partial>M) \<le> (\<integral>\<^isup>+ x. ereal \<bar>g x\<bar> \<partial>M)"
-    by (auto intro!: positive_integral_mono)
-  also have "\<dots> \<le> (\<integral>\<^isup>+ x. ereal (f x) \<partial>M)"
-    using f by (auto intro!: positive_integral_mono)
-  also have "\<dots> < \<infinity>"
-    using `integrable M f` unfolding integrable_def by auto
-  finally have pos: "(\<integral>\<^isup>+ x. ereal (g x) \<partial>M) < \<infinity>" .
-
-  have "(\<integral>\<^isup>+ x. ereal (- g x) \<partial>M) \<le> (\<integral>\<^isup>+ x. ereal (\<bar>g x\<bar>) \<partial>M)"
-    by (auto intro!: positive_integral_mono)
-  also have "\<dots> \<le> (\<integral>\<^isup>+ x. ereal (f x) \<partial>M)"
-    using f by (auto intro!: positive_integral_mono)
-  also have "\<dots> < \<infinity>"
-    using `integrable M f` unfolding integrable_def by auto
-  finally have neg: "(\<integral>\<^isup>+ x. ereal (- g x) \<partial>M) < \<infinity>" .
-
-  from neg pos borel show ?thesis
-    unfolding integrable_def by auto
 qed
 
 lemma lebesgue_integral_nonneg:
   assumes ae: "(AE x in M. 0 \<le> f x)" shows "0 \<le> integral\<^isup>L M f"
 proof -

 proof (rule integrable_bound)
   show "integrable M (\<lambda>x. \<bar>f x\<bar> + \<bar>g x\<bar>)"
     using int by (simp add: integrable_abs)
   show "(\<lambda>x. max (f x) (g x)) \<in> borel_measurable M"
     using int unfolding integrable_def by auto
-next
-  fix x assume "x \<in> space M"
-  show "0 \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" "\<bar>max (f x) (g x)\<bar> \<le> \<bar>f x\<bar> + \<bar>g x\<bar>"
-    by auto
-qed
+qed auto
 
 lemma integrable_min:
   assumes int: "integrable M f" "integrable M g"
   shows "integrable M (\<lambda> x. min (f x) (g x))"
 proof (rule integrable_bound)
   show "integrable M (\<lambda>x. \<bar>f x\<bar> + \<bar>g x\<bar>)"
     using int by (simp add: integrable_abs)
   show "(\<lambda>x. min (f x) (g x)) \<in> borel_measurable M"
     using int unfolding integrable_def by auto
-next
-  fix x assume "x \<in> space M"
-  show "0 \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" "\<bar>min (f x) (g x)\<bar> \<le> \<bar>f x\<bar> + \<bar>g x\<bar>"
-    by auto
-qed
+qed auto
 
 lemma integral_triangle_inequality:
   assumes "integrable M f"
   shows "\<bar>integral\<^isup>L M f\<bar> \<le> (\<integral>x. \<bar>f x\<bar> \<partial>M)"
 proof -

     using assms by (rule integral_mono[OF integral_zero(1)])
   finally show ?thesis .
 qed
 
 lemma integral_monotone_convergence_pos:
-  assumes i: "\<And>i. integrable M (f i)" and mono: "\<And>x. mono (\<lambda>n. f n x)"
-  and pos: "\<And>x i. 0 \<le> f i x"
-  and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
-  and ilim: "(\<lambda>i. integral\<^isup>L M (f i)) ----> x"
+  assumes i: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
+    and pos: "\<And>i. AE x in M. 0 \<le> f i x"
+    and lim: "AE x in M. (\<lambda>i. f i x) ----> u x"
+    and ilim: "(\<lambda>i. integral\<^isup>L M (f i)) ----> x"
+    and u: "u \<in> borel_measurable M"
   shows "integrable M u"
   and "integral\<^isup>L M u = x"
 proof -
-  { fix x have "0 \<le> u x"
-      using mono pos[of 0 x] incseq_le[OF _ lim, of x 0]
-      by (simp add: mono_def incseq_def) }
-  note pos_u = this
-
-  have SUP_F: "\<And>x. (SUP n. ereal (f n x)) = ereal (u x)"
-    unfolding SUP_eq_LIMSEQ[OF mono] by (rule lim)
-
-  have borel_f: "\<And>i. (\<lambda>x. ereal (f i x)) \<in> borel_measurable M"
-    using i unfolding integrable_def by auto
-  hence "(\<lambda>x. SUP i. ereal (f i x)) \<in> borel_measurable M"
-    by auto
-  hence borel_u: "u \<in> borel_measurable M"
-    by (auto simp: borel_measurable_ereal_iff SUP_F)
-
-  hence [simp]: "\<And>i. (\<integral>\<^isup>+x. ereal (- f i x) \<partial>M) = 0" "(\<integral>\<^isup>+x. ereal (- u x) \<partial>M) = 0"
-    using i borel_u pos pos_u by (auto simp: positive_integral_0_iff_AE integrable_def)
-
-  have integral_eq: "\<And>n. (\<integral>\<^isup>+ x. ereal (f n x) \<partial>M) = ereal (integral\<^isup>L M (f n))"
-    using i positive_integral_positive[of M] by (auto simp: ereal_real lebesgue_integral_def integrable_def)
-
-  have pos_integral: "\<And>n. 0 \<le> integral\<^isup>L M (f n)"
-    using pos i by (auto simp: integral_positive)
-  hence "0 \<le> x"
-    using LIMSEQ_le_const[OF ilim, of 0] by auto
-
-  from mono pos i have pI: "(\<integral>\<^isup>+ x. ereal (u x) \<partial>M) = (SUP n. (\<integral>\<^isup>+ x. ereal (f n x) \<partial>M))"
-    by (auto intro!: positive_integral_monotone_convergence_SUP
-      simp: integrable_def incseq_mono incseq_Suc_iff le_fun_def SUP_F[symmetric])
-  also have "\<dots> = ereal x" unfolding integral_eq
-  proof (rule SUP_eq_LIMSEQ[THEN iffD2])
-    show "mono (\<lambda>n. integral\<^isup>L M (f n))"
-      using mono i by (auto simp: mono_def intro!: integral_mono)
-    show "(\<lambda>n. integral\<^isup>L M (f n)) ----> x" using ilim .
+  have "(\<integral>\<^isup>+ x. ereal (u x) \<partial>M) = (SUP n. (\<integral>\<^isup>+ x. ereal (f n x) \<partial>M))"
+  proof (subst positive_integral_monotone_convergence_SUP_AE[symmetric])
+    fix i
+    from mono pos show "AE x in M. ereal (f i x) \<le> ereal (f (Suc i) x) \<and> 0 \<le> ereal (f i x)"
+      by eventually_elim (auto simp: mono_def)
+    show "(\<lambda>x. ereal (f i x)) \<in> borel_measurable M"
+      using i by (auto simp: integrable_def)
+  next
+    show "(\<integral>\<^isup>+ x. ereal (u x) \<partial>M) = \<integral>\<^isup>+ x. (SUP i. ereal (f i x)) \<partial>M"
+      apply (rule positive_integral_cong_AE)
+      using lim mono
+      by eventually_elim (simp add: SUP_eq_LIMSEQ[THEN iffD2])
   qed
-  finally show  "integrable M u" "integral\<^isup>L M u = x" using borel_u `0 \<le> x`
-    unfolding integrable_def lebesgue_integral_def by auto
+  also have "\<dots> = ereal x"
+    using mono i unfolding positive_integral_eq_integral[OF i pos]
+    by (subst SUP_eq_LIMSEQ) (auto simp: mono_def intro!: integral_mono_AE ilim)
+  finally have "(\<integral>\<^isup>+ x. ereal (u x) \<partial>M) = ereal x" .
+  moreover have "(\<integral>\<^isup>+ x. ereal (- u x) \<partial>M) = 0"
+  proof (subst positive_integral_0_iff_AE)
+    show "(\<lambda>x. ereal (- u x)) \<in> borel_measurable M"
+      using u by auto
+    from mono pos[of 0] lim show "AE x in M. ereal (- u x) \<le> 0"
+    proof eventually_elim
+      fix x assume "mono (\<lambda>n. f n x)" "0 \<le> f 0 x" "(\<lambda>i. f i x) ----> u x"
+      then show "ereal (- u x) \<le> 0"
+        using incseq_le[of "\<lambda>n. f n x" "u x" 0] by (simp add: mono_def incseq_def)
+    qed
+  qed
+  ultimately show "integrable M u" "integral\<^isup>L M u = x"
+    by (auto simp: integrable_def lebesgue_integral_def u)
 qed
 
 lemma integral_monotone_convergence:
-  assumes f: "\<And>i. integrable M (f i)" and "mono f"
-  and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
+  assumes f: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
+  and lim: "AE x in M. (\<lambda>i. f i x) ----> u x"
   and ilim: "(\<lambda>i. integral\<^isup>L M (f i)) ----> x"
+  and u: "u \<in> borel_measurable M"
   shows "integrable M u"
   and "integral\<^isup>L M u = x"
 proof -
   have 1: "\<And>i. integrable M (\<lambda>x. f i x - f 0 x)"
-      using f by (auto intro!: integral_diff)
-  have 2: "\<And>x. mono (\<lambda>n. f n x - f 0 x)" using `mono f`
-      unfolding mono_def le_fun_def by auto
-  have 3: "\<And>x n. 0 \<le> f n x - f 0 x" using `mono f`
-      unfolding mono_def le_fun_def by (auto simp: field_simps)
-  have 4: "\<And>x. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x"
+    using f by auto
+  have 2: "AE x in M. mono (\<lambda>n. f n x - f 0 x)"
+    using mono by (auto simp: mono_def le_fun_def)
+  have 3: "\<And>n. AE x in M. 0 \<le> f n x - f 0 x"
+    using mono by (auto simp: field_simps mono_def le_fun_def)
+  have 4: "AE x in M. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x"
     using lim by (auto intro!: tendsto_diff)
   have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>M)) ----> x - integral\<^isup>L M (f 0)"
-    using f ilim by (auto intro!: tendsto_diff simp: integral_diff)
-  note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5]
+    using f ilim by (auto intro!: tendsto_diff)
+  have 6: "(\<lambda>x. u x - f 0 x) \<in> borel_measurable M"
+    using f[of 0] u by auto
+  note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5 6]
   have "integrable M (\<lambda>x. (u x - f 0 x) + f 0 x)"
     using diff(1) f by (rule integral_add(1))
   with diff(2) f show "integrable M u" "integral\<^isup>L M u = x"
-    by (auto simp: integral_diff)
+    by auto
 qed
 
 lemma integral_0_iff:
   assumes "integrable M f"
   shows "(\<integral>x. \<bar>f x\<bar> \<partial>M) = 0 \<longleftrightarrow> (emeasure M) {x\<in>space M. f x \<noteq> 0} = 0"

   assumes gt: "AE x in M. X x < Y x" "(emeasure M) (space M) \<noteq> 0"
   shows "integral\<^isup>L M X < integral\<^isup>L M Y"
   using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
 
 lemma integral_dominated_convergence:
-  assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>x j. x\<in>space M \<Longrightarrow> \<bar>u j x\<bar> \<le> w x"
+  assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>j. AE x in M. \<bar>u j x\<bar> \<le> w x"
   and w: "integrable M w"
-  and u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
+  and u': "AE x in M. (\<lambda>i. u i x) ----> u' x"
+  and borel: "u' \<in> borel_measurable M"
   shows "integrable M u'"
   and "(\<lambda>i. (\<integral>x. \<bar>u i x - u' x\<bar> \<partial>M)) ----> 0" (is "?lim_diff")
   and "(\<lambda>i. integral\<^isup>L M (u i)) ----> integral\<^isup>L M u'" (is ?lim)
 proof -
-  { fix x j assume x: "x \<in> space M"
-    from u'[OF x] have "(\<lambda>i. \<bar>u i x\<bar>) ----> \<bar>u' x\<bar>" by (rule tendsto_rabs)
-    from LIMSEQ_le_const2[OF this]
-    have "\<bar>u' x\<bar> \<le> w x" using bound[OF x] by auto }
-  note u'_bound = this
-
-  from u[unfolded integrable_def]
-  have u'_borel: "u' \<in> borel_measurable M"
-    using u' by (blast intro: borel_measurable_LIMSEQ[of M u])
-
-  { fix x assume x: "x \<in> space M"
-    then have "0 \<le> \<bar>u 0 x\<bar>" by auto
-    also have "\<dots> \<le> w x" using bound[OF x] by auto
-    finally have "0 \<le> w x" . }
-  note w_pos = this
+  have all_bound: "AE x in M. \<forall>j. \<bar>u j x\<bar> \<le> w x"
+    using bound by (auto simp: AE_all_countable)
+  with u' have u'_bound: "AE x in M. \<bar>u' x\<bar> \<le> w x"
+    by eventually_elim (auto intro: LIMSEQ_le_const2 tendsto_rabs)
+
+  from bound[of 0] have w_pos: "AE x in M. 0 \<le> w x"
+    by eventually_elim auto
 
   show "integrable M u'"
-  proof (rule integrable_bound)
-    show "integrable M w" by fact
-    show "u' \<in> borel_measurable M" by fact
-  next
-    fix x assume x: "x \<in> space M" then show "0 \<le> w x" by fact
-    show "\<bar>u' x\<bar> \<le> w x" using u'_bound[OF x] .
-  qed
+    by (rule integrable_bound) fact+
 
   let ?diff = "\<lambda>n x. 2 * w x - \<bar>u n x - u' x\<bar>"
   have diff: "\<And>n. integrable M (\<lambda>x. \<bar>u n x - u' x\<bar>)"
-    using w u `integrable M u'`
-    by (auto intro!: integral_add integral_diff integral_cmult integrable_abs)
-
-  { fix j x assume x: "x \<in> space M"
-    have "\<bar>u j x - u' x\<bar> \<le> \<bar>u j x\<bar> + \<bar>u' x\<bar>" by auto
+    using w u `integrable M u'` by (auto intro!: integrable_abs)
+
+  from u'_bound all_bound
+  have diff_less_2w: "AE x in M. \<forall>j. \<bar>u j x - u' x\<bar> \<le> 2 * w x"
+  proof (eventually_elim, intro allI)
+    fix x j assume *: "\<bar>u' x\<bar> \<le> w x" "\<forall>j. \<bar>u j x\<bar> \<le> w x"
+    then have "\<bar>u j x - u' x\<bar> \<le> \<bar>u j x\<bar> + \<bar>u' x\<bar>" by auto
     also have "\<dots> \<le> w x + w x"
-      by (rule add_mono[OF bound[OF x] u'_bound[OF x]])
-    finally have "\<bar>u j x - u' x\<bar> \<le> 2 * w x" by simp }
-  note diff_less_2w = this
+      using * by (intro add_mono) auto
+    finally show "\<bar>u j x - u' x\<bar> \<le> 2 * w x" by simp
+  qed
 
   have PI_diff: "\<And>n. (\<integral>\<^isup>+ x. ereal (?diff n x) \<partial>M) =
     (\<integral>\<^isup>+ x. ereal (2 * w x) \<partial>M) - (\<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)"
     using diff w diff_less_2w w_pos
     by (subst positive_integral_diff[symmetric])
-       (auto simp: integrable_def intro!: positive_integral_cong)
+       (auto simp: integrable_def intro!: positive_integral_cong_AE)
 
   have "integrable M (\<lambda>x. 2 * w x)"
-    using w by (auto intro: integral_cmult)
+    using w by auto
   hence I2w_fin: "(\<integral>\<^isup>+ x. ereal (2 * w x) \<partial>M) \<noteq> \<infinity>" and
     borel_2w: "(\<lambda>x. ereal (2 * w x)) \<in> borel_measurable M"
     unfolding integrable_def by auto
 
   have "limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M) = 0" (is "limsup ?f = 0")
   proof cases
     assume eq_0: "(\<integral>\<^isup>+ x. max 0 (ereal (2 * w x)) \<partial>M) = 0" (is "?wx = 0")
     { fix n
       have "?f n \<le> ?wx" (is "integral\<^isup>P M ?f' \<le> _")
-        using diff_less_2w[of _ n] unfolding positive_integral_max_0
-        by (intro positive_integral_mono) auto
+        using diff_less_2w unfolding positive_integral_max_0
+        by (intro positive_integral_mono_AE) auto
       then have "?f n = 0"
         using positive_integral_positive[of M ?f'] eq_0 by auto }
     then show ?thesis by (simp add: Limsup_const)
   next
     assume neq_0: "(\<integral>\<^isup>+ x. max 0 (ereal (2 * w x)) \<partial>M) \<noteq> 0" (is "?wx \<noteq> 0")
     have "0 = limsup (\<lambda>n. 0 :: ereal)" by (simp add: Limsup_const)
     also have "\<dots> \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)"
       by (intro limsup_mono positive_integral_positive)
     finally have pos: "0 \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)" .
     have "?wx = (\<integral>\<^isup>+ x. liminf (\<lambda>n. max 0 (ereal (?diff n x))) \<partial>M)"
-    proof (rule positive_integral_cong)
-      fix x assume x: "x \<in> space M"
+      using u'
+    proof (intro positive_integral_cong_AE, eventually_elim)
+      fix x assume u': "(\<lambda>i. u i x) ----> u' x"
       show "max 0 (ereal (2 * w x)) = liminf (\<lambda>n. max 0 (ereal (?diff n x)))"
         unfolding ereal_max_0
       proof (rule lim_imp_Liminf[symmetric], unfold lim_ereal)
         have "(\<lambda>i. ?diff i x) ----> 2 * w x - \<bar>u' x - u' x\<bar>"
-          using u'[OF x] by (safe intro!: tendsto_intros)
+          using u' by (safe intro!: tendsto_intros)
         then show "(\<lambda>i. max 0 (?diff i x)) ----> max 0 (2 * w x)"
-          by (auto intro!: tendsto_real_max simp add: lim_ereal)
+          by (auto intro!: tendsto_real_max)
       qed (rule trivial_limit_sequentially)
     qed
     also have "\<dots> \<le> liminf (\<lambda>n. \<integral>\<^isup>+ x. max 0 (ereal (?diff n x)) \<partial>M)"
-      using u'_borel w u unfolding integrable_def
+      using borel w u unfolding integrable_def
       by (intro positive_integral_lim_INF) (auto intro!: positive_integral_lim_INF)
     also have "\<dots> = (\<integral>\<^isup>+ x. ereal (2 * w x) \<partial>M) -
         limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)"
       unfolding PI_diff positive_integral_max_0
       using positive_integral_positive[of M "\<lambda>x. ereal (2 * w x)"]

   have "\<And>n. (\<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M) = ereal (\<integral>x. \<bar>u n x - u' x\<bar> \<partial>M)"
     using diff positive_integral_positive[of M]
     by (subst integral_eq_positive_integral[of _ M]) (auto simp: ereal_real integrable_def)
   then show ?lim_diff
     using ereal_Liminf_eq_Limsup[OF trivial_limit_sequentially liminf_limsup_eq]
-    by (simp add: lim_ereal)
+    by simp
 
   show ?lim
   proof (rule LIMSEQ_I)
     fix r :: real assume "0 < r"
     from LIMSEQ_D[OF `?lim_diff` this]

 
     show "\<exists>N. \<forall>n\<ge>N. norm (integral\<^isup>L M (u n) - integral\<^isup>L M u') < r"
     proof (safe intro!: exI[of _ N])
       fix n assume "N \<le> n"
       have "\<bar>integral\<^isup>L M (u n) - integral\<^isup>L M u'\<bar> = \<bar>(\<integral>x. u n x - u' x \<partial>M)\<bar>"
-        using u `integrable M u'` by (auto simp: integral_diff)
+        using u `integrable M u'` by auto
       also have "\<dots> \<le> (\<integral>x. \<bar>u n x - u' x\<bar> \<partial>M)" using u `integrable M u'`
-        by (rule_tac integral_triangle_inequality) (auto intro!: integral_diff)
+        by (rule_tac integral_triangle_inequality) auto
       also note N[OF `N \<le> n`]
       finally show "norm (integral\<^isup>L M (u n) - integral\<^isup>L M u') < r" by simp
     qed
   qed
 qed

 proof -
   have "\<forall>x\<in>space M. \<exists>w. (\<lambda>i. \<bar>f i x\<bar>) sums w"
     using summable unfolding summable_def by auto
   from bchoice[OF this]
   obtain w where w: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. \<bar>f i x\<bar>) sums w x" by auto
+  then have w_borel: "w \<in> borel_measurable M" unfolding sums_def
+    by (rule borel_measurable_LIMSEQ) (auto simp: borel[THEN integrableD(1)])
 
   let ?w = "\<lambda>y. if y \<in> space M then w y else 0"
 
   obtain x where abs_sum: "(\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M)) sums x"
     using sums unfolding summable_def ..
 
   have 1: "\<And>n. integrable M (\<lambda>x. \<Sum>i = 0..<n. f i x)"
-    using borel by (auto intro!: integral_setsum)
-
-  { fix j x assume [simp]: "x \<in> space M"
+    using borel by auto
+
+  have 2: "\<And>j. AE x in M. \<bar>\<Sum>i = 0..<j. f i x\<bar> \<le> ?w x"
+    using AE_space
+  proof eventually_elim
+    fix j x assume [simp]: "x \<in> space M"
     have "\<bar>\<Sum>i = 0..< j. f i x\<bar> \<le> (\<Sum>i = 0..< j. \<bar>f i x\<bar>)" by (rule setsum_abs)
     also have "\<dots> \<le> w x" using w[of x] series_pos_le[of "\<lambda>i. \<bar>f i x\<bar>"] unfolding sums_iff by auto
-    finally have "\<bar>\<Sum>i = 0..<j. f i x\<bar> \<le> ?w x" by simp }
-  note 2 = this
+    finally show "\<bar>\<Sum>i = 0..<j. f i x\<bar> \<le> ?w x" by simp
+  qed
 
   have 3: "integrable M ?w"
   proof (rule integral_monotone_convergence(1))
     let ?F = "\<lambda>n y. (\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
     let ?w' = "\<lambda>n y. if y \<in> space M then ?F n y else 0"
     have "\<And>n. integrable M (?F n)"
       using borel by (auto intro!: integral_setsum integrable_abs)
     thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
-    show "mono ?w'"
+    show "AE x in M. mono (\<lambda>n. ?w' n x)"
       by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
-    { fix x show "(\<lambda>n. ?w' n x) ----> ?w x"
-        using w by (cases "x \<in> space M") (simp_all add: tendsto_const sums_def) }
+    show "AE x in M. (\<lambda>n. ?w' n x) ----> ?w x"
+        using w by (simp_all add: tendsto_const sums_def)
     have *: "\<And>n. integral\<^isup>L M (?w' n) = (\<Sum>i = 0..< n. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
-      using borel by (simp add: integral_setsum integrable_abs cong: integral_cong)
+      using borel by (simp add: integrable_abs cong: integral_cong)
     from abs_sum
     show "(\<lambda>i. integral\<^isup>L M (?w' i)) ----> x" unfolding * sums_def .
-  qed
+  qed (simp add: w_borel measurable_If_set)
 
   from summable[THEN summable_rabs_cancel]
-  have 4: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>n. \<Sum>i = 0..<n. f i x) ----> (\<Sum>i. f i x)"
+  have 4: "AE x in M. (\<lambda>n. \<Sum>i = 0..<n. f i x) ----> (\<Sum>i. f i x)"
     by (auto intro: summable_sumr_LIMSEQ_suminf)
 
-  note int = integral_dominated_convergence(1,3)[OF 1 2 3 4]
+  note int = integral_dominated_convergence(1,3)[OF 1 2 3 4
+    borel_measurable_suminf[OF integrableD(1)[OF borel]]]
 
   from int show "integrable M ?S" by simp
 
   show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF borel]
     using int(2) by simp

   then show ?thesis
     using f unfolding lebesgue_integral_def integrable_def
     by (auto simp: borel[THEN positive_integral_distr[OF T]])
 qed
 
+lemma integrable_distr_eq:
+  assumes T: "T \<in> measurable M M'" "f \<in> borel_measurable M'"
+  shows "integrable (distr M M' T) f \<longleftrightarrow> integrable M (\<lambda>x. f (T x))"
+  using T measurable_comp[OF T]
+  unfolding integrable_def 
+  by (subst (1 2) positive_integral_distr) (auto simp: comp_def)
+
 lemma integrable_distr:
-  assumes T: "T \<in> measurable M M'" and f: "integrable (distr M M' T) f"
-  shows "integrable M (\<lambda>x. f (T x))"
-proof -
-  from measurable_comp[OF T, of f borel]
-  have borel: "(\<lambda>x. ereal (f x)) \<in> borel_measurable M'" "(\<lambda>x. ereal (- f x)) \<in> borel_measurable M'"
-    and "(\<lambda>x. f (T x)) \<in> borel_measurable M"
-    using f by (auto simp: comp_def)
-  then show ?thesis
-    using f unfolding lebesgue_integral_def integrable_def
-    using borel[THEN positive_integral_distr[OF T]]
-    by (auto simp: borel[THEN positive_integral_distr[OF T]])
-qed
+  assumes T: "T \<in> measurable M M'" shows "integrable (distr M M' T) f \<Longrightarrow> integrable M (\<lambda>x. f (T x))"
+  by (subst integrable_distr_eq[symmetric, OF T]) auto
 
 section {* Lebesgue integration on @{const count_space} *}
 
 lemma simple_function_count_space[simp]:
   "simple_function (count_space A) f \<longleftrightarrow> finite (f ` A)"

 lemma positive_integral_count_space_finite:
     "finite A \<Longrightarrow> (\<integral>\<^isup>+x. f x \<partial>count_space A) = (\<Sum>a\<in>A. max 0 (f a))"
   by (subst positive_integral_max_0[symmetric])
      (auto intro!: setsum_mono_zero_left simp: positive_integral_count_space less_le)
 
+lemma lebesgue_integral_count_space_finite_support:
+  assumes f: "finite {a\<in>A. f a \<noteq> 0}" shows "(\<integral>x. f x \<partial>count_space A) = (\<Sum>a | a \<in> A \<and> f a \<noteq> 0. f a)"
+proof -
+  have *: "\<And>r::real. 0 < max 0 r \<longleftrightarrow> 0 < r" "\<And>x. max 0 (ereal x) = ereal (max 0 x)"
+    "\<And>a. a \<in> A \<and> 0 < f a \<Longrightarrow> max 0 (f a) = f a"
+    "\<And>a. a \<in> A \<and> f a < 0 \<Longrightarrow> max 0 (- f a) = - f a"
+    "{a \<in> A. f a \<noteq> 0} = {a \<in> A. 0 < f a} \<union> {a \<in> A. f a < 0}"
+    "({a \<in> A. 0 < f a} \<inter> {a \<in> A. f a < 0}) = {}"
+    by (auto split: split_max)
+  have "finite {a \<in> A. 0 < f a}" "finite {a \<in> A. f a < 0}"
+    by (auto intro: finite_subset[OF _ f])
+  then show ?thesis
+    unfolding lebesgue_integral_def
+    apply (subst (1 2) positive_integral_max_0[symmetric])
+    apply (subst (1 2) positive_integral_count_space)
+    apply (auto simp add: * setsum_negf setsum_Un
+                simp del: ereal_max)
+    done
+qed
+
 lemma lebesgue_integral_count_space_finite:
     "finite A \<Longrightarrow> (\<integral>x. f x \<partial>count_space A) = (\<Sum>a\<in>A. f a)"
   apply (auto intro!: setsum_mono_zero_left
               simp: positive_integral_count_space_finite lebesgue_integral_def)
   apply (subst (1 2)  setsum_real_of_ereal[symmetric])
   apply (auto simp: max_def setsum_subtractf[symmetric] intro!: setsum_cong)
   done
+
+lemma borel_measurable_count_space[simp, intro!]:
+  "f \<in> borel_measurable (count_space A)"
+  by simp
 
 section {* Measure spaces with an associated density *}
 
 definition density :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
   "density M f = measure_of (space M) (sets M) (\<lambda>A. \<integral>\<^isup>+ x. f x * indicator A x \<partial>M)"

   then have g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
     using g' by auto
   from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess G . note G = this
   note G' = borel_measurable_simple_function[OF this(1)] simple_functionD[OF G(1)]
   note G'(2)[simp]
-  { fix P have "AE x in M. P x \<Longrightarrow> AE x in M. P x"
-      using positive_integral_null_set[of _ _ f]
-      by (auto simp: eventually_ae_filter ) }
-  note ac = this
   with G(4) f g have G_M': "AE x in density M f. (SUP i. G i x) = g x"
     by (auto simp add: AE_density[OF f(1)] max_def)
   { fix i
     let ?I = "\<lambda>y x. indicator (G i -` {y} \<inter> space M) x"
     { fix x assume *: "x \<in> space M" "0 \<le> f x" "0 \<le> g x"