unfortunately, there is no general function space in the measurable spaces
authorhoelzl
Wed Dec 17 16:10:30 2014 +0100 (2014-12-17)
changeset 59144c9b75c03de3c
parent 59143 15c342a9a8e0
child 59145 0e304b1568a5
unfortunately, there is no general function space in the measurable spaces
src/HOL/Probability/document/root.tex
src/HOL/Probability/ex/Measure_Not_CCC.thy
src/HOL/ROOT
     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 +