# HG changeset patch
# User hoelzl
# Date 1349863936 -7200
# Node ID dfa8ddb874ceb094b1b8721510ad99ee65396df0
# Parent  16907431e477c79314ce6e4a1181086d5bc3f078
use continuity to show Borel-measurability

diff -r 16907431e477 -r dfa8ddb874ce src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Oct 10 12:12:15 2012 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Oct 10 12:12:16 2012 +0200
@@ -632,7 +632,7 @@
   "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
   using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
 
-lemma borel_measurable_euclidean_component:
+lemma borel_measurable_euclidean_component':
   "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel"
 proof (rule borel_measurableI)
   fix S::"real set" assume "open S"
@@ -641,13 +641,18 @@
     by (auto intro: borel_open)
 qed
 
+lemma borel_measurable_euclidean_component:
+  fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
+  assumes f: "f \<in> borel_measurable M"
+  shows "(\<lambda>x. f x $$ i) \<in> borel_measurable M"
+  using measurable_comp[OF f borel_measurable_euclidean_component'] by (simp add: comp_def)
+
 lemma borel_measurable_euclidean_space:
   fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M)"
 proof safe
   fix i assume "f \<in> borel_measurable M"
   then show "(\<lambda>x. f x $$ i) \<in> borel_measurable M"
-    using measurable_comp[of f _ _ "\<lambda>x. x $$ i", unfolded comp_def]
     by (auto intro: borel_measurable_euclidean_component)
 next
   assume f: "\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M"
@@ -657,6 +662,144 @@
 
 subsection "Borel measurable operators"
 
+lemma borel_measurable_continuous_on1:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes "continuous_on UNIV f"
+  shows "f \<in> borel_measurable borel"
+  apply(rule borel_measurableI)
+  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
+
+lemma borel_measurable_continuous_on:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. f (g x)) \<in> borel_measurable M"
+  using measurable_comp[OF g borel_measurable_continuous_on1[OF f]] by (simp add: comp_def)
+
+lemma borel_measurable_continuous_on_open':
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
+  assumes cont: "continuous_on A f" "open A"
+  shows "(\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel" (is "?f \<in> _")
+proof (rule borel_measurableI)
+  fix S :: "'b set" assume "open S"
+  then have "open {x\<in>A. f x \<in> S}"
+    by (intro continuous_open_preimage[OF cont]) auto
+  then have *: "{x\<in>A. f x \<in> S} \<in> sets borel" by auto
+  have "?f -` S \<inter> space borel = 
+    {x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel - A else {})"
+    by (auto split: split_if_asm)
+  also have "\<dots> \<in> sets borel"
+    using * `open A` by (auto simp del: space_borel intro!: Un)
+  finally show "?f -` S \<inter> space borel \<in> sets borel" .
+qed
+
+lemma borel_measurable_continuous_on_open:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
+  assumes cont: "continuous_on A f" "open A"
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. if g x \<in> A then f (g x) else c) \<in> borel_measurable M"
+  using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
+  by (simp add: comp_def)
+
+lemma borel_measurable_uminus[simp, intro]:
+  fixes g :: "'a \<Rightarrow> real"
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. - g x) \<in> borel_measurable M"
+  by (rule borel_measurable_continuous_on[OF _ g]) (auto intro: continuous_on_minus continuous_on_id)
+
+lemma euclidean_component_prod:
+  fixes x :: "'a :: euclidean_space \<times> 'b :: euclidean_space"
+  shows "x $$ i = (if i < DIM('a) then fst x $$ i else snd x $$ (i - DIM('a)))"
+  unfolding euclidean_component_def basis_prod_def inner_prod_def by auto
+
+lemma borel_measurable_Pair[simp, intro]:
+  fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. (f x, g x)) \<in> borel_measurable M"
+proof (intro borel_measurable_iff_halfspace_le[THEN iffD2] allI impI)
+  fix i and a :: real assume i: "i < DIM('b \<times> 'c)"
+  have [simp]: "\<And>P A B C. {w. (P \<longrightarrow> A w \<and> B w) \<and> (\<not> P \<longrightarrow> A w \<and> C w)} = 
+    {w. A w \<and> (P \<longrightarrow> B w) \<and> (\<not> P \<longrightarrow> C w)}" by auto
+  from i f g show "{w \<in> space M. (f w, g w) $$ i \<le> a} \<in> sets M"
+    by (auto simp: euclidean_component_prod intro!: sets_Collect borel_measurable_euclidean_component)
+qed
+
+lemma continuous_on_fst: "continuous_on UNIV fst"
+proof -
+  have [simp]: "range fst = UNIV" by (auto simp: image_iff)
+  show ?thesis
+    using closed_vimage_fst
+    by (auto simp: continuous_on_closed closed_closedin vimage_def)
+qed
+
+lemma continuous_on_snd: "continuous_on UNIV snd"
+proof -
+  have [simp]: "range snd = UNIV" by (auto simp: image_iff)
+  show ?thesis
+    using closed_vimage_snd
+    by (auto simp: continuous_on_closed closed_closedin vimage_def)
+qed
+
+lemma borel_measurable_continuous_Pair:
+  fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
+  assumes [simp]: "f \<in> borel_measurable M"
+  assumes [simp]: "g \<in> borel_measurable M"
+  assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
+  shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
+proof -
+  have eq: "(\<lambda>x. H (f x) (g x)) = (\<lambda>x. (\<lambda>x. H (fst x) (snd x)) (f x, g x))" by auto
+  show ?thesis
+    unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
+qed
+
+lemma borel_measurable_add[simp, intro]:
+  fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
+  using f g
+  by (rule borel_measurable_continuous_Pair)
+     (auto intro: continuous_on_fst continuous_on_snd continuous_on_add)
+
+lemma borel_measurable_setsum[simp, intro]:
+  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
+  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
+  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
+proof cases
+  assume "finite S"
+  thus ?thesis using assms by induct auto
+qed simp
+
+lemma borel_measurable_diff[simp, intro]:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
+  unfolding diff_minus using assms by fast
+
+lemma borel_measurable_times[simp, intro]:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
+  using f g
+  by (rule borel_measurable_continuous_Pair)
+     (auto intro: continuous_on_fst continuous_on_snd continuous_on_mult)
+
+lemma continuous_on_dist:
+  fixes f :: "'a :: t2_space \<Rightarrow> 'b :: metric_space"
+  shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. dist (f x) (g x))"
+  unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist)
+
+lemma borel_measurable_dist[simp, intro]:
+  fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. dist (f x) (g x)) \<in> borel_measurable M"
+  using f g
+  by (rule borel_measurable_continuous_Pair)
+     (intro continuous_on_dist continuous_on_fst continuous_on_snd)
+  
 lemma affine_borel_measurable_vector:
   fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
   assumes "f \<in> borel_measurable M"
@@ -683,116 +826,6 @@
   shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
   using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute)
 
-lemma borel_measurable_add[simp, intro]:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes f: "f \<in> borel_measurable M"
-  assumes g: "g \<in> borel_measurable M"
-  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
-proof -
-  have 1: "\<And>a. {w\<in>space M. a \<le> f w + g w} = {w \<in> space M. a + g w * -1 \<le> f w}"
-    by auto
-  have "\<And>a. (\<lambda>w. a + (g w) * -1) \<in> borel_measurable M"
-    by (rule affine_borel_measurable [OF g])
-  then have "\<And>a. {w \<in> space M. (\<lambda>w. a + (g w) * -1)(w) \<le> f w} \<in> sets M" using f
-    by auto
-  then have "\<And>a. {w \<in> space M. a \<le> f w + g w} \<in> sets M"
-    by (simp add: 1)
-  then show ?thesis
-    by (simp add: borel_measurable_iff_ge)
-qed
-
-lemma borel_measurable_setsum[simp, intro]:
-  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
-  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
-  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
-proof cases
-  assume "finite S"
-  thus ?thesis using assms by induct auto
-qed simp
-
-lemma borel_measurable_square:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes f: "f \<in> borel_measurable M"
-  shows "(\<lambda>x. (f x)^2) \<in> borel_measurable M"
-proof -
-  {
-    fix a
-    have "{w \<in> space M. (f w)\<twosuperior> \<le> a} \<in> sets M"
-    proof (cases rule: linorder_cases [of a 0])
-      case less
-      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = {}"
-        by auto (metis less order_le_less_trans power2_less_0)
-      also have "... \<in> sets M"
-        by (rule empty_sets)
-      finally show ?thesis .
-    next
-      case equal
-      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
-             {w \<in> space M. f w \<le> 0} \<inter> {w \<in> space M. 0 \<le> f w}"
-        by auto
-      also have "... \<in> sets M"
-        apply (insert f)
-        apply (rule Int)
-        apply (simp add: borel_measurable_iff_le)
-        apply (simp add: borel_measurable_iff_ge)
-        done
-      finally show ?thesis .
-    next
-      case greater
-      have "\<forall>x. (f x ^ 2 \<le> sqrt a ^ 2) = (- sqrt a  \<le> f x & f x \<le> sqrt a)"
-        by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs
-                  real_sqrt_le_iff real_sqrt_power)
-      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
-             {w \<in> space M. -(sqrt a) \<le> f w} \<inter> {w \<in> space M. f w \<le> sqrt a}"
-        using greater by auto
-      also have "... \<in> sets M"
-        apply (insert f)
-        apply (rule Int)
-        apply (simp add: borel_measurable_iff_ge)
-        apply (simp add: borel_measurable_iff_le)
-        done
-      finally show ?thesis .
-    qed
-  }
-  thus ?thesis by (auto simp add: borel_measurable_iff_le)
-qed
-
-lemma times_eq_sum_squares:
-   fixes x::real
-   shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4"
-by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric])
-
-lemma borel_measurable_uminus[simp, intro]:
-  fixes g :: "'a \<Rightarrow> real"
-  assumes g: "g \<in> borel_measurable M"
-  shows "(\<lambda>x. - g x) \<in> borel_measurable M"
-proof -
-  have "(\<lambda>x. - g x) = (\<lambda>x. 0 + (g x) * -1)"
-    by simp
-  also have "... \<in> borel_measurable M"
-    by (fast intro: affine_borel_measurable g)
-  finally show ?thesis .
-qed
-
-lemma borel_measurable_times[simp, intro]:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes f: "f \<in> borel_measurable M"
-  assumes g: "g \<in> borel_measurable M"
-  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
-proof -
-  have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M"
-    using assms by (fast intro: affine_borel_measurable borel_measurable_square)
-  have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) =
-        (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
-    by (simp add: minus_divide_right)
-  also have "... \<in> borel_measurable M"
-    using f g by (fast intro: affine_borel_measurable borel_measurable_square f g)
-  finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
-  show ?thesis
-    apply (simp add: times_eq_sum_squares diff_minus)
-    using 1 2 by simp
-qed
-
 lemma borel_measurable_setprod[simp, intro]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
@@ -802,26 +835,17 @@
   thus ?thesis using assms by induct auto
 qed simp
 
-lemma borel_measurable_diff[simp, intro]:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes f: "f \<in> borel_measurable M"
-  assumes g: "g \<in> borel_measurable M"
-  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
-  unfolding diff_minus using assms by fast
-
 lemma borel_measurable_inverse[simp, intro]:
   fixes f :: "'a \<Rightarrow> real"
-  assumes "f \<in> borel_measurable M"
+  assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
-  unfolding borel_measurable_iff_ge unfolding inverse_eq_divide
-proof safe
-  fix a :: real
-  have *: "{w \<in> space M. a \<le> 1 / f w} =
-      ({w \<in> space M. 0 < f w} \<inter> {w \<in> space M. a * f w \<le> 1}) \<union>
-      ({w \<in> space M. f w < 0} \<inter> {w \<in> space M. 1 \<le> a * f w}) \<union>
-      ({w \<in> space M. f w = 0} \<inter> {w \<in> space M. a \<le> 0})" by (auto simp: le_divide_eq)
-  show "{w \<in> space M. a \<le> 1 / f w} \<in> sets M" using assms unfolding *
-    by (auto intro!: Int Un)
+proof -
+  have *: "\<And>x::real. inverse x = (if x \<in> UNIV - {0} then inverse x else 0)" by auto
+  show ?thesis
+    apply (subst *)
+    apply (rule borel_measurable_continuous_on_open)
+    apply (auto intro!: f continuous_on_inverse continuous_on_id)
+    done
 qed
 
 lemma borel_measurable_divide[simp, intro]:
@@ -837,30 +861,14 @@
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
   shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
-  unfolding borel_measurable_iff_le
-proof safe
-  fix a
-  have "{x \<in> space M. max (g x) (f x) \<le> a} =
-    {x \<in> space M. g x \<le> a} \<inter> {x \<in> space M. f x \<le> a}" by auto
-  thus "{x \<in> space M. max (g x) (f x) \<le> a} \<in> sets M"
-    using assms unfolding borel_measurable_iff_le
-    by (auto intro!: Int)
-qed
+  unfolding max_def by (auto intro!: assms measurable_If)
 
 lemma borel_measurable_min[intro, simp]:
   fixes f g :: "'a \<Rightarrow> real"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
   shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
-  unfolding borel_measurable_iff_ge
-proof safe
-  fix a
-  have "{x \<in> space M. a \<le> min (g x) (f x)} =
-    {x \<in> space M. a \<le> g x} \<inter> {x \<in> space M. a \<le> f x}" by auto
-  thus "{x \<in> space M. a \<le> min (g x) (f x)} \<in> sets M"
-    using assms unfolding borel_measurable_iff_ge
-    by (auto intro!: Int)
-qed
+  unfolding min_def by (auto intro!: assms measurable_If)
 
 lemma borel_measurable_abs[simp, intro]:
   assumes "f \<in> borel_measurable M"
@@ -872,76 +880,50 @@
 
 lemma borel_measurable_nth[simp, intro]:
   "(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel"
-  using borel_measurable_euclidean_component
+  using borel_measurable_euclidean_component'
   unfolding nth_conv_component by auto
 
-lemma borel_measurable_continuous_on1:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
-  assumes "continuous_on UNIV f"
-  shows "f \<in> borel_measurable borel"
-  apply(rule borel_measurableI)
-  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
-
-lemma borel_measurable_continuous_on:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
-  assumes cont: "continuous_on A f" "open A"
-  shows "(\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel" (is "?f \<in> _")
-proof (rule borel_measurableI)
-  fix S :: "'b set" assume "open S"
-  then have "open {x\<in>A. f x \<in> S}"
-    by (intro continuous_open_preimage[OF cont]) auto
-  then have *: "{x\<in>A. f x \<in> S} \<in> sets borel" by auto
-  have "?f -` S \<inter> space borel = 
-    {x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel - A else {})"
-    by (auto split: split_if_asm)
-  also have "\<dots> \<in> sets borel"
-    using * `open A` by (auto simp del: space_borel intro!: Un)
-  finally show "?f -` S \<inter> space borel \<in> sets borel" .
-qed
-
 lemma convex_measurable:
   fixes a b :: real
   assumes X: "X \<in> borel_measurable M" "X ` space M \<subseteq> { a <..< b}"
   assumes q: "convex_on { a <..< b} q"
-  shows "q \<circ> X \<in> borel_measurable M"
+  shows "(\<lambda>x. q (X x)) \<in> borel_measurable M"
 proof -
-  have "(\<lambda>x. if x \<in> {a <..< b} then q x else 0) \<in> borel_measurable borel"
-  proof (rule borel_measurable_continuous_on)
+  have "(\<lambda>x. if X x \<in> {a <..< b} then q (X x) else 0) \<in> borel_measurable M" (is "?qX")
+  proof (rule borel_measurable_continuous_on_open[OF _ _ X(1)])
     show "open {a<..<b}" by auto
     from this q show "continuous_on {a<..<b} q"
       by (rule convex_on_continuous)
   qed
-  then have "(\<lambda>x. if x \<in> {a <..< b} then q x else 0) \<circ> X \<in> borel_measurable M" (is ?qX)
-    using X by (intro measurable_comp) auto
-  moreover have "?qX \<longleftrightarrow> q \<circ> X \<in> borel_measurable M"
+  moreover have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M"
     using X by (intro measurable_cong) auto
   ultimately show ?thesis by simp
 qed
 
-lemma borel_measurable_borel_log: assumes "1 < b" shows "log b \<in> borel_measurable borel"
+lemma borel_measurable_ln[simp,intro]:
+  assumes f: "f \<in> borel_measurable M"
+  shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
 proof -
   { fix x :: real assume x: "x \<le> 0"
     { fix x::real assume "x \<le> 0" then have "\<And>u. exp u = x \<longleftrightarrow> False" by auto }
-    from this[of x] x this[of 0] have "log b 0 = log b x"
-      by (auto simp: ln_def log_def) }
-  note log_imp = this
-  have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) \<in> borel_measurable borel"
-  proof (rule borel_measurable_continuous_on)
-    show "continuous_on {0<..} (log b)"
-      by (auto intro!: continuous_at_imp_continuous_on DERIV_log DERIV_isCont
+    from this[of x] x this[of 0] have "ln 0 = ln x"
+      by (auto simp: ln_def) }
+  note ln_imp = this
+  have "(\<lambda>x. if f x \<in> {0<..} then ln (f x) else ln 0) \<in> borel_measurable M"
+  proof (rule borel_measurable_continuous_on_open[OF _ _ f])
+    show "continuous_on {0<..} ln"
+      by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont
                simp: continuous_isCont[symmetric])
     show "open ({0<..}::real set)" by auto
   qed
-  also have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) = log b"
-    by (simp add: fun_eq_iff not_less log_imp)
+  also have "(\<lambda>x. if x \<in> {0<..} then ln x else ln 0) = ln"
+    by (simp add: fun_eq_iff not_less ln_imp)
   finally show ?thesis .
 qed
 
 lemma borel_measurable_log[simp,intro]:
-  assumes f: "f \<in> borel_measurable M" and "1 < b"
-  shows "(\<lambda>x. log b (f x)) \<in> borel_measurable M"
-  using measurable_comp[OF f borel_measurable_borel_log[OF `1 < b`]]
-  by (simp add: comp_def)
+  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log b (f x)) \<in> borel_measurable M"
+  unfolding log_def by auto
 
 lemma borel_measurable_real_floor:
   "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
@@ -967,45 +949,91 @@
 
 subsection "Borel space on the extended reals"
 
-lemma borel_measurable_ereal_borel:
-  "ereal \<in> borel_measurable borel"
-proof (rule borel_measurableI)
-  fix X :: "ereal set" assume "open X"
-  then have "open (ereal -` X \<inter> space borel)"
-    by (simp add: open_ereal_vimage)
-  then show "ereal -` X \<inter> space borel \<in> sets borel" by auto
-qed
-
 lemma borel_measurable_ereal[simp, intro]:
   assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
-  using measurable_comp[OF f borel_measurable_ereal_borel] unfolding comp_def .
+  using continuous_on_ereal f by (rule borel_measurable_continuous_on)
 
-lemma borel_measurable_real_of_ereal_borel:
-  "(real :: ereal \<Rightarrow> real) \<in> borel_measurable borel"
-proof (rule borel_measurableI)
-  fix B :: "real set" assume "open B"
-  have *: "ereal -` real -` (B - {0}) = B - {0}" by auto
-  have open_real: "open (real -` (B - {0}) :: ereal set)"
-    unfolding open_ereal_def * using `open B` by auto
-  show "(real -` B \<inter> space borel :: ereal set) \<in> sets borel"
-  proof cases
-    assume "0 \<in> B"
-    then have *: "real -` B = real -` (B - {0}) \<union> {-\<infinity>, \<infinity>, 0::ereal}"
-      by (auto simp add: real_of_ereal_eq_0)
-    then show "(real -` B :: ereal set) \<inter> space borel \<in> sets borel"
-      using open_real by auto
-  next
-    assume "0 \<notin> B"
-    then have *: "(real -` B :: ereal set) = real -` (B - {0})"
-      by (auto simp add: real_of_ereal_eq_0)
-    then show "(real -` B :: ereal set) \<inter> space borel \<in> sets borel"
-      using open_real by auto
-  qed
+lemma borel_measurable_real_of_ereal[simp, intro]:
+  fixes f :: "'a \<Rightarrow> ereal" 
+  assumes f: "f \<in> borel_measurable M"
+  shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
+proof -
+  have "(\<lambda>x. if f x \<in> UNIV - { \<infinity>, - \<infinity> } then real (f x) else 0) \<in> borel_measurable M"
+    using continuous_on_real
+    by (rule borel_measurable_continuous_on_open[OF _ _ f]) auto
+  also have "(\<lambda>x. if f x \<in> UNIV - { \<infinity>, - \<infinity> } then real (f x) else 0) = (\<lambda>x. real (f x))"
+    by auto
+  finally show ?thesis .
+qed
+
+lemma borel_measurable_ereal_cases:
+  fixes f :: "'a \<Rightarrow> ereal" 
+  assumes f: "f \<in> borel_measurable M"
+  assumes H: "(\<lambda>x. H (ereal (real (f x)))) \<in> borel_measurable M"
+  shows "(\<lambda>x. H (f x)) \<in> borel_measurable M"
+proof -
+  let ?F = "\<lambda>x. if x \<in> f -` {\<infinity>} then H \<infinity> else if x \<in> f -` {-\<infinity>} then H (-\<infinity>) else H (ereal (real (f x)))"
+  { fix x have "H (f x) = ?F x" by (cases "f x") auto }
+  moreover 
+  have "?F \<in> borel_measurable M"
+    by (intro measurable_If_set f measurable_sets[OF f] H) auto
+  ultimately
+  show ?thesis by simp
 qed
 
-lemma borel_measurable_real_of_ereal[simp, intro]:
-  assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. real (f x :: ereal)) \<in> borel_measurable M"
-  using measurable_comp[OF f borel_measurable_real_of_ereal_borel] unfolding comp_def .
+lemma
+  fixes f :: "'a \<Rightarrow> ereal" assumes f[simp]: "f \<in> borel_measurable M"
+  shows borel_measurable_ereal_abs[intro, simp]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
+    and borel_measurable_ereal_inverse[simp, intro]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
+    and borel_measurable_uminus_ereal[intro]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
+  by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
+
+lemma borel_measurable_uminus_eq_ereal[simp]:
+  "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r")
+proof
+  assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
+qed auto
+
+lemma sets_Collect_If_set:
+  assumes "A \<inter> space M \<in> sets M" "{x \<in> space M. P x} \<in> sets M" "{x \<in> space M. Q x} \<in> sets M"
+  shows "{x \<in> space M. if x \<in> A then P x else Q x} \<in> sets M"
+proof -
+  have *: "{x \<in> space M. if x \<in> A then P x else Q x} = 
+    {x \<in> space M. if x \<in> A \<inter> space M then P x else Q x}" by auto
+  show ?thesis unfolding * unfolding if_bool_eq_conj using assms
+    by (auto intro!: sets_Collect simp: Int_def conj_commute)
+qed
+
+lemma set_Collect_ereal2:
+  fixes f g :: "'a \<Rightarrow> ereal" 
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  assumes H: "{x \<in> space M. H (ereal (real (f x))) (ereal (real (g x)))} \<in> sets M"
+    "{x \<in> space M. H (-\<infinity>) (ereal (real (g x)))} \<in> sets M"
+    "{x \<in> space M. H (\<infinity>) (ereal (real (g x)))} \<in> sets M"
+    "{x \<in> space M. H (ereal (real (f x))) (-\<infinity>)} \<in> sets M"
+    "{x \<in> space M. H (ereal (real (f x))) (\<infinity>)} \<in> sets M"
+  shows "{x \<in> space M. H (f x) (g x)} \<in> sets M"
+proof -
+  let ?G = "\<lambda>y x. if x \<in> g -` {\<infinity>} then H y \<infinity> else if x \<in> g -` {-\<infinity>} then H y (-\<infinity>) else H y (ereal (real (g x)))"
+  let ?F = "\<lambda>x. if x \<in> f -` {\<infinity>} then ?G \<infinity> x else if x \<in> f -` {-\<infinity>} then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
+  { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
+  moreover 
+  have "{x \<in> space M. ?F x} \<in> sets M"
+    by (intro sets_Collect H measurable_sets[OF f] measurable_sets[OF g] sets_Collect_If_set) auto
+  ultimately
+  show ?thesis by simp
+qed
+
+lemma
+  fixes f g :: "'a \<Rightarrow> ereal"
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows borel_measurable_ereal_le[intro,simp]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
+    and borel_measurable_ereal_less[intro,simp]: "{x \<in> space M. f x < g x} \<in> sets M"
+    and borel_measurable_ereal_eq[intro,simp]: "{w \<in> space M. f w = g w} \<in> sets M"
+    and borel_measurable_ereal_neq[intro,simp]: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
+  using f g by (auto simp: f g set_Collect_ereal2[OF f g] intro!: sets_Collect_neg)
 
 lemma borel_measurable_ereal_iff:
   shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
@@ -1029,52 +1057,6 @@
   finally show "f \<in> borel_measurable M" .
 qed (auto intro: measurable_sets borel_measurable_real_of_ereal)
 
-lemma less_eq_ge_measurable:
-  fixes f :: "'a \<Rightarrow> 'c::linorder"
-  shows "f -` {a <..} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {..a} \<inter> space M \<in> sets M"
-proof
-  assume "f -` {a <..} \<inter> space M \<in> sets M"
-  moreover have "f -` {..a} \<inter> space M = space M - f -` {a <..} \<inter> space M" by auto
-  ultimately show "f -` {..a} \<inter> space M \<in> sets M" by auto
-next
-  assume "f -` {..a} \<inter> space M \<in> sets M"
-  moreover have "f -` {a <..} \<inter> space M = space M - f -` {..a} \<inter> space M" by auto
-  ultimately show "f -` {a <..} \<inter> space M \<in> sets M" by auto
-qed
-
-lemma greater_eq_le_measurable:
-  fixes f :: "'a \<Rightarrow> 'c::linorder"
-  shows "f -` {..< a} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {a ..} \<inter> space M \<in> sets M"
-proof
-  assume "f -` {a ..} \<inter> space M \<in> sets M"
-  moreover have "f -` {..< a} \<inter> space M = space M - f -` {a ..} \<inter> space M" by auto
-  ultimately show "f -` {..< a} \<inter> space M \<in> sets M" by auto
-next
-  assume "f -` {..< a} \<inter> space M \<in> sets M"
-  moreover have "f -` {a ..} \<inter> space M = space M - f -` {..< a} \<inter> space M" by auto
-  ultimately show "f -` {a ..} \<inter> space M \<in> sets M" by auto
-qed
-
-lemma borel_measurable_uminus_borel_ereal:
-  "(uminus :: ereal \<Rightarrow> ereal) \<in> borel_measurable borel"
-proof (rule borel_measurableI)
-  fix X :: "ereal set" assume "open X"
-  have "uminus -` X = uminus ` X" by (force simp: image_iff)
-  then have "open (uminus -` X)" using `open X` ereal_open_uminus by auto
-  then show "uminus -` X \<inter> space borel \<in> sets borel" by auto
-qed
-
-lemma borel_measurable_uminus_ereal[intro]:
-  assumes "f \<in> borel_measurable M"
-  shows "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
-  using measurable_comp[OF assms borel_measurable_uminus_borel_ereal] by (simp add: comp_def)
-
-lemma borel_measurable_uminus_eq_ereal[simp]:
-  "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r")
-proof
-  assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
-qed auto
-
 lemma borel_measurable_eq_atMost_ereal:
   fixes f :: "'a \<Rightarrow> ereal"
   shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
@@ -1118,94 +1100,88 @@
   then show "f \<in> borel_measurable M" by simp
 qed (simp add: measurable_sets)
 
+lemma greater_eq_le_measurable:
+  fixes f :: "'a \<Rightarrow> 'c::linorder"
+  shows "f -` {..< a} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {a ..} \<inter> space M \<in> sets M"
+proof
+  assume "f -` {a ..} \<inter> space M \<in> sets M"
+  moreover have "f -` {..< a} \<inter> space M = space M - f -` {a ..} \<inter> space M" by auto
+  ultimately show "f -` {..< a} \<inter> space M \<in> sets M" by auto
+next
+  assume "f -` {..< a} \<inter> space M \<in> sets M"
+  moreover have "f -` {a ..} \<inter> space M = space M - f -` {..< a} \<inter> space M" by auto
+  ultimately show "f -` {a ..} \<inter> space M \<in> sets M" by auto
+qed
+
 lemma borel_measurable_ereal_iff_less:
   "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..< a} \<inter> space M \<in> sets M)"
   unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable ..
 
+lemma less_eq_ge_measurable:
+  fixes f :: "'a \<Rightarrow> 'c::linorder"
+  shows "f -` {a <..} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {..a} \<inter> space M \<in> sets M"
+proof
+  assume "f -` {a <..} \<inter> space M \<in> sets M"
+  moreover have "f -` {..a} \<inter> space M = space M - f -` {a <..} \<inter> space M" by auto
+  ultimately show "f -` {..a} \<inter> space M \<in> sets M" by auto
+next
+  assume "f -` {..a} \<inter> space M \<in> sets M"
+  moreover have "f -` {a <..} \<inter> space M = space M - f -` {..a} \<inter> space M" by auto
+  ultimately show "f -` {a <..} \<inter> space M \<in> sets M" by auto
+qed
+
 lemma borel_measurable_ereal_iff_ge:
   "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a <..} \<inter> space M \<in> sets M)"
   unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable ..
 
-lemma borel_measurable_ereal_eq_const:
-  fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M"
-  shows "{x\<in>space M. f x = c} \<in> sets M"
-proof -
-  have "{x\<in>space M. f x = c} = (f -` {c} \<inter> space M)" by auto
-  then show ?thesis using assms by (auto intro!: measurable_sets)
-qed
-
-lemma borel_measurable_ereal_neq_const:
-  fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M"
-  shows "{x\<in>space M. f x \<noteq> c} \<in> sets M"
-proof -
-  have "{x\<in>space M. f x \<noteq> c} = space M - (f -` {c} \<inter> space M)" by auto
-  then show ?thesis using assms by (auto intro!: measurable_sets)
-qed
-
-lemma borel_measurable_ereal_le[intro,simp]:
-  fixes f g :: "'a \<Rightarrow> ereal"
+lemma borel_measurable_ereal2:
+  fixes f g :: "'a \<Rightarrow> ereal" 
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
-  shows "{x \<in> space M. f x \<le> g x} \<in> sets M"
+  assumes H: "(\<lambda>x. H (ereal (real (f x))) (ereal (real (g x)))) \<in> borel_measurable M"
+    "(\<lambda>x. H (-\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M"
+    "(\<lambda>x. H (\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M"
+    "(\<lambda>x. H (ereal (real (f x))) (-\<infinity>)) \<in> borel_measurable M"
+    "(\<lambda>x. H (ereal (real (f x))) (\<infinity>)) \<in> borel_measurable M"
+  shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
 proof -
-  have "{x \<in> space M. f x \<le> g x} =
-    {x \<in> space M. real (f x) \<le> real (g x)} - (f -` {\<infinity>, -\<infinity>} \<inter> space M \<union> g -` {\<infinity>, -\<infinity>} \<inter> space M) \<union>
-    f -` {-\<infinity>} \<inter> space M \<union> g -` {\<infinity>} \<inter> space M" (is "?l = ?r")
-  proof (intro set_eqI)
-    fix x show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" by (cases rule: ereal2_cases[of "f x" "g x"]) auto
-  qed
-  with f g show ?thesis by (auto intro!: Un simp: measurable_sets)
+  let ?G = "\<lambda>y x. if x \<in> g -` {\<infinity>} then H y \<infinity> else if x \<in> g -` {-\<infinity>} then H y (-\<infinity>) else H y (ereal (real (g x)))"
+  let ?F = "\<lambda>x. if x \<in> f -` {\<infinity>} then ?G \<infinity> x else if x \<in> f -` {-\<infinity>} then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
+  { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
+  moreover 
+  have "?F \<in> borel_measurable M"
+    by (intro measurable_If_set measurable_sets[OF f] measurable_sets[OF g] H) auto
+  ultimately
+  show ?thesis by simp
 qed
 
-lemma borel_measurable_ereal_less[intro,simp]:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes f: "f \<in> borel_measurable M"
-  assumes g: "g \<in> borel_measurable M"
-  shows "{x \<in> space M. f x < g x} \<in> sets M"
-proof -
-  have "{x \<in> space M. f x < g x} = space M - {x \<in> space M. g x \<le> f x}" by auto
-  then show ?thesis using g f by auto
-qed
-
-lemma borel_measurable_ereal_eq[intro,simp]:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes f: "f \<in> borel_measurable M"
-  assumes g: "g \<in> borel_measurable M"
-  shows "{w \<in> space M. f w = g w} \<in> sets M"
-proof -
-  have "{x \<in> space M. f x = g x} = {x \<in> space M. g x \<le> f x} \<inter> {x \<in> space M. f x \<le> g x}" by auto
-  then show ?thesis using g f by auto
-qed
-
-lemma borel_measurable_ereal_neq[intro,simp]:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes f: "f \<in> borel_measurable M"
-  assumes g: "g \<in> borel_measurable M"
-  shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
-proof -
-  have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}" by auto
-  thus ?thesis using f g by auto
-qed
+lemma
+  fixes f :: "'a \<Rightarrow> ereal" assumes f: "f \<in> borel_measurable M"
+  shows borel_measurable_ereal_eq_const: "{x\<in>space M. f x = c} \<in> sets M"
+    and borel_measurable_ereal_neq_const: "{x\<in>space M. f x \<noteq> c} \<in> sets M"
+  using f by auto
 
 lemma split_sets:
   "{x\<in>space M. P x \<or> Q x} = {x\<in>space M. P x} \<union> {x\<in>space M. Q x}"
   "{x\<in>space M. P x \<and> Q x} = {x\<in>space M. P x} \<inter> {x\<in>space M. Q x}"
   by auto
 
-lemma borel_measurable_ereal_add[intro, simp]:
+lemma
   fixes f :: "'a \<Rightarrow> ereal"
-  assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
-  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
-proof -
-  { fix x assume "x \<in> space M" then have "f x + g x =
-      (if f x = \<infinity> \<or> g x = \<infinity> then \<infinity>
-        else if f x = -\<infinity> \<or> g x = -\<infinity> then -\<infinity>
-        else ereal (real (f x) + real (g x)))"
-      by (cases rule: ereal2_cases[of "f x" "g x"]) auto }
-  with assms show ?thesis
-    by (auto cong: measurable_cong simp: split_sets
-             intro!: Un measurable_If measurable_sets)
-qed
+  assumes [simp]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+  shows borel_measurable_ereal_add[intro, simp]: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
+    and borel_measurable_ereal_times[intro, simp]: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
+    and borel_measurable_ereal_min[simp, intro]: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
+    and borel_measurable_ereal_max[simp, intro]: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
+  by (auto simp add: borel_measurable_ereal2 measurable_If min_def max_def)
+
+lemma
+  fixes f g :: "'a \<Rightarrow> ereal"
+  assumes "f \<in> borel_measurable M"
+  assumes "g \<in> borel_measurable M"
+  shows borel_measurable_ereal_diff[simp, intro]: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
+    and borel_measurable_ereal_divide[simp, intro]: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
+  unfolding minus_ereal_def divide_ereal_def using assms by auto
 
 lemma borel_measurable_ereal_setsum[simp, intro]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
@@ -1215,39 +1191,7 @@
   assume "finite S"
   thus ?thesis using assms
     by induct auto
-qed (simp add: borel_measurable_const)
-
-lemma borel_measurable_ereal_abs[intro, simp]:
-  fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M"
-  shows "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
-proof -
-  { fix x have "\<bar>f x\<bar> = (if 0 \<le> f x then f x else - f x)" by auto }
-  then show ?thesis using assms by (auto intro!: measurable_If)
-qed
-
-lemma borel_measurable_ereal_times[intro, simp]:
-  fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
-  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
-proof -
-  { fix f g :: "'a \<Rightarrow> ereal"
-    assume b: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
-      and pos: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x"
-    { fix x have *: "f x * g x = (if f x = 0 \<or> g x = 0 then 0
-        else if f x = \<infinity> \<or> g x = \<infinity> then \<infinity>
-        else ereal (real (f x) * real (g x)))"
-      apply (cases rule: ereal2_cases[of "f x" "g x"])
-      using pos[of x] by auto }
-    with b have "(\<lambda>x. f x * g x) \<in> borel_measurable M"
-      by (auto cong: measurable_cong simp: split_sets
-               intro!: Un measurable_If measurable_sets) }
-  note pos_times = this
-  have *: "(\<lambda>x. f x * g x) =
-    (\<lambda>x. if 0 \<le> f x \<and> 0 \<le> g x \<or> f x < 0 \<and> g x < 0 then \<bar>f x\<bar> * \<bar>g x\<bar> else - (\<bar>f x\<bar> * \<bar>g x\<bar>))"
-    by (auto simp: fun_eq_iff)
-  show ?thesis using assms unfolding *
-    by (intro measurable_If pos_times borel_measurable_uminus_ereal)
-       (auto simp: split_sets intro!: Int)
-qed
+qed simp
 
 lemma borel_measurable_ereal_setprod[simp, intro]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
@@ -1258,20 +1202,6 @@
   thus ?thesis using assms by induct auto
 qed simp
 
-lemma borel_measurable_ereal_min[simp, intro]:
-  fixes f g :: "'a \<Rightarrow> ereal"
-  assumes "f \<in> borel_measurable M"
-  assumes "g \<in> borel_measurable M"
-  shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
-  using assms unfolding min_def by (auto intro!: measurable_If)
-
-lemma borel_measurable_ereal_max[simp, intro]:
-  fixes f g :: "'a \<Rightarrow> ereal"
-  assumes "f \<in> borel_measurable M"
-  and "g \<in> borel_measurable M"
-  shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
-  using assms unfolding max_def by (auto intro!: measurable_If)
-
 lemma borel_measurable_SUP[simp, intro]:
   fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
@@ -1298,38 +1228,24 @@
     using assms by auto
 qed
 
-lemma borel_measurable_liminf[simp, intro]:
-  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
-  assumes "\<And>i. f i \<in> borel_measurable M"
-  shows "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
-  unfolding liminf_SUPR_INFI using assms by auto
-
-lemma borel_measurable_limsup[simp, intro]:
+lemma
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. f i \<in> borel_measurable M"
-  shows "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
-  unfolding limsup_INFI_SUPR using assms by auto
-
-lemma borel_measurable_ereal_diff[simp, intro]:
-  fixes f g :: "'a \<Rightarrow> ereal"
-  assumes "f \<in> borel_measurable M"
-  assumes "g \<in> borel_measurable M"
-  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
-  unfolding minus_ereal_def using assms by auto
+  shows borel_measurable_liminf[simp, intro]: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
+    and borel_measurable_limsup[simp, intro]: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
+  unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
 
-lemma borel_measurable_ereal_inverse[simp, intro]:
-  assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
+lemma borel_measurable_ereal_LIMSEQ:
+  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
+  assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
+  and u: "\<And>i. u i \<in> borel_measurable M"
+  shows "u' \<in> borel_measurable M"
 proof -
-  { fix x have "inverse (f x) = (if f x = 0 then \<infinity> else ereal (inverse (real (f x))))"
-      by (cases "f x") auto }
-  with f show ?thesis
-    by (auto intro!: measurable_If)
+  have "\<And>x. x \<in> space M \<Longrightarrow> u' x = liminf (\<lambda>n. u n x)"
+    using u' by (simp add: lim_imp_Liminf[symmetric])
+  then show ?thesis by (simp add: u cong: measurable_cong)
 qed
 
-lemma borel_measurable_ereal_divide[simp, intro]:
-  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. f x / g x :: ereal) \<in> borel_measurable M"
-  unfolding divide_ereal_def by auto
-
 lemma borel_measurable_psuminf[simp, intro]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. f i \<in> borel_measurable M" and pos: "\<And>i x. x \<in> space M \<Longrightarrow> 0 \<le> f i x"
@@ -1354,4 +1270,38 @@
   ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff)
 qed
 
-end
+lemma sets_Collect_Cauchy: 
+  fixes f :: "nat \<Rightarrow> 'a => real"
+  assumes f: "\<And>i. f i \<in> borel_measurable M"
+  shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
+  unfolding Cauchy_iff2 using f by (auto intro!: sets_Collect)
+
+lemma borel_measurable_lim:
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
+  assumes f: "\<And>i. f i \<in> borel_measurable M"
+  shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
+proof -
+  have *: "\<And>x. lim (\<lambda>i. f i x) =
+    (if Cauchy (\<lambda>i. f i x) then lim (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) else (THE x. False))"
+    by (auto simp: lim_def convergent_eq_cauchy[symmetric])
+  { fix x have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
+      by (cases "Cauchy (\<lambda>i. f i x)")
+         (auto simp add: convergent_eq_cauchy[symmetric] convergent_def) }
+  note convergent = this
+  show ?thesis
+    unfolding *
+    apply (intro measurable_If sets_Collect_Cauchy f borel_measurable_const)
+    apply (rule borel_measurable_LIMSEQ)
+    apply (rule convergent_LIMSEQ_iff[THEN iffD1, OF convergent])
+    apply (intro measurable_If sets_Collect_Cauchy f borel_measurable_const)
+    done
+qed
+
+lemma borel_measurable_suminf:
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
+  assumes f: "\<And>i. f i \<in> borel_measurable M"
+  shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
+  unfolding suminf_def sums_def[abs_def] lim_def[symmetric]
+  by (simp add: f borel_measurable_lim)
+
+end