author hoelzl Wed Oct 10 12:12:16 2012 +0200 (2012-10-10) changeset 49774 dfa8ddb874ce parent 49773 16907431e477 child 49775 970964690b3d
use continuity to show Borel-measurability
```     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Oct 10 12:12:15 2012 +0200
1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Oct 10 12:12:16 2012 +0200
1.3 @@ -632,7 +632,7 @@
1.4    "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
1.5    using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
1.6
1.7 -lemma borel_measurable_euclidean_component:
1.8 +lemma borel_measurable_euclidean_component':
1.9    "(\<lambda>x::'a::euclidean_space. x \$\$ i) \<in> borel_measurable borel"
1.10  proof (rule borel_measurableI)
1.11    fix S::"real set" assume "open S"
1.12 @@ -641,13 +641,18 @@
1.13      by (auto intro: borel_open)
1.14  qed
1.15
1.16 +lemma borel_measurable_euclidean_component:
1.17 +  fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
1.18 +  assumes f: "f \<in> borel_measurable M"
1.19 +  shows "(\<lambda>x. f x \$\$ i) \<in> borel_measurable M"
1.20 +  using measurable_comp[OF f borel_measurable_euclidean_component'] by (simp add: comp_def)
1.21 +
1.22  lemma borel_measurable_euclidean_space:
1.23    fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
1.24    shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x \$\$ i) \<in> borel_measurable M)"
1.25  proof safe
1.26    fix i assume "f \<in> borel_measurable M"
1.27    then show "(\<lambda>x. f x \$\$ i) \<in> borel_measurable M"
1.28 -    using measurable_comp[of f _ _ "\<lambda>x. x \$\$ i", unfolded comp_def]
1.29      by (auto intro: borel_measurable_euclidean_component)
1.30  next
1.31    assume f: "\<forall>i<DIM('c). (\<lambda>x. f x \$\$ i) \<in> borel_measurable M"
1.32 @@ -657,6 +662,144 @@
1.33
1.34  subsection "Borel measurable operators"
1.35
1.36 +lemma borel_measurable_continuous_on1:
1.37 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
1.38 +  assumes "continuous_on UNIV f"
1.39 +  shows "f \<in> borel_measurable borel"
1.40 +  apply(rule borel_measurableI)
1.41 +  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
1.42 +
1.43 +lemma borel_measurable_continuous_on:
1.44 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
1.45 +  assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
1.46 +  shows "(\<lambda>x. f (g x)) \<in> borel_measurable M"
1.47 +  using measurable_comp[OF g borel_measurable_continuous_on1[OF f]] by (simp add: comp_def)
1.48 +
1.49 +lemma borel_measurable_continuous_on_open':
1.50 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
1.51 +  assumes cont: "continuous_on A f" "open A"
1.52 +  shows "(\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel" (is "?f \<in> _")
1.53 +proof (rule borel_measurableI)
1.54 +  fix S :: "'b set" assume "open S"
1.55 +  then have "open {x\<in>A. f x \<in> S}"
1.56 +    by (intro continuous_open_preimage[OF cont]) auto
1.57 +  then have *: "{x\<in>A. f x \<in> S} \<in> sets borel" by auto
1.58 +  have "?f -` S \<inter> space borel =
1.59 +    {x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel - A else {})"
1.60 +    by (auto split: split_if_asm)
1.61 +  also have "\<dots> \<in> sets borel"
1.62 +    using * `open A` by (auto simp del: space_borel intro!: Un)
1.63 +  finally show "?f -` S \<inter> space borel \<in> sets borel" .
1.64 +qed
1.65 +
1.66 +lemma borel_measurable_continuous_on_open:
1.67 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
1.68 +  assumes cont: "continuous_on A f" "open A"
1.69 +  assumes g: "g \<in> borel_measurable M"
1.70 +  shows "(\<lambda>x. if g x \<in> A then f (g x) else c) \<in> borel_measurable M"
1.71 +  using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
1.72 +  by (simp add: comp_def)
1.73 +
1.74 +lemma borel_measurable_uminus[simp, intro]:
1.75 +  fixes g :: "'a \<Rightarrow> real"
1.76 +  assumes g: "g \<in> borel_measurable M"
1.77 +  shows "(\<lambda>x. - g x) \<in> borel_measurable M"
1.78 +  by (rule borel_measurable_continuous_on[OF _ g]) (auto intro: continuous_on_minus continuous_on_id)
1.79 +
1.80 +lemma euclidean_component_prod:
1.81 +  fixes x :: "'a :: euclidean_space \<times> 'b :: euclidean_space"
1.82 +  shows "x \$\$ i = (if i < DIM('a) then fst x \$\$ i else snd x \$\$ (i - DIM('a)))"
1.83 +  unfolding euclidean_component_def basis_prod_def inner_prod_def by auto
1.84 +
1.85 +lemma borel_measurable_Pair[simp, intro]:
1.86 +  fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
1.87 +  assumes f: "f \<in> borel_measurable M"
1.88 +  assumes g: "g \<in> borel_measurable M"
1.89 +  shows "(\<lambda>x. (f x, g x)) \<in> borel_measurable M"
1.90 +proof (intro borel_measurable_iff_halfspace_le[THEN iffD2] allI impI)
1.91 +  fix i and a :: real assume i: "i < DIM('b \<times> 'c)"
1.92 +  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.93 +    {w. A w \<and> (P \<longrightarrow> B w) \<and> (\<not> P \<longrightarrow> C w)}" by auto
1.94 +  from i f g show "{w \<in> space M. (f w, g w) \$\$ i \<le> a} \<in> sets M"
1.95 +    by (auto simp: euclidean_component_prod intro!: sets_Collect borel_measurable_euclidean_component)
1.96 +qed
1.97 +
1.98 +lemma continuous_on_fst: "continuous_on UNIV fst"
1.99 +proof -
1.100 +  have [simp]: "range fst = UNIV" by (auto simp: image_iff)
1.101 +  show ?thesis
1.102 +    using closed_vimage_fst
1.103 +    by (auto simp: continuous_on_closed closed_closedin vimage_def)
1.104 +qed
1.105 +
1.106 +lemma continuous_on_snd: "continuous_on UNIV snd"
1.107 +proof -
1.108 +  have [simp]: "range snd = UNIV" by (auto simp: image_iff)
1.109 +  show ?thesis
1.110 +    using closed_vimage_snd
1.111 +    by (auto simp: continuous_on_closed closed_closedin vimage_def)
1.112 +qed
1.113 +
1.114 +lemma borel_measurable_continuous_Pair:
1.115 +  fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
1.116 +  assumes [simp]: "f \<in> borel_measurable M"
1.117 +  assumes [simp]: "g \<in> borel_measurable M"
1.118 +  assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
1.119 +  shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
1.120 +proof -
1.121 +  have eq: "(\<lambda>x. H (f x) (g x)) = (\<lambda>x. (\<lambda>x. H (fst x) (snd x)) (f x, g x))" by auto
1.122 +  show ?thesis
1.123 +    unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
1.124 +qed
1.125 +
1.127 +  fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
1.128 +  assumes f: "f \<in> borel_measurable M"
1.129 +  assumes g: "g \<in> borel_measurable M"
1.130 +  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
1.131 +  using f g
1.132 +  by (rule borel_measurable_continuous_Pair)
1.133 +     (auto intro: continuous_on_fst continuous_on_snd continuous_on_add)
1.134 +
1.135 +lemma borel_measurable_setsum[simp, intro]:
1.136 +  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
1.137 +  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
1.138 +  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
1.139 +proof cases
1.140 +  assume "finite S"
1.141 +  thus ?thesis using assms by induct auto
1.142 +qed simp
1.143 +
1.144 +lemma borel_measurable_diff[simp, intro]:
1.145 +  fixes f :: "'a \<Rightarrow> real"
1.146 +  assumes f: "f \<in> borel_measurable M"
1.147 +  assumes g: "g \<in> borel_measurable M"
1.148 +  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
1.149 +  unfolding diff_minus using assms by fast
1.150 +
1.151 +lemma borel_measurable_times[simp, intro]:
1.152 +  fixes f :: "'a \<Rightarrow> real"
1.153 +  assumes f: "f \<in> borel_measurable M"
1.154 +  assumes g: "g \<in> borel_measurable M"
1.155 +  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
1.156 +  using f g
1.157 +  by (rule borel_measurable_continuous_Pair)
1.158 +     (auto intro: continuous_on_fst continuous_on_snd continuous_on_mult)
1.159 +
1.160 +lemma continuous_on_dist:
1.161 +  fixes f :: "'a :: t2_space \<Rightarrow> 'b :: metric_space"
1.162 +  shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. dist (f x) (g x))"
1.163 +  unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist)
1.164 +
1.165 +lemma borel_measurable_dist[simp, intro]:
1.166 +  fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
1.167 +  assumes f: "f \<in> borel_measurable M"
1.168 +  assumes g: "g \<in> borel_measurable M"
1.169 +  shows "(\<lambda>x. dist (f x) (g x)) \<in> borel_measurable M"
1.170 +  using f g
1.171 +  by (rule borel_measurable_continuous_Pair)
1.172 +     (intro continuous_on_dist continuous_on_fst continuous_on_snd)
1.173 +
1.174  lemma affine_borel_measurable_vector:
1.175    fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
1.176    assumes "f \<in> borel_measurable M"
1.177 @@ -683,116 +826,6 @@
1.178    shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
1.179    using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute)
1.180
1.182 -  fixes f :: "'a \<Rightarrow> real"
1.183 -  assumes f: "f \<in> borel_measurable M"
1.184 -  assumes g: "g \<in> borel_measurable M"
1.185 -  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
1.186 -proof -
1.187 -  have 1: "\<And>a. {w\<in>space M. a \<le> f w + g w} = {w \<in> space M. a + g w * -1 \<le> f w}"
1.188 -    by auto
1.189 -  have "\<And>a. (\<lambda>w. a + (g w) * -1) \<in> borel_measurable M"
1.190 -    by (rule affine_borel_measurable [OF g])
1.191 -  then have "\<And>a. {w \<in> space M. (\<lambda>w. a + (g w) * -1)(w) \<le> f w} \<in> sets M" using f
1.192 -    by auto
1.193 -  then have "\<And>a. {w \<in> space M. a \<le> f w + g w} \<in> sets M"
1.194 -    by (simp add: 1)
1.195 -  then show ?thesis
1.196 -    by (simp add: borel_measurable_iff_ge)
1.197 -qed
1.198 -
1.199 -lemma borel_measurable_setsum[simp, intro]:
1.200 -  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
1.201 -  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
1.202 -  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
1.203 -proof cases
1.204 -  assume "finite S"
1.205 -  thus ?thesis using assms by induct auto
1.206 -qed simp
1.207 -
1.208 -lemma borel_measurable_square:
1.209 -  fixes f :: "'a \<Rightarrow> real"
1.210 -  assumes f: "f \<in> borel_measurable M"
1.211 -  shows "(\<lambda>x. (f x)^2) \<in> borel_measurable M"
1.212 -proof -
1.213 -  {
1.214 -    fix a
1.215 -    have "{w \<in> space M. (f w)\<twosuperior> \<le> a} \<in> sets M"
1.216 -    proof (cases rule: linorder_cases [of a 0])
1.217 -      case less
1.218 -      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = {}"
1.219 -        by auto (metis less order_le_less_trans power2_less_0)
1.220 -      also have "... \<in> sets M"
1.221 -        by (rule empty_sets)
1.222 -      finally show ?thesis .
1.223 -    next
1.224 -      case equal
1.225 -      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
1.226 -             {w \<in> space M. f w \<le> 0} \<inter> {w \<in> space M. 0 \<le> f w}"
1.227 -        by auto
1.228 -      also have "... \<in> sets M"
1.229 -        apply (insert f)
1.230 -        apply (rule Int)
1.231 -        apply (simp add: borel_measurable_iff_le)
1.232 -        apply (simp add: borel_measurable_iff_ge)
1.233 -        done
1.234 -      finally show ?thesis .
1.235 -    next
1.236 -      case greater
1.237 -      have "\<forall>x. (f x ^ 2 \<le> sqrt a ^ 2) = (- sqrt a  \<le> f x & f x \<le> sqrt a)"
1.238 -        by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs
1.239 -                  real_sqrt_le_iff real_sqrt_power)
1.240 -      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
1.241 -             {w \<in> space M. -(sqrt a) \<le> f w} \<inter> {w \<in> space M. f w \<le> sqrt a}"
1.242 -        using greater by auto
1.243 -      also have "... \<in> sets M"
1.244 -        apply (insert f)
1.245 -        apply (rule Int)
1.246 -        apply (simp add: borel_measurable_iff_ge)
1.247 -        apply (simp add: borel_measurable_iff_le)
1.248 -        done
1.249 -      finally show ?thesis .
1.250 -    qed
1.251 -  }
1.252 -  thus ?thesis by (auto simp add: borel_measurable_iff_le)
1.253 -qed
1.254 -
1.255 -lemma times_eq_sum_squares:
1.256 -   fixes x::real
1.257 -   shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4"
1.258 -by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric])
1.259 -
1.260 -lemma borel_measurable_uminus[simp, intro]:
1.261 -  fixes g :: "'a \<Rightarrow> real"
1.262 -  assumes g: "g \<in> borel_measurable M"
1.263 -  shows "(\<lambda>x. - g x) \<in> borel_measurable M"
1.264 -proof -
1.265 -  have "(\<lambda>x. - g x) = (\<lambda>x. 0 + (g x) * -1)"
1.266 -    by simp
1.267 -  also have "... \<in> borel_measurable M"
1.268 -    by (fast intro: affine_borel_measurable g)
1.269 -  finally show ?thesis .
1.270 -qed
1.271 -
1.272 -lemma borel_measurable_times[simp, intro]:
1.273 -  fixes f :: "'a \<Rightarrow> real"
1.274 -  assumes f: "f \<in> borel_measurable M"
1.275 -  assumes g: "g \<in> borel_measurable M"
1.276 -  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
1.277 -proof -
1.278 -  have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M"
1.279 -    using assms by (fast intro: affine_borel_measurable borel_measurable_square)
1.280 -  have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) =
1.281 -        (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
1.282 -    by (simp add: minus_divide_right)
1.283 -  also have "... \<in> borel_measurable M"
1.284 -    using f g by (fast intro: affine_borel_measurable borel_measurable_square f g)
1.285 -  finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
1.286 -  show ?thesis
1.287 -    apply (simp add: times_eq_sum_squares diff_minus)
1.288 -    using 1 2 by simp
1.289 -qed
1.290 -
1.291  lemma borel_measurable_setprod[simp, intro]:
1.292    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
1.293    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
1.294 @@ -802,26 +835,17 @@
1.295    thus ?thesis using assms by induct auto
1.296  qed simp
1.297
1.298 -lemma borel_measurable_diff[simp, intro]:
1.299 -  fixes f :: "'a \<Rightarrow> real"
1.300 -  assumes f: "f \<in> borel_measurable M"
1.301 -  assumes g: "g \<in> borel_measurable M"
1.302 -  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
1.303 -  unfolding diff_minus using assms by fast
1.304 -
1.305  lemma borel_measurable_inverse[simp, intro]:
1.306    fixes f :: "'a \<Rightarrow> real"
1.307 -  assumes "f \<in> borel_measurable M"
1.308 +  assumes f: "f \<in> borel_measurable M"
1.309    shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
1.310 -  unfolding borel_measurable_iff_ge unfolding inverse_eq_divide
1.311 -proof safe
1.312 -  fix a :: real
1.313 -  have *: "{w \<in> space M. a \<le> 1 / f w} =
1.314 -      ({w \<in> space M. 0 < f w} \<inter> {w \<in> space M. a * f w \<le> 1}) \<union>
1.315 -      ({w \<in> space M. f w < 0} \<inter> {w \<in> space M. 1 \<le> a * f w}) \<union>
1.316 -      ({w \<in> space M. f w = 0} \<inter> {w \<in> space M. a \<le> 0})" by (auto simp: le_divide_eq)
1.317 -  show "{w \<in> space M. a \<le> 1 / f w} \<in> sets M" using assms unfolding *
1.318 -    by (auto intro!: Int Un)
1.319 +proof -
1.320 +  have *: "\<And>x::real. inverse x = (if x \<in> UNIV - {0} then inverse x else 0)" by auto
1.321 +  show ?thesis
1.322 +    apply (subst *)
1.323 +    apply (rule borel_measurable_continuous_on_open)
1.324 +    apply (auto intro!: f continuous_on_inverse continuous_on_id)
1.325 +    done
1.326  qed
1.327
1.328  lemma borel_measurable_divide[simp, intro]:
1.329 @@ -837,30 +861,14 @@
1.330    assumes "f \<in> borel_measurable M"
1.331    assumes "g \<in> borel_measurable M"
1.332    shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
1.333 -  unfolding borel_measurable_iff_le
1.334 -proof safe
1.335 -  fix a
1.336 -  have "{x \<in> space M. max (g x) (f x) \<le> a} =
1.337 -    {x \<in> space M. g x \<le> a} \<inter> {x \<in> space M. f x \<le> a}" by auto
1.338 -  thus "{x \<in> space M. max (g x) (f x) \<le> a} \<in> sets M"
1.339 -    using assms unfolding borel_measurable_iff_le
1.340 -    by (auto intro!: Int)
1.341 -qed
1.342 +  unfolding max_def by (auto intro!: assms measurable_If)
1.343
1.344  lemma borel_measurable_min[intro, simp]:
1.345    fixes f g :: "'a \<Rightarrow> real"
1.346    assumes "f \<in> borel_measurable M"
1.347    assumes "g \<in> borel_measurable M"
1.348    shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
1.349 -  unfolding borel_measurable_iff_ge
1.350 -proof safe
1.351 -  fix a
1.352 -  have "{x \<in> space M. a \<le> min (g x) (f x)} =
1.353 -    {x \<in> space M. a \<le> g x} \<inter> {x \<in> space M. a \<le> f x}" by auto
1.354 -  thus "{x \<in> space M. a \<le> min (g x) (f x)} \<in> sets M"
1.355 -    using assms unfolding borel_measurable_iff_ge
1.356 -    by (auto intro!: Int)
1.357 -qed
1.358 +  unfolding min_def by (auto intro!: assms measurable_If)
1.359
1.360  lemma borel_measurable_abs[simp, intro]:
1.361    assumes "f \<in> borel_measurable M"
1.362 @@ -872,76 +880,50 @@
1.363
1.364  lemma borel_measurable_nth[simp, intro]:
1.365    "(\<lambda>x::real^'n. x \$ i) \<in> borel_measurable borel"
1.366 -  using borel_measurable_euclidean_component
1.367 +  using borel_measurable_euclidean_component'
1.368    unfolding nth_conv_component by auto
1.369
1.370 -lemma borel_measurable_continuous_on1:
1.371 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
1.372 -  assumes "continuous_on UNIV f"
1.373 -  shows "f \<in> borel_measurable borel"
1.374 -  apply(rule borel_measurableI)
1.375 -  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
1.376 -
1.377 -lemma borel_measurable_continuous_on:
1.378 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
1.379 -  assumes cont: "continuous_on A f" "open A"
1.380 -  shows "(\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel" (is "?f \<in> _")
1.381 -proof (rule borel_measurableI)
1.382 -  fix S :: "'b set" assume "open S"
1.383 -  then have "open {x\<in>A. f x \<in> S}"
1.384 -    by (intro continuous_open_preimage[OF cont]) auto
1.385 -  then have *: "{x\<in>A. f x \<in> S} \<in> sets borel" by auto
1.386 -  have "?f -` S \<inter> space borel =
1.387 -    {x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel - A else {})"
1.388 -    by (auto split: split_if_asm)
1.389 -  also have "\<dots> \<in> sets borel"
1.390 -    using * `open A` by (auto simp del: space_borel intro!: Un)
1.391 -  finally show "?f -` S \<inter> space borel \<in> sets borel" .
1.392 -qed
1.393 -
1.394  lemma convex_measurable:
1.395    fixes a b :: real
1.396    assumes X: "X \<in> borel_measurable M" "X ` space M \<subseteq> { a <..< b}"
1.397    assumes q: "convex_on { a <..< b} q"
1.398 -  shows "q \<circ> X \<in> borel_measurable M"
1.399 +  shows "(\<lambda>x. q (X x)) \<in> borel_measurable M"
1.400  proof -
1.401 -  have "(\<lambda>x. if x \<in> {a <..< b} then q x else 0) \<in> borel_measurable borel"
1.402 -  proof (rule borel_measurable_continuous_on)
1.403 +  have "(\<lambda>x. if X x \<in> {a <..< b} then q (X x) else 0) \<in> borel_measurable M" (is "?qX")
1.404 +  proof (rule borel_measurable_continuous_on_open[OF _ _ X(1)])
1.405      show "open {a<..<b}" by auto
1.406      from this q show "continuous_on {a<..<b} q"
1.407        by (rule convex_on_continuous)
1.408    qed
1.409 -  then have "(\<lambda>x. if x \<in> {a <..< b} then q x else 0) \<circ> X \<in> borel_measurable M" (is ?qX)
1.410 -    using X by (intro measurable_comp) auto
1.411 -  moreover have "?qX \<longleftrightarrow> q \<circ> X \<in> borel_measurable M"
1.412 +  moreover have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M"
1.413      using X by (intro measurable_cong) auto
1.414    ultimately show ?thesis by simp
1.415  qed
1.416
1.417 -lemma borel_measurable_borel_log: assumes "1 < b" shows "log b \<in> borel_measurable borel"
1.418 +lemma borel_measurable_ln[simp,intro]:
1.419 +  assumes f: "f \<in> borel_measurable M"
1.420 +  shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
1.421  proof -
1.422    { fix x :: real assume x: "x \<le> 0"
1.423      { fix x::real assume "x \<le> 0" then have "\<And>u. exp u = x \<longleftrightarrow> False" by auto }
1.424 -    from this[of x] x this[of 0] have "log b 0 = log b x"
1.425 -      by (auto simp: ln_def log_def) }
1.426 -  note log_imp = this
1.427 -  have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) \<in> borel_measurable borel"
1.428 -  proof (rule borel_measurable_continuous_on)
1.429 -    show "continuous_on {0<..} (log b)"
1.430 -      by (auto intro!: continuous_at_imp_continuous_on DERIV_log DERIV_isCont
1.431 +    from this[of x] x this[of 0] have "ln 0 = ln x"
1.432 +      by (auto simp: ln_def) }
1.433 +  note ln_imp = this
1.434 +  have "(\<lambda>x. if f x \<in> {0<..} then ln (f x) else ln 0) \<in> borel_measurable M"
1.435 +  proof (rule borel_measurable_continuous_on_open[OF _ _ f])
1.436 +    show "continuous_on {0<..} ln"
1.437 +      by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont
1.438                 simp: continuous_isCont[symmetric])
1.439      show "open ({0<..}::real set)" by auto
1.440    qed
1.441 -  also have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) = log b"
1.442 -    by (simp add: fun_eq_iff not_less log_imp)
1.443 +  also have "(\<lambda>x. if x \<in> {0<..} then ln x else ln 0) = ln"
1.444 +    by (simp add: fun_eq_iff not_less ln_imp)
1.445    finally show ?thesis .
1.446  qed
1.447
1.448  lemma borel_measurable_log[simp,intro]:
1.449 -  assumes f: "f \<in> borel_measurable M" and "1 < b"
1.450 -  shows "(\<lambda>x. log b (f x)) \<in> borel_measurable M"
1.451 -  using measurable_comp[OF f borel_measurable_borel_log[OF `1 < b`]]
1.452 -  by (simp add: comp_def)
1.453 +  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log b (f x)) \<in> borel_measurable M"
1.454 +  unfolding log_def by auto
1.455
1.456  lemma borel_measurable_real_floor:
1.457    "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
1.458 @@ -967,45 +949,91 @@
1.459
1.460  subsection "Borel space on the extended reals"
1.461
1.462 -lemma borel_measurable_ereal_borel:
1.463 -  "ereal \<in> borel_measurable borel"
1.464 -proof (rule borel_measurableI)
1.465 -  fix X :: "ereal set" assume "open X"
1.466 -  then have "open (ereal -` X \<inter> space borel)"
1.467 -    by (simp add: open_ereal_vimage)
1.468 -  then show "ereal -` X \<inter> space borel \<in> sets borel" by auto
1.469 -qed
1.470 -
1.471  lemma borel_measurable_ereal[simp, intro]:
1.472    assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
1.473 -  using measurable_comp[OF f borel_measurable_ereal_borel] unfolding comp_def .
1.474 +  using continuous_on_ereal f by (rule borel_measurable_continuous_on)
1.475
1.476 -lemma borel_measurable_real_of_ereal_borel:
1.477 -  "(real :: ereal \<Rightarrow> real) \<in> borel_measurable borel"
1.478 -proof (rule borel_measurableI)
1.479 -  fix B :: "real set" assume "open B"
1.480 -  have *: "ereal -` real -` (B - {0}) = B - {0}" by auto
1.481 -  have open_real: "open (real -` (B - {0}) :: ereal set)"
1.482 -    unfolding open_ereal_def * using `open B` by auto
1.483 -  show "(real -` B \<inter> space borel :: ereal set) \<in> sets borel"
1.484 -  proof cases
1.485 -    assume "0 \<in> B"
1.486 -    then have *: "real -` B = real -` (B - {0}) \<union> {-\<infinity>, \<infinity>, 0::ereal}"
1.487 -      by (auto simp add: real_of_ereal_eq_0)
1.488 -    then show "(real -` B :: ereal set) \<inter> space borel \<in> sets borel"
1.489 -      using open_real by auto
1.490 -  next
1.491 -    assume "0 \<notin> B"
1.492 -    then have *: "(real -` B :: ereal set) = real -` (B - {0})"
1.493 -      by (auto simp add: real_of_ereal_eq_0)
1.494 -    then show "(real -` B :: ereal set) \<inter> space borel \<in> sets borel"
1.495 -      using open_real by auto
1.496 -  qed
1.497 +lemma borel_measurable_real_of_ereal[simp, intro]:
1.498 +  fixes f :: "'a \<Rightarrow> ereal"
1.499 +  assumes f: "f \<in> borel_measurable M"
1.500 +  shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
1.501 +proof -
1.502 +  have "(\<lambda>x. if f x \<in> UNIV - { \<infinity>, - \<infinity> } then real (f x) else 0) \<in> borel_measurable M"
1.503 +    using continuous_on_real
1.504 +    by (rule borel_measurable_continuous_on_open[OF _ _ f]) auto
1.505 +  also have "(\<lambda>x. if f x \<in> UNIV - { \<infinity>, - \<infinity> } then real (f x) else 0) = (\<lambda>x. real (f x))"
1.506 +    by auto
1.507 +  finally show ?thesis .
1.508 +qed
1.509 +
1.510 +lemma borel_measurable_ereal_cases:
1.511 +  fixes f :: "'a \<Rightarrow> ereal"
1.512 +  assumes f: "f \<in> borel_measurable M"
1.513 +  assumes H: "(\<lambda>x. H (ereal (real (f x)))) \<in> borel_measurable M"
1.514 +  shows "(\<lambda>x. H (f x)) \<in> borel_measurable M"
1.515 +proof -
1.516 +  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.517 +  { fix x have "H (f x) = ?F x" by (cases "f x") auto }
1.518 +  moreover
1.519 +  have "?F \<in> borel_measurable M"
1.520 +    by (intro measurable_If_set f measurable_sets[OF f] H) auto
1.521 +  ultimately
1.522 +  show ?thesis by simp
1.523  qed
1.524
1.525 -lemma borel_measurable_real_of_ereal[simp, intro]:
1.526 -  assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. real (f x :: ereal)) \<in> borel_measurable M"
1.527 -  using measurable_comp[OF f borel_measurable_real_of_ereal_borel] unfolding comp_def .
1.528 +lemma
1.529 +  fixes f :: "'a \<Rightarrow> ereal" assumes f[simp]: "f \<in> borel_measurable M"
1.530 +  shows borel_measurable_ereal_abs[intro, simp]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
1.531 +    and borel_measurable_ereal_inverse[simp, intro]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
1.532 +    and borel_measurable_uminus_ereal[intro]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
1.533 +  by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
1.534 +
1.535 +lemma borel_measurable_uminus_eq_ereal[simp]:
1.536 +  "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r")
1.537 +proof
1.538 +  assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
1.539 +qed auto
1.540 +
1.541 +lemma sets_Collect_If_set:
1.542 +  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.543 +  shows "{x \<in> space M. if x \<in> A then P x else Q x} \<in> sets M"
1.544 +proof -
1.545 +  have *: "{x \<in> space M. if x \<in> A then P x else Q x} =
1.546 +    {x \<in> space M. if x \<in> A \<inter> space M then P x else Q x}" by auto
1.547 +  show ?thesis unfolding * unfolding if_bool_eq_conj using assms
1.548 +    by (auto intro!: sets_Collect simp: Int_def conj_commute)
1.549 +qed
1.550 +
1.551 +lemma set_Collect_ereal2:
1.552 +  fixes f g :: "'a \<Rightarrow> ereal"
1.553 +  assumes f: "f \<in> borel_measurable M"
1.554 +  assumes g: "g \<in> borel_measurable M"
1.555 +  assumes H: "{x \<in> space M. H (ereal (real (f x))) (ereal (real (g x)))} \<in> sets M"
1.556 +    "{x \<in> space M. H (-\<infinity>) (ereal (real (g x)))} \<in> sets M"
1.557 +    "{x \<in> space M. H (\<infinity>) (ereal (real (g x)))} \<in> sets M"
1.558 +    "{x \<in> space M. H (ereal (real (f x))) (-\<infinity>)} \<in> sets M"
1.559 +    "{x \<in> space M. H (ereal (real (f x))) (\<infinity>)} \<in> sets M"
1.560 +  shows "{x \<in> space M. H (f x) (g x)} \<in> sets M"
1.561 +proof -
1.562 +  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.563 +  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.564 +  { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
1.565 +  moreover
1.566 +  have "{x \<in> space M. ?F x} \<in> sets M"
1.567 +    by (intro sets_Collect H measurable_sets[OF f] measurable_sets[OF g] sets_Collect_If_set) auto
1.568 +  ultimately
1.569 +  show ?thesis by simp
1.570 +qed
1.571 +
1.572 +lemma
1.573 +  fixes f g :: "'a \<Rightarrow> ereal"
1.574 +  assumes f: "f \<in> borel_measurable M"
1.575 +  assumes g: "g \<in> borel_measurable M"
1.576 +  shows borel_measurable_ereal_le[intro,simp]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
1.577 +    and borel_measurable_ereal_less[intro,simp]: "{x \<in> space M. f x < g x} \<in> sets M"
1.578 +    and borel_measurable_ereal_eq[intro,simp]: "{w \<in> space M. f w = g w} \<in> sets M"
1.579 +    and borel_measurable_ereal_neq[intro,simp]: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
1.580 +  using f g by (auto simp: f g set_Collect_ereal2[OF f g] intro!: sets_Collect_neg)
1.581
1.582  lemma borel_measurable_ereal_iff:
1.583    shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
1.584 @@ -1029,52 +1057,6 @@
1.585    finally show "f \<in> borel_measurable M" .
1.586  qed (auto intro: measurable_sets borel_measurable_real_of_ereal)
1.587
1.588 -lemma less_eq_ge_measurable:
1.589 -  fixes f :: "'a \<Rightarrow> 'c::linorder"
1.590 -  shows "f -` {a <..} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {..a} \<inter> space M \<in> sets M"
1.591 -proof
1.592 -  assume "f -` {a <..} \<inter> space M \<in> sets M"
1.593 -  moreover have "f -` {..a} \<inter> space M = space M - f -` {a <..} \<inter> space M" by auto
1.594 -  ultimately show "f -` {..a} \<inter> space M \<in> sets M" by auto
1.595 -next
1.596 -  assume "f -` {..a} \<inter> space M \<in> sets M"
1.597 -  moreover have "f -` {a <..} \<inter> space M = space M - f -` {..a} \<inter> space M" by auto
1.598 -  ultimately show "f -` {a <..} \<inter> space M \<in> sets M" by auto
1.599 -qed
1.600 -
1.601 -lemma greater_eq_le_measurable:
1.602 -  fixes f :: "'a \<Rightarrow> 'c::linorder"
1.603 -  shows "f -` {..< a} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {a ..} \<inter> space M \<in> sets M"
1.604 -proof
1.605 -  assume "f -` {a ..} \<inter> space M \<in> sets M"
1.606 -  moreover have "f -` {..< a} \<inter> space M = space M - f -` {a ..} \<inter> space M" by auto
1.607 -  ultimately show "f -` {..< a} \<inter> space M \<in> sets M" by auto
1.608 -next
1.609 -  assume "f -` {..< a} \<inter> space M \<in> sets M"
1.610 -  moreover have "f -` {a ..} \<inter> space M = space M - f -` {..< a} \<inter> space M" by auto
1.611 -  ultimately show "f -` {a ..} \<inter> space M \<in> sets M" by auto
1.612 -qed
1.613 -
1.614 -lemma borel_measurable_uminus_borel_ereal:
1.615 -  "(uminus :: ereal \<Rightarrow> ereal) \<in> borel_measurable borel"
1.616 -proof (rule borel_measurableI)
1.617 -  fix X :: "ereal set" assume "open X"
1.618 -  have "uminus -` X = uminus ` X" by (force simp: image_iff)
1.619 -  then have "open (uminus -` X)" using `open X` ereal_open_uminus by auto
1.620 -  then show "uminus -` X \<inter> space borel \<in> sets borel" by auto
1.621 -qed
1.622 -
1.623 -lemma borel_measurable_uminus_ereal[intro]:
1.624 -  assumes "f \<in> borel_measurable M"
1.625 -  shows "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
1.626 -  using measurable_comp[OF assms borel_measurable_uminus_borel_ereal] by (simp add: comp_def)
1.627 -
1.628 -lemma borel_measurable_uminus_eq_ereal[simp]:
1.629 -  "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r")
1.630 -proof
1.631 -  assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
1.632 -qed auto
1.633 -
1.634  lemma borel_measurable_eq_atMost_ereal:
1.635    fixes f :: "'a \<Rightarrow> ereal"
1.636    shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
1.637 @@ -1118,94 +1100,88 @@
1.638    then show "f \<in> borel_measurable M" by simp
1.640
1.641 +lemma greater_eq_le_measurable:
1.642 +  fixes f :: "'a \<Rightarrow> 'c::linorder"
1.643 +  shows "f -` {..< a} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {a ..} \<inter> space M \<in> sets M"
1.644 +proof
1.645 +  assume "f -` {a ..} \<inter> space M \<in> sets M"
1.646 +  moreover have "f -` {..< a} \<inter> space M = space M - f -` {a ..} \<inter> space M" by auto
1.647 +  ultimately show "f -` {..< a} \<inter> space M \<in> sets M" by auto
1.648 +next
1.649 +  assume "f -` {..< a} \<inter> space M \<in> sets M"
1.650 +  moreover have "f -` {a ..} \<inter> space M = space M - f -` {..< a} \<inter> space M" by auto
1.651 +  ultimately show "f -` {a ..} \<inter> space M \<in> sets M" by auto
1.652 +qed
1.653 +
1.654  lemma borel_measurable_ereal_iff_less:
1.655    "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..< a} \<inter> space M \<in> sets M)"
1.656    unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable ..
1.657
1.658 +lemma less_eq_ge_measurable:
1.659 +  fixes f :: "'a \<Rightarrow> 'c::linorder"
1.660 +  shows "f -` {a <..} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {..a} \<inter> space M \<in> sets M"
1.661 +proof
1.662 +  assume "f -` {a <..} \<inter> space M \<in> sets M"
1.663 +  moreover have "f -` {..a} \<inter> space M = space M - f -` {a <..} \<inter> space M" by auto
1.664 +  ultimately show "f -` {..a} \<inter> space M \<in> sets M" by auto
1.665 +next
1.666 +  assume "f -` {..a} \<inter> space M \<in> sets M"
1.667 +  moreover have "f -` {a <..} \<inter> space M = space M - f -` {..a} \<inter> space M" by auto
1.668 +  ultimately show "f -` {a <..} \<inter> space M \<in> sets M" by auto
1.669 +qed
1.670 +
1.671  lemma borel_measurable_ereal_iff_ge:
1.672    "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a <..} \<inter> space M \<in> sets M)"
1.673    unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable ..
1.674
1.675 -lemma borel_measurable_ereal_eq_const:
1.676 -  fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M"
1.677 -  shows "{x\<in>space M. f x = c} \<in> sets M"
1.678 -proof -
1.679 -  have "{x\<in>space M. f x = c} = (f -` {c} \<inter> space M)" by auto
1.680 -  then show ?thesis using assms by (auto intro!: measurable_sets)
1.681 -qed
1.682 -
1.683 -lemma borel_measurable_ereal_neq_const:
1.684 -  fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M"
1.685 -  shows "{x\<in>space M. f x \<noteq> c} \<in> sets M"
1.686 -proof -
1.687 -  have "{x\<in>space M. f x \<noteq> c} = space M - (f -` {c} \<inter> space M)" by auto
1.688 -  then show ?thesis using assms by (auto intro!: measurable_sets)
1.689 -qed
1.690 -
1.691 -lemma borel_measurable_ereal_le[intro,simp]:
1.692 -  fixes f g :: "'a \<Rightarrow> ereal"
1.693 +lemma borel_measurable_ereal2:
1.694 +  fixes f g :: "'a \<Rightarrow> ereal"
1.695    assumes f: "f \<in> borel_measurable M"
1.696    assumes g: "g \<in> borel_measurable M"
1.697 -  shows "{x \<in> space M. f x \<le> g x} \<in> sets M"
1.698 +  assumes H: "(\<lambda>x. H (ereal (real (f x))) (ereal (real (g x)))) \<in> borel_measurable M"
1.699 +    "(\<lambda>x. H (-\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M"
1.700 +    "(\<lambda>x. H (\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M"
1.701 +    "(\<lambda>x. H (ereal (real (f x))) (-\<infinity>)) \<in> borel_measurable M"
1.702 +    "(\<lambda>x. H (ereal (real (f x))) (\<infinity>)) \<in> borel_measurable M"
1.703 +  shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
1.704  proof -
1.705 -  have "{x \<in> space M. f x \<le> g x} =
1.706 -    {x \<in> space M. real (f x) \<le> real (g x)} - (f -` {\<infinity>, -\<infinity>} \<inter> space M \<union> g -` {\<infinity>, -\<infinity>} \<inter> space M) \<union>
1.707 -    f -` {-\<infinity>} \<inter> space M \<union> g -` {\<infinity>} \<inter> space M" (is "?l = ?r")
1.708 -  proof (intro set_eqI)
1.709 -    fix x show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" by (cases rule: ereal2_cases[of "f x" "g x"]) auto
1.710 -  qed
1.711 -  with f g show ?thesis by (auto intro!: Un simp: measurable_sets)
1.712 +  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.713 +  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.714 +  { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
1.715 +  moreover
1.716 +  have "?F \<in> borel_measurable M"
1.717 +    by (intro measurable_If_set measurable_sets[OF f] measurable_sets[OF g] H) auto
1.718 +  ultimately
1.719 +  show ?thesis by simp
1.720  qed
1.721
1.722 -lemma borel_measurable_ereal_less[intro,simp]:
1.723 -  fixes f :: "'a \<Rightarrow> ereal"
1.724 -  assumes f: "f \<in> borel_measurable M"
1.725 -  assumes g: "g \<in> borel_measurable M"
1.726 -  shows "{x \<in> space M. f x < g x} \<in> sets M"
1.727 -proof -
1.728 -  have "{x \<in> space M. f x < g x} = space M - {x \<in> space M. g x \<le> f x}" by auto
1.729 -  then show ?thesis using g f by auto
1.730 -qed
1.731 -
1.732 -lemma borel_measurable_ereal_eq[intro,simp]:
1.733 -  fixes f :: "'a \<Rightarrow> ereal"
1.734 -  assumes f: "f \<in> borel_measurable M"
1.735 -  assumes g: "g \<in> borel_measurable M"
1.736 -  shows "{w \<in> space M. f w = g w} \<in> sets M"
1.737 -proof -
1.738 -  have "{x \<in> space M. f x = g x} = {x \<in> space M. g x \<le> f x} \<inter> {x \<in> space M. f x \<le> g x}" by auto
1.739 -  then show ?thesis using g f by auto
1.740 -qed
1.741 -
1.742 -lemma borel_measurable_ereal_neq[intro,simp]:
1.743 -  fixes f :: "'a \<Rightarrow> ereal"
1.744 -  assumes f: "f \<in> borel_measurable M"
1.745 -  assumes g: "g \<in> borel_measurable M"
1.746 -  shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
1.747 -proof -
1.748 -  have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}" by auto
1.749 -  thus ?thesis using f g by auto
1.750 -qed
1.751 +lemma
1.752 +  fixes f :: "'a \<Rightarrow> ereal" assumes f: "f \<in> borel_measurable M"
1.753 +  shows borel_measurable_ereal_eq_const: "{x\<in>space M. f x = c} \<in> sets M"
1.754 +    and borel_measurable_ereal_neq_const: "{x\<in>space M. f x \<noteq> c} \<in> sets M"
1.755 +  using f by auto
1.756
1.757  lemma split_sets:
1.758    "{x\<in>space M. P x \<or> Q x} = {x\<in>space M. P x} \<union> {x\<in>space M. Q x}"
1.759    "{x\<in>space M. P x \<and> Q x} = {x\<in>space M. P x} \<inter> {x\<in>space M. Q x}"
1.760    by auto
1.761
1.763 +lemma
1.764    fixes f :: "'a \<Rightarrow> ereal"
1.765 -  assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
1.766 -  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
1.767 -proof -
1.768 -  { fix x assume "x \<in> space M" then have "f x + g x =
1.769 -      (if f x = \<infinity> \<or> g x = \<infinity> then \<infinity>
1.770 -        else if f x = -\<infinity> \<or> g x = -\<infinity> then -\<infinity>
1.771 -        else ereal (real (f x) + real (g x)))"
1.772 -      by (cases rule: ereal2_cases[of "f x" "g x"]) auto }
1.773 -  with assms show ?thesis
1.774 -    by (auto cong: measurable_cong simp: split_sets
1.775 -             intro!: Un measurable_If measurable_sets)
1.776 -qed
1.777 +  assumes [simp]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
1.778 +  shows borel_measurable_ereal_add[intro, simp]: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
1.779 +    and borel_measurable_ereal_times[intro, simp]: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
1.780 +    and borel_measurable_ereal_min[simp, intro]: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
1.781 +    and borel_measurable_ereal_max[simp, intro]: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
1.782 +  by (auto simp add: borel_measurable_ereal2 measurable_If min_def max_def)
1.783 +
1.784 +lemma
1.785 +  fixes f g :: "'a \<Rightarrow> ereal"
1.786 +  assumes "f \<in> borel_measurable M"
1.787 +  assumes "g \<in> borel_measurable M"
1.788 +  shows borel_measurable_ereal_diff[simp, intro]: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
1.789 +    and borel_measurable_ereal_divide[simp, intro]: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
1.790 +  unfolding minus_ereal_def divide_ereal_def using assms by auto
1.791
1.792  lemma borel_measurable_ereal_setsum[simp, intro]:
1.793    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
1.794 @@ -1215,39 +1191,7 @@
1.795    assume "finite S"
1.796    thus ?thesis using assms
1.797      by induct auto
1.799 -
1.800 -lemma borel_measurable_ereal_abs[intro, simp]:
1.801 -  fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M"
1.802 -  shows "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
1.803 -proof -
1.804 -  { fix x have "\<bar>f x\<bar> = (if 0 \<le> f x then f x else - f x)" by auto }
1.805 -  then show ?thesis using assms by (auto intro!: measurable_If)
1.806 -qed
1.807 -
1.808 -lemma borel_measurable_ereal_times[intro, simp]:
1.809 -  fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
1.810 -  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
1.811 -proof -
1.812 -  { fix f g :: "'a \<Rightarrow> ereal"
1.813 -    assume b: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
1.814 -      and pos: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x"
1.815 -    { fix x have *: "f x * g x = (if f x = 0 \<or> g x = 0 then 0
1.816 -        else if f x = \<infinity> \<or> g x = \<infinity> then \<infinity>
1.817 -        else ereal (real (f x) * real (g x)))"
1.818 -      apply (cases rule: ereal2_cases[of "f x" "g x"])
1.819 -      using pos[of x] by auto }
1.820 -    with b have "(\<lambda>x. f x * g x) \<in> borel_measurable M"
1.821 -      by (auto cong: measurable_cong simp: split_sets
1.822 -               intro!: Un measurable_If measurable_sets) }
1.823 -  note pos_times = this
1.824 -  have *: "(\<lambda>x. f x * g x) =
1.825 -    (\<lambda>x. if 0 \<le> f x \<and> 0 \<le> g x \<or> f x < 0 \<and> g x < 0 then \<bar>f x\<bar> * \<bar>g x\<bar> else - (\<bar>f x\<bar> * \<bar>g x\<bar>))"
1.826 -    by (auto simp: fun_eq_iff)
1.827 -  show ?thesis using assms unfolding *
1.828 -    by (intro measurable_If pos_times borel_measurable_uminus_ereal)
1.829 -       (auto simp: split_sets intro!: Int)
1.830 -qed
1.831 +qed simp
1.832
1.833  lemma borel_measurable_ereal_setprod[simp, intro]:
1.834    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
1.835 @@ -1258,20 +1202,6 @@
1.836    thus ?thesis using assms by induct auto
1.837  qed simp
1.838
1.839 -lemma borel_measurable_ereal_min[simp, intro]:
1.840 -  fixes f g :: "'a \<Rightarrow> ereal"
1.841 -  assumes "f \<in> borel_measurable M"
1.842 -  assumes "g \<in> borel_measurable M"
1.843 -  shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
1.844 -  using assms unfolding min_def by (auto intro!: measurable_If)
1.845 -
1.846 -lemma borel_measurable_ereal_max[simp, intro]:
1.847 -  fixes f g :: "'a \<Rightarrow> ereal"
1.848 -  assumes "f \<in> borel_measurable M"
1.849 -  and "g \<in> borel_measurable M"
1.850 -  shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
1.851 -  using assms unfolding max_def by (auto intro!: measurable_If)
1.852 -
1.853  lemma borel_measurable_SUP[simp, intro]:
1.854    fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
1.855    assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
1.856 @@ -1298,38 +1228,24 @@
1.857      using assms by auto
1.858  qed
1.859
1.860 -lemma borel_measurable_liminf[simp, intro]:
1.861 -  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
1.862 -  assumes "\<And>i. f i \<in> borel_measurable M"
1.863 -  shows "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
1.864 -  unfolding liminf_SUPR_INFI using assms by auto
1.865 -
1.866 -lemma borel_measurable_limsup[simp, intro]:
1.867 +lemma
1.868    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
1.869    assumes "\<And>i. f i \<in> borel_measurable M"
1.870 -  shows "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
1.871 -  unfolding limsup_INFI_SUPR using assms by auto
1.872 -
1.873 -lemma borel_measurable_ereal_diff[simp, intro]:
1.874 -  fixes f g :: "'a \<Rightarrow> ereal"
1.875 -  assumes "f \<in> borel_measurable M"
1.876 -  assumes "g \<in> borel_measurable M"
1.877 -  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
1.878 -  unfolding minus_ereal_def using assms by auto
1.879 +  shows borel_measurable_liminf[simp, intro]: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
1.880 +    and borel_measurable_limsup[simp, intro]: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
1.881 +  unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
1.882
1.883 -lemma borel_measurable_ereal_inverse[simp, intro]:
1.884 -  assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
1.885 +lemma borel_measurable_ereal_LIMSEQ:
1.886 +  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
1.887 +  assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
1.888 +  and u: "\<And>i. u i \<in> borel_measurable M"
1.889 +  shows "u' \<in> borel_measurable M"
1.890  proof -
1.891 -  { fix x have "inverse (f x) = (if f x = 0 then \<infinity> else ereal (inverse (real (f x))))"
1.892 -      by (cases "f x") auto }
1.893 -  with f show ?thesis
1.894 -    by (auto intro!: measurable_If)
1.895 +  have "\<And>x. x \<in> space M \<Longrightarrow> u' x = liminf (\<lambda>n. u n x)"
1.896 +    using u' by (simp add: lim_imp_Liminf[symmetric])
1.897 +  then show ?thesis by (simp add: u cong: measurable_cong)
1.898  qed
1.899
1.900 -lemma borel_measurable_ereal_divide[simp, intro]:
1.901 -  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. f x / g x :: ereal) \<in> borel_measurable M"
1.902 -  unfolding divide_ereal_def by auto
1.903 -
1.904  lemma borel_measurable_psuminf[simp, intro]:
1.905    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
1.906    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.907 @@ -1354,4 +1270,38 @@
1.908    ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff)
1.909  qed
1.910
1.911 -end
1.912 +lemma sets_Collect_Cauchy:
1.913 +  fixes f :: "nat \<Rightarrow> 'a => real"
1.914 +  assumes f: "\<And>i. f i \<in> borel_measurable M"
1.915 +  shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
1.916 +  unfolding Cauchy_iff2 using f by (auto intro!: sets_Collect)
1.917 +
1.918 +lemma borel_measurable_lim:
1.919 +  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
1.920 +  assumes f: "\<And>i. f i \<in> borel_measurable M"
1.921 +  shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
1.922 +proof -
1.923 +  have *: "\<And>x. lim (\<lambda>i. f i x) =
1.924 +    (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.925 +    by (auto simp: lim_def convergent_eq_cauchy[symmetric])
1.926 +  { fix x have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
1.927 +      by (cases "Cauchy (\<lambda>i. f i x)")
1.928 +         (auto simp add: convergent_eq_cauchy[symmetric] convergent_def) }
1.929 +  note convergent = this
1.930 +  show ?thesis
1.931 +    unfolding *
1.932 +    apply (intro measurable_If sets_Collect_Cauchy f borel_measurable_const)
1.933 +    apply (rule borel_measurable_LIMSEQ)
1.934 +    apply (rule convergent_LIMSEQ_iff[THEN iffD1, OF convergent])
1.935 +    apply (intro measurable_If sets_Collect_Cauchy f borel_measurable_const)
1.936 +    done
1.937 +qed
1.938 +
1.939 +lemma borel_measurable_suminf:
1.940 +  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
1.941 +  assumes f: "\<And>i. f i \<in> borel_measurable M"
1.942 +  shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
1.943 +  unfolding suminf_def sums_def[abs_def] lim_def[symmetric]
1.944 +  by (simp add: f borel_measurable_lim)
1.945 +
1.946 +end
```