src/HOL/Probability/Borel_Space.thy
changeset 50002 ce0d316b5b44
parent 50001 382bd3173584
child 50003 8c213922ed49
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:00:39 2012 +0100
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:23:40 2012 +0100
     1.3 @@ -30,14 +30,20 @@
     1.4  lemma space_borel[simp]: "space borel = UNIV"
     1.5    unfolding borel_def by auto
     1.6  
     1.7 -lemma borel_open[simp]:
     1.8 +lemma space_in_borel[measurable]: "UNIV \<in> sets borel"
     1.9 +  unfolding borel_def by auto
    1.10 +
    1.11 +lemma pred_Collect_borel[measurable (raw)]: "Sigma_Algebra.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
    1.12 +  unfolding borel_def pred_def by auto
    1.13 +
    1.14 +lemma borel_open[simp, measurable (raw generic)]:
    1.15    assumes "open A" shows "A \<in> sets borel"
    1.16  proof -
    1.17    have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
    1.18    thus ?thesis unfolding borel_def by auto
    1.19  qed
    1.20  
    1.21 -lemma borel_closed[simp]:
    1.22 +lemma borel_closed[simp, measurable (raw generic)]:
    1.23    assumes "closed A" shows "A \<in> sets borel"
    1.24  proof -
    1.25    have "space borel - (- A) \<in> sets borel"
    1.26 @@ -45,23 +51,18 @@
    1.27    thus ?thesis by simp
    1.28  qed
    1.29  
    1.30 -lemma borel_comp[intro,simp]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
    1.31 -  unfolding Compl_eq_Diff_UNIV by (intro Diff) auto
    1.32 +lemma borel_insert[measurable]:
    1.33 +  "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t2_space measure)"
    1.34 +  unfolding insert_def by (rule Un) auto
    1.35 +
    1.36 +lemma borel_comp[intro, simp, measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
    1.37 +  unfolding Compl_eq_Diff_UNIV by simp
    1.38  
    1.39  lemma borel_measurable_vimage:
    1.40    fixes f :: "'a \<Rightarrow> 'x::t2_space"
    1.41 -  assumes borel: "f \<in> borel_measurable M"
    1.42 +  assumes borel[measurable]: "f \<in> borel_measurable M"
    1.43    shows "f -` {x} \<inter> space M \<in> sets M"
    1.44 -proof (cases "x \<in> f ` space M")
    1.45 -  case True then obtain y where "x = f y" by auto
    1.46 -  from closed_singleton[of "f y"]
    1.47 -  have "{f y} \<in> sets borel" by (rule borel_closed)
    1.48 -  with assms show ?thesis
    1.49 -    unfolding in_borel_measurable_borel `x = f y` by auto
    1.50 -next
    1.51 -  case False hence "f -` {x} \<inter> space M = {}" by auto
    1.52 -  thus ?thesis by auto
    1.53 -qed
    1.54 +  by simp
    1.55  
    1.56  lemma borel_measurableI:
    1.57    fixes f :: "'a \<Rightarrow> 'x\<Colon>topological_space"
    1.58 @@ -81,7 +82,7 @@
    1.59        using closed_singleton[of x] by (rule borel_closed)
    1.60    qed simp
    1.61  
    1.62 -lemma borel_measurable_const[simp, intro]:
    1.63 +lemma borel_measurable_const[simp, intro, measurable (raw)]:
    1.64    "(\<lambda>x. c) \<in> borel_measurable M"
    1.65    by auto
    1.66  
    1.67 @@ -91,7 +92,7 @@
    1.68    unfolding indicator_def [abs_def] using A
    1.69    by (auto intro!: measurable_If_set)
    1.70  
    1.71 -lemma borel_measurable_indicator': 
    1.72 +lemma borel_measurable_indicator'[measurable]:
    1.73    "{x\<in>space M. x \<in> A} \<in> sets M \<Longrightarrow> indicator A \<in> borel_measurable M"
    1.74    unfolding indicator_def[abs_def]
    1.75    by (auto intro!: measurable_If)
    1.76 @@ -119,115 +120,63 @@
    1.77    shows "f \<in> borel_measurable M"
    1.78    using assms unfolding measurable_def by auto
    1.79  
    1.80 +lemma borel_measurable_continuous_on1:
    1.81 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
    1.82 +  assumes "continuous_on UNIV f"
    1.83 +  shows "f \<in> borel_measurable borel"
    1.84 +  apply(rule borel_measurableI)
    1.85 +  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
    1.86 +
    1.87  section "Borel spaces on euclidean spaces"
    1.88  
    1.89 -lemma lessThan_borel[simp, intro]:
    1.90 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
    1.91 -  shows "{..< a} \<in> sets borel"
    1.92 -  by (blast intro: borel_open)
    1.93 -
    1.94 -lemma greaterThan_borel[simp, intro]:
    1.95 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
    1.96 -  shows "{a <..} \<in> sets borel"
    1.97 -  by (blast intro: borel_open)
    1.98 -
    1.99 -lemma greaterThanLessThan_borel[simp, intro]:
   1.100 -  fixes a b :: "'a\<Colon>ordered_euclidean_space"
   1.101 -  shows "{a<..<b} \<in> sets borel"
   1.102 -  by (blast intro: borel_open)
   1.103 +lemma borel_measurable_euclidean_component'[measurable]:
   1.104 +  "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel"
   1.105 +  by (intro continuous_on_euclidean_component continuous_on_id borel_measurable_continuous_on1)
   1.106  
   1.107 -lemma atMost_borel[simp, intro]:
   1.108 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.109 -  shows "{..a} \<in> sets borel"
   1.110 -  by (blast intro: borel_closed)
   1.111 -
   1.112 -lemma atLeast_borel[simp, intro]:
   1.113 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.114 -  shows "{a..} \<in> sets borel"
   1.115 -  by (blast intro: borel_closed)
   1.116 -
   1.117 -lemma atLeastAtMost_borel[simp, intro]:
   1.118 -  fixes a b :: "'a\<Colon>ordered_euclidean_space"
   1.119 -  shows "{a..b} \<in> sets borel"
   1.120 -  by (blast intro: borel_closed)
   1.121 +lemma borel_measurable_euclidean_component:
   1.122 +  "(f :: 'a \<Rightarrow> 'b::euclidean_space) \<in> borel_measurable M \<Longrightarrow>(\<lambda>x. f x $$ i) \<in> borel_measurable M"
   1.123 +  by simp
   1.124  
   1.125 -lemma greaterThanAtMost_borel[simp, intro]:
   1.126 -  fixes a b :: "'a\<Colon>ordered_euclidean_space"
   1.127 -  shows "{a<..b} \<in> sets borel"
   1.128 -  unfolding greaterThanAtMost_def by blast
   1.129 -
   1.130 -lemma atLeastLessThan_borel[simp, intro]:
   1.131 +lemma [simp, intro, measurable]:
   1.132    fixes a b :: "'a\<Colon>ordered_euclidean_space"
   1.133 -  shows "{a..<b} \<in> sets borel"
   1.134 -  unfolding atLeastLessThan_def by blast
   1.135 -
   1.136 -lemma hafspace_less_borel[simp, intro]:
   1.137 -  fixes a :: real
   1.138 -  shows "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
   1.139 -  by (auto intro!: borel_open open_halfspace_component_gt)
   1.140 +  shows lessThan_borel: "{..< a} \<in> sets borel"
   1.141 +    and greaterThan_borel: "{a <..} \<in> sets borel"
   1.142 +    and greaterThanLessThan_borel: "{a<..<b} \<in> sets borel"
   1.143 +    and atMost_borel: "{..a} \<in> sets borel"
   1.144 +    and atLeast_borel: "{a..} \<in> sets borel"
   1.145 +    and atLeastAtMost_borel: "{a..b} \<in> sets borel"
   1.146 +    and greaterThanAtMost_borel: "{a<..b} \<in> sets borel"
   1.147 +    and atLeastLessThan_borel: "{a..<b} \<in> sets borel"
   1.148 +  unfolding greaterThanAtMost_def atLeastLessThan_def
   1.149 +  by (blast intro: borel_open borel_closed)+
   1.150  
   1.151 -lemma hafspace_greater_borel[simp, intro]:
   1.152 -  fixes a :: real
   1.153 -  shows "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
   1.154 -  by (auto intro!: borel_open open_halfspace_component_lt)
   1.155 +lemma 
   1.156 +  shows hafspace_less_borel[simp, intro]: "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
   1.157 +    and hafspace_greater_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
   1.158 +    and hafspace_less_eq_borel[simp, intro]: "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
   1.159 +    and hafspace_greater_eq_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
   1.160 +  by simp_all
   1.161  
   1.162 -lemma hafspace_less_eq_borel[simp, intro]:
   1.163 -  fixes a :: real
   1.164 -  shows "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
   1.165 -  by (auto intro!: borel_closed closed_halfspace_component_ge)
   1.166 -
   1.167 -lemma hafspace_greater_eq_borel[simp, intro]:
   1.168 -  fixes a :: real
   1.169 -  shows "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
   1.170 -  by (auto intro!: borel_closed closed_halfspace_component_le)
   1.171 -
   1.172 -lemma borel_measurable_less[simp, intro]:
   1.173 +lemma borel_measurable_less[simp, intro, measurable]:
   1.174    fixes f :: "'a \<Rightarrow> real"
   1.175    assumes f: "f \<in> borel_measurable M"
   1.176    assumes g: "g \<in> borel_measurable M"
   1.177    shows "{w \<in> space M. f w < g w} \<in> sets M"
   1.178  proof -
   1.179 -  have "{w \<in> space M. f w < g w} =
   1.180 -        (\<Union>r. (f -` {..< of_rat r} \<inter> space M) \<inter> (g -` {of_rat r <..} \<inter> space M))"
   1.181 +  have "{w \<in> space M. f w < g w} = {x \<in> space M. \<exists>r. f x < of_rat r \<and> of_rat r < g x}"
   1.182      using Rats_dense_in_real by (auto simp add: Rats_def)
   1.183 -  then show ?thesis using f g
   1.184 -    by simp (blast intro: measurable_sets)
   1.185 -qed
   1.186 -
   1.187 -lemma borel_measurable_le[simp, intro]:
   1.188 -  fixes f :: "'a \<Rightarrow> real"
   1.189 -  assumes f: "f \<in> borel_measurable M"
   1.190 -  assumes g: "g \<in> borel_measurable M"
   1.191 -  shows "{w \<in> space M. f w \<le> g w} \<in> sets M"
   1.192 -proof -
   1.193 -  have "{w \<in> space M. f w \<le> g w} = space M - {w \<in> space M. g w < f w}"
   1.194 -    by auto
   1.195 -  thus ?thesis using f g
   1.196 -    by simp blast
   1.197 +  with f g show ?thesis
   1.198 +    by simp
   1.199  qed
   1.200  
   1.201 -lemma borel_measurable_eq[simp, intro]:
   1.202 +lemma [simp, intro]:
   1.203    fixes f :: "'a \<Rightarrow> real"
   1.204 -  assumes f: "f \<in> borel_measurable M"
   1.205 -  assumes g: "g \<in> borel_measurable M"
   1.206 -  shows "{w \<in> space M. f w = g w} \<in> sets M"
   1.207 -proof -
   1.208 -  have "{w \<in> space M. f w = g w} =
   1.209 -        {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
   1.210 -    by auto
   1.211 -  thus ?thesis using f g by auto
   1.212 -qed
   1.213 -
   1.214 -lemma borel_measurable_neq[simp, intro]:
   1.215 -  fixes f :: "'a \<Rightarrow> real"
   1.216 -  assumes f: "f \<in> borel_measurable M"
   1.217 -  assumes g: "g \<in> borel_measurable M"
   1.218 -  shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
   1.219 -proof -
   1.220 -  have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}"
   1.221 -    by auto
   1.222 -  thus ?thesis using f g by auto
   1.223 -qed
   1.224 +  assumes f[measurable]: "f \<in> borel_measurable M"
   1.225 +  assumes g[measurable]: "g \<in> borel_measurable M"
   1.226 +  shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
   1.227 +    and borel_measurable_eq[measurable]: "{w \<in> space M. f w = g w} \<in> sets M"
   1.228 +    and borel_measurable_neq: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
   1.229 +  unfolding eq_iff not_less[symmetric] by measurable+
   1.230  
   1.231  subsection "Borel space equals sigma algebras over intervals"
   1.232  
   1.233 @@ -377,7 +326,7 @@
   1.234      by (intro sigma_algebra_sigma_sets) simp_all
   1.235    have *: "?set = (\<Union>n. UNIV - {x\<Colon>'a. x $$ i < a + 1 / real (Suc n)})"
   1.236    proof (safe, simp_all add: not_less)
   1.237 -    fix x assume "a < x $$ i"
   1.238 +    fix x :: 'a assume "a < x $$ i"
   1.239      with reals_Archimedean[of "x $$ i - a"]
   1.240      obtain n where "a + 1 / real (Suc n) < x $$ i"
   1.241        by (auto simp: inverse_eq_divide field_simps)
   1.242 @@ -390,7 +339,7 @@
   1.243      finally show "a < x" .
   1.244    qed
   1.245    show "?set \<in> ?SIGMA" unfolding *
   1.246 -    by (auto intro!: Diff)
   1.247 +    by (auto del: Diff intro!: Diff)
   1.248  qed
   1.249  
   1.250  lemma borel_eq_halfspace_less:
   1.251 @@ -631,27 +580,13 @@
   1.252  
   1.253  lemma borel_measurable_iff_ge:
   1.254    "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)"
   1.255 -  using borel_measurable_iff_halfspace_ge[where 'c=real] by simp
   1.256 +  using borel_measurable_iff_halfspace_ge[where 'c=real]
   1.257 +  by simp
   1.258  
   1.259  lemma borel_measurable_iff_greater:
   1.260    "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
   1.261    using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
   1.262  
   1.263 -lemma borel_measurable_euclidean_component':
   1.264 -  "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel"
   1.265 -proof (rule borel_measurableI)
   1.266 -  fix S::"real set" assume "open S"
   1.267 -  from open_vimage_euclidean_component[OF this]
   1.268 -  show "(\<lambda>x. x $$ i) -` S \<inter> space borel \<in> sets borel"
   1.269 -    by (auto intro: borel_open)
   1.270 -qed
   1.271 -
   1.272 -lemma borel_measurable_euclidean_component:
   1.273 -  fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
   1.274 -  assumes f: "f \<in> borel_measurable M"
   1.275 -  shows "(\<lambda>x. f x $$ i) \<in> borel_measurable M"
   1.276 -  using measurable_comp[OF f borel_measurable_euclidean_component'] by (simp add: comp_def)
   1.277 -
   1.278  lemma borel_measurable_euclidean_space:
   1.279    fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   1.280    shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M)"
   1.281 @@ -667,13 +602,6 @@
   1.282  
   1.283  subsection "Borel measurable operators"
   1.284  
   1.285 -lemma borel_measurable_continuous_on1:
   1.286 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   1.287 -  assumes "continuous_on UNIV f"
   1.288 -  shows "f \<in> borel_measurable borel"
   1.289 -  apply(rule borel_measurableI)
   1.290 -  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
   1.291 -
   1.292  lemma borel_measurable_continuous_on:
   1.293    fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   1.294    assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
   1.295 @@ -693,7 +621,7 @@
   1.296      {x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel - A else {})"
   1.297      by (auto split: split_if_asm)
   1.298    also have "\<dots> \<in> sets borel"
   1.299 -    using * `open A` by (auto simp del: space_borel intro!: Un)
   1.300 +    using * `open A` by auto
   1.301    finally show "?f -` S \<inter> space borel \<in> sets borel" .
   1.302  qed
   1.303  
   1.304 @@ -705,7 +633,7 @@
   1.305    using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
   1.306    by (simp add: comp_def)
   1.307  
   1.308 -lemma borel_measurable_uminus[simp, intro]:
   1.309 +lemma borel_measurable_uminus[simp, intro, measurable (raw)]:
   1.310    fixes g :: "'a \<Rightarrow> real"
   1.311    assumes g: "g \<in> borel_measurable M"
   1.312    shows "(\<lambda>x. - g x) \<in> borel_measurable M"
   1.313 @@ -716,7 +644,7 @@
   1.314    shows "x $$ i = (if i < DIM('a) then fst x $$ i else snd x $$ (i - DIM('a)))"
   1.315    unfolding euclidean_component_def basis_prod_def inner_prod_def by auto
   1.316  
   1.317 -lemma borel_measurable_Pair[simp, intro]:
   1.318 +lemma borel_measurable_Pair[simp, intro, measurable (raw)]:
   1.319    fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   1.320    assumes f: "f \<in> borel_measurable M"
   1.321    assumes g: "g \<in> borel_measurable M"
   1.322 @@ -726,7 +654,7 @@
   1.323    have [simp]: "\<And>P A B C. {w. (P \<longrightarrow> A w \<and> B w) \<and> (\<not> P \<longrightarrow> A w \<and> C w)} = 
   1.324      {w. A w \<and> (P \<longrightarrow> B w) \<and> (\<not> P \<longrightarrow> C w)}" by auto
   1.325    from i f g show "{w \<in> space M. (f w, g w) $$ i \<le> a} \<in> sets M"
   1.326 -    by (auto simp: euclidean_component_prod intro!: sets_Collect borel_measurable_euclidean_component)
   1.327 +    by (auto simp: euclidean_component_prod)
   1.328  qed
   1.329  
   1.330  lemma continuous_on_fst: "continuous_on UNIV fst"
   1.331 @@ -757,7 +685,7 @@
   1.332      unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
   1.333  qed
   1.334  
   1.335 -lemma borel_measurable_add[simp, intro]:
   1.336 +lemma borel_measurable_add[simp, intro, measurable (raw)]:
   1.337    fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   1.338    assumes f: "f \<in> borel_measurable M"
   1.339    assumes g: "g \<in> borel_measurable M"
   1.340 @@ -766,7 +694,7 @@
   1.341    by (rule borel_measurable_continuous_Pair)
   1.342       (auto intro: continuous_on_fst continuous_on_snd continuous_on_add)
   1.343  
   1.344 -lemma borel_measurable_setsum[simp, intro]:
   1.345 +lemma borel_measurable_setsum[simp, intro, measurable (raw)]:
   1.346    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
   1.347    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   1.348    shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
   1.349 @@ -775,14 +703,14 @@
   1.350    thus ?thesis using assms by induct auto
   1.351  qed simp
   1.352  
   1.353 -lemma borel_measurable_diff[simp, intro]:
   1.354 +lemma borel_measurable_diff[simp, intro, measurable (raw)]:
   1.355    fixes f :: "'a \<Rightarrow> real"
   1.356    assumes f: "f \<in> borel_measurable M"
   1.357    assumes g: "g \<in> borel_measurable M"
   1.358    shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   1.359    unfolding diff_minus using assms by fast
   1.360  
   1.361 -lemma borel_measurable_times[simp, intro]:
   1.362 +lemma borel_measurable_times[simp, intro, measurable (raw)]:
   1.363    fixes f :: "'a \<Rightarrow> real"
   1.364    assumes f: "f \<in> borel_measurable M"
   1.365    assumes g: "g \<in> borel_measurable M"
   1.366 @@ -796,7 +724,7 @@
   1.367    shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. dist (f x) (g x))"
   1.368    unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist)
   1.369  
   1.370 -lemma borel_measurable_dist[simp, intro]:
   1.371 +lemma borel_measurable_dist[simp, intro, measurable (raw)]:
   1.372    fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
   1.373    assumes f: "f \<in> borel_measurable M"
   1.374    assumes g: "g \<in> borel_measurable M"
   1.375 @@ -805,6 +733,14 @@
   1.376    by (rule borel_measurable_continuous_Pair)
   1.377       (intro continuous_on_dist continuous_on_fst continuous_on_snd)
   1.378    
   1.379 +lemma borel_measurable_scaleR[measurable (raw)]:
   1.380 +  fixes g :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
   1.381 +  assumes f: "f \<in> borel_measurable M"
   1.382 +  assumes g: "g \<in> borel_measurable M"
   1.383 +  shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"
   1.384 +  by (rule borel_measurable_continuous_Pair[OF f g])
   1.385 +     (auto intro!: continuous_on_scaleR continuous_on_fst continuous_on_snd)
   1.386 +
   1.387  lemma affine_borel_measurable_vector:
   1.388    fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
   1.389    assumes "f \<in> borel_measurable M"
   1.390 @@ -825,13 +761,15 @@
   1.391    qed simp
   1.392  qed
   1.393  
   1.394 -lemma affine_borel_measurable:
   1.395 -  fixes g :: "'a \<Rightarrow> real"
   1.396 -  assumes g: "g \<in> borel_measurable M"
   1.397 -  shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
   1.398 -  using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute)
   1.399 +lemma borel_measurable_const_scaleR[measurable (raw)]:
   1.400 +  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. b *\<^sub>R f x ::'a::real_normed_vector) \<in> borel_measurable M"
   1.401 +  using affine_borel_measurable_vector[of f M 0 b] by simp
   1.402  
   1.403 -lemma borel_measurable_setprod[simp, intro]:
   1.404 +lemma borel_measurable_const_add[measurable (raw)]:
   1.405 +  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. a + f x ::'a::real_normed_vector) \<in> borel_measurable M"
   1.406 +  using affine_borel_measurable_vector[of f M a 1] by simp
   1.407 +
   1.408 +lemma borel_measurable_setprod[simp, intro, measurable (raw)]:
   1.409    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
   1.410    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   1.411    shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
   1.412 @@ -840,7 +778,7 @@
   1.413    thus ?thesis using assms by induct auto
   1.414  qed simp
   1.415  
   1.416 -lemma borel_measurable_inverse[simp, intro]:
   1.417 +lemma borel_measurable_inverse[simp, intro, measurable (raw)]:
   1.418    fixes f :: "'a \<Rightarrow> real"
   1.419    assumes f: "f \<in> borel_measurable M"
   1.420    shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
   1.421 @@ -853,7 +791,7 @@
   1.422      done
   1.423  qed
   1.424  
   1.425 -lemma borel_measurable_divide[simp, intro]:
   1.426 +lemma borel_measurable_divide[simp, intro, measurable (raw)]:
   1.427    fixes f :: "'a \<Rightarrow> real"
   1.428    assumes "f \<in> borel_measurable M"
   1.429    and "g \<in> borel_measurable M"
   1.430 @@ -861,21 +799,21 @@
   1.431    unfolding field_divide_inverse
   1.432    by (rule borel_measurable_inverse borel_measurable_times assms)+
   1.433  
   1.434 -lemma borel_measurable_max[intro, simp]:
   1.435 +lemma borel_measurable_max[intro, simp, measurable (raw)]:
   1.436    fixes f g :: "'a \<Rightarrow> real"
   1.437    assumes "f \<in> borel_measurable M"
   1.438    assumes "g \<in> borel_measurable M"
   1.439    shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
   1.440    unfolding max_def by (auto intro!: assms measurable_If)
   1.441  
   1.442 -lemma borel_measurable_min[intro, simp]:
   1.443 +lemma borel_measurable_min[intro, simp, measurable (raw)]:
   1.444    fixes f g :: "'a \<Rightarrow> real"
   1.445    assumes "f \<in> borel_measurable M"
   1.446    assumes "g \<in> borel_measurable M"
   1.447    shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
   1.448    unfolding min_def by (auto intro!: assms measurable_If)
   1.449  
   1.450 -lemma borel_measurable_abs[simp, intro]:
   1.451 +lemma borel_measurable_abs[simp, intro, measurable (raw)]:
   1.452    assumes "f \<in> borel_measurable M"
   1.453    shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
   1.454  proof -
   1.455 @@ -883,7 +821,7 @@
   1.456    show ?thesis unfolding * using assms by auto
   1.457  qed
   1.458  
   1.459 -lemma borel_measurable_nth[simp, intro]:
   1.460 +lemma borel_measurable_nth[simp, intro, measurable (raw)]:
   1.461    "(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel"
   1.462    using borel_measurable_euclidean_component'
   1.463    unfolding nth_conv_component by auto
   1.464 @@ -900,12 +838,12 @@
   1.465      from this q show "continuous_on {a<..<b} q"
   1.466        by (rule convex_on_continuous)
   1.467    qed
   1.468 -  moreover have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M"
   1.469 +  also have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M"
   1.470      using X by (intro measurable_cong) auto
   1.471 -  ultimately show ?thesis by simp
   1.472 +  finally show ?thesis .
   1.473  qed
   1.474  
   1.475 -lemma borel_measurable_ln[simp,intro]:
   1.476 +lemma borel_measurable_ln[simp, intro, measurable (raw)]:
   1.477    assumes f: "f \<in> borel_measurable M"
   1.478    shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
   1.479  proof -
   1.480 @@ -926,39 +864,55 @@
   1.481    finally show ?thesis .
   1.482  qed
   1.483  
   1.484 -lemma borel_measurable_log[simp,intro]:
   1.485 -  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log b (f x)) \<in> borel_measurable M"
   1.486 +lemma borel_measurable_log[simp, intro, measurable (raw)]:
   1.487 +  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"
   1.488    unfolding log_def by auto
   1.489  
   1.490 -lemma borel_measurable_real_floor:
   1.491 -  "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
   1.492 -  unfolding borel_measurable_iff_ge
   1.493 -proof (intro allI)
   1.494 -  fix a :: real
   1.495 -  { fix x have "a \<le> real \<lfloor>x\<rfloor> \<longleftrightarrow> real \<lceil>a\<rceil> \<le> x"
   1.496 -      using le_floor_eq[of "\<lceil>a\<rceil>" x] ceiling_le_iff[of a "\<lfloor>x\<rfloor>"]
   1.497 -      unfolding real_eq_of_int by simp }
   1.498 -  then have "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} = {real \<lceil>a\<rceil>..}" by auto
   1.499 -  then show "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} \<in> sets borel" by auto
   1.500 +lemma measurable_count_space_eq2_countable:
   1.501 +  fixes f :: "'a => 'c::countable"
   1.502 +  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
   1.503 +proof -
   1.504 +  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
   1.505 +    then have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)"
   1.506 +      by auto
   1.507 +    moreover assume "\<And>a. a\<in>A \<Longrightarrow> f -` {a} \<inter> space M \<in> sets M"
   1.508 +    ultimately have "f -` X \<inter> space M \<in> sets M"
   1.509 +      using `X \<subseteq> A` by (simp add: subset_eq del: UN_simps) }
   1.510 +  then show ?thesis
   1.511 +    unfolding measurable_def by auto
   1.512  qed
   1.513  
   1.514 -lemma borel_measurable_real_natfloor[intro, simp]:
   1.515 -  assumes "f \<in> borel_measurable M"
   1.516 -  shows "(\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
   1.517 +lemma measurable_real_floor[measurable]:
   1.518 +  "(floor :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
   1.519  proof -
   1.520 -  have "\<And>x. real (natfloor (f x)) = max 0 (real \<lfloor>f x\<rfloor>)"
   1.521 -    by (auto simp: max_def natfloor_def)
   1.522 -  with borel_measurable_max[OF measurable_comp[OF assms borel_measurable_real_floor] borel_measurable_const]
   1.523 -  show ?thesis by (simp add: comp_def)
   1.524 +  have "\<And>a x. \<lfloor>x\<rfloor> = a \<longleftrightarrow> (real a \<le> x \<and> x < real (a + 1))"
   1.525 +    by (auto intro: floor_eq2)
   1.526 +  then show ?thesis
   1.527 +    by (auto simp: vimage_def measurable_count_space_eq2_countable)
   1.528  qed
   1.529  
   1.530 +lemma measurable_real_natfloor[measurable]:
   1.531 +  "(natfloor :: real \<Rightarrow> nat) \<in> measurable borel (count_space UNIV)"
   1.532 +  by (simp add: natfloor_def[abs_def])
   1.533 +
   1.534 +lemma measurable_real_ceiling[measurable]:
   1.535 +  "(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
   1.536 +  unfolding ceiling_def[abs_def] by simp
   1.537 +
   1.538 +lemma borel_measurable_real_floor: "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
   1.539 +  by simp
   1.540 +
   1.541 +lemma borel_measurable_real_natfloor[intro, simp]:
   1.542 +  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
   1.543 +  by simp
   1.544 +
   1.545  subsection "Borel space on the extended reals"
   1.546  
   1.547 -lemma borel_measurable_ereal[simp, intro]:
   1.548 +lemma borel_measurable_ereal[simp, intro, measurable (raw)]:
   1.549    assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
   1.550    using continuous_on_ereal f by (rule borel_measurable_continuous_on)
   1.551  
   1.552 -lemma borel_measurable_real_of_ereal[simp, intro]:
   1.553 +lemma borel_measurable_real_of_ereal[simp, intro, measurable (raw)]:
   1.554    fixes f :: "'a \<Rightarrow> ereal" 
   1.555    assumes f: "f \<in> borel_measurable M"
   1.556    shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
   1.557 @@ -977,20 +931,16 @@
   1.558    assumes H: "(\<lambda>x. H (ereal (real (f x)))) \<in> borel_measurable M"
   1.559    shows "(\<lambda>x. H (f x)) \<in> borel_measurable M"
   1.560  proof -
   1.561 -  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)))"
   1.562 +  let ?F = "\<lambda>x. if f x = \<infinity> then H \<infinity> else if f x = - \<infinity> then H (-\<infinity>) else H (ereal (real (f x)))"
   1.563    { fix x have "H (f x) = ?F x" by (cases "f x") auto }
   1.564 -  moreover 
   1.565 -  have "?F \<in> borel_measurable M"
   1.566 -    by (intro measurable_If_set f measurable_sets[OF f] H) auto
   1.567 -  ultimately
   1.568 -  show ?thesis by simp
   1.569 +  with f H show ?thesis by simp
   1.570  qed
   1.571  
   1.572  lemma
   1.573    fixes f :: "'a \<Rightarrow> ereal" assumes f[simp]: "f \<in> borel_measurable M"
   1.574 -  shows borel_measurable_ereal_abs[intro, simp]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
   1.575 -    and borel_measurable_ereal_inverse[simp, intro]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
   1.576 -    and borel_measurable_uminus_ereal[intro]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
   1.577 +  shows borel_measurable_ereal_abs[intro, simp, measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
   1.578 +    and borel_measurable_ereal_inverse[simp, intro, measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
   1.579 +    and borel_measurable_uminus_ereal[intro, measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
   1.580    by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
   1.581  
   1.582  lemma borel_measurable_uminus_eq_ereal[simp]:
   1.583 @@ -999,44 +949,32 @@
   1.584    assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
   1.585  qed auto
   1.586  
   1.587 -lemma sets_Collect_If_set:
   1.588 -  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"
   1.589 -  shows "{x \<in> space M. if x \<in> A then P x else Q x} \<in> sets M"
   1.590 -proof -
   1.591 -  have *: "{x \<in> space M. if x \<in> A then P x else Q x} = 
   1.592 -    {x \<in> space M. if x \<in> A \<inter> space M then P x else Q x}" by auto
   1.593 -  show ?thesis unfolding * unfolding if_bool_eq_conj using assms
   1.594 -    by (auto intro!: sets_Collect simp: Int_def conj_commute)
   1.595 -qed
   1.596 -
   1.597  lemma set_Collect_ereal2:
   1.598    fixes f g :: "'a \<Rightarrow> ereal" 
   1.599    assumes f: "f \<in> borel_measurable M"
   1.600    assumes g: "g \<in> borel_measurable M"
   1.601    assumes H: "{x \<in> space M. H (ereal (real (f x))) (ereal (real (g x)))} \<in> sets M"
   1.602 -    "{x \<in> space M. H (-\<infinity>) (ereal (real (g x)))} \<in> sets M"
   1.603 -    "{x \<in> space M. H (\<infinity>) (ereal (real (g x)))} \<in> sets M"
   1.604 -    "{x \<in> space M. H (ereal (real (f x))) (-\<infinity>)} \<in> sets M"
   1.605 -    "{x \<in> space M. H (ereal (real (f x))) (\<infinity>)} \<in> sets M"
   1.606 +    "{x \<in> space borel. H (-\<infinity>) (ereal x)} \<in> sets borel"
   1.607 +    "{x \<in> space borel. H (\<infinity>) (ereal x)} \<in> sets borel"
   1.608 +    "{x \<in> space borel. H (ereal x) (-\<infinity>)} \<in> sets borel"
   1.609 +    "{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel"
   1.610    shows "{x \<in> space M. H (f x) (g x)} \<in> sets M"
   1.611  proof -
   1.612 -  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)))"
   1.613 -  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"
   1.614 +  let ?G = "\<lambda>y x. if g x = \<infinity> then H y \<infinity> else if g x = -\<infinity> then H y (-\<infinity>) else H y (ereal (real (g x)))"
   1.615 +  let ?F = "\<lambda>x. if f x = \<infinity> then ?G \<infinity> x else if f x = -\<infinity> then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
   1.616    { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
   1.617 -  moreover 
   1.618 -  have "{x \<in> space M. ?F x} \<in> sets M"
   1.619 -    by (intro sets_Collect H measurable_sets[OF f] measurable_sets[OF g] sets_Collect_If_set) auto
   1.620 -  ultimately
   1.621 -  show ?thesis by simp
   1.622 +  note * = this
   1.623 +  from assms show ?thesis
   1.624 +    by (subst *) (simp del: space_borel split del: split_if)
   1.625  qed
   1.626  
   1.627  lemma
   1.628    fixes f g :: "'a \<Rightarrow> ereal"
   1.629    assumes f: "f \<in> borel_measurable M"
   1.630    assumes g: "g \<in> borel_measurable M"
   1.631 -  shows borel_measurable_ereal_le[intro,simp]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
   1.632 -    and borel_measurable_ereal_less[intro,simp]: "{x \<in> space M. f x < g x} \<in> sets M"
   1.633 -    and borel_measurable_ereal_eq[intro,simp]: "{w \<in> space M. f w = g w} \<in> sets M"
   1.634 +  shows borel_measurable_ereal_le[intro,simp,measurable(raw)]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
   1.635 +    and borel_measurable_ereal_less[intro,simp,measurable(raw)]: "{x \<in> space M. f x < g x} \<in> sets M"
   1.636 +    and borel_measurable_ereal_eq[intro,simp,measurable(raw)]: "{w \<in> space M. f w = g w} \<in> sets M"
   1.637      and borel_measurable_ereal_neq[intro,simp]: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
   1.638    using f g by (auto simp: f g set_Collect_ereal2[OF f g] intro!: sets_Collect_neg)
   1.639  
   1.640 @@ -1060,7 +998,7 @@
   1.641    have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto
   1.642    also have "?f = f" by (auto simp: fun_eq_iff ereal_real)
   1.643    finally show "f \<in> borel_measurable M" .
   1.644 -qed (auto intro: measurable_sets borel_measurable_real_of_ereal)
   1.645 +qed simp_all
   1.646  
   1.647  lemma borel_measurable_eq_atMost_ereal:
   1.648    fixes f :: "'a \<Rightarrow> ereal"
   1.649 @@ -1080,7 +1018,8 @@
   1.650        qed }
   1.651      then have "f -` {\<infinity>} \<inter> space M = space M - (\<Union>i::nat. f -` {.. real i} \<inter> space M)"
   1.652        by (auto simp: not_le)
   1.653 -    then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos by (auto simp del: UN_simps intro!: Diff)
   1.654 +    then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos
   1.655 +      by (auto simp del: UN_simps)
   1.656      moreover
   1.657      have "{-\<infinity>::ereal} = {..-\<infinity>}" by auto
   1.658      then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto
   1.659 @@ -1150,14 +1089,11 @@
   1.660      "(\<lambda>x. H (ereal (real (f x))) (\<infinity>)) \<in> borel_measurable M"
   1.661    shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
   1.662  proof -
   1.663 -  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)))"
   1.664 -  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"
   1.665 +  let ?G = "\<lambda>y x. if g x = \<infinity> then H y \<infinity> else if g x = - \<infinity> then H y (-\<infinity>) else H y (ereal (real (g x)))"
   1.666 +  let ?F = "\<lambda>x. if f x = \<infinity> then ?G \<infinity> x else if f x = - \<infinity> then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
   1.667    { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
   1.668 -  moreover 
   1.669 -  have "?F \<in> borel_measurable M"
   1.670 -    by (intro measurable_If_set measurable_sets[OF f] measurable_sets[OF g] H) auto
   1.671 -  ultimately
   1.672 -  show ?thesis by simp
   1.673 +  note * = this
   1.674 +  from assms show ?thesis unfolding * by simp
   1.675  qed
   1.676  
   1.677  lemma
   1.678 @@ -1166,29 +1102,24 @@
   1.679      and borel_measurable_ereal_neq_const: "{x\<in>space M. f x \<noteq> c} \<in> sets M"
   1.680    using f by auto
   1.681  
   1.682 -lemma split_sets:
   1.683 -  "{x\<in>space M. P x \<or> Q x} = {x\<in>space M. P x} \<union> {x\<in>space M. Q x}"
   1.684 -  "{x\<in>space M. P x \<and> Q x} = {x\<in>space M. P x} \<inter> {x\<in>space M. Q x}"
   1.685 -  by auto
   1.686 -
   1.687 -lemma
   1.688 +lemma [intro, simp, measurable(raw)]:
   1.689    fixes f :: "'a \<Rightarrow> ereal"
   1.690    assumes [simp]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   1.691 -  shows borel_measurable_ereal_add[intro, simp]: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
   1.692 -    and borel_measurable_ereal_times[intro, simp]: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
   1.693 -    and borel_measurable_ereal_min[simp, intro]: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
   1.694 -    and borel_measurable_ereal_max[simp, intro]: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
   1.695 +  shows borel_measurable_ereal_add: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
   1.696 +    and borel_measurable_ereal_times: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
   1.697 +    and borel_measurable_ereal_min: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
   1.698 +    and borel_measurable_ereal_max: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
   1.699    by (auto simp add: borel_measurable_ereal2 measurable_If min_def max_def)
   1.700  
   1.701 -lemma
   1.702 +lemma [simp, intro, measurable(raw)]:
   1.703    fixes f g :: "'a \<Rightarrow> ereal"
   1.704    assumes "f \<in> borel_measurable M"
   1.705    assumes "g \<in> borel_measurable M"
   1.706 -  shows borel_measurable_ereal_diff[simp, intro]: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   1.707 -    and borel_measurable_ereal_divide[simp, intro]: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
   1.708 +  shows borel_measurable_ereal_diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   1.709 +    and borel_measurable_ereal_divide: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
   1.710    unfolding minus_ereal_def divide_ereal_def using assms by auto
   1.711  
   1.712 -lemma borel_measurable_ereal_setsum[simp, intro]:
   1.713 +lemma borel_measurable_ereal_setsum[simp, intro,measurable (raw)]:
   1.714    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   1.715    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   1.716    shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
   1.717 @@ -1198,7 +1129,7 @@
   1.718      by induct auto
   1.719  qed simp
   1.720  
   1.721 -lemma borel_measurable_ereal_setprod[simp, intro]:
   1.722 +lemma borel_measurable_ereal_setprod[simp, intro,measurable (raw)]:
   1.723    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   1.724    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   1.725    shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
   1.726 @@ -1207,7 +1138,7 @@
   1.727    thus ?thesis using assms by induct auto
   1.728  qed simp
   1.729  
   1.730 -lemma borel_measurable_SUP[simp, intro]:
   1.731 +lemma borel_measurable_SUP[simp, intro,measurable (raw)]:
   1.732    fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
   1.733    assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   1.734    shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
   1.735 @@ -1220,7 +1151,7 @@
   1.736      using assms by auto
   1.737  qed
   1.738  
   1.739 -lemma borel_measurable_INF[simp, intro]:
   1.740 +lemma borel_measurable_INF[simp, intro,measurable (raw)]:
   1.741    fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
   1.742    assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   1.743    shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
   1.744 @@ -1233,11 +1164,11 @@
   1.745      using assms by auto
   1.746  qed
   1.747  
   1.748 -lemma
   1.749 +lemma [simp, intro, measurable (raw)]:
   1.750    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   1.751    assumes "\<And>i. f i \<in> borel_measurable M"
   1.752 -  shows borel_measurable_liminf[simp, intro]: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
   1.753 -    and borel_measurable_limsup[simp, intro]: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
   1.754 +  shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
   1.755 +    and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
   1.756    unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
   1.757  
   1.758  lemma borel_measurable_ereal_LIMSEQ:
   1.759 @@ -1251,7 +1182,7 @@
   1.760    then show ?thesis by (simp add: u cong: measurable_cong)
   1.761  qed
   1.762  
   1.763 -lemma borel_measurable_psuminf[simp, intro]:
   1.764 +lemma borel_measurable_psuminf[simp, intro, measurable (raw)]:
   1.765    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   1.766    assumes "\<And>i. f i \<in> borel_measurable M" and pos: "\<And>i x. x \<in> space M \<Longrightarrow> 0 \<le> f i x"
   1.767    shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
   1.768 @@ -1275,38 +1206,38 @@
   1.769    ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff)
   1.770  qed
   1.771  
   1.772 -lemma sets_Collect_Cauchy: 
   1.773 +lemma sets_Collect_Cauchy[measurable]: 
   1.774    fixes f :: "nat \<Rightarrow> 'a => real"
   1.775 -  assumes f: "\<And>i. f i \<in> borel_measurable M"
   1.776 +  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   1.777    shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
   1.778 -  unfolding Cauchy_iff2 using f by (auto intro!: sets_Collect)
   1.779 +  unfolding Cauchy_iff2 using f by auto
   1.780  
   1.781 -lemma borel_measurable_lim:
   1.782 +lemma borel_measurable_lim[measurable (raw)]:
   1.783    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
   1.784 -  assumes f: "\<And>i. f i \<in> borel_measurable M"
   1.785 +  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   1.786    shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
   1.787  proof -
   1.788 -  have *: "\<And>x. lim (\<lambda>i. f i x) =
   1.789 -    (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))"
   1.790 +  def u' \<equiv> "\<lambda>x. lim (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
   1.791 +  then have *: "\<And>x. lim (\<lambda>i. f i x) = (if Cauchy (\<lambda>i. f i x) then u' x else (THE x. False))"
   1.792      by (auto simp: lim_def convergent_eq_cauchy[symmetric])
   1.793 -  { fix x have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
   1.794 +  have "u' \<in> borel_measurable M"
   1.795 +  proof (rule borel_measurable_LIMSEQ)
   1.796 +    fix x
   1.797 +    have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
   1.798        by (cases "Cauchy (\<lambda>i. f i x)")
   1.799 -         (auto simp add: convergent_eq_cauchy[symmetric] convergent_def) }
   1.800 -  note convergent = this
   1.801 -  show ?thesis
   1.802 -    unfolding *
   1.803 -    apply (intro measurable_If sets_Collect_Cauchy f borel_measurable_const)
   1.804 -    apply (rule borel_measurable_LIMSEQ)
   1.805 -    apply (rule convergent_LIMSEQ_iff[THEN iffD1, OF convergent])
   1.806 -    apply (intro measurable_If sets_Collect_Cauchy f borel_measurable_const)
   1.807 -    done
   1.808 +         (auto simp add: convergent_eq_cauchy[symmetric] convergent_def)
   1.809 +    then show "(\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) ----> u' x"
   1.810 +      unfolding u'_def 
   1.811 +      by (rule convergent_LIMSEQ_iff[THEN iffD1])
   1.812 +  qed measurable
   1.813 +  then show ?thesis
   1.814 +    unfolding * by measurable
   1.815  qed
   1.816  
   1.817 -lemma borel_measurable_suminf:
   1.818 +lemma borel_measurable_suminf[measurable (raw)]:
   1.819    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
   1.820 -  assumes f: "\<And>i. f i \<in> borel_measurable M"
   1.821 +  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   1.822    shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
   1.823 -  unfolding suminf_def sums_def[abs_def] lim_def[symmetric]
   1.824 -  by (simp add: f borel_measurable_lim)
   1.825 +  unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
   1.826  
   1.827  end