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 *) |
|
7 |
|
8 section \<open>Describing measurable sets\<close> |
|
9 |
|
10 theory Sigma_Algebra |
|
11 imports |
|
12 Complex_Main |
|
13 "~~/src/HOL/Library/Countable_Set" |
|
14 "~~/src/HOL/Library/FuncSet" |
|
15 "~~/src/HOL/Library/Indicator_Function" |
|
16 "~~/src/HOL/Library/Extended_Nonnegative_Real" |
|
17 "~~/src/HOL/Library/Disjoint_Sets" |
|
18 begin |
|
19 |
|
20 text \<open>Sigma algebras are an elementary concept in measure |
|
21 theory. To measure --- that is to integrate --- functions, we first have |
|
22 to measure sets. Unfortunately, when dealing with a large universe, |
|
23 it is often not possible to consistently assign a measure to every |
|
24 subset. Therefore it is necessary to define the set of measurable |
|
25 subsets of the universe. A sigma algebra is such a set that has |
|
26 three very natural and desirable properties.\<close> |
|
27 |
|
28 subsection \<open>Families of sets\<close> |
|
29 |
|
30 locale subset_class = |
|
31 fixes \<Omega> :: "'a set" and M :: "'a set set" |
|
32 assumes space_closed: "M \<subseteq> Pow \<Omega>" |
|
33 |
|
34 lemma (in subset_class) sets_into_space: "x \<in> M \<Longrightarrow> x \<subseteq> \<Omega>" |
|
35 by (metis PowD contra_subsetD space_closed) |
|
36 |
|
37 subsubsection \<open>Semiring of sets\<close> |
|
38 |
|
39 locale semiring_of_sets = subset_class + |
|
40 assumes empty_sets[iff]: "{} \<in> M" |
|
41 assumes Int[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M" |
|
42 assumes Diff_cover: |
|
43 "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> \<exists>C\<subseteq>M. finite C \<and> disjoint C \<and> a - b = \<Union>C" |
|
44 |
|
45 lemma (in semiring_of_sets) finite_INT[intro]: |
|
46 assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" |
|
47 shows "(\<Inter>i\<in>I. A i) \<in> M" |
|
48 using assms by (induct rule: finite_ne_induct) auto |
|
49 |
|
50 lemma (in semiring_of_sets) Int_space_eq1 [simp]: "x \<in> M \<Longrightarrow> \<Omega> \<inter> x = x" |
|
51 by (metis Int_absorb1 sets_into_space) |
|
52 |
|
53 lemma (in semiring_of_sets) Int_space_eq2 [simp]: "x \<in> M \<Longrightarrow> x \<inter> \<Omega> = x" |
|
54 by (metis Int_absorb2 sets_into_space) |
|
55 |
|
56 lemma (in semiring_of_sets) sets_Collect_conj: |
|
57 assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M" |
|
58 shows "{x\<in>\<Omega>. Q x \<and> P x} \<in> M" |
|
59 proof - |
|
60 have "{x\<in>\<Omega>. Q x \<and> P x} = {x\<in>\<Omega>. Q x} \<inter> {x\<in>\<Omega>. P x}" |
|
61 by auto |
|
62 with assms show ?thesis by auto |
|
63 qed |
|
64 |
|
65 lemma (in semiring_of_sets) sets_Collect_finite_All': |
|
66 assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" "S \<noteq> {}" |
|
67 shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M" |
|
68 proof - |
|
69 have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (\<Inter>i\<in>S. {x\<in>\<Omega>. P i x})" |
|
70 using \<open>S \<noteq> {}\<close> by auto |
|
71 with assms show ?thesis by auto |
|
72 qed |
|
73 |
|
74 locale ring_of_sets = semiring_of_sets + |
|
75 assumes Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M" |
|
76 |
|
77 lemma (in ring_of_sets) finite_Union [intro]: |
|
78 "finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> \<Union>X \<in> M" |
|
79 by (induct set: finite) (auto simp add: Un) |
|
80 |
|
81 lemma (in ring_of_sets) finite_UN[intro]: |
|
82 assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" |
|
83 shows "(\<Union>i\<in>I. A i) \<in> M" |
|
84 using assms by induct auto |
|
85 |
|
86 lemma (in ring_of_sets) Diff [intro]: |
|
87 assumes "a \<in> M" "b \<in> M" shows "a - b \<in> M" |
|
88 using Diff_cover[OF assms] by auto |
|
89 |
|
90 lemma ring_of_setsI: |
|
91 assumes space_closed: "M \<subseteq> Pow \<Omega>" |
|
92 assumes empty_sets[iff]: "{} \<in> M" |
|
93 assumes Un[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M" |
|
94 assumes Diff[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a - b \<in> M" |
|
95 shows "ring_of_sets \<Omega> M" |
|
96 proof |
|
97 fix a b assume ab: "a \<in> M" "b \<in> M" |
|
98 from ab show "\<exists>C\<subseteq>M. finite C \<and> disjoint C \<and> a - b = \<Union>C" |
|
99 by (intro exI[of _ "{a - b}"]) (auto simp: disjoint_def) |
|
100 have "a \<inter> b = a - (a - b)" by auto |
|
101 also have "\<dots> \<in> M" using ab by auto |
|
102 finally show "a \<inter> b \<in> M" . |
|
103 qed fact+ |
|
104 |
|
105 lemma ring_of_sets_iff: "ring_of_sets \<Omega> M \<longleftrightarrow> M \<subseteq> Pow \<Omega> \<and> {} \<in> M \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a \<union> b \<in> M) \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a - b \<in> M)" |
|
106 proof |
|
107 assume "ring_of_sets \<Omega> M" |
|
108 then interpret ring_of_sets \<Omega> M . |
|
109 show "M \<subseteq> Pow \<Omega> \<and> {} \<in> M \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a \<union> b \<in> M) \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a - b \<in> M)" |
|
110 using space_closed by auto |
|
111 qed (auto intro!: ring_of_setsI) |
|
112 |
|
113 lemma (in ring_of_sets) insert_in_sets: |
|
114 assumes "{x} \<in> M" "A \<in> M" shows "insert x A \<in> M" |
|
115 proof - |
|
116 have "{x} \<union> A \<in> M" using assms by (rule Un) |
|
117 thus ?thesis by auto |
|
118 qed |
|
119 |
|
120 lemma (in ring_of_sets) sets_Collect_disj: |
|
121 assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M" |
|
122 shows "{x\<in>\<Omega>. Q x \<or> P x} \<in> M" |
|
123 proof - |
|
124 have "{x\<in>\<Omega>. Q x \<or> P x} = {x\<in>\<Omega>. Q x} \<union> {x\<in>\<Omega>. P x}" |
|
125 by auto |
|
126 with assms show ?thesis by auto |
|
127 qed |
|
128 |
|
129 lemma (in ring_of_sets) sets_Collect_finite_Ex: |
|
130 assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" |
|
131 shows "{x\<in>\<Omega>. \<exists>i\<in>S. P i x} \<in> M" |
|
132 proof - |
|
133 have "{x\<in>\<Omega>. \<exists>i\<in>S. P i x} = (\<Union>i\<in>S. {x\<in>\<Omega>. P i x})" |
|
134 by auto |
|
135 with assms show ?thesis by auto |
|
136 qed |
|
137 |
|
138 locale algebra = ring_of_sets + |
|
139 assumes top [iff]: "\<Omega> \<in> M" |
|
140 |
|
141 lemma (in algebra) compl_sets [intro]: |
|
142 "a \<in> M \<Longrightarrow> \<Omega> - a \<in> M" |
|
143 by auto |
|
144 |
|
145 lemma algebra_iff_Un: |
|
146 "algebra \<Omega> M \<longleftrightarrow> |
|
147 M \<subseteq> Pow \<Omega> \<and> |
|
148 {} \<in> M \<and> |
|
149 (\<forall>a \<in> M. \<Omega> - a \<in> M) \<and> |
|
150 (\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un") |
|
151 proof |
|
152 assume "algebra \<Omega> M" |
|
153 then interpret algebra \<Omega> M . |
|
154 show ?Un using sets_into_space by auto |
|
155 next |
|
156 assume ?Un |
|
157 then have "\<Omega> \<in> M" by auto |
|
158 interpret ring_of_sets \<Omega> M |
|
159 proof (rule ring_of_setsI) |
|
160 show \<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M" |
|
161 using \<open>?Un\<close> by auto |
|
162 fix a b assume a: "a \<in> M" and b: "b \<in> M" |
|
163 then show "a \<union> b \<in> M" using \<open>?Un\<close> by auto |
|
164 have "a - b = \<Omega> - ((\<Omega> - a) \<union> b)" |
|
165 using \<Omega> a b by auto |
|
166 then show "a - b \<in> M" |
|
167 using a b \<open>?Un\<close> by auto |
|
168 qed |
|
169 show "algebra \<Omega> M" proof qed fact |
|
170 qed |
|
171 |
|
172 lemma algebra_iff_Int: |
|
173 "algebra \<Omega> M \<longleftrightarrow> |
|
174 M \<subseteq> Pow \<Omega> & {} \<in> M & |
|
175 (\<forall>a \<in> M. \<Omega> - a \<in> M) & |
|
176 (\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int") |
|
177 proof |
|
178 assume "algebra \<Omega> M" |
|
179 then interpret algebra \<Omega> M . |
|
180 show ?Int using sets_into_space by auto |
|
181 next |
|
182 assume ?Int |
|
183 show "algebra \<Omega> M" |
|
184 proof (unfold algebra_iff_Un, intro conjI ballI) |
|
185 show \<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M" |
|
186 using \<open>?Int\<close> by auto |
|
187 from \<open>?Int\<close> show "\<And>a. a \<in> M \<Longrightarrow> \<Omega> - a \<in> M" by auto |
|
188 fix a b assume M: "a \<in> M" "b \<in> M" |
|
189 hence "a \<union> b = \<Omega> - ((\<Omega> - a) \<inter> (\<Omega> - b))" |
|
190 using \<Omega> by blast |
|
191 also have "... \<in> M" |
|
192 using M \<open>?Int\<close> by auto |
|
193 finally show "a \<union> b \<in> M" . |
|
194 qed |
|
195 qed |
|
196 |
|
197 lemma (in algebra) sets_Collect_neg: |
|
198 assumes "{x\<in>\<Omega>. P x} \<in> M" |
|
199 shows "{x\<in>\<Omega>. \<not> P x} \<in> M" |
|
200 proof - |
|
201 have "{x\<in>\<Omega>. \<not> P x} = \<Omega> - {x\<in>\<Omega>. P x}" by auto |
|
202 with assms show ?thesis by auto |
|
203 qed |
|
204 |
|
205 lemma (in algebra) sets_Collect_imp: |
|
206 "{x\<in>\<Omega>. P x} \<in> M \<Longrightarrow> {x\<in>\<Omega>. Q x} \<in> M \<Longrightarrow> {x\<in>\<Omega>. Q x \<longrightarrow> P x} \<in> M" |
|
207 unfolding imp_conv_disj by (intro sets_Collect_disj sets_Collect_neg) |
|
208 |
|
209 lemma (in algebra) sets_Collect_const: |
|
210 "{x\<in>\<Omega>. P} \<in> M" |
|
211 by (cases P) auto |
|
212 |
|
213 lemma algebra_single_set: |
|
214 "X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S - X, S }" |
|
215 by (auto simp: algebra_iff_Int) |
|
216 |
|
217 subsubsection \<open>Restricted algebras\<close> |
|
218 |
|
219 abbreviation (in algebra) |
|
220 "restricted_space A \<equiv> (op \<inter> A) ` M" |
|
221 |
|
222 lemma (in algebra) restricted_algebra: |
|
223 assumes "A \<in> M" shows "algebra A (restricted_space A)" |
|
224 using assms by (auto simp: algebra_iff_Int) |
|
225 |
|
226 subsubsection \<open>Sigma Algebras\<close> |
|
227 |
|
228 locale sigma_algebra = algebra + |
|
229 assumes countable_nat_UN [intro]: "\<And>A. range A \<subseteq> M \<Longrightarrow> (\<Union>i::nat. A i) \<in> M" |
|
230 |
|
231 lemma (in algebra) is_sigma_algebra: |
|
232 assumes "finite M" |
|
233 shows "sigma_algebra \<Omega> M" |
|
234 proof |
|
235 fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> M" |
|
236 then have "(\<Union>i. A i) = (\<Union>s\<in>M \<inter> range A. s)" |
|
237 by auto |
|
238 also have "(\<Union>s\<in>M \<inter> range A. s) \<in> M" |
|
239 using \<open>finite M\<close> by auto |
|
240 finally show "(\<Union>i. A i) \<in> M" . |
|
241 qed |
|
242 |
|
243 lemma countable_UN_eq: |
|
244 fixes A :: "'i::countable \<Rightarrow> 'a set" |
|
245 shows "(range A \<subseteq> M \<longrightarrow> (\<Union>i. A i) \<in> M) \<longleftrightarrow> |
|
246 (range (A \<circ> from_nat) \<subseteq> M \<longrightarrow> (\<Union>i. (A \<circ> from_nat) i) \<in> M)" |
|
247 proof - |
|
248 let ?A' = "A \<circ> from_nat" |
|
249 have *: "(\<Union>i. ?A' i) = (\<Union>i. A i)" (is "?l = ?r") |
|
250 proof safe |
|
251 fix x i assume "x \<in> A i" thus "x \<in> ?l" |
|
252 by (auto intro!: exI[of _ "to_nat i"]) |
|
253 next |
|
254 fix x i assume "x \<in> ?A' i" thus "x \<in> ?r" |
|
255 by (auto intro!: exI[of _ "from_nat i"]) |
|
256 qed |
|
257 have **: "range ?A' = range A" |
|
258 using surj_from_nat |
|
259 by (auto simp: image_comp [symmetric] intro!: imageI) |
|
260 show ?thesis unfolding * ** .. |
|
261 qed |
|
262 |
|
263 lemma (in sigma_algebra) countable_Union [intro]: |
|
264 assumes "countable X" "X \<subseteq> M" shows "\<Union>X \<in> M" |
|
265 proof cases |
|
266 assume "X \<noteq> {}" |
|
267 hence "\<Union>X = (\<Union>n. from_nat_into X n)" |
|
268 using assms by (auto intro: from_nat_into) (metis from_nat_into_surj) |
|
269 also have "\<dots> \<in> M" using assms |
|
270 by (auto intro!: countable_nat_UN) (metis \<open>X \<noteq> {}\<close> from_nat_into set_mp) |
|
271 finally show ?thesis . |
|
272 qed simp |
|
273 |
|
274 lemma (in sigma_algebra) countable_UN[intro]: |
|
275 fixes A :: "'i::countable \<Rightarrow> 'a set" |
|
276 assumes "A`X \<subseteq> M" |
|
277 shows "(\<Union>x\<in>X. A x) \<in> M" |
|
278 proof - |
|
279 let ?A = "\<lambda>i. if i \<in> X then A i else {}" |
|
280 from assms have "range ?A \<subseteq> M" by auto |
|
281 with countable_nat_UN[of "?A \<circ> from_nat"] countable_UN_eq[of ?A M] |
|
282 have "(\<Union>x. ?A x) \<in> M" by auto |
|
283 moreover have "(\<Union>x. ?A x) = (\<Union>x\<in>X. A x)" by (auto split: if_split_asm) |
|
284 ultimately show ?thesis by simp |
|
285 qed |
|
286 |
|
287 lemma (in sigma_algebra) countable_UN': |
|
288 fixes A :: "'i \<Rightarrow> 'a set" |
|
289 assumes X: "countable X" |
|
290 assumes A: "A`X \<subseteq> M" |
|
291 shows "(\<Union>x\<in>X. A x) \<in> M" |
|
292 proof - |
|
293 have "(\<Union>x\<in>X. A x) = (\<Union>i\<in>to_nat_on X ` X. A (from_nat_into X i))" |
|
294 using X by auto |
|
295 also have "\<dots> \<in> M" |
|
296 using A X |
|
297 by (intro countable_UN) auto |
|
298 finally show ?thesis . |
|
299 qed |
|
300 |
|
301 lemma (in sigma_algebra) countable_UN'': |
|
302 "\<lbrakk> countable X; \<And>x y. x \<in> X \<Longrightarrow> A x \<in> M \<rbrakk> \<Longrightarrow> (\<Union>x\<in>X. A x) \<in> M" |
|
303 by(erule countable_UN')(auto) |
|
304 |
|
305 lemma (in sigma_algebra) countable_INT [intro]: |
|
306 fixes A :: "'i::countable \<Rightarrow> 'a set" |
|
307 assumes A: "A`X \<subseteq> M" "X \<noteq> {}" |
|
308 shows "(\<Inter>i\<in>X. A i) \<in> M" |
|
309 proof - |
|
310 from A have "\<forall>i\<in>X. A i \<in> M" by fast |
|
311 hence "\<Omega> - (\<Union>i\<in>X. \<Omega> - A i) \<in> M" by blast |
|
312 moreover |
|
313 have "(\<Inter>i\<in>X. A i) = \<Omega> - (\<Union>i\<in>X. \<Omega> - A i)" using space_closed A |
|
314 by blast |
|
315 ultimately show ?thesis by metis |
|
316 qed |
|
317 |
|
318 lemma (in sigma_algebra) countable_INT': |
|
319 fixes A :: "'i \<Rightarrow> 'a set" |
|
320 assumes X: "countable X" "X \<noteq> {}" |
|
321 assumes A: "A`X \<subseteq> M" |
|
322 shows "(\<Inter>x\<in>X. A x) \<in> M" |
|
323 proof - |
|
324 have "(\<Inter>x\<in>X. A x) = (\<Inter>i\<in>to_nat_on X ` X. A (from_nat_into X i))" |
|
325 using X by auto |
|
326 also have "\<dots> \<in> M" |
|
327 using A X |
|
328 by (intro countable_INT) auto |
|
329 finally show ?thesis . |
|
330 qed |
|
331 |
|
332 lemma (in sigma_algebra) countable_INT'': |
|
333 "UNIV \<in> M \<Longrightarrow> countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i \<in> M) \<Longrightarrow> (\<Inter>i\<in>I. F i) \<in> M" |
|
334 by (cases "I = {}") (auto intro: countable_INT') |
|
335 |
|
336 lemma (in sigma_algebra) countable: |
|
337 assumes "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> M" "countable A" |
|
338 shows "A \<in> M" |
|
339 proof - |
|
340 have "(\<Union>a\<in>A. {a}) \<in> M" |
|
341 using assms by (intro countable_UN') auto |
|
342 also have "(\<Union>a\<in>A. {a}) = A" by auto |
|
343 finally show ?thesis by auto |
|
344 qed |
|
345 |
|
346 lemma ring_of_sets_Pow: "ring_of_sets sp (Pow sp)" |
|
347 by (auto simp: ring_of_sets_iff) |
|
348 |
|
349 lemma algebra_Pow: "algebra sp (Pow sp)" |
|
350 by (auto simp: algebra_iff_Un) |
|
351 |
|
352 lemma sigma_algebra_iff: |
|
353 "sigma_algebra \<Omega> M \<longleftrightarrow> |
|
354 algebra \<Omega> M \<and> (\<forall>A. range A \<subseteq> M \<longrightarrow> (\<Union>i::nat. A i) \<in> M)" |
|
355 by (simp add: sigma_algebra_def sigma_algebra_axioms_def) |
|
356 |
|
357 lemma sigma_algebra_Pow: "sigma_algebra sp (Pow sp)" |
|
358 by (auto simp: sigma_algebra_iff algebra_iff_Int) |
|
359 |
|
360 lemma (in sigma_algebra) sets_Collect_countable_All: |
|
361 assumes "\<And>i. {x\<in>\<Omega>. P i x} \<in> M" |
|
362 shows "{x\<in>\<Omega>. \<forall>i::'i::countable. P i x} \<in> M" |
|
363 proof - |
|
364 have "{x\<in>\<Omega>. \<forall>i::'i::countable. P i x} = (\<Inter>i. {x\<in>\<Omega>. P i x})" by auto |
|
365 with assms show ?thesis by auto |
|
366 qed |
|
367 |
|
368 lemma (in sigma_algebra) sets_Collect_countable_Ex: |
|
369 assumes "\<And>i. {x\<in>\<Omega>. P i x} \<in> M" |
|
370 shows "{x\<in>\<Omega>. \<exists>i::'i::countable. P i x} \<in> M" |
|
371 proof - |
|
372 have "{x\<in>\<Omega>. \<exists>i::'i::countable. P i x} = (\<Union>i. {x\<in>\<Omega>. P i x})" by auto |
|
373 with assms show ?thesis by auto |
|
374 qed |
|
375 |
|
376 lemma (in sigma_algebra) sets_Collect_countable_Ex': |
|
377 assumes "\<And>i. i \<in> I \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" |
|
378 assumes "countable I" |
|
379 shows "{x\<in>\<Omega>. \<exists>i\<in>I. P i x} \<in> M" |
|
380 proof - |
|
381 have "{x\<in>\<Omega>. \<exists>i\<in>I. P i x} = (\<Union>i\<in>I. {x\<in>\<Omega>. P i x})" by auto |
|
382 with assms show ?thesis |
|
383 by (auto intro!: countable_UN') |
|
384 qed |
|
385 |
|
386 lemma (in sigma_algebra) sets_Collect_countable_All': |
|
387 assumes "\<And>i. i \<in> I \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" |
|
388 assumes "countable I" |
|
389 shows "{x\<in>\<Omega>. \<forall>i\<in>I. P i x} \<in> M" |
|
390 proof - |
|
391 have "{x\<in>\<Omega>. \<forall>i\<in>I. P i x} = (\<Inter>i\<in>I. {x\<in>\<Omega>. P i x}) \<inter> \<Omega>" by auto |
|
392 with assms show ?thesis |
|
393 by (cases "I = {}") (auto intro!: countable_INT') |
|
394 qed |
|
395 |
|
396 lemma (in sigma_algebra) sets_Collect_countable_Ex1': |
|
397 assumes "\<And>i. i \<in> I \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" |
|
398 assumes "countable I" |
|
399 shows "{x\<in>\<Omega>. \<exists>!i\<in>I. P i x} \<in> M" |
|
400 proof - |
|
401 have "{x\<in>\<Omega>. \<exists>!i\<in>I. P i x} = {x\<in>\<Omega>. \<exists>i\<in>I. P i x \<and> (\<forall>j\<in>I. P j x \<longrightarrow> i = j)}" |
|
402 by auto |
|
403 with assms show ?thesis |
|
404 by (auto intro!: sets_Collect_countable_All' sets_Collect_countable_Ex' sets_Collect_conj sets_Collect_imp sets_Collect_const) |
|
405 qed |
|
406 |
|
407 lemmas (in sigma_algebra) sets_Collect = |
|
408 sets_Collect_imp sets_Collect_disj sets_Collect_conj sets_Collect_neg sets_Collect_const |
|
409 sets_Collect_countable_All sets_Collect_countable_Ex sets_Collect_countable_All |
|
410 |
|
411 lemma (in sigma_algebra) sets_Collect_countable_Ball: |
|
412 assumes "\<And>i. {x\<in>\<Omega>. P i x} \<in> M" |
|
413 shows "{x\<in>\<Omega>. \<forall>i::'i::countable\<in>X. P i x} \<in> M" |
|
414 unfolding Ball_def by (intro sets_Collect assms) |
|
415 |
|
416 lemma (in sigma_algebra) sets_Collect_countable_Bex: |
|
417 assumes "\<And>i. {x\<in>\<Omega>. P i x} \<in> M" |
|
418 shows "{x\<in>\<Omega>. \<exists>i::'i::countable\<in>X. P i x} \<in> M" |
|
419 unfolding Bex_def by (intro sets_Collect assms) |
|
420 |
|
421 lemma sigma_algebra_single_set: |
|
422 assumes "X \<subseteq> S" |
|
423 shows "sigma_algebra S { {}, X, S - X, S }" |
|
424 using algebra.is_sigma_algebra[OF algebra_single_set[OF \<open>X \<subseteq> S\<close>]] by simp |
|
425 |
|
426 subsubsection \<open>Binary Unions\<close> |
|
427 |
|
428 definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" |
|
429 where "binary a b = (\<lambda>x. b)(0 := a)" |
|
430 |
|
431 lemma range_binary_eq: "range(binary a b) = {a,b}" |
|
432 by (auto simp add: binary_def) |
|
433 |
|
434 lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)" |
|
435 by (simp add: range_binary_eq cong del: strong_SUP_cong) |
|
436 |
|
437 lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)" |
|
438 by (simp add: range_binary_eq cong del: strong_INF_cong) |
|
439 |
|
440 lemma sigma_algebra_iff2: |
|
441 "sigma_algebra \<Omega> M \<longleftrightarrow> |
|
442 M \<subseteq> Pow \<Omega> \<and> |
|
443 {} \<in> M \<and> (\<forall>s \<in> M. \<Omega> - s \<in> M) \<and> |
|
444 (\<forall>A. range A \<subseteq> M \<longrightarrow> (\<Union>i::nat. A i) \<in> M)" |
|
445 by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def |
|
446 algebra_iff_Un Un_range_binary) |
|
447 |
|
448 subsubsection \<open>Initial Sigma Algebra\<close> |
|
449 |
|
450 text \<open>Sigma algebras can naturally be created as the closure of any set of |
|
451 M with regard to the properties just postulated.\<close> |
|
452 |
|
453 inductive_set sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" |
|
454 for sp :: "'a set" and A :: "'a set set" |
|
455 where |
|
456 Basic[intro, simp]: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A" |
|
457 | Empty: "{} \<in> sigma_sets sp A" |
|
458 | Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp - a \<in> sigma_sets sp A" |
|
459 | Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A" |
|
460 |
|
461 lemma (in sigma_algebra) sigma_sets_subset: |
|
462 assumes a: "a \<subseteq> M" |
|
463 shows "sigma_sets \<Omega> a \<subseteq> M" |
|
464 proof |
|
465 fix x |
|
466 assume "x \<in> sigma_sets \<Omega> a" |
|
467 from this show "x \<in> M" |
|
468 by (induct rule: sigma_sets.induct, auto) (metis a subsetD) |
|
469 qed |
|
470 |
|
471 lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp" |
|
472 by (erule sigma_sets.induct, auto) |
|
473 |
|
474 lemma sigma_algebra_sigma_sets: |
|
475 "a \<subseteq> Pow \<Omega> \<Longrightarrow> sigma_algebra \<Omega> (sigma_sets \<Omega> a)" |
|
476 by (auto simp add: sigma_algebra_iff2 dest: sigma_sets_into_sp |
|
477 intro!: sigma_sets.Union sigma_sets.Empty sigma_sets.Compl) |
|
478 |
|
479 lemma sigma_sets_least_sigma_algebra: |
|
480 assumes "A \<subseteq> Pow S" |
|
481 shows "sigma_sets S A = \<Inter>{B. A \<subseteq> B \<and> sigma_algebra S B}" |
|
482 proof safe |
|
483 fix B X assume "A \<subseteq> B" and sa: "sigma_algebra S B" |
|
484 and X: "X \<in> sigma_sets S A" |
|
485 from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF \<open>A \<subseteq> B\<close>] X |
|
486 show "X \<in> B" by auto |
|
487 next |
|
488 fix X assume "X \<in> \<Inter>{B. A \<subseteq> B \<and> sigma_algebra S B}" |
|
489 then have [intro!]: "\<And>B. A \<subseteq> B \<Longrightarrow> sigma_algebra S B \<Longrightarrow> X \<in> B" |
|
490 by simp |
|
491 have "A \<subseteq> sigma_sets S A" using assms by auto |
|
492 moreover have "sigma_algebra S (sigma_sets S A)" |
|
493 using assms by (intro sigma_algebra_sigma_sets[of A]) auto |
|
494 ultimately show "X \<in> sigma_sets S A" by auto |
|
495 qed |
|
496 |
|
497 lemma sigma_sets_top: "sp \<in> sigma_sets sp A" |
|
498 by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty) |
|
499 |
|
500 lemma sigma_sets_Un: |
|
501 "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A" |
|
502 apply (simp add: Un_range_binary range_binary_eq) |
|
503 apply (rule Union, simp add: binary_def) |
|
504 done |
|
505 |
|
506 lemma sigma_sets_Inter: |
|
507 assumes Asb: "A \<subseteq> Pow sp" |
|
508 shows "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Inter>i. a i) \<in> sigma_sets sp A" |
|
509 proof - |
|
510 assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A" |
|
511 hence "\<And>i::nat. sp-(a i) \<in> sigma_sets sp A" |
|
512 by (rule sigma_sets.Compl) |
|
513 hence "(\<Union>i. sp-(a i)) \<in> sigma_sets sp A" |
|
514 by (rule sigma_sets.Union) |
|
515 hence "sp-(\<Union>i. sp-(a i)) \<in> sigma_sets sp A" |
|
516 by (rule sigma_sets.Compl) |
|
517 also have "sp-(\<Union>i. sp-(a i)) = sp Int (\<Inter>i. a i)" |
|
518 by auto |
|
519 also have "... = (\<Inter>i. a i)" using ai |
|
520 by (blast dest: sigma_sets_into_sp [OF Asb]) |
|
521 finally show ?thesis . |
|
522 qed |
|
523 |
|
524 lemma sigma_sets_INTER: |
|
525 assumes Asb: "A \<subseteq> Pow sp" |
|
526 and ai: "\<And>i::nat. i \<in> S \<Longrightarrow> a i \<in> sigma_sets sp A" and non: "S \<noteq> {}" |
|
527 shows "(\<Inter>i\<in>S. a i) \<in> sigma_sets sp A" |
|
528 proof - |
|
529 from ai have "\<And>i. (if i\<in>S then a i else sp) \<in> sigma_sets sp A" |
|
530 by (simp add: sigma_sets.intros(2-) sigma_sets_top) |
|
531 hence "(\<Inter>i. (if i\<in>S then a i else sp)) \<in> sigma_sets sp A" |
|
532 by (rule sigma_sets_Inter [OF Asb]) |
|
533 also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>S. a i)" |
|
534 by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+ |
|
535 finally show ?thesis . |
|
536 qed |
|
537 |
|
538 lemma sigma_sets_UNION: |
|
539 "countable B \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets X A) \<Longrightarrow> (\<Union>B) \<in> sigma_sets X A" |
|
540 apply (cases "B = {}") |
|
541 apply (simp add: sigma_sets.Empty) |
|
542 using from_nat_into [of B] range_from_nat_into [of B] sigma_sets.Union [of "from_nat_into B" X A] |
|
543 apply simp |
|
544 apply auto |
|
545 apply (metis Sup_bot_conv(1) Union_empty \<open>\<lbrakk>B \<noteq> {}; countable B\<rbrakk> \<Longrightarrow> range (from_nat_into B) = B\<close>) |
|
546 done |
|
547 |
|
548 lemma (in sigma_algebra) sigma_sets_eq: |
|
549 "sigma_sets \<Omega> M = M" |
|
550 proof |
|
551 show "M \<subseteq> sigma_sets \<Omega> M" |
|
552 by (metis Set.subsetI sigma_sets.Basic) |
|
553 next |
|
554 show "sigma_sets \<Omega> M \<subseteq> M" |
|
555 by (metis sigma_sets_subset subset_refl) |
|
556 qed |
|
557 |
|
558 lemma sigma_sets_eqI: |
|
559 assumes A: "\<And>a. a \<in> A \<Longrightarrow> a \<in> sigma_sets M B" |
|
560 assumes B: "\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets M A" |
|
561 shows "sigma_sets M A = sigma_sets M B" |
|
562 proof (intro set_eqI iffI) |
|
563 fix a assume "a \<in> sigma_sets M A" |
|
564 from this A show "a \<in> sigma_sets M B" |
|
565 by induct (auto intro!: sigma_sets.intros(2-) del: sigma_sets.Basic) |
|
566 next |
|
567 fix b assume "b \<in> sigma_sets M B" |
|
568 from this B show "b \<in> sigma_sets M A" |
|
569 by induct (auto intro!: sigma_sets.intros(2-) del: sigma_sets.Basic) |
|
570 qed |
|
571 |
|
572 lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B" |
|
573 proof |
|
574 fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B" |
|
575 by induct (insert \<open>A \<subseteq> B\<close>, auto intro: sigma_sets.intros(2-)) |
|
576 qed |
|
577 |
|
578 lemma sigma_sets_mono: assumes "A \<subseteq> sigma_sets X B" shows "sigma_sets X A \<subseteq> sigma_sets X B" |
|
579 proof |
|
580 fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B" |
|
581 by induct (insert \<open>A \<subseteq> sigma_sets X B\<close>, auto intro: sigma_sets.intros(2-)) |
|
582 qed |
|
583 |
|
584 lemma sigma_sets_mono': assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B" |
|
585 proof |
|
586 fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B" |
|
587 by induct (insert \<open>A \<subseteq> B\<close>, auto intro: sigma_sets.intros(2-)) |
|
588 qed |
|
589 |
|
590 lemma sigma_sets_superset_generator: "A \<subseteq> sigma_sets X A" |
|
591 by (auto intro: sigma_sets.Basic) |
|
592 |
|
593 lemma (in sigma_algebra) restriction_in_sets: |
|
594 fixes A :: "nat \<Rightarrow> 'a set" |
|
595 assumes "S \<in> M" |
|
596 and *: "range A \<subseteq> (\<lambda>A. S \<inter> A) ` M" (is "_ \<subseteq> ?r") |
|
597 shows "range A \<subseteq> M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` M" |
|
598 proof - |
|
599 { fix i have "A i \<in> ?r" using * by auto |
|
600 hence "\<exists>B. A i = B \<inter> S \<and> B \<in> M" by auto |
|
601 hence "A i \<subseteq> S" "A i \<in> M" using \<open>S \<in> M\<close> by auto } |
|
602 thus "range A \<subseteq> M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` M" |
|
603 by (auto intro!: image_eqI[of _ _ "(\<Union>i. A i)"]) |
|
604 qed |
|
605 |
|
606 lemma (in sigma_algebra) restricted_sigma_algebra: |
|
607 assumes "S \<in> M" |
|
608 shows "sigma_algebra S (restricted_space S)" |
|
609 unfolding sigma_algebra_def sigma_algebra_axioms_def |
|
610 proof safe |
|
611 show "algebra S (restricted_space S)" using restricted_algebra[OF assms] . |
|
612 next |
|
613 fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> restricted_space S" |
|
614 from restriction_in_sets[OF assms this[simplified]] |
|
615 show "(\<Union>i. A i) \<in> restricted_space S" by simp |
|
616 qed |
|
617 |
|
618 lemma sigma_sets_Int: |
|
619 assumes "A \<in> sigma_sets sp st" "A \<subseteq> sp" |
|
620 shows "op \<inter> A ` sigma_sets sp st = sigma_sets A (op \<inter> A ` st)" |
|
621 proof (intro equalityI subsetI) |
|
622 fix x assume "x \<in> op \<inter> A ` sigma_sets sp st" |
|
623 then obtain y where "y \<in> sigma_sets sp st" "x = y \<inter> A" by auto |
|
624 then have "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)" |
|
625 proof (induct arbitrary: x) |
|
626 case (Compl a) |
|
627 then show ?case |
|
628 by (force intro!: sigma_sets.Compl simp: Diff_Int_distrib ac_simps) |
|
629 next |
|
630 case (Union a) |
|
631 then show ?case |
|
632 by (auto intro!: sigma_sets.Union |
|
633 simp add: UN_extend_simps simp del: UN_simps) |
|
634 qed (auto intro!: sigma_sets.intros(2-)) |
|
635 then show "x \<in> sigma_sets A (op \<inter> A ` st)" |
|
636 using \<open>A \<subseteq> sp\<close> by (simp add: Int_absorb2) |
|
637 next |
|
638 fix x assume "x \<in> sigma_sets A (op \<inter> A ` st)" |
|
639 then show "x \<in> op \<inter> A ` sigma_sets sp st" |
|
640 proof induct |
|
641 case (Compl a) |
|
642 then obtain x where "a = A \<inter> x" "x \<in> sigma_sets sp st" by auto |
|
643 then show ?case using \<open>A \<subseteq> sp\<close> |
|
644 by (force simp add: image_iff intro!: bexI[of _ "sp - x"] sigma_sets.Compl) |
|
645 next |
|
646 case (Union a) |
|
647 then have "\<forall>i. \<exists>x. x \<in> sigma_sets sp st \<and> a i = A \<inter> x" |
|
648 by (auto simp: image_iff Bex_def) |
|
649 from choice[OF this] guess f .. |
|
650 then show ?case |
|
651 by (auto intro!: bexI[of _ "(\<Union>x. f x)"] sigma_sets.Union |
|
652 simp add: image_iff) |
|
653 qed (auto intro!: sigma_sets.intros(2-)) |
|
654 qed |
|
655 |
|
656 lemma sigma_sets_empty_eq: "sigma_sets A {} = {{}, A}" |
|
657 proof (intro set_eqI iffI) |
|
658 fix a assume "a \<in> sigma_sets A {}" then show "a \<in> {{}, A}" |
|
659 by induct blast+ |
|
660 qed (auto intro: sigma_sets.Empty sigma_sets_top) |
|
661 |
|
662 lemma sigma_sets_single[simp]: "sigma_sets A {A} = {{}, A}" |
|
663 proof (intro set_eqI iffI) |
|
664 fix x assume "x \<in> sigma_sets A {A}" |
|
665 then show "x \<in> {{}, A}" |
|
666 by induct blast+ |
|
667 next |
|
668 fix x assume "x \<in> {{}, A}" |
|
669 then show "x \<in> sigma_sets A {A}" |
|
670 by (auto intro: sigma_sets.Empty sigma_sets_top) |
|
671 qed |
|
672 |
|
673 lemma sigma_sets_sigma_sets_eq: |
|
674 "M \<subseteq> Pow S \<Longrightarrow> sigma_sets S (sigma_sets S M) = sigma_sets S M" |
|
675 by (rule sigma_algebra.sigma_sets_eq[OF sigma_algebra_sigma_sets, of M S]) auto |
|
676 |
|
677 lemma sigma_sets_singleton: |
|
678 assumes "X \<subseteq> S" |
|
679 shows "sigma_sets S { X } = { {}, X, S - X, S }" |
|
680 proof - |
|
681 interpret sigma_algebra S "{ {}, X, S - X, S }" |
|
682 by (rule sigma_algebra_single_set) fact |
|
683 have "sigma_sets S { X } \<subseteq> sigma_sets S { {}, X, S - X, S }" |
|
684 by (rule sigma_sets_subseteq) simp |
|
685 moreover have "\<dots> = { {}, X, S - X, S }" |
|
686 using sigma_sets_eq by simp |
|
687 moreover |
|
688 { fix A assume "A \<in> { {}, X, S - X, S }" |
|
689 then have "A \<in> sigma_sets S { X }" |
|
690 by (auto intro: sigma_sets.intros(2-) sigma_sets_top) } |
|
691 ultimately have "sigma_sets S { X } = sigma_sets S { {}, X, S - X, S }" |
|
692 by (intro antisym) auto |
|
693 with sigma_sets_eq show ?thesis by simp |
|
694 qed |
|
695 |
|
696 lemma restricted_sigma: |
|
697 assumes S: "S \<in> sigma_sets \<Omega> M" and M: "M \<subseteq> Pow \<Omega>" |
|
698 shows "algebra.restricted_space (sigma_sets \<Omega> M) S = |
|
699 sigma_sets S (algebra.restricted_space M S)" |
|
700 proof - |
|
701 from S sigma_sets_into_sp[OF M] |
|
702 have "S \<in> sigma_sets \<Omega> M" "S \<subseteq> \<Omega>" by auto |
|
703 from sigma_sets_Int[OF this] |
|
704 show ?thesis by simp |
|
705 qed |
|
706 |
|
707 lemma sigma_sets_vimage_commute: |
|
708 assumes X: "X \<in> \<Omega> \<rightarrow> \<Omega>'" |
|
709 shows "{X -` A \<inter> \<Omega> |A. A \<in> sigma_sets \<Omega>' M'} |
|
710 = sigma_sets \<Omega> {X -` A \<inter> \<Omega> |A. A \<in> M'}" (is "?L = ?R") |
|
711 proof |
|
712 show "?L \<subseteq> ?R" |
|
713 proof clarify |
|
714 fix A assume "A \<in> sigma_sets \<Omega>' M'" |
|
715 then show "X -` A \<inter> \<Omega> \<in> ?R" |
|
716 proof induct |
|
717 case Empty then show ?case |
|
718 by (auto intro!: sigma_sets.Empty) |
|
719 next |
|
720 case (Compl B) |
|
721 have [simp]: "X -` (\<Omega>' - B) \<inter> \<Omega> = \<Omega> - (X -` B \<inter> \<Omega>)" |
|
722 by (auto simp add: funcset_mem [OF X]) |
|
723 with Compl show ?case |
|
724 by (auto intro!: sigma_sets.Compl) |
|
725 next |
|
726 case (Union F) |
|
727 then show ?case |
|
728 by (auto simp add: vimage_UN UN_extend_simps(4) simp del: UN_simps |
|
729 intro!: sigma_sets.Union) |
|
730 qed auto |
|
731 qed |
|
732 show "?R \<subseteq> ?L" |
|
733 proof clarify |
|
734 fix A assume "A \<in> ?R" |
|
735 then show "\<exists>B. A = X -` B \<inter> \<Omega> \<and> B \<in> sigma_sets \<Omega>' M'" |
|
736 proof induct |
|
737 case (Basic B) then show ?case by auto |
|
738 next |
|
739 case Empty then show ?case |
|
740 by (auto intro!: sigma_sets.Empty exI[of _ "{}"]) |
|
741 next |
|
742 case (Compl B) |
|
743 then obtain A where A: "B = X -` A \<inter> \<Omega>" "A \<in> sigma_sets \<Omega>' M'" by auto |
|
744 then have [simp]: "\<Omega> - B = X -` (\<Omega>' - A) \<inter> \<Omega>" |
|
745 by (auto simp add: funcset_mem [OF X]) |
|
746 with A(2) show ?case |
|
747 by (auto intro: sigma_sets.Compl) |
|
748 next |
|
749 case (Union F) |
|
750 then have "\<forall>i. \<exists>B. F i = X -` B \<inter> \<Omega> \<and> B \<in> sigma_sets \<Omega>' M'" by auto |
|
751 from choice[OF this] guess A .. note A = this |
|
752 with A show ?case |
|
753 by (auto simp: vimage_UN[symmetric] intro: sigma_sets.Union) |
|
754 qed |
|
755 qed |
|
756 qed |
|
757 |
|
758 lemma (in ring_of_sets) UNION_in_sets: |
|
759 fixes A:: "nat \<Rightarrow> 'a set" |
|
760 assumes A: "range A \<subseteq> M" |
|
761 shows "(\<Union>i\<in>{0..<n}. A i) \<in> M" |
|
762 proof (induct n) |
|
763 case 0 show ?case by simp |
|
764 next |
|
765 case (Suc n) |
|
766 thus ?case |
|
767 by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff) |
|
768 qed |
|
769 |
|
770 lemma (in ring_of_sets) range_disjointed_sets: |
|
771 assumes A: "range A \<subseteq> M" |
|
772 shows "range (disjointed A) \<subseteq> M" |
|
773 proof (auto simp add: disjointed_def) |
|
774 fix n |
|
775 show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> M" using UNION_in_sets |
|
776 by (metis A Diff UNIV_I image_subset_iff) |
|
777 qed |
|
778 |
|
779 lemma (in algebra) range_disjointed_sets': |
|
780 "range A \<subseteq> M \<Longrightarrow> range (disjointed A) \<subseteq> M" |
|
781 using range_disjointed_sets . |
|
782 |
|
783 lemma sigma_algebra_disjoint_iff: |
|
784 "sigma_algebra \<Omega> M \<longleftrightarrow> algebra \<Omega> M \<and> |
|
785 (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> M)" |
|
786 proof (auto simp add: sigma_algebra_iff) |
|
787 fix A :: "nat \<Rightarrow> 'a set" |
|
788 assume M: "algebra \<Omega> M" |
|
789 and A: "range A \<subseteq> M" |
|
790 and UnA: "\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> M" |
|
791 hence "range (disjointed A) \<subseteq> M \<longrightarrow> |
|
792 disjoint_family (disjointed A) \<longrightarrow> |
|
793 (\<Union>i. disjointed A i) \<in> M" by blast |
|
794 hence "(\<Union>i. disjointed A i) \<in> M" |
|
795 by (simp add: algebra.range_disjointed_sets'[of \<Omega>] M A disjoint_family_disjointed) |
|
796 thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq) |
|
797 qed |
|
798 |
|
799 subsubsection \<open>Ring generated by a semiring\<close> |
|
800 |
|
801 definition (in semiring_of_sets) |
|
802 "generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }" |
|
803 |
|
804 lemma (in semiring_of_sets) generated_ringE[elim?]: |
|
805 assumes "a \<in> generated_ring" |
|
806 obtains C where "finite C" "disjoint C" "C \<subseteq> M" "a = \<Union>C" |
|
807 using assms unfolding generated_ring_def by auto |
|
808 |
|
809 lemma (in semiring_of_sets) generated_ringI[intro?]: |
|
810 assumes "finite C" "disjoint C" "C \<subseteq> M" "a = \<Union>C" |
|
811 shows "a \<in> generated_ring" |
|
812 using assms unfolding generated_ring_def by auto |
|
813 |
|
814 lemma (in semiring_of_sets) generated_ringI_Basic: |
|
815 "A \<in> M \<Longrightarrow> A \<in> generated_ring" |
|
816 by (rule generated_ringI[of "{A}"]) (auto simp: disjoint_def) |
|
817 |
|
818 lemma (in semiring_of_sets) generated_ring_disjoint_Un[intro]: |
|
819 assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring" |
|
820 and "a \<inter> b = {}" |
|
821 shows "a \<union> b \<in> generated_ring" |
|
822 proof - |
|
823 from a guess Ca .. note Ca = this |
|
824 from b guess Cb .. note Cb = this |
|
825 show ?thesis |
|
826 proof |
|
827 show "disjoint (Ca \<union> Cb)" |
|
828 using \<open>a \<inter> b = {}\<close> Ca Cb by (auto intro!: disjoint_union) |
|
829 qed (insert Ca Cb, auto) |
|
830 qed |
|
831 |
|
832 lemma (in semiring_of_sets) generated_ring_empty: "{} \<in> generated_ring" |
|
833 by (auto simp: generated_ring_def disjoint_def) |
|
834 |
|
835 lemma (in semiring_of_sets) generated_ring_disjoint_Union: |
|
836 assumes "finite A" shows "A \<subseteq> generated_ring \<Longrightarrow> disjoint A \<Longrightarrow> \<Union>A \<in> generated_ring" |
|
837 using assms by (induct A) (auto simp: disjoint_def intro!: generated_ring_disjoint_Un generated_ring_empty) |
|
838 |
|
839 lemma (in semiring_of_sets) generated_ring_disjoint_UNION: |
|
840 "finite I \<Longrightarrow> disjoint (A ` I) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> UNION I A \<in> generated_ring" |
|
841 by (intro generated_ring_disjoint_Union) auto |
|
842 |
|
843 lemma (in semiring_of_sets) generated_ring_Int: |
|
844 assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring" |
|
845 shows "a \<inter> b \<in> generated_ring" |
|
846 proof - |
|
847 from a guess Ca .. note Ca = this |
|
848 from b guess Cb .. note Cb = this |
|
849 define C where "C = (\<lambda>(a,b). a \<inter> b)` (Ca\<times>Cb)" |
|
850 show ?thesis |
|
851 proof |
|
852 show "disjoint C" |
|
853 proof (simp add: disjoint_def C_def, intro ballI impI) |
|
854 fix a1 b1 a2 b2 assume sets: "a1 \<in> Ca" "b1 \<in> Cb" "a2 \<in> Ca" "b2 \<in> Cb" |
|
855 assume "a1 \<inter> b1 \<noteq> a2 \<inter> b2" |
|
856 then have "a1 \<noteq> a2 \<or> b1 \<noteq> b2" by auto |
|
857 then show "(a1 \<inter> b1) \<inter> (a2 \<inter> b2) = {}" |
|
858 proof |
|
859 assume "a1 \<noteq> a2" |
|
860 with sets Ca have "a1 \<inter> a2 = {}" |
|
861 by (auto simp: disjoint_def) |
|
862 then show ?thesis by auto |
|
863 next |
|
864 assume "b1 \<noteq> b2" |
|
865 with sets Cb have "b1 \<inter> b2 = {}" |
|
866 by (auto simp: disjoint_def) |
|
867 then show ?thesis by auto |
|
868 qed |
|
869 qed |
|
870 qed (insert Ca Cb, auto simp: C_def) |
|
871 qed |
|
872 |
|
873 lemma (in semiring_of_sets) generated_ring_Inter: |
|
874 assumes "finite A" "A \<noteq> {}" shows "A \<subseteq> generated_ring \<Longrightarrow> \<Inter>A \<in> generated_ring" |
|
875 using assms by (induct A rule: finite_ne_induct) (auto intro: generated_ring_Int) |
|
876 |
|
877 lemma (in semiring_of_sets) generated_ring_INTER: |
|
878 "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> INTER I A \<in> generated_ring" |
|
879 by (intro generated_ring_Inter) auto |
|
880 |
|
881 lemma (in semiring_of_sets) generating_ring: |
|
882 "ring_of_sets \<Omega> generated_ring" |
|
883 proof (rule ring_of_setsI) |
|
884 let ?R = generated_ring |
|
885 show "?R \<subseteq> Pow \<Omega>" |
|
886 using sets_into_space by (auto simp: generated_ring_def generated_ring_empty) |
|
887 show "{} \<in> ?R" by (rule generated_ring_empty) |
|
888 |
|
889 { fix a assume a: "a \<in> ?R" then guess Ca .. note Ca = this |
|
890 fix b assume b: "b \<in> ?R" then guess Cb .. note Cb = this |
|
891 |
|
892 show "a - b \<in> ?R" |
|
893 proof cases |
|
894 assume "Cb = {}" with Cb \<open>a \<in> ?R\<close> show ?thesis |
|
895 by simp |
|
896 next |
|
897 assume "Cb \<noteq> {}" |
|
898 with Ca Cb have "a - b = (\<Union>a'\<in>Ca. \<Inter>b'\<in>Cb. a' - b')" by auto |
|
899 also have "\<dots> \<in> ?R" |
|
900 proof (intro generated_ring_INTER generated_ring_disjoint_UNION) |
|
901 fix a b assume "a \<in> Ca" "b \<in> Cb" |
|
902 with Ca Cb Diff_cover[of a b] show "a - b \<in> ?R" |
|
903 by (auto simp add: generated_ring_def) |
|
904 (metis DiffI Diff_eq_empty_iff empty_iff) |
|
905 next |
|
906 show "disjoint ((\<lambda>a'. \<Inter>b'\<in>Cb. a' - b')`Ca)" |
|
907 using Ca by (auto simp add: disjoint_def \<open>Cb \<noteq> {}\<close>) |
|
908 next |
|
909 show "finite Ca" "finite Cb" "Cb \<noteq> {}" by fact+ |
|
910 qed |
|
911 finally show "a - b \<in> ?R" . |
|
912 qed } |
|
913 note Diff = this |
|
914 |
|
915 fix a b assume sets: "a \<in> ?R" "b \<in> ?R" |
|
916 have "a \<union> b = (a - b) \<union> (a \<inter> b) \<union> (b - a)" by auto |
|
917 also have "\<dots> \<in> ?R" |
|
918 by (intro sets generated_ring_disjoint_Un generated_ring_Int Diff) auto |
|
919 finally show "a \<union> b \<in> ?R" . |
|
920 qed |
|
921 |
|
922 lemma (in semiring_of_sets) sigma_sets_generated_ring_eq: "sigma_sets \<Omega> generated_ring = sigma_sets \<Omega> M" |
|
923 proof |
|
924 interpret M: sigma_algebra \<Omega> "sigma_sets \<Omega> M" |
|
925 using space_closed by (rule sigma_algebra_sigma_sets) |
|
926 show "sigma_sets \<Omega> generated_ring \<subseteq> sigma_sets \<Omega> M" |
|
927 by (blast intro!: sigma_sets_mono elim: generated_ringE) |
|
928 qed (auto intro!: generated_ringI_Basic sigma_sets_mono) |
|
929 |
|
930 subsubsection \<open>A Two-Element Series\<close> |
|
931 |
|
932 definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set" |
|
933 where "binaryset A B = (\<lambda>x. {})(0 := A, Suc 0 := B)" |
|
934 |
|
935 lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}" |
|
936 apply (simp add: binaryset_def) |
|
937 apply (rule set_eqI) |
|
938 apply (auto simp add: image_iff) |
|
939 done |
|
940 |
|
941 lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B" |
|
942 by (simp add: range_binaryset_eq cong del: strong_SUP_cong) |
|
943 |
|
944 subsubsection \<open>Closed CDI\<close> |
|
945 |
|
946 definition closed_cdi where |
|
947 "closed_cdi \<Omega> M \<longleftrightarrow> |
|
948 M \<subseteq> Pow \<Omega> & |
|
949 (\<forall>s \<in> M. \<Omega> - s \<in> M) & |
|
950 (\<forall>A. (range A \<subseteq> M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow> |
|
951 (\<Union>i. A i) \<in> M) & |
|
952 (\<forall>A. (range A \<subseteq> M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> M)" |
|
953 |
|
954 inductive_set |
|
955 smallest_ccdi_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" |
|
956 for \<Omega> M |
|
957 where |
|
958 Basic [intro]: |
|
959 "a \<in> M \<Longrightarrow> a \<in> smallest_ccdi_sets \<Omega> M" |
|
960 | Compl [intro]: |
|
961 "a \<in> smallest_ccdi_sets \<Omega> M \<Longrightarrow> \<Omega> - a \<in> smallest_ccdi_sets \<Omega> M" |
|
962 | Inc: |
|
963 "range A \<in> Pow(smallest_ccdi_sets \<Omega> M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n)) |
|
964 \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets \<Omega> M" |
|
965 | Disj: |
|
966 "range A \<in> Pow(smallest_ccdi_sets \<Omega> M) \<Longrightarrow> disjoint_family A |
|
967 \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets \<Omega> M" |
|
968 |
|
969 lemma (in subset_class) smallest_closed_cdi1: "M \<subseteq> smallest_ccdi_sets \<Omega> M" |
|
970 by auto |
|
971 |
|
972 lemma (in subset_class) smallest_ccdi_sets: "smallest_ccdi_sets \<Omega> M \<subseteq> Pow \<Omega>" |
|
973 apply (rule subsetI) |
|
974 apply (erule smallest_ccdi_sets.induct) |
|
975 apply (auto intro: range_subsetD dest: sets_into_space) |
|
976 done |
|
977 |
|
978 lemma (in subset_class) smallest_closed_cdi2: "closed_cdi \<Omega> (smallest_ccdi_sets \<Omega> M)" |
|
979 apply (auto simp add: closed_cdi_def smallest_ccdi_sets) |
|
980 apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) + |
|
981 done |
|
982 |
|
983 lemma closed_cdi_subset: "closed_cdi \<Omega> M \<Longrightarrow> M \<subseteq> Pow \<Omega>" |
|
984 by (simp add: closed_cdi_def) |
|
985 |
|
986 lemma closed_cdi_Compl: "closed_cdi \<Omega> M \<Longrightarrow> s \<in> M \<Longrightarrow> \<Omega> - s \<in> M" |
|
987 by (simp add: closed_cdi_def) |
|
988 |
|
989 lemma closed_cdi_Inc: |
|
990 "closed_cdi \<Omega> M \<Longrightarrow> range A \<subseteq> M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow> (\<Union>i. A i) \<in> M" |
|
991 by (simp add: closed_cdi_def) |
|
992 |
|
993 lemma closed_cdi_Disj: |
|
994 "closed_cdi \<Omega> M \<Longrightarrow> range A \<subseteq> M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> M" |
|
995 by (simp add: closed_cdi_def) |
|
996 |
|
997 lemma closed_cdi_Un: |
|
998 assumes cdi: "closed_cdi \<Omega> M" and empty: "{} \<in> M" |
|
999 and A: "A \<in> M" and B: "B \<in> M" |
|
1000 and disj: "A \<inter> B = {}" |
|
1001 shows "A \<union> B \<in> M" |
|
1002 proof - |
|
1003 have ra: "range (binaryset A B) \<subseteq> M" |
|
1004 by (simp add: range_binaryset_eq empty A B) |
|
1005 have di: "disjoint_family (binaryset A B)" using disj |
|
1006 by (simp add: disjoint_family_on_def binaryset_def Int_commute) |
|
1007 from closed_cdi_Disj [OF cdi ra di] |
|
1008 show ?thesis |
|
1009 by (simp add: UN_binaryset_eq) |
|
1010 qed |
|
1011 |
|
1012 lemma (in algebra) smallest_ccdi_sets_Un: |
|
1013 assumes A: "A \<in> smallest_ccdi_sets \<Omega> M" and B: "B \<in> smallest_ccdi_sets \<Omega> M" |
|
1014 and disj: "A \<inter> B = {}" |
|
1015 shows "A \<union> B \<in> smallest_ccdi_sets \<Omega> M" |
|
1016 proof - |
|
1017 have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets \<Omega> M)" |
|
1018 by (simp add: range_binaryset_eq A B smallest_ccdi_sets.Basic) |
|
1019 have di: "disjoint_family (binaryset A B)" using disj |
|
1020 by (simp add: disjoint_family_on_def binaryset_def Int_commute) |
|
1021 from Disj [OF ra di] |
|
1022 show ?thesis |
|
1023 by (simp add: UN_binaryset_eq) |
|
1024 qed |
|
1025 |
|
1026 lemma (in algebra) smallest_ccdi_sets_Int1: |
|
1027 assumes a: "a \<in> M" |
|
1028 shows "b \<in> smallest_ccdi_sets \<Omega> M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets \<Omega> M" |
|
1029 proof (induct rule: smallest_ccdi_sets.induct) |
|
1030 case (Basic x) |
|
1031 thus ?case |
|
1032 by (metis a Int smallest_ccdi_sets.Basic) |
|
1033 next |
|
1034 case (Compl x) |
|
1035 have "a \<inter> (\<Omega> - x) = \<Omega> - ((\<Omega> - a) \<union> (a \<inter> x))" |
|
1036 by blast |
|
1037 also have "... \<in> smallest_ccdi_sets \<Omega> M" |
|
1038 by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2 |
|
1039 Diff_disjoint Int_Diff Int_empty_right smallest_ccdi_sets_Un |
|
1040 smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl) |
|
1041 finally show ?case . |
|
1042 next |
|
1043 case (Inc A) |
|
1044 have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)" |
|
1045 by blast |
|
1046 have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets \<Omega> M)" using Inc |
|
1047 by blast |
|
1048 moreover have "(\<lambda>i. a \<inter> A i) 0 = {}" |
|
1049 by (simp add: Inc) |
|
1050 moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc |
|
1051 by blast |
|
1052 ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets \<Omega> M" |
|
1053 by (rule smallest_ccdi_sets.Inc) |
|
1054 show ?case |
|
1055 by (metis 1 2) |
|
1056 next |
|
1057 case (Disj A) |
|
1058 have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)" |
|
1059 by blast |
|
1060 have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets \<Omega> M)" using Disj |
|
1061 by blast |
|
1062 moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj |
|
1063 by (auto simp add: disjoint_family_on_def) |
|
1064 ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets \<Omega> M" |
|
1065 by (rule smallest_ccdi_sets.Disj) |
|
1066 show ?case |
|
1067 by (metis 1 2) |
|
1068 qed |
|
1069 |
|
1070 |
|
1071 lemma (in algebra) smallest_ccdi_sets_Int: |
|
1072 assumes b: "b \<in> smallest_ccdi_sets \<Omega> M" |
|
1073 shows "a \<in> smallest_ccdi_sets \<Omega> M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets \<Omega> M" |
|
1074 proof (induct rule: smallest_ccdi_sets.induct) |
|
1075 case (Basic x) |
|
1076 thus ?case |
|
1077 by (metis b smallest_ccdi_sets_Int1) |
|
1078 next |
|
1079 case (Compl x) |
|
1080 have "(\<Omega> - x) \<inter> b = \<Omega> - (x \<inter> b \<union> (\<Omega> - b))" |
|
1081 by blast |
|
1082 also have "... \<in> smallest_ccdi_sets \<Omega> M" |
|
1083 by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b |
|
1084 smallest_ccdi_sets.Compl smallest_ccdi_sets_Un) |
|
1085 finally show ?case . |
|
1086 next |
|
1087 case (Inc A) |
|
1088 have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b" |
|
1089 by blast |
|
1090 have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets \<Omega> M)" using Inc |
|
1091 by blast |
|
1092 moreover have "(\<lambda>i. A i \<inter> b) 0 = {}" |
|
1093 by (simp add: Inc) |
|
1094 moreover have "!!n. (\<lambda>i. A i \<inter> b) n \<subseteq> (\<lambda>i. A i \<inter> b) (Suc n)" using Inc |
|
1095 by blast |
|
1096 ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets \<Omega> M" |
|
1097 by (rule smallest_ccdi_sets.Inc) |
|
1098 show ?case |
|
1099 by (metis 1 2) |
|
1100 next |
|
1101 case (Disj A) |
|
1102 have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b" |
|
1103 by blast |
|
1104 have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets \<Omega> M)" using Disj |
|
1105 by blast |
|
1106 moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj |
|
1107 by (auto simp add: disjoint_family_on_def) |
|
1108 ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets \<Omega> M" |
|
1109 by (rule smallest_ccdi_sets.Disj) |
|
1110 show ?case |
|
1111 by (metis 1 2) |
|
1112 qed |
|
1113 |
|
1114 lemma (in algebra) sigma_property_disjoint_lemma: |
|
1115 assumes sbC: "M \<subseteq> C" |
|
1116 and ccdi: "closed_cdi \<Omega> C" |
|
1117 shows "sigma_sets \<Omega> M \<subseteq> C" |
|
1118 proof - |
|
1119 have "smallest_ccdi_sets \<Omega> M \<in> {B . M \<subseteq> B \<and> sigma_algebra \<Omega> B}" |
|
1120 apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int |
|
1121 smallest_ccdi_sets_Int) |
|
1122 apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets) |
|
1123 apply (blast intro: smallest_ccdi_sets.Disj) |
|
1124 done |
|
1125 hence "sigma_sets (\<Omega>) (M) \<subseteq> smallest_ccdi_sets \<Omega> M" |
|
1126 by clarsimp |
|
1127 (drule sigma_algebra.sigma_sets_subset [where a="M"], auto) |
|
1128 also have "... \<subseteq> C" |
|
1129 proof |
|
1130 fix x |
|
1131 assume x: "x \<in> smallest_ccdi_sets \<Omega> M" |
|
1132 thus "x \<in> C" |
|
1133 proof (induct rule: smallest_ccdi_sets.induct) |
|
1134 case (Basic x) |
|
1135 thus ?case |
|
1136 by (metis Basic subsetD sbC) |
|
1137 next |
|
1138 case (Compl x) |
|
1139 thus ?case |
|
1140 by (blast intro: closed_cdi_Compl [OF ccdi, simplified]) |
|
1141 next |
|
1142 case (Inc A) |
|
1143 thus ?case |
|
1144 by (auto intro: closed_cdi_Inc [OF ccdi, simplified]) |
|
1145 next |
|
1146 case (Disj A) |
|
1147 thus ?case |
|
1148 by (auto intro: closed_cdi_Disj [OF ccdi, simplified]) |
|
1149 qed |
|
1150 qed |
|
1151 finally show ?thesis . |
|
1152 qed |
|
1153 |
|
1154 lemma (in algebra) sigma_property_disjoint: |
|
1155 assumes sbC: "M \<subseteq> C" |
|
1156 and compl: "!!s. s \<in> C \<inter> sigma_sets (\<Omega>) (M) \<Longrightarrow> \<Omega> - s \<in> C" |
|
1157 and inc: "!!A. range A \<subseteq> C \<inter> sigma_sets (\<Omega>) (M) |
|
1158 \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) |
|
1159 \<Longrightarrow> (\<Union>i. A i) \<in> C" |
|
1160 and disj: "!!A. range A \<subseteq> C \<inter> sigma_sets (\<Omega>) (M) |
|
1161 \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C" |
|
1162 shows "sigma_sets (\<Omega>) (M) \<subseteq> C" |
|
1163 proof - |
|
1164 have "sigma_sets (\<Omega>) (M) \<subseteq> C \<inter> sigma_sets (\<Omega>) (M)" |
|
1165 proof (rule sigma_property_disjoint_lemma) |
|
1166 show "M \<subseteq> C \<inter> sigma_sets (\<Omega>) (M)" |
|
1167 by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic) |
|
1168 next |
|
1169 show "closed_cdi \<Omega> (C \<inter> sigma_sets (\<Omega>) (M))" |
|
1170 by (simp add: closed_cdi_def compl inc disj) |
|
1171 (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed |
|
1172 IntE sigma_sets.Compl range_subsetD sigma_sets.Union) |
|
1173 qed |
|
1174 thus ?thesis |
|
1175 by blast |
|
1176 qed |
|
1177 |
|
1178 subsubsection \<open>Dynkin systems\<close> |
|
1179 |
|
1180 locale dynkin_system = subset_class + |
|
1181 assumes space: "\<Omega> \<in> M" |
|
1182 and compl[intro!]: "\<And>A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M" |
|
1183 and UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> M |
|
1184 \<Longrightarrow> (\<Union>i::nat. A i) \<in> M" |
|
1185 |
|
1186 lemma (in dynkin_system) empty[intro, simp]: "{} \<in> M" |
|
1187 using space compl[of "\<Omega>"] by simp |
|
1188 |
|
1189 lemma (in dynkin_system) diff: |
|
1190 assumes sets: "D \<in> M" "E \<in> M" and "D \<subseteq> E" |
|
1191 shows "E - D \<in> M" |
|
1192 proof - |
|
1193 let ?f = "\<lambda>x. if x = 0 then D else if x = Suc 0 then \<Omega> - E else {}" |
|
1194 have "range ?f = {D, \<Omega> - E, {}}" |
|
1195 by (auto simp: image_iff) |
|
1196 moreover have "D \<union> (\<Omega> - E) = (\<Union>i. ?f i)" |
|
1197 by (auto simp: image_iff split: if_split_asm) |
|
1198 moreover |
|
1199 have "disjoint_family ?f" unfolding disjoint_family_on_def |
|
1200 using \<open>D \<in> M\<close>[THEN sets_into_space] \<open>D \<subseteq> E\<close> by auto |
|
1201 ultimately have "\<Omega> - (D \<union> (\<Omega> - E)) \<in> M" |
|
1202 using sets by auto |
|
1203 also have "\<Omega> - (D \<union> (\<Omega> - E)) = E - D" |
|
1204 using assms sets_into_space by auto |
|
1205 finally show ?thesis . |
|
1206 qed |
|
1207 |
|
1208 lemma dynkin_systemI: |
|
1209 assumes "\<And> A. A \<in> M \<Longrightarrow> A \<subseteq> \<Omega>" "\<Omega> \<in> M" |
|
1210 assumes "\<And> A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M" |
|
1211 assumes "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> M |
|
1212 \<Longrightarrow> (\<Union>i::nat. A i) \<in> M" |
|
1213 shows "dynkin_system \<Omega> M" |
|
1214 using assms by (auto simp: dynkin_system_def dynkin_system_axioms_def subset_class_def) |
|
1215 |
|
1216 lemma dynkin_systemI': |
|
1217 assumes 1: "\<And> A. A \<in> M \<Longrightarrow> A \<subseteq> \<Omega>" |
|
1218 assumes empty: "{} \<in> M" |
|
1219 assumes Diff: "\<And> A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M" |
|
1220 assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> M |
|
1221 \<Longrightarrow> (\<Union>i::nat. A i) \<in> M" |
|
1222 shows "dynkin_system \<Omega> M" |
|
1223 proof - |
|
1224 from Diff[OF empty] have "\<Omega> \<in> M" by auto |
|
1225 from 1 this Diff 2 show ?thesis |
|
1226 by (intro dynkin_systemI) auto |
|
1227 qed |
|
1228 |
|
1229 lemma dynkin_system_trivial: |
|
1230 shows "dynkin_system A (Pow A)" |
|
1231 by (rule dynkin_systemI) auto |
|
1232 |
|
1233 lemma sigma_algebra_imp_dynkin_system: |
|
1234 assumes "sigma_algebra \<Omega> M" shows "dynkin_system \<Omega> M" |
|
1235 proof - |
|
1236 interpret sigma_algebra \<Omega> M by fact |
|
1237 show ?thesis using sets_into_space by (fastforce intro!: dynkin_systemI) |
|
1238 qed |
|
1239 |
|
1240 subsubsection "Intersection sets systems" |
|
1241 |
|
1242 definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" |
|
1243 |
|
1244 lemma (in algebra) Int_stable: "Int_stable M" |
|
1245 unfolding Int_stable_def by auto |
|
1246 |
|
1247 lemma Int_stableI: |
|
1248 "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A) \<Longrightarrow> Int_stable A" |
|
1249 unfolding Int_stable_def by auto |
|
1250 |
|
1251 lemma Int_stableD: |
|
1252 "Int_stable M \<Longrightarrow> a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M" |
|
1253 unfolding Int_stable_def by auto |
|
1254 |
|
1255 lemma (in dynkin_system) sigma_algebra_eq_Int_stable: |
|
1256 "sigma_algebra \<Omega> M \<longleftrightarrow> Int_stable M" |
|
1257 proof |
|
1258 assume "sigma_algebra \<Omega> M" then show "Int_stable M" |
|
1259 unfolding sigma_algebra_def using algebra.Int_stable by auto |
|
1260 next |
|
1261 assume "Int_stable M" |
|
1262 show "sigma_algebra \<Omega> M" |
|
1263 unfolding sigma_algebra_disjoint_iff algebra_iff_Un |
|
1264 proof (intro conjI ballI allI impI) |
|
1265 show "M \<subseteq> Pow (\<Omega>)" using sets_into_space by auto |
|
1266 next |
|
1267 fix A B assume "A \<in> M" "B \<in> M" |
|
1268 then have "A \<union> B = \<Omega> - ((\<Omega> - A) \<inter> (\<Omega> - B))" |
|
1269 "\<Omega> - A \<in> M" "\<Omega> - B \<in> M" |
|
1270 using sets_into_space by auto |
|
1271 then show "A \<union> B \<in> M" |
|
1272 using \<open>Int_stable M\<close> unfolding Int_stable_def by auto |
|
1273 qed auto |
|
1274 qed |
|
1275 |
|
1276 subsubsection "Smallest Dynkin systems" |
|
1277 |
|
1278 definition dynkin where |
|
1279 "dynkin \<Omega> M = (\<Inter>{D. dynkin_system \<Omega> D \<and> M \<subseteq> D})" |
|
1280 |
|
1281 lemma dynkin_system_dynkin: |
|
1282 assumes "M \<subseteq> Pow (\<Omega>)" |
|
1283 shows "dynkin_system \<Omega> (dynkin \<Omega> M)" |
|
1284 proof (rule dynkin_systemI) |
|
1285 fix A assume "A \<in> dynkin \<Omega> M" |
|
1286 moreover |
|
1287 { fix D assume "A \<in> D" and d: "dynkin_system \<Omega> D" |
|
1288 then have "A \<subseteq> \<Omega>" by (auto simp: dynkin_system_def subset_class_def) } |
|
1289 moreover have "{D. dynkin_system \<Omega> D \<and> M \<subseteq> D} \<noteq> {}" |
|
1290 using assms dynkin_system_trivial by fastforce |
|
1291 ultimately show "A \<subseteq> \<Omega>" |
|
1292 unfolding dynkin_def using assms |
|
1293 by auto |
|
1294 next |
|
1295 show "\<Omega> \<in> dynkin \<Omega> M" |
|
1296 unfolding dynkin_def using dynkin_system.space by fastforce |
|
1297 next |
|
1298 fix A assume "A \<in> dynkin \<Omega> M" |
|
1299 then show "\<Omega> - A \<in> dynkin \<Omega> M" |
|
1300 unfolding dynkin_def using dynkin_system.compl by force |
|
1301 next |
|
1302 fix A :: "nat \<Rightarrow> 'a set" |
|
1303 assume A: "disjoint_family A" "range A \<subseteq> dynkin \<Omega> M" |
|
1304 show "(\<Union>i. A i) \<in> dynkin \<Omega> M" unfolding dynkin_def |
|
1305 proof (simp, safe) |
|
1306 fix D assume "dynkin_system \<Omega> D" "M \<subseteq> D" |
|
1307 with A have "(\<Union>i. A i) \<in> D" |
|
1308 by (intro dynkin_system.UN) (auto simp: dynkin_def) |
|
1309 then show "(\<Union>i. A i) \<in> D" by auto |
|
1310 qed |
|
1311 qed |
|
1312 |
|
1313 lemma dynkin_Basic[intro]: "A \<in> M \<Longrightarrow> A \<in> dynkin \<Omega> M" |
|
1314 unfolding dynkin_def by auto |
|
1315 |
|
1316 lemma (in dynkin_system) restricted_dynkin_system: |
|
1317 assumes "D \<in> M" |
|
1318 shows "dynkin_system \<Omega> {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> D \<in> M}" |
|
1319 proof (rule dynkin_systemI, simp_all) |
|
1320 have "\<Omega> \<inter> D = D" |
|
1321 using \<open>D \<in> M\<close> sets_into_space by auto |
|
1322 then show "\<Omega> \<inter> D \<in> M" |
|
1323 using \<open>D \<in> M\<close> by auto |
|
1324 next |
|
1325 fix A assume "A \<subseteq> \<Omega> \<and> A \<inter> D \<in> M" |
|
1326 moreover have "(\<Omega> - A) \<inter> D = (\<Omega> - (A \<inter> D)) - (\<Omega> - D)" |
|
1327 by auto |
|
1328 ultimately show "\<Omega> - A \<subseteq> \<Omega> \<and> (\<Omega> - A) \<inter> D \<in> M" |
|
1329 using \<open>D \<in> M\<close> by (auto intro: diff) |
|
1330 next |
|
1331 fix A :: "nat \<Rightarrow> 'a set" |
|
1332 assume "disjoint_family A" "range A \<subseteq> {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> D \<in> M}" |
|
1333 then have "\<And>i. A i \<subseteq> \<Omega>" "disjoint_family (\<lambda>i. A i \<inter> D)" |
|
1334 "range (\<lambda>i. A i \<inter> D) \<subseteq> M" "(\<Union>x. A x) \<inter> D = (\<Union>x. A x \<inter> D)" |
|
1335 by ((fastforce simp: disjoint_family_on_def)+) |
|
1336 then show "(\<Union>x. A x) \<subseteq> \<Omega> \<and> (\<Union>x. A x) \<inter> D \<in> M" |
|
1337 by (auto simp del: UN_simps) |
|
1338 qed |
|
1339 |
|
1340 lemma (in dynkin_system) dynkin_subset: |
|
1341 assumes "N \<subseteq> M" |
|
1342 shows "dynkin \<Omega> N \<subseteq> M" |
|
1343 proof - |
|
1344 have "dynkin_system \<Omega> M" .. |
|
1345 then have "dynkin_system \<Omega> M" |
|
1346 using assms unfolding dynkin_system_def dynkin_system_axioms_def subset_class_def by simp |
|
1347 with \<open>N \<subseteq> M\<close> show ?thesis by (auto simp add: dynkin_def) |
|
1348 qed |
|
1349 |
|
1350 lemma sigma_eq_dynkin: |
|
1351 assumes sets: "M \<subseteq> Pow \<Omega>" |
|
1352 assumes "Int_stable M" |
|
1353 shows "sigma_sets \<Omega> M = dynkin \<Omega> M" |
|
1354 proof - |
|
1355 have "dynkin \<Omega> M \<subseteq> sigma_sets (\<Omega>) (M)" |
|
1356 using sigma_algebra_imp_dynkin_system |
|
1357 unfolding dynkin_def sigma_sets_least_sigma_algebra[OF sets] by auto |
|
1358 moreover |
|
1359 interpret dynkin_system \<Omega> "dynkin \<Omega> M" |
|
1360 using dynkin_system_dynkin[OF sets] . |
|
1361 have "sigma_algebra \<Omega> (dynkin \<Omega> M)" |
|
1362 unfolding sigma_algebra_eq_Int_stable Int_stable_def |
|
1363 proof (intro ballI) |
|
1364 fix A B assume "A \<in> dynkin \<Omega> M" "B \<in> dynkin \<Omega> M" |
|
1365 let ?D = "\<lambda>E. {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> E \<in> dynkin \<Omega> M}" |
|
1366 have "M \<subseteq> ?D B" |
|
1367 proof |
|
1368 fix E assume "E \<in> M" |
|
1369 then have "M \<subseteq> ?D E" "E \<in> dynkin \<Omega> M" |
|
1370 using sets_into_space \<open>Int_stable M\<close> by (auto simp: Int_stable_def) |
|
1371 then have "dynkin \<Omega> M \<subseteq> ?D E" |
|
1372 using restricted_dynkin_system \<open>E \<in> dynkin \<Omega> M\<close> |
|
1373 by (intro dynkin_system.dynkin_subset) simp_all |
|
1374 then have "B \<in> ?D E" |
|
1375 using \<open>B \<in> dynkin \<Omega> M\<close> by auto |
|
1376 then have "E \<inter> B \<in> dynkin \<Omega> M" |
|
1377 by (subst Int_commute) simp |
|
1378 then show "E \<in> ?D B" |
|
1379 using sets \<open>E \<in> M\<close> by auto |
|
1380 qed |
|
1381 then have "dynkin \<Omega> M \<subseteq> ?D B" |
|
1382 using restricted_dynkin_system \<open>B \<in> dynkin \<Omega> M\<close> |
|
1383 by (intro dynkin_system.dynkin_subset) simp_all |
|
1384 then show "A \<inter> B \<in> dynkin \<Omega> M" |
|
1385 using \<open>A \<in> dynkin \<Omega> M\<close> sets_into_space by auto |
|
1386 qed |
|
1387 from sigma_algebra.sigma_sets_subset[OF this, of "M"] |
|
1388 have "sigma_sets (\<Omega>) (M) \<subseteq> dynkin \<Omega> M" by auto |
|
1389 ultimately have "sigma_sets (\<Omega>) (M) = dynkin \<Omega> M" by auto |
|
1390 then show ?thesis |
|
1391 by (auto simp: dynkin_def) |
|
1392 qed |
|
1393 |
|
1394 lemma (in dynkin_system) dynkin_idem: |
|
1395 "dynkin \<Omega> M = M" |
|
1396 proof - |
|
1397 have "dynkin \<Omega> M = M" |
|
1398 proof |
|
1399 show "M \<subseteq> dynkin \<Omega> M" |
|
1400 using dynkin_Basic by auto |
|
1401 show "dynkin \<Omega> M \<subseteq> M" |
|
1402 by (intro dynkin_subset) auto |
|
1403 qed |
|
1404 then show ?thesis |
|
1405 by (auto simp: dynkin_def) |
|
1406 qed |
|
1407 |
|
1408 lemma (in dynkin_system) dynkin_lemma: |
|
1409 assumes "Int_stable E" |
|
1410 and E: "E \<subseteq> M" "M \<subseteq> sigma_sets \<Omega> E" |
|
1411 shows "sigma_sets \<Omega> E = M" |
|
1412 proof - |
|
1413 have "E \<subseteq> Pow \<Omega>" |
|
1414 using E sets_into_space by force |
|
1415 then have *: "sigma_sets \<Omega> E = dynkin \<Omega> E" |
|
1416 using \<open>Int_stable E\<close> by (rule sigma_eq_dynkin) |
|
1417 then have "dynkin \<Omega> E = M" |
|
1418 using assms dynkin_subset[OF E(1)] by simp |
|
1419 with * show ?thesis |
|
1420 using assms by (auto simp: dynkin_def) |
|
1421 qed |
|
1422 |
|
1423 subsubsection \<open>Induction rule for intersection-stable generators\<close> |
|
1424 |
|
1425 text \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras |
|
1426 generated by a generator closed under intersection.\<close> |
|
1427 |
|
1428 lemma sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]: |
|
1429 assumes "Int_stable G" |
|
1430 and closed: "G \<subseteq> Pow \<Omega>" |
|
1431 and A: "A \<in> sigma_sets \<Omega> G" |
|
1432 assumes basic: "\<And>A. A \<in> G \<Longrightarrow> P A" |
|
1433 and empty: "P {}" |
|
1434 and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)" |
|
1435 and union: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sigma_sets \<Omega> G \<Longrightarrow> (\<And>i. P (A i)) \<Longrightarrow> P (\<Union>i::nat. A i)" |
|
1436 shows "P A" |
|
1437 proof - |
|
1438 let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }" |
|
1439 interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G" |
|
1440 using closed by (rule sigma_algebra_sigma_sets) |
|
1441 from compl[OF _ empty] closed have space: "P \<Omega>" by simp |
|
1442 interpret dynkin_system \<Omega> ?D |
|
1443 by standard (auto dest: sets_into_space intro!: space compl union) |
|
1444 have "sigma_sets \<Omega> G = ?D" |
|
1445 by (rule dynkin_lemma) (auto simp: basic \<open>Int_stable G\<close>) |
|
1446 with A show ?thesis by auto |
|
1447 qed |
|
1448 |
|
1449 subsection \<open>Measure type\<close> |
|
1450 |
|
1451 definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where |
|
1452 "positive M \<mu> \<longleftrightarrow> \<mu> {} = 0" |
|
1453 |
|
1454 definition countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where |
|
1455 "countably_additive M f \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> |
|
1456 (\<Sum>i. f (A i)) = f (\<Union>i. A i))" |
|
1457 |
|
1458 definition measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where |
|
1459 "measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>" |
|
1460 |
|
1461 typedef 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }" |
|
1462 proof |
|
1463 have "sigma_algebra UNIV {{}, UNIV}" |
|
1464 by (auto simp: sigma_algebra_iff2) |
|
1465 then show "(UNIV, {{}, UNIV}, \<lambda>A. 0) \<in> {(\<Omega>, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu>} " |
|
1466 by (auto simp: measure_space_def positive_def countably_additive_def) |
|
1467 qed |
|
1468 |
|
1469 definition space :: "'a measure \<Rightarrow> 'a set" where |
|
1470 "space M = fst (Rep_measure M)" |
|
1471 |
|
1472 definition sets :: "'a measure \<Rightarrow> 'a set set" where |
|
1473 "sets M = fst (snd (Rep_measure M))" |
|
1474 |
|
1475 definition emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where |
|
1476 "emeasure M = snd (snd (Rep_measure M))" |
|
1477 |
|
1478 definition measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where |
|
1479 "measure M A = enn2real (emeasure M A)" |
|
1480 |
|
1481 declare [[coercion sets]] |
|
1482 |
|
1483 declare [[coercion measure]] |
|
1484 |
|
1485 declare [[coercion emeasure]] |
|
1486 |
|
1487 lemma measure_space: "measure_space (space M) (sets M) (emeasure M)" |
|
1488 by (cases M) (auto simp: space_def sets_def emeasure_def Abs_measure_inverse) |
|
1489 |
|
1490 interpretation sets: sigma_algebra "space M" "sets M" for M :: "'a measure" |
|
1491 using measure_space[of M] by (auto simp: measure_space_def) |
|
1492 |
|
1493 definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where |
|
1494 "measure_of \<Omega> A \<mu> = Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>}, |
|
1495 \<lambda>a. if a \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> a else 0)" |
|
1496 |
|
1497 abbreviation "sigma \<Omega> A \<equiv> measure_of \<Omega> A (\<lambda>x. 0)" |
|
1498 |
|
1499 lemma measure_space_0: "A \<subseteq> Pow \<Omega> \<Longrightarrow> measure_space \<Omega> (sigma_sets \<Omega> A) (\<lambda>x. 0)" |
|
1500 unfolding measure_space_def |
|
1501 by (auto intro!: sigma_algebra_sigma_sets simp: positive_def countably_additive_def) |
|
1502 |
|
1503 lemma sigma_algebra_trivial: "sigma_algebra \<Omega> {{}, \<Omega>}" |
|
1504 by unfold_locales(fastforce intro: exI[where x="{{}}"] exI[where x="{\<Omega>}"])+ |
|
1505 |
|
1506 lemma measure_space_0': "measure_space \<Omega> {{}, \<Omega>} (\<lambda>x. 0)" |
|
1507 by(simp add: measure_space_def positive_def countably_additive_def sigma_algebra_trivial) |
|
1508 |
|
1509 lemma measure_space_closed: |
|
1510 assumes "measure_space \<Omega> M \<mu>" |
|
1511 shows "M \<subseteq> Pow \<Omega>" |
|
1512 proof - |
|
1513 interpret sigma_algebra \<Omega> M using assms by(simp add: measure_space_def) |
|
1514 show ?thesis by(rule space_closed) |
|
1515 qed |
|
1516 |
|
1517 lemma (in ring_of_sets) positive_cong_eq: |
|
1518 "(\<And>a. a \<in> M \<Longrightarrow> \<mu>' a = \<mu> a) \<Longrightarrow> positive M \<mu>' = positive M \<mu>" |
|
1519 by (auto simp add: positive_def) |
|
1520 |
|
1521 lemma (in sigma_algebra) countably_additive_eq: |
|
1522 "(\<And>a. a \<in> M \<Longrightarrow> \<mu>' a = \<mu> a) \<Longrightarrow> countably_additive M \<mu>' = countably_additive M \<mu>" |
|
1523 unfolding countably_additive_def |
|
1524 by (intro arg_cong[where f=All] ext) (auto simp add: countably_additive_def subset_eq) |
|
1525 |
|
1526 lemma measure_space_eq: |
|
1527 assumes closed: "A \<subseteq> Pow \<Omega>" and eq: "\<And>a. a \<in> sigma_sets \<Omega> A \<Longrightarrow> \<mu> a = \<mu>' a" |
|
1528 shows "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>'" |
|
1529 proof - |
|
1530 interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" using closed by (rule sigma_algebra_sigma_sets) |
|
1531 from positive_cong_eq[OF eq, of "\<lambda>i. i"] countably_additive_eq[OF eq, of "\<lambda>i. i"] show ?thesis |
|
1532 by (auto simp: measure_space_def) |
|
1533 qed |
|
1534 |
|
1535 lemma measure_of_eq: |
|
1536 assumes closed: "A \<subseteq> Pow \<Omega>" and eq: "(\<And>a. a \<in> sigma_sets \<Omega> A \<Longrightarrow> \<mu> a = \<mu>' a)" |
|
1537 shows "measure_of \<Omega> A \<mu> = measure_of \<Omega> A \<mu>'" |
|
1538 proof - |
|
1539 have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>'" |
|
1540 using assms by (rule measure_space_eq) |
|
1541 with eq show ?thesis |
|
1542 by (auto simp add: measure_of_def intro!: arg_cong[where f=Abs_measure]) |
|
1543 qed |
|
1544 |
|
1545 lemma |
|
1546 shows space_measure_of_conv: "space (measure_of \<Omega> A \<mu>) = \<Omega>" (is ?space) |
|
1547 and sets_measure_of_conv: |
|
1548 "sets (measure_of \<Omega> A \<mu>) = (if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>})" (is ?sets) |
|
1549 and emeasure_measure_of_conv: |
|
1550 "emeasure (measure_of \<Omega> A \<mu>) = |
|
1551 (\<lambda>B. if B \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> B else 0)" (is ?emeasure) |
|
1552 proof - |
|
1553 have "?space \<and> ?sets \<and> ?emeasure" |
|
1554 proof(cases "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>") |
|
1555 case True |
|
1556 from measure_space_closed[OF this] sigma_sets_superset_generator[of A \<Omega>] |
|
1557 have "A \<subseteq> Pow \<Omega>" by simp |
|
1558 hence "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A) |
|
1559 (\<lambda>a. if a \<in> sigma_sets \<Omega> A then \<mu> a else 0)" |
|
1560 by(rule measure_space_eq) auto |
|
1561 with True \<open>A \<subseteq> Pow \<Omega>\<close> show ?thesis |
|
1562 by(simp add: measure_of_def space_def sets_def emeasure_def Abs_measure_inverse) |
|
1563 next |
|
1564 case False thus ?thesis |
|
1565 by(cases "A \<subseteq> Pow \<Omega>")(simp_all add: Abs_measure_inverse measure_of_def sets_def space_def emeasure_def measure_space_0 measure_space_0') |
|
1566 qed |
|
1567 thus ?space ?sets ?emeasure by simp_all |
|
1568 qed |
|
1569 |
|
1570 lemma [simp]: |
|
1571 assumes A: "A \<subseteq> Pow \<Omega>" |
|
1572 shows sets_measure_of: "sets (measure_of \<Omega> A \<mu>) = sigma_sets \<Omega> A" |
|
1573 and space_measure_of: "space (measure_of \<Omega> A \<mu>) = \<Omega>" |
|
1574 using assms |
|
1575 by(simp_all add: sets_measure_of_conv space_measure_of_conv) |
|
1576 |
|
1577 lemma (in sigma_algebra) sets_measure_of_eq[simp]: "sets (measure_of \<Omega> M \<mu>) = M" |
|
1578 using space_closed by (auto intro!: sigma_sets_eq) |
|
1579 |
|
1580 lemma (in sigma_algebra) space_measure_of_eq[simp]: "space (measure_of \<Omega> M \<mu>) = \<Omega>" |
|
1581 by (rule space_measure_of_conv) |
|
1582 |
|
1583 lemma measure_of_subset: "M \<subseteq> Pow \<Omega> \<Longrightarrow> M' \<subseteq> M \<Longrightarrow> sets (measure_of \<Omega> M' \<mu>) \<subseteq> sets (measure_of \<Omega> M \<mu>')" |
|
1584 by (auto intro!: sigma_sets_subseteq) |
|
1585 |
|
1586 lemma emeasure_sigma: "emeasure (sigma \<Omega> A) = (\<lambda>x. 0)" |
|
1587 unfolding measure_of_def emeasure_def |
|
1588 by (subst Abs_measure_inverse) |
|
1589 (auto simp: measure_space_def positive_def countably_additive_def |
|
1590 intro!: sigma_algebra_sigma_sets sigma_algebra_trivial) |
|
1591 |
|
1592 lemma sigma_sets_mono'': |
|
1593 assumes "A \<in> sigma_sets C D" |
|
1594 assumes "B \<subseteq> D" |
|
1595 assumes "D \<subseteq> Pow C" |
|
1596 shows "sigma_sets A B \<subseteq> sigma_sets C D" |
|
1597 proof |
|
1598 fix x assume "x \<in> sigma_sets A B" |
|
1599 thus "x \<in> sigma_sets C D" |
|
1600 proof induct |
|
1601 case (Basic a) with assms have "a \<in> D" by auto |
|
1602 thus ?case .. |
|
1603 next |
|
1604 case Empty show ?case by (rule sigma_sets.Empty) |
|
1605 next |
|
1606 from assms have "A \<in> sets (sigma C D)" by (subst sets_measure_of[OF \<open>D \<subseteq> Pow C\<close>]) |
|
1607 moreover case (Compl a) hence "a \<in> sets (sigma C D)" by (subst sets_measure_of[OF \<open>D \<subseteq> Pow C\<close>]) |
|
1608 ultimately have "A - a \<in> sets (sigma C D)" .. |
|
1609 thus ?case by (subst (asm) sets_measure_of[OF \<open>D \<subseteq> Pow C\<close>]) |
|
1610 next |
|
1611 case (Union a) |
|
1612 thus ?case by (intro sigma_sets.Union) |
|
1613 qed |
|
1614 qed |
|
1615 |
|
1616 lemma in_measure_of[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)" |
|
1617 by auto |
|
1618 |
|
1619 lemma space_empty_iff: "space N = {} \<longleftrightarrow> sets N = {{}}" |
|
1620 by (metis Pow_empty Sup_bot_conv(1) cSup_singleton empty_iff |
|
1621 sets.sigma_sets_eq sets.space_closed sigma_sets_top subset_singletonD) |
|
1622 |
|
1623 subsubsection \<open>Constructing simple @{typ "'a measure"}\<close> |
|
1624 |
|
1625 lemma emeasure_measure_of: |
|
1626 assumes M: "M = measure_of \<Omega> A \<mu>" |
|
1627 assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>" |
|
1628 assumes X: "X \<in> sets M" |
|
1629 shows "emeasure M X = \<mu> X" |
|
1630 proof - |
|
1631 interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact |
|
1632 have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>" |
|
1633 using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets) |
|
1634 thus ?thesis using X ms |
|
1635 by(simp add: M emeasure_measure_of_conv sets_measure_of_conv) |
|
1636 qed |
|
1637 |
|
1638 lemma emeasure_measure_of_sigma: |
|
1639 assumes ms: "sigma_algebra \<Omega> M" "positive M \<mu>" "countably_additive M \<mu>" |
|
1640 assumes A: "A \<in> M" |
|
1641 shows "emeasure (measure_of \<Omega> M \<mu>) A = \<mu> A" |
|
1642 proof - |
|
1643 interpret sigma_algebra \<Omega> M by fact |
|
1644 have "measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>" |
|
1645 using ms sigma_sets_eq by (simp add: measure_space_def) |
|
1646 thus ?thesis by(simp add: emeasure_measure_of_conv A) |
|
1647 qed |
|
1648 |
|
1649 lemma measure_cases[cases type: measure]: |
|
1650 obtains (measure) \<Omega> A \<mu> where "x = Abs_measure (\<Omega>, A, \<mu>)" "\<forall>a\<in>-A. \<mu> a = 0" "measure_space \<Omega> A \<mu>" |
|
1651 by atomize_elim (cases x, auto) |
|
1652 |
|
1653 lemma sets_le_imp_space_le: "sets A \<subseteq> sets B \<Longrightarrow> space A \<subseteq> space B" |
|
1654 by (auto dest: sets.sets_into_space) |
|
1655 |
|
1656 lemma sets_eq_imp_space_eq: "sets M = sets M' \<Longrightarrow> space M = space M'" |
|
1657 by (auto intro!: antisym sets_le_imp_space_le) |
|
1658 |
|
1659 lemma emeasure_notin_sets: "A \<notin> sets M \<Longrightarrow> emeasure M A = 0" |
|
1660 by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def) |
|
1661 |
|
1662 lemma emeasure_neq_0_sets: "emeasure M A \<noteq> 0 \<Longrightarrow> A \<in> sets M" |
|
1663 using emeasure_notin_sets[of A M] by blast |
|
1664 |
|
1665 lemma measure_notin_sets: "A \<notin> sets M \<Longrightarrow> measure M A = 0" |
|
1666 by (simp add: measure_def emeasure_notin_sets zero_ennreal.rep_eq) |
|
1667 |
|
1668 lemma measure_eqI: |
|
1669 fixes M N :: "'a measure" |
|
1670 assumes "sets M = sets N" and eq: "\<And>A. A \<in> sets M \<Longrightarrow> emeasure M A = emeasure N A" |
|
1671 shows "M = N" |
|
1672 proof (cases M N rule: measure_cases[case_product measure_cases]) |
|
1673 case (measure_measure \<Omega> A \<mu> \<Omega>' A' \<mu>') |
|
1674 interpret M: sigma_algebra \<Omega> A using measure_measure by (auto simp: measure_space_def) |
|
1675 interpret N: sigma_algebra \<Omega>' A' using measure_measure by (auto simp: measure_space_def) |
|
1676 have "A = sets M" "A' = sets N" |
|
1677 using measure_measure by (simp_all add: sets_def Abs_measure_inverse) |
|
1678 with \<open>sets M = sets N\<close> have AA': "A = A'" by simp |
|
1679 moreover from M.top N.top M.space_closed N.space_closed AA' have "\<Omega> = \<Omega>'" by auto |
|
1680 moreover { fix B have "\<mu> B = \<mu>' B" |
|
1681 proof cases |
|
1682 assume "B \<in> A" |
|
1683 with eq \<open>A = sets M\<close> have "emeasure M B = emeasure N B" by simp |
|
1684 with measure_measure show "\<mu> B = \<mu>' B" |
|
1685 by (simp add: emeasure_def Abs_measure_inverse) |
|
1686 next |
|
1687 assume "B \<notin> A" |
|
1688 with \<open>A = sets M\<close> \<open>A' = sets N\<close> \<open>A = A'\<close> have "B \<notin> sets M" "B \<notin> sets N" |
|
1689 by auto |
|
1690 then have "emeasure M B = 0" "emeasure N B = 0" |
|
1691 by (simp_all add: emeasure_notin_sets) |
|
1692 with measure_measure show "\<mu> B = \<mu>' B" |
|
1693 by (simp add: emeasure_def Abs_measure_inverse) |
|
1694 qed } |
|
1695 then have "\<mu> = \<mu>'" by auto |
|
1696 ultimately show "M = N" |
|
1697 by (simp add: measure_measure) |
|
1698 qed |
|
1699 |
|
1700 lemma sigma_eqI: |
|
1701 assumes [simp]: "M \<subseteq> Pow \<Omega>" "N \<subseteq> Pow \<Omega>" "sigma_sets \<Omega> M = sigma_sets \<Omega> N" |
|
1702 shows "sigma \<Omega> M = sigma \<Omega> N" |
|
1703 by (rule measure_eqI) (simp_all add: emeasure_sigma) |
|
1704 |
|
1705 subsubsection \<open>Measurable functions\<close> |
|
1706 |
|
1707 definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>M" 60) where |
|
1708 "measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}" |
|
1709 |
|
1710 lemma measurableI: |
|
1711 "(\<And>x. x \<in> space M \<Longrightarrow> f x \<in> space N) \<Longrightarrow> (\<And>A. A \<in> sets N \<Longrightarrow> f -` A \<inter> space M \<in> sets M) \<Longrightarrow> |
|
1712 f \<in> measurable M N" |
|
1713 by (auto simp: measurable_def) |
|
1714 |
|
1715 lemma measurable_space: |
|
1716 "f \<in> measurable M A \<Longrightarrow> x \<in> space M \<Longrightarrow> f x \<in> space A" |
|
1717 unfolding measurable_def by auto |
|
1718 |
|
1719 lemma measurable_sets: |
|
1720 "f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f -` S \<inter> space M \<in> sets M" |
|
1721 unfolding measurable_def by auto |
|
1722 |
|
1723 lemma measurable_sets_Collect: |
|
1724 assumes f: "f \<in> measurable M N" and P: "{x\<in>space N. P x} \<in> sets N" shows "{x\<in>space M. P (f x)} \<in> sets M" |
|
1725 proof - |
|
1726 have "f -` {x \<in> space N. P x} \<inter> space M = {x\<in>space M. P (f x)}" |
|
1727 using measurable_space[OF f] by auto |
|
1728 with measurable_sets[OF f P] show ?thesis |
|
1729 by simp |
|
1730 qed |
|
1731 |
|
1732 lemma measurable_sigma_sets: |
|
1733 assumes B: "sets N = sigma_sets \<Omega> A" "A \<subseteq> Pow \<Omega>" |
|
1734 and f: "f \<in> space M \<rightarrow> \<Omega>" |
|
1735 and ba: "\<And>y. y \<in> A \<Longrightarrow> (f -` y) \<inter> space M \<in> sets M" |
|
1736 shows "f \<in> measurable M N" |
|
1737 proof - |
|
1738 interpret A: sigma_algebra \<Omega> "sigma_sets \<Omega> A" using B(2) by (rule sigma_algebra_sigma_sets) |
|
1739 from B sets.top[of N] A.top sets.space_closed[of N] A.space_closed have \<Omega>: "\<Omega> = space N" by force |
|
1740 |
|
1741 { fix X assume "X \<in> sigma_sets \<Omega> A" |
|
1742 then have "f -` X \<inter> space M \<in> sets M \<and> X \<subseteq> \<Omega>" |
|
1743 proof induct |
|
1744 case (Basic a) then show ?case |
|
1745 by (auto simp add: ba) (metis B(2) subsetD PowD) |
|
1746 next |
|
1747 case (Compl a) |
|
1748 have [simp]: "f -` \<Omega> \<inter> space M = space M" |
|
1749 by (auto simp add: funcset_mem [OF f]) |
|
1750 then show ?case |
|
1751 by (auto simp add: vimage_Diff Diff_Int_distrib2 sets.compl_sets Compl) |
|
1752 next |
|
1753 case (Union a) |
|
1754 then show ?case |
|
1755 by (simp add: vimage_UN, simp only: UN_extend_simps(4)) blast |
|
1756 qed auto } |
|
1757 with f show ?thesis |
|
1758 by (auto simp add: measurable_def B \<Omega>) |
|
1759 qed |
|
1760 |
|
1761 lemma measurable_measure_of: |
|
1762 assumes B: "N \<subseteq> Pow \<Omega>" |
|
1763 and f: "f \<in> space M \<rightarrow> \<Omega>" |
|
1764 and ba: "\<And>y. y \<in> N \<Longrightarrow> (f -` y) \<inter> space M \<in> sets M" |
|
1765 shows "f \<in> measurable M (measure_of \<Omega> N \<mu>)" |
|
1766 proof - |
|
1767 have "sets (measure_of \<Omega> N \<mu>) = sigma_sets \<Omega> N" |
|
1768 using B by (rule sets_measure_of) |
|
1769 from this assms show ?thesis by (rule measurable_sigma_sets) |
|
1770 qed |
|
1771 |
|
1772 lemma measurable_iff_measure_of: |
|
1773 assumes "N \<subseteq> Pow \<Omega>" "f \<in> space M \<rightarrow> \<Omega>" |
|
1774 shows "f \<in> measurable M (measure_of \<Omega> N \<mu>) \<longleftrightarrow> (\<forall>A\<in>N. f -` A \<inter> space M \<in> sets M)" |
|
1775 by (metis assms in_measure_of measurable_measure_of assms measurable_sets) |
|
1776 |
|
1777 lemma measurable_cong_sets: |
|
1778 assumes sets: "sets M = sets M'" "sets N = sets N'" |
|
1779 shows "measurable M N = measurable M' N'" |
|
1780 using sets[THEN sets_eq_imp_space_eq] sets by (simp add: measurable_def) |
|
1781 |
|
1782 lemma measurable_cong: |
|
1783 assumes "\<And>w. w \<in> space M \<Longrightarrow> f w = g w" |
|
1784 shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'" |
|
1785 unfolding measurable_def using assms |
|
1786 by (simp cong: vimage_inter_cong Pi_cong) |
|
1787 |
|
1788 lemma measurable_cong': |
|
1789 assumes "\<And>w. w \<in> space M =simp=> f w = g w" |
|
1790 shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'" |
|
1791 unfolding measurable_def using assms |
|
1792 by (simp cong: vimage_inter_cong Pi_cong add: simp_implies_def) |
|
1793 |
|
1794 lemma measurable_cong_strong: |
|
1795 "M = N \<Longrightarrow> M' = N' \<Longrightarrow> (\<And>w. w \<in> space M \<Longrightarrow> f w = g w) \<Longrightarrow> |
|
1796 f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable N N'" |
|
1797 by (metis measurable_cong) |
|
1798 |
|
1799 lemma measurable_compose: |
|
1800 assumes f: "f \<in> measurable M N" and g: "g \<in> measurable N L" |
|
1801 shows "(\<lambda>x. g (f x)) \<in> measurable M L" |
|
1802 proof - |
|
1803 have "\<And>A. (\<lambda>x. g (f x)) -` A \<inter> space M = f -` (g -` A \<inter> space N) \<inter> space M" |
|
1804 using measurable_space[OF f] by auto |
|
1805 with measurable_space[OF f] measurable_space[OF g] show ?thesis |
|
1806 by (auto intro: measurable_sets[OF f] measurable_sets[OF g] |
|
1807 simp del: vimage_Int simp add: measurable_def) |
|
1808 qed |
|
1809 |
|
1810 lemma measurable_comp: |
|
1811 "f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> g \<circ> f \<in> measurable M L" |
|
1812 using measurable_compose[of f M N g L] by (simp add: comp_def) |
|
1813 |
|
1814 lemma measurable_const: |
|
1815 "c \<in> space M' \<Longrightarrow> (\<lambda>x. c) \<in> measurable M M'" |
|
1816 by (auto simp add: measurable_def) |
|
1817 |
|
1818 lemma measurable_ident: "id \<in> measurable M M" |
|
1819 by (auto simp add: measurable_def) |
|
1820 |
|
1821 lemma measurable_id: "(\<lambda>x. x) \<in> measurable M M" |
|
1822 by (simp add: measurable_def) |
|
1823 |
|
1824 lemma measurable_ident_sets: |
|
1825 assumes eq: "sets M = sets M'" shows "(\<lambda>x. x) \<in> measurable M M'" |
|
1826 using measurable_ident[of M] |
|
1827 unfolding id_def measurable_def eq sets_eq_imp_space_eq[OF eq] . |
|
1828 |
|
1829 lemma sets_Least: |
|
1830 assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> M" |
|
1831 shows "(\<lambda>x. LEAST j. P j x) -` A \<inter> space M \<in> sets M" |
|
1832 proof - |
|
1833 { fix i have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M \<in> sets M" |
|
1834 proof cases |
|
1835 assume i: "(LEAST j. False) = i" |
|
1836 have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M = |
|
1837 {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}))" |
|
1838 by (simp add: set_eq_iff, safe) |
|
1839 (insert i, auto dest: Least_le intro: LeastI intro!: Least_equality) |
|
1840 with meas show ?thesis |
|
1841 by (auto intro!: sets.Int) |
|
1842 next |
|
1843 assume i: "(LEAST j. False) \<noteq> i" |
|
1844 then have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M = |
|
1845 {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x}))" |
|
1846 proof (simp add: set_eq_iff, safe) |
|
1847 fix x assume neq: "(LEAST j. False) \<noteq> (LEAST j. P j x)" |
|
1848 have "\<exists>j. P j x" |
|
1849 by (rule ccontr) (insert neq, auto) |
|
1850 then show "P (LEAST j. P j x) x" by (rule LeastI_ex) |
|
1851 qed (auto dest: Least_le intro!: Least_equality) |
|
1852 with meas show ?thesis |
|
1853 by auto |
|
1854 qed } |
|
1855 then have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) \<in> sets M" |
|
1856 by (intro sets.countable_UN) auto |
|
1857 moreover have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) = |
|
1858 (\<lambda>x. LEAST j. P j x) -` A \<inter> space M" by auto |
|
1859 ultimately show ?thesis by auto |
|
1860 qed |
|
1861 |
|
1862 lemma measurable_mono1: |
|
1863 "M' \<subseteq> Pow \<Omega> \<Longrightarrow> M \<subseteq> M' \<Longrightarrow> |
|
1864 measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N" |
|
1865 using measure_of_subset[of M' \<Omega> M] by (auto simp add: measurable_def) |
|
1866 |
|
1867 subsubsection \<open>Counting space\<close> |
|
1868 |
|
1869 definition count_space :: "'a set \<Rightarrow> 'a measure" where |
|
1870 "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then of_nat (card A) else \<infinity>)" |
|
1871 |
|
1872 lemma |
|
1873 shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>" |
|
1874 and sets_count_space[simp]: "sets (count_space \<Omega>) = Pow \<Omega>" |
|
1875 using sigma_sets_into_sp[of "Pow \<Omega>" \<Omega>] |
|
1876 by (auto simp: count_space_def) |
|
1877 |
|
1878 lemma measurable_count_space_eq1[simp]: |
|
1879 "f \<in> measurable (count_space A) M \<longleftrightarrow> f \<in> A \<rightarrow> space M" |
|
1880 unfolding measurable_def by simp |
|
1881 |
|
1882 lemma measurable_compose_countable': |
|
1883 assumes f: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f i x) \<in> measurable M N" |
|
1884 and g: "g \<in> measurable M (count_space I)" and I: "countable I" |
|
1885 shows "(\<lambda>x. f (g x) x) \<in> measurable M N" |
|
1886 unfolding measurable_def |
|
1887 proof safe |
|
1888 fix x assume "x \<in> space M" then show "f (g x) x \<in> space N" |
|
1889 using measurable_space[OF f] g[THEN measurable_space] by auto |
|
1890 next |
|
1891 fix A assume A: "A \<in> sets N" |
|
1892 have "(\<lambda>x. f (g x) x) -` A \<inter> space M = (\<Union>i\<in>I. (g -` {i} \<inter> space M) \<inter> (f i -` A \<inter> space M))" |
|
1893 using measurable_space[OF g] by auto |
|
1894 also have "\<dots> \<in> sets M" |
|
1895 using f[THEN measurable_sets, OF _ A] g[THEN measurable_sets] |
|
1896 by (auto intro!: sets.countable_UN' I intro: sets.Int[OF measurable_sets measurable_sets]) |
|
1897 finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" . |
|
1898 qed |
|
1899 |
|
1900 lemma measurable_count_space_eq_countable: |
|
1901 assumes "countable A" |
|
1902 shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))" |
|
1903 proof - |
|
1904 { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A" |
|
1905 with \<open>countable A\<close> have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "countable X" |
|
1906 by (auto dest: countable_subset) |
|
1907 moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M" |
|
1908 ultimately have "f -` X \<inter> space M \<in> sets M" |
|
1909 using \<open>X \<subseteq> A\<close> by (auto intro!: sets.countable_UN' simp del: UN_simps) } |
|
1910 then show ?thesis |
|
1911 unfolding measurable_def by auto |
|
1912 qed |
|
1913 |
|
1914 lemma measurable_count_space_eq2: |
|
1915 "finite A \<Longrightarrow> f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))" |
|
1916 by (intro measurable_count_space_eq_countable countable_finite) |
|
1917 |
|
1918 lemma measurable_count_space_eq2_countable: |
|
1919 fixes f :: "'a => 'c::countable" |
|
1920 shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))" |
|
1921 by (intro measurable_count_space_eq_countable countableI_type) |
|
1922 |
|
1923 lemma measurable_compose_countable: |
|
1924 assumes f: "\<And>i::'i::countable. (\<lambda>x. f i x) \<in> measurable M N" and g: "g \<in> measurable M (count_space UNIV)" |
|
1925 shows "(\<lambda>x. f (g x) x) \<in> measurable M N" |
|
1926 by (rule measurable_compose_countable'[OF assms]) auto |
|
1927 |
|
1928 lemma measurable_count_space_const: |
|
1929 "(\<lambda>x. c) \<in> measurable M (count_space UNIV)" |
|
1930 by (simp add: measurable_const) |
|
1931 |
|
1932 lemma measurable_count_space: |
|
1933 "f \<in> measurable (count_space A) (count_space UNIV)" |
|
1934 by simp |
|
1935 |
|
1936 lemma measurable_compose_rev: |
|
1937 assumes f: "f \<in> measurable L N" and g: "g \<in> measurable M L" |
|
1938 shows "(\<lambda>x. f (g x)) \<in> measurable M N" |
|
1939 using measurable_compose[OF g f] . |
|
1940 |
|
1941 lemma measurable_empty_iff: |
|
1942 "space N = {} \<Longrightarrow> f \<in> measurable M N \<longleftrightarrow> space M = {}" |
|
1943 by (auto simp add: measurable_def Pi_iff) |
|
1944 |
|
1945 subsubsection \<open>Extend measure\<close> |
|
1946 |
|
1947 definition "extend_measure \<Omega> I G \<mu> = |
|
1948 (if (\<exists>\<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>') \<and> \<not> (\<forall>i\<in>I. \<mu> i = 0) |
|
1949 then measure_of \<Omega> (G`I) (SOME \<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>') |
|
1950 else measure_of \<Omega> (G`I) (\<lambda>_. 0))" |
|
1951 |
|
1952 lemma space_extend_measure: "G ` I \<subseteq> Pow \<Omega> \<Longrightarrow> space (extend_measure \<Omega> I G \<mu>) = \<Omega>" |
|
1953 unfolding extend_measure_def by simp |
|
1954 |
|
1955 lemma sets_extend_measure: "G ` I \<subseteq> Pow \<Omega> \<Longrightarrow> sets (extend_measure \<Omega> I G \<mu>) = sigma_sets \<Omega> (G`I)" |
|
1956 unfolding extend_measure_def by simp |
|
1957 |
|
1958 lemma emeasure_extend_measure: |
|
1959 assumes M: "M = extend_measure \<Omega> I G \<mu>" |
|
1960 and eq: "\<And>i. i \<in> I \<Longrightarrow> \<mu>' (G i) = \<mu> i" |
|
1961 and ms: "G ` I \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>'" "countably_additive (sets M) \<mu>'" |
|
1962 and "i \<in> I" |
|
1963 shows "emeasure M (G i) = \<mu> i" |
|
1964 proof cases |
|
1965 assume *: "(\<forall>i\<in>I. \<mu> i = 0)" |
|
1966 with M have M_eq: "M = measure_of \<Omega> (G`I) (\<lambda>_. 0)" |
|
1967 by (simp add: extend_measure_def) |
|
1968 from measure_space_0[OF ms(1)] ms \<open>i\<in>I\<close> |
|
1969 have "emeasure M (G i) = 0" |
|
1970 by (intro emeasure_measure_of[OF M_eq]) (auto simp add: M measure_space_def sets_extend_measure) |
|
1971 with \<open>i\<in>I\<close> * show ?thesis |
|
1972 by simp |
|
1973 next |
|
1974 define P where "P \<mu>' \<longleftrightarrow> (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>'" for \<mu>' |
|
1975 assume "\<not> (\<forall>i\<in>I. \<mu> i = 0)" |
|
1976 moreover |
|
1977 have "measure_space (space M) (sets M) \<mu>'" |
|
1978 using ms unfolding measure_space_def by auto standard |
|
1979 with ms eq have "\<exists>\<mu>'. P \<mu>'" |
|
1980 unfolding P_def |
|
1981 by (intro exI[of _ \<mu>']) (auto simp add: M space_extend_measure sets_extend_measure) |
|
1982 ultimately have M_eq: "M = measure_of \<Omega> (G`I) (Eps P)" |
|
1983 by (simp add: M extend_measure_def P_def[symmetric]) |
|
1984 |
|
1985 from \<open>\<exists>\<mu>'. P \<mu>'\<close> have P: "P (Eps P)" by (rule someI_ex) |
|
1986 show "emeasure M (G i) = \<mu> i" |
|
1987 proof (subst emeasure_measure_of[OF M_eq]) |
|
1988 have sets_M: "sets M = sigma_sets \<Omega> (G`I)" |
|
1989 using M_eq ms by (auto simp: sets_extend_measure) |
|
1990 then show "G i \<in> sets M" using \<open>i \<in> I\<close> by auto |
|
1991 show "positive (sets M) (Eps P)" "countably_additive (sets M) (Eps P)" "Eps P (G i) = \<mu> i" |
|
1992 using P \<open>i\<in>I\<close> by (auto simp add: sets_M measure_space_def P_def) |
|
1993 qed fact |
|
1994 qed |
|
1995 |
|
1996 lemma emeasure_extend_measure_Pair: |
|
1997 assumes M: "M = extend_measure \<Omega> {(i, j). I i j} (\<lambda>(i, j). G i j) (\<lambda>(i, j). \<mu> i j)" |
|
1998 and eq: "\<And>i j. I i j \<Longrightarrow> \<mu>' (G i j) = \<mu> i j" |
|
1999 and ms: "\<And>i j. I i j \<Longrightarrow> G i j \<in> Pow \<Omega>" "positive (sets M) \<mu>'" "countably_additive (sets M) \<mu>'" |
|
2000 and "I i j" |
|
2001 shows "emeasure M (G i j) = \<mu> i j" |
|
2002 using emeasure_extend_measure[OF M _ _ ms(2,3), of "(i,j)"] eq ms(1) \<open>I i j\<close> |
|
2003 by (auto simp: subset_eq) |
|
2004 |
|
2005 subsection \<open>The smallest $\sigma$-algebra regarding a function\<close> |
|
2006 |
|
2007 definition |
|
2008 "vimage_algebra X f M = sigma X {f -` A \<inter> X | A. A \<in> sets M}" |
|
2009 |
|
2010 lemma space_vimage_algebra[simp]: "space (vimage_algebra X f M) = X" |
|
2011 unfolding vimage_algebra_def by (rule space_measure_of) auto |
|
2012 |
|
2013 lemma sets_vimage_algebra: "sets (vimage_algebra X f M) = sigma_sets X {f -` A \<inter> X | A. A \<in> sets M}" |
|
2014 unfolding vimage_algebra_def by (rule sets_measure_of) auto |
|
2015 |
|
2016 lemma sets_vimage_algebra2: |
|
2017 "f \<in> X \<rightarrow> space M \<Longrightarrow> sets (vimage_algebra X f M) = {f -` A \<inter> X | A. A \<in> sets M}" |
|
2018 using sigma_sets_vimage_commute[of f X "space M" "sets M"] |
|
2019 unfolding sets_vimage_algebra sets.sigma_sets_eq by simp |
|
2020 |
|
2021 lemma sets_vimage_algebra_cong: "sets M = sets N \<Longrightarrow> sets (vimage_algebra X f M) = sets (vimage_algebra X f N)" |
|
2022 by (simp add: sets_vimage_algebra) |
|
2023 |
|
2024 lemma vimage_algebra_cong: |
|
2025 assumes "X = Y" |
|
2026 assumes "\<And>x. x \<in> Y \<Longrightarrow> f x = g x" |
|
2027 assumes "sets M = sets N" |
|
2028 shows "vimage_algebra X f M = vimage_algebra Y g N" |
|
2029 by (auto simp: vimage_algebra_def assms intro!: arg_cong2[where f=sigma]) |
|
2030 |
|
2031 lemma in_vimage_algebra: "A \<in> sets M \<Longrightarrow> f -` A \<inter> X \<in> sets (vimage_algebra X f M)" |
|
2032 by (auto simp: vimage_algebra_def) |
|
2033 |
|
2034 lemma sets_image_in_sets: |
|
2035 assumes N: "space N = X" |
|
2036 assumes f: "f \<in> measurable N M" |
|
2037 shows "sets (vimage_algebra X f M) \<subseteq> sets N" |
|
2038 unfolding sets_vimage_algebra N[symmetric] |
|
2039 by (rule sets.sigma_sets_subset) (auto intro!: measurable_sets f) |
|
2040 |
|
2041 lemma measurable_vimage_algebra1: "f \<in> X \<rightarrow> space M \<Longrightarrow> f \<in> measurable (vimage_algebra X f M) M" |
|
2042 unfolding measurable_def by (auto intro: in_vimage_algebra) |
|
2043 |
|
2044 lemma measurable_vimage_algebra2: |
|
2045 assumes g: "g \<in> space N \<rightarrow> X" and f: "(\<lambda>x. f (g x)) \<in> measurable N M" |
|
2046 shows "g \<in> measurable N (vimage_algebra X f M)" |
|
2047 unfolding vimage_algebra_def |
|
2048 proof (rule measurable_measure_of) |
|
2049 fix A assume "A \<in> {f -` A \<inter> X | A. A \<in> sets M}" |
|
2050 then obtain Y where Y: "Y \<in> sets M" and A: "A = f -` Y \<inter> X" |
|
2051 by auto |
|
2052 then have "g -` A \<inter> space N = (\<lambda>x. f (g x)) -` Y \<inter> space N" |
|
2053 using g by auto |
|
2054 also have "\<dots> \<in> sets N" |
|
2055 using f Y by (rule measurable_sets) |
|
2056 finally show "g -` A \<inter> space N \<in> sets N" . |
|
2057 qed (insert g, auto) |
|
2058 |
|
2059 lemma vimage_algebra_sigma: |
|
2060 assumes X: "X \<subseteq> Pow \<Omega>'" and f: "f \<in> \<Omega> \<rightarrow> \<Omega>'" |
|
2061 shows "vimage_algebra \<Omega> f (sigma \<Omega>' X) = sigma \<Omega> {f -` A \<inter> \<Omega> | A. A \<in> X }" (is "?V = ?S") |
|
2062 proof (rule measure_eqI) |
|
2063 have \<Omega>: "{f -` A \<inter> \<Omega> |A. A \<in> X} \<subseteq> Pow \<Omega>" by auto |
|
2064 show "sets ?V = sets ?S" |
|
2065 using sigma_sets_vimage_commute[OF f, of X] |
|
2066 by (simp add: space_measure_of_conv f sets_vimage_algebra2 \<Omega> X) |
|
2067 qed (simp add: vimage_algebra_def emeasure_sigma) |
|
2068 |
|
2069 lemma vimage_algebra_vimage_algebra_eq: |
|
2070 assumes *: "f \<in> X \<rightarrow> Y" "g \<in> Y \<rightarrow> space M" |
|
2071 shows "vimage_algebra X f (vimage_algebra Y g M) = vimage_algebra X (\<lambda>x. g (f x)) M" |
|
2072 (is "?VV = ?V") |
|
2073 proof (rule measure_eqI) |
|
2074 have "(\<lambda>x. g (f x)) \<in> X \<rightarrow> space M" "\<And>A. A \<inter> f -` Y \<inter> X = A \<inter> X" |
|
2075 using * by auto |
|
2076 with * show "sets ?VV = sets ?V" |
|
2077 by (simp add: sets_vimage_algebra2 ex_simps[symmetric] vimage_comp comp_def del: ex_simps) |
|
2078 qed (simp add: vimage_algebra_def emeasure_sigma) |
|
2079 |
|
2080 subsubsection \<open>Restricted Space Sigma Algebra\<close> |
|
2081 |
|
2082 definition restrict_space where |
|
2083 "restrict_space M \<Omega> = measure_of (\<Omega> \<inter> space M) ((op \<inter> \<Omega>) ` sets M) (emeasure M)" |
|
2084 |
|
2085 lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega> \<inter> space M" |
|
2086 using sets.sets_into_space unfolding restrict_space_def by (subst space_measure_of) auto |
|
2087 |
|
2088 lemma space_restrict_space2: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>" |
|
2089 by (simp add: space_restrict_space sets.sets_into_space) |
|
2090 |
|
2091 lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M" |
|
2092 unfolding restrict_space_def |
|
2093 proof (subst sets_measure_of) |
|
2094 show "op \<inter> \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)" |
|
2095 by (auto dest: sets.sets_into_space) |
|
2096 have "sigma_sets (\<Omega> \<inter> space M) {((\<lambda>x. x) -` X) \<inter> (\<Omega> \<inter> space M) | X. X \<in> sets M} = |
|
2097 (\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M" |
|
2098 by (subst sigma_sets_vimage_commute[symmetric, where \<Omega>' = "space M"]) |
|
2099 (auto simp add: sets.sigma_sets_eq) |
|
2100 moreover have "{((\<lambda>x. x) -` X) \<inter> (\<Omega> \<inter> space M) | X. X \<in> sets M} = (\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M" |
|
2101 by auto |
|
2102 moreover have "(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M = (op \<inter> \<Omega>) ` sets M" |
|
2103 by (intro image_cong) (auto dest: sets.sets_into_space) |
|
2104 ultimately show "sigma_sets (\<Omega> \<inter> space M) (op \<inter> \<Omega> ` sets M) = op \<inter> \<Omega> ` sets M" |
|
2105 by simp |
|
2106 qed |
|
2107 |
|
2108 lemma restrict_space_sets_cong: |
|
2109 "A = B \<Longrightarrow> sets M = sets N \<Longrightarrow> sets (restrict_space M A) = sets (restrict_space N B)" |
|
2110 by (auto simp: sets_restrict_space) |
|
2111 |
|
2112 lemma sets_restrict_space_count_space : |
|
2113 "sets (restrict_space (count_space A) B) = sets (count_space (A \<inter> B))" |
|
2114 by(auto simp add: sets_restrict_space) |
|
2115 |
|
2116 lemma sets_restrict_UNIV[simp]: "sets (restrict_space M UNIV) = sets M" |
|
2117 by (auto simp add: sets_restrict_space) |
|
2118 |
|
2119 lemma sets_restrict_restrict_space: |
|
2120 "sets (restrict_space (restrict_space M A) B) = sets (restrict_space M (A \<inter> B))" |
|
2121 unfolding sets_restrict_space image_comp by (intro image_cong) auto |
|
2122 |
|
2123 lemma sets_restrict_space_iff: |
|
2124 "\<Omega> \<inter> space M \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)" |
|
2125 proof (subst sets_restrict_space, safe) |
|
2126 fix A assume "\<Omega> \<inter> space M \<in> sets M" and A: "A \<in> sets M" |
|
2127 then have "(\<Omega> \<inter> space M) \<inter> A \<in> sets M" |
|
2128 by rule |
|
2129 also have "(\<Omega> \<inter> space M) \<inter> A = \<Omega> \<inter> A" |
|
2130 using sets.sets_into_space[OF A] by auto |
|
2131 finally show "\<Omega> \<inter> A \<in> sets M" |
|
2132 by auto |
|
2133 qed auto |
|
2134 |
|
2135 lemma sets_restrict_space_cong: "sets M = sets N \<Longrightarrow> sets (restrict_space M \<Omega>) = sets (restrict_space N \<Omega>)" |
|
2136 by (simp add: sets_restrict_space) |
|
2137 |
|
2138 lemma restrict_space_eq_vimage_algebra: |
|
2139 "\<Omega> \<subseteq> space M \<Longrightarrow> sets (restrict_space M \<Omega>) = sets (vimage_algebra \<Omega> (\<lambda>x. x) M)" |
|
2140 unfolding restrict_space_def |
|
2141 apply (subst sets_measure_of) |
|
2142 apply (auto simp add: image_subset_iff dest: sets.sets_into_space) [] |
|
2143 apply (auto simp add: sets_vimage_algebra intro!: arg_cong2[where f=sigma_sets]) |
|
2144 done |
|
2145 |
|
2146 lemma sets_Collect_restrict_space_iff: |
|
2147 assumes "S \<in> sets M" |
|
2148 shows "{x\<in>space (restrict_space M S). P x} \<in> sets (restrict_space M S) \<longleftrightarrow> {x\<in>space M. x \<in> S \<and> P x} \<in> sets M" |
|
2149 proof - |
|
2150 have "{x\<in>S. P x} = {x\<in>space M. x \<in> S \<and> P x}" |
|
2151 using sets.sets_into_space[OF assms] by auto |
|
2152 then show ?thesis |
|
2153 by (subst sets_restrict_space_iff) (auto simp add: space_restrict_space assms) |
|
2154 qed |
|
2155 |
|
2156 lemma measurable_restrict_space1: |
|
2157 assumes f: "f \<in> measurable M N" |
|
2158 shows "f \<in> measurable (restrict_space M \<Omega>) N" |
|
2159 unfolding measurable_def |
|
2160 proof (intro CollectI conjI ballI) |
|
2161 show sp: "f \<in> space (restrict_space M \<Omega>) \<rightarrow> space N" |
|
2162 using measurable_space[OF f] by (auto simp: space_restrict_space) |
|
2163 |
|
2164 fix A assume "A \<in> sets N" |
|
2165 have "f -` A \<inter> space (restrict_space M \<Omega>) = (f -` A \<inter> space M) \<inter> (\<Omega> \<inter> space M)" |
|
2166 by (auto simp: space_restrict_space) |
|
2167 also have "\<dots> \<in> sets (restrict_space M \<Omega>)" |
|
2168 unfolding sets_restrict_space |
|
2169 using measurable_sets[OF f \<open>A \<in> sets N\<close>] by blast |
|
2170 finally show "f -` A \<inter> space (restrict_space M \<Omega>) \<in> sets (restrict_space M \<Omega>)" . |
|
2171 qed |
|
2172 |
|
2173 lemma measurable_restrict_space2_iff: |
|
2174 "f \<in> measurable M (restrict_space N \<Omega>) \<longleftrightarrow> (f \<in> measurable M N \<and> f \<in> space M \<rightarrow> \<Omega>)" |
|
2175 proof - |
|
2176 have "\<And>A. f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f -` \<Omega> \<inter> f -` A \<inter> space M = f -` A \<inter> space M" |
|
2177 by auto |
|
2178 then show ?thesis |
|
2179 by (auto simp: measurable_def space_restrict_space Pi_Int[symmetric] sets_restrict_space) |
|
2180 qed |
|
2181 |
|
2182 lemma measurable_restrict_space2: |
|
2183 "f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> f \<in> measurable M (restrict_space N \<Omega>)" |
|
2184 by (simp add: measurable_restrict_space2_iff) |
|
2185 |
|
2186 lemma measurable_piecewise_restrict: |
|
2187 assumes I: "countable C" |
|
2188 and X: "\<And>\<Omega>. \<Omega> \<in> C \<Longrightarrow> \<Omega> \<inter> space M \<in> sets M" "space M \<subseteq> \<Union>C" |
|
2189 and f: "\<And>\<Omega>. \<Omega> \<in> C \<Longrightarrow> f \<in> measurable (restrict_space M \<Omega>) N" |
|
2190 shows "f \<in> measurable M N" |
|
2191 proof (rule measurableI) |
|
2192 fix x assume "x \<in> space M" |
|
2193 with X obtain \<Omega> where "\<Omega> \<in> C" "x \<in> \<Omega>" "x \<in> space M" by auto |
|
2194 then show "f x \<in> space N" |
|
2195 by (auto simp: space_restrict_space intro: f measurable_space) |
|
2196 next |
|
2197 fix A assume A: "A \<in> sets N" |
|
2198 have "f -` A \<inter> space M = (\<Union>\<Omega>\<in>C. (f -` A \<inter> (\<Omega> \<inter> space M)))" |
|
2199 using X by (auto simp: subset_eq) |
|
2200 also have "\<dots> \<in> sets M" |
|
2201 using measurable_sets[OF f A] X I |
|
2202 by (intro sets.countable_UN') (auto simp: sets_restrict_space_iff space_restrict_space) |
|
2203 finally show "f -` A \<inter> space M \<in> sets M" . |
|
2204 qed |
|
2205 |
|
2206 lemma measurable_piecewise_restrict_iff: |
|
2207 "countable C \<Longrightarrow> (\<And>\<Omega>. \<Omega> \<in> C \<Longrightarrow> \<Omega> \<inter> space M \<in> sets M) \<Longrightarrow> space M \<subseteq> (\<Union>C) \<Longrightarrow> |
|
2208 f \<in> measurable M N \<longleftrightarrow> (\<forall>\<Omega>\<in>C. f \<in> measurable (restrict_space M \<Omega>) N)" |
|
2209 by (auto intro: measurable_piecewise_restrict measurable_restrict_space1) |
|
2210 |
|
2211 lemma measurable_If_restrict_space_iff: |
|
2212 "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> |
|
2213 (\<lambda>x. if P x then f x else g x) \<in> measurable M N \<longleftrightarrow> |
|
2214 (f \<in> measurable (restrict_space M {x. P x}) N \<and> g \<in> measurable (restrict_space M {x. \<not> P x}) N)" |
|
2215 by (subst measurable_piecewise_restrict_iff[where C="{{x. P x}, {x. \<not> P x}}"]) |
|
2216 (auto simp: Int_def sets.sets_Collect_neg space_restrict_space conj_commute[of _ "x \<in> space M" for x] |
|
2217 cong: measurable_cong') |
|
2218 |
|
2219 lemma measurable_If: |
|
2220 "f \<in> measurable M M' \<Longrightarrow> g \<in> measurable M M' \<Longrightarrow> {x\<in>space M. P x} \<in> sets M \<Longrightarrow> |
|
2221 (\<lambda>x. if P x then f x else g x) \<in> measurable M M'" |
|
2222 unfolding measurable_If_restrict_space_iff by (auto intro: measurable_restrict_space1) |
|
2223 |
|
2224 lemma measurable_If_set: |
|
2225 assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'" |
|
2226 assumes P: "A \<inter> space M \<in> sets M" |
|
2227 shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> measurable M M'" |
|
2228 proof (rule measurable_If[OF measure]) |
|
2229 have "{x \<in> space M. x \<in> A} = A \<inter> space M" by auto |
|
2230 thus "{x \<in> space M. x \<in> A} \<in> sets M" using \<open>A \<inter> space M \<in> sets M\<close> by auto |
|
2231 qed |
|
2232 |
|
2233 lemma measurable_restrict_space_iff: |
|
2234 "\<Omega> \<inter> space M \<in> sets M \<Longrightarrow> c \<in> space N \<Longrightarrow> |
|
2235 f \<in> measurable (restrict_space M \<Omega>) N \<longleftrightarrow> (\<lambda>x. if x \<in> \<Omega> then f x else c) \<in> measurable M N" |
|
2236 by (subst measurable_If_restrict_space_iff) |
|
2237 (simp_all add: Int_def conj_commute measurable_const) |
|
2238 |
|
2239 lemma restrict_space_singleton: "{x} \<in> sets M \<Longrightarrow> sets (restrict_space M {x}) = sets (count_space {x})" |
|
2240 using sets_restrict_space_iff[of "{x}" M] |
|
2241 by (auto simp add: sets_restrict_space_iff dest!: subset_singletonD) |
|
2242 |
|
2243 lemma measurable_restrict_countable: |
|
2244 assumes X[intro]: "countable X" |
|
2245 assumes sets[simp]: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M" |
|
2246 assumes space[simp]: "\<And>x. x \<in> X \<Longrightarrow> f x \<in> space N" |
|
2247 assumes f: "f \<in> measurable (restrict_space M (- X)) N" |
|
2248 shows "f \<in> measurable M N" |
|
2249 using f sets.countable[OF sets X] |
|
2250 by (intro measurable_piecewise_restrict[where M=M and C="{- X} \<union> ((\<lambda>x. {x}) ` X)"]) |
|
2251 (auto simp: Diff_Int_distrib2 Compl_eq_Diff_UNIV Int_insert_left sets.Diff restrict_space_singleton |
|
2252 simp del: sets_count_space cong: measurable_cong_sets) |
|
2253 |
|
2254 lemma measurable_discrete_difference: |
|
2255 assumes f: "f \<in> measurable M N" |
|
2256 assumes X: "countable X" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M" "\<And>x. x \<in> X \<Longrightarrow> g x \<in> space N" |
|
2257 assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x" |
|
2258 shows "g \<in> measurable M N" |
|
2259 by (rule measurable_restrict_countable[OF X]) |
|
2260 (auto simp: eq[symmetric] space_restrict_space cong: measurable_cong' intro: f measurable_restrict_space1) |
|
2261 |
|
2262 end |
|