1(* Author: Johannes H��lzl <hoelzl@in.tum.de> *) 2 3section \<open>The Category of Measurable Spaces is not Cartesian Closed\<close> 4 5theory Measure_Not_CCC 6 imports "HOL-Probability.Probability" 7begin 8 9text \<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>\<open>\<lambda>x y. x = y\<close> is $\mathbb{R}$-$\mathbb{B}^\mathbb{C}$-measurable, 20 but \<^term>\<open>\<lambda>(x, y). x = y\<close> is not $(\mathbb{R} \times \mathbb{C})$-$\mathbb{B}$-measurable. 21\<close> 22 23definition COCOUNT :: "real measure" where 24 "COCOUNT = sigma UNIV {{x} | x. True}" 25 26abbreviation POW :: "real measure" where 27 "POW \<equiv> count_space UNIV" 28 29abbreviation BOOL :: "bool measure" where 30 "BOOL \<equiv> count_space UNIV" 31 32lemma 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 35lemma measurable_eq[measurable]: "((=) x) \<in> measurable COCOUNT BOOL" 36 unfolding pred_def by (auto simp: COCOUNT_def) 37 38lemma COCOUNT_eq: "A \<in> COCOUNT \<longleftrightarrow> countable A \<or> countable (UNIV - A)" 39proof 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) 53next 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 71qed 72 73lemma 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 77proof 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 89next 90 case Empty then show ?case 91 by (intro exI[of _ "{}"] exI[of _ "\<lambda>_. {}"] exI[of _ "{}"]) auto 92next 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 102next 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 define G where "G j = (\<Union>i. if j \<in> J i then F i j else X i)" for j 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>(A ` UNIV) = (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: if_split_asm) 114 qed 115qed 116 117context 118 fixes EXP :: "(real \<Rightarrow> bool) measure" 119 assumes eq: "\<And>P. case_prod P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP" 120begin 121 122lemma space_EXP: "space EXP = measurable COCOUNT BOOL" 123proof - 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 131qed 132 133lemma measurable_eq_EXP: "(\<lambda>x y. x = y) \<in> measurable POW EXP" 134 unfolding measurable_def by (auto simp: space_EXP) 135 136lemma 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 140lemma ce: False 141proof - 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 \<open>countable J\<close> 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 163qed 164 165end 166 167corollary "\<not> (\<exists>EXP. \<forall>P. case_prod P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP)" 168 using ce by blast 169 170end 171 172