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
```