author paulson Mon Nov 09 15:50:15 2009 +0000 (2009-11-09) changeset 33533 40b44cb20c8c parent 33530 535789c26230 child 33534 b21c820dfb63
New theory Probability/Borel.thy, and some associated lemmas
 src/HOL/IsaMakefile file | annotate | diff | revisions src/HOL/Probability/Borel.thy file | annotate | diff | revisions src/HOL/Probability/Sigma_Algebra.thy file | annotate | diff | revisions src/HOL/Set.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/IsaMakefile	Mon Nov 09 11:34:22 2009 +0100
1.2 +++ b/src/HOL/IsaMakefile	Mon Nov 09 15:50:15 2009 +0000
1.3 @@ -1069,7 +1069,8 @@
1.4    Probability/Sigma_Algebra.thy \
1.5    Probability/SeriesPlus.thy \
1.6    Probability/Caratheodory.thy \
1.7 -  Probability/Measure.thy
1.8 +  Probability/Measure.thy \
1.9 +  Probability/Borel.thy
1.10  	@\$(ISABELLE_TOOL) usedir -g true \$(OUT)/HOL Probability
1.11
1.12
```
```     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Probability/Borel.thy	Mon Nov 09 15:50:15 2009 +0000
2.3 @@ -0,0 +1,425 @@
2.5 +
2.6 +theory Borel
2.7 +  imports Measure
2.8 +begin
2.9 +
2.10 +text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
2.11 +
2.12 +definition borel_space where
2.13 +  "borel_space = sigma (UNIV::real set) (range (\<lambda>a::real. {x. x \<le> a}))"
2.14 +
2.15 +definition borel_measurable where
2.16 +  "borel_measurable a = measurable a borel_space"
2.17 +
2.18 +definition indicator_fn where
2.19 +  "indicator_fn s = (\<lambda>x. if x \<in> s then 1 else (0::real))"
2.20 +
2.21 +definition mono_convergent where
2.22 +  "mono_convergent u f s \<equiv>
2.23 +	(\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
2.24 +	(\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
2.25 +
2.26 +lemma in_borel_measurable:
2.27 +   "f \<in> borel_measurable M \<longleftrightarrow>
2.28 +    sigma_algebra M \<and>
2.29 +    (\<forall>s \<in> sets (sigma UNIV (range (\<lambda>a::real. {x. x \<le> a}))).
2.30 +      f -` s \<inter> space M \<in> sets M)"
2.31 +apply (auto simp add: borel_measurable_def measurable_def borel_space_def)
2.32 +apply (metis PowD UNIV_I Un_commute sigma_algebra_sigma subset_Pow_Union subset_UNIV subset_Un_eq)
2.33 +done
2.34 +
2.35 +lemma (in sigma_algebra) borel_measurable_const:
2.36 +   "(\<lambda>x. c) \<in> borel_measurable M"
2.37 +  by (auto simp add: in_borel_measurable prems)
2.38 +
2.39 +lemma (in sigma_algebra) borel_measurable_indicator:
2.40 +  assumes a: "a \<in> sets M"
2.41 +  shows "indicator_fn a \<in> borel_measurable M"
2.42 +apply (auto simp add: in_borel_measurable indicator_fn_def prems)
2.43 +apply (metis Diff_eq Int_commute a compl_sets)
2.44 +done
2.45 +
2.46 +lemma Collect_eq: "{w \<in> X. f w \<le> a} = {w. f w \<le> a} \<inter> X"
2.47 +  by (metis Collect_conj_eq Collect_mem_eq Int_commute)
2.48 +
2.49 +lemma (in measure_space) borel_measurable_le_iff:
2.50 +   "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)"
2.51 +proof
2.52 +  assume f: "f \<in> borel_measurable M"
2.53 +  { fix a
2.54 +    have "{w \<in> space M. f w \<le> a} \<in> sets M" using f
2.55 +      apply (auto simp add: in_borel_measurable sigma_def Collect_eq)
2.56 +      apply (drule_tac x="{x. x \<le> a}" in bspec, auto)
2.57 +      apply (metis equalityE rangeI subsetD sigma_sets.Basic)
2.58 +      done
2.59 +    }
2.60 +  thus "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M" by blast
2.61 +next
2.62 +  assume "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M"
2.63 +  thus "f \<in> borel_measurable M"
2.64 +    apply (simp add: borel_measurable_def borel_space_def Collect_eq)
2.65 +    apply (rule measurable_sigma, auto)
2.66 +    done
2.67 +qed
2.68 +
2.69 +lemma Collect_less_le:
2.70 +     "{w \<in> X. f w < g w} = (\<Union>n. {w \<in> X. f w \<le> g w - inverse(real(Suc n))})"
2.71 +  proof auto
2.72 +    fix w
2.73 +    assume w: "f w < g w"
2.74 +    hence nz: "g w - f w \<noteq> 0"
2.75 +      by arith
2.76 +    with w have "real(Suc(natceiling(inverse(g w - f w)))) > inverse(g w - f w)"
2.77 +      by (metis lessI order_le_less_trans real_natceiling_ge real_of_nat_less_iff)       hence "inverse(real(Suc(natceiling(inverse(g w - f w)))))
2.78 +             < inverse(inverse(g w - f w))"
2.79 +      by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_ordered_idom nz positive_imp_inverse_positive real_le_anti_sym real_less_def w)
2.80 +    hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < g w - f w"
2.81 +      by (metis inverse_inverse_eq order_less_le_trans real_le_refl)
2.82 +    thus "\<exists>n. f w \<le> g w - inverse(real(Suc n))" using w
2.83 +      by (rule_tac x="natceiling(inverse(g w - f w))" in exI, auto)
2.84 +  next
2.85 +    fix w n
2.86 +    assume le: "f w \<le> g w - inverse(real(Suc n))"
2.87 +    hence "0 < inverse(real(Suc n))"
2.88 +      by (metis inverse_real_of_nat_gt_zero)
2.89 +    thus "f w < g w" using le
2.90 +      by arith
2.91 +  qed
2.92 +
2.93 +
2.94 +lemma (in sigma_algebra) sigma_le_less:
2.95 +  assumes M: "!!a::real. {w \<in> space M. f w \<le> a} \<in> sets M"
2.96 +  shows "{w \<in> space M. f w < a} \<in> sets M"
2.97 +proof -
2.98 +  show ?thesis using Collect_less_le [of "space M" f "\<lambda>x. a"]
2.99 +    by (auto simp add: countable_UN M)
2.100 +qed
2.101 +
2.102 +lemma (in sigma_algebra) sigma_less_ge:
2.103 +  assumes M: "!!a::real. {w \<in> space M. f w < a} \<in> sets M"
2.104 +  shows "{w \<in> space M. a \<le> f w} \<in> sets M"
2.105 +proof -
2.106 +  have "{w \<in> space M. a \<le> f w} = space M - {w \<in> space M. f w < a}"
2.107 +    by auto
2.108 +  thus ?thesis using M
2.109 +    by auto
2.110 +qed
2.111 +
2.112 +lemma (in sigma_algebra) sigma_ge_gr:
2.113 +  assumes M: "!!a::real. {w \<in> space M. a \<le> f w} \<in> sets M"
2.114 +  shows "{w \<in> space M. a < f w} \<in> sets M"
2.115 +proof -
2.116 +  show ?thesis using Collect_less_le [of "space M" "\<lambda>x. a" f]
2.117 +    by (auto simp add: countable_UN le_diff_eq M)
2.118 +qed
2.119 +
2.120 +lemma (in sigma_algebra) sigma_gr_le:
2.121 +  assumes M: "!!a::real. {w \<in> space M. a < f w} \<in> sets M"
2.122 +  shows "{w \<in> space M. f w \<le> a} \<in> sets M"
2.123 +proof -
2.124 +  have "{w \<in> space M. f w \<le> a} = space M - {w \<in> space M. a < f w}"
2.125 +    by auto
2.126 +  thus ?thesis
2.127 +    by (simp add: M compl_sets)
2.128 +qed
2.129 +
2.130 +lemma (in measure_space) borel_measurable_gr_iff:
2.131 +   "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
2.132 +proof (auto simp add: borel_measurable_le_iff sigma_gr_le)
2.133 +  fix u
2.134 +  assume M: "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M"
2.135 +  have "{w \<in> space M. u < f w} = space M - {w \<in> space M. f w \<le> u}"
2.136 +    by auto
2.137 +  thus "{w \<in> space M. u < f w} \<in> sets M"
2.138 +    by (force simp add: compl_sets countable_UN M)
2.139 +qed
2.140 +
2.141 +lemma (in measure_space) borel_measurable_less_iff:
2.142 +   "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)"
2.143 +proof (auto simp add: borel_measurable_le_iff sigma_le_less)
2.144 +  fix u
2.145 +  assume M: "\<forall>a. {w \<in> space M. f w < a} \<in> sets M"
2.146 +  have "{w \<in> space M. f w \<le> u} = space M - {w \<in> space M. u < f w}"
2.147 +    by auto
2.148 +  thus "{w \<in> space M. f w \<le> u} \<in> sets M"
2.149 +    using Collect_less_le [of "space M" "\<lambda>x. u" f]
2.150 +    by (force simp add: compl_sets countable_UN le_diff_eq sigma_less_ge M)
2.151 +qed
2.152 +
2.153 +lemma (in measure_space) borel_measurable_ge_iff:
2.154 +   "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)"
2.155 +proof (auto simp add: borel_measurable_less_iff sigma_le_less sigma_ge_gr sigma_gr_le)
2.156 +  fix u
2.157 +  assume M: "\<forall>a. {w \<in> space M. f w < a} \<in> sets M"
2.158 +  have "{w \<in> space M. u \<le> f w} = space M - {w \<in> space M. f w < u}"
2.159 +    by auto
2.160 +  thus "{w \<in> space M. u \<le> f w} \<in> sets M"
2.161 +    by (force simp add: compl_sets countable_UN M)
2.162 +qed
2.163 +
2.164 +lemma (in measure_space) affine_borel_measurable:
2.165 +  assumes g: "g \<in> borel_measurable M"
2.166 +  shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
2.167 +proof (cases rule: linorder_cases [of b 0])
2.168 +  case equal thus ?thesis
2.169 +    by (simp add: borel_measurable_const)
2.170 +next
2.171 +  case less
2.172 +    {
2.173 +      fix w c
2.174 +      have "a + g w * b \<le> c \<longleftrightarrow> g w * b \<le> c - a"
2.175 +        by auto
2.176 +      also have "... \<longleftrightarrow> (c-a)/b \<le> g w" using less
2.177 +        by (metis divide_le_eq less less_asym)
2.178 +      finally have "a + g w * b \<le> c \<longleftrightarrow> (c-a)/b \<le> g w" .
2.179 +    }
2.180 +    hence "\<And>w c. a + g w * b \<le> c \<longleftrightarrow> (c-a)/b \<le> g w" .
2.181 +    thus ?thesis using less g
2.182 +      by (simp add: borel_measurable_ge_iff [of g])
2.184 +next
2.185 +  case greater
2.186 +    hence 0: "\<And>x c. (g x * b \<le> c - a) \<longleftrightarrow> (g x \<le> (c - a) / b)"
2.187 +      by (metis mult_imp_le_div_pos le_divide_eq)
2.188 +    have 1: "\<And>x c. (a + g x * b \<le> c) \<longleftrightarrow> (g x * b \<le> c - a)"
2.189 +      by auto
2.190 +    from greater g
2.191 +    show ?thesis
2.192 +      by (simp add: borel_measurable_le_iff 0 1)
2.193 +qed
2.194 +
2.195 +definition
2.196 +  nat_to_rat_surj :: "nat \<Rightarrow> rat" where
2.197 + "nat_to_rat_surj n = (let (i,j) = nat_to_nat2 n
2.198 +                       in Fract (nat_to_int_bij i) (nat_to_int_bij j))"
2.199 +
2.200 +lemma nat_to_rat_surj: "surj nat_to_rat_surj"
2.201 +proof (auto simp add: surj_def nat_to_rat_surj_def)
2.202 +  fix y
2.203 +  show "\<exists>x. y = (\<lambda>(i, j). Fract (nat_to_int_bij i) (nat_to_int_bij j)) (nat_to_nat2 x)"
2.204 +  proof (cases y)
2.205 +    case (Fract a b)
2.206 +      obtain i where i: "nat_to_int_bij i = a" using surj_nat_to_int_bij
2.207 +        by (metis surj_def)
2.208 +      obtain j where j: "nat_to_int_bij j = b" using surj_nat_to_int_bij
2.209 +        by (metis surj_def)
2.210 +      obtain n where n: "nat_to_nat2 n = (i,j)" using nat_to_nat2_surj
2.211 +        by (metis surj_def)
2.212 +
2.213 +      from Fract i j n show ?thesis
2.214 +        by (metis prod.cases prod_case_split)
2.215 +  qed
2.216 +qed
2.217 +
2.218 +lemma rats_enumeration: "\<rat> = range (of_rat o nat_to_rat_surj)"
2.219 +  using nat_to_rat_surj
2.220 +  by (auto simp add: image_def surj_def) (metis Rats_cases)
2.221 +
2.222 +lemma (in measure_space) borel_measurable_less_borel_measurable:
2.223 +  assumes f: "f \<in> borel_measurable M"
2.224 +  assumes g: "g \<in> borel_measurable M"
2.225 +  shows "{w \<in> space M. f w < g w} \<in> sets M"
2.226 +proof -
2.227 +  have "{w \<in> space M. f w < g w} =
2.228 +	(\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
2.229 +    by (auto simp add: Rats_dense_in_real)
2.230 +  thus ?thesis using f g
2.231 +    by (simp add: borel_measurable_less_iff [of f]
2.232 +                  borel_measurable_gr_iff [of g])
2.233 +       (blast intro: gen_countable_UN [OF rats_enumeration])
2.234 +qed
2.235 +
2.236 +lemma (in measure_space) borel_measurable_leq_borel_measurable:
2.237 +  assumes f: "f \<in> borel_measurable M"
2.238 +  assumes g: "g \<in> borel_measurable M"
2.239 +  shows "{w \<in> space M. f w \<le> g w} \<in> sets M"
2.240 +proof -
2.241 +  have "{w \<in> space M. f w \<le> g w} = space M - {w \<in> space M. g w < f w}"
2.242 +    by auto
2.243 +  thus ?thesis using f g
2.244 +    by (simp add: borel_measurable_less_borel_measurable compl_sets)
2.245 +qed
2.246 +
2.247 +lemma (in measure_space) borel_measurable_eq_borel_measurable:
2.248 +  assumes f: "f \<in> borel_measurable M"
2.249 +  assumes g: "g \<in> borel_measurable M"
2.250 +  shows "{w \<in> space M. f w = g w} \<in> sets M"
2.251 +proof -
2.252 +  have "{w \<in> space M. f w = g w} =
2.253 +	{w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
2.254 +    by auto
2.255 +  thus ?thesis using f g
2.256 +    by (simp add: borel_measurable_leq_borel_measurable Int)
2.257 +qed
2.258 +
2.259 +lemma (in measure_space) borel_measurable_neq_borel_measurable:
2.260 +  assumes f: "f \<in> borel_measurable M"
2.261 +  assumes g: "g \<in> borel_measurable M"
2.262 +  shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
2.263 +proof -
2.264 +  have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}"
2.265 +    by auto
2.266 +  thus ?thesis using f g
2.267 +    by (simp add: borel_measurable_eq_borel_measurable compl_sets)
2.268 +qed
2.269 +
2.270 +lemma (in measure_space) borel_measurable_plus_borel_measurable:
2.271 +  assumes f: "f \<in> borel_measurable M"
2.272 +  assumes g: "g \<in> borel_measurable M"
2.273 +  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
2.274 +proof -
2.275 +  have 1:"!!a. {w \<in> space M. a \<le> f w + g w} = {w \<in> space M. a + (g w) * -1 \<le> f w}"
2.276 +    by auto
2.277 +  have "!!a. (\<lambda>w. a + (g w) * -1) \<in> borel_measurable M"
2.278 +    by (rule affine_borel_measurable [OF g])
2.279 +  hence "!!a. {w \<in> space M. (\<lambda>w. a + (g w) * -1)(w) \<le> f w} \<in> sets M" using f
2.280 +    by (rule borel_measurable_leq_borel_measurable)
2.281 +  hence "!!a. {w \<in> space M. a \<le> f w + g w} \<in> sets M"
2.282 +    by (simp add: 1)
2.283 +  thus ?thesis
2.284 +    by (simp add: borel_measurable_ge_iff)
2.285 +qed
2.286 +
2.287 +
2.288 +lemma (in measure_space) borel_measurable_square:
2.289 +  assumes f: "f \<in> borel_measurable M"
2.290 +  shows "(\<lambda>x. (f x)^2) \<in> borel_measurable M"
2.291 +proof -
2.292 +  {
2.293 +    fix a
2.294 +    have "{w \<in> space M. (f w)\<twosuperior> \<le> a} \<in> sets M"
2.295 +    proof (cases rule: linorder_cases [of a 0])
2.296 +      case less
2.297 +      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = {}"
2.298 +        by auto (metis less order_le_less_trans power2_less_0)
2.299 +      also have "... \<in> sets M"
2.300 +        by (rule empty_sets)
2.301 +      finally show ?thesis .
2.302 +    next
2.303 +      case equal
2.304 +      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
2.305 +             {w \<in> space M. f w \<le> 0} \<inter> {w \<in> space M. 0 \<le> f w}"
2.306 +        by auto
2.307 +      also have "... \<in> sets M"
2.308 +        apply (insert f)
2.309 +        apply (rule Int)
2.310 +        apply (simp add: borel_measurable_le_iff)
2.311 +        apply (simp add: borel_measurable_ge_iff)
2.312 +        done
2.313 +      finally show ?thesis .
2.314 +    next
2.315 +      case greater
2.316 +      have "\<forall>x. (f x ^ 2 \<le> sqrt a ^ 2) = (- sqrt a  \<le> f x & f x \<le> sqrt a)"
2.317 +        by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs
2.318 +                  real_sqrt_le_iff real_sqrt_power)
2.319 +      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
2.320 +             {w \<in> space M. -(sqrt a) \<le> f w} \<inter> {w \<in> space M. f w \<le> sqrt a}"
2.321 +        using greater by auto
2.322 +      also have "... \<in> sets M"
2.323 +        apply (insert f)
2.324 +        apply (rule Int)
2.325 +        apply (simp add: borel_measurable_ge_iff)
2.326 +        apply (simp add: borel_measurable_le_iff)
2.327 +        done
2.328 +      finally show ?thesis .
2.329 +    qed
2.330 +  }
2.331 +  thus ?thesis by (auto simp add: borel_measurable_le_iff)
2.332 +qed
2.333 +
2.334 +lemma times_eq_sum_squares:
2.335 +   fixes x::real
2.336 +   shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4"
2.337 +by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric])
2.338 +
2.339 +
2.340 +lemma (in measure_space) borel_measurable_uminus_borel_measurable:
2.341 +  assumes g: "g \<in> borel_measurable M"
2.342 +  shows "(\<lambda>x. - g x) \<in> borel_measurable M"
2.343 +proof -
2.344 +  have "(\<lambda>x. - g x) = (\<lambda>x. 0 + (g x) * -1)"
2.345 +    by simp
2.346 +  also have "... \<in> borel_measurable M"
2.347 +    by (fast intro: affine_borel_measurable g)
2.348 +  finally show ?thesis .
2.349 +qed
2.350 +
2.351 +lemma (in measure_space) borel_measurable_times_borel_measurable:
2.352 +  assumes f: "f \<in> borel_measurable M"
2.353 +  assumes g: "g \<in> borel_measurable M"
2.354 +  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
2.355 +proof -
2.356 +  have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M"
2.357 +    by (fast intro: affine_borel_measurable borel_measurable_square
2.358 +                    borel_measurable_plus_borel_measurable f g)
2.359 +  have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) =
2.360 +        (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
2.361 +    by (simp add: Ring_and_Field.minus_divide_right)
2.362 +  also have "... \<in> borel_measurable M"
2.363 +    by (fast intro: affine_borel_measurable borel_measurable_square
2.364 +                    borel_measurable_plus_borel_measurable
2.365 +                    borel_measurable_uminus_borel_measurable f g)
2.366 +  finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
2.367 +  show ?thesis
2.368 +    apply (simp add: times_eq_sum_squares real_diff_def)
2.369 +    using 1 2 apply (simp add: borel_measurable_plus_borel_measurable)
2.370 +    done
2.371 +qed
2.372 +
2.373 +lemma (in measure_space) borel_measurable_diff_borel_measurable:
2.374 +  assumes f: "f \<in> borel_measurable M"
2.375 +  assumes g: "g \<in> borel_measurable M"
2.376 +  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
2.377 +unfolding real_diff_def
2.378 +  by (fast intro: borel_measurable_plus_borel_measurable
2.379 +                  borel_measurable_uminus_borel_measurable f g)
2.380 +
2.381 +lemma (in measure_space) mono_convergent_borel_measurable:
2.382 +  assumes u: "!!n. u n \<in> borel_measurable M"
2.383 +  assumes mc: "mono_convergent u f (space M)"
2.384 +  shows "f \<in> borel_measurable M"
2.385 +proof -
2.386 +  {
2.387 +    fix a
2.388 +    have 1: "!!w. w \<in> space M & f w <= a \<longleftrightarrow> w \<in> space M & (\<forall>i. u i w <= a)"
2.389 +      proof safe
2.390 +        fix w i
2.391 +        assume w: "w \<in> space M" and f: "f w \<le> a"
2.392 +        hence "u i w \<le> f w"
2.393 +          by (auto intro: SEQ.incseq_le
2.394 +                   simp add: incseq_def mc [unfolded mono_convergent_def])
2.395 +        thus "u i w \<le> a" using f
2.396 +          by auto
2.397 +      next
2.398 +        fix w
2.399 +        assume w: "w \<in> space M" and u: "\<forall>i. u i w \<le> a"
2.400 +        thus "f w \<le> a"
2.401 +          by (metis LIMSEQ_le_const2 mc [unfolded mono_convergent_def])
2.402 +      qed
2.403 +    have "{w \<in> space M. f w \<le> a} = {w \<in> space M. (\<forall>i. u i w <= a)}"
2.404 +      by (simp add: 1)
2.405 +    also have "... = (\<Inter>i. {w \<in> space M. u i w \<le> a})"
2.406 +      by auto
2.407 +    also have "...  \<in> sets M" using u
2.408 +      by (auto simp add: borel_measurable_le_iff intro: countable_INT)
2.409 +    finally have "{w \<in> space M. f w \<le> a} \<in> sets M" .
2.410 +  }
2.411 +  thus ?thesis
2.412 +    by (auto simp add: borel_measurable_le_iff)
2.413 +qed
2.414 +
2.415 +lemma (in measure_space) borel_measurable_SIGMA_borel_measurable:
2.416 +  assumes s: "finite s"
2.417 +  shows "(!!i. i \<in> s ==> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) s) \<in> borel_measurable M" using s
2.418 +proof (induct s)
2.419 +  case empty
2.420 +  thus ?case
2.421 +    by (simp add: borel_measurable_const)
2.422 +next
2.423 +  case (insert x s)
2.424 +  thus ?case
2.425 +    by (auto simp add: borel_measurable_plus_borel_measurable)
2.426 +qed
2.427 +
2.428 +end
```
```     3.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 09 11:34:22 2009 +0100
3.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 09 15:50:15 2009 +0000
3.3 @@ -71,7 +71,7 @@
3.4    assumes countable_UN [intro]:
3.5           "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
3.6
3.7 -lemma (in sigma_algebra) countable_INT:
3.8 +lemma (in sigma_algebra) countable_INT [intro]:
3.9    assumes a: "range a \<subseteq> sets M"
3.10    shows "(\<Inter>i::nat. a i) \<in> sets M"
3.11  proof -
3.12 @@ -83,6 +83,15 @@
3.13    ultimately show ?thesis by metis
3.14  qed
3.15
3.16 +lemma (in sigma_algebra) gen_countable_UN:
3.17 +  fixes f :: "nat \<Rightarrow> 'c"
3.18 +  shows  "I = range f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> (\<Union>x\<in>I. A x) \<in> sets M"
3.19 +by auto
3.20 +
3.21 +lemma (in sigma_algebra) gen_countable_INT:
3.22 +  fixes f :: "nat \<Rightarrow> 'c"
3.23 +  shows  "I = range f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> (\<Inter>x\<in>I. A x) \<in> sets M"
3.24 +by auto
3.25
3.26  lemma algebra_Pow:
3.27       "algebra (| space = sp, sets = Pow sp |)"
```
```     4.1 --- a/src/HOL/Set.thy	Mon Nov 09 11:34:22 2009 +0100
4.2 +++ b/src/HOL/Set.thy	Mon Nov 09 15:50:15 2009 +0000
4.3 @@ -1645,6 +1645,14 @@
4.4  lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
4.5  by blast
4.6
4.7 +lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
4.8 +  by auto
4.9 +
4.10 +lemma vimage_if [simp]: "((\<lambda>x. if x \<in> B then c else d) -` A) =
4.11 +   (if c \<in> A then (if d \<in> A then UNIV else B)
4.12 +    else if d \<in> A then -B else {})"
4.13 +  by (auto simp add: vimage_def)
4.14 +
4.15  lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
4.16  by blast
4.17
```