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