1 (* Title: HOL/Probability/Borel_Space.thy
2 Author: Johannes Hölzl, TU München
3 Author: Armin Heller, TU München
6 header {*Borel spaces*}
9 imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
12 section "Generic Borel spaces"
14 definition borel :: "'a::topological_space measure" where
15 "borel = sigma UNIV {S. open S}"
17 abbreviation "borel_measurable M \<equiv> measurable M borel"
19 lemma in_borel_measurable:
20 "f \<in> borel_measurable M \<longleftrightarrow>
21 (\<forall>S \<in> sigma_sets UNIV {S. open S}. f -` S \<inter> space M \<in> sets M)"
22 by (auto simp add: measurable_def borel_def)
24 lemma in_borel_measurable_borel:
25 "f \<in> borel_measurable M \<longleftrightarrow>
26 (\<forall>S \<in> sets borel.
27 f -` S \<inter> space M \<in> sets M)"
28 by (auto simp add: measurable_def borel_def)
30 lemma space_borel[simp]: "space borel = UNIV"
31 unfolding borel_def by auto
33 lemma borel_open[simp]:
34 assumes "open A" shows "A \<in> sets borel"
36 have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
37 thus ?thesis unfolding borel_def by auto
40 lemma borel_closed[simp]:
41 assumes "closed A" shows "A \<in> sets borel"
43 have "space borel - (- A) \<in> sets borel"
44 using assms unfolding closed_def by (blast intro: borel_open)
48 lemma borel_comp[intro,simp]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
49 unfolding Compl_eq_Diff_UNIV by (intro Diff) auto
51 lemma borel_measurable_vimage:
52 fixes f :: "'a \<Rightarrow> 'x::t2_space"
53 assumes borel: "f \<in> borel_measurable M"
54 shows "f -` {x} \<inter> space M \<in> sets M"
55 proof (cases "x \<in> f ` space M")
56 case True then obtain y where "x = f y" by auto
57 from closed_singleton[of "f y"]
58 have "{f y} \<in> sets borel" by (rule borel_closed)
59 with assms show ?thesis
60 unfolding in_borel_measurable_borel `x = f y` by auto
62 case False hence "f -` {x} \<inter> space M = {}" by auto
66 lemma borel_measurableI:
67 fixes f :: "'a \<Rightarrow> 'x\<Colon>topological_space"
68 assumes "\<And>S. open S \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
69 shows "f \<in> borel_measurable M"
71 proof (rule measurable_measure_of, simp_all)
72 fix S :: "'x set" assume "open S" thus "f -` S \<inter> space M \<in> sets M"
73 using assms[of S] by simp
76 lemma borel_singleton[simp, intro]:
77 fixes x :: "'a::t1_space"
78 shows "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets borel"
79 proof (rule insert_in_sets)
80 show "{x} \<in> sets borel"
81 using closed_singleton[of x] by (rule borel_closed)
84 lemma borel_measurable_const[simp, intro]:
85 "(\<lambda>x. c) \<in> borel_measurable M"
88 lemma borel_measurable_indicator[simp, intro!]:
89 assumes A: "A \<in> sets M"
90 shows "indicator A \<in> borel_measurable M"
91 unfolding indicator_def [abs_def] using A
92 by (auto intro!: measurable_If_set)
94 lemma borel_measurable_indicator_iff:
95 "(indicator A :: 'a \<Rightarrow> 'x::{t1_space, zero_neq_one}) \<in> borel_measurable M \<longleftrightarrow> A \<inter> space M \<in> sets M"
96 (is "?I \<in> borel_measurable M \<longleftrightarrow> _")
98 assume "?I \<in> borel_measurable M"
99 then have "?I -` {1} \<inter> space M \<in> sets M"
100 unfolding measurable_def by auto
101 also have "?I -` {1} \<inter> space M = A \<inter> space M"
102 unfolding indicator_def [abs_def] by auto
103 finally show "A \<inter> space M \<in> sets M" .
105 assume "A \<inter> space M \<in> sets M"
106 moreover have "?I \<in> borel_measurable M \<longleftrightarrow>
107 (indicator (A \<inter> space M) :: 'a \<Rightarrow> 'x) \<in> borel_measurable M"
108 by (intro measurable_cong) (auto simp: indicator_def)
109 ultimately show "?I \<in> borel_measurable M" by auto
112 lemma borel_measurable_subalgebra:
113 assumes "sets N \<subseteq> sets M" "space N = space M" "f \<in> borel_measurable N"
114 shows "f \<in> borel_measurable M"
115 using assms unfolding measurable_def by auto
117 section "Borel spaces on euclidean spaces"
119 lemma lessThan_borel[simp, intro]:
120 fixes a :: "'a\<Colon>ordered_euclidean_space"
121 shows "{..< a} \<in> sets borel"
122 by (blast intro: borel_open)
124 lemma greaterThan_borel[simp, intro]:
125 fixes a :: "'a\<Colon>ordered_euclidean_space"
126 shows "{a <..} \<in> sets borel"
127 by (blast intro: borel_open)
129 lemma greaterThanLessThan_borel[simp, intro]:
130 fixes a b :: "'a\<Colon>ordered_euclidean_space"
131 shows "{a<..<b} \<in> sets borel"
132 by (blast intro: borel_open)
134 lemma atMost_borel[simp, intro]:
135 fixes a :: "'a\<Colon>ordered_euclidean_space"
136 shows "{..a} \<in> sets borel"
137 by (blast intro: borel_closed)
139 lemma atLeast_borel[simp, intro]:
140 fixes a :: "'a\<Colon>ordered_euclidean_space"
141 shows "{a..} \<in> sets borel"
142 by (blast intro: borel_closed)
144 lemma atLeastAtMost_borel[simp, intro]:
145 fixes a b :: "'a\<Colon>ordered_euclidean_space"
146 shows "{a..b} \<in> sets borel"
147 by (blast intro: borel_closed)
149 lemma greaterThanAtMost_borel[simp, intro]:
150 fixes a b :: "'a\<Colon>ordered_euclidean_space"
151 shows "{a<..b} \<in> sets borel"
152 unfolding greaterThanAtMost_def by blast
154 lemma atLeastLessThan_borel[simp, intro]:
155 fixes a b :: "'a\<Colon>ordered_euclidean_space"
156 shows "{a..<b} \<in> sets borel"
157 unfolding atLeastLessThan_def by blast
159 lemma hafspace_less_borel[simp, intro]:
161 shows "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
162 by (auto intro!: borel_open open_halfspace_component_gt)
164 lemma hafspace_greater_borel[simp, intro]:
166 shows "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
167 by (auto intro!: borel_open open_halfspace_component_lt)
169 lemma hafspace_less_eq_borel[simp, intro]:
171 shows "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
172 by (auto intro!: borel_closed closed_halfspace_component_ge)
174 lemma hafspace_greater_eq_borel[simp, intro]:
176 shows "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
177 by (auto intro!: borel_closed closed_halfspace_component_le)
179 lemma borel_measurable_less[simp, intro]:
180 fixes f :: "'a \<Rightarrow> real"
181 assumes f: "f \<in> borel_measurable M"
182 assumes g: "g \<in> borel_measurable M"
183 shows "{w \<in> space M. f w < g w} \<in> sets M"
185 have "{w \<in> space M. f w < g w} =
186 (\<Union>r. (f -` {..< of_rat r} \<inter> space M) \<inter> (g -` {of_rat r <..} \<inter> space M))"
187 using Rats_dense_in_real by (auto simp add: Rats_def)
188 then show ?thesis using f g
189 by simp (blast intro: measurable_sets)
192 lemma borel_measurable_le[simp, intro]:
193 fixes f :: "'a \<Rightarrow> real"
194 assumes f: "f \<in> borel_measurable M"
195 assumes g: "g \<in> borel_measurable M"
196 shows "{w \<in> space M. f w \<le> g w} \<in> sets M"
198 have "{w \<in> space M. f w \<le> g w} = space M - {w \<in> space M. g w < f w}"
200 thus ?thesis using f g
204 lemma borel_measurable_eq[simp, intro]:
205 fixes f :: "'a \<Rightarrow> real"
206 assumes f: "f \<in> borel_measurable M"
207 assumes g: "g \<in> borel_measurable M"
208 shows "{w \<in> space M. f w = g w} \<in> sets M"
210 have "{w \<in> space M. f w = g w} =
211 {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
213 thus ?thesis using f g by auto
216 lemma borel_measurable_neq[simp, intro]:
217 fixes f :: "'a \<Rightarrow> real"
218 assumes f: "f \<in> borel_measurable M"
219 assumes g: "g \<in> borel_measurable M"
220 shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
222 have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}"
224 thus ?thesis using f g by auto
227 subsection "Borel space equals sigma algebras over intervals"
229 lemma rational_boxes:
230 fixes x :: "'a\<Colon>ordered_euclidean_space"
232 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"
234 def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
235 then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos)
236 have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x $$ i \<and> x $$ i - y < e'" (is "\<forall>i. ?th i")
238 fix i from Rats_dense_in_real[of "x $$ i - e'" "x $$ i"] e
241 from choice[OF this] guess a .. note a = this
242 have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x $$ i < y \<and> y - x $$ i < e'" (is "\<forall>i. ?th i")
244 fix i from Rats_dense_in_real[of "x $$ i" "x $$ i + e'"] e
247 from choice[OF this] guess b .. note b = this
248 { fix y :: 'a assume *: "Chi a < y" "y < Chi b"
249 have "dist x y = sqrt (\<Sum>i<DIM('a). (dist (x $$ i) (y $$ i))\<twosuperior>)"
250 unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
251 also have "\<dots> < sqrt (\<Sum>i<DIM('a). e^2 / real (DIM('a)))"
252 proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
253 fix i assume i: "i \<in> {..<DIM('a)}"
254 have "a i < y$$i \<and> y$$i < b i" using * i eucl_less[where 'a='a] by auto
255 moreover have "a i < x$$i" "x$$i - a i < e'" using a by auto
256 moreover have "x$$i < b i" "b i - x$$i < e'" using b by auto
257 ultimately have "\<bar>x$$i - y$$i\<bar> < 2 * e'" by auto
258 then have "dist (x $$ i) (y $$ i) < e/sqrt (real (DIM('a)))"
259 unfolding e'_def by (auto simp: dist_real_def)
260 then have "(dist (x $$ i) (y $$ i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
261 by (rule power_strict_mono) auto
262 then show "(dist (x $$ i) (y $$ i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
263 by (simp add: power_divide)
265 also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive)
266 finally have "dist x y < e" . }
267 with a b show ?thesis
268 apply (rule_tac exI[of _ "Chi a"])
269 apply (rule_tac exI[of _ "Chi b"])
270 using eucl_less[where 'a='a] by auto
274 fixes x :: "'a\<Colon>ordered_euclidean_space"
275 assumes "\<And> i. x $$ i \<in> \<rat>"
276 shows "\<exists> r. length r = DIM('a) \<and> (\<forall> i < DIM('a). of_rat (r ! i) = x $$ i)"
278 have "\<forall>i. \<exists>r. x $$ i = of_rat r" using assms unfolding Rats_def by blast
279 from choice[OF this] guess r ..
280 then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"])
284 fixes M :: "'a\<Colon>ordered_euclidean_space set"
286 shows "M = UNION {(a, b) | a b. {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)} \<subseteq> M}
287 (\<lambda> (a, b). {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)})"
288 (is "M = UNION ?idx ?box")
290 fix x assume "x \<in> M"
291 obtain e where e: "e > 0" "ball x e \<subseteq> M"
292 using openE[OF assms `x \<in> M`] by auto
293 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"
294 using rational_boxes[OF e(1)] by blast
295 then obtain p q where pq: "length p = DIM ('a)"
296 "length q = DIM ('a)"
297 "\<forall> i < DIM ('a). of_rat (p ! i) = a $$ i \<and> of_rat (q ! i) = b $$ i"
298 using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast
299 hence p: "Chi (of_rat \<circ> op ! p) = a"
300 using euclidean_eq[of "Chi (of_rat \<circ> op ! p)" a]
301 unfolding o_def by auto
302 from pq have q: "Chi (of_rat \<circ> op ! q) = b"
303 using euclidean_eq[of "Chi (of_rat \<circ> op ! q)" b]
304 unfolding o_def by auto
305 have "x \<in> ?box (p, q)"
307 thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto
310 lemma borel_sigma_sets_subset:
311 "A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel"
312 using sigma_sets_subset[of A borel] by simp
314 lemma borel_eq_sigmaI1:
315 fixes F :: "'i \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
316 assumes borel_eq: "borel = sigma UNIV X"
317 assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV (range F))"
318 assumes F: "\<And>i. F i \<in> sets borel"
319 shows "borel = sigma UNIV (range F)"
321 proof (intro sigma_eqI antisym)
322 have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel"
323 unfolding borel_def by simp
324 also have "\<dots> = sigma_sets UNIV X"
325 unfolding borel_eq by simp
326 also have "\<dots> \<subseteq> sigma_sets UNIV (range F)"
327 using X by (intro sigma_algebra.sigma_sets_subset[OF sigma_algebra_sigma_sets]) auto
328 finally show "sigma_sets UNIV {S. open S} \<subseteq> sigma_sets UNIV (range F)" .
329 show "sigma_sets UNIV (range F) \<subseteq> sigma_sets UNIV {S. open S}"
330 unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto
333 lemma borel_eq_sigmaI2:
334 fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set"
335 and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set"
336 assumes borel_eq: "borel = sigma UNIV (range (\<lambda>(i, j). G i j))"
337 assumes X: "\<And>i j. G i j \<in> sets (sigma UNIV (range (\<lambda>(i, j). F i j)))"
338 assumes F: "\<And>i j. F i j \<in> sets borel"
339 shows "borel = sigma UNIV (range (\<lambda>(i, j). F i j))"
340 using assms by (intro borel_eq_sigmaI1[where X="range (\<lambda>(i, j). G i j)" and F="(\<lambda>(i, j). F i j)"]) auto
342 lemma borel_eq_sigmaI3:
343 fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
344 assumes borel_eq: "borel = sigma UNIV X"
345 assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV (range (\<lambda>(i, j). F i j)))"
346 assumes F: "\<And>i j. F i j \<in> sets borel"
347 shows "borel = sigma UNIV (range (\<lambda>(i, j). F i j))"
348 using assms by (intro borel_eq_sigmaI1[where X=X and F="(\<lambda>(i, j). F i j)"]) auto
350 lemma borel_eq_sigmaI4:
351 fixes F :: "'i \<Rightarrow> 'a::topological_space set"
352 and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set"
353 assumes borel_eq: "borel = sigma UNIV (range (\<lambda>(i, j). G i j))"
354 assumes X: "\<And>i j. G i j \<in> sets (sigma UNIV (range F))"
355 assumes F: "\<And>i. F i \<in> sets borel"
356 shows "borel = sigma UNIV (range F)"
357 using assms by (intro borel_eq_sigmaI1[where X="range (\<lambda>(i, j). G i j)" and F=F]) auto
359 lemma borel_eq_sigmaI5:
360 fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and G :: "'l \<Rightarrow> 'a::topological_space set"
361 assumes borel_eq: "borel = sigma UNIV (range G)"
362 assumes X: "\<And>i. G i \<in> sets (sigma UNIV (range (\<lambda>(i, j). F i j)))"
363 assumes F: "\<And>i j. F i j \<in> sets borel"
364 shows "borel = sigma UNIV (range (\<lambda>(i, j). F i j))"
365 using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(\<lambda>(i, j). F i j)"]) auto
367 lemma halfspace_gt_in_halfspace:
368 "{x\<Colon>'a. a < x $$ i} \<in> sigma_sets UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a}))"
369 (is "?set \<in> ?SIGMA")
371 interpret sigma_algebra UNIV ?SIGMA
372 by (intro sigma_algebra_sigma_sets) simp_all
373 have *: "?set = (\<Union>n. UNIV - {x\<Colon>'a. x $$ i < a + 1 / real (Suc n)})"
374 proof (safe, simp_all add: not_less)
375 fix x assume "a < x $$ i"
376 with reals_Archimedean[of "x $$ i - a"]
377 obtain n where "a + 1 / real (Suc n) < x $$ i"
378 by (auto simp: inverse_eq_divide field_simps)
379 then show "\<exists>n. a + 1 / real (Suc n) \<le> x $$ i"
380 by (blast intro: less_imp_le)
383 have "a < a + 1 / real (Suc n)" by auto
384 also assume "\<dots> \<le> x"
385 finally show "a < x" .
387 show "?set \<in> ?SIGMA" unfolding *
388 by (auto intro!: Diff)
391 lemma borel_eq_halfspace_less:
392 "borel = sigma UNIV (range (\<lambda>(a, i). {x::'a::ordered_euclidean_space. x $$ i < a}))"
394 proof (rule borel_eq_sigmaI3[OF borel_def])
395 fix S :: "'a set" assume "S \<in> {S. open S}"
396 then have "open S" by simp
397 from open_UNION[OF this]
398 obtain I where *: "S =
399 (\<Union>(a, b)\<in>I.
400 (\<Inter> i<DIM('a). {x. (Chi (real_of_rat \<circ> op ! a)::'a) $$ i < x $$ i}) \<inter>
401 (\<Inter> i<DIM('a). {x. x $$ i < (Chi (real_of_rat \<circ> op ! b)::'a) $$ i}))"
402 unfolding greaterThanLessThan_def
403 unfolding eucl_greaterThan_eq_halfspaces[where 'a='a]
404 unfolding eucl_lessThan_eq_halfspaces[where 'a='a]
406 show "S \<in> ?SIGMA"
408 by (safe intro!: countable_UN Int countable_INT) (auto intro!: halfspace_gt_in_halfspace)
411 lemma borel_eq_halfspace_le:
412 "borel = sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x $$ i \<le> a}))"
414 proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less])
416 have *: "{x::'a. x$$i < a} = (\<Union>n. {x. x$$i \<le> a - 1/real (Suc n)})"
417 proof (safe, simp_all)
418 fix x::'a assume *: "x$$i < a"
419 with reals_Archimedean[of "a - x$$i"]
420 obtain n where "x $$ i < a - 1 / (real (Suc n))"
421 by (auto simp: field_simps inverse_eq_divide)
422 then show "\<exists>n. x $$ i \<le> a - 1 / (real (Suc n))"
423 by (blast intro: less_imp_le)
426 assume "x$$i \<le> a - 1 / real (Suc n)"
427 also have "\<dots> < a" by auto
428 finally show "x$$i < a" .
430 show "{x. x$$i < a} \<in> ?SIGMA" unfolding *
431 by (safe intro!: countable_UN) auto
434 lemma borel_eq_halfspace_ge:
435 "borel = sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. a \<le> x $$ i}))"
437 proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less])
438 fix a i have *: "{x::'a. x$$i < a} = space ?SIGMA - {x::'a. a \<le> x$$i}" by auto
439 show "{x. x$$i < a} \<in> ?SIGMA" unfolding *
440 by (safe intro!: compl_sets) auto
443 lemma borel_eq_halfspace_greater:
444 "borel = sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. a < x $$ i}))"
446 proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le])
447 fix a i have *: "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto
448 show "{x. x$$i \<le> a} \<in> ?SIGMA" unfolding *
449 by (safe intro!: compl_sets) auto
452 lemma borel_eq_atMost:
453 "borel = sigma UNIV (range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space}))"
455 proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
456 fix a i show "{x. x$$i \<le> a} \<in> ?SIGMA"
459 then have *: "{x::'a. x$$i \<le> a} = (\<Union>k::nat. {.. (\<chi>\<chi> n. if n = i then a else real k)})"
460 proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm)
462 from real_arch_simple[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"] guess k::nat ..
463 then have "\<And>i. i < DIM('a) \<Longrightarrow> x$$i \<le> real k"
464 by (subst (asm) Max_le_iff) auto
465 then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia \<le> real k"
466 by (auto intro!: exI[of _ k])
468 show "{x. x$$i \<le> a} \<in> ?SIGMA" unfolding *
469 by (safe intro!: countable_UN) auto
470 qed (auto intro: sigma_sets_top sigma_sets.Empty)
473 lemma borel_eq_greaterThan:
474 "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {a<..}))"
476 proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
477 fix a i show "{x. x$$i \<le> a} \<in> ?SIGMA"
480 have "{x::'a. x$$i \<le> a} = UNIV - {x::'a. a < x$$i}" by auto
481 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)`
482 proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
484 from reals_Archimedean2[of "Max ((\<lambda>i. -x$$i)`{..<DIM('a)})"]
485 guess k::nat .. note k = this
486 { fix i assume "i < DIM('a)"
487 then have "-x$$i < real k"
488 using k by (subst (asm) Max_less_iff) auto
489 then have "- real k < x$$i" by simp }
490 then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> -real k < x $$ ia"
491 by (auto intro!: exI[of _ k])
493 finally show "{x. x$$i \<le> a} \<in> ?SIGMA"
495 apply (safe intro!: countable_UN Diff)
496 apply (auto intro: sigma_sets_top)
498 qed (auto intro: sigma_sets_top sigma_sets.Empty)
501 lemma borel_eq_lessThan:
502 "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {..<a}))"
504 proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge])
505 fix a i show "{x. a \<le> x$$i} \<in> ?SIGMA"
507 fix a i assume "i < DIM('a)"
508 have "{x::'a. a \<le> x$$i} = UNIV - {x::'a. x$$i < a}" by auto
509 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)`
510 proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
512 from reals_Archimedean2[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"]
513 guess k::nat .. note k = this
514 { fix i assume "i < DIM('a)"
515 then have "x$$i < real k"
516 using k by (subst (asm) Max_less_iff) auto
517 then have "x$$i < real k" by simp }
518 then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia < real k"
519 by (auto intro!: exI[of _ k])
521 finally show "{x. a \<le> x$$i} \<in> ?SIGMA"
523 apply (safe intro!: countable_UN Diff)
524 apply (auto intro: sigma_sets_top)
526 qed (auto intro: sigma_sets_top sigma_sets.Empty)
529 lemma borel_eq_atLeastAtMost:
530 "borel = sigma UNIV (range (\<lambda>(a,b). {a..b} \<Colon>'a\<Colon>ordered_euclidean_space set))"
532 proof (rule borel_eq_sigmaI5[OF borel_eq_atMost])
534 have *: "{..a} = (\<Union>n::nat. {- real n *\<^sub>R One .. a})"
535 proof (safe, simp_all add: eucl_le[where 'a='a])
537 from real_arch_simple[of "Max ((\<lambda>i. - x$$i)`{..<DIM('a)})"]
538 guess k::nat .. note k = this
539 { fix i assume "i < DIM('a)"
540 with k have "- x$$i \<le> real k"
541 by (subst (asm) Max_le_iff) (auto simp: field_simps)
542 then have "- real k \<le> x$$i" by simp }
543 then show "\<exists>n::nat. \<forall>i<DIM('a). - real n \<le> x $$ i"
544 by (auto intro!: exI[of _ k])
546 show "{..a} \<in> ?SIGMA" unfolding *
547 by (safe intro!: countable_UN)
548 (auto intro!: sigma_sets_top)
551 lemma borel_eq_greaterThanLessThan:
552 "borel = sigma UNIV (range (\<lambda> (a, b). {a <..< b} :: 'a \<Colon> ordered_euclidean_space set))"
554 proof (rule borel_eq_sigmaI1[OF borel_def])
555 fix M :: "'a set" assume "M \<in> {S. open S}"
556 then have "open M" by simp
557 show "M \<in> ?SIGMA"
558 apply (subst open_UNION[OF `open M`])
559 apply (safe intro!: countable_UN)
564 lemma borel_eq_atLeastLessThan:
565 "borel = sigma UNIV (range (\<lambda>(a, b). {a ..< b :: real}))" (is "_ = ?SIGMA")
566 proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan])
567 have move_uminus: "\<And>x y::real. -x \<le> y \<longleftrightarrow> -y \<le> x" by auto
569 have "{..<x} = (\<Union>i::nat. {-real i ..< x})"
570 by (auto simp: move_uminus real_arch_simple)
571 then show "{..< x} \<in> ?SIGMA"
572 by (auto intro: sigma_sets.intros)
575 lemma borel_measurable_halfspacesI:
576 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
577 assumes F: "borel = sigma UNIV (range F)"
578 and S_eq: "\<And>a i. S a i = f -` F (a,i) \<inter> space M"
579 and S: "\<And>a i. \<not> i < DIM('c) \<Longrightarrow> S a i \<in> sets M"
580 shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a::real. S a i \<in> sets M)"
582 fix a :: real and i assume i: "i < DIM('c)" and f: "f \<in> borel_measurable M"
583 then show "S a i \<in> sets M" unfolding assms
584 by (auto intro!: measurable_sets sigma_sets.Basic simp: assms(1))
586 assume a: "\<forall>i<DIM('c). \<forall>a. S a i \<in> sets M"
587 { fix a i have "S a i \<in> sets M"
590 with a show ?thesis unfolding assms(2) by simp
592 assume "\<not> i < DIM('c)"
593 from S[OF this] show ?thesis .
595 then show "f \<in> borel_measurable M"
596 by (auto intro!: measurable_measure_of simp: S_eq F)
599 lemma borel_measurable_iff_halfspace_le:
600 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
601 shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. f w $$ i \<le> a} \<in> sets M)"
602 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto
604 lemma borel_measurable_iff_halfspace_less:
605 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
606 shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. f w $$ i < a} \<in> sets M)"
607 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto
609 lemma borel_measurable_iff_halfspace_ge:
610 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
611 shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. a \<le> f w $$ i} \<in> sets M)"
612 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto
614 lemma borel_measurable_iff_halfspace_greater:
615 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
616 shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. a < f w $$ i} \<in> sets M)"
617 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_greater]) auto
619 lemma borel_measurable_iff_le:
620 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)"
621 using borel_measurable_iff_halfspace_le[where 'c=real] by simp
623 lemma borel_measurable_iff_less:
624 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)"
625 using borel_measurable_iff_halfspace_less[where 'c=real] by simp
627 lemma borel_measurable_iff_ge:
628 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)"
629 using borel_measurable_iff_halfspace_ge[where 'c=real] by simp
631 lemma borel_measurable_iff_greater:
632 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
633 using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
635 lemma borel_measurable_euclidean_component:
636 "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel"
637 proof (rule borel_measurableI)
638 fix S::"real set" assume "open S"
639 from open_vimage_euclidean_component[OF this]
640 show "(\<lambda>x. x $$ i) -` S \<inter> space borel \<in> sets borel"
641 by (auto intro: borel_open)
644 lemma borel_measurable_euclidean_space:
645 fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
646 shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M)"
648 fix i assume "f \<in> borel_measurable M"
649 then show "(\<lambda>x. f x $$ i) \<in> borel_measurable M"
650 using measurable_comp[of f _ _ "\<lambda>x. x $$ i", unfolded comp_def]
651 by (auto intro: borel_measurable_euclidean_component)
653 assume f: "\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M"
654 then show "f \<in> borel_measurable M"
655 unfolding borel_measurable_iff_halfspace_le by auto
658 subsection "Borel measurable operators"
660 lemma affine_borel_measurable_vector:
661 fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
662 assumes "f \<in> borel_measurable M"
663 shows "(\<lambda>x. a + b *\<^sub>R f x) \<in> borel_measurable M"
664 proof (rule borel_measurableI)
665 fix S :: "'x set" assume "open S"
666 show "(\<lambda>x. a + b *\<^sub>R f x) -` S \<inter> space M \<in> sets M"
668 assume "b \<noteq> 0"
669 with `open S` have "open ((\<lambda>x. (- a + x) /\<^sub>R b) ` S)" (is "open ?S")
670 by (auto intro!: open_affinity simp: scaleR_add_right)
671 hence "?S \<in> sets borel" by auto
673 from `b \<noteq> 0` have "(\<lambda>x. a + b *\<^sub>R f x) -` S = f -` ?S"
674 apply auto by (rule_tac x="a + b *\<^sub>R f x" in image_eqI, simp_all)
675 ultimately show ?thesis using assms unfolding in_borel_measurable_borel
680 lemma affine_borel_measurable:
681 fixes g :: "'a \<Rightarrow> real"
682 assumes g: "g \<in> borel_measurable M"
683 shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
684 using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute)
686 lemma borel_measurable_add[simp, intro]:
687 fixes f :: "'a \<Rightarrow> real"
688 assumes f: "f \<in> borel_measurable M"
689 assumes g: "g \<in> borel_measurable M"
690 shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
692 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}"
694 have "\<And>a. (\<lambda>w. a + (g w) * -1) \<in> borel_measurable M"
695 by (rule affine_borel_measurable [OF g])
696 then have "\<And>a. {w \<in> space M. (\<lambda>w. a + (g w) * -1)(w) \<le> f w} \<in> sets M" using f
698 then have "\<And>a. {w \<in> space M. a \<le> f w + g w} \<in> sets M"
701 by (simp add: borel_measurable_iff_ge)
704 lemma borel_measurable_setsum[simp, intro]:
705 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
706 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
707 shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
710 thus ?thesis using assms by induct auto
713 lemma borel_measurable_square:
714 fixes f :: "'a \<Rightarrow> real"
715 assumes f: "f \<in> borel_measurable M"
716 shows "(\<lambda>x. (f x)^2) \<in> borel_measurable M"
720 have "{w \<in> space M. (f w)\<twosuperior> \<le> a} \<in> sets M"
721 proof (cases rule: linorder_cases [of a 0])
723 hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = {}"
724 by auto (metis less order_le_less_trans power2_less_0)
725 also have "... \<in> sets M"
727 finally show ?thesis .
730 hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
731 {w \<in> space M. f w \<le> 0} \<inter> {w \<in> space M. 0 \<le> f w}"
733 also have "... \<in> sets M"
736 apply (simp add: borel_measurable_iff_le)
737 apply (simp add: borel_measurable_iff_ge)
739 finally show ?thesis .
742 have "\<forall>x. (f x ^ 2 \<le> sqrt a ^ 2) = (- sqrt a \<le> f x & f x \<le> sqrt a)"
743 by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs
744 real_sqrt_le_iff real_sqrt_power)
745 hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
746 {w \<in> space M. -(sqrt a) \<le> f w} \<inter> {w \<in> space M. f w \<le> sqrt a}"
747 using greater by auto
748 also have "... \<in> sets M"
751 apply (simp add: borel_measurable_iff_ge)
752 apply (simp add: borel_measurable_iff_le)
754 finally show ?thesis .
757 thus ?thesis by (auto simp add: borel_measurable_iff_le)
760 lemma times_eq_sum_squares:
762 shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4"
763 by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric])
765 lemma borel_measurable_uminus[simp, intro]:
766 fixes g :: "'a \<Rightarrow> real"
767 assumes g: "g \<in> borel_measurable M"
768 shows "(\<lambda>x. - g x) \<in> borel_measurable M"
770 have "(\<lambda>x. - g x) = (\<lambda>x. 0 + (g x) * -1)"
772 also have "... \<in> borel_measurable M"
773 by (fast intro: affine_borel_measurable g)
774 finally show ?thesis .
777 lemma borel_measurable_times[simp, intro]:
778 fixes f :: "'a \<Rightarrow> real"
779 assumes f: "f \<in> borel_measurable M"
780 assumes g: "g \<in> borel_measurable M"
781 shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
783 have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M"
784 using assms by (fast intro: affine_borel_measurable borel_measurable_square)
785 have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) =
786 (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
787 by (simp add: minus_divide_right)
788 also have "... \<in> borel_measurable M"
789 using f g by (fast intro: affine_borel_measurable borel_measurable_square f g)
790 finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
792 apply (simp add: times_eq_sum_squares diff_minus)
796 lemma borel_measurable_setprod[simp, intro]:
797 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
798 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
799 shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
802 thus ?thesis using assms by induct auto
805 lemma borel_measurable_diff[simp, intro]:
806 fixes f :: "'a \<Rightarrow> real"
807 assumes f: "f \<in> borel_measurable M"
808 assumes g: "g \<in> borel_measurable M"
809 shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
810 unfolding diff_minus using assms by fast
812 lemma borel_measurable_inverse[simp, intro]:
813 fixes f :: "'a \<Rightarrow> real"
814 assumes "f \<in> borel_measurable M"
815 shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
816 unfolding borel_measurable_iff_ge unfolding inverse_eq_divide
819 have *: "{w \<in> space M. a \<le> 1 / f w} =
820 ({w \<in> space M. 0 < f w} \<inter> {w \<in> space M. a * f w \<le> 1}) \<union>
821 ({w \<in> space M. f w < 0} \<inter> {w \<in> space M. 1 \<le> a * f w}) \<union>
822 ({w \<in> space M. f w = 0} \<inter> {w \<in> space M. a \<le> 0})" by (auto simp: le_divide_eq)
823 show "{w \<in> space M. a \<le> 1 / f w} \<in> sets M" using assms unfolding *
824 by (auto intro!: Int Un)
827 lemma borel_measurable_divide[simp, intro]:
828 fixes f :: "'a \<Rightarrow> real"
829 assumes "f \<in> borel_measurable M"
830 and "g \<in> borel_measurable M"
831 shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
832 unfolding field_divide_inverse
833 by (rule borel_measurable_inverse borel_measurable_times assms)+
835 lemma borel_measurable_max[intro, simp]:
836 fixes f g :: "'a \<Rightarrow> real"
837 assumes "f \<in> borel_measurable M"
838 assumes "g \<in> borel_measurable M"
839 shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
840 unfolding borel_measurable_iff_le
843 have "{x \<in> space M. max (g x) (f x) \<le> a} =
844 {x \<in> space M. g x \<le> a} \<inter> {x \<in> space M. f x \<le> a}" by auto
845 thus "{x \<in> space M. max (g x) (f x) \<le> a} \<in> sets M"
846 using assms unfolding borel_measurable_iff_le
847 by (auto intro!: Int)
850 lemma borel_measurable_min[intro, simp]:
851 fixes f g :: "'a \<Rightarrow> real"
852 assumes "f \<in> borel_measurable M"
853 assumes "g \<in> borel_measurable M"
854 shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
855 unfolding borel_measurable_iff_ge
858 have "{x \<in> space M. a \<le> min (g x) (f x)} =
859 {x \<in> space M. a \<le> g x} \<inter> {x \<in> space M. a \<le> f x}" by auto
860 thus "{x \<in> space M. a \<le> min (g x) (f x)} \<in> sets M"
861 using assms unfolding borel_measurable_iff_ge
862 by (auto intro!: Int)
865 lemma borel_measurable_abs[simp, intro]:
866 assumes "f \<in> borel_measurable M"
867 shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
869 have *: "\<And>x. \<bar>f x\<bar> = max 0 (f x) + max 0 (- f x)" by (simp add: max_def)
870 show ?thesis unfolding * using assms by auto
873 lemma borel_measurable_nth[simp, intro]:
874 "(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel"
875 using borel_measurable_euclidean_component
876 unfolding nth_conv_component by auto
878 lemma borel_measurable_continuous_on1:
879 fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
880 assumes "continuous_on UNIV f"
881 shows "f \<in> borel_measurable borel"
882 apply(rule borel_measurableI)
883 using continuous_open_preimage[OF assms] unfolding vimage_def by auto
885 lemma borel_measurable_continuous_on:
886 fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
887 assumes cont: "continuous_on A f" "open A"
888 shows "(\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel" (is "?f \<in> _")
889 proof (rule borel_measurableI)
890 fix S :: "'b set" assume "open S"
891 then have "open {x\<in>A. f x \<in> S}"
892 by (intro continuous_open_preimage[OF cont]) auto
893 then have *: "{x\<in>A. f x \<in> S} \<in> sets borel" by auto
894 have "?f -` S \<inter> space borel =
895 {x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel - A else {})"
896 by (auto split: split_if_asm)
897 also have "\<dots> \<in> sets borel"
898 using * `open A` by (auto simp del: space_borel intro!: Un)
899 finally show "?f -` S \<inter> space borel \<in> sets borel" .
902 lemma convex_measurable:
904 assumes X: "X \<in> borel_measurable M" "X ` space M \<subseteq> { a <..< b}"
905 assumes q: "convex_on { a <..< b} q"
906 shows "q \<circ> X \<in> borel_measurable M"
908 have "(\<lambda>x. if x \<in> {a <..< b} then q x else 0) \<in> borel_measurable borel"
909 proof (rule borel_measurable_continuous_on)
910 show "open {a<..<b}" by auto
911 from this q show "continuous_on {a<..<b} q"
912 by (rule convex_on_continuous)
914 then have "(\<lambda>x. if x \<in> {a <..< b} then q x else 0) \<circ> X \<in> borel_measurable M" (is ?qX)
915 using X by (intro measurable_comp) auto
916 moreover have "?qX \<longleftrightarrow> q \<circ> X \<in> borel_measurable M"
917 using X by (intro measurable_cong) auto
918 ultimately show ?thesis by simp
921 lemma borel_measurable_borel_log: assumes "1 < b" shows "log b \<in> borel_measurable borel"
923 { fix x :: real assume x: "x \<le> 0"
924 { fix x::real assume "x \<le> 0" then have "\<And>u. exp u = x \<longleftrightarrow> False" by auto }
925 from this[of x] x this[of 0] have "log b 0 = log b x"
926 by (auto simp: ln_def log_def) }
928 have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) \<in> borel_measurable borel"
929 proof (rule borel_measurable_continuous_on)
930 show "continuous_on {0<..} (log b)"
931 by (auto intro!: continuous_at_imp_continuous_on DERIV_log DERIV_isCont
932 simp: continuous_isCont[symmetric])
933 show "open ({0<..}::real set)" by auto
935 also have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) = log b"
936 by (simp add: fun_eq_iff not_less log_imp)
937 finally show ?thesis .
940 lemma borel_measurable_log[simp,intro]:
941 assumes f: "f \<in> borel_measurable M" and "1 < b"
942 shows "(\<lambda>x. log b (f x)) \<in> borel_measurable M"
943 using measurable_comp[OF f borel_measurable_borel_log[OF `1 < b`]]
944 by (simp add: comp_def)
946 subsection "Borel space on the extended reals"
948 lemma borel_measurable_ereal_borel:
949 "ereal \<in> borel_measurable borel"
950 proof (rule borel_measurableI)
951 fix X :: "ereal set" assume "open X"
952 then have "open (ereal -` X \<inter> space borel)"
953 by (simp add: open_ereal_vimage)
954 then show "ereal -` X \<inter> space borel \<in> sets borel" by auto
957 lemma borel_measurable_ereal[simp, intro]:
958 assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
959 using measurable_comp[OF f borel_measurable_ereal_borel] unfolding comp_def .
961 lemma borel_measurable_real_of_ereal_borel:
962 "(real :: ereal \<Rightarrow> real) \<in> borel_measurable borel"
963 proof (rule borel_measurableI)
964 fix B :: "real set" assume "open B"
965 have *: "ereal -` real -` (B - {0}) = B - {0}" by auto
966 have open_real: "open (real -` (B - {0}) :: ereal set)"
967 unfolding open_ereal_def * using `open B` by auto
968 show "(real -` B \<inter> space borel :: ereal set) \<in> sets borel"
971 then have *: "real -` B = real -` (B - {0}) \<union> {-\<infinity>, \<infinity>, 0::ereal}"
972 by (auto simp add: real_of_ereal_eq_0)
973 then show "(real -` B :: ereal set) \<inter> space borel \<in> sets borel"
974 using open_real by auto
976 assume "0 \<notin> B"
977 then have *: "(real -` B :: ereal set) = real -` (B - {0})"
978 by (auto simp add: real_of_ereal_eq_0)
979 then show "(real -` B :: ereal set) \<inter> space borel \<in> sets borel"
980 using open_real by auto
984 lemma borel_measurable_real_of_ereal[simp, intro]:
985 assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. real (f x :: ereal)) \<in> borel_measurable M"
986 using measurable_comp[OF f borel_measurable_real_of_ereal_borel] unfolding comp_def .
988 lemma borel_measurable_ereal_iff:
989 shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
991 assume "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
992 from borel_measurable_real_of_ereal[OF this]
993 show "f \<in> borel_measurable M" by auto
996 lemma borel_measurable_ereal_iff_real:
997 fixes f :: "'a \<Rightarrow> ereal"
998 shows "f \<in> borel_measurable M \<longleftrightarrow>
999 ((\<lambda>x. real (f x)) \<in> borel_measurable M \<and> f -` {\<infinity>} \<inter> space M \<in> sets M \<and> f -` {-\<infinity>} \<inter> space M \<in> sets M)"
1001 assume *: "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f -` {\<infinity>} \<inter> space M \<in> sets M" "f -` {-\<infinity>} \<inter> space M \<in> sets M"
1002 have "f -` {\<infinity>} \<inter> space M = {x\<in>space M. f x = \<infinity>}" "f -` {-\<infinity>} \<inter> space M = {x\<in>space M. f x = -\<infinity>}" by auto
1003 with * have **: "{x\<in>space M. f x = \<infinity>} \<in> sets M" "{x\<in>space M. f x = -\<infinity>} \<in> sets M" by simp_all
1004 let ?f = "\<lambda>x. if f x = \<infinity> then \<infinity> else if f x = -\<infinity> then -\<infinity> else ereal (real (f x))"
1005 have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto
1006 also have "?f = f" by (auto simp: fun_eq_iff ereal_real)
1007 finally show "f \<in> borel_measurable M" .
1008 qed (auto intro: measurable_sets borel_measurable_real_of_ereal)
1010 lemma less_eq_ge_measurable:
1011 fixes f :: "'a \<Rightarrow> 'c::linorder"
1012 shows "f -` {a <..} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {..a} \<inter> space M \<in> sets M"
1014 assume "f -` {a <..} \<inter> space M \<in> sets M"
1015 moreover have "f -` {..a} \<inter> space M = space M - f -` {a <..} \<inter> space M" by auto
1016 ultimately show "f -` {..a} \<inter> space M \<in> sets M" by auto
1018 assume "f -` {..a} \<inter> space M \<in> sets M"
1019 moreover have "f -` {a <..} \<inter> space M = space M - f -` {..a} \<inter> space M" by auto
1020 ultimately show "f -` {a <..} \<inter> space M \<in> sets M" by auto
1023 lemma greater_eq_le_measurable:
1024 fixes f :: "'a \<Rightarrow> 'c::linorder"
1025 shows "f -` {..< a} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {a ..} \<inter> space M \<in> sets M"
1027 assume "f -` {a ..} \<inter> space M \<in> sets M"
1028 moreover have "f -` {..< a} \<inter> space M = space M - f -` {a ..} \<inter> space M" by auto
1029 ultimately show "f -` {..< a} \<inter> space M \<in> sets M" by auto
1031 assume "f -` {..< a} \<inter> space M \<in> sets M"
1032 moreover have "f -` {a ..} \<inter> space M = space M - f -` {..< a} \<inter> space M" by auto
1033 ultimately show "f -` {a ..} \<inter> space M \<in> sets M" by auto
1036 lemma borel_measurable_uminus_borel_ereal:
1037 "(uminus :: ereal \<Rightarrow> ereal) \<in> borel_measurable borel"
1038 proof (rule borel_measurableI)
1039 fix X :: "ereal set" assume "open X"
1040 have "uminus -` X = uminus ` X" by (force simp: image_iff)
1041 then have "open (uminus -` X)" using `open X` ereal_open_uminus by auto
1042 then show "uminus -` X \<inter> space borel \<in> sets borel" by auto
1045 lemma borel_measurable_uminus_ereal[intro]:
1046 assumes "f \<in> borel_measurable M"
1047 shows "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
1048 using measurable_comp[OF assms borel_measurable_uminus_borel_ereal] by (simp add: comp_def)
1050 lemma borel_measurable_uminus_eq_ereal[simp]:
1051 "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r")
1053 assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
1056 lemma borel_measurable_eq_atMost_ereal:
1057 fixes f :: "'a \<Rightarrow> ereal"
1058 shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
1059 proof (intro iffI allI)
1060 assume pos[rule_format]: "\<forall>a. f -` {..a} \<inter> space M \<in> sets M"
1061 show "f \<in> borel_measurable M"
1062 unfolding borel_measurable_ereal_iff_real borel_measurable_iff_le
1063 proof (intro conjI allI)
1065 { fix x :: ereal assume *: "\<forall>i::nat. real i < x"
1066 have "x = \<infinity>"
1067 proof (rule ereal_top)
1068 fix B from reals_Archimedean2[of B] guess n ..
1069 then have "ereal B < real n" by auto
1070 with * show "B \<le> x" by (metis less_trans less_imp_le)
1072 then have "f -` {\<infinity>} \<inter> space M = space M - (\<Union>i::nat. f -` {.. real i} \<inter> space M)"
1073 by (auto simp: not_le)
1074 then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos by (auto simp del: UN_simps intro!: Diff)
1076 have "{-\<infinity>::ereal} = {..-\<infinity>}" by auto
1077 then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto
1078 moreover have "{x\<in>space M. f x \<le> ereal a} \<in> sets M"
1079 using pos[of "ereal a"] by (simp add: vimage_def Int_def conj_commute)
1080 moreover have "{w \<in> space M. real (f w) \<le> a} =
1081 (if a < 0 then {w \<in> space M. f w \<le> ereal a} - f -` {-\<infinity>} \<inter> space M
1082 else {w \<in> space M. f w \<le> ereal a} \<union> (f -` {\<infinity>} \<inter> space M) \<union> (f -` {-\<infinity>} \<inter> space M))" (is "?l = ?r")
1083 proof (intro set_eqI) fix x show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" by (cases "f x") auto qed
1084 ultimately show "{w \<in> space M. real (f w) \<le> a} \<in> sets M" by auto
1086 qed (simp add: measurable_sets)
1088 lemma borel_measurable_eq_atLeast_ereal:
1089 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a..} \<inter> space M \<in> sets M)"
1091 assume pos: "\<forall>a. f -` {a..} \<inter> space M \<in> sets M"
1092 moreover have "\<And>a. (\<lambda>x. - f x) -` {..a} = f -` {-a ..}"
1093 by (auto simp: ereal_uminus_le_reorder)
1094 ultimately have "(\<lambda>x. - f x) \<in> borel_measurable M"
1095 unfolding borel_measurable_eq_atMost_ereal by auto
1096 then show "f \<in> borel_measurable M" by simp
1097 qed (simp add: measurable_sets)
1099 lemma borel_measurable_ereal_iff_less:
1100 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..< a} \<inter> space M \<in> sets M)"
1101 unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable ..
1103 lemma borel_measurable_ereal_iff_ge:
1104 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a <..} \<inter> space M \<in> sets M)"
1105 unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable ..
1107 lemma borel_measurable_ereal_eq_const:
1108 fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M"
1109 shows "{x\<in>space M. f x = c} \<in> sets M"
1111 have "{x\<in>space M. f x = c} = (f -` {c} \<inter> space M)" by auto
1112 then show ?thesis using assms by (auto intro!: measurable_sets)
1115 lemma borel_measurable_ereal_neq_const:
1116 fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M"
1117 shows "{x\<in>space M. f x \<noteq> c} \<in> sets M"
1119 have "{x\<in>space M. f x \<noteq> c} = space M - (f -` {c} \<inter> space M)" by auto
1120 then show ?thesis using assms by (auto intro!: measurable_sets)
1123 lemma borel_measurable_ereal_le[intro,simp]:
1124 fixes f g :: "'a \<Rightarrow> ereal"
1125 assumes f: "f \<in> borel_measurable M"
1126 assumes g: "g \<in> borel_measurable M"
1127 shows "{x \<in> space M. f x \<le> g x} \<in> sets M"
1129 have "{x \<in> space M. f x \<le> g x} =
1130 {x \<in> space M. real (f x) \<le> real (g x)} - (f -` {\<infinity>, -\<infinity>} \<inter> space M \<union> g -` {\<infinity>, -\<infinity>} \<inter> space M) \<union>
1131 f -` {-\<infinity>} \<inter> space M \<union> g -` {\<infinity>} \<inter> space M" (is "?l = ?r")
1132 proof (intro set_eqI)
1133 fix x show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" by (cases rule: ereal2_cases[of "f x" "g x"]) auto
1135 with f g show ?thesis by (auto intro!: Un simp: measurable_sets)
1138 lemma borel_measurable_ereal_less[intro,simp]:
1139 fixes f :: "'a \<Rightarrow> ereal"
1140 assumes f: "f \<in> borel_measurable M"
1141 assumes g: "g \<in> borel_measurable M"
1142 shows "{x \<in> space M. f x < g x} \<in> sets M"
1144 have "{x \<in> space M. f x < g x} = space M - {x \<in> space M. g x \<le> f x}" by auto
1145 then show ?thesis using g f by auto
1148 lemma borel_measurable_ereal_eq[intro,simp]:
1149 fixes f :: "'a \<Rightarrow> ereal"
1150 assumes f: "f \<in> borel_measurable M"
1151 assumes g: "g \<in> borel_measurable M"
1152 shows "{w \<in> space M. f w = g w} \<in> sets M"
1154 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
1155 then show ?thesis using g f by auto
1158 lemma borel_measurable_ereal_neq[intro,simp]:
1159 fixes f :: "'a \<Rightarrow> ereal"
1160 assumes f: "f \<in> borel_measurable M"
1161 assumes g: "g \<in> borel_measurable M"
1162 shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
1164 have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}" by auto
1165 thus ?thesis using f g by auto
1169 "{x\<in>space M. P x \<or> Q x} = {x\<in>space M. P x} \<union> {x\<in>space M. Q x}"
1170 "{x\<in>space M. P x \<and> Q x} = {x\<in>space M. P x} \<inter> {x\<in>space M. Q x}"
1173 lemma borel_measurable_ereal_add[intro, simp]:
1174 fixes f :: "'a \<Rightarrow> ereal"
1175 assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
1176 shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
1178 { fix x assume "x \<in> space M" then have "f x + g x =
1179 (if f x = \<infinity> \<or> g x = \<infinity> then \<infinity>
1180 else if f x = -\<infinity> \<or> g x = -\<infinity> then -\<infinity>
1181 else ereal (real (f x) + real (g x)))"
1182 by (cases rule: ereal2_cases[of "f x" "g x"]) auto }
1183 with assms show ?thesis
1184 by (auto cong: measurable_cong simp: split_sets
1185 intro!: Un measurable_If measurable_sets)
1188 lemma borel_measurable_ereal_setsum[simp, intro]:
1189 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
1190 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
1191 shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
1194 thus ?thesis using assms
1196 qed (simp add: borel_measurable_const)
1198 lemma borel_measurable_ereal_abs[intro, simp]:
1199 fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M"
1200 shows "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
1202 { fix x have "\<bar>f x\<bar> = (if 0 \<le> f x then f x else - f x)" by auto }
1203 then show ?thesis using assms by (auto intro!: measurable_If)
1206 lemma borel_measurable_ereal_times[intro, simp]:
1207 fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
1208 shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
1210 { fix f g :: "'a \<Rightarrow> ereal"
1211 assume b: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
1212 and pos: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x"
1213 { fix x have *: "f x * g x = (if f x = 0 \<or> g x = 0 then 0
1214 else if f x = \<infinity> \<or> g x = \<infinity> then \<infinity>
1215 else ereal (real (f x) * real (g x)))"
1216 apply (cases rule: ereal2_cases[of "f x" "g x"])
1217 using pos[of x] by auto }
1218 with b have "(\<lambda>x. f x * g x) \<in> borel_measurable M"
1219 by (auto cong: measurable_cong simp: split_sets
1220 intro!: Un measurable_If measurable_sets) }
1221 note pos_times = this
1222 have *: "(\<lambda>x. f x * g x) =
1223 (\<lambda>x. if 0 \<le> f x \<and> 0 \<le> g x \<or> f x < 0 \<and> g x < 0 then \<bar>f x\<bar> * \<bar>g x\<bar> else - (\<bar>f x\<bar> * \<bar>g x\<bar>))"
1224 by (auto simp: fun_eq_iff)
1225 show ?thesis using assms unfolding *
1226 by (intro measurable_If pos_times borel_measurable_uminus_ereal)
1227 (auto simp: split_sets intro!: Int)
1230 lemma borel_measurable_ereal_setprod[simp, intro]:
1231 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
1232 assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
1233 shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
1236 thus ?thesis using assms by induct auto
1239 lemma borel_measurable_ereal_min[simp, intro]:
1240 fixes f g :: "'a \<Rightarrow> ereal"
1241 assumes "f \<in> borel_measurable M"
1242 assumes "g \<in> borel_measurable M"
1243 shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
1244 using assms unfolding min_def by (auto intro!: measurable_If)
1246 lemma borel_measurable_ereal_max[simp, intro]:
1247 fixes f g :: "'a \<Rightarrow> ereal"
1248 assumes "f \<in> borel_measurable M"
1249 and "g \<in> borel_measurable M"
1250 shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
1251 using assms unfolding max_def by (auto intro!: measurable_If)
1253 lemma borel_measurable_SUP[simp, intro]:
1254 fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
1255 assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
1256 shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
1257 unfolding borel_measurable_ereal_iff_ge
1260 have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
1261 by (auto simp: less_SUP_iff)
1262 then show "?sup -` {a<..} \<inter> space M \<in> sets M"
1266 lemma borel_measurable_INF[simp, intro]:
1267 fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
1268 assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
1269 shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
1270 unfolding borel_measurable_ereal_iff_less
1273 have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
1274 by (auto simp: INF_less_iff)
1275 then show "?inf -` {..<a} \<inter> space M \<in> sets M"
1279 lemma borel_measurable_liminf[simp, intro]:
1280 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
1281 assumes "\<And>i. f i \<in> borel_measurable M"
1282 shows "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
1283 unfolding liminf_SUPR_INFI using assms by auto
1285 lemma borel_measurable_limsup[simp, intro]:
1286 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
1287 assumes "\<And>i. f i \<in> borel_measurable M"
1288 shows "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
1289 unfolding limsup_INFI_SUPR using assms by auto
1291 lemma borel_measurable_ereal_diff[simp, intro]:
1292 fixes f g :: "'a \<Rightarrow> ereal"
1293 assumes "f \<in> borel_measurable M"
1294 assumes "g \<in> borel_measurable M"
1295 shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
1296 unfolding minus_ereal_def using assms by auto
1298 lemma borel_measurable_ereal_inverse[simp, intro]:
1299 assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
1301 { fix x have "inverse (f x) = (if f x = 0 then \<infinity> else ereal (inverse (real (f x))))"
1302 by (cases "f x") auto }
1304 by (auto intro!: measurable_If)
1307 lemma borel_measurable_ereal_divide[simp, intro]:
1308 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. f x / g x :: ereal) \<in> borel_measurable M"
1309 unfolding divide_ereal_def by auto
1311 lemma borel_measurable_psuminf[simp, intro]:
1312 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
1313 assumes "\<And>i. f i \<in> borel_measurable M" and pos: "\<And>i x. x \<in> space M \<Longrightarrow> 0 \<le> f i x"
1314 shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
1315 apply (subst measurable_cong)
1316 apply (subst suminf_ereal_eq_SUPR)
1320 section "LIMSEQ is borel measurable"
1322 lemma borel_measurable_LIMSEQ:
1323 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real"
1324 assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
1325 and u: "\<And>i. u i \<in> borel_measurable M"
1326 shows "u' \<in> borel_measurable M"
1328 have "\<And>x. x \<in> space M \<Longrightarrow> liminf (\<lambda>n. ereal (u n x)) = ereal (u' x)"
1329 using u' by (simp add: lim_imp_Liminf)
1330 moreover from u have "(\<lambda>x. liminf (\<lambda>n. ereal (u n x))) \<in> borel_measurable M"
1332 ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff)