src/HOL/Probability/Borel.thy
author hoelzl
Mon Aug 23 19:35:57 2010 +0200 (2010-08-23)
changeset 38656 d5d342611edb
parent 37887 2ae085b07f2f
child 38705 aaee86c0e237
permissions -rw-r--r--
Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
hoelzl@38656
     1
(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
hoelzl@38656
     2
hoelzl@38656
     3
header {*Borel spaces*}
paulson@33533
     4
paulson@33533
     5
theory Borel
hoelzl@38656
     6
  imports Sigma_Algebra Positive_Infinite_Real Multivariate_Analysis
paulson@33533
     7
begin
paulson@33533
     8
hoelzl@38656
     9
section "Generic Borel spaces"
paulson@33533
    10
hoelzl@38656
    11
definition "borel_space = sigma (UNIV::'a::topological_space set) open"
hoelzl@38656
    12
abbreviation "borel_measurable M \<equiv> measurable M borel_space"
paulson@33533
    13
hoelzl@38656
    14
interpretation borel_space: sigma_algebra borel_space
hoelzl@38656
    15
  using sigma_algebra_sigma by (auto simp: borel_space_def)
paulson@33533
    16
paulson@33533
    17
lemma in_borel_measurable:
paulson@33533
    18
   "f \<in> borel_measurable M \<longleftrightarrow>
hoelzl@38656
    19
    (\<forall>S \<in> sets (sigma UNIV open).
hoelzl@38656
    20
      f -` S \<inter> space M \<in> sets M)"
hoelzl@38656
    21
  by (auto simp add: measurable_def borel_space_def)
paulson@33533
    22
hoelzl@38656
    23
lemma in_borel_measurable_borel_space:
hoelzl@38656
    24
   "f \<in> borel_measurable M \<longleftrightarrow>
hoelzl@38656
    25
    (\<forall>S \<in> sets borel_space.
hoelzl@38656
    26
      f -` S \<inter> space M \<in> sets M)"
hoelzl@38656
    27
  by (auto simp add: measurable_def borel_space_def)
paulson@33533
    28
hoelzl@38656
    29
lemma space_borel_space[simp]: "space borel_space = UNIV"
hoelzl@38656
    30
  unfolding borel_space_def by auto
hoelzl@38656
    31
hoelzl@38656
    32
lemma borel_space_open[simp]:
hoelzl@38656
    33
  assumes "open A" shows "A \<in> sets borel_space"
hoelzl@38656
    34
proof -
hoelzl@38656
    35
  have "A \<in> open" unfolding mem_def using assms .
hoelzl@38656
    36
  thus ?thesis unfolding borel_space_def sigma_def by (auto intro!: sigma_sets.Basic)
paulson@33533
    37
qed
paulson@33533
    38
hoelzl@38656
    39
lemma borel_space_closed[simp]:
hoelzl@38656
    40
  assumes "closed A" shows "A \<in> sets borel_space"
paulson@33533
    41
proof -
hoelzl@38656
    42
  have "space borel_space - (- A) \<in> sets borel_space"
hoelzl@38656
    43
    using assms unfolding closed_def by (blast intro: borel_space_open)
hoelzl@38656
    44
  thus ?thesis by simp
paulson@33533
    45
qed
paulson@33533
    46
hoelzl@38656
    47
lemma (in sigma_algebra) borel_measurable_vimage:
hoelzl@38656
    48
  fixes f :: "'a \<Rightarrow> 'x::t2_space"
hoelzl@38656
    49
  assumes borel: "f \<in> borel_measurable M"
hoelzl@38656
    50
  shows "f -` {x} \<inter> space M \<in> sets M"
hoelzl@38656
    51
proof (cases "x \<in> f ` space M")
hoelzl@38656
    52
  case True then obtain y where "x = f y" by auto
hoelzl@38656
    53
  from closed_sing[of "f y"]
hoelzl@38656
    54
  have "{f y} \<in> sets borel_space" by (rule borel_space_closed)
hoelzl@38656
    55
  with assms show ?thesis
hoelzl@38656
    56
    unfolding in_borel_measurable_borel_space `x = f y` by auto
hoelzl@38656
    57
next
hoelzl@38656
    58
  case False hence "f -` {x} \<inter> space M = {}" by auto
hoelzl@38656
    59
  thus ?thesis by auto
paulson@33533
    60
qed
paulson@33533
    61
hoelzl@38656
    62
lemma (in sigma_algebra) borel_measurableI:
hoelzl@38656
    63
  fixes f :: "'a \<Rightarrow> 'x\<Colon>topological_space"
hoelzl@38656
    64
  assumes "\<And>S. open S \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
hoelzl@38656
    65
  shows "f \<in> borel_measurable M"
hoelzl@38656
    66
  unfolding borel_space_def
hoelzl@38656
    67
proof (rule measurable_sigma)
hoelzl@38656
    68
  fix S :: "'x set" assume "S \<in> open" thus "f -` S \<inter> space M \<in> sets M"
hoelzl@38656
    69
    using assms[of S] by (simp add: mem_def)
hoelzl@38656
    70
qed simp_all
paulson@33533
    71
hoelzl@38656
    72
lemma borel_space_singleton[simp, intro]:
hoelzl@38656
    73
  fixes x :: "'a::t1_space"
hoelzl@38656
    74
  shows "A \<in> sets borel_space \<Longrightarrow> insert x A \<in> sets borel_space"
hoelzl@38656
    75
  proof (rule borel_space.insert_in_sets)
hoelzl@38656
    76
    show "{x} \<in> sets borel_space"
hoelzl@38656
    77
      using closed_sing[of x] by (rule borel_space_closed)
hoelzl@38656
    78
  qed simp
hoelzl@38656
    79
hoelzl@38656
    80
lemma (in sigma_algebra) borel_measurable_const[simp, intro]:
hoelzl@38656
    81
  "(\<lambda>x. c) \<in> borel_measurable M"
hoelzl@38656
    82
  by (auto intro!: measurable_const)
paulson@33533
    83
hoelzl@38656
    84
lemma (in sigma_algebra) borel_measurable_indicator:
hoelzl@38656
    85
  assumes A: "A \<in> sets M"
hoelzl@38656
    86
  shows "indicator A \<in> borel_measurable M"
hoelzl@38656
    87
  unfolding indicator_def_raw using A
hoelzl@38656
    88
  by (auto intro!: measurable_If_set borel_measurable_const)
paulson@33533
    89
hoelzl@38656
    90
lemma borel_measurable_translate:
hoelzl@38656
    91
  assumes "A \<in> sets borel_space" and trans: "\<And>B. open B \<Longrightarrow> f -` B \<in> sets borel_space"
hoelzl@38656
    92
  shows "f -` A \<in> sets borel_space"
hoelzl@38656
    93
proof -
hoelzl@38656
    94
  have "A \<in> sigma_sets UNIV open" using assms
hoelzl@38656
    95
    by (simp add: borel_space_def sigma_def)
hoelzl@38656
    96
  thus ?thesis
hoelzl@38656
    97
  proof (induct rule: sigma_sets.induct)
hoelzl@38656
    98
    case (Basic a) thus ?case using trans[of a] by (simp add: mem_def)
hoelzl@38656
    99
  next
hoelzl@38656
   100
    case (Compl a)
hoelzl@38656
   101
    moreover have "UNIV \<in> sets borel_space"
hoelzl@38656
   102
      by (metis borel_space.top borel_space_def_raw mem_def space_sigma)
hoelzl@38656
   103
    ultimately show ?case
hoelzl@38656
   104
      by (auto simp: vimage_Diff borel_space.Diff)
hoelzl@38656
   105
  qed (auto simp add: vimage_UN)
paulson@33533
   106
qed
paulson@33533
   107
hoelzl@38656
   108
section "Borel spaces on euclidean spaces"
hoelzl@38656
   109
hoelzl@38656
   110
lemma lessThan_borel[simp, intro]:
hoelzl@38656
   111
  fixes a :: "'a\<Colon>ordered_euclidean_space"
hoelzl@38656
   112
  shows "{..< a} \<in> sets borel_space"
hoelzl@38656
   113
  by (blast intro: borel_space_open)
hoelzl@38656
   114
hoelzl@38656
   115
lemma greaterThan_borel[simp, intro]:
hoelzl@38656
   116
  fixes a :: "'a\<Colon>ordered_euclidean_space"
hoelzl@38656
   117
  shows "{a <..} \<in> sets borel_space"
hoelzl@38656
   118
  by (blast intro: borel_space_open)
hoelzl@38656
   119
hoelzl@38656
   120
lemma greaterThanLessThan_borel[simp, intro]:
hoelzl@38656
   121
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
hoelzl@38656
   122
  shows "{a<..<b} \<in> sets borel_space"
hoelzl@38656
   123
  by (blast intro: borel_space_open)
hoelzl@38656
   124
hoelzl@38656
   125
lemma atMost_borel[simp, intro]:
hoelzl@38656
   126
  fixes a :: "'a\<Colon>ordered_euclidean_space"
hoelzl@38656
   127
  shows "{..a} \<in> sets borel_space"
hoelzl@38656
   128
  by (blast intro: borel_space_closed)
hoelzl@38656
   129
hoelzl@38656
   130
lemma atLeast_borel[simp, intro]:
hoelzl@38656
   131
  fixes a :: "'a\<Colon>ordered_euclidean_space"
hoelzl@38656
   132
  shows "{a..} \<in> sets borel_space"
hoelzl@38656
   133
  by (blast intro: borel_space_closed)
hoelzl@38656
   134
hoelzl@38656
   135
lemma atLeastAtMost_borel[simp, intro]:
hoelzl@38656
   136
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
hoelzl@38656
   137
  shows "{a..b} \<in> sets borel_space"
hoelzl@38656
   138
  by (blast intro: borel_space_closed)
paulson@33533
   139
hoelzl@38656
   140
lemma greaterThanAtMost_borel[simp, intro]:
hoelzl@38656
   141
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
hoelzl@38656
   142
  shows "{a<..b} \<in> sets borel_space"
hoelzl@38656
   143
  unfolding greaterThanAtMost_def by blast
hoelzl@38656
   144
hoelzl@38656
   145
lemma atLeastLessThan_borel[simp, intro]:
hoelzl@38656
   146
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
hoelzl@38656
   147
  shows "{a..<b} \<in> sets borel_space"
hoelzl@38656
   148
  unfolding atLeastLessThan_def by blast
hoelzl@38656
   149
hoelzl@38656
   150
lemma hafspace_less_borel[simp, intro]:
hoelzl@38656
   151
  fixes a :: real
hoelzl@38656
   152
  shows "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel_space"
hoelzl@38656
   153
  by (auto intro!: borel_space_open open_halfspace_component_gt)
paulson@33533
   154
hoelzl@38656
   155
lemma hafspace_greater_borel[simp, intro]:
hoelzl@38656
   156
  fixes a :: real
hoelzl@38656
   157
  shows "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel_space"
hoelzl@38656
   158
  by (auto intro!: borel_space_open open_halfspace_component_lt)
paulson@33533
   159
hoelzl@38656
   160
lemma hafspace_less_eq_borel[simp, intro]:
hoelzl@38656
   161
  fixes a :: real
hoelzl@38656
   162
  shows "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel_space"
hoelzl@38656
   163
  by (auto intro!: borel_space_closed closed_halfspace_component_ge)
paulson@33533
   164
hoelzl@38656
   165
lemma hafspace_greater_eq_borel[simp, intro]:
hoelzl@38656
   166
  fixes a :: real
hoelzl@38656
   167
  shows "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel_space"
hoelzl@38656
   168
  by (auto intro!: borel_space_closed closed_halfspace_component_le)
paulson@33533
   169
hoelzl@38656
   170
lemma (in sigma_algebra) borel_measurable_less[simp, intro]:
hoelzl@38656
   171
  fixes f :: "'a \<Rightarrow> real"
paulson@33533
   172
  assumes f: "f \<in> borel_measurable M"
paulson@33533
   173
  assumes g: "g \<in> borel_measurable M"
paulson@33533
   174
  shows "{w \<in> space M. f w < g w} \<in> sets M"
paulson@33533
   175
proof -
paulson@33533
   176
  have "{w \<in> space M. f w < g w} =
hoelzl@38656
   177
        (\<Union>r. (f -` {..< of_rat r} \<inter> space M) \<inter> (g -` {of_rat r <..} \<inter> space M))"
hoelzl@38656
   178
    using Rats_dense_in_real by (auto simp add: Rats_def)
hoelzl@38656
   179
  then show ?thesis using f g
hoelzl@38656
   180
    by simp (blast intro: measurable_sets)
paulson@33533
   181
qed
hoelzl@38656
   182
hoelzl@38656
   183
lemma (in sigma_algebra) borel_measurable_le[simp, intro]:
hoelzl@38656
   184
  fixes f :: "'a \<Rightarrow> real"
paulson@33533
   185
  assumes f: "f \<in> borel_measurable M"
paulson@33533
   186
  assumes g: "g \<in> borel_measurable M"
paulson@33533
   187
  shows "{w \<in> space M. f w \<le> g w} \<in> sets M"
paulson@33533
   188
proof -
hoelzl@38656
   189
  have "{w \<in> space M. f w \<le> g w} = space M - {w \<in> space M. g w < f w}"
hoelzl@38656
   190
    by auto
hoelzl@38656
   191
  thus ?thesis using f g
hoelzl@38656
   192
    by simp blast
paulson@33533
   193
qed
paulson@33533
   194
hoelzl@38656
   195
lemma (in sigma_algebra) borel_measurable_eq[simp, intro]:
hoelzl@38656
   196
  fixes f :: "'a \<Rightarrow> real"
paulson@33533
   197
  assumes f: "f \<in> borel_measurable M"
paulson@33533
   198
  assumes g: "g \<in> borel_measurable M"
paulson@33533
   199
  shows "{w \<in> space M. f w = g w} \<in> sets M"
paulson@33533
   200
proof -
paulson@33533
   201
  have "{w \<in> space M. f w = g w} =
wenzelm@33536
   202
        {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
paulson@33533
   203
    by auto
hoelzl@38656
   204
  thus ?thesis using f g by auto
paulson@33533
   205
qed
paulson@33533
   206
hoelzl@38656
   207
lemma (in sigma_algebra) borel_measurable_neq[simp, intro]:
hoelzl@38656
   208
  fixes f :: "'a \<Rightarrow> real"
paulson@33533
   209
  assumes f: "f \<in> borel_measurable M"
paulson@33533
   210
  assumes g: "g \<in> borel_measurable M"
paulson@33533
   211
  shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
paulson@33533
   212
proof -
paulson@33533
   213
  have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}"
paulson@33533
   214
    by auto
hoelzl@38656
   215
  thus ?thesis using f g by auto
hoelzl@38656
   216
qed
hoelzl@38656
   217
hoelzl@38656
   218
subsection "Borel space equals sigma algebras over intervals"
hoelzl@38656
   219
hoelzl@38656
   220
lemma rational_boxes:
hoelzl@38656
   221
  fixes x :: "'a\<Colon>ordered_euclidean_space"
hoelzl@38656
   222
  assumes "0 < e"
hoelzl@38656
   223
  shows "\<exists>a b. (\<forall>i. a $$ i \<in> \<rat>) \<and> (\<forall>i. b $$ i \<in> \<rat>) \<and> x \<in> {a <..< b} \<and> {a <..< b} \<subseteq> ball x e"
hoelzl@38656
   224
proof -
hoelzl@38656
   225
  def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
hoelzl@38656
   226
  then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos)
hoelzl@38656
   227
  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x $$ i \<and> x $$ i - y < e'" (is "\<forall>i. ?th i")
hoelzl@38656
   228
  proof
hoelzl@38656
   229
    fix i from Rats_dense_in_real[of "x $$ i - e'" "x $$ i"] e
hoelzl@38656
   230
    show "?th i" by auto
hoelzl@38656
   231
  qed
hoelzl@38656
   232
  from choice[OF this] guess a .. note a = this
hoelzl@38656
   233
  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x $$ i < y \<and> y - x $$ i < e'" (is "\<forall>i. ?th i")
hoelzl@38656
   234
  proof
hoelzl@38656
   235
    fix i from Rats_dense_in_real[of "x $$ i" "x $$ i + e'"] e
hoelzl@38656
   236
    show "?th i" by auto
hoelzl@38656
   237
  qed
hoelzl@38656
   238
  from choice[OF this] guess b .. note b = this
hoelzl@38656
   239
  { fix y :: 'a assume *: "Chi a < y" "y < Chi b"
hoelzl@38656
   240
    have "dist x y = sqrt (\<Sum>i<DIM('a). (dist (x $$ i) (y $$ i))\<twosuperior>)"
hoelzl@38656
   241
      unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
hoelzl@38656
   242
    also have "\<dots> < sqrt (\<Sum>i<DIM('a). e^2 / real (DIM('a)))"
hoelzl@38656
   243
    proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
hoelzl@38656
   244
      fix i assume i: "i \<in> {..<DIM('a)}"
hoelzl@38656
   245
      have "a i < y$$i \<and> y$$i < b i" using * i eucl_less[where 'a='a] by auto
hoelzl@38656
   246
      moreover have "a i < x$$i" "x$$i - a i < e'" using a by auto
hoelzl@38656
   247
      moreover have "x$$i < b i" "b i - x$$i < e'" using b by auto
hoelzl@38656
   248
      ultimately have "\<bar>x$$i - y$$i\<bar> < 2 * e'" by auto
hoelzl@38656
   249
      then have "dist (x $$ i) (y $$ i) < e/sqrt (real (DIM('a)))"
hoelzl@38656
   250
        unfolding e'_def by (auto simp: dist_real_def)
hoelzl@38656
   251
      then have "(dist (x $$ i) (y $$ i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
hoelzl@38656
   252
        by (rule power_strict_mono) auto
hoelzl@38656
   253
      then show "(dist (x $$ i) (y $$ i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
hoelzl@38656
   254
        by (simp add: power_divide)
hoelzl@38656
   255
    qed auto
hoelzl@38656
   256
    also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive)
hoelzl@38656
   257
    finally have "dist x y < e" . }
hoelzl@38656
   258
  with a b show ?thesis
hoelzl@38656
   259
    apply (rule_tac exI[of _ "Chi a"])
hoelzl@38656
   260
    apply (rule_tac exI[of _ "Chi b"])
hoelzl@38656
   261
    using eucl_less[where 'a='a] by auto
hoelzl@38656
   262
qed
hoelzl@38656
   263
hoelzl@38656
   264
lemma ex_rat_list:
hoelzl@38656
   265
  fixes x :: "'a\<Colon>ordered_euclidean_space"
hoelzl@38656
   266
  assumes "\<And> i. x $$ i \<in> \<rat>"
hoelzl@38656
   267
  shows "\<exists> r. length r = DIM('a) \<and> (\<forall> i < DIM('a). of_rat (r ! i) = x $$ i)"
hoelzl@38656
   268
proof -
hoelzl@38656
   269
  have "\<forall>i. \<exists>r. x $$ i = of_rat r" using assms unfolding Rats_def by blast
hoelzl@38656
   270
  from choice[OF this] guess r ..
hoelzl@38656
   271
  then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"])
hoelzl@38656
   272
qed
hoelzl@38656
   273
hoelzl@38656
   274
lemma open_UNION:
hoelzl@38656
   275
  fixes M :: "'a\<Colon>ordered_euclidean_space set"
hoelzl@38656
   276
  assumes "open M"
hoelzl@38656
   277
  shows "M = UNION {(a, b) | a b. {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)} \<subseteq> M}
hoelzl@38656
   278
                   (\<lambda> (a, b). {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)})"
hoelzl@38656
   279
    (is "M = UNION ?idx ?box")
hoelzl@38656
   280
proof safe
hoelzl@38656
   281
  fix x assume "x \<in> M"
hoelzl@38656
   282
  obtain e where e: "e > 0" "ball x e \<subseteq> M"
hoelzl@38656
   283
    using openE[OF assms `x \<in> M`] by auto
hoelzl@38656
   284
  then obtain a b where ab: "x \<in> {a <..< b}" "\<And>i. a $$ i \<in> \<rat>" "\<And>i. b $$ i \<in> \<rat>" "{a <..< b} \<subseteq> ball x e"
hoelzl@38656
   285
    using rational_boxes[OF e(1)] by blast
hoelzl@38656
   286
  then obtain p q where pq: "length p = DIM ('a)"
hoelzl@38656
   287
                            "length q = DIM ('a)"
hoelzl@38656
   288
                            "\<forall> i < DIM ('a). of_rat (p ! i) = a $$ i \<and> of_rat (q ! i) = b $$ i"
hoelzl@38656
   289
    using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast
hoelzl@38656
   290
  hence p: "Chi (of_rat \<circ> op ! p) = a"
hoelzl@38656
   291
    using euclidean_eq[of "Chi (of_rat \<circ> op ! p)" a]
hoelzl@38656
   292
    unfolding o_def by auto
hoelzl@38656
   293
  from pq have q: "Chi (of_rat \<circ> op ! q) = b"
hoelzl@38656
   294
    using euclidean_eq[of "Chi (of_rat \<circ> op ! q)" b]
hoelzl@38656
   295
    unfolding o_def by auto
hoelzl@38656
   296
  have "x \<in> ?box (p, q)"
hoelzl@38656
   297
    using p q ab by auto
hoelzl@38656
   298
  thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto
hoelzl@38656
   299
qed auto
hoelzl@38656
   300
hoelzl@38656
   301
lemma halfspace_span_open:
hoelzl@38656
   302
  "sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})))
hoelzl@38656
   303
    \<subseteq> sets borel_space"
hoelzl@38656
   304
  by (auto intro!: borel_space.sigma_sets_subset[simplified] borel_space_open
hoelzl@38656
   305
                   open_halfspace_component_lt simp: sets_sigma)
hoelzl@38656
   306
hoelzl@38656
   307
lemma halfspace_lt_in_halfspace:
hoelzl@38656
   308
  "{x\<Colon>'a. x $$ i < a} \<in> sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})))"
hoelzl@38656
   309
  unfolding sets_sigma by (rule sigma_sets.Basic) auto
hoelzl@38656
   310
hoelzl@38656
   311
lemma halfspace_gt_in_halfspace:
hoelzl@38656
   312
  "{x\<Colon>'a. a < x $$ i} \<in> sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})))"
hoelzl@38656
   313
    (is "?set \<in> sets ?SIGMA")
hoelzl@38656
   314
proof -
hoelzl@38656
   315
  interpret sigma_algebra ?SIGMA by (rule sigma_algebra_sigma) simp
hoelzl@38656
   316
  have *: "?set = (\<Union>n. space ?SIGMA - {x\<Colon>'a. x $$ i < a + 1 / real (Suc n)})"
hoelzl@38656
   317
  proof (safe, simp_all add: not_less)
hoelzl@38656
   318
    fix x assume "a < x $$ i"
hoelzl@38656
   319
    with reals_Archimedean[of "x $$ i - a"]
hoelzl@38656
   320
    obtain n where "a + 1 / real (Suc n) < x $$ i"
hoelzl@38656
   321
      by (auto simp: inverse_eq_divide field_simps)
hoelzl@38656
   322
    then show "\<exists>n. a + 1 / real (Suc n) \<le> x $$ i"
hoelzl@38656
   323
      by (blast intro: less_imp_le)
hoelzl@38656
   324
  next
hoelzl@38656
   325
    fix x n
hoelzl@38656
   326
    have "a < a + 1 / real (Suc n)" by auto
hoelzl@38656
   327
    also assume "\<dots> \<le> x"
hoelzl@38656
   328
    finally show "a < x" .
hoelzl@38656
   329
  qed
hoelzl@38656
   330
  show "?set \<in> sets ?SIGMA" unfolding *
hoelzl@38656
   331
    by (safe intro!: countable_UN Diff halfspace_lt_in_halfspace)
paulson@33533
   332
qed
paulson@33533
   333
hoelzl@38656
   334
lemma (in sigma_algebra) sets_sigma_subset:
hoelzl@38656
   335
  assumes "A = space M"
hoelzl@38656
   336
  assumes "B \<subseteq> sets M"
hoelzl@38656
   337
  shows "sets (sigma A B) \<subseteq> sets M"
hoelzl@38656
   338
  by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms)
hoelzl@38656
   339
hoelzl@38656
   340
lemma open_span_halfspace:
hoelzl@38656
   341
  "sets borel_space \<subseteq> sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x $$ i < a})))"
hoelzl@38656
   342
    (is "_ \<subseteq> sets ?SIGMA")
hoelzl@38656
   343
proof (unfold borel_space_def, rule sigma_algebra.sets_sigma_subset, safe)
hoelzl@38656
   344
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) simp
hoelzl@38656
   345
  then interpret sigma_algebra ?SIGMA .
hoelzl@38656
   346
  fix S :: "'a set" assume "S \<in> open" then have "open S" unfolding mem_def .
hoelzl@38656
   347
  from open_UNION[OF this]
hoelzl@38656
   348
  obtain I where *: "S =
hoelzl@38656
   349
    (\<Union>(a, b)\<in>I.
hoelzl@38656
   350
        (\<Inter> i<DIM('a). {x. (Chi (real_of_rat \<circ> op ! a)::'a) $$ i < x $$ i}) \<inter>
hoelzl@38656
   351
        (\<Inter> i<DIM('a). {x. x $$ i < (Chi (real_of_rat \<circ> op ! b)::'a) $$ i}))"
hoelzl@38656
   352
    unfolding greaterThanLessThan_def
hoelzl@38656
   353
    unfolding eucl_greaterThan_eq_halfspaces[where 'a='a]
hoelzl@38656
   354
    unfolding eucl_lessThan_eq_halfspaces[where 'a='a]
hoelzl@38656
   355
    by blast
hoelzl@38656
   356
  show "S \<in> sets ?SIGMA"
hoelzl@38656
   357
    unfolding *
hoelzl@38656
   358
    by (auto intro!: countable_UN Int countable_INT halfspace_lt_in_halfspace halfspace_gt_in_halfspace)
hoelzl@38656
   359
qed auto
hoelzl@38656
   360
hoelzl@38656
   361
lemma halfspace_span_halfspace_le:
hoelzl@38656
   362
  "sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a}))) \<subseteq>
hoelzl@38656
   363
   sets (sigma UNIV (range (\<lambda> (a, i). {x. x $$ i \<le> a})))"
hoelzl@38656
   364
  (is "_ \<subseteq> sets ?SIGMA")
hoelzl@38656
   365
proof (rule sigma_algebra.sets_sigma_subset, safe)
hoelzl@38656
   366
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
hoelzl@38656
   367
  then interpret sigma_algebra ?SIGMA .
hoelzl@38656
   368
  fix a i
hoelzl@38656
   369
  have *: "{x::'a. x$$i < a} = (\<Union>n. {x. x$$i \<le> a - 1/real (Suc n)})"
hoelzl@38656
   370
  proof (safe, simp_all)
hoelzl@38656
   371
    fix x::'a assume *: "x$$i < a"
hoelzl@38656
   372
    with reals_Archimedean[of "a - x$$i"]
hoelzl@38656
   373
    obtain n where "x $$ i < a - 1 / (real (Suc n))"
hoelzl@38656
   374
      by (auto simp: field_simps inverse_eq_divide)
hoelzl@38656
   375
    then show "\<exists>n. x $$ i \<le> a - 1 / (real (Suc n))"
hoelzl@38656
   376
      by (blast intro: less_imp_le)
hoelzl@38656
   377
  next
hoelzl@38656
   378
    fix x::'a and n
hoelzl@38656
   379
    assume "x$$i \<le> a - 1 / real (Suc n)"
hoelzl@38656
   380
    also have "\<dots> < a" by auto
hoelzl@38656
   381
    finally show "x$$i < a" .
hoelzl@38656
   382
  qed
hoelzl@38656
   383
  show "{x. x$$i < a} \<in> sets ?SIGMA" unfolding *
hoelzl@38656
   384
    by (safe intro!: countable_UN)
hoelzl@38656
   385
       (auto simp: sets_sigma intro!: sigma_sets.Basic)
hoelzl@38656
   386
qed auto
hoelzl@38656
   387
hoelzl@38656
   388
lemma halfspace_span_halfspace_ge:
hoelzl@38656
   389
  "sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a}))) \<subseteq> 
hoelzl@38656
   390
   sets (sigma UNIV (range (\<lambda> (a, i). {x. a \<le> x $$ i})))"
hoelzl@38656
   391
  (is "_ \<subseteq> sets ?SIGMA")
hoelzl@38656
   392
proof (rule sigma_algebra.sets_sigma_subset, safe)
hoelzl@38656
   393
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
hoelzl@38656
   394
  then interpret sigma_algebra ?SIGMA .
hoelzl@38656
   395
  fix a i have *: "{x::'a. x$$i < a} = space ?SIGMA - {x::'a. a \<le> x$$i}" by auto
hoelzl@38656
   396
  show "{x. x$$i < a} \<in> sets ?SIGMA" unfolding *
hoelzl@38656
   397
    by (safe intro!: Diff)
hoelzl@38656
   398
       (auto simp: sets_sigma intro!: sigma_sets.Basic)
hoelzl@38656
   399
qed auto
hoelzl@38656
   400
hoelzl@38656
   401
lemma halfspace_le_span_halfspace_gt:
hoelzl@38656
   402
  "sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a}))) \<subseteq> 
hoelzl@38656
   403
   sets (sigma UNIV (range (\<lambda> (a, i). {x. a < x $$ i})))"
hoelzl@38656
   404
  (is "_ \<subseteq> sets ?SIGMA")
hoelzl@38656
   405
proof (rule sigma_algebra.sets_sigma_subset, safe)
hoelzl@38656
   406
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
hoelzl@38656
   407
  then interpret sigma_algebra ?SIGMA .
hoelzl@38656
   408
  fix a i have *: "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto
hoelzl@38656
   409
  show "{x. x$$i \<le> a} \<in> sets ?SIGMA" unfolding *
hoelzl@38656
   410
    by (safe intro!: Diff)
hoelzl@38656
   411
       (auto simp: sets_sigma intro!: sigma_sets.Basic)
hoelzl@38656
   412
qed auto
hoelzl@38656
   413
hoelzl@38656
   414
lemma halfspace_le_span_atMost:
hoelzl@38656
   415
  "sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a}))) \<subseteq>
hoelzl@38656
   416
   sets (sigma UNIV (range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space})))"
hoelzl@38656
   417
  (is "_ \<subseteq> sets ?SIGMA")
hoelzl@38656
   418
proof (rule sigma_algebra.sets_sigma_subset, safe)
hoelzl@38656
   419
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
hoelzl@38656
   420
  then interpret sigma_algebra ?SIGMA .
hoelzl@38656
   421
  fix a i
hoelzl@38656
   422
  show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
hoelzl@38656
   423
  proof cases
hoelzl@38656
   424
    assume "i < DIM('a)"
hoelzl@38656
   425
    then have *: "{x::'a. x$$i \<le> a} = (\<Union>k::nat. {.. (\<chi>\<chi> n. if n = i then a else real k)})"
hoelzl@38656
   426
    proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm)
hoelzl@38656
   427
      fix x
hoelzl@38656
   428
      from real_arch_simple[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"] guess k::nat ..
hoelzl@38656
   429
      then have "\<And>i. i < DIM('a) \<Longrightarrow> x$$i \<le> real k"
hoelzl@38656
   430
        by (subst (asm) Max_le_iff) auto
hoelzl@38656
   431
      then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia \<le> real k"
hoelzl@38656
   432
        by (auto intro!: exI[of _ k])
hoelzl@38656
   433
    qed
hoelzl@38656
   434
    show "{x. x$$i \<le> a} \<in> sets ?SIGMA" unfolding *
hoelzl@38656
   435
      by (safe intro!: countable_UN)
hoelzl@38656
   436
         (auto simp: sets_sigma intro!: sigma_sets.Basic)
hoelzl@38656
   437
  next
hoelzl@38656
   438
    assume "\<not> i < DIM('a)"
hoelzl@38656
   439
    then show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
hoelzl@38656
   440
      using top by auto
hoelzl@38656
   441
  qed
hoelzl@38656
   442
qed auto
hoelzl@38656
   443
hoelzl@38656
   444
lemma halfspace_le_span_greaterThan:
hoelzl@38656
   445
  "sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a}))) \<subseteq>
hoelzl@38656
   446
   sets (sigma UNIV (range (\<lambda>a. {a<..})))"
hoelzl@38656
   447
  (is "_ \<subseteq> sets ?SIGMA")
hoelzl@38656
   448
proof (rule sigma_algebra.sets_sigma_subset, safe)
hoelzl@38656
   449
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
hoelzl@38656
   450
  then interpret sigma_algebra ?SIGMA .
hoelzl@38656
   451
  fix a i
hoelzl@38656
   452
  show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
hoelzl@38656
   453
  proof cases
hoelzl@38656
   454
    assume "i < DIM('a)"
hoelzl@38656
   455
    have "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto
hoelzl@38656
   456
    also have *: "{x::'a. a < x$$i} = (\<Union>k::nat. {(\<chi>\<chi> n. if n = i then a else -real k) <..})" using `i <DIM('a)`
hoelzl@38656
   457
    proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
hoelzl@38656
   458
      fix x
hoelzl@38656
   459
      from real_arch_lt[of "Max ((\<lambda>i. -x$$i)`{..<DIM('a)})"]
hoelzl@38656
   460
      guess k::nat .. note k = this
hoelzl@38656
   461
      { fix i assume "i < DIM('a)"
hoelzl@38656
   462
        then have "-x$$i < real k"
hoelzl@38656
   463
          using k by (subst (asm) Max_less_iff) auto
hoelzl@38656
   464
        then have "- real k < x$$i" by simp }
hoelzl@38656
   465
      then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> -real k < x $$ ia"
hoelzl@38656
   466
        by (auto intro!: exI[of _ k])
hoelzl@38656
   467
    qed
hoelzl@38656
   468
    finally show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
hoelzl@38656
   469
      apply (simp only:)
hoelzl@38656
   470
      apply (safe intro!: countable_UN Diff)
hoelzl@38656
   471
      by (auto simp: sets_sigma intro!: sigma_sets.Basic)
hoelzl@38656
   472
  next
hoelzl@38656
   473
    assume "\<not> i < DIM('a)"
hoelzl@38656
   474
    then show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
hoelzl@38656
   475
      using top by auto
hoelzl@38656
   476
  qed
hoelzl@38656
   477
qed auto
hoelzl@38656
   478
hoelzl@38656
   479
lemma atMost_span_atLeastAtMost:
hoelzl@38656
   480
  "sets (sigma UNIV (range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space}))) \<subseteq>
hoelzl@38656
   481
   sets (sigma UNIV (range (\<lambda>(a,b). {a..b})))"
hoelzl@38656
   482
  (is "_ \<subseteq> sets ?SIGMA")
hoelzl@38656
   483
proof (rule sigma_algebra.sets_sigma_subset, safe)
hoelzl@38656
   484
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
hoelzl@38656
   485
  then interpret sigma_algebra ?SIGMA .
hoelzl@38656
   486
  fix a::'a
hoelzl@38656
   487
  have *: "{..a} = (\<Union>n::nat. {- real n *\<^sub>R One .. a})"
hoelzl@38656
   488
  proof (safe, simp_all add: eucl_le[where 'a='a])
hoelzl@38656
   489
    fix x
hoelzl@38656
   490
    from real_arch_simple[of "Max ((\<lambda>i. - x$$i)`{..<DIM('a)})"]
hoelzl@38656
   491
    guess k::nat .. note k = this
hoelzl@38656
   492
    { fix i assume "i < DIM('a)"
hoelzl@38656
   493
      with k have "- x$$i \<le> real k"
hoelzl@38656
   494
        by (subst (asm) Max_le_iff) (auto simp: field_simps)
hoelzl@38656
   495
      then have "- real k \<le> x$$i" by simp }
hoelzl@38656
   496
    then show "\<exists>n::nat. \<forall>i<DIM('a). - real n \<le> x $$ i"
hoelzl@38656
   497
      by (auto intro!: exI[of _ k])
hoelzl@38656
   498
  qed
hoelzl@38656
   499
  show "{..a} \<in> sets ?SIGMA" unfolding *
hoelzl@38656
   500
    by (safe intro!: countable_UN)
hoelzl@38656
   501
       (auto simp: sets_sigma intro!: sigma_sets.Basic)
hoelzl@38656
   502
qed auto
hoelzl@38656
   503
hoelzl@38656
   504
lemma borel_space_eq_greaterThanLessThan:
hoelzl@38656
   505
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a, b). {a <..< (b :: 'a \<Colon> ordered_euclidean_space)})))"
hoelzl@38656
   506
    (is "_ = sets ?SIGMA")
hoelzl@38656
   507
proof (rule antisym)
hoelzl@38656
   508
  show "sets ?SIGMA \<subseteq> sets borel_space"
hoelzl@38656
   509
    by (rule borel_space.sets_sigma_subset) auto
hoelzl@38656
   510
  show "sets borel_space \<subseteq> sets ?SIGMA"
hoelzl@38656
   511
    unfolding borel_space_def
hoelzl@38656
   512
  proof (rule sigma_algebra.sets_sigma_subset, safe)
hoelzl@38656
   513
    show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
hoelzl@38656
   514
    then interpret sigma_algebra ?SIGMA .
hoelzl@38656
   515
    fix M :: "'a set" assume "M \<in> open"
hoelzl@38656
   516
    then have "open M" by (simp add: mem_def)
hoelzl@38656
   517
    show "M \<in> sets ?SIGMA"
hoelzl@38656
   518
      apply (subst open_UNION[OF `open M`])
hoelzl@38656
   519
      apply (safe intro!: countable_UN)
hoelzl@38656
   520
      by (auto simp add: sigma_def intro!: sigma_sets.Basic)
hoelzl@38656
   521
  qed auto
hoelzl@38656
   522
qed
hoelzl@38656
   523
hoelzl@38656
   524
lemma borel_space_eq_atMost:
hoelzl@38656
   525
  "sets borel_space = sets (sigma UNIV (range (\<lambda> a. {.. a::'a\<Colon>ordered_euclidean_space})))"
hoelzl@38656
   526
    (is "_ = sets ?SIGMA")
hoelzl@38656
   527
proof (rule antisym)
hoelzl@38656
   528
  show "sets borel_space \<subseteq> sets ?SIGMA"
hoelzl@38656
   529
    using halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace
hoelzl@38656
   530
    by auto
hoelzl@38656
   531
  show "sets ?SIGMA \<subseteq> sets borel_space"
hoelzl@38656
   532
    by (rule borel_space.sets_sigma_subset) auto
hoelzl@38656
   533
qed
hoelzl@38656
   534
hoelzl@38656
   535
lemma borel_space_eq_atLeastAtMost:
hoelzl@38656
   536
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space, b). {a .. b})))"
hoelzl@38656
   537
   (is "_ = sets ?SIGMA")
hoelzl@38656
   538
proof (rule antisym)
hoelzl@38656
   539
  show "sets borel_space \<subseteq> sets ?SIGMA"
hoelzl@38656
   540
    using atMost_span_atLeastAtMost halfspace_le_span_atMost
hoelzl@38656
   541
      halfspace_span_halfspace_le open_span_halfspace
hoelzl@38656
   542
    by auto
hoelzl@38656
   543
  show "sets ?SIGMA \<subseteq> sets borel_space"
hoelzl@38656
   544
    by (rule borel_space.sets_sigma_subset) auto
hoelzl@38656
   545
qed
hoelzl@38656
   546
hoelzl@38656
   547
lemma borel_space_eq_greaterThan:
hoelzl@38656
   548
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space). {a <..})))"
hoelzl@38656
   549
   (is "_ = sets ?SIGMA")
hoelzl@38656
   550
proof (rule antisym)
hoelzl@38656
   551
  show "sets borel_space \<subseteq> sets ?SIGMA"
hoelzl@38656
   552
    using halfspace_le_span_greaterThan
hoelzl@38656
   553
      halfspace_span_halfspace_le open_span_halfspace
hoelzl@38656
   554
    by auto
hoelzl@38656
   555
  show "sets ?SIGMA \<subseteq> sets borel_space"
hoelzl@38656
   556
    by (rule borel_space.sets_sigma_subset) auto
hoelzl@38656
   557
qed
hoelzl@38656
   558
hoelzl@38656
   559
lemma borel_space_eq_halfspace_le:
hoelzl@38656
   560
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i \<le> a})))"
hoelzl@38656
   561
   (is "_ = sets ?SIGMA")
hoelzl@38656
   562
proof (rule antisym)
hoelzl@38656
   563
  show "sets borel_space \<subseteq> sets ?SIGMA"
hoelzl@38656
   564
    using open_span_halfspace halfspace_span_halfspace_le by auto
hoelzl@38656
   565
  show "sets ?SIGMA \<subseteq> sets borel_space"
hoelzl@38656
   566
    by (rule borel_space.sets_sigma_subset) auto
hoelzl@38656
   567
qed
hoelzl@38656
   568
hoelzl@38656
   569
lemma borel_space_eq_halfspace_less:
hoelzl@38656
   570
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i < a})))"
hoelzl@38656
   571
   (is "_ = sets ?SIGMA")
hoelzl@38656
   572
proof (rule antisym)
hoelzl@38656
   573
  show "sets borel_space \<subseteq> sets ?SIGMA"
hoelzl@38656
   574
    using open_span_halfspace .
hoelzl@38656
   575
  show "sets ?SIGMA \<subseteq> sets borel_space"
hoelzl@38656
   576
    by (rule borel_space.sets_sigma_subset) auto
hoelzl@38656
   577
qed
hoelzl@38656
   578
hoelzl@38656
   579
lemma borel_space_eq_halfspace_gt:
hoelzl@38656
   580
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a < x$$i})))"
hoelzl@38656
   581
   (is "_ = sets ?SIGMA")
hoelzl@38656
   582
proof (rule antisym)
hoelzl@38656
   583
  show "sets borel_space \<subseteq> sets ?SIGMA"
hoelzl@38656
   584
    using halfspace_le_span_halfspace_gt open_span_halfspace halfspace_span_halfspace_le by auto
hoelzl@38656
   585
  show "sets ?SIGMA \<subseteq> sets borel_space"
hoelzl@38656
   586
    by (rule borel_space.sets_sigma_subset) auto
hoelzl@38656
   587
qed
hoelzl@38656
   588
hoelzl@38656
   589
lemma borel_space_eq_halfspace_ge:
hoelzl@38656
   590
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a \<le> x$$i})))"
hoelzl@38656
   591
   (is "_ = sets ?SIGMA")
hoelzl@38656
   592
proof (rule antisym)
hoelzl@38656
   593
  show "sets borel_space \<subseteq> sets ?SIGMA"
hoelzl@38656
   594
    using halfspace_span_halfspace_ge open_span_halfspace by auto
hoelzl@38656
   595
  show "sets ?SIGMA \<subseteq> sets borel_space"
hoelzl@38656
   596
    by (rule borel_space.sets_sigma_subset) auto
hoelzl@38656
   597
qed
hoelzl@38656
   598
hoelzl@38656
   599
lemma (in sigma_algebra) borel_measurable_halfspacesI:
hoelzl@38656
   600
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
hoelzl@38656
   601
  assumes "sets borel_space = sets (sigma UNIV (range F))"
hoelzl@38656
   602
  and "\<And>a i. S a i = f -` F (a,i) \<inter> space M"
hoelzl@38656
   603
  and "\<And>a i. \<not> i < DIM('c) \<Longrightarrow> S a i \<in> sets M"
hoelzl@38656
   604
  shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a::real. S a i \<in> sets M)"
hoelzl@38656
   605
proof safe
hoelzl@38656
   606
  fix a :: real and i assume i: "i < DIM('c)" and f: "f \<in> borel_measurable M"
hoelzl@38656
   607
  then show "S a i \<in> sets M" unfolding assms
hoelzl@38656
   608
    by (auto intro!: measurable_sets sigma_sets.Basic simp: assms(1) sigma_def)
hoelzl@38656
   609
next
hoelzl@38656
   610
  assume a: "\<forall>i<DIM('c). \<forall>a. S a i \<in> sets M"
hoelzl@38656
   611
  { fix a i have "S a i \<in> sets M"
hoelzl@38656
   612
    proof cases
hoelzl@38656
   613
      assume "i < DIM('c)"
hoelzl@38656
   614
      with a show ?thesis unfolding assms(2) by simp
hoelzl@38656
   615
    next
hoelzl@38656
   616
      assume "\<not> i < DIM('c)"
hoelzl@38656
   617
      from assms(3)[OF this] show ?thesis .
hoelzl@38656
   618
    qed }
hoelzl@38656
   619
  then have "f \<in> measurable M (sigma UNIV (range F))"
hoelzl@38656
   620
    by (auto intro!: measurable_sigma simp: assms(2))
hoelzl@38656
   621
  then show "f \<in> borel_measurable M" unfolding measurable_def
hoelzl@38656
   622
    unfolding assms(1) by simp
hoelzl@38656
   623
qed
hoelzl@38656
   624
hoelzl@38656
   625
lemma (in sigma_algebra) borel_measurable_iff_halfspace_le:
hoelzl@38656
   626
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
hoelzl@38656
   627
  shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. f w $$ i \<le> a} \<in> sets M)"
hoelzl@38656
   628
  by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_le]) auto
hoelzl@38656
   629
hoelzl@38656
   630
lemma (in sigma_algebra) borel_measurable_iff_halfspace_less:
hoelzl@38656
   631
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
hoelzl@38656
   632
  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. f w $$ i < a} \<in> sets M)"
hoelzl@38656
   633
  by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_less]) auto
hoelzl@38656
   634
hoelzl@38656
   635
lemma (in sigma_algebra) borel_measurable_iff_halfspace_ge:
hoelzl@38656
   636
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
hoelzl@38656
   637
  shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. a \<le> f w $$ i} \<in> sets M)"
hoelzl@38656
   638
  by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_ge]) auto
hoelzl@38656
   639
hoelzl@38656
   640
lemma (in sigma_algebra) borel_measurable_iff_halfspace_greater:
hoelzl@38656
   641
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
hoelzl@38656
   642
  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. a < f w $$ i} \<in> sets M)"
hoelzl@38656
   643
  by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_gt]) auto
hoelzl@38656
   644
hoelzl@38656
   645
lemma (in sigma_algebra) borel_measurable_iff_le:
hoelzl@38656
   646
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)"
hoelzl@38656
   647
  using borel_measurable_iff_halfspace_le[where 'c=real] by simp
hoelzl@38656
   648
hoelzl@38656
   649
lemma (in sigma_algebra) borel_measurable_iff_less:
hoelzl@38656
   650
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)"
hoelzl@38656
   651
  using borel_measurable_iff_halfspace_less[where 'c=real] by simp
hoelzl@38656
   652
hoelzl@38656
   653
lemma (in sigma_algebra) borel_measurable_iff_ge:
hoelzl@38656
   654
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)"
hoelzl@38656
   655
  using borel_measurable_iff_halfspace_ge[where 'c=real] by simp
hoelzl@38656
   656
hoelzl@38656
   657
lemma (in sigma_algebra) borel_measurable_iff_greater:
hoelzl@38656
   658
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
hoelzl@38656
   659
  using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
hoelzl@38656
   660
hoelzl@38656
   661
subsection "Borel measurable operators"
hoelzl@38656
   662
hoelzl@38656
   663
lemma (in sigma_algebra) affine_borel_measurable_vector:
hoelzl@38656
   664
  fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
hoelzl@38656
   665
  assumes "f \<in> borel_measurable M"
hoelzl@38656
   666
  shows "(\<lambda>x. a + b *\<^sub>R f x) \<in> borel_measurable M"
hoelzl@38656
   667
proof (rule borel_measurableI)
hoelzl@38656
   668
  fix S :: "'x set" assume "open S"
hoelzl@38656
   669
  show "(\<lambda>x. a + b *\<^sub>R f x) -` S \<inter> space M \<in> sets M"
hoelzl@38656
   670
  proof cases
hoelzl@38656
   671
    assume "b \<noteq> 0"
hoelzl@38656
   672
    with `open S` have "((\<lambda>x. (- a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open")
hoelzl@38656
   673
      by (auto intro!: open_affinity simp: scaleR.add_right mem_def)
hoelzl@38656
   674
    hence "?S \<in> sets borel_space"
hoelzl@38656
   675
      unfolding borel_space_def by (auto simp: sigma_def intro!: sigma_sets.Basic)
hoelzl@38656
   676
    moreover
hoelzl@38656
   677
    from `b \<noteq> 0` have "(\<lambda>x. a + b *\<^sub>R f x) -` S = f -` ?S"
hoelzl@38656
   678
      apply auto by (rule_tac x="a + b *\<^sub>R f x" in image_eqI, simp_all)
hoelzl@38656
   679
    ultimately show ?thesis using assms unfolding in_borel_measurable_borel_space
hoelzl@38656
   680
      by auto
hoelzl@38656
   681
  qed simp
hoelzl@38656
   682
qed
hoelzl@38656
   683
hoelzl@38656
   684
lemma (in sigma_algebra) affine_borel_measurable:
hoelzl@38656
   685
  fixes g :: "'a \<Rightarrow> real"
hoelzl@38656
   686
  assumes g: "g \<in> borel_measurable M"
hoelzl@38656
   687
  shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
hoelzl@38656
   688
  using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute)
hoelzl@38656
   689
hoelzl@38656
   690
lemma (in sigma_algebra) borel_measurable_add[simp, intro]:
hoelzl@38656
   691
  fixes f :: "'a \<Rightarrow> real"
paulson@33533
   692
  assumes f: "f \<in> borel_measurable M"
paulson@33533
   693
  assumes g: "g \<in> borel_measurable M"
paulson@33533
   694
  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
paulson@33533
   695
proof -
hoelzl@38656
   696
  have 1: "\<And>a. {w\<in>space M. a \<le> f w + g w} = {w \<in> space M. a + g w * -1 \<le> f w}"
paulson@33533
   697
    by auto
hoelzl@38656
   698
  have "\<And>a. (\<lambda>w. a + (g w) * -1) \<in> borel_measurable M"
hoelzl@38656
   699
    by (rule affine_borel_measurable [OF g])
hoelzl@38656
   700
  then have "\<And>a. {w \<in> space M. (\<lambda>w. a + (g w) * -1)(w) \<le> f w} \<in> sets M" using f
hoelzl@38656
   701
    by auto
hoelzl@38656
   702
  then have "\<And>a. {w \<in> space M. a \<le> f w + g w} \<in> sets M"
hoelzl@38656
   703
    by (simp add: 1)
hoelzl@38656
   704
  then show ?thesis
hoelzl@38656
   705
    by (simp add: borel_measurable_iff_ge)
paulson@33533
   706
qed
paulson@33533
   707
hoelzl@38656
   708
lemma (in sigma_algebra) borel_measurable_square:
hoelzl@38656
   709
  fixes f :: "'a \<Rightarrow> real"
paulson@33533
   710
  assumes f: "f \<in> borel_measurable M"
paulson@33533
   711
  shows "(\<lambda>x. (f x)^2) \<in> borel_measurable M"
paulson@33533
   712
proof -
paulson@33533
   713
  {
paulson@33533
   714
    fix a
paulson@33533
   715
    have "{w \<in> space M. (f w)\<twosuperior> \<le> a} \<in> sets M"
paulson@33533
   716
    proof (cases rule: linorder_cases [of a 0])
paulson@33533
   717
      case less
hoelzl@38656
   718
      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = {}"
paulson@33533
   719
        by auto (metis less order_le_less_trans power2_less_0)
paulson@33533
   720
      also have "... \<in> sets M"
hoelzl@38656
   721
        by (rule empty_sets)
paulson@33533
   722
      finally show ?thesis .
paulson@33533
   723
    next
paulson@33533
   724
      case equal
hoelzl@38656
   725
      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
paulson@33533
   726
             {w \<in> space M. f w \<le> 0} \<inter> {w \<in> space M. 0 \<le> f w}"
paulson@33533
   727
        by auto
paulson@33533
   728
      also have "... \<in> sets M"
hoelzl@38656
   729
        apply (insert f)
hoelzl@38656
   730
        apply (rule Int)
hoelzl@38656
   731
        apply (simp add: borel_measurable_iff_le)
hoelzl@38656
   732
        apply (simp add: borel_measurable_iff_ge)
paulson@33533
   733
        done
paulson@33533
   734
      finally show ?thesis .
paulson@33533
   735
    next
paulson@33533
   736
      case greater
paulson@33533
   737
      have "\<forall>x. (f x ^ 2 \<le> sqrt a ^ 2) = (- sqrt a  \<le> f x & f x \<le> sqrt a)"
paulson@33533
   738
        by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs
paulson@33533
   739
                  real_sqrt_le_iff real_sqrt_power)
paulson@33533
   740
      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
hoelzl@38656
   741
             {w \<in> space M. -(sqrt a) \<le> f w} \<inter> {w \<in> space M. f w \<le> sqrt a}"
paulson@33533
   742
        using greater by auto
paulson@33533
   743
      also have "... \<in> sets M"
hoelzl@38656
   744
        apply (insert f)
hoelzl@38656
   745
        apply (rule Int)
hoelzl@38656
   746
        apply (simp add: borel_measurable_iff_ge)
hoelzl@38656
   747
        apply (simp add: borel_measurable_iff_le)
paulson@33533
   748
        done
paulson@33533
   749
      finally show ?thesis .
paulson@33533
   750
    qed
paulson@33533
   751
  }
hoelzl@38656
   752
  thus ?thesis by (auto simp add: borel_measurable_iff_le)
paulson@33533
   753
qed
paulson@33533
   754
paulson@33533
   755
lemma times_eq_sum_squares:
paulson@33533
   756
   fixes x::real
paulson@33533
   757
   shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4"
hoelzl@38656
   758
by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric])
paulson@33533
   759
hoelzl@38656
   760
lemma (in sigma_algebra) borel_measurable_uminus[simp, intro]:
hoelzl@38656
   761
  fixes g :: "'a \<Rightarrow> real"
paulson@33533
   762
  assumes g: "g \<in> borel_measurable M"
paulson@33533
   763
  shows "(\<lambda>x. - g x) \<in> borel_measurable M"
paulson@33533
   764
proof -
paulson@33533
   765
  have "(\<lambda>x. - g x) = (\<lambda>x. 0 + (g x) * -1)"
paulson@33533
   766
    by simp
hoelzl@38656
   767
  also have "... \<in> borel_measurable M"
hoelzl@38656
   768
    by (fast intro: affine_borel_measurable g)
paulson@33533
   769
  finally show ?thesis .
paulson@33533
   770
qed
paulson@33533
   771
hoelzl@38656
   772
lemma (in sigma_algebra) borel_measurable_times[simp, intro]:
hoelzl@38656
   773
  fixes f :: "'a \<Rightarrow> real"
paulson@33533
   774
  assumes f: "f \<in> borel_measurable M"
paulson@33533
   775
  assumes g: "g \<in> borel_measurable M"
paulson@33533
   776
  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
paulson@33533
   777
proof -
paulson@33533
   778
  have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M"
hoelzl@38656
   779
    using assms by (fast intro: affine_borel_measurable borel_measurable_square)
hoelzl@38656
   780
  have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) =
paulson@33533
   781
        (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
hoelzl@35582
   782
    by (simp add: minus_divide_right)
hoelzl@38656
   783
  also have "... \<in> borel_measurable M"
hoelzl@38656
   784
    using f g by (fast intro: affine_borel_measurable borel_measurable_square f g)
paulson@33533
   785
  finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
paulson@33533
   786
  show ?thesis
hoelzl@38656
   787
    apply (simp add: times_eq_sum_squares diff_minus)
hoelzl@38656
   788
    using 1 2 by simp
paulson@33533
   789
qed
paulson@33533
   790
hoelzl@38656
   791
lemma (in sigma_algebra) borel_measurable_diff[simp, intro]:
hoelzl@38656
   792
  fixes f :: "'a \<Rightarrow> real"
paulson@33533
   793
  assumes f: "f \<in> borel_measurable M"
paulson@33533
   794
  assumes g: "g \<in> borel_measurable M"
paulson@33533
   795
  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
hoelzl@38656
   796
  unfolding diff_minus using assms by fast
paulson@33533
   797
hoelzl@38656
   798
lemma (in sigma_algebra) borel_measurable_setsum[simp, intro]:
hoelzl@38656
   799
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
hoelzl@38656
   800
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
hoelzl@38656
   801
  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
hoelzl@38656
   802
proof cases
hoelzl@38656
   803
  assume "finite S"
hoelzl@38656
   804
  thus ?thesis using assms by induct auto
hoelzl@38656
   805
qed simp
hoelzl@35692
   806
hoelzl@38656
   807
lemma (in sigma_algebra) borel_measurable_inverse[simp, intro]:
hoelzl@38656
   808
  fixes f :: "'a \<Rightarrow> real"
hoelzl@35692
   809
  assumes "f \<in> borel_measurable M"
hoelzl@35692
   810
  shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
hoelzl@38656
   811
  unfolding borel_measurable_iff_ge unfolding inverse_eq_divide
hoelzl@38656
   812
proof safe
hoelzl@38656
   813
  fix a :: real
hoelzl@38656
   814
  have *: "{w \<in> space M. a \<le> 1 / f w} =
hoelzl@38656
   815
      ({w \<in> space M. 0 < f w} \<inter> {w \<in> space M. a * f w \<le> 1}) \<union>
hoelzl@38656
   816
      ({w \<in> space M. f w < 0} \<inter> {w \<in> space M. 1 \<le> a * f w}) \<union>
hoelzl@38656
   817
      ({w \<in> space M. f w = 0} \<inter> {w \<in> space M. a \<le> 0})" by (auto simp: le_divide_eq)
hoelzl@38656
   818
  show "{w \<in> space M. a \<le> 1 / f w} \<in> sets M" using assms unfolding *
hoelzl@38656
   819
    by (auto intro!: Int Un)
hoelzl@35692
   820
qed
hoelzl@35692
   821
hoelzl@38656
   822
lemma (in sigma_algebra) borel_measurable_divide[simp, intro]:
hoelzl@38656
   823
  fixes f :: "'a \<Rightarrow> real"
hoelzl@35692
   824
  assumes "f \<in> borel_measurable M"
hoelzl@35692
   825
  and "g \<in> borel_measurable M"
hoelzl@35692
   826
  shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
hoelzl@35692
   827
  unfolding field_divide_inverse
hoelzl@38656
   828
  by (rule borel_measurable_inverse borel_measurable_times assms)+
hoelzl@38656
   829
hoelzl@38656
   830
lemma (in sigma_algebra) borel_measurable_max[intro, simp]:
hoelzl@38656
   831
  fixes f g :: "'a \<Rightarrow> real"
hoelzl@38656
   832
  assumes "f \<in> borel_measurable M"
hoelzl@38656
   833
  assumes "g \<in> borel_measurable M"
hoelzl@38656
   834
  shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
hoelzl@38656
   835
  unfolding borel_measurable_iff_le
hoelzl@38656
   836
proof safe
hoelzl@38656
   837
  fix a
hoelzl@38656
   838
  have "{x \<in> space M. max (g x) (f x) \<le> a} =
hoelzl@38656
   839
    {x \<in> space M. g x \<le> a} \<inter> {x \<in> space M. f x \<le> a}" by auto
hoelzl@38656
   840
  thus "{x \<in> space M. max (g x) (f x) \<le> a} \<in> sets M"
hoelzl@38656
   841
    using assms unfolding borel_measurable_iff_le
hoelzl@38656
   842
    by (auto intro!: Int)
hoelzl@38656
   843
qed
hoelzl@38656
   844
hoelzl@38656
   845
lemma (in sigma_algebra) borel_measurable_min[intro, simp]:
hoelzl@38656
   846
  fixes f g :: "'a \<Rightarrow> real"
hoelzl@38656
   847
  assumes "f \<in> borel_measurable M"
hoelzl@38656
   848
  assumes "g \<in> borel_measurable M"
hoelzl@38656
   849
  shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
hoelzl@38656
   850
  unfolding borel_measurable_iff_ge
hoelzl@38656
   851
proof safe
hoelzl@38656
   852
  fix a
hoelzl@38656
   853
  have "{x \<in> space M. a \<le> min (g x) (f x)} =
hoelzl@38656
   854
    {x \<in> space M. a \<le> g x} \<inter> {x \<in> space M. a \<le> f x}" by auto
hoelzl@38656
   855
  thus "{x \<in> space M. a \<le> min (g x) (f x)} \<in> sets M"
hoelzl@38656
   856
    using assms unfolding borel_measurable_iff_ge
hoelzl@38656
   857
    by (auto intro!: Int)
hoelzl@38656
   858
qed
hoelzl@38656
   859
hoelzl@38656
   860
lemma (in sigma_algebra) borel_measurable_abs[simp, intro]:
hoelzl@38656
   861
  assumes "f \<in> borel_measurable M"
hoelzl@38656
   862
  shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
hoelzl@38656
   863
proof -
hoelzl@38656
   864
  have *: "\<And>x. \<bar>f x\<bar> = max 0 (f x) + max 0 (- f x)" by (simp add: max_def)
hoelzl@38656
   865
  show ?thesis unfolding * using assms by auto
hoelzl@38656
   866
qed
hoelzl@38656
   867
hoelzl@38656
   868
section "Borel space over the real line with infinity"
hoelzl@35692
   869
hoelzl@38656
   870
lemma borel_space_Real_measurable:
hoelzl@38656
   871
  "A \<in> sets borel_space \<Longrightarrow> Real -` A \<in> sets borel_space"
hoelzl@38656
   872
proof (rule borel_measurable_translate)
hoelzl@38656
   873
  fix B :: "pinfreal set" assume "open B"
hoelzl@38656
   874
  then obtain T x where T: "open T" "Real ` (T \<inter> {0..}) = B - {\<omega>}" and
hoelzl@38656
   875
    x: "\<omega> \<in> B \<Longrightarrow> 0 \<le> x" "\<omega> \<in> B \<Longrightarrow> {Real x <..} \<subseteq> B"
hoelzl@38656
   876
    unfolding open_pinfreal_def by blast
hoelzl@38656
   877
hoelzl@38656
   878
  have "Real -` B = Real -` (B - {\<omega>})" by auto
hoelzl@38656
   879
  also have "\<dots> = Real -` (Real ` (T \<inter> {0..}))" using T by simp
hoelzl@38656
   880
  also have "\<dots> = (if 0 \<in> T then T \<union> {.. 0} else T \<inter> {0..})"
hoelzl@38656
   881
    apply (auto simp add: Real_eq_Real image_iff)
hoelzl@38656
   882
    apply (rule_tac x="max 0 x" in bexI)
hoelzl@38656
   883
    by (auto simp: max_def)
hoelzl@38656
   884
  finally show "Real -` B \<in> sets borel_space"
hoelzl@38656
   885
    using `open T` by auto
hoelzl@38656
   886
qed simp
hoelzl@38656
   887
hoelzl@38656
   888
lemma borel_space_real_measurable:
hoelzl@38656
   889
  "A \<in> sets borel_space \<Longrightarrow> (real -` A :: pinfreal set) \<in> sets borel_space"
hoelzl@38656
   890
proof (rule borel_measurable_translate)
hoelzl@38656
   891
  fix B :: "real set" assume "open B"
hoelzl@38656
   892
  { fix x have "0 < real x \<longleftrightarrow> (\<exists>r>0. x = Real r)" by (cases x) auto }
hoelzl@38656
   893
  note Ex_less_real = this
hoelzl@38656
   894
  have *: "real -` B = (if 0 \<in> B then real -` (B \<inter> {0 <..}) \<union> {0, \<omega>} else real -` (B \<inter> {0 <..}))"
hoelzl@38656
   895
    by (force simp: Ex_less_real)
hoelzl@38656
   896
hoelzl@38656
   897
  have "open (real -` (B \<inter> {0 <..}) :: pinfreal set)"
hoelzl@38656
   898
    unfolding open_pinfreal_def using `open B`
hoelzl@38656
   899
    by (auto intro!: open_Int exI[of _ "B \<inter> {0 <..}"] simp: image_iff Ex_less_real)
hoelzl@38656
   900
  then show "(real -` B :: pinfreal set) \<in> sets borel_space" unfolding * by auto
hoelzl@38656
   901
qed simp
hoelzl@38656
   902
hoelzl@38656
   903
lemma (in sigma_algebra) borel_measurable_Real[intro, simp]:
hoelzl@38656
   904
  assumes "f \<in> borel_measurable M"
hoelzl@38656
   905
  shows "(\<lambda>x. Real (f x)) \<in> borel_measurable M"
hoelzl@38656
   906
  unfolding in_borel_measurable_borel_space
hoelzl@38656
   907
proof safe
hoelzl@38656
   908
  fix S :: "pinfreal set" assume "S \<in> sets borel_space"
hoelzl@38656
   909
  from borel_space_Real_measurable[OF this]
hoelzl@38656
   910
  have "(Real \<circ> f) -` S \<inter> space M \<in> sets M"
hoelzl@38656
   911
    using assms
hoelzl@38656
   912
    unfolding vimage_compose in_borel_measurable_borel_space
hoelzl@38656
   913
    by auto
hoelzl@38656
   914
  thus "(\<lambda>x. Real (f x)) -` S \<inter> space M \<in> sets M" by (simp add: comp_def)
hoelzl@35748
   915
qed
hoelzl@35692
   916
hoelzl@38656
   917
lemma (in sigma_algebra) borel_measurable_real[intro, simp]:
hoelzl@38656
   918
  fixes f :: "'a \<Rightarrow> pinfreal"
hoelzl@38656
   919
  assumes "f \<in> borel_measurable M"
hoelzl@38656
   920
  shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
hoelzl@38656
   921
  unfolding in_borel_measurable_borel_space
hoelzl@38656
   922
proof safe
hoelzl@38656
   923
  fix S :: "real set" assume "S \<in> sets borel_space"
hoelzl@38656
   924
  from borel_space_real_measurable[OF this]
hoelzl@38656
   925
  have "(real \<circ> f) -` S \<inter> space M \<in> sets M"
hoelzl@38656
   926
    using assms
hoelzl@38656
   927
    unfolding vimage_compose in_borel_measurable_borel_space
hoelzl@38656
   928
    by auto
hoelzl@38656
   929
  thus "(\<lambda>x. real (f x)) -` S \<inter> space M \<in> sets M" by (simp add: comp_def)
hoelzl@38656
   930
qed
hoelzl@35692
   931
hoelzl@38656
   932
lemma (in sigma_algebra) borel_measurable_Real_eq:
hoelzl@38656
   933
  assumes "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
hoelzl@38656
   934
  shows "(\<lambda>x. Real (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
hoelzl@38656
   935
proof
hoelzl@38656
   936
  have [simp]: "(\<lambda>x. Real (f x)) -` {\<omega>} \<inter> space M = {}"
hoelzl@38656
   937
    by auto
hoelzl@38656
   938
  assume "(\<lambda>x. Real (f x)) \<in> borel_measurable M"
hoelzl@38656
   939
  hence "(\<lambda>x. real (Real (f x))) \<in> borel_measurable M"
hoelzl@38656
   940
    by (rule borel_measurable_real)
hoelzl@38656
   941
  moreover have "\<And>x. x \<in> space M \<Longrightarrow> real (Real (f x)) = f x"
hoelzl@38656
   942
    using assms by auto
hoelzl@38656
   943
  ultimately show "f \<in> borel_measurable M"
hoelzl@38656
   944
    by (simp cong: measurable_cong)
hoelzl@38656
   945
qed auto
hoelzl@35692
   946
hoelzl@38656
   947
lemma (in sigma_algebra) borel_measurable_pinfreal_eq_real:
hoelzl@38656
   948
  "f \<in> borel_measurable M \<longleftrightarrow>
hoelzl@38656
   949
    ((\<lambda>x. real (f x)) \<in> borel_measurable M \<and> f -` {\<omega>} \<inter> space M \<in> sets M)"
hoelzl@38656
   950
proof safe
hoelzl@38656
   951
  assume "f \<in> borel_measurable M"
hoelzl@38656
   952
  then show "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f -` {\<omega>} \<inter> space M \<in> sets M"
hoelzl@38656
   953
    by (auto intro: borel_measurable_vimage borel_measurable_real)
hoelzl@38656
   954
next
hoelzl@38656
   955
  assume *: "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f -` {\<omega>} \<inter> space M \<in> sets M"
hoelzl@38656
   956
  have "f -` {\<omega>} \<inter> space M = {x\<in>space M. f x = \<omega>}" by auto
hoelzl@38656
   957
  with * have **: "{x\<in>space M. f x = \<omega>} \<in> sets M" by simp
hoelzl@38656
   958
  have f: "f = (\<lambda>x. if f x = \<omega> then \<omega> else Real (real (f x)))"
hoelzl@38656
   959
    by (simp add: expand_fun_eq Real_real)
hoelzl@38656
   960
  show "f \<in> borel_measurable M"
hoelzl@38656
   961
    apply (subst f)
hoelzl@38656
   962
    apply (rule measurable_If)
hoelzl@38656
   963
    using * ** by auto
hoelzl@38656
   964
qed
hoelzl@38656
   965
hoelzl@38656
   966
lemma (in sigma_algebra) less_eq_ge_measurable:
hoelzl@38656
   967
  fixes f :: "'a \<Rightarrow> 'c::linorder"
hoelzl@38656
   968
  shows "{x\<in>space M. a < f x} \<in> sets M \<longleftrightarrow> {x\<in>space M. f x \<le> a} \<in> sets M"
hoelzl@38656
   969
proof
hoelzl@38656
   970
  assume "{x\<in>space M. f x \<le> a} \<in> sets M"
hoelzl@38656
   971
  moreover have "{x\<in>space M. a < f x} = space M - {x\<in>space M. f x \<le> a}" by auto
hoelzl@38656
   972
  ultimately show "{x\<in>space M. a < f x} \<in> sets M" by auto
hoelzl@38656
   973
next
hoelzl@38656
   974
  assume "{x\<in>space M. a < f x} \<in> sets M"
hoelzl@38656
   975
  moreover have "{x\<in>space M. f x \<le> a} = space M - {x\<in>space M. a < f x}" by auto
hoelzl@38656
   976
  ultimately show "{x\<in>space M. f x \<le> a} \<in> sets M" by auto
hoelzl@38656
   977
qed
hoelzl@35692
   978
hoelzl@38656
   979
lemma (in sigma_algebra) greater_eq_le_measurable:
hoelzl@38656
   980
  fixes f :: "'a \<Rightarrow> 'c::linorder"
hoelzl@38656
   981
  shows "{x\<in>space M. f x < a} \<in> sets M \<longleftrightarrow> {x\<in>space M. a \<le> f x} \<in> sets M"
hoelzl@38656
   982
proof
hoelzl@38656
   983
  assume "{x\<in>space M. a \<le> f x} \<in> sets M"
hoelzl@38656
   984
  moreover have "{x\<in>space M. f x < a} = space M - {x\<in>space M. a \<le> f x}" by auto
hoelzl@38656
   985
  ultimately show "{x\<in>space M. f x < a} \<in> sets M" by auto
hoelzl@38656
   986
next
hoelzl@38656
   987
  assume "{x\<in>space M. f x < a} \<in> sets M"
hoelzl@38656
   988
  moreover have "{x\<in>space M. a \<le> f x} = space M - {x\<in>space M. f x < a}" by auto
hoelzl@38656
   989
  ultimately show "{x\<in>space M. a \<le> f x} \<in> sets M" by auto
hoelzl@38656
   990
qed
hoelzl@38656
   991
hoelzl@38656
   992
lemma (in sigma_algebra) less_eq_le_pinfreal_measurable:
hoelzl@38656
   993
  fixes f :: "'a \<Rightarrow> pinfreal"
hoelzl@38656
   994
  shows "(\<forall>a. {x\<in>space M. a < f x} \<in> sets M) \<longleftrightarrow> (\<forall>a. {x\<in>space M. a \<le> f x} \<in> sets M)"
hoelzl@38656
   995
proof
hoelzl@38656
   996
  assume a: "\<forall>a. {x\<in>space M. a \<le> f x} \<in> sets M"
hoelzl@38656
   997
  show "\<forall>a. {x \<in> space M. a < f x} \<in> sets M"
hoelzl@38656
   998
  proof
hoelzl@38656
   999
    fix a show "{x \<in> space M. a < f x} \<in> sets M"
hoelzl@38656
  1000
    proof (cases a)
hoelzl@38656
  1001
      case (preal r)
hoelzl@38656
  1002
      have "{x\<in>space M. a < f x} = (\<Union>i. {x\<in>space M. a + inverse (of_nat (Suc i)) \<le> f x})"
paulson@33533
  1003
      proof safe
hoelzl@38656
  1004
        fix x assume "a < f x" and [simp]: "x \<in> space M"
hoelzl@38656
  1005
        with ex_pinfreal_inverse_of_nat_Suc_less[of "f x - a"]
hoelzl@38656
  1006
        obtain n where "a + inverse (of_nat (Suc n)) < f x"
hoelzl@38656
  1007
          by (cases "f x", auto simp: pinfreal_minus_order)
hoelzl@38656
  1008
        then have "a + inverse (of_nat (Suc n)) \<le> f x" by simp
hoelzl@38656
  1009
        then show "x \<in> (\<Union>i. {x \<in> space M. a + inverse (of_nat (Suc i)) \<le> f x})"
paulson@33533
  1010
          by auto
paulson@33533
  1011
      next
hoelzl@38656
  1012
        fix i x assume [simp]: "x \<in> space M"
hoelzl@38656
  1013
        have "a < a + inverse (of_nat (Suc i))" using preal by auto
hoelzl@38656
  1014
        also assume "a + inverse (of_nat (Suc i)) \<le> f x"
hoelzl@38656
  1015
        finally show "a < f x" .
paulson@33533
  1016
      qed
hoelzl@38656
  1017
      with a show ?thesis by auto
hoelzl@38656
  1018
    qed simp
hoelzl@35582
  1019
  qed
hoelzl@35582
  1020
next
hoelzl@38656
  1021
  assume a': "\<forall>a. {x \<in> space M. a < f x} \<in> sets M"
hoelzl@38656
  1022
  then have a: "\<forall>a. {x \<in> space M. f x \<le> a} \<in> sets M" unfolding less_eq_ge_measurable .
hoelzl@38656
  1023
  show "\<forall>a. {x \<in> space M. a \<le> f x} \<in> sets M" unfolding greater_eq_le_measurable[symmetric]
hoelzl@38656
  1024
  proof
hoelzl@38656
  1025
    fix a show "{x \<in> space M. f x < a} \<in> sets M"
hoelzl@38656
  1026
    proof (cases a)
hoelzl@38656
  1027
      case (preal r)
hoelzl@38656
  1028
      show ?thesis
hoelzl@38656
  1029
      proof cases
hoelzl@38656
  1030
        assume "a = 0" then show ?thesis by simp
hoelzl@38656
  1031
      next
hoelzl@38656
  1032
        assume "a \<noteq> 0"
hoelzl@38656
  1033
        have "{x\<in>space M. f x < a} = (\<Union>i. {x\<in>space M. f x \<le> a - inverse (of_nat (Suc i))})"
hoelzl@38656
  1034
        proof safe
hoelzl@38656
  1035
          fix x assume "f x < a" and [simp]: "x \<in> space M"
hoelzl@38656
  1036
          with ex_pinfreal_inverse_of_nat_Suc_less[of "a - f x"]
hoelzl@38656
  1037
          obtain n where "inverse (of_nat (Suc n)) < a - f x"
hoelzl@38656
  1038
            using preal by (cases "f x") auto
hoelzl@38656
  1039
          then have "f x \<le> a - inverse (of_nat (Suc n)) "
hoelzl@38656
  1040
            using preal by (cases "f x") (auto split: split_if_asm)
hoelzl@38656
  1041
          then show "x \<in> (\<Union>i. {x \<in> space M. f x \<le> a - inverse (of_nat (Suc i))})"
hoelzl@38656
  1042
            by auto
hoelzl@38656
  1043
        next
hoelzl@38656
  1044
          fix i x assume [simp]: "x \<in> space M"
hoelzl@38656
  1045
          assume "f x \<le> a - inverse (of_nat (Suc i))"
hoelzl@38656
  1046
          also have "\<dots> < a" using `a \<noteq> 0` preal by auto
hoelzl@38656
  1047
          finally show "f x < a" .
hoelzl@38656
  1048
        qed
hoelzl@38656
  1049
        with a show ?thesis by auto
hoelzl@38656
  1050
      qed
hoelzl@38656
  1051
    next
hoelzl@38656
  1052
      case infinite
hoelzl@38656
  1053
      have "f -` {\<omega>} \<inter> space M = (\<Inter>n. {x\<in>space M. of_nat n < f x})"
hoelzl@38656
  1054
      proof (safe, simp_all, safe)
hoelzl@38656
  1055
        fix x assume *: "\<forall>n::nat. Real (real n) < f x"
hoelzl@38656
  1056
        show "f x = \<omega>"    proof (rule ccontr)
hoelzl@38656
  1057
          assume "f x \<noteq> \<omega>"
hoelzl@38656
  1058
          with real_arch_lt[of "real (f x)"] obtain n where "f x < of_nat n"
hoelzl@38656
  1059
            by (auto simp: pinfreal_noteq_omega_Ex)
hoelzl@38656
  1060
          with *[THEN spec, of n] show False by auto
hoelzl@38656
  1061
        qed
hoelzl@38656
  1062
      qed
hoelzl@38656
  1063
      with a' have \<omega>: "f -` {\<omega>} \<inter> space M \<in> sets M" by auto
hoelzl@38656
  1064
      moreover have "{x \<in> space M. f x < a} = space M - f -` {\<omega>} \<inter> space M"
hoelzl@38656
  1065
        using infinite by auto
hoelzl@38656
  1066
      ultimately show ?thesis by auto
hoelzl@38656
  1067
    qed
hoelzl@35582
  1068
  qed
hoelzl@35582
  1069
qed
hoelzl@35582
  1070
hoelzl@38656
  1071
lemma (in sigma_algebra) borel_measurable_pinfreal_iff_greater:
hoelzl@38656
  1072
  "(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. a < f x} \<in> sets M)"
hoelzl@38656
  1073
proof safe
hoelzl@38656
  1074
  fix a assume f: "f \<in> borel_measurable M"
hoelzl@38656
  1075
  have "{x\<in>space M. a < f x} = f -` {a <..} \<inter> space M" by auto
hoelzl@38656
  1076
  with f show "{x\<in>space M. a < f x} \<in> sets M"
hoelzl@38656
  1077
    by (auto intro!: measurable_sets)
hoelzl@38656
  1078
next
hoelzl@38656
  1079
  assume *: "\<forall>a. {x\<in>space M. a < f x} \<in> sets M"
hoelzl@38656
  1080
  hence **: "\<forall>a. {x\<in>space M. f x < a} \<in> sets M"
hoelzl@38656
  1081
    unfolding less_eq_le_pinfreal_measurable
hoelzl@38656
  1082
    unfolding greater_eq_le_measurable .
hoelzl@35582
  1083
hoelzl@38656
  1084
  show "f \<in> borel_measurable M" unfolding borel_measurable_pinfreal_eq_real borel_measurable_iff_greater
hoelzl@38656
  1085
  proof safe
hoelzl@38656
  1086
    have "f -` {\<omega>} \<inter> space M = space M - {x\<in>space M. f x < \<omega>}" by auto
hoelzl@38656
  1087
    then show \<omega>: "f -` {\<omega>} \<inter> space M \<in> sets M" using ** by auto
hoelzl@35582
  1088
hoelzl@38656
  1089
    fix a
hoelzl@38656
  1090
    have "{w \<in> space M. a < real (f w)} =
hoelzl@38656
  1091
      (if 0 \<le> a then {w\<in>space M. Real a < f w} - (f -` {\<omega>} \<inter> space M) else space M)"
hoelzl@38656
  1092
    proof (split split_if, safe del: notI)
hoelzl@38656
  1093
      fix x assume "0 \<le> a"
hoelzl@38656
  1094
      { assume "a < real (f x)" then show "Real a < f x" "x \<notin> f -` {\<omega>} \<inter> space M"
hoelzl@38656
  1095
          using `0 \<le> a` by (cases "f x", auto) }
hoelzl@38656
  1096
      { assume "Real a < f x" "x \<notin> f -` {\<omega>}" then show "a < real (f x)"
hoelzl@38656
  1097
          using `0 \<le> a` by (cases "f x", auto) }
hoelzl@38656
  1098
    next
hoelzl@38656
  1099
      fix x assume "\<not> 0 \<le> a" then show "a < real (f x)" by (cases "f x") auto
hoelzl@38656
  1100
    qed
hoelzl@38656
  1101
    then show "{w \<in> space M. a < real (f w)} \<in> sets M"
hoelzl@38656
  1102
      using \<omega> * by (auto intro!: Diff)
hoelzl@35582
  1103
  qed
hoelzl@35582
  1104
qed
hoelzl@35582
  1105
hoelzl@38656
  1106
lemma (in sigma_algebra) borel_measurable_pinfreal_iff_less:
hoelzl@38656
  1107
  "(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. f x < a} \<in> sets M)"
hoelzl@38656
  1108
  using borel_measurable_pinfreal_iff_greater unfolding less_eq_le_pinfreal_measurable greater_eq_le_measurable .
hoelzl@38656
  1109
hoelzl@38656
  1110
lemma (in sigma_algebra) borel_measurable_pinfreal_iff_le:
hoelzl@38656
  1111
  "(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. f x \<le> a} \<in> sets M)"
hoelzl@38656
  1112
  using borel_measurable_pinfreal_iff_greater unfolding less_eq_ge_measurable .
hoelzl@38656
  1113
hoelzl@38656
  1114
lemma (in sigma_algebra) borel_measurable_pinfreal_iff_ge:
hoelzl@38656
  1115
  "(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. a \<le> f x} \<in> sets M)"
hoelzl@38656
  1116
  using borel_measurable_pinfreal_iff_greater unfolding less_eq_le_pinfreal_measurable .
hoelzl@38656
  1117
hoelzl@38656
  1118
lemma (in sigma_algebra) borel_measurable_pinfreal_eq_const:
hoelzl@38656
  1119
  fixes f :: "'a \<Rightarrow> pinfreal" assumes "f \<in> borel_measurable M"
hoelzl@38656
  1120
  shows "{x\<in>space M. f x = c} \<in> sets M"
hoelzl@38656
  1121
proof -
hoelzl@38656
  1122
  have "{x\<in>space M. f x = c} = (f -` {c} \<inter> space M)" by auto
hoelzl@38656
  1123
  then show ?thesis using assms by (auto intro!: measurable_sets)
hoelzl@38656
  1124
qed
hoelzl@38656
  1125
hoelzl@38656
  1126
lemma (in sigma_algebra) borel_measurable_pinfreal_neq_const:
hoelzl@38656
  1127
  fixes f :: "'a \<Rightarrow> pinfreal"
hoelzl@38656
  1128
  assumes "f \<in> borel_measurable M"
hoelzl@38656
  1129
  shows "{x\<in>space M. f x \<noteq> c} \<in> sets M"
hoelzl@38656
  1130
proof -
hoelzl@38656
  1131
  have "{x\<in>space M. f x \<noteq> c} = space M - (f -` {c} \<inter> space M)" by auto
hoelzl@38656
  1132
  then show ?thesis using assms by (auto intro!: measurable_sets)
hoelzl@38656
  1133
qed
hoelzl@38656
  1134
hoelzl@38656
  1135
lemma (in sigma_algebra) borel_measurable_pinfreal_less[intro,simp]:
hoelzl@38656
  1136
  fixes f g :: "'a \<Rightarrow> pinfreal"
hoelzl@38656
  1137
  assumes f: "f \<in> borel_measurable M"
hoelzl@38656
  1138
  assumes g: "g \<in> borel_measurable M"
hoelzl@38656
  1139
  shows "{x \<in> space M. f x < g x} \<in> sets M"
hoelzl@38656
  1140
proof -
hoelzl@38656
  1141
  have "(\<lambda>x. real (f x)) \<in> borel_measurable M"
hoelzl@38656
  1142
    "(\<lambda>x. real (g x)) \<in> borel_measurable M"
hoelzl@38656
  1143
    using assms by (auto intro!: borel_measurable_real)
hoelzl@38656
  1144
  from borel_measurable_less[OF this]
hoelzl@38656
  1145
  have "{x \<in> space M. real (f x) < real (g x)} \<in> sets M" .
hoelzl@38656
  1146
  moreover have "{x \<in> space M. f x \<noteq> \<omega>} \<in> sets M" using f by (rule borel_measurable_pinfreal_neq_const)
hoelzl@38656
  1147
  moreover have "{x \<in> space M. g x = \<omega>} \<in> sets M" using g by (rule borel_measurable_pinfreal_eq_const)
hoelzl@38656
  1148
  moreover have "{x \<in> space M. g x \<noteq> \<omega>} \<in> sets M" using g by (rule borel_measurable_pinfreal_neq_const)
hoelzl@38656
  1149
  moreover have "{x \<in> space M. f x < g x} = ({x \<in> space M. g x = \<omega>} \<inter> {x \<in> space M. f x \<noteq> \<omega>}) \<union>
hoelzl@38656
  1150
    ({x \<in> space M. g x \<noteq> \<omega>} \<inter> {x \<in> space M. f x \<noteq> \<omega>} \<inter> {x \<in> space M. real (f x) < real (g x)})"
hoelzl@38656
  1151
    by (auto simp: real_of_pinfreal_strict_mono_iff)
hoelzl@38656
  1152
  ultimately show ?thesis by auto
hoelzl@38656
  1153
qed
hoelzl@38656
  1154
hoelzl@38656
  1155
lemma (in sigma_algebra) borel_measurable_pinfreal_le[intro,simp]:
hoelzl@38656
  1156
  fixes f :: "'a \<Rightarrow> pinfreal"
hoelzl@38656
  1157
  assumes f: "f \<in> borel_measurable M"
hoelzl@38656
  1158
  assumes g: "g \<in> borel_measurable M"
hoelzl@38656
  1159
  shows "{x \<in> space M. f x \<le> g x} \<in> sets M"
hoelzl@38656
  1160
proof -
hoelzl@38656
  1161
  have "{x \<in> space M. f x \<le> g x} = space M - {x \<in> space M. g x < f x}" by auto
hoelzl@38656
  1162
  then show ?thesis using g f by auto
hoelzl@38656
  1163
qed
hoelzl@38656
  1164
hoelzl@38656
  1165
lemma (in sigma_algebra) borel_measurable_pinfreal_eq[intro,simp]:
hoelzl@38656
  1166
  fixes f :: "'a \<Rightarrow> pinfreal"
hoelzl@38656
  1167
  assumes f: "f \<in> borel_measurable M"
hoelzl@38656
  1168
  assumes g: "g \<in> borel_measurable M"
hoelzl@38656
  1169
  shows "{w \<in> space M. f w = g w} \<in> sets M"
hoelzl@38656
  1170
proof -
hoelzl@38656
  1171
  have "{x \<in> space M. f x = g x} = {x \<in> space M. g x \<le> f x} \<inter> {x \<in> space M. f x \<le> g x}" by auto
hoelzl@38656
  1172
  then show ?thesis using g f by auto
hoelzl@38656
  1173
qed
hoelzl@38656
  1174
hoelzl@38656
  1175
lemma (in sigma_algebra) borel_measurable_pinfreal_neq[intro,simp]:
hoelzl@38656
  1176
  fixes f :: "'a \<Rightarrow> pinfreal"
hoelzl@38656
  1177
  assumes f: "f \<in> borel_measurable M"
hoelzl@38656
  1178
  assumes g: "g \<in> borel_measurable M"
hoelzl@38656
  1179
  shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
hoelzl@35692
  1180
proof -
hoelzl@38656
  1181
  have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}" by auto
hoelzl@38656
  1182
  thus ?thesis using f g by auto
hoelzl@38656
  1183
qed
hoelzl@38656
  1184
hoelzl@38656
  1185
lemma (in sigma_algebra) borel_measurable_pinfreal_add[intro, simp]:
hoelzl@38656
  1186
  fixes f :: "'a \<Rightarrow> pinfreal"
hoelzl@38656
  1187
  assumes measure: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
hoelzl@38656
  1188
  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
hoelzl@38656
  1189
proof -
hoelzl@38656
  1190
  have *: "(\<lambda>x. f x + g x) =
hoelzl@38656
  1191
     (\<lambda>x. if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else Real (real (f x) + real (g x)))"
hoelzl@38656
  1192
     by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex)
hoelzl@38656
  1193
  show ?thesis using assms unfolding *
hoelzl@38656
  1194
    by (auto intro!: measurable_If)
hoelzl@38656
  1195
qed
hoelzl@38656
  1196
hoelzl@38656
  1197
lemma (in sigma_algebra) borel_measurable_pinfreal_times[intro, simp]:
hoelzl@38656
  1198
  fixes f :: "'a \<Rightarrow> pinfreal" assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
hoelzl@38656
  1199
  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
hoelzl@38656
  1200
proof -
hoelzl@38656
  1201
  have *: "(\<lambda>x. f x * g x) =
hoelzl@38656
  1202
     (\<lambda>x. if f x = 0 then 0 else if g x = 0 then 0 else if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else
hoelzl@38656
  1203
      Real (real (f x) * real (g x)))"
hoelzl@38656
  1204
     by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex)
hoelzl@38656
  1205
  show ?thesis using assms unfolding *
hoelzl@38656
  1206
    by (auto intro!: measurable_If)
hoelzl@38656
  1207
qed
hoelzl@38656
  1208
hoelzl@38656
  1209
lemma (in sigma_algebra) borel_measurable_pinfreal_setsum[simp, intro]:
hoelzl@38656
  1210
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pinfreal"
hoelzl@38656
  1211
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
hoelzl@38656
  1212
  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
hoelzl@38656
  1213
proof cases
hoelzl@38656
  1214
  assume "finite S"
hoelzl@38656
  1215
  thus ?thesis using assms
hoelzl@38656
  1216
    by induct auto
hoelzl@38656
  1217
qed (simp add: borel_measurable_const)
hoelzl@38656
  1218
hoelzl@38656
  1219
lemma (in sigma_algebra) borel_measurable_pinfreal_min[intro, simp]:
hoelzl@38656
  1220
  fixes f g :: "'a \<Rightarrow> pinfreal"
hoelzl@38656
  1221
  assumes "f \<in> borel_measurable M"
hoelzl@38656
  1222
  assumes "g \<in> borel_measurable M"
hoelzl@38656
  1223
  shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
hoelzl@38656
  1224
  using assms unfolding min_def by (auto intro!: measurable_If)
hoelzl@38656
  1225
hoelzl@38656
  1226
lemma (in sigma_algebra) borel_measurable_pinfreal_max[intro]:
hoelzl@38656
  1227
  fixes f g :: "'a \<Rightarrow> pinfreal"
hoelzl@38656
  1228
  assumes "f \<in> borel_measurable M"
hoelzl@38656
  1229
  and "g \<in> borel_measurable M"
hoelzl@38656
  1230
  shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
hoelzl@38656
  1231
  using assms unfolding max_def by (auto intro!: measurable_If)
hoelzl@38656
  1232
hoelzl@38656
  1233
lemma (in sigma_algebra) borel_measurable_SUP[simp, intro]:
hoelzl@38656
  1234
  fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> pinfreal"
hoelzl@38656
  1235
  assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
hoelzl@38656
  1236
  shows "(SUP i : A. f i) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
hoelzl@38656
  1237
  unfolding borel_measurable_pinfreal_iff_greater
hoelzl@38656
  1238
proof safe
hoelzl@38656
  1239
  fix a
hoelzl@38656
  1240
  have "{x\<in>space M. a < ?sup x} = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
hoelzl@38656
  1241
    by (auto simp: less_Sup_iff SUPR_def[where 'a=pinfreal] SUPR_fun_expand[where 'b=pinfreal])
hoelzl@38656
  1242
  then show "{x\<in>space M. a < ?sup x} \<in> sets M"
hoelzl@38656
  1243
    using assms by auto
hoelzl@38656
  1244
qed
hoelzl@38656
  1245
hoelzl@38656
  1246
lemma (in sigma_algebra) borel_measurable_INF[simp, intro]:
hoelzl@38656
  1247
  fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> pinfreal"
hoelzl@38656
  1248
  assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
hoelzl@38656
  1249
  shows "(INF i : A. f i) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
hoelzl@38656
  1250
  unfolding borel_measurable_pinfreal_iff_less
hoelzl@38656
  1251
proof safe
hoelzl@38656
  1252
  fix a
hoelzl@38656
  1253
  have "{x\<in>space M. ?inf x < a} = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
hoelzl@38656
  1254
    by (auto simp: Inf_less_iff INFI_def[where 'a=pinfreal] INFI_fun_expand)
hoelzl@38656
  1255
  then show "{x\<in>space M. ?inf x < a} \<in> sets M"
hoelzl@38656
  1256
    using assms by auto
hoelzl@38656
  1257
qed
hoelzl@38656
  1258
hoelzl@38656
  1259
lemma (in sigma_algebra) borel_measurable_pinfreal_diff:
hoelzl@38656
  1260
  fixes f g :: "'a \<Rightarrow> pinfreal"
hoelzl@38656
  1261
  assumes "f \<in> borel_measurable M"
hoelzl@38656
  1262
  assumes "g \<in> borel_measurable M"
hoelzl@38656
  1263
  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
hoelzl@38656
  1264
  unfolding borel_measurable_pinfreal_iff_greater
hoelzl@38656
  1265
proof safe
hoelzl@38656
  1266
  fix a
hoelzl@38656
  1267
  have "{x \<in> space M. a < f x - g x} = {x \<in> space M. g x + a < f x}"
hoelzl@38656
  1268
    by (simp add: pinfreal_less_minus_iff)
hoelzl@38656
  1269
  then show "{x \<in> space M. a < f x - g x} \<in> sets M"
hoelzl@38656
  1270
    using assms by auto
hoelzl@35692
  1271
qed
hoelzl@35692
  1272
paulson@33533
  1273
end