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