src/HOL/Probability/Sigma_Algebra.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 46731 5302e932d1e5
child 47694 05663f75964c
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
wenzelm@41983
     1
(*  Title:      HOL/Probability/Sigma_Algebra.thy
hoelzl@42067
     2
    Author:     Stefan Richter, Markus Wenzel, TU München
hoelzl@42067
     3
    Author:     Johannes Hölzl, TU München
hoelzl@41981
     4
    Plus material from the Hurd/Coble measure theory development,
hoelzl@41981
     5
    translated by Lawrence Paulson.
paulson@33271
     6
*)
paulson@33271
     7
paulson@33271
     8
header {* Sigma Algebras *}
paulson@33271
     9
wenzelm@41413
    10
theory Sigma_Algebra
wenzelm@41413
    11
imports
hoelzl@42145
    12
  Complex_Main
wenzelm@41413
    13
  "~~/src/HOL/Library/Countable"
wenzelm@41413
    14
  "~~/src/HOL/Library/FuncSet"
wenzelm@41413
    15
  "~~/src/HOL/Library/Indicator_Function"
wenzelm@41413
    16
begin
paulson@33271
    17
paulson@33271
    18
text {* Sigma algebras are an elementary concept in measure
paulson@33271
    19
  theory. To measure --- that is to integrate --- functions, we first have
paulson@33271
    20
  to measure sets. Unfortunately, when dealing with a large universe,
paulson@33271
    21
  it is often not possible to consistently assign a measure to every
paulson@33271
    22
  subset. Therefore it is necessary to define the set of measurable
paulson@33271
    23
  subsets of the universe. A sigma algebra is such a set that has
paulson@33271
    24
  three very natural and desirable properties. *}
paulson@33271
    25
paulson@33271
    26
subsection {* Algebras *}
paulson@33271
    27
hoelzl@38656
    28
record 'a algebra =
hoelzl@38656
    29
  space :: "'a set"
paulson@33271
    30
  sets :: "'a set set"
paulson@33271
    31
hoelzl@42065
    32
locale subset_class =
hoelzl@41689
    33
  fixes M :: "('a, 'b) algebra_scheme"
paulson@33271
    34
  assumes space_closed: "sets M \<subseteq> Pow (space M)"
paulson@33271
    35
hoelzl@42065
    36
lemma (in subset_class) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
paulson@33271
    37
  by (metis PowD contra_subsetD space_closed)
paulson@33271
    38
hoelzl@42065
    39
locale ring_of_sets = subset_class +
hoelzl@42065
    40
  assumes empty_sets [iff]: "{} \<in> sets M"
hoelzl@42065
    41
     and  Diff [intro]: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a - b \<in> sets M"
hoelzl@42065
    42
     and  Un [intro]: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
hoelzl@42065
    43
hoelzl@42065
    44
lemma (in ring_of_sets) Int [intro]:
paulson@33271
    45
  assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M"
paulson@33271
    46
proof -
hoelzl@42065
    47
  have "a \<inter> b = a - (a - b)"
hoelzl@42065
    48
    by auto
hoelzl@42065
    49
  then show "a \<inter> b \<in> sets M"
hoelzl@42065
    50
    using a b by auto
paulson@33271
    51
qed
paulson@33271
    52
hoelzl@42065
    53
lemma (in ring_of_sets) finite_Union [intro]:
paulson@33271
    54
  "finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M"
hoelzl@38656
    55
  by (induct set: finite) (auto simp add: Un)
paulson@33271
    56
hoelzl@42065
    57
lemma (in ring_of_sets) finite_UN[intro]:
hoelzl@41981
    58
  assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
hoelzl@41981
    59
  shows "(\<Union>i\<in>I. A i) \<in> sets M"
hoelzl@41981
    60
  using assms by induct auto
hoelzl@41981
    61
hoelzl@42065
    62
lemma (in ring_of_sets) finite_INT[intro]:
hoelzl@41981
    63
  assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
hoelzl@41981
    64
  shows "(\<Inter>i\<in>I. A i) \<in> sets M"
hoelzl@41981
    65
  using assms by (induct rule: finite_ne_induct) auto
hoelzl@41981
    66
hoelzl@42065
    67
lemma (in ring_of_sets) insert_in_sets:
hoelzl@38656
    68
  assumes "{x} \<in> sets M" "A \<in> sets M" shows "insert x A \<in> sets M"
hoelzl@38656
    69
proof -
hoelzl@38656
    70
  have "{x} \<union> A \<in> sets M" using assms by (rule Un)
hoelzl@38656
    71
  thus ?thesis by auto
hoelzl@38656
    72
qed
hoelzl@38656
    73
hoelzl@42065
    74
lemma (in ring_of_sets) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
hoelzl@38656
    75
  by (metis Int_absorb1 sets_into_space)
hoelzl@38656
    76
hoelzl@42065
    77
lemma (in ring_of_sets) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
hoelzl@38656
    78
  by (metis Int_absorb2 sets_into_space)
hoelzl@38656
    79
hoelzl@42867
    80
lemma (in ring_of_sets) sets_Collect_conj:
hoelzl@42867
    81
  assumes "{x\<in>space M. P x} \<in> sets M" "{x\<in>space M. Q x} \<in> sets M"
hoelzl@42867
    82
  shows "{x\<in>space M. Q x \<and> P x} \<in> sets M"
hoelzl@42867
    83
proof -
hoelzl@42867
    84
  have "{x\<in>space M. Q x \<and> P x} = {x\<in>space M. Q x} \<inter> {x\<in>space M. P x}"
hoelzl@42867
    85
    by auto
hoelzl@42867
    86
  with assms show ?thesis by auto
hoelzl@42867
    87
qed
hoelzl@42867
    88
hoelzl@42867
    89
lemma (in ring_of_sets) sets_Collect_disj:
hoelzl@42867
    90
  assumes "{x\<in>space M. P x} \<in> sets M" "{x\<in>space M. Q x} \<in> sets M"
hoelzl@42867
    91
  shows "{x\<in>space M. Q x \<or> P x} \<in> sets M"
hoelzl@42867
    92
proof -
hoelzl@42867
    93
  have "{x\<in>space M. Q x \<or> P x} = {x\<in>space M. Q x} \<union> {x\<in>space M. P x}"
hoelzl@42867
    94
    by auto
hoelzl@42867
    95
  with assms show ?thesis by auto
hoelzl@42867
    96
qed
hoelzl@42867
    97
hoelzl@42867
    98
lemma (in ring_of_sets) sets_Collect_finite_All:
hoelzl@42867
    99
  assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" "finite S" "S \<noteq> {}"
hoelzl@42867
   100
  shows "{x\<in>space M. \<forall>i\<in>S. P i x} \<in> sets M"
hoelzl@42867
   101
proof -
hoelzl@42867
   102
  have "{x\<in>space M. \<forall>i\<in>S. P i x} = (\<Inter>i\<in>S. {x\<in>space M. P i x})"
hoelzl@42867
   103
    using `S \<noteq> {}` by auto
hoelzl@42867
   104
  with assms show ?thesis by auto
hoelzl@42867
   105
qed
hoelzl@42867
   106
hoelzl@42867
   107
lemma (in ring_of_sets) sets_Collect_finite_Ex:
hoelzl@42867
   108
  assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" "finite S"
hoelzl@42867
   109
  shows "{x\<in>space M. \<exists>i\<in>S. P i x} \<in> sets M"
hoelzl@42867
   110
proof -
hoelzl@42867
   111
  have "{x\<in>space M. \<exists>i\<in>S. P i x} = (\<Union>i\<in>S. {x\<in>space M. P i x})"
hoelzl@42867
   112
    by auto
hoelzl@42867
   113
  with assms show ?thesis by auto
hoelzl@42867
   114
qed
hoelzl@42867
   115
hoelzl@42065
   116
locale algebra = ring_of_sets +
hoelzl@42065
   117
  assumes top [iff]: "space M \<in> sets M"
hoelzl@42065
   118
hoelzl@42065
   119
lemma (in algebra) compl_sets [intro]:
hoelzl@42065
   120
  "a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
hoelzl@42065
   121
  by auto
hoelzl@42065
   122
hoelzl@42065
   123
lemma algebra_iff_Un:
hoelzl@42065
   124
  "algebra M \<longleftrightarrow>
hoelzl@42065
   125
    sets M \<subseteq> Pow (space M) &
hoelzl@42065
   126
    {} \<in> sets M &
hoelzl@42065
   127
    (\<forall>a \<in> sets M. space M - a \<in> sets M) &
hoelzl@42065
   128
    (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<union> b \<in> sets M)" (is "_ \<longleftrightarrow> ?Un")
hoelzl@42065
   129
proof
hoelzl@42065
   130
  assume "algebra M"
hoelzl@42065
   131
  then interpret algebra M .
hoelzl@42065
   132
  show ?Un using sets_into_space by auto
hoelzl@42065
   133
next
hoelzl@42065
   134
  assume ?Un
hoelzl@42065
   135
  show "algebra M"
hoelzl@42065
   136
  proof
hoelzl@42065
   137
    show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M" "space M \<in> sets M"
hoelzl@42065
   138
      using `?Un` by auto
hoelzl@42065
   139
    fix a b assume a: "a \<in> sets M" and b: "b \<in> sets M"
hoelzl@42065
   140
    then show "a \<union> b \<in> sets M" using `?Un` by auto
hoelzl@42065
   141
    have "a - b = space M - ((space M - a) \<union> b)"
hoelzl@42065
   142
      using space a b by auto
hoelzl@42065
   143
    then show "a - b \<in> sets M"
hoelzl@42065
   144
      using a b  `?Un` by auto
hoelzl@42065
   145
  qed
hoelzl@42065
   146
qed
hoelzl@42065
   147
hoelzl@42065
   148
lemma algebra_iff_Int:
hoelzl@42065
   149
     "algebra M \<longleftrightarrow>
hoelzl@42065
   150
       sets M \<subseteq> Pow (space M) & {} \<in> sets M &
hoelzl@42065
   151
       (\<forall>a \<in> sets M. space M - a \<in> sets M) &
hoelzl@42065
   152
       (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)" (is "_ \<longleftrightarrow> ?Int")
hoelzl@42065
   153
proof
hoelzl@42065
   154
  assume "algebra M"
hoelzl@42065
   155
  then interpret algebra M .
hoelzl@42065
   156
  show ?Int using sets_into_space by auto
hoelzl@42065
   157
next
hoelzl@42065
   158
  assume ?Int
hoelzl@42065
   159
  show "algebra M"
hoelzl@42065
   160
  proof (unfold algebra_iff_Un, intro conjI ballI)
hoelzl@42065
   161
    show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M"
hoelzl@42065
   162
      using `?Int` by auto
hoelzl@42065
   163
    from `?Int` show "\<And>a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M" by auto
hoelzl@42065
   164
    fix a b assume sets: "a \<in> sets M" "b \<in> sets M"
hoelzl@42065
   165
    hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
hoelzl@42065
   166
      using space by blast
hoelzl@42065
   167
    also have "... \<in> sets M"
hoelzl@42065
   168
      using sets `?Int` by auto
hoelzl@42065
   169
    finally show "a \<union> b \<in> sets M" .
hoelzl@42065
   170
  qed
hoelzl@42065
   171
qed
hoelzl@42065
   172
hoelzl@42867
   173
lemma (in algebra) sets_Collect_neg:
hoelzl@42867
   174
  assumes "{x\<in>space M. P x} \<in> sets M"
hoelzl@42867
   175
  shows "{x\<in>space M. \<not> P x} \<in> sets M"
hoelzl@42867
   176
proof -
hoelzl@42867
   177
  have "{x\<in>space M. \<not> P x} = space M - {x\<in>space M. P x}" by auto
hoelzl@42867
   178
  with assms show ?thesis by auto
hoelzl@42867
   179
qed
hoelzl@42867
   180
hoelzl@42867
   181
lemma (in algebra) sets_Collect_imp:
hoelzl@42867
   182
  "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> {x\<in>space M. Q x} \<in> sets M \<Longrightarrow> {x\<in>space M. Q x \<longrightarrow> P x} \<in> sets M"
hoelzl@42867
   183
  unfolding imp_conv_disj by (intro sets_Collect_disj sets_Collect_neg)
hoelzl@42867
   184
hoelzl@42867
   185
lemma (in algebra) sets_Collect_const:
hoelzl@42867
   186
  "{x\<in>space M. P} \<in> sets M"
hoelzl@42867
   187
  by (cases P) auto
hoelzl@42867
   188
hoelzl@42984
   189
lemma algebra_single_set:
hoelzl@42984
   190
  assumes "X \<subseteq> S"
hoelzl@42984
   191
  shows "algebra \<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
hoelzl@42984
   192
  by default (insert `X \<subseteq> S`, auto)
hoelzl@42984
   193
hoelzl@39092
   194
section {* Restricted algebras *}
hoelzl@39092
   195
hoelzl@39092
   196
abbreviation (in algebra)
hoelzl@41689
   197
  "restricted_space A \<equiv> \<lparr> space = A, sets = (\<lambda>S. (A \<inter> S)) ` sets M, \<dots> = more M \<rparr>"
hoelzl@39092
   198
hoelzl@38656
   199
lemma (in algebra) restricted_algebra:
hoelzl@39092
   200
  assumes "A \<in> sets M" shows "algebra (restricted_space A)"
hoelzl@38656
   201
  using assms by unfold_locales auto
paulson@33271
   202
paulson@33271
   203
subsection {* Sigma Algebras *}
paulson@33271
   204
paulson@33271
   205
locale sigma_algebra = algebra +
hoelzl@38656
   206
  assumes countable_nat_UN [intro]:
paulson@33271
   207
         "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
paulson@33271
   208
hoelzl@42984
   209
lemma (in algebra) is_sigma_algebra:
hoelzl@42984
   210
  assumes "finite (sets M)"
hoelzl@42984
   211
  shows "sigma_algebra M"
hoelzl@42984
   212
proof
hoelzl@42984
   213
  fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets M"
hoelzl@42984
   214
  then have "(\<Union>i. A i) = (\<Union>s\<in>sets M \<inter> range A. s)"
hoelzl@42984
   215
    by auto
hoelzl@42984
   216
  also have "(\<Union>s\<in>sets M \<inter> range A. s) \<in> sets M"
wenzelm@46731
   217
    using `finite (sets M)` by auto
hoelzl@42984
   218
  finally show "(\<Union>i. A i) \<in> sets M" .
hoelzl@42984
   219
qed
hoelzl@42984
   220
hoelzl@38656
   221
lemma countable_UN_eq:
hoelzl@38656
   222
  fixes A :: "'i::countable \<Rightarrow> 'a set"
hoelzl@38656
   223
  shows "(range A \<subseteq> sets M \<longrightarrow> (\<Union>i. A i) \<in> sets M) \<longleftrightarrow>
hoelzl@38656
   224
    (range (A \<circ> from_nat) \<subseteq> sets M \<longrightarrow> (\<Union>i. (A \<circ> from_nat) i) \<in> sets M)"
hoelzl@38656
   225
proof -
hoelzl@38656
   226
  let ?A' = "A \<circ> from_nat"
hoelzl@38656
   227
  have *: "(\<Union>i. ?A' i) = (\<Union>i. A i)" (is "?l = ?r")
hoelzl@38656
   228
  proof safe
hoelzl@38656
   229
    fix x i assume "x \<in> A i" thus "x \<in> ?l"
hoelzl@38656
   230
      by (auto intro!: exI[of _ "to_nat i"])
hoelzl@38656
   231
  next
hoelzl@38656
   232
    fix x i assume "x \<in> ?A' i" thus "x \<in> ?r"
hoelzl@38656
   233
      by (auto intro!: exI[of _ "from_nat i"])
hoelzl@38656
   234
  qed
hoelzl@38656
   235
  have **: "range ?A' = range A"
hoelzl@40702
   236
    using surj_from_nat
hoelzl@38656
   237
    by (auto simp: image_compose intro!: imageI)
hoelzl@38656
   238
  show ?thesis unfolding * ** ..
hoelzl@38656
   239
qed
hoelzl@38656
   240
hoelzl@38656
   241
lemma (in sigma_algebra) countable_UN[intro]:
hoelzl@38656
   242
  fixes A :: "'i::countable \<Rightarrow> 'a set"
hoelzl@38656
   243
  assumes "A`X \<subseteq> sets M"
hoelzl@38656
   244
  shows  "(\<Union>x\<in>X. A x) \<in> sets M"
hoelzl@38656
   245
proof -
wenzelm@46731
   246
  let ?A = "\<lambda>i. if i \<in> X then A i else {}"
hoelzl@38656
   247
  from assms have "range ?A \<subseteq> sets M" by auto
hoelzl@38656
   248
  with countable_nat_UN[of "?A \<circ> from_nat"] countable_UN_eq[of ?A M]
hoelzl@38656
   249
  have "(\<Union>x. ?A x) \<in> sets M" by auto
hoelzl@38656
   250
  moreover have "(\<Union>x. ?A x) = (\<Union>x\<in>X. A x)" by (auto split: split_if_asm)
hoelzl@38656
   251
  ultimately show ?thesis by simp
hoelzl@38656
   252
qed
hoelzl@38656
   253
paulson@33533
   254
lemma (in sigma_algebra) countable_INT [intro]:
hoelzl@38656
   255
  fixes A :: "'i::countable \<Rightarrow> 'a set"
hoelzl@38656
   256
  assumes A: "A`X \<subseteq> sets M" "X \<noteq> {}"
hoelzl@38656
   257
  shows "(\<Inter>i\<in>X. A i) \<in> sets M"
paulson@33271
   258
proof -
hoelzl@38656
   259
  from A have "\<forall>i\<in>X. A i \<in> sets M" by fast
hoelzl@38656
   260
  hence "space M - (\<Union>i\<in>X. space M - A i) \<in> sets M" by blast
paulson@33271
   261
  moreover
hoelzl@38656
   262
  have "(\<Inter>i\<in>X. A i) = space M - (\<Union>i\<in>X. space M - A i)" using space_closed A
paulson@33271
   263
    by blast
paulson@33271
   264
  ultimately show ?thesis by metis
paulson@33271
   265
qed
paulson@33271
   266
hoelzl@42145
   267
lemma ring_of_sets_Pow:
hoelzl@42145
   268
 "ring_of_sets \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
hoelzl@42145
   269
  by default auto
hoelzl@42145
   270
paulson@33271
   271
lemma algebra_Pow:
hoelzl@42145
   272
  "algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
hoelzl@42145
   273
  by default auto
paulson@33271
   274
paulson@33271
   275
lemma sigma_algebra_Pow:
hoelzl@38656
   276
     "sigma_algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
hoelzl@42145
   277
  by default auto
hoelzl@38656
   278
hoelzl@38656
   279
lemma sigma_algebra_iff:
hoelzl@38656
   280
     "sigma_algebra M \<longleftrightarrow>
hoelzl@38656
   281
      algebra M \<and> (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
hoelzl@38656
   282
  by (simp add: sigma_algebra_def sigma_algebra_axioms_def)
paulson@33271
   283
hoelzl@42867
   284
lemma (in sigma_algebra) sets_Collect_countable_All:
hoelzl@42867
   285
  assumes "\<And>i. {x\<in>space M. P i x} \<in> sets M"
hoelzl@42867
   286
  shows "{x\<in>space M. \<forall>i::'i::countable. P i x} \<in> sets M"
hoelzl@42867
   287
proof -
hoelzl@42867
   288
  have "{x\<in>space M. \<forall>i::'i::countable. P i x} = (\<Inter>i. {x\<in>space M. P i x})" by auto
hoelzl@42867
   289
  with assms show ?thesis by auto
hoelzl@42867
   290
qed
hoelzl@42867
   291
hoelzl@42867
   292
lemma (in sigma_algebra) sets_Collect_countable_Ex:
hoelzl@42867
   293
  assumes "\<And>i. {x\<in>space M. P i x} \<in> sets M"
hoelzl@42867
   294
  shows "{x\<in>space M. \<exists>i::'i::countable. P i x} \<in> sets M"
hoelzl@42867
   295
proof -
hoelzl@42867
   296
  have "{x\<in>space M. \<exists>i::'i::countable. P i x} = (\<Union>i. {x\<in>space M. P i x})" by auto
hoelzl@42867
   297
  with assms show ?thesis by auto
hoelzl@42867
   298
qed
hoelzl@42867
   299
hoelzl@42867
   300
lemmas (in sigma_algebra) sets_Collect =
hoelzl@42867
   301
  sets_Collect_imp sets_Collect_disj sets_Collect_conj sets_Collect_neg sets_Collect_const
hoelzl@42867
   302
  sets_Collect_countable_All sets_Collect_countable_Ex sets_Collect_countable_All
hoelzl@42867
   303
hoelzl@42984
   304
lemma sigma_algebra_single_set:
hoelzl@42984
   305
  assumes "X \<subseteq> S"
hoelzl@42984
   306
  shows "sigma_algebra \<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
hoelzl@42984
   307
  using algebra.is_sigma_algebra[OF algebra_single_set[OF `X \<subseteq> S`]] by simp
hoelzl@42984
   308
paulson@33271
   309
subsection {* Binary Unions *}
paulson@33271
   310
paulson@33271
   311
definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
paulson@33271
   312
  where "binary a b =  (\<lambda>\<^isup>x. b)(0 := a)"
paulson@33271
   313
hoelzl@38656
   314
lemma range_binary_eq: "range(binary a b) = {a,b}"
hoelzl@38656
   315
  by (auto simp add: binary_def)
paulson@33271
   316
hoelzl@38656
   317
lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
haftmann@44106
   318
  by (simp add: SUP_def range_binary_eq)
paulson@33271
   319
hoelzl@38656
   320
lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
haftmann@44106
   321
  by (simp add: INF_def range_binary_eq)
paulson@33271
   322
paulson@33271
   323
lemma sigma_algebra_iff2:
paulson@33271
   324
     "sigma_algebra M \<longleftrightarrow>
hoelzl@38656
   325
       sets M \<subseteq> Pow (space M) \<and>
hoelzl@38656
   326
       {} \<in> sets M \<and> (\<forall>s \<in> sets M. space M - s \<in> sets M) \<and>
paulson@33271
   327
       (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
hoelzl@38656
   328
  by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
hoelzl@42065
   329
         algebra_iff_Un Un_range_binary)
paulson@33271
   330
paulson@33271
   331
subsection {* Initial Sigma Algebra *}
paulson@33271
   332
paulson@33271
   333
text {*Sigma algebras can naturally be created as the closure of any set of
paulson@33271
   334
  sets with regard to the properties just postulated.  *}
paulson@33271
   335
paulson@33271
   336
inductive_set
paulson@33271
   337
  sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
paulson@33271
   338
  for sp :: "'a set" and A :: "'a set set"
paulson@33271
   339
  where
paulson@33271
   340
    Basic: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
paulson@33271
   341
  | Empty: "{} \<in> sigma_sets sp A"
paulson@33271
   342
  | Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp - a \<in> sigma_sets sp A"
paulson@33271
   343
  | Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A"
paulson@33271
   344
hoelzl@40859
   345
definition
hoelzl@41689
   346
  "sigma M = \<lparr> space = space M, sets = sigma_sets (space M) (sets M), \<dots> = more M \<rparr>"
hoelzl@41543
   347
hoelzl@41543
   348
lemma (in sigma_algebra) sigma_sets_subset:
hoelzl@41543
   349
  assumes a: "a \<subseteq> sets M"
hoelzl@41543
   350
  shows "sigma_sets (space M) a \<subseteq> sets M"
hoelzl@41543
   351
proof
hoelzl@41543
   352
  fix x
hoelzl@41543
   353
  assume "x \<in> sigma_sets (space M) a"
hoelzl@41543
   354
  from this show "x \<in> sets M"
hoelzl@41543
   355
    by (induct rule: sigma_sets.induct, auto) (metis a subsetD)
hoelzl@41543
   356
qed
hoelzl@41543
   357
hoelzl@41543
   358
lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
hoelzl@41543
   359
  by (erule sigma_sets.induct, auto)
hoelzl@41543
   360
hoelzl@41543
   361
lemma sigma_algebra_sigma_sets:
hoelzl@41543
   362
     "a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M"
hoelzl@41543
   363
  by (auto simp add: sigma_algebra_iff2 dest: sigma_sets_into_sp
hoelzl@41543
   364
           intro!: sigma_sets.Union sigma_sets.Empty sigma_sets.Compl)
hoelzl@41543
   365
hoelzl@41543
   366
lemma sigma_sets_least_sigma_algebra:
hoelzl@41543
   367
  assumes "A \<subseteq> Pow S"
hoelzl@41543
   368
  shows "sigma_sets S A = \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
hoelzl@41543
   369
proof safe
hoelzl@41543
   370
  fix B X assume "A \<subseteq> B" and sa: "sigma_algebra \<lparr> space = S, sets = B \<rparr>"
hoelzl@41543
   371
    and X: "X \<in> sigma_sets S A"
hoelzl@41543
   372
  from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF `A \<subseteq> B`] X
hoelzl@41543
   373
  show "X \<in> B" by auto
hoelzl@41543
   374
next
hoelzl@41543
   375
  fix X assume "X \<in> \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
hoelzl@41543
   376
  then have [intro!]: "\<And>B. A \<subseteq> B \<Longrightarrow> sigma_algebra \<lparr>space = S, sets = B\<rparr> \<Longrightarrow> X \<in> B"
hoelzl@41543
   377
     by simp
hoelzl@41543
   378
  have "A \<subseteq> sigma_sets S A" using assms
hoelzl@41543
   379
    by (auto intro!: sigma_sets.Basic)
hoelzl@41543
   380
  moreover have "sigma_algebra \<lparr>space = S, sets = sigma_sets S A\<rparr>"
hoelzl@41543
   381
    using assms by (intro sigma_algebra_sigma_sets[of A]) auto
hoelzl@41543
   382
  ultimately show "X \<in> sigma_sets S A" by auto
hoelzl@41543
   383
qed
paulson@33271
   384
hoelzl@40859
   385
lemma sets_sigma: "sets (sigma M) = sigma_sets (space M) (sets M)"
hoelzl@38656
   386
  unfolding sigma_def by simp
paulson@33271
   387
hoelzl@40859
   388
lemma space_sigma [simp]: "space (sigma M) = space M"
hoelzl@38656
   389
  by (simp add: sigma_def)
paulson@33271
   390
paulson@33271
   391
lemma sigma_sets_top: "sp \<in> sigma_sets sp A"
paulson@33271
   392
  by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)
paulson@33271
   393
hoelzl@38656
   394
lemma sigma_sets_Un:
paulson@33271
   395
  "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
hoelzl@38656
   396
apply (simp add: Un_range_binary range_binary_eq)
hoelzl@40859
   397
apply (rule Union, simp add: binary_def)
paulson@33271
   398
done
paulson@33271
   399
paulson@33271
   400
lemma sigma_sets_Inter:
paulson@33271
   401
  assumes Asb: "A \<subseteq> Pow sp"
paulson@33271
   402
  shows "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Inter>i. a i) \<in> sigma_sets sp A"
paulson@33271
   403
proof -
paulson@33271
   404
  assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A"
hoelzl@38656
   405
  hence "\<And>i::nat. sp-(a i) \<in> sigma_sets sp A"
paulson@33271
   406
    by (rule sigma_sets.Compl)
hoelzl@38656
   407
  hence "(\<Union>i. sp-(a i)) \<in> sigma_sets sp A"
paulson@33271
   408
    by (rule sigma_sets.Union)
hoelzl@38656
   409
  hence "sp-(\<Union>i. sp-(a i)) \<in> sigma_sets sp A"
paulson@33271
   410
    by (rule sigma_sets.Compl)
hoelzl@38656
   411
  also have "sp-(\<Union>i. sp-(a i)) = sp Int (\<Inter>i. a i)"
paulson@33271
   412
    by auto
paulson@33271
   413
  also have "... = (\<Inter>i. a i)" using ai
hoelzl@38656
   414
    by (blast dest: sigma_sets_into_sp [OF Asb])
hoelzl@38656
   415
  finally show ?thesis .
paulson@33271
   416
qed
paulson@33271
   417
paulson@33271
   418
lemma sigma_sets_INTER:
hoelzl@38656
   419
  assumes Asb: "A \<subseteq> Pow sp"
paulson@33271
   420
      and ai: "\<And>i::nat. i \<in> S \<Longrightarrow> a i \<in> sigma_sets sp A" and non: "S \<noteq> {}"
paulson@33271
   421
  shows "(\<Inter>i\<in>S. a i) \<in> sigma_sets sp A"
paulson@33271
   422
proof -
paulson@33271
   423
  from ai have "\<And>i. (if i\<in>S then a i else sp) \<in> sigma_sets sp A"
paulson@33271
   424
    by (simp add: sigma_sets.intros sigma_sets_top)
paulson@33271
   425
  hence "(\<Inter>i. (if i\<in>S then a i else sp)) \<in> sigma_sets sp A"
paulson@33271
   426
    by (rule sigma_sets_Inter [OF Asb])
paulson@33271
   427
  also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>S. a i)"
paulson@33271
   428
    by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+
paulson@33271
   429
  finally show ?thesis .
paulson@33271
   430
qed
paulson@33271
   431
paulson@33271
   432
lemma (in sigma_algebra) sigma_sets_eq:
paulson@33271
   433
     "sigma_sets (space M) (sets M) = sets M"
paulson@33271
   434
proof
paulson@33271
   435
  show "sets M \<subseteq> sigma_sets (space M) (sets M)"
huffman@37032
   436
    by (metis Set.subsetI sigma_sets.Basic)
paulson@33271
   437
  next
paulson@33271
   438
  show "sigma_sets (space M) (sets M) \<subseteq> sets M"
paulson@33271
   439
    by (metis sigma_sets_subset subset_refl)
paulson@33271
   440
qed
paulson@33271
   441
hoelzl@42981
   442
lemma sigma_sets_eqI:
hoelzl@42981
   443
  assumes A: "\<And>a. a \<in> A \<Longrightarrow> a \<in> sigma_sets M B"
hoelzl@42981
   444
  assumes B: "\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets M A"
hoelzl@42981
   445
  shows "sigma_sets M A = sigma_sets M B"
hoelzl@42981
   446
proof (intro set_eqI iffI)
hoelzl@42981
   447
  fix a assume "a \<in> sigma_sets M A"
hoelzl@42981
   448
  from this A show "a \<in> sigma_sets M B"
hoelzl@42981
   449
    by induct (auto intro!: sigma_sets.intros del: sigma_sets.Basic)
hoelzl@42981
   450
next
hoelzl@42981
   451
  fix b assume "b \<in> sigma_sets M B"
hoelzl@42981
   452
  from this B show "b \<in> sigma_sets M A"
hoelzl@42981
   453
    by induct (auto intro!: sigma_sets.intros del: sigma_sets.Basic)
hoelzl@42981
   454
qed
hoelzl@42981
   455
paulson@33271
   456
lemma sigma_algebra_sigma:
hoelzl@40859
   457
    "sets M \<subseteq> Pow (space M) \<Longrightarrow> sigma_algebra (sigma M)"
hoelzl@38656
   458
  apply (rule sigma_algebra_sigma_sets)
hoelzl@38656
   459
  apply (auto simp add: sigma_def)
paulson@33271
   460
  done
paulson@33271
   461
paulson@33271
   462
lemma (in sigma_algebra) sigma_subset:
hoelzl@40859
   463
    "sets N \<subseteq> sets M \<Longrightarrow> space N = space M \<Longrightarrow> sets (sigma N) \<subseteq> (sets M)"
paulson@33271
   464
  by (simp add: sigma_def sigma_sets_subset)
paulson@33271
   465
hoelzl@42984
   466
lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
hoelzl@42984
   467
proof
hoelzl@42984
   468
  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
hoelzl@42984
   469
    by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
hoelzl@42984
   470
qed
hoelzl@42984
   471
hoelzl@38656
   472
lemma (in sigma_algebra) restriction_in_sets:
hoelzl@38656
   473
  fixes A :: "nat \<Rightarrow> 'a set"
hoelzl@38656
   474
  assumes "S \<in> sets M"
hoelzl@38656
   475
  and *: "range A \<subseteq> (\<lambda>A. S \<inter> A) ` sets M" (is "_ \<subseteq> ?r")
hoelzl@38656
   476
  shows "range A \<subseteq> sets M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` sets M"
hoelzl@38656
   477
proof -
hoelzl@38656
   478
  { fix i have "A i \<in> ?r" using * by auto
hoelzl@38656
   479
    hence "\<exists>B. A i = B \<inter> S \<and> B \<in> sets M" by auto
hoelzl@38656
   480
    hence "A i \<subseteq> S" "A i \<in> sets M" using `S \<in> sets M` by auto }
hoelzl@38656
   481
  thus "range A \<subseteq> sets M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` sets M"
hoelzl@38656
   482
    by (auto intro!: image_eqI[of _ _ "(\<Union>i. A i)"])
hoelzl@38656
   483
qed
hoelzl@38656
   484
hoelzl@38656
   485
lemma (in sigma_algebra) restricted_sigma_algebra:
hoelzl@38656
   486
  assumes "S \<in> sets M"
hoelzl@39092
   487
  shows "sigma_algebra (restricted_space S)"
hoelzl@38656
   488
  unfolding sigma_algebra_def sigma_algebra_axioms_def
hoelzl@38656
   489
proof safe
hoelzl@39092
   490
  show "algebra (restricted_space S)" using restricted_algebra[OF assms] .
hoelzl@38656
   491
next
hoelzl@39092
   492
  fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets (restricted_space S)"
hoelzl@38656
   493
  from restriction_in_sets[OF assms this[simplified]]
hoelzl@39092
   494
  show "(\<Union>i. A i) \<in> sets (restricted_space S)" by simp
hoelzl@38656
   495
qed
hoelzl@38656
   496
hoelzl@40859
   497
lemma sigma_sets_Int:
hoelzl@41689
   498
  assumes "A \<in> sigma_sets sp st" "A \<subseteq> sp"
hoelzl@41689
   499
  shows "op \<inter> A ` sigma_sets sp st = sigma_sets A (op \<inter> A ` st)"
hoelzl@40859
   500
proof (intro equalityI subsetI)
hoelzl@40859
   501
  fix x assume "x \<in> op \<inter> A ` sigma_sets sp st"
hoelzl@40859
   502
  then obtain y where "y \<in> sigma_sets sp st" "x = y \<inter> A" by auto
hoelzl@41689
   503
  then have "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
hoelzl@40859
   504
  proof (induct arbitrary: x)
hoelzl@40859
   505
    case (Compl a)
hoelzl@40859
   506
    then show ?case
hoelzl@40859
   507
      by (force intro!: sigma_sets.Compl simp: Diff_Int_distrib ac_simps)
hoelzl@40859
   508
  next
hoelzl@40859
   509
    case (Union a)
hoelzl@40859
   510
    then show ?case
hoelzl@40859
   511
      by (auto intro!: sigma_sets.Union
hoelzl@40859
   512
               simp add: UN_extend_simps simp del: UN_simps)
hoelzl@40859
   513
  qed (auto intro!: sigma_sets.intros)
hoelzl@41689
   514
  then show "x \<in> sigma_sets A (op \<inter> A ` st)"
hoelzl@41689
   515
    using `A \<subseteq> sp` by (simp add: Int_absorb2)
hoelzl@40859
   516
next
hoelzl@41689
   517
  fix x assume "x \<in> sigma_sets A (op \<inter> A ` st)"
hoelzl@40859
   518
  then show "x \<in> op \<inter> A ` sigma_sets sp st"
hoelzl@40859
   519
  proof induct
hoelzl@40859
   520
    case (Compl a)
hoelzl@40859
   521
    then obtain x where "a = A \<inter> x" "x \<in> sigma_sets sp st" by auto
hoelzl@41689
   522
    then show ?case using `A \<subseteq> sp`
hoelzl@40859
   523
      by (force simp add: image_iff intro!: bexI[of _ "sp - x"] sigma_sets.Compl)
hoelzl@40859
   524
  next
hoelzl@40859
   525
    case (Union a)
hoelzl@40859
   526
    then have "\<forall>i. \<exists>x. x \<in> sigma_sets sp st \<and> a i = A \<inter> x"
hoelzl@40859
   527
      by (auto simp: image_iff Bex_def)
hoelzl@40859
   528
    from choice[OF this] guess f ..
hoelzl@40859
   529
    then show ?case
hoelzl@40859
   530
      by (auto intro!: bexI[of _ "(\<Union>x. f x)"] sigma_sets.Union
hoelzl@40859
   531
               simp add: image_iff)
hoelzl@40859
   532
  qed (auto intro!: sigma_sets.intros)
hoelzl@40859
   533
qed
hoelzl@40859
   534
hoelzl@40859
   535
lemma sigma_sets_single[simp]: "sigma_sets {X} {{X}} = {{}, {X}}"
hoelzl@40859
   536
proof (intro set_eqI iffI)
hoelzl@40859
   537
  fix x assume "x \<in> sigma_sets {X} {{X}}"
hoelzl@40859
   538
  from sigma_sets_into_sp[OF _ this]
hoelzl@40859
   539
  show "x \<in> {{}, {X}}" by auto
hoelzl@40859
   540
next
hoelzl@40859
   541
  fix x assume "x \<in> {{}, {X}}"
hoelzl@40859
   542
  then show "x \<in> sigma_sets {X} {{X}}"
hoelzl@40859
   543
    by (auto intro: sigma_sets.Empty sigma_sets_top)
hoelzl@40859
   544
qed
hoelzl@40859
   545
hoelzl@40869
   546
lemma (in sigma_algebra) sets_sigma_subset:
hoelzl@40869
   547
  assumes "space N = space M"
hoelzl@40869
   548
  assumes "sets N \<subseteq> sets M"
hoelzl@40869
   549
  shows "sets (sigma N) \<subseteq> sets M"
hoelzl@40869
   550
  by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms)
hoelzl@40869
   551
hoelzl@40871
   552
lemma in_sigma[intro, simp]: "A \<in> sets M \<Longrightarrow> A \<in> sets (sigma M)"
hoelzl@40871
   553
  unfolding sigma_def by (auto intro!: sigma_sets.Basic)
hoelzl@40871
   554
hoelzl@40871
   555
lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M"
hoelzl@40871
   556
  unfolding sigma_def sigma_sets_eq by simp
hoelzl@40871
   557
hoelzl@42987
   558
lemma sigma_sigma_eq:
hoelzl@42987
   559
  assumes "sets M \<subseteq> Pow (space M)"
hoelzl@42987
   560
  shows "sigma (sigma M) = sigma M"
hoelzl@42987
   561
  using sigma_algebra.sigma_eq[OF sigma_algebra_sigma, OF assms] .
hoelzl@42987
   562
hoelzl@42987
   563
lemma sigma_sets_sigma_sets_eq:
hoelzl@42987
   564
  "M \<subseteq> Pow S \<Longrightarrow> sigma_sets S (sigma_sets S M) = sigma_sets S M"
hoelzl@42987
   565
  using sigma_sigma_eq[of "\<lparr> space = S, sets = M \<rparr>"]
hoelzl@42987
   566
  by (simp add: sigma_def)
hoelzl@42987
   567
hoelzl@42984
   568
lemma sigma_sets_singleton:
hoelzl@42984
   569
  assumes "X \<subseteq> S"
hoelzl@42984
   570
  shows "sigma_sets S { X } = { {}, X, S - X, S }"
hoelzl@42984
   571
proof -
hoelzl@42984
   572
  interpret sigma_algebra "\<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
hoelzl@42984
   573
    by (rule sigma_algebra_single_set) fact
hoelzl@42984
   574
  have "sigma_sets S { X } \<subseteq> sigma_sets S { {}, X, S - X, S }"
hoelzl@42984
   575
    by (rule sigma_sets_subseteq) simp
hoelzl@42984
   576
  moreover have "\<dots> = { {}, X, S - X, S }"
hoelzl@42984
   577
    using sigma_eq unfolding sigma_def by simp
hoelzl@42984
   578
  moreover
hoelzl@42984
   579
  { fix A assume "A \<in> { {}, X, S - X, S }"
hoelzl@42984
   580
    then have "A \<in> sigma_sets S { X }"
hoelzl@42984
   581
      by (auto intro: sigma_sets.intros sigma_sets_top) }
hoelzl@42984
   582
  ultimately have "sigma_sets S { X } = sigma_sets S { {}, X, S - X, S }"
hoelzl@42984
   583
    by (intro antisym) auto
hoelzl@42984
   584
  with sigma_eq show ?thesis
hoelzl@42984
   585
    unfolding sigma_def by simp
hoelzl@42984
   586
qed
hoelzl@42984
   587
hoelzl@42863
   588
lemma restricted_sigma:
hoelzl@42863
   589
  assumes S: "S \<in> sets (sigma M)" and M: "sets M \<subseteq> Pow (space M)"
hoelzl@42863
   590
  shows "algebra.restricted_space (sigma M) S = sigma (algebra.restricted_space M S)"
hoelzl@42863
   591
proof -
hoelzl@42863
   592
  from S sigma_sets_into_sp[OF M]
hoelzl@42863
   593
  have "S \<in> sigma_sets (space M) (sets M)" "S \<subseteq> space M"
hoelzl@42863
   594
    by (auto simp: sigma_def)
hoelzl@42863
   595
  from sigma_sets_Int[OF this]
hoelzl@42863
   596
  show ?thesis
hoelzl@42863
   597
    by (simp add: sigma_def)
hoelzl@42863
   598
qed
hoelzl@42863
   599
hoelzl@42987
   600
lemma sigma_sets_vimage_commute:
hoelzl@42987
   601
  assumes X: "X \<in> space M \<rightarrow> space M'"
hoelzl@42987
   602
  shows "{X -` A \<inter> space M |A. A \<in> sets (sigma M')}
hoelzl@42987
   603
       = sigma_sets (space M) {X -` A \<inter> space M |A. A \<in> sets M'}" (is "?L = ?R")
hoelzl@42987
   604
proof
hoelzl@42987
   605
  show "?L \<subseteq> ?R"
hoelzl@42987
   606
  proof clarify
hoelzl@42987
   607
    fix A assume "A \<in> sets (sigma M')"
hoelzl@42987
   608
    then have "A \<in> sigma_sets (space M') (sets M')" by (simp add: sets_sigma)
hoelzl@42987
   609
    then show "X -` A \<inter> space M \<in> ?R"
hoelzl@42987
   610
    proof induct
hoelzl@42987
   611
      case (Basic B) then show ?case
hoelzl@42987
   612
        by (auto intro!: sigma_sets.Basic)
hoelzl@42987
   613
    next
hoelzl@42987
   614
      case Empty then show ?case
hoelzl@42987
   615
        by (auto intro!: sigma_sets.Empty)
hoelzl@42987
   616
    next
hoelzl@42987
   617
      case (Compl B)
hoelzl@42987
   618
      have [simp]: "X -` (space M' - B) \<inter> space M = space M - (X -` B \<inter> space M)"
hoelzl@42987
   619
        by (auto simp add: funcset_mem [OF X])
hoelzl@42987
   620
      with Compl show ?case
hoelzl@42987
   621
        by (auto intro!: sigma_sets.Compl)
hoelzl@42987
   622
    next
hoelzl@42987
   623
      case (Union F)
hoelzl@42987
   624
      then show ?case
hoelzl@42987
   625
        by (auto simp add: vimage_UN UN_extend_simps(4) simp del: UN_simps
hoelzl@42987
   626
                 intro!: sigma_sets.Union)
hoelzl@42987
   627
    qed
hoelzl@42987
   628
  qed
hoelzl@42987
   629
  show "?R \<subseteq> ?L"
hoelzl@42987
   630
  proof clarify
hoelzl@42987
   631
    fix A assume "A \<in> ?R"
hoelzl@42987
   632
    then show "\<exists>B. A = X -` B \<inter> space M \<and> B \<in> sets (sigma M')"
hoelzl@42987
   633
    proof induct
hoelzl@42987
   634
      case (Basic B) then show ?case by auto
hoelzl@42987
   635
    next
hoelzl@42987
   636
      case Empty then show ?case
hoelzl@42987
   637
        by (auto simp: sets_sigma intro!: sigma_sets.Empty exI[of _ "{}"])
hoelzl@42987
   638
    next
hoelzl@42987
   639
      case (Compl B)
hoelzl@42987
   640
      then obtain A where A: "B = X -` A \<inter> space M" "A \<in> sets (sigma M')" by auto
hoelzl@42987
   641
      then have [simp]: "space M - B = X -` (space M' - A) \<inter> space M"
hoelzl@42987
   642
        by (auto simp add: funcset_mem [OF X])
hoelzl@42987
   643
      with A(2) show ?case
hoelzl@42987
   644
        by (auto simp: sets_sigma intro: sigma_sets.Compl)
hoelzl@42987
   645
    next
hoelzl@42987
   646
      case (Union F)
hoelzl@42987
   647
      then have "\<forall>i. \<exists>B. F i = X -` B \<inter> space M \<and> B \<in> sets (sigma M')" by auto
hoelzl@42987
   648
      from choice[OF this] guess A .. note A = this
hoelzl@42987
   649
      with A show ?case
hoelzl@42987
   650
        by (auto simp: sets_sigma vimage_UN[symmetric] intro: sigma_sets.Union)
hoelzl@42987
   651
    qed
hoelzl@42987
   652
  qed
hoelzl@42987
   653
qed
hoelzl@42987
   654
hoelzl@38656
   655
section {* Measurable functions *}
hoelzl@38656
   656
hoelzl@38656
   657
definition
hoelzl@38656
   658
  "measurable A B = {f \<in> space A -> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
hoelzl@38656
   659
hoelzl@38656
   660
lemma (in sigma_algebra) measurable_sigma:
hoelzl@40859
   661
  assumes B: "sets N \<subseteq> Pow (space N)"
hoelzl@40859
   662
      and f: "f \<in> space M -> space N"
hoelzl@40859
   663
      and ba: "\<And>y. y \<in> sets N \<Longrightarrow> (f -` y) \<inter> space M \<in> sets M"
hoelzl@40859
   664
  shows "f \<in> measurable M (sigma N)"
hoelzl@38656
   665
proof -
hoelzl@40859
   666
  have "sigma_sets (space N) (sets N) \<subseteq> {y . (f -` y) \<inter> space M \<in> sets M & y \<subseteq> space N}"
hoelzl@38656
   667
    proof clarify
hoelzl@38656
   668
      fix x
hoelzl@40859
   669
      assume "x \<in> sigma_sets (space N) (sets N)"
hoelzl@40859
   670
      thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> space N"
hoelzl@38656
   671
        proof induct
hoelzl@38656
   672
          case (Basic a)
hoelzl@38656
   673
          thus ?case
hoelzl@38656
   674
            by (auto simp add: ba) (metis B subsetD PowD)
hoelzl@38656
   675
        next
hoelzl@38656
   676
          case Empty
hoelzl@38656
   677
          thus ?case
hoelzl@38656
   678
            by auto
hoelzl@38656
   679
        next
hoelzl@38656
   680
          case (Compl a)
hoelzl@40859
   681
          have [simp]: "f -` space N \<inter> space M = space M"
hoelzl@38656
   682
            by (auto simp add: funcset_mem [OF f])
hoelzl@38656
   683
          thus ?case
hoelzl@38656
   684
            by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
hoelzl@38656
   685
        next
hoelzl@38656
   686
          case (Union a)
hoelzl@38656
   687
          thus ?case
hoelzl@40859
   688
            by (simp add: vimage_UN, simp only: UN_extend_simps(4)) blast
hoelzl@38656
   689
        qed
hoelzl@38656
   690
    qed
hoelzl@38656
   691
  thus ?thesis
hoelzl@38656
   692
    by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f)
hoelzl@38656
   693
       (auto simp add: sigma_def)
hoelzl@38656
   694
qed
hoelzl@38656
   695
hoelzl@38656
   696
lemma measurable_cong:
hoelzl@38656
   697
  assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
hoelzl@38656
   698
  shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'"
hoelzl@38656
   699
  unfolding measurable_def using assms
hoelzl@38656
   700
  by (simp cong: vimage_inter_cong Pi_cong)
hoelzl@38656
   701
hoelzl@38656
   702
lemma measurable_space:
hoelzl@38656
   703
  "f \<in> measurable M A \<Longrightarrow> x \<in> space M \<Longrightarrow> f x \<in> space A"
hoelzl@38656
   704
   unfolding measurable_def by auto
hoelzl@38656
   705
hoelzl@38656
   706
lemma measurable_sets:
hoelzl@38656
   707
  "f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
hoelzl@38656
   708
   unfolding measurable_def by auto
hoelzl@38656
   709
hoelzl@38656
   710
lemma (in sigma_algebra) measurable_subset:
hoelzl@40859
   711
     "(\<And>S. S \<in> sets A \<Longrightarrow> S \<subseteq> space A) \<Longrightarrow> measurable M A \<subseteq> measurable M (sigma A)"
hoelzl@38656
   712
  by (auto intro: measurable_sigma measurable_sets measurable_space)
hoelzl@38656
   713
hoelzl@38656
   714
lemma measurable_eqI:
hoelzl@38656
   715
     "\<lbrakk> space m1 = space m1' ; space m2 = space m2' ;
hoelzl@38656
   716
        sets m1 = sets m1' ; sets m2 = sets m2' \<rbrakk>
hoelzl@38656
   717
      \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
hoelzl@38656
   718
  by (simp add: measurable_def sigma_algebra_iff2)
hoelzl@38656
   719
hoelzl@38656
   720
lemma (in sigma_algebra) measurable_const[intro, simp]:
hoelzl@38656
   721
  assumes "c \<in> space M'"
hoelzl@38656
   722
  shows "(\<lambda>x. c) \<in> measurable M M'"
hoelzl@38656
   723
  using assms by (auto simp add: measurable_def)
hoelzl@38656
   724
hoelzl@38656
   725
lemma (in sigma_algebra) measurable_If:
hoelzl@38656
   726
  assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
hoelzl@38656
   727
  assumes P: "{x\<in>space M. P x} \<in> sets M"
hoelzl@38656
   728
  shows "(\<lambda>x. if P x then f x else g x) \<in> measurable M M'"
hoelzl@38656
   729
  unfolding measurable_def
hoelzl@38656
   730
proof safe
hoelzl@38656
   731
  fix x assume "x \<in> space M"
hoelzl@38656
   732
  thus "(if P x then f x else g x) \<in> space M'"
hoelzl@38656
   733
    using measure unfolding measurable_def by auto
hoelzl@38656
   734
next
hoelzl@38656
   735
  fix A assume "A \<in> sets M'"
hoelzl@38656
   736
  hence *: "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M =
hoelzl@38656
   737
    ((f -` A \<inter> space M) \<inter> {x\<in>space M. P x}) \<union>
hoelzl@38656
   738
    ((g -` A \<inter> space M) \<inter> (space M - {x\<in>space M. P x}))"
hoelzl@38656
   739
    using measure unfolding measurable_def by (auto split: split_if_asm)
hoelzl@38656
   740
  show "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M \<in> sets M"
hoelzl@38656
   741
    using `A \<in> sets M'` measure P unfolding * measurable_def
hoelzl@38656
   742
    by (auto intro!: Un)
hoelzl@38656
   743
qed
hoelzl@38656
   744
hoelzl@38656
   745
lemma (in sigma_algebra) measurable_If_set:
hoelzl@38656
   746
  assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
hoelzl@38656
   747
  assumes P: "A \<in> sets M"
hoelzl@38656
   748
  shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> measurable M M'"
hoelzl@38656
   749
proof (rule measurable_If[OF measure])
hoelzl@38656
   750
  have "{x \<in> space M. x \<in> A} = A" using `A \<in> sets M` sets_into_space by auto
hoelzl@38656
   751
  thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<in> sets M` by auto
hoelzl@38656
   752
qed
hoelzl@38656
   753
hoelzl@42065
   754
lemma (in ring_of_sets) measurable_ident[intro, simp]: "id \<in> measurable M M"
hoelzl@38656
   755
  by (auto simp add: measurable_def)
hoelzl@38656
   756
hoelzl@38656
   757
lemma measurable_comp[intro]:
hoelzl@38656
   758
  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
hoelzl@38656
   759
  shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
hoelzl@38656
   760
  apply (auto simp add: measurable_def vimage_compose)
hoelzl@38656
   761
  apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
hoelzl@38656
   762
  apply force+
hoelzl@38656
   763
  done
hoelzl@38656
   764
hoelzl@38656
   765
lemma measurable_strong:
hoelzl@38656
   766
  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
hoelzl@38656
   767
  assumes f: "f \<in> measurable a b" and g: "g \<in> (space b -> space c)"
hoelzl@38656
   768
      and a: "sigma_algebra a" and b: "sigma_algebra b" and c: "sigma_algebra c"
hoelzl@38656
   769
      and t: "f ` (space a) \<subseteq> t"
hoelzl@38656
   770
      and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g -` s) \<inter> t \<in> sets b"
hoelzl@38656
   771
  shows "(g o f) \<in> measurable a c"
hoelzl@38656
   772
proof -
hoelzl@38656
   773
  have fab: "f \<in> (space a -> space b)"
hoelzl@38656
   774
   and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
hoelzl@38656
   775
     by (auto simp add: measurable_def)
hoelzl@38656
   776
  have eq: "f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
hoelzl@38656
   777
    by force
hoelzl@38656
   778
  show ?thesis
hoelzl@38656
   779
    apply (auto simp add: measurable_def vimage_compose a c)
hoelzl@38656
   780
    apply (metis funcset_mem fab g)
hoelzl@38656
   781
    apply (subst eq, metis ba cb)
hoelzl@38656
   782
    done
hoelzl@38656
   783
qed
hoelzl@38656
   784
hoelzl@38656
   785
lemma measurable_mono1:
hoelzl@38656
   786
     "a \<subseteq> b \<Longrightarrow> sigma_algebra \<lparr>space = X, sets = b\<rparr>
hoelzl@38656
   787
      \<Longrightarrow> measurable \<lparr>space = X, sets = a\<rparr> c \<subseteq> measurable \<lparr>space = X, sets = b\<rparr> c"
hoelzl@38656
   788
  by (auto simp add: measurable_def)
hoelzl@38656
   789
hoelzl@38656
   790
lemma measurable_up_sigma:
hoelzl@40859
   791
  "measurable A M \<subseteq> measurable (sigma A) M"
hoelzl@38656
   792
  unfolding measurable_def
hoelzl@38656
   793
  by (auto simp: sigma_def intro: sigma_sets.Basic)
hoelzl@38656
   794
hoelzl@38656
   795
lemma (in sigma_algebra) measurable_range_reduce:
hoelzl@38656
   796
   "\<lbrakk> f \<in> measurable M \<lparr>space = s, sets = Pow s\<rparr> ; s \<noteq> {} \<rbrakk>
hoelzl@38656
   797
    \<Longrightarrow> f \<in> measurable M \<lparr>space = s \<inter> (f ` space M), sets = Pow (s \<inter> (f ` space M))\<rparr>"
hoelzl@38656
   798
  by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast
hoelzl@38656
   799
hoelzl@38656
   800
lemma (in sigma_algebra) measurable_Pow_to_Pow:
hoelzl@38656
   801
   "(sets M = Pow (space M)) \<Longrightarrow> f \<in> measurable M \<lparr>space = UNIV, sets = Pow UNIV\<rparr>"
hoelzl@38656
   802
  by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def)
hoelzl@38656
   803
hoelzl@38656
   804
lemma (in sigma_algebra) measurable_Pow_to_Pow_image:
hoelzl@38656
   805
   "sets M = Pow (space M)
hoelzl@38656
   806
    \<Longrightarrow> f \<in> measurable M \<lparr>space = f ` space M, sets = Pow (f ` space M)\<rparr>"
hoelzl@38656
   807
  by (simp add: measurable_def sigma_algebra_Pow) intro_locales
hoelzl@38656
   808
hoelzl@40859
   809
lemma (in sigma_algebra) measurable_iff_sigma:
hoelzl@40859
   810
  assumes "sets E \<subseteq> Pow (space E)" and "f \<in> space M \<rightarrow> space E"
hoelzl@40859
   811
  shows "f \<in> measurable M (sigma E) \<longleftrightarrow> (\<forall>A\<in>sets E. f -` A \<inter> space M \<in> sets M)"
hoelzl@40859
   812
  using measurable_sigma[OF assms]
nipkow@44890
   813
  by (fastforce simp: measurable_def sets_sigma intro: sigma_sets.intros)
hoelzl@38656
   814
hoelzl@38656
   815
section "Disjoint families"
hoelzl@38656
   816
hoelzl@38656
   817
definition
hoelzl@38656
   818
  disjoint_family_on  where
hoelzl@38656
   819
  "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
   820
hoelzl@38656
   821
abbreviation
hoelzl@38656
   822
  "disjoint_family A \<equiv> disjoint_family_on A UNIV"
hoelzl@38656
   823
hoelzl@38656
   824
lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
hoelzl@38656
   825
  by blast
hoelzl@38656
   826
hoelzl@38656
   827
lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
hoelzl@38656
   828
  by blast
hoelzl@38656
   829
hoelzl@38656
   830
lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
hoelzl@38656
   831
  by blast
hoelzl@38656
   832
hoelzl@38656
   833
lemma disjoint_family_subset:
hoelzl@38656
   834
     "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
hoelzl@38656
   835
  by (force simp add: disjoint_family_on_def)
hoelzl@38656
   836
hoelzl@40859
   837
lemma disjoint_family_on_bisimulation:
hoelzl@40859
   838
  assumes "disjoint_family_on f S"
hoelzl@40859
   839
  and "\<And>n m. n \<in> S \<Longrightarrow> m \<in> S \<Longrightarrow> n \<noteq> m \<Longrightarrow> f n \<inter> f m = {} \<Longrightarrow> g n \<inter> g m = {}"
hoelzl@40859
   840
  shows "disjoint_family_on g S"
hoelzl@40859
   841
  using assms unfolding disjoint_family_on_def by auto
hoelzl@40859
   842
hoelzl@38656
   843
lemma disjoint_family_on_mono:
hoelzl@38656
   844
  "A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A"
hoelzl@38656
   845
  unfolding disjoint_family_on_def by auto
hoelzl@38656
   846
hoelzl@38656
   847
lemma disjoint_family_Suc:
hoelzl@38656
   848
  assumes Suc: "!!n. A n \<subseteq> A (Suc n)"
hoelzl@38656
   849
  shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
hoelzl@38656
   850
proof -
hoelzl@38656
   851
  {
hoelzl@38656
   852
    fix m
hoelzl@38656
   853
    have "!!n. A n \<subseteq> A (m+n)"
hoelzl@38656
   854
    proof (induct m)
hoelzl@38656
   855
      case 0 show ?case by simp
hoelzl@38656
   856
    next
hoelzl@38656
   857
      case (Suc m) thus ?case
hoelzl@38656
   858
        by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
hoelzl@38656
   859
    qed
hoelzl@38656
   860
  }
hoelzl@38656
   861
  hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
hoelzl@38656
   862
    by (metis add_commute le_add_diff_inverse nat_less_le)
hoelzl@38656
   863
  thus ?thesis
hoelzl@38656
   864
    by (auto simp add: disjoint_family_on_def)
hoelzl@38656
   865
      (metis insert_absorb insert_subset le_SucE le_antisym not_leE)
hoelzl@38656
   866
qed
hoelzl@38656
   867
hoelzl@39092
   868
lemma setsum_indicator_disjoint_family:
hoelzl@39092
   869
  fixes f :: "'d \<Rightarrow> 'e::semiring_1"
hoelzl@39092
   870
  assumes d: "disjoint_family_on A P" and "x \<in> A j" and "finite P" and "j \<in> P"
hoelzl@39092
   871
  shows "(\<Sum>i\<in>P. f i * indicator (A i) x) = f j"
hoelzl@39092
   872
proof -
hoelzl@39092
   873
  have "P \<inter> {i. x \<in> A i} = {j}"
hoelzl@39092
   874
    using d `x \<in> A j` `j \<in> P` unfolding disjoint_family_on_def
hoelzl@39092
   875
    by auto
hoelzl@39092
   876
  thus ?thesis
hoelzl@39092
   877
    unfolding indicator_def
hoelzl@39092
   878
    by (simp add: if_distrib setsum_cases[OF `finite P`])
hoelzl@39092
   879
qed
hoelzl@39092
   880
hoelzl@38656
   881
definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
hoelzl@38656
   882
  where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
hoelzl@38656
   883
hoelzl@38656
   884
lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
hoelzl@38656
   885
proof (induct n)
hoelzl@38656
   886
  case 0 show ?case by simp
hoelzl@38656
   887
next
hoelzl@38656
   888
  case (Suc n)
hoelzl@38656
   889
  thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
hoelzl@38656
   890
qed
hoelzl@38656
   891
hoelzl@38656
   892
lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
hoelzl@38656
   893
  apply (rule UN_finite2_eq [where k=0])
hoelzl@38656
   894
  apply (simp add: finite_UN_disjointed_eq)
hoelzl@38656
   895
  done
hoelzl@38656
   896
hoelzl@38656
   897
lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
hoelzl@38656
   898
  by (auto simp add: disjointed_def)
hoelzl@38656
   899
hoelzl@38656
   900
lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
hoelzl@38656
   901
  by (simp add: disjoint_family_on_def)
hoelzl@38656
   902
     (metis neq_iff Int_commute less_disjoint_disjointed)
hoelzl@38656
   903
hoelzl@38656
   904
lemma disjointed_subset: "disjointed A n \<subseteq> A n"
hoelzl@38656
   905
  by (auto simp add: disjointed_def)
hoelzl@38656
   906
hoelzl@42065
   907
lemma (in ring_of_sets) UNION_in_sets:
hoelzl@38656
   908
  fixes A:: "nat \<Rightarrow> 'a set"
hoelzl@38656
   909
  assumes A: "range A \<subseteq> sets M "
hoelzl@38656
   910
  shows  "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
hoelzl@38656
   911
proof (induct n)
hoelzl@38656
   912
  case 0 show ?case by simp
hoelzl@38656
   913
next
hoelzl@38656
   914
  case (Suc n)
hoelzl@38656
   915
  thus ?case
hoelzl@38656
   916
    by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
hoelzl@38656
   917
qed
hoelzl@38656
   918
hoelzl@42065
   919
lemma (in ring_of_sets) range_disjointed_sets:
hoelzl@38656
   920
  assumes A: "range A \<subseteq> sets M "
hoelzl@38656
   921
  shows  "range (disjointed A) \<subseteq> sets M"
hoelzl@38656
   922
proof (auto simp add: disjointed_def)
hoelzl@38656
   923
  fix n
hoelzl@38656
   924
  show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets
hoelzl@38656
   925
    by (metis A Diff UNIV_I image_subset_iff)
hoelzl@38656
   926
qed
hoelzl@38656
   927
hoelzl@42065
   928
lemma (in algebra) range_disjointed_sets':
hoelzl@42065
   929
  "range A \<subseteq> sets M \<Longrightarrow> range (disjointed A) \<subseteq> sets M"
hoelzl@42065
   930
  using range_disjointed_sets .
hoelzl@42065
   931
hoelzl@42145
   932
lemma disjointed_0[simp]: "disjointed A 0 = A 0"
hoelzl@42145
   933
  by (simp add: disjointed_def)
hoelzl@42145
   934
hoelzl@42145
   935
lemma incseq_Un:
hoelzl@42145
   936
  "incseq A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
hoelzl@42145
   937
  unfolding incseq_def by auto
hoelzl@42145
   938
hoelzl@42145
   939
lemma disjointed_incseq:
hoelzl@42145
   940
  "incseq A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
hoelzl@42145
   941
  using incseq_Un[of A]
hoelzl@42145
   942
  by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
hoelzl@42145
   943
hoelzl@38656
   944
lemma sigma_algebra_disjoint_iff:
hoelzl@38656
   945
     "sigma_algebra M \<longleftrightarrow>
hoelzl@38656
   946
      algebra M &
hoelzl@38656
   947
      (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow>
hoelzl@38656
   948
           (\<Union>i::nat. A i) \<in> sets M)"
hoelzl@38656
   949
proof (auto simp add: sigma_algebra_iff)
hoelzl@38656
   950
  fix A :: "nat \<Rightarrow> 'a set"
hoelzl@38656
   951
  assume M: "algebra M"
hoelzl@38656
   952
     and A: "range A \<subseteq> sets M"
hoelzl@38656
   953
     and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow>
hoelzl@38656
   954
               disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
hoelzl@38656
   955
  hence "range (disjointed A) \<subseteq> sets M \<longrightarrow>
hoelzl@38656
   956
         disjoint_family (disjointed A) \<longrightarrow>
hoelzl@38656
   957
         (\<Union>i. disjointed A i) \<in> sets M" by blast
hoelzl@38656
   958
  hence "(\<Union>i. disjointed A i) \<in> sets M"
hoelzl@42065
   959
    by (simp add: algebra.range_disjointed_sets' M A disjoint_family_disjointed)
hoelzl@38656
   960
  thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
hoelzl@38656
   961
qed
hoelzl@38656
   962
hoelzl@39090
   963
subsection {* Sigma algebra generated by function preimages *}
hoelzl@39090
   964
hoelzl@39090
   965
definition (in sigma_algebra)
hoelzl@41689
   966
  "vimage_algebra S f = \<lparr> space = S, sets = (\<lambda>A. f -` A \<inter> S) ` sets M, \<dots> = more M \<rparr>"
hoelzl@39090
   967
hoelzl@39090
   968
lemma (in sigma_algebra) in_vimage_algebra[simp]:
hoelzl@39090
   969
  "A \<in> sets (vimage_algebra S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)"
hoelzl@39090
   970
  by (simp add: vimage_algebra_def image_iff)
hoelzl@39090
   971
hoelzl@39090
   972
lemma (in sigma_algebra) space_vimage_algebra[simp]:
hoelzl@39090
   973
  "space (vimage_algebra S f) = S"
hoelzl@39090
   974
  by (simp add: vimage_algebra_def)
hoelzl@39090
   975
hoelzl@40859
   976
lemma (in sigma_algebra) sigma_algebra_preimages:
hoelzl@40859
   977
  fixes f :: "'x \<Rightarrow> 'a"
hoelzl@40859
   978
  assumes "f \<in> A \<rightarrow> space M"
hoelzl@40859
   979
  shows "sigma_algebra \<lparr> space = A, sets = (\<lambda>M. f -` M \<inter> A) ` sets M \<rparr>"
hoelzl@40859
   980
    (is "sigma_algebra \<lparr> space = _, sets = ?F ` sets M \<rparr>")
hoelzl@40859
   981
proof (simp add: sigma_algebra_iff2, safe)
hoelzl@40859
   982
  show "{} \<in> ?F ` sets M" by blast
hoelzl@40859
   983
next
hoelzl@40859
   984
  fix S assume "S \<in> sets M"
hoelzl@40859
   985
  moreover have "A - ?F S = ?F (space M - S)"
hoelzl@40859
   986
    using assms by auto
hoelzl@40859
   987
  ultimately show "A - ?F S \<in> ?F ` sets M"
hoelzl@40859
   988
    by blast
hoelzl@40859
   989
next
hoelzl@40859
   990
  fix S :: "nat \<Rightarrow> 'x set" assume *: "range S \<subseteq> ?F ` sets M"
hoelzl@40859
   991
  have "\<forall>i. \<exists>b. b \<in> sets M \<and> S i = ?F b"
hoelzl@40859
   992
  proof safe
hoelzl@40859
   993
    fix i
hoelzl@40859
   994
    have "S i \<in> ?F ` sets M" using * by auto
hoelzl@40859
   995
    then show "\<exists>b. b \<in> sets M \<and> S i = ?F b" by auto
hoelzl@40859
   996
  qed
hoelzl@40859
   997
  from choice[OF this] obtain b where b: "range b \<subseteq> sets M" "\<And>i. S i = ?F (b i)"
hoelzl@40859
   998
    by auto
hoelzl@40859
   999
  then have "(\<Union>i. S i) = ?F (\<Union>i. b i)" by auto
hoelzl@40859
  1000
  then show "(\<Union>i. S i) \<in> ?F ` sets M" using b(1) by blast
hoelzl@40859
  1001
qed
hoelzl@40859
  1002
hoelzl@39090
  1003
lemma (in sigma_algebra) sigma_algebra_vimage:
hoelzl@39090
  1004
  fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
hoelzl@39090
  1005
  shows "sigma_algebra (vimage_algebra S f)"
hoelzl@40859
  1006
proof -
hoelzl@40859
  1007
  from sigma_algebra_preimages[OF assms]
hoelzl@40859
  1008
  show ?thesis unfolding vimage_algebra_def by (auto simp: sigma_algebra_iff2)
hoelzl@40859
  1009
qed
hoelzl@39090
  1010
hoelzl@39090
  1011
lemma (in sigma_algebra) measurable_vimage_algebra:
hoelzl@39090
  1012
  fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
hoelzl@39090
  1013
  shows "f \<in> measurable (vimage_algebra S f) M"
hoelzl@39090
  1014
    unfolding measurable_def using assms by force
hoelzl@39090
  1015
hoelzl@40859
  1016
lemma (in sigma_algebra) measurable_vimage:
hoelzl@40859
  1017
  fixes g :: "'a \<Rightarrow> 'c" and f :: "'d \<Rightarrow> 'a"
hoelzl@40859
  1018
  assumes "g \<in> measurable M M2" "f \<in> S \<rightarrow> space M"
hoelzl@40859
  1019
  shows "(\<lambda>x. g (f x)) \<in> measurable (vimage_algebra S f) M2"
hoelzl@40859
  1020
proof -
hoelzl@40859
  1021
  note measurable_vimage_algebra[OF assms(2)]
hoelzl@40859
  1022
  from measurable_comp[OF this assms(1)]
hoelzl@40859
  1023
  show ?thesis by (simp add: comp_def)
hoelzl@40859
  1024
qed
hoelzl@40859
  1025
hoelzl@40859
  1026
lemma sigma_sets_vimage:
hoelzl@40859
  1027
  assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S"
hoelzl@40859
  1028
  shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A"
hoelzl@40859
  1029
proof (intro set_eqI iffI)
hoelzl@40859
  1030
  let ?F = "\<lambda>X. f -` X \<inter> S'"
hoelzl@40859
  1031
  fix X assume "X \<in> sigma_sets S' (?F ` A)"
hoelzl@40859
  1032
  then show "X \<in> ?F ` sigma_sets S A"
hoelzl@40859
  1033
  proof induct
hoelzl@40859
  1034
    case (Basic X) then obtain X' where "X = ?F X'" "X' \<in> A"
hoelzl@40859
  1035
      by auto
hoelzl@40859
  1036
    then show ?case by (auto intro!: sigma_sets.Basic)
hoelzl@40859
  1037
  next
hoelzl@40859
  1038
    case Empty then show ?case
hoelzl@40859
  1039
      by (auto intro!: image_eqI[of _ _ "{}"] sigma_sets.Empty)
hoelzl@40859
  1040
  next
hoelzl@40859
  1041
    case (Compl X) then obtain X' where X: "X = ?F X'" and "X' \<in> sigma_sets S A"
hoelzl@40859
  1042
      by auto
hoelzl@40859
  1043
    then have "S - X' \<in> sigma_sets S A"
hoelzl@40859
  1044
      by (auto intro!: sigma_sets.Compl)
hoelzl@40859
  1045
    then show ?case
hoelzl@40859
  1046
      using X assms by (auto intro!: image_eqI[where x="S - X'"])
hoelzl@40859
  1047
  next
hoelzl@40859
  1048
    case (Union F)
hoelzl@40859
  1049
    then have "\<forall>i. \<exists>F'.  F' \<in> sigma_sets S A \<and> F i = f -` F' \<inter> S'"
hoelzl@40859
  1050
      by (auto simp: image_iff Bex_def)
hoelzl@40859
  1051
    from choice[OF this] obtain F' where
hoelzl@40859
  1052
      "\<And>i. F' i \<in> sigma_sets S A" and "\<And>i. F i = f -` F' i \<inter> S'"
hoelzl@40859
  1053
      by auto
hoelzl@40859
  1054
    then show ?case
hoelzl@40859
  1055
      by (auto intro!: sigma_sets.Union image_eqI[where x="\<Union>i. F' i"])
hoelzl@40859
  1056
  qed
hoelzl@40859
  1057
next
hoelzl@40859
  1058
  let ?F = "\<lambda>X. f -` X \<inter> S'"
hoelzl@40859
  1059
  fix X assume "X \<in> ?F ` sigma_sets S A"
hoelzl@40859
  1060
  then obtain X' where "X' \<in> sigma_sets S A" "X = ?F X'" by auto
hoelzl@40859
  1061
  then show "X \<in> sigma_sets S' (?F ` A)"
hoelzl@40859
  1062
  proof (induct arbitrary: X)
hoelzl@40859
  1063
    case (Basic X') then show ?case by (auto intro: sigma_sets.Basic)
hoelzl@40859
  1064
  next
hoelzl@40859
  1065
    case Empty then show ?case by (auto intro: sigma_sets.Empty)
hoelzl@40859
  1066
  next
hoelzl@40859
  1067
    case (Compl X')
hoelzl@40859
  1068
    have "S' - (S' - X) \<in> sigma_sets S' (?F ` A)"
hoelzl@40859
  1069
      apply (rule sigma_sets.Compl)
hoelzl@40859
  1070
      using assms by (auto intro!: Compl.hyps simp: Compl.prems)
hoelzl@40859
  1071
    also have "S' - (S' - X) = X"
hoelzl@40859
  1072
      using assms Compl by auto
hoelzl@40859
  1073
    finally show ?case .
hoelzl@40859
  1074
  next
hoelzl@40859
  1075
    case (Union F)
hoelzl@40859
  1076
    have "(\<Union>i. f -` F i \<inter> S') \<in> sigma_sets S' (?F ` A)"
hoelzl@40859
  1077
      by (intro sigma_sets.Union Union.hyps) simp
hoelzl@40859
  1078
    also have "(\<Union>i. f -` F i \<inter> S') = X"
hoelzl@40859
  1079
      using assms Union by auto
hoelzl@40859
  1080
    finally show ?case .
hoelzl@40859
  1081
  qed
hoelzl@40859
  1082
qed
hoelzl@40859
  1083
hoelzl@39092
  1084
section {* Conditional space *}
hoelzl@39092
  1085
hoelzl@39092
  1086
definition (in algebra)
hoelzl@41689
  1087
  "image_space X = \<lparr> space = X`space M, sets = (\<lambda>S. X`S) ` sets M, \<dots> = more M \<rparr>"
hoelzl@39092
  1088
hoelzl@39092
  1089
definition (in algebra)
hoelzl@39092
  1090
  "conditional_space X A = algebra.image_space (restricted_space A) X"
hoelzl@39092
  1091
hoelzl@39092
  1092
lemma (in algebra) space_conditional_space:
hoelzl@39092
  1093
  assumes "A \<in> sets M" shows "space (conditional_space X A) = X`A"
hoelzl@39092
  1094
proof -
hoelzl@39092
  1095
  interpret r: algebra "restricted_space A" using assms by (rule restricted_algebra)
hoelzl@39092
  1096
  show ?thesis unfolding conditional_space_def r.image_space_def
hoelzl@39092
  1097
    by simp
hoelzl@39092
  1098
qed
hoelzl@39092
  1099
hoelzl@38656
  1100
subsection {* A Two-Element Series *}
hoelzl@38656
  1101
hoelzl@38656
  1102
definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
hoelzl@38656
  1103
  where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
hoelzl@38656
  1104
hoelzl@38656
  1105
lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
hoelzl@38656
  1106
  apply (simp add: binaryset_def)
nipkow@39302
  1107
  apply (rule set_eqI)
hoelzl@38656
  1108
  apply (auto simp add: image_iff)
hoelzl@38656
  1109
  done
hoelzl@38656
  1110
hoelzl@38656
  1111
lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
haftmann@44106
  1112
  by (simp add: SUP_def range_binaryset_eq)
hoelzl@38656
  1113
hoelzl@38656
  1114
section {* Closed CDI *}
hoelzl@38656
  1115
hoelzl@38656
  1116
definition
hoelzl@38656
  1117
  closed_cdi  where
hoelzl@38656
  1118
  "closed_cdi M \<longleftrightarrow>
hoelzl@38656
  1119
   sets M \<subseteq> Pow (space M) &
hoelzl@38656
  1120
   (\<forall>s \<in> sets M. space M - s \<in> sets M) &
hoelzl@38656
  1121
   (\<forall>A. (range A \<subseteq> sets M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
hoelzl@38656
  1122
        (\<Union>i. A i) \<in> sets M) &
hoelzl@38656
  1123
   (\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
hoelzl@38656
  1124
hoelzl@38656
  1125
inductive_set
hoelzl@38656
  1126
  smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
hoelzl@38656
  1127
  for M
hoelzl@38656
  1128
  where
hoelzl@38656
  1129
    Basic [intro]:
hoelzl@38656
  1130
      "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M"
hoelzl@38656
  1131
  | Compl [intro]:
hoelzl@38656
  1132
      "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M"
hoelzl@38656
  1133
  | Inc:
hoelzl@38656
  1134
      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n))
hoelzl@38656
  1135
       \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets M"
hoelzl@38656
  1136
  | Disj:
hoelzl@38656
  1137
      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A
hoelzl@38656
  1138
       \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets M"
hoelzl@38656
  1139
hoelzl@38656
  1140
hoelzl@38656
  1141
definition
hoelzl@38656
  1142
  smallest_closed_cdi  where
hoelzl@38656
  1143
  "smallest_closed_cdi M = (|space = space M, sets = smallest_ccdi_sets M|)"
hoelzl@38656
  1144
hoelzl@38656
  1145
lemma space_smallest_closed_cdi [simp]:
hoelzl@38656
  1146
     "space (smallest_closed_cdi M) = space M"
hoelzl@38656
  1147
  by (simp add: smallest_closed_cdi_def)
hoelzl@38656
  1148
hoelzl@38656
  1149
lemma (in algebra) smallest_closed_cdi1: "sets M \<subseteq> sets (smallest_closed_cdi M)"
hoelzl@38656
  1150
  by (auto simp add: smallest_closed_cdi_def)
hoelzl@38656
  1151
hoelzl@38656
  1152
lemma (in algebra) smallest_ccdi_sets:
hoelzl@38656
  1153
     "smallest_ccdi_sets M \<subseteq> Pow (space M)"
hoelzl@38656
  1154
  apply (rule subsetI)
hoelzl@38656
  1155
  apply (erule smallest_ccdi_sets.induct)
hoelzl@38656
  1156
  apply (auto intro: range_subsetD dest: sets_into_space)
hoelzl@38656
  1157
  done
hoelzl@38656
  1158
hoelzl@38656
  1159
lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)"
hoelzl@38656
  1160
  apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets)
hoelzl@38656
  1161
  apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) +
hoelzl@38656
  1162
  done
hoelzl@38656
  1163
hoelzl@38656
  1164
lemma (in algebra) smallest_closed_cdi3:
hoelzl@38656
  1165
     "sets (smallest_closed_cdi M) \<subseteq> Pow (space M)"
hoelzl@38656
  1166
  by (simp add: smallest_closed_cdi_def smallest_ccdi_sets)
hoelzl@38656
  1167
hoelzl@38656
  1168
lemma closed_cdi_subset: "closed_cdi M \<Longrightarrow> sets M \<subseteq> Pow (space M)"
hoelzl@38656
  1169
  by (simp add: closed_cdi_def)
hoelzl@38656
  1170
hoelzl@38656
  1171
lemma closed_cdi_Compl: "closed_cdi M \<Longrightarrow> s \<in> sets M \<Longrightarrow> space M - s \<in> sets M"
hoelzl@38656
  1172
  by (simp add: closed_cdi_def)
hoelzl@38656
  1173
hoelzl@38656
  1174
lemma closed_cdi_Inc:
hoelzl@38656
  1175
     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow>
hoelzl@38656
  1176
        (\<Union>i. A i) \<in> sets M"
hoelzl@38656
  1177
  by (simp add: closed_cdi_def)
hoelzl@38656
  1178
hoelzl@38656
  1179
lemma closed_cdi_Disj:
hoelzl@38656
  1180
     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
hoelzl@38656
  1181
  by (simp add: closed_cdi_def)
hoelzl@38656
  1182
hoelzl@38656
  1183
lemma closed_cdi_Un:
hoelzl@38656
  1184
  assumes cdi: "closed_cdi M" and empty: "{} \<in> sets M"
hoelzl@38656
  1185
      and A: "A \<in> sets M" and B: "B \<in> sets M"
hoelzl@38656
  1186
      and disj: "A \<inter> B = {}"
hoelzl@38656
  1187
    shows "A \<union> B \<in> sets M"
hoelzl@38656
  1188
proof -
hoelzl@38656
  1189
  have ra: "range (binaryset A B) \<subseteq> sets M"
hoelzl@38656
  1190
   by (simp add: range_binaryset_eq empty A B)
hoelzl@38656
  1191
 have di:  "disjoint_family (binaryset A B)" using disj
hoelzl@38656
  1192
   by (simp add: disjoint_family_on_def binaryset_def Int_commute)
hoelzl@38656
  1193
 from closed_cdi_Disj [OF cdi ra di]
hoelzl@38656
  1194
 show ?thesis
hoelzl@38656
  1195
   by (simp add: UN_binaryset_eq)
hoelzl@38656
  1196
qed
hoelzl@38656
  1197
hoelzl@38656
  1198
lemma (in algebra) smallest_ccdi_sets_Un:
hoelzl@38656
  1199
  assumes A: "A \<in> smallest_ccdi_sets M" and B: "B \<in> smallest_ccdi_sets M"
hoelzl@38656
  1200
      and disj: "A \<inter> B = {}"
hoelzl@38656
  1201
    shows "A \<union> B \<in> smallest_ccdi_sets M"
hoelzl@38656
  1202
proof -
hoelzl@38656
  1203
  have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)"
hoelzl@38656
  1204
    by (simp add: range_binaryset_eq  A B smallest_ccdi_sets.Basic)
hoelzl@38656
  1205
  have di:  "disjoint_family (binaryset A B)" using disj
hoelzl@38656
  1206
    by (simp add: disjoint_family_on_def binaryset_def Int_commute)
hoelzl@38656
  1207
  from Disj [OF ra di]
hoelzl@38656
  1208
  show ?thesis
hoelzl@38656
  1209
    by (simp add: UN_binaryset_eq)
hoelzl@38656
  1210
qed
hoelzl@38656
  1211
hoelzl@38656
  1212
lemma (in algebra) smallest_ccdi_sets_Int1:
hoelzl@38656
  1213
  assumes a: "a \<in> sets M"
hoelzl@38656
  1214
  shows "b \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
hoelzl@38656
  1215
proof (induct rule: smallest_ccdi_sets.induct)
hoelzl@38656
  1216
  case (Basic x)
hoelzl@38656
  1217
  thus ?case
hoelzl@38656
  1218
    by (metis a Int smallest_ccdi_sets.Basic)
hoelzl@38656
  1219
next
hoelzl@38656
  1220
  case (Compl x)
hoelzl@38656
  1221
  have "a \<inter> (space M - x) = space M - ((space M - a) \<union> (a \<inter> x))"
hoelzl@38656
  1222
    by blast
hoelzl@38656
  1223
  also have "... \<in> smallest_ccdi_sets M"
hoelzl@38656
  1224
    by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2
hoelzl@38656
  1225
           Diff_disjoint Int_Diff Int_empty_right Un_commute
hoelzl@38656
  1226
           smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl
hoelzl@38656
  1227
           smallest_ccdi_sets_Un)
hoelzl@38656
  1228
  finally show ?case .
hoelzl@38656
  1229
next
hoelzl@38656
  1230
  case (Inc A)
hoelzl@38656
  1231
  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
hoelzl@38656
  1232
    by blast
hoelzl@38656
  1233
  have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Inc
hoelzl@38656
  1234
    by blast
hoelzl@38656
  1235
  moreover have "(\<lambda>i. a \<inter> A i) 0 = {}"
hoelzl@38656
  1236
    by (simp add: Inc)
hoelzl@38656
  1237
  moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc
hoelzl@38656
  1238
    by blast
hoelzl@38656
  1239
  ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
hoelzl@38656
  1240
    by (rule smallest_ccdi_sets.Inc)
hoelzl@38656
  1241
  show ?case
hoelzl@38656
  1242
    by (metis 1 2)
hoelzl@38656
  1243
next
hoelzl@38656
  1244
  case (Disj A)
hoelzl@38656
  1245
  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
hoelzl@38656
  1246
    by blast
hoelzl@38656
  1247
  have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj
hoelzl@38656
  1248
    by blast
hoelzl@38656
  1249
  moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj
hoelzl@38656
  1250
    by (auto simp add: disjoint_family_on_def)
hoelzl@38656
  1251
  ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
hoelzl@38656
  1252
    by (rule smallest_ccdi_sets.Disj)
hoelzl@38656
  1253
  show ?case
hoelzl@38656
  1254
    by (metis 1 2)
hoelzl@38656
  1255
qed
hoelzl@38656
  1256
hoelzl@38656
  1257
hoelzl@38656
  1258
lemma (in algebra) smallest_ccdi_sets_Int:
hoelzl@38656
  1259
  assumes b: "b \<in> smallest_ccdi_sets M"
hoelzl@38656
  1260
  shows "a \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
hoelzl@38656
  1261
proof (induct rule: smallest_ccdi_sets.induct)
hoelzl@38656
  1262
  case (Basic x)
hoelzl@38656
  1263
  thus ?case
hoelzl@38656
  1264
    by (metis b smallest_ccdi_sets_Int1)
hoelzl@38656
  1265
next
hoelzl@38656
  1266
  case (Compl x)
hoelzl@38656
  1267
  have "(space M - x) \<inter> b = space M - (x \<inter> b \<union> (space M - b))"
hoelzl@38656
  1268
    by blast
hoelzl@38656
  1269
  also have "... \<in> smallest_ccdi_sets M"
hoelzl@38656
  1270
    by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b
hoelzl@38656
  1271
           smallest_ccdi_sets.Compl smallest_ccdi_sets_Un)
hoelzl@38656
  1272
  finally show ?case .
hoelzl@38656
  1273
next
hoelzl@38656
  1274
  case (Inc A)
hoelzl@38656
  1275
  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
hoelzl@38656
  1276
    by blast
hoelzl@38656
  1277
  have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Inc
hoelzl@38656
  1278
    by blast
hoelzl@38656
  1279
  moreover have "(\<lambda>i. A i \<inter> b) 0 = {}"
hoelzl@38656
  1280
    by (simp add: Inc)
hoelzl@38656
  1281
  moreover have "!!n. (\<lambda>i. A i \<inter> b) n \<subseteq> (\<lambda>i. A i \<inter> b) (Suc n)" using Inc
hoelzl@38656
  1282
    by blast
hoelzl@38656
  1283
  ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
hoelzl@38656
  1284
    by (rule smallest_ccdi_sets.Inc)
hoelzl@38656
  1285
  show ?case
hoelzl@38656
  1286
    by (metis 1 2)
hoelzl@38656
  1287
next
hoelzl@38656
  1288
  case (Disj A)
hoelzl@38656
  1289
  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
hoelzl@38656
  1290
    by blast
hoelzl@38656
  1291
  have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj
hoelzl@38656
  1292
    by blast
hoelzl@38656
  1293
  moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj
hoelzl@38656
  1294
    by (auto simp add: disjoint_family_on_def)
hoelzl@38656
  1295
  ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
hoelzl@38656
  1296
    by (rule smallest_ccdi_sets.Disj)
hoelzl@38656
  1297
  show ?case
hoelzl@38656
  1298
    by (metis 1 2)
hoelzl@38656
  1299
qed
hoelzl@38656
  1300
hoelzl@38656
  1301
lemma (in algebra) sets_smallest_closed_cdi_Int:
hoelzl@38656
  1302
   "a \<in> sets (smallest_closed_cdi M) \<Longrightarrow> b \<in> sets (smallest_closed_cdi M)
hoelzl@38656
  1303
    \<Longrightarrow> a \<inter> b \<in> sets (smallest_closed_cdi M)"
hoelzl@38656
  1304
  by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def)
hoelzl@38656
  1305
hoelzl@38656
  1306
lemma (in algebra) sigma_property_disjoint_lemma:
hoelzl@38656
  1307
  assumes sbC: "sets M \<subseteq> C"
hoelzl@38656
  1308
      and ccdi: "closed_cdi (|space = space M, sets = C|)"
hoelzl@38656
  1309
  shows "sigma_sets (space M) (sets M) \<subseteq> C"
hoelzl@38656
  1310
proof -
hoelzl@38656
  1311
  have "smallest_ccdi_sets M \<in> {B . sets M \<subseteq> B \<and> sigma_algebra (|space = space M, sets = B|)}"
hoelzl@38656
  1312
    apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int
hoelzl@38656
  1313
            smallest_ccdi_sets_Int)
hoelzl@38656
  1314
    apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets)
hoelzl@38656
  1315
    apply (blast intro: smallest_ccdi_sets.Disj)
hoelzl@38656
  1316
    done
hoelzl@38656
  1317
  hence "sigma_sets (space M) (sets M) \<subseteq> smallest_ccdi_sets M"
hoelzl@38656
  1318
    by clarsimp
hoelzl@38656
  1319
       (drule sigma_algebra.sigma_sets_subset [where a="sets M"], auto)
hoelzl@38656
  1320
  also have "...  \<subseteq> C"
hoelzl@38656
  1321
    proof
hoelzl@38656
  1322
      fix x
hoelzl@38656
  1323
      assume x: "x \<in> smallest_ccdi_sets M"
hoelzl@38656
  1324
      thus "x \<in> C"
hoelzl@38656
  1325
        proof (induct rule: smallest_ccdi_sets.induct)
hoelzl@38656
  1326
          case (Basic x)
hoelzl@38656
  1327
          thus ?case
hoelzl@38656
  1328
            by (metis Basic subsetD sbC)
hoelzl@38656
  1329
        next
hoelzl@38656
  1330
          case (Compl x)
hoelzl@38656
  1331
          thus ?case
hoelzl@38656
  1332
            by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
hoelzl@38656
  1333
        next
hoelzl@38656
  1334
          case (Inc A)
hoelzl@38656
  1335
          thus ?case
hoelzl@38656
  1336
               by (auto intro: closed_cdi_Inc [OF ccdi, simplified])
hoelzl@38656
  1337
        next
hoelzl@38656
  1338
          case (Disj A)
hoelzl@38656
  1339
          thus ?case
hoelzl@38656
  1340
               by (auto intro: closed_cdi_Disj [OF ccdi, simplified])
hoelzl@38656
  1341
        qed
hoelzl@38656
  1342
    qed
hoelzl@38656
  1343
  finally show ?thesis .
hoelzl@38656
  1344
qed
hoelzl@38656
  1345
hoelzl@38656
  1346
lemma (in algebra) sigma_property_disjoint:
hoelzl@38656
  1347
  assumes sbC: "sets M \<subseteq> C"
hoelzl@38656
  1348
      and compl: "!!s. s \<in> C \<inter> sigma_sets (space M) (sets M) \<Longrightarrow> space M - s \<in> C"
hoelzl@38656
  1349
      and inc: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
hoelzl@38656
  1350
                     \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n))
hoelzl@38656
  1351
                     \<Longrightarrow> (\<Union>i. A i) \<in> C"
hoelzl@38656
  1352
      and disj: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
hoelzl@38656
  1353
                      \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C"
hoelzl@38656
  1354
  shows "sigma_sets (space M) (sets M) \<subseteq> C"
hoelzl@38656
  1355
proof -
hoelzl@38656
  1356
  have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
hoelzl@38656
  1357
    proof (rule sigma_property_disjoint_lemma)
hoelzl@38656
  1358
      show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
hoelzl@38656
  1359
        by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
hoelzl@38656
  1360
    next
hoelzl@38656
  1361
      show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
hoelzl@38656
  1362
        by (simp add: closed_cdi_def compl inc disj)
hoelzl@38656
  1363
           (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
hoelzl@38656
  1364
             IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
hoelzl@38656
  1365
    qed
hoelzl@38656
  1366
  thus ?thesis
hoelzl@38656
  1367
    by blast
hoelzl@38656
  1368
qed
hoelzl@38656
  1369
hoelzl@40859
  1370
section {* Dynkin systems *}
hoelzl@40859
  1371
hoelzl@42065
  1372
locale dynkin_system = subset_class +
hoelzl@42065
  1373
  assumes space: "space M \<in> sets M"
hoelzl@40859
  1374
    and   compl[intro!]: "\<And>A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
hoelzl@40859
  1375
    and   UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
hoelzl@40859
  1376
                           \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
hoelzl@40859
  1377
hoelzl@40859
  1378
lemma (in dynkin_system) empty[intro, simp]: "{} \<in> sets M"
hoelzl@40859
  1379
  using space compl[of "space M"] by simp
hoelzl@40859
  1380
hoelzl@40859
  1381
lemma (in dynkin_system) diff:
hoelzl@40859
  1382
  assumes sets: "D \<in> sets M" "E \<in> sets M" and "D \<subseteq> E"
hoelzl@40859
  1383
  shows "E - D \<in> sets M"
hoelzl@40859
  1384
proof -
hoelzl@40859
  1385
  let ?f = "\<lambda>x. if x = 0 then D else if x = Suc 0 then space M - E else {}"
hoelzl@40859
  1386
  have "range ?f = {D, space M - E, {}}"
hoelzl@40859
  1387
    by (auto simp: image_iff)
hoelzl@40859
  1388
  moreover have "D \<union> (space M - E) = (\<Union>i. ?f i)"
hoelzl@40859
  1389
    by (auto simp: image_iff split: split_if_asm)
hoelzl@40859
  1390
  moreover
hoelzl@40859
  1391
  then have "disjoint_family ?f" unfolding disjoint_family_on_def
hoelzl@40859
  1392
    using `D \<in> sets M`[THEN sets_into_space] `D \<subseteq> E` by auto
hoelzl@40859
  1393
  ultimately have "space M - (D \<union> (space M - E)) \<in> sets M"
hoelzl@40859
  1394
    using sets by auto
hoelzl@40859
  1395
  also have "space M - (D \<union> (space M - E)) = E - D"
hoelzl@40859
  1396
    using assms sets_into_space by auto
hoelzl@40859
  1397
  finally show ?thesis .
hoelzl@40859
  1398
qed
hoelzl@40859
  1399
hoelzl@40859
  1400
lemma dynkin_systemI:
hoelzl@40859
  1401
  assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M" "space M \<in> sets M"
hoelzl@40859
  1402
  assumes "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
hoelzl@40859
  1403
  assumes "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
hoelzl@40859
  1404
          \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
hoelzl@40859
  1405
  shows "dynkin_system M"
hoelzl@42065
  1406
  using assms by (auto simp: dynkin_system_def dynkin_system_axioms_def subset_class_def)
hoelzl@40859
  1407
hoelzl@42988
  1408
lemma dynkin_systemI':
hoelzl@42988
  1409
  assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
hoelzl@42988
  1410
  assumes empty: "{} \<in> sets M"
hoelzl@42988
  1411
  assumes Diff: "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
hoelzl@42988
  1412
  assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
hoelzl@42988
  1413
          \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
hoelzl@42988
  1414
  shows "dynkin_system M"
hoelzl@42988
  1415
proof -
hoelzl@42988
  1416
  from Diff[OF empty] have "space M \<in> sets M" by auto
hoelzl@42988
  1417
  from 1 this Diff 2 show ?thesis
hoelzl@42988
  1418
    by (intro dynkin_systemI) auto
hoelzl@42988
  1419
qed
hoelzl@42988
  1420
hoelzl@40859
  1421
lemma dynkin_system_trivial:
hoelzl@40859
  1422
  shows "dynkin_system \<lparr> space = A, sets = Pow A \<rparr>"
hoelzl@40859
  1423
  by (rule dynkin_systemI) auto
hoelzl@40859
  1424
hoelzl@40859
  1425
lemma sigma_algebra_imp_dynkin_system:
hoelzl@40859
  1426
  assumes "sigma_algebra M" shows "dynkin_system M"
hoelzl@40859
  1427
proof -
hoelzl@40859
  1428
  interpret sigma_algebra M by fact
nipkow@44890
  1429
  show ?thesis using sets_into_space by (fastforce intro!: dynkin_systemI)
hoelzl@40859
  1430
qed
hoelzl@40859
  1431
hoelzl@40859
  1432
subsection "Intersection stable algebras"
hoelzl@40859
  1433
hoelzl@40859
  1434
definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
hoelzl@40859
  1435
hoelzl@40859
  1436
lemma (in algebra) Int_stable: "Int_stable M"
hoelzl@40859
  1437
  unfolding Int_stable_def by auto
hoelzl@40859
  1438
hoelzl@42981
  1439
lemma Int_stableI:
hoelzl@42981
  1440
  "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A) \<Longrightarrow> Int_stable \<lparr> space = \<Omega>, sets = A \<rparr>"
hoelzl@42981
  1441
  unfolding Int_stable_def by auto
hoelzl@42981
  1442
hoelzl@42981
  1443
lemma Int_stableD:
hoelzl@42981
  1444
  "Int_stable M \<Longrightarrow> a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b \<in> sets M"
hoelzl@42981
  1445
  unfolding Int_stable_def by auto
hoelzl@42981
  1446
hoelzl@40859
  1447
lemma (in dynkin_system) sigma_algebra_eq_Int_stable:
hoelzl@40859
  1448
  "sigma_algebra M \<longleftrightarrow> Int_stable M"
hoelzl@40859
  1449
proof
hoelzl@40859
  1450
  assume "sigma_algebra M" then show "Int_stable M"
hoelzl@40859
  1451
    unfolding sigma_algebra_def using algebra.Int_stable by auto
hoelzl@40859
  1452
next
hoelzl@40859
  1453
  assume "Int_stable M"
hoelzl@40859
  1454
  show "sigma_algebra M"
hoelzl@42065
  1455
    unfolding sigma_algebra_disjoint_iff algebra_iff_Un
hoelzl@40859
  1456
  proof (intro conjI ballI allI impI)
hoelzl@40859
  1457
    show "sets M \<subseteq> Pow (space M)" using sets_into_space by auto
hoelzl@40859
  1458
  next
hoelzl@40859
  1459
    fix A B assume "A \<in> sets M" "B \<in> sets M"
hoelzl@40859
  1460
    then have "A \<union> B = space M - ((space M - A) \<inter> (space M - B))"
hoelzl@40859
  1461
              "space M - A \<in> sets M" "space M - B \<in> sets M"
hoelzl@40859
  1462
      using sets_into_space by auto
hoelzl@40859
  1463
    then show "A \<union> B \<in> sets M"
hoelzl@40859
  1464
      using `Int_stable M` unfolding Int_stable_def by auto
hoelzl@40859
  1465
  qed auto
hoelzl@40859
  1466
qed
hoelzl@40859
  1467
hoelzl@40859
  1468
subsection "Smallest Dynkin systems"
hoelzl@40859
  1469
hoelzl@41689
  1470
definition dynkin where
hoelzl@40859
  1471
  "dynkin M = \<lparr> space = space M,
hoelzl@41689
  1472
     sets = \<Inter>{D. dynkin_system \<lparr> space = space M, sets = D \<rparr> \<and> sets M \<subseteq> D},
hoelzl@41689
  1473
     \<dots> = more M \<rparr>"
hoelzl@40859
  1474
hoelzl@40859
  1475
lemma dynkin_system_dynkin:
hoelzl@40859
  1476
  assumes "sets M \<subseteq> Pow (space M)"
hoelzl@40859
  1477
  shows "dynkin_system (dynkin M)"
hoelzl@40859
  1478
proof (rule dynkin_systemI)
hoelzl@40859
  1479
  fix A assume "A \<in> sets (dynkin M)"
hoelzl@40859
  1480
  moreover
hoelzl@40859
  1481
  { fix D assume "A \<in> D" and d: "dynkin_system \<lparr> space = space M, sets = D \<rparr>"
hoelzl@42065
  1482
    then have "A \<subseteq> space M" by (auto simp: dynkin_system_def subset_class_def) }
hoelzl@40859
  1483
  moreover have "{D. dynkin_system \<lparr> space = space M, sets = D\<rparr> \<and> sets M \<subseteq> D} \<noteq> {}"
nipkow@44890
  1484
    using assms dynkin_system_trivial by fastforce
hoelzl@40859
  1485
  ultimately show "A \<subseteq> space (dynkin M)"
hoelzl@40859
  1486
    unfolding dynkin_def using assms
huffman@44537
  1487
    by simp (metis dynkin_system_def subset_class_def in_mono)
hoelzl@40859
  1488
next
hoelzl@40859
  1489
  show "space (dynkin M) \<in> sets (dynkin M)"
nipkow@44890
  1490
    unfolding dynkin_def using dynkin_system.space by fastforce
hoelzl@40859
  1491
next
hoelzl@40859
  1492
  fix A assume "A \<in> sets (dynkin M)"
hoelzl@40859
  1493
  then show "space (dynkin M) - A \<in> sets (dynkin M)"
hoelzl@40859
  1494
    unfolding dynkin_def using dynkin_system.compl by force
hoelzl@40859
  1495
next
hoelzl@40859
  1496
  fix A :: "nat \<Rightarrow> 'a set"
hoelzl@40859
  1497
  assume A: "disjoint_family A" "range A \<subseteq> sets (dynkin M)"
hoelzl@40859
  1498
  show "(\<Union>i. A i) \<in> sets (dynkin M)" unfolding dynkin_def
hoelzl@40859
  1499
  proof (simp, safe)
hoelzl@40859
  1500
    fix D assume "dynkin_system \<lparr>space = space M, sets = D\<rparr>" "sets M \<subseteq> D"
hoelzl@40859
  1501
    with A have "(\<Union>i. A i) \<in> sets \<lparr>space = space M, sets = D\<rparr>"
hoelzl@40859
  1502
      by (intro dynkin_system.UN) (auto simp: dynkin_def)
hoelzl@40859
  1503
    then show "(\<Union>i. A i) \<in> D" by auto
hoelzl@40859
  1504
  qed
hoelzl@40859
  1505
qed
hoelzl@40859
  1506
hoelzl@40859
  1507
lemma dynkin_Basic[intro]:
hoelzl@40859
  1508
  "A \<in> sets M \<Longrightarrow> A \<in> sets (dynkin M)"
hoelzl@40859
  1509
  unfolding dynkin_def by auto
hoelzl@40859
  1510
hoelzl@40859
  1511
lemma dynkin_space[simp]:
hoelzl@40859
  1512
  "space (dynkin M) = space M"
hoelzl@40859
  1513
  unfolding dynkin_def by auto
hoelzl@40859
  1514
hoelzl@40859
  1515
lemma (in dynkin_system) restricted_dynkin_system:
hoelzl@40859
  1516
  assumes "D \<in> sets M"
hoelzl@40859
  1517
  shows "dynkin_system \<lparr> space = space M,
hoelzl@40859
  1518
                         sets = {Q. Q \<subseteq> space M \<and> Q \<inter> D \<in> sets M} \<rparr>"
hoelzl@40859
  1519
proof (rule dynkin_systemI, simp_all)
hoelzl@40859
  1520
  have "space M \<inter> D = D"
hoelzl@40859
  1521
    using `D \<in> sets M` sets_into_space by auto
hoelzl@40859
  1522
  then show "space M \<inter> D \<in> sets M"
hoelzl@40859
  1523
    using `D \<in> sets M` by auto
hoelzl@40859
  1524
next
hoelzl@40859
  1525
  fix A assume "A \<subseteq> space M \<and> A \<inter> D \<in> sets M"
hoelzl@40859
  1526
  moreover have "(space M - A) \<inter> D = (space M - (A \<inter> D)) - (space M - D)"
hoelzl@40859
  1527
    by auto
hoelzl@40859
  1528
  ultimately show "space M - A \<subseteq> space M \<and> (space M - A) \<inter> D \<in> sets M"
hoelzl@40859
  1529
    using  `D \<in> sets M` by (auto intro: diff)
hoelzl@40859
  1530
next
hoelzl@40859
  1531
  fix A :: "nat \<Rightarrow> 'a set"
hoelzl@40859
  1532
  assume "disjoint_family A" "range A \<subseteq> {Q. Q \<subseteq> space M \<and> Q \<inter> D \<in> sets M}"
hoelzl@40859
  1533
  then have "\<And>i. A i \<subseteq> space M" "disjoint_family (\<lambda>i. A i \<inter> D)"
hoelzl@40859
  1534
    "range (\<lambda>i. A i \<inter> D) \<subseteq> sets M" "(\<Union>x. A x) \<inter> D = (\<Union>x. A x \<inter> D)"
nipkow@44890
  1535
    by ((fastforce simp: disjoint_family_on_def)+)
hoelzl@40859
  1536
  then show "(\<Union>x. A x) \<subseteq> space M \<and> (\<Union>x. A x) \<inter> D \<in> sets M"
hoelzl@40859
  1537
    by (auto simp del: UN_simps)
hoelzl@40859
  1538
qed
hoelzl@40859
  1539
hoelzl@40859
  1540
lemma (in dynkin_system) dynkin_subset:
hoelzl@40859
  1541
  assumes "sets N \<subseteq> sets M"
hoelzl@40859
  1542
  assumes "space N = space M"
hoelzl@40859
  1543
  shows "sets (dynkin N) \<subseteq> sets M"
hoelzl@40859
  1544
proof -
hoelzl@40859
  1545
  have "dynkin_system M" by default
hoelzl@41689
  1546
  then have "dynkin_system \<lparr>space = space N, sets = sets M \<rparr>"
hoelzl@42065
  1547
    using assms unfolding dynkin_system_def dynkin_system_axioms_def subset_class_def by simp
hoelzl@40859
  1548
  with `sets N \<subseteq> sets M` show ?thesis by (auto simp add: dynkin_def)
hoelzl@40859
  1549
qed
hoelzl@40859
  1550
hoelzl@40859
  1551
lemma sigma_eq_dynkin:
hoelzl@40859
  1552
  assumes sets: "sets M \<subseteq> Pow (space M)"
hoelzl@40859
  1553
  assumes "Int_stable M"
hoelzl@40859
  1554
  shows "sigma M = dynkin M"
hoelzl@40859
  1555
proof -
hoelzl@40859
  1556
  have "sets (dynkin M) \<subseteq> sigma_sets (space M) (sets M)"
hoelzl@40859
  1557
    using sigma_algebra_imp_dynkin_system
hoelzl@40859
  1558
    unfolding dynkin_def sigma_def sigma_sets_least_sigma_algebra[OF sets] by auto
hoelzl@40859
  1559
  moreover
hoelzl@40859
  1560
  interpret dynkin_system "dynkin M"
hoelzl@40859
  1561
    using dynkin_system_dynkin[OF sets] .
hoelzl@40859
  1562
  have "sigma_algebra (dynkin M)"
hoelzl@40859
  1563
    unfolding sigma_algebra_eq_Int_stable Int_stable_def
hoelzl@40859
  1564
  proof (intro ballI)
hoelzl@40859
  1565
    fix A B assume "A \<in> sets (dynkin M)" "B \<in> sets (dynkin M)"
wenzelm@46731
  1566
    let ?D = "\<lambda>E. \<lparr> space = space M,
hoelzl@40859
  1567
                    sets = {Q. Q \<subseteq> space M \<and> Q \<inter> E \<in> sets (dynkin M)} \<rparr>"
hoelzl@40859
  1568
    have "sets M \<subseteq> sets (?D B)"
hoelzl@40859
  1569
    proof
hoelzl@40859
  1570
      fix E assume "E \<in> sets M"
hoelzl@40859
  1571
      then have "sets M \<subseteq> sets (?D E)" "E \<in> sets (dynkin M)"
hoelzl@40859
  1572
        using sets_into_space `Int_stable M` by (auto simp: Int_stable_def)
hoelzl@40859
  1573
      then have "sets (dynkin M) \<subseteq> sets (?D E)"
hoelzl@40859
  1574
        using restricted_dynkin_system `E \<in> sets (dynkin M)`
hoelzl@40859
  1575
        by (intro dynkin_system.dynkin_subset) simp_all
hoelzl@40859
  1576
      then have "B \<in> sets (?D E)"
hoelzl@40859
  1577
        using `B \<in> sets (dynkin M)` by auto
hoelzl@40859
  1578
      then have "E \<inter> B \<in> sets (dynkin M)"
hoelzl@40859
  1579
        by (subst Int_commute) simp
hoelzl@40859
  1580
      then show "E \<in> sets (?D B)"
hoelzl@40859
  1581
        using sets `E \<in> sets M` by auto
hoelzl@40859
  1582
    qed
hoelzl@40859
  1583
    then have "sets (dynkin M) \<subseteq> sets (?D B)"
hoelzl@40859
  1584
      using restricted_dynkin_system `B \<in> sets (dynkin M)`
hoelzl@40859
  1585
      by (intro dynkin_system.dynkin_subset) simp_all
hoelzl@40859
  1586
    then show "A \<inter> B \<in> sets (dynkin M)"
hoelzl@40859
  1587
      using `A \<in> sets (dynkin M)` sets_into_space by auto
hoelzl@40859
  1588
  qed
hoelzl@40859
  1589
  from sigma_algebra.sigma_sets_subset[OF this, of "sets M"]
hoelzl@40859
  1590
  have "sigma_sets (space M) (sets M) \<subseteq> sets (dynkin M)" by auto
hoelzl@40859
  1591
  ultimately have "sigma_sets (space M) (sets M) = sets (dynkin M)" by auto
hoelzl@40859
  1592
  then show ?thesis
hoelzl@41689
  1593
    by (auto intro!: algebra.equality simp: sigma_def dynkin_def)
hoelzl@40859
  1594
qed