src/HOL/Probability/ex/Measure_Not_CCC.thy
 author haftmann Tue Oct 13 09:21:15 2015 +0200 (2015-10-13) changeset 61424 c3658c18b7bc parent 59144 c9b75c03de3c child 61808 fc1556774cfe permissions -rw-r--r--
prod_case as canonical name for product type eliminator
     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. case_prod 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. case_prod P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP)"

   168   using ce by blast

   169

   170 end

   171