author | haftmann |
Sun, 18 Nov 2018 18:07:51 +0000 | |
changeset 69313 | b021008c5397 |
parent 67399 | eab6ce8368fa |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
59144
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
1 |
(* Author: Johannes Hölzl <hoelzl@in.tum.de> *) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
2 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
3 |
section \<open>The Category of Measurable Spaces is not Cartesian Closed\<close> |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
4 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
5 |
theory Measure_Not_CCC |
66992
69673025292e
less global theories -- avoid confusion about special cases;
wenzelm
parents:
66453
diff
changeset
|
6 |
imports "HOL-Probability.Probability" |
59144
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
7 |
begin |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
8 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
9 |
text \<open> |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
10 |
We show that the category of measurable spaces with measurable functions as morphisms is not a |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
11 |
Cartesian closed category. While the category has products and terminal objects, the exponential |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
12 |
does not exist for each pair of measurable spaces. |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
13 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
14 |
We show that the exponential $\mathbb{B}^\mathbb{C}$ does not exist, where $\mathbb{B}$ is the |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
15 |
discrete measurable space on boolean values, and $\mathbb{C}$ is the $\sigma$-algebra consisting |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
16 |
of all countable and co-countable real sets. We also define $\mathbb{R}$ to be the discrete |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
17 |
measurable space on the reals. |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
18 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
19 |
Now, the diagonal predicate @{term "\<lambda>x y. x = y"} is $\mathbb{R}$-$\mathbb{B}^\mathbb{C}$-measurable, |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
20 |
but @{term "\<lambda>(x, y). x = y"} is not $(\mathbb{R} \times \mathbb{C})$-$\mathbb{B}$-measurable. |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
21 |
\<close> |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
22 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
23 |
definition COCOUNT :: "real measure" where |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
24 |
"COCOUNT = sigma UNIV {{x} | x. True}" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
25 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
26 |
abbreviation POW :: "real measure" where |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
27 |
"POW \<equiv> count_space UNIV" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
28 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
29 |
abbreviation BOOL :: "bool measure" where |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
30 |
"BOOL \<equiv> count_space UNIV" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
31 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
32 |
lemma measurable_const_iff: "(\<lambda>x. c) \<in> measurable A B \<longleftrightarrow> (space A = {} \<or> c \<in> space B)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
33 |
by (auto simp: measurable_def) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
34 |
|
67399 | 35 |
lemma measurable_eq[measurable]: "((=) x) \<in> measurable COCOUNT BOOL" |
59144
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
36 |
unfolding pred_def by (auto simp: COCOUNT_def) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
37 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
38 |
lemma COCOUNT_eq: "A \<in> COCOUNT \<longleftrightarrow> countable A \<or> countable (UNIV - A)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
39 |
proof |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
40 |
fix A assume "A \<in> COCOUNT" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
41 |
then have "A \<in> sigma_sets UNIV {{x} | x. True}" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
42 |
by (auto simp: COCOUNT_def) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
43 |
then show "countable A \<or> countable (UNIV - A)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
44 |
proof induction |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
45 |
case (Union F) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
46 |
moreover |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
47 |
{ fix i assume "countable (UNIV - F i)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
48 |
then have "countable (UNIV - (\<Union>i. F i))" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
49 |
by (rule countable_subset[rotated]) auto } |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
50 |
ultimately show "countable (\<Union>i. F i) \<or> countable (UNIV - (\<Union>i. F i))" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
51 |
by blast |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
52 |
qed (auto simp: Diff_Diff_Int) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
53 |
next |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
54 |
assume "countable A \<or> countable (UNIV - A)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
55 |
moreover |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
56 |
{ fix A :: "real set" assume A: "countable A" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
57 |
have "A = (\<Union>a\<in>A. {a})" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
58 |
by auto |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
59 |
also have "\<dots> \<in> COCOUNT" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
60 |
by (intro sets.countable_UN' A) (auto simp: COCOUNT_def) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
61 |
finally have "A \<in> COCOUNT" . } |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
62 |
note A = this |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
63 |
note A[of A] |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
64 |
moreover |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
65 |
{ assume "countable (UNIV - A)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
66 |
with A have "space COCOUNT - (UNIV - A) \<in> COCOUNT" by simp |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
67 |
then have "A \<in> COCOUNT" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
68 |
by (auto simp: COCOUNT_def Diff_Diff_Int) } |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
69 |
ultimately show "A \<in> COCOUNT" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
70 |
by blast |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
71 |
qed |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
72 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
73 |
lemma pair_COCOUNT: |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
74 |
assumes A: "A \<in> sets (COCOUNT \<Otimes>\<^sub>M M)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
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)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
76 |
using A unfolding sets_pair_measure |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
77 |
proof induction |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
78 |
case (Basic X) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
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)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
80 |
by (auto simp: COCOUNT_eq) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
81 |
from a show ?case |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
82 |
proof |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
83 |
assume "countable a" with X b show ?thesis |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
84 |
by (intro exI[of _ a] exI[of _ "\<lambda>_. b"] exI[of _ "{}"]) auto |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
85 |
next |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
86 |
assume "countable (UNIV - a)" with X b show ?thesis |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
87 |
by (intro exI[of _ "UNIV - a"] exI[of _ "\<lambda>_. {}"] exI[of _ "b"]) auto |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
88 |
qed |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
89 |
next |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
90 |
case Empty then show ?case |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
91 |
by (intro exI[of _ "{}"] exI[of _ "\<lambda>_. {}"] exI[of _ "{}"]) auto |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
92 |
next |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
93 |
case (Compl A) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
94 |
then obtain J F X where XFJ: "X \<in> sets M" "F \<in> J \<rightarrow> sets M" "countable J" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
95 |
and A: "A = (UNIV - J) \<times> X \<union> Sigma J F" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
96 |
by auto |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
97 |
have *: "space COCOUNT \<times> space M - A = (UNIV - J) \<times> (space M - X) \<union> (SIGMA j:J. space M - F j)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
98 |
unfolding A by (auto simp: COCOUNT_def) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
99 |
show ?case |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
100 |
using XFJ unfolding * |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
101 |
by (intro exI[of _ J] exI[of _ "space M - X"] exI[of _ "\<lambda>j. space M - F j"]) auto |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
102 |
next |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
103 |
case (Union A) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
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)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
105 |
and A_eq: "A = (\<lambda>i. (UNIV - J i) \<times> X i \<union> Sigma (J i) (F i))" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
106 |
unfolding fun_eq_iff using Union.IH by metis |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
107 |
show ?case |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
108 |
proof (intro exI conjI) |
63040 | 109 |
define G where "G j = (\<Union>i. if j \<in> J i then F i j else X i)" for j |
59144
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
110 |
show "(\<Union>i. X i) \<in> sets M" "countable (\<Union>i. J i)" "G \<in> (\<Union>i. J i) \<rightarrow> sets M" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
111 |
using XFJ by (auto simp: G_def Pi_iff) |
69313 | 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)" |
62390 | 113 |
unfolding A_eq by (auto split: if_split_asm) |
59144
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
114 |
qed |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
115 |
qed |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
116 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
117 |
context |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
118 |
fixes EXP :: "(real \<Rightarrow> bool) measure" |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
59144
diff
changeset
|
119 |
assumes eq: "\<And>P. case_prod P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP" |
59144
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
120 |
begin |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
121 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
122 |
lemma space_EXP: "space EXP = measurable COCOUNT BOOL" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
123 |
proof - |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
124 |
{ fix f |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
125 |
have "f \<in> space EXP \<longleftrightarrow> (\<lambda>(a, b). f b) \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
126 |
using eq[of "\<lambda>x. f"] by (simp add: measurable_const_iff) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
127 |
also have "\<dots> \<longleftrightarrow> f \<in> measurable COCOUNT BOOL" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
128 |
by auto |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
129 |
finally have "f \<in> space EXP \<longleftrightarrow> f \<in> measurable COCOUNT BOOL" . } |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
130 |
then show ?thesis by auto |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
131 |
qed |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
132 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
133 |
lemma measurable_eq_EXP: "(\<lambda>x y. x = y) \<in> measurable POW EXP" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
134 |
unfolding measurable_def by (auto simp: space_EXP) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
135 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
136 |
lemma measurable_eq_pair: "(\<lambda>(y, x). x = y) \<in> measurable (COCOUNT \<Otimes>\<^sub>M POW) BOOL" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
137 |
using measurable_eq_EXP unfolding eq[symmetric] |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
138 |
by (subst measurable_pair_swap_iff) simp |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
139 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
140 |
lemma ce: False |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
141 |
proof - |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
142 |
have "{(y, x) \<in> space (COCOUNT \<Otimes>\<^sub>M POW). x = y} \<in> sets (COCOUNT \<Otimes>\<^sub>M POW)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
143 |
using measurable_eq_pair unfolding pred_def by (simp add: split_beta') |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
144 |
also have "{(y, x) \<in> space (COCOUNT \<Otimes>\<^sub>M POW). x = y} = (SIGMA j:UNIV. {j})" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
145 |
by (auto simp: space_pair_measure COCOUNT_def) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
146 |
finally obtain X F J where "countable (J::real set)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
147 |
and eq: "(SIGMA j:UNIV. {j}) = (UNIV - J) \<times> X \<union> (SIGMA j:J. F j)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
148 |
using pair_COCOUNT[of "SIGMA j:UNIV. {j}" POW] by auto |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
149 |
have X_single: "\<And>x. x \<notin> J \<Longrightarrow> X = {x}" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
150 |
using eq[unfolded set_eq_iff] by force |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
151 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
152 |
have "uncountable (UNIV - J)" |
61808 | 153 |
using \<open>countable J\<close> uncountable_UNIV_real uncountable_minus_countable by blast |
59144
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
154 |
then have "infinite (UNIV - J)" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
155 |
by (auto intro: countable_finite) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
156 |
then have "\<exists>A. finite A \<and> card A = 2 \<and> A \<subseteq> UNIV - J" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
157 |
by (rule infinite_arbitrarily_large) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
158 |
then obtain i j where ij: "i \<in> UNIV - J" "j \<in> UNIV - J" "i \<noteq> j" |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
159 |
by (auto simp add: card_Suc_eq numeral_2_eq_2) |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
160 |
have "{(i, i), (j, j)} \<subseteq> (SIGMA j:UNIV. {j})" by auto |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
161 |
with ij X_single[of i] X_single[of j] show False |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
162 |
by auto |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
163 |
qed |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
164 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
165 |
end |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
166 |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
59144
diff
changeset
|
167 |
corollary "\<not> (\<exists>EXP. \<forall>P. case_prod P \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL \<longleftrightarrow> P \<in> measurable POW EXP)" |
59144
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
168 |
using ce by blast |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
169 |
|
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
170 |
end |
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
diff
changeset
|
171 |