src/HOL/Probability/Sigma_Algebra.thy
author hoelzl
Mon Aug 23 19:35:57 2010 +0200 (2010-08-23)
changeset 38656 d5d342611edb
parent 37032 58a0757031dd
child 39090 a2d38b8b693e
permissions -rw-r--r--
Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
paulson@33271
     1
(*  Title:      Sigma_Algebra.thy
paulson@33271
     2
    Author:     Stefan Richter, Markus Wenzel, TU Muenchen
hoelzl@38656
     3
    Plus material from the Hurd/Coble measure theory development,
paulson@33271
     4
    translated by Lawrence Paulson.
paulson@33271
     5
*)
paulson@33271
     6
paulson@33271
     7
header {* Sigma Algebras *}
paulson@33271
     8
hoelzl@38656
     9
theory Sigma_Algebra imports Main Countable FuncSet begin
paulson@33271
    10
paulson@33271
    11
text {* Sigma algebras are an elementary concept in measure
paulson@33271
    12
  theory. To measure --- that is to integrate --- functions, we first have
paulson@33271
    13
  to measure sets. Unfortunately, when dealing with a large universe,
paulson@33271
    14
  it is often not possible to consistently assign a measure to every
paulson@33271
    15
  subset. Therefore it is necessary to define the set of measurable
paulson@33271
    16
  subsets of the universe. A sigma algebra is such a set that has
paulson@33271
    17
  three very natural and desirable properties. *}
paulson@33271
    18
paulson@33271
    19
subsection {* Algebras *}
paulson@33271
    20
hoelzl@38656
    21
record 'a algebra =
hoelzl@38656
    22
  space :: "'a set"
paulson@33271
    23
  sets :: "'a set set"
paulson@33271
    24
paulson@33271
    25
locale algebra =
paulson@33271
    26
  fixes M
paulson@33271
    27
  assumes space_closed: "sets M \<subseteq> Pow (space M)"
paulson@33271
    28
     and  empty_sets [iff]: "{} \<in> sets M"
paulson@33271
    29
     and  compl_sets [intro]: "!!a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
paulson@33271
    30
     and  Un [intro]: "!!a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
paulson@33271
    31
paulson@33271
    32
lemma (in algebra) top [iff]: "space M \<in> sets M"
paulson@33271
    33
  by (metis Diff_empty compl_sets empty_sets)
paulson@33271
    34
paulson@33271
    35
lemma (in algebra) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
paulson@33271
    36
  by (metis PowD contra_subsetD space_closed)
paulson@33271
    37
hoelzl@38656
    38
lemma (in algebra) Int [intro]:
paulson@33271
    39
  assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M"
paulson@33271
    40
proof -
hoelzl@38656
    41
  have "((space M - a) \<union> (space M - b)) \<in> sets M"
paulson@33271
    42
    by (metis a b compl_sets Un)
paulson@33271
    43
  moreover
hoelzl@38656
    44
  have "a \<inter> b = space M - ((space M - a) \<union> (space M - b))"
paulson@33271
    45
    using space_closed a b
paulson@33271
    46
    by blast
paulson@33271
    47
  ultimately show ?thesis
paulson@33271
    48
    by (metis compl_sets)
paulson@33271
    49
qed
paulson@33271
    50
hoelzl@38656
    51
lemma (in algebra) Diff [intro]:
paulson@33271
    52
  assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a - b \<in> sets M"
paulson@33271
    53
proof -
paulson@33271
    54
  have "(a \<inter> (space M - b)) \<in> sets M"
paulson@33271
    55
    by (metis a b compl_sets Int)
paulson@33271
    56
  moreover
paulson@33271
    57
  have "a - b = (a \<inter> (space M - b))"
paulson@33271
    58
    by (metis Int_Diff Int_absorb1 Int_commute a sets_into_space)
paulson@33271
    59
  ultimately show ?thesis
paulson@33271
    60
    by metis
paulson@33271
    61
qed
paulson@33271
    62
hoelzl@38656
    63
lemma (in algebra) finite_union [intro]:
paulson@33271
    64
  "finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M"
hoelzl@38656
    65
  by (induct set: finite) (auto simp add: Un)
paulson@33271
    66
hoelzl@38656
    67
lemma algebra_iff_Int:
hoelzl@38656
    68
     "algebra M \<longleftrightarrow>
hoelzl@38656
    69
       sets M \<subseteq> Pow (space M) & {} \<in> sets M &
hoelzl@38656
    70
       (\<forall>a \<in> sets M. space M - a \<in> sets M) &
hoelzl@38656
    71
       (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
hoelzl@38656
    72
proof (auto simp add: algebra.Int, auto simp add: algebra_def)
hoelzl@38656
    73
  fix a b
hoelzl@38656
    74
  assume ab: "sets M \<subseteq> Pow (space M)"
hoelzl@38656
    75
             "\<forall>a\<in>sets M. space M - a \<in> sets M"
hoelzl@38656
    76
             "\<forall>a\<in>sets M. \<forall>b\<in>sets M. a \<inter> b \<in> sets M"
hoelzl@38656
    77
             "a \<in> sets M" "b \<in> sets M"
hoelzl@38656
    78
  hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
hoelzl@38656
    79
    by blast
hoelzl@38656
    80
  also have "... \<in> sets M"
hoelzl@38656
    81
    by (metis ab)
hoelzl@38656
    82
  finally show "a \<union> b \<in> sets M" .
hoelzl@38656
    83
qed
hoelzl@38656
    84
hoelzl@38656
    85
lemma (in algebra) insert_in_sets:
hoelzl@38656
    86
  assumes "{x} \<in> sets M" "A \<in> sets M" shows "insert x A \<in> sets M"
hoelzl@38656
    87
proof -
hoelzl@38656
    88
  have "{x} \<union> A \<in> sets M" using assms by (rule Un)
hoelzl@38656
    89
  thus ?thesis by auto
hoelzl@38656
    90
qed
hoelzl@38656
    91
hoelzl@38656
    92
lemma (in algebra) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
hoelzl@38656
    93
  by (metis Int_absorb1 sets_into_space)
hoelzl@38656
    94
hoelzl@38656
    95
lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
hoelzl@38656
    96
  by (metis Int_absorb2 sets_into_space)
hoelzl@38656
    97
hoelzl@38656
    98
lemma (in algebra) restricted_algebra:
hoelzl@38656
    99
  assumes "S \<in> sets M"
hoelzl@38656
   100
  shows "algebra (M\<lparr> space := S, sets := (\<lambda>A. S \<inter> A) ` sets M \<rparr>)"
hoelzl@38656
   101
    (is "algebra ?r")
hoelzl@38656
   102
  using assms by unfold_locales auto
paulson@33271
   103
paulson@33271
   104
subsection {* Sigma Algebras *}
paulson@33271
   105
paulson@33271
   106
locale sigma_algebra = algebra +
hoelzl@38656
   107
  assumes countable_nat_UN [intro]:
paulson@33271
   108
         "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
paulson@33271
   109
hoelzl@38656
   110
lemma countable_UN_eq:
hoelzl@38656
   111
  fixes A :: "'i::countable \<Rightarrow> 'a set"
hoelzl@38656
   112
  shows "(range A \<subseteq> sets M \<longrightarrow> (\<Union>i. A i) \<in> sets M) \<longleftrightarrow>
hoelzl@38656
   113
    (range (A \<circ> from_nat) \<subseteq> sets M \<longrightarrow> (\<Union>i. (A \<circ> from_nat) i) \<in> sets M)"
hoelzl@38656
   114
proof -
hoelzl@38656
   115
  let ?A' = "A \<circ> from_nat"
hoelzl@38656
   116
  have *: "(\<Union>i. ?A' i) = (\<Union>i. A i)" (is "?l = ?r")
hoelzl@38656
   117
  proof safe
hoelzl@38656
   118
    fix x i assume "x \<in> A i" thus "x \<in> ?l"
hoelzl@38656
   119
      by (auto intro!: exI[of _ "to_nat i"])
hoelzl@38656
   120
  next
hoelzl@38656
   121
    fix x i assume "x \<in> ?A' i" thus "x \<in> ?r"
hoelzl@38656
   122
      by (auto intro!: exI[of _ "from_nat i"])
hoelzl@38656
   123
  qed
hoelzl@38656
   124
  have **: "range ?A' = range A"
hoelzl@38656
   125
    using surj_range[OF surj_from_nat]
hoelzl@38656
   126
    by (auto simp: image_compose intro!: imageI)
hoelzl@38656
   127
  show ?thesis unfolding * ** ..
hoelzl@38656
   128
qed
hoelzl@38656
   129
hoelzl@38656
   130
lemma (in sigma_algebra) countable_UN[intro]:
hoelzl@38656
   131
  fixes A :: "'i::countable \<Rightarrow> 'a set"
hoelzl@38656
   132
  assumes "A`X \<subseteq> sets M"
hoelzl@38656
   133
  shows  "(\<Union>x\<in>X. A x) \<in> sets M"
hoelzl@38656
   134
proof -
hoelzl@38656
   135
  let "?A i" = "if i \<in> X then A i else {}"
hoelzl@38656
   136
  from assms have "range ?A \<subseteq> sets M" by auto
hoelzl@38656
   137
  with countable_nat_UN[of "?A \<circ> from_nat"] countable_UN_eq[of ?A M]
hoelzl@38656
   138
  have "(\<Union>x. ?A x) \<in> sets M" by auto
hoelzl@38656
   139
  moreover have "(\<Union>x. ?A x) = (\<Union>x\<in>X. A x)" by (auto split: split_if_asm)
hoelzl@38656
   140
  ultimately show ?thesis by simp
hoelzl@38656
   141
qed
hoelzl@38656
   142
hoelzl@38656
   143
lemma (in sigma_algebra) finite_UN:
hoelzl@38656
   144
  assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
hoelzl@38656
   145
  shows "(\<Union>i\<in>I. A i) \<in> sets M"
hoelzl@38656
   146
  using assms by induct auto
hoelzl@38656
   147
paulson@33533
   148
lemma (in sigma_algebra) countable_INT [intro]:
hoelzl@38656
   149
  fixes A :: "'i::countable \<Rightarrow> 'a set"
hoelzl@38656
   150
  assumes A: "A`X \<subseteq> sets M" "X \<noteq> {}"
hoelzl@38656
   151
  shows "(\<Inter>i\<in>X. A i) \<in> sets M"
paulson@33271
   152
proof -
hoelzl@38656
   153
  from A have "\<forall>i\<in>X. A i \<in> sets M" by fast
hoelzl@38656
   154
  hence "space M - (\<Union>i\<in>X. space M - A i) \<in> sets M" by blast
paulson@33271
   155
  moreover
hoelzl@38656
   156
  have "(\<Inter>i\<in>X. A i) = space M - (\<Union>i\<in>X. space M - A i)" using space_closed A
paulson@33271
   157
    by blast
paulson@33271
   158
  ultimately show ?thesis by metis
paulson@33271
   159
qed
paulson@33271
   160
hoelzl@38656
   161
lemma (in sigma_algebra) finite_INT:
hoelzl@38656
   162
  assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
hoelzl@38656
   163
  shows "(\<Inter>i\<in>I. A i) \<in> sets M"
hoelzl@38656
   164
  using assms by (induct rule: finite_ne_induct) auto
paulson@33271
   165
paulson@33271
   166
lemma algebra_Pow:
hoelzl@38656
   167
     "algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
hoelzl@38656
   168
  by (auto simp add: algebra_def)
paulson@33271
   169
paulson@33271
   170
lemma sigma_algebra_Pow:
hoelzl@38656
   171
     "sigma_algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
hoelzl@38656
   172
  by (auto simp add: sigma_algebra_def sigma_algebra_axioms_def algebra_Pow)
hoelzl@38656
   173
hoelzl@38656
   174
lemma sigma_algebra_iff:
hoelzl@38656
   175
     "sigma_algebra M \<longleftrightarrow>
hoelzl@38656
   176
      algebra M \<and> (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
hoelzl@38656
   177
  by (simp add: sigma_algebra_def sigma_algebra_axioms_def)
paulson@33271
   178
paulson@33271
   179
subsection {* Binary Unions *}
paulson@33271
   180
paulson@33271
   181
definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
paulson@33271
   182
  where "binary a b =  (\<lambda>\<^isup>x. b)(0 := a)"
paulson@33271
   183
hoelzl@38656
   184
lemma range_binary_eq: "range(binary a b) = {a,b}"
hoelzl@38656
   185
  by (auto simp add: binary_def)
paulson@33271
   186
hoelzl@38656
   187
lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
hoelzl@38656
   188
  by (simp add: UNION_eq_Union_image range_binary_eq)
paulson@33271
   189
hoelzl@38656
   190
lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
hoelzl@38656
   191
  by (simp add: INTER_eq_Inter_image range_binary_eq)
paulson@33271
   192
paulson@33271
   193
lemma sigma_algebra_iff2:
paulson@33271
   194
     "sigma_algebra M \<longleftrightarrow>
hoelzl@38656
   195
       sets M \<subseteq> Pow (space M) \<and>
hoelzl@38656
   196
       {} \<in> sets M \<and> (\<forall>s \<in> sets M. space M - s \<in> sets M) \<and>
paulson@33271
   197
       (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
hoelzl@38656
   198
  by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
hoelzl@38656
   199
         algebra_def Un_range_binary)
paulson@33271
   200
paulson@33271
   201
subsection {* Initial Sigma Algebra *}
paulson@33271
   202
paulson@33271
   203
text {*Sigma algebras can naturally be created as the closure of any set of
paulson@33271
   204
  sets with regard to the properties just postulated.  *}
paulson@33271
   205
paulson@33271
   206
inductive_set
paulson@33271
   207
  sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
paulson@33271
   208
  for sp :: "'a set" and A :: "'a set set"
paulson@33271
   209
  where
paulson@33271
   210
    Basic: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
paulson@33271
   211
  | Empty: "{} \<in> sigma_sets sp A"
paulson@33271
   212
  | Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp - a \<in> sigma_sets sp A"
paulson@33271
   213
  | Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A"
paulson@33271
   214
paulson@33271
   215
paulson@33271
   216
definition
paulson@33271
   217
  sigma  where
paulson@33271
   218
  "sigma sp A = (| space = sp, sets = sigma_sets sp A |)"
paulson@33271
   219
hoelzl@38656
   220
lemma sets_sigma: "sets (sigma A B) = sigma_sets A B"
hoelzl@38656
   221
  unfolding sigma_def by simp
paulson@33271
   222
paulson@33271
   223
lemma space_sigma [simp]: "space (sigma X B) = X"
hoelzl@38656
   224
  by (simp add: sigma_def)
paulson@33271
   225
paulson@33271
   226
lemma sigma_sets_top: "sp \<in> sigma_sets sp A"
paulson@33271
   227
  by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)
paulson@33271
   228
paulson@33271
   229
lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
hoelzl@38656
   230
  by (erule sigma_sets.induct, auto)
paulson@33271
   231
hoelzl@38656
   232
lemma sigma_sets_Un:
paulson@33271
   233
  "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
hoelzl@38656
   234
apply (simp add: Un_range_binary range_binary_eq)
huffman@37032
   235
apply (rule Union, simp add: binary_def COMBK_def fun_upd_apply)
paulson@33271
   236
done
paulson@33271
   237
paulson@33271
   238
lemma sigma_sets_Inter:
paulson@33271
   239
  assumes Asb: "A \<subseteq> Pow sp"
paulson@33271
   240
  shows "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Inter>i. a i) \<in> sigma_sets sp A"
paulson@33271
   241
proof -
paulson@33271
   242
  assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A"
hoelzl@38656
   243
  hence "\<And>i::nat. sp-(a i) \<in> sigma_sets sp A"
paulson@33271
   244
    by (rule sigma_sets.Compl)
hoelzl@38656
   245
  hence "(\<Union>i. sp-(a i)) \<in> sigma_sets sp A"
paulson@33271
   246
    by (rule sigma_sets.Union)
hoelzl@38656
   247
  hence "sp-(\<Union>i. sp-(a i)) \<in> sigma_sets sp A"
paulson@33271
   248
    by (rule sigma_sets.Compl)
hoelzl@38656
   249
  also have "sp-(\<Union>i. sp-(a i)) = sp Int (\<Inter>i. a i)"
paulson@33271
   250
    by auto
paulson@33271
   251
  also have "... = (\<Inter>i. a i)" using ai
hoelzl@38656
   252
    by (blast dest: sigma_sets_into_sp [OF Asb])
hoelzl@38656
   253
  finally show ?thesis .
paulson@33271
   254
qed
paulson@33271
   255
paulson@33271
   256
lemma sigma_sets_INTER:
hoelzl@38656
   257
  assumes Asb: "A \<subseteq> Pow sp"
paulson@33271
   258
      and ai: "\<And>i::nat. i \<in> S \<Longrightarrow> a i \<in> sigma_sets sp A" and non: "S \<noteq> {}"
paulson@33271
   259
  shows "(\<Inter>i\<in>S. a i) \<in> sigma_sets sp A"
paulson@33271
   260
proof -
paulson@33271
   261
  from ai have "\<And>i. (if i\<in>S then a i else sp) \<in> sigma_sets sp A"
paulson@33271
   262
    by (simp add: sigma_sets.intros sigma_sets_top)
paulson@33271
   263
  hence "(\<Inter>i. (if i\<in>S then a i else sp)) \<in> sigma_sets sp A"
paulson@33271
   264
    by (rule sigma_sets_Inter [OF Asb])
paulson@33271
   265
  also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>S. a i)"
paulson@33271
   266
    by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+
paulson@33271
   267
  finally show ?thesis .
paulson@33271
   268
qed
paulson@33271
   269
paulson@33271
   270
lemma (in sigma_algebra) sigma_sets_subset:
hoelzl@38656
   271
  assumes a: "a \<subseteq> sets M"
paulson@33271
   272
  shows "sigma_sets (space M) a \<subseteq> sets M"
paulson@33271
   273
proof
paulson@33271
   274
  fix x
paulson@33271
   275
  assume "x \<in> sigma_sets (space M) a"
paulson@33271
   276
  from this show "x \<in> sets M"
hoelzl@38656
   277
    by (induct rule: sigma_sets.induct, auto) (metis a subsetD)
paulson@33271
   278
qed
paulson@33271
   279
paulson@33271
   280
lemma (in sigma_algebra) sigma_sets_eq:
paulson@33271
   281
     "sigma_sets (space M) (sets M) = sets M"
paulson@33271
   282
proof
paulson@33271
   283
  show "sets M \<subseteq> sigma_sets (space M) (sets M)"
huffman@37032
   284
    by (metis Set.subsetI sigma_sets.Basic)
paulson@33271
   285
  next
paulson@33271
   286
  show "sigma_sets (space M) (sets M) \<subseteq> sets M"
paulson@33271
   287
    by (metis sigma_sets_subset subset_refl)
paulson@33271
   288
qed
paulson@33271
   289
paulson@33271
   290
lemma sigma_algebra_sigma_sets:
paulson@33271
   291
     "a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M"
paulson@33271
   292
  apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def
hoelzl@38656
   293
      algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un)
paulson@33271
   294
  apply (blast dest: sigma_sets_into_sp)
huffman@37032
   295
  apply (rule sigma_sets.Union, fast)
paulson@33271
   296
  done
paulson@33271
   297
paulson@33271
   298
lemma sigma_algebra_sigma:
paulson@33271
   299
     "a \<subseteq> Pow X \<Longrightarrow> sigma_algebra (sigma X a)"
hoelzl@38656
   300
  apply (rule sigma_algebra_sigma_sets)
hoelzl@38656
   301
  apply (auto simp add: sigma_def)
paulson@33271
   302
  done
paulson@33271
   303
paulson@33271
   304
lemma (in sigma_algebra) sigma_subset:
paulson@33271
   305
     "a \<subseteq> sets M ==> sets (sigma (space M) a) \<subseteq> (sets M)"
paulson@33271
   306
  by (simp add: sigma_def sigma_sets_subset)
paulson@33271
   307
hoelzl@38656
   308
lemma (in sigma_algebra) restriction_in_sets:
hoelzl@38656
   309
  fixes A :: "nat \<Rightarrow> 'a set"
hoelzl@38656
   310
  assumes "S \<in> sets M"
hoelzl@38656
   311
  and *: "range A \<subseteq> (\<lambda>A. S \<inter> A) ` sets M" (is "_ \<subseteq> ?r")
hoelzl@38656
   312
  shows "range A \<subseteq> sets M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` sets M"
hoelzl@38656
   313
proof -
hoelzl@38656
   314
  { fix i have "A i \<in> ?r" using * by auto
hoelzl@38656
   315
    hence "\<exists>B. A i = B \<inter> S \<and> B \<in> sets M" by auto
hoelzl@38656
   316
    hence "A i \<subseteq> S" "A i \<in> sets M" using `S \<in> sets M` by auto }
hoelzl@38656
   317
  thus "range A \<subseteq> sets M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` sets M"
hoelzl@38656
   318
    by (auto intro!: image_eqI[of _ _ "(\<Union>i. A i)"])
hoelzl@38656
   319
qed
hoelzl@38656
   320
hoelzl@38656
   321
lemma (in sigma_algebra) restricted_sigma_algebra:
hoelzl@38656
   322
  assumes "S \<in> sets M"
hoelzl@38656
   323
  shows "sigma_algebra (M\<lparr> space := S, sets := (\<lambda>A. S \<inter> A) ` sets M \<rparr>)"
hoelzl@38656
   324
    (is "sigma_algebra ?r")
hoelzl@38656
   325
  unfolding sigma_algebra_def sigma_algebra_axioms_def
hoelzl@38656
   326
proof safe
hoelzl@38656
   327
  show "algebra ?r" using restricted_algebra[OF assms] .
hoelzl@38656
   328
next
hoelzl@38656
   329
  fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets ?r"
hoelzl@38656
   330
  from restriction_in_sets[OF assms this[simplified]]
hoelzl@38656
   331
  show "(\<Union>i. A i) \<in> sets ?r" by simp
hoelzl@38656
   332
qed
hoelzl@38656
   333
hoelzl@38656
   334
section {* Measurable functions *}
hoelzl@38656
   335
hoelzl@38656
   336
definition
hoelzl@38656
   337
  "measurable A B = {f \<in> space A -> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
hoelzl@38656
   338
hoelzl@38656
   339
lemma (in sigma_algebra) measurable_sigma:
hoelzl@38656
   340
  assumes B: "B \<subseteq> Pow X"
hoelzl@38656
   341
      and f: "f \<in> space M -> X"
hoelzl@38656
   342
      and ba: "\<And>y. y \<in> B \<Longrightarrow> (f -` y) \<inter> space M \<in> sets M"
hoelzl@38656
   343
  shows "f \<in> measurable M (sigma X B)"
hoelzl@38656
   344
proof -
hoelzl@38656
   345
  have "sigma_sets X B \<subseteq> {y . (f -` y) \<inter> space M \<in> sets M & y \<subseteq> X}"
hoelzl@38656
   346
    proof clarify
hoelzl@38656
   347
      fix x
hoelzl@38656
   348
      assume "x \<in> sigma_sets X B"
hoelzl@38656
   349
      thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> X"
hoelzl@38656
   350
        proof induct
hoelzl@38656
   351
          case (Basic a)
hoelzl@38656
   352
          thus ?case
hoelzl@38656
   353
            by (auto simp add: ba) (metis B subsetD PowD)
hoelzl@38656
   354
        next
hoelzl@38656
   355
          case Empty
hoelzl@38656
   356
          thus ?case
hoelzl@38656
   357
            by auto
hoelzl@38656
   358
        next
hoelzl@38656
   359
          case (Compl a)
hoelzl@38656
   360
          have [simp]: "f -` X \<inter> space M = space M"
hoelzl@38656
   361
            by (auto simp add: funcset_mem [OF f])
hoelzl@38656
   362
          thus ?case
hoelzl@38656
   363
            by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
hoelzl@38656
   364
        next
hoelzl@38656
   365
          case (Union a)
hoelzl@38656
   366
          thus ?case
hoelzl@38656
   367
            by (simp add: vimage_UN, simp only: UN_extend_simps(4))
hoelzl@38656
   368
               (blast intro: countable_UN)
hoelzl@38656
   369
        qed
hoelzl@38656
   370
    qed
hoelzl@38656
   371
  thus ?thesis
hoelzl@38656
   372
    by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f)
hoelzl@38656
   373
       (auto simp add: sigma_def)
hoelzl@38656
   374
qed
hoelzl@38656
   375
hoelzl@38656
   376
lemma measurable_cong:
hoelzl@38656
   377
  assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
hoelzl@38656
   378
  shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'"
hoelzl@38656
   379
  unfolding measurable_def using assms
hoelzl@38656
   380
  by (simp cong: vimage_inter_cong Pi_cong)
hoelzl@38656
   381
hoelzl@38656
   382
lemma measurable_space:
hoelzl@38656
   383
  "f \<in> measurable M A \<Longrightarrow> x \<in> space M \<Longrightarrow> f x \<in> space A"
hoelzl@38656
   384
   unfolding measurable_def by auto
hoelzl@38656
   385
hoelzl@38656
   386
lemma measurable_sets:
hoelzl@38656
   387
  "f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
hoelzl@38656
   388
   unfolding measurable_def by auto
hoelzl@38656
   389
hoelzl@38656
   390
lemma (in sigma_algebra) measurable_subset:
hoelzl@38656
   391
     "(\<And>S. S \<in> sets A \<Longrightarrow> S \<subseteq> space A) \<Longrightarrow> measurable M A \<subseteq> measurable M (sigma (space A) (sets A))"
hoelzl@38656
   392
  by (auto intro: measurable_sigma measurable_sets measurable_space)
hoelzl@38656
   393
hoelzl@38656
   394
lemma measurable_eqI:
hoelzl@38656
   395
     "\<lbrakk> space m1 = space m1' ; space m2 = space m2' ;
hoelzl@38656
   396
        sets m1 = sets m1' ; sets m2 = sets m2' \<rbrakk>
hoelzl@38656
   397
      \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
hoelzl@38656
   398
  by (simp add: measurable_def sigma_algebra_iff2)
hoelzl@38656
   399
hoelzl@38656
   400
lemma (in sigma_algebra) measurable_const[intro, simp]:
hoelzl@38656
   401
  assumes "c \<in> space M'"
hoelzl@38656
   402
  shows "(\<lambda>x. c) \<in> measurable M M'"
hoelzl@38656
   403
  using assms by (auto simp add: measurable_def)
hoelzl@38656
   404
hoelzl@38656
   405
lemma (in sigma_algebra) measurable_If:
hoelzl@38656
   406
  assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
hoelzl@38656
   407
  assumes P: "{x\<in>space M. P x} \<in> sets M"
hoelzl@38656
   408
  shows "(\<lambda>x. if P x then f x else g x) \<in> measurable M M'"
hoelzl@38656
   409
  unfolding measurable_def
hoelzl@38656
   410
proof safe
hoelzl@38656
   411
  fix x assume "x \<in> space M"
hoelzl@38656
   412
  thus "(if P x then f x else g x) \<in> space M'"
hoelzl@38656
   413
    using measure unfolding measurable_def by auto
hoelzl@38656
   414
next
hoelzl@38656
   415
  fix A assume "A \<in> sets M'"
hoelzl@38656
   416
  hence *: "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M =
hoelzl@38656
   417
    ((f -` A \<inter> space M) \<inter> {x\<in>space M. P x}) \<union>
hoelzl@38656
   418
    ((g -` A \<inter> space M) \<inter> (space M - {x\<in>space M. P x}))"
hoelzl@38656
   419
    using measure unfolding measurable_def by (auto split: split_if_asm)
hoelzl@38656
   420
  show "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M \<in> sets M"
hoelzl@38656
   421
    using `A \<in> sets M'` measure P unfolding * measurable_def
hoelzl@38656
   422
    by (auto intro!: Un)
hoelzl@38656
   423
qed
hoelzl@38656
   424
hoelzl@38656
   425
lemma (in sigma_algebra) measurable_If_set:
hoelzl@38656
   426
  assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
hoelzl@38656
   427
  assumes P: "A \<in> sets M"
hoelzl@38656
   428
  shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> measurable M M'"
hoelzl@38656
   429
proof (rule measurable_If[OF measure])
hoelzl@38656
   430
  have "{x \<in> space M. x \<in> A} = A" using `A \<in> sets M` sets_into_space by auto
hoelzl@38656
   431
  thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<in> sets M` by auto
hoelzl@38656
   432
qed
hoelzl@38656
   433
hoelzl@38656
   434
lemma (in algebra) measurable_ident[intro, simp]: "id \<in> measurable M M"
hoelzl@38656
   435
  by (auto simp add: measurable_def)
hoelzl@38656
   436
hoelzl@38656
   437
lemma measurable_comp[intro]:
hoelzl@38656
   438
  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
hoelzl@38656
   439
  shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
hoelzl@38656
   440
  apply (auto simp add: measurable_def vimage_compose)
hoelzl@38656
   441
  apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
hoelzl@38656
   442
  apply force+
hoelzl@38656
   443
  done
hoelzl@38656
   444
hoelzl@38656
   445
lemma measurable_strong:
hoelzl@38656
   446
  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
hoelzl@38656
   447
  assumes f: "f \<in> measurable a b" and g: "g \<in> (space b -> space c)"
hoelzl@38656
   448
      and a: "sigma_algebra a" and b: "sigma_algebra b" and c: "sigma_algebra c"
hoelzl@38656
   449
      and t: "f ` (space a) \<subseteq> t"
hoelzl@38656
   450
      and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g -` s) \<inter> t \<in> sets b"
hoelzl@38656
   451
  shows "(g o f) \<in> measurable a c"
hoelzl@38656
   452
proof -
hoelzl@38656
   453
  have fab: "f \<in> (space a -> space b)"
hoelzl@38656
   454
   and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
hoelzl@38656
   455
     by (auto simp add: measurable_def)
hoelzl@38656
   456
  have eq: "f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
hoelzl@38656
   457
    by force
hoelzl@38656
   458
  show ?thesis
hoelzl@38656
   459
    apply (auto simp add: measurable_def vimage_compose a c)
hoelzl@38656
   460
    apply (metis funcset_mem fab g)
hoelzl@38656
   461
    apply (subst eq, metis ba cb)
hoelzl@38656
   462
    done
hoelzl@38656
   463
qed
hoelzl@38656
   464
hoelzl@38656
   465
lemma measurable_mono1:
hoelzl@38656
   466
     "a \<subseteq> b \<Longrightarrow> sigma_algebra \<lparr>space = X, sets = b\<rparr>
hoelzl@38656
   467
      \<Longrightarrow> measurable \<lparr>space = X, sets = a\<rparr> c \<subseteq> measurable \<lparr>space = X, sets = b\<rparr> c"
hoelzl@38656
   468
  by (auto simp add: measurable_def)
hoelzl@38656
   469
hoelzl@38656
   470
lemma measurable_up_sigma:
hoelzl@38656
   471
  "measurable A M \<subseteq> measurable (sigma (space A) (sets A)) M"
hoelzl@38656
   472
  unfolding measurable_def
hoelzl@38656
   473
  by (auto simp: sigma_def intro: sigma_sets.Basic)
hoelzl@38656
   474
hoelzl@38656
   475
lemma (in sigma_algebra) measurable_range_reduce:
hoelzl@38656
   476
   "\<lbrakk> f \<in> measurable M \<lparr>space = s, sets = Pow s\<rparr> ; s \<noteq> {} \<rbrakk>
hoelzl@38656
   477
    \<Longrightarrow> f \<in> measurable M \<lparr>space = s \<inter> (f ` space M), sets = Pow (s \<inter> (f ` space M))\<rparr>"
hoelzl@38656
   478
  by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast
hoelzl@38656
   479
hoelzl@38656
   480
lemma (in sigma_algebra) measurable_Pow_to_Pow:
hoelzl@38656
   481
   "(sets M = Pow (space M)) \<Longrightarrow> f \<in> measurable M \<lparr>space = UNIV, sets = Pow UNIV\<rparr>"
hoelzl@38656
   482
  by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def)
hoelzl@38656
   483
hoelzl@38656
   484
lemma (in sigma_algebra) measurable_Pow_to_Pow_image:
hoelzl@38656
   485
   "sets M = Pow (space M)
hoelzl@38656
   486
    \<Longrightarrow> f \<in> measurable M \<lparr>space = f ` space M, sets = Pow (f ` space M)\<rparr>"
hoelzl@38656
   487
  by (simp add: measurable_def sigma_algebra_Pow) intro_locales
hoelzl@38656
   488
hoelzl@38656
   489
lemma (in sigma_algebra) sigma_algebra_preimages:
hoelzl@38656
   490
  fixes f :: "'x \<Rightarrow> 'a"
hoelzl@38656
   491
  assumes "f \<in> A \<rightarrow> space M"
hoelzl@38656
   492
  shows "sigma_algebra \<lparr> space = A, sets = (\<lambda>M. f -` M \<inter> A) ` sets M \<rparr>"
hoelzl@38656
   493
    (is "sigma_algebra \<lparr> space = _, sets = ?F ` sets M \<rparr>")
hoelzl@38656
   494
proof (simp add: sigma_algebra_iff2, safe)
hoelzl@38656
   495
  show "{} \<in> ?F ` sets M" by blast
hoelzl@38656
   496
next
hoelzl@38656
   497
  fix S assume "S \<in> sets M"
hoelzl@38656
   498
  moreover have "A - ?F S = ?F (space M - S)"
hoelzl@38656
   499
    using assms by auto
hoelzl@38656
   500
  ultimately show "A - ?F S \<in> ?F ` sets M"
hoelzl@38656
   501
    by blast
hoelzl@38656
   502
next
hoelzl@38656
   503
  fix S :: "nat \<Rightarrow> 'x set" assume *: "range S \<subseteq> ?F ` sets M"
hoelzl@38656
   504
  have "\<forall>i. \<exists>b. b \<in> sets M \<and> S i = ?F b"
hoelzl@38656
   505
  proof safe
hoelzl@38656
   506
    fix i
hoelzl@38656
   507
    have "S i \<in> ?F ` sets M" using * by auto
hoelzl@38656
   508
    then show "\<exists>b. b \<in> sets M \<and> S i = ?F b" by auto
hoelzl@38656
   509
  qed
hoelzl@38656
   510
  from choice[OF this] obtain b where b: "range b \<subseteq> sets M" "\<And>i. S i = ?F (b i)"
hoelzl@38656
   511
    by auto
hoelzl@38656
   512
  then have "(\<Union>i. S i) = ?F (\<Union>i. b i)" by auto
hoelzl@38656
   513
  then show "(\<Union>i. S i) \<in> ?F ` sets M" using b(1) by blast
hoelzl@38656
   514
qed
hoelzl@38656
   515
hoelzl@38656
   516
section "Disjoint families"
hoelzl@38656
   517
hoelzl@38656
   518
definition
hoelzl@38656
   519
  disjoint_family_on  where
hoelzl@38656
   520
  "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
hoelzl@38656
   521
hoelzl@38656
   522
abbreviation
hoelzl@38656
   523
  "disjoint_family A \<equiv> disjoint_family_on A UNIV"
hoelzl@38656
   524
hoelzl@38656
   525
lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
hoelzl@38656
   526
  by blast
hoelzl@38656
   527
hoelzl@38656
   528
lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
hoelzl@38656
   529
  by blast
hoelzl@38656
   530
hoelzl@38656
   531
lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
hoelzl@38656
   532
  by blast
hoelzl@38656
   533
hoelzl@38656
   534
lemma disjoint_family_subset:
hoelzl@38656
   535
     "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
hoelzl@38656
   536
  by (force simp add: disjoint_family_on_def)
hoelzl@38656
   537
hoelzl@38656
   538
lemma disjoint_family_on_mono:
hoelzl@38656
   539
  "A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A"
hoelzl@38656
   540
  unfolding disjoint_family_on_def by auto
hoelzl@38656
   541
hoelzl@38656
   542
lemma disjoint_family_Suc:
hoelzl@38656
   543
  assumes Suc: "!!n. A n \<subseteq> A (Suc n)"
hoelzl@38656
   544
  shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
hoelzl@38656
   545
proof -
hoelzl@38656
   546
  {
hoelzl@38656
   547
    fix m
hoelzl@38656
   548
    have "!!n. A n \<subseteq> A (m+n)"
hoelzl@38656
   549
    proof (induct m)
hoelzl@38656
   550
      case 0 show ?case by simp
hoelzl@38656
   551
    next
hoelzl@38656
   552
      case (Suc m) thus ?case
hoelzl@38656
   553
        by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
hoelzl@38656
   554
    qed
hoelzl@38656
   555
  }
hoelzl@38656
   556
  hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
hoelzl@38656
   557
    by (metis add_commute le_add_diff_inverse nat_less_le)
hoelzl@38656
   558
  thus ?thesis
hoelzl@38656
   559
    by (auto simp add: disjoint_family_on_def)
hoelzl@38656
   560
      (metis insert_absorb insert_subset le_SucE le_antisym not_leE)
hoelzl@38656
   561
qed
hoelzl@38656
   562
hoelzl@38656
   563
definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
hoelzl@38656
   564
  where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
hoelzl@38656
   565
hoelzl@38656
   566
lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
hoelzl@38656
   567
proof (induct n)
hoelzl@38656
   568
  case 0 show ?case by simp
hoelzl@38656
   569
next
hoelzl@38656
   570
  case (Suc n)
hoelzl@38656
   571
  thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
hoelzl@38656
   572
qed
hoelzl@38656
   573
hoelzl@38656
   574
lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
hoelzl@38656
   575
  apply (rule UN_finite2_eq [where k=0])
hoelzl@38656
   576
  apply (simp add: finite_UN_disjointed_eq)
hoelzl@38656
   577
  done
hoelzl@38656
   578
hoelzl@38656
   579
lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
hoelzl@38656
   580
  by (auto simp add: disjointed_def)
hoelzl@38656
   581
hoelzl@38656
   582
lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
hoelzl@38656
   583
  by (simp add: disjoint_family_on_def)
hoelzl@38656
   584
     (metis neq_iff Int_commute less_disjoint_disjointed)
hoelzl@38656
   585
hoelzl@38656
   586
lemma disjointed_subset: "disjointed A n \<subseteq> A n"
hoelzl@38656
   587
  by (auto simp add: disjointed_def)
hoelzl@38656
   588
hoelzl@38656
   589
lemma (in algebra) UNION_in_sets:
hoelzl@38656
   590
  fixes A:: "nat \<Rightarrow> 'a set"
hoelzl@38656
   591
  assumes A: "range A \<subseteq> sets M "
hoelzl@38656
   592
  shows  "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
hoelzl@38656
   593
proof (induct n)
hoelzl@38656
   594
  case 0 show ?case by simp
hoelzl@38656
   595
next
hoelzl@38656
   596
  case (Suc n)
hoelzl@38656
   597
  thus ?case
hoelzl@38656
   598
    by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
hoelzl@38656
   599
qed
hoelzl@38656
   600
hoelzl@38656
   601
lemma (in algebra) range_disjointed_sets:
hoelzl@38656
   602
  assumes A: "range A \<subseteq> sets M "
hoelzl@38656
   603
  shows  "range (disjointed A) \<subseteq> sets M"
hoelzl@38656
   604
proof (auto simp add: disjointed_def)
hoelzl@38656
   605
  fix n
hoelzl@38656
   606
  show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets
hoelzl@38656
   607
    by (metis A Diff UNIV_I image_subset_iff)
hoelzl@38656
   608
qed
hoelzl@38656
   609
hoelzl@38656
   610
lemma sigma_algebra_disjoint_iff:
hoelzl@38656
   611
     "sigma_algebra M \<longleftrightarrow>
hoelzl@38656
   612
      algebra M &
hoelzl@38656
   613
      (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow>
hoelzl@38656
   614
           (\<Union>i::nat. A i) \<in> sets M)"
hoelzl@38656
   615
proof (auto simp add: sigma_algebra_iff)
hoelzl@38656
   616
  fix A :: "nat \<Rightarrow> 'a set"
hoelzl@38656
   617
  assume M: "algebra M"
hoelzl@38656
   618
     and A: "range A \<subseteq> sets M"
hoelzl@38656
   619
     and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow>
hoelzl@38656
   620
               disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
hoelzl@38656
   621
  hence "range (disjointed A) \<subseteq> sets M \<longrightarrow>
hoelzl@38656
   622
         disjoint_family (disjointed A) \<longrightarrow>
hoelzl@38656
   623
         (\<Union>i. disjointed A i) \<in> sets M" by blast
hoelzl@38656
   624
  hence "(\<Union>i. disjointed A i) \<in> sets M"
hoelzl@38656
   625
    by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed)
hoelzl@38656
   626
  thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
hoelzl@38656
   627
qed
hoelzl@38656
   628
hoelzl@38656
   629
subsection {* A Two-Element Series *}
hoelzl@38656
   630
hoelzl@38656
   631
definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
hoelzl@38656
   632
  where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
hoelzl@38656
   633
hoelzl@38656
   634
lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
hoelzl@38656
   635
  apply (simp add: binaryset_def)
hoelzl@38656
   636
  apply (rule set_ext)
hoelzl@38656
   637
  apply (auto simp add: image_iff)
hoelzl@38656
   638
  done
hoelzl@38656
   639
hoelzl@38656
   640
lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
hoelzl@38656
   641
  by (simp add: UNION_eq_Union_image range_binaryset_eq)
hoelzl@38656
   642
hoelzl@38656
   643
section {* Closed CDI *}
hoelzl@38656
   644
hoelzl@38656
   645
definition
hoelzl@38656
   646
  closed_cdi  where
hoelzl@38656
   647
  "closed_cdi M \<longleftrightarrow>
hoelzl@38656
   648
   sets M \<subseteq> Pow (space M) &
hoelzl@38656
   649
   (\<forall>s \<in> sets M. space M - s \<in> sets M) &
hoelzl@38656
   650
   (\<forall>A. (range A \<subseteq> sets M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
hoelzl@38656
   651
        (\<Union>i. A i) \<in> sets M) &
hoelzl@38656
   652
   (\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
hoelzl@38656
   653
hoelzl@38656
   654
hoelzl@38656
   655
inductive_set
hoelzl@38656
   656
  smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
hoelzl@38656
   657
  for M
hoelzl@38656
   658
  where
hoelzl@38656
   659
    Basic [intro]:
hoelzl@38656
   660
      "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M"
hoelzl@38656
   661
  | Compl [intro]:
hoelzl@38656
   662
      "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M"
hoelzl@38656
   663
  | Inc:
hoelzl@38656
   664
      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n))
hoelzl@38656
   665
       \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets M"
hoelzl@38656
   666
  | Disj:
hoelzl@38656
   667
      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A
hoelzl@38656
   668
       \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets M"
hoelzl@38656
   669
  monos Pow_mono
hoelzl@38656
   670
hoelzl@38656
   671
hoelzl@38656
   672
definition
hoelzl@38656
   673
  smallest_closed_cdi  where
hoelzl@38656
   674
  "smallest_closed_cdi M = (|space = space M, sets = smallest_ccdi_sets M|)"
hoelzl@38656
   675
hoelzl@38656
   676
lemma space_smallest_closed_cdi [simp]:
hoelzl@38656
   677
     "space (smallest_closed_cdi M) = space M"
hoelzl@38656
   678
  by (simp add: smallest_closed_cdi_def)
hoelzl@38656
   679
hoelzl@38656
   680
lemma (in algebra) smallest_closed_cdi1: "sets M \<subseteq> sets (smallest_closed_cdi M)"
hoelzl@38656
   681
  by (auto simp add: smallest_closed_cdi_def)
hoelzl@38656
   682
hoelzl@38656
   683
lemma (in algebra) smallest_ccdi_sets:
hoelzl@38656
   684
     "smallest_ccdi_sets M \<subseteq> Pow (space M)"
hoelzl@38656
   685
  apply (rule subsetI)
hoelzl@38656
   686
  apply (erule smallest_ccdi_sets.induct)
hoelzl@38656
   687
  apply (auto intro: range_subsetD dest: sets_into_space)
hoelzl@38656
   688
  done
hoelzl@38656
   689
hoelzl@38656
   690
lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)"
hoelzl@38656
   691
  apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets)
hoelzl@38656
   692
  apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) +
hoelzl@38656
   693
  done
hoelzl@38656
   694
hoelzl@38656
   695
lemma (in algebra) smallest_closed_cdi3:
hoelzl@38656
   696
     "sets (smallest_closed_cdi M) \<subseteq> Pow (space M)"
hoelzl@38656
   697
  by (simp add: smallest_closed_cdi_def smallest_ccdi_sets)
hoelzl@38656
   698
hoelzl@38656
   699
lemma closed_cdi_subset: "closed_cdi M \<Longrightarrow> sets M \<subseteq> Pow (space M)"
hoelzl@38656
   700
  by (simp add: closed_cdi_def)
hoelzl@38656
   701
hoelzl@38656
   702
lemma closed_cdi_Compl: "closed_cdi M \<Longrightarrow> s \<in> sets M \<Longrightarrow> space M - s \<in> sets M"
hoelzl@38656
   703
  by (simp add: closed_cdi_def)
hoelzl@38656
   704
hoelzl@38656
   705
lemma closed_cdi_Inc:
hoelzl@38656
   706
     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow>
hoelzl@38656
   707
        (\<Union>i. A i) \<in> sets M"
hoelzl@38656
   708
  by (simp add: closed_cdi_def)
hoelzl@38656
   709
hoelzl@38656
   710
lemma closed_cdi_Disj:
hoelzl@38656
   711
     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
hoelzl@38656
   712
  by (simp add: closed_cdi_def)
hoelzl@38656
   713
hoelzl@38656
   714
lemma closed_cdi_Un:
hoelzl@38656
   715
  assumes cdi: "closed_cdi M" and empty: "{} \<in> sets M"
hoelzl@38656
   716
      and A: "A \<in> sets M" and B: "B \<in> sets M"
hoelzl@38656
   717
      and disj: "A \<inter> B = {}"
hoelzl@38656
   718
    shows "A \<union> B \<in> sets M"
hoelzl@38656
   719
proof -
hoelzl@38656
   720
  have ra: "range (binaryset A B) \<subseteq> sets M"
hoelzl@38656
   721
   by (simp add: range_binaryset_eq empty A B)
hoelzl@38656
   722
 have di:  "disjoint_family (binaryset A B)" using disj
hoelzl@38656
   723
   by (simp add: disjoint_family_on_def binaryset_def Int_commute)
hoelzl@38656
   724
 from closed_cdi_Disj [OF cdi ra di]
hoelzl@38656
   725
 show ?thesis
hoelzl@38656
   726
   by (simp add: UN_binaryset_eq)
hoelzl@38656
   727
qed
hoelzl@38656
   728
hoelzl@38656
   729
lemma (in algebra) smallest_ccdi_sets_Un:
hoelzl@38656
   730
  assumes A: "A \<in> smallest_ccdi_sets M" and B: "B \<in> smallest_ccdi_sets M"
hoelzl@38656
   731
      and disj: "A \<inter> B = {}"
hoelzl@38656
   732
    shows "A \<union> B \<in> smallest_ccdi_sets M"
hoelzl@38656
   733
proof -
hoelzl@38656
   734
  have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)"
hoelzl@38656
   735
    by (simp add: range_binaryset_eq  A B smallest_ccdi_sets.Basic)
hoelzl@38656
   736
  have di:  "disjoint_family (binaryset A B)" using disj
hoelzl@38656
   737
    by (simp add: disjoint_family_on_def binaryset_def Int_commute)
hoelzl@38656
   738
  from Disj [OF ra di]
hoelzl@38656
   739
  show ?thesis
hoelzl@38656
   740
    by (simp add: UN_binaryset_eq)
hoelzl@38656
   741
qed
hoelzl@38656
   742
hoelzl@38656
   743
lemma (in algebra) smallest_ccdi_sets_Int1:
hoelzl@38656
   744
  assumes a: "a \<in> sets M"
hoelzl@38656
   745
  shows "b \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
hoelzl@38656
   746
proof (induct rule: smallest_ccdi_sets.induct)
hoelzl@38656
   747
  case (Basic x)
hoelzl@38656
   748
  thus ?case
hoelzl@38656
   749
    by (metis a Int smallest_ccdi_sets.Basic)
hoelzl@38656
   750
next
hoelzl@38656
   751
  case (Compl x)
hoelzl@38656
   752
  have "a \<inter> (space M - x) = space M - ((space M - a) \<union> (a \<inter> x))"
hoelzl@38656
   753
    by blast
hoelzl@38656
   754
  also have "... \<in> smallest_ccdi_sets M"
hoelzl@38656
   755
    by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2
hoelzl@38656
   756
           Diff_disjoint Int_Diff Int_empty_right Un_commute
hoelzl@38656
   757
           smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl
hoelzl@38656
   758
           smallest_ccdi_sets_Un)
hoelzl@38656
   759
  finally show ?case .
hoelzl@38656
   760
next
hoelzl@38656
   761
  case (Inc A)
hoelzl@38656
   762
  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
hoelzl@38656
   763
    by blast
hoelzl@38656
   764
  have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Inc
hoelzl@38656
   765
    by blast
hoelzl@38656
   766
  moreover have "(\<lambda>i. a \<inter> A i) 0 = {}"
hoelzl@38656
   767
    by (simp add: Inc)
hoelzl@38656
   768
  moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc
hoelzl@38656
   769
    by blast
hoelzl@38656
   770
  ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
hoelzl@38656
   771
    by (rule smallest_ccdi_sets.Inc)
hoelzl@38656
   772
  show ?case
hoelzl@38656
   773
    by (metis 1 2)
hoelzl@38656
   774
next
hoelzl@38656
   775
  case (Disj A)
hoelzl@38656
   776
  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
hoelzl@38656
   777
    by blast
hoelzl@38656
   778
  have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj
hoelzl@38656
   779
    by blast
hoelzl@38656
   780
  moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj
hoelzl@38656
   781
    by (auto simp add: disjoint_family_on_def)
hoelzl@38656
   782
  ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
hoelzl@38656
   783
    by (rule smallest_ccdi_sets.Disj)
hoelzl@38656
   784
  show ?case
hoelzl@38656
   785
    by (metis 1 2)
hoelzl@38656
   786
qed
hoelzl@38656
   787
hoelzl@38656
   788
hoelzl@38656
   789
lemma (in algebra) smallest_ccdi_sets_Int:
hoelzl@38656
   790
  assumes b: "b \<in> smallest_ccdi_sets M"
hoelzl@38656
   791
  shows "a \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
hoelzl@38656
   792
proof (induct rule: smallest_ccdi_sets.induct)
hoelzl@38656
   793
  case (Basic x)
hoelzl@38656
   794
  thus ?case
hoelzl@38656
   795
    by (metis b smallest_ccdi_sets_Int1)
hoelzl@38656
   796
next
hoelzl@38656
   797
  case (Compl x)
hoelzl@38656
   798
  have "(space M - x) \<inter> b = space M - (x \<inter> b \<union> (space M - b))"
hoelzl@38656
   799
    by blast
hoelzl@38656
   800
  also have "... \<in> smallest_ccdi_sets M"
hoelzl@38656
   801
    by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b
hoelzl@38656
   802
           smallest_ccdi_sets.Compl smallest_ccdi_sets_Un)
hoelzl@38656
   803
  finally show ?case .
hoelzl@38656
   804
next
hoelzl@38656
   805
  case (Inc A)
hoelzl@38656
   806
  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
hoelzl@38656
   807
    by blast
hoelzl@38656
   808
  have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Inc
hoelzl@38656
   809
    by blast
hoelzl@38656
   810
  moreover have "(\<lambda>i. A i \<inter> b) 0 = {}"
hoelzl@38656
   811
    by (simp add: Inc)
hoelzl@38656
   812
  moreover have "!!n. (\<lambda>i. A i \<inter> b) n \<subseteq> (\<lambda>i. A i \<inter> b) (Suc n)" using Inc
hoelzl@38656
   813
    by blast
hoelzl@38656
   814
  ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
hoelzl@38656
   815
    by (rule smallest_ccdi_sets.Inc)
hoelzl@38656
   816
  show ?case
hoelzl@38656
   817
    by (metis 1 2)
hoelzl@38656
   818
next
hoelzl@38656
   819
  case (Disj A)
hoelzl@38656
   820
  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
hoelzl@38656
   821
    by blast
hoelzl@38656
   822
  have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj
hoelzl@38656
   823
    by blast
hoelzl@38656
   824
  moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj
hoelzl@38656
   825
    by (auto simp add: disjoint_family_on_def)
hoelzl@38656
   826
  ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
hoelzl@38656
   827
    by (rule smallest_ccdi_sets.Disj)
hoelzl@38656
   828
  show ?case
hoelzl@38656
   829
    by (metis 1 2)
hoelzl@38656
   830
qed
hoelzl@38656
   831
hoelzl@38656
   832
lemma (in algebra) sets_smallest_closed_cdi_Int:
hoelzl@38656
   833
   "a \<in> sets (smallest_closed_cdi M) \<Longrightarrow> b \<in> sets (smallest_closed_cdi M)
hoelzl@38656
   834
    \<Longrightarrow> a \<inter> b \<in> sets (smallest_closed_cdi M)"
hoelzl@38656
   835
  by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def)
hoelzl@38656
   836
hoelzl@38656
   837
lemma (in algebra) sigma_property_disjoint_lemma:
hoelzl@38656
   838
  assumes sbC: "sets M \<subseteq> C"
hoelzl@38656
   839
      and ccdi: "closed_cdi (|space = space M, sets = C|)"
hoelzl@38656
   840
  shows "sigma_sets (space M) (sets M) \<subseteq> C"
hoelzl@38656
   841
proof -
hoelzl@38656
   842
  have "smallest_ccdi_sets M \<in> {B . sets M \<subseteq> B \<and> sigma_algebra (|space = space M, sets = B|)}"
hoelzl@38656
   843
    apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int
hoelzl@38656
   844
            smallest_ccdi_sets_Int)
hoelzl@38656
   845
    apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets)
hoelzl@38656
   846
    apply (blast intro: smallest_ccdi_sets.Disj)
hoelzl@38656
   847
    done
hoelzl@38656
   848
  hence "sigma_sets (space M) (sets M) \<subseteq> smallest_ccdi_sets M"
hoelzl@38656
   849
    by clarsimp
hoelzl@38656
   850
       (drule sigma_algebra.sigma_sets_subset [where a="sets M"], auto)
hoelzl@38656
   851
  also have "...  \<subseteq> C"
hoelzl@38656
   852
    proof
hoelzl@38656
   853
      fix x
hoelzl@38656
   854
      assume x: "x \<in> smallest_ccdi_sets M"
hoelzl@38656
   855
      thus "x \<in> C"
hoelzl@38656
   856
        proof (induct rule: smallest_ccdi_sets.induct)
hoelzl@38656
   857
          case (Basic x)
hoelzl@38656
   858
          thus ?case
hoelzl@38656
   859
            by (metis Basic subsetD sbC)
hoelzl@38656
   860
        next
hoelzl@38656
   861
          case (Compl x)
hoelzl@38656
   862
          thus ?case
hoelzl@38656
   863
            by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
hoelzl@38656
   864
        next
hoelzl@38656
   865
          case (Inc A)
hoelzl@38656
   866
          thus ?case
hoelzl@38656
   867
               by (auto intro: closed_cdi_Inc [OF ccdi, simplified])
hoelzl@38656
   868
        next
hoelzl@38656
   869
          case (Disj A)
hoelzl@38656
   870
          thus ?case
hoelzl@38656
   871
               by (auto intro: closed_cdi_Disj [OF ccdi, simplified])
hoelzl@38656
   872
        qed
hoelzl@38656
   873
    qed
hoelzl@38656
   874
  finally show ?thesis .
hoelzl@38656
   875
qed
hoelzl@38656
   876
hoelzl@38656
   877
lemma (in algebra) sigma_property_disjoint:
hoelzl@38656
   878
  assumes sbC: "sets M \<subseteq> C"
hoelzl@38656
   879
      and compl: "!!s. s \<in> C \<inter> sigma_sets (space M) (sets M) \<Longrightarrow> space M - s \<in> C"
hoelzl@38656
   880
      and inc: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
hoelzl@38656
   881
                     \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n))
hoelzl@38656
   882
                     \<Longrightarrow> (\<Union>i. A i) \<in> C"
hoelzl@38656
   883
      and disj: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
hoelzl@38656
   884
                      \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C"
hoelzl@38656
   885
  shows "sigma_sets (space M) (sets M) \<subseteq> C"
hoelzl@38656
   886
proof -
hoelzl@38656
   887
  have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
hoelzl@38656
   888
    proof (rule sigma_property_disjoint_lemma)
hoelzl@38656
   889
      show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
hoelzl@38656
   890
        by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
hoelzl@38656
   891
    next
hoelzl@38656
   892
      show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
hoelzl@38656
   893
        by (simp add: closed_cdi_def compl inc disj)
hoelzl@38656
   894
           (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
hoelzl@38656
   895
             IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
hoelzl@38656
   896
    qed
hoelzl@38656
   897
  thus ?thesis
hoelzl@38656
   898
    by blast
hoelzl@38656
   899
qed
hoelzl@38656
   900
paulson@33271
   901
end