src/HOL/Probability/Borel.thy
 author wenzelm Thu Feb 11 23:00:22 2010 +0100 (2010-02-11) changeset 35115 446c5063e4fd parent 35050 9f841f20dca6 child 35347 be0c69c06176 permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
```     1 header {*Borel Sets*}
```
```     2
```
```     3 theory Borel
```
```     4   imports Measure
```
```     5 begin
```
```     6
```
```     7 text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
```
```     8
```
```     9 definition borel_space where
```
```    10   "borel_space = sigma (UNIV::real set) (range (\<lambda>a::real. {x. x \<le> a}))"
```
```    11
```
```    12 definition borel_measurable where
```
```    13   "borel_measurable a = measurable a borel_space"
```
```    14
```
```    15 definition indicator_fn where
```
```    16   "indicator_fn s = (\<lambda>x. if x \<in> s then 1 else (0::real))"
```
```    17
```
```    18 definition mono_convergent where
```
```    19   "mono_convergent u f s \<equiv>
```
```    20         (\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
```
```    21         (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
```
```    22
```
```    23 lemma in_borel_measurable:
```
```    24    "f \<in> borel_measurable M \<longleftrightarrow>
```
```    25     sigma_algebra M \<and>
```
```    26     (\<forall>s \<in> sets (sigma UNIV (range (\<lambda>a::real. {x. x \<le> a}))).
```
```    27       f -` s \<inter> space M \<in> sets M)"
```
```    28 apply (auto simp add: borel_measurable_def measurable_def borel_space_def)
```
```    29 apply (metis PowD UNIV_I Un_commute sigma_algebra_sigma subset_Pow_Union subset_UNIV subset_Un_eq)
```
```    30 done
```
```    31
```
```    32 lemma (in sigma_algebra) borel_measurable_const:
```
```    33    "(\<lambda>x. c) \<in> borel_measurable M"
```
```    34   by (auto simp add: in_borel_measurable prems)
```
```    35
```
```    36 lemma (in sigma_algebra) borel_measurable_indicator:
```
```    37   assumes a: "a \<in> sets M"
```
```    38   shows "indicator_fn a \<in> borel_measurable M"
```
```    39 apply (auto simp add: in_borel_measurable indicator_fn_def prems)
```
```    40 apply (metis Diff_eq Int_commute a compl_sets)
```
```    41 done
```
```    42
```
```    43 lemma Collect_eq: "{w \<in> X. f w \<le> a} = {w. f w \<le> a} \<inter> X"
```
```    44   by (metis Collect_conj_eq Collect_mem_eq Int_commute)
```
```    45
```
```    46 lemma (in measure_space) borel_measurable_le_iff:
```
```    47    "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)"
```
```    48 proof
```
```    49   assume f: "f \<in> borel_measurable M"
```
```    50   { fix a
```
```    51     have "{w \<in> space M. f w \<le> a} \<in> sets M" using f
```
```    52       apply (auto simp add: in_borel_measurable sigma_def Collect_eq)
```
```    53       apply (drule_tac x="{x. x \<le> a}" in bspec, auto)
```
```    54       apply (metis equalityE rangeI subsetD sigma_sets.Basic)
```
```    55       done
```
```    56     }
```
```    57   thus "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M" by blast
```
```    58 next
```
```    59   assume "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M"
```
```    60   thus "f \<in> borel_measurable M"
```
```    61     apply (simp add: borel_measurable_def borel_space_def Collect_eq)
```
```    62     apply (rule measurable_sigma, auto)
```
```    63     done
```
```    64 qed
```
```    65
```
```    66 lemma Collect_less_le:
```
```    67      "{w \<in> X. f w < g w} = (\<Union>n. {w \<in> X. f w \<le> g w - inverse(real(Suc n))})"
```
```    68   proof auto
```
```    69     fix w
```
```    70     assume w: "f w < g w"
```
```    71     hence nz: "g w - f w \<noteq> 0"
```
```    72       by arith
```
```    73     with w have "real(Suc(natceiling(inverse(g w - f w)))) > inverse(g w - f w)"
```
```    74       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)))))
```
```    75              < inverse(inverse(g w - f w))"
```
```    76       by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_linordered_idom nz positive_imp_inverse_positive real_le_antisym real_less_def w)
```
```    77     hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < g w - f w"
```
```    78       by (metis inverse_inverse_eq order_less_le_trans real_le_refl)
```
```    79     thus "\<exists>n. f w \<le> g w - inverse(real(Suc n))" using w
```
```    80       by (rule_tac x="natceiling(inverse(g w - f w))" in exI, auto)
```
```    81   next
```
```    82     fix w n
```
```    83     assume le: "f w \<le> g w - inverse(real(Suc n))"
```
```    84     hence "0 < inverse(real(Suc n))"
```
```    85       by (metis inverse_real_of_nat_gt_zero)
```
```    86     thus "f w < g w" using le
```
```    87       by arith
```
```    88   qed
```
```    89
```
```    90
```
```    91 lemma (in sigma_algebra) sigma_le_less:
```
```    92   assumes M: "!!a::real. {w \<in> space M. f w \<le> a} \<in> sets M"
```
```    93   shows "{w \<in> space M. f w < a} \<in> sets M"
```
```    94 proof -
```
```    95   show ?thesis using Collect_less_le [of "space M" f "\<lambda>x. a"]
```
```    96     by (auto simp add: countable_UN M)
```
```    97 qed
```
```    98
```
```    99 lemma (in sigma_algebra) sigma_less_ge:
```
```   100   assumes M: "!!a::real. {w \<in> space M. f w < a} \<in> sets M"
```
```   101   shows "{w \<in> space M. a \<le> f w} \<in> sets M"
```
```   102 proof -
```
```   103   have "{w \<in> space M. a \<le> f w} = space M - {w \<in> space M. f w < a}"
```
```   104     by auto
```
```   105   thus ?thesis using M
```
```   106     by auto
```
```   107 qed
```
```   108
```
```   109 lemma (in sigma_algebra) sigma_ge_gr:
```
```   110   assumes M: "!!a::real. {w \<in> space M. a \<le> f w} \<in> sets M"
```
```   111   shows "{w \<in> space M. a < f w} \<in> sets M"
```
```   112 proof -
```
```   113   show ?thesis using Collect_less_le [of "space M" "\<lambda>x. a" f]
```
```   114     by (auto simp add: countable_UN le_diff_eq M)
```
```   115 qed
```
```   116
```
```   117 lemma (in sigma_algebra) sigma_gr_le:
```
```   118   assumes M: "!!a::real. {w \<in> space M. a < f w} \<in> sets M"
```
```   119   shows "{w \<in> space M. f w \<le> a} \<in> sets M"
```
```   120 proof -
```
```   121   have "{w \<in> space M. f w \<le> a} = space M - {w \<in> space M. a < f w}"
```
```   122     by auto
```
```   123   thus ?thesis
```
```   124     by (simp add: M compl_sets)
```
```   125 qed
```
```   126
```
```   127 lemma (in measure_space) borel_measurable_gr_iff:
```
```   128    "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
```
```   129 proof (auto simp add: borel_measurable_le_iff sigma_gr_le)
```
```   130   fix u
```
```   131   assume M: "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M"
```
```   132   have "{w \<in> space M. u < f w} = space M - {w \<in> space M. f w \<le> u}"
```
```   133     by auto
```
```   134   thus "{w \<in> space M. u < f w} \<in> sets M"
```
```   135     by (force simp add: compl_sets countable_UN M)
```
```   136 qed
```
```   137
```
```   138 lemma (in measure_space) borel_measurable_less_iff:
```
```   139    "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)"
```
```   140 proof (auto simp add: borel_measurable_le_iff sigma_le_less)
```
```   141   fix u
```
```   142   assume M: "\<forall>a. {w \<in> space M. f w < a} \<in> sets M"
```
```   143   have "{w \<in> space M. f w \<le> u} = space M - {w \<in> space M. u < f w}"
```
```   144     by auto
```
```   145   thus "{w \<in> space M. f w \<le> u} \<in> sets M"
```
```   146     using Collect_less_le [of "space M" "\<lambda>x. u" f]
```
```   147     by (force simp add: compl_sets countable_UN le_diff_eq sigma_less_ge M)
```
```   148 qed
```
```   149
```
```   150 lemma (in measure_space) borel_measurable_ge_iff:
```
```   151    "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)"
```
```   152 proof (auto simp add: borel_measurable_less_iff sigma_le_less sigma_ge_gr sigma_gr_le)
```
```   153   fix u
```
```   154   assume M: "\<forall>a. {w \<in> space M. f w < a} \<in> sets M"
```
```   155   have "{w \<in> space M. u \<le> f w} = space M - {w \<in> space M. f w < u}"
```
```   156     by auto
```
```   157   thus "{w \<in> space M. u \<le> f w} \<in> sets M"
```
```   158     by (force simp add: compl_sets countable_UN M)
```
```   159 qed
```
```   160
```
```   161 lemma (in measure_space) affine_borel_measurable:
```
```   162   assumes g: "g \<in> borel_measurable M"
```
```   163   shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
```
```   164 proof (cases rule: linorder_cases [of b 0])
```
```   165   case equal thus ?thesis
```
```   166     by (simp add: borel_measurable_const)
```
```   167 next
```
```   168   case less
```
```   169     {
```
```   170       fix w c
```
```   171       have "a + g w * b \<le> c \<longleftrightarrow> g w * b \<le> c - a"
```
```   172         by auto
```
```   173       also have "... \<longleftrightarrow> (c-a)/b \<le> g w" using less
```
```   174         by (metis divide_le_eq less less_asym)
```
```   175       finally have "a + g w * b \<le> c \<longleftrightarrow> (c-a)/b \<le> g w" .
```
```   176     }
```
```   177     hence "\<And>w c. a + g w * b \<le> c \<longleftrightarrow> (c-a)/b \<le> g w" .
```
```   178     thus ?thesis using less g
```
```   179       by (simp add: borel_measurable_ge_iff [of g])
```
```   180          (simp add: borel_measurable_le_iff)
```
```   181 next
```
```   182   case greater
```
```   183     hence 0: "\<And>x c. (g x * b \<le> c - a) \<longleftrightarrow> (g x \<le> (c - a) / b)"
```
```   184       by (metis mult_imp_le_div_pos le_divide_eq)
```
```   185     have 1: "\<And>x c. (a + g x * b \<le> c) \<longleftrightarrow> (g x * b \<le> c - a)"
```
```   186       by auto
```
```   187     from greater g
```
```   188     show ?thesis
```
```   189       by (simp add: borel_measurable_le_iff 0 1)
```
```   190 qed
```
```   191
```
```   192 definition
```
```   193   nat_to_rat_surj :: "nat \<Rightarrow> rat" where
```
```   194  "nat_to_rat_surj n = (let (i,j) = nat_to_nat2 n
```
```   195                        in Fract (nat_to_int_bij i) (nat_to_int_bij j))"
```
```   196
```
```   197 lemma nat_to_rat_surj: "surj nat_to_rat_surj"
```
```   198 proof (auto simp add: surj_def nat_to_rat_surj_def)
```
```   199   fix y
```
```   200   show "\<exists>x. y = (\<lambda>(i, j). Fract (nat_to_int_bij i) (nat_to_int_bij j)) (nat_to_nat2 x)"
```
```   201   proof (cases y)
```
```   202     case (Fract a b)
```
```   203       obtain i where i: "nat_to_int_bij i = a" using surj_nat_to_int_bij
```
```   204         by (metis surj_def)
```
```   205       obtain j where j: "nat_to_int_bij j = b" using surj_nat_to_int_bij
```
```   206         by (metis surj_def)
```
```   207       obtain n where n: "nat_to_nat2 n = (i,j)" using nat_to_nat2_surj
```
```   208         by (metis surj_def)
```
```   209
```
```   210       from Fract i j n show ?thesis
```
```   211         by (metis prod.cases prod_case_split)
```
```   212   qed
```
```   213 qed
```
```   214
```
```   215 lemma rats_enumeration: "\<rat> = range (of_rat o nat_to_rat_surj)"
```
```   216   using nat_to_rat_surj
```
```   217   by (auto simp add: image_def surj_def) (metis Rats_cases)
```
```   218
```
```   219 lemma (in measure_space) borel_measurable_less_borel_measurable:
```
```   220   assumes f: "f \<in> borel_measurable M"
```
```   221   assumes g: "g \<in> borel_measurable M"
```
```   222   shows "{w \<in> space M. f w < g w} \<in> sets M"
```
```   223 proof -
```
```   224   have "{w \<in> space M. f w < g w} =
```
```   225         (\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
```
```   226     by (auto simp add: Rats_dense_in_real)
```
```   227   thus ?thesis using f g
```
```   228     by (simp add: borel_measurable_less_iff [of f]
```
```   229                   borel_measurable_gr_iff [of g])
```
```   230        (blast intro: gen_countable_UN [OF rats_enumeration])
```
```   231 qed
```
```   232
```
```   233 lemma (in measure_space) borel_measurable_leq_borel_measurable:
```
```   234   assumes f: "f \<in> borel_measurable M"
```
```   235   assumes g: "g \<in> borel_measurable M"
```
```   236   shows "{w \<in> space M. f w \<le> g w} \<in> sets M"
```
```   237 proof -
```
```   238   have "{w \<in> space M. f w \<le> g w} = space M - {w \<in> space M. g w < f w}"
```
```   239     by auto
```
```   240   thus ?thesis using f g
```
```   241     by (simp add: borel_measurable_less_borel_measurable compl_sets)
```
```   242 qed
```
```   243
```
```   244 lemma (in measure_space) borel_measurable_eq_borel_measurable:
```
```   245   assumes f: "f \<in> borel_measurable M"
```
```   246   assumes g: "g \<in> borel_measurable M"
```
```   247   shows "{w \<in> space M. f w = g w} \<in> sets M"
```
```   248 proof -
```
```   249   have "{w \<in> space M. f w = g w} =
```
```   250         {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
```
```   251     by auto
```
```   252   thus ?thesis using f g
```
```   253     by (simp add: borel_measurable_leq_borel_measurable Int)
```
```   254 qed
```
```   255
```
```   256 lemma (in measure_space) borel_measurable_neq_borel_measurable:
```
```   257   assumes f: "f \<in> borel_measurable M"
```
```   258   assumes g: "g \<in> borel_measurable M"
```
```   259   shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
```
```   260 proof -
```
```   261   have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}"
```
```   262     by auto
```
```   263   thus ?thesis using f g
```
```   264     by (simp add: borel_measurable_eq_borel_measurable compl_sets)
```
```   265 qed
```
```   266
```
```   267 lemma (in measure_space) borel_measurable_add_borel_measurable:
```
```   268   assumes f: "f \<in> borel_measurable M"
```
```   269   assumes g: "g \<in> borel_measurable M"
```
```   270   shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
```
```   271 proof -
```
```   272   have 1:"!!a. {w \<in> space M. a \<le> f w + g w} = {w \<in> space M. a + (g w) * -1 \<le> f w}"
```
```   273     by auto
```
```   274   have "!!a. (\<lambda>w. a + (g w) * -1) \<in> borel_measurable M"
```
```   275     by (rule affine_borel_measurable [OF g])
```
```   276   hence "!!a. {w \<in> space M. (\<lambda>w. a + (g w) * -1)(w) \<le> f w} \<in> sets M" using f
```
```   277     by (rule borel_measurable_leq_borel_measurable)
```
```   278   hence "!!a. {w \<in> space M. a \<le> f w + g w} \<in> sets M"
```
```   279     by (simp add: 1)
```
```   280   thus ?thesis
```
```   281     by (simp add: borel_measurable_ge_iff)
```
```   282 qed
```
```   283
```
```   284
```
```   285 lemma (in measure_space) borel_measurable_square:
```
```   286   assumes f: "f \<in> borel_measurable M"
```
```   287   shows "(\<lambda>x. (f x)^2) \<in> borel_measurable M"
```
```   288 proof -
```
```   289   {
```
```   290     fix a
```
```   291     have "{w \<in> space M. (f w)\<twosuperior> \<le> a} \<in> sets M"
```
```   292     proof (cases rule: linorder_cases [of a 0])
```
```   293       case less
```
```   294       hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = {}"
```
```   295         by auto (metis less order_le_less_trans power2_less_0)
```
```   296       also have "... \<in> sets M"
```
```   297         by (rule empty_sets)
```
```   298       finally show ?thesis .
```
```   299     next
```
```   300       case equal
```
```   301       hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
```
```   302              {w \<in> space M. f w \<le> 0} \<inter> {w \<in> space M. 0 \<le> f w}"
```
```   303         by auto
```
```   304       also have "... \<in> sets M"
```
```   305         apply (insert f)
```
```   306         apply (rule Int)
```
```   307         apply (simp add: borel_measurable_le_iff)
```
```   308         apply (simp add: borel_measurable_ge_iff)
```
```   309         done
```
```   310       finally show ?thesis .
```
```   311     next
```
```   312       case greater
```
```   313       have "\<forall>x. (f x ^ 2 \<le> sqrt a ^ 2) = (- sqrt a  \<le> f x & f x \<le> sqrt a)"
```
```   314         by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs
```
```   315                   real_sqrt_le_iff real_sqrt_power)
```
```   316       hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
```
```   317              {w \<in> space M. -(sqrt a) \<le> f w} \<inter> {w \<in> space M. f w \<le> sqrt a}"
```
```   318         using greater by auto
```
```   319       also have "... \<in> sets M"
```
```   320         apply (insert f)
```
```   321         apply (rule Int)
```
```   322         apply (simp add: borel_measurable_ge_iff)
```
```   323         apply (simp add: borel_measurable_le_iff)
```
```   324         done
```
```   325       finally show ?thesis .
```
```   326     qed
```
```   327   }
```
```   328   thus ?thesis by (auto simp add: borel_measurable_le_iff)
```
```   329 qed
```
```   330
```
```   331 lemma times_eq_sum_squares:
```
```   332    fixes x::real
```
```   333    shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4"
```
```   334 by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric])
```
```   335
```
```   336
```
```   337 lemma (in measure_space) borel_measurable_uminus_borel_measurable:
```
```   338   assumes g: "g \<in> borel_measurable M"
```
```   339   shows "(\<lambda>x. - g x) \<in> borel_measurable M"
```
```   340 proof -
```
```   341   have "(\<lambda>x. - g x) = (\<lambda>x. 0 + (g x) * -1)"
```
```   342     by simp
```
```   343   also have "... \<in> borel_measurable M"
```
```   344     by (fast intro: affine_borel_measurable g)
```
```   345   finally show ?thesis .
```
```   346 qed
```
```   347
```
```   348 lemma (in measure_space) borel_measurable_times_borel_measurable:
```
```   349   assumes f: "f \<in> borel_measurable M"
```
```   350   assumes g: "g \<in> borel_measurable M"
```
```   351   shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
```
```   352 proof -
```
```   353   have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M"
```
```   354     by (fast intro: affine_borel_measurable borel_measurable_square
```
```   355                     borel_measurable_add_borel_measurable f g)
```
```   356   have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) =
```
```   357         (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
```
```   358     by (simp add: minus_divide_right)
```
```   359   also have "... \<in> borel_measurable M"
```
```   360     by (fast intro: affine_borel_measurable borel_measurable_square
```
```   361                     borel_measurable_add_borel_measurable
```
```   362                     borel_measurable_uminus_borel_measurable f g)
```
```   363   finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
```
```   364   show ?thesis
```
```   365     apply (simp add: times_eq_sum_squares real_diff_def)
```
```   366     using 1 2 apply (simp add: borel_measurable_add_borel_measurable)
```
```   367     done
```
```   368 qed
```
```   369
```
```   370 lemma (in measure_space) borel_measurable_diff_borel_measurable:
```
```   371   assumes f: "f \<in> borel_measurable M"
```
```   372   assumes g: "g \<in> borel_measurable M"
```
```   373   shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
```
```   374 unfolding real_diff_def
```
```   375   by (fast intro: borel_measurable_add_borel_measurable
```
```   376                   borel_measurable_uminus_borel_measurable f g)
```
```   377
```
```   378 lemma (in measure_space) mono_convergent_borel_measurable:
```
```   379   assumes u: "!!n. u n \<in> borel_measurable M"
```
```   380   assumes mc: "mono_convergent u f (space M)"
```
```   381   shows "f \<in> borel_measurable M"
```
```   382 proof -
```
```   383   {
```
```   384     fix a
```
```   385     have 1: "!!w. w \<in> space M & f w <= a \<longleftrightarrow> w \<in> space M & (\<forall>i. u i w <= a)"
```
```   386       proof safe
```
```   387         fix w i
```
```   388         assume w: "w \<in> space M" and f: "f w \<le> a"
```
```   389         hence "u i w \<le> f w"
```
```   390           by (auto intro: SEQ.incseq_le
```
```   391                    simp add: incseq_def mc [unfolded mono_convergent_def])
```
```   392         thus "u i w \<le> a" using f
```
```   393           by auto
```
```   394       next
```
```   395         fix w
```
```   396         assume w: "w \<in> space M" and u: "\<forall>i. u i w \<le> a"
```
```   397         thus "f w \<le> a"
```
```   398           by (metis LIMSEQ_le_const2 mc [unfolded mono_convergent_def])
```
```   399       qed
```
```   400     have "{w \<in> space M. f w \<le> a} = {w \<in> space M. (\<forall>i. u i w <= a)}"
```
```   401       by (simp add: 1)
```
```   402     also have "... = (\<Inter>i. {w \<in> space M. u i w \<le> a})"
```
```   403       by auto
```
```   404     also have "...  \<in> sets M" using u
```
```   405       by (auto simp add: borel_measurable_le_iff intro: countable_INT)
```
```   406     finally have "{w \<in> space M. f w \<le> a} \<in> sets M" .
```
```   407   }
```
```   408   thus ?thesis
```
```   409     by (auto simp add: borel_measurable_le_iff)
```
```   410 qed
```
```   411
```
```   412 lemma (in measure_space) borel_measurable_setsum_borel_measurable:
```
```   413   assumes s: "finite s"
```
```   414   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
```
```   415 proof (induct s)
```
```   416   case empty
```
```   417   thus ?case
```
```   418     by (simp add: borel_measurable_const)
```
```   419 next
```
```   420   case (insert x s)
```
```   421   thus ?case
```
```   422     by (auto simp add: borel_measurable_add_borel_measurable)
```
```   423 qed
```
```   424
```
```   425 end
```