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