349 have "x \<in> ?box (p, q)" |
305 have "x \<in> ?box (p, q)" |
350 using p q ab by auto |
306 using p q ab by auto |
351 thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto |
307 thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto |
352 qed auto |
308 qed auto |
353 |
309 |
354 lemma halfspace_span_open: |
310 lemma borel_sigma_sets_subset: |
355 "sigma_sets UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})) |
311 "A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel" |
356 \<subseteq> sets borel" |
312 using sigma_sets_subset[of A borel] by simp |
357 by (auto intro!: borel.sigma_sets_subset[simplified] borel_open |
313 |
358 open_halfspace_component_lt) |
314 lemma borel_eq_sigmaI1: |
359 |
315 fixes F :: "'i \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set" |
360 lemma halfspace_lt_in_halfspace: |
316 assumes borel_eq: "borel = sigma UNIV X" |
361 "{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>)" |
317 assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV (range F))" |
362 by (auto intro!: sigma_sets.Basic simp: sets_sigma) |
318 assumes F: "\<And>i. F i \<in> sets borel" |
|
319 shows "borel = sigma UNIV (range F)" |
|
320 unfolding borel_def |
|
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 |
|
331 qed auto |
|
332 |
|
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 |
|
341 |
|
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 |
|
349 |
|
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 |
|
358 |
|
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 |
363 |
366 |
364 lemma halfspace_gt_in_halfspace: |
367 lemma halfspace_gt_in_halfspace: |
365 "{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>)" |
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}))" |
366 (is "?set \<in> sets ?SIGMA") |
369 (is "?set \<in> ?SIGMA") |
367 proof - |
370 proof - |
368 interpret sigma_algebra "?SIGMA" |
371 interpret sigma_algebra UNIV ?SIGMA |
369 by (intro sigma_algebra_sigma_sets) (simp_all add: sets_sigma) |
372 by (intro sigma_algebra_sigma_sets) simp_all |
370 have *: "?set = (\<Union>n. space ?SIGMA - {x\<Colon>'a. x $$ i < a + 1 / real (Suc n)})" |
373 have *: "?set = (\<Union>n. UNIV - {x\<Colon>'a. x $$ i < a + 1 / real (Suc n)})" |
371 proof (safe, simp_all add: not_less) |
374 proof (safe, simp_all add: not_less) |
372 fix x assume "a < x $$ i" |
375 fix x assume "a < x $$ i" |
373 with reals_Archimedean[of "x $$ i - a"] |
376 with reals_Archimedean[of "x $$ i - a"] |
374 obtain n where "a + 1 / real (Suc n) < x $$ i" |
377 obtain n where "a + 1 / real (Suc n) < x $$ i" |
375 by (auto simp: inverse_eq_divide field_simps) |
378 by (auto simp: inverse_eq_divide field_simps) |
379 fix x n |
382 fix x n |
380 have "a < a + 1 / real (Suc n)" by auto |
383 have "a < a + 1 / real (Suc n)" by auto |
381 also assume "\<dots> \<le> x" |
384 also assume "\<dots> \<le> x" |
382 finally show "a < x" . |
385 finally show "a < x" . |
383 qed |
386 qed |
384 show "?set \<in> sets ?SIGMA" unfolding * |
387 show "?set \<in> ?SIGMA" unfolding * |
385 by (safe intro!: countable_UN Diff halfspace_lt_in_halfspace) |
388 by (auto intro!: Diff) |
386 qed |
389 qed |
387 |
390 |
388 lemma open_span_halfspace: |
391 lemma borel_eq_halfspace_less: |
389 "sets borel \<subseteq> sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x $$ i < a})\<rparr>)" |
392 "borel = sigma UNIV (range (\<lambda>(a, i). {x::'a::ordered_euclidean_space. x $$ i < a}))" |
390 (is "_ \<subseteq> sets ?SIGMA") |
393 (is "_ = ?SIGMA") |
391 proof - |
394 proof (rule borel_eq_sigmaI3[OF borel_def]) |
392 have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) simp |
395 fix S :: "'a set" assume "S \<in> {S. open S}" |
393 then interpret sigma_algebra ?SIGMA . |
396 then have "open S" by simp |
394 { fix S :: "'a set" assume "S \<in> {S. open S}" |
397 from open_UNION[OF this] |
395 then have "open S" unfolding mem_Collect_eq . |
398 obtain I where *: "S = |
396 from open_UNION[OF this] |
399 (\<Union>(a, b)\<in>I. |
397 obtain I where *: "S = |
400 (\<Inter> i<DIM('a). {x. (Chi (real_of_rat \<circ> op ! a)::'a) $$ i < x $$ i}) \<inter> |
398 (\<Union>(a, b)\<in>I. |
401 (\<Inter> i<DIM('a). {x. x $$ i < (Chi (real_of_rat \<circ> op ! b)::'a) $$ i}))" |
399 (\<Inter> i<DIM('a). {x. (Chi (real_of_rat \<circ> op ! a)::'a) $$ i < x $$ i}) \<inter> |
402 unfolding greaterThanLessThan_def |
400 (\<Inter> i<DIM('a). {x. x $$ i < (Chi (real_of_rat \<circ> op ! b)::'a) $$ i}))" |
403 unfolding eucl_greaterThan_eq_halfspaces[where 'a='a] |
401 unfolding greaterThanLessThan_def |
404 unfolding eucl_lessThan_eq_halfspaces[where 'a='a] |
402 unfolding eucl_greaterThan_eq_halfspaces[where 'a='a] |
405 by blast |
403 unfolding eucl_lessThan_eq_halfspaces[where 'a='a] |
406 show "S \<in> ?SIGMA" |
404 by blast |
407 unfolding * |
405 have "S \<in> sets ?SIGMA" |
408 by (safe intro!: countable_UN Int countable_INT) (auto intro!: halfspace_gt_in_halfspace) |
406 unfolding * |
409 qed auto |
407 by (auto intro!: countable_UN Int countable_INT halfspace_lt_in_halfspace halfspace_gt_in_halfspace) } |
410 |
408 then show ?thesis unfolding borel_def |
411 lemma borel_eq_halfspace_le: |
409 by (intro sets_sigma_subset) auto |
412 "borel = sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x $$ i \<le> a}))" |
410 qed |
413 (is "_ = ?SIGMA") |
411 |
414 proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less]) |
412 lemma halfspace_span_halfspace_le: |
415 fix a i |
413 "sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})\<rparr>) \<subseteq> |
416 have *: "{x::'a. x$$i < a} = (\<Union>n. {x. x$$i \<le> a - 1/real (Suc n)})" |
414 sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x. x $$ i \<le> a})\<rparr>)" |
417 proof (safe, simp_all) |
415 (is "_ \<subseteq> sets ?SIGMA") |
418 fix x::'a assume *: "x$$i < a" |
416 proof - |
419 with reals_Archimedean[of "a - x$$i"] |
417 have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto |
420 obtain n where "x $$ i < a - 1 / (real (Suc n))" |
418 then interpret sigma_algebra ?SIGMA . |
421 by (auto simp: field_simps inverse_eq_divide) |
419 { fix a i |
422 then show "\<exists>n. x $$ i \<le> a - 1 / (real (Suc n))" |
420 have *: "{x::'a. x$$i < a} = (\<Union>n. {x. x$$i \<le> a - 1/real (Suc n)})" |
423 by (blast intro: less_imp_le) |
421 proof (safe, simp_all) |
424 next |
422 fix x::'a assume *: "x$$i < a" |
425 fix x::'a and n |
423 with reals_Archimedean[of "a - x$$i"] |
426 assume "x$$i \<le> a - 1 / real (Suc n)" |
424 obtain n where "x $$ i < a - 1 / (real (Suc n))" |
427 also have "\<dots> < a" by auto |
425 by (auto simp: field_simps inverse_eq_divide) |
428 finally show "x$$i < a" . |
426 then show "\<exists>n. x $$ i \<le> a - 1 / (real (Suc n))" |
429 qed |
427 by (blast intro: less_imp_le) |
430 show "{x. x$$i < a} \<in> ?SIGMA" unfolding * |
428 next |
431 by (safe intro!: countable_UN) auto |
429 fix x::'a and n |
432 qed auto |
430 assume "x$$i \<le> a - 1 / real (Suc n)" |
433 |
431 also have "\<dots> < a" by auto |
434 lemma borel_eq_halfspace_ge: |
432 finally show "x$$i < a" . |
435 "borel = sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. a \<le> x $$ i}))" |
433 qed |
436 (is "_ = ?SIGMA") |
434 have "{x. x$$i < a} \<in> sets ?SIGMA" unfolding * |
437 proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less]) |
435 by (safe intro!: countable_UN) |
438 fix a i have *: "{x::'a. x$$i < a} = space ?SIGMA - {x::'a. a \<le> x$$i}" by auto |
436 (auto simp: sets_sigma intro!: sigma_sets.Basic) } |
439 show "{x. x$$i < a} \<in> ?SIGMA" unfolding * |
437 then show ?thesis by (intro sets_sigma_subset) auto |
440 by (safe intro!: compl_sets) auto |
438 qed |
441 qed auto |
439 |
442 |
440 lemma halfspace_span_halfspace_ge: |
443 lemma borel_eq_halfspace_greater: |
441 "sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})\<rparr>) \<subseteq> |
444 "borel = sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. a < x $$ i}))" |
442 sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x. a \<le> x $$ i})\<rparr>)" |
445 (is "_ = ?SIGMA") |
443 (is "_ \<subseteq> sets ?SIGMA") |
446 proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le]) |
444 proof - |
447 fix a i have *: "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto |
445 have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto |
448 show "{x. x$$i \<le> a} \<in> ?SIGMA" unfolding * |
446 then interpret sigma_algebra ?SIGMA . |
449 by (safe intro!: compl_sets) auto |
447 { fix a i have *: "{x::'a. x$$i < a} = space ?SIGMA - {x::'a. a \<le> x$$i}" by auto |
450 qed auto |
448 have "{x. x$$i < a} \<in> sets ?SIGMA" unfolding * |
451 |
449 by (safe intro!: Diff) |
452 lemma borel_eq_atMost: |
450 (auto simp: sets_sigma intro!: sigma_sets.Basic) } |
453 "borel = sigma UNIV (range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space}))" |
451 then show ?thesis by (intro sets_sigma_subset) auto |
454 (is "_ = ?SIGMA") |
452 qed |
455 proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le]) |
453 |
456 fix a i show "{x. x$$i \<le> a} \<in> ?SIGMA" |
454 lemma halfspace_le_span_halfspace_gt: |
|
455 "sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a})\<rparr>) \<subseteq> |
|
456 sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x. a < x $$ i})\<rparr>)" |
|
457 (is "_ \<subseteq> sets ?SIGMA") |
|
458 proof - |
|
459 have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto |
|
460 then interpret sigma_algebra ?SIGMA . |
|
461 { fix a i have *: "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto |
|
462 have "{x. x$$i \<le> a} \<in> sets ?SIGMA" unfolding * |
|
463 by (safe intro!: Diff) |
|
464 (auto simp: sets_sigma intro!: sigma_sets.Basic) } |
|
465 then show ?thesis by (intro sets_sigma_subset) auto |
|
466 qed |
|
467 |
|
468 lemma halfspace_le_span_atMost: |
|
469 "sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a})\<rparr>) \<subseteq> |
|
470 sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space})\<rparr>)" |
|
471 (is "_ \<subseteq> sets ?SIGMA") |
|
472 proof - |
|
473 have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto |
|
474 then interpret sigma_algebra ?SIGMA . |
|
475 have "\<And>a i. {x. x$$i \<le> a} \<in> sets ?SIGMA" |
|
476 proof cases |
457 proof cases |
477 fix a i assume "i < DIM('a)" |
458 assume "i < DIM('a)" |
478 then have *: "{x::'a. x$$i \<le> a} = (\<Union>k::nat. {.. (\<chi>\<chi> n. if n = i then a else real k)})" |
459 then have *: "{x::'a. x$$i \<le> a} = (\<Union>k::nat. {.. (\<chi>\<chi> n. if n = i then a else real k)})" |
479 proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm) |
460 proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm) |
480 fix x |
461 fix x |
481 from real_arch_simple[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"] guess k::nat .. |
462 from real_arch_simple[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"] guess k::nat .. |
482 then have "\<And>i. i < DIM('a) \<Longrightarrow> x$$i \<le> real k" |
463 then have "\<And>i. i < DIM('a) \<Longrightarrow> x$$i \<le> real k" |
483 by (subst (asm) Max_le_iff) auto |
464 by (subst (asm) Max_le_iff) auto |
484 then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia \<le> real k" |
465 then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia \<le> real k" |
485 by (auto intro!: exI[of _ k]) |
466 by (auto intro!: exI[of _ k]) |
486 qed |
467 qed |
487 show "{x. x$$i \<le> a} \<in> sets ?SIGMA" unfolding * |
468 show "{x. x$$i \<le> a} \<in> ?SIGMA" unfolding * |
488 by (safe intro!: countable_UN) |
469 by (safe intro!: countable_UN) auto |
489 (auto simp: sets_sigma intro!: sigma_sets.Basic) |
470 qed (auto intro: sigma_sets_top sigma_sets.Empty) |
490 next |
471 qed auto |
491 fix a i assume "\<not> i < DIM('a)" |
472 |
492 then show "{x. x$$i \<le> a} \<in> sets ?SIGMA" |
473 lemma borel_eq_greaterThan: |
493 using top by auto |
474 "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {a<..}))" |
494 qed |
475 (is "_ = ?SIGMA") |
495 then show ?thesis by (intro sets_sigma_subset) auto |
476 proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le]) |
496 qed |
477 fix a i show "{x. x$$i \<le> a} \<in> ?SIGMA" |
497 |
|
498 lemma halfspace_le_span_greaterThan: |
|
499 "sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a})\<rparr>) \<subseteq> |
|
500 sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>a. {a<..})\<rparr>)" |
|
501 (is "_ \<subseteq> sets ?SIGMA") |
|
502 proof - |
|
503 have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto |
|
504 then interpret sigma_algebra ?SIGMA . |
|
505 have "\<And>a i. {x. x$$i \<le> a} \<in> sets ?SIGMA" |
|
506 proof cases |
478 proof cases |
507 fix a i assume "i < DIM('a)" |
479 assume "i < DIM('a)" |
508 have "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto |
480 have "{x::'a. x$$i \<le> a} = UNIV - {x::'a. a < x$$i}" by auto |
509 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)` |
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)` |
510 proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm) |
482 proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm) |
511 fix x |
483 fix x |
512 from reals_Archimedean2[of "Max ((\<lambda>i. -x$$i)`{..<DIM('a)})"] |
484 from reals_Archimedean2[of "Max ((\<lambda>i. -x$$i)`{..<DIM('a)})"] |
513 guess k::nat .. note k = this |
485 guess k::nat .. note k = this |
552 using k by (subst (asm) Max_less_iff) auto |
516 using k by (subst (asm) Max_less_iff) auto |
553 then have "x$$i < real k" by simp } |
517 then have "x$$i < real k" by simp } |
554 then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia < real k" |
518 then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia < real k" |
555 by (auto intro!: exI[of _ k]) |
519 by (auto intro!: exI[of _ k]) |
556 qed |
520 qed |
557 finally show "{x. a \<le> x$$i} \<in> sets ?SIGMA" |
521 finally show "{x. a \<le> x$$i} \<in> ?SIGMA" |
558 apply (simp only:) |
522 apply (simp only:) |
559 apply (safe intro!: countable_UN Diff) |
523 apply (safe intro!: countable_UN Diff) |
560 apply (auto simp: sets_sigma intro!: sigma_sets.Basic) |
524 apply (auto intro: sigma_sets_top) |
561 done |
525 done |
562 next |
526 qed (auto intro: sigma_sets_top sigma_sets.Empty) |
563 fix a i assume "\<not> i < DIM('a)" |
527 qed auto |
564 then show "{x. a \<le> x$$i} \<in> sets ?SIGMA" |
528 |
565 using top by auto |
529 lemma borel_eq_atLeastAtMost: |
|
530 "borel = sigma UNIV (range (\<lambda>(a,b). {a..b} \<Colon>'a\<Colon>ordered_euclidean_space set))" |
|
531 (is "_ = ?SIGMA") |
|
532 proof (rule borel_eq_sigmaI5[OF borel_eq_atMost]) |
|
533 fix a::'a |
|
534 have *: "{..a} = (\<Union>n::nat. {- real n *\<^sub>R One .. a})" |
|
535 proof (safe, simp_all add: eucl_le[where 'a='a]) |
|
536 fix x |
|
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]) |
566 qed |
545 qed |
567 then show ?thesis by (intro sets_sigma_subset) auto |
546 show "{..a} \<in> ?SIGMA" unfolding * |
568 qed |
547 by (safe intro!: countable_UN) |
569 |
548 (auto intro!: sigma_sets_top) |
570 lemma atMost_span_atLeastAtMost: |
549 qed auto |
571 "sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space})\<rparr>) \<subseteq> |
550 |
572 sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>(a,b). {a..b})\<rparr>)" |
551 lemma borel_eq_greaterThanLessThan: |
573 (is "_ \<subseteq> sets ?SIGMA") |
552 "borel = sigma UNIV (range (\<lambda> (a, b). {a <..< b} :: 'a \<Colon> ordered_euclidean_space set))" |
574 proof - |
|
575 have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto |
|
576 then interpret sigma_algebra ?SIGMA . |
|
577 { fix a::'a |
|
578 have *: "{..a} = (\<Union>n::nat. {- real n *\<^sub>R One .. a})" |
|
579 proof (safe, simp_all add: eucl_le[where 'a='a]) |
|
580 fix x |
|
581 from real_arch_simple[of "Max ((\<lambda>i. - x$$i)`{..<DIM('a)})"] |
|
582 guess k::nat .. note k = this |
|
583 { fix i assume "i < DIM('a)" |
|
584 with k have "- x$$i \<le> real k" |
|
585 by (subst (asm) Max_le_iff) (auto simp: field_simps) |
|
586 then have "- real k \<le> x$$i" by simp } |
|
587 then show "\<exists>n::nat. \<forall>i<DIM('a). - real n \<le> x $$ i" |
|
588 by (auto intro!: exI[of _ k]) |
|
589 qed |
|
590 have "{..a} \<in> sets ?SIGMA" unfolding * |
|
591 by (safe intro!: countable_UN) |
|
592 (auto simp: sets_sigma intro!: sigma_sets.Basic) } |
|
593 then show ?thesis by (intro sets_sigma_subset) auto |
|
594 qed |
|
595 |
|
596 lemma borel_eq_atMost: |
|
597 "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> a. {.. a::'a\<Colon>ordered_euclidean_space})\<rparr>)" |
|
598 (is "_ = ?SIGMA") |
553 (is "_ = ?SIGMA") |
599 proof (intro algebra.equality antisym) |
554 proof (rule borel_eq_sigmaI1[OF borel_def]) |
600 show "sets borel \<subseteq> sets ?SIGMA" |
555 fix M :: "'a set" assume "M \<in> {S. open S}" |
601 using halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace |
556 then have "open M" by simp |
602 by auto |
557 show "M \<in> ?SIGMA" |
603 show "sets ?SIGMA \<subseteq> sets borel" |
558 apply (subst open_UNION[OF `open M`]) |
604 by (rule borel.sets_sigma_subset) auto |
559 apply (safe intro!: countable_UN) |
|
560 apply auto |
|
561 done |
605 qed auto |
562 qed auto |
606 |
563 |
607 lemma borel_eq_atLeastAtMost: |
564 lemma borel_eq_atLeastLessThan: |
608 "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space, b). {a .. b})\<rparr>)" |
565 "borel = sigma UNIV (range (\<lambda>(a, b). {a ..< b :: real}))" (is "_ = ?SIGMA") |
609 (is "_ = ?SIGMA") |
566 proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan]) |
610 proof (intro algebra.equality antisym) |
567 have move_uminus: "\<And>x y::real. -x \<le> y \<longleftrightarrow> -y \<le> x" by auto |
611 show "sets borel \<subseteq> sets ?SIGMA" |
568 fix x :: real |
612 using atMost_span_atLeastAtMost halfspace_le_span_atMost |
569 have "{..<x} = (\<Union>i::nat. {-real i ..< x})" |
613 halfspace_span_halfspace_le open_span_halfspace |
570 by (auto simp: move_uminus real_arch_simple) |
614 by auto |
571 then show "{..< x} \<in> ?SIGMA" |
615 show "sets ?SIGMA \<subseteq> sets borel" |
572 by (auto intro: sigma_sets.intros) |
616 by (rule borel.sets_sigma_subset) auto |
|
617 qed auto |
573 qed auto |
618 |
574 |
619 lemma borel_eq_greaterThan: |
575 lemma borel_measurable_halfspacesI: |
620 "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space). {a <..})\<rparr>)" |
|
621 (is "_ = ?SIGMA") |
|
622 proof (intro algebra.equality antisym) |
|
623 show "sets borel \<subseteq> sets ?SIGMA" |
|
624 using halfspace_le_span_greaterThan |
|
625 halfspace_span_halfspace_le open_span_halfspace |
|
626 by auto |
|
627 show "sets ?SIGMA \<subseteq> sets borel" |
|
628 by (rule borel.sets_sigma_subset) auto |
|
629 qed auto |
|
630 |
|
631 lemma borel_eq_lessThan: |
|
632 "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space). {..< a})\<rparr>)" |
|
633 (is "_ = ?SIGMA") |
|
634 proof (intro algebra.equality antisym) |
|
635 show "sets borel \<subseteq> sets ?SIGMA" |
|
636 using halfspace_le_span_lessThan |
|
637 halfspace_span_halfspace_ge open_span_halfspace |
|
638 by auto |
|
639 show "sets ?SIGMA \<subseteq> sets borel" |
|
640 by (rule borel.sets_sigma_subset) auto |
|
641 qed auto |
|
642 |
|
643 lemma borel_eq_greaterThanLessThan: |
|
644 "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, b). {a <..< (b :: 'a \<Colon> ordered_euclidean_space)})\<rparr>)" |
|
645 (is "_ = ?SIGMA") |
|
646 proof (intro algebra.equality antisym) |
|
647 show "sets ?SIGMA \<subseteq> sets borel" |
|
648 by (rule borel.sets_sigma_subset) auto |
|
649 show "sets borel \<subseteq> sets ?SIGMA" |
|
650 proof - |
|
651 have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto |
|
652 then interpret sigma_algebra ?SIGMA . |
|
653 { fix M :: "'a set" assume "M \<in> {S. open S}" |
|
654 then have "open M" by simp |
|
655 have "M \<in> sets ?SIGMA" |
|
656 apply (subst open_UNION[OF `open M`]) |
|
657 apply (safe intro!: countable_UN) |
|
658 apply (auto simp add: sigma_def intro!: sigma_sets.Basic) |
|
659 done } |
|
660 then show ?thesis |
|
661 unfolding borel_def by (intro sets_sigma_subset) auto |
|
662 qed |
|
663 qed auto |
|
664 |
|
665 lemma borel_eq_atLeastLessThan: |
|
666 "borel = sigma \<lparr>space=UNIV, sets=range (\<lambda>(a, b). {a ..< b :: real})\<rparr>" (is "_ = ?S") |
|
667 proof (intro algebra.equality antisym) |
|
668 interpret sigma_algebra ?S |
|
669 by (rule sigma_algebra_sigma) auto |
|
670 show "sets borel \<subseteq> sets ?S" |
|
671 unfolding borel_eq_lessThan |
|
672 proof (intro sets_sigma_subset subsetI) |
|
673 have move_uminus: "\<And>x y::real. -x \<le> y \<longleftrightarrow> -y \<le> x" by auto |
|
674 fix A :: "real set" assume "A \<in> sets \<lparr>space = UNIV, sets = range lessThan\<rparr>" |
|
675 then obtain x where "A = {..< x}" by auto |
|
676 then have "A = (\<Union>i::nat. {-real i ..< x})" |
|
677 by (auto simp: move_uminus real_arch_simple) |
|
678 then show "A \<in> sets ?S" |
|
679 by (auto simp: sets_sigma intro!: sigma_sets.intros) |
|
680 qed simp |
|
681 show "sets ?S \<subseteq> sets borel" |
|
682 by (intro borel.sets_sigma_subset) auto |
|
683 qed simp_all |
|
684 |
|
685 lemma borel_eq_halfspace_le: |
|
686 "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i \<le> a})\<rparr>)" |
|
687 (is "_ = ?SIGMA") |
|
688 proof (intro algebra.equality antisym) |
|
689 show "sets borel \<subseteq> sets ?SIGMA" |
|
690 using open_span_halfspace halfspace_span_halfspace_le by auto |
|
691 show "sets ?SIGMA \<subseteq> sets borel" |
|
692 by (rule borel.sets_sigma_subset) auto |
|
693 qed auto |
|
694 |
|
695 lemma borel_eq_halfspace_less: |
|
696 "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i < a})\<rparr>)" |
|
697 (is "_ = ?SIGMA") |
|
698 proof (intro algebra.equality antisym) |
|
699 show "sets borel \<subseteq> sets ?SIGMA" |
|
700 using open_span_halfspace . |
|
701 show "sets ?SIGMA \<subseteq> sets borel" |
|
702 by (rule borel.sets_sigma_subset) auto |
|
703 qed auto |
|
704 |
|
705 lemma borel_eq_halfspace_gt: |
|
706 "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a < x$$i})\<rparr>)" |
|
707 (is "_ = ?SIGMA") |
|
708 proof (intro algebra.equality antisym) |
|
709 show "sets borel \<subseteq> sets ?SIGMA" |
|
710 using halfspace_le_span_halfspace_gt open_span_halfspace halfspace_span_halfspace_le by auto |
|
711 show "sets ?SIGMA \<subseteq> sets borel" |
|
712 by (rule borel.sets_sigma_subset) auto |
|
713 qed auto |
|
714 |
|
715 lemma borel_eq_halfspace_ge: |
|
716 "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a \<le> x$$i})\<rparr>)" |
|
717 (is "_ = ?SIGMA") |
|
718 proof (intro algebra.equality antisym) |
|
719 show "sets borel \<subseteq> sets ?SIGMA" |
|
720 using halfspace_span_halfspace_ge open_span_halfspace by auto |
|
721 show "sets ?SIGMA \<subseteq> sets borel" |
|
722 by (rule borel.sets_sigma_subset) auto |
|
723 qed auto |
|
724 |
|
725 lemma (in sigma_algebra) borel_measurable_halfspacesI: |
|
726 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" |
576 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" |
727 assumes "borel = (sigma \<lparr>space=UNIV, sets=range F\<rparr>)" |
577 assumes F: "borel = sigma UNIV (range F)" |
728 and "\<And>a i. S a i = f -` F (a,i) \<inter> space M" |
578 and S_eq: "\<And>a i. S a i = f -` F (a,i) \<inter> space M" |
729 and "\<And>a i. \<not> i < DIM('c) \<Longrightarrow> S a i \<in> sets M" |
579 and S: "\<And>a i. \<not> i < DIM('c) \<Longrightarrow> S a i \<in> sets M" |
730 shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a::real. 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)" |
731 proof safe |
581 proof safe |
732 fix a :: real and i assume i: "i < DIM('c)" and f: "f \<in> borel_measurable M" |
582 fix a :: real and i assume i: "i < DIM('c)" and f: "f \<in> borel_measurable M" |
733 then show "S a i \<in> sets M" unfolding assms |
583 then show "S a i \<in> sets M" unfolding assms |
734 by (auto intro!: measurable_sets sigma_sets.Basic simp: assms(1) sigma_def) |
584 by (auto intro!: measurable_sets sigma_sets.Basic simp: assms(1)) |
735 next |
585 next |
736 assume a: "\<forall>i<DIM('c). \<forall>a. S a i \<in> sets M" |
586 assume a: "\<forall>i<DIM('c). \<forall>a. S a i \<in> sets M" |
737 { fix a i have "S a i \<in> sets M" |
587 { fix a i have "S a i \<in> sets M" |
738 proof cases |
588 proof cases |
739 assume "i < DIM('c)" |
589 assume "i < DIM('c)" |
740 with a show ?thesis unfolding assms(2) by simp |
590 with a show ?thesis unfolding assms(2) by simp |
741 next |
591 next |
742 assume "\<not> i < DIM('c)" |
592 assume "\<not> i < DIM('c)" |
743 from assms(3)[OF this] show ?thesis . |
593 from S[OF this] show ?thesis . |
744 qed } |
594 qed } |
745 then have "f \<in> measurable M (sigma \<lparr>space=UNIV, sets=range F\<rparr>)" |
595 then show "f \<in> borel_measurable M" |
746 by (auto intro!: measurable_sigma simp: assms(2)) |
596 by (auto intro!: measurable_measure_of simp: S_eq F) |
747 then show "f \<in> borel_measurable M" unfolding measurable_def |
597 qed |
748 unfolding assms(1) by simp |
598 |
749 qed |
599 lemma borel_measurable_iff_halfspace_le: |
750 |
|
751 lemma (in sigma_algebra) borel_measurable_iff_halfspace_le: |
|
752 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" |
600 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" |
753 shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. f w $$ i \<le> a} \<in> sets M)" |
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)" |
754 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto |
602 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto |
755 |
603 |
756 lemma (in sigma_algebra) borel_measurable_iff_halfspace_less: |
604 lemma borel_measurable_iff_halfspace_less: |
757 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" |
605 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" |
758 shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. f w $$ i < a} \<in> sets M)" |
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)" |
759 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto |
607 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto |
760 |
608 |
761 lemma (in sigma_algebra) borel_measurable_iff_halfspace_ge: |
609 lemma borel_measurable_iff_halfspace_ge: |
762 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" |
610 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" |
763 shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. a \<le> f w $$ i} \<in> sets M)" |
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)" |
764 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto |
612 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto |
765 |
613 |
766 lemma (in sigma_algebra) borel_measurable_iff_halfspace_greater: |
614 lemma borel_measurable_iff_halfspace_greater: |
767 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" |
615 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" |
768 shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. a < f w $$ i} \<in> sets M)" |
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)" |
769 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_gt]) auto |
617 by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_greater]) auto |
770 |
618 |
771 lemma (in sigma_algebra) borel_measurable_iff_le: |
619 lemma borel_measurable_iff_le: |
772 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)" |
620 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)" |
773 using borel_measurable_iff_halfspace_le[where 'c=real] by simp |
621 using borel_measurable_iff_halfspace_le[where 'c=real] by simp |
774 |
622 |
775 lemma (in sigma_algebra) borel_measurable_iff_less: |
623 lemma borel_measurable_iff_less: |
776 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)" |
624 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)" |
777 using borel_measurable_iff_halfspace_less[where 'c=real] by simp |
625 using borel_measurable_iff_halfspace_less[where 'c=real] by simp |
778 |
626 |
779 lemma (in sigma_algebra) borel_measurable_iff_ge: |
627 lemma borel_measurable_iff_ge: |
780 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)" |
628 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)" |
781 using borel_measurable_iff_halfspace_ge[where 'c=real] by simp |
629 using borel_measurable_iff_halfspace_ge[where 'c=real] by simp |
782 |
630 |
783 lemma (in sigma_algebra) borel_measurable_iff_greater: |
631 lemma borel_measurable_iff_greater: |
784 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)" |
632 "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)" |
785 using borel_measurable_iff_halfspace_greater[where 'c=real] by simp |
633 using borel_measurable_iff_halfspace_greater[where 'c=real] by simp |
786 |
634 |
787 lemma borel_measurable_euclidean_component: |
635 lemma borel_measurable_euclidean_component: |
788 "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel" |
636 "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel" |
789 unfolding borel_def[where 'a=real] |
637 proof (rule borel_measurableI) |
790 proof (rule borel.measurable_sigma, simp_all) |
|
791 fix S::"real set" assume "open S" |
638 fix S::"real set" assume "open S" |
792 from open_vimage_euclidean_component[OF this] |
639 from open_vimage_euclidean_component[OF this] |
793 show "(\<lambda>x. x $$ i) -` S \<in> sets borel" |
640 show "(\<lambda>x. x $$ i) -` S \<inter> space borel \<in> sets borel" |
794 by (auto intro: borel_open) |
641 by (auto intro: borel_open) |
795 qed |
642 qed |
796 |
643 |
797 lemma (in sigma_algebra) borel_measurable_euclidean_space: |
644 lemma borel_measurable_euclidean_space: |
798 fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space" |
645 fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space" |
799 shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M)" |
646 shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M)" |
800 proof safe |
647 proof safe |
801 fix i assume "f \<in> borel_measurable M" |
648 fix i assume "f \<in> borel_measurable M" |
802 then show "(\<lambda>x. f x $$ i) \<in> borel_measurable M" |
649 then show "(\<lambda>x. f x $$ i) \<in> borel_measurable M" |
1089 also have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) = log b" |
935 also have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) = log b" |
1090 by (simp add: fun_eq_iff not_less log_imp) |
936 by (simp add: fun_eq_iff not_less log_imp) |
1091 finally show ?thesis . |
937 finally show ?thesis . |
1092 qed |
938 qed |
1093 |
939 |
1094 lemma (in sigma_algebra) borel_measurable_log[simp,intro]: |
940 lemma borel_measurable_log[simp,intro]: |
1095 assumes f: "f \<in> borel_measurable M" and "1 < b" |
941 assumes f: "f \<in> borel_measurable M" and "1 < b" |
1096 shows "(\<lambda>x. log b (f x)) \<in> borel_measurable M" |
942 shows "(\<lambda>x. log b (f x)) \<in> borel_measurable M" |
1097 using measurable_comp[OF f borel_measurable_borel_log[OF `1 < b`]] |
943 using measurable_comp[OF f borel_measurable_borel_log[OF `1 < b`]] |
1098 by (simp add: comp_def) |
944 by (simp add: comp_def) |
1099 |
945 |
1100 subsection "Borel space on the extended reals" |
946 subsection "Borel space on the extended reals" |
1101 |
947 |
1102 lemma borel_measurable_ereal_borel: |
948 lemma borel_measurable_ereal_borel: |
1103 "ereal \<in> borel_measurable borel" |
949 "ereal \<in> borel_measurable borel" |
1104 unfolding borel_def[where 'a=ereal] |
950 proof (rule borel_measurableI) |
1105 proof (rule borel.measurable_sigma) |
951 fix X :: "ereal set" assume "open X" |
1106 fix X :: "ereal set" assume "X \<in> sets \<lparr>space = UNIV, sets = {S. open S} \<rparr>" |
|
1107 then have "open X" by simp |
|
1108 then have "open (ereal -` X \<inter> space borel)" |
952 then have "open (ereal -` X \<inter> space borel)" |
1109 by (simp add: open_ereal_vimage) |
953 by (simp add: open_ereal_vimage) |
1110 then show "ereal -` X \<inter> space borel \<in> sets borel" by auto |
954 then show "ereal -` X \<inter> space borel \<in> sets borel" by auto |
1111 qed auto |
955 qed |
1112 |
956 |
1113 lemma (in sigma_algebra) borel_measurable_ereal[simp, intro]: |
957 lemma borel_measurable_ereal[simp, intro]: |
1114 assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" |
958 assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M" |
1115 using measurable_comp[OF f borel_measurable_ereal_borel] unfolding comp_def . |
959 using measurable_comp[OF f borel_measurable_ereal_borel] unfolding comp_def . |
1116 |
960 |
1117 lemma borel_measurable_real_of_ereal_borel: |
961 lemma borel_measurable_real_of_ereal_borel: |
1118 "(real :: ereal \<Rightarrow> real) \<in> borel_measurable borel" |
962 "(real :: ereal \<Rightarrow> real) \<in> borel_measurable borel" |
1119 unfolding borel_def[where 'a=real] |
963 proof (rule borel_measurableI) |
1120 proof (rule borel.measurable_sigma) |
964 fix B :: "real set" assume "open B" |
1121 fix B :: "real set" assume "B \<in> sets \<lparr>space = UNIV, sets = {S. open S} \<rparr>" |
|
1122 then have "open B" by simp |
|
1123 have *: "ereal -` real -` (B - {0}) = B - {0}" by auto |
965 have *: "ereal -` real -` (B - {0}) = B - {0}" by auto |
1124 have open_real: "open (real -` (B - {0}) :: ereal set)" |
966 have open_real: "open (real -` (B - {0}) :: ereal set)" |
1125 unfolding open_ereal_def * using `open B` by auto |
967 unfolding open_ereal_def * using `open B` by auto |
1126 show "(real -` B \<inter> space borel :: ereal set) \<in> sets borel" |
968 show "(real -` B \<inter> space borel :: ereal set) \<in> sets borel" |
1127 proof cases |
969 proof cases |
1242 proof (intro set_eqI) fix x show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" by (cases "f x") auto qed |
1083 proof (intro set_eqI) fix x show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" by (cases "f x") auto qed |
1243 ultimately show "{w \<in> space M. real (f w) \<le> a} \<in> sets M" by auto |
1084 ultimately show "{w \<in> space M. real (f w) \<le> a} \<in> sets M" by auto |
1244 qed |
1085 qed |
1245 qed (simp add: measurable_sets) |
1086 qed (simp add: measurable_sets) |
1246 |
1087 |
1247 lemma (in sigma_algebra) borel_measurable_eq_atLeast_ereal: |
1088 lemma borel_measurable_eq_atLeast_ereal: |
1248 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a..} \<inter> space M \<in> sets M)" |
1089 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a..} \<inter> space M \<in> sets M)" |
1249 proof |
1090 proof |
1250 assume pos: "\<forall>a. f -` {a..} \<inter> space M \<in> sets M" |
1091 assume pos: "\<forall>a. f -` {a..} \<inter> space M \<in> sets M" |
1251 moreover have "\<And>a. (\<lambda>x. - f x) -` {..a} = f -` {-a ..}" |
1092 moreover have "\<And>a. (\<lambda>x. - f x) -` {..a} = f -` {-a ..}" |
1252 by (auto simp: ereal_uminus_le_reorder) |
1093 by (auto simp: ereal_uminus_le_reorder) |
1253 ultimately have "(\<lambda>x. - f x) \<in> borel_measurable M" |
1094 ultimately have "(\<lambda>x. - f x) \<in> borel_measurable M" |
1254 unfolding borel_measurable_eq_atMost_ereal by auto |
1095 unfolding borel_measurable_eq_atMost_ereal by auto |
1255 then show "f \<in> borel_measurable M" by simp |
1096 then show "f \<in> borel_measurable M" by simp |
1256 qed (simp add: measurable_sets) |
1097 qed (simp add: measurable_sets) |
1257 |
1098 |
1258 lemma (in sigma_algebra) borel_measurable_ereal_iff_less: |
1099 lemma borel_measurable_ereal_iff_less: |
1259 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..< a} \<inter> space M \<in> sets M)" |
1100 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..< a} \<inter> space M \<in> sets M)" |
1260 unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable .. |
1101 unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable .. |
1261 |
1102 |
1262 lemma (in sigma_algebra) borel_measurable_ereal_iff_ge: |
1103 lemma borel_measurable_ereal_iff_ge: |
1263 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a <..} \<inter> space M \<in> sets M)" |
1104 "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a <..} \<inter> space M \<in> sets M)" |
1264 unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable .. |
1105 unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable .. |
1265 |
1106 |
1266 lemma (in sigma_algebra) borel_measurable_ereal_eq_const: |
1107 lemma borel_measurable_ereal_eq_const: |
1267 fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M" |
1108 fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M" |
1268 shows "{x\<in>space M. f x = c} \<in> sets M" |
1109 shows "{x\<in>space M. f x = c} \<in> sets M" |
1269 proof - |
1110 proof - |
1270 have "{x\<in>space M. f x = c} = (f -` {c} \<inter> space M)" by auto |
1111 have "{x\<in>space M. f x = c} = (f -` {c} \<inter> space M)" by auto |
1271 then show ?thesis using assms by (auto intro!: measurable_sets) |
1112 then show ?thesis using assms by (auto intro!: measurable_sets) |
1272 qed |
1113 qed |
1273 |
1114 |
1274 lemma (in sigma_algebra) borel_measurable_ereal_neq_const: |
1115 lemma borel_measurable_ereal_neq_const: |
1275 fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M" |
1116 fixes f :: "'a \<Rightarrow> ereal" assumes "f \<in> borel_measurable M" |
1276 shows "{x\<in>space M. f x \<noteq> c} \<in> sets M" |
1117 shows "{x\<in>space M. f x \<noteq> c} \<in> sets M" |
1277 proof - |
1118 proof - |
1278 have "{x\<in>space M. f x \<noteq> c} = space M - (f -` {c} \<inter> space M)" by auto |
1119 have "{x\<in>space M. f x \<noteq> c} = space M - (f -` {c} \<inter> space M)" by auto |
1279 then show ?thesis using assms by (auto intro!: measurable_sets) |
1120 then show ?thesis using assms by (auto intro!: measurable_sets) |
1280 qed |
1121 qed |
1281 |
1122 |
1282 lemma (in sigma_algebra) borel_measurable_ereal_le[intro,simp]: |
1123 lemma borel_measurable_ereal_le[intro,simp]: |
1283 fixes f g :: "'a \<Rightarrow> ereal" |
1124 fixes f g :: "'a \<Rightarrow> ereal" |
1284 assumes f: "f \<in> borel_measurable M" |
1125 assumes f: "f \<in> borel_measurable M" |
1285 assumes g: "g \<in> borel_measurable M" |
1126 assumes g: "g \<in> borel_measurable M" |
1286 shows "{x \<in> space M. f x \<le> g x} \<in> sets M" |
1127 shows "{x \<in> space M. f x \<le> g x} \<in> sets M" |
1287 proof - |
1128 proof - |
1292 fix x show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" by (cases rule: ereal2_cases[of "f x" "g x"]) auto |
1133 fix x show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" by (cases rule: ereal2_cases[of "f x" "g x"]) auto |
1293 qed |
1134 qed |
1294 with f g show ?thesis by (auto intro!: Un simp: measurable_sets) |
1135 with f g show ?thesis by (auto intro!: Un simp: measurable_sets) |
1295 qed |
1136 qed |
1296 |
1137 |
1297 lemma (in sigma_algebra) borel_measurable_ereal_less[intro,simp]: |
1138 lemma borel_measurable_ereal_less[intro,simp]: |
1298 fixes f :: "'a \<Rightarrow> ereal" |
1139 fixes f :: "'a \<Rightarrow> ereal" |
1299 assumes f: "f \<in> borel_measurable M" |
1140 assumes f: "f \<in> borel_measurable M" |
1300 assumes g: "g \<in> borel_measurable M" |
1141 assumes g: "g \<in> borel_measurable M" |
1301 shows "{x \<in> space M. f x < g x} \<in> sets M" |
1142 shows "{x \<in> space M. f x < g x} \<in> sets M" |
1302 proof - |
1143 proof - |
1303 have "{x \<in> space M. f x < g x} = space M - {x \<in> space M. g x \<le> f x}" by auto |
1144 have "{x \<in> space M. f x < g x} = space M - {x \<in> space M. g x \<le> f x}" by auto |
1304 then show ?thesis using g f by auto |
1145 then show ?thesis using g f by auto |
1305 qed |
1146 qed |
1306 |
1147 |
1307 lemma (in sigma_algebra) borel_measurable_ereal_eq[intro,simp]: |
1148 lemma borel_measurable_ereal_eq[intro,simp]: |
1308 fixes f :: "'a \<Rightarrow> ereal" |
1149 fixes f :: "'a \<Rightarrow> ereal" |
1309 assumes f: "f \<in> borel_measurable M" |
1150 assumes f: "f \<in> borel_measurable M" |
1310 assumes g: "g \<in> borel_measurable M" |
1151 assumes g: "g \<in> borel_measurable M" |
1311 shows "{w \<in> space M. f w = g w} \<in> sets M" |
1152 shows "{w \<in> space M. f w = g w} \<in> sets M" |
1312 proof - |
1153 proof - |
1313 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 |
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 |
1314 then show ?thesis using g f by auto |
1155 then show ?thesis using g f by auto |
1315 qed |
1156 qed |
1316 |
1157 |
1317 lemma (in sigma_algebra) borel_measurable_ereal_neq[intro,simp]: |
1158 lemma borel_measurable_ereal_neq[intro,simp]: |
1318 fixes f :: "'a \<Rightarrow> ereal" |
1159 fixes f :: "'a \<Rightarrow> ereal" |
1319 assumes f: "f \<in> borel_measurable M" |
1160 assumes f: "f \<in> borel_measurable M" |
1320 assumes g: "g \<in> borel_measurable M" |
1161 assumes g: "g \<in> borel_measurable M" |
1321 shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M" |
1162 shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M" |
1322 proof - |
1163 proof - |
1323 have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}" by auto |
1164 have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}" by auto |
1324 thus ?thesis using f g by auto |
1165 thus ?thesis using f g by auto |
1325 qed |
1166 qed |
1326 |
1167 |
1327 lemma (in sigma_algebra) split_sets: |
1168 lemma split_sets: |
1328 "{x\<in>space M. P x \<or> Q x} = {x\<in>space M. P x} \<union> {x\<in>space M. Q x}" |
1169 "{x\<in>space M. P x \<or> Q x} = {x\<in>space M. P x} \<union> {x\<in>space M. Q x}" |
1329 "{x\<in>space M. P x \<and> Q x} = {x\<in>space M. P x} \<inter> {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}" |
1330 by auto |
1171 by auto |
1331 |
1172 |
1332 lemma (in sigma_algebra) borel_measurable_ereal_add[intro, simp]: |
1173 lemma borel_measurable_ereal_add[intro, simp]: |
1333 fixes f :: "'a \<Rightarrow> ereal" |
1174 fixes f :: "'a \<Rightarrow> ereal" |
1334 assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M" |
1175 assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M" |
1335 shows "(\<lambda>x. f x + g x) \<in> borel_measurable M" |
1176 shows "(\<lambda>x. f x + g x) \<in> borel_measurable M" |
1336 proof - |
1177 proof - |
1337 { fix x assume "x \<in> space M" then have "f x + g x = |
1178 { fix x assume "x \<in> space M" then have "f x + g x = |
1433 by (auto simp: INF_less_iff) |
1274 by (auto simp: INF_less_iff) |
1434 then show "?inf -` {..<a} \<inter> space M \<in> sets M" |
1275 then show "?inf -` {..<a} \<inter> space M \<in> sets M" |
1435 using assms by auto |
1276 using assms by auto |
1436 qed |
1277 qed |
1437 |
1278 |
1438 lemma (in sigma_algebra) borel_measurable_liminf[simp, intro]: |
1279 lemma borel_measurable_liminf[simp, intro]: |
1439 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" |
1280 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" |
1440 assumes "\<And>i. f i \<in> borel_measurable M" |
1281 assumes "\<And>i. f i \<in> borel_measurable M" |
1441 shows "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M" |
1282 shows "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M" |
1442 unfolding liminf_SUPR_INFI using assms by auto |
1283 unfolding liminf_SUPR_INFI using assms by auto |
1443 |
1284 |
1444 lemma (in sigma_algebra) borel_measurable_limsup[simp, intro]: |
1285 lemma borel_measurable_limsup[simp, intro]: |
1445 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" |
1286 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" |
1446 assumes "\<And>i. f i \<in> borel_measurable M" |
1287 assumes "\<And>i. f i \<in> borel_measurable M" |
1447 shows "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M" |
1288 shows "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M" |
1448 unfolding limsup_INFI_SUPR using assms by auto |
1289 unfolding limsup_INFI_SUPR using assms by auto |
1449 |
1290 |
1450 lemma (in sigma_algebra) borel_measurable_ereal_diff[simp, intro]: |
1291 lemma borel_measurable_ereal_diff[simp, intro]: |
1451 fixes f g :: "'a \<Rightarrow> ereal" |
1292 fixes f g :: "'a \<Rightarrow> ereal" |
1452 assumes "f \<in> borel_measurable M" |
1293 assumes "f \<in> borel_measurable M" |
1453 assumes "g \<in> borel_measurable M" |
1294 assumes "g \<in> borel_measurable M" |
1454 shows "(\<lambda>x. f x - g x) \<in> borel_measurable M" |
1295 shows "(\<lambda>x. f x - g x) \<in> borel_measurable M" |
1455 unfolding minus_ereal_def using assms by auto |
1296 unfolding minus_ereal_def using assms by auto |
1456 |
1297 |
1457 lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]: |
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" |
|
1300 proof - |
|
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 } |
|
1303 with f show ?thesis |
|
1304 by (auto intro!: measurable_If) |
|
1305 qed |
|
1306 |
|
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 |
|
1310 |
|
1311 lemma borel_measurable_psuminf[simp, intro]: |
1458 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" |
1312 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal" |
1459 assumes "\<And>i. f i \<in> borel_measurable M" and pos: "\<And>i x. x \<in> space M \<Longrightarrow> 0 \<le> f i x" |
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" |
1460 shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M" |
1314 shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M" |
1461 apply (subst measurable_cong) |
1315 apply (subst measurable_cong) |
1462 apply (subst suminf_ereal_eq_SUPR) |
1316 apply (subst suminf_ereal_eq_SUPR) |
1463 apply (rule pos) |
1317 apply (rule pos) |
1464 using assms by auto |
1318 using assms by auto |
1465 |
1319 |
1466 section "LIMSEQ is borel measurable" |
1320 section "LIMSEQ is borel measurable" |
1467 |
1321 |
1468 lemma (in sigma_algebra) borel_measurable_LIMSEQ: |
1322 lemma borel_measurable_LIMSEQ: |
1469 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real" |
1323 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real" |
1470 assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x" |
1324 assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x" |
1471 and u: "\<And>i. u i \<in> borel_measurable M" |
1325 and u: "\<And>i. u i \<in> borel_measurable M" |
1472 shows "u' \<in> borel_measurable M" |
1326 shows "u' \<in> borel_measurable M" |
1473 proof - |
1327 proof - |