Theory Measure_Not_CCC

(* 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 = (aA. {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