1 (* Title: HOL/Probability/Fin_Map.thy |
1 (* Title: HOL/Probability/Fin_Map.thy |
2 Author: Fabian Immler, TU München |
2 Author: Fabian Immler, TU München |
3 *) |
3 *) |
4 |
4 |
5 section {* Finite Maps *} |
5 section \<open>Finite Maps\<close> |
6 |
6 |
7 theory Fin_Map |
7 theory Fin_Map |
8 imports Finite_Product_Measure |
8 imports Finite_Product_Measure |
9 begin |
9 begin |
10 |
10 |
11 text {* Auxiliary type that is instantiated to @{class polish_space}, needed for the proof of |
11 text \<open>Auxiliary type that is instantiated to @{class polish_space}, needed for the proof of |
12 projective limit. @{const extensional} functions are used for the representation in order to |
12 projective limit. @{const extensional} functions are used for the representation in order to |
13 stay close to the developments of (finite) products @{const Pi\<^sub>E} and their sigma-algebra |
13 stay close to the developments of (finite) products @{const Pi\<^sub>E} and their sigma-algebra |
14 @{const Pi\<^sub>M}. *} |
14 @{const Pi\<^sub>M}.\<close> |
15 |
15 |
16 typedef ('i, 'a) finmap ("(_ \<Rightarrow>\<^sub>F /_)" [22, 21] 21) = |
16 typedef ('i, 'a) finmap ("(_ \<Rightarrow>\<^sub>F /_)" [22, 21] 21) = |
17 "{(I::'i set, f::'i \<Rightarrow> 'a). finite I \<and> f \<in> extensional I}" by auto |
17 "{(I::'i set, f::'i \<Rightarrow> 'a). finite I \<and> f \<in> extensional I}" by auto |
18 |
18 |
19 subsection {* Domain and Application *} |
19 subsection \<open>Domain and Application\<close> |
20 |
20 |
21 definition domain where "domain P = fst (Rep_finmap P)" |
21 definition domain where "domain P = fst (Rep_finmap P)" |
22 |
22 |
23 lemma finite_domain[simp, intro]: "finite (domain P)" |
23 lemma finite_domain[simp, intro]: "finite (domain P)" |
24 by (cases P) (auto simp: domain_def Abs_finmap_inverse) |
24 by (cases P) (auto simp: domain_def Abs_finmap_inverse) |
36 lemma finmap_eq_iff: "P = Q \<longleftrightarrow> (domain P = domain Q \<and> (\<forall>i\<in>domain P. P i = Q i))" |
36 lemma finmap_eq_iff: "P = Q \<longleftrightarrow> (domain P = domain Q \<and> (\<forall>i\<in>domain P. P i = Q i))" |
37 by (cases P, cases Q) |
37 by (cases P, cases Q) |
38 (auto simp add: Abs_finmap_inject extensional_def domain_def proj_def Abs_finmap_inverse |
38 (auto simp add: Abs_finmap_inject extensional_def domain_def proj_def Abs_finmap_inverse |
39 intro: extensionalityI) |
39 intro: extensionalityI) |
40 |
40 |
41 subsection {* Countable Finite Maps *} |
41 subsection \<open>Countable Finite Maps\<close> |
42 |
42 |
43 instance finmap :: (countable, countable) countable |
43 instance finmap :: (countable, countable) countable |
44 proof |
44 proof |
45 obtain mapper where mapper: "\<And>fm :: 'a \<Rightarrow>\<^sub>F 'b. set (mapper fm) = domain fm" |
45 obtain mapper where mapper: "\<And>fm :: 'a \<Rightarrow>\<^sub>F 'b. set (mapper fm) = domain fm" |
46 by (metis finite_list[OF finite_domain]) |
46 by (metis finite_list[OF finite_domain]) |
48 proof (rule inj_onI) |
48 proof (rule inj_onI) |
49 fix f1 f2 assume "?F f1 = ?F f2" |
49 fix f1 f2 assume "?F f1 = ?F f2" |
50 then have "map fst (?F f1) = map fst (?F f2)" by simp |
50 then have "map fst (?F f1) = map fst (?F f2)" by simp |
51 then have "mapper f1 = mapper f2" by (simp add: comp_def) |
51 then have "mapper f1 = mapper f2" by (simp add: comp_def) |
52 then have "domain f1 = domain f2" by (simp add: mapper[symmetric]) |
52 then have "domain f1 = domain f2" by (simp add: mapper[symmetric]) |
53 with `?F f1 = ?F f2` show "f1 = f2" |
53 with \<open>?F f1 = ?F f2\<close> show "f1 = f2" |
54 unfolding `mapper f1 = mapper f2` map_eq_conv mapper |
54 unfolding \<open>mapper f1 = mapper f2\<close> map_eq_conv mapper |
55 by (simp add: finmap_eq_iff) |
55 by (simp add: finmap_eq_iff) |
56 qed |
56 qed |
57 then show "\<exists>to_nat :: 'a \<Rightarrow>\<^sub>F 'b \<Rightarrow> nat. inj to_nat" |
57 then show "\<exists>to_nat :: 'a \<Rightarrow>\<^sub>F 'b \<Rightarrow> nat. inj to_nat" |
58 by (intro exI[of _ "to_nat \<circ> ?F"] inj_comp) auto |
58 by (intro exI[of _ "to_nat \<circ> ?F"] inj_comp) auto |
59 qed |
59 qed |
60 |
60 |
61 subsection {* Constructor of Finite Maps *} |
61 subsection \<open>Constructor of Finite Maps\<close> |
62 |
62 |
63 definition "finmap_of inds f = Abs_finmap (inds, restrict f inds)" |
63 definition "finmap_of inds f = Abs_finmap (inds, restrict f inds)" |
64 |
64 |
65 lemma proj_finmap_of[simp]: |
65 lemma proj_finmap_of[simp]: |
66 assumes "finite inds" |
66 assumes "finite inds" |
91 assume "x \<in> S" "y \<in> S" hence "x \<in> extensional K" "y \<in> extensional K" using assms by auto |
91 assume "x \<in> S" "y \<in> S" hence "x \<in> extensional K" "y \<in> extensional K" using assms by auto |
92 ultimately |
92 ultimately |
93 show "x = y" using assms by (simp add: extensional_restrict) |
93 show "x = y" using assms by (simp add: extensional_restrict) |
94 qed |
94 qed |
95 |
95 |
96 subsection {* Product set of Finite Maps *} |
96 subsection \<open>Product set of Finite Maps\<close> |
97 |
97 |
98 text {* This is @{term Pi} for Finite Maps, most of this is copied *} |
98 text \<open>This is @{term Pi} for Finite Maps, most of this is copied\<close> |
99 |
99 |
100 definition Pi' :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a set) \<Rightarrow> ('i \<Rightarrow>\<^sub>F 'a) set" where |
100 definition Pi' :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a set) \<Rightarrow> ('i \<Rightarrow>\<^sub>F 'a) set" where |
101 "Pi' I A = { P. domain P = I \<and> (\<forall>i. i \<in> I \<longrightarrow> (P)\<^sub>F i \<in> A i) } " |
101 "Pi' I A = { P. domain P = I \<and> (\<forall>i. i \<in> I \<longrightarrow> (P)\<^sub>F i \<in> A i) } " |
102 |
102 |
103 syntax |
103 syntax |
105 syntax (xsymbols) |
105 syntax (xsymbols) |
106 "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>' _\<in>_./ _)" 10) |
106 "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>' _\<in>_./ _)" 10) |
107 translations |
107 translations |
108 "PI' x:A. B" == "CONST Pi' A (%x. B)" |
108 "PI' x:A. B" == "CONST Pi' A (%x. B)" |
109 |
109 |
110 subsubsection{*Basic Properties of @{term Pi'}*} |
110 subsubsection\<open>Basic Properties of @{term Pi'}\<close> |
111 |
111 |
112 lemma Pi'_I[intro!]: "domain f = A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi' A B" |
112 lemma Pi'_I[intro!]: "domain f = A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi' A B" |
113 by (simp add: Pi'_def) |
113 by (simp add: Pi'_def) |
114 |
114 |
115 lemma Pi'_I'[simp]: "domain f = A \<Longrightarrow> (\<And>x. x \<in> A \<longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi' A B" |
115 lemma Pi'_I'[simp]: "domain f = A \<Longrightarrow> (\<And>x. x \<in> A \<longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi' A B" |
169 also have "open \<dots>" |
169 also have "open \<dots>" |
170 proof (rule, safe, cases) |
170 proof (rule, safe, cases) |
171 fix i::"'a set" |
171 fix i::"'a set" |
172 assume "finite i" |
172 assume "finite i" |
173 hence "{m. domain m = i} = Pi' i (\<lambda>_. UNIV)" by (auto simp: Pi'_def) |
173 hence "{m. domain m = i} = Pi' i (\<lambda>_. UNIV)" by (auto simp: Pi'_def) |
174 also have "open \<dots>" by (auto intro: open_Pi'I simp: `finite i`) |
174 also have "open \<dots>" by (auto intro: open_Pi'I simp: \<open>finite i\<close>) |
175 finally show "open {m. domain m = i}" . |
175 finally show "open {m. domain m = i}" . |
176 next |
176 next |
177 fix i::"'a set" |
177 fix i::"'a set" |
178 assume "\<not> finite i" hence "{m. domain m = i} = {}" by auto |
178 assume "\<not> finite i" hence "{m. domain m = i} = {}" by auto |
179 also have "open \<dots>" by simp |
179 also have "open \<dots>" by simp |
194 let ?S = "Pi' (domain a) (\<lambda>x. if x = i then S else UNIV)" |
194 let ?S = "Pi' (domain a) (\<lambda>x. if x = i then S else UNIV)" |
195 assume "open S" hence "open ?S" by (auto intro!: open_Pi'I) |
195 assume "open S" hence "open ?S" by (auto intro!: open_Pi'I) |
196 moreover assume "\<forall>S. open S \<longrightarrow> a \<in> S \<longrightarrow> eventually (\<lambda>x. x \<in> S) F" "a i \<in> S" |
196 moreover assume "\<forall>S. open S \<longrightarrow> a \<in> S \<longrightarrow> eventually (\<lambda>x. x \<in> S) F" "a i \<in> S" |
197 ultimately have "eventually (\<lambda>x. x \<in> ?S) F" by auto |
197 ultimately have "eventually (\<lambda>x. x \<in> ?S) F" by auto |
198 thus "eventually (\<lambda>x. (x)\<^sub>F i \<in> S) F" |
198 thus "eventually (\<lambda>x. (x)\<^sub>F i \<in> S) F" |
199 by eventually_elim (insert `a i \<in> S`, force simp: Pi'_iff split: split_if_asm) |
199 by eventually_elim (insert \<open>a i \<in> S\<close>, force simp: Pi'_iff split: split_if_asm) |
200 qed |
200 qed |
201 |
201 |
202 lemma continuous_proj: |
202 lemma continuous_proj: |
203 shows "continuous_on s (\<lambda>x. (x)\<^sub>F i)" |
203 shows "continuous_on s (\<lambda>x. (x)\<^sub>F i)" |
204 unfolding continuous_on_def by (safe intro!: tendsto_proj tendsto_ident_at) |
204 unfolding continuous_on_def by (safe intro!: tendsto_proj tendsto_ident_at) |
234 intro!: bexI[where x="\<lambda>i. f i \<inter> g i"]) |
234 intro!: bexI[where x="\<lambda>i. f i \<inter> g i"]) |
235 next |
235 next |
236 case (UN B) |
236 case (UN B) |
237 then obtain b where "x \<in> b" "b \<in> B" by auto |
237 then obtain b where "x \<in> b" "b \<in> B" by auto |
238 hence "\<exists>a\<in>?A. a \<subseteq> b" using UN by simp |
238 hence "\<exists>a\<in>?A. a \<subseteq> b" using UN by simp |
239 thus ?case using `b \<in> B` by blast |
239 thus ?case using \<open>b \<in> B\<close> by blast |
240 next |
240 next |
241 case (Basis s) |
241 case (Basis s) |
242 then obtain a b where xs: "x\<in> Pi' a b" "s = Pi' a b" "\<And>i. i\<in>a \<Longrightarrow> open (b i)" by auto |
242 then obtain a b where xs: "x\<in> Pi' a b" "s = Pi' a b" "\<And>i. i\<in>a \<Longrightarrow> open (b i)" by auto |
243 have "\<forall>i. \<exists>a. (i \<in> domain x \<and> open (b i) \<and> (x)\<^sub>F i \<in> b i) \<longrightarrow> (a\<in>A i \<and> a \<subseteq> b i)" |
243 have "\<forall>i. \<exists>a. (i \<in> domain x \<and> open (b i) \<and> (x)\<^sub>F i \<in> b i) \<longrightarrow> (a\<in>A i \<and> a \<subseteq> b i)" |
244 using open_sub[of _ b] by auto |
244 using open_sub[of _ b] by auto |
340 show ?case |
340 show ?case |
341 proof safe |
341 proof safe |
342 fix x assume "x \<in> s" |
342 fix x assume "x \<in> s" |
343 hence [simp]: "finite a" and a_dom: "a = domain x" using s by (auto simp: Pi'_iff) |
343 hence [simp]: "finite a" and a_dom: "a = domain x" using s by (auto simp: Pi'_iff) |
344 obtain es where es: "\<forall>i \<in> a. es i > 0 \<and> (\<forall>y. dist y (proj x i) < es i \<longrightarrow> y \<in> b i)" |
344 obtain es where es: "\<forall>i \<in> a. es i > 0 \<and> (\<forall>y. dist y (proj x i) < es i \<longrightarrow> y \<in> b i)" |
345 using b `x \<in> s` by atomize_elim (intro bchoice, auto simp: open_dist s) |
345 using b \<open>x \<in> s\<close> by atomize_elim (intro bchoice, auto simp: open_dist s) |
346 hence in_b: "\<And>i y. i \<in> a \<Longrightarrow> dist y (proj x i) < es i \<Longrightarrow> y \<in> b i" by auto |
346 hence in_b: "\<And>i y. i \<in> a \<Longrightarrow> dist y (proj x i) < es i \<Longrightarrow> y \<in> b i" by auto |
347 show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> s" |
347 show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> s" |
348 proof (cases, rule, safe) |
348 proof (cases, rule, safe) |
349 assume "a \<noteq> {}" |
349 assume "a \<noteq> {}" |
350 show "0 < min 1 (Min (es ` a))" using es by (auto simp: `a \<noteq> {}`) |
350 show "0 < min 1 (Min (es ` a))" using es by (auto simp: \<open>a \<noteq> {}\<close>) |
351 fix y assume d: "dist y x < min 1 (Min (es ` a))" |
351 fix y assume d: "dist y x < min 1 (Min (es ` a))" |
352 show "y \<in> s" unfolding s |
352 show "y \<in> s" unfolding s |
353 proof |
353 proof |
354 show "domain y = a" using d s `a \<noteq> {}` by (auto simp: dist_le_1_imp_domain_eq a_dom) |
354 show "domain y = a" using d s \<open>a \<noteq> {}\<close> by (auto simp: dist_le_1_imp_domain_eq a_dom) |
355 fix i assume i: "i \<in> a" |
355 fix i assume i: "i \<in> a" |
356 hence "dist ((y)\<^sub>F i) ((x)\<^sub>F i) < es i" using d |
356 hence "dist ((y)\<^sub>F i) ((x)\<^sub>F i) < es i" using d |
357 by (auto simp: dist_finmap_def `a \<noteq> {}` intro!: le_less_trans[OF dist_proj]) |
357 by (auto simp: dist_finmap_def \<open>a \<noteq> {}\<close> intro!: le_less_trans[OF dist_proj]) |
358 with i show "y i \<in> b i" by (rule in_b) |
358 with i show "y i \<in> b i" by (rule in_b) |
359 qed |
359 qed |
360 next |
360 next |
361 assume "\<not>a \<noteq> {}" |
361 assume "\<not>a \<noteq> {}" |
362 thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> s" |
362 thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> s" |
363 using s `x \<in> s` by (auto simp: Pi'_def dist_le_1_imp_domain_eq intro!: exI[where x=1]) |
363 using s \<open>x \<in> s\<close> by (auto simp: Pi'_def dist_le_1_imp_domain_eq intro!: exI[where x=1]) |
364 qed |
364 qed |
365 qed |
365 qed |
366 qed |
366 qed |
367 next |
367 next |
368 assume "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" |
368 assume "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" |
413 finally show "dist P Q \<le> dist P R + dist Q R" by (simp add: dist_finmap_def ac_simps) |
413 finally show "dist P Q \<le> dist P R + dist Q R" by (simp add: dist_finmap_def ac_simps) |
414 qed |
414 qed |
415 |
415 |
416 end |
416 end |
417 |
417 |
418 subsection {* Complete Space of Finite Maps *} |
418 subsection \<open>Complete Space of Finite Maps\<close> |
419 |
419 |
420 lemma tendsto_finmap: |
420 lemma tendsto_finmap: |
421 fixes f::"nat \<Rightarrow> ('i \<Rightarrow>\<^sub>F ('a::metric_space))" |
421 fixes f::"nat \<Rightarrow> ('i \<Rightarrow>\<^sub>F ('a::metric_space))" |
422 assumes ind_f: "\<And>n. domain (f n) = domain g" |
422 assumes ind_f: "\<And>n. domain (f n) = domain g" |
423 assumes proj_g: "\<And>i. i \<in> domain g \<Longrightarrow> (\<lambda>n. (f n) i) ----> g i" |
423 assumes proj_g: "\<And>i. i \<in> domain g \<Longrightarrow> (\<lambda>n. (f n) i) ----> g i" |
428 let ?dists = "\<lambda>x i. dist ((f x)\<^sub>F i) ((g)\<^sub>F i)" |
428 let ?dists = "\<lambda>x i. dist ((f x)\<^sub>F i) ((g)\<^sub>F i)" |
429 have "eventually (\<lambda>x. \<forall>i\<in>domain g. ?dists x i < e) sequentially" |
429 have "eventually (\<lambda>x. \<forall>i\<in>domain g. ?dists x i < e) sequentially" |
430 using finite_domain[of g] proj_g |
430 using finite_domain[of g] proj_g |
431 proof induct |
431 proof induct |
432 case (insert i G) |
432 case (insert i G) |
433 with `0 < e` have "eventually (\<lambda>x. ?dists x i < e) sequentially" by (auto simp add: tendsto_iff) |
433 with \<open>0 < e\<close> have "eventually (\<lambda>x. ?dists x i < e) sequentially" by (auto simp add: tendsto_iff) |
434 moreover |
434 moreover |
435 from insert have "eventually (\<lambda>x. \<forall>i\<in>G. dist ((f x)\<^sub>F i) ((g)\<^sub>F i) < e) sequentially" by simp |
435 from insert have "eventually (\<lambda>x. \<forall>i\<in>G. dist ((f x)\<^sub>F i) ((g)\<^sub>F i) < e) sequentially" by simp |
436 ultimately show ?case by eventually_elim auto |
436 ultimately show ?case by eventually_elim auto |
437 qed simp |
437 qed simp |
438 thus "eventually (\<lambda>x. dist (f x) g < e) sequentially" |
438 thus "eventually (\<lambda>x. dist (f x) g < e) sequentially" |
439 by eventually_elim (auto simp add: dist_finmap_def finite_proj_diag ind_f `0 < e`) |
439 by eventually_elim (auto simp add: dist_finmap_def finite_proj_diag ind_f \<open>0 < e\<close>) |
440 qed |
440 qed |
441 |
441 |
442 instance finmap :: (type, complete_space) complete_space |
442 instance finmap :: (type, complete_space) complete_space |
443 proof |
443 proof |
444 fix P::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>F 'b" |
444 fix P::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>F 'b" |
455 { |
455 { |
456 fix i assume "i \<in> d" |
456 fix i assume "i \<in> d" |
457 have "Cauchy (p i)" unfolding cauchy p_def |
457 have "Cauchy (p i)" unfolding cauchy p_def |
458 proof safe |
458 proof safe |
459 fix e::real assume "0 < e" |
459 fix e::real assume "0 < e" |
460 with `Cauchy P` obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> dist (P n) (P N) < min e 1" |
460 with \<open>Cauchy P\<close> obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> dist (P n) (P N) < min e 1" |
461 by (force simp: cauchy min_def) |
461 by (force simp: cauchy min_def) |
462 hence "\<And>n. n \<ge> N \<Longrightarrow> domain (P n) = domain (P N)" using dist_le_1_imp_domain_eq by auto |
462 hence "\<And>n. n \<ge> N \<Longrightarrow> domain (P n) = domain (P N)" using dist_le_1_imp_domain_eq by auto |
463 with dim have dim: "\<And>n. n \<ge> N \<Longrightarrow> domain (P n) = d" by (metis nat_le_linear) |
463 with dim have dim: "\<And>n. n \<ge> N \<Longrightarrow> domain (P n) = d" by (metis nat_le_linear) |
464 show "\<exists>N. \<forall>n\<ge>N. dist ((P n) i) ((P N) i) < e" |
464 show "\<exists>N. \<forall>n\<ge>N. dist ((P n) i) ((P N) i) < e" |
465 proof (safe intro!: exI[where x="N"]) |
465 proof (safe intro!: exI[where x="N"]) |
466 fix n assume "N \<le> n" have "N \<le> N" by simp |
466 fix n assume "N \<le> n" have "N \<le> N" by simp |
467 have "dist ((P n) i) ((P N) i) \<le> dist (P n) (P N)" |
467 have "dist ((P n) i) ((P N) i) \<le> dist (P n) (P N)" |
468 using dim[OF `N \<le> n`] dim[OF `N \<le> N`] `i \<in> d` |
468 using dim[OF \<open>N \<le> n\<close>] dim[OF \<open>N \<le> N\<close>] \<open>i \<in> d\<close> |
469 by (auto intro!: dist_proj) |
469 by (auto intro!: dist_proj) |
470 also have "\<dots> < e" using N[OF `N \<le> n`] by simp |
470 also have "\<dots> < e" using N[OF \<open>N \<le> n\<close>] by simp |
471 finally show "dist ((P n) i) ((P N) i) < e" . |
471 finally show "dist ((P n) i) ((P N) i) < e" . |
472 qed |
472 qed |
473 qed |
473 qed |
474 hence "convergent (p i)" by (metis Cauchy_convergent_iff) |
474 hence "convergent (p i)" by (metis Cauchy_convergent_iff) |
475 hence "p i ----> q i" unfolding q_def convergent_def by (metis limI) |
475 hence "p i ----> q i" unfolding q_def convergent_def by (metis limI) |
478 proof (rule metric_LIMSEQ_I) |
478 proof (rule metric_LIMSEQ_I) |
479 fix e::real assume "0 < e" |
479 fix e::real assume "0 < e" |
480 have "\<exists>ni. \<forall>i\<in>d. \<forall>n\<ge>ni i. dist (p i n) (q i) < e" |
480 have "\<exists>ni. \<forall>i\<in>d. \<forall>n\<ge>ni i. dist (p i n) (q i) < e" |
481 proof (safe intro!: bchoice) |
481 proof (safe intro!: bchoice) |
482 fix i assume "i \<in> d" |
482 fix i assume "i \<in> d" |
483 from p[OF `i \<in> d`, THEN metric_LIMSEQ_D, OF `0 < e`] |
483 from p[OF \<open>i \<in> d\<close>, THEN metric_LIMSEQ_D, OF \<open>0 < e\<close>] |
484 show "\<exists>no. \<forall>n\<ge>no. dist (p i n) (q i) < e" . |
484 show "\<exists>no. \<forall>n\<ge>no. dist (p i n) (q i) < e" . |
485 qed then guess ni .. note ni = this |
485 qed then guess ni .. note ni = this |
486 def N \<equiv> "max Nd (Max (ni ` d))" |
486 def N \<equiv> "max Nd (Max (ni ` d))" |
487 show "\<exists>N. \<forall>n\<ge>N. dist (P n) Q < e" |
487 show "\<exists>N. \<forall>n\<ge>N. dist (P n) Q < e" |
488 proof (safe intro!: exI[where x="N"]) |
488 proof (safe intro!: exI[where x="N"]) |
489 fix n assume "N \<le> n" |
489 fix n assume "N \<le> n" |
490 hence dom: "domain (P n) = d" "domain Q = d" "domain (P n) = domain Q" |
490 hence dom: "domain (P n) = d" "domain Q = d" "domain (P n) = domain Q" |
491 using dim by (simp_all add: N_def Q_def dim_def Abs_finmap_inverse) |
491 using dim by (simp_all add: N_def Q_def dim_def Abs_finmap_inverse) |
492 show "dist (P n) Q < e" |
492 show "dist (P n) Q < e" |
493 proof (rule dist_finmap_lessI[OF dom(3) `0 < e`]) |
493 proof (rule dist_finmap_lessI[OF dom(3) \<open>0 < e\<close>]) |
494 fix i |
494 fix i |
495 assume "i \<in> domain (P n)" |
495 assume "i \<in> domain (P n)" |
496 hence "ni i \<le> Max (ni ` d)" using dom by simp |
496 hence "ni i \<le> Max (ni ` d)" using dom by simp |
497 also have "\<dots> \<le> N" by (simp add: N_def) |
497 also have "\<dots> \<le> N" by (simp add: N_def) |
498 finally show "dist ((P n)\<^sub>F i) ((Q)\<^sub>F i) < e" using ni `i \<in> domain (P n)` `N \<le> n` dom |
498 finally show "dist ((P n)\<^sub>F i) ((Q)\<^sub>F i) < e" using ni \<open>i \<in> domain (P n)\<close> \<open>N \<le> n\<close> dom |
499 by (auto simp: p_def q N_def less_imp_le) |
499 by (auto simp: p_def q N_def less_imp_le) |
500 qed |
500 qed |
501 qed |
501 qed |
502 qed |
502 qed |
503 thus "convergent P" by (auto simp: convergent_def) |
503 thus "convergent P" by (auto simp: convergent_def) |
504 qed |
504 qed |
505 |
505 |
506 subsection {* Second Countable Space of Finite Maps *} |
506 subsection \<open>Second Countable Space of Finite Maps\<close> |
507 |
507 |
508 instantiation finmap :: (countable, second_countable_topology) second_countable_topology |
508 instantiation finmap :: (countable, second_countable_topology) second_countable_topology |
509 begin |
509 begin |
510 |
510 |
511 definition basis_proj::"'b set set" |
511 definition basis_proj::"'b set set" |
580 thus "\<exists>y. x i \<in> y \<and> y \<subseteq> a i \<and> y \<in> basis_proj" by auto |
580 thus "\<exists>y. x i \<in> y \<and> y \<subseteq> a i \<and> y \<in> basis_proj" by auto |
581 qed |
581 qed |
582 then guess B .. note B = this |
582 then guess B .. note B = this |
583 def B' \<equiv> "Pi' (domain x) (\<lambda>i. (B i)::'b set)" |
583 def B' \<equiv> "Pi' (domain x) (\<lambda>i. (B i)::'b set)" |
584 have "B' \<subseteq> Pi' (domain x) a" using B by (auto intro!: Pi'_mono simp: B'_def) |
584 have "B' \<subseteq> Pi' (domain x) a" using B by (auto intro!: Pi'_mono simp: B'_def) |
585 also note `\<dots> \<subseteq> O'` |
585 also note \<open>\<dots> \<subseteq> O'\<close> |
586 finally show "\<exists>B'\<in>basis_finmap. x \<in> B' \<and> B' \<subseteq> O'" using B |
586 finally show "\<exists>B'\<in>basis_finmap. x \<in> B' \<and> B' \<subseteq> O'" using B |
587 by (auto intro!: bexI[where x=B'] Pi'_mono in_basis_finmapI simp: B'_def) |
587 by (auto intro!: bexI[where x=B'] Pi'_mono in_basis_finmapI simp: B'_def) |
588 qed |
588 qed |
589 |
589 |
590 lemma range_enum_basis_finmap_imp_open: |
590 lemma range_enum_basis_finmap_imp_open: |
594 |
594 |
595 instance proof qed (blast intro: finmap_topological_basis countable_basis_finmap topological_basis_imp_subbasis) |
595 instance proof qed (blast intro: finmap_topological_basis countable_basis_finmap topological_basis_imp_subbasis) |
596 |
596 |
597 end |
597 end |
598 |
598 |
599 subsection {* Polish Space of Finite Maps *} |
599 subsection \<open>Polish Space of Finite Maps\<close> |
600 |
600 |
601 instance finmap :: (countable, polish_space) polish_space proof qed |
601 instance finmap :: (countable, polish_space) polish_space proof qed |
602 |
602 |
603 |
603 |
604 subsection {* Product Measurable Space of Finite Maps *} |
604 subsection \<open>Product Measurable Space of Finite Maps\<close> |
605 |
605 |
606 definition "PiF I M \<equiv> |
606 definition "PiF I M \<equiv> |
607 sigma (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j))) {(\<Pi>' j\<in>J. X j) |X J. J \<in> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}" |
607 sigma (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j))) {(\<Pi>' j\<in>J. X j) |X J. J \<in> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}" |
608 |
608 |
609 abbreviation |
609 abbreviation |
698 proof - |
698 proof - |
699 have "\<Union>{f s|s. P s} = (\<Union>n::nat. let s = set (from_nat n) in if P s then f s else {})" |
699 have "\<Union>{f s|s. P s} = (\<Union>n::nat. let s = set (from_nat n) in if P s then f s else {})" |
700 proof safe |
700 proof safe |
701 fix x X s assume *: "x \<in> f s" "P s" |
701 fix x X s assume *: "x \<in> f s" "P s" |
702 with assms obtain l where "s = set l" using finite_list by blast |
702 with assms obtain l where "s = set l" using finite_list by blast |
703 with * show "x \<in> (\<Union>n. let s = set (from_nat n) in if P s then f s else {})" using `P s` |
703 with * show "x \<in> (\<Union>n. let s = set (from_nat n) in if P s then f s else {})" using \<open>P s\<close> |
704 by (auto intro!: exI[where x="to_nat l"]) |
704 by (auto intro!: exI[where x="to_nat l"]) |
705 next |
705 next |
706 fix x n assume "x \<in> (let s = set (from_nat n) in if P s then f s else {})" |
706 fix x n assume "x \<in> (let s = set (from_nat n) in if P s then f s else {})" |
707 thus "x \<in> \<Union>{f s|s. P s}" using assms by (auto simp: Let_def split: split_if_asm) |
707 thus "x \<in> \<Union>{f s|s. P s}" using assms by (auto simp: Let_def split: split_if_asm) |
708 qed |
708 qed |
753 also have "\<dots> \<in> sets (PiF I M)" |
753 also have "\<dots> \<in> sets (PiF I M)" |
754 apply (intro sets.Int sets.countable_nat_UN subsetI, safe) |
754 apply (intro sets.Int sets.countable_nat_UN subsetI, safe) |
755 apply (case_tac "set (from_nat i) \<in> I") |
755 apply (case_tac "set (from_nat i) \<in> I") |
756 apply simp_all |
756 apply simp_all |
757 apply (rule singleton_subspace_set_in_sets[OF measurable_sets[OF MN]]) |
757 apply (rule singleton_subspace_set_in_sets[OF measurable_sets[OF MN]]) |
758 using assms `y \<in> sets N` |
758 using assms \<open>y \<in> sets N\<close> |
759 apply (auto simp: space_PiF) |
759 apply (auto simp: space_PiF) |
760 done |
760 done |
761 finally show "A -` y \<inter> space (PiF I M) \<in> sets (PiF I M)" . |
761 finally show "A -` y \<inter> space (PiF I M) \<in> sets (PiF I M)" . |
762 next |
762 next |
763 fix x assume "x \<in> space (PiF I M)" thus "A x \<in> space N" |
763 fix x assume "x \<in> space (PiF I M)" thus "A x \<in> space N" |
804 also have "\<dots> \<in> sets (PiF J M)" using Union by (intro sets.countable_nat_UN) auto |
804 also have "\<dots> \<in> sets (PiF J M)" using Union by (intro sets.countable_nat_UN) auto |
805 finally show ?case . |
805 finally show ?case . |
806 next |
806 next |
807 case (Compl a) |
807 case (Compl a) |
808 have "(space (PiF I M) - a) \<inter> {m. domain m \<in> J} = (space (PiF J M) - (a \<inter> {m. domain m \<in> J}))" |
808 have "(space (PiF I M) - a) \<inter> {m. domain m \<in> J} = (space (PiF J M) - (a \<inter> {m. domain m \<in> J}))" |
809 using `J \<subseteq> I` by (auto simp: space_PiF Pi'_def) |
809 using \<open>J \<subseteq> I\<close> by (auto simp: space_PiF Pi'_def) |
810 also have "\<dots> \<in> sets (PiF J M)" using Compl by auto |
810 also have "\<dots> \<in> sets (PiF J M)" using Compl by auto |
811 finally show ?case by (simp add: space_PiF) |
811 finally show ?case by (simp add: space_PiF) |
812 qed simp |
812 qed simp |
813 |
813 |
814 lemma measurable_finmap_of: |
814 lemma measurable_finmap_of: |
846 shows "finmap_of J \<in> measurable (Pi\<^sub>M J M) (PiF {J} M)" |
846 shows "finmap_of J \<in> measurable (Pi\<^sub>M J M) (PiF {J} M)" |
847 apply (rule measurable_finmap_of) |
847 apply (rule measurable_finmap_of) |
848 apply (rule measurable_component_singleton) |
848 apply (rule measurable_component_singleton) |
849 apply simp |
849 apply simp |
850 apply rule |
850 apply rule |
851 apply (rule `finite J`) |
851 apply (rule \<open>finite J\<close>) |
852 apply simp |
852 apply simp |
853 done |
853 done |
854 |
854 |
855 lemma proj_measurable_singleton: |
855 lemma proj_measurable_singleton: |
856 assumes "A \<in> sets (M i)" |
856 assumes "A \<in> sets (M i)" |
857 shows "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space (PiF {I} M) \<in> sets (PiF {I} M)" |
857 shows "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space (PiF {I} M) \<in> sets (PiF {I} M)" |
858 proof cases |
858 proof cases |
859 assume "i \<in> I" |
859 assume "i \<in> I" |
860 hence "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space (PiF {I} M) = |
860 hence "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space (PiF {I} M) = |
861 Pi' I (\<lambda>x. if x = i then A else space (M x))" |
861 Pi' I (\<lambda>x. if x = i then A else space (M x))" |
862 using sets.sets_into_space[OF ] `A \<in> sets (M i)` assms |
862 using sets.sets_into_space[OF ] \<open>A \<in> sets (M i)\<close> assms |
863 by (auto simp: space_PiF Pi'_def) |
863 by (auto simp: space_PiF Pi'_def) |
864 thus ?thesis using assms `A \<in> sets (M i)` |
864 thus ?thesis using assms \<open>A \<in> sets (M i)\<close> |
865 by (intro in_sets_PiFI) auto |
865 by (intro in_sets_PiFI) auto |
866 next |
866 next |
867 assume "i \<notin> I" |
867 assume "i \<notin> I" |
868 hence "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space (PiF {I} M) = |
868 hence "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space (PiF {I} M) = |
869 (if undefined \<in> A then space (PiF {I} M) else {})" by (auto simp: space_PiF Pi'_def) |
869 (if undefined \<in> A then space (PiF {I} M) else {})" by (auto simp: space_PiF Pi'_def) |
872 |
872 |
873 lemma measurable_proj_singleton: |
873 lemma measurable_proj_singleton: |
874 assumes "i \<in> I" |
874 assumes "i \<in> I" |
875 shows "(\<lambda>x. (x)\<^sub>F i) \<in> measurable (PiF {I} M) (M i)" |
875 shows "(\<lambda>x. (x)\<^sub>F i) \<in> measurable (PiF {I} M) (M i)" |
876 by (unfold measurable_def, intro CollectI conjI ballI proj_measurable_singleton assms) |
876 by (unfold measurable_def, intro CollectI conjI ballI proj_measurable_singleton assms) |
877 (insert `i \<in> I`, auto simp: space_PiF) |
877 (insert \<open>i \<in> I\<close>, auto simp: space_PiF) |
878 |
878 |
879 lemma measurable_proj_countable: |
879 lemma measurable_proj_countable: |
880 fixes I::"'a::countable set set" |
880 fixes I::"'a::countable set set" |
881 assumes "y \<in> space (M i)" |
881 assumes "y \<in> space (M i)" |
882 shows "(\<lambda>x. if i \<in> domain x then (x)\<^sub>F i else y) \<in> measurable (PiF I M) (M i)" |
882 shows "(\<lambda>x. if i \<in> domain x then (x)\<^sub>F i else y) \<in> measurable (PiF I M) (M i)" |
887 proof safe |
887 proof safe |
888 fix z assume "z \<in> sets (M i)" |
888 fix z assume "z \<in> sets (M i)" |
889 have "(\<lambda>x. if i \<in> domain x then x i else y) -` z \<inter> space (PiF {J} M) = |
889 have "(\<lambda>x. if i \<in> domain x then x i else y) -` z \<inter> space (PiF {J} M) = |
890 (\<lambda>x. if i \<in> J then (x)\<^sub>F i else y) -` z \<inter> space (PiF {J} M)" |
890 (\<lambda>x. if i \<in> J then (x)\<^sub>F i else y) -` z \<inter> space (PiF {J} M)" |
891 by (auto simp: space_PiF Pi'_def) |
891 by (auto simp: space_PiF Pi'_def) |
892 also have "\<dots> \<in> sets (PiF {J} M)" using `z \<in> sets (M i)` `finite J` |
892 also have "\<dots> \<in> sets (PiF {J} M)" using \<open>z \<in> sets (M i)\<close> \<open>finite J\<close> |
893 by (cases "i \<in> J") (auto intro!: measurable_sets[OF measurable_proj_singleton]) |
893 by (cases "i \<in> J") (auto intro!: measurable_sets[OF measurable_proj_singleton]) |
894 finally show "(\<lambda>x. if i \<in> domain x then x i else y) -` z \<inter> space (PiF {J} M) \<in> |
894 finally show "(\<lambda>x. if i \<in> domain x then x i else y) -` z \<inter> space (PiF {J} M) \<in> |
895 sets (PiF {J} M)" . |
895 sets (PiF {J} M)" . |
896 qed (insert `y \<in> space (M i)`, auto simp: space_PiF Pi'_def) |
896 qed (insert \<open>y \<in> space (M i)\<close>, auto simp: space_PiF Pi'_def) |
897 qed |
897 qed |
898 |
898 |
899 lemma measurable_restrict_proj: |
899 lemma measurable_restrict_proj: |
900 assumes "J \<in> II" "finite J" |
900 assumes "J \<in> II" "finite J" |
901 shows "finmap_of J \<in> measurable (PiM J M) (PiF II M)" |
901 shows "finmap_of J \<in> measurable (PiM J M) (PiF II M)" |
925 lemma space_PiF_singleton_eq_product: |
925 lemma space_PiF_singleton_eq_product: |
926 assumes "finite I" |
926 assumes "finite I" |
927 shows "space (PiF {I} M) = (\<Pi>' i\<in>I. space (M i))" |
927 shows "space (PiF {I} M) = (\<Pi>' i\<in>I. space (M i))" |
928 by (auto simp: product_def space_PiF assms) |
928 by (auto simp: product_def space_PiF assms) |
929 |
929 |
930 text {* adapted from @{thm sets_PiM_single} *} |
930 text \<open>adapted from @{thm sets_PiM_single}\<close> |
931 |
931 |
932 lemma sets_PiF_single: |
932 lemma sets_PiF_single: |
933 assumes "finite I" "I \<noteq> {}" |
933 assumes "finite I" "I \<noteq> {}" |
934 shows "sets (PiF {I} M) = |
934 shows "sets (PiF {I} M) = |
935 sigma_sets (\<Pi>' i\<in>I. space (M i)) |
935 sigma_sets (\<Pi>' i\<in>I. space (M i)) |
940 interpret R: sigma_algebra ?\<Omega> "sigma_sets ?\<Omega> ?R" by (rule sigma_algebra_sigma_sets) auto |
940 interpret R: sigma_algebra ?\<Omega> "sigma_sets ?\<Omega> ?R" by (rule sigma_algebra_sigma_sets) auto |
941 fix A assume "A \<in> {Pi' I X |X. X \<in> (\<Pi> j\<in>I. sets (M j))}" |
941 fix A assume "A \<in> {Pi' I X |X. X \<in> (\<Pi> j\<in>I. sets (M j))}" |
942 then obtain X where X: "A = Pi' I X" "X \<in> (\<Pi> j\<in>I. sets (M j))" by auto |
942 then obtain X where X: "A = Pi' I X" "X \<in> (\<Pi> j\<in>I. sets (M j))" by auto |
943 show "A \<in> sigma_sets ?\<Omega> ?R" |
943 show "A \<in> sigma_sets ?\<Omega> ?R" |
944 proof - |
944 proof - |
945 from `I \<noteq> {}` X have "A = (\<Inter>j\<in>I. {f\<in>space (PiF {I} M). f j \<in> X j})" |
945 from \<open>I \<noteq> {}\<close> X have "A = (\<Inter>j\<in>I. {f\<in>space (PiF {I} M). f j \<in> X j})" |
946 using sets.sets_into_space |
946 using sets.sets_into_space |
947 by (auto simp: space_PiF product_def) blast |
947 by (auto simp: space_PiF product_def) blast |
948 also have "\<dots> \<in> sigma_sets ?\<Omega> ?R" |
948 also have "\<dots> \<in> sigma_sets ?\<Omega> ?R" |
949 using X `I \<noteq> {}` assms by (intro R.finite_INT) (auto simp: space_PiF) |
949 using X \<open>I \<noteq> {}\<close> assms by (intro R.finite_INT) (auto simp: space_PiF) |
950 finally show "A \<in> sigma_sets ?\<Omega> ?R" . |
950 finally show "A \<in> sigma_sets ?\<Omega> ?R" . |
951 qed |
951 qed |
952 next |
952 next |
953 fix A assume "A \<in> ?R" |
953 fix A assume "A \<in> ?R" |
954 then obtain i B where A: "A = {f\<in>\<Pi>' i\<in>I. space (M i). f i \<in> B}" "i \<in> I" "B \<in> sets (M i)" |
954 then obtain i B where A: "A = {f\<in>\<Pi>' i\<in>I. space (M i). f i \<in> B}" "i \<in> I" "B \<in> sets (M i)" |
963 by (intro sigma_sets.Basic ) |
963 by (intro sigma_sets.Basic ) |
964 (auto intro: exI[where x="\<lambda>j. if j = i then B else space (M j)"]) |
964 (auto intro: exI[where x="\<lambda>j. if j = i then B else space (M j)"]) |
965 finally show "A \<in> sigma_sets ?\<Omega> {Pi' I X |X. X \<in> (\<Pi> j\<in>I. sets (M j))}" . |
965 finally show "A \<in> sigma_sets ?\<Omega> {Pi' I X |X. X \<in> (\<Pi> j\<in>I. sets (M j))}" . |
966 qed |
966 qed |
967 |
967 |
968 text {* adapted from @{thm PiE_cong} *} |
968 text \<open>adapted from @{thm PiE_cong}\<close> |
969 |
969 |
970 lemma Pi'_cong: |
970 lemma Pi'_cong: |
971 assumes "finite I" |
971 assumes "finite I" |
972 assumes "\<And>i. i \<in> I \<Longrightarrow> f i = g i" |
972 assumes "\<And>i. i \<in> I \<Longrightarrow> f i = g i" |
973 shows "Pi' I f = Pi' I g" |
973 shows "Pi' I f = Pi' I g" |
974 using assms by (auto simp: Pi'_def) |
974 using assms by (auto simp: Pi'_def) |
975 |
975 |
976 text {* adapted from @{thm Pi_UN} *} |
976 text \<open>adapted from @{thm Pi_UN}\<close> |
977 |
977 |
978 lemma Pi'_UN: |
978 lemma Pi'_UN: |
979 fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set" |
979 fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set" |
980 assumes "finite I" |
980 assumes "finite I" |
981 assumes mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i" |
981 assumes mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i" |
982 shows "(\<Union>n. Pi' I (A n)) = Pi' I (\<lambda>i. \<Union>n. A n i)" |
982 shows "(\<Union>n. Pi' I (A n)) = Pi' I (\<lambda>i. \<Union>n. A n i)" |
983 proof (intro set_eqI iffI) |
983 proof (intro set_eqI iffI) |
984 fix f assume "f \<in> Pi' I (\<lambda>i. \<Union>n. A n i)" |
984 fix f assume "f \<in> Pi' I (\<lambda>i. \<Union>n. A n i)" |
985 then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" "domain f = I" by (auto simp: `finite I` Pi'_def) |
985 then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" "domain f = I" by (auto simp: \<open>finite I\<close> Pi'_def) |
986 from bchoice[OF this(1)] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto |
986 from bchoice[OF this(1)] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto |
987 obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k" |
987 obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k" |
988 using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto |
988 using \<open>finite I\<close> finite_nat_set_iff_bounded_le[of "n`I"] by auto |
989 have "f \<in> Pi' I (\<lambda>i. A k i)" |
989 have "f \<in> Pi' I (\<lambda>i. A k i)" |
990 proof |
990 proof |
991 fix i assume "i \<in> I" |
991 fix i assume "i \<in> I" |
992 from mono[OF this, of "n i" k] k[OF this] n[OF this] `domain f = I` `i \<in> I` |
992 from mono[OF this, of "n i" k] k[OF this] n[OF this] \<open>domain f = I\<close> \<open>i \<in> I\<close> |
993 show "f i \<in> A k i " by (auto simp: `finite I`) |
993 show "f i \<in> A k i " by (auto simp: \<open>finite I\<close>) |
994 qed (simp add: `domain f = I` `finite I`) |
994 qed (simp add: \<open>domain f = I\<close> \<open>finite I\<close>) |
995 then show "f \<in> (\<Union>n. Pi' I (A n))" by auto |
995 then show "f \<in> (\<Union>n. Pi' I (A n))" by auto |
996 qed (auto simp: Pi'_def `finite I`) |
996 qed (auto simp: Pi'_def \<open>finite I\<close>) |
997 |
997 |
998 text {* adapted from @{thm sets_PiM_sigma} *} |
998 text \<open>adapted from @{thm sets_PiM_sigma}\<close> |
999 |
999 |
1000 lemma sigma_fprod_algebra_sigma_eq: |
1000 lemma sigma_fprod_algebra_sigma_eq: |
1001 fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" |
1001 fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" |
1002 assumes [simp]: "finite I" "I \<noteq> {}" |
1002 assumes [simp]: "finite I" "I \<noteq> {}" |
1003 and S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)" |
1003 and S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)" |
1006 and E_generates: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sigma_sets (space (M i)) (E i)" |
1006 and E_generates: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sigma_sets (space (M i)) (E i)" |
1007 defines "P == { Pi' I F | F. \<forall>i\<in>I. F i \<in> E i }" |
1007 defines "P == { Pi' I F | F. \<forall>i\<in>I. F i \<in> E i }" |
1008 shows "sets (PiF {I} M) = sigma_sets (space (PiF {I} M)) P" |
1008 shows "sets (PiF {I} M) = sigma_sets (space (PiF {I} M)) P" |
1009 proof |
1009 proof |
1010 let ?P = "sigma (space (Pi\<^sub>F {I} M)) P" |
1010 let ?P = "sigma (space (Pi\<^sub>F {I} M)) P" |
1011 from `finite I`[THEN ex_bij_betw_finite_nat] guess T .. |
1011 from \<open>finite I\<close>[THEN ex_bij_betw_finite_nat] guess T .. |
1012 then have T: "\<And>i. i \<in> I \<Longrightarrow> T i < card I" "\<And>i. i\<in>I \<Longrightarrow> the_inv_into I T (T i) = i" |
1012 then have T: "\<And>i. i \<in> I \<Longrightarrow> T i < card I" "\<And>i. i\<in>I \<Longrightarrow> the_inv_into I T (T i) = i" |
1013 by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f simp del: `finite I`) |
1013 by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f simp del: \<open>finite I\<close>) |
1014 have P_closed: "P \<subseteq> Pow (space (Pi\<^sub>F {I} M))" |
1014 have P_closed: "P \<subseteq> Pow (space (Pi\<^sub>F {I} M))" |
1015 using E_closed by (auto simp: space_PiF P_def Pi'_iff subset_eq) |
1015 using E_closed by (auto simp: space_PiF P_def Pi'_iff subset_eq) |
1016 then have space_P: "space ?P = (\<Pi>' i\<in>I. space (M i))" |
1016 then have space_P: "space ?P = (\<Pi>' i\<in>I. space (M i))" |
1017 by (simp add: space_PiF) |
1017 by (simp add: space_PiF) |
1018 have "sets (PiF {I} M) = |
1018 have "sets (PiF {I} M) = |
1021 also have "\<dots> \<subseteq> sets (sigma (space (PiF {I} M)) P)" |
1021 also have "\<dots> \<subseteq> sets (sigma (space (PiF {I} M)) P)" |
1022 proof (safe intro!: sets.sigma_sets_subset) |
1022 proof (safe intro!: sets.sigma_sets_subset) |
1023 fix i A assume "i \<in> I" and A: "A \<in> sets (M i)" |
1023 fix i A assume "i \<in> I" and A: "A \<in> sets (M i)" |
1024 have "(\<lambda>x. (x)\<^sub>F i) \<in> measurable ?P (sigma (space (M i)) (E i))" |
1024 have "(\<lambda>x. (x)\<^sub>F i) \<in> measurable ?P (sigma (space (M i)) (E i))" |
1025 proof (subst measurable_iff_measure_of) |
1025 proof (subst measurable_iff_measure_of) |
1026 show "E i \<subseteq> Pow (space (M i))" using `i \<in> I` by fact |
1026 show "E i \<subseteq> Pow (space (M i))" using \<open>i \<in> I\<close> by fact |
1027 from space_P `i \<in> I` show "(\<lambda>x. (x)\<^sub>F i) \<in> space ?P \<rightarrow> space (M i)" |
1027 from space_P \<open>i \<in> I\<close> show "(\<lambda>x. (x)\<^sub>F i) \<in> space ?P \<rightarrow> space (M i)" |
1028 by auto |
1028 by auto |
1029 show "\<forall>A\<in>E i. (\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P \<in> sets ?P" |
1029 show "\<forall>A\<in>E i. (\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P \<in> sets ?P" |
1030 proof |
1030 proof |
1031 fix A assume A: "A \<in> E i" |
1031 fix A assume A: "A \<in> E i" |
1032 then have "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P = (\<Pi>' j\<in>I. if i = j then A else space (M j))" |
1032 then have "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P = (\<Pi>' j\<in>I. if i = j then A else space (M j))" |
1033 using E_closed `i \<in> I` by (auto simp: space_P Pi_iff subset_eq split: split_if_asm) |
1033 using E_closed \<open>i \<in> I\<close> by (auto simp: space_P Pi_iff subset_eq split: split_if_asm) |
1034 also have "\<dots> = (\<Pi>' j\<in>I. \<Union>n. if i = j then A else S j n)" |
1034 also have "\<dots> = (\<Pi>' j\<in>I. \<Union>n. if i = j then A else S j n)" |
1035 by (intro Pi'_cong) (simp_all add: S_union) |
1035 by (intro Pi'_cong) (simp_all add: S_union) |
1036 also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>' j\<in>I. if i = j then A else S j (xs ! T j))" |
1036 also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>' j\<in>I. if i = j then A else S j (xs ! T j))" |
1037 using T |
1037 using T |
1038 apply auto |
1038 apply auto |
1050 qed |
1050 qed |
1051 finally show "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P \<in> sets ?P" |
1051 finally show "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P \<in> sets ?P" |
1052 using P_closed by simp |
1052 using P_closed by simp |
1053 qed |
1053 qed |
1054 qed |
1054 qed |
1055 from measurable_sets[OF this, of A] A `i \<in> I` E_closed |
1055 from measurable_sets[OF this, of A] A \<open>i \<in> I\<close> E_closed |
1056 have "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P \<in> sets ?P" |
1056 have "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P \<in> sets ?P" |
1057 by (simp add: E_generates) |
1057 by (simp add: E_generates) |
1058 also have "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P = {f \<in> \<Pi>' i\<in>I. space (M i). f i \<in> A}" |
1058 also have "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P = {f \<in> \<Pi>' i\<in>I. space (M i). f i \<in> A}" |
1059 using P_closed by (auto simp: space_PiF) |
1059 using P_closed by (auto simp: space_PiF) |
1060 finally show "\<dots> \<in> sets ?P" . |
1060 finally show "\<dots> \<in> sets ?P" . |
1061 qed |
1061 qed |
1062 finally show "sets (PiF {I} M) \<subseteq> sigma_sets (space (PiF {I} M)) P" |
1062 finally show "sets (PiF {I} M) \<subseteq> sigma_sets (space (PiF {I} M)) P" |
1063 by (simp add: P_closed) |
1063 by (simp add: P_closed) |
1064 show "sigma_sets (space (PiF {I} M)) P \<subseteq> sets (PiF {I} M)" |
1064 show "sigma_sets (space (PiF {I} M)) P \<subseteq> sets (PiF {I} M)" |
1065 using `finite I` `I \<noteq> {}` |
1065 using \<open>finite I\<close> \<open>I \<noteq> {}\<close> |
1066 by (auto intro!: sets.sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def) |
1066 by (auto intro!: sets.sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def) |
1067 qed |
1067 qed |
1068 |
1068 |
1069 lemma product_open_generates_sets_PiF_single: |
1069 lemma product_open_generates_sets_PiF_single: |
1070 assumes "I \<noteq> {}" |
1070 assumes "I \<noteq> {}" |
1103 proof (rule measure_eqI, clarsimp, rule sigma_sets_eqI) |
1103 proof (rule measure_eqI, clarsimp, rule sigma_sets_eqI) |
1104 fix a::"('i \<Rightarrow>\<^sub>F 'a) set" assume "a \<in> Collect open" hence "open a" by simp |
1104 fix a::"('i \<Rightarrow>\<^sub>F 'a) set" assume "a \<in> Collect open" hence "open a" by simp |
1105 then obtain B' where B': "B'\<subseteq>basis_finmap" "a = \<Union>B'" |
1105 then obtain B' where B': "B'\<subseteq>basis_finmap" "a = \<Union>B'" |
1106 using finmap_topological_basis by (force simp add: topological_basis_def) |
1106 using finmap_topological_basis by (force simp add: topological_basis_def) |
1107 have "a \<in> sigma UNIV {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}" |
1107 have "a \<in> sigma UNIV {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}" |
1108 unfolding `a = \<Union>B'` |
1108 unfolding \<open>a = \<Union>B'\<close> |
1109 proof (rule sets.countable_Union) |
1109 proof (rule sets.countable_Union) |
1110 from B' countable_basis_finmap show "countable B'" by (metis countable_subset) |
1110 from B' countable_basis_finmap show "countable B'" by (metis countable_subset) |
1111 next |
1111 next |
1112 show "B' \<subseteq> sets (sigma UNIV |
1112 show "B' \<subseteq> sets (sigma UNIV |
1113 {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)})" (is "_ \<subseteq> sets ?s") |
1113 {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)})" (is "_ \<subseteq> sets ?s") |
1132 { assume ef: "J = {}" |
1132 { assume ef: "J = {}" |
1133 have "?b J \<in> sets borel" |
1133 have "?b J \<in> sets borel" |
1134 proof cases |
1134 proof cases |
1135 assume "?b J \<noteq> {}" |
1135 assume "?b J \<noteq> {}" |
1136 then obtain f where "f \<in> b" "domain f = {}" using ef by auto |
1136 then obtain f where "f \<in> b" "domain f = {}" using ef by auto |
1137 hence "?b J = {f}" using `J = {}` |
1137 hence "?b J = {f}" using \<open>J = {}\<close> |
1138 by (auto simp: finmap_eq_iff) |
1138 by (auto simp: finmap_eq_iff) |
1139 also have "{f} \<in> sets borel" by simp |
1139 also have "{f} \<in> sets borel" by simp |
1140 finally show ?thesis . |
1140 finally show ?thesis . |
1141 qed simp |
1141 qed simp |
1142 } moreover { |
1142 } moreover { |
1143 assume "J \<noteq> ({}::'i set)" |
1143 assume "J \<noteq> ({}::'i set)" |
1144 have "(?b J) = b \<inter> {m. domain m \<in> {J}}" by auto |
1144 have "(?b J) = b \<inter> {m. domain m \<in> {J}}" by auto |
1145 also have "\<dots> \<in> sets (PiF {J} (\<lambda>_. borel))" |
1145 also have "\<dots> \<in> sets (PiF {J} (\<lambda>_. borel))" |
1146 using b' by (rule restrict_sets_measurable) (auto simp: `finite J`) |
1146 using b' by (rule restrict_sets_measurable) (auto simp: \<open>finite J\<close>) |
1147 also have "\<dots> = sigma_sets (space (PiF {J} (\<lambda>_. borel))) |
1147 also have "\<dots> = sigma_sets (space (PiF {J} (\<lambda>_. borel))) |
1148 {Pi' (J) F |F. (\<forall>j\<in>J. F j \<in> Collect open)}" |
1148 {Pi' (J) F |F. (\<forall>j\<in>J. F j \<in> Collect open)}" |
1149 (is "_ = sigma_sets _ ?P") |
1149 (is "_ = sigma_sets _ ?P") |
1150 by (rule product_open_generates_sets_PiF_single[OF `J \<noteq> {}` `finite J`]) |
1150 by (rule product_open_generates_sets_PiF_single[OF \<open>J \<noteq> {}\<close> \<open>finite J\<close>]) |
1151 also have "\<dots> \<subseteq> sigma_sets UNIV (Collect open)" |
1151 also have "\<dots> \<subseteq> sigma_sets UNIV (Collect open)" |
1152 by (intro sigma_sets_mono'') (auto intro!: open_Pi'I simp: space_PiF) |
1152 by (intro sigma_sets_mono'') (auto intro!: open_Pi'I simp: space_PiF) |
1153 finally have "(?b J) \<in> sets borel" by (simp add: borel_def) |
1153 finally have "(?b J) \<in> sets borel" by (simp add: borel_def) |
1154 } ultimately show "(?b J) \<in> sets borel" by blast |
1154 } ultimately show "(?b J) \<in> sets borel" by blast |
1155 qed (simp add: countable_Collect_finite) |
1155 qed (simp add: countable_Collect_finite) |
1156 finally show "b \<in> sigma_sets UNIV (Collect open)" by (simp add: borel_def) |
1156 finally show "b \<in> sigma_sets UNIV (Collect open)" by (simp add: borel_def) |
1157 qed (simp add: emeasure_sigma borel_def PiF_def) |
1157 qed (simp add: emeasure_sigma borel_def PiF_def) |
1158 |
1158 |
1159 subsection {* Isomorphism between Functions and Finite Maps *} |
1159 subsection \<open>Isomorphism between Functions and Finite Maps\<close> |
1160 |
1160 |
1161 lemma measurable_finmap_compose: |
1161 lemma measurable_finmap_compose: |
1162 shows "(\<lambda>m. compose J m f) \<in> measurable (PiM (f ` J) (\<lambda>_. M)) (PiM J (\<lambda>_. M))" |
1162 shows "(\<lambda>m. compose J m f) \<in> measurable (PiM (f ` J) (\<lambda>_. M)) (PiM J (\<lambda>_. M))" |
1163 unfolding compose_def by measurable |
1163 unfolding compose_def by measurable |
1164 |
1164 |
1171 fixes J::"'a set" and f :: "'a \<Rightarrow> 'b::countable" and f' |
1171 fixes J::"'a set" and f :: "'a \<Rightarrow> 'b::countable" and f' |
1172 assumes [simp]: "finite J" |
1172 assumes [simp]: "finite J" |
1173 assumes inv: "i \<in> J \<Longrightarrow> f' (f i) = i" |
1173 assumes inv: "i \<in> J \<Longrightarrow> f' (f i) = i" |
1174 begin |
1174 begin |
1175 |
1175 |
1176 text {* to measure finmaps *} |
1176 text \<open>to measure finmaps\<close> |
1177 |
1177 |
1178 definition "fm = (finmap_of (f ` J)) o (\<lambda>g. compose (f ` J) g f')" |
1178 definition "fm = (finmap_of (f ` J)) o (\<lambda>g. compose (f ` J) g f')" |
1179 |
1179 |
1180 lemma domain_fm[simp]: "domain (fm x) = f ` J" |
1180 lemma domain_fm[simp]: "domain (fm x) = f ` J" |
1181 unfolding fm_def by simp |
1181 unfolding fm_def by simp |
1282 assumes "X \<in> sets (Pi\<^sub>M J (\<lambda>_. M::'c measure))" |
1282 assumes "X \<in> sets (Pi\<^sub>M J (\<lambda>_. M::'c measure))" |
1283 shows "fm ` X \<in> sets (PiF (Collect finite) (\<lambda>_. M::'c measure))" |
1283 shows "fm ` X \<in> sets (PiF (Collect finite) (\<lambda>_. M::'c measure))" |
1284 using fm_image_measurable[OF assms] |
1284 using fm_image_measurable[OF assms] |
1285 by (rule subspace_set_in_sets) (auto simp: finite_subset) |
1285 by (rule subspace_set_in_sets) (auto simp: finite_subset) |
1286 |
1286 |
1287 text {* measure on finmaps *} |
1287 text \<open>measure on finmaps\<close> |
1288 |
1288 |
1289 definition "mapmeasure M N = distr M (PiF (Collect finite) N) (fm)" |
1289 definition "mapmeasure M N = distr M (PiF (Collect finite) N) (fm)" |
1290 |
1290 |
1291 lemma sets_mapmeasure[simp]: "sets (mapmeasure M N) = sets (PiF (Collect finite) N)" |
1291 lemma sets_mapmeasure[simp]: "sets (mapmeasure M N) = sets (PiF (Collect finite) N)" |
1292 unfolding mapmeasure_def by simp |
1292 unfolding mapmeasure_def by simp |