use continuity to show Borel-measurability
authorhoelzl
Wed Oct 10 12:12:16 2012 +0200 (2012-10-10)
changeset 49774dfa8ddb874ce
parent 49773 16907431e477
child 49775 970964690b3d
use continuity to show Borel-measurability
src/HOL/Probability/Borel_Space.thy
     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.126 +lemma borel_measurable_add[simp, intro]:
   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.181 -lemma borel_measurable_add[simp, intro]:
   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.639  qed (simp add: measurable_sets)
   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.762 -lemma borel_measurable_ereal_add[intro, simp]:
   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.798 -qed (simp add: borel_measurable_const)
   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