diff --git a/thys/Standard_Borel_Spaces/StandardBorel.thy b/thys/Standard_Borel_Spaces/StandardBorel.thy --- a/thys/Standard_Borel_Spaces/StandardBorel.thy +++ b/thys/Standard_Borel_Spaces/StandardBorel.thy @@ -1,1479 +1,1525 @@ (* 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 \\<^sub>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 \\<^sub>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 \\<^sub>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 (\\<^sub>M i\I. 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 (\\<^sub>M i\I. M i) = sets (\\<^sub>M i\I. 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 (\\<^sub>M i\I. 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 (\\<^sub>M i\I. 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 ereal_standard_ne: "standard_borel_ne (borel :: ereal measure)" proof - interpret s: standard_borel_ne "restrict_space borel {0..1::real}" by auto define f :: "real \ ereal" where "f \ (\r. if r = 0 then bot else if r = 1 then top else tan (pi * r - (pi / 2)))" define g :: "ereal \ real" where "g \ (\r. if r = top then 1 else if r = bot then 0 else arctan (real_of_ereal r) / pi + 1 / 2)" show ?thesis proof(rule s.measurable_isomorphic_standard_ne[OF measurable_isomorphic_byWitness[where f=f and g = g]]) show "f \ borel_measurable (restrict_space borel {0..1})" proof - have 1:"{0..1} \ {r. r \ 0} \ {x. x \ 1} = {0<..<1::real}" by auto have 2:"(\x. ereal (tan (pi * x - pi / 2))) \ borel_measurable (restrict_space borel ({0..1} \ {r. r \ 0} \ {x. x \ 1}))" unfolding 1 proof(safe intro!: borel_measurable_continuous_on_restrict continuous_on_ereal Transcendental.continuous_on_tan) show "continuous_on {0<..<1} (\x::real. pi * x - pi / 2)" by(auto intro!: continuous_at_imp_continuous_on) next fix x :: real assume h:"cos (pi * x - pi / 2) = 0" "x \ {0<..<1}" hence "- (pi / 2) < pi * x - pi / 2" "pi * x - pi / 2 < pi / 2" by simp_all from cos_gt_zero_pi[OF this] h(1) show False by simp qed have "{r:: real. r = 0 \ 0 \ r \ r \ 1} \ sets (restrict_space borel {0..1})" "{x::real. x = 1 \ 0 \ x \ x \ 1 \ x \ 0} \ sets (restrict_space borel ({0..1} \ {r. r \ 0}))" by(auto simp: sets_restrict_space) with 2 show ?thesis by(auto intro!: measurable_If_restrict_space_iff[THEN iffD2] simp: restrict_restrict_space f_def) qed next show "g \ borel \\<^sub>M restrict_space borel {0..1}" unfolding g_def measurable_restrict_space2_iff proof safe fix x :: ereal have "-1 / 2 < arctan (real_of_ereal x) / pi" "arctan (real_of_ereal x) / pi < 1 / 2" using arctan_lbound[of "real_of_ereal x"] arctan_ubound[of "real_of_ereal x"] by (simp_all add: mult_imp_less_div_pos) hence "0 \ arctan (real_of_ereal x) / pi + 1 / 2" "arctan (real_of_ereal x) / pi + 1 / 2 \ 1" by linarith+ thus "(if x = \ then 1 else if x = \ then 0 else arctan (real_of_ereal x) / pi + 1 / 2) \ {0..1}" by auto qed measurable next fix r ::real assume "r \ space (restrict_space borel {0..1})" then consider "r = 0" | "r = 1" | "0 < r" "r < 1" by auto linarith then show " g (f r) = r" proof cases case 3 then have 1:"- (pi / 2) < pi * r - pi / 2" "pi * r - pi / 2 < pi / 2" by simp_all have "arctan (tan (pi * r - pi / 2)) / pi + 1 / 2 = r" by(simp add: arctan_tan[OF 1] diff_divide_distrib) thus ?thesis by(auto simp: f_def g_def top_ereal_def bot_ereal_def) qed(auto simp: g_def f_def top_ereal_def bot_ereal_def) next fix y :: ereal consider "y = top" | "y = bot" | "y \ bot" "y \ top" by auto then show "f (g y) = y" proof cases case 3 hence [simp]: "\y\ \ \" by(auto simp: top_ereal_def bot_ereal_def) have "-1 / 2 < arctan (real_of_ereal y) / pi" "arctan (real_of_ereal y) / pi < 1 / 2" using arctan_lbound[of "real_of_ereal y"] arctan_ubound[of "real_of_ereal y"] by (simp_all add: mult_imp_less_div_pos) hence "arctan (real_of_ereal y) / pi + 1 / 2 < 1" "arctan (real_of_ereal y) / pi + 1 / 2 > 0" by linarith+ thus ?thesis using arctan_lbound[of "real_of_ereal y"] arctan_ubound[of "real_of_ereal y"] by(auto simp: f_def g_def distrib_left tan_arctan ereal_real') qed(auto simp: f_def g_def) qed qed corollary ennreal_stanndard_ne: "standard_borel_ne (borel :: ennreal measure)" by(auto intro!: standard_borel_ne.measurable_isomorphic_standard_ne[OF standard_borel_ne.standard_borel_ne_restrict_space[OF ereal_standard_ne,of "{0..}",simplified]] measurable_isomorphic_byWitness[where f=e2ennreal and g=enn2ereal] measurable_restrict_space1 measurable_restrict_space2 enn2ereal_e2ennreal) text \ Cantor space $\mathscr{C}$ \ definition Cantor_space :: "(nat \ real) measure" where "Cantor_space \ (\\<^sub>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 (\\<^sub>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 \ (\\<^sub>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 (\\<^sub>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 = (\\<^sub>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 \\<^sub>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 \\<^sub>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 (\\<^sub>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 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" using \\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(\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)\) + (\mx 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 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. \x\space 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 \\<^sub>E {0, 1}" using y by(fastforce simp: pd.Product_metric.limit_metric_sequentially) with \\n. xn n \ {0..1}\ show "\N. \n\N. 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) \\<^sub>E {0, 1::real}" by simp show "\\>0. \y\mspace 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) \\<^sub>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 \\<^sub>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} \\<^sub>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 r" "r - (\i (1/2)^(Suc n) \ r - (\i r - (\i {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. \i2^(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 * (\k2^(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 r" and "r - (\i (1/2)^(Suc n) \ r - (\i r - (\ii r" "r - (\i (1/2)^n" "to_Cantor_from_01 r n = 1 \ (1/2)^(Suc n) \ r - (\i r - (\i {0..1}" for r n proof - have nsum:"(\i{0..<1}" using assms by fastforce hence "(\i r \ r - (\i (1/2)^n \ (to_Cantor_from_01 r n = 1 \ (1/2)^(Suc n) \ r - (\i (to_Cantor_from_01 r n = 0 \ r - (\ii r" and "r - (\i (1/2)^n" and "to_Cantor_from_01 r n = 1 \ (1/2)^(Suc n) \ r - (\i r - (\in. (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 (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. \n\no. (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': "(\im. (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.\k\n. to_Cantor_from_01 r k = 0" if assms:"r \ {0..<1}" for r proof(rule ccontr) assume "\ (\n.\k\n. 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 \ (\k\i. to_Cantor_from_01 r k = 1)}" have n0in: "n0 \ {i. i \ n0 \ (\k\i. 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 \ (\k\i. 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 \ (\k\i. 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 \ (\k\i. to_Cantor_from_01 r k = 1)}" n'] by(simp add: n_def) thus False using eqn by simp qed hence le1:"r - (\iim. (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.\k\n. 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 - (\in. (1/2)^(Suc (n + x))* a (n + x))" (is "?lhs = ?rhs") proof - have "?lhs = (\n. (1 / 2) ^ Suc (n + x) * a (n + x)) + (\iin. (1 / 2) ^ (Suc n) * a n" x] by simp also have "... = (\n. (1 / 2) ^ Suc (n + x) * a (n + x)) + (\iin. (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 \\<^sub>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 \\<^sub>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:"(\\<^sub>E i\ UNIV. {0,1}) - ?A \ sets Cantor_space" proof - have eq1:"?A = {\n. 1} \ {x. (\n. x n \ {0,1}) \ (\n. \k\n. x k = 0)}" proof show "?A \ {\n. 1} \ {x. (\n. x n \ {0, 1}) \ (\n. \k\n. 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. \k\n. 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. \k\n. x k = 0)} \ ?A" proof fix x :: "nat \ real" assume "x \ {\n. 1} \ {x. (\n. x n \ {0,1}) \ (\n. \k\n. x k = 0)}" then consider "x = (\n. 1)" | "(\n. x n \ {0,1}) \ (\n. \k\n. 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 "(\\<^sub>E i\ UNIV. {0,1}) - ?A = {x. (\n. x n \ {0,1}) \ (\n. \k\n. x k = 1)} - {\n. 1}" proof show "(\\<^sub>E i\ UNIV. {0,1}) - ?A \ {x. (\n. x n \ {0,1}) \ (\n. \k\n. x k = 1)} - {\n. 1}" proof fix x :: "nat \ real" assume "x \ (\\<^sub>E i\ UNIV. {0,1}) - ?A" then have "\n. x n \ {0,1}" "\ (\n. \k\n. x k = 0)" "x \ (\n. 1)" using eq1 by blast+ thus "x \ {x. (\n. x n \ {0,1}) \ (\n. \k\n. x k = 1)} - {\n. 1}" by blast qed next show "(\\<^sub>E i\ UNIV. {0,1}) - ?A \ {x. (\n. x n \ {0,1}) \ (\n. \k\n. x k = 1)} - {\n. 1}" proof fix x :: "nat \ real" assume h:"x \ {x. (\n. x n \ {0,1}) \ (\n. \k\n. x k = 1)} - {\n. 1}" then have "\n. x n \ {0,1}" "\n. \k\n. x k = 1" "x \ (\n. 1)" by blast+ hence "\ (\n. \k\n. x k = 0)" by fastforce with \\n. x n \ {0,1}\ \x \ (\n. 1)\ show "x \ (\\<^sub>E i\ UNIV. {0,1}) - ?A" using eq1 by blast qed qed also have "... = (\ ((\n. {x. (\n. x n \ {0,1}) \ (\k\n. 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) \ (\k\m. x k = 1)}" for m :: nat proof - let ?C = "{x::nat \ real. (\n. x n = 0 \ x n = 1) \ (\k\m. x k = 1)}" define g where "g = (\(x::nat \ real) n. if n < m then x n else undefined)" have 1:"g ` ?C = (\\<^sub>E i \{.. g ` ?C" then show "x \ (\\<^sub>E i \{.. (\\<^sub>E i \{..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) \ (\k\m. 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 - ((\\<^sub>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 (\\<^sub>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:"(\\<^sub>M (i::nat,j::nat)\ UNIV \ UNIV. restrict_space borel {0,1::real}) measurable_isomorphic (\\<^sub>M (i::nat)\ UNIV. Cantor_space)" unfolding Cantor_space_def by(rule measurable_isomorphic_sym[OF PiM_PiM_isomorphic_to_PiM]) have 3:"(\\<^sub>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 "\B\A. 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 = (\c\C. {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 \\<^sub>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 \\<^sub>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 \\<^sub>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 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(cases "space M = {}") - case True - then show ?thesis - by (meson countable_empty measurable_isomorphic_empty sets.empty_sets space_restrict_space2 that) -next - case nin:False - define A where "A \ to_real ` (space M)" - have "countable A" "A \ sets borel" "M measurable_isomorphic (restrict_space borel A)" - proof - - show "countable A" "A \ sets borel" - using assms(1) standard_borel.countable_sets[of borel A] standard_borel_ne_borel by(auto simp: A_def standard_borel_ne_def) - show "M measurable_isomorphic restrict_space borel A" - using from_real_to_real A_def \A \ sets borel\ - by(auto intro!: measurable_isomorphic_byWitness[OF measurable_restrict_space2[OF _ to_real_measurable] _ measurable_restrict_space1[OF from_real_measurable'[OF nin]]]) - qed - with that show ?thesis - by auto -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 \\<^sub>M M" by(simp add: from_real_measurable' space_ne) end \ No newline at end of file