# HG changeset patch
# User hoelzl
# Date 1399973747 -7200
# Node ID d1a937cbf8582063ef46dce9093409b3abc50ec0
# Parent  1144d7ec892a26f63c1628f23a9e0e770c6f0e05
clean up Lebesgue integration

diff -r 1144d7ec892a -r d1a937cbf858 src/HOL/Probability/Complete_Measure.thy
--- a/src/HOL/Probability/Complete_Measure.thy	Tue May 13 11:11:51 2014 +0200
+++ b/src/HOL/Probability/Complete_Measure.thy	Tue May 13 11:35:47 2014 +0200
@@ -288,7 +288,7 @@
       ultimately show "g x = ?f x" by auto
     qed
     show "?f \<in> borel_measurable M"
-      using sf by (auto intro: borel_measurable_simple_function)
+      using sf[THEN borel_measurable_simple_function] by auto
   qed
 qed
 
diff -r 1144d7ec892a -r d1a937cbf858 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue May 13 11:11:51 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue May 13 11:35:47 2014 +0200
@@ -9,28 +9,9 @@
   imports Measure_Space Borel_Space
 begin
 
-lemma tendsto_real_max:
-  fixes x y :: real
-  assumes "(X ---> x) net"
-  assumes "(Y ---> y) net"
-  shows "((\<lambda>x. max (X x) (Y x)) ---> max x y) net"
-proof -
-  have *: "\<And>x y :: real. max x y = y + ((x - y) + norm (x - y)) / 2"
-    by (auto split: split_max simp: field_simps)
-  show ?thesis
-    unfolding *
-    by (intro tendsto_add assms tendsto_divide tendsto_norm tendsto_diff) auto
-qed
-
-lemma measurable_sets2[intro]:
-  assumes "f \<in> measurable M M'" "g \<in> measurable M M''"
-  and "A \<in> sets M'" "B \<in> sets M''"
-  shows "f -` A \<inter> g -` B \<inter> space M \<in> sets M"
-proof -
-  have "f -` A \<inter> g -` B \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)"
-    by auto
-  then show ?thesis using assms by (auto intro: measurable_sets)
-qed
+lemma indicator_less_ereal[simp]:
+  "indicator A x \<le> (indicator B x::ereal) \<longleftrightarrow> (x \<in> A \<longrightarrow> x \<in> B)"
+  by (simp add: indicator_def not_le)
 
 section "Simple function"
 
@@ -58,6 +39,22 @@
     by (auto simp del: UN_simps simp: simple_function_def)
 qed
 
+lemma measurable_simple_function[measurable_dest]:
+  "simple_function M f \<Longrightarrow> f \<in> measurable M (count_space UNIV)"
+  unfolding simple_function_def measurable_def
+proof safe
+  fix A assume "finite (f ` space M)" "\<forall>x\<in>f ` space M. f -` {x} \<inter> space M \<in> sets M"
+  then have "(\<Union>x\<in>f ` space M. if x \<in> A then f -` {x} \<inter> space M else {}) \<in> sets M"
+    by (intro sets.finite_UN) auto
+  also have "(\<Union>x\<in>f ` space M. if x \<in> A then f -` {x} \<inter> space M else {}) = f -` A \<inter> space M"
+    by (auto split: split_if_asm)
+  finally show "f -` A \<inter> space M \<in> sets M" .
+qed simp
+
+lemma borel_measurable_simple_function:
+  "simple_function M f \<Longrightarrow> f \<in> borel_measurable M"
+  by (auto dest!: measurable_simple_function simp: measurable_def)
+
 lemma simple_function_measurable2[intro]:
   assumes "simple_function M f" "simple_function M g"
   shows "f -` A \<inter> g -` B \<inter> space M \<in> sets M"
@@ -106,22 +103,6 @@
   shows "simple_function M f \<longleftrightarrow> simple_function N f"
   unfolding simple_function_def assms ..
 
-lemma borel_measurable_simple_function[measurable_dest]:
-  assumes "simple_function M f"
-  shows "f \<in> borel_measurable M"
-proof (rule borel_measurableI)
-  fix S
-  let ?I = "f ` (f -` S \<inter> space M)"
-  have *: "(\<Union>x\<in>?I. f -` {x} \<inter> space M) = f -` S \<inter> space M" (is "?U = _") by auto
-  have "finite ?I"
-    using assms unfolding simple_function_def
-    using finite_subset[of "f ` (f -` S \<inter> space M)" "f ` space M"] by auto
-  hence "?U \<in> sets M"
-    apply (rule sets.finite_UN)
-    using assms unfolding simple_function_def by auto
-  thus "f -` S \<inter> space M \<in> sets M" unfolding * .
-qed
-
 lemma simple_function_borel_measurable:
   fixes f :: "'a \<Rightarrow> 'x::{t2_space}"
   assumes "f \<in> borel_measurable M" and "finite (f ` space M)"
@@ -129,10 +110,10 @@
   using assms unfolding simple_function_def
   by (auto intro: borel_measurable_vimage)
 
-lemma simple_function_eq_borel_measurable:
+lemma simple_function_eq_measurable:
   fixes f :: "'a \<Rightarrow> ereal"
-  shows "simple_function M f \<longleftrightarrow> finite (f`space M) \<and> f \<in> borel_measurable M"
-  using simple_function_borel_measurable[of f] borel_measurable_simple_function[of M f]
+  shows "simple_function M f \<longleftrightarrow> finite (f`space M) \<and> f \<in> measurable M (count_space UNIV)"
+  using simple_function_borel_measurable[of f] measurable_simple_function[of M f]
   by (fastforce simp: simple_function_def)
 
 lemma simple_function_const[intro, simp]:
@@ -215,14 +196,14 @@
   assume "finite P" from this assms show ?thesis by induct auto
 qed auto
 
-lemma
+lemma simple_function_ereal[intro, simp]: 
   fixes f g :: "'a \<Rightarrow> real" assumes sf: "simple_function M f"
-  shows simple_function_ereal[intro, simp]: "simple_function M (\<lambda>x. ereal (f x))"
+  shows "simple_function M (\<lambda>x. ereal (f x))"
   by (auto intro!: simple_function_compose1[OF sf])
 
-lemma
+lemma simple_function_real_of_nat[intro, simp]: 
   fixes f g :: "'a \<Rightarrow> nat" assumes sf: "simple_function M f"
-  shows simple_function_real_of_nat[intro, simp]: "simple_function M (\<lambda>x. real (f x))"
+  shows "simple_function M (\<lambda>x. real (f x))"
   by (auto intro!: simple_function_compose1[OF sf])
 
 lemma borel_measurable_implies_simple_function_sequence:
@@ -521,68 +502,67 @@
 
 lemma simple_function_partition:
   assumes f: "simple_function M f" and g: "simple_function M g"
-  shows "integral\<^sup>S M f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. the_elem (f`A) * (emeasure M) A)"
-    (is "_ = setsum _ (?p ` space M)")
-proof-
-  let ?sub = "\<lambda>x. ?p ` (f -` {x} \<inter> space M)"
-  let ?SIGMA = "Sigma (f`space M) ?sub"
+  assumes sub: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow> g x = g y \<Longrightarrow> f x = f y"
+  assumes v: "\<And>x. x \<in> space M \<Longrightarrow> f x = v (g x)"
+  shows "integral\<^sup>S M f = (\<Sum>y\<in>g ` space M. v y * emeasure M {x\<in>space M. g x = y})"
+    (is "_ = ?r")
+proof -
+  from f g have [simp]: "finite (f`space M)" "finite (g`space M)"
+    by (auto simp: simple_function_def)
+  from f g have [measurable]: "f \<in> measurable M (count_space UNIV)" "g \<in> measurable M (count_space UNIV)"
+    by (auto intro: measurable_simple_function)
 
-  have [intro]:
-    "finite (f ` space M)"
-    "finite (g ` space M)"
-    using assms unfolding simple_function_def by simp_all
-
-  { fix A
-    have "?p ` (A \<inter> space M) \<subseteq>
-      (\<lambda>(x,y). f -` {x} \<inter> g -` {y} \<inter> space M) ` (f`space M \<times> g`space M)"
-      by auto
-    hence "finite (?p ` (A \<inter> space M))"
-      by (rule finite_subset) auto }
-  note this[intro, simp]
-  note sets = simple_function_measurable2[OF f g]
+  { fix y assume "y \<in> space M"
+    then have "f ` space M \<inter> {i. \<exists>x\<in>space M. i = f x \<and> g y = g x} = {v (g y)}"
+      by (auto cong: sub simp: v[symmetric]) }
+  note eq = this
 
-  { fix x assume "x \<in> space M"
-    have "\<Union>(?sub (f x)) = (f -` {f x} \<inter> space M)" by auto
-    with sets have "(emeasure M) (f -` {f x} \<inter> space M) = setsum (emeasure M) (?sub (f x))"
-      by (subst setsum_emeasure) (auto simp: disjoint_family_on_def) }
-  hence "integral\<^sup>S M f = (\<Sum>(x,A)\<in>?SIGMA. x * (emeasure M) A)"
-    unfolding simple_integral_def using f sets
-    by (subst setsum_Sigma[symmetric])
-       (auto intro!: setsum_cong setsum_ereal_right_distrib)
-  also have "\<dots> = (\<Sum>A\<in>?p ` space M. the_elem (f`A) * (emeasure M) A)"
-  proof -
-    have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI)
-    have "(\<lambda>A. (the_elem (f ` A), A)) ` ?p ` space M
-      = (\<lambda>x. (f x, ?p x)) ` space M"
-    proof safe
-      fix x assume "x \<in> space M"
-      thus "(f x, ?p x) \<in> (\<lambda>A. (the_elem (f`A), A)) ` ?p ` space M"
-        by (auto intro!: image_eqI[of _ _ "?p x"])
-    qed auto
-    thus ?thesis
-      apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (the_elem (f`A), A)"] inj_onI)
-      apply (rule_tac x="xa" in image_eqI)
-      by simp_all
+  have "integral\<^sup>S M f =
+    (\<Sum>y\<in>f`space M. y * (\<Sum>z\<in>g`space M. 
+      if \<exists>x\<in>space M. y = f x \<and> z = g x then emeasure M {x\<in>space M. g x = z} else 0))"
+    unfolding simple_integral_def
+  proof (safe intro!: setsum_cong ereal_left_mult_cong)
+    fix y assume y: "y \<in> space M" "f y \<noteq> 0"
+    have [simp]: "g ` space M \<inter> {z. \<exists>x\<in>space M. f y = f x \<and> z = g x} = 
+        {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"
+      by auto
+    have eq:"(\<Union>i\<in>{z. \<exists>x\<in>space M. f y = f x \<and> z = g x}. {x \<in> space M. g x = i}) =
+        f -` {f y} \<inter> space M"
+      by (auto simp: eq_commute cong: sub rev_conj_cong)
+    have "finite (g`space M)" by simp
+    then have "finite {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"
+      by (rule rev_finite_subset) auto
+    then show "emeasure M (f -` {f y} \<inter> space M) =
+      (\<Sum>z\<in>g ` space M. if \<exists>x\<in>space M. f y = f x \<and> z = g x then emeasure M {x \<in> space M. g x = z} else 0)"
+      apply (simp add: setsum_cases)
+      apply (subst setsum_emeasure)
+      apply (auto simp: disjoint_family_on_def eq)
+      done
   qed
-  finally show ?thesis .
+  also have "\<dots> = (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M. 
+      if \<exists>x\<in>space M. y = f x \<and> z = g x then y * emeasure M {x\<in>space M. g x = z} else 0))"
+    by (auto intro!: setsum_cong simp: setsum_ereal_right_distrib emeasure_nonneg)
+  also have "\<dots> = ?r"
+    by (subst setsum_commute)
+       (auto intro!: setsum_cong simp: setsum_cases scaleR_setsum_right[symmetric] eq)
+  finally show "integral\<^sup>S M f = ?r" .
 qed
 
 lemma simple_integral_add[simp]:
   assumes f: "simple_function M f" and "\<And>x. 0 \<le> f x" and g: "simple_function M g" and "\<And>x. 0 \<le> g x"
   shows "(\<integral>\<^sup>Sx. f x + g x \<partial>M) = integral\<^sup>S M f + integral\<^sup>S M g"
 proof -
-  { fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
-    assume "x \<in> space M"
-    hence "(\<lambda>a. f a + g a) ` ?S = {f x + g x}" "f ` ?S = {f x}" "g ` ?S = {g x}"
-        "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M = ?S"
-      by auto }
-  with assms show ?thesis
-    unfolding
-      simple_function_partition[OF simple_function_add[OF f g] simple_function_Pair[OF f g]]
-      simple_function_partition[OF f g]
-      simple_function_partition[OF g f]
-    by (subst (3) Int_commute)
-       (auto simp add: ereal_left_distrib setsum_addf[symmetric] intro!: setsum_cong)
+  have "(\<integral>\<^sup>Sx. f x + g x \<partial>M) =
+    (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. (fst y + snd y) * emeasure M {x\<in>space M. (f x, g x) = y})"
+    by (intro simple_function_partition) (auto intro: f g)
+  also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. fst y * emeasure M {x\<in>space M. (f x, g x) = y}) +
+    (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. snd y * emeasure M {x\<in>space M. (f x, g x) = y})"
+    using assms(2,4) by (auto intro!: setsum_cong ereal_left_distrib simp: setsum_addf[symmetric])
+  also have "(\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. fst y * emeasure M {x\<in>space M. (f x, g x) = y}) = (\<integral>\<^sup>Sx. f x \<partial>M)"
+    by (intro simple_function_partition[symmetric]) (auto intro: f g)
+  also have "(\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. snd y * emeasure M {x\<in>space M. (f x, g x) = y}) = (\<integral>\<^sup>Sx. g x \<partial>M)"
+    by (intro simple_function_partition[symmetric]) (auto intro: f g)
+  finally show ?thesis .
 qed
 
 lemma simple_integral_setsum[simp]:
@@ -599,53 +579,42 @@
   assumes f: "simple_function M f" "\<And>x. 0 \<le> f x"
   shows "(\<integral>\<^sup>Sx. c * f x \<partial>M) = c * integral\<^sup>S M f"
 proof -
-  note mult = simple_function_mult[OF simple_function_const[of _ c] f(1)]
-  { fix x let ?S = "f -` {f x} \<inter> (\<lambda>x. c * f x) -` {c * f x} \<inter> space M"
-    assume "x \<in> space M"
-    hence "(\<lambda>x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}"
-      by auto }
-  with assms show ?thesis
-    unfolding simple_function_partition[OF mult f(1)]
-              simple_function_partition[OF f(1) mult]
-    by (subst setsum_ereal_right_distrib)
-       (auto intro!: ereal_0_le_mult setsum_cong simp: mult_assoc)
+  have "(\<integral>\<^sup>Sx. c * f x \<partial>M) = (\<Sum>y\<in>f ` space M. (c * y) * emeasure M {x\<in>space M. f x = y})"
+    using f by (intro simple_function_partition) auto
+  also have "\<dots> = c * integral\<^sup>S M f"
+    using f unfolding simple_integral_def
+    by (subst setsum_ereal_right_distrib) (auto simp: emeasure_nonneg mult_assoc Int_def conj_commute)
+  finally show ?thesis .
 qed
 
 lemma simple_integral_mono_AE:
-  assumes f: "simple_function M f" and g: "simple_function M g"
+  assumes f[measurable]: "simple_function M f" and g[measurable]: "simple_function M g"
   and mono: "AE x in M. f x \<le> g x"
   shows "integral\<^sup>S M f \<le> integral\<^sup>S M g"
 proof -
-  let ?S = "\<lambda>x. (g -` {g x} \<inter> space M) \<inter> (f -` {f x} \<inter> space M)"
-  have *: "\<And>x. g -` {g x} \<inter> f -` {f x} \<inter> space M = ?S x"
-    "\<And>x. f -` {f x} \<inter> g -` {g x} \<inter> space M = ?S x" by auto
-  show ?thesis
-    unfolding *
-      simple_function_partition[OF f g]
-      simple_function_partition[OF g f]
-  proof (safe intro!: setsum_mono)
+  let ?\<mu> = "\<lambda>P. emeasure M {x\<in>space M. P x}"
+  have "integral\<^sup>S M f = (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. fst y * ?\<mu> (\<lambda>x. (f x, g x) = y))"
+    using f g by (intro simple_function_partition) auto
+  also have "\<dots> \<le> (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. snd y * ?\<mu> (\<lambda>x. (f x, g x) = y))"
+  proof (clarsimp intro!: setsum_mono)
     fix x assume "x \<in> space M"
-    then have *: "f ` ?S x = {f x}" "g ` ?S x = {g x}" by auto
-    show "the_elem (f`?S x) * (emeasure M) (?S x) \<le> the_elem (g`?S x) * (emeasure M) (?S x)"
-    proof (cases "f x \<le> g x")
-      case True then show ?thesis
-        using * assms(1,2)[THEN simple_functionD(2)]
-        by (auto intro!: ereal_mult_right_mono)
-    next
-      case False
-      obtain N where N: "{x\<in>space M. \<not> f x \<le> g x} \<subseteq> N" "N \<in> sets M" "(emeasure M) N = 0"
-        using mono by (auto elim!: AE_E)
-      have "?S x \<subseteq> N" using N `x \<in> space M` False by auto
-      moreover have "?S x \<in> sets M" using assms
-        by (rule_tac sets.Int) (auto intro!: simple_functionD)
-      ultimately have "(emeasure M) (?S x) \<le> (emeasure M) N"
-        using `N \<in> sets M` by (auto intro!: emeasure_mono)
-      moreover have "0 \<le> (emeasure M) (?S x)"
-        using assms(1,2)[THEN simple_functionD(2)] by auto
-      ultimately have "(emeasure M) (?S x) = 0" using `(emeasure M) N = 0` by auto
-      then show ?thesis by simp
-    qed
+    let ?M = "?\<mu> (\<lambda>y. f y = f x \<and> g y = g x)"
+    show "f x * ?M \<le> g x * ?M"
+    proof cases
+      assume "?M \<noteq> 0"
+      then have "0 < ?M"
+        by (simp add: less_le emeasure_nonneg)
+      also have "\<dots> \<le> ?\<mu> (\<lambda>y. f x \<le> g x)"
+        using mono by (intro emeasure_mono_AE) auto
+      finally have "\<not> \<not> f x \<le> g x"
+        by (intro notI) auto
+      then show ?thesis
+        by (intro ereal_mult_right_mono) auto
+    qed simp
   qed
+  also have "\<dots> = integral\<^sup>S M g"
+    using f g by (intro simple_function_partition[symmetric]) auto
+  finally show ?thesis .
 qed
 
 lemma simple_integral_mono:
@@ -671,64 +640,37 @@
 qed simp
 
 lemma simple_integral_indicator:
-  assumes "A \<in> sets M"
+  assumes A: "A \<in> sets M"
   assumes f: "simple_function M f"
   shows "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) =
-    (\<Sum>x \<in> f ` space M. x * (emeasure M) (f -` {x} \<inter> space M \<inter> A))"
-proof (cases "A = space M")
-  case True
-  then have "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = integral\<^sup>S M f"
-    by (auto intro!: simple_integral_cong)
-  with True show ?thesis by (simp add: simple_integral_def)
-next
-  assume "A \<noteq> space M"
-  then obtain x where x: "x \<in> space M" "x \<notin> A" using sets.sets_into_space[OF assms(1)] by auto
-  have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _")
-  proof safe
-    fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto
-  next
-    fix y assume "y \<in> A" thus "f y \<in> ?I ` space M"
-      using sets.sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y])
-  next
-    show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x])
-  qed
-  have *: "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) =
-    (\<Sum>x \<in> f ` space M \<union> {0}. x * (emeasure M) (f -` {x} \<inter> space M \<inter> A))"
-    unfolding simple_integral_def I
-  proof (rule setsum_mono_zero_cong_left)
-    show "finite (f ` space M \<union> {0})"
-      using assms(2) unfolding simple_function_def by auto
-    show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}"
-      using sets.sets_into_space[OF assms(1)] by auto
-    have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}"
-      by (auto simp: image_iff)
-    thus "\<forall>i\<in>f ` space M \<union> {0} - (f ` A \<union> {0}).
-      i * (emeasure M) (f -` {i} \<inter> space M \<inter> A) = 0" by auto
-  next
-    fix x assume "x \<in> f`A \<union> {0}"
-    hence "x \<noteq> 0 \<Longrightarrow> ?I -` {x} \<inter> space M = f -` {x} \<inter> space M \<inter> A"
-      by (auto simp: indicator_def split: split_if_asm)
-    thus "x * (emeasure M) (?I -` {x} \<inter> space M) =
-      x * (emeasure M) (f -` {x} \<inter> space M \<inter> A)" by (cases "x = 0") simp_all
-  qed
-  show ?thesis unfolding *
-    using assms(2) unfolding simple_function_def
-    by (auto intro!: setsum_mono_zero_cong_right)
+    (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M \<inter> A))"
+proof -
+  have eq: "(\<lambda>x. (f x, indicator A x)) ` space M \<inter> {x. snd x = 1} = (\<lambda>x. (f x, 1::ereal))`A"
+    using A[THEN sets.sets_into_space] by (auto simp: indicator_def image_iff split: split_if_asm)
+  have eq2: "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}"
+    by (auto simp: image_iff)
+
+  have "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) =
+    (\<Sum>y\<in>(\<lambda>x. (f x, indicator A x))`space M. (fst y * snd y) * emeasure M {x\<in>space M. (f x, indicator A x) = y})"
+    using assms by (intro simple_function_partition) auto
+  also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, indicator A x::ereal))`space M.
+    if snd y = 1 then fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A) else 0)"
+    by (auto simp: indicator_def split: split_if_asm intro!: arg_cong2[where f="op *"] arg_cong2[where f=emeasure] setsum_cong)
+  also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, 1::ereal))`A. fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A))"
+    using assms by (subst setsum_cases) (auto intro!: simple_functionD(1) simp: eq)
+  also have "\<dots> = (\<Sum>y\<in>fst`(\<lambda>x. (f x, 1::ereal))`A. y * emeasure M (f -` {y} \<inter> space M \<inter> A))"
+    by (subst setsum_reindex[where f=fst]) (auto simp: inj_on_def)
+  also have "\<dots> = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M \<inter> A))"
+    using A[THEN sets.sets_into_space]
+    by (intro setsum_mono_zero_cong_left simple_functionD f) (auto simp: image_comp comp_def eq2)
+  finally show ?thesis .
 qed
 
 lemma simple_integral_indicator_only[simp]:
   assumes "A \<in> sets M"
   shows "integral\<^sup>S M (indicator A) = emeasure M A"
-proof cases
-  assume "space M = {}" hence "A = {}" using sets.sets_into_space[OF assms] by auto
-  thus ?thesis unfolding simple_integral_def using `space M = {}` by auto
-next
-  assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::ereal}" by auto
-  thus ?thesis
-    using simple_integral_indicator[OF assms simple_function_const[of _ 1]]
-    using sets.sets_into_space[OF assms]
-    by (auto intro!: arg_cong[where f="(emeasure M)"])
-qed
+  using simple_integral_indicator[OF assms, of "\<lambda>x. 1"] sets.sets_into_space[OF assms]
+  by (simp_all add: image_constant_conv Int_absorb1 split: split_if_asm)
 
 lemma simple_integral_null_set:
   assumes "simple_function M u" "\<And>x. 0 \<le> u x" and "N \<in> null_sets M"
@@ -748,7 +690,7 @@
 
 lemma simple_integral_cmult_indicator:
   assumes A: "A \<in> sets M"
-  shows "(\<integral>\<^sup>Sx. c * indicator A x \<partial>M) = c * (emeasure M) A"
+  shows "(\<integral>\<^sup>Sx. c * indicator A x \<partial>M) = c * emeasure M A"
   using simple_integral_mult[OF simple_function_indicator[OF A]]
   unfolding simple_integral_indicator_only[OF A] by simp
 
@@ -902,7 +844,7 @@
   hence "a \<noteq> 0" by auto
   let ?B = "\<lambda>i. {x \<in> space M. a * u x \<le> f i x}"
   have B: "\<And>i. ?B i \<in> sets M"
-    using f `simple_function M u` by auto
+    using f `simple_function M u`[THEN borel_measurable_simple_function] by auto
 
   let ?uB = "\<lambda>i x. u x * indicator (?B i) x"
 
@@ -1247,6 +1189,42 @@
   finally show False using `integral\<^sup>P M g \<noteq> \<infinity>` by auto
 qed
 
+lemma positive_integral_PInf:
+  assumes f: "f \<in> borel_measurable M"
+  and not_Inf: "integral\<^sup>P M f \<noteq> \<infinity>"
+  shows "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
+proof -
+  have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) = (\<integral>\<^sup>+ x. \<infinity> * indicator (f -` {\<infinity>} \<inter> space M) x \<partial>M)"
+    using f by (subst positive_integral_cmult_indicator) (auto simp: measurable_sets)
+  also have "\<dots> \<le> integral\<^sup>P M (\<lambda>x. max 0 (f x))"
+    by (auto intro!: positive_integral_mono simp: indicator_def max_def)
+  finally have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) \<le> integral\<^sup>P M f"
+    by (simp add: positive_integral_max_0)
+  moreover have "0 \<le> (emeasure M) (f -` {\<infinity>} \<inter> space M)"
+    by (rule emeasure_nonneg)
+  ultimately show ?thesis
+    using assms by (auto split: split_if_asm)
+qed
+
+lemma positive_integral_PInf_AE:
+  assumes "f \<in> borel_measurable M" "integral\<^sup>P M f \<noteq> \<infinity>" shows "AE x in M. f x \<noteq> \<infinity>"
+proof (rule AE_I)
+  show "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
+    by (rule positive_integral_PInf[OF assms])
+  show "f -` {\<infinity>} \<inter> space M \<in> sets M"
+    using assms by (auto intro: borel_measurable_vimage)
+qed auto
+
+lemma simple_integral_PInf:
+  assumes "simple_function M f" "\<And>x. 0 \<le> f x"
+  and "integral\<^sup>S M f \<noteq> \<infinity>"
+  shows "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
+proof (rule positive_integral_PInf)
+  show "f \<in> borel_measurable M" using assms by (auto intro: borel_measurable_simple_function)
+  show "integral\<^sup>P M f \<noteq> \<infinity>"
+    using assms by (simp add: positive_integral_eq_simple_integral)
+qed
+
 lemma positive_integral_diff:
   assumes f: "f \<in> borel_measurable M"
   and g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
@@ -1977,42 +1955,6 @@
     by (auto simp add: real_of_ereal_eq_0)
 qed
 
-lemma positive_integral_PInf:
-  assumes f: "f \<in> borel_measurable M"
-  and not_Inf: "integral\<^sup>P M f \<noteq> \<infinity>"
-  shows "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
-proof -
-  have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) = (\<integral>\<^sup>+ x. \<infinity> * indicator (f -` {\<infinity>} \<inter> space M) x \<partial>M)"
-    using f by (subst positive_integral_cmult_indicator) (auto simp: measurable_sets)
-  also have "\<dots> \<le> integral\<^sup>P M (\<lambda>x. max 0 (f x))"
-    by (auto intro!: positive_integral_mono simp: indicator_def max_def)
-  finally have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) \<le> integral\<^sup>P M f"
-    by (simp add: positive_integral_max_0)
-  moreover have "0 \<le> (emeasure M) (f -` {\<infinity>} \<inter> space M)"
-    by (rule emeasure_nonneg)
-  ultimately show ?thesis
-    using assms by (auto split: split_if_asm)
-qed
-
-lemma positive_integral_PInf_AE:
-  assumes "f \<in> borel_measurable M" "integral\<^sup>P M f \<noteq> \<infinity>" shows "AE x in M. f x \<noteq> \<infinity>"
-proof (rule AE_I)
-  show "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
-    by (rule positive_integral_PInf[OF assms])
-  show "f -` {\<infinity>} \<inter> space M \<in> sets M"
-    using assms by (auto intro: borel_measurable_vimage)
-qed auto
-
-lemma simple_integral_PInf:
-  assumes "simple_function M f" "\<And>x. 0 \<le> f x"
-  and "integral\<^sup>S M f \<noteq> \<infinity>"
-  shows "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
-proof (rule positive_integral_PInf)
-  show "f \<in> borel_measurable M" using assms by (auto intro: borel_measurable_simple_function)
-  show "integral\<^sup>P M f \<noteq> \<infinity>"
-    using assms by (simp add: positive_integral_eq_simple_integral)
-qed
-
 lemma integral_real:
   "AE x in M. \<bar>f x\<bar> \<noteq> \<infinity> \<Longrightarrow> (\<integral>x. real (f x) \<partial>M) = real (integral\<^sup>P M f) - real (integral\<^sup>P M (\<lambda>x. - f x))"
   using assms unfolding lebesgue_integral_def
@@ -2046,10 +1988,6 @@
   assumes "AE x in M. \<bar>f x\<bar> \<le> B" and "f \<in> borel_measurable M" shows "integrable M f"
   by (auto intro: integrable_bound[where f="\<lambda>x. B"] lebesgue_integral_const assms)
 
-lemma indicator_less[simp]:
-  "indicator A x \<le> (indicator B x::ereal) \<longleftrightarrow> (x \<in> A \<longrightarrow> x \<in> B)"
-  by (simp add: indicator_def not_le)
-
 lemma (in finite_measure) integral_less_AE:
   assumes int: "integrable M X" "integrable M Y"
   assumes A: "(emeasure M) A \<noteq> 0" "A \<in> sets M" "AE x in M. x \<in> A \<longrightarrow> X x \<noteq> Y x"
@@ -2158,7 +2096,7 @@
         have "(\<lambda>i. ?diff i x) ----> 2 * w x - \<bar>u' x - u' x\<bar>"
           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)
+          by (auto intro!: tendsto_max)
       qed (rule trivial_limit_sequentially)
     qed
     also have "\<dots> \<le> liminf (\<lambda>n. \<integral>\<^sup>+ x. max 0 (ereal (?diff n x)) \<partial>M)"
@@ -2517,13 +2455,6 @@
   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
-
-lemma lessThan_eq_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
-  by auto
-
 lemma emeasure_UN_countable:
   assumes sets: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" and I: "countable I" 
   assumes disj: "disjoint_family_on X I"
@@ -2943,9 +2874,6 @@
   finally show ?thesis .
 qed
 
-lemma emeasure_neq_0_sets: "emeasure M A \<noteq> 0 \<Longrightarrow> A \<in> sets M"
-  using emeasure_notin_sets[of A M] by blast
-
 lemma measure_uniform_measure[simp]:
   assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>" and B: "B \<in> sets M"
   shows "measure (uniform_measure M A) B = measure M (A \<inter> B) / measure M A"
diff -r 1144d7ec892a -r d1a937cbf858 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue May 13 11:11:51 2014 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue May 13 11:35:47 2014 +0200
@@ -1266,6 +1266,9 @@
 lemma emeasure_notin_sets: "A \<notin> sets M \<Longrightarrow> emeasure M A = 0"
   by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)
 
+lemma emeasure_neq_0_sets: "emeasure M A \<noteq> 0 \<Longrightarrow> A \<in> sets M"
+  using emeasure_notin_sets[of A M] by blast
+
 lemma measure_notin_sets: "A \<notin> sets M \<Longrightarrow> measure M A = 0"
   by (simp add: measure_def emeasure_notin_sets)
 
diff -r 1144d7ec892a -r d1a937cbf858 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue May 13 11:11:51 2014 +0200
+++ b/src/HOL/Set_Interval.thy	Tue May 13 11:35:47 2014 +0200
@@ -467,6 +467,12 @@
   "{x..y} = UNIV \<longleftrightarrow> (x = bot \<and> y = top)"
 by (auto simp: set_eq_iff intro: top_le le_bot)
 
+lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \<longleftrightarrow> n = bot"
+  by (auto simp: set_eq_iff not_less le_bot)
+
+lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
+  by (simp add: Iio_eq_empty_iff bot_nat_def)
+
 
 subsection {* Infinite intervals *}
 
diff -r 1144d7ec892a -r d1a937cbf858 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue May 13 11:11:51 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy	Tue May 13 11:35:47 2014 +0200
@@ -973,6 +973,41 @@
 lemma tendsto_bot [simp]: "(f ---> a) bot"
   unfolding tendsto_def by simp
 
+lemma tendsto_max:
+  fixes x y :: "'a::linorder_topology"
+  assumes X: "(X ---> x) net"
+  assumes Y: "(Y ---> y) net"
+  shows "((\<lambda>x. max (X x) (Y x)) ---> max x y) net"
+proof (rule order_tendstoI)
+  fix a assume "a < max x y"
+  then show "eventually (\<lambda>x. a < max (X x) (Y x)) net"
+    using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a]
+    by (auto simp: less_max_iff_disj elim: eventually_elim1)
+next
+  fix a assume "max x y < a"
+  then show "eventually (\<lambda>x. max (X x) (Y x) < a) net"
+    using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a]
+    by (auto simp: eventually_conj_iff)
+qed
+
+lemma tendsto_min:
+  fixes x y :: "'a::linorder_topology"
+  assumes X: "(X ---> x) net"
+  assumes Y: "(Y ---> y) net"
+  shows "((\<lambda>x. min (X x) (Y x)) ---> min x y) net"
+proof (rule order_tendstoI)
+  fix a assume "a < min x y"
+  then show "eventually (\<lambda>x. a < min (X x) (Y x)) net"
+    using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a]
+    by (auto simp: eventually_conj_iff)
+next
+  fix a assume "min x y < a"
+  then show "eventually (\<lambda>x. min (X x) (Y x) < a) net"
+    using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a]
+    by (auto simp: min_less_iff_disj elim: eventually_elim1)
+qed
+
+
 lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a within s)"
   unfolding tendsto_def eventually_at_topological by auto