SSL Measure_Not_CCC.thy Sprache: Isabelle

(* Author: Johannes Hölzl <hoelzl@in.tum.de> *)

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
    have "countable (UNIV - (\i. F i))" if "countable (UNIV - F i)" for i
      using that 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
  have A: "A \ COCOUNT" if "countable A" for A :: "real set"
  proof -
    have "A = (\a\A. {a})"
      by auto
    also have "\ \ COCOUNT"
      by (intro sets.countable_UN' that) (auto simp: COCOUNT_def)
    finally show ?thesis .
  qed
  note A[of A]
  moreover
  have "A \ COCOUNT" if "countable (UNIV - A)"
  proof -
    from A that have "space COCOUNT - (UNIV - A) \ COCOUNT" by simp
    then show ?thesis
      by (auto simp: COCOUNT_def Diff_Diff_Int)
  qed
  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 -
  have "f \ space EXP \ f \ measurable COCOUNT BOOL" for f
  proof -
    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 show ?thesis .
  qed
  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

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.