src/HOL/Probability/Borel_Space.thy
author hoelzl
Wed, 01 Dec 2010 19:20:30 +0100
changeset 40859 de0b30e6c2d2
parent 39302 src/HOL/Probability/Borel.thy@d7728f65b353
child 40869 251df82c0088
permissions -rw-r--r--
Support product spaces on sigma finite measures. Introduce the almost everywhere quantifier. Introduce 'morphism' theorems for most constants. Prove uniqueness of measures on cut stable generators. Prove uniqueness of the Radon-Nikodym derivative. Removed misleading suffix from borel_space and lebesgue_space. Use product spaces to introduce Fubini on the Lebesgue integral. Combine Euclidean_Lebesgue and Lebesgue_Measure. Generalize theorems about mutual information and entropy to arbitrary probability spaces. Remove simproc mult_log as it does not work with interpretations. Introduce completion of measure spaces. Change type of sigma. Introduce dynkin systems.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
     1
(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
     2
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
     3
header {*Borel spaces*}
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
     4
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
     5
theory Borel_Space
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
     6
  imports Sigma_Algebra Positive_Infinite_Real Multivariate_Analysis
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
     7
begin
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
     8
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
     9
lemma (in sigma_algebra) sets_sigma_subset:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    10
  assumes "space N = space M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    11
  assumes "sets N \<subseteq> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    12
  shows "sets (sigma N) \<subseteq> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    13
  by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    14
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
    15
lemma LIMSEQ_max:
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
    16
  "u ----> (x::real) \<Longrightarrow> (\<lambda>i. max (u i) 0) ----> max x 0"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
    17
  by (fastsimp intro!: LIMSEQ_I dest!: LIMSEQ_D)
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
    18
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    19
section "Generic Borel spaces"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    20
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    21
definition "borel = sigma \<lparr> space = UNIV::'a::topological_space set, sets = open\<rparr>"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    22
abbreviation "borel_measurable M \<equiv> measurable M borel"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    23
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    24
interpretation borel: sigma_algebra borel
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    25
  by (auto simp: borel_def intro!: sigma_algebra_sigma)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    26
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    27
lemma in_borel_measurable:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    28
   "f \<in> borel_measurable M \<longleftrightarrow>
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    29
    (\<forall>S \<in> sets (sigma \<lparr> space = UNIV, sets = open\<rparr>).
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    30
      f -` S \<inter> space M \<in> sets M)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    31
  by (auto simp add: measurable_def borel_def)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    32
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    33
lemma in_borel_measurable_borel:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    34
   "f \<in> borel_measurable M \<longleftrightarrow>
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    35
    (\<forall>S \<in> sets borel.
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    36
      f -` S \<inter> space M \<in> sets M)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    37
  by (auto simp add: measurable_def borel_def)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    38
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    39
lemma space_borel[simp]: "space borel = UNIV"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    40
  unfolding borel_def by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    41
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    42
lemma borel_open[simp]:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    43
  assumes "open A" shows "A \<in> sets borel"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    44
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    45
  have "A \<in> open" unfolding mem_def using assms .
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    46
  thus ?thesis unfolding borel_def sigma_def by (auto intro!: sigma_sets.Basic)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    47
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    48
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    49
lemma borel_closed[simp]:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    50
  assumes "closed A" shows "A \<in> sets borel"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    51
proof -
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    52
  have "space borel - (- A) \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    53
    using assms unfolding closed_def by (blast intro: borel_open)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    54
  thus ?thesis by simp
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    55
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    56
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    57
lemma (in sigma_algebra) borel_measurable_vimage:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    58
  fixes f :: "'a \<Rightarrow> 'x::t2_space"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    59
  assumes borel: "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    60
  shows "f -` {x} \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    61
proof (cases "x \<in> f ` space M")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    62
  case True then obtain y where "x = f y" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    63
  from closed_sing[of "f y"]
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    64
  have "{f y} \<in> sets borel" by (rule borel_closed)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    65
  with assms show ?thesis
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    66
    unfolding in_borel_measurable_borel `x = f y` by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    67
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    68
  case False hence "f -` {x} \<inter> space M = {}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    69
  thus ?thesis by auto
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    70
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    71
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    72
lemma (in sigma_algebra) borel_measurableI:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    73
  fixes f :: "'a \<Rightarrow> 'x\<Colon>topological_space"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    74
  assumes "\<And>S. open S \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    75
  shows "f \<in> borel_measurable M"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    76
  unfolding borel_def
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    77
proof (rule measurable_sigma, simp_all)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    78
  fix S :: "'x set" assume "S \<in> open" thus "f -` S \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    79
    using assms[of S] by (simp add: mem_def)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    80
qed
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    81
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    82
lemma borel_singleton[simp, intro]:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    83
  fixes x :: "'a::t1_space"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    84
  shows "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    85
  proof (rule borel.insert_in_sets)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    86
    show "{x} \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    87
      using closed_sing[of x] by (rule borel_closed)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    88
  qed simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    89
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    90
lemma (in sigma_algebra) borel_measurable_const[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    91
  "(\<lambda>x. c) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    92
  by (auto intro!: measurable_const)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    93
39083
e46acc0ea1fe introduced integration on subalgebras
hoelzl
parents: 38705
diff changeset
    94
lemma (in sigma_algebra) borel_measurable_indicator[simp, intro!]:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    95
  assumes A: "A \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    96
  shows "indicator A \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    97
  unfolding indicator_def_raw using A
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
    98
  by (auto intro!: measurable_If_set borel_measurable_const)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
    99
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   100
lemma (in sigma_algebra) borel_measurable_indicator_iff:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   101
  "(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
   102
    (is "?I \<in> borel_measurable M \<longleftrightarrow> _")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   103
proof
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   104
  assume "?I \<in> borel_measurable M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   105
  then have "?I -` {1} \<inter> space M \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   106
    unfolding measurable_def by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   107
  also have "?I -` {1} \<inter> space M = A \<inter> space M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   108
    unfolding indicator_def_raw by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   109
  finally show "A \<inter> space M \<in> sets M" .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   110
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   111
  assume "A \<inter> space M \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   112
  moreover have "?I \<in> borel_measurable M \<longleftrightarrow>
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   113
    (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
   114
    by (intro measurable_cong) (auto simp: indicator_def)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   115
  ultimately show "?I \<in> borel_measurable M" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   116
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   117
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   118
lemma borel_measurable_translate:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   119
  assumes "A \<in> sets borel" and trans: "\<And>B. open B \<Longrightarrow> f -` B \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   120
  shows "f -` A \<in> sets borel"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   121
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   122
  have "A \<in> sigma_sets UNIV open" using assms
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   123
    by (simp add: borel_def sigma_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   124
  thus ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   125
  proof (induct rule: sigma_sets.induct)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   126
    case (Basic a) thus ?case using trans[of a] by (simp add: mem_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   127
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   128
    case (Compl a)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   129
    moreover have "UNIV \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   130
      using borel.top by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   131
    ultimately show ?case
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   132
      by (auto simp: vimage_Diff borel.Diff)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   133
  qed (auto simp add: vimage_UN)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   134
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   135
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   136
lemma (in sigma_algebra) borel_measurable_restricted:
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   137
  fixes f :: "'a \<Rightarrow> 'x\<Colon>{topological_space, semiring_1}" assumes "A \<in> sets M"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   138
  shows "f \<in> borel_measurable (restricted_space A) \<longleftrightarrow>
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   139
    (\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   140
    (is "f \<in> borel_measurable ?R \<longleftrightarrow> ?f \<in> borel_measurable M")
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   141
proof -
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   142
  interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \<in> sets M`])
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   143
  have *: "f \<in> borel_measurable ?R \<longleftrightarrow> ?f \<in> borel_measurable ?R"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   144
    by (auto intro!: measurable_cong)
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   145
  show ?thesis unfolding *
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   146
    unfolding in_borel_measurable_borel
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   147
  proof (simp, safe)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   148
    fix S :: "'x set" assume "S \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   149
      "\<forall>S\<in>sets borel. ?f -` S \<inter> A \<in> op \<inter> A ` sets M"
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   150
    then have "?f -` S \<inter> A \<in> op \<inter> A ` sets M" by auto
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   151
    then have f: "?f -` S \<inter> A \<in> sets M"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   152
      using `A \<in> sets M` sets_into_space by fastsimp
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   153
    show "?f -` S \<inter> space M \<in> sets M"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   154
    proof cases
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   155
      assume "0 \<in> S"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   156
      then have "?f -` S \<inter> space M = ?f -` S \<inter> A \<union> (space M - A)"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   157
        using `A \<in> sets M` sets_into_space by auto
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   158
      then show ?thesis using f `A \<in> sets M` by (auto intro!: Un Diff)
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   159
    next
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   160
      assume "0 \<notin> S"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   161
      then have "?f -` S \<inter> space M = ?f -` S \<inter> A"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   162
        using `A \<in> sets M` sets_into_space
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   163
        by (auto simp: indicator_def split: split_if_asm)
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   164
      then show ?thesis using f by auto
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   165
    qed
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   166
  next
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   167
    fix S :: "'x set" assume "S \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   168
      "\<forall>S\<in>sets borel. ?f -` S \<inter> space M \<in> sets M"
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   169
    then have f: "?f -` S \<inter> space M \<in> sets M" by auto
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   170
    then show "?f -` S \<inter> A \<in> op \<inter> A ` sets M"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   171
      using `A \<in> sets M` sets_into_space
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   172
      apply (simp add: image_iff)
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   173
      apply (rule bexI[OF _ f])
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   174
      by auto
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   175
  qed
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   176
qed
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   177
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   178
lemma (in sigma_algebra) borel_measurable_subalgebra:
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   179
  assumes "N \<subseteq> sets M" "f \<in> borel_measurable (M\<lparr>sets:=N\<rparr>)"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   180
  shows "f \<in> borel_measurable M"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   181
  using assms unfolding measurable_def by auto
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39087
diff changeset
   182
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   183
section "Borel spaces on euclidean spaces"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   184
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   185
lemma lessThan_borel[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   186
  fixes a :: "'a\<Colon>ordered_euclidean_space"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   187
  shows "{..< a} \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   188
  by (blast intro: borel_open)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   189
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   190
lemma greaterThan_borel[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   191
  fixes a :: "'a\<Colon>ordered_euclidean_space"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   192
  shows "{a <..} \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   193
  by (blast intro: borel_open)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   194
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   195
lemma greaterThanLessThan_borel[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   196
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   197
  shows "{a<..<b} \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   198
  by (blast intro: borel_open)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   199
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   200
lemma atMost_borel[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   201
  fixes a :: "'a\<Colon>ordered_euclidean_space"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   202
  shows "{..a} \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   203
  by (blast intro: borel_closed)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   204
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   205
lemma atLeast_borel[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   206
  fixes a :: "'a\<Colon>ordered_euclidean_space"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   207
  shows "{a..} \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   208
  by (blast intro: borel_closed)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   209
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   210
lemma atLeastAtMost_borel[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   211
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   212
  shows "{a..b} \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   213
  by (blast intro: borel_closed)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   214
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   215
lemma greaterThanAtMost_borel[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   216
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   217
  shows "{a<..b} \<in> sets borel"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   218
  unfolding greaterThanAtMost_def by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   219
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   220
lemma atLeastLessThan_borel[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   221
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   222
  shows "{a..<b} \<in> sets borel"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   223
  unfolding atLeastLessThan_def by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   224
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   225
lemma hafspace_less_borel[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   226
  fixes a :: real
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   227
  shows "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   228
  by (auto intro!: borel_open open_halfspace_component_gt)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   229
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   230
lemma hafspace_greater_borel[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   231
  fixes a :: real
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   232
  shows "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   233
  by (auto intro!: borel_open open_halfspace_component_lt)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   234
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   235
lemma hafspace_less_eq_borel[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   236
  fixes a :: real
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   237
  shows "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   238
  by (auto intro!: borel_closed closed_halfspace_component_ge)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   239
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   240
lemma hafspace_greater_eq_borel[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   241
  fixes a :: real
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   242
  shows "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   243
  by (auto intro!: borel_closed closed_halfspace_component_le)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   244
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   245
lemma (in sigma_algebra) borel_measurable_less[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   246
  fixes f :: "'a \<Rightarrow> real"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   247
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   248
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   249
  shows "{w \<in> space M. f w < g w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   250
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   251
  have "{w \<in> space M. f w < g w} =
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   252
        (\<Union>r. (f -` {..< of_rat r} \<inter> space M) \<inter> (g -` {of_rat r <..} \<inter> space M))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   253
    using Rats_dense_in_real by (auto simp add: Rats_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   254
  then show ?thesis using f g
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   255
    by simp (blast intro: measurable_sets)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   256
qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   257
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   258
lemma (in sigma_algebra) borel_measurable_le[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   259
  fixes f :: "'a \<Rightarrow> real"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   260
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   261
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   262
  shows "{w \<in> space M. f w \<le> g w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   263
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   264
  have "{w \<in> space M. f w \<le> g w} = space M - {w \<in> space M. g w < f w}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   265
    by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   266
  thus ?thesis using f g
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   267
    by simp blast
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   268
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   269
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   270
lemma (in sigma_algebra) borel_measurable_eq[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   271
  fixes f :: "'a \<Rightarrow> real"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   272
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   273
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   274
  shows "{w \<in> space M. f w = g w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   275
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   276
  have "{w \<in> space M. f w = g w} =
33536
fd28b7399f2b eliminated hard tabulators;
wenzelm
parents: 33535
diff changeset
   277
        {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   278
    by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   279
  thus ?thesis using f g by auto
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   280
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   281
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   282
lemma (in sigma_algebra) borel_measurable_neq[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   283
  fixes f :: "'a \<Rightarrow> real"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   284
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   285
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   286
  shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   287
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   288
  have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   289
    by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   290
  thus ?thesis using f g by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   291
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   292
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   293
subsection "Borel space equals sigma algebras over intervals"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   294
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   295
lemma rational_boxes:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   296
  fixes x :: "'a\<Colon>ordered_euclidean_space"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   297
  assumes "0 < e"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   298
  shows "\<exists>a b. (\<forall>i. a $$ i \<in> \<rat>) \<and> (\<forall>i. b $$ i \<in> \<rat>) \<and> x \<in> {a <..< b} \<and> {a <..< b} \<subseteq> ball x e"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   299
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   300
  def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   301
  then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   302
  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x $$ i \<and> x $$ i - y < e'" (is "\<forall>i. ?th i")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   303
  proof
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   304
    fix i from Rats_dense_in_real[of "x $$ i - e'" "x $$ i"] e
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   305
    show "?th i" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   306
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   307
  from choice[OF this] guess a .. note a = this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   308
  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x $$ i < y \<and> y - x $$ i < e'" (is "\<forall>i. ?th i")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   309
  proof
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   310
    fix i from Rats_dense_in_real[of "x $$ i" "x $$ i + e'"] e
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   311
    show "?th i" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   312
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   313
  from choice[OF this] guess b .. note b = this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   314
  { fix y :: 'a assume *: "Chi a < y" "y < Chi b"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   315
    have "dist x y = sqrt (\<Sum>i<DIM('a). (dist (x $$ i) (y $$ i))\<twosuperior>)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   316
      unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   317
    also have "\<dots> < sqrt (\<Sum>i<DIM('a). e^2 / real (DIM('a)))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   318
    proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   319
      fix i assume i: "i \<in> {..<DIM('a)}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   320
      have "a i < y$$i \<and> y$$i < b i" using * i eucl_less[where 'a='a] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   321
      moreover have "a i < x$$i" "x$$i - a i < e'" using a by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   322
      moreover have "x$$i < b i" "b i - x$$i < e'" using b by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   323
      ultimately have "\<bar>x$$i - y$$i\<bar> < 2 * e'" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   324
      then have "dist (x $$ i) (y $$ i) < e/sqrt (real (DIM('a)))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   325
        unfolding e'_def by (auto simp: dist_real_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   326
      then have "(dist (x $$ i) (y $$ i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   327
        by (rule power_strict_mono) auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   328
      then show "(dist (x $$ i) (y $$ i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   329
        by (simp add: power_divide)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   330
    qed auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   331
    also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   332
    finally have "dist x y < e" . }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   333
  with a b show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   334
    apply (rule_tac exI[of _ "Chi a"])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   335
    apply (rule_tac exI[of _ "Chi b"])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   336
    using eucl_less[where 'a='a] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   337
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   338
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   339
lemma ex_rat_list:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   340
  fixes x :: "'a\<Colon>ordered_euclidean_space"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   341
  assumes "\<And> i. x $$ i \<in> \<rat>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   342
  shows "\<exists> r. length r = DIM('a) \<and> (\<forall> i < DIM('a). of_rat (r ! i) = x $$ i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   343
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   344
  have "\<forall>i. \<exists>r. x $$ i = of_rat r" using assms unfolding Rats_def by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   345
  from choice[OF this] guess r ..
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   346
  then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   347
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   348
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   349
lemma open_UNION:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   350
  fixes M :: "'a\<Colon>ordered_euclidean_space set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   351
  assumes "open M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   352
  shows "M = UNION {(a, b) | a b. {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)} \<subseteq> M}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   353
                   (\<lambda> (a, b). {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   354
    (is "M = UNION ?idx ?box")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   355
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   356
  fix x assume "x \<in> M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   357
  obtain e where e: "e > 0" "ball x e \<subseteq> M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   358
    using openE[OF assms `x \<in> M`] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   359
  then obtain a b where ab: "x \<in> {a <..< b}" "\<And>i. a $$ i \<in> \<rat>" "\<And>i. b $$ i \<in> \<rat>" "{a <..< b} \<subseteq> ball x e"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   360
    using rational_boxes[OF e(1)] by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   361
  then obtain p q where pq: "length p = DIM ('a)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   362
                            "length q = DIM ('a)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   363
                            "\<forall> i < DIM ('a). of_rat (p ! i) = a $$ i \<and> of_rat (q ! i) = b $$ i"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   364
    using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   365
  hence p: "Chi (of_rat \<circ> op ! p) = a"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   366
    using euclidean_eq[of "Chi (of_rat \<circ> op ! p)" a]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   367
    unfolding o_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   368
  from pq have q: "Chi (of_rat \<circ> op ! q) = b"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   369
    using euclidean_eq[of "Chi (of_rat \<circ> op ! q)" b]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   370
    unfolding o_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   371
  have "x \<in> ?box (p, q)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   372
    using p q ab by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   373
  thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   374
qed auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   375
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   376
lemma halfspace_span_open:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   377
  "sigma_sets UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a}))
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   378
    \<subseteq> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   379
  by (auto intro!: borel.sigma_sets_subset[simplified] borel_open
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   380
                   open_halfspace_component_lt)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   381
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   382
lemma halfspace_lt_in_halfspace:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   383
  "{x\<Colon>'a. x $$ i < a} \<in> sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})\<rparr>)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   384
  by (auto intro!: sigma_sets.Basic simp: sets_sigma)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   385
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   386
lemma halfspace_gt_in_halfspace:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   387
  "{x\<Colon>'a. a < x $$ i} \<in> sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})\<rparr>)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   388
  (is "?set \<in> sets ?SIGMA")
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   389
proof -
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   390
  interpret sigma_algebra "?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   391
    by (intro sigma_algebra_sigma_sets) (simp_all add: sets_sigma)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   392
  have *: "?set = (\<Union>n. space ?SIGMA - {x\<Colon>'a. x $$ i < a + 1 / real (Suc n)})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   393
  proof (safe, simp_all add: not_less)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   394
    fix x assume "a < x $$ i"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   395
    with reals_Archimedean[of "x $$ i - a"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   396
    obtain n where "a + 1 / real (Suc n) < x $$ i"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   397
      by (auto simp: inverse_eq_divide field_simps)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   398
    then show "\<exists>n. a + 1 / real (Suc n) \<le> x $$ i"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   399
      by (blast intro: less_imp_le)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   400
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   401
    fix x n
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   402
    have "a < a + 1 / real (Suc n)" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   403
    also assume "\<dots> \<le> x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   404
    finally show "a < x" .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   405
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   406
  show "?set \<in> sets ?SIGMA" unfolding *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   407
    by (safe intro!: countable_UN Diff halfspace_lt_in_halfspace)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   408
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   409
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   410
lemma open_span_halfspace:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   411
  "sets borel \<subseteq> sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x $$ i < a})\<rparr>)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   412
    (is "_ \<subseteq> sets ?SIGMA")
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   413
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   414
  have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   415
  then interpret sigma_algebra ?SIGMA .
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   416
  { fix S :: "'a set" assume "S \<in> open" then have "open S" unfolding mem_def .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   417
    from open_UNION[OF this]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   418
    obtain I where *: "S =
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   419
      (\<Union>(a, b)\<in>I.
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   420
          (\<Inter> i<DIM('a). {x. (Chi (real_of_rat \<circ> op ! a)::'a) $$ i < x $$ i}) \<inter>
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   421
          (\<Inter> i<DIM('a). {x. x $$ i < (Chi (real_of_rat \<circ> op ! b)::'a) $$ i}))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   422
      unfolding greaterThanLessThan_def
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   423
      unfolding eucl_greaterThan_eq_halfspaces[where 'a='a]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   424
      unfolding eucl_lessThan_eq_halfspaces[where 'a='a]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   425
      by blast
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   426
    have "S \<in> sets ?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   427
      unfolding *
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   428
      by (auto intro!: countable_UN Int countable_INT halfspace_lt_in_halfspace halfspace_gt_in_halfspace) }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   429
  then show ?thesis unfolding borel_def
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   430
    by (intro sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   431
qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   432
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   433
lemma halfspace_span_halfspace_le:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   434
  "sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})\<rparr>) \<subseteq>
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   435
   sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x. x $$ i \<le> a})\<rparr>)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   436
  (is "_ \<subseteq> sets ?SIGMA")
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   437
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   438
  have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   439
  then interpret sigma_algebra ?SIGMA .
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   440
  { fix a i
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   441
    have *: "{x::'a. x$$i < a} = (\<Union>n. {x. x$$i \<le> a - 1/real (Suc n)})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   442
    proof (safe, simp_all)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   443
      fix x::'a assume *: "x$$i < a"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   444
      with reals_Archimedean[of "a - x$$i"]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   445
      obtain n where "x $$ i < a - 1 / (real (Suc n))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   446
        by (auto simp: field_simps inverse_eq_divide)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   447
      then show "\<exists>n. x $$ i \<le> a - 1 / (real (Suc n))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   448
        by (blast intro: less_imp_le)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   449
    next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   450
      fix x::'a and n
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   451
      assume "x$$i \<le> a - 1 / real (Suc n)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   452
      also have "\<dots> < a" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   453
      finally show "x$$i < a" .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   454
    qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   455
    have "{x. x$$i < a} \<in> sets ?SIGMA" unfolding *
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   456
      by (safe intro!: countable_UN)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   457
         (auto simp: sets_sigma intro!: sigma_sets.Basic) }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   458
  then show ?thesis by (intro sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   459
qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   460
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   461
lemma halfspace_span_halfspace_ge:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   462
  "sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})\<rparr>) \<subseteq>
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   463
   sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x. a \<le> x $$ i})\<rparr>)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   464
  (is "_ \<subseteq> sets ?SIGMA")
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   465
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   466
  have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   467
  then interpret sigma_algebra ?SIGMA .
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   468
  { fix a i have *: "{x::'a. x$$i < a} = space ?SIGMA - {x::'a. a \<le> x$$i}" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   469
    have "{x. x$$i < a} \<in> sets ?SIGMA" unfolding *
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   470
      by (safe intro!: Diff)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   471
         (auto simp: sets_sigma intro!: sigma_sets.Basic) }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   472
  then show ?thesis by (intro sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   473
qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   474
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   475
lemma halfspace_le_span_halfspace_gt:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   476
  "sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a})\<rparr>) \<subseteq>
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   477
   sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x. a < x $$ i})\<rparr>)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   478
  (is "_ \<subseteq> sets ?SIGMA")
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   479
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   480
  have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   481
  then interpret sigma_algebra ?SIGMA .
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   482
  { fix a i have *: "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   483
    have "{x. x$$i \<le> a} \<in> sets ?SIGMA" unfolding *
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   484
      by (safe intro!: Diff)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   485
         (auto simp: sets_sigma intro!: sigma_sets.Basic) }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   486
  then show ?thesis by (intro sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   487
qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   488
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   489
lemma halfspace_le_span_atMost:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   490
  "sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a})\<rparr>) \<subseteq>
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   491
   sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space})\<rparr>)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   492
  (is "_ \<subseteq> sets ?SIGMA")
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   493
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   494
  have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   495
  then interpret sigma_algebra ?SIGMA .
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   496
  have "\<And>a i. {x. x$$i \<le> a} \<in> sets ?SIGMA"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   497
  proof cases
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   498
    fix a i assume "i < DIM('a)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   499
    then have *: "{x::'a. x$$i \<le> a} = (\<Union>k::nat. {.. (\<chi>\<chi> n. if n = i then a else real k)})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   500
    proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   501
      fix x
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   502
      from real_arch_simple[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"] guess k::nat ..
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   503
      then have "\<And>i. i < DIM('a) \<Longrightarrow> x$$i \<le> real k"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   504
        by (subst (asm) Max_le_iff) auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   505
      then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia \<le> real k"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   506
        by (auto intro!: exI[of _ k])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   507
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   508
    show "{x. x$$i \<le> a} \<in> sets ?SIGMA" unfolding *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   509
      by (safe intro!: countable_UN)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   510
         (auto simp: sets_sigma intro!: sigma_sets.Basic)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   511
  next
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   512
    fix a i assume "\<not> i < DIM('a)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   513
    then show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   514
      using top by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   515
  qed
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   516
  then show ?thesis by (intro sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   517
qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   518
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   519
lemma halfspace_le_span_greaterThan:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   520
  "sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a})\<rparr>) \<subseteq>
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   521
   sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>a. {a<..})\<rparr>)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   522
  (is "_ \<subseteq> sets ?SIGMA")
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   523
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   524
  have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   525
  then interpret sigma_algebra ?SIGMA .
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   526
  have "\<And>a i. {x. x$$i \<le> a} \<in> sets ?SIGMA"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   527
  proof cases
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   528
    fix a i assume "i < DIM('a)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   529
    have "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   530
    also have *: "{x::'a. a < x$$i} = (\<Union>k::nat. {(\<chi>\<chi> n. if n = i then a else -real k) <..})" using `i <DIM('a)`
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   531
    proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   532
      fix x
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   533
      from real_arch_lt[of "Max ((\<lambda>i. -x$$i)`{..<DIM('a)})"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   534
      guess k::nat .. note k = this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   535
      { fix i assume "i < DIM('a)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   536
        then have "-x$$i < real k"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   537
          using k by (subst (asm) Max_less_iff) auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   538
        then have "- real k < x$$i" by simp }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   539
      then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> -real k < x $$ ia"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   540
        by (auto intro!: exI[of _ k])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   541
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   542
    finally show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   543
      apply (simp only:)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   544
      apply (safe intro!: countable_UN Diff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   545
      by (auto simp: sets_sigma intro!: sigma_sets.Basic)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   546
  next
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   547
    fix a i assume "\<not> i < DIM('a)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   548
    then show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   549
      using top by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   550
  qed
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   551
  then show ?thesis by (intro sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   552
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   553
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   554
lemma halfspace_le_span_lessThan:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   555
  "sets (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. a \<le> x $$ i})\<rparr>) \<subseteq>
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   556
   sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>a. {..<a})\<rparr>)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   557
  (is "_ \<subseteq> sets ?SIGMA")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   558
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   559
  have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   560
  then interpret sigma_algebra ?SIGMA .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   561
  have "\<And>a i. {x. a \<le> x$$i} \<in> sets ?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   562
  proof cases
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   563
    fix a i assume "i < DIM('a)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   564
    have "{x::'a. a \<le> x$$i} = space ?SIGMA - {x::'a. x$$i < a}" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   565
    also have *: "{x::'a. x$$i < a} = (\<Union>k::nat. {..< (\<chi>\<chi> n. if n = i then a else real k)})" using `i <DIM('a)`
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   566
    proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   567
      fix x
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   568
      from real_arch_lt[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   569
      guess k::nat .. note k = this
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   570
      { fix i assume "i < DIM('a)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   571
        then have "x$$i < real k"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   572
          using k by (subst (asm) Max_less_iff) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   573
        then have "x$$i < real k" by simp }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   574
      then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia < real k"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   575
        by (auto intro!: exI[of _ k])
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   576
    qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   577
    finally show "{x. a \<le> x$$i} \<in> sets ?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   578
      apply (simp only:)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   579
      apply (safe intro!: countable_UN Diff)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   580
      by (auto simp: sets_sigma intro!: sigma_sets.Basic)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   581
  next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   582
    fix a i assume "\<not> i < DIM('a)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   583
    then show "{x. a \<le> x$$i} \<in> sets ?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   584
      using top by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   585
  qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   586
  then show ?thesis by (intro sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   587
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   588
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   589
lemma atMost_span_atLeastAtMost:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   590
  "sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space})\<rparr>) \<subseteq>
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   591
   sets (sigma \<lparr>space=UNIV, sets=range (\<lambda>(a,b). {a..b})\<rparr>)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   592
  (is "_ \<subseteq> sets ?SIGMA")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   593
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   594
  have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   595
  then interpret sigma_algebra ?SIGMA .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   596
  { fix a::'a
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   597
    have *: "{..a} = (\<Union>n::nat. {- real n *\<^sub>R One .. a})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   598
    proof (safe, simp_all add: eucl_le[where 'a='a])
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   599
      fix x
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   600
      from real_arch_simple[of "Max ((\<lambda>i. - x$$i)`{..<DIM('a)})"]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   601
      guess k::nat .. note k = this
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   602
      { fix i assume "i < DIM('a)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   603
        with k have "- x$$i \<le> real k"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   604
          by (subst (asm) Max_le_iff) (auto simp: field_simps)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   605
        then have "- real k \<le> x$$i" by simp }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   606
      then show "\<exists>n::nat. \<forall>i<DIM('a). - real n \<le> x $$ i"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   607
        by (auto intro!: exI[of _ k])
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   608
    qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   609
    have "{..a} \<in> sets ?SIGMA" unfolding *
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   610
      by (safe intro!: countable_UN)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   611
         (auto simp: sets_sigma intro!: sigma_sets.Basic) }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   612
  then show ?thesis by (intro sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   613
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   614
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   615
lemma algebra_eqI: assumes "sets A = sets (B::'a algebra)" "space A = space B"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   616
  shows "A = B" using assms by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   617
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   618
lemma borel_eq_atMost:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   619
  "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> a. {.. a::'a\<Colon>ordered_euclidean_space})\<rparr>)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   620
    (is "_ = ?SIGMA")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   621
proof (rule algebra_eqI, rule antisym)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   622
  show "sets borel \<subseteq> sets ?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   623
    using halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   624
    by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   625
  show "sets ?SIGMA \<subseteq> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   626
    by (rule borel.sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   627
qed auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   628
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   629
lemma borel_eq_atLeastAtMost:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   630
  "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space, b). {a .. b})\<rparr>)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   631
   (is "_ = ?SIGMA")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   632
proof (rule algebra_eqI, rule antisym)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   633
  show "sets borel \<subseteq> sets ?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   634
    using atMost_span_atLeastAtMost halfspace_le_span_atMost
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   635
      halfspace_span_halfspace_le open_span_halfspace
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   636
    by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   637
  show "sets ?SIGMA \<subseteq> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   638
    by (rule borel.sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   639
qed auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   640
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   641
lemma borel_eq_greaterThan:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   642
  "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space). {a <..})\<rparr>)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   643
   (is "_ = ?SIGMA")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   644
proof (rule algebra_eqI, rule antisym)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   645
  show "sets borel \<subseteq> sets ?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   646
    using halfspace_le_span_greaterThan
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   647
      halfspace_span_halfspace_le open_span_halfspace
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   648
    by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   649
  show "sets ?SIGMA \<subseteq> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   650
    by (rule borel.sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   651
qed auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   652
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   653
lemma borel_eq_lessThan:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   654
  "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space). {..< a})\<rparr>)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   655
   (is "_ = ?SIGMA")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   656
proof (rule algebra_eqI, rule antisym)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   657
  show "sets borel \<subseteq> sets ?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   658
    using halfspace_le_span_lessThan
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   659
      halfspace_span_halfspace_ge open_span_halfspace
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   660
    by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   661
  show "sets ?SIGMA \<subseteq> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   662
    by (rule borel.sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   663
qed auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   664
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   665
lemma borel_eq_greaterThanLessThan:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   666
  "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, b). {a <..< (b :: 'a \<Colon> ordered_euclidean_space)})\<rparr>)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   667
    (is "_ = ?SIGMA")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   668
proof (rule algebra_eqI, rule antisym)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   669
  show "sets ?SIGMA \<subseteq> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   670
    by (rule borel.sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   671
  show "sets borel \<subseteq> sets ?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   672
  proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   673
    have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   674
    then interpret sigma_algebra ?SIGMA .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   675
    { fix M :: "'a set" assume "M \<in> open"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   676
      then have "open M" by (simp add: mem_def)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   677
      have "M \<in> sets ?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   678
        apply (subst open_UNION[OF `open M`])
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   679
        apply (safe intro!: countable_UN)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   680
        by (auto simp add: sigma_def intro!: sigma_sets.Basic) }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   681
    then show ?thesis
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   682
      unfolding borel_def by (intro sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   683
  qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   684
qed auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   685
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   686
lemma borel_eq_halfspace_le:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   687
  "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i \<le> a})\<rparr>)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   688
   (is "_ = ?SIGMA")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   689
proof (rule algebra_eqI, rule antisym)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   690
  show "sets borel \<subseteq> sets ?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   691
    using open_span_halfspace halfspace_span_halfspace_le by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   692
  show "sets ?SIGMA \<subseteq> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   693
    by (rule borel.sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   694
qed auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   695
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   696
lemma borel_eq_halfspace_less:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   697
  "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i < a})\<rparr>)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   698
   (is "_ = ?SIGMA")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   699
proof (rule algebra_eqI, rule antisym)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   700
  show "sets borel \<subseteq> sets ?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   701
    using open_span_halfspace .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   702
  show "sets ?SIGMA \<subseteq> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   703
    by (rule borel.sets_sigma_subset) auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   704
qed auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   705
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   706
lemma borel_eq_halfspace_gt:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   707
  "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a < x$$i})\<rparr>)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   708
   (is "_ = ?SIGMA")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   709
proof (rule algebra_eqI, rule antisym)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   710
  show "sets borel \<subseteq> sets ?SIGMA"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   711
    using halfspace_le_span_halfspace_gt open_span_halfspace halfspace_span_halfspace_le by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   712
  show "sets ?SIGMA \<subseteq> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   713
    by (rule borel.sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   714
qed auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   715
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   716
lemma borel_eq_halfspace_ge:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   717
  "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a \<le> x$$i})\<rparr>)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   718
   (is "_ = ?SIGMA")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   719
proof (rule algebra_eqI, rule antisym)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   720
  show "sets borel \<subseteq> sets ?SIGMA"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   721
    using halfspace_span_halfspace_ge open_span_halfspace by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   722
  show "sets ?SIGMA \<subseteq> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   723
    by (rule borel.sets_sigma_subset) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   724
qed auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   725
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   726
lemma (in sigma_algebra) borel_measurable_halfspacesI:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   727
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   728
  assumes "borel = (sigma \<lparr>space=UNIV, sets=range F\<rparr>)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   729
  and "\<And>a i. S a i = f -` F (a,i) \<inter> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   730
  and "\<And>a i. \<not> i < DIM('c) \<Longrightarrow> S a i \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   731
  shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a::real. S a i \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   732
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   733
  fix a :: real and i assume i: "i < DIM('c)" and f: "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   734
  then show "S a i \<in> sets M" unfolding assms
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   735
    by (auto intro!: measurable_sets sigma_sets.Basic simp: assms(1) sigma_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   736
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   737
  assume a: "\<forall>i<DIM('c). \<forall>a. S a i \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   738
  { fix a i have "S a i \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   739
    proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   740
      assume "i < DIM('c)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   741
      with a show ?thesis unfolding assms(2) by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   742
    next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   743
      assume "\<not> i < DIM('c)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   744
      from assms(3)[OF this] show ?thesis .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   745
    qed }
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   746
  then have "f \<in> measurable M (sigma \<lparr>space=UNIV, sets=range F\<rparr>)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   747
    by (auto intro!: measurable_sigma simp: assms(2))
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   748
  then show "f \<in> borel_measurable M" unfolding measurable_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   749
    unfolding assms(1) by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   750
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   751
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   752
lemma (in sigma_algebra) borel_measurable_iff_halfspace_le:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   753
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   754
  shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. f w $$ i \<le> a} \<in> sets M)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   755
  by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   756
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   757
lemma (in sigma_algebra) borel_measurable_iff_halfspace_less:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   758
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   759
  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. f w $$ i < a} \<in> sets M)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   760
  by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   761
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   762
lemma (in sigma_algebra) borel_measurable_iff_halfspace_ge:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   763
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   764
  shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. a \<le> f w $$ i} \<in> sets M)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   765
  by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   766
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   767
lemma (in sigma_algebra) borel_measurable_iff_halfspace_greater:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   768
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   769
  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. a < f w $$ i} \<in> sets M)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   770
  by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_gt]) auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   771
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   772
lemma (in sigma_algebra) borel_measurable_iff_le:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   773
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   774
  using borel_measurable_iff_halfspace_le[where 'c=real] by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   775
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   776
lemma (in sigma_algebra) borel_measurable_iff_less:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   777
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   778
  using borel_measurable_iff_halfspace_less[where 'c=real] by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   779
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   780
lemma (in sigma_algebra) borel_measurable_iff_ge:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   781
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   782
  using borel_measurable_iff_halfspace_ge[where 'c=real] by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   783
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   784
lemma (in sigma_algebra) borel_measurable_iff_greater:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   785
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   786
  using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   787
39087
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   788
lemma borel_measureable_euclidean_component:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   789
  "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   790
  unfolding borel_def[where 'a=real]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   791
proof (rule borel.measurable_sigma, simp_all)
39087
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   792
  fix S::"real set" assume "S \<in> open" then have "open S" unfolding mem_def .
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   793
  from open_vimage_euclidean_component[OF this]
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   794
  show "(\<lambda>x. x $$ i) -` S \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   795
    by (auto intro: borel_open)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   796
qed
39087
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   797
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   798
lemma (in sigma_algebra) borel_measureable_euclidean_space:
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   799
  fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   800
  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M)"
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   801
proof safe
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   802
  fix i assume "f \<in> borel_measurable M"
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   803
  then show "(\<lambda>x. f x $$ i) \<in> borel_measurable M"
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   804
    using measurable_comp[of f _ _ "\<lambda>x. x $$ i", unfolded comp_def]
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   805
    by (auto intro: borel_measureable_euclidean_component)
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   806
next
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   807
  assume f: "\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M"
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   808
  then show "f \<in> borel_measurable M"
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   809
    unfolding borel_measurable_iff_halfspace_le by auto
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   810
qed
96984bf6fa5b Measurable on euclidean space is equiv. to measurable components
hoelzl
parents: 39083
diff changeset
   811
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   812
subsection "Borel measurable operators"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   813
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   814
lemma (in sigma_algebra) affine_borel_measurable_vector:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   815
  fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   816
  assumes "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   817
  shows "(\<lambda>x. a + b *\<^sub>R f x) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   818
proof (rule borel_measurableI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   819
  fix S :: "'x set" assume "open S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   820
  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
   821
  proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   822
    assume "b \<noteq> 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   823
    with `open S` have "((\<lambda>x. (- a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   824
      by (auto intro!: open_affinity simp: scaleR.add_right mem_def)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   825
    hence "?S \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   826
      unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   827
    moreover
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   828
    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
   829
      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
   830
    ultimately show ?thesis using assms unfolding in_borel_measurable_borel
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   831
      by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   832
  qed simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   833
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   834
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   835
lemma (in sigma_algebra) affine_borel_measurable:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   836
  fixes g :: "'a \<Rightarrow> real"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   837
  assumes g: "g \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   838
  shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   839
  using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   840
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   841
lemma (in sigma_algebra) borel_measurable_add[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   842
  fixes f :: "'a \<Rightarrow> real"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   843
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   844
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   845
  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   846
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   847
  have 1: "\<And>a. {w\<in>space M. a \<le> f w + g w} = {w \<in> space M. a + g w * -1 \<le> f w}"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   848
    by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   849
  have "\<And>a. (\<lambda>w. a + (g w) * -1) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   850
    by (rule affine_borel_measurable [OF g])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   851
  then have "\<And>a. {w \<in> space M. (\<lambda>w. a + (g w) * -1)(w) \<le> f w} \<in> sets M" using f
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   852
    by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   853
  then have "\<And>a. {w \<in> space M. a \<le> f w + g w} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   854
    by (simp add: 1)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   855
  then show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   856
    by (simp add: borel_measurable_iff_ge)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   857
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   858
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   859
lemma (in sigma_algebra) borel_measurable_square:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   860
  fixes f :: "'a \<Rightarrow> real"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   861
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   862
  shows "(\<lambda>x. (f x)^2) \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   863
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   864
  {
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   865
    fix a
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   866
    have "{w \<in> space M. (f w)\<twosuperior> \<le> a} \<in> sets M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   867
    proof (cases rule: linorder_cases [of a 0])
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   868
      case less
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   869
      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = {}"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   870
        by auto (metis less order_le_less_trans power2_less_0)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   871
      also have "... \<in> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   872
        by (rule empty_sets)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   873
      finally show ?thesis .
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   874
    next
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   875
      case equal
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   876
      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   877
             {w \<in> space M. f w \<le> 0} \<inter> {w \<in> space M. 0 \<le> f w}"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   878
        by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   879
      also have "... \<in> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   880
        apply (insert f)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   881
        apply (rule Int)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   882
        apply (simp add: borel_measurable_iff_le)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   883
        apply (simp add: borel_measurable_iff_ge)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   884
        done
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   885
      finally show ?thesis .
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   886
    next
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   887
      case greater
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   888
      have "\<forall>x. (f x ^ 2 \<le> sqrt a ^ 2) = (- sqrt a  \<le> f x & f x \<le> sqrt a)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   889
        by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   890
                  real_sqrt_le_iff real_sqrt_power)
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   891
      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   892
             {w \<in> space M. -(sqrt a) \<le> f w} \<inter> {w \<in> space M. f w \<le> sqrt a}"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   893
        using greater by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   894
      also have "... \<in> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   895
        apply (insert f)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   896
        apply (rule Int)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   897
        apply (simp add: borel_measurable_iff_ge)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   898
        apply (simp add: borel_measurable_iff_le)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   899
        done
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   900
      finally show ?thesis .
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   901
    qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   902
  }
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   903
  thus ?thesis by (auto simp add: borel_measurable_iff_le)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   904
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   905
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   906
lemma times_eq_sum_squares:
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   907
   fixes x::real
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   908
   shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   909
by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric])
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   910
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   911
lemma (in sigma_algebra) borel_measurable_uminus[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   912
  fixes g :: "'a \<Rightarrow> real"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   913
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   914
  shows "(\<lambda>x. - g x) \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   915
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   916
  have "(\<lambda>x. - g x) = (\<lambda>x. 0 + (g x) * -1)"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   917
    by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   918
  also have "... \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   919
    by (fast intro: affine_borel_measurable g)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   920
  finally show ?thesis .
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   921
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   922
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   923
lemma (in sigma_algebra) borel_measurable_times[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   924
  fixes f :: "'a \<Rightarrow> real"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   925
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   926
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   927
  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   928
proof -
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   929
  have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   930
    using assms by (fast intro: affine_borel_measurable borel_measurable_square)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   931
  have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) =
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   932
        (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
   933
    by (simp add: minus_divide_right)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   934
  also have "... \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   935
    using f g by (fast intro: affine_borel_measurable borel_measurable_square f g)
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   936
  finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   937
  show ?thesis
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   938
    apply (simp add: times_eq_sum_squares diff_minus)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   939
    using 1 2 by simp
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   940
qed
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   941
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   942
lemma (in sigma_algebra) borel_measurable_diff[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   943
  fixes f :: "'a \<Rightarrow> real"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   944
  assumes f: "f \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   945
  assumes g: "g \<in> borel_measurable M"
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   946
  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   947
  unfolding diff_minus using assms by fast
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
   948
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   949
lemma (in sigma_algebra) borel_measurable_setsum[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   950
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   951
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   952
  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   953
proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   954
  assume "finite S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   955
  thus ?thesis using assms by induct auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   956
qed simp
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   957
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   958
lemma (in sigma_algebra) borel_measurable_inverse[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   959
  fixes f :: "'a \<Rightarrow> real"
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   960
  assumes "f \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   961
  shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   962
  unfolding borel_measurable_iff_ge unfolding inverse_eq_divide
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   963
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   964
  fix a :: real
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   965
  have *: "{w \<in> space M. a \<le> 1 / f w} =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   966
      ({w \<in> space M. 0 < f w} \<inter> {w \<in> space M. a * f w \<le> 1}) \<union>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   967
      ({w \<in> space M. f w < 0} \<inter> {w \<in> space M. 1 \<le> a * f w}) \<union>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   968
      ({w \<in> space M. f w = 0} \<inter> {w \<in> space M. a \<le> 0})" by (auto simp: le_divide_eq)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   969
  show "{w \<in> space M. a \<le> 1 / f w} \<in> sets M" using assms unfolding *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   970
    by (auto intro!: Int Un)
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   971
qed
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   972
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   973
lemma (in sigma_algebra) borel_measurable_divide[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   974
  fixes f :: "'a \<Rightarrow> real"
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   975
  assumes "f \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   976
  and "g \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   977
  shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
   978
  unfolding field_divide_inverse
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   979
  by (rule borel_measurable_inverse borel_measurable_times assms)+
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   980
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   981
lemma (in sigma_algebra) borel_measurable_max[intro, simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   982
  fixes f g :: "'a \<Rightarrow> real"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   983
  assumes "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   984
  assumes "g \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   985
  shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   986
  unfolding borel_measurable_iff_le
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   987
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   988
  fix a
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   989
  have "{x \<in> space M. max (g x) (f x) \<le> a} =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   990
    {x \<in> space M. g x \<le> a} \<inter> {x \<in> space M. f x \<le> a}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   991
  thus "{x \<in> space M. max (g x) (f x) \<le> a} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   992
    using assms unfolding borel_measurable_iff_le
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   993
    by (auto intro!: Int)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   994
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   995
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   996
lemma (in sigma_algebra) borel_measurable_min[intro, simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   997
  fixes f g :: "'a \<Rightarrow> real"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   998
  assumes "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
   999
  assumes "g \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1000
  shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1001
  unfolding borel_measurable_iff_ge
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1002
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1003
  fix a
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1004
  have "{x \<in> space M. a \<le> min (g x) (f x)} =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1005
    {x \<in> space M. a \<le> g x} \<inter> {x \<in> space M. a \<le> f x}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1006
  thus "{x \<in> space M. a \<le> min (g x) (f x)} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1007
    using assms unfolding borel_measurable_iff_ge
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1008
    by (auto intro!: Int)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1009
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1010
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1011
lemma (in sigma_algebra) borel_measurable_abs[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1012
  assumes "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1013
  shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1014
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1015
  have *: "\<And>x. \<bar>f x\<bar> = max 0 (f x) + max 0 (- f x)" by (simp add: max_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1016
  show ?thesis unfolding * using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1017
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1018
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1019
section "Borel space over the real line with infinity"
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1020
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1021
lemma borel_Real_measurable:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1022
  "A \<in> sets borel \<Longrightarrow> Real -` A \<in> sets borel"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1023
proof (rule borel_measurable_translate)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1024
  fix B :: "pinfreal set" assume "open B"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1025
  then obtain T x where T: "open T" "Real ` (T \<inter> {0..}) = B - {\<omega>}" and
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1026
    x: "\<omega> \<in> B \<Longrightarrow> 0 \<le> x" "\<omega> \<in> B \<Longrightarrow> {Real x <..} \<subseteq> B"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1027
    unfolding open_pinfreal_def by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1028
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1029
  have "Real -` B = Real -` (B - {\<omega>})" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1030
  also have "\<dots> = Real -` (Real ` (T \<inter> {0..}))" using T by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1031
  also have "\<dots> = (if 0 \<in> T then T \<union> {.. 0} else T \<inter> {0..})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1032
    apply (auto simp add: Real_eq_Real image_iff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1033
    apply (rule_tac x="max 0 x" in bexI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1034
    by (auto simp: max_def)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1035
  finally show "Real -` B \<in> sets borel"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1036
    using `open T` by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1037
qed simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1038
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1039
lemma borel_real_measurable:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1040
  "A \<in> sets borel \<Longrightarrow> (real -` A :: pinfreal set) \<in> sets borel"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1041
proof (rule borel_measurable_translate)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1042
  fix B :: "real set" assume "open B"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1043
  { fix x have "0 < real x \<longleftrightarrow> (\<exists>r>0. x = Real r)" by (cases x) auto }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1044
  note Ex_less_real = this
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1045
  have *: "real -` B = (if 0 \<in> B then real -` (B \<inter> {0 <..}) \<union> {0, \<omega>} else real -` (B \<inter> {0 <..}))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1046
    by (force simp: Ex_less_real)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1047
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1048
  have "open (real -` (B \<inter> {0 <..}) :: pinfreal set)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1049
    unfolding open_pinfreal_def using `open B`
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1050
    by (auto intro!: open_Int exI[of _ "B \<inter> {0 <..}"] simp: image_iff Ex_less_real)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1051
  then show "(real -` B :: pinfreal set) \<in> sets borel" unfolding * by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1052
qed simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1053
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1054
lemma (in sigma_algebra) borel_measurable_Real[intro, simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1055
  assumes "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1056
  shows "(\<lambda>x. Real (f x)) \<in> borel_measurable M"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1057
  unfolding in_borel_measurable_borel
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1058
proof safe
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1059
  fix S :: "pinfreal set" assume "S \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1060
  from borel_Real_measurable[OF this]
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1061
  have "(Real \<circ> f) -` S \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1062
    using assms
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1063
    unfolding vimage_compose in_borel_measurable_borel
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1064
    by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1065
  thus "(\<lambda>x. Real (f x)) -` S \<inter> space M \<in> sets M" by (simp add: comp_def)
35748
5f35613d9a65 Equality of integral and infinite sum.
hoelzl
parents: 35704
diff changeset
  1066
qed
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1067
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1068
lemma (in sigma_algebra) borel_measurable_real[intro, simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1069
  fixes f :: "'a \<Rightarrow> pinfreal"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1070
  assumes "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1071
  shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1072
  unfolding in_borel_measurable_borel
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1073
proof safe
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1074
  fix S :: "real set" assume "S \<in> sets borel"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1075
  from borel_real_measurable[OF this]
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1076
  have "(real \<circ> f) -` S \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1077
    using assms
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1078
    unfolding vimage_compose in_borel_measurable_borel
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1079
    by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1080
  thus "(\<lambda>x. real (f x)) -` S \<inter> space M \<in> sets M" by (simp add: comp_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1081
qed
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1082
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1083
lemma (in sigma_algebra) borel_measurable_Real_eq:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1084
  assumes "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1085
  shows "(\<lambda>x. Real (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1086
proof
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1087
  have [simp]: "(\<lambda>x. Real (f x)) -` {\<omega>} \<inter> space M = {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1088
    by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1089
  assume "(\<lambda>x. Real (f x)) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1090
  hence "(\<lambda>x. real (Real (f x))) \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1091
    by (rule borel_measurable_real)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1092
  moreover have "\<And>x. x \<in> space M \<Longrightarrow> real (Real (f x)) = f x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1093
    using assms by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1094
  ultimately show "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1095
    by (simp cong: measurable_cong)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1096
qed auto
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1097
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1098
lemma (in sigma_algebra) borel_measurable_pinfreal_eq_real:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1099
  "f \<in> borel_measurable M \<longleftrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1100
    ((\<lambda>x. real (f x)) \<in> borel_measurable M \<and> f -` {\<omega>} \<inter> space M \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1101
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1102
  assume "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1103
  then show "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f -` {\<omega>} \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1104
    by (auto intro: borel_measurable_vimage borel_measurable_real)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1105
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1106
  assume *: "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f -` {\<omega>} \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1107
  have "f -` {\<omega>} \<inter> space M = {x\<in>space M. f x = \<omega>}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1108
  with * have **: "{x\<in>space M. f x = \<omega>} \<in> sets M" by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1109
  have f: "f = (\<lambda>x. if f x = \<omega> then \<omega> else Real (real (f x)))"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
  1110
    by (simp add: fun_eq_iff Real_real)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1111
  show "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1112
    apply (subst f)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1113
    apply (rule measurable_If)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1114
    using * ** by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1115
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1116
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1117
lemma (in sigma_algebra) less_eq_ge_measurable:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1118
  fixes f :: "'a \<Rightarrow> 'c::linorder"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1119
  shows "{x\<in>space M. a < f x} \<in> sets M \<longleftrightarrow> {x\<in>space M. f x \<le> a} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1120
proof
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1121
  assume "{x\<in>space M. f x \<le> a} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1122
  moreover have "{x\<in>space M. a < f x} = space M - {x\<in>space M. f x \<le> a}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1123
  ultimately show "{x\<in>space M. a < f x} \<in> sets M" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1124
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1125
  assume "{x\<in>space M. a < f x} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1126
  moreover have "{x\<in>space M. f x \<le> a} = space M - {x\<in>space M. a < f x}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1127
  ultimately show "{x\<in>space M. f x \<le> a} \<in> sets M" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1128
qed
35692
f1315bbf1bc9 Moved theorems in Lebesgue to the right places
hoelzl
parents: 35582
diff changeset
  1129
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1130
lemma (in sigma_algebra) greater_eq_le_measurable:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1131
  fixes f :: "'a \<Rightarrow> 'c::linorder"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1132
  shows "{x\<in>space M. f x < a} \<in> sets M \<longleftrightarrow> {x\<in>space M. a \<le> f x} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1133
proof
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1134
  assume "{x\<in>space M. a \<le> f x} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1135
  moreover have "{x\<in>space M. f x < a} = space M - {x\<in>space M. a \<le> f x}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1136
  ultimately show "{x\<in>space M. f x < a} \<in> sets M" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1137
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1138
  assume "{x\<in>space M. f x < a} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1139
  moreover have "{x\<in>space M. a \<le> f x} = space M - {x\<in>space M. f x < a}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1140
  ultimately show "{x\<in>space M. a \<le> f x} \<in> sets M" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1141
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1142
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1143
lemma (in sigma_algebra) less_eq_le_pinfreal_measurable:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1144
  fixes f :: "'a \<Rightarrow> pinfreal"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1145
  shows "(\<forall>a. {x\<in>space M. a < f x} \<in> sets M) \<longleftrightarrow> (\<forall>a. {x\<in>space M. a \<le> f x} \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1146
proof
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1147
  assume a: "\<forall>a. {x\<in>space M. a \<le> f x} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1148
  show "\<forall>a. {x \<in> space M. a < f x} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1149
  proof
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1150
    fix a show "{x \<in> space M. a < f x} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1151
    proof (cases a)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1152
      case (preal r)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1153
      have "{x\<in>space M. a < f x} = (\<Union>i. {x\<in>space M. a + inverse (of_nat (Suc i)) \<le> f x})"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
  1154
      proof safe
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1155
        fix x assume "a < f x" and [simp]: "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1156
        with ex_pinfreal_inverse_of_nat_Suc_less[of "f x - a"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1157
        obtain n where "a + inverse (of_nat (Suc n)) < f x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1158
          by (cases "f x", auto simp: pinfreal_minus_order)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1159
        then have "a + inverse (of_nat (Suc n)) \<le> f x" by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1160
        then show "x \<in> (\<Union>i. {x \<in> space M. a + inverse (of_nat (Suc i)) \<le> f x})"
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
  1161
          by auto
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
  1162
      next
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1163
        fix i x assume [simp]: "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1164
        have "a < a + inverse (of_nat (Suc i))" using preal by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1165
        also assume "a + inverse (of_nat (Suc i)) \<le> f x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1166
        finally show "a < f x" .
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff changeset
  1167
      qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1168
      with a show ?thesis by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1169
    qed simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1170
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1171
next
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1172
  assume a': "\<forall>a. {x \<in> space M. a < f x} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1173
  then have a: "\<forall>a. {x \<in> space M. f x \<le> a} \<in> sets M" unfolding less_eq_ge_measurable .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1174
  show "\<forall>a. {x \<in> space M. a \<le> f x} \<in> sets M" unfolding greater_eq_le_measurable[symmetric]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1175
  proof
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1176
    fix a show "{x \<in> space M. f x < a} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1177
    proof (cases a)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1178
      case (preal r)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1179
      show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1180
      proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1181
        assume "a = 0" then show ?thesis by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1182
      next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1183
        assume "a \<noteq> 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1184
        have "{x\<in>space M. f x < a} = (\<Union>i. {x\<in>space M. f x \<le> a - inverse (of_nat (Suc i))})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1185
        proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1186
          fix x assume "f x < a" and [simp]: "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1187
          with ex_pinfreal_inverse_of_nat_Suc_less[of "a - f x"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1188
          obtain n where "inverse (of_nat (Suc n)) < a - f x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1189
            using preal by (cases "f x") auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1190
          then have "f x \<le> a - inverse (of_nat (Suc n)) "
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1191
            using preal by (cases "f x") (auto split: split_if_asm)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1192
          then show "x \<in> (\<Union>i. {x \<in> space M. f x \<le> a - inverse (of_nat (Suc i))})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1193
            by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1194
        next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1195
          fix i x assume [simp]: "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1196
          assume "f x \<le> a - inverse (of_nat (Suc i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1197
          also have "\<dots> < a" using `a \<noteq> 0` preal by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1198
          finally show "f x < a" .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1199
        qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1200
        with a show ?thesis by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1201
      qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1202
    next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1203
      case infinite
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1204
      have "f -` {\<omega>} \<inter> space M = (\<Inter>n. {x\<in>space M. of_nat n < f x})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1205
      proof (safe, simp_all, safe)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1206
        fix x assume *: "\<forall>n::nat. Real (real n) < f x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1207
        show "f x = \<omega>"    proof (rule ccontr)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1208
          assume "f x \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1209
          with real_arch_lt[of "real (f x)"] obtain n where "f x < of_nat n"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1210
            by (auto simp: pinfreal_noteq_omega_Ex)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1211
          with *[THEN spec, of n] show False by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1212
        qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1213
      qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1214
      with a' have \<omega>: "f -` {\<omega>} \<inter> space M \<in> sets M" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1215
      moreover have "{x \<in> space M. f x < a} = space M - f -` {\<omega>} \<inter> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1216
        using infinite by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1217
      ultimately show ?thesis by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1218
    qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1219
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1220
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1221
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1222
lemma (in sigma_algebra) borel_measurable_pinfreal_iff_greater:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1223
  "(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. a < f x} \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1224
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1225
  fix a assume f: "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1226
  have "{x\<in>space M. a < f x} = f -` {a <..} \<inter> space M" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1227
  with f show "{x\<in>space M. a < f x} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1228
    by (auto intro!: measurable_sets)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1229
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1230
  assume *: "\<forall>a. {x\<in>space M. a < f x} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1231
  hence **: "\<forall>a. {x\<in>space M. f x < a} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1232
    unfolding less_eq_le_pinfreal_measurable
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1233
    unfolding greater_eq_le_measurable .
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1234
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1235
  show "f \<in> borel_measurable M" unfolding borel_measurable_pinfreal_eq_real borel_measurable_iff_greater
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1236
  proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1237
    have "f -` {\<omega>} \<inter> space M = space M - {x\<in>space M. f x < \<omega>}" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1238
    then show \<omega>: "f -` {\<omega>} \<inter> space M \<in> sets M" using ** by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1239
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1240
    fix a
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1241
    have "{w \<in> space M. a < real (f w)} =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1242
      (if 0 \<le> a then {w\<in>space M. Real a < f w} - (f -` {\<omega>} \<inter> space M) else space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1243
    proof (split split_if, safe del: notI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1244
      fix x assume "0 \<le> a"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1245
      { assume "a < real (f x)" then show "Real a < f x" "x \<notin> f -` {\<omega>} \<inter> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1246
          using `0 \<le> a` by (cases "f x", auto) }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1247
      { assume "Real a < f x" "x \<notin> f -` {\<omega>}" then show "a < real (f x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1248
          using `0 \<le> a` by (cases "f x", auto) }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1249
    next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1250
      fix x assume "\<not> 0 \<le> a" then show "a < real (f x)" by (cases "f x") auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1251
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1252
    then show "{w \<in> space M. a < real (f w)} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1253
      using \<omega> * by (auto intro!: Diff)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1254
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1255
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents: 35347
diff changeset
  1256
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1257
lemma (in sigma_algebra) borel_measurable_pinfreal_iff_less:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1258
  "(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. f x < a} \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1259
  using borel_measurable_pinfreal_iff_greater unfolding less_eq_le_pinfreal_measurable greater_eq_le_measurable .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1260
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1261
lemma (in sigma_algebra) borel_measurable_pinfreal_iff_le:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1262
  "(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. f x \<le> a} \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1263
  using borel_measurable_pinfreal_iff_greater unfolding less_eq_ge_measurable .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1264
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1265
lemma (in sigma_algebra) borel_measurable_pinfreal_iff_ge:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37887
diff changeset
  1266
  "(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. a \<le> f x} \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: