src/HOL/Probability/Borel_Space.thy
author hoelzl
Mon, 19 May 2014 12:04:45 +0200
changeset 56993 e5366291d6aa
parent 56371 fb9ae0727548
child 56994 8d5e5ec1cac3
permissions -rw-r--r--
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
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
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   224
  by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   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
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   240
notation
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   241
  eucl_less (infix "<e" 50)
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   242
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   243
lemma box_oc: "{x. a <e x \<and> x \<le> b} = {x. a <e x} \<inter> {..b}"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   244
  and box_co: "{x. a \<le> x \<and> x <e b} = {a..} \<inter> {x. x <e b}"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   245
  by auto
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   246
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   247
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
   248
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   249
  shows "{x. x <e a} \<in> sets borel"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   250
    and "{x. a <e x} \<in> sets borel"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   251
    and "box a b \<in> sets borel"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   252
    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
   253
    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
   254
    and "{a..b} \<in> sets borel"
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   255
    and  "{x. a <e x \<and> x \<le> b} \<in> sets borel"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   256
    and "{x. a \<le> x \<and>  x <e b} \<in> sets borel"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   257
  unfolding box_oc box_co
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   258
  by (auto intro: borel_open borel_closed)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   259
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   260
lemma open_Collect_less:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51683
diff changeset
   261
  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   262
  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
   263
  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
   264
  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
   265
proof -
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   266
  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
   267
    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
   268
  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
   269
    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
   270
  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
   271
qed
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   272
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   273
lemma closed_Collect_le:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51683
diff changeset
   274
  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   275
  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
   276
  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
   277
  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
   278
  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
   279
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
   280
lemma borel_measurable_less[measurable]:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51683
diff changeset
   281
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   282
  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
   283
  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
   284
  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
   285
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
   286
  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
   287
    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
   288
  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
   289
    by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less]
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   290
              continuous_intros)
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   291
  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
   292
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
   293
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
lemma
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51683
diff changeset
   295
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   296
  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
   297
  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
   298
  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
   299
    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
   300
    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
   301
  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
   302
  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
   303
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
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
   305
  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
   306
  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
   307
    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
   308
    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
   309
    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
   310
  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
   311
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
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
   313
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
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
   315
  "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
   316
  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
   317
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
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
   319
  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
   320
  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
   321
  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
   322
  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
   323
  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
   324
  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
   325
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
   326
  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
   327
    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
   328
  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
   329
    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
   330
  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
   331
    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
   332
  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
   333
  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
   334
    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
   335
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
   336
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   337
lemma 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
   338
  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
   339
    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
   340
  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
   341
  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
   342
  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
   343
  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
   344
  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
   345
  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
   346
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   347
lemma borel_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
   348
  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
   349
  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
   350
  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
   351
  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
   352
  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
   353
  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
   354
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
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
   356
  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
   357
    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
   358
  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
   359
  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
   360
  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
   361
  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
   362
  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
   363
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
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
   365
  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
   366
  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
   367
  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
   368
  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
   369
  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
   370
  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
   371
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
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
   373
  "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
   374
    (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
   375
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
   376
  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
   377
  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
   378
  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
   379
    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
   380
    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
   381
    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
   382
    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
   383
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
   384
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
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
   386
  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
   387
  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
   388
    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
   389
  (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
   390
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
   391
  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
   392
    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
   393
  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
   394
  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
   395
    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
   396
    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
   397
    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
   398
      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
   399
    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
   400
      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
   401
  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
   402
    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
   403
    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
   404
    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
   405
    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
   406
  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
   407
  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
   408
    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
   409
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
   410
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
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
   412
  "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
   413
  (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
   414
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
   415
  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
   416
  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
   417
    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
   418
  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
   419
    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
   420
       (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
   421
  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
   422
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
   423
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
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
   425
  "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
   426
  (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
   427
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
   428
  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
   429
  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
   430
  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
   431
  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
   432
    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
   433
    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
   434
    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
   435
      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
   436
    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
   437
      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
   438
  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
   439
    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
   440
    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
   441
    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
   442
    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
   443
  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
   444
  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
   445
    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
   446
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
   447
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
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
   449
  "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
   450
  (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
   451
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
   452
  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
   453
  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
   454
  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
   455
    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
   456
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
   457
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
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
   459
  "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
   460
  (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
   461
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
   462
  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
   463
  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
   464
  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
   465
  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
   466
    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
   467
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
   468
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
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
   470
  "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
   471
  (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
   472
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
   473
  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
   474
  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
   475
  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
   476
  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
   477
    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
   478
    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
   479
    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
   480
      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
   481
    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
   482
      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
   483
  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
   484
  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
   485
    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
   486
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
   487
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
lemma borel_eq_greaterThan:
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   489
  "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {x. a <e x}))"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   490
  (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
   491
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
   492
  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
   493
  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
   494
  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
   495
  also have *: "{x::'a. a < x\<bullet>i} =
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   496
      (\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n) <e x})" using i
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   497
  proof (safe, simp_all add: eucl_less_def split: split_if_asm)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   498
    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
   499
    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
   500
    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
   501
    { 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
   502
      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
   503
        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
   504
      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
   505
    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
   506
      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
   507
  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
   508
  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
   509
    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
   510
    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
   511
    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
   512
    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
   513
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
   514
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
lemma borel_eq_lessThan:
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   516
  "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {x. x <e a}))"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   517
  (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
   518
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
   519
  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
   520
  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
   521
  have "{x::'a. a \<le> x\<bullet>i} = UNIV - {x::'a. x\<bullet>i < a}" by auto
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   522
  also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" using `i\<in> Basis`
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   523
  proof (safe, simp_all add: eucl_less_def split: split_if_asm)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   524
    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
   525
    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
   526
    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
   527
    { 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
   528
      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
   529
        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
   530
      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
   531
    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
   532
      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
   533
  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
   534
  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
   535
    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
   536
    apply (safe intro!: sets.countable_UN sets.Diff)
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   537
    apply (auto intro: sigma_sets_top )
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   538
    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
   539
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
   540
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
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
   542
  "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
   543
  (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
   544
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
   545
  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
   546
  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
   547
  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
   548
    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
   549
    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
   550
    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
   551
    { 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
   552
      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
   553
        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
   554
      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
   555
    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
   556
      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
   557
  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
   558
  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
   559
    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
   560
       (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
   561
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
   562
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   563
lemma eucl_lessThan: "{x::real. x <e a} = lessThan a"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   564
  by (simp add: eucl_less_def lessThan_def)
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   565
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
   566
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
   567
  "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
   568
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
   569
  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
   570
  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
   571
  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
   572
    by (auto simp: move_uminus real_arch_simple)
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   573
  then show "{y. y <e x} \<in> ?SIGMA"
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   574
    by (auto intro: sigma_sets.intros simp: eucl_lessThan)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   575
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
   576
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
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
   578
  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
   579
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
   580
  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
   581
  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
   582
  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
   583
    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
   584
       (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
   585
  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
   586
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
   587
  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
   588
  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
   589
  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
   590
    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
   591
       (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
   592
  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
   593
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
   594
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
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
   596
  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
   597
  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
   598
  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
   599
  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
   600
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
   601
  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
   602
  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
   603
    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
   604
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
   605
  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
   606
  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
   607
    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
   608
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
   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_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
   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 = (\<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
   613
  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
   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_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
   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 \<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
   618
  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
   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_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
   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 = (\<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
   623
  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
   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_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
   626
  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
   627
  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
   628
  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
   629
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
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
   631
  "(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
   632
  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
   633
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   634
lemma borel_measurable_iff_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
   635
  "(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
   636
  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
   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_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
   639
  "(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
   640
  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
   641
  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
   642
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   643
lemma borel_measurable_iff_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
   644
  "(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
   645
  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
   646
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
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
   648
  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
   649
  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
   650
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
   651
  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
   652
  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
   653
    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
   654
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
   655
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
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
   657
56993
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
   658
lemma borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
   659
  by (intro borel_measurable_continuous_on1 continuous_intros)
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
   660
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
   661
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
   662
  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
   663
  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
   664
  shows "(\<lambda>x. - g x) \<in> borel_measurable M"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   665
  by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50419
diff changeset
   666
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   667
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
   668
  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
   669
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   670
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   671
  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   672
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   673
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   674
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
   675
  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
   676
  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
   677
  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
   678
proof cases
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   679
  assume "finite S"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   680
  thus ?thesis using assms by induct auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   681
qed simp
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   682
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   683
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
   684
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   685
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   686
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   687
  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 53216
diff changeset
   688
  using borel_measurable_add [of f M "- g"] assms by (simp add: fun_Compl_def)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   689
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   690
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
   691
  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_algebra}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   692
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   693
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   694
  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   695
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   696
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   697
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
   698
  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
   699
  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
   700
  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
   701
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
   702
  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
   703
  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
   704
qed simp
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   705
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   706
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
   707
  fixes g f :: "'a \<Rightarrow> 'b::{second_countable_topology, metric_space}"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   708
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   709
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   710
  shows "(\<lambda>x. dist (f x) (g x)) \<in> borel_measurable M"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   711
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   712
  
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   713
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
   714
  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
   715
  assumes f: "f \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   716
  assumes g: "g \<in> borel_measurable M"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   717
  shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   718
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   719
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   720
lemma affine_borel_measurable_vector:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   721
  fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   722
  assumes "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   723
  shows "(\<lambda>x. a + b *\<^sub>R f x) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   724
proof (rule borel_measurableI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   725
  fix S :: "'x set" assume "open S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   726
  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
   727
  proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   728
    assume "b \<noteq> 0"
44537
c10485a6a7af make HOL-Probability respect set/pred distinction
huffman
parents: 44282
diff changeset
   729
    with `open S` have "open ((\<lambda>x. (- a + x) /\<^sub>R b) ` S)" (is "open ?S")
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 53216
diff changeset
   730
      using open_affinity [of S "inverse b" "- a /\<^sub>R b"]
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 53216
diff changeset
   731
      by (auto simp: algebra_simps)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   732
    hence "?S \<in> sets borel" by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   733
    moreover
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   734
    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
   735
      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
   736
    ultimately show ?thesis using assms unfolding in_borel_measurable_borel
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   737
      by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   738
  qed simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   739
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   740
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   741
lemma borel_measurable_const_scaleR[measurable (raw)]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   742
  "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
   743
  using affine_borel_measurable_vector[of f M 0 b] by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   744
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   745
lemma borel_measurable_const_add[measurable (raw)]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   746
  "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
   747
  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
   748
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   749
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
   750
  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
   751
  assumes f: "f \<in> borel_measurable M"
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   752
  shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   753
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
   754
  have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) \<in> borel_measurable borel"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56212
diff changeset
   755
    by (intro borel_measurable_continuous_on_open' continuous_intros) auto
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51478
diff changeset
   756
  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
   757
    by (intro ext) auto
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   758
  finally show ?thesis using f by simp
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   759
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   760
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   761
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
   762
  "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
   763
    (\<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
   764
  by (simp add: field_divide_inverse)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   765
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   766
lemma borel_measurable_max[measurable (raw)]:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51683
diff changeset
   767
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   768
  by (simp add: max_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   769
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   770
lemma borel_measurable_min[measurable (raw)]:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51683
diff changeset
   771
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   772
  by (simp add: min_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   773
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   774
lemma borel_measurable_abs[measurable (raw)]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   775
  "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
   776
  unfolding abs_real_def by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   777
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   778
lemma borel_measurable_nth[measurable (raw)]:
41026
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   779
  "(\<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
   780
  by (simp add: cart_eq_inner_axis)
41026
bea75746dc9d folding on arbitrary Lebesgue integrable functions
hoelzl
parents: 41025
diff changeset
   781
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   782
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
   783
  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
   784
  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
   785
  assumes q: "convex_on A q"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   786
  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
   787
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
   788
  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
   789
  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
   790
    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
   791
    from this q show "continuous_on A q"
42990
3706951a6421 composition of convex and measurable function is measurable
hoelzl
parents: 42950
diff changeset
   792
      by (rule convex_on_continuous)
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   793
  qed
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   794
  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
   795
    using X by (intro measurable_cong) auto
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   796
  finally show ?thesis .
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   797
qed
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   798
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   799
lemma borel_measurable_ln[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   800
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   801
  shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   802
proof -
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   803
  { fix x :: real assume x: "x \<le> 0"
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   804
    { 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
   805
    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
   806
      by (auto simp: ln_def) }
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   807
  note ln_imp = this
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   808
  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
   809
  proof (rule borel_measurable_continuous_on_open[OF _ _ f])
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   810
    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
   811
      by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont)
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   812
    show "open ({0<..}::real set)" by auto
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   813
  qed
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   814
  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
   815
    by (simp add: fun_eq_iff not_less ln_imp)
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   816
  finally show ?thesis .
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   817
qed
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   818
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   819
lemma borel_measurable_log[measurable (raw)]:
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   820
  "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
   821
  unfolding log_def by auto
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   822
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50387
diff changeset
   823
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
   824
  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
   825
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   826
lemma measurable_real_floor[measurable]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   827
  "(floor :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   828
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   829
  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
   830
    by (auto intro: floor_eq2)
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   831
  then show ?thesis
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   832
    by (auto simp: vimage_def measurable_count_space_eq2_countable)
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   833
qed
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 47694
diff changeset
   834
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   835
lemma measurable_real_natfloor[measurable]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   836
  "(natfloor :: real \<Rightarrow> nat) \<in> measurable borel (count_space UNIV)"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   837
  by (simp add: natfloor_def[abs_def])
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   838
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   839
lemma measurable_real_ceiling[measurable]:
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   840
  "(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   841
  unfolding ceiling_def[abs_def] by simp
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   842
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   843
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
   844
  by simp
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   845
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   846
lemma borel_measurable_real_natfloor:
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   847
  "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
   848
  by simp
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   849
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   850
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
   851
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   852
lemma borel_measurable_ereal[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   853
  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
   854
  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
   855
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   856
lemma borel_measurable_real_of_ereal[measurable (raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   857
  fixes f :: "'a \<Rightarrow> ereal" 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   858
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   859
  shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   860
proof -
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   861
  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
   862
    using continuous_on_real
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   863
    by (rule borel_measurable_continuous_on_open[OF _ _ f]) auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   864
  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
   865
    by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   866
  finally show ?thesis .
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   867
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   868
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   869
lemma borel_measurable_ereal_cases:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   870
  fixes f :: "'a \<Rightarrow> ereal" 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   871
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   872
  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
   873
  shows "(\<lambda>x. H (f x)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   874
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   875
  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
   876
  { 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
   877
  with f H show ?thesis by simp
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   878
qed
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   879
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   880
lemma
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   881
  fixes f :: "'a \<Rightarrow> ereal" assumes f[measurable]: "f \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   882
  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
   883
    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
   884
    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
   885
  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
   886
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   887
lemma borel_measurable_uminus_eq_ereal[simp]:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   888
  "(\<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
   889
proof
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   890
  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
   891
qed auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   892
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   893
lemma set_Collect_ereal2:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   894
  fixes f g :: "'a \<Rightarrow> ereal" 
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   895
  assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   896
  assumes g: "g \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   897
  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
   898
    "{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
   899
    "{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
   900
    "{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
   901
    "{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   902
  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
   903
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   904
  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
   905
  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
   906
  { 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
   907
  note * = this
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   908
  from assms show ?thesis
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   909
    by (subst *) (simp del: space_borel split del: split_if)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   910
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   911
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   912
lemma borel_measurable_ereal_iff:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   913
  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
   914
proof
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   915
  assume "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   916
  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
   917
  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
   918
qed auto
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   919
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   920
lemma borel_measurable_ereal_iff_real:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   921
  fixes f :: "'a \<Rightarrow> ereal"
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   922
  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
   923
    ((\<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
   924
proof safe
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   925
  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
   926
  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
   927
  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
   928
  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
   929
  have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   930
  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
   931
  finally show "f \<in> borel_measurable M" .
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   932
qed simp_all
41830
719b0a517c33 log is borel measurable
hoelzl
parents: 41545
diff changeset
   933
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   934
lemma borel_measurable_eq_atMost_ereal:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   935
  fixes f :: "'a \<Rightarrow> ereal"
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   936
  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
   937
proof (intro iffI allI)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   938
  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
   939
  show "f \<in> borel_measurable M"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   940
    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
   941
  proof (intro conjI allI)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   942
    fix a :: real
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   943
    { 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
   944
      have "x = \<infinity>"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   945
      proof (rule ereal_top)
44666
8670a39d4420 remove more duplicate lemmas
huffman
parents: 44537
diff changeset
   946
        fix B from reals_Archimedean2[of B] guess n ..
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   947
        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
   948
        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
   949
      qed }
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   950
    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
   951
      by (auto simp: not_le)
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   952
    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
   953
      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
   954
    moreover
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   955
    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
   956
    then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   957
    moreover have "{x\<in>space M. f x \<le> ereal a} \<in> sets M"
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   958
      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
   959
    moreover have "{w \<in> space M. real (f w) \<le> a} =
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   960
      (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
   961
      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
   962
      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
   963
    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
   964
  qed
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   965
qed (simp add: measurable_sets)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   966
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   967
lemma borel_measurable_eq_atLeast_ereal:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   968
  "(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
   969
proof
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
   970
  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
   971
  moreover have "\<And>a. (\<lambda>x. - f x) -` {..a} = f -` {-a ..}"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   972
    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
   973
  ultimately have "(\<lambda>x. - f x) \<in> borel_measurable M"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   974
    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
   975
  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
   976
qed (simp add: measurable_sets)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   977
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   978
lemma greater_eq_le_measurable:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   979
  fixes f :: "'a \<Rightarrow> 'c::linorder"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   980
  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
   981
proof
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   982
  assume "f -` {a ..} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   983
  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
   984
  ultimately show "f -` {..< a} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   985
next
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   986
  assume "f -` {..< a} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   987
  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
   988
  ultimately show "f -` {a ..} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   989
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   990
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   991
lemma borel_measurable_ereal_iff_less:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
   992
  "(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
   993
  unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable ..
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   994
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   995
lemma less_eq_ge_measurable:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   996
  fixes f :: "'a \<Rightarrow> 'c::linorder"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   997
  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
   998
proof
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
   999
  assume "f -` {a <..} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1000
  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
  1001
  ultimately show "f -` {..a} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1002
next
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1003
  assume "f -` {..a} \<inter> space M \<in> sets M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1004
  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
  1005
  ultimately show "f -` {a <..} \<inter> space M \<in> sets M" by auto
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1006
qed
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1007
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1008
lemma borel_measurable_ereal_iff_ge:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1009
  "(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
  1010
  unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable ..
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1011
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1012
lemma borel_measurable_ereal2:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1013
  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
  1014
  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
  1015
  assumes g: "g \<in> borel_measurable M"
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1016
  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
  1017
    "(\<lambda>x. H (-\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1018
    "(\<lambda>x. H (\<infinity>) (ereal (real (g x)))) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1019
    "(\<lambda>x. H (ereal (real (f x))) (-\<infinity>)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1020
    "(\<lambda>x. H (ereal (real (f x))) (\<infinity>)) \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1021
  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
  1022
proof -
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1023
  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
  1024
  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
  1025
  { 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
  1026
  note * = this
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1027
  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
  1028
qed
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1029
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1030
lemma
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1031
  fixes f :: "'a \<Rightarrow> ereal" assumes f: "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1032
  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
  1033
    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
  1034
  using f by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1035
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1036
lemma [measurable(raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1037
  fixes f :: "'a \<Rightarrow> ereal"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1038
  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
  1039
  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
  1040
    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
  1041
    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
  1042
    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
  1043
  by (simp_all add: borel_measurable_ereal2 min_def max_def)
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1044
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1045
lemma [measurable(raw)]:
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1046
  fixes f g :: "'a \<Rightarrow> ereal"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1047
  assumes "f \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1048
  assumes "g \<in> borel_measurable M"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1049
  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
  1050
    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
  1051
  using assms by (simp_all add: minus_ereal_def divide_ereal_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1052
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1053
lemma borel_measurable_ereal_setsum[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1054
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
41096
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1055
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1056
  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1057
proof cases
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1058
  assume "finite S"
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1059
  thus ?thesis using assms
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1060
    by induct auto
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1061
qed simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1062
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1063
lemma borel_measurable_ereal_setprod[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1064
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1065
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
41096
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1066
  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
  1067
proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1068
  assume "finite S"
41096
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1069
  thus ?thesis using assms by induct auto
843c40bbc379 integral over setprod
hoelzl
parents: 41083
diff changeset
  1070
qed simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1071
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1072
lemma borel_measurable_SUP[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1073
  fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1074
  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
  1075
  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
  1076
  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
  1077
proof
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1078
  fix a
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1079
  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
  1080
    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
  1081
  then show "?sup -` {a<..} \<inter> space M \<in> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1082
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1083
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1084
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1085
lemma borel_measurable_INF[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1086
  fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1087
  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
  1088
  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
  1089
  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
  1090
proof
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1091
  fix a
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41969
diff changeset
  1092
  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
  1093
    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
  1094
  then show "?inf -` {..<a} \<inter> space M \<in> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1095
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1096
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1097
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1098
lemma [measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1099
  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
  1100
  assumes "\<And>i. f i \<in> borel_measurable M"
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
  1101
  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
  1102
    and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 54775
diff changeset
  1103
  unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1104
50104
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 50096
diff changeset
  1105
lemma sets_Collect_eventually_sequentially[measurable]:
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1106
  "(\<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
  1107
  unfolding eventually_sequentially by simp
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1108
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1109
lemma sets_Collect_ereal_convergent[measurable]: 
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1110
  fixes f :: "nat \<Rightarrow> 'a => ereal"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1111
  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1112
  shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1113
  unfolding convergent_ereal by auto
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1114
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1115
lemma borel_measurable_extreal_lim[measurable (raw)]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1116
  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1117
  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1118
  shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1119
proof -
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1120
  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
  1121
    by (simp add: lim_def convergent_def convergent_limsup_cl)
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1122
  then show ?thesis
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1123
    by simp
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1124
qed
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1125
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1126
lemma borel_measurable_ereal_LIMSEQ:
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1127
  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1128
  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
  1129
  and u: "\<And>i. u i \<in> borel_measurable M"
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1130
  shows "u' \<in> borel_measurable M"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1131
proof -
49774
dfa8ddb874ce use continuity to show Borel-measurability
hoelzl
parents: 47761
diff changeset
  1132
  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
  1133
    using u' by (simp add: lim_imp_Liminf[symmetric])
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1134
  with u show ?thesis by (simp cong: measurable_cong)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1135
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1136
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1137
lemma borel_measurable_extreal_suminf[measurable (raw)]:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1138
  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1139
  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
  1140
  shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1141
  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
  1142
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1143
section "LIMSEQ is borel measurable"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1144
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1145
lemma borel_measurable_LIMSEQ:
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1146
  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1147
  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
  1148
  and u: "\<And>i. u i \<in> borel_measurable M"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1149
  shows "u' \<in> borel_measurable M"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1150
proof -
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1151
  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
  1152
    using u' by (simp add: lim_imp_Liminf)
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1153
  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
  1154
    by auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42990
diff changeset
  1155
  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
  1156
qed
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
  1157
56993
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1158
lemma borel_measurable_LIMSEQ_metric:
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1159
  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: metric_space"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1160
  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1161
  assumes lim: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. f i x) ----> g x"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1162
  shows "g \<in> borel_measurable M"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1163
  unfolding borel_eq_closed
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1164
proof (safe intro!: measurable_measure_of)
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1165
  fix A :: "'b set" assume "closed A" 
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1166
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1167
  have [measurable]: "(\<lambda>x. infdist (g x) A) \<in> borel_measurable M"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1168
  proof (rule borel_measurable_LIMSEQ)
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1169
    show "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. infdist (f i x) A) ----> infdist (g x) A"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1170
      by (intro tendsto_infdist lim)
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1171
    show "\<And>i. (\<lambda>x. infdist (f i x) A) \<in> borel_measurable M"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1172
      by (intro borel_measurable_continuous_on[where f="\<lambda>x. infdist x A"]
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1173
        continuous_at_imp_continuous_on ballI continuous_infdist isCont_ident) auto
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1174
  qed
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1175
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1176
  show "g -` A \<inter> space M \<in> sets M"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1177
  proof cases
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1178
    assume "A \<noteq> {}"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56371
diff changeset
  1179
    then have "\<And>x. infdist x A = 0 \<longleftrightarrow> x \<in> A"