author | hoelzl |

Wed Dec 17 16:10:30 2014 +0100 (2014-12-17) | |

changeset 59144 | c9b75c03de3c |

parent 59143 | 15c342a9a8e0 |

child 59145 | 0e304b1568a5 |

unfortunately, there is no general function space in the measurable spaces

src/HOL/Probability/document/root.tex | file | annotate | diff | revisions | |

src/HOL/Probability/ex/Measure_Not_CCC.thy | file | annotate | diff | revisions | |

src/HOL/ROOT | file | annotate | diff | revisions |

1.1 --- a/src/HOL/Probability/document/root.tex Mon Dec 15 07:20:49 2014 +0100 1.2 +++ b/src/HOL/Probability/document/root.tex Wed Dec 17 16:10:30 2014 +0100 1.3 @@ -3,6 +3,7 @@ 1.4 1.5 \documentclass[11pt,a4paper]{article} 1.6 \usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp} 1.7 +\usepackage{amssymb} 1.8 \usepackage[only,bigsqcap]{stmaryrd} 1.9 \usepackage[utf8]{inputenc} 1.10 \usepackage{pdfsetup}

2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 2.2 +++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy Wed Dec 17 16:10:30 2014 +0100 2.3 @@ -0,0 +1,171 @@ 2.4 +(* Author: Johannes Hölzl <hoelzl@in.tum.de> *) 2.5 + 2.6 +section \<open>The Category of Measurable Spaces is not Cartesian Closed\<close> 2.7 + 2.8 +theory Measure_Not_CCC 2.9 + imports "~~/src/HOL/Probability/Probability" "~~/src/HOL/Library/ContNotDenum" 2.10 +begin 2.11 + 2.12 +text \<open> 2.13 + We show that the category of measurable spaces with measurable functions as morphisms is not a 2.14 + Cartesian closed category. While the category has products and terminal objects, the exponential 2.15 + does not exist for each pair of measurable spaces. 2.16 + 2.17 + We show that the exponential $\mathbb{B}^\mathbb{C}$ does not exist, where $\mathbb{B}$ is the 2.18 + discrete measurable space on boolean values, and $\mathbb{C}$ is the $\sigma$-algebra consisting 2.19 + of all countable and co-countable real sets. We also define $\mathbb{R}$ to be the discrete 2.20 + measurable space on the reals. 2.21 + 2.22 + Now, the diagonal predicate @{term "\<lambda>x y. x = y"} is $\mathbb{R}$-$\mathbb{B}^\mathbb{C}$-measurable, 2.23 + but @{term "\<lambda>(x, y). x = y"} is not $(\mathbb{R} \times \mathbb{C})$-$\mathbb{B}$-measurable. 2.24 +\<close> 2.25 + 2.26 +definition COCOUNT :: "real measure" where 2.27 + "COCOUNT = sigma UNIV {{x} | x. True}" 2.28 + 2.29 +abbreviation POW :: "real measure" where 2.30 + "POW \<equiv> count_space UNIV" 2.31 + 2.32 +abbreviation BOOL :: "bool measure" where 2.33 + "BOOL \<equiv> count_space UNIV" 2.34 + 2.35 +lemma measurable_const_iff: "(\<lambda>x. c) \<in> measurable A B \<longleftrightarrow> (space A = {} \<or> c \<in> space B)" 2.36 + by (auto simp: measurable_def) 2.37 + 2.38 +lemma measurable_eq[measurable]: "(op = x) \<in> measurable COCOUNT BOOL" 2.39 + unfolding pred_def by (auto simp: COCOUNT_def) 2.40 + 2.41 +lemma COCOUNT_eq: "A \<in> COCOUNT \<longleftrightarrow> countable A \<or> countable (UNIV - A)" 2.42 +proof 2.43 + fix A assume "A \<in> COCOUNT" 2.44 + then have "A \<in> sigma_sets UNIV {{x} | x. True}" 2.45 + by (auto simp: COCOUNT_def) 2.46 + then show "countable A \<or> countable (UNIV - A)" 2.47 + proof induction 2.48 + case (Union F) 2.49 + moreover 2.50 + { fix i assume "countable (UNIV - F i)" 2.51 + then have "countable (UNIV - (\<Union>i. F i))" 2.52 + by (rule countable_subset[rotated]) auto } 2.53 + ultimately show "countable (\<Union>i. F i) \<or> countable (UNIV - (\<Union>i. F i))" 2.54 + by blast 2.55 + qed (auto simp: Diff_Diff_Int) 2.56 +next 2.57 + assume "countable A \<or> countable (UNIV - A)" 2.58 + moreover 2.59 + { fix A :: "real set" assume A: "countable A" 2.60 + have "A = (\<Union>a\<in>A. {a})" 2.61 + by auto 2.62 + also have "\<dots> \<in> COCOUNT" 2.63 + by (intro sets.countable_UN' A) (auto simp: COCOUNT_def) 2.64 + finally have "A \<in> COCOUNT" . } 2.65 + note A = this 2.66 + note A[of A] 2.67 + moreover 2.68 + { assume "countable (UNIV - A)" 2.69 + with A have "space COCOUNT - (UNIV - A) \<in> COCOUNT" by simp 2.70 + then have "A \<in> COCOUNT" 2.71 + by (auto simp: COCOUNT_def Diff_Diff_Int) } 2.72 + ultimately show "A \<in> COCOUNT" 2.73 + by blast 2.74 +qed 2.75 + 2.76 +lemma pair_COCOUNT: 2.77 + assumes A: "A \<in> sets (COCOUNT \<Otimes>\<^sub>M M)" 2.78 + 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)" 2.79 + using A unfolding sets_pair_measure 2.80 +proof induction 2.81 + case (Basic X) 2.82 + then obtain a b where X: "X = a \<times> b" and b: "b \<in> sets M" and a: "countable a \<or> countable (UNIV - a)" 2.83 + by (auto simp: COCOUNT_eq) 2.84 + from a show ?case 2.85 + proof 2.86 + assume "countable a" with X b show ?thesis 2.87 + by (intro exI[of _ a] exI[of _ "\<lambda>_. b"] exI[of _ "{}"]) auto 2.88 + next 2.89 + assume "countable (UNIV - a)" with X b show ?thesis 2.90 + by (intro exI[of _ "UNIV - a"] exI[of _ "\<lambda>_. {}"] exI[of _ "b"]) auto 2.91 + qed 2.92 +next 2.93 + case Empty then show ?case 2.94 + by (intro exI[of _ "{}"] exI[of _ "\<lambda>_. {}"] exI[of _ "{}"]) auto 2.95 +next 2.96 + case (Compl A) 2.97 + then obtain J F X where XFJ: "X \<in> sets M" "F \<in> J \<rightarrow> sets M" "countable J" 2.98 + and A: "A = (UNIV - J) \<times> X \<union> Sigma J F" 2.99 + by auto 2.100 + have *: "space COCOUNT \<times> space M - A = (UNIV - J) \<times> (space M - X) \<union> (SIGMA j:J. space M - F j)" 2.101 + unfolding A by (auto simp: COCOUNT_def) 2.102 + show ?case 2.103 + using XFJ unfolding * 2.104 + by (intro exI[of _ J] exI[of _ "space M - X"] exI[of _ "\<lambda>j. space M - F j"]) auto 2.105 +next 2.106 + case (Union A) 2.107 + 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)" 2.108 + and A_eq: "A = (\<lambda>i. (UNIV - J i) \<times> X i \<union> Sigma (J i) (F i))" 2.109 + unfolding fun_eq_iff using Union.IH by metis 2.110 + show ?case 2.111 + proof (intro exI conjI) 2.112 + def G \<equiv> "\<lambda>j. (\<Union>i. if j \<in> J i then F i j else X i)" 2.113 + show "(\<Union>i. X i) \<in> sets M" "countable (\<Union>i. J i)" "G \<in> (\<Union>i. J i) \<rightarrow> sets M" 2.114 + using XFJ by (auto simp: G_def Pi_iff) 2.115 + 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)" 2.116 + unfolding A_eq by (auto split: split_if_asm) 2.117 + qed 2.118 +qed 2.119 + 2.120 +context 2.121 + fixes EXP :: "(real \<Rightarrow> bool) measure" 2.122 + assumes eq: "\<And>P. split P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP" 2.123 +begin 2.124 + 2.125 +lemma space_EXP: "space EXP = measurable COCOUNT BOOL" 2.126 +proof - 2.127 + { fix f 2.128 + have "f \<in> space EXP \<longleftrightarrow> (\<lambda>(a, b). f b) \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL" 2.129 + using eq[of "\<lambda>x. f"] by (simp add: measurable_const_iff) 2.130 + also have "\<dots> \<longleftrightarrow> f \<in> measurable COCOUNT BOOL" 2.131 + by auto 2.132 + finally have "f \<in> space EXP \<longleftrightarrow> f \<in> measurable COCOUNT BOOL" . } 2.133 + then show ?thesis by auto 2.134 +qed 2.135 + 2.136 +lemma measurable_eq_EXP: "(\<lambda>x y. x = y) \<in> measurable POW EXP" 2.137 + unfolding measurable_def by (auto simp: space_EXP) 2.138 + 2.139 +lemma measurable_eq_pair: "(\<lambda>(y, x). x = y) \<in> measurable (COCOUNT \<Otimes>\<^sub>M POW) BOOL" 2.140 + using measurable_eq_EXP unfolding eq[symmetric] 2.141 + by (subst measurable_pair_swap_iff) simp 2.142 + 2.143 +lemma ce: False 2.144 +proof - 2.145 + have "{(y, x) \<in> space (COCOUNT \<Otimes>\<^sub>M POW). x = y} \<in> sets (COCOUNT \<Otimes>\<^sub>M POW)" 2.146 + using measurable_eq_pair unfolding pred_def by (simp add: split_beta') 2.147 + also have "{(y, x) \<in> space (COCOUNT \<Otimes>\<^sub>M POW). x = y} = (SIGMA j:UNIV. {j})" 2.148 + by (auto simp: space_pair_measure COCOUNT_def) 2.149 + finally obtain X F J where "countable (J::real set)" 2.150 + and eq: "(SIGMA j:UNIV. {j}) = (UNIV - J) \<times> X \<union> (SIGMA j:J. F j)" 2.151 + using pair_COCOUNT[of "SIGMA j:UNIV. {j}" POW] by auto 2.152 + have X_single: "\<And>x. x \<notin> J \<Longrightarrow> X = {x}" 2.153 + using eq[unfolded set_eq_iff] by force 2.154 + 2.155 + have "uncountable (UNIV - J)" 2.156 + using `countable J` uncountable_UNIV_real uncountable_minus_countable by blast 2.157 + then have "infinite (UNIV - J)" 2.158 + by (auto intro: countable_finite) 2.159 + then have "\<exists>A. finite A \<and> card A = 2 \<and> A \<subseteq> UNIV - J" 2.160 + by (rule infinite_arbitrarily_large) 2.161 + then obtain i j where ij: "i \<in> UNIV - J" "j \<in> UNIV - J" "i \<noteq> j" 2.162 + by (auto simp add: card_Suc_eq numeral_2_eq_2) 2.163 + have "{(i, i), (j, j)} \<subseteq> (SIGMA j:UNIV. {j})" by auto 2.164 + with ij X_single[of i] X_single[of j] show False 2.165 + by auto 2.166 +qed 2.167 + 2.168 +end 2.169 + 2.170 +corollary "\<not> (\<exists>EXP. \<forall>P. split P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP)" 2.171 + using ce by blast 2.172 + 2.173 +end 2.174 +

3.1 --- a/src/HOL/ROOT Mon Dec 15 07:20:49 2014 +0100 3.2 +++ b/src/HOL/ROOT Wed Dec 17 16:10:30 2014 +0100 3.3 @@ -715,6 +715,7 @@ 3.4 Probability 3.5 "ex/Dining_Cryptographers" 3.6 "ex/Koepf_Duermuth_Countermeasure" 3.7 + "ex/Measure_Not_CCC" 3.8 document_files "root.tex" 3.9 3.10 session "HOL-Nominal" (main) in Nominal = HOL +