New theory Probability/Borel.thy, and some associated lemmas
authorpaulson
Mon Nov 09 15:50:15 2009 +0000 (2009-11-09)
changeset 3353340b44cb20c8c
parent 33530 535789c26230
child 33534 b21c820dfb63
New theory Probability/Borel.thy, and some associated lemmas
src/HOL/IsaMakefile
src/HOL/Probability/Borel.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Set.thy
     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.4 +header {*Borel Sets*}
     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.183 +         (simp add: borel_measurable_le_iff)
   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