Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Measure_Not_CCC.thy
Sprache: Unknown
(* Author: Johannes Hölzl <[email protected]> *)
section \<open>The Category of Measurable Spaces is not Cartesian Closed\<close>
theory Measure_Not_CCC
imports "HOL-Probability.Probability"
begin
text \<open>
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>\<open>\<lambda>x y. x = y\<close> is $\mathbb{R}$-$\mathbb{B}^\mathbb{C}$-measurable,
but \<^term>\<open>\<lambda>(x, y). x = y\<close> is not $(\mathbb{R} \times \mathbb{C})$-$\mathbb{B}$-measurable.
\<close>
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 \\<^sub>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 \\<^sub>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 \\<^sub>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 \\<^sub>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 \\<^sub>M POW). x = y} \ sets (COCOUNT \\<^sub>M POW)"
using measurable_eq_pair unfolding pred_def by (simp add: split_beta')
also have "{(y, x) \ space (COCOUNT \\<^sub>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 \<open>countable J\<close> 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 \\<^sub>M COCOUNT) BOOL \ P \ measurable POW EXP)"
using ce by blast
end
[ Verzeichnis aufwärts0.21unsichere Verbindung
Übersetzung europäischer Sprachen durch Browser
]
|
|
