src/HOL/Probability/Borel_Space.thy
author hoelzl
Mon, 14 Jan 2013 17:29:04 +0100
changeset 50881 ae630bab13da
parent 50526 899c9c4e4a4c
child 50882 a382bf90867e
permissions -rw-r--r--
renamed countable_basis_space to second_countable_topology
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
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    14
section "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
50387
3d8863c41fe8 Move the measurability prover to its own file
hoelzl
parents: 50245
diff changeset
    38
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
    39
  unfolding borel_def pred_def by auto
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    40
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    41
lemma borel_open[measurable (raw generic)]:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    42
  assumes "open A" shows "A \<in> sets borel"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    43
proof -
44537
c10485a6a7af make HOL-Probability respect set/pred distinction
huffman
parents: 44282
diff changeset
    44
  have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    45
  thus ?thesis unfolding borel_def by auto
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    46
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    47
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    48
lemma borel_closed[measurable (raw generic)]:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    49
  assumes "closed A" shows "A \<in> sets borel"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    50
proof -
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    51
  have "space borel - (- A) \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    52
    using assms unfolding closed_def by (blast intro: borel_open)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    53
  thus ?thesis by simp
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    54
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    55
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    56
lemma borel_singleton[measurable]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    57
  "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
    58
  unfolding insert_def by (rule sets.Un) auto
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    59
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    60
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
    61
  unfolding Compl_eq_Diff_UNIV by simp
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
    62
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    63
lemma borel_measurable_vimage:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    64
  fixes f :: "'a \<Rightarrow> 'x::t2_space"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    65
  assumes borel[measurable]: "f \<in> borel_measurable M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    66
  shows "f -` {x} \<inter> space M \<in> sets M"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
    67
  by simp
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    68
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    69
lemma borel_measurableI:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    70
  fixes f :: "'a \<Rightarrow> 'x\<Colon>topological_space"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    71
  assumes "\<And>S. open S \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    72
  shows "f \<in> borel_measurable M"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    73
  unfolding borel_def
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    74
proof (rule measurable_measure_of, simp_all)
44537
c10485a6a7af make HOL-Probability respect set/pred distinction
huffman
parents: 44282
diff changeset
    75
  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
    76
    using assms[of S] by simp
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    77
qed
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    78
50021
d96a3f468203 add support for function application to measurability prover
hoelzl
parents: 50003
diff changeset
    79
lemma borel_measurable_const:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    80
  "(\<lambda>x. c) \<in> borel_measurable M"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    81
  by auto
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    82
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    83
lemma borel_measurable_indicator:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    84
  assumes A: "A \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    85
  shows "indicator A \<in> borel_measurable M"
46905
6b1c0a80a57a prefer abs_def over def_raw;
wenzelm
parents: 46884
diff changeset
    86
  unfolding indicator_def [abs_def] using A
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    87
  by (auto intro!: measurable_If_set)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    88
50096
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    89
lemma borel_measurable_count_space[measurable (raw)]:
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    90
  "f \<in> borel_measurable (count_space S)"
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    91
  unfolding measurable_def by auto
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    92
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    93
lemma borel_measurable_indicator'[measurable (raw)]:
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    94
  assumes [measurable]: "{x\<in>space M. f x \<in> A x} \<in> sets M"
7c9c5b1b6cd7 more measurability rules
hoelzl
parents: 50094
diff changeset
    95
  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
    96
  unfolding indicator_def[abs_def]
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49774
diff changeset
    97
  by (auto intro!: measurable_If)
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49774
diff changeset
    98
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    99
lemma borel_measurable_indicator_iff:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   100
  "(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
   101
    (is "?I \<in> borel_measurable M \<longleftrightarrow> _")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   102
proof
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   103
  assume "?I \<in> borel_measurable M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   104
  then have "?I -` {1} \<inter> space M \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   105
    unfolding measurable_def by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   106
  also have "?I -` {1} \<inter> space M = A \<inter> space M"
46905
6b1c0a80a57a prefer abs_def over def_raw;
wenzelm
parents: 46884
diff changeset
   107
    unfolding indicator_def [abs_def] by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   108
  finally show "A \<inter> space M \<in> sets M" .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   109
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   110
  assume "A \<inter> space M \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   111
  moreover have "?I \<in> borel_measurable M \<longleftrightarrow>
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   112
    (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
   113
    by (intro measurable_cong) (auto simp: indicator_def)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   114
  ultimately show "?I \<in> borel_measurable M" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   115
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   116
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   117
lemma borel_measurable_subalgebra:
41545
9c869baf1c66 tuned formalization of subalgebra
hoelzl
parents: 41097
diff changeset
   118
  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
   119
  shows "f \<in> borel_measurable M"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   120
  using assms unfolding measurable_def by auto
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   121
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   122
lemma borel_measurable_continuous_on1:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   123
  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   124
  assumes "continuous_on UNIV f"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   125
  shows "f \<in> borel_measurable borel"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   126
  apply(rule borel_measurableI)
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   127
  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   128
50245
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   129
lemma borel_eq_countable_basis:
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   130
  fixes B::"'a::topological_space set set"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   131
  assumes "countable B"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   132
  assumes "topological_basis B"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   133
  shows "borel = sigma UNIV B"
50087
635d73673b5e regularity of measures, therefore:
immler
parents: 50021
diff changeset
   134
  unfolding borel_def
635d73673b5e regularity of measures, therefore:
immler
parents: 50021
diff changeset
   135
proof (intro sigma_eqI sigma_sets_eqI, safe)
50245
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   136
  interpret countable_basis using assms by unfold_locales
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   137
  fix X::"'a set" assume "open X"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   138
  from open_countable_basisE[OF this] guess B' . note B' = this
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   139
  show "X \<in> sigma_sets UNIV B"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   140
  proof cases
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   141
    assume "B' \<noteq> {}"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   142
    thus "X \<in> sigma_sets UNIV B" using assms B'
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   143
      by (metis from_nat_into Union_image_eq countable_subset range_from_nat_into
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   144
        in_mono sigma_sets.Basic sigma_sets.Union)
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   145
  qed (simp add: sigma_sets.Empty B')
50087
635d73673b5e regularity of measures, therefore:
immler
parents: 50021
diff changeset
   146
next
50245
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   147
  fix b assume "b \<in> B"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   148
  hence "open b" by (rule topological_basis_open[OF assms(2)])
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   149
  thus "b \<in> sigma_sets UNIV (Collect open)" by auto
50087
635d73673b5e regularity of measures, therefore:
immler
parents: 50021
diff changeset
   150
qed simp_all
635d73673b5e regularity of measures, therefore:
immler
parents: 50021
diff changeset
   151
50245
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   152
lemma borel_eq_union_closed_basis:
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   153
  "borel = sigma UNIV union_closed_basis"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   154
  by (rule borel_eq_countable_basis[OF countable_union_closed_basis basis_union_closed_basis])
50094
84ddcf5364b4 allow arbitrary enumerations of basis in locale for generation of borel sets
immler
parents: 50087
diff changeset
   155
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
   156
lemma topological_basis_prod:
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   157
  assumes A: "topological_basis A" and B: "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
   158
  shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> 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
   159
  unfolding topological_basis_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
   160
proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[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
   161
  fix S :: "('a \<times> 'b) set" assume "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
   162
  then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = 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
   163
  proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> 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
   164
    fix x y assume "(x, y) \<in> 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
   165
    from open_prod_elim[OF `open S` 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
   166
    obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> 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
   167
      by (metis mem_Sigma_iff)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   168
    moreover from topological_basisE[OF A a] guess A0 .
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   169
    moreover from topological_basisE[OF B b] guess B0 .
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   170
    ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> 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
   171
      by (intro UN_I[of "(A0, B0)"]) 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
   172
  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
   173
qed (metis A B topological_basis_open open_Times)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   174
50881
ae630bab13da renamed countable_basis_space to second_countable_topology
hoelzl
parents: 50526
diff changeset
   175
instance prod :: (second_countable_topology, second_countable_topology) 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
   176
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
   177
  obtain A :: "'a set set" where "countable A" "topological_basis 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
   178
    using ex_countable_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
   179
  moreover
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   180
  obtain B :: "'b set set" where "countable B" "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
   181
    using ex_countable_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
   182
  ultimately show "\<exists>B::('a \<times> '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
   183
    by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   184
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   185
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
   186
lemma borel_measurable_Pair[measurable (raw)]:
50881
ae630bab13da renamed countable_basis_space to second_countable_topology
hoelzl
parents: 50526
diff changeset
   187
  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
   188
  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
   189
  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
   190
  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
   191
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
   192
  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
   193
  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
   194
  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
   195
  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
   196
    by (auto intro!: countable_basis topological_basis_prod is_basis)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   197
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
   198
  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
   199
  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
   200
    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
   201
    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
   202
    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
   203
      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
   204
    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
   205
      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
   206
    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
   207
      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
   208
    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
   209
  qed auto
39087
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   210
qed
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   211
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   212
lemma borel_measurable_continuous_on:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   213
  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   214
  assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   215
  shows "(\<lambda>x. f (g x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   216
  using measurable_comp[OF g borel_measurable_continuous_on1[OF f]] by (simp add: comp_def)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   217
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   218
lemma borel_measurable_continuous_on_open':
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   219
  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   220
  assumes cont: "continuous_on A f" "open A"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   221
  shows "(\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel" (is "?f \<in> _")
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   222
proof (rule borel_measurableI)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   223
  fix S :: "'b set" assume "open S"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   224
  then have "open {x\<in>A. f x \<in> S}"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   225
    by (intro continuous_open_preimage[OF cont]) auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   226
  then have *: "{x\<in>A. f x \<in> S} \<in> sets borel" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   227
  have "?f -` S \<inter> space borel = 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   228
    {x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel - A else {})"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   229
    by (auto split: split_if_asm)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   230
  also have "\<dots> \<in> sets borel"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   231
    using * `open A` by auto
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   232
  finally show "?f -` S \<inter> space borel \<in> sets borel" .
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   233
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   234
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   235
lemma borel_measurable_continuous_on_open:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   236
  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   237
  assumes cont: "continuous_on A f" "open A"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   238
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   239
  shows "(\<lambda>x. if g x \<in> A then f (g x) else c) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   240
  using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   241
  by (simp add: comp_def)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   242
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   243
lemma continuous_on_fst: "continuous_on UNIV fst"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   244
proof -
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   245
  have [simp]: "range fst = UNIV" by (auto simp: image_iff)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   246
  show ?thesis
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   247
    using closed_vimage_fst
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   248
    by (auto simp: continuous_on_closed closed_closedin vimage_def)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   249
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   250
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   251
lemma continuous_on_snd: "continuous_on UNIV snd"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   252
proof -
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   253
  have [simp]: "range snd = UNIV" by (auto simp: image_iff)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   254
  show ?thesis
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   255
    using closed_vimage_snd
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   256
    by (auto simp: continuous_on_closed closed_closedin vimage_def)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   257
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   258
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   259
lemma borel_measurable_continuous_Pair:
50881
ae630bab13da renamed countable_basis_space to second_countable_topology
hoelzl
parents: 50526
diff changeset
   260
  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
   261
  assumes [measurable]: "f \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   262
  assumes [measurable]: "g \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   263
  assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   264
  shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   265
proof -
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   266
  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
   267
  show ?thesis
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   268
    unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   269
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   270
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
   271
section "Borel spaces on euclidean spaces"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   272
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   273
lemma borel_measurable_inner[measurable (raw)]:
50881
ae630bab13da renamed countable_basis_space to second_countable_topology
hoelzl
parents: 50526
diff changeset
   274
  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
   275
  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
   276
  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
   277
  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
   278
  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
   279
  by (rule borel_measurable_continuous_Pair)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   280
     (intro continuous_on_inner continuous_on_snd continuous_on_fst)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   281
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   282
lemma [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
   283
  fixes a b :: "'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
   284
  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
   285
    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
   286
    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
   287
    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
   288
    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
   289
    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
   290
    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
   291
    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
   292
  unfolding greaterThanAtMost_def atLeastLessThan_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
   293
  by (blast intro: borel_open borel_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
   294
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   295
lemma borel_measurable_less[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
   296
  fixes f :: "'a \<Rightarrow> 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
   297
  assumes 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
   298
  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
   299
  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
   300
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
   301
  have "{w \<in> space M. f w < g w} = {x \<in> space M. \<exists>r. f x < of_rat r \<and> of_rat r < g 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
   302
    using Rats_dense_in_real by (auto simp add: Rats_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
   303
  with f g show ?thesis
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   304
    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
   305
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
   306
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   307
lemma
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   308
  fixes f :: "'a \<Rightarrow> 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
   309
  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
   310
  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
   311
  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
   312
    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
   313
    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
   314
  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
   315
  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
   316
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
lemma 
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
  shows hafspace_less_borel: "{x::'a::euclidean_space. a < x \<bullet> 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
   319
    and hafspace_greater_borel: "{x::'a::euclidean_space. x \<bullet> i < 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
   320
    and hafspace_less_eq_borel: "{x::'a::euclidean_space. a \<le> x \<bullet> 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
   321
    and hafspace_greater_eq_borel: "{x::'a::euclidean_space. x \<bullet> i \<le> 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
   322
  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
   323
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   324
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
   325
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
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
   327
  "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
   328
  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
   329
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
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
   331
  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
   332
  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
   333
  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
   334
  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
   335
  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
   336
  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
   337
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
   338
  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
   339
    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
   340
  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
   341
    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
   342
  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
   343
    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
   344
  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
   345
  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
   346
    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
   347
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
   348
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
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
   350
  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
   351
    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
   352
  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
   353
  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
   354
  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
   355
  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
   356
  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
   357
  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
   358
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
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
   360
  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
   361
  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
   362
  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
   363
  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
   364
  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
   365
  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
   366
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
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
   368
  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
   369
    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
   370
  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
   371
  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
   372
  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
   373
  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
   374
  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
   375
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
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
   377
  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
   378
  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
   379
  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
   380
  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
   381
  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
   382
  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
   383
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
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
   385
  "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
   386
    (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
   387
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
   388
  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
   389
  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
   390
  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
   391
    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
   392
    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
   393
    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
   394
    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
   395
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
   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_greaterThanLessThan:
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
  "borel = sigma UNIV (range (\<lambda> (a, b). {a <..< b} :: '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
   399
  unfolding borel_eq_box apply (rule arg_cong2[where f=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
   400
  by (auto simp: box_def image_iff mem_interval set_eq_iff simp del: greaterThanLessThan_iff)
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
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
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
   403
  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
   404
  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
   405
    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
   406
  (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
   407
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
   408
  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
   409
    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
   410
  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
   411
  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
   412
    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
   413
    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
   414
    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
   415
      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
   416
    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
   417
      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
   418
  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
   419
    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
   420
    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
   421
    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
   422
    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
   423
  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
   424
  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
   425
    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
   426
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
   427
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
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
   429
  "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
   430
  (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
   431
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
   432
  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
   433
  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
   434
    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
   435
  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
   436
    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
   437
       (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
   438
  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
   439
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
   440
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
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
   442
  "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
   443
  (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
   444
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
   445
  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
   446
  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
   447
  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
   448
  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
   449
    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
   450
    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
   451
    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
   452
      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
   453
    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
   454
      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
   455
  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
   456
    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
   457
    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
   458
    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
   459
    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
   460
  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
   461
  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
   462
    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
   463
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
   464
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
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
   466
  "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
   467
  (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
   468
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
   469
  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
   470
  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
   471
  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
   472
    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
   473
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
   474
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
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
   476
  "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
   477
  (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
   478
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
   479
  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
   480
  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
   481
  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
   482
  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
   483
    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
   484
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
   485
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
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
   487
  "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
   488
  (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
   489
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
   490
  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
   491
  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
   492
  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
   493
  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
   494
    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
   495
    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
   496
    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
   497
      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
   498
    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
   499
      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
   500
  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
   501
  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
   502
    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
   503
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
   504
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
lemma borel_eq_greaterThan:
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
  "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {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
   507
  (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
   508
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
   509
  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
   510
  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
   511
  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
   512
  also have *: "{x::'a. 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
   513
      (\<Union>k::nat. {\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n <..})" using 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
   514
  proof (safe, simp_all add: eucl_less[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
   515
    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
   516
    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
   517
    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
   518
    { 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
   519
      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
   520
        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
   521
      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
   522
    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
   523
      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
   524
  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
   525
  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
   526
    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
   527
    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
   528
    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
   529
    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
   530
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
   531
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
lemma 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
   533
  "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {..<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
   534
  (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
   535
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
   536
  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
   537
  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
   538
  have "{x::'a. a \<le> x\<bullet>i} = UNIV - {x::'a. x\<bullet>i < 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
   539
  also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {..< \<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n})" using `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
   540
  proof (safe, simp_all add: eucl_less[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
   541
    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
   542
    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
   543
    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
   544
    { 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
   545
      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
   546
        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
   547
      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
   548
    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
   549
      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
   550
  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
   551
  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
   552
    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
   553
    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
   554
    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
   555
    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
   556
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
   557
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
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
   559
  "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
   560
  (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
   561
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
   562
  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
   563
  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
   564
  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
   565
    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
   566
    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
   567
    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
   568
    { 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
   569
      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
   570
        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
   571
      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
   572
    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
   573
      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
   574
  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
   575
  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
   576
    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
   577
       (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
   578
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
   579
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
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
   581
  "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
   582
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
   583
  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
   584
  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
   585
  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
   586
    by (auto simp: move_uminus real_arch_simple)
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 show "{..< x} \<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
   588
    by (auto intro: sigma_sets.intros)
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
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
   590
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
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
   592
  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
   593
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
   594
  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
   595
  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
   596
  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
   597
    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
   598
       (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
   599
  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
   600
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
   601
  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
   602
  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
   603
  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
   604
    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
   605
       (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
   606
  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
   607
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
   608
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
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
   610
  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
   611
  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
   612
  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
   613
  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
   614
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
   615
  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
   616
  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
   617
    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
   618
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
   619
  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
   620
  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
   621
    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
   622
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
   623
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
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
   625
  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
   626
  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
   627
  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
   628
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
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
   630
  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
   631
  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
   632
  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
   633
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
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
   635
  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
   636
  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
   637
  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
   638
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
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
   640
  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
   641
  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
   642
  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
   643
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
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
   645
  "(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
   646
  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
   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_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
  "(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
   650
  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
   651
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
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
   653
  "(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
   654
  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
   655
  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
   656
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
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
   658
  "(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
   659
  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
   660
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
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
   662
  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
   663
  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
   664
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
   665
  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
   666
  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
   667
    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
   668
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
   669
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
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
   671
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
lemma borel_measurable_uminus[measurable (raw)]:
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
  fixes g :: "'a \<Rightarrow> 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
  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
   675
  shows "(\<lambda>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
   676
  by (rule borel_measurable_continuous_on[OF _ g]) (auto intro: continuous_on_minus continuous_on_id)
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
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   678
lemma borel_measurable_add[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   679
  fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   680
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   681
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   682
  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   683
  using f g
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   684
  by (rule borel_measurable_continuous_Pair)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   685
     (auto intro: continuous_on_fst continuous_on_snd continuous_on_add)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   686
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   687
lemma borel_measurable_setsum[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   688
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   689
  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
   690
  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
   691
proof cases
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   692
  assume "finite S"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   693
  thus ?thesis using assms by induct auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   694
qed simp
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   695
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   696
lemma borel_measurable_diff[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   697
  fixes f :: "'a \<Rightarrow> real"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   698
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   699
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   700
  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   701
  unfolding diff_minus using assms by simp
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   702
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   703
lemma borel_measurable_times[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   704
  fixes f :: "'a \<Rightarrow> real"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   705
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   706
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   707
  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   708
  using f g
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   709
  by (rule borel_measurable_continuous_Pair)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   710
     (auto intro: continuous_on_fst continuous_on_snd continuous_on_mult)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   711
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   712
lemma continuous_on_dist:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   713
  fixes f :: "'a :: t2_space \<Rightarrow> 'b :: metric_space"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   714
  shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. dist (f x) (g x))"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   715
  unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   716
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   717
lemma borel_measurable_dist[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   718
  fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   719
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   720
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   721
  shows "(\<lambda>x. dist (f x) (g x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   722
  using f g
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   723
  by (rule borel_measurable_continuous_Pair)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   724
     (intro continuous_on_dist continuous_on_fst continuous_on_snd)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   725
  
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   726
lemma borel_measurable_scaleR[measurable (raw)]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   727
  fixes g :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   728
  assumes f: "f \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   729
  assumes g: "g \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   730
  shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   731
  by (rule borel_measurable_continuous_Pair[OF f g])
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   732
     (auto intro!: continuous_on_scaleR continuous_on_fst continuous_on_snd)
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   733
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   734
lemma affine_borel_measurable_vector:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   735
  fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   736
  assumes "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   737
  shows "(\<lambda>x. a + b *\<^sub>R f x) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   738
proof (rule borel_measurableI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   739
  fix S :: "'x set" assume "open S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   740
  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
   741
  proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   742
    assume "b \<noteq> 0"
44537
c10485a6a7af make HOL-Probability respect set/pred distinction
huffman
parents: 44282
diff changeset
   743
    with `open S` have "open ((\<lambda>x. (- a + x) /\<^sub>R b) ` S)" (is "open ?S")
c10485a6a7af make HOL-Probability respect set/pred distinction
huffman
parents: 44282
diff changeset
   744
      by (auto intro!: open_affinity simp: scaleR_add_right)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   745
    hence "?S \<in> sets borel" by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   746
    moreover
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   747
    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
   748
      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
   749
    ultimately show ?thesis using assms unfolding in_borel_measurable_borel
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   750
      by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   751
  qed simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   752
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   753
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   754
lemma borel_measurable_const_scaleR[measurable (raw)]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   755
  "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
   756
  using affine_borel_measurable_vector[of f M 0 b] by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   757
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   758
lemma borel_measurable_const_add[measurable (raw)]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   759
  "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
   760
  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
   761
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   762
lemma borel_measurable_setprod[measurable (raw)]:
41026
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   763
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   764
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   765
  shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   766
proof cases
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   767
  assume "finite S"
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   768
  thus ?thesis using assms by induct auto
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   769
qed simp
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   770
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   771
lemma borel_measurable_inverse[measurable (raw)]:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   772
  fixes f :: "'a \<Rightarrow> real"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   773
  assumes f: "f \<in> borel_measurable M"
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   774
  shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   775
proof -
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   776
  have "(\<lambda>x::real. if x \<in> UNIV - {0} then inverse x else 0) \<in> borel_measurable borel"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   777
    by (intro borel_measurable_continuous_on_open' continuous_on_inverse continuous_on_id) auto
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   778
  also have "(\<lambda>x::real. if x \<in> UNIV - {0} then inverse x else 0) = inverse" by (intro ext) auto
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   779
  finally show ?thesis using f by simp
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   780
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   781
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   782
lemma borel_measurable_divide[measurable (raw)]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   783
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. f x / g x::real) \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   784
  by (simp add: field_divide_inverse)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   785
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   786
lemma borel_measurable_max[measurable (raw)]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   787
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: real) \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   788
  by (simp add: max_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   789
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   790
lemma borel_measurable_min[measurable (raw)]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   791
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: real) \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   792
  by (simp add: min_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   793
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   794
lemma borel_measurable_abs[measurable (raw)]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   795
  "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
   796
  unfolding abs_real_def by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   797
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   798
lemma borel_measurable_nth[measurable (raw)]:
41026
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   799
  "(\<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
   800
  by (simp add: cart_eq_inner_axis)
41026
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   801
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   802
lemma convex_measurable:
42990
3706951a6421 composition of convex and measurable function is measurable
hoelzl
parents: 42950
diff changeset
   803
  fixes a b :: real
3706951a6421 composition of convex and measurable function is measurable
hoelzl
parents: 42950
diff changeset
   804
  assumes X: "X \<in> borel_measurable M" "X ` space M \<subseteq> { a <..< b}"
3706951a6421 composition of convex and measurable function is measurable
hoelzl
parents: 42950
diff changeset
   805
  assumes q: "convex_on { a <..< b} q"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   806
  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
   807
proof -
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   808
  have "(\<lambda>x. if X x \<in> {a <..< b} then q (X x) else 0) \<in> borel_measurable M" (is "?qX")
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   809
  proof (rule borel_measurable_continuous_on_open[OF _ _ X(1)])
42990
3706951a6421 composition of convex and measurable function is measurable
hoelzl
parents: 42950
diff changeset
   810
    show "open {a<..<b}" by auto
3706951a6421 composition of convex and measurable function is measurable
hoelzl
parents: 42950
diff changeset
   811
    from this q show "continuous_on {a<..<b} q"
3706951a6421 composition of convex and measurable function is measurable
hoelzl
parents: 42950
diff changeset
   812
      by (rule convex_on_continuous)
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   813
  qed
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   814
  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
   815
    using X by (intro measurable_cong) auto
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   816
  finally show ?thesis .
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   817
qed
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   818
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   819
lemma borel_measurable_ln[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   820
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   821
  shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   822
proof -
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   823
  { fix x :: real assume x: "x \<le> 0"
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   824
    { 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
   825
    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
   826
      by (auto simp: ln_def) }
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   827
  note ln_imp = this
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   828
  have "(\<lambda>x. if f x \<in> {0<..} then ln (f x) else ln 0) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   829
  proof (rule borel_measurable_continuous_on_open[OF _ _ f])
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   830
    show "continuous_on {0<..} ln"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   831
      by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   832
               simp: continuous_isCont[symmetric])
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   833
    show "open ({0<..}::real set)" by auto
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   834
  qed
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   835
  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
   836
    by (simp add: fun_eq_iff not_less ln_imp)
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   837
  finally show ?thesis .
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   838
qed
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   839
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   840
lemma borel_measurable_log[measurable (raw)]:
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   841
  "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
   842
  unfolding log_def by auto
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   843
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50387
diff changeset
   844
lemma borel_measurable_exp[measurable]: "exp \<in> borel_measurable borel"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50387
diff changeset
   845
  by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50387
diff changeset
   846
            continuous_isCont[THEN iffD1] isCont_exp)
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50387
diff changeset
   847
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   848
lemma measurable_count_space_eq2_countable:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   849
  fixes f :: "'a => 'c::countable"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   850
  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   851
proof -
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   852
  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   853
    then have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   854
      by auto
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   855
    moreover assume "\<And>a. a\<in>A \<Longrightarrow> f -` {a} \<inter> space M \<in> sets M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   856
    ultimately have "f -` X \<inter> space M \<in> sets M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   857
      using `X \<subseteq> A` by (simp add: subset_eq del: UN_simps) }
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   858
  then show ?thesis
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   859
    unfolding measurable_def by auto
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   860
qed
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   861
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   862
lemma measurable_real_floor[measurable]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   863
  "(floor :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   864
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   865
  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
   866
    by (auto intro: floor_eq2)
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   867
  then show ?thesis
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   868
    by (auto simp: vimage_def measurable_count_space_eq2_countable)
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   869
qed
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   870
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   871
lemma measurable_real_natfloor[measurable]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   872
  "(natfloor :: real \<Rightarrow> nat) \<in> measurable borel (count_space UNIV)"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   873
  by (simp add: natfloor_def[abs_def])
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   874
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   875
lemma measurable_real_ceiling[measurable]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   876
  "(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   877
  unfolding ceiling_def[abs_def] by simp
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   878
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   879
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
   880
  by simp
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   881
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   882
lemma borel_measurable_real_natfloor:
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   883
  "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
   884
  by simp
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   885
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   886
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
   887
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   888
lemma borel_measurable_ereal[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   889
  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
   890
  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
   891
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   892
lemma borel_measurable_real_of_ereal[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   893
  fixes f :: "'a \<Rightarrow> ereal" 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   894
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   895
  shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   896
proof -
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   897
  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
   898
    using continuous_on_real
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   899
    by (rule borel_measurable_continuous_on_open[OF _ _ f]) auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   900
  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
   901
    by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   902
  finally show ?thesis .
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   903
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   904
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   905
lemma borel_measurable_ereal_cases:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   906
  fixes f :: "'a \<Rightarrow> ereal" 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   907
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   908
  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
   909
  shows "(\<lambda>x. H (f x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   910
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   911
  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
   912
  { 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
   913
  with f H show ?thesis by simp
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   914
qed
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   915
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   916
lemma
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   917
  fixes f :: "'a \<Rightarrow> ereal" assumes f[measurable]: "f \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   918
  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
   919
    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
   920
    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
   921
  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
   922
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   923
lemma borel_measurable_uminus_eq_ereal[simp]:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   924
  "(\<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
   925
proof
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   926
  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
   927
qed auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   928
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   929
lemma set_Collect_ereal2:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   930
  fixes f g :: "'a \<Rightarrow> ereal" 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   931
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   932
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   933
  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
   934
    "{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
   935
    "{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
   936
    "{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
   937
    "{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   938
  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
   939
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   940
  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
   941
  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
   942
  { 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
   943
  note * = this
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   944
  from assms show ?thesis
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   945
    by (subst *) (simp del: space_borel split del: split_if)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   946
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   947
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   948
lemma [measurable]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   949
  fixes f g :: "'a \<Rightarrow> ereal"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   950
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   951
  assumes g: "g \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   952
  shows borel_measurable_ereal_le: "{x \<in> space M. f x \<le> g x} \<in> sets M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   953
    and borel_measurable_ereal_less: "{x \<in> space M. f x < g x} \<in> sets M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   954
    and borel_measurable_ereal_eq: "{w \<in> space M. f w = g w} \<in> sets M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   955
  using f g by (simp_all add: set_Collect_ereal2)
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   956
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   957
lemma borel_measurable_ereal_neq:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   958
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> {w \<in> space M. f w \<noteq> (g w :: ereal)} \<in> sets M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   959
  by simp
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   960
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   961
lemma borel_measurable_ereal_iff:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   962
  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
   963
proof
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   964
  assume "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   965
  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
   966
  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
   967
qed auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   968
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   969
lemma borel_measurable_ereal_iff_real:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   970
  fixes f :: "'a \<Rightarrow> ereal"
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   971
  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
   972
    ((\<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
   973
proof safe
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   974
  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
   975
  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
   976
  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
   977
  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
   978
  have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   979
  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
   980
  finally show "f \<in> borel_measurable M" .
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   981
qed simp_all
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   982
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   983
lemma borel_measurable_eq_atMost_ereal:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   984
  fixes f :: "'a \<Rightarrow> ereal"
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   985
  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
   986
proof (intro iffI allI)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   987
  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
   988
  show "f \<in> borel_measurable M"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   989
    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
   990
  proof (intro conjI allI)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   991
    fix a :: real
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   992
    { 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
   993
      have "x = \<infinity>"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   994
      proof (rule ereal_top)
44666
8670a39d4420 remove more duplicate lemmas
huffman
parents: 44537
diff changeset
   995
        fix B from reals_Archimedean2[of B] guess n ..
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   996
        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
   997
        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
   998
      qed }
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   999
    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
  1000
      by (auto simp: not_le)
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1001
    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
  1002
      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
  1003
    moreover
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
  1004
    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
  1005
    then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1006
    moreover have "{x\<in>space M. f x \<le> ereal a} \<in> sets M"
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1007
      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
  1008
    moreover have "{w \<in> space M. real (f w) \<le> a} =
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1009
      (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
  1010
      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
  1011
      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
  1012
    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
  1013
  qed
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1014
qed (simp add: measurable_sets)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1015
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1016
lemma borel_measurable_eq_atLeast_ereal:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1017
  "(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
  1018
proof
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1019
  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
  1020
  moreover have "\<And>a. (\<lambda>x. - f x) -` {..a} = f -` {-a ..}"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1021
    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
  1022
  ultimately have "(\<lambda>x. - f x) \<in> borel_measurable M"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1023
    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
  1024
  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
  1025
qed (simp add: measurable_sets)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1026
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1027
lemma greater_eq_le_measurable:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1028
  fixes f :: "'a \<Rightarrow> 'c::linorder"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1029
  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
  1030
proof
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1031
  assume "f -` {a ..} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1032
  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
  1033
  ultimately show "f -` {..< a} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1034
next
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1035
  assume "f -` {..< a} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1036
  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
  1037
  ultimately show "f -` {a ..} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1038
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1039
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1040
lemma borel_measurable_ereal_iff_less:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1041
  "(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
  1042
  unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable ..
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1043
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1044
lemma less_eq_ge_measurable:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1045
  fixes f :: "'a \<Rightarrow> 'c::linorder"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1046
  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
  1047
proof
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1048
  assume "f -` {a <..} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1049
  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
  1050
  ultimately show "f -` {..a} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1051
next
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1052
  assume "f -` {..a} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1053
  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
  1054
  ultimately show "f -` {a <..} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1055
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1056
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1057
lemma borel_measurable_ereal_iff_ge:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1058
  "(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
  1059
  unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable ..
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1060
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1061
lemma borel_measurable_ereal2:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1062
  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
  1063
  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
  1064
  assumes g: "g \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1065
  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
  1066
    "(\<lambda>x. H (-\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1067
    "(\<lambda>x. H (\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1068
    "(\<lambda>x. H (ereal (real (f x))) (-\<infinity>)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1069
    "(\<lambda>x. H (ereal (real (f x))) (\<infinity>)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1070
  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
  1071
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1072
  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
  1073
  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
  1074
  { 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
  1075
  note * = this
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1076
  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
  1077
qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1078
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1079
lemma
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1080
  fixes f :: "'a \<Rightarrow> ereal" assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1081
  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
  1082
    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
  1083
  using f by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1084
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1085
lemma [measurable(raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1086
  fixes f :: "'a \<Rightarrow> ereal"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1087
  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
  1088
  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
  1089
    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
  1090
    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
  1091
    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
  1092
  by (simp_all add: borel_measurable_ereal2 min_def max_def)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1093
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1094
lemma [measurable(raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1095
  fixes f g :: "'a \<Rightarrow> ereal"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1096
  assumes "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1097
  assumes "g \<in> borel_measurable M"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1098
  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
  1099
    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
  1100
  using assms by (simp_all add: minus_ereal_def divide_ereal_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1101
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1102
lemma borel_measurable_ereal_setsum[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1103
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
41096
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1104
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1105
  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1106
proof cases
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1107
  assume "finite S"
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1108
  thus ?thesis using assms
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1109
    by induct auto
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1110
qed simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1111
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1112
lemma borel_measurable_ereal_setprod[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1113
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1114
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
41096
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1115
  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
  1116
proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1117
  assume "finite S"
41096
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1118
  thus ?thesis using assms by induct auto
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1119
qed simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1120
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1121
lemma borel_measurable_SUP[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1122
  fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1123
  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
  1124
  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
  1125
  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
  1126
proof
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1127
  fix a
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1128
  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
  1129
    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
  1130
  then show "?sup -` {a<..} \<inter> space M \<in> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1131
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1132
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1133
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1134
lemma borel_measurable_INF[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1135
  fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1136
  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
  1137
  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
  1138
  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
  1139
proof
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1140
  fix a
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1141
  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
  1142
    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
  1143
  then show "?inf -` {..<a} \<inter> space M \<in> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1144
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1145
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1146
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1147
lemma [measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1148
  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
  1149
  assumes "\<And>i. f i \<in> borel_measurable M"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1150
  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
  1151
    and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1152
  unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1153
50104
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 50096
diff changeset
  1154
lemma sets_Collect_eventually_sequentially[measurable]:
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1155
  "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1156
  unfolding eventually_sequentially by simp
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1157
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1158
lemma sets_Collect_ereal_convergent[measurable]: 
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1159
  fixes f :: "nat \<Rightarrow> 'a => ereal"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1160
  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1161
  shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1162
  unfolding convergent_ereal by auto
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1163
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1164
lemma borel_measurable_extreal_lim[measurable (raw)]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1165
  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1166
  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1167
  shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1168
proof -
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1169
  have "\<And>x. lim (\<lambda>i. f i x) = (if convergent (\<lambda>i. f i x) then limsup (\<lambda>i. f i x) else (THE i. False))"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1170
    using convergent_ereal_limsup by (simp add: lim_def convergent_def)
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1171
  then show ?thesis
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1172
    by simp
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1173
qed
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1174
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1175
lemma borel_measurable_ereal_LIMSEQ:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1176
  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1177
  assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1178
  and u: "\<And>i. u i \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1179
  shows "u' \<in> borel_measurable M"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1180
proof -
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1181
  have "\<And>x. x \<in> space M \<Longrightarrow> u' x = liminf (\<lambda>n. u n x)"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1182
    using u' by (simp add: lim_imp_Liminf[symmetric])
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1183
  with u show ?thesis by (simp cong: measurable_cong)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1184
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1185
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1186
lemma borel_measurable_extreal_suminf[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1187
  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1188
  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1189
  shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1190
  unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1191
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1192
section "LIMSEQ is borel measurable"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1193
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1194
lemma borel_measurable_LIMSEQ: