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