src/HOL/Probability/Borel_Space.thy
author hoelzl
Thu, 12 Jun 2014 15:47:36 +0200
changeset 57235 b0b9a10e4bf4
parent 57138 7b3146180291
child 57259 3a448982a74a
permissions -rw-r--r--
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42150
b0c0638c4aad tuned headers;
wenzelm
parents: 42067
diff changeset
     1
(*  Title:      HOL/Probability/Borel_Space.thy
42067
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     2
    Author:     Johannes Hölzl, TU München
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     3
    Author:     Armin Heller, TU München
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     4
*)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
     5
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
     6
header {*Borel spaces*}
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
     7
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
     8
theory Borel_Space
50387
3d8863c41fe8 Move the measurability prover to its own file
hoelzl
parents: 50245
diff changeset
     9
imports
3d8863c41fe8 Move the measurability prover to its own file
hoelzl
parents: 50245
diff changeset
    10
  Measurable
3d8863c41fe8 Move the measurability prover to its own file
hoelzl
parents: 50245
diff changeset
    11
  "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    12
begin
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    13
56994
8d5e5ec1cac3 fixed document generation for HOL-Probability
hoelzl
parents: 56993
diff changeset
    14
subsection {* Generic Borel spaces *}
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    15
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    16
definition borel :: "'a::topological_space measure" where
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    17
  "borel = sigma UNIV {S. open S}"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    18
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    19
abbreviation "borel_measurable M \<equiv> measurable M borel"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    20
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    21
lemma in_borel_measurable:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    22
   "f \<in> borel_measurable M \<longleftrightarrow>
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    23
    (\<forall>S \<in> sigma_sets UNIV {S. open S}. f -` S \<inter> space M \<in> sets M)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    24
  by (auto simp add: measurable_def borel_def)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    25
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    26
lemma in_borel_measurable_borel:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    27
   "f \<in> borel_measurable M \<longleftrightarrow>
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    28
    (\<forall>S \<in> sets borel.
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    29
      f -` S \<inter> space M \<in> sets M)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    30
  by (auto simp add: measurable_def borel_def)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    31
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    32
lemma space_borel[simp]: "space borel = UNIV"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    33
  unfolding borel_def by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    34
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    35
lemma space_in_borel[measurable]: "UNIV \<in> sets borel"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    36
  unfolding borel_def by auto
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    37
57235
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
    38
lemma sets_borel: "sets borel = sigma_sets UNIV {S. open S}"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
    39
  unfolding borel_def by (rule sets_measure_of) simp
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
    40
50387
3d8863c41fe8 Move the measurability prover to its own file
hoelzl
parents: 50245
diff changeset
    41
lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    42
  unfolding borel_def pred_def by auto
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    43
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    44
lemma borel_open[measurable (raw generic)]:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    45
  assumes "open A" shows "A \<in> sets borel"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    46
proof -
44537
c10485a6a7af make HOL-Probability respect set/pred distinction
huffman
parents: 44282
diff changeset
    47
  have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    48
  thus ?thesis unfolding borel_def by auto
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    49
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    50
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    51
lemma borel_closed[measurable (raw generic)]:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    52
  assumes "closed A" shows "A \<in> sets borel"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    53
proof -
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    54
  have "space borel - (- A) \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    55
    using assms unfolding closed_def by (blast intro: borel_open)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    56
  thus ?thesis by simp
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    57
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    58
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    59
lemma borel_singleton[measurable]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    60
  "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)"
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
    61
  unfolding insert_def by (rule sets.Un) auto
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    62
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    63
lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    64
  unfolding Compl_eq_Diff_UNIV by simp
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
    65
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    66
lemma borel_measurable_vimage:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    67
  fixes f :: "'a \<Rightarrow> 'x::t2_space"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    68
  assumes borel[measurable]: "f \<in> borel_measurable M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    69
  shows "f -` {x} \<inter> space M \<in> sets M"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    70
  by simp
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    71
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    72
lemma borel_measurableI:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    73
  fixes f :: "'a \<Rightarrow> 'x\<Colon>topological_space"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    74
  assumes "\<And>S. open S \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    75
  shows "f \<in> borel_measurable M"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    76
  unfolding borel_def
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    77
proof (rule measurable_measure_of, simp_all)
44537
c10485a6a7af make HOL-Probability respect set/pred distinction
huffman
parents: 44282
diff changeset
    78
  fix S :: "'x set" assume "open S" thus "f -` S \<inter> space M \<in> sets M"
c10485a6a7af make HOL-Probability respect set/pred distinction
huffman
parents: 44282
diff changeset
    79
    using assms[of S] by simp
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    80
qed
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    81
50021
d96a3f468203 add support for function application to measurability prover
hoelzl
parents: 50003
diff changeset
    82
lemma borel_measurable_const:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    83
  "(\<lambda>x. c) \<in> borel_measurable M"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    84
  by auto
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    85
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    86
lemma borel_measurable_indicator:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    87
  assumes A: "A \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    88
  shows "indicator A \<in> borel_measurable M"
46905
6b1c0a80a57a prefer abs_def over def_raw;
wenzelm
parents: 46884
diff changeset
    89
  unfolding indicator_def [abs_def] using A
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    90
  by (auto intro!: measurable_If_set)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    91
50096
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    92
lemma borel_measurable_count_space[measurable (raw)]:
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    93
  "f \<in> borel_measurable (count_space S)"
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    94
  unfolding measurable_def by auto
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    95
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    96
lemma borel_measurable_indicator'[measurable (raw)]:
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    97
  assumes [measurable]: "{x\<in>space M. f x \<in> A x} \<in> sets M"
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    98
  shows "(\<lambda>x. indicator (A x) (f x)) \<in> borel_measurable M"
50001
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49774
diff changeset
    99
  unfolding indicator_def[abs_def]
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49774
diff changeset
   100
  by (auto intro!: measurable_If)
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49774
diff changeset
   101
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   102
lemma borel_measurable_indicator_iff:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   103
  "(indicator A :: 'a \<Rightarrow> 'x::{t1_space, zero_neq_one}) \<in> borel_measurable M \<longleftrightarrow> A \<inter> space M \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   104
    (is "?I \<in> borel_measurable M \<longleftrightarrow> _")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   105
proof
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   106
  assume "?I \<in> borel_measurable M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   107
  then have "?I -` {1} \<inter> space M \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   108
    unfolding measurable_def by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   109
  also have "?I -` {1} \<inter> space M = A \<inter> space M"
46905
6b1c0a80a57a prefer abs_def over def_raw;
wenzelm
parents: 46884
diff changeset
   110
    unfolding indicator_def [abs_def] by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   111
  finally show "A \<inter> space M \<in> sets M" .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   112
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   113
  assume "A \<inter> space M \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   114
  moreover have "?I \<in> borel_measurable M \<longleftrightarrow>
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   115
    (indicator (A \<inter> space M) :: 'a \<Rightarrow> 'x) \<in> borel_measurable M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   116
    by (intro measurable_cong) (auto simp: indicator_def)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   117
  ultimately show "?I \<in> borel_measurable M" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   118
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   119
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   120
lemma borel_measurable_subalgebra:
41545
9c869baf1c66 tuned formalization of subalgebra
hoelzl
parents: 41097
diff changeset
   121
  assumes "sets N \<subseteq> sets M" "space N = space M" "f \<in> borel_measurable N"
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   122
  shows "f \<in> borel_measurable M"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   123
  using assms unfolding measurable_def by auto
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   124
57137
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   125
lemma borel_measurable_restrict_space_iff_ereal:
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   126
  fixes f :: "'a \<Rightarrow> ereal"
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   127
  assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M"
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   128
  shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   129
    (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
57138
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   130
  by (subst measurable_restrict_space_iff)
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   131
     (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_cong)
57137
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   132
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   133
lemma borel_measurable_restrict_space_iff:
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   134
  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   135
  assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M"
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   136
  shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   137
    (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M"
57138
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   138
  by (subst measurable_restrict_space_iff)
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   139
     (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] mult_ac cong del: if_cong)
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   140
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   141
lemma cbox_borel[measurable]: "cbox a b \<in> sets borel"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   142
  by (auto intro: borel_closed)
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   143
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   144
lemma borel_compact: "compact (A::'a::t2_space set) \<Longrightarrow> A \<in> sets borel"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   145
  by (auto intro: borel_closed dest!: compact_imp_closed)
57137
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   146
57138
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   147
lemma borel_measurable_continuous_on_if:
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   148
  assumes A: "A \<in> sets borel" and f: "continuous_on A f" and g: "continuous_on (- A) g"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   149
  shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> borel_measurable borel"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   150
proof (rule borel_measurableI)
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   151
  fix S :: "'b set" assume "open S"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   152
  have "(\<lambda>x. if x \<in> A then f x else g x) -` S \<inter> space borel = (f -` S \<inter> A) \<union> (g -` S \<inter> -A)"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   153
    by (auto split: split_if_asm)
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   154
  moreover obtain A' where "f -` S \<inter> A = A' \<inter> A" "open A'"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   155
    using continuous_on_open_invariant[THEN iffD1, rule_format, OF f `open S`] by metis
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   156
  moreover obtain B' where "g -` S \<inter> -A = B' \<inter> -A" "open B'"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   157
    using continuous_on_open_invariant[THEN iffD1, rule_format, OF g `open S`] by metis
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   158
  ultimately show "(\<lambda>x. if x \<in> A then f x else g x) -` S \<inter> space borel \<in> sets borel"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   159
    using A by auto
57137
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   160
qed
f174712d0a84 better support for restrict_space
hoelzl
parents: 57036
diff changeset
   161
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   162
lemma borel_measurable_continuous_on1:
57138
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   163
  "continuous_on UNIV f \<Longrightarrow> f \<in> borel_measurable borel"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   164
  using borel_measurable_continuous_on_if[of UNIV f "\<lambda>_. undefined"]
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   165
  by (auto intro: continuous_on_const)
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   166
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   167
lemma borel_measurable_continuous_on:
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   168
  assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   169
  shows "(\<lambda>x. f (g x)) \<in> borel_measurable M"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   170
  using measurable_comp[OF g borel_measurable_continuous_on1[OF f]] by (simp add: comp_def)
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   171
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   172
lemma borel_measurable_continuous_on_open':
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   173
  "continuous_on A f \<Longrightarrow> open A \<Longrightarrow>
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   174
    (\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   175
  using borel_measurable_continuous_on_if[of A f "\<lambda>_. c"] by (auto intro: continuous_on_const)
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   176
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   177
lemma borel_measurable_continuous_on_open:
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   178
  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   179
  assumes cont: "continuous_on A f" "open A"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   180
  assumes g: "g \<in> borel_measurable M"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   181
  shows "(\<lambda>x. if g x \<in> A then f (g x) else c) \<in> borel_measurable M"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   182
  using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   183
  by (simp add: comp_def)
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   184
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   185
lemma borel_measurable_continuous_on_indicator:
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   186
  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   187
  assumes A: "A \<in> sets borel" and f: "continuous_on A f"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   188
  shows "(\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable borel"
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   189
  using borel_measurable_continuous_on_if[OF assms, of "\<lambda>_. 0"]
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   190
  by (simp add: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] continuous_on_const
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   191
           cong del: if_cong)
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   192
50245
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   193
lemma borel_eq_countable_basis:
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   194
  fixes B::"'a::topological_space set set"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   195
  assumes "countable B"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   196
  assumes "topological_basis B"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   197
  shows "borel = sigma UNIV B"
50087
635d73673b5e regularity of measures, therefore:
immler
parents: 50021
diff changeset
   198
  unfolding borel_def
635d73673b5e regularity of measures, therefore:
immler
parents: 50021
diff changeset
   199
proof (intro sigma_eqI sigma_sets_eqI, safe)
50245
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   200
  interpret countable_basis using assms by unfold_locales
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   201
  fix X::"'a set" assume "open X"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   202
  from open_countable_basisE[OF this] guess B' . note B' = this
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   203
  then show "X \<in> sigma_sets UNIV B"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   204
    by (blast intro: sigma_sets_UNION `countable B` countable_subset)
50087
635d73673b5e regularity of measures, therefore:
immler
parents: 50021
diff changeset
   205
next
50245
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   206
  fix b assume "b \<in> B"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   207
  hence "open b" by (rule topological_basis_open[OF assms(2)])
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   208
  thus "b \<in> sigma_sets UNIV (Collect open)" by auto
50087
635d73673b5e regularity of measures, therefore:
immler
parents: 50021
diff changeset
   209
qed simp_all
635d73673b5e regularity of measures, therefore:
immler
parents: 50021
diff changeset
   210
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   211
lemma borel_measurable_Pair[measurable (raw)]:
50881
ae630bab13da renamed countable_basis_space to second_countable_topology
hoelzl
parents: 50526
diff changeset
   212
  fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   213
  assumes f[measurable]: "f \<in> borel_measurable M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   214
  assumes g[measurable]: "g \<in> borel_measurable M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   215
  shows "(\<lambda>x. (f x, g x)) \<in> borel_measurable M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   216
proof (subst borel_eq_countable_basis)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   217
  let ?B = "SOME B::'b set set. countable B \<and> topological_basis B"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   218
  let ?C = "SOME B::'c set set. countable B \<and> topological_basis B"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   219
  let ?P = "(\<lambda>(b, c). b \<times> c) ` (?B \<times> ?C)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   220
  show "countable ?P" "topological_basis ?P"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   221
    by (auto intro!: countable_basis topological_basis_prod is_basis)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   222
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   223
  show "(\<lambda>x. (f x, g x)) \<in> measurable M (sigma UNIV ?P)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   224
  proof (rule measurable_measure_of)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   225
    fix S assume "S \<in> ?P"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   226
    then obtain b c where "b \<in> ?B" "c \<in> ?C" and S: "S = b \<times> c" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   227
    then have borel: "open b" "open c"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   228
      by (auto intro: is_basis topological_basis_open)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   229
    have "(\<lambda>x. (f x, g x)) -` S \<inter> space M = (f -` b \<inter> space M) \<inter> (g -` c \<inter> space M)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   230
      unfolding S by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   231
    also have "\<dots> \<in> sets M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   232
      using borel by simp
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   233
    finally show "(\<lambda>x. (f x, g x)) -` S \<inter> space M \<in> sets M" .
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   234
  qed auto
39087
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   235
qed
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   236
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   237
lemma borel_measurable_continuous_Pair:
50881
ae630bab13da renamed countable_basis_space to second_countable_topology
hoelzl
parents: 50526
diff changeset
   238
  fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   239
  assumes [measurable]: "f \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   240
  assumes [measurable]: "g \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   241
  assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   242
  shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   243
proof -
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   244
  have eq: "(\<lambda>x. H (f x) (g x)) = (\<lambda>x. (\<lambda>x. H (fst x) (snd x)) (f x, g x))" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   245
  show ?thesis
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   246
    unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   247
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   248
56994
8d5e5ec1cac3 fixed document generation for HOL-Probability
hoelzl
parents: 56993
diff changeset
   249
subsection {* Borel spaces on euclidean spaces *}
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   250
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   251
lemma borel_measurable_inner[measurable (raw)]:
50881
ae630bab13da renamed countable_basis_space to second_countable_topology
hoelzl
parents: 50526
diff changeset
   252
  fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   253
  assumes "f \<in> borel_measurable M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   254
  assumes "g \<in> borel_measurable M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   255
  shows "(\<lambda>x. f x \<bullet> g x) \<in> borel_measurable M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   256
  using assms
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   257
  by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   258
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   259
lemma [measurable]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   260
  fixes a b :: "'a\<Colon>linorder_topology"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   261
  shows lessThan_borel: "{..< a} \<in> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   262
    and greaterThan_borel: "{a <..} \<in> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   263
    and greaterThanLessThan_borel: "{a<..<b} \<in> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   264
    and atMost_borel: "{..a} \<in> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   265
    and atLeast_borel: "{a..} \<in> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   266
    and atLeastAtMost_borel: "{a..b} \<in> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   267
    and greaterThanAtMost_borel: "{a<..b} \<in> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   268
    and atLeastLessThan_borel: "{a..<b} \<in> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   269
  unfolding greaterThanAtMost_def atLeastLessThan_def
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   270
  by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   271
                   closed_atMost closed_atLeast closed_atLeastAtMost)+
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   272
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   273
notation
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   274
  eucl_less (infix "<e" 50)
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   275
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   276
lemma box_oc: "{x. a <e x \<and> x \<le> b} = {x. a <e x} \<inter> {..b}"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   277
  and box_co: "{x. a \<le> x \<and> x <e b} = {a..} \<inter> {x. x <e b}"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   278
  by auto
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   279
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   280
lemma eucl_ivals[measurable]:
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   281
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   282
  shows "{x. x <e a} \<in> sets borel"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   283
    and "{x. a <e x} \<in> sets borel"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   284
    and "box a b \<in> sets borel"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   285
    and "{..a} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   286
    and "{a..} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   287
    and "{a..b} \<in> sets borel"
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   288
    and  "{x. a <e x \<and> x \<le> b} \<in> sets borel"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   289
    and "{x. a \<le> x \<and>  x <e b} \<in> sets borel"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   290
  unfolding box_oc box_co
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   291
  by (auto intro: borel_open borel_closed)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   292
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   293
lemma open_Collect_less:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51683
diff changeset
   294
  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   295
  assumes "continuous_on UNIV f"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   296
  assumes "continuous_on UNIV g"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   297
  shows "open {x. f x < g x}"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   298
proof -
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   299
  have "open (\<Union>y. {x \<in> UNIV. f x \<in> {..< y}} \<inter> {x \<in> UNIV. g x \<in> {y <..}})" (is "open ?X")
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   300
    by (intro open_UN ballI open_Int continuous_open_preimage assms) auto
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   301
  also have "?X = {x. f x < g x}"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   302
    by (auto intro: dense)
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   303
  finally show ?thesis .
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   304
qed
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   305
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   306
lemma closed_Collect_le:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51683
diff changeset
   307
  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   308
  assumes f: "continuous_on UNIV f"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   309
  assumes g: "continuous_on UNIV g"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   310
  shows "closed {x. f x \<le> g x}"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   311
  using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed .
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   312
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   313
lemma borel_measurable_less[measurable]:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51683
diff changeset
   314
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   315
  assumes "f \<in> borel_measurable M"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   316
  assumes "g \<in> borel_measurable M"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   317
  shows "{w \<in> space M. f w < g w} \<in> sets M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   318
proof -
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   319
  have "{w \<in> space M. f w < g w} = (\<lambda>x. (f x, g x)) -` {x. fst x < snd x} \<inter> space M"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   320
    by auto
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   321
  also have "\<dots> \<in> sets M"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   322
    by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less]
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   323
              continuous_intros)
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   324
  finally show ?thesis .
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   325
qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   326
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   327
lemma
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51683
diff changeset
   328
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   329
  assumes f[measurable]: "f \<in> borel_measurable M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   330
  assumes g[measurable]: "g \<in> borel_measurable M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   331
  shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   332
    and borel_measurable_eq[measurable]: "{w \<in> space M. f w = g w} \<in> sets M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   333
    and borel_measurable_neq: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   334
  unfolding eq_iff not_less[symmetric]
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   335
  by measurable
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   336
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   337
lemma 
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   338
  fixes i :: "'a::{second_countable_topology, real_inner}"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   339
  shows hafspace_less_borel: "{x. a < x \<bullet> i} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   340
    and hafspace_greater_borel: "{x. x \<bullet> i < a} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   341
    and hafspace_less_eq_borel: "{x. a \<le> x \<bullet> i} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   342
    and hafspace_greater_eq_borel: "{x. x \<bullet> i \<le> a} \<in> sets borel"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   343
  by simp_all
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   344
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   345
subsection "Borel space equals sigma algebras over intervals"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   346
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   347
lemma borel_sigma_sets_subset:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   348
  "A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   349
  using sets.sigma_sets_subset[of A borel] by simp
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   350
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   351
lemma borel_eq_sigmaI1:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   352
  fixes F :: "'i \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   353
  assumes borel_eq: "borel = sigma UNIV X"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   354
  assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV (F ` A))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   355
  assumes F: "\<And>i. i \<in> A \<Longrightarrow> F i \<in> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   356
  shows "borel = sigma UNIV (F ` A)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   357
  unfolding borel_def
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   358
proof (intro sigma_eqI antisym)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   359
  have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   360
    unfolding borel_def by simp
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   361
  also have "\<dots> = sigma_sets UNIV X"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   362
    unfolding borel_eq by simp
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   363
  also have "\<dots> \<subseteq> sigma_sets UNIV (F`A)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   364
    using X by (intro sigma_algebra.sigma_sets_subset[OF sigma_algebra_sigma_sets]) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   365
  finally show "sigma_sets UNIV {S. open S} \<subseteq> sigma_sets UNIV (F`A)" .
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   366
  show "sigma_sets UNIV (F`A) \<subseteq> sigma_sets UNIV {S. open S}"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   367
    unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   368
qed auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   369
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   370
lemma borel_eq_sigmaI2:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   371
  fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   372
    and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   373
  assumes borel_eq: "borel = sigma UNIV ((\<lambda>(i, j). G i j)`B)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   374
  assumes X: "\<And>i j. (i, j) \<in> B \<Longrightarrow> G i j \<in> sets (sigma UNIV ((\<lambda>(i, j). F i j) ` A))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   375
  assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   376
  shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   377
  using assms
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   378
  by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` B" and F="(\<lambda>(i, j). F i j)"]) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   379
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   380
lemma borel_eq_sigmaI3:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   381
  fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   382
  assumes borel_eq: "borel = sigma UNIV X"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   383
  assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV ((\<lambda>(i, j). F i j) ` A))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   384
  assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   385
  shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   386
  using assms by (intro borel_eq_sigmaI1[where X=X and F="(\<lambda>(i, j). F i j)"]) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   387
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   388
lemma borel_eq_sigmaI4:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   389
  fixes F :: "'i \<Rightarrow> 'a::topological_space set"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   390
    and G :: "'l \<Rightarrow> 'k \<Rightarrow> 'a::topological_space set"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   391
  assumes borel_eq: "borel = sigma UNIV ((\<lambda>(i, j). G i j)`A)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   392
  assumes X: "\<And>i j. (i, j) \<in> A \<Longrightarrow> G i j \<in> sets (sigma UNIV (range F))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   393
  assumes F: "\<And>i. F i \<in> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   394
  shows "borel = sigma UNIV (range F)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   395
  using assms by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` A" and F=F]) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   396
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   397
lemma borel_eq_sigmaI5:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   398
  fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and G :: "'l \<Rightarrow> 'a::topological_space set"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   399
  assumes borel_eq: "borel = sigma UNIV (range G)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   400
  assumes X: "\<And>i. G i \<in> sets (sigma UNIV (range (\<lambda>(i, j). F i j)))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   401
  assumes F: "\<And>i j. F i j \<in> sets borel"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   402
  shows "borel = sigma UNIV (range (\<lambda>(i, j). F i j))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   403
  using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(\<lambda>(i, j). F i j)"]) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   404
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   405
lemma borel_eq_box:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   406
  "borel = sigma UNIV (range (\<lambda> (a, b). box a b :: 'a \<Colon> euclidean_space set))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   407
    (is "_ = ?SIGMA")
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   408
proof (rule borel_eq_sigmaI1[OF borel_def])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   409
  fix M :: "'a set" assume "M \<in> {S. open S}"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   410
  then have "open M" by simp
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   411
  show "M \<in> ?SIGMA"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   412
    apply (subst open_UNION_box[OF `open M`])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   413
    apply (safe intro!: sets.countable_UN' countable_PiE countable_Collect)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   414
    apply (auto intro: countable_rat)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   415
    done
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   416
qed (auto simp: box_def)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   417
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   418
lemma halfspace_gt_in_halfspace:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   419
  assumes i: "i \<in> A"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   420
  shows "{x\<Colon>'a. a < x \<bullet> i} \<in> 
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   421
    sigma_sets UNIV ((\<lambda> (a, i). {x\<Colon>'a\<Colon>euclidean_space. x \<bullet> i < a}) ` (UNIV \<times> A))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   422
  (is "?set \<in> ?SIGMA")
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   423
proof -
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   424
  interpret sigma_algebra UNIV ?SIGMA
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   425
    by (intro sigma_algebra_sigma_sets) simp_all
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   426
  have *: "?set = (\<Union>n. UNIV - {x\<Colon>'a. x \<bullet> i < a + 1 / real (Suc n)})"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   427
  proof (safe, simp_all add: not_less)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   428
    fix x :: 'a assume "a < x \<bullet> i"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   429
    with reals_Archimedean[of "x \<bullet> i - a"]
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   430
    obtain n where "a + 1 / real (Suc n) < x \<bullet> i"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   431
      by (auto simp: inverse_eq_divide field_simps)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   432
    then show "\<exists>n. a + 1 / real (Suc n) \<le> x \<bullet> i"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   433
      by (blast intro: less_imp_le)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   434
  next
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   435
    fix x n
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   436
    have "a < a + 1 / real (Suc n)" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   437
    also assume "\<dots> \<le> x"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   438
    finally show "a < x" .
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   439
  qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   440
  show "?set \<in> ?SIGMA" unfolding *
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   441
    by (auto del: Diff intro!: Diff i)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   442
qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   443
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   444
lemma borel_eq_halfspace_less:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   445
  "borel = sigma UNIV ((\<lambda>(a, i). {x::'a::euclidean_space. x \<bullet> i < a}) ` (UNIV \<times> Basis))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   446
  (is "_ = ?SIGMA")
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   447
proof (rule borel_eq_sigmaI2[OF borel_eq_box])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   448
  fix a b :: 'a
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   449
  have "box a b = {x\<in>space ?SIGMA. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   450
    by (auto simp: box_def)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   451
  also have "\<dots> \<in> sets ?SIGMA"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   452
    by (intro sets.sets_Collect_conj sets.sets_Collect_finite_All sets.sets_Collect_const)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   453
       (auto intro!: halfspace_gt_in_halfspace countable_PiE countable_rat)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   454
  finally show "box a b \<in> sets ?SIGMA" .
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   455
qed auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   456
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   457
lemma borel_eq_halfspace_le:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   458
  "borel = sigma UNIV ((\<lambda> (a, i). {x::'a::euclidean_space. x \<bullet> i \<le> a}) ` (UNIV \<times> Basis))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   459
  (is "_ = ?SIGMA")
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   460
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   461
  fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   462
  then have i: "i \<in> Basis" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   463
  have *: "{x::'a. x\<bullet>i < a} = (\<Union>n. {x. x\<bullet>i \<le> a - 1/real (Suc n)})"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   464
  proof (safe, simp_all)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   465
    fix x::'a assume *: "x\<bullet>i < a"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   466
    with reals_Archimedean[of "a - x\<bullet>i"]
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   467
    obtain n where "x \<bullet> i < a - 1 / (real (Suc n))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   468
      by (auto simp: field_simps inverse_eq_divide)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   469
    then show "\<exists>n. x \<bullet> i \<le> a - 1 / (real (Suc n))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   470
      by (blast intro: less_imp_le)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   471
  next
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   472
    fix x::'a and n
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   473
    assume "x\<bullet>i \<le> a - 1 / real (Suc n)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   474
    also have "\<dots> < a" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   475
    finally show "x\<bullet>i < a" .
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   476
  qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   477
  show "{x. x\<bullet>i < a} \<in> ?SIGMA" unfolding *
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   478
    by (safe intro!: sets.countable_UN) (auto intro: i)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   479
qed auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   480
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   481
lemma borel_eq_halfspace_ge:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   482
  "borel = sigma UNIV ((\<lambda> (a, i). {x\<Colon>'a\<Colon>euclidean_space. a \<le> x \<bullet> i}) ` (UNIV \<times> Basis))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   483
  (is "_ = ?SIGMA")
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   484
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   485
  fix a :: real and i :: 'a assume i: "(a, i) \<in> UNIV \<times> Basis"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   486
  have *: "{x::'a. x\<bullet>i < a} = space ?SIGMA - {x::'a. a \<le> x\<bullet>i}" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   487
  show "{x. x\<bullet>i < a} \<in> ?SIGMA" unfolding *
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   488
    using i by (safe intro!: sets.compl_sets) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   489
qed auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   490
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   491
lemma borel_eq_halfspace_greater:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   492
  "borel = sigma UNIV ((\<lambda> (a, i). {x\<Colon>'a\<Colon>euclidean_space. a < x \<bullet> i}) ` (UNIV \<times> Basis))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   493
  (is "_ = ?SIGMA")
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   494
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   495
  fix a :: real and i :: 'a assume "(a, i) \<in> (UNIV \<times> Basis)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   496
  then have i: "i \<in> Basis" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   497
  have *: "{x::'a. x\<bullet>i \<le> a} = space ?SIGMA - {x::'a. a < x\<bullet>i}" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   498
  show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA" unfolding *
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   499
    by (safe intro!: sets.compl_sets) (auto intro: i)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   500
qed auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   501
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   502
lemma borel_eq_atMost:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   503
  "borel = sigma UNIV (range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space}))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   504
  (is "_ = ?SIGMA")
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   505
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   506
  fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   507
  then have "i \<in> Basis" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   508
  then have *: "{x::'a. x\<bullet>i \<le> a} = (\<Union>k::nat. {.. (\<Sum>n\<in>Basis. (if n = i then a else real k)*\<^sub>R n)})"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   509
  proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   510
    fix x :: 'a
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   511
    from real_arch_simple[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"] guess k::nat ..
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   512
    then have "\<And>i. i \<in> Basis \<Longrightarrow> x\<bullet>i \<le> real k"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   513
      by (subst (asm) Max_le_iff) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   514
    then show "\<exists>k::nat. \<forall>ia\<in>Basis. ia \<noteq> i \<longrightarrow> x \<bullet> ia \<le> real k"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   515
      by (auto intro!: exI[of _ k])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   516
  qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   517
  show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA" unfolding *
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   518
    by (safe intro!: sets.countable_UN) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   519
qed auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   520
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   521
lemma borel_eq_greaterThan:
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   522
  "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {x. a <e x}))"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   523
  (is "_ = ?SIGMA")
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   524
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   525
  fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   526
  then have i: "i \<in> Basis" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   527
  have "{x::'a. x\<bullet>i \<le> a} = UNIV - {x::'a. a < x\<bullet>i}" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   528
  also have *: "{x::'a. a < x\<bullet>i} =
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   529
      (\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n) <e x})" using i
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   530
  proof (safe, simp_all add: eucl_less_def split: split_if_asm)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   531
    fix x :: 'a
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   532
    from reals_Archimedean2[of "Max ((\<lambda>i. -x\<bullet>i)`Basis)"]
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   533
    guess k::nat .. note k = this
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   534
    { fix i :: 'a assume "i \<in> Basis"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   535
      then have "-x\<bullet>i < real k"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   536
        using k by (subst (asm) Max_less_iff) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   537
      then have "- real k < x\<bullet>i" by simp }
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   538
    then show "\<exists>k::nat. \<forall>ia\<in>Basis. ia \<noteq> i \<longrightarrow> -real k < x \<bullet> ia"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   539
      by (auto intro!: exI[of _ k])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   540
  qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   541
  finally show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   542
    apply (simp only:)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   543
    apply (safe intro!: sets.countable_UN sets.Diff)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   544
    apply (auto intro: sigma_sets_top)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   545
    done
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   546
qed auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   547
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   548
lemma borel_eq_lessThan:
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   549
  "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {x. x <e a}))"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   550
  (is "_ = ?SIGMA")
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   551
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   552
  fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   553
  then have i: "i \<in> Basis" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   554
  have "{x::'a. a \<le> x\<bullet>i} = UNIV - {x::'a. x\<bullet>i < a}" by auto
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   555
  also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" using `i\<in> Basis`
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   556
  proof (safe, simp_all add: eucl_less_def split: split_if_asm)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   557
    fix x :: 'a
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   558
    from reals_Archimedean2[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"]
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   559
    guess k::nat .. note k = this
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   560
    { fix i :: 'a assume "i \<in> Basis"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   561
      then have "x\<bullet>i < real k"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   562
        using k by (subst (asm) Max_less_iff) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   563
      then have "x\<bullet>i < real k" by simp }
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   564
    then show "\<exists>k::nat. \<forall>ia\<in>Basis. ia \<noteq> i \<longrightarrow> x \<bullet> ia < real k"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   565
      by (auto intro!: exI[of _ k])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   566
  qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   567
  finally show "{x. a \<le> x\<bullet>i} \<in> ?SIGMA"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   568
    apply (simp only:)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   569
    apply (safe intro!: sets.countable_UN sets.Diff)
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   570
    apply (auto intro: sigma_sets_top )
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   571
    done
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   572
qed auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   573
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   574
lemma borel_eq_atLeastAtMost:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   575
  "borel = sigma UNIV (range (\<lambda>(a,b). {a..b} \<Colon>'a\<Colon>ordered_euclidean_space set))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   576
  (is "_ = ?SIGMA")
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   577
proof (rule borel_eq_sigmaI5[OF borel_eq_atMost])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   578
  fix a::'a
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   579
  have *: "{..a} = (\<Union>n::nat. {- real n *\<^sub>R One .. a})"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   580
  proof (safe, simp_all add: eucl_le[where 'a='a])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   581
    fix x :: 'a
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   582
    from real_arch_simple[of "Max ((\<lambda>i. - x\<bullet>i)`Basis)"]
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   583
    guess k::nat .. note k = this
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   584
    { fix i :: 'a assume "i \<in> Basis"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   585
      with k have "- x\<bullet>i \<le> real k"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   586
        by (subst (asm) Max_le_iff) (auto simp: field_simps)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   587
      then have "- real k \<le> x\<bullet>i" by simp }
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   588
    then show "\<exists>n::nat. \<forall>i\<in>Basis. - real n \<le> x \<bullet> i"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   589
      by (auto intro!: exI[of _ k])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   590
  qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   591
  show "{..a} \<in> ?SIGMA" unfolding *
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   592
    by (safe intro!: sets.countable_UN)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   593
       (auto intro!: sigma_sets_top)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   594
qed auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   595
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   596
lemma eucl_lessThan: "{x::real. x <e a} = lessThan a"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   597
  by (simp add: eucl_less_def lessThan_def)
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   598
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   599
lemma borel_eq_atLeastLessThan:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   600
  "borel = sigma UNIV (range (\<lambda>(a, b). {a ..< b :: real}))" (is "_ = ?SIGMA")
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   601
proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan])
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   602
  have move_uminus: "\<And>x y::real. -x \<le> y \<longleftrightarrow> -y \<le> x" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   603
  fix x :: real
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   604
  have "{..<x} = (\<Union>i::nat. {-real i ..< x})"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   605
    by (auto simp: move_uminus real_arch_simple)
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   606
  then show "{y. y <e x} \<in> ?SIGMA"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   607
    by (auto intro: sigma_sets.intros simp: eucl_lessThan)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   608
qed auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   609
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   610
lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   611
  unfolding borel_def
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   612
proof (intro sigma_eqI sigma_sets_eqI, safe)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   613
  fix x :: "'a set" assume "open x"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   614
  hence "x = UNIV - (UNIV - x)" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   615
  also have "\<dots> \<in> sigma_sets UNIV (Collect closed)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   616
    by (rule sigma_sets.Compl)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   617
       (auto intro!: sigma_sets.Basic simp: `open x`)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   618
  finally show "x \<in> sigma_sets UNIV (Collect closed)" by simp
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   619
next
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   620
  fix x :: "'a set" assume "closed x"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   621
  hence "x = UNIV - (UNIV - x)" by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   622
  also have "\<dots> \<in> sigma_sets UNIV (Collect open)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   623
    by (rule sigma_sets.Compl)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   624
       (auto intro!: sigma_sets.Basic simp: `closed x`)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   625
  finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   626
qed simp_all
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   627
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   628
lemma borel_measurable_halfspacesI:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   629
  fixes f :: "'a \<Rightarrow> 'c\<Colon>euclidean_space"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   630
  assumes F: "borel = sigma UNIV (F ` (UNIV \<times> Basis))"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   631
  and S_eq: "\<And>a i. S a i = f -` F (a,i) \<inter> space M" 
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   632
  shows "f \<in> borel_measurable M = (\<forall>i\<in>Basis. \<forall>a::real. S a i \<in> sets M)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   633
proof safe
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   634
  fix a :: real and i :: 'b assume i: "i \<in> Basis" and f: "f \<in> borel_measurable M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   635
  then show "S a i \<in> sets M" unfolding assms
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   636
    by (auto intro!: measurable_sets simp: assms(1))
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   637
next
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   638
  assume a: "\<forall>i\<in>Basis. \<forall>a. S a i \<in> sets M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   639
  then show "f \<in> borel_measurable M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   640
    by (auto intro!: measurable_measure_of simp: S_eq F)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   641
qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   642
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   643
lemma borel_measurable_iff_halfspace_le:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   644
  fixes f :: "'a \<Rightarrow> 'c\<Colon>euclidean_space"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   645
  shows "f \<in> borel_measurable M = (\<forall>i\<in>Basis. \<forall>a. {w \<in> space M. f w \<bullet> i \<le> a} \<in> sets M)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   646
  by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   647
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   648
lemma borel_measurable_iff_halfspace_less:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   649
  fixes f :: "'a \<Rightarrow> 'c\<Colon>euclidean_space"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   650
  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i\<in>Basis. \<forall>a. {w \<in> space M. f w \<bullet> i < a} \<in> sets M)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   651
  by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   652
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   653
lemma borel_measurable_iff_halfspace_ge:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   654
  fixes f :: "'a \<Rightarrow> 'c\<Colon>euclidean_space"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   655
  shows "f \<in> borel_measurable M = (\<forall>i\<in>Basis. \<forall>a. {w \<in> space M. a \<le> f w \<bullet> i} \<in> sets M)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   656
  by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   657
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   658
lemma borel_measurable_iff_halfspace_greater:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   659
  fixes f :: "'a \<Rightarrow> 'c\<Colon>euclidean_space"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   660
  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i\<in>Basis. \<forall>a. {w \<in> space M. a < f w \<bullet> i} \<in> sets M)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   661
  by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_greater]) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   662
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   663
lemma borel_measurable_iff_le:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   664
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   665
  using borel_measurable_iff_halfspace_le[where 'c=real] by simp
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   666
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   667
lemma borel_measurable_iff_less:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   668
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   669
  using borel_measurable_iff_halfspace_less[where 'c=real] by simp
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   670
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   671
lemma borel_measurable_iff_ge:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   672
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   673
  using borel_measurable_iff_halfspace_ge[where 'c=real]
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   674
  by simp
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   675
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   676
lemma borel_measurable_iff_greater:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   677
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   678
  using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   679
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   680
lemma borel_measurable_euclidean_space:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   681
  fixes f :: "'a \<Rightarrow> 'c::euclidean_space"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   682
  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i\<in>Basis. (\<lambda>x. f x \<bullet> i) \<in> borel_measurable M)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   683
proof safe
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   684
  assume f: "\<forall>i\<in>Basis. (\<lambda>x. f x \<bullet> i) \<in> borel_measurable M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   685
  then show "f \<in> borel_measurable M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   686
    by (subst borel_measurable_iff_halfspace_le) auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   687
qed auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   688
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   689
subsection "Borel measurable operators"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   690
56993
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
   691
lemma borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
   692
  by (intro borel_measurable_continuous_on1 continuous_intros)
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
   693
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   694
lemma borel_measurable_uminus[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   695
  fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   696
  assumes g: "g \<in> borel_measurable M"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   697
  shows "(\<lambda>x. - g x) \<in> borel_measurable M"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   698
  by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   699
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   700
lemma borel_measurable_add[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   701
  fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   702
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   703
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   704
  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   705
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   706
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   707
lemma borel_measurable_setsum[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   708
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   709
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   710
  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   711
proof cases
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   712
  assume "finite S"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   713
  thus ?thesis using assms by induct auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   714
qed simp
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   715
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   716
lemma borel_measurable_diff[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   717
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   718
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   719
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   720
  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 53216
diff changeset
   721
  using borel_measurable_add [of f M "- g"] assms by (simp add: fun_Compl_def)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   722
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   723
lemma borel_measurable_times[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   724
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_algebra}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   725
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   726
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   727
  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   728
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   729
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   730
lemma borel_measurable_setprod[measurable (raw)]:
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   731
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_field}"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   732
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   733
  shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   734
proof cases
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   735
  assume "finite S"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   736
  thus ?thesis using assms by induct auto
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   737
qed simp
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   738
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   739
lemma borel_measurable_dist[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   740
  fixes g f :: "'a \<Rightarrow> 'b::{second_countable_topology, metric_space}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   741
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   742
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   743
  shows "(\<lambda>x. dist (f x) (g x)) \<in> borel_measurable M"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   744
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   745
  
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   746
lemma borel_measurable_scaleR[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   747
  fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   748
  assumes f: "f \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   749
  assumes g: "g \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   750
  shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   751
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   752
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   753
lemma affine_borel_measurable_vector:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   754
  fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   755
  assumes "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   756
  shows "(\<lambda>x. a + b *\<^sub>R f x) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   757
proof (rule borel_measurableI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   758
  fix S :: "'x set" assume "open S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   759
  show "(\<lambda>x. a + b *\<^sub>R f x) -` S \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   760
  proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   761
    assume "b \<noteq> 0"
44537
c10485a6a7af make HOL-Probability respect set/pred distinction
huffman
parents: 44282
diff changeset
   762
    with `open S` have "open ((\<lambda>x. (- a + x) /\<^sub>R b) ` S)" (is "open ?S")
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 53216
diff changeset
   763
      using open_affinity [of S "inverse b" "- a /\<^sub>R b"]
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 53216
diff changeset
   764
      by (auto simp: algebra_simps)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   765
    hence "?S \<in> sets borel" by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   766
    moreover
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   767
    from `b \<noteq> 0` have "(\<lambda>x. a + b *\<^sub>R f x) -` S = f -` ?S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   768
      apply auto by (rule_tac x="a + b *\<^sub>R f x" in image_eqI, simp_all)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   769
    ultimately show ?thesis using assms unfolding in_borel_measurable_borel
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   770
      by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   771
  qed simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   772
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   773
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   774
lemma borel_measurable_const_scaleR[measurable (raw)]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   775
  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. b *\<^sub>R f x ::'a::real_normed_vector) \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   776
  using affine_borel_measurable_vector[of f M 0 b] by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   777
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   778
lemma borel_measurable_const_add[measurable (raw)]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   779
  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. a + f x ::'a::real_normed_vector) \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   780
  using affine_borel_measurable_vector[of f M a 1] by simp
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   781
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   782
lemma borel_measurable_inverse[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   783
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_div_algebra}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   784
  assumes f: "f \<in> borel_measurable M"
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   785
  shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   786
proof -
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   787
  have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) \<in> borel_measurable borel"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   788
    by (intro borel_measurable_continuous_on_open' continuous_intros) auto
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   789
  also have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) = inverse"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   790
    by (intro ext) auto
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   791
  finally show ?thesis using f by simp
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   792
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   793
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   794
lemma borel_measurable_divide[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   795
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   796
    (\<lambda>x. f x / g x::'b::{second_countable_topology, real_normed_field}) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   797
  by (simp add: field_divide_inverse)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   798
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   799
lemma borel_measurable_max[measurable (raw)]:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51683
diff changeset
   800
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   801
  by (simp add: max_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   802
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   803
lemma borel_measurable_min[measurable (raw)]:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51683
diff changeset
   804
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   805
  by (simp add: min_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   806
57235
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   807
lemma borel_measurable_Min[measurable (raw)]:
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   808
  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Min ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   809
proof (induct I rule: finite_induct)
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   810
  case (insert i I) then show ?case
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   811
    by (cases "I = {}") auto
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   812
qed auto
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   813
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   814
lemma borel_measurable_Max[measurable (raw)]:
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   815
  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Max ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   816
proof (induct I rule: finite_induct)
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   817
  case (insert i I) then show ?case
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   818
    by (cases "I = {}") auto
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   819
qed auto
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   820
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   821
lemma borel_measurable_abs[measurable (raw)]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   822
  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   823
  unfolding abs_real_def by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   824
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   825
lemma borel_measurable_nth[measurable (raw)]:
41026
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   826
  "(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   827
  by (simp add: cart_eq_inner_axis)
41026
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   828
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   829
lemma convex_measurable:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   830
  fixes A :: "'a :: ordered_euclidean_space set"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   831
  assumes X: "X \<in> borel_measurable M" "X ` space M \<subseteq> A" "open A"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   832
  assumes q: "convex_on A q"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   833
  shows "(\<lambda>x. q (X x)) \<in> borel_measurable M"
42990
3706951a6421 composition of convex and measurable function is measurable
hoelzl
parents: 42950
diff changeset
   834
proof -
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   835
  have "(\<lambda>x. if X x \<in> A then q (X x) else 0) \<in> borel_measurable M" (is "?qX")
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   836
  proof (rule borel_measurable_continuous_on_open[OF _ _ X(1)])
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   837
    show "open A" by fact
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   838
    from this q show "continuous_on A q"
42990
3706951a6421 composition of convex and measurable function is measurable
hoelzl
parents: 42950
diff changeset
   839
      by (rule convex_on_continuous)
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   840
  qed
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   841
  also have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M"
42990
3706951a6421 composition of convex and measurable function is measurable
hoelzl
parents: 42950
diff changeset
   842
    using X by (intro measurable_cong) auto
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   843
  finally show ?thesis .
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   844
qed
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   845
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   846
lemma borel_measurable_ln[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   847
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   848
  shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   849
proof -
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   850
  { fix x :: real assume x: "x \<le> 0"
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   851
    { fix x::real assume "x \<le> 0" then have "\<And>u. exp u = x \<longleftrightarrow> False" by auto }
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   852
    from this[of x] x this[of 0] have "ln 0 = ln x"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   853
      by (auto simp: ln_def) }
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   854
  note ln_imp = this
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   855
  have "(\<lambda>x. if f x \<in> {0<..} then ln (f x) else ln 0) \<in> borel_measurable M"
57138
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   856
    by (rule borel_measurable_continuous_on_open[OF _ _ f])
7b3146180291 generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents: 57137
diff changeset
   857
       (auto intro!: continuous_intros)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   858
  also have "(\<lambda>x. if x \<in> {0<..} then ln x else ln 0) = ln"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   859
    by (simp add: fun_eq_iff not_less ln_imp)
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   860
  finally show ?thesis .
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   861
qed
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   862
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   863
lemma borel_measurable_log[measurable (raw)]:
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   864
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   865
  unfolding log_def by auto
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   866
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50387
diff changeset
   867
lemma borel_measurable_exp[measurable]: "exp \<in> borel_measurable borel"
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51351
diff changeset
   868
  by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50387
diff changeset
   869
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   870
lemma measurable_real_floor[measurable]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   871
  "(floor :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   872
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   873
  have "\<And>a x. \<lfloor>x\<rfloor> = a \<longleftrightarrow> (real a \<le> x \<and> x < real (a + 1))"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   874
    by (auto intro: floor_eq2)
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   875
  then show ?thesis
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   876
    by (auto simp: vimage_def measurable_count_space_eq2_countable)
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   877
qed
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   878
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   879
lemma measurable_real_natfloor[measurable]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   880
  "(natfloor :: real \<Rightarrow> nat) \<in> measurable borel (count_space UNIV)"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   881
  by (simp add: natfloor_def[abs_def])
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   882
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   883
lemma measurable_real_ceiling[measurable]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   884
  "(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   885
  unfolding ceiling_def[abs_def] by simp
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   886
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   887
lemma borel_measurable_real_floor: "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   888
  by simp
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   889
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   890
lemma borel_measurable_real_natfloor:
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   891
  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   892
  by simp
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   893
57235
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   894
lemma borel_measurable_root [measurable]: "(root n) \<in> borel_measurable borel"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   895
  by (intro borel_measurable_continuous_on1 continuous_intros)
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   896
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   897
lemma borel_measurable_sqrt [measurable]: "sqrt \<in> borel_measurable borel"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   898
  by (intro borel_measurable_continuous_on1 continuous_intros)
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   899
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   900
lemma borel_measurable_power [measurable (raw)]:
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   901
   fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   902
   assumes f: "f \<in> borel_measurable M"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   903
   shows "(\<lambda>x. (f x) ^ n) \<in> borel_measurable M"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   904
   by (intro borel_measurable_continuous_on [OF _ f] continuous_intros)
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   905
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   906
lemma borel_measurable_Re [measurable]: "Re \<in> borel_measurable borel"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   907
  by (intro borel_measurable_continuous_on1 continuous_intros)
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   908
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   909
lemma borel_measurable_Im [measurable]: "Im \<in> borel_measurable borel"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   910
  by (intro borel_measurable_continuous_on1 continuous_intros)
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   911
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   912
lemma borel_measurable_of_real [measurable]: "(of_real :: _ \<Rightarrow> (_::real_normed_algebra)) \<in> borel_measurable borel"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   913
  by (intro borel_measurable_continuous_on1 continuous_intros)
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   914
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   915
lemma borel_measurable_sin [measurable]: "sin \<in> borel_measurable borel"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   916
  by (intro borel_measurable_continuous_on1 continuous_intros)
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   917
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   918
lemma borel_measurable_cos [measurable]: "cos \<in> borel_measurable borel"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   919
  by (intro borel_measurable_continuous_on1 continuous_intros)
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   920
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   921
lemma borel_measurable_arctan [measurable]: "arctan \<in> borel_measurable borel"
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   922
  by (intro borel_measurable_continuous_on1 continuous_intros)
b0b9a10e4bf4 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57138
diff changeset
   923
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   924
subsection "Borel space on the extended reals"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   925
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   926
lemma borel_measurable_ereal[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   927
  assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   928
  using continuous_on_ereal f by (rule borel_measurable_continuous_on)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   929
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   930
lemma borel_measurable_real_of_ereal[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   931
  fixes f :: "'a \<Rightarrow> ereal" 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   932
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   933
  shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   934
proof -
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   935
  have "(\<lambda>x. if f x \<in> UNIV - { \<infinity>, - \<infinity> } then real (f x) else 0) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   936
    using continuous_on_real
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   937
    by (rule borel_measurable_continuous_on_open[OF _ _ f]) auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   938
  also have "(\<lambda>x. if f x \<in> UNIV - { \<infinity>, - \<infinity> } then real (f x) else 0) = (\<lambda>x. real (f x))"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   939
    by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   940
  finally show ?thesis .
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   941
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   942
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   943
lemma borel_measurable_ereal_cases:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   944
  fixes f :: "'a \<Rightarrow> ereal" 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   945
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   946
  assumes H: "(\<lambda>x. H (ereal (real (f x)))) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   947
  shows "(\<lambda>x. H (f x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   948
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   949
  let ?F = "\<lambda>x. if f x = \<infinity> then H \<infinity> else if f x = - \<infinity> then H (-\<infinity>) else H (ereal (real (f x)))"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   950
  { fix x have "H (f x) = ?F x" by (cases "f x") auto }
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   951
  with f H show ?thesis by simp
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   952
qed
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   953
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   954
lemma
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   955
  fixes f :: "'a \<Rightarrow> ereal" assumes f[measurable]: "f \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   956
  shows borel_measurable_ereal_abs[measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   957
    and borel_measurable_ereal_inverse[measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   958
    and borel_measurable_uminus_ereal[measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   959
  by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   960
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   961
lemma borel_measurable_uminus_eq_ereal[simp]:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   962
  "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r")
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   963
proof
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   964
  assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   965
qed auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   966
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   967
lemma set_Collect_ereal2:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   968
  fixes f g :: "'a \<Rightarrow> ereal" 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   969
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   970
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   971
  assumes H: "{x \<in> space M. H (ereal (real (f x))) (ereal (real (g x)))} \<in> sets M"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   972
    "{x \<in> space borel. H (-\<infinity>) (ereal x)} \<in> sets borel"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   973
    "{x \<in> space borel. H (\<infinity>) (ereal x)} \<in> sets borel"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   974
    "{x \<in> space borel. H (ereal x) (-\<infinity>)} \<in> sets borel"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   975
    "{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   976
  shows "{x \<in> space M. H (f x) (g x)} \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   977
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   978
  let ?G = "\<lambda>y x. if g x = \<infinity> then H y \<infinity> else if g x = -\<infinity> then H y (-\<infinity>) else H y (ereal (real (g x)))"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   979
  let ?F = "\<lambda>x. if f x = \<infinity> then ?G \<infinity> x else if f x = -\<infinity> then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   980
  { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   981
  note * = this
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   982
  from assms show ?thesis
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   983
    by (subst *) (simp del: space_borel split del: split_if)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   984
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   985
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   986
lemma borel_measurable_ereal_iff:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   987
  shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   988
proof
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   989
  assume "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   990
  from borel_measurable_real_of_ereal[OF this]
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   991
  show "f \<in> borel_measurable M" by auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   992
qed auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   993
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   994
lemma borel_measurable_ereal_iff_real:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   995
  fixes f :: "'a \<Rightarrow> ereal"
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   996
  shows "f \<in> borel_measurable M \<longleftrightarrow>
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   997
    ((\<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)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   998
proof safe
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   999
  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"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1000
  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
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1001
  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
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 45288
diff changeset
  1002
  let ?f = "\<lambda>x. if f x = \<infinity> then \<infinity> else if f x = -\<infinity> then -\<infinity> else ereal (real (f x))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1003
  have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1004
  also have "?f = f" by (auto simp: fun_eq_iff ereal_real)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1005
  finally show "f \<in> borel_measurable M" .
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1006
qed simp_all
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
  1007
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1008
lemma borel_measurable_eq_atMost_ereal:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
  1009
  fixes f :: "'a \<Rightarrow> ereal"
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
  1010
  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1011
proof (intro iffI allI)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1012
  assume pos[rule_format]: "\<forall>a. f -` {..a} \<inter> space M \<in> sets M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1013
  show "f \<in> borel_measurable M"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1014
    unfolding borel_measurable_ereal_iff_real borel_measurable_iff_le
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1015
  proof (intro conjI allI)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1016
    fix a :: real
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1017
    { fix x :: ereal assume *: "\<forall>i::nat. real i < x"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1018
      have "x = \<infinity>"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1019
      proof (rule ereal_top)
44666
8670a39d4420 remove more duplicate lemmas
huffman
parents: 44537
diff changeset
  1020
        fix B from reals_Archimedean2[of B] guess n ..
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1021
        then have "ereal B < real n" by auto
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1022
        with * show "B \<le> x" by (metis less_trans less_imp_le)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1023
      qed }
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1024
    then have "f -` {\<infinity>} \<inter> space M = space M - (\<Union>i::nat. f -` {.. real i} \<inter> space M)"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1025
      by (auto simp: not_le)
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1026
    then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1027
      by (auto simp del: UN_simps)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1028
    moreover
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
  1029
    have "{-\<infinity>::ereal} = {..-\<infinity>}" by auto
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1030
    then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1031
    moreover have "{x\<in>space M. f x \<le> ereal a} \<in> sets M"
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1032
      using pos[of "ereal a"] by (simp add: vimage_def Int_def conj_commute)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1033
    moreover have "{w \<in> space M. real (f w) \<le> a} =
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1034
      (if a < 0 then {w \<in> space M. f w \<le> ereal a} - f -` {-\<infinity>} \<inter> space M
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1035
      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")
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1036
      proof (intro set_eqI) fix x show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" by (cases "f x") auto qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1037
    ultimately show "{w \<in> space M. real (f w) \<le> a} \<in> sets M" by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1038
  qed
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1039
qed (simp add: measurable_sets)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1040
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1041
lemma borel_measurable_eq_atLeast_ereal:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1042
  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a..} \<inter> space M \<in> sets M)"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1043
proof
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1044
  assume pos: "\<forall>a. f -` {a..} \<inter> space M \<in> sets M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1045
  moreover have "\<And>a. (\<lambda>x. - f x) -` {..a} = f -` {-a ..}"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1046
    by (auto simp: ereal_uminus_le_reorder)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1047
  ultimately have "(\<lambda>x. - f x) \<in> borel_measurable M"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1048
    unfolding borel_measurable_eq_atMost_ereal by auto
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1049
  then show "f \<in> borel_measurable M" by simp
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1050
qed (simp add: measurable_sets)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1051
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1052
lemma greater_eq_le_measurable:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1053
  fixes f :: "'a \<Rightarrow> 'c::linorder"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1054
  shows "f -` {..< a} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {a ..} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1055
proof
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1056
  assume "f -` {a ..} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1057
  moreover have "f -` {..< a} \<inter> space M = space M - f -` {a ..} \<inter> space M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1058
  ultimately show "f -` {..< a} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1059
next
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1060
  assume "f -` {..< a} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1061
  moreover have "f -` {a ..} \<inter> space M = space M - f -` {..< a} \<inter> space M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1062
  ultimately show "f -` {a ..} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1063
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1064
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1065
lemma borel_measurable_ereal_iff_less:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1066
  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..< a} \<inter> space M \<in> sets M)"
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1067
  unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable ..
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1068
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1069
lemma less_eq_ge_measurable:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1070
  fixes f :: "'a \<Rightarrow> 'c::linorder"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1071
  shows "f -` {a <..} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {..a} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1072
proof
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1073
  assume "f -` {a <..} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1074
  moreover have "f -` {..a} \<inter> space M = space M - f -` {a <..} \<inter> space M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1075
  ultimately show "f -` {..a} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1076
next
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1077
  assume "f -` {..a} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1078
  moreover have "f -` {a <..} \<inter> space M = space M - f -` {..a} \<inter> space M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1079
  ultimately show "f -` {a <..} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1080
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1081
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1082
lemma borel_measurable_ereal_iff_ge:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1083
  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a <..} \<inter> space M \<in> sets M)"
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1084
  unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable ..
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1085
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1086
lemma borel_measurable_ereal2:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1087
  fixes f g :: "'a \<Rightarrow> ereal" 
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1088
  assumes f: "f \<in> borel_measurable M"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1089
  assumes g: "g \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1090
  assumes H: "(\<lambda>x. H (ereal (real (f x))) (ereal (real (g x)))) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1091
    "(\<lambda>x. H (-\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1092
    "(\<lambda>x. H (\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1093
    "(\<lambda>x. H (ereal (real (f x))) (-\<infinity>)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1094
    "(\<lambda>x. H (ereal (real (f x))) (\<infinity>)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1095
  shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1096
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1097
  let ?G = "\<lambda>y x. if g x = \<infinity> then H y \<infinity> else if g x = - \<infinity> then H y (-\<infinity>) else H y (ereal (real (g x)))"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1098
  let ?F = "\<lambda>x. if f x = \<infinity> then ?G \<infinity> x else if f x = - \<infinity> then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1099
  { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1100
  note * = this
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1101
  from assms show ?thesis unfolding * by simp
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1102
qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1103
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1104
lemma
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1105
  fixes f :: "'a \<Rightarrow> ereal" assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1106
  shows borel_measurable_ereal_eq_const: "{x\<in>space M. f x = c} \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1107
    and borel_measurable_ereal_neq_const: "{x\<in>space M. f x \<noteq> c} \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1108
  using f by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1109
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1110
lemma [measurable(raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1111
  fixes f :: "'a \<Rightarrow> ereal"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1112
  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1113
  shows borel_measurable_ereal_add: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1114
    and borel_measurable_ereal_times: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1115
    and borel_measurable_ereal_min: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1116
    and borel_measurable_ereal_max: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1117
  by (simp_all add: borel_measurable_ereal2 min_def max_def)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1118
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1119
lemma [measurable(raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1120
  fixes f g :: "'a \<Rightarrow> ereal"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1121
  assumes "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1122
  assumes "g \<in> borel_measurable M"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1123
  shows borel_measurable_ereal_diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1124
    and borel_measurable_ereal_divide: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1125
  using assms by (simp_all add: minus_ereal_def divide_ereal_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1126
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1127
lemma borel_measurable_ereal_setsum[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1128
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
41096
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1129
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1130
  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1131
proof cases
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1132
  assume "finite S"
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1133
  thus ?thesis using assms
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1134
    by induct auto
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1135
qed simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1136
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1137
lemma borel_measurable_ereal_setprod[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1138
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1139
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
41096
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1140
  shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1141
proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1142
  assume "finite S"
41096
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1143
  thus ?thesis using assms by induct auto
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1144
qed simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1145
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1146
lemma borel_measurable_SUP[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1147
  fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1148
  assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
41097
a1abfa4e2b44 use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents: 41096
diff changeset
  1149
  shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1150
  unfolding borel_measurable_ereal_iff_ge
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1151
proof
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1152
  fix a
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1153
  have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
46884
154dc6ec0041 tuned proofs
noschinl
parents: 46731
diff changeset
  1154
    by (auto simp: less_SUP_iff)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1155
  then show "?sup -` {a<..} \<inter> space M \<in> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1156
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1157
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1158
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1159
lemma borel_measurable_INF[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1160
  fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1161
  assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
41097
a1abfa4e2b44 use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents: 41096
diff changeset
  1162
  shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1163
  unfolding borel_measurable_ereal_iff_less
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1164
proof
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1165
  fix a
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1166
  have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
46884
154dc6ec0041 tuned proofs
noschinl
parents: 46731
diff changeset
  1167
    by (auto simp: INF_less_iff)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1168
  then show "?inf -` {..<a} \<inter> space M \<in> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1169
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1170
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1171
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1172
lemma [measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1173
  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1174
  assumes "\<And>i. f i \<in> borel_measurable M"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1175
  shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1176
    and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: