src/HOL/Probability/Borel_Space.thy
author wenzelm
Thu, 18 Apr 2013 17:07:01 +0200
changeset 51717 9e7d1c139569
parent 51683 baefa3b461c2
child 53216 ad2e09c30aa8
permissions -rw-r--r--
simplifier uses proper Proof.context instead of historic type simpset;
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
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   139
  then show "X \<in> sigma_sets UNIV B"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   140
    by (blast intro: sigma_sets_UNION `countable B` countable_subset)
50087
635d73673b5e regularity of measures, therefore:
immler
parents: 50021
diff changeset
   141
next
50245
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   142
  fix b assume "b \<in> B"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   143
  hence "open b" by (rule topological_basis_open[OF assms(2)])
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50244
diff changeset
   144
  thus "b \<in> sigma_sets UNIV (Collect open)" by auto
50087
635d73673b5e regularity of measures, therefore:
immler
parents: 50021
diff changeset
   145
qed simp_all
635d73673b5e regularity of measures, therefore:
immler
parents: 50021
diff changeset
   146
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
   147
lemma borel_measurable_Pair[measurable (raw)]:
50881
ae630bab13da renamed countable_basis_space to second_countable_topology
hoelzl
parents: 50526
diff changeset
   148
  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
   149
  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
   150
  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
   151
  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
   152
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
   153
  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
   154
  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
   155
  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
   156
  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
   157
    by (auto intro!: countable_basis topological_basis_prod is_basis)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   158
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
   159
  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
   160
  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
   161
    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
   162
    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
   163
    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
   164
      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
   165
    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
   166
      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
   167
    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
   168
      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
   169
    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
   170
  qed auto
39087
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   171
qed
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   172
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   173
lemma borel_measurable_continuous_on:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   174
  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   175
  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
   176
  shows "(\<lambda>x. f (g x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   177
  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
   178
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   179
lemma borel_measurable_continuous_on_open':
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   180
  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   181
  assumes cont: "continuous_on A f" "open A"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   182
  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
   183
proof (rule borel_measurableI)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   184
  fix S :: "'b set" assume "open S"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   185
  then have "open {x\<in>A. f x \<in> S}"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   186
    by (intro continuous_open_preimage[OF cont]) auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   187
  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
   188
  have "?f -` S \<inter> space borel = 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   189
    {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
   190
    by (auto split: split_if_asm)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   191
  also have "\<dots> \<in> sets borel"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   192
    using * `open A` by auto
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   193
  finally show "?f -` S \<inter> space borel \<in> sets borel" .
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   194
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   195
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   196
lemma borel_measurable_continuous_on_open:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   197
  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   198
  assumes cont: "continuous_on A f" "open A"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   199
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   200
  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
   201
  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
   202
  by (simp add: comp_def)
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   203
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   204
lemma borel_measurable_continuous_Pair:
50881
ae630bab13da renamed countable_basis_space to second_countable_topology
hoelzl
parents: 50526
diff changeset
   205
  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
   206
  assumes [measurable]: "f \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   207
  assumes [measurable]: "g \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   208
  assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   209
  shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   210
proof -
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   211
  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
   212
  show ?thesis
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   213
    unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   214
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   215
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
   216
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
   217
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   218
lemma borel_measurable_inner[measurable (raw)]:
50881
ae630bab13da renamed countable_basis_space to second_countable_topology
hoelzl
parents: 50526
diff changeset
   219
  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
   220
  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
   221
  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
   222
  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
   223
  using assms
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   224
  by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   225
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   226
lemma [measurable]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   227
  fixes a b :: "'a\<Colon>linorder_topology"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   228
  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
   229
    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
   230
    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
   231
    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
   232
    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
   233
    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
   234
    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
   235
    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
   236
  unfolding greaterThanAtMost_def atLeastLessThan_def
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   237
  by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   238
                   closed_atMost closed_atLeast closed_atLeastAtMost)+
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   239
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   240
lemma eucl_ivals[measurable]:
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   241
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   242
  shows "{..< a} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   243
    and "{a <..} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   244
    and "{a<..<b} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   245
    and "{..a} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   246
    and "{a..} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   247
    and "{a..b} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   248
    and  "{a<..b} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   249
    and "{a..<b} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   250
  unfolding greaterThanAtMost_def atLeastLessThan_def
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
   251
  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
   252
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   253
lemma open_Collect_less:
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   254
  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   255
  assumes "continuous_on UNIV f"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   256
  assumes "continuous_on UNIV g"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   257
  shows "open {x. f x < g x}"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   258
proof -
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   259
  have "open (\<Union>y. {x \<in> UNIV. f x \<in> {..< y}} \<inter> {x \<in> UNIV. g x \<in> {y <..}})" (is "open ?X")
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   260
    by (intro open_UN ballI open_Int continuous_open_preimage assms) auto
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   261
  also have "?X = {x. f x < g x}"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   262
    by (auto intro: dense)
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   263
  finally show ?thesis .
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   264
qed
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   265
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   266
lemma closed_Collect_le:
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   267
  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   268
  assumes f: "continuous_on UNIV f"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   269
  assumes g: "continuous_on UNIV g"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   270
  shows "closed {x. f x \<le> g x}"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   271
  using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed .
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   272
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
   273
lemma borel_measurable_less[measurable]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   274
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   275
  assumes "f \<in> borel_measurable M"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   276
  assumes "g \<in> borel_measurable M"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   277
  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
   278
proof -
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   279
  have "{w \<in> space M. f w < g w} = (\<lambda>x. (f x, g x)) -` {x. fst x < snd x} \<inter> space M"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   280
    by auto
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   281
  also have "\<dots> \<in> sets M"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   282
    by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less]
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   283
              continuous_on_intros)
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   284
  finally show ?thesis .
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   285
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
   286
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
lemma
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   288
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   289
  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
   290
  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
   291
  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
   292
    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
   293
    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
   294
  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
   295
  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
   296
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
lemma 
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   298
  fixes i :: "'a::{second_countable_topology, real_inner}"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   299
  shows hafspace_less_borel: "{x. a < x \<bullet> i} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   300
    and hafspace_greater_borel: "{x. x \<bullet> i < a} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   301
    and hafspace_less_eq_borel: "{x. a \<le> x \<bullet> i} \<in> sets borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   302
    and hafspace_greater_eq_borel: "{x. x \<bullet> i \<le> a} \<in> sets borel"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   303
  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
   304
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
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
   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 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
   308
  "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
   309
  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
   310
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
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
   312
  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
   313
  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
   314
  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
   315
  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
   316
  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
   317
  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
   318
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
   319
  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
   320
    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
   321
  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
   322
    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
   323
  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
   324
    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
   325
  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
   326
  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
   327
    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
   328
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
   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_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
   331
  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
   332
    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
   333
  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
   334
  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
   335
  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
   336
  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
   337
  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
   338
  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
   339
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
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
   341
  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
   342
  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
   343
  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
   344
  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
   345
  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
   346
  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
   347
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
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
   349
  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
   350
    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
   351
  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
   352
  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
   353
  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
   354
  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
   355
  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
   356
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
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
   358
  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
   359
  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
   360
  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
   361
  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
   362
  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
   363
  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
   364
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
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
   366
  "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
   367
    (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
   368
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
   369
  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
   370
  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
   371
  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
   372
    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
   373
    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
   374
    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
   375
    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
   376
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
   377
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
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
   379
  "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
   380
  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
   381
  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
   382
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
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
   384
  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
   385
  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
   386
    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
   387
  (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
   388
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
   389
  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
   390
    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
   391
  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
   392
  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
   393
    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
   394
    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
   395
    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
   396
      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
   397
    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
   398
      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
   399
  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
   400
    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
   401
    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
   402
    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
   403
    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
   404
  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
   405
  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
   406
    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
   407
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
   408
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
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
   410
  "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
   411
  (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
   412
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
   413
  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
   414
  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
   415
    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
   416
  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
   417
    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
   418
       (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
   419
  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
   420
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
   421
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
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
   423
  "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
   424
  (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
   425
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
   426
  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
   427
  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
   428
  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
   429
  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
   430
    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
   431
    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
   432
    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
   433
      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
   434
    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
   435
      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
   436
  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
   437
    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
   438
    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
   439
    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
   440
    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
   441
  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
   442
  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
   443
    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
   444
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
   445
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
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
   447
  "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
   448
  (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
   449
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
   450
  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
   451
  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
   452
  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
   453
    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
   454
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
   455
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
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
   457
  "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
   458
  (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
   459
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
   460
  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
   461
  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
   462
  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
   463
  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
   464
    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
   465
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
   466
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
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
   468
  "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
   469
  (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
   470
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
   471
  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
   472
  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
   473
  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
   474
  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
   475
    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
   476
    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
   477
    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
   478
      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
   479
    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
   480
      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
   481
  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
   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.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
   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_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
   487
  "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
   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: "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
  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
   493
  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
   494
      (\<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
   495
  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
   496
    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
   497
    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
   498
    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
   499
    { 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
   500
      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
   501
        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
   502
      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
   503
    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
   504
      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
   505
  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
   506
  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
   507
    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
   508
    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
   509
    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
   510
    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
   511
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
   512
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
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
   514
  "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
   515
  (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
   516
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
   517
  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
   518
  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
   519
  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
   520
  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
   521
  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
   522
    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
   523
    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
   524
    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
   525
    { 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
   526
      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
   527
        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
   528
      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
   529
    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
   530
      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
   531
  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
   532
  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
   533
    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
   534
    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
   535
    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
   536
    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
   537
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
   538
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
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
   540
  "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
   541
  (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
   542
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
   543
  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
   544
  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
   545
  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
   546
    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
   547
    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
   548
    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
   549
    { 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
   550
      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
   551
        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
   552
      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
   553
    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
   554
      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
   555
  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
   556
  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
   557
    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
   558
       (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
   559
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
   560
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
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
   562
  "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
   563
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
   564
  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
   565
  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
   566
  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
   567
    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
   568
  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
   569
    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
   570
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
   571
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
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
   573
  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
   574
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
   575
  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
   576
  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
   577
  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
   578
    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
   579
       (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
   580
  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
   581
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
   582
  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
   583
  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
   584
  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
   585
    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
   586
       (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
   587
  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
   588
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
   589
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
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
   591
  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
   592
  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
   593
  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
   594
  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
   595
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
   596
  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
   597
  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
   598
    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
   599
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
   600
  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
   601
  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
   602
    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
   603
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
   604
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
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
   606
  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
   607
  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
   608
  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
   609
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   610
lemma borel_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
   611
  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
   612
  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
   613
  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
   614
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
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
   616
  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
   617
  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
   618
  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
   619
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
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
   621
  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
   622
  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
   623
  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
   624
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
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
   626
  "(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
   627
  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
   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_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
  "(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
   631
  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
   632
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
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
   634
  "(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
   635
  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
   636
  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
   637
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
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
   639
  "(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
   640
  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
   641
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
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
   643
  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
   644
  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
   645
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
   646
  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
   647
  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
   648
    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
   649
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
   650
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
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
   652
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   653
lemma borel_measurable_uminus[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   654
  fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   655
  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
   656
  shows "(\<lambda>x. - g x) \<in> borel_measurable M"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   657
  by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_on_intros)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   658
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   659
lemma borel_measurable_add[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   660
  fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   661
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   662
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   663
  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   664
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   665
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   666
lemma borel_measurable_setsum[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   667
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   668
  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
   669
  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
   670
proof cases
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   671
  assume "finite S"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   672
  thus ?thesis using assms by induct auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   673
qed simp
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   674
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   675
lemma borel_measurable_diff[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   676
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   677
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   678
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   679
  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   680
  unfolding diff_minus using assms by simp
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   681
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   682
lemma borel_measurable_times[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   683
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_algebra}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   684
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   685
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   686
  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   687
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   688
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   689
lemma borel_measurable_setprod[measurable (raw)]:
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   690
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_field}"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   691
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   692
  shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   693
proof cases
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   694
  assume "finite S"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   695
  thus ?thesis using assms by induct auto
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   696
qed simp
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   697
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   698
lemma borel_measurable_dist[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   699
  fixes g f :: "'a \<Rightarrow> 'b::{second_countable_topology, metric_space}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   700
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   701
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   702
  shows "(\<lambda>x. dist (f x) (g x)) \<in> borel_measurable M"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   703
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   704
  
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   705
lemma borel_measurable_scaleR[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   706
  fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   707
  assumes f: "f \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   708
  assumes g: "g \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   709
  shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   710
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   711
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   712
lemma affine_borel_measurable_vector:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   713
  fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   714
  assumes "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   715
  shows "(\<lambda>x. a + b *\<^sub>R f x) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   716
proof (rule borel_measurableI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   717
  fix S :: "'x set" assume "open S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   718
  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
   719
  proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   720
    assume "b \<noteq> 0"
44537
c10485a6a7af make HOL-Probability respect set/pred distinction
huffman
parents: 44282
diff changeset
   721
    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
   722
      by (auto intro!: open_affinity simp: scaleR_add_right)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   723
    hence "?S \<in> sets borel" by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   724
    moreover
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   725
    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
   726
      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
   727
    ultimately show ?thesis using assms unfolding in_borel_measurable_borel
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   728
      by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   729
  qed simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   730
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   731
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   732
lemma borel_measurable_const_scaleR[measurable (raw)]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   733
  "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
   734
  using affine_borel_measurable_vector[of f M 0 b] by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   735
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   736
lemma borel_measurable_const_add[measurable (raw)]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   737
  "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
   738
  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
   739
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   740
lemma borel_measurable_inverse[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   741
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_div_algebra}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   742
  assumes f: "f \<in> borel_measurable M"
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   743
  shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   744
proof -
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   745
  have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) \<in> borel_measurable borel"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   746
    by (intro borel_measurable_continuous_on_open' continuous_on_intros) auto
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   747
  also have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) = inverse"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   748
    by (intro ext) auto
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   749
  finally show ?thesis using f by simp
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   750
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   751
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   752
lemma borel_measurable_divide[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   753
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   754
    (\<lambda>x. f x / g x::'b::{second_countable_topology, real_normed_field}) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   755
  by (simp add: field_divide_inverse)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   756
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   757
lemma borel_measurable_max[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   758
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   759
  by (simp add: max_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   760
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   761
lemma borel_measurable_min[measurable (raw)]:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   762
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   763
  by (simp add: min_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   764
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   765
lemma borel_measurable_abs[measurable (raw)]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   766
  "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
   767
  unfolding abs_real_def by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   768
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   769
lemma borel_measurable_nth[measurable (raw)]:
41026
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   770
  "(\<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
   771
  by (simp add: cart_eq_inner_axis)
41026
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   772
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   773
lemma convex_measurable:
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   774
  fixes A :: "'a :: ordered_euclidean_space set"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   775
  assumes X: "X \<in> borel_measurable M" "X ` space M \<subseteq> A" "open A"
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   776
  assumes q: "convex_on A q"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   777
  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
   778
proof -
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   779
  have "(\<lambda>x. if X x \<in> A then q (X x) else 0) \<in> borel_measurable M" (is "?qX")
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   780
  proof (rule borel_measurable_continuous_on_open[OF _ _ X(1)])
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   781
    show "open A" by fact
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   782
    from this q show "continuous_on A q"
42990
3706951a6421 composition of convex and measurable function is measurable
hoelzl
parents: 42950
diff changeset
   783
      by (rule convex_on_continuous)
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   784
  qed
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   785
  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
   786
    using X by (intro measurable_cong) auto
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   787
  finally show ?thesis .
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   788
qed
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   789
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   790
lemma borel_measurable_ln[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   791
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   792
  shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   793
proof -
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   794
  { fix x :: real assume x: "x \<le> 0"
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   795
    { 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
   796
    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
   797
      by (auto simp: ln_def) }
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   798
  note ln_imp = this
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   799
  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
   800
  proof (rule borel_measurable_continuous_on_open[OF _ _ f])
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   801
    show "continuous_on {0<..} ln"
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51351
diff changeset
   802
      by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont)
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   803
    show "open ({0<..}::real set)" by auto
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   804
  qed
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   805
  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
   806
    by (simp add: fun_eq_iff not_less ln_imp)
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   807
  finally show ?thesis .
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   808
qed
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   809
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   810
lemma borel_measurable_log[measurable (raw)]:
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   811
  "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
   812
  unfolding log_def by auto
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   813
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50387
diff changeset
   814
lemma borel_measurable_exp[measurable]: "exp \<in> borel_measurable borel"
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51351
diff changeset
   815
  by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50387
diff changeset
   816
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   817
lemma measurable_count_space_eq2_countable:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   818
  fixes f :: "'a => 'c::countable"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   819
  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
   820
proof -
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   821
  { 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
   822
    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
   823
      by auto
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   824
    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
   825
    ultimately have "f -` X \<inter> space M \<in> sets M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   826
      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
   827
  then show ?thesis
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   828
    unfolding measurable_def by auto
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   829
qed
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   830
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   831
lemma measurable_real_floor[measurable]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   832
  "(floor :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   833
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   834
  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
   835
    by (auto intro: floor_eq2)
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   836
  then show ?thesis
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   837
    by (auto simp: vimage_def measurable_count_space_eq2_countable)
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   838
qed
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   839
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   840
lemma measurable_real_natfloor[measurable]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   841
  "(natfloor :: real \<Rightarrow> nat) \<in> measurable borel (count_space UNIV)"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   842
  by (simp add: natfloor_def[abs_def])
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   843
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   844
lemma measurable_real_ceiling[measurable]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   845
  "(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   846
  unfolding ceiling_def[abs_def] by simp
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   847
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   848
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
   849
  by simp
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   850
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   851
lemma borel_measurable_real_natfloor:
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   852
  "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
   853
  by simp
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   854
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   855
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
   856
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   857
lemma borel_measurable_ereal[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   858
  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
   859
  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
   860
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   861
lemma borel_measurable_real_of_ereal[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   862
  fixes f :: "'a \<Rightarrow> ereal" 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   863
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   864
  shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   865
proof -
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   866
  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
   867
    using continuous_on_real
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   868
    by (rule borel_measurable_continuous_on_open[OF _ _ f]) auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   869
  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
   870
    by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   871
  finally show ?thesis .
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   872
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   873
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   874
lemma borel_measurable_ereal_cases:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   875
  fixes f :: "'a \<Rightarrow> ereal" 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   876
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   877
  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
   878
  shows "(\<lambda>x. H (f x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   879
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   880
  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
   881
  { 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
   882
  with f H show ?thesis by simp
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   883
qed
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   884
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   885
lemma
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   886
  fixes f :: "'a \<Rightarrow> ereal" assumes f[measurable]: "f \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   887
  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
   888
    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
   889
    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
   890
  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
   891
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   892
lemma borel_measurable_uminus_eq_ereal[simp]:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   893
  "(\<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
   894
proof
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   895
  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
   896
qed auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   897
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   898
lemma set_Collect_ereal2:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   899
  fixes f g :: "'a \<Rightarrow> ereal" 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   900
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   901
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   902
  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
   903
    "{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
   904
    "{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
   905
    "{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
   906
    "{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   907
  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
   908
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   909
  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
   910
  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
   911
  { 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
   912
  note * = this
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   913
  from assms show ?thesis
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   914
    by (subst *) (simp del: space_borel split del: split_if)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   915
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   916
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   917
lemma borel_measurable_ereal_iff:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   918
  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
   919
proof
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   920
  assume "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   921
  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
   922
  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
   923
qed auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   924
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   925
lemma borel_measurable_ereal_iff_real:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   926
  fixes f :: "'a \<Rightarrow> ereal"
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   927
  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
   928
    ((\<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
   929
proof safe
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   930
  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
   931
  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
   932
  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
   933
  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
   934
  have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   935
  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
   936
  finally show "f \<in> borel_measurable M" .
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   937
qed simp_all
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   938
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   939
lemma borel_measurable_eq_atMost_ereal:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   940
  fixes f :: "'a \<Rightarrow> ereal"
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   941
  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
   942
proof (intro iffI allI)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   943
  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
   944
  show "f \<in> borel_measurable M"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   945
    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
   946
  proof (intro conjI allI)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   947
    fix a :: real
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   948
    { 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
   949
      have "x = \<infinity>"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   950
      proof (rule ereal_top)
44666
8670a39d4420 remove more duplicate lemmas
huffman
parents: 44537
diff changeset
   951
        fix B from reals_Archimedean2[of B] guess n ..
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   952
        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
   953
        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
   954
      qed }
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   955
    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
   956
      by (auto simp: not_le)
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   957
    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
   958
      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
   959
    moreover
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   960
    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
   961
    then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   962
    moreover have "{x\<in>space M. f x \<le> ereal a} \<in> sets M"
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   963
      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
   964
    moreover have "{w \<in> space M. real (f w) \<le> a} =
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   965
      (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
   966
      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
   967
      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
   968
    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
   969
  qed
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   970
qed (simp add: measurable_sets)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   971
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   972
lemma borel_measurable_eq_atLeast_ereal:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   973
  "(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
   974
proof
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   975
  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
   976
  moreover have "\<And>a. (\<lambda>x. - f x) -` {..a} = f -` {-a ..}"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   977
    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
   978
  ultimately have "(\<lambda>x. - f x) \<in> borel_measurable M"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   979
    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
   980
  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
   981
qed (simp add: measurable_sets)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   982
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   983
lemma greater_eq_le_measurable:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   984
  fixes f :: "'a \<Rightarrow> 'c::linorder"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   985
  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
   986
proof
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   987
  assume "f -` {a ..} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   988
  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
   989
  ultimately show "f -` {..< a} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   990
next
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   991
  assume "f -` {..< a} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   992
  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
   993
  ultimately show "f -` {a ..} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   994
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   995
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   996
lemma borel_measurable_ereal_iff_less:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   997
  "(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
   998
  unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable ..
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   999
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1000
lemma less_eq_ge_measurable:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1001
  fixes f :: "'a \<Rightarrow> 'c::linorder"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1002
  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
  1003
proof
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1004
  assume "f -` {a <..} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1005
  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
  1006
  ultimately show "f -` {..a} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1007
next
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1008
  assume "f -` {..a} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1009
  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
  1010
  ultimately show "f -` {a <..} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1011
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1012
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1013
lemma borel_measurable_ereal_iff_ge:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1014
  "(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
  1015
  unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable ..
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1016
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1017
lemma borel_measurable_ereal2:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1018
  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
  1019
  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
  1020
  assumes g: "g \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1021
  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
  1022
    "(\<lambda>x. H (-\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1023
    "(\<lambda>x. H (\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1024
    "(\<lambda>x. H (ereal (real (f x))) (-\<infinity>)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1025
    "(\<lambda>x. H (ereal (real (f x))) (\<infinity>)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1026
  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
  1027
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1028
  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
  1029
  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
  1030
  { 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
  1031
  note * = this
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1032
  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
  1033
qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1034
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1035
lemma
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1036
  fixes f :: "'a \<Rightarrow> ereal" assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1037
  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
  1038
    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
  1039
  using f by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1040
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1041
lemma [measurable(raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1042
  fixes f :: "'a \<Rightarrow> ereal"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1043
  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
  1044
  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
  1045
    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
  1046
    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
  1047
    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
  1048
  by (simp_all add: borel_measurable_ereal2 min_def max_def)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1049
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1050
lemma [measurable(raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1051
  fixes f g :: "'a \<Rightarrow> ereal"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1052
  assumes "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1053
  assumes "g \<in> borel_measurable M"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1054
  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
  1055
    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
  1056
  using assms by (simp_all add: minus_ereal_def divide_ereal_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1057
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1058
lemma borel_measurable_ereal_setsum[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1059
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
41096
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1060
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1061
  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1062
proof cases
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1063
  assume "finite S"
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1064
  thus ?thesis using assms
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1065
    by induct auto
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1066
qed simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1067
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1068
lemma borel_measurable_ereal_setprod[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1069
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1070
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
41096
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1071
  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
  1072
proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1073
  assume "finite S"
41096
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1074
  thus ?thesis using assms by induct auto
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1075
qed simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1076
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1077
lemma borel_measurable_SUP[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1078
  fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1079
  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
  1080
  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
  1081
  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
  1082
proof
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1083
  fix a
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1084
  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
  1085
    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
  1086
  then show "?sup -` {a<..} \<inter> space M \<in> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1087
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1088
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1089
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1090
lemma borel_measurable_INF[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1091
  fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1092
  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
  1093
  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
  1094
  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
  1095
proof
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1096
  fix a
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1097
  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
  1098
    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
  1099
  then show "?inf -` {..<a} \<inter> space M \<in> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1100
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1101
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1102
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1103
lemma [measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1104
  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
  1105
  assumes "\<And>i. f i \<in> borel_measurable M"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1106
  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
  1107
    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
  1108
  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
  1109
50104
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 50096
diff changeset
  1110
lemma sets_Collect_eventually_sequentially[measurable]:
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1111
  "(\<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
  1112
  unfolding eventually_sequentially by simp
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1113
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1114
lemma sets_Collect_ereal_convergent[measurable]: 
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1115
  fixes f :: "nat \<Rightarrow> 'a => ereal"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1116
  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1117
  shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1118
  unfolding convergent_ereal by auto
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1119
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1120
lemma borel_measurable_extreal_lim[measurable (raw)]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1121
  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1122
  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1123
  shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1124
proof -
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1125
  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))"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51106
diff changeset
  1126
    by (simp add: lim_def convergent_def convergent_limsup_cl)
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1127
  then show ?thesis
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1128
    by simp
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1129
qed
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1130
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1131
lemma borel_measurable_ereal_LIMSEQ:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1132
  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1133
  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
  1134
  and u: "\<And>i. u i \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1135
  shows "u' \<in> borel_measurable M"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1136
proof -
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1137
  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
  1138
    using u' by (simp add: lim_imp_Liminf[symmetric])
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1139
  with u show ?thesis by (simp cong: measurable_cong)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1140
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1141
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1142
lemma borel_measurable_extreal_suminf[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1143
  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1144
  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
  1145
  shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1146
  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
  1147
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1148
section "LIMSEQ is borel measurable"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1149
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1150
lemma borel_measurable_LIMSEQ:
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1151
  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1152
  assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1153
  and u: "\<And>i. u i \<in> borel_measurable M"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1154
  shows "u' \<in> borel_measurable M"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1155
proof -
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1156
  have "\<And>x. x \<in> space M \<Longrightarrow> liminf (\<lambda>n. ereal (u n x)) = ereal (u' x)"
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 45288
diff changeset
  1157
    using u' by (simp add: lim_imp_Liminf)
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1158
  moreover from u have "(\<lambda>x. liminf (\<lambda>n. ereal (u n x))) \<in> borel_measurable M"
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1159
    by auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1160
  ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff)
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1161
qed
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1162
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1163
lemma sets_Collect_Cauchy[measurable]: 
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1164
  fixes f :: "nat \<Rightarrow> 'a => real"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1165
  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1166
  shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1167
  unfolding Cauchy_iff2 using f by auto
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1168
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1169
lemma borel_measurable_lim[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1170
  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1171
  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1172
  shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1173
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1174
  def u' \<equiv> "\<lambda>x. lim (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1175
  then have *: "\<And>x. lim (\<lambda>i. f i x) = (if Cauchy (\<lambda>i. f i x) then u' x else (THE x. False))"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1176
    by (auto simp: lim_def convergent_eq_cauchy[symmetric])
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1177
  have "u' \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1178
  proof (rule borel_measurable_LIMSEQ)
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1179
    fix x
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1180
    have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1181
      by (cases "Cauchy (\<lambda>i. f i x)")
50002