1179 by blast |
1179 by blast |
1180 qed |
1180 qed |
1181 |
1181 |
1182 subsubsection \<open>Dynkin systems\<close> |
1182 subsubsection \<open>Dynkin systems\<close> |
1183 |
1183 |
1184 locale%important dynkin_system = subset_class + |
1184 locale%important Dynkin_system = subset_class + |
1185 assumes space: "\<Omega> \<in> M" |
1185 assumes space: "\<Omega> \<in> M" |
1186 and compl[intro!]: "\<And>A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M" |
1186 and compl[intro!]: "\<And>A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M" |
1187 and UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> M |
1187 and UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> M |
1188 \<Longrightarrow> (\<Union>i::nat. A i) \<in> M" |
1188 \<Longrightarrow> (\<Union>i::nat. A i) \<in> M" |
1189 |
1189 |
1190 lemma (in dynkin_system) empty[intro, simp]: "{} \<in> M" |
1190 lemma (in Dynkin_system) empty[intro, simp]: "{} \<in> M" |
1191 using space compl[of "\<Omega>"] by simp |
1191 using space compl[of "\<Omega>"] by simp |
1192 |
1192 |
1193 lemma (in dynkin_system) diff: |
1193 lemma (in Dynkin_system) diff: |
1194 assumes sets: "D \<in> M" "E \<in> M" and "D \<subseteq> E" |
1194 assumes sets: "D \<in> M" "E \<in> M" and "D \<subseteq> E" |
1195 shows "E - D \<in> M" |
1195 shows "E - D \<in> M" |
1196 proof - |
1196 proof - |
1197 let ?f = "\<lambda>x. if x = 0 then D else if x = Suc 0 then \<Omega> - E else {}" |
1197 let ?f = "\<lambda>x. if x = 0 then D else if x = Suc 0 then \<Omega> - E else {}" |
1198 have "range ?f = {D, \<Omega> - E, {}}" |
1198 have "range ?f = {D, \<Omega> - E, {}}" |
1207 also have "\<Omega> - (D \<union> (\<Omega> - E)) = E - D" |
1207 also have "\<Omega> - (D \<union> (\<Omega> - E)) = E - D" |
1208 using assms sets_into_space by auto |
1208 using assms sets_into_space by auto |
1209 finally show ?thesis . |
1209 finally show ?thesis . |
1210 qed |
1210 qed |
1211 |
1211 |
1212 lemma dynkin_systemI: |
1212 lemma Dynkin_systemI: |
1213 assumes "\<And> A. A \<in> M \<Longrightarrow> A \<subseteq> \<Omega>" "\<Omega> \<in> M" |
1213 assumes "\<And> A. A \<in> M \<Longrightarrow> A \<subseteq> \<Omega>" "\<Omega> \<in> M" |
1214 assumes "\<And> A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M" |
1214 assumes "\<And> A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M" |
1215 assumes "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> M |
1215 assumes "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> M |
1216 \<Longrightarrow> (\<Union>i::nat. A i) \<in> M" |
1216 \<Longrightarrow> (\<Union>i::nat. A i) \<in> M" |
1217 shows "dynkin_system \<Omega> M" |
1217 shows "Dynkin_system \<Omega> M" |
1218 using assms by (auto simp: dynkin_system_def dynkin_system_axioms_def subset_class_def) |
1218 using assms by (auto simp: Dynkin_system_def Dynkin_system_axioms_def subset_class_def) |
1219 |
1219 |
1220 lemma dynkin_systemI': |
1220 lemma Dynkin_systemI': |
1221 assumes 1: "\<And> A. A \<in> M \<Longrightarrow> A \<subseteq> \<Omega>" |
1221 assumes 1: "\<And> A. A \<in> M \<Longrightarrow> A \<subseteq> \<Omega>" |
1222 assumes empty: "{} \<in> M" |
1222 assumes empty: "{} \<in> M" |
1223 assumes Diff: "\<And> A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M" |
1223 assumes Diff: "\<And> A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M" |
1224 assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> M |
1224 assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> M |
1225 \<Longrightarrow> (\<Union>i::nat. A i) \<in> M" |
1225 \<Longrightarrow> (\<Union>i::nat. A i) \<in> M" |
1226 shows "dynkin_system \<Omega> M" |
1226 shows "Dynkin_system \<Omega> M" |
1227 proof - |
1227 proof - |
1228 from Diff[OF empty] have "\<Omega> \<in> M" by auto |
1228 from Diff[OF empty] have "\<Omega> \<in> M" by auto |
1229 from 1 this Diff 2 show ?thesis |
1229 from 1 this Diff 2 show ?thesis |
1230 by (intro dynkin_systemI) auto |
1230 by (intro Dynkin_systemI) auto |
1231 qed |
1231 qed |
1232 |
1232 |
1233 lemma dynkin_system_trivial: |
1233 lemma Dynkin_system_trivial: |
1234 shows "dynkin_system A (Pow A)" |
1234 shows "Dynkin_system A (Pow A)" |
1235 by (rule dynkin_systemI) auto |
1235 by (rule Dynkin_systemI) auto |
1236 |
1236 |
1237 lemma sigma_algebra_imp_dynkin_system: |
1237 lemma sigma_algebra_imp_Dynkin_system: |
1238 assumes "sigma_algebra \<Omega> M" shows "dynkin_system \<Omega> M" |
1238 assumes "sigma_algebra \<Omega> M" shows "Dynkin_system \<Omega> M" |
1239 proof - |
1239 proof - |
1240 interpret sigma_algebra \<Omega> M by fact |
1240 interpret sigma_algebra \<Omega> M by fact |
1241 show ?thesis using sets_into_space by (fastforce intro!: dynkin_systemI) |
1241 show ?thesis using sets_into_space by (fastforce intro!: Dynkin_systemI) |
1242 qed |
1242 qed |
1243 |
1243 |
1244 subsubsection "Intersection sets systems" |
1244 subsubsection "Intersection sets systems" |
1245 |
1245 |
1246 definition%important Int_stable :: "'a set set \<Rightarrow> bool" where |
1246 definition%important Int_stable :: "'a set set \<Rightarrow> bool" where |
1282 qed auto |
1282 qed auto |
1283 qed |
1283 qed |
1284 |
1284 |
1285 subsubsection "Smallest Dynkin systems" |
1285 subsubsection "Smallest Dynkin systems" |
1286 |
1286 |
1287 definition%important dynkin :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" where |
1287 definition%important Dynkin :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" where |
1288 "dynkin \<Omega> M = (\<Inter>{D. dynkin_system \<Omega> D \<and> M \<subseteq> D})" |
1288 "Dynkin \<Omega> M = (\<Inter>{D. Dynkin_system \<Omega> D \<and> M \<subseteq> D})" |
1289 |
1289 |
1290 lemma dynkin_system_dynkin: |
1290 lemma Dynkin_system_Dynkin: |
1291 assumes "M \<subseteq> Pow (\<Omega>)" |
1291 assumes "M \<subseteq> Pow (\<Omega>)" |
1292 shows "dynkin_system \<Omega> (dynkin \<Omega> M)" |
1292 shows "Dynkin_system \<Omega> (Dynkin \<Omega> M)" |
1293 proof (rule dynkin_systemI) |
1293 proof (rule Dynkin_systemI) |
1294 fix A assume "A \<in> dynkin \<Omega> M" |
1294 fix A assume "A \<in> Dynkin \<Omega> M" |
1295 moreover |
1295 moreover |
1296 { fix D assume "A \<in> D" and d: "dynkin_system \<Omega> D" |
1296 { fix D assume "A \<in> D" and d: "Dynkin_system \<Omega> D" |
1297 then have "A \<subseteq> \<Omega>" by (auto simp: dynkin_system_def subset_class_def) } |
1297 then have "A \<subseteq> \<Omega>" by (auto simp: Dynkin_system_def subset_class_def) } |
1298 moreover have "{D. dynkin_system \<Omega> D \<and> M \<subseteq> D} \<noteq> {}" |
1298 moreover have "{D. Dynkin_system \<Omega> D \<and> M \<subseteq> D} \<noteq> {}" |
1299 using assms dynkin_system_trivial by fastforce |
1299 using assms Dynkin_system_trivial by fastforce |
1300 ultimately show "A \<subseteq> \<Omega>" |
1300 ultimately show "A \<subseteq> \<Omega>" |
1301 unfolding dynkin_def using assms |
1301 unfolding Dynkin_def using assms |
1302 by auto |
1302 by auto |
1303 next |
1303 next |
1304 show "\<Omega> \<in> dynkin \<Omega> M" |
1304 show "\<Omega> \<in> Dynkin \<Omega> M" |
1305 unfolding dynkin_def using dynkin_system.space by fastforce |
1305 unfolding Dynkin_def using Dynkin_system.space by fastforce |
1306 next |
1306 next |
1307 fix A assume "A \<in> dynkin \<Omega> M" |
1307 fix A assume "A \<in> Dynkin \<Omega> M" |
1308 then show "\<Omega> - A \<in> dynkin \<Omega> M" |
1308 then show "\<Omega> - A \<in> Dynkin \<Omega> M" |
1309 unfolding dynkin_def using dynkin_system.compl by force |
1309 unfolding Dynkin_def using Dynkin_system.compl by force |
1310 next |
1310 next |
1311 fix A :: "nat \<Rightarrow> 'a set" |
1311 fix A :: "nat \<Rightarrow> 'a set" |
1312 assume A: "disjoint_family A" "range A \<subseteq> dynkin \<Omega> M" |
1312 assume A: "disjoint_family A" "range A \<subseteq> Dynkin \<Omega> M" |
1313 show "(\<Union>i. A i) \<in> dynkin \<Omega> M" unfolding dynkin_def |
1313 show "(\<Union>i. A i) \<in> Dynkin \<Omega> M" unfolding Dynkin_def |
1314 proof (simp, safe) |
1314 proof (simp, safe) |
1315 fix D assume "dynkin_system \<Omega> D" "M \<subseteq> D" |
1315 fix D assume "Dynkin_system \<Omega> D" "M \<subseteq> D" |
1316 with A have "(\<Union>i. A i) \<in> D" |
1316 with A have "(\<Union>i. A i) \<in> D" |
1317 by (intro dynkin_system.UN) (auto simp: dynkin_def) |
1317 by (intro Dynkin_system.UN) (auto simp: Dynkin_def) |
1318 then show "(\<Union>i. A i) \<in> D" by auto |
1318 then show "(\<Union>i. A i) \<in> D" by auto |
1319 qed |
1319 qed |
1320 qed |
1320 qed |
1321 |
1321 |
1322 lemma dynkin_Basic[intro]: "A \<in> M \<Longrightarrow> A \<in> dynkin \<Omega> M" |
1322 lemma Dynkin_Basic[intro]: "A \<in> M \<Longrightarrow> A \<in> Dynkin \<Omega> M" |
1323 unfolding dynkin_def by auto |
1323 unfolding Dynkin_def by auto |
1324 |
1324 |
1325 lemma (in dynkin_system) restricted_dynkin_system: |
1325 lemma (in Dynkin_system) restricted_Dynkin_system: |
1326 assumes "D \<in> M" |
1326 assumes "D \<in> M" |
1327 shows "dynkin_system \<Omega> {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> D \<in> M}" |
1327 shows "Dynkin_system \<Omega> {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> D \<in> M}" |
1328 proof (rule dynkin_systemI, simp_all) |
1328 proof (rule Dynkin_systemI, simp_all) |
1329 have "\<Omega> \<inter> D = D" |
1329 have "\<Omega> \<inter> D = D" |
1330 using \<open>D \<in> M\<close> sets_into_space by auto |
1330 using \<open>D \<in> M\<close> sets_into_space by auto |
1331 then show "\<Omega> \<inter> D \<in> M" |
1331 then show "\<Omega> \<inter> D \<in> M" |
1332 using \<open>D \<in> M\<close> by auto |
1332 using \<open>D \<in> M\<close> by auto |
1333 next |
1333 next |
1344 by ((fastforce simp: disjoint_family_on_def)+) |
1344 by ((fastforce simp: disjoint_family_on_def)+) |
1345 then show "(\<Union>x. A x) \<subseteq> \<Omega> \<and> (\<Union>x. A x) \<inter> D \<in> M" |
1345 then show "(\<Union>x. A x) \<subseteq> \<Omega> \<and> (\<Union>x. A x) \<inter> D \<in> M" |
1346 by (auto simp del: UN_simps) |
1346 by (auto simp del: UN_simps) |
1347 qed |
1347 qed |
1348 |
1348 |
1349 lemma (in dynkin_system) dynkin_subset: |
1349 lemma (in Dynkin_system) Dynkin_subset: |
1350 assumes "N \<subseteq> M" |
1350 assumes "N \<subseteq> M" |
1351 shows "dynkin \<Omega> N \<subseteq> M" |
1351 shows "Dynkin \<Omega> N \<subseteq> M" |
1352 proof - |
1352 proof - |
1353 have "dynkin_system \<Omega> M" .. |
1353 have "Dynkin_system \<Omega> M" .. |
1354 then have "dynkin_system \<Omega> M" |
1354 then have "Dynkin_system \<Omega> M" |
1355 using assms unfolding dynkin_system_def dynkin_system_axioms_def subset_class_def by simp |
1355 using assms unfolding Dynkin_system_def Dynkin_system_axioms_def subset_class_def by simp |
1356 with \<open>N \<subseteq> M\<close> show ?thesis by (auto simp add: dynkin_def) |
1356 with \<open>N \<subseteq> M\<close> show ?thesis by (auto simp add: Dynkin_def) |
1357 qed |
1357 qed |
1358 |
1358 |
1359 lemma sigma_eq_dynkin: |
1359 lemma sigma_eq_Dynkin: |
1360 assumes sets: "M \<subseteq> Pow \<Omega>" |
1360 assumes sets: "M \<subseteq> Pow \<Omega>" |
1361 assumes "Int_stable M" |
1361 assumes "Int_stable M" |
1362 shows "sigma_sets \<Omega> M = dynkin \<Omega> M" |
1362 shows "sigma_sets \<Omega> M = Dynkin \<Omega> M" |
1363 proof - |
1363 proof - |
1364 have "dynkin \<Omega> M \<subseteq> sigma_sets (\<Omega>) (M)" |
1364 have "Dynkin \<Omega> M \<subseteq> sigma_sets (\<Omega>) (M)" |
1365 using sigma_algebra_imp_dynkin_system |
1365 using sigma_algebra_imp_Dynkin_system |
1366 unfolding dynkin_def sigma_sets_least_sigma_algebra[OF sets] by auto |
1366 unfolding Dynkin_def sigma_sets_least_sigma_algebra[OF sets] by auto |
1367 moreover |
1367 moreover |
1368 interpret dynkin_system \<Omega> "dynkin \<Omega> M" |
1368 interpret Dynkin_system \<Omega> "Dynkin \<Omega> M" |
1369 using dynkin_system_dynkin[OF sets] . |
1369 using Dynkin_system_Dynkin[OF sets] . |
1370 have "sigma_algebra \<Omega> (dynkin \<Omega> M)" |
1370 have "sigma_algebra \<Omega> (Dynkin \<Omega> M)" |
1371 unfolding sigma_algebra_eq_Int_stable Int_stable_def |
1371 unfolding sigma_algebra_eq_Int_stable Int_stable_def |
1372 proof (intro ballI) |
1372 proof (intro ballI) |
1373 fix A B assume "A \<in> dynkin \<Omega> M" "B \<in> dynkin \<Omega> M" |
1373 fix A B assume "A \<in> Dynkin \<Omega> M" "B \<in> Dynkin \<Omega> M" |
1374 let ?D = "\<lambda>E. {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> E \<in> dynkin \<Omega> M}" |
1374 let ?D = "\<lambda>E. {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> E \<in> Dynkin \<Omega> M}" |
1375 have "M \<subseteq> ?D B" |
1375 have "M \<subseteq> ?D B" |
1376 proof |
1376 proof |
1377 fix E assume "E \<in> M" |
1377 fix E assume "E \<in> M" |
1378 then have "M \<subseteq> ?D E" "E \<in> dynkin \<Omega> M" |
1378 then have "M \<subseteq> ?D E" "E \<in> Dynkin \<Omega> M" |
1379 using sets_into_space \<open>Int_stable M\<close> by (auto simp: Int_stable_def) |
1379 using sets_into_space \<open>Int_stable M\<close> by (auto simp: Int_stable_def) |
1380 then have "dynkin \<Omega> M \<subseteq> ?D E" |
1380 then have "Dynkin \<Omega> M \<subseteq> ?D E" |
1381 using restricted_dynkin_system \<open>E \<in> dynkin \<Omega> M\<close> |
1381 using restricted_Dynkin_system \<open>E \<in> Dynkin \<Omega> M\<close> |
1382 by (intro dynkin_system.dynkin_subset) simp_all |
1382 by (intro Dynkin_system.Dynkin_subset) simp_all |
1383 then have "B \<in> ?D E" |
1383 then have "B \<in> ?D E" |
1384 using \<open>B \<in> dynkin \<Omega> M\<close> by auto |
1384 using \<open>B \<in> Dynkin \<Omega> M\<close> by auto |
1385 then have "E \<inter> B \<in> dynkin \<Omega> M" |
1385 then have "E \<inter> B \<in> Dynkin \<Omega> M" |
1386 by (subst Int_commute) simp |
1386 by (subst Int_commute) simp |
1387 then show "E \<in> ?D B" |
1387 then show "E \<in> ?D B" |
1388 using sets \<open>E \<in> M\<close> by auto |
1388 using sets \<open>E \<in> M\<close> by auto |
1389 qed |
1389 qed |
1390 then have "dynkin \<Omega> M \<subseteq> ?D B" |
1390 then have "Dynkin \<Omega> M \<subseteq> ?D B" |
1391 using restricted_dynkin_system \<open>B \<in> dynkin \<Omega> M\<close> |
1391 using restricted_Dynkin_system \<open>B \<in> Dynkin \<Omega> M\<close> |
1392 by (intro dynkin_system.dynkin_subset) simp_all |
1392 by (intro Dynkin_system.Dynkin_subset) simp_all |
1393 then show "A \<inter> B \<in> dynkin \<Omega> M" |
1393 then show "A \<inter> B \<in> Dynkin \<Omega> M" |
1394 using \<open>A \<in> dynkin \<Omega> M\<close> sets_into_space by auto |
1394 using \<open>A \<in> Dynkin \<Omega> M\<close> sets_into_space by auto |
1395 qed |
1395 qed |
1396 from sigma_algebra.sigma_sets_subset[OF this, of "M"] |
1396 from sigma_algebra.sigma_sets_subset[OF this, of "M"] |
1397 have "sigma_sets (\<Omega>) (M) \<subseteq> dynkin \<Omega> M" by auto |
1397 have "sigma_sets (\<Omega>) (M) \<subseteq> Dynkin \<Omega> M" by auto |
1398 ultimately have "sigma_sets (\<Omega>) (M) = dynkin \<Omega> M" by auto |
1398 ultimately have "sigma_sets (\<Omega>) (M) = Dynkin \<Omega> M" by auto |
1399 then show ?thesis |
1399 then show ?thesis |
1400 by (auto simp: dynkin_def) |
1400 by (auto simp: Dynkin_def) |
1401 qed |
1401 qed |
1402 |
1402 |
1403 lemma (in dynkin_system) dynkin_idem: |
1403 lemma (in Dynkin_system) Dynkin_idem: |
1404 "dynkin \<Omega> M = M" |
1404 "Dynkin \<Omega> M = M" |
1405 proof - |
1405 proof - |
1406 have "dynkin \<Omega> M = M" |
1406 have "Dynkin \<Omega> M = M" |
1407 proof |
1407 proof |
1408 show "M \<subseteq> dynkin \<Omega> M" |
1408 show "M \<subseteq> Dynkin \<Omega> M" |
1409 using dynkin_Basic by auto |
1409 using Dynkin_Basic by auto |
1410 show "dynkin \<Omega> M \<subseteq> M" |
1410 show "Dynkin \<Omega> M \<subseteq> M" |
1411 by (intro dynkin_subset) auto |
1411 by (intro Dynkin_subset) auto |
1412 qed |
1412 qed |
1413 then show ?thesis |
1413 then show ?thesis |
1414 by (auto simp: dynkin_def) |
1414 by (auto simp: Dynkin_def) |
1415 qed |
1415 qed |
1416 |
1416 |
1417 lemma (in dynkin_system) dynkin_lemma: |
1417 lemma (in Dynkin_system) Dynkin_lemma: |
1418 assumes "Int_stable E" |
1418 assumes "Int_stable E" |
1419 and E: "E \<subseteq> M" "M \<subseteq> sigma_sets \<Omega> E" |
1419 and E: "E \<subseteq> M" "M \<subseteq> sigma_sets \<Omega> E" |
1420 shows "sigma_sets \<Omega> E = M" |
1420 shows "sigma_sets \<Omega> E = M" |
1421 proof - |
1421 proof - |
1422 have "E \<subseteq> Pow \<Omega>" |
1422 have "E \<subseteq> Pow \<Omega>" |
1423 using E sets_into_space by force |
1423 using E sets_into_space by force |
1424 then have *: "sigma_sets \<Omega> E = dynkin \<Omega> E" |
1424 then have *: "sigma_sets \<Omega> E = Dynkin \<Omega> E" |
1425 using \<open>Int_stable E\<close> by (rule sigma_eq_dynkin) |
1425 using \<open>Int_stable E\<close> by (rule sigma_eq_Dynkin) |
1426 then have "dynkin \<Omega> E = M" |
1426 then have "Dynkin \<Omega> E = M" |
1427 using assms dynkin_subset[OF E(1)] by simp |
1427 using assms Dynkin_subset[OF E(1)] by simp |
1428 with * show ?thesis |
1428 with * show ?thesis |
1429 using assms by (auto simp: dynkin_def) |
1429 using assms by (auto simp: Dynkin_def) |
1430 qed |
1430 qed |
1431 |
1431 |
1432 subsubsection \<open>Induction rule for intersection-stable generators\<close> |
1432 subsubsection \<open>Induction rule for intersection-stable generators\<close> |
1433 |
1433 |
1434 text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras |
1434 text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras |