# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1458137130 0
# Node ID 20288ba55e853a0e8c67554fdc5c6cc1be953ccb
# Parent  de25474ce728ef8e4824b87c9f6dbf39973725da# Parent  2d73385aa5f35b7a171756c38664a31517163678
Merge

diff -r de25474ce728 -r 20288ba55e85 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Wed Mar 16 13:57:06 2016 +0000
+++ b/src/HOL/Library/Liminf_Limsup.thy	Wed Mar 16 14:05:30 2016 +0000
@@ -3,18 +3,58 @@
     Author:     Manuel Eberl, TU München
 *)
 
-section \<open>Liminf and Limsup on complete lattices\<close>
+section \<open>Liminf and Limsup on conditionally complete lattices\<close>
 
 theory Liminf_Limsup
 imports Complex_Main
 begin
 
+lemma (in conditionally_complete_linorder) le_cSup_iff:
+  assumes "A \<noteq> {}" "bdd_above A"
+  shows "x \<le> Sup A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
+proof safe
+  fix y assume "x \<le> Sup A" "y < x"
+  then have "y < Sup A" by auto
+  then show "\<exists>a\<in>A. y < a"
+    unfolding less_cSup_iff[OF assms] .
+qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] cSup_upper assms)
+
+lemma (in conditionally_complete_linorder) le_cSUP_iff:
+  "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> SUPREMUM A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
+  using le_cSup_iff [of "f ` A"] by simp
+
+lemma le_cSup_iff_less:
+  fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
+  shows "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)"
+  by (simp add: le_cSUP_iff)
+     (blast intro: less_imp_le less_trans less_le_trans dest: dense)
+
 lemma le_Sup_iff_less:
   fixes x :: "'a :: {complete_linorder, dense_linorder}"
   shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
   unfolding le_SUP_iff
   by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
 
+lemma (in conditionally_complete_linorder) cInf_le_iff:
+  assumes "A \<noteq> {}" "bdd_below A"
+  shows "Inf A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
+proof safe
+  fix y assume "x \<ge> Inf A" "y > x"
+  then have "y > Inf A" by auto
+  then show "\<exists>a\<in>A. y > a"
+    unfolding cInf_less_iff[OF assms] .
+qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] cInf_lower assms)
+
+lemma (in conditionally_complete_linorder) cINF_le_iff:
+  "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
+  using cInf_le_iff [of "f ` A"] by simp
+
+lemma cInf_le_iff_less:
+  fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
+  shows "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
+  by (simp add: cINF_le_iff)
+     (blast intro: less_imp_le less_trans le_less_trans dest: dense)
+
 lemma Inf_le_iff_less:
   fixes x :: "'a :: {complete_linorder, dense_linorder}"
   shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
diff -r de25474ce728 -r 20288ba55e85 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Mar 16 13:57:06 2016 +0000
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Mar 16 14:05:30 2016 +0000
@@ -11,6 +11,30 @@
   "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
 begin
 
+lemma sets_Collect_eventually_sequentially[measurable]:
+  "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
+  unfolding eventually_sequentially by simp
+
+lemma open_Collect_less:
+  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
+  assumes "continuous_on UNIV f"
+  assumes "continuous_on UNIV g"
+  shows "open {x. f x < g x}"
+proof -
+  have "open (\<Union>y. {x \<in> UNIV. f x \<in> {..< y}} \<inter> {x \<in> UNIV. g x \<in> {y <..}})" (is "open ?X")
+    by (intro open_UN ballI open_Int continuous_open_preimage assms) auto
+  also have "?X = {x. f x < g x}"
+    by (auto intro: dense)
+  finally show ?thesis .
+qed
+
+lemma closed_Collect_le:
+  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
+  assumes f: "continuous_on UNIV f"
+  assumes g: "continuous_on UNIV g"
+  shows "closed {x. f x \<le> g x}"
+  using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed .
+
 lemma topological_basis_trivial: "topological_basis {A. open A}"
   by (auto simp: topological_basis_def)
 
@@ -428,6 +452,64 @@
 lemma borel_compact: "compact (A::'a::t2_space set) \<Longrightarrow> A \<in> sets borel"
   by (auto intro: borel_closed dest!: compact_imp_closed)
 
+lemma borel_sigma_sets_subset:
+  "A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel"
+  using sets.sigma_sets_subset[of A borel] by simp
+
+lemma borel_eq_sigmaI1:
+  fixes F :: "'i \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
+  assumes borel_eq: "borel = sigma UNIV X"
+  assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV (F ` A))"
+  assumes F: "\<And>i. i \<in> A \<Longrightarrow> F i \<in> sets borel"
+  shows "borel = sigma UNIV (F ` A)"
+  unfolding borel_def
+proof (intro sigma_eqI antisym)
+  have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel"
+    unfolding borel_def by simp
+  also have "\<dots> = sigma_sets UNIV X"
+    unfolding borel_eq by simp
+  also have "\<dots> \<subseteq> sigma_sets UNIV (F`A)"
+    using X by (intro sigma_algebra.sigma_sets_subset[OF sigma_algebra_sigma_sets]) auto
+  finally show "sigma_sets UNIV {S. open S} \<subseteq> sigma_sets UNIV (F`A)" .
+  show "sigma_sets UNIV (F`A) \<subseteq> sigma_sets UNIV {S. open S}"
+    unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto
+qed auto
+
+lemma borel_eq_sigmaI2:
+  fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set"
+    and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set"
+  assumes borel_eq: "borel = sigma UNIV ((\<lambda>(i, j). G i j)`B)"
+  assumes X: "\<And>i j. (i, j) \<in> B \<Longrightarrow> G i j \<in> sets (sigma UNIV ((\<lambda>(i, j). F i j) ` A))"
+  assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel"
+  shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)"
+  using assms
+  by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` B" and F="(\<lambda>(i, j). F i j)"]) auto
+
+lemma borel_eq_sigmaI3:
+  fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
+  assumes borel_eq: "borel = sigma UNIV X"
+  assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV ((\<lambda>(i, j). F i j) ` A))"
+  assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel"
+  shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)"
+  using assms by (intro borel_eq_sigmaI1[where X=X and F="(\<lambda>(i, j). F i j)"]) auto
+
+lemma borel_eq_sigmaI4:
+  fixes F :: "'i \<Rightarrow> 'a::topological_space set"
+    and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set"
+  assumes borel_eq: "borel = sigma UNIV ((\<lambda>(i, j). G i j)`A)"
+  assumes X: "\<And>i j. (i, j) \<in> A \<Longrightarrow> G i j \<in> sets (sigma UNIV (range F))"
+  assumes F: "\<And>i. F i \<in> sets borel"
+  shows "borel = sigma UNIV (range F)"
+  using assms by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` A" and F=F]) auto
+
+lemma borel_eq_sigmaI5:
+  fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and G :: "'l \<Rightarrow> 'a::topological_space set"
+  assumes borel_eq: "borel = sigma UNIV (range G)"
+  assumes X: "\<And>i. G i \<in> sets (sigma UNIV (range (\<lambda>(i, j). F i j)))"
+  assumes F: "\<And>i j. F i j \<in> sets borel"
+  shows "borel = sigma UNIV (range (\<lambda>(i, j). F i j))"
+  using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(\<lambda>(i, j). F i j)"]) auto
+
 lemma second_countable_borel_measurable:
   fixes X :: "'a::second_countable_topology set set"
   assumes eq: "open = generate_topology X"
@@ -472,6 +554,40 @@
   qed auto
 qed (auto simp: eq intro: generate_topology.Basis)
 
+lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
+  unfolding borel_def
+proof (intro sigma_eqI sigma_sets_eqI, safe)
+  fix x :: "'a set" assume "open x"
+  hence "x = UNIV - (UNIV - x)" by auto
+  also have "\<dots> \<in> sigma_sets UNIV (Collect closed)"
+    by (force intro: sigma_sets.Compl simp: \<open>open x\<close>)
+  finally show "x \<in> sigma_sets UNIV (Collect closed)" by simp
+next
+  fix x :: "'a set" assume "closed x"
+  hence "x = UNIV - (UNIV - x)" by auto
+  also have "\<dots> \<in> sigma_sets UNIV (Collect open)"
+    by (force intro: sigma_sets.Compl simp: \<open>closed x\<close>)
+  finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
+qed simp_all
+
+lemma borel_eq_countable_basis:
+  fixes B::"'a::topological_space set set"
+  assumes "countable B"
+  assumes "topological_basis B"
+  shows "borel = sigma UNIV B"
+  unfolding borel_def
+proof (intro sigma_eqI sigma_sets_eqI, safe)
+  interpret countable_basis using assms by unfold_locales
+  fix X::"'a set" assume "open X"
+  from open_countable_basisE[OF this] guess B' . note B' = this
+  then show "X \<in> sigma_sets UNIV B"
+    by (blast intro: sigma_sets_UNION \<open>countable B\<close> countable_subset)
+next
+  fix b assume "b \<in> B"
+  hence "open b" by (rule topological_basis_open[OF assms(2)])
+  thus "b \<in> sigma_sets UNIV (Collect open)" by auto
+qed simp_all
+
 lemma borel_measurable_continuous_on_restrict:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   assumes f: "continuous_on A f"
@@ -516,24 +632,6 @@
   by (subst borel_measurable_restrict_space_iff[symmetric])
      (auto intro: borel_measurable_continuous_on_restrict)
 
-lemma borel_eq_countable_basis:
-  fixes B::"'a::topological_space set set"
-  assumes "countable B"
-  assumes "topological_basis B"
-  shows "borel = sigma UNIV B"
-  unfolding borel_def
-proof (intro sigma_eqI sigma_sets_eqI, safe)
-  interpret countable_basis using assms by unfold_locales
-  fix X::"'a set" assume "open X"
-  from open_countable_basisE[OF this] guess B' . note B' = this
-  then show "X \<in> sigma_sets UNIV B"
-    by (blast intro: sigma_sets_UNION \<open>countable B\<close> countable_subset)
-next
-  fix b assume "b \<in> B"
-  hence "open b" by (rule topological_basis_open[OF assms(2)])
-  thus "b \<in> sigma_sets UNIV (Collect open)" by auto
-qed simp_all
-
 lemma borel_measurable_Pair[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
   assumes f[measurable]: "f \<in> borel_measurable M"
@@ -574,6 +672,19 @@
 
 subsection \<open>Borel spaces on order topologies\<close>
 
+lemma [measurable]:
+  fixes a b :: "'a::linorder_topology"
+  shows lessThan_borel: "{..< a} \<in> sets borel"
+    and greaterThan_borel: "{a <..} \<in> sets borel"
+    and greaterThanLessThan_borel: "{a<..<b} \<in> sets borel"
+    and atMost_borel: "{..a} \<in> sets borel"
+    and atLeast_borel: "{a..} \<in> sets borel"
+    and atLeastAtMost_borel: "{a..b} \<in> sets borel"
+    and greaterThanAtMost_borel: "{a<..b} \<in> sets borel"
+    and atLeastLessThan_borel: "{a..<b} \<in> sets borel"
+  unfolding greaterThanAtMost_def atLeastLessThan_def
+  by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan
+                   closed_atMost closed_atLeast closed_atLeastAtMost)+
 
 lemma borel_Iio:
   "borel = sigma UNIV (range lessThan :: 'a::{linorder_topology, second_countable_topology} set set)"
@@ -663,6 +774,40 @@
   unfolding borel_Ioi
   by (rule measurable_measure_of) (auto simp: Int_def conj_commute)
 
+lemma borel_measurableI_le:
+  fixes f :: "'a \<Rightarrow> 'b::{linorder_topology, second_countable_topology}"
+  shows "(\<And>y. {x\<in>space M. f x \<le> y} \<in> sets M) \<Longrightarrow> f \<in> borel_measurable M"
+  by (rule borel_measurableI_greater) (auto simp: not_le[symmetric])
+
+lemma borel_measurableI_ge:
+  fixes f :: "'a \<Rightarrow> 'b::{linorder_topology, second_countable_topology}"
+  shows "(\<And>y. {x\<in>space M. y \<le> f x} \<in> sets M) \<Longrightarrow> f \<in> borel_measurable M"
+  by (rule borel_measurableI_less) (auto simp: not_le[symmetric])
+
+lemma borel_measurable_less[measurable]:
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
+  assumes "f \<in> borel_measurable M"
+  assumes "g \<in> borel_measurable M"
+  shows "{w \<in> space M. f w < g w} \<in> sets M"
+proof -
+  have "{w \<in> space M. f w < g w} = (\<lambda>x. (f x, g x)) -` {x. fst x < snd x} \<inter> space M"
+    by auto
+  also have "\<dots> \<in> sets M"
+    by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less]
+              continuous_intros)
+  finally show ?thesis .
+qed
+
+lemma
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
+  assumes f[measurable]: "f \<in> borel_measurable M"
+  assumes g[measurable]: "g \<in> borel_measurable M"
+  shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
+    and borel_measurable_eq[measurable]: "{w \<in> space M. f w = g w} \<in> sets M"
+    and borel_measurable_neq: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
+  unfolding eq_iff not_less[symmetric]
+  by measurable
+
 lemma borel_measurable_SUP[measurable (raw)]:
   fixes F :: "_ \<Rightarrow> _ \<Rightarrow> _::{complete_linorder, linorder_topology, second_countable_topology}"
   assumes [simp]: "countable I"
@@ -677,6 +822,50 @@
   shows "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable M"
   by (rule borel_measurableI_less) (simp add: INF_less_iff)
 
+lemma borel_measurable_cSUP[measurable (raw)]:
+  fixes F :: "_ \<Rightarrow> _ \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}"
+  assumes [simp]: "countable I"
+  assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
+  assumes bdd: "\<And>x. x \<in> space M \<Longrightarrow> bdd_above ((\<lambda>i. F i x) ` I)"
+  shows "(\<lambda>x. SUP i:I. F i x) \<in> borel_measurable M"
+proof cases
+  assume "I = {}" then show ?thesis
+    unfolding \<open>I = {}\<close> image_empty by simp
+next
+  assume "I \<noteq> {}"
+  show ?thesis
+  proof (rule borel_measurableI_le)
+    fix y
+    have "{x \<in> space M. \<forall>i\<in>I. F i x \<le> y} \<in> sets M"
+      by measurable
+    also have "{x \<in> space M. \<forall>i\<in>I. F i x \<le> y} = {x \<in> space M. (SUP i:I. F i x) \<le> y}"
+      by (simp add: cSUP_le_iff \<open>I \<noteq> {}\<close> bdd cong: conj_cong)
+    finally show "{x \<in> space M. (SUP i:I. F i x) \<le>  y} \<in> sets M"  .
+  qed
+qed
+
+lemma borel_measurable_cINF[measurable (raw)]:
+  fixes F :: "_ \<Rightarrow> _ \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}"
+  assumes [simp]: "countable I"
+  assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
+  assumes bdd: "\<And>x. x \<in> space M \<Longrightarrow> bdd_below ((\<lambda>i. F i x) ` I)"
+  shows "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable M"
+proof cases
+  assume "I = {}" then show ?thesis
+    unfolding \<open>I = {}\<close> image_empty by simp
+next
+  assume "I \<noteq> {}"
+  show ?thesis
+  proof (rule borel_measurableI_ge)
+    fix y
+    have "{x \<in> space M. \<forall>i\<in>I. y \<le> F i x} \<in> sets M"
+      by measurable
+    also have "{x \<in> space M. \<forall>i\<in>I. y \<le> F i x} = {x \<in> space M. y \<le> (INF i:I. F i x)}"
+      by (simp add: le_cINF_iff \<open>I \<noteq> {}\<close> bdd cong: conj_cong)
+    finally show "{x \<in> space M. y \<le> (INF i:I. F i x)} \<in> sets M"  .
+  qed
+qed
+
 lemma borel_measurable_lfp[consumes 1, case_names continuity step]:
   fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_linorder, linorder_topology, second_countable_topology})"
   assumes "sup_continuous F"
@@ -711,7 +900,102 @@
   finally show ?thesis .
 qed
 
-subsection \<open>Borel spaces on euclidean spaces\<close>
+lemma borel_measurable_max[measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) \<in> borel_measurable M"
+  by (rule borel_measurableI_less) simp
+
+lemma borel_measurable_min[measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) \<in> borel_measurable M"
+  by (rule borel_measurableI_greater) simp
+
+lemma borel_measurable_Min[measurable (raw)]:
+  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Min ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) \<in> borel_measurable M"
+proof (induct I rule: finite_induct)
+  case (insert i I) then show ?case
+    by (cases "I = {}") auto
+qed auto
+
+lemma borel_measurable_Max[measurable (raw)]:
+  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Max ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) \<in> borel_measurable M"
+proof (induct I rule: finite_induct)
+  case (insert i I) then show ?case
+    by (cases "I = {}") auto
+qed auto
+
+lemma borel_measurable_sup[measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. sup (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) \<in> borel_measurable M"
+  unfolding sup_max by measurable
+
+lemma borel_measurable_inf[measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. inf (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) \<in> borel_measurable M"
+  unfolding inf_min by measurable
+
+lemma [measurable (raw)]:
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}"
+  assumes "\<And>i. f i \<in> borel_measurable M"
+  shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
+    and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
+  unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto
+
+lemma measurable_convergent[measurable (raw)]:
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}"
+  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
+  shows "Measurable.pred M (\<lambda>x. convergent (\<lambda>i. f i x))"
+  unfolding convergent_ereal by measurable
+
+lemma sets_Collect_convergent[measurable]:
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}"
+  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
+  shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M"
+  by measurable
+
+lemma borel_measurable_lim[measurable (raw)]:
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}"
+  assumes [measurable]: "\<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 convergent (\<lambda>i. f i x) then limsup (\<lambda>i. f i x) else (THE i. False))"
+    by (simp add: lim_def convergent_def convergent_limsup_cl)
+  then show ?thesis
+    by simp
+qed
+
+lemma borel_measurable_LIMSEQ_order:
+  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}"
+  assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
+  and u: "\<And>i. u i \<in> borel_measurable M"
+  shows "u' \<in> borel_measurable M"
+proof -
+  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])
+  with u show ?thesis by (simp cong: measurable_cong)
+qed
+
+subsection \<open>Borel spaces on topological monoids\<close>
+
+lemma borel_measurable_add[measurable (raw)]:
+  fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, topological_monoid_add}"
+  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) (intro continuous_intros)
+
+lemma borel_measurable_setsum[measurable (raw)]:
+  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, topological_comm_monoid_add}"
+  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_suminf_order[measurable (raw)]:
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology, topological_comm_monoid_add}"
+  assumes f[measurable]: "\<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
+
+subsection \<open>Borel spaces on Euclidean spaces\<close>
 
 lemma borel_measurable_inner[measurable (raw)]:
   fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}"
@@ -721,20 +1005,6 @@
   using assms
   by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
 
-lemma [measurable]:
-  fixes a b :: "'a::linorder_topology"
-  shows lessThan_borel: "{..< a} \<in> sets borel"
-    and greaterThan_borel: "{a <..} \<in> sets borel"
-    and greaterThanLessThan_borel: "{a<..<b} \<in> sets borel"
-    and atMost_borel: "{..a} \<in> sets borel"
-    and atLeast_borel: "{a..} \<in> sets borel"
-    and atLeastAtMost_borel: "{a..b} \<in> sets borel"
-    and greaterThanAtMost_borel: "{a<..b} \<in> sets borel"
-    and atLeastLessThan_borel: "{a..<b} \<in> sets borel"
-  unfolding greaterThanAtMost_def atLeastLessThan_def
-  by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan
-                   closed_atMost closed_atLeast closed_atLeastAtMost)+
-
 notation
   eucl_less (infix "<e" 50)
 
@@ -754,50 +1024,6 @@
   unfolding box_oc box_co
   by (auto intro: borel_open borel_closed)
 
-lemma open_Collect_less:
-  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
-  assumes "continuous_on UNIV f"
-  assumes "continuous_on UNIV g"
-  shows "open {x. f x < g x}"
-proof -
-  have "open (\<Union>y. {x \<in> UNIV. f x \<in> {..< y}} \<inter> {x \<in> UNIV. g x \<in> {y <..}})" (is "open ?X")
-    by (intro open_UN ballI open_Int continuous_open_preimage assms) auto
-  also have "?X = {x. f x < g x}"
-    by (auto intro: dense)
-  finally show ?thesis .
-qed
-
-lemma closed_Collect_le:
-  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
-  assumes f: "continuous_on UNIV f"
-  assumes g: "continuous_on UNIV g"
-  shows "closed {x. f x \<le> g x}"
-  using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed .
-
-lemma borel_measurable_less[measurable]:
-  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
-  assumes "f \<in> borel_measurable M"
-  assumes "g \<in> borel_measurable M"
-  shows "{w \<in> space M. f w < g w} \<in> sets M"
-proof -
-  have "{w \<in> space M. f w < g w} = (\<lambda>x. (f x, g x)) -` {x. fst x < snd x} \<inter> space M"
-    by auto
-  also have "\<dots> \<in> sets M"
-    by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less]
-              continuous_intros)
-  finally show ?thesis .
-qed
-
-lemma
-  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
-  assumes f[measurable]: "f \<in> borel_measurable M"
-  assumes g[measurable]: "g \<in> borel_measurable M"
-  shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
-    and borel_measurable_eq[measurable]: "{w \<in> space M. f w = g w} \<in> sets M"
-    and borel_measurable_neq: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
-  unfolding eq_iff not_less[symmetric]
-  by measurable
-
 lemma
   fixes i :: "'a::{second_countable_topology, real_inner}"
   shows hafspace_less_borel: "{x. a < x \<bullet> i} \<in> sets borel"
@@ -806,66 +1032,6 @@
     and hafspace_greater_eq_borel: "{x. x \<bullet> i \<le> a} \<in> sets borel"
   by simp_all
 
-subsection "Borel space equals sigma algebras over intervals"
-
-lemma borel_sigma_sets_subset:
-  "A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel"
-  using sets.sigma_sets_subset[of A borel] by simp
-
-lemma borel_eq_sigmaI1:
-  fixes F :: "'i \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
-  assumes borel_eq: "borel = sigma UNIV X"
-  assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV (F ` A))"
-  assumes F: "\<And>i. i \<in> A \<Longrightarrow> F i \<in> sets borel"
-  shows "borel = sigma UNIV (F ` A)"
-  unfolding borel_def
-proof (intro sigma_eqI antisym)
-  have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel"
-    unfolding borel_def by simp
-  also have "\<dots> = sigma_sets UNIV X"
-    unfolding borel_eq by simp
-  also have "\<dots> \<subseteq> sigma_sets UNIV (F`A)"
-    using X by (intro sigma_algebra.sigma_sets_subset[OF sigma_algebra_sigma_sets]) auto
-  finally show "sigma_sets UNIV {S. open S} \<subseteq> sigma_sets UNIV (F`A)" .
-  show "sigma_sets UNIV (F`A) \<subseteq> sigma_sets UNIV {S. open S}"
-    unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto
-qed auto
-
-lemma borel_eq_sigmaI2:
-  fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set"
-    and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set"
-  assumes borel_eq: "borel = sigma UNIV ((\<lambda>(i, j). G i j)`B)"
-  assumes X: "\<And>i j. (i, j) \<in> B \<Longrightarrow> G i j \<in> sets (sigma UNIV ((\<lambda>(i, j). F i j) ` A))"
-  assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel"
-  shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)"
-  using assms
-  by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` B" and F="(\<lambda>(i, j). F i j)"]) auto
-
-lemma borel_eq_sigmaI3:
-  fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
-  assumes borel_eq: "borel = sigma UNIV X"
-  assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV ((\<lambda>(i, j). F i j) ` A))"
-  assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel"
-  shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)"
-  using assms by (intro borel_eq_sigmaI1[where X=X and F="(\<lambda>(i, j). F i j)"]) auto
-
-lemma borel_eq_sigmaI4:
-  fixes F :: "'i \<Rightarrow> 'a::topological_space set"
-    and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set"
-  assumes borel_eq: "borel = sigma UNIV ((\<lambda>(i, j). G i j)`A)"
-  assumes X: "\<And>i j. (i, j) \<in> A \<Longrightarrow> G i j \<in> sets (sigma UNIV (range F))"
-  assumes F: "\<And>i. F i \<in> sets borel"
-  shows "borel = sigma UNIV (range F)"
-  using assms by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` A" and F=F]) auto
-
-lemma borel_eq_sigmaI5:
-  fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and G :: "'l \<Rightarrow> 'a::topological_space set"
-  assumes borel_eq: "borel = sigma UNIV (range G)"
-  assumes X: "\<And>i. G i \<in> sets (sigma UNIV (range (\<lambda>(i, j). F i j)))"
-  assumes F: "\<And>i j. F i j \<in> sets borel"
-  shows "borel = sigma UNIV (range (\<lambda>(i, j). F i j))"
-  using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(\<lambda>(i, j). F i j)"]) auto
-
 lemma borel_eq_box:
   "borel = sigma UNIV (range (\<lambda> (a, b). box a b :: 'a :: euclidean_space set))"
     (is "_ = ?SIGMA")
@@ -1057,6 +1223,28 @@
        (auto intro!: sigma_sets_top)
 qed auto
 
+lemma borel_set_induct[consumes 1, case_names empty interval compl union]:
+  assumes "A \<in> sets borel"
+  assumes empty: "P {}" and int: "\<And>a b. a \<le> b \<Longrightarrow> P {a..b}" and compl: "\<And>A. A \<in> sets borel \<Longrightarrow> P A \<Longrightarrow> P (-A)" and
+          un: "\<And>f. disjoint_family f \<Longrightarrow> (\<And>i. f i \<in> sets borel) \<Longrightarrow>  (\<And>i. P (f i)) \<Longrightarrow> P (\<Union>i::nat. f i)"
+  shows "P (A::real set)"
+proof-
+  let ?G = "range (\<lambda>(a,b). {a..b::real})"
+  have "Int_stable ?G" "?G \<subseteq> Pow UNIV" "A \<in> sigma_sets UNIV ?G"
+      using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def)
+  thus ?thesis
+  proof (induction rule: sigma_sets_induct_disjoint)
+    case (union f)
+      from union.hyps(2) have "\<And>i. f i \<in> sets borel" by (auto simp: borel_eq_atLeastAtMost)
+      with union show ?case by (auto intro: un)
+  next
+    case (basic A)
+    then obtain a b where "A = {a .. b}" by auto
+    then show ?case
+      by (cases "a \<le> b") (auto intro: int empty)
+  qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost)
+qed
+
 lemma borel_sigma_sets_Ioc: "borel = sigma UNIV (range (\<lambda>(a, b). {a <.. b::real}))"
 proof (rule borel_eq_sigmaI5[OF borel_eq_atMost])
   fix i :: real
@@ -1081,22 +1269,6 @@
     by (auto intro: sigma_sets.intros(2-) simp: eucl_lessThan)
 qed auto
 
-lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
-  unfolding borel_def
-proof (intro sigma_eqI sigma_sets_eqI, safe)
-  fix x :: "'a set" assume "open x"
-  hence "x = UNIV - (UNIV - x)" by auto
-  also have "\<dots> \<in> sigma_sets UNIV (Collect closed)"
-    by (force intro: sigma_sets.Compl simp: \<open>open x\<close>)
-  finally show "x \<in> sigma_sets UNIV (Collect closed)" by simp
-next
-  fix x :: "'a set" assume "closed x"
-  hence "x = UNIV - (UNIV - x)" by auto
-  also have "\<dots> \<in> sigma_sets UNIV (Collect open)"
-    by (force intro: sigma_sets.Compl simp: \<open>closed x\<close>)
-  finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
-qed simp_all
-
 lemma borel_measurable_halfspacesI:
   fixes f :: "'a \<Rightarrow> 'c::euclidean_space"
   assumes F: "borel = sigma UNIV (F ` (UNIV \<times> Basis))"
@@ -1158,28 +1330,6 @@
     by (subst borel_measurable_iff_halfspace_le) auto
 qed auto
 
-lemma borel_set_induct[consumes 1, case_names empty interval compl union]:
-  assumes "A \<in> sets borel"
-  assumes empty: "P {}" and int: "\<And>a b. a \<le> b \<Longrightarrow> P {a..b}" and compl: "\<And>A. A \<in> sets borel \<Longrightarrow> P A \<Longrightarrow> P (-A)" and
-          un: "\<And>f. disjoint_family f \<Longrightarrow> (\<And>i. f i \<in> sets borel) \<Longrightarrow>  (\<And>i. P (f i)) \<Longrightarrow> P (\<Union>i::nat. f i)"
-  shows "P (A::real set)"
-proof-
-  let ?G = "range (\<lambda>(a,b). {a..b::real})"
-  have "Int_stable ?G" "?G \<subseteq> Pow UNIV" "A \<in> sigma_sets UNIV ?G"
-      using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def)
-  thus ?thesis
-  proof (induction rule: sigma_sets_induct_disjoint)
-    case (union f)
-      from union.hyps(2) have "\<And>i. f i \<in> sets borel" by (auto simp: borel_eq_atLeastAtMost)
-      with union show ?case by (auto intro: un)
-  next
-    case (basic A)
-    then obtain a b where "A = {a .. b}" by auto
-    then show ?case
-      by (cases "a \<le> b") (auto intro: int empty)
-  qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost)
-qed
-
 subsection "Borel measurable operators"
 
 lemma borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel"
@@ -1195,22 +1345,6 @@
   shows "(\<lambda>x. - g x) \<in> borel_measurable M"
   by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros)
 
-lemma borel_measurable_add[measurable (raw)]:
-  fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
-  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) (intro continuous_intros)
-
-lemma borel_measurable_setsum[measurable (raw)]:
-  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
-  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[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   assumes f: "f \<in> borel_measurable M"
@@ -1291,28 +1425,6 @@
     (\<lambda>x. f x / g x::'b::{second_countable_topology, real_normed_div_algebra}) \<in> borel_measurable M"
   by (simp add: divide_inverse)
 
-lemma borel_measurable_max[measurable (raw)]:
-  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
-  by (simp add: max_def)
-
-lemma borel_measurable_min[measurable (raw)]:
-  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
-  by (simp add: min_def)
-
-lemma borel_measurable_Min[measurable (raw)]:
-  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Min ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
-proof (induct I rule: finite_induct)
-  case (insert i I) then show ?case
-    by (cases "I = {}") auto
-qed auto
-
-lemma borel_measurable_Max[measurable (raw)]:
-  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Max ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
-proof (induct I rule: finite_induct)
-  case (insert i I) then show ?case
-    by (cases "I = {}") auto
-qed auto
-
 lemma borel_measurable_abs[measurable (raw)]:
   "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
   unfolding abs_real_def by simp
@@ -1538,9 +1650,7 @@
   assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   shows borel_measurable_ereal_add: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
     and borel_measurable_ereal_times: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
-    and borel_measurable_ereal_min: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
-    and borel_measurable_ereal_max: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
-  by (simp_all add: borel_measurable_ereal2 min_def max_def)
+  by (simp_all add: borel_measurable_ereal2)
 
 lemma [measurable(raw)]:
   fixes f g :: "'a \<Rightarrow> ereal"
@@ -1562,54 +1672,67 @@
   shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
   using assms by (induction S rule: infinite_finite_induct) auto
 
-lemma [measurable (raw)]:
-  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
-  assumes "\<And>i. f i \<in> borel_measurable M"
-  shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
-    and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
-  unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto
-
-lemma sets_Collect_eventually_sequentially[measurable]:
-  "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
-  unfolding eventually_sequentially by simp
-
-lemma sets_Collect_ereal_convergent[measurable]:
-  fixes f :: "nat \<Rightarrow> 'a => ereal"
-  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
-  shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M"
-  unfolding convergent_ereal by auto
-
-lemma borel_measurable_extreal_lim[measurable (raw)]:
-  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
-  assumes [measurable]: "\<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 convergent (\<lambda>i. f i x) then limsup (\<lambda>i. f i x) else (THE i. False))"
-    by (simp add: lim_def convergent_def convergent_limsup_cl)
-  then show ?thesis
-    by simp
-qed
-
-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) \<longlonglongrightarrow> u' x"
-  and u: "\<And>i. u i \<in> borel_measurable M"
-  shows "u' \<in> borel_measurable M"
-proof -
-  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])
-  with u show ?thesis by (simp cong: measurable_cong)
-qed
-
 lemma borel_measurable_extreal_suminf[measurable (raw)]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
   shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
   unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
 
+subsection "Borel space on the extended non-negative reals"
+
+text \<open> @{type ennreal} is a topological monoid, so no rules for plus are required, also all order
+  statements are usually done on type classes. \<close>
+
+lemma measurable_enn2ereal[measurable]: "enn2ereal \<in> borel \<rightarrow>\<^sub>M borel"
+  by (intro borel_measurable_continuous_on1 continuous_on_enn2ereal)
+
+lemma measurable_e2ennreal[measurable]: "e2ennreal \<in> borel \<rightarrow>\<^sub>M borel"
+  by (intro borel_measurable_continuous_on1 continuous_on_e2ennreal)
+
+definition [simp]: "is_borel f M \<longleftrightarrow> f \<in> borel_measurable M"
+
+lemma is_borel_transfer[transfer_rule]: "rel_fun (rel_fun op = pcr_ennreal) op = is_borel is_borel"
+  unfolding is_borel_def[abs_def]
+proof (safe intro!: rel_funI ext dest!: rel_fun_eq_pcr_ennreal[THEN iffD1])
+  fix f and M :: "'a measure"
+  show "f \<in> borel_measurable M" if f: "enn2ereal \<circ> f \<in> borel_measurable M"
+    using measurable_compose[OF f measurable_e2ennreal] by simp
+qed simp
+
+lemma measurable_ennreal[measurable]: "ennreal \<in> borel \<rightarrow>\<^sub>M borel"
+  unfolding is_borel_def[symmetric] by transfer simp
+
+lemma borel_measurable_times_ennreal[measurable (raw)]:
+  fixes f g :: "'a \<Rightarrow> ennreal"
+  shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> g \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. f x * g x) \<in> M \<rightarrow>\<^sub>M borel"
+  unfolding is_borel_def[symmetric] by transfer simp
+
+lemma borel_measurable_inverse_ennreal[measurable (raw)]:
+  fixes f :: "'a \<Rightarrow> ennreal"
+  shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. inverse (f x)) \<in> M \<rightarrow>\<^sub>M borel"
+  unfolding is_borel_def[symmetric] by transfer simp
+
+lemma borel_measurable_divide_ennreal[measurable (raw)]:
+  fixes f :: "'a \<Rightarrow> ennreal"
+  shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> g \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. f x / g x) \<in> M \<rightarrow>\<^sub>M borel"
+  unfolding divide_ennreal_def by simp
+
+lemma borel_measurable_minus_ennreal[measurable (raw)]:
+  fixes f :: "'a \<Rightarrow> ennreal"
+  shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> g \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. f x - g x) \<in> M \<rightarrow>\<^sub>M borel"
+  unfolding is_borel_def[symmetric] by transfer simp
+
+lemma borel_measurable_setprod_ennreal[measurable (raw)]:
+  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ennreal"
+  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
+  shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
+  using assms by (induction S rule: infinite_finite_induct) auto
+
+hide_const (open) is_borel
+
 subsection \<open>LIMSEQ is borel measurable\<close>
 
-lemma borel_measurable_LIMSEQ:
+lemma borel_measurable_LIMSEQ_real:
   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real"
   assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
   and u: "\<And>i. u i \<in> borel_measurable M"
@@ -1632,7 +1755,7 @@
   fix A :: "'b set" assume "closed A"
 
   have [measurable]: "(\<lambda>x. infdist (g x) A) \<in> borel_measurable M"
-  proof (rule borel_measurable_LIMSEQ)
+  proof (rule borel_measurable_LIMSEQ_real)
     show "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. infdist (f i x) A) \<longlonglongrightarrow> infdist (g x) A"
       by (intro tendsto_infdist lim)
     show "\<And>i. (\<lambda>x. infdist (f i x) A) \<in> borel_measurable M"
@@ -1659,7 +1782,7 @@
   shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
   unfolding metric_Cauchy_iff2 using f by auto
 
-lemma borel_measurable_lim[measurable (raw)]:
+lemma borel_measurable_lim_metric[measurable (raw)]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
@@ -1687,11 +1810,6 @@
   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
 
-lemma borel_measurable_sup[measurable (raw)]:
-  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
-    (\<lambda>x. sup (f x) (g x)::ereal) \<in> borel_measurable M"
-  by simp
-
 (* Proof by Jeremy Avigad and Luke Serafin *)
 lemma isCont_borel:
   fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
diff -r de25474ce728 -r 20288ba55e85 src/HOL/Probability/Set_Integral.thy
--- a/src/HOL/Probability/Set_Integral.thy	Wed Mar 16 13:57:06 2016 +0000
+++ b/src/HOL/Probability/Set_Integral.thy	Wed Mar 16 14:05:30 2016 +0000
@@ -363,7 +363,7 @@
         done
     qed auto }
   then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
-    apply (rule borel_measurable_LIMSEQ)
+    apply (rule borel_measurable_LIMSEQ_real)
     apply assumption
     apply (intro borel_measurable_integrable intgbl)
     done