|
1 (* Author: Johannes Hölzl <hoelzl@in.tum.de> *) |
|
2 |
|
3 section \<open>The Category of Measurable Spaces is not Cartesian Closed\<close> |
|
4 |
|
5 theory Measure_Not_CCC |
|
6 imports "~~/src/HOL/Probability/Probability" "~~/src/HOL/Library/ContNotDenum" |
|
7 begin |
|
8 |
|
9 text \<open> |
|
10 We show that the category of measurable spaces with measurable functions as morphisms is not a |
|
11 Cartesian closed category. While the category has products and terminal objects, the exponential |
|
12 does not exist for each pair of measurable spaces. |
|
13 |
|
14 We show that the exponential $\mathbb{B}^\mathbb{C}$ does not exist, where $\mathbb{B}$ is the |
|
15 discrete measurable space on boolean values, and $\mathbb{C}$ is the $\sigma$-algebra consisting |
|
16 of all countable and co-countable real sets. We also define $\mathbb{R}$ to be the discrete |
|
17 measurable space on the reals. |
|
18 |
|
19 Now, the diagonal predicate @{term "\<lambda>x y. x = y"} is $\mathbb{R}$-$\mathbb{B}^\mathbb{C}$-measurable, |
|
20 but @{term "\<lambda>(x, y). x = y"} is not $(\mathbb{R} \times \mathbb{C})$-$\mathbb{B}$-measurable. |
|
21 \<close> |
|
22 |
|
23 definition COCOUNT :: "real measure" where |
|
24 "COCOUNT = sigma UNIV {{x} | x. True}" |
|
25 |
|
26 abbreviation POW :: "real measure" where |
|
27 "POW \<equiv> count_space UNIV" |
|
28 |
|
29 abbreviation BOOL :: "bool measure" where |
|
30 "BOOL \<equiv> count_space UNIV" |
|
31 |
|
32 lemma measurable_const_iff: "(\<lambda>x. c) \<in> measurable A B \<longleftrightarrow> (space A = {} \<or> c \<in> space B)" |
|
33 by (auto simp: measurable_def) |
|
34 |
|
35 lemma measurable_eq[measurable]: "(op = x) \<in> measurable COCOUNT BOOL" |
|
36 unfolding pred_def by (auto simp: COCOUNT_def) |
|
37 |
|
38 lemma COCOUNT_eq: "A \<in> COCOUNT \<longleftrightarrow> countable A \<or> countable (UNIV - A)" |
|
39 proof |
|
40 fix A assume "A \<in> COCOUNT" |
|
41 then have "A \<in> sigma_sets UNIV {{x} | x. True}" |
|
42 by (auto simp: COCOUNT_def) |
|
43 then show "countable A \<or> countable (UNIV - A)" |
|
44 proof induction |
|
45 case (Union F) |
|
46 moreover |
|
47 { fix i assume "countable (UNIV - F i)" |
|
48 then have "countable (UNIV - (\<Union>i. F i))" |
|
49 by (rule countable_subset[rotated]) auto } |
|
50 ultimately show "countable (\<Union>i. F i) \<or> countable (UNIV - (\<Union>i. F i))" |
|
51 by blast |
|
52 qed (auto simp: Diff_Diff_Int) |
|
53 next |
|
54 assume "countable A \<or> countable (UNIV - A)" |
|
55 moreover |
|
56 { fix A :: "real set" assume A: "countable A" |
|
57 have "A = (\<Union>a\<in>A. {a})" |
|
58 by auto |
|
59 also have "\<dots> \<in> COCOUNT" |
|
60 by (intro sets.countable_UN' A) (auto simp: COCOUNT_def) |
|
61 finally have "A \<in> COCOUNT" . } |
|
62 note A = this |
|
63 note A[of A] |
|
64 moreover |
|
65 { assume "countable (UNIV - A)" |
|
66 with A have "space COCOUNT - (UNIV - A) \<in> COCOUNT" by simp |
|
67 then have "A \<in> COCOUNT" |
|
68 by (auto simp: COCOUNT_def Diff_Diff_Int) } |
|
69 ultimately show "A \<in> COCOUNT" |
|
70 by blast |
|
71 qed |
|
72 |
|
73 lemma pair_COCOUNT: |
|
74 assumes A: "A \<in> sets (COCOUNT \<Otimes>\<^sub>M M)" |
|
75 shows "\<exists>J F X. X \<in> sets M \<and> F \<in> J \<rightarrow> sets M \<and> countable J \<and> A = (UNIV - J) \<times> X \<union> (SIGMA j:J. F j)" |
|
76 using A unfolding sets_pair_measure |
|
77 proof induction |
|
78 case (Basic X) |
|
79 then obtain a b where X: "X = a \<times> b" and b: "b \<in> sets M" and a: "countable a \<or> countable (UNIV - a)" |
|
80 by (auto simp: COCOUNT_eq) |
|
81 from a show ?case |
|
82 proof |
|
83 assume "countable a" with X b show ?thesis |
|
84 by (intro exI[of _ a] exI[of _ "\<lambda>_. b"] exI[of _ "{}"]) auto |
|
85 next |
|
86 assume "countable (UNIV - a)" with X b show ?thesis |
|
87 by (intro exI[of _ "UNIV - a"] exI[of _ "\<lambda>_. {}"] exI[of _ "b"]) auto |
|
88 qed |
|
89 next |
|
90 case Empty then show ?case |
|
91 by (intro exI[of _ "{}"] exI[of _ "\<lambda>_. {}"] exI[of _ "{}"]) auto |
|
92 next |
|
93 case (Compl A) |
|
94 then obtain J F X where XFJ: "X \<in> sets M" "F \<in> J \<rightarrow> sets M" "countable J" |
|
95 and A: "A = (UNIV - J) \<times> X \<union> Sigma J F" |
|
96 by auto |
|
97 have *: "space COCOUNT \<times> space M - A = (UNIV - J) \<times> (space M - X) \<union> (SIGMA j:J. space M - F j)" |
|
98 unfolding A by (auto simp: COCOUNT_def) |
|
99 show ?case |
|
100 using XFJ unfolding * |
|
101 by (intro exI[of _ J] exI[of _ "space M - X"] exI[of _ "\<lambda>j. space M - F j"]) auto |
|
102 next |
|
103 case (Union A) |
|
104 obtain J F X where XFJ: "\<And>i. X i \<in> sets M" "\<And>i. F i \<in> J i \<rightarrow> sets M" "\<And>i. countable (J i)" |
|
105 and A_eq: "A = (\<lambda>i. (UNIV - J i) \<times> X i \<union> Sigma (J i) (F i))" |
|
106 unfolding fun_eq_iff using Union.IH by metis |
|
107 show ?case |
|
108 proof (intro exI conjI) |
|
109 def G \<equiv> "\<lambda>j. (\<Union>i. if j \<in> J i then F i j else X i)" |
|
110 show "(\<Union>i. X i) \<in> sets M" "countable (\<Union>i. J i)" "G \<in> (\<Union>i. J i) \<rightarrow> sets M" |
|
111 using XFJ by (auto simp: G_def Pi_iff) |
|
112 show "UNION UNIV A = (UNIV - (\<Union>i. J i)) \<times> (\<Union>i. X i) \<union> (SIGMA j:\<Union>i. J i. \<Union>i. if j \<in> J i then F i j else X i)" |
|
113 unfolding A_eq by (auto split: split_if_asm) |
|
114 qed |
|
115 qed |
|
116 |
|
117 context |
|
118 fixes EXP :: "(real \<Rightarrow> bool) measure" |
|
119 assumes eq: "\<And>P. split P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP" |
|
120 begin |
|
121 |
|
122 lemma space_EXP: "space EXP = measurable COCOUNT BOOL" |
|
123 proof - |
|
124 { fix f |
|
125 have "f \<in> space EXP \<longleftrightarrow> (\<lambda>(a, b). f b) \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL" |
|
126 using eq[of "\<lambda>x. f"] by (simp add: measurable_const_iff) |
|
127 also have "\<dots> \<longleftrightarrow> f \<in> measurable COCOUNT BOOL" |
|
128 by auto |
|
129 finally have "f \<in> space EXP \<longleftrightarrow> f \<in> measurable COCOUNT BOOL" . } |
|
130 then show ?thesis by auto |
|
131 qed |
|
132 |
|
133 lemma measurable_eq_EXP: "(\<lambda>x y. x = y) \<in> measurable POW EXP" |
|
134 unfolding measurable_def by (auto simp: space_EXP) |
|
135 |
|
136 lemma measurable_eq_pair: "(\<lambda>(y, x). x = y) \<in> measurable (COCOUNT \<Otimes>\<^sub>M POW) BOOL" |
|
137 using measurable_eq_EXP unfolding eq[symmetric] |
|
138 by (subst measurable_pair_swap_iff) simp |
|
139 |
|
140 lemma ce: False |
|
141 proof - |
|
142 have "{(y, x) \<in> space (COCOUNT \<Otimes>\<^sub>M POW). x = y} \<in> sets (COCOUNT \<Otimes>\<^sub>M POW)" |
|
143 using measurable_eq_pair unfolding pred_def by (simp add: split_beta') |
|
144 also have "{(y, x) \<in> space (COCOUNT \<Otimes>\<^sub>M POW). x = y} = (SIGMA j:UNIV. {j})" |
|
145 by (auto simp: space_pair_measure COCOUNT_def) |
|
146 finally obtain X F J where "countable (J::real set)" |
|
147 and eq: "(SIGMA j:UNIV. {j}) = (UNIV - J) \<times> X \<union> (SIGMA j:J. F j)" |
|
148 using pair_COCOUNT[of "SIGMA j:UNIV. {j}" POW] by auto |
|
149 have X_single: "\<And>x. x \<notin> J \<Longrightarrow> X = {x}" |
|
150 using eq[unfolded set_eq_iff] by force |
|
151 |
|
152 have "uncountable (UNIV - J)" |
|
153 using `countable J` uncountable_UNIV_real uncountable_minus_countable by blast |
|
154 then have "infinite (UNIV - J)" |
|
155 by (auto intro: countable_finite) |
|
156 then have "\<exists>A. finite A \<and> card A = 2 \<and> A \<subseteq> UNIV - J" |
|
157 by (rule infinite_arbitrarily_large) |
|
158 then obtain i j where ij: "i \<in> UNIV - J" "j \<in> UNIV - J" "i \<noteq> j" |
|
159 by (auto simp add: card_Suc_eq numeral_2_eq_2) |
|
160 have "{(i, i), (j, j)} \<subseteq> (SIGMA j:UNIV. {j})" by auto |
|
161 with ij X_single[of i] X_single[of j] show False |
|
162 by auto |
|
163 qed |
|
164 |
|
165 end |
|
166 |
|
167 corollary "\<not> (\<exists>EXP. \<forall>P. split P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP)" |
|
168 using ce by blast |
|
169 |
|
170 end |
|
171 |