Theory StandardBorel

(*  Title:   StandardBorel.thy
    Author:  Michikazu Hirata, Tokyo Institute of Technology
*)

section ‹Standard Borel Spaces›
subsection  ‹Standard Borel Spaces›
theory StandardBorel
  imports Abstract_Metrizable_Topology
begin

locale standard_borel =
  fixes M :: "'a measure"
  assumes Polish_space: "S. Polish_space S  sets M = sets (borel_of S)"
begin

lemma singleton_sets:
  assumes "x  space M"
  shows "{x}  sets M"
proof -
  obtain S where s:"Polish_space S" "sets M = sets (borel_of S)"
    using Polish_space by blast
  have "closedin S {x}"
    using assms by(simp add: sets_eq_imp_space_eq[OF s(2)] closedin_Hausdorff_sing_eq[OF metrizable_imp_Hausdorff_space[OF Polish_space_imp_metrizable_space[OF s(1)]]] space_borel_of)
  thus ?thesis
    using borel_of_closed s by simp
qed

corollary countable_sets:
  assumes "A  space M" "countable A"
  shows "A  sets M"
  using sets.countable[OF singleton_sets assms(2)] assms(1)
  by auto

lemma standard_borel_restrict_space:
  assumes "A  sets M"
  shows "standard_borel (restrict_space M A)"
proof -
  obtain S where s:"Polish_space S" "sets M = sets (borel_of S)"
    using Polish_space by blast
  obtain S' where S':"Polish_space S'" "sets M = sets (borel_of S')" "openin S' A"
    using sets_clopen_topology[OF s(1),simplified s(2)[symmetric],OF assms] by auto
  show ?thesis
    using Polish_space_openin[OF S'(1,3)] S'(2)
    by(auto simp: standard_borel_def borel_of_subtopology sets_restrict_space intro!: exI[where x="subtopology S' A"] )
qed

end

locale standard_borel_ne = standard_borel +
  assumes space_ne: "space M  {}"
begin

lemma standard_borel_ne_restrict_space:
  assumes "A  sets M" "A  {}"
  shows "standard_borel_ne (restrict_space M A)"
  using assms by(auto simp: standard_borel_ne_def standard_borel_ne_axioms_def standard_borel_restrict_space)

lemma standard_borel: "standard_borel M"
  by(rule standard_borel_axioms)

end

lemma standard_borel_sets:
  assumes "standard_borel M" and "sets M = sets N"
  shows "standard_borel N"
  using assms by(simp add: standard_borel_def)

lemma standard_borel_ne_sets:
  assumes "standard_borel_ne M" and "sets M = sets N"
  shows "standard_borel_ne N"
  using assms by(simp add: standard_borel_def standard_borel_ne_def sets_eq_imp_space_eq[OF assms(2)] standard_borel_ne_axioms_def)

lemma pair_standard_borel:
  assumes "standard_borel M" "standard_borel N"
  shows "standard_borel (M M N)"
proof -
  obtain S S' where hs:
   "Polish_space S" "sets M = sets (borel_of S)" "Polish_space S'" "sets N = sets (borel_of S')"
    using assms by(auto simp: standard_borel_def)
  have "sets (M M N) = sets (borel_of (prod_topology S S'))"
    unfolding borel_of_prod[OF Polish_space_imp_second_countable[OF hs(1)] Polish_space_imp_second_countable[OF hs(3)],symmetric]
    using sets_pair_measure_cong[OF hs(2,4)] .
  thus ?thesis
    unfolding standard_borel_def by(auto intro!: exI[where x="prod_topology S S'"] simp: Polish_space_prod[OF hs(1,3)])
qed

lemma pair_standard_borel_ne:
  assumes "standard_borel_ne M" "standard_borel_ne N"
  shows "standard_borel_ne (M M N)"
  using assms by(auto simp: pair_standard_borel standard_borel_ne_def standard_borel_ne_axioms_def space_pair_measure)

lemma product_standard_borel:
  assumes "countable I"
      and "i. i  I  standard_borel (M i)"
    shows "standard_borel (ΠM iI. M i)"
proof -
  obtain S where hs:
   "i. i  I  Polish_space (S i)" "i. i  I  sets (M i) = sets (borel_of (S i))"
    using assms(2) by(auto simp: standard_borel_def) metis
  have "sets (ΠM iI. M i) = sets (ΠM iI. borel_of (S i))"
    using hs(2) by(auto intro!: sets_PiM_cong)
  also have "... = sets (borel_of (product_topology S I))"
    using assms(1) Polish_space_imp_second_countable[OF hs(1)] by(auto intro!: sets_PiM_equal_borel_of)
  finally have 1:"sets (ΠM iI. M i) = sets (borel_of (product_topology S I))".
  show ?thesis
    unfolding standard_borel_def
    using assms(1) hs(1) by(auto intro!: exI[where x="product_topology S I"] Polish_space_product simp: 1)
qed

lemma product_standard_borel_ne:
  assumes "countable I"
      and "i. i  I  standard_borel_ne (M i)"
    shows "standard_borel_ne (ΠM iI. M i)"
  using assms by(auto simp: standard_borel_ne_def standard_borel_ne_axioms_def product_standard_borel)

lemma closed_set_standard_borel[simp]:
  fixes U :: "'a :: topological_space set"
  assumes "Polish_space (euclidean :: 'a topology)" "closed U"
  shows "standard_borel (restrict_space borel U)"
  by(auto simp: standard_borel_def borel_of_euclidean borel_of_subtopology assms intro!: exI[where x="subtopology euclidean U"] Polish_space_closedin)

lemma closed_set_standard_borel_ne[simp]:
  fixes U :: "'a :: topological_space set"
  assumes "Polish_space (euclidean :: 'a topology)" "closed U" "U  {}"
  shows "standard_borel_ne (restrict_space borel U)"
  using assms by(simp add: standard_borel_ne_def standard_borel_ne_axioms_def)

lemma open_set_standard_borel[simp]:
  fixes U :: "'a :: topological_space set"
  assumes "Polish_space (euclidean :: 'a topology)" "open U"
  shows "standard_borel (restrict_space borel U)"
  by(auto simp: standard_borel_def borel_of_euclidean borel_of_subtopology assms intro!: exI[where x="subtopology euclidean U"] Polish_space_openin)

lemma open_set_standard_borel_ne[simp]:
  fixes U :: "'a :: topological_space set"
  assumes "Polish_space (euclidean :: 'a topology)" "open U" "U  {}"
  shows "standard_borel_ne (restrict_space borel U)"
  using assms by(simp add: standard_borel_ne_def standard_borel_ne_axioms_def)

lemma standard_borel_ne_borel[simp]: "standard_borel_ne (borel :: ('a :: polish_space) measure)"
  and standard_borel_ne_lborel[simp]: "standard_borel_ne lborel"
  unfolding standard_borel_def standard_borel_ne_def standard_borel_ne_axioms_def
  by(auto intro!: exI[where x=euclidean] simp: borel_of_euclidean)

lemma count_space_standard'[simp]:
  assumes "countable I"
  shows "standard_borel (count_space I)"
  by(rule standard_borel_sets[OF _ sets_borel_of_discrete_topology]) (auto simp add: assms Polish_space_discrete_topology standard_borel_def intro!: exI[where x="discrete_topology I"])

lemma count_space_standard_ne[simp]: "standard_borel_ne (count_space (UNIV :: (_ :: countable) set))"
  by (simp add: standard_borel_ne_def standard_borel_ne_axioms_def)

corollary measure_pmf_standard_borel_ne[simp]: "standard_borel_ne (measure_pmf (p :: (_ :: countable) pmf))"
  using count_space_standard_ne sets_measure_pmf_count_space standard_borel_ne_sets by blast

corollary measure_spmf_standard_borel_ne[simp]: "standard_borel_ne (measure_spmf (p :: (_ :: countable) spmf))"
  using count_space_standard_ne sets_measure_spmf standard_borel_ne_sets by blast

corollary countable_standard_ne[simp]:
 "standard_borel_ne (borel :: 'a :: {countable,t2_space} measure)"
  by(simp add: standard_borel_sets[OF _ sets_borel_eq_count_space[symmetric]] standard_borel_ne_def standard_borel_ne_axioms_def)

lemma(in standard_borel) countable_discrete_space:
  assumes "countable (space M)"
  shows "sets M = Pow (space M)"
proof safe
  fix A
  assume "A  space M"
  with assms have "countable A"
    by(simp add: countable_subset)
  thus "A  sets M"
    using A  space M singleton_sets
    by(auto intro!: sets.countable[of A])
qed(use sets.sets_into_space in auto)

lemma(in standard_borel) measurable_isomorphic_standard:
  assumes "M measurable_isomorphic N"
  shows "standard_borel N"
proof -
  obtain S where S:"Polish_space S" "sets M = sets (borel_of S)"
    using Polish_space by auto
  from measurable_isomorphic_borels[OF S(2) assms]
  obtain S' where S': "S homeomorphic_space S'  sets N = sets (borel_of S')"
    by auto
  thus ?thesis
    by(auto simp: standard_borel_def homeomorphic_Polish_space_aux[OF S(1)] intro!:exI[where x=S'])
qed

lemma(in standard_borel_ne) measurable_isomorphic_standard_ne:
  assumes "M measurable_isomorphic N"
  shows "standard_borel_ne N"
  using measurable_ismorphic_empty2[OF _ assms] by(auto simp: measurable_isomorphic_standard[OF assms] standard_borel_ne_def standard_borel_ne_axioms_def space_ne)

lemma(in standard_borel) standard_borel_embed_measure:
  assumes"inj_on f (space M)"
  shows "standard_borel (embed_measure M f)"
  using measurable_embed_measure2'[OF assms]
  by(auto intro!: measurable_isomorphic_standard exI[where x=f] simp: measurable_isomorphic_def measurable_isomorphic_map_def assms in_sets_embed_measure measurable_def sets.sets_into_space space_embed_measure the_inv_into_into the_inv_into_vimage bij_betw_def)

corollary(in standard_borel_ne) standard_borel_ne_embed_measure:
  assumes"inj_on f (space M)"
  shows "standard_borel_ne (embed_measure M f)"
  by (simp add: assms space_embed_measure space_ne standard_borel_embed_measure standard_borel_ne_axioms_def standard_borel_ne_def)

lemma
  shows standard_ne_ereal: "standard_borel_ne (borel :: ereal measure)"
    and standard_ne_ennreal: "standard_borel_ne (borel :: ennreal measure)"
  using Polish_space_ereal Polish_space_ennreal by(auto simp: standard_borel_ne_def standard_borel_ne_axioms_def standard_borel_def borel_of_euclidean)

text ‹ Cantor space $\mathscr{C}$ ›
definition Cantor_space :: "(nat  real) measure" where
"Cantor_space  (ΠM i UNIV. restrict_space borel {0,1})"

lemma Cantor_space_standard_ne: "standard_borel_ne Cantor_space"
  by(auto simp: Cantor_space_def intro!: product_standard_borel_ne)

lemma Cantor_space_borel:
 "sets (borel_of Cantor_space_topology) = sets Cantor_space"
  (is "?lhs = _")
proof -
  have "?lhs = sets (ΠM i UNIV. borel_of (top_of_set {0,1}))"
    by(auto intro!: sets_PiM_equal_borel_of[symmetric] second_countable_subtopology)
  thus ?thesis
    by(simp add: borel_of_subtopology Cantor_space_def borel_of_euclidean)
qed

text ‹ Hilbert cube $\mathscr{H}$ ›
definition Hilbert_cube :: "(nat  real) measure" where
"Hilbert_cube  (ΠM i UNIV. restrict_space borel {0..1})"

lemma Hilbert_cube_standard_ne: "standard_borel_ne Hilbert_cube"
  by(auto simp: Hilbert_cube_def intro!: product_standard_borel_ne)

lemma Hilbert_cube_borel:
 "sets (borel_of Hilbert_cube_topology) = sets Hilbert_cube" (is "?lhs = _")
proof -
  have "?lhs = sets (ΠM i UNIV. borel_of (top_of_set {0..1}))"
    by(auto intro!: sets_PiM_equal_borel_of[symmetric] second_countable_subtopology)
  thus ?thesis
    by(simp add: borel_of_subtopology Hilbert_cube_def borel_of_euclidean)
qed

subsection ‹ Isomorphism between $\mathscr{C}$ and $\mathscr{H}$›
lemma Cantor_space_isomorphic_to_Hilbert_cube:
 "Cantor_space measurable_isomorphic Hilbert_cube"
proof -
  text ‹ Isomorphism between $\mathscr{C}$ and $[0,1]$›

  have Cantor_space_isomorphic_to_01closed: "Cantor_space measurable_isomorphic (restrict_space borel {0..1::real})"
  proof -
    have space_Cantor_space: "space Cantor_space = (ΠE i UNIV. {0,1})"
      by(simp add: Cantor_space_def space_PiM)
    have space_Cantor_space_01[simp]: "0  x n" "x n  1" "x n  {0,1}" if "x  space Cantor_space" for x n
      using PiE_mem[OF that[simplified space_Cantor_space],of n]
      by auto
    have Cantor_minus_abs_cantor: "(λn. ¦x n - y n¦)  space Cantor_space" if assms:"x  space Cantor_space" "y  space Cantor_space" for x y
      unfolding space_Cantor_space
    proof safe
      fix n
      assume "¦x n - y n¦  0"
      then consider "x n = 0  y n = 1" | "x n = 1  y n = 0"
        using space_Cantor_space_01[OF assms(1),of n] space_Cantor_space_01[OF assms(2),of n]
        by auto
      thus "¦x n - y n¦ = 1"
        by cases auto
    qed simp

    define Cantor_to_01 :: "(nat  real)  real" where
      "Cantor_to_01  (λx. (n. (1/3)^(Suc n)* x n))"
    text @{term Cantor_to_01} is a measurable injective embedding.›
    have Cantor_to_01_summable'[simp]: "summable (λn. (1/3)^(Suc n)* x n)" if "x  space Cantor_space" for x
    proof(rule summable_comparison_test'[where g="λn. (1/3)^ n" and N=0])
      show "norm ((1 / 3) ^ Suc n * x n)  (1 / 3) ^ n" for n
        using space_Cantor_space_01[OF that,of n] by auto
    qed simp

    have Cantor_to_01_summable[simp]: "x. x  space Cantor_space  summable (λn. (1/3)^ n* x n)"
      using Cantor_to_01_summable' by simp

    have Cantor_to_01_subst_summable[simp]: "summable (λn. (1/3)^ n* (x n - y n))" if assms:"x  space Cantor_space" "y  space Cantor_space" for x y
    proof(rule summable_comparison_test'[where g="λn. (1/3)^ n" and N=0])
      show " norm ((1 / 3) ^ n * (x n - y n))  (1 / 3) ^ n" for n
        using space_Cantor_space_01[OF Cantor_minus_abs_cantor[OF assms],of n]
        by(auto simp: idom_abs_sgn_class.abs_mult)
    qed simp

    have Cantor_to_01_image: "Cantor_to_01  space Cantor_space  {0..1}"
    proof
      fix x
      assume h:"x  space Cantor_space"
      have "Cantor_to_01 x  (n. (1/3)^(Suc n))"
        unfolding Cantor_to_01_def
        by(rule suminf_le) (use h Cantor_to_01_summable[OF h] in auto)
      also have "... = (n. (1 / 3) ^ n) - (1::real)"
        using suminf_minus_initial_segment[OF complete_algebra_summable_geometric[of "1/3::real"],of 1]
        by auto
      finally have "Cantor_to_01 x  1"
        by(simp add: suminf_geometric[of "1/3"])
      moreover have "0  Cantor_to_01 x"
        unfolding Cantor_to_01_def
        by(rule suminf_nonneg) (use Cantor_to_01_summable[OF h] h in auto)
      ultimately show "Cantor_to_01 x  {0..1}"
        by simp
    qed
    have Cantor_to_01_measurable: "Cantor_to_01  Cantor_space M restrict_space borel {0..1}"
    proof(rule measurable_restrict_space2)
      show "Cantor_to_01  borel_measurable Cantor_space"
        unfolding Cantor_to_01_def
      proof(rule borel_measurable_suminf)
        fix n
        have "(λx. x n)  Cantor_space M restrict_space borel {0, 1}"
          by(simp add: Cantor_space_def)
        hence "(λx. x n)  borel_measurable Cantor_space"
          by(simp add: measurable_restrict_space2_iff)
        thus "(λx. (1 / 3) ^ Suc n * x n)  borel_measurable Cantor_space"
          by simp
      qed
    qed(rule Cantor_to_01_image)

    have Cantor_to_01_inj: "inj_on Cantor_to_01 (space Cantor_space)"
      and Cantor_to_01_preserves_sets: "A  sets Cantor_space  Cantor_to_01 ` A  sets (restrict_space borel {0..1})" for A
    proof -
      have sets_Cantor: "sets Cantor_space = sets (borel_of (product_topology (λ_. subtopology euclidean {0,1}) UNIV))"
        (is "?lhs = _")
      proof -
        have "?lhs =  sets (ΠM i UNIV. borel_of (subtopology euclidean {0,1}))"
          by (simp add: Cantor_space_def borel_of_euclidean borel_of_subtopology)
        thus ?thesis
          by(auto intro!: sets_PiM_equal_borel_of second_countable_subtopology Polish_space_imp_second_countable[of "euclideanreal"])
      qed
      have s:"space Cantor_space = topspace (product_topology (λ_. subtopology euclidean {0,1}) UNIV)"
        by(simp add: space_Cantor_space)

      let ?d = "λx y::real. if (x = 0  x = 1)  (y = 0  y = 1) then dist x y else 0"
      interpret d01: Metric_space "{0,1::real}" ?d
        by(auto simp: Metric_space_def)
      have d01: "d01.mtopology = top_of_set {0,1}" d01.mcomplete
      proof -
        interpret Metric_space "{0,1}" dist
          by (simp add: Met_TC.subspace)
        have "d01.mtopology = mtopology"
          by(auto intro!: Metric_space_eq_mtopology simp: Metric_space_def metric_space_class.dist_commute)
        also have "... = top_of_set {0,1}"
          by(auto intro!: Submetric.mtopology_submetric[of UNIV dist "{0,1::real}",simplified] simp: Submetric_def Metric_space_def Submetric_axioms_def dist_real_def)
        finally show "d01.mtopology = top_of_set {0,1}" .
        show d01.mcomplete
          using Metric_space_eq_mcomplete[OF d01.Metric_space_axioms,of dist] d01.compact_space_eq_Bolzano_Weierstrass d01.compact_space_imp_mcomplete finite.emptyI finite_subset by blast
      qed
      interpret pd: Product_metric "1/3" UNIV id id "λ_. {0,1::real}" "λ_. ?d" 1
        by(auto intro!: product_metric_natI d01.Metric_space_axioms)
      have mpd_top: "pd.Product_metric.mtopology = Cantor_space_topology"
        by(auto simp: pd.Product_metric_mtopology_eq[symmetric] d01 intro!: product_topology_cong)
      have pd_mcomplete: pd.Product_metric.mcomplete
        by(auto intro!: pd.mcomplete_Mi_mcomplete_M d01)
      interpret m01: Submetric UNIV dist "{0..1::real}"
        by(simp add: Submetric_def Submetric_axioms_def Met_TC.Metric_space_axioms)
      have "restrict_space borel {0..1} = borel_of m01.sub.mtopology"
        by (simp add: borel_of_euclidean borel_of_subtopology m01.mtopology_submetric)
      have pd_def: "pd.product_dist x y = (n. (1/3)^n * ¦x n - y n¦)" if "x  space Cantor_space" "y  space Cantor_space" for x y
        using space_Cantor_space_01[OF that(1)] space_Cantor_space_01[OF that(2)] that by(auto simp: product_dist_def dist_real_def)
      have 1: "¦Cantor_to_01 x - Cantor_to_01 y¦  pd.product_dist x y" (is "?lhs  ?rhs") if "x  space Cantor_space" "y  space Cantor_space" for x y
      proof -
        have "?lhs = ¦(n. (1/3)^(Suc n)* x n - (1/3)^(Suc n)* y n)¦"
          using that by(simp add: suminf_diff Cantor_to_01_def)
        also have "... = ¦n. (1/3)^(Suc n) * (x n - y n) ¦"
          by (simp add: right_diff_distrib)
        also have "...  (n. ¦(1/3)^(Suc n) * (x n - y n)¦)"
        proof(rule summable_rabs)
          have "(λn. ¦(1 / 3) ^ Suc n * (x n - y n)¦) = (λn. (1 / 3) ^ Suc n * ¦(x n - y n)¦)"
            by (simp add: abs_mult_pos mult.commute)
          moreover have "summable ..."
            using Cantor_minus_abs_cantor[OF that] by simp
          ultimately show "summable (λn. ¦(1 / 3) ^ Suc n * (x n - y n)¦)" by simp
        qed
        also have "... = (n. (1/3)^(Suc n) * ¦x n - y n¦)"
          by (simp add: abs_mult_pos mult.commute)
        also have "...  pd.product_dist x y"
          unfolding pd_def[OF that]
          by(rule suminf_le) (use Cantor_minus_abs_cantor[OF that] in auto)
        finally show ?thesis .
      qed

      have 2:"¦Cantor_to_01 x - Cantor_to_01 y¦   1 / 9 * pd.product_dist x y" (is "?lhs  ?rhs") if "x  space Cantor_space" "y  space Cantor_space" for x y
      proof(cases "x = y")
        case True
        then show ?thesis
          using pd.Product_metric.zero[of x y] that by(simp add: space_Cantor_space)
      next
        case False
        then obtain n' where "x n'  y n'" by auto
        define n where "n  Min {n. n  n'  x n  y n}"
        have "n  n'"
          using x n'  y n' n_def by fastforce
        have "x n  y n"
          using x n'  y n' linorder_class.Min_in[of "{n. n  n'  x n  y n}"]
          by(auto simp: n_def)
        have "i<n. x i = y i"
        proof safe
          fix i
          assume "i < n"
          show "x i = y i"
          proof(rule ccontr)
            assume "x i  y i"
            then have "i  {n. n  n'  x n  y n}"
              using n  n' i < n by auto
            thus False
              using i < n linorder_class.Min_gr_iff[of "{n. n  n'  x n  y n}" i] x n'  y n'
              by(auto simp: n_def)
          qed
        qed
        have u1: "(1/3) ^ (Suc n) * (1/2)  ¦Cantor_to_01 x - Cantor_to_01 y¦"
        proof -
          have "(1/3) ^ (Suc n) * (1/2)  ¦(m. (1/3)^(Suc (m + Suc n)) * (x (m + Suc n) - y (m + Suc n))) + (1 / 3) ^ Suc n * (x n - y n)¦"
          proof -
            have "(1 / 3) ^ Suc n - (1/3)^(n + 2) * 3/2  (1 / 3) ^ Suc n -  ¦(m. (1 / 3) ^ Suc (m + Suc n) * (y (m + Suc n) - x (m + Suc n)))¦"
            proof -
              have "¦(m. (1 / 3) ^ Suc (m + Suc n) * (y (m + Suc n) - x (m + Suc n)))¦  (1/3)^(n + 2) * 3/2"
                (is "?lhs  _")
              proof -
                have "?lhs  (m. ¦(1 / 3) ^ Suc (m + Suc n) * (y (m + Suc n) - x (m + Suc n))¦)"
                  apply(rule summable_rabs,rule summable_ignore_initial_segment[of _ "Suc n"])
                  using Cantor_minus_abs_cantor[OF that(2,1)] by(simp add: abs_mult)
                also have "... = (m. (1 / 3) ^ Suc (m + Suc n) * ¦y (m + Suc n) - x (m + Suc n)¦)"
                  by(simp add: abs_mult)
                also have "...  (m. (1 / 3) ^ Suc (m + Suc n))"
                  apply(rule suminf_le)
                  using space_Cantor_space_01[OF Cantor_minus_abs_cantor[OF that(2,1)]]
                    apply simp
                   apply(rule summable_ignore_initial_segment[of _ "Suc n"])
                  using Cantor_minus_abs_cantor[OF that(2,1)] by auto
                also have "... = (m. (1 / 3) ^ (m + Suc (Suc n)) * 1)" by simp
                also have "... = (1/3)^(n + 2) * 3/(2::real)"
                  by(simp only: pd.nsum_of_rK[of "Suc (Suc n)"],simp)
                finally show ?thesis .
              qed
              thus ?thesis by simp
            qed
            also have "... = ¦(1 / 3) ^ Suc n * (x n - y n)¦ - ¦m. (1 / 3) ^ Suc (m + Suc n) * (y (m + Suc n) - x (m + Suc n))¦"
              using x n  y n space_Cantor_space_01[OF Cantor_minus_abs_cantor[OF that],of n] by(simp add: abs_mult)
            also have "...  ¦(1 / 3) ^ Suc n * (x n - y n) - (m. (1 / 3) ^ Suc (m + Suc n) * (y (m + Suc n) - x (m + Suc n)))¦"
              by simp
            also have "... = ¦(1 / 3) ^ Suc n * (x n - y n) + (m. (1 / 3) ^ Suc (m + Suc n) * (x (m + Suc n) - y (m + Suc n)))¦"
            proof -
              have "(m. (1 / 3) ^ Suc (m + Suc n) * (x (m + Suc n) - y (m + Suc n))) = (m. - ((1 / 3) ^ Suc (m + Suc n) * (y (m + Suc n) - x (m + Suc n))))"
              proof -
                { fix nn :: nat
                  have "r ra rb. - ((- (r::real) + ra) / (1 / rb)) = (- ra + r) / (1 / rb)"
                    by (simp add: left_diff_distrib)
                  then have "- ((y (Suc (n + nn)) + - x (Suc (n + nn))) * (1 / 3) ^ Suc (Suc (n + nn))) = (x (Suc (n + nn)) + - y (Suc (n + nn))) * (1 / 3) ^ Suc (Suc (n + nn))"
                    by fastforce
                  then have "- ((1 / 3) ^ Suc (nn + Suc n) * (y (nn + Suc n) - x (nn + Suc n))) = (1 / 3) ^ Suc (nn + Suc n) * (x (nn + Suc n) - y (nn + Suc n))"
                    by (simp add: add.commute mult.commute) }
                then show ?thesis
                  by presburger
              qed
              also have "... = - (m. (1 / 3) ^ Suc (m + Suc n) * (y (m + Suc n) - x (m + Suc n)))"
                apply(rule suminf_minus)
                apply(rule summable_ignore_initial_segment[of _ "Suc n"])
                using that by simp
              finally show ?thesis by simp
            qed
            also have "... = ¦(m. (1 / 3) ^ Suc (m + Suc n) * (x (m + Suc n) - y (m + Suc n))) + (1 / 3) ^ Suc n * (x n - y n)¦"
              using 1 by simp
            finally show ?thesis by simp
          qed
          also have "... = ¦(m. (1/3)^(Suc (m + Suc n)) * (x (m + Suc n) - y (m + Suc n))) + (m<Suc n. (1/3)^(Suc m) * (x m - y m))¦"
            using i<n. x i = y i by auto
          also have "... = ¦n. (1/3)^(Suc n) * (x n - y n)¦"
          proof -
            have "(n. (1 / 3) ^ Suc n * (x n - y n)) = (m. (1 / 3) ^ Suc (m + Suc n) * (x (m + Suc n) - y (m + Suc n))) + (m<Suc n. (1 / 3) ^ Suc m * (x m - y m))"
              by(rule suminf_split_initial_segment) (use that in simp)
            thus ?thesis by simp
          qed
          also have "... = ¦(n. (1/3)^(Suc n)* x n - (1/3)^(Suc n)* y n)¦"
            by (simp add: right_diff_distrib)
          also have "... = ¦Cantor_to_01 x - Cantor_to_01 y¦"
            using that by(simp add: suminf_diff Cantor_to_01_def)
          finally show ?thesis .
        qed
        have u2: "(1/9) * pd.product_dist x y  (1/3) ^ (Suc n) * (1/2)"
        proof -
          have "pd.product_dist x y = (m. (1/3)^m * ¦x m - y m¦)"
            by(simp add: that pd_def)
          also have "... = (m. (1/3)^(m + n) * ¦x (m + n) - y (m + n)¦) + (m<n. (1/3)^m * ¦x m - y m¦)"
            using Cantor_minus_abs_cantor[OF that] by(auto intro!: suminf_split_initial_segment)
          also have "... = (m. (1/3)^(m + n) * ¦x (m + n) - y (m + n)¦)"
            using i<n. x i = y i  by simp
          also have "...  (m. (1/3)^(m + n))"
            using space_Cantor_space_01[OF Cantor_minus_abs_cantor[OF that]] Cantor_minus_abs_cantor[OF that]
            by(auto intro!: suminf_le summable_ignore_initial_segment[of _ n])
          also have "... =  (1 / 3) ^ n * (3 / 2)"
            using pd.nsum_of_rK[of n] by auto
          finally show ?thesis
            by auto
        qed
        from u1 u2 show ?thesis by simp
      qed

      have inj: "inj_on Cantor_to_01 (space Cantor_space)"
      proof
        fix x y
        assume h:"x  space Cantor_space" "y  space Cantor_space"
                 "Cantor_to_01 x = Cantor_to_01 y"
        then have "pd.product_dist x y = 0"
          using 2[OF h(1,2)] pd.Product_metric.nonneg[of x y]
          by simp
        thus "x = y"
          using pd.Product_metric.zero[of x y] h(1,2)
          by(simp add: space_Cantor_space)
      qed

      have closed: "closedin m01.sub.mtopology (Cantor_to_01 ` (space Cantor_space))"
        unfolding m01.sub.metric_closedin_iff_sequentially_closed
      proof safe
        show "a  space Cantor_space  Cantor_to_01 a  {0..1}" for a
          using Cantor_to_01_image by auto
      next
        fix xn x
        assume h:"range xn  Cantor_to_01 ` space Cantor_space" "limitin m01.sub.mtopology xn x sequentially"
        have "n. xn n  {0..1}"
          using h(1) measurable_space[OF Cantor_to_01_measurable]
          by (metis (no_types, lifting) UNIV_I atLeastAtMost_borel image_subset_iff space_restrict_space2 subsetD)
        with h(2) have xnC:"m01.sub.MCauchy xn"
          by(auto intro!: m01.sub.convergent_imp_MCauchy)
        have "n. xspace Cantor_space. xn n = Cantor_to_01 x" using h(1) by auto
        then obtain yn where hx:"n. yn n  space Cantor_space" "n. xn n = Cantor_to_01 (yn n)" by metis
        have "pd.Product_metric.MCauchy yn"
          unfolding pd.Product_metric.MCauchy_def
        proof safe
          fix ε
          assume "(0 :: real) < ε"
          hence "0 < ε / 9" by auto
          then obtain N' where "n m. n  N'  m  N'  ¦xn n - xn m¦ < ε / 9"
            using xnC m01.sub.MCauchy_def xnC unfolding dist_real_def by blast
          thus "N. n n'. N  n  N  n'  pd.product_dist (yn n) (yn n') < ε"
            using order.strict_trans1[OF 2[OF hx(1) hx(1)],of _ _ "ε/9"] hx(1)
            by(auto intro!: exI[where x=N'] simp: hx(2) space_Cantor_space)
        qed(use hx space_Cantor_space in auto)
        then obtain y where y:"limitin pd.Product_metric.mtopology yn y sequentially"
          using pd_mcomplete pd.Product_metric.mcomplete_def by blast
        hence "y  space Cantor_space"
          by (simp add: pd.Product_metric.limitin_mspace space_Cantor_space)
        have "limitin m01.sub.mtopology xn (Cantor_to_01 y) sequentially"
          unfolding m01.sub.limit_metric_sequentially
        proof safe
          show "Cantor_to_01 y  {0..1}"
            using h(1) funcset_image[OF Cantor_to_01_image] y  space Cantor_space by blast
        next
          fix ε
          assume "(0 :: real) < ε"
          then obtain N where "n. n  N  pd.product_dist (yn n) y < ε" "n. n  N  yn n  UNIV E {0, 1}"
            using y by(fastforce simp: pd.Product_metric.limit_metric_sequentially)
          with n. xn n  {0..1} show "N. nN. xn n  {0..1}  dist (xn n) (Cantor_to_01 y) < ε"
            by(auto intro!: exI[where x=N] order.strict_trans1[OF 1[OF hx(1) y  space Cantor_space]] simp: submetric_def 0 < ε hx(2) dist_real_def)
        qed
        hence "Cantor_to_01 y = x"
          using h(2) by(auto dest: m01.sub.limitin_metric_unique)
        with y  space Cantor_space show "x  Cantor_to_01 ` space Cantor_space"
          by auto
      qed

      have open_map:"open_map pd.Product_metric.mtopology (subtopology m01.sub.mtopology (Cantor_to_01 ` (space Cantor_space))) Cantor_to_01"
      proof -
        have "open_map (mtopology_of pd.Product_metric.Self) (subtopology (mtopology_of m01.sub.Self) (Cantor_to_01 ` mspace pd.Product_metric.Self)) Cantor_to_01"
        proof(rule Metric_space_open_map_from_dist)
          fix x ε
          assume "(0 :: real) < ε" " x  mspace pd.Product_metric.Self"
          then have "x  (UNIV :: nat set) E {0, 1::real}"
            by simp
          show "δ>0. ymspace pd.Product_metric.Self. mdist m01.sub.Self (Cantor_to_01 x) (Cantor_to_01 y) < δ  mdist pd.Product_metric.Self x y < ε"
            unfolding pd.Product_metric.mspace_Self pd.Product_metric.mdist_Self m01.sub.mdist_Self
          proof(safe intro!: exI[where x="ε/9"])
            fix y
            assume h:"y  (UNIV :: nat set) E {0, 1::real}" "dist (Cantor_to_01 x) (Cantor_to_01 y) < ε / 9"
            then have sc:"x  space Cantor_space" "y  space Cantor_space"
              using x  UNIV E {0, 1} by(simp_all add: space_Cantor_space)
            have "¦Cantor_to_01 x - Cantor_to_01 y¦ < ε / 9"
              using h by(simp add: dist_real_def)
            with 2[OF sc] show "pd.product_dist x y < ε "
              by simp
          qed (use ε > 0 in auto)
        qed(use Cantor_to_01_image space_Cantor_space in auto)
        thus ?thesis
          by (simp add: mtopology_of_def space_Cantor_space)
      qed
      have "Cantor_to_01 ` A  sets (restrict_space borel {0..1})" if "A  sets Cantor_space" for A
        using open_map_preserves_sets'[of pd.Product_metric.mtopology m01.sub.mtopology Cantor_to_01 A] borel_of_closed[OF closed] inj sets_Cantor open_map that mpd_top restrict_space borel {0..1} = borel_of m01.sub.mtopology
        by (simp add: space_Cantor_space)
      with inj show "inj_on Cantor_to_01 (space Cantor_space)"
        and"A  sets Cantor_space  Cantor_to_01 ` A  sets (restrict_space borel {0..1})"
        by simp_all
    qed

    text ‹ Next, we construct measurable embedding from $[0,1]$ to ${0,1}^{\mathbb{N}}$.›
    define to_Cantor_from_01 :: "real  nat  real"  where
      "to_Cantor_from_01  (λr n. if r = 1 then 1 else real_of_int (2^(Suc n) * r mod 2))"

    text @{term to_Cantor_from_01} is a measurable injective embedding into Cantor space.›
    have to_Cantor_from_01_image': "to_Cantor_from_01 r n  {0,1}" for r n
      unfolding to_Cantor_from_01_def by auto
    have to_Cantor_from_01_image'': "r n. 0  to_Cantor_from_01 r n" "r n. to_Cantor_from_01 r n  1"
      by (auto simp add: to_Cantor_from_01_def)
    have to_Cantor_from_01_image: "to_Cantor_from_01  {0..1}  space Cantor_space"
      using to_Cantor_from_01_image' by(auto simp: space_Cantor_space)
    have to_Cantor_from_01_measurable:
      "to_Cantor_from_01  restrict_space borel {0..1} M Cantor_space"
      unfolding to_Cantor_from_01_def Cantor_space_def
      by(auto intro!: measurable_restrict_space3 measurable_abs_UNIV)
    have to_Cantor_from_01_summable[simp]:
      "summable (λn. (1/2)^n * to_Cantor_from_01 r n)" for r
    proof(rule summable_comparison_test'[where g="λn. (1/2)^ n"])
      show "norm ((1 / 2) ^ n * to_Cantor_from_01 r n)  (1 / 2) ^ n" for n
        using to_Cantor_from_01_image'[of r n] by auto
    qed simp

    have to_Cantor_from_sumn': "(i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i)  r"
      "r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i) < (1/2)^n"
      "to_Cantor_from_01 r n = 1  (1/2)^(Suc n)  r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i)"
      "to_Cantor_from_01 r n = 0  r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i) < (1/2)^(Suc n)" if assms:"r  {0..<1}" for r n
    proof -
      let ?f = "to_Cantor_from_01 r"
      have f_simp: "?f l = real_of_int ( 2^(Suc l) * r mod 2)" for l
        using assms by(simp add: to_Cantor_from_01_def)
      define S where "S = (λn. i<n. (1/2)^(Suc i)*?f i)"
      have SSuc:"S (Suc k) = S k + (1/2)^(Suc k) * to_Cantor_from_01 r k" for k
        by(simp add: S_def)
      have Sfloor: "2^(Suc m) * (l - S m) mod 2 = 2^(Suc m) * l mod 2" for l m
      proof -
        have "z. 2^(Suc m) * ((1/2)^(Suc k) * ?f k) = 2*real_of_int z" if "k < m" for k
        proof -
          have 0:"(2::real) ^ m * (1 / 2) ^ k = 2 * 2^(m-k-1)"
            using that by (simp add: power_diff_conv_inverse)
          consider "?f k = 0" | "?f k = 1"
            using to_Cantor_from_01_image'[of r k] by auto
          thus ?thesis
            apply cases using that 0 by auto
        qed
        then obtain z where "k. k < m  2^(Suc m) * ((1/2)^(Suc k) * ?f k) = 2*real_of_int (z k)"
          by metis
        hence Sm: "2^(Suc m) * S m = real_of_int (2 * (k<m. (z k)))"
          by(auto simp: S_def sum_distrib_left)
        have "2^(Suc m) * (l - S m) mod 2 = 2^(Suc m) * l - 2^(Suc m) *  S m mod 2"
          by (simp add: right_diff_distrib)
        also have "... = 2^(Suc m) * l mod 2"
          unfolding Sm
          by(simp only: floor_diff_of_int) presburger
        finally show ?thesis .
      qed
      have "S n  r  r - S n < (1/2)^n  (?f n = 1  (1/2)^(Suc n)  r - S n)  (?f n = 0  r - S n < (1/2)^(Suc n))"
      proof(induction n)
        case 0
        then show ?case
          using assms by(auto simp: S_def to_Cantor_from_01_def) linarith+
      next
        case (Suc n)
        hence ih: "S n  r" "r - S n < (1 / 2) ^ n"
          "?f n = 1  (1 / 2) ^ Suc n  r - S n"
          "?f n = 0  r - S n < (1 / 2) ^ Suc n"
          by simp_all
        have SSuc':"?f n = 0  S (Suc n) = S n  ?f n = 1  S (Suc n) = S n + (1/2)^(Suc n)"
          using to_Cantor_from_01_image'[of r n] by(simp add: SSuc)
        have goal1:"S (Suc n)  r"
          using SSuc' ih(1) ih(3) by auto
        have goal2: "r - S (Suc n) < (1 / 2) ^ Suc n"
          using SSuc' ih(4) ih(2) by auto
        have goal3_1: "(1 / 2) ^ Suc (Suc n)  r - S (Suc n)" if "?f (Suc n) = 1"
        proof(rule ccontr)
          assume "¬ (1 / 2) ^ Suc (Suc n)  r - S (Suc n)"
          then have "r - S (Suc n) < (1 / 2) ^ Suc (Suc n)" by simp
          hence h:"2 ^ Suc (Suc n) * (r - S (Suc n)) < 1"
            using mult_less_cancel_left_pos[of "2 ^ Suc (Suc n)" "r - S (Suc n)" "(1 / 2) ^ Suc (Suc n)"]
            by (simp add: power_one_over)
          moreover have "0  2 ^ Suc (Suc n) * (r - S (Suc n))"
            using goal1 by simp
          ultimately have "2 ^ Suc (Suc n) * (r - S (Suc n)) = 0"
            by linarith
          thus False
            using that[simplified f_simp] Sfloor[of "Suc n" r]
            by fastforce
        qed
        have goal3_2: "?f (Suc n) = 1" if "(1 / 2) ^ Suc (Suc n)  r - S (Suc n)"
        proof -
          have "1  2 ^ Suc (Suc n) * (r - S (Suc n))"
            using that[simplified f_simp] mult_le_cancel_left_pos[of "2 ^ Suc (Suc n)" "(1 / 2) ^ Suc (Suc n)" "r - S (Suc n)"]
            by (simp add: power_one_over)
          moreover have "2 ^ Suc (Suc n) * (r - S (Suc n)) < 2"
            using mult_less_cancel_left_pos[of "2 ^ Suc (Suc n)" "r - S (Suc n)" "(1 / 2) ^ Suc n"] goal2
            by (simp add: power_one_over)
          ultimately have "2 ^ Suc (Suc n) * (r - S (Suc n)) = 1"
            by linarith
          thus ?thesis
            using Sfloor[of "Suc n" r] by(auto simp: f_simp)
        qed
        have goal4_1: "r - S (Suc n) < (1 / 2) ^ Suc (Suc n)" if "?f (Suc n) = 0"
        proof(rule ccontr)
          assume "¬ r - S (Suc n) < (1 / 2) ^ Suc (Suc n)"
          then have "(1 / 2) ^ Suc (Suc n)  r - S (Suc n)" by simp 
          hence "1  2 ^ Suc (Suc n) * (r - S (Suc n))"
            using mult_le_cancel_left_pos[of "2 ^ Suc (Suc n)" "(1 / 2) ^ Suc (Suc n)" "r - S (Suc n)"]
            by (simp add: power_one_over)
          moreover have "2 ^ Suc (Suc n) * (r - S (Suc n)) < 2"
            using mult_less_cancel_left_pos[of "2 ^ Suc (Suc n)" "r - S (Suc n)" "(1 / 2) ^ Suc n"] goal2
            by (simp add: power_one_over)
          ultimately have "2 ^ Suc (Suc n) * (r - S (Suc n)) = 1"
            by linarith
          thus False
            using that Sfloor[of "Suc n" r] by(auto simp: f_simp)
        qed
        have goal4_2: "?f (Suc n) = 0" if "r - S (Suc n) < (1 / 2) ^ Suc (Suc n)"
        proof -
          have h:"2 ^ Suc (Suc n) * (r - S (Suc n)) < 1"
            using mult_less_cancel_left_pos[of "2 ^ Suc (Suc n)" "r - S (Suc n)" "(1 / 2) ^ Suc (Suc n)"] that
            by (simp add: power_one_over)
          moreover have "0  2 ^ Suc (Suc n) * (r - S (Suc n))"
            using goal1 by simp
          ultimately have "2 ^ Suc (Suc n) * (r - S (Suc n)) = 0"
            by linarith
          thus ?thesis
            using Sfloor[of "Suc n" r] by(auto simp: f_simp)
        qed
        show ?case
          using goal1 goal2 goal3_1 goal3_2 goal4_1 goal4_2 by blast
      qed
      thus "(i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i)  r"
        and "r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i) < (1/2)^n"
        and "to_Cantor_from_01 r n = 1  (1/2)^(Suc n)  r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i)"
        and "to_Cantor_from_01 r n = 0  r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i) < (1/2)^(Suc n)"
        by(simp_all add: S_def)
    qed
    have to_Cantor_from_sumn: "(i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i)  r"
      "r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i)  (1/2)^n"
      "to_Cantor_from_01 r n = 1  (1/2)^(Suc n)  r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i)"
      "to_Cantor_from_01 r n = 0  r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i) < (1/2)^(Suc n)" if assms:"r  {0..1}" for r n
    proof -
      have nsum:"(i<n. (1/2)^(Suc i)) = 1 - (1 / (2::real)) ^ n"
        using one_diff_power_eq[of "1/(2::real)" n] by(auto simp: sum_divide_distrib[symmetric])

      consider "r = 1" | "r {0..<1}" using assms by fastforce
      hence "(i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i)  r  r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i)  (1/2)^n  (to_Cantor_from_01 r n = 1  (1/2)^(Suc n)  r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i))  (to_Cantor_from_01 r n = 0  r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i) < (1/2)^(Suc n))"
      proof cases
        case 1
        then show ?thesis
          using nsum by(auto simp: to_Cantor_from_01_def)
      next
        case 2
        from to_Cantor_from_sumn'[OF this]
        show ?thesis
          using less_eq_real_def by blast
      qed
      thus "(i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i)  r"
        and "r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i)  (1/2)^n"
        and "to_Cantor_from_01 r n = 1  (1/2)^(Suc n)  r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i)"
        and "to_Cantor_from_01 r n = 0  r - (i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i) < (1/2)^(Suc n)"
        by simp_all
    qed

    have to_Cantor_from_sum: "(n. (1/2)^(Suc n)*to_Cantor_from_01 r n) = r" if assms:"r  {0..1}" for r
    proof -
      have 1:"r  (n. (1/2)^(Suc n)*to_Cantor_from_01 r n)"
      proof -
        have 0:"r  (1 / 2) ^ n + (n. (1/2)^(Suc n)*to_Cantor_from_01 r n)" for n
        proof -
          have "r  (1 / 2) ^ n + (i<n. (1 / 2) ^ Suc i * to_Cantor_from_01 r i)"
            using to_Cantor_from_sumn(2)[OF assms,of n] by auto
          also have "...  (1 / 2) ^ n + (n. (1/2)^(Suc n)*to_Cantor_from_01 r n)"
            using to_Cantor_from_01_image''[of r] by(auto intro!: sum_le_suminf)
          finally show ?thesis .
        qed
        have 00:"no. nno. (1 / 2) ^ n < r" if "r>0" for r :: real
        proof -
          obtain n0 where "(1 / 2) ^ n0 < r"
            using reals_power_lt_ex[of _ "2 :: real",OF r>0] by auto
          thus ?thesis
            using order.strict_trans1[OF power_decreasing[of n0 _ "1/2::real"]]
            by(auto intro!: exI[where x=n0])
        qed
        show ?thesis
          apply(rule Lim_bounded2[where f="λn. (1 / 2) ^ n + (n. (1/2)^(Suc n)*to_Cantor_from_01 r n)" and N=0])
          using 0 00 by(auto simp: LIMSEQ_iff)
      qed
      have 2:"(n. (1/2)^(Suc n)*to_Cantor_from_01 r n)  r"
        using to_Cantor_from_sumn[OF assms] by(auto intro!: suminf_le_const)
      show ?thesis
        using 1 2 by simp
    qed
    have to_Cantor_from_sum': "(i<n. (1/2)^(Suc i)*to_Cantor_from_01 r i) = r - (m. (1/2)^(Suc (m + n))*to_Cantor_from_01 r (m + n))" if assms:"r  {0..1}" for r n
      using suminf_minus_initial_segment[of "λn. (1 / 2) ^ Suc n * to_Cantor_from_01 r n" n] to_Cantor_from_sum[OF assms]
      by auto

    have to_Cantor_from_01_exist0: "n.kn. to_Cantor_from_01 r k = 0" if assms:"r  {0..<1}" for r
    proof(rule ccontr)
      assume "¬ (n.kn. to_Cantor_from_01 r k = 0)"
      then obtain n0 where hn0:
        "k. k  n0  to_Cantor_from_01 r k = 1"
        using to_Cantor_from_01_image'[of r] by auto
      define n where "n = Min {i. i  n0  (ki. to_Cantor_from_01 r k = 1)}"
      have n0in: "n0  {i. i  n0  (ki. to_Cantor_from_01 r k = 1)}"
        using hn0 by auto
      have hn:"n  n0" "k. k  n  to_Cantor_from_01 r k = 1"
        using n0in Min_in[of "{i. i  n0  (ki. to_Cantor_from_01 r k = 1)}"]
        by(auto simp: n_def)
      show False
      proof(cases n)
        case 0
        then have "r = (n. (1 / 2) ^ Suc n)"
          using to_Cantor_from_sum[of r] assms hn(2) by simp
        also have "... = 1"
          using nsum_of_r'[of "1/2" 1 1] by auto
        finally show ?thesis
          using assms by auto
      next
        case eqn:(Suc n')
        have "to_Cantor_from_01 r n' = 0"
        proof(rule ccontr)
          assume "to_Cantor_from_01 r n'  0"
          then have "to_Cantor_from_01 r n' = 1"
            using to_Cantor_from_01_image'[of r n'] by auto
          hence "n'  {i. i  n0  (ki. to_Cantor_from_01 r k = 1)}"
            using hn eqn not_less_eq_eq order_antisym_conv by fastforce
          hence "n  n'"
            using Min.coboundedI[of "{i. i  n0  (ki. to_Cantor_from_01 r k = 1)}" n']
            by(simp add: n_def)
          thus False
            using eqn by simp
        qed
        hence le1:"r - (i<n'. (1 / 2) ^ Suc i * to_Cantor_from_01 r i) < (1 / 2) ^ n"
          using to_Cantor_from_sumn'(4)[OF assms,of n'] by (simp add: eqn)
        have "r - (i<n'. (1 / 2) ^ Suc i * to_Cantor_from_01 r i) = (1 / 2) ^ n"
          (is "?lhs = _")
        proof -
          have "?lhs = (m. (1/2)^(m + Suc n')*to_Cantor_from_01 r (m + n'))"
            using to_Cantor_from_sum'[of r n'] assms by simp
          also have "... = (m. (1/2)^(m + Suc n)*to_Cantor_from_01 r (m + n))"
          proof -
            have "(n. (1 / 2) ^ (Suc n + Suc n') * to_Cantor_from_01 r (Suc n + n')) = (m. (1 / 2) ^ (m + Suc n') * to_Cantor_from_01 r (m + n')) - (1 / 2) ^ (0 + Suc n') * to_Cantor_from_01 r (0 + n')"
              by(rule suminf_split_head) (auto intro!: summable_ignore_initial_segment)
            thus ?thesis
              using to_Cantor_from_01 r n' = 0 by(simp add: eqn)
          qed
          also have "... = (m. (1/2)^(m + Suc n))"
            using hn by simp
          also have "... = (1 / 2) ^ n"
            using nsum_of_r'[of "1/2" "Suc n" 1,simplified] by simp
          finally show ?thesis .
        qed
        with le1 show False
          by simp
      qed
    qed
    have to_Cantor_from_01_if_exist0: "to_Cantor_from_01 (n. (1 / 2) ^ Suc n * a n) = a" if assms:"n. a n  {0,1}" "n.kn. a k = 0" for a
    proof
      fix n
      have [simp]: "summable (λn. (1 / 2) ^ n * a n)"
      proof(rule summable_comparison_test'[where g="λn. (1/2)^ n"])
        show "norm ((1 / 2) ^ n * a n)  (1 / 2) ^ n" for n
          using assms(1)[of n] by auto
      qed simp
      let ?r = "n. (1 / 2) ^ Suc n * a n"
      have "?r  {0..1}"
        using assms(1) space_Cantor_space_01[of a,simplified space_Cantor_space] nsum_of_r_leq[of "1/2" a 1 1 0]
        by auto
      show "to_Cantor_from_01 ?r n = a n"
      proof(rule less_induct)
        fix x
        assume ih:"y < x  to_Cantor_from_01 ?r y = a y" for y
        have eq1:"?r - (i<x. (1/2)^(Suc i)*to_Cantor_from_01 ?r i) = (n. (1/2)^(Suc (n + x))* a (n + x))"
          (is "?lhs = ?rhs")
        proof -
          have "?lhs = (n. (1 / 2) ^ Suc (n + x) * a (n + x)) + (i<x. (1/2)^(Suc i)* a i) - (i<x. (1/2)^(Suc i)*to_Cantor_from_01 ?r i)"
            using suminf_split_initial_segment[of "λn. (1 / 2) ^ (Suc n) * a n" x] by simp
          also have "... = (n. (1 / 2) ^ Suc (n + x) * a (n + x)) + (i<x. (1/2)^(Suc i)* a i) - (i<x. (1/2)^(Suc i)*a i)"
            using ih by simp
          finally show ?thesis by simp
        qed
        define Sn where "Sn = (n. (1/2)^(Suc (n + x))* a (n + x))"
        define Sn' where "Sn' = (n. (1/2)^(Suc (n + (Suc x)))* a (n + (Suc x)))"
        have SnSn':"Sn = (1/2)^(Suc x) * a x + Sn'"
          using suminf_split_head[of "λn. (1/2)^(Suc (n + x))* a (n + x)",OF summable_ignore_initial_segment]
          by(auto simp: Sn_def Sn'_def)
        have hsn:"0  Sn'" "Sn' < (1/2)^(Suc x)"
        proof -
          show "0  Sn'"
            unfolding Sn'_def
            by(rule suminf_nonneg,rule summable_ignore_initial_segment) (use assms(1) space_Cantor_space_01[of a,simplified space_Cantor_space] in fastforce)+
        next
          have "n'Suc x. a n' < 1"
            using assms by fastforce
          thus "Sn' <  (1/2)^(Suc x)"
            using nsum_of_r_le[of "1/2" a 1 "Suc x" "Suc (Suc x)"] assms(1) space_Cantor_space_01[of a,simplified space_Cantor_space]
            by(auto simp: Sn'_def)
        qed
        have goal1: "to_Cantor_from_01 ?r x = 1  a x = 1"
        proof -
          have "to_Cantor_from_01 ?r x = 1  (1 / 2) ^ Suc x  Sn"
            using to_Cantor_from_sumn(3)[OF ?r  {0..1}] eq1
            by(fastforce simp: Sn_def)
          also have "...  (1 / 2) ^ Suc x  (1/2)^(Suc x) * a x + Sn'"
            by(simp add: SnSn')
          also have "...  a x = 1"
          proof -
            have "a x = 1" if "(1 / 2) ^ Suc x  (1/2)^(Suc x) * a x + Sn'"
            proof(rule ccontr)
              assume "a x  1"
              then have "a x = 0"
                using assms(1) by auto
              hence "(1 / 2) ^ Suc x  Sn'"
                using that by simp
              thus False
                using hsn by auto
            qed
            thus ?thesis
              by(auto simp: hsn)
          qed
          finally show ?thesis .
        qed
        have goal2: "to_Cantor_from_01 ?r x = 0  a x = 0"
        proof -
          have "to_Cantor_from_01 ?r x = 0  Sn < (1 / 2) ^ Suc x"
            using to_Cantor_from_sumn(4)[OF ?r  {0..1}] eq1
            by(fastforce simp: Sn_def)
          also have "...  (1/2)^(Suc x) * a x + Sn' < (1 / 2) ^ Suc x"
            by(simp add: SnSn')
          also have "...  a x = 0"
          proof -
            have "a x = 0" if "(1/2)^(Suc x) * a x + Sn' < (1 / 2) ^ Suc x"
            proof(rule ccontr)
              assume "a x  0"
              then have "a x = 1"
                using assms(1) by auto
              thus False
                using that hsn by auto
            qed
            thus ?thesis
              using hsn by auto
          qed
          finally show ?thesis .
        qed
        show "to_Cantor_from_01 ?r x = a x"
          using goal1 goal2 to_Cantor_from_01_image'[of ?r x] by auto
      qed
    qed
    have to_Cantor_from_01_sum_of_to_Cantor_from_01: "to_Cantor_from_01 (n. (1 / 2) ^ Suc n * to_Cantor_from_01 r n) = to_Cantor_from_01 r" if assms:"r  {0..1}" for r
    proof -
      consider "r = 1" | "r  {0..<1}"
        using assms by fastforce
      then show ?thesis
      proof cases
        case 1
        then show ?thesis
          using nsum_of_r'[of "1/2" 1 1]
          by(auto simp: to_Cantor_from_01_def)
      next
        case 2
        from to_Cantor_from_01_if_exist0[OF to_Cantor_from_01_image' to_Cantor_from_01_exist0[OF this]]
        show ?thesis .
      qed
    qed
    have to_Cantor_from_01_inj: "inj_on to_Cantor_from_01 (space (restrict_space borel {0..1}))"
    proof
      fix x y :: real
      assume "x  space (restrict_space borel {0..1})" "y  space (restrict_space borel {0..1})"
        and h:"to_Cantor_from_01 x = to_Cantor_from_01 y"
      then have xyin:"x  {0..1}" "y  {0..1}"
        by simp_all
      show "x = y"
        using to_Cantor_from_sum[OF xyin(1)] to_Cantor_from_sum[OF xyin(2)] h
        by simp
    qed
    have to_Cantor_from_01_preserves_sets: "to_Cantor_from_01 ` A  sets Cantor_space" if assms: "A  sets (restrict_space borel {0..1})" for A
    proof -
      define f :: "(nat  real)  real" where "f  (λx. n. (1/2)^(Suc n)* x n)"
      have f_meas:"f  Cantor_space M restrict_space borel {0..1}"
      proof -
        have "f  borel_measurable Cantor_space"
          unfolding Cantor_to_01_def f_def
        proof(rule borel_measurable_suminf)
          fix n
          have "(λx. x n)  Cantor_space M restrict_space borel {0, 1}"
            by(simp add: Cantor_space_def)
          hence "(λx. x n)  borel_measurable Cantor_space"
            by(simp add: measurable_restrict_space2_iff)
          thus "(λx. (1 / 2) ^ Suc n * x n)  borel_measurable Cantor_space"
            by simp
        qed
        moreover have "0  f x" "f x  1" if "x  space Cantor_space" for x
        proof -
          have [simp]:"summable (λn. (1/2)^n* x n)"
          proof(rule summable_comparison_test'[where g="λn. (1/2)^ n"])
            show "norm ((1 / 2) ^ n * x n)  (1 / 2) ^ n" for n
              using that by simp
          qed simp
          show "0  f x"
            using that by(auto intro!: suminf_nonneg simp: f_def)
          show "f x  1"
          proof -
            have "f x  (n. (1/2)^(Suc n))"
              using that by(auto intro!: suminf_le simp: f_def)
            also have "... = 1"
              using nsum_of_r'[of "1/2" 1 1] by simp
            finally show ?thesis .
          qed
        qed
        ultimately show ?thesis
          by(auto intro!: measurable_restrict_space2)
      qed
      have image_sets:"to_Cantor_from_01 ` (space (restrict_space borel {0..1}))  sets Cantor_space"
        (is "?A  _")
      proof -
        have "?A  space Cantor_space"
          using to_Cantor_from_01_image by auto
        have comple_sets:"(ΠE i UNIV. {0,1}) - ?A  sets Cantor_space"
        proof -
          have eq1:"?A = {λn. 1}  {x. (n. x n  {0,1})  (n. kn. x k = 0)}"
          proof
            show "?A  {λn. 1}  {x. (n. x n  {0, 1})  (n. kn. x k = 0)}"
            proof
              fix x
              assume "x  ?A"
              then obtain r where hr:"r  {0..1}" "x = to_Cantor_from_01 r"
                by auto
              then consider "r = 1" | "r  {0..<1}" by fastforce
              thus "x  {λn. 1}  {x. (n. x n  {0,1})  (n. kn. x k = 0)}"
              proof cases
                case 1
                then show ?thesis
                  by(simp add: hr(2) to_Cantor_from_01_def)
              next
                case 2
                from to_Cantor_from_01_exist0[OF this] to_Cantor_from_01_image'
                show ?thesis by(auto simp: hr(2))
              qed
            qed
          next
            show "{λn. 1}  {x. (n. x n  {0, 1})  (n. kn. x k = 0)}  ?A"
            proof
              fix x :: "nat  real"
              assume "x  {λn. 1}  {x. (n. x n  {0,1})  (n. kn. x k = 0)}"
              then consider "x = (λn. 1)" | "(n. x n  {0,1})  (n. kn. x k = 0)"
                by auto
              thus "x  ?A"
              proof cases
                case 1
                then show ?thesis
                  by(auto intro!: image_eqI[where x=1] simp: to_Cantor_from_01_def)
              next
                case 2
                hence "n. 0  x n" "n. x n  1"
                  by (metis dual_order.refl empty_iff insert_iff zero_less_one_class.zero_le_one)+
                with 2 to_Cantor_from_01_if_exist0[of x] nsum_of_r_leq[of "1/2" x 1 1 0]
                show ?thesis
                  by(auto intro!: image_eqI[where x="n. (1 / 2) ^ Suc n * x n"])
              qed
            qed
          qed
          have "(ΠE i UNIV. {0,1}) - ?A = {x. (n. x n  {0,1})  (n. kn. x k = 1)} - {λn. 1}"
          proof
            show "(ΠE i UNIV. {0,1}) - ?A  {x. (n. x n  {0,1})  (n. kn. x k = 1)} - {λn. 1}"
            proof
              fix x :: "nat  real"
              assume "x  (ΠE i UNIV. {0,1}) - ?A"
              then have "n. x n  {0,1}" "¬ (n. kn. x k = 0)" "x  (λn. 1)"
                using eq1 by blast+
              thus "x  {x. (n. x n  {0,1})  (n. kn. x k = 1)} - {λn. 1}"
                by blast
            qed
          next
            show "(ΠE i UNIV. {0,1}) - ?A  {x. (n. x n  {0,1})  (n. kn. x k = 1)} - {λn. 1}"
            proof
              fix x :: "nat  real"
              assume h:"x  {x. (n. x n  {0,1})  (n. kn. x k = 1)} - {λn. 1}"
              then have "n. x n  {0,1}" "n. kn. x k = 1" "x  (λn. 1)"
                by blast+
              hence "¬ (n. kn. x k = 0)"
                by fastforce
              with n. x n  {0,1} x  (λn. 1)
              show "x  (ΠE i UNIV. {0,1}) - ?A"
                using eq1 by blast
            qed
          qed
          also have "... = ( ((λn. {x. (n. x n  {0,1})  (kn. x k = 1)}) ` UNIV)) - {λn. 1}"
            by blast
          also have "...  sets Cantor_space" (is "?B  _")
          proof -
            have "countable ?B"
            proof -
              have "countable {x :: nat  real. (n. x n = 0  x n = 1)  (km. x k = 1)}" for m :: nat
              proof -
                let ?C = "{x::nat  real. (n. x n = 0  x n = 1)  (km. x k = 1)}"
                define g where "g = (λ(x::nat  real) n. if n < m then x n else undefined)"
                have 1:"g ` ?C = (ΠE i {..<m}. {0,1})"
                proof(standard; standard)
                  fix x
                  assume "x  g ` ?C"
                  then show "x  (ΠE i {..<m}. {0,1})"
                    by(auto simp: g_def PiE_def extensional_def)
                next
                  fix x
                  assume h:"x  (ΠE i {..<m}. {0,1::real})"
                  then have "x = g (λn. if n < m then x n else 1)"
                    by(auto simp add: g_def PiE_def extensional_def)
                  moreover have "(λn. if n < m then x n else 1)  ?C"
                    using h by auto
                  ultimately show "x  g ` ?C"
                    by auto
                qed
                have 2:"inj_on g ?C"
                proof
                  fix x y
                  assume hxyg:"x  ?C" "y :  ?C" "g x = g y"
                  show "x = y"
                  proof
                    fix n
                    consider "n < m" | "m  n" by fastforce
                    thus "x n = y n"
                    proof cases
                      case 1
                      then show ?thesis
                        using fun_cong[OF hxyg(3),of n] by(simp add: g_def)
                    next
                      case 2
                      then show ?thesis
                        using hxyg(1,2) by auto
                    qed
                  qed
                qed
                show "countable {x::nat  real. (n. x n = 0  x n = 1)  (km. x k = 1)}"
                  by(rule countable_image_inj_on[OF _ 2]) (auto intro!: countable_PiE simp: 1)
              qed
              thus ?thesis
                by auto
            qed
            moreover have "?B  space Cantor_space"
              by(auto simp: space_Cantor_space)
            ultimately show ?thesis
              using Cantor_space_standard_ne by(simp add: standard_borel.countable_sets standard_borel_ne_def)
          qed
          finally show ?thesis .
        qed
        moreover have "space Cantor_space - ((ΠE i UNIV. {0,1}) - ?A) = ?A"
          using ?A  space Cantor_space space_Cantor_space  by blast
        ultimately show ?thesis
          using sets.compl_sets[OF comple_sets] by auto
      qed
      have "to_Cantor_from_01 ` A = f -` A  to_Cantor_from_01 ` (space (restrict_space borel {0..1}))"
      proof
        show "to_Cantor_from_01 ` A   f -` A  to_Cantor_from_01 ` space (restrict_space borel {0..1})"
        proof
          fix x
          assume "x  to_Cantor_from_01 ` A"
          then obtain a where ha:"a  A" "x = to_Cantor_from_01 a" by auto
          hence "a  {0..1}"
            using sets.sets_into_space[OF assms] by auto
          have "f x = a"
            using to_Cantor_from_sum[OF a  {0..1}] by(simp add: f_def ha(2))
          thus " x  f -` A  to_Cantor_from_01 ` space (restrict_space borel {0..1})"
            using sets.sets_into_space[OF assms] ha by auto
        qed
      next
        show "to_Cantor_from_01 ` A  f -` A  to_Cantor_from_01 ` space (restrict_space borel {0..1})"
        proof
          fix x
          assume h:"x  f -` A  to_Cantor_from_01 ` space (restrict_space borel {0..1})"
          then obtain r where "r  {0..1}" "x = to_Cantor_from_01 r"
            by auto
          from h have "f x  A"
            by simp
          hence "to_Cantor_from_01 (f x) = x"
            using to_Cantor_from_01_sum_of_to_Cantor_from_01[OF r  {0..1}]
            by(simp add: f_def x = to_Cantor_from_01 r)
          with f x  A
          show "x  to_Cantor_from_01 ` A"
            by (simp add: rev_image_eqI)
        qed
      qed
      also have "...  sets Cantor_space"
      proof -
        have " f -` A  space Cantor_space  to_Cantor_from_01 ` space (restrict_space borel {0..1}) = f -` A  to_Cantor_from_01 ` (space (restrict_space borel {0..1}))"
          using to_Cantor_from_01_image sets.sets_into_space[OF assms,simplified] by auto
        thus ?thesis
          using sets.Int[OF measurable_sets[OF f_meas assms] image_sets]
          by fastforce
      qed
      finally show ?thesis .
    qed
    show ?thesis
      using Schroeder_Bernstein_measurable[OF Cantor_to_01_measurable Cantor_to_01_preserves_sets Cantor_to_01_inj to_Cantor_from_01_measurable to_Cantor_from_01_preserves_sets to_Cantor_from_01_inj]
      by(simp add: measurable_isomorphic_def)
  qed
  have 1:"Cantor_space measurable_isomorphic (ΠM (i::nat,j::nat) UNIV × UNIV. restrict_space borel {0,1::real})"
    unfolding Cantor_space_def
    by(auto intro!: measurable_isomorphic_sym[OF countable_infinite_isomorphisc_to_nat_index] simp: split_beta' finite_prod)
  have 2:"(ΠM (i::nat,j::nat) UNIV × UNIV. restrict_space borel {0,1::real}) measurable_isomorphic (ΠM (i::nat) UNIV. Cantor_space)"
    unfolding Cantor_space_def by(rule measurable_isomorphic_sym[OF PiM_PiM_isomorphic_to_PiM])
  have 3:"(ΠM (i::nat) UNIV. Cantor_space) measurable_isomorphic Hilbert_cube"
    unfolding Hilbert_cube_def by(rule measurable_isomorphic_lift_product[OF Cantor_space_isomorphic_to_01closed])
  show ?thesis
    by(rule measurable_isomorphic_trans[OF measurable_isomorphic_trans[OF 1 2] 3])
qed

subsection ‹ Final Results ›
lemma(in standard_borel) embedding_into_Hilbert_cube:
 "A  sets Hilbert_cube. M measurable_isomorphic (restrict_space Hilbert_cube A)"
proof -
  obtain S where S:"Polish_space S" "sets (borel_of S) = sets M"
    using Polish_space by blast
  obtain A where A:"gdelta_in Hilbert_cube_topology A" "S homeomorphic_space subtopology Hilbert_cube_topology A"
    using embedding_into_Hilbert_cube_gdelta_in[OF S(1)] by blast
  show ?thesis
    using borel_of_gdelta_in[OF A(1)] homeomorphic_space_measurable_isomorphic[OF A(2)]  measurable_isomorphic_sets_cong[OF S(2),of "borel_of (subtopology Hilbert_cube_topology A)" "restrict_space Hilbert_cube A"] Hilbert_cube_borel sets_restrict_space_cong[OF Hilbert_cube_borel]
    by(auto intro!: bexI[where x=A] simp: borel_of_subtopology)
qed

lemma(in standard_borel) embedding_from_Cantor_space:
  assumes "uncountable (space M)"
  shows "A  sets M. Cantor_space measurable_isomorphic (restrict_space M A)"
proof -
  obtain S where S:"Polish_space S" "sets (borel_of S) = sets M"
    using Polish_space by blast
  then obtain A where A:"gdelta_in S A" "Cantor_space_topology homeomorphic_space subtopology S A"
    using embedding_from_Cantor_space[of S] assms sets_eq_imp_space_eq[OF S(2)]
    by(auto simp: space_borel_of)
  show ?thesis
    using borel_of_gdelta_in[OF A(1)] S(2) homeomorphic_space_measurable_isomorphic[OF A(2)] measurable_isomorphic_sets_cong[OF Cantor_space_borel restrict_space_sets_cong[OF refl S(2)],of A]
    by(auto intro!: bexI[where x=A] simp: borel_of_subtopology)
qed

corollary(in standard_borel) uncountable_isomorphic_to_Hilbert_cube:
  assumes "uncountable (space M)"
  shows "Hilbert_cube measurable_isomorphic M"
proof -
  obtain A B where AB:
   "M measurable_isomorphic (restrict_space Hilbert_cube A)" "Cantor_space measurable_isomorphic (restrict_space M B)"
   "A  sets Hilbert_cube""B  sets M" 
    using embedding_into_Hilbert_cube embedding_from_Cantor_space[OF assms] by auto
  show ?thesis
    by(rule measurable_isomorphic_antisym[OF AB measurable_isomorphic_sym[OF Cantor_space_isomorphic_to_Hilbert_cube]])
qed

corollary(in standard_borel) uncountable_isomorphic_to_real:
  assumes "uncountable (space M)"
  shows "M measurable_isomorphic (borel :: real measure)"
proof -
  interpret r: standard_borel_ne "borel :: real measure"
    by simp
  show ?thesis
    by(auto intro!: measurable_isomorphic_trans[OF measurable_isomorphic_sym[OF uncountable_isomorphic_to_Hilbert_cube[OF assms]] r.uncountable_isomorphic_to_Hilbert_cube] simp: uncountable_UNIV_real)
qed

lemma(in standard_borel) isomorphic_subset_real:
  assumes "A  sets (borel :: real measure)" "uncountable A"
  obtains B where "B  sets borel" "B  A" "M measurable_isomorphic restrict_space borel B"
proof(cases "countable (space M)")
  assume count:"countable (space M)"
  have "BA. space M  B"
  proof(cases "finite (space M)")
    assume fin:"finite (space M)"
    then obtain B where B:"card B = card (space M)" "finite B" "B  A"
      by (meson assms(2) countable_finite infinite_arbitrarily_large)
    thus ?thesis
      using fin by(auto intro!: exI[where x=B] simp:eqpoll_iff_card)
  next
    assume inf:"infinite (space M)"
    obtain B where B: "B  A" "countable B" "infinite B"
      using assms(2) countable_finite infinite_countable_subset' that by auto
    thus ?thesis
      using bij_betw_from_nat_into[OF count inf] bij_betw_from_nat_into[OF B(2,3)]
      by (meson eqpoll_def eqpoll_sym eqpoll_trans)
  qed
  then obtain B where B:"B  A" "space M  B" "countable B"
    by (metis countable_eqpoll eqpoll_sym count)
  then obtain f where f:"bij_betw f (space M) B"
    using eqpoll_def by blast
  have 1:"C  sets borel" if C:"C  B" for C
  proof -
    have "C = (cC. {c})"
      by auto
    also have "...  sets borel"
      using B C by(intro sets.countable_UN') (auto simp: countable_subset)
    finally show ?thesis .
  qed
  have 2:"sets M = sets (count_space (space M))"
    by (simp add: countable_discrete_space count)
  have 3:"sets (restrict_space borel B) = sets (count_space B)"
    using 1 by(auto simp: sets_restrict_space)
  have [simp]:"measurable M (restrict_space borel B) = measurable (count_space (space M)) (count_space B)"
    "measurable (restrict_space borel B) M = measurable (count_space B) (count_space (space M))"
    using 2 3 by(auto intro!: measurable_cong_sets)
  have "M measurable_isomorphic restrict_space borel B"
    using bij_betw_the_inv_into[OF f] f by(auto simp: measurable_isomorphic_def measurable_isomorphic_map_def space_restrict_space intro!: exI[where x=f] dest: bij_betwE)
  with 1 B that show ?thesis
    by blast
next
  assume "uncountable (space M)"
  then have "M measurable_isomorphic (borel :: real measure)"
    using uncountable_isomorphic_to_real by blast
  moreover have "restrict_space borel A measurable_isomorphic (borel :: real measure)"
    by(auto intro!: standard_borel.uncountable_isomorphic_to_real standard_borel.standard_borel_restrict_space[OF standard_borel_ne.standard_borel] simp: assms space_restrict_space)
  ultimately have "M measurable_isomorphic restrict_space borel A"
    using measurable_isomorphic_sym measurable_isomorphic_trans by blast
  with assms(1) that show ?thesis
    by blast
qed

lemma(in standard_borel) countable_isomorphic_to_subset_real:
  assumes "countable (space M)"
  obtains A :: "real set"
  where "countable A" "A  sets borel" "M measurable_isomorphic restrict_space borel A"
proof -
  obtain A :: "real set" where A:"A  sets borel" "M measurable_isomorphic restrict_space borel A"
    using isomorphic_subset_real[of UNIV] uncountable_UNIV_real by auto
  moreover have "countable A"
    using measurable_isomorphic_cardinality_eq[OF A(2)] assms(1)
    by(simp add: space_restrict_space countable_eqpoll[OF _ eqpoll_sym])
  ultimately show ?thesis
    using that by blast
qed

theorem Borel_isomorphism_theorem:
  assumes "standard_borel M" "standard_borel N"
  shows "space M  space N  M measurable_isomorphic N"
proof
  assume h:"space M  space N"
  interpret M: standard_borel M by fact
  interpret N: standard_borel N by fact
  consider "countable (space M)" "countable (space N)" | "uncountable (space M)" "uncountable (space N)"
    by (meson countable_eqpoll eqpoll_sym h)
  thus "M measurable_isomorphic N"
  proof cases
    case 1
    then have 2:"sets M = sets (count_space (space M))" "sets N = sets (count_space (space N))"
      by (simp_all add: M.countable_discrete_space N.countable_discrete_space)
    show ?thesis
      by(simp add: measurable_isomorphic_sets_cong[OF 2] measurable_isomorphic_count_spaces h)
  next
    case 2
    then have "M measurable_isomorphic (borel :: real measure)" "N measurable_isomorphic (borel :: real measure)"
      by(simp_all add: M.uncountable_isomorphic_to_real N.uncountable_isomorphic_to_real)
    thus ?thesis
      using measurable_isomorphic_sym measurable_isomorphic_trans by blast
  qed
qed(rule measurable_isomorphic_cardinality_eq)

definition to_real_on :: "'a measure  'a  real" where
"to_real_on M  (if uncountable (space M) then (SOME f. measurable_isomorphic_map M (borel :: real measure) f) else (real  to_nat_on (space M)))"

definition from_real_into :: "'a measure  real  'a" where
"from_real_into M  (if uncountable (space M) then the_inv_into (space M) (to_real_on M) else (λr. from_nat_into (space M) (nat r)))"

context standard_borel
begin

abbreviation "to_real    to_real_on M"
abbreviation "from_real  from_real_into M"

lemma to_real_def_countable:
  assumes "countable (space M)"
  shows "to_real = (λr. real (to_nat_on (space M) r))"
  using assms by(auto simp: to_real_on_def)

lemma from_real_def_countable:
  assumes "countable (space M)"
  shows "from_real = (λr. from_nat_into (space M) (nat r))"
  using assms by(simp add: from_real_into_def)

lemma from_real_to_real[simp]:
  assumes "x  space M"
  shows "from_real (to_real x) = x"
proof -
  have [simp]: "space M  {}"
    using assms by auto
  consider "countable (space M)" | "uncountable (space M)" by auto
  then show ?thesis
  proof cases
    case 1
    then show ?thesis
      by(simp add: to_real_def_countable from_real_def_countable assms)
  next
    case 2
    then obtain f where f: "measurable_isomorphic_map M (borel :: real measure) f"
      using uncountable_isomorphic_to_real by(auto simp: measurable_isomorphic_def)
    have 1:"to_real = Eps (measurable_isomorphic_map M borel)" "from_real = the_inv_into (space M) (Eps (measurable_isomorphic_map M borel))"
      by(simp_all add: to_real_on_def 2 from_real_into_def)
    show ?thesis
      unfolding 1
      by(rule someI2[of "measurable_isomorphic_map M (borel :: real measure)" f,OF f])
        (meson assms bij_betw_imp_inj_on measurable_isomorphic_map_def the_inv_into_f_f)
  qed
qed

lemma to_real_measurable[measurable]:
 "to_real  M M borel"
proof(cases "countable (space M)")
  case 1:True
  then have "sets M = Pow (space M)"
    by(rule countable_discrete_space)
  then show ?thesis
    by(simp add: to_real_def_countable 1 borel_measurableI_le)
next
  case 1:False
  then obtain f where f: "measurable_isomorphic_map M (borel :: real measure) f"
    using uncountable_isomorphic_to_real by(auto simp: measurable_isomorphic_def)
  have 2:"to_real = Eps (measurable_isomorphic_map M borel)"
    by(simp add: to_real_on_def 1 from_real_into_def)
  show ?thesis
    unfolding 2
    by(rule someI2[of "measurable_isomorphic_map M (borel :: real measure)" f,OF f],simp add: measurable_isomorphic_map_def)
qed

lemma from_real_measurable':
  assumes "space M  {}"
  shows "from_real  borel M M"
proof(cases "countable (space M)")
  case 1:True
  then have 2:"sets M = Pow (space M)"
    by(rule countable_discrete_space)
  have [measurable]:"from_nat_into (space M)  count_space UNIV M M"
    using from_nat_into[OF assms] by auto
  show ?thesis
    by(simp add: from_real_def_countable 1 borel_measurableI_le)
next
  case 2:False
  then obtain f where f: "measurable_isomorphic_map M (borel :: real measure) f"
    using uncountable_isomorphic_to_real by(auto simp: measurable_isomorphic_def)
  have 1: "from_real = the_inv_into (space M) (Eps (measurable_isomorphic_map M borel))"
    by(simp add: to_real_on_def 2 from_real_into_def)
  show ?thesis
    unfolding 1
    by(rule someI2[of "measurable_isomorphic_map M (borel :: real measure)" f,OF f],simp add: measurable_isomorphic_map_def)
qed

lemma to_real_from_real:
  assumes "uncountable (space M)"
  shows "to_real (from_real r) = r"
proof -
  obtain f where f: "measurable_isomorphic_map M (borel :: real measure) f"
    using assms uncountable_isomorphic_to_real by(auto simp: measurable_isomorphic_def)
  have 1:"to_real = Eps (measurable_isomorphic_map M borel)" "from_real = the_inv_into (space M) (Eps (measurable_isomorphic_map M borel))"
    by(simp_all add: to_real_on_def assms from_real_into_def)
  show ?thesis
    unfolding 1
    by(rule someI2[of "measurable_isomorphic_map M (borel :: real measure)" f,OF f])
      (metis UNIV_I f_the_inv_into_f_bij_betw measurable_isomorphic_map_def space_borel)
qed

end

lemma(in standard_borel_ne) from_real_measurable[measurable]: "from_real  borel M M"
  by(simp add: from_real_measurable' space_ne)

end