(* Author: Johannes Hölzl <hoelzl@in.tum.de> *) section ‹The Category of Measurable Spaces is not Cartesian Closed› theory Measure_Not_CCC imports "HOL-Probability.Probability" begin text ‹ We show that the category of measurable spaces with measurable functions as morphisms is not a Cartesian closed category. While the category has products and terminal objects, the exponential does not exist for each pair of measurable spaces. We show that the exponential $\mathbb{B}^\mathbb{C}$ does not exist, where $\mathbb{B}$ is the discrete measurable space on boolean values, and $\mathbb{C}$ is the $\sigma$-algebra consisting of all countable and co-countable real sets. We also define $\mathbb{R}$ to be the discrete measurable space on the reals. Now, the diagonal predicate \<^term>‹λx y. x = y› is $\mathbb{R}$-$\mathbb{B}^\mathbb{C}$-measurable, but \<^term>‹λ(x, y). x = y› is not $(\mathbb{R} \times \mathbb{C})$-$\mathbb{B}$-measurable. › definition COCOUNT :: "real measure" where "COCOUNT = sigma UNIV {{x} | x. True}" abbreviation POW :: "real measure" where "POW ≡ count_space UNIV" abbreviation BOOL :: "bool measure" where "BOOL ≡ count_space UNIV" lemma measurable_const_iff: "(λx. c) ∈ measurable A B ⟷ (space A = {} ∨ c ∈ space B)" by (auto simp: measurable_def) lemma measurable_eq[measurable]: "((=) x) ∈ measurable COCOUNT BOOL" unfolding pred_def by (auto simp: COCOUNT_def) lemma COCOUNT_eq: "A ∈ COCOUNT ⟷ countable A ∨ countable (UNIV - A)" proof fix A assume "A ∈ COCOUNT" then have "A ∈ sigma_sets UNIV {{x} | x. True}" by (auto simp: COCOUNT_def) then show "countable A ∨ countable (UNIV - A)" proof induction case (Union F) moreover { fix i assume "countable (UNIV - F i)" then have "countable (UNIV - (⋃i. F i))" by (rule countable_subset[rotated]) auto } ultimately show "countable (⋃i. F i) ∨ countable (UNIV - (⋃i. F i))" by blast qed (auto simp: Diff_Diff_Int) next assume "countable A ∨ countable (UNIV - A)" moreover { fix A :: "real set" assume A: "countable A" have "A = (⋃a∈A. {a})" by auto also have "… ∈ COCOUNT" by (intro sets.countable_UN' A) (auto simp: COCOUNT_def) finally have "A ∈ COCOUNT" . } note A = this note A[of A] moreover { assume "countable (UNIV - A)" with A have "space COCOUNT - (UNIV - A) ∈ COCOUNT" by simp then have "A ∈ COCOUNT" by (auto simp: COCOUNT_def Diff_Diff_Int) } ultimately show "A ∈ COCOUNT" by blast qed lemma pair_COCOUNT: assumes A: "A ∈ sets (COCOUNT ⨂⇩_{M}M)" shows "∃J F X. X ∈ sets M ∧ F ∈ J → sets M ∧ countable J ∧ A = (UNIV - J) × X ∪ (SIGMA j:J. F j)" using A unfolding sets_pair_measure proof induction case (Basic X) then obtain a b where X: "X = a × b" and b: "b ∈ sets M" and a: "countable a ∨ countable (UNIV - a)" by (auto simp: COCOUNT_eq) from a show ?case proof assume "countable a" with X b show ?thesis by (intro exI[of _ a] exI[of _ "λ_. b"] exI[of _ "{}"]) auto next assume "countable (UNIV - a)" with X b show ?thesis by (intro exI[of _ "UNIV - a"] exI[of _ "λ_. {}"] exI[of _ "b"]) auto qed next case Empty then show ?case by (intro exI[of _ "{}"] exI[of _ "λ_. {}"] exI[of _ "{}"]) auto next case (Compl A) then obtain J F X where XFJ: "X ∈ sets M" "F ∈ J → sets M" "countable J" and A: "A = (UNIV - J) × X ∪ Sigma J F" by auto have *: "space COCOUNT × space M - A = (UNIV - J) × (space M - X) ∪ (SIGMA j:J. space M - F j)" unfolding A by (auto simp: COCOUNT_def) show ?case using XFJ unfolding * by (intro exI[of _ J] exI[of _ "space M - X"] exI[of _ "λj. space M - F j"]) auto next case (Union A) obtain J F X where XFJ: "⋀i. X i ∈ sets M" "⋀i. F i ∈ J i → sets M" "⋀i. countable (J i)" and A_eq: "A = (λi. (UNIV - J i) × X i ∪ Sigma (J i) (F i))" unfolding fun_eq_iff using Union.IH by metis show ?case proof (intro exI conjI) define G where "G j = (⋃i. if j ∈ J i then F i j else X i)" for j show "(⋃i. X i) ∈ sets M" "countable (⋃i. J i)" "G ∈ (⋃i. J i) → sets M" using XFJ by (auto simp: G_def Pi_iff) show "⋃(A ` UNIV) = (UNIV - (⋃i. J i)) × (⋃i. X i) ∪ (SIGMA j:⋃i. J i. ⋃i. if j ∈ J i then F i j else X i)" unfolding A_eq by (auto split: if_split_asm) qed qed context fixes EXP :: "(real ⇒ bool) measure" assumes eq: "⋀P. case_prod P ∈ measurable (POW ⨂⇩_{M}COCOUNT) BOOL ⟷ P ∈ measurable POW EXP" begin lemma space_EXP: "space EXP = measurable COCOUNT BOOL" proof - { fix f have "f ∈ space EXP ⟷ (λ(a, b). f b) ∈ measurable (POW ⨂⇩_{M}COCOUNT) BOOL" using eq[of "λx. f"] by (simp add: measurable_const_iff) also have "… ⟷ f ∈ measurable COCOUNT BOOL" by auto finally have "f ∈ space EXP ⟷ f ∈ measurable COCOUNT BOOL" . } then show ?thesis by auto qed lemma measurable_eq_EXP: "(λx y. x = y) ∈ measurable POW EXP" unfolding measurable_def by (auto simp: space_EXP) lemma measurable_eq_pair: "(λ(y, x). x = y) ∈ measurable (COCOUNT ⨂⇩_{M}POW) BOOL" using measurable_eq_EXP unfolding eq[symmetric] by (subst measurable_pair_swap_iff) simp lemma ce: False proof - have "{(y, x) ∈ space (COCOUNT ⨂⇩_{M}POW). x = y} ∈ sets (COCOUNT ⨂⇩_{M}POW)" using measurable_eq_pair unfolding pred_def by (simp add: split_beta') also have "{(y, x) ∈ space (COCOUNT ⨂⇩_{M}POW). x = y} = (SIGMA j:UNIV. {j})" by (auto simp: space_pair_measure COCOUNT_def) finally obtain X F J where "countable (J::real set)" and eq: "(SIGMA j:UNIV. {j}) = (UNIV - J) × X ∪ (SIGMA j:J. F j)" using pair_COCOUNT[of "SIGMA j:UNIV. {j}" POW] by auto have X_single: "⋀x. x ∉ J ⟹ X = {x}" using eq[unfolded set_eq_iff] by force have "uncountable (UNIV - J)" using ‹countable J› uncountable_UNIV_real uncountable_minus_countable by blast then have "infinite (UNIV - J)" by (auto intro: countable_finite) then have "∃A. finite A ∧ card A = 2 ∧ A ⊆ UNIV - J" by (rule infinite_arbitrarily_large) then obtain i j where ij: "i ∈ UNIV - J" "j ∈ UNIV - J" "i ≠ j" by (auto simp add: card_Suc_eq numeral_2_eq_2) have "{(i, i), (j, j)} ⊆ (SIGMA j:UNIV. {j})" by auto with ij X_single[of i] X_single[of j] show False by auto qed end corollary "¬ (∃EXP. ∀P. case_prod P ∈ measurable (POW ⨂⇩_{M}COCOUNT) BOOL ⟷ P ∈ measurable POW EXP)" using ce by blast end