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.
8 header {* Sigma Algebras *}
13 "~~/src/HOL/Library/Countable"
14 "~~/src/HOL/Library/FuncSet"
15 "~~/src/HOL/Library/Indicator_Function"
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 *}
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"
47 have "a \<inter> b = a - (a - b)"
49 then show "a \<inter> b \<in> sets M"
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"
70 have "{x} \<union> A \<in> sets M" using assms by (rule Un)
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"
84 have "{x\<in>space M. Q x \<and> P x} = {x\<in>space M. Q x} \<inter> {x\<in>space M. P x}"
86 with assms show ?thesis by auto
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"
93 have "{x\<in>space M. Q x \<or> P x} = {x\<in>space M. Q x} \<union> {x\<in>space M. P x}"
95 with assms show ?thesis by auto
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"
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
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"
111 have "{x\<in>space M. \<exists>i\<in>S. P i x} = (\<Union>i\<in>S. {x\<in>space M. P i x})"
113 with assms show ?thesis by auto
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"
123 lemma algebra_iff_Un:
124 "algebra M \<longleftrightarrow>
125 sets M \<subseteq> Pow (space 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")
131 then interpret algebra M .
132 show ?Un using sets_into_space by auto
137 show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M" "space M \<in> sets M"
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
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")
155 then interpret algebra M .
156 show ?Int using sets_into_space by auto
160 proof (unfold algebra_iff_Un, intro conjI ballI)
161 show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M"
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))"
167 also have "... \<in> sets M"
168 using sets `?Int` by auto
169 finally show "a \<union> b \<in> sets M" .
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"
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
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"
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"
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)"
216 also have "(\<Union>s\<in>sets M \<inter> range A. s) \<in> sets M"
217 using `finite (sets M)` by (auto intro: finite_UN)
218 finally show "(\<Union>i. A i) \<in> sets M" .
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)"
226 let ?A' = "A \<circ> from_nat"
227 have *: "(\<Union>i. ?A' i) = (\<Union>i. A i)" (is "?l = ?r")
229 fix x i assume "x \<in> A i" thus "x \<in> ?l"
230 by (auto intro!: exI[of _ "to_nat i"])
232 fix x i assume "x \<in> ?A' i" thus "x \<in> ?r"
233 by (auto intro!: exI[of _ "from_nat i"])
235 have **: "range ?A' = range A"
237 by (auto simp: image_compose intro!: imageI)
238 show ?thesis unfolding * ** ..
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"
246 let "?A 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
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"
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
262 have "(\<Inter>i\<in>X. A i) = space M - (\<Union>i\<in>X. space M - A i)" using space_closed A
264 ultimately show ?thesis by metis
267 lemma ring_of_sets_Pow:
268 "ring_of_sets \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
272 "algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
275 lemma sigma_algebra_Pow:
276 "sigma_algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
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"
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
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"
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
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: UNION_eq_Union_image range_binary_eq)
320 lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
321 by (simp add: INTER_eq_Inter_image 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. *}
337 sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
338 for sp :: "'a set" and A :: "'a set set"
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"
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"
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)
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>}"
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
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"
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
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)
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)
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"
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)"
413 also have "... = (\<Inter>i. a i)" using ai
414 by (blast dest: sigma_sets_into_sp [OF Asb])
415 finally show ?thesis .
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"
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 .
432 lemma (in sigma_algebra) sigma_sets_eq:
433 "sigma_sets (space M) (sets M) = sets M"
435 show "sets M \<subseteq> sigma_sets (space M) (sets M)"
436 by (metis Set.subsetI sigma_sets.Basic)
438 show "sigma_sets (space M) (sets M) \<subseteq> sets M"
439 by (metis sigma_sets_subset subset_refl)
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)
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)
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)
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"
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)
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"
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)"])
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
490 show "algebra (restricted_space S)" using restricted_algebra[OF assms] .
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
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)
507 by (force intro!: sigma_sets.Compl simp: Diff_Int_distrib ac_simps)
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)
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"
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)
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 ..
530 by (auto intro!: bexI[of _ "(\<Union>x. f x)"] sigma_sets.Union
532 qed (auto intro!: sigma_sets.intros)
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
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)
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_sets_singleton:
559 assumes "X \<subseteq> S"
560 shows "sigma_sets S { X } = { {}, X, S - X, S }"
562 interpret sigma_algebra "\<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
563 by (rule sigma_algebra_single_set) fact
564 have "sigma_sets S { X } \<subseteq> sigma_sets S { {}, X, S - X, S }"
565 by (rule sigma_sets_subseteq) simp
566 moreover have "\<dots> = { {}, X, S - X, S }"
567 using sigma_eq unfolding sigma_def by simp
569 { fix A assume "A \<in> { {}, X, S - X, S }"
570 then have "A \<in> sigma_sets S { X }"
571 by (auto intro: sigma_sets.intros sigma_sets_top) }
572 ultimately have "sigma_sets S { X } = sigma_sets S { {}, X, S - X, S }"
573 by (intro antisym) auto
574 with sigma_eq show ?thesis
575 unfolding sigma_def by simp
578 lemma restricted_sigma:
579 assumes S: "S \<in> sets (sigma M)" and M: "sets M \<subseteq> Pow (space M)"
580 shows "algebra.restricted_space (sigma M) S = sigma (algebra.restricted_space M S)"
582 from S sigma_sets_into_sp[OF M]
583 have "S \<in> sigma_sets (space M) (sets M)" "S \<subseteq> space M"
584 by (auto simp: sigma_def)
585 from sigma_sets_Int[OF this]
587 by (simp add: sigma_def)
590 section {* Measurable functions *}
593 "measurable A B = {f \<in> space A -> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
595 lemma (in sigma_algebra) measurable_sigma:
596 assumes B: "sets N \<subseteq> Pow (space N)"
597 and f: "f \<in> space M -> space N"
598 and ba: "\<And>y. y \<in> sets N \<Longrightarrow> (f -` y) \<inter> space M \<in> sets M"
599 shows "f \<in> measurable M (sigma N)"
601 have "sigma_sets (space N) (sets N) \<subseteq> {y . (f -` y) \<inter> space M \<in> sets M & y \<subseteq> space N}"
604 assume "x \<in> sigma_sets (space N) (sets N)"
605 thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> space N"
609 by (auto simp add: ba) (metis B subsetD PowD)
616 have [simp]: "f -` space N \<inter> space M = space M"
617 by (auto simp add: funcset_mem [OF f])
619 by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
623 by (simp add: vimage_UN, simp only: UN_extend_simps(4)) blast
627 by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f)
628 (auto simp add: sigma_def)
631 lemma measurable_cong:
632 assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
633 shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'"
634 unfolding measurable_def using assms
635 by (simp cong: vimage_inter_cong Pi_cong)
637 lemma measurable_space:
638 "f \<in> measurable M A \<Longrightarrow> x \<in> space M \<Longrightarrow> f x \<in> space A"
639 unfolding measurable_def by auto
641 lemma measurable_sets:
642 "f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
643 unfolding measurable_def by auto
645 lemma (in sigma_algebra) measurable_subset:
646 "(\<And>S. S \<in> sets A \<Longrightarrow> S \<subseteq> space A) \<Longrightarrow> measurable M A \<subseteq> measurable M (sigma A)"
647 by (auto intro: measurable_sigma measurable_sets measurable_space)
649 lemma measurable_eqI:
650 "\<lbrakk> space m1 = space m1' ; space m2 = space m2' ;
651 sets m1 = sets m1' ; sets m2 = sets m2' \<rbrakk>
652 \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
653 by (simp add: measurable_def sigma_algebra_iff2)
655 lemma (in sigma_algebra) measurable_const[intro, simp]:
656 assumes "c \<in> space M'"
657 shows "(\<lambda>x. c) \<in> measurable M M'"
658 using assms by (auto simp add: measurable_def)
660 lemma (in sigma_algebra) measurable_If:
661 assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
662 assumes P: "{x\<in>space M. P x} \<in> sets M"
663 shows "(\<lambda>x. if P x then f x else g x) \<in> measurable M M'"
664 unfolding measurable_def
666 fix x assume "x \<in> space M"
667 thus "(if P x then f x else g x) \<in> space M'"
668 using measure unfolding measurable_def by auto
670 fix A assume "A \<in> sets M'"
671 hence *: "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M =
672 ((f -` A \<inter> space M) \<inter> {x\<in>space M. P x}) \<union>
673 ((g -` A \<inter> space M) \<inter> (space M - {x\<in>space M. P x}))"
674 using measure unfolding measurable_def by (auto split: split_if_asm)
675 show "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M \<in> sets M"
676 using `A \<in> sets M'` measure P unfolding * measurable_def
680 lemma (in sigma_algebra) measurable_If_set:
681 assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
682 assumes P: "A \<in> sets M"
683 shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> measurable M M'"
684 proof (rule measurable_If[OF measure])
685 have "{x \<in> space M. x \<in> A} = A" using `A \<in> sets M` sets_into_space by auto
686 thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<in> sets M` by auto
689 lemma (in ring_of_sets) measurable_ident[intro, simp]: "id \<in> measurable M M"
690 by (auto simp add: measurable_def)
692 lemma measurable_comp[intro]:
693 fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
694 shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
695 apply (auto simp add: measurable_def vimage_compose)
696 apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
700 lemma measurable_strong:
701 fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
702 assumes f: "f \<in> measurable a b" and g: "g \<in> (space b -> space c)"
703 and a: "sigma_algebra a" and b: "sigma_algebra b" and c: "sigma_algebra c"
704 and t: "f ` (space a) \<subseteq> t"
705 and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g -` s) \<inter> t \<in> sets b"
706 shows "(g o f) \<in> measurable a c"
708 have fab: "f \<in> (space a -> space b)"
709 and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
710 by (auto simp add: measurable_def)
711 have eq: "f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
714 apply (auto simp add: measurable_def vimage_compose a c)
715 apply (metis funcset_mem fab g)
716 apply (subst eq, metis ba cb)
720 lemma measurable_mono1:
721 "a \<subseteq> b \<Longrightarrow> sigma_algebra \<lparr>space = X, sets = b\<rparr>
722 \<Longrightarrow> measurable \<lparr>space = X, sets = a\<rparr> c \<subseteq> measurable \<lparr>space = X, sets = b\<rparr> c"
723 by (auto simp add: measurable_def)
725 lemma measurable_up_sigma:
726 "measurable A M \<subseteq> measurable (sigma A) M"
727 unfolding measurable_def
728 by (auto simp: sigma_def intro: sigma_sets.Basic)
730 lemma (in sigma_algebra) measurable_range_reduce:
731 "\<lbrakk> f \<in> measurable M \<lparr>space = s, sets = Pow s\<rparr> ; s \<noteq> {} \<rbrakk>
732 \<Longrightarrow> f \<in> measurable M \<lparr>space = s \<inter> (f ` space M), sets = Pow (s \<inter> (f ` space M))\<rparr>"
733 by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast
735 lemma (in sigma_algebra) measurable_Pow_to_Pow:
736 "(sets M = Pow (space M)) \<Longrightarrow> f \<in> measurable M \<lparr>space = UNIV, sets = Pow UNIV\<rparr>"
737 by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def)
739 lemma (in sigma_algebra) measurable_Pow_to_Pow_image:
740 "sets M = Pow (space M)
741 \<Longrightarrow> f \<in> measurable M \<lparr>space = f ` space M, sets = Pow (f ` space M)\<rparr>"
742 by (simp add: measurable_def sigma_algebra_Pow) intro_locales
744 lemma (in sigma_algebra) measurable_iff_sigma:
745 assumes "sets E \<subseteq> Pow (space E)" and "f \<in> space M \<rightarrow> space E"
746 shows "f \<in> measurable M (sigma E) \<longleftrightarrow> (\<forall>A\<in>sets E. f -` A \<inter> space M \<in> sets M)"
747 using measurable_sigma[OF assms]
748 by (fastsimp simp: measurable_def sets_sigma intro: sigma_sets.intros)
750 section "Disjoint families"
753 disjoint_family_on where
754 "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
757 "disjoint_family A \<equiv> disjoint_family_on A UNIV"
759 lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
762 lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
765 lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
768 lemma disjoint_family_subset:
769 "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
770 by (force simp add: disjoint_family_on_def)
772 lemma disjoint_family_on_bisimulation:
773 assumes "disjoint_family_on f S"
774 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 = {}"
775 shows "disjoint_family_on g S"
776 using assms unfolding disjoint_family_on_def by auto
778 lemma disjoint_family_on_mono:
779 "A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A"
780 unfolding disjoint_family_on_def by auto
782 lemma disjoint_family_Suc:
783 assumes Suc: "!!n. A n \<subseteq> A (Suc n)"
784 shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
788 have "!!n. A n \<subseteq> A (m+n)"
790 case 0 show ?case by simp
792 case (Suc m) thus ?case
793 by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
796 hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
797 by (metis add_commute le_add_diff_inverse nat_less_le)
799 by (auto simp add: disjoint_family_on_def)
800 (metis insert_absorb insert_subset le_SucE le_antisym not_leE)
803 lemma setsum_indicator_disjoint_family:
804 fixes f :: "'d \<Rightarrow> 'e::semiring_1"
805 assumes d: "disjoint_family_on A P" and "x \<in> A j" and "finite P" and "j \<in> P"
806 shows "(\<Sum>i\<in>P. f i * indicator (A i) x) = f j"
808 have "P \<inter> {i. x \<in> A i} = {j}"
809 using d `x \<in> A j` `j \<in> P` unfolding disjoint_family_on_def
812 unfolding indicator_def
813 by (simp add: if_distrib setsum_cases[OF `finite P`])
816 definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
817 where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
819 lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
821 case 0 show ?case by simp
824 thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
827 lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
828 apply (rule UN_finite2_eq [where k=0])
829 apply (simp add: finite_UN_disjointed_eq)
832 lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
833 by (auto simp add: disjointed_def)
835 lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
836 by (simp add: disjoint_family_on_def)
837 (metis neq_iff Int_commute less_disjoint_disjointed)
839 lemma disjointed_subset: "disjointed A n \<subseteq> A n"
840 by (auto simp add: disjointed_def)
842 lemma (in ring_of_sets) UNION_in_sets:
843 fixes A:: "nat \<Rightarrow> 'a set"
844 assumes A: "range A \<subseteq> sets M "
845 shows "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
847 case 0 show ?case by simp
851 by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
854 lemma (in ring_of_sets) range_disjointed_sets:
855 assumes A: "range A \<subseteq> sets M "
856 shows "range (disjointed A) \<subseteq> sets M"
857 proof (auto simp add: disjointed_def)
859 show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets
860 by (metis A Diff UNIV_I image_subset_iff)
863 lemma (in algebra) range_disjointed_sets':
864 "range A \<subseteq> sets M \<Longrightarrow> range (disjointed A) \<subseteq> sets M"
865 using range_disjointed_sets .
867 lemma disjointed_0[simp]: "disjointed A 0 = A 0"
868 by (simp add: disjointed_def)
871 "incseq A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
872 unfolding incseq_def by auto
874 lemma disjointed_incseq:
875 "incseq A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
876 using incseq_Un[of A]
877 by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
879 lemma sigma_algebra_disjoint_iff:
880 "sigma_algebra M \<longleftrightarrow>
882 (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow>
883 (\<Union>i::nat. A i) \<in> sets M)"
884 proof (auto simp add: sigma_algebra_iff)
885 fix A :: "nat \<Rightarrow> 'a set"
886 assume M: "algebra M"
887 and A: "range A \<subseteq> sets M"
888 and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow>
889 disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
890 hence "range (disjointed A) \<subseteq> sets M \<longrightarrow>
891 disjoint_family (disjointed A) \<longrightarrow>
892 (\<Union>i. disjointed A i) \<in> sets M" by blast
893 hence "(\<Union>i. disjointed A i) \<in> sets M"
894 by (simp add: algebra.range_disjointed_sets' M A disjoint_family_disjointed)
895 thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
898 subsection {* Sigma algebra generated by function preimages *}
900 definition (in sigma_algebra)
901 "vimage_algebra S f = \<lparr> space = S, sets = (\<lambda>A. f -` A \<inter> S) ` sets M, \<dots> = more M \<rparr>"
903 lemma (in sigma_algebra) in_vimage_algebra[simp]:
904 "A \<in> sets (vimage_algebra S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)"
905 by (simp add: vimage_algebra_def image_iff)
907 lemma (in sigma_algebra) space_vimage_algebra[simp]:
908 "space (vimage_algebra S f) = S"
909 by (simp add: vimage_algebra_def)
911 lemma (in sigma_algebra) sigma_algebra_preimages:
912 fixes f :: "'x \<Rightarrow> 'a"
913 assumes "f \<in> A \<rightarrow> space M"
914 shows "sigma_algebra \<lparr> space = A, sets = (\<lambda>M. f -` M \<inter> A) ` sets M \<rparr>"
915 (is "sigma_algebra \<lparr> space = _, sets = ?F ` sets M \<rparr>")
916 proof (simp add: sigma_algebra_iff2, safe)
917 show "{} \<in> ?F ` sets M" by blast
919 fix S assume "S \<in> sets M"
920 moreover have "A - ?F S = ?F (space M - S)"
922 ultimately show "A - ?F S \<in> ?F ` sets M"
925 fix S :: "nat \<Rightarrow> 'x set" assume *: "range S \<subseteq> ?F ` sets M"
926 have "\<forall>i. \<exists>b. b \<in> sets M \<and> S i = ?F b"
929 have "S i \<in> ?F ` sets M" using * by auto
930 then show "\<exists>b. b \<in> sets M \<and> S i = ?F b" by auto
932 from choice[OF this] obtain b where b: "range b \<subseteq> sets M" "\<And>i. S i = ?F (b i)"
934 then have "(\<Union>i. S i) = ?F (\<Union>i. b i)" by auto
935 then show "(\<Union>i. S i) \<in> ?F ` sets M" using b(1) by blast
938 lemma (in sigma_algebra) sigma_algebra_vimage:
939 fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
940 shows "sigma_algebra (vimage_algebra S f)"
942 from sigma_algebra_preimages[OF assms]
943 show ?thesis unfolding vimage_algebra_def by (auto simp: sigma_algebra_iff2)
946 lemma (in sigma_algebra) measurable_vimage_algebra:
947 fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
948 shows "f \<in> measurable (vimage_algebra S f) M"
949 unfolding measurable_def using assms by force
951 lemma (in sigma_algebra) measurable_vimage:
952 fixes g :: "'a \<Rightarrow> 'c" and f :: "'d \<Rightarrow> 'a"
953 assumes "g \<in> measurable M M2" "f \<in> S \<rightarrow> space M"
954 shows "(\<lambda>x. g (f x)) \<in> measurable (vimage_algebra S f) M2"
956 note measurable_vimage_algebra[OF assms(2)]
957 from measurable_comp[OF this assms(1)]
958 show ?thesis by (simp add: comp_def)
961 lemma sigma_sets_vimage:
962 assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S"
963 shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A"
964 proof (intro set_eqI iffI)
965 let ?F = "\<lambda>X. f -` X \<inter> S'"
966 fix X assume "X \<in> sigma_sets S' (?F ` A)"
967 then show "X \<in> ?F ` sigma_sets S A"
969 case (Basic X) then obtain X' where "X = ?F X'" "X' \<in> A"
971 then show ?case by (auto intro!: sigma_sets.Basic)
973 case Empty then show ?case
974 by (auto intro!: image_eqI[of _ _ "{}"] sigma_sets.Empty)
976 case (Compl X) then obtain X' where X: "X = ?F X'" and "X' \<in> sigma_sets S A"
978 then have "S - X' \<in> sigma_sets S A"
979 by (auto intro!: sigma_sets.Compl)
981 using X assms by (auto intro!: image_eqI[where x="S - X'"])
984 then have "\<forall>i. \<exists>F'. F' \<in> sigma_sets S A \<and> F i = f -` F' \<inter> S'"
985 by (auto simp: image_iff Bex_def)
986 from choice[OF this] obtain F' where
987 "\<And>i. F' i \<in> sigma_sets S A" and "\<And>i. F i = f -` F' i \<inter> S'"
990 by (auto intro!: sigma_sets.Union image_eqI[where x="\<Union>i. F' i"])
993 let ?F = "\<lambda>X. f -` X \<inter> S'"
994 fix X assume "X \<in> ?F ` sigma_sets S A"
995 then obtain X' where "X' \<in> sigma_sets S A" "X = ?F X'" by auto
996 then show "X \<in> sigma_sets S' (?F ` A)"
997 proof (induct arbitrary: X)
998 case (Basic X') then show ?case by (auto intro: sigma_sets.Basic)
1000 case Empty then show ?case by (auto intro: sigma_sets.Empty)
1003 have "S' - (S' - X) \<in> sigma_sets S' (?F ` A)"
1004 apply (rule sigma_sets.Compl)
1005 using assms by (auto intro!: Compl.hyps simp: Compl.prems)
1006 also have "S' - (S' - X) = X"
1007 using assms Compl by auto
1008 finally show ?case .
1011 have "(\<Union>i. f -` F i \<inter> S') \<in> sigma_sets S' (?F ` A)"
1012 by (intro sigma_sets.Union Union.hyps) simp
1013 also have "(\<Union>i. f -` F i \<inter> S') = X"
1014 using assms Union by auto
1015 finally show ?case .
1019 section {* Conditional space *}
1021 definition (in algebra)
1022 "image_space X = \<lparr> space = X`space M, sets = (\<lambda>S. X`S) ` sets M, \<dots> = more M \<rparr>"
1024 definition (in algebra)
1025 "conditional_space X A = algebra.image_space (restricted_space A) X"
1027 lemma (in algebra) space_conditional_space:
1028 assumes "A \<in> sets M" shows "space (conditional_space X A) = X`A"
1030 interpret r: algebra "restricted_space A" using assms by (rule restricted_algebra)
1031 show ?thesis unfolding conditional_space_def r.image_space_def
1035 subsection {* A Two-Element Series *}
1037 definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
1038 where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
1040 lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
1041 apply (simp add: binaryset_def)
1042 apply (rule set_eqI)
1043 apply (auto simp add: image_iff)
1046 lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
1047 by (simp add: UNION_eq_Union_image range_binaryset_eq)
1049 section {* Closed CDI *}
1053 "closed_cdi M \<longleftrightarrow>
1054 sets M \<subseteq> Pow (space M) &
1055 (\<forall>s \<in> sets M. space M - s \<in> sets M) &
1056 (\<forall>A. (range A \<subseteq> sets M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
1057 (\<Union>i. A i) \<in> sets M) &
1058 (\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
1061 smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
1065 "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M"
1067 "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M"
1069 "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n))
1070 \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets M"
1072 "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A
1073 \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets M"
1078 smallest_closed_cdi where
1079 "smallest_closed_cdi M = (|space = space M, sets = smallest_ccdi_sets M|)"
1081 lemma space_smallest_closed_cdi [simp]:
1082 "space (smallest_closed_cdi M) = space M"
1083 by (simp add: smallest_closed_cdi_def)
1085 lemma (in algebra) smallest_closed_cdi1: "sets M \<subseteq> sets (smallest_closed_cdi M)"
1086 by (auto simp add: smallest_closed_cdi_def)
1088 lemma (in algebra) smallest_ccdi_sets:
1089 "smallest_ccdi_sets M \<subseteq> Pow (space M)"
1090 apply (rule subsetI)
1091 apply (erule smallest_ccdi_sets.induct)
1092 apply (auto intro: range_subsetD dest: sets_into_space)
1095 lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)"
1096 apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets)
1097 apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) +
1100 lemma (in algebra) smallest_closed_cdi3:
1101 "sets (smallest_closed_cdi M) \<subseteq> Pow (space M)"
1102 by (simp add: smallest_closed_cdi_def smallest_ccdi_sets)
1104 lemma closed_cdi_subset: "closed_cdi M \<Longrightarrow> sets M \<subseteq> Pow (space M)"
1105 by (simp add: closed_cdi_def)
1107 lemma closed_cdi_Compl: "closed_cdi M \<Longrightarrow> s \<in> sets M \<Longrightarrow> space M - s \<in> sets M"
1108 by (simp add: closed_cdi_def)
1110 lemma closed_cdi_Inc:
1111 "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow>
1112 (\<Union>i. A i) \<in> sets M"
1113 by (simp add: closed_cdi_def)
1115 lemma closed_cdi_Disj:
1116 "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
1117 by (simp add: closed_cdi_def)
1119 lemma closed_cdi_Un:
1120 assumes cdi: "closed_cdi M" and empty: "{} \<in> sets M"
1121 and A: "A \<in> sets M" and B: "B \<in> sets M"
1122 and disj: "A \<inter> B = {}"
1123 shows "A \<union> B \<in> sets M"
1125 have ra: "range (binaryset A B) \<subseteq> sets M"
1126 by (simp add: range_binaryset_eq empty A B)
1127 have di: "disjoint_family (binaryset A B)" using disj
1128 by (simp add: disjoint_family_on_def binaryset_def Int_commute)
1129 from closed_cdi_Disj [OF cdi ra di]
1131 by (simp add: UN_binaryset_eq)
1134 lemma (in algebra) smallest_ccdi_sets_Un:
1135 assumes A: "A \<in> smallest_ccdi_sets M" and B: "B \<in> smallest_ccdi_sets M"
1136 and disj: "A \<inter> B = {}"
1137 shows "A \<union> B \<in> smallest_ccdi_sets M"
1139 have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)"
1140 by (simp add: range_binaryset_eq A B smallest_ccdi_sets.Basic)
1141 have di: "disjoint_family (binaryset A B)" using disj
1142 by (simp add: disjoint_family_on_def binaryset_def Int_commute)
1143 from Disj [OF ra di]
1145 by (simp add: UN_binaryset_eq)
1148 lemma (in algebra) smallest_ccdi_sets_Int1:
1149 assumes a: "a \<in> sets M"
1150 shows "b \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
1151 proof (induct rule: smallest_ccdi_sets.induct)
1154 by (metis a Int smallest_ccdi_sets.Basic)
1157 have "a \<inter> (space M - x) = space M - ((space M - a) \<union> (a \<inter> x))"
1159 also have "... \<in> smallest_ccdi_sets M"
1160 by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2
1161 Diff_disjoint Int_Diff Int_empty_right Un_commute
1162 smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl
1163 smallest_ccdi_sets_Un)
1164 finally show ?case .
1167 have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
1169 have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Inc
1171 moreover have "(\<lambda>i. a \<inter> A i) 0 = {}"
1173 moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc
1175 ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
1176 by (rule smallest_ccdi_sets.Inc)
1181 have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
1183 have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj
1185 moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj
1186 by (auto simp add: disjoint_family_on_def)
1187 ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
1188 by (rule smallest_ccdi_sets.Disj)
1194 lemma (in algebra) smallest_ccdi_sets_Int:
1195 assumes b: "b \<in> smallest_ccdi_sets M"
1196 shows "a \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
1197 proof (induct rule: smallest_ccdi_sets.induct)
1200 by (metis b smallest_ccdi_sets_Int1)
1203 have "(space M - x) \<inter> b = space M - (x \<inter> b \<union> (space M - b))"
1205 also have "... \<in> smallest_ccdi_sets M"
1206 by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b
1207 smallest_ccdi_sets.Compl smallest_ccdi_sets_Un)
1208 finally show ?case .
1211 have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
1213 have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Inc
1215 moreover have "(\<lambda>i. A i \<inter> b) 0 = {}"
1217 moreover have "!!n. (\<lambda>i. A i \<inter> b) n \<subseteq> (\<lambda>i. A i \<inter> b) (Suc n)" using Inc
1219 ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
1220 by (rule smallest_ccdi_sets.Inc)
1225 have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
1227 have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj
1229 moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj
1230 by (auto simp add: disjoint_family_on_def)
1231 ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
1232 by (rule smallest_ccdi_sets.Disj)
1237 lemma (in algebra) sets_smallest_closed_cdi_Int:
1238 "a \<in> sets (smallest_closed_cdi M) \<Longrightarrow> b \<in> sets (smallest_closed_cdi M)
1239 \<Longrightarrow> a \<inter> b \<in> sets (smallest_closed_cdi M)"
1240 by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def)
1242 lemma (in algebra) sigma_property_disjoint_lemma:
1243 assumes sbC: "sets M \<subseteq> C"
1244 and ccdi: "closed_cdi (|space = space M, sets = C|)"
1245 shows "sigma_sets (space M) (sets M) \<subseteq> C"
1247 have "smallest_ccdi_sets M \<in> {B . sets M \<subseteq> B \<and> sigma_algebra (|space = space M, sets = B|)}"
1248 apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int
1249 smallest_ccdi_sets_Int)
1250 apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets)
1251 apply (blast intro: smallest_ccdi_sets.Disj)
1253 hence "sigma_sets (space M) (sets M) \<subseteq> smallest_ccdi_sets M"
1255 (drule sigma_algebra.sigma_sets_subset [where a="sets M"], auto)
1256 also have "... \<subseteq> C"
1259 assume x: "x \<in> smallest_ccdi_sets M"
1261 proof (induct rule: smallest_ccdi_sets.induct)
1264 by (metis Basic subsetD sbC)
1268 by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
1272 by (auto intro: closed_cdi_Inc [OF ccdi, simplified])
1276 by (auto intro: closed_cdi_Disj [OF ccdi, simplified])
1279 finally show ?thesis .
1282 lemma (in algebra) sigma_property_disjoint:
1283 assumes sbC: "sets M \<subseteq> C"
1284 and compl: "!!s. s \<in> C \<inter> sigma_sets (space M) (sets M) \<Longrightarrow> space M - s \<in> C"
1285 and inc: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
1286 \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n))
1287 \<Longrightarrow> (\<Union>i. A i) \<in> C"
1288 and disj: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
1289 \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C"
1290 shows "sigma_sets (space M) (sets M) \<subseteq> C"
1292 have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
1293 proof (rule sigma_property_disjoint_lemma)
1294 show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
1295 by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
1297 show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
1298 by (simp add: closed_cdi_def compl inc disj)
1299 (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
1300 IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
1306 section {* Dynkin systems *}
1308 locale dynkin_system = subset_class +
1309 assumes space: "space M \<in> sets M"
1310 and compl[intro!]: "\<And>A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
1311 and UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
1312 \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
1314 lemma (in dynkin_system) empty[intro, simp]: "{} \<in> sets M"
1315 using space compl[of "space M"] by simp
1317 lemma (in dynkin_system) diff:
1318 assumes sets: "D \<in> sets M" "E \<in> sets M" and "D \<subseteq> E"
1319 shows "E - D \<in> sets M"
1321 let ?f = "\<lambda>x. if x = 0 then D else if x = Suc 0 then space M - E else {}"
1322 have "range ?f = {D, space M - E, {}}"
1323 by (auto simp: image_iff)
1324 moreover have "D \<union> (space M - E) = (\<Union>i. ?f i)"
1325 by (auto simp: image_iff split: split_if_asm)
1327 then have "disjoint_family ?f" unfolding disjoint_family_on_def
1328 using `D \<in> sets M`[THEN sets_into_space] `D \<subseteq> E` by auto
1329 ultimately have "space M - (D \<union> (space M - E)) \<in> sets M"
1331 also have "space M - (D \<union> (space M - E)) = E - D"
1332 using assms sets_into_space by auto
1333 finally show ?thesis .
1336 lemma dynkin_systemI:
1337 assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M" "space M \<in> sets M"
1338 assumes "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
1339 assumes "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
1340 \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
1341 shows "dynkin_system M"
1342 using assms by (auto simp: dynkin_system_def dynkin_system_axioms_def subset_class_def)
1344 lemma dynkin_system_trivial:
1345 shows "dynkin_system \<lparr> space = A, sets = Pow A \<rparr>"
1346 by (rule dynkin_systemI) auto
1348 lemma sigma_algebra_imp_dynkin_system:
1349 assumes "sigma_algebra M" shows "dynkin_system M"
1351 interpret sigma_algebra M by fact
1352 show ?thesis using sets_into_space by (fastsimp intro!: dynkin_systemI)
1355 subsection "Intersection stable algebras"
1357 definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
1359 lemma (in algebra) Int_stable: "Int_stable M"
1360 unfolding Int_stable_def by auto
1363 "(\<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>"
1364 unfolding Int_stable_def by auto
1367 "Int_stable M \<Longrightarrow> a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b \<in> sets M"
1368 unfolding Int_stable_def by auto
1370 lemma (in dynkin_system) sigma_algebra_eq_Int_stable:
1371 "sigma_algebra M \<longleftrightarrow> Int_stable M"
1373 assume "sigma_algebra M" then show "Int_stable M"
1374 unfolding sigma_algebra_def using algebra.Int_stable by auto
1376 assume "Int_stable M"
1377 show "sigma_algebra M"
1378 unfolding sigma_algebra_disjoint_iff algebra_iff_Un
1379 proof (intro conjI ballI allI impI)
1380 show "sets M \<subseteq> Pow (space M)" using sets_into_space by auto
1382 fix A B assume "A \<in> sets M" "B \<in> sets M"
1383 then have "A \<union> B = space M - ((space M - A) \<inter> (space M - B))"
1384 "space M - A \<in> sets M" "space M - B \<in> sets M"
1385 using sets_into_space by auto
1386 then show "A \<union> B \<in> sets M"
1387 using `Int_stable M` unfolding Int_stable_def by auto
1391 subsection "Smallest Dynkin systems"
1393 definition dynkin where
1394 "dynkin M = \<lparr> space = space M,
1395 sets = \<Inter>{D. dynkin_system \<lparr> space = space M, sets = D \<rparr> \<and> sets M \<subseteq> D},
1396 \<dots> = more M \<rparr>"
1398 lemma dynkin_system_dynkin:
1399 assumes "sets M \<subseteq> Pow (space M)"
1400 shows "dynkin_system (dynkin M)"
1401 proof (rule dynkin_systemI)
1402 fix A assume "A \<in> sets (dynkin M)"
1404 { fix D assume "A \<in> D" and d: "dynkin_system \<lparr> space = space M, sets = D \<rparr>"
1405 then have "A \<subseteq> space M" by (auto simp: dynkin_system_def subset_class_def) }
1406 moreover have "{D. dynkin_system \<lparr> space = space M, sets = D\<rparr> \<and> sets M \<subseteq> D} \<noteq> {}"
1407 using assms dynkin_system_trivial by fastsimp
1408 ultimately show "A \<subseteq> space (dynkin M)"
1409 unfolding dynkin_def using assms
1410 by simp (metis dynkin_system_def subset_class_def in_mono mem_def)
1412 show "space (dynkin M) \<in> sets (dynkin M)"
1413 unfolding dynkin_def using dynkin_system.space by fastsimp
1415 fix A assume "A \<in> sets (dynkin M)"
1416 then show "space (dynkin M) - A \<in> sets (dynkin M)"
1417 unfolding dynkin_def using dynkin_system.compl by force
1419 fix A :: "nat \<Rightarrow> 'a set"
1420 assume A: "disjoint_family A" "range A \<subseteq> sets (dynkin M)"
1421 show "(\<Union>i. A i) \<in> sets (dynkin M)" unfolding dynkin_def
1423 fix D assume "dynkin_system \<lparr>space = space M, sets = D\<rparr>" "sets M \<subseteq> D"
1424 with A have "(\<Union>i. A i) \<in> sets \<lparr>space = space M, sets = D\<rparr>"
1425 by (intro dynkin_system.UN) (auto simp: dynkin_def)
1426 then show "(\<Union>i. A i) \<in> D" by auto
1430 lemma dynkin_Basic[intro]:
1431 "A \<in> sets M \<Longrightarrow> A \<in> sets (dynkin M)"
1432 unfolding dynkin_def by auto
1434 lemma dynkin_space[simp]:
1435 "space (dynkin M) = space M"
1436 unfolding dynkin_def by auto
1438 lemma (in dynkin_system) restricted_dynkin_system:
1439 assumes "D \<in> sets M"
1440 shows "dynkin_system \<lparr> space = space M,
1441 sets = {Q. Q \<subseteq> space M \<and> Q \<inter> D \<in> sets M} \<rparr>"
1442 proof (rule dynkin_systemI, simp_all)
1443 have "space M \<inter> D = D"
1444 using `D \<in> sets M` sets_into_space by auto
1445 then show "space M \<inter> D \<in> sets M"
1446 using `D \<in> sets M` by auto
1448 fix A assume "A \<subseteq> space M \<and> A \<inter> D \<in> sets M"
1449 moreover have "(space M - A) \<inter> D = (space M - (A \<inter> D)) - (space M - D)"
1451 ultimately show "space M - A \<subseteq> space M \<and> (space M - A) \<inter> D \<in> sets M"
1452 using `D \<in> sets M` by (auto intro: diff)
1454 fix A :: "nat \<Rightarrow> 'a set"
1455 assume "disjoint_family A" "range A \<subseteq> {Q. Q \<subseteq> space M \<and> Q \<inter> D \<in> sets M}"
1456 then have "\<And>i. A i \<subseteq> space M" "disjoint_family (\<lambda>i. A i \<inter> D)"
1457 "range (\<lambda>i. A i \<inter> D) \<subseteq> sets M" "(\<Union>x. A x) \<inter> D = (\<Union>x. A x \<inter> D)"
1458 by ((fastsimp simp: disjoint_family_on_def)+)
1459 then show "(\<Union>x. A x) \<subseteq> space M \<and> (\<Union>x. A x) \<inter> D \<in> sets M"
1460 by (auto simp del: UN_simps)
1463 lemma (in dynkin_system) dynkin_subset:
1464 assumes "sets N \<subseteq> sets M"
1465 assumes "space N = space M"
1466 shows "sets (dynkin N) \<subseteq> sets M"
1468 have "dynkin_system M" by default
1469 then have "dynkin_system \<lparr>space = space N, sets = sets M \<rparr>"
1470 using assms unfolding dynkin_system_def dynkin_system_axioms_def subset_class_def by simp
1471 with `sets N \<subseteq> sets M` show ?thesis by (auto simp add: dynkin_def)
1474 lemma sigma_eq_dynkin:
1475 assumes sets: "sets M \<subseteq> Pow (space M)"
1476 assumes "Int_stable M"
1477 shows "sigma M = dynkin M"
1479 have "sets (dynkin M) \<subseteq> sigma_sets (space M) (sets M)"
1480 using sigma_algebra_imp_dynkin_system
1481 unfolding dynkin_def sigma_def sigma_sets_least_sigma_algebra[OF sets] by auto
1483 interpret dynkin_system "dynkin M"
1484 using dynkin_system_dynkin[OF sets] .
1485 have "sigma_algebra (dynkin M)"
1486 unfolding sigma_algebra_eq_Int_stable Int_stable_def
1488 fix A B assume "A \<in> sets (dynkin M)" "B \<in> sets (dynkin M)"
1489 let "?D E" = "\<lparr> space = space M,
1490 sets = {Q. Q \<subseteq> space M \<and> Q \<inter> E \<in> sets (dynkin M)} \<rparr>"
1491 have "sets M \<subseteq> sets (?D B)"
1493 fix E assume "E \<in> sets M"
1494 then have "sets M \<subseteq> sets (?D E)" "E \<in> sets (dynkin M)"
1495 using sets_into_space `Int_stable M` by (auto simp: Int_stable_def)
1496 then have "sets (dynkin M) \<subseteq> sets (?D E)"
1497 using restricted_dynkin_system `E \<in> sets (dynkin M)`
1498 by (intro dynkin_system.dynkin_subset) simp_all
1499 then have "B \<in> sets (?D E)"
1500 using `B \<in> sets (dynkin M)` by auto
1501 then have "E \<inter> B \<in> sets (dynkin M)"
1502 by (subst Int_commute) simp
1503 then show "E \<in> sets (?D B)"
1504 using sets `E \<in> sets M` by auto
1506 then have "sets (dynkin M) \<subseteq> sets (?D B)"
1507 using restricted_dynkin_system `B \<in> sets (dynkin M)`
1508 by (intro dynkin_system.dynkin_subset) simp_all
1509 then show "A \<inter> B \<in> sets (dynkin M)"
1510 using `A \<in> sets (dynkin M)` sets_into_space by auto
1512 from sigma_algebra.sigma_sets_subset[OF this, of "sets M"]
1513 have "sigma_sets (space M) (sets M) \<subseteq> sets (dynkin M)" by auto
1514 ultimately have "sigma_sets (space M) (sets M) = sets (dynkin M)" by auto
1516 by (auto intro!: algebra.equality simp: sigma_def dynkin_def)
1519 lemma (in dynkin_system) dynkin_idem:
1522 have "sets (dynkin M) = sets M"
1524 show "sets M \<subseteq> sets (dynkin M)"
1525 using dynkin_Basic by auto
1526 show "sets (dynkin M) \<subseteq> sets M"
1527 by (intro dynkin_subset) auto
1530 by (auto intro!: algebra.equality simp: dynkin_def)
1533 lemma (in dynkin_system) dynkin_lemma:
1534 assumes "Int_stable E"
1535 and E: "sets E \<subseteq> sets M" "space E = space M" "sets M \<subseteq> sets (sigma E)"
1536 shows "sets (sigma E) = sets M"
1538 have "sets E \<subseteq> Pow (space E)"
1539 using E sets_into_space by force
1540 then have "sigma E = dynkin E"
1541 using `Int_stable E` by (rule sigma_eq_dynkin)
1542 moreover then have "sets (dynkin E) = sets M"
1543 using assms dynkin_subset[OF E(1,2)] by simp
1544 ultimately show ?thesis
1545 using assms by (auto intro!: algebra.equality simp: dynkin_def)
1548 subsection "Sigma algebras on finite sets"
1550 locale finite_sigma_algebra = sigma_algebra +
1551 assumes finite_space: "finite (space M)"
1552 and sets_eq_Pow[simp]: "sets M = Pow (space M)"
1554 lemma (in finite_sigma_algebra) sets_image_space_eq_Pow:
1555 "sets (image_space X) = Pow (space (image_space X))"
1557 fix x S assume "S \<in> sets (image_space X)" "x \<in> S"
1558 then show "x \<in> space (image_space X)"
1559 using sets_into_space by (auto intro!: imageI simp: image_space_def)
1561 fix S assume "S \<subseteq> space (image_space X)"
1562 then obtain S' where "S = X`S'" "S'\<in>sets M"
1563 by (auto simp: subset_image_iff sets_eq_Pow image_space_def)
1564 then show "S \<in> sets (image_space X)"
1565 by (auto simp: image_space_def)
1568 lemma measurable_sigma_sigma:
1569 assumes M: "sets M \<subseteq> Pow (space M)" and N: "sets N \<subseteq> Pow (space N)"
1570 shows "f \<in> measurable M N \<Longrightarrow> f \<in> measurable (sigma M) (sigma N)"
1571 using sigma_algebra.measurable_subset[OF sigma_algebra_sigma[OF M], of N]
1572 using measurable_up_sigma[of M N] N by auto
1574 lemma (in sigma_algebra) measurable_Least:
1575 assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> sets M"
1576 shows "(\<lambda>x. LEAST j. P j x) -` A \<inter> space M \<in> sets M"
1578 { fix i have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M \<in> sets M"
1580 assume i: "(LEAST j. False) = i"
1581 have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
1582 {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}))"
1583 by (simp add: set_eq_iff, safe)
1584 (insert i, auto dest: Least_le intro: LeastI intro!: Least_equality)
1585 with meas show ?thesis
1586 by (auto intro!: Int)
1588 assume i: "(LEAST j. False) \<noteq> i"
1589 then have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
1590 {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x}))"
1591 proof (simp add: set_eq_iff, safe)
1592 fix x assume neq: "(LEAST j. False) \<noteq> (LEAST j. P j x)"
1593 have "\<exists>j. P j x"
1594 by (rule ccontr) (insert neq, auto)
1595 then show "P (LEAST j. P j x) x" by (rule LeastI_ex)
1596 qed (auto dest: Least_le intro!: Least_equality)
1597 with meas show ?thesis
1598 by (auto intro!: Int)
1600 then have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) \<in> sets M"
1601 by (intro countable_UN) auto
1602 moreover have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) =
1603 (\<lambda>x. LEAST j. P j x) -` A \<inter> space M" by auto
1604 ultimately show ?thesis by auto