diff --git a/thys/Standard_Borel_Spaces/Abstract_Metrizable_Topology.thy b/thys/Standard_Borel_Spaces/Abstract_Metrizable_Topology.thy --- a/thys/Standard_Borel_Spaces/Abstract_Metrizable_Topology.thy +++ b/thys/Standard_Borel_Spaces/Abstract_Metrizable_Topology.thy @@ -1,1004 +1,1395 @@ (* Title: Abstract_Metrizable_Topology.thy Author: Michikazu Hirata, Tokyo Institute of Technology *) section \Abstract Polish Spaces \ theory Abstract_Metrizable_Topology imports "Set_Based_Metric_Product" begin subsection \ Polish Spaces \ definition "polish_space X \ completely_metrizable_space X \ separable_space X" lemma(in Metric_space) polish_space_mtopology: assumes mcomplete "separable_space mtopology" shows "polish_space mtopology" by (simp add: assms completely_metrizable_space_mtopology polish_space_def) lemma assumes "polish_space X" shows polish_space_imp_completely_metrizable_space: "completely_metrizable_space X" and polish_space_imp_metrizable_space: "metrizable_space X" and polish_space_imp_second_countable: "second_countable X" and polish_space_imp_separable_space: "separable_space X" using assms by(auto simp: completely_metrizable_imp_metrizable_space polish_space_def metrizable_space_separable_iff_second_countable) lemma polish_space_closedin: assumes "polish_space X" "closedin X A" shows "polish_space (subtopology X A)" using assms by(auto simp: completely_metrizable_imp_metrizable_space polish_space_def completely_metrizable_space_closedin second_countable_subtopology metrizable_space_separable_iff_second_countable) lemma polish_space_gdelta_in: assumes "polish_space X" "gdelta_in X A" shows "polish_space (subtopology X A)" using assms by(auto simp: completely_metrizable_imp_metrizable_space polish_space_def completely_metrizable_space_gdelta_in second_countable_subtopology metrizable_space_separable_iff_second_countable) corollary polish_space_openin: assumes "polish_space X" "openin X A" shows "polish_space (subtopology X A)" by (simp add: open_imp_gdelta_in assms polish_space_gdelta_in) lemma homeomorphic_polish_space_aux: assumes "polish_space X" "X homeomorphic_space Y" shows "polish_space Y" using assms by(simp add: homeomorphic_completely_metrizable_space_aux homeomorphic_separable_space polish_space_def) corollary homeomorphic_polish_space: assumes "X homeomorphic_space Y" shows "polish_space X \ polish_space Y" by (meson assms homeomorphic_polish_space_aux homeomorphic_space_sym) lemma polish_space_euclidean[simp]: "polish_space (euclidean :: ('a :: polish_space) topology)" by (simp add: completely_metrizable_space_euclidean polish_space_def second_countable_imp_separable_space) lemma polish_space_countable[simp]: "polish_space (euclidean :: 'a :: {countable,discrete_topology} topology)" proof - interpret discrete_metric "UNIV :: 'a set" . have [simp]:"euclidean = disc.mtopology" by (metis discrete_topology_class.open_discrete discrete_topology_unique istopology_open mtopology_discrete_metric topology_inverse' topspace_euclidean) show ?thesis by(auto simp: polish_space_def intro!: disc.completely_metrizable_space_mtopology mcomplete_discrete_metric countable_space_separable_space) qed lemma polish_space_discrete_topology: "polish_space (discrete_topology I) \ countable I" by (simp add: completely_metrizable_space_discrete_topology polish_space_def separable_space_discrete_topology) lemma polish_space_prod: assumes "polish_space X" and "polish_space Y" shows "polish_space (prod_topology X Y)" using assms by (simp add: completely_metrizable_space_prod_topology polish_space_def separable_space_prod) lemma polish_space_product: assumes "countable I" and "\i. i \ I \ polish_space (S i)" shows "polish_space (product_topology S I)" using assms by(auto simp: separable_countable_product polish_space_def completely_metrizable_space_product_topology) lemma(in Product_metric) polish_spaceI: assumes "\i. i \ I \ separable_space (Metric_space.mtopology (Mi i) (di i))" and "\i. i \ I \ Metric_space.mcomplete (Mi i) (di i)" shows "polish_space Product_metric.mtopology" using assms I by(auto simp: polish_space_def Product_metric_mtopology_eq[symmetric] completely_metrizable_space_product_topology intro!: separable_countable_product Metric_space.completely_metrizable_space_mtopology Md_metric) lemma(in Sum_metric) polish_spaceI: assumes "countable I" and "\i. i \ I \ separable_space (Metric_space.mtopology (Mi i) (di i))" and "\i. i \ I \ Metric_space.mcomplete (Mi i) (di i)" shows "polish_space Sum_metric.mtopology" by(auto simp: polish_space_def intro!: separable_Mi_separable_M assms mcomplete_Mi_mcomplete_M Sum_metric.completely_metrizable_space_mtopology) lemma compact_metrizable_imp_polish_space: assumes "metrizable_space X" "compact_space X" shows "polish_space X" proof - obtain d where "Metric_space (topspace X) d" "Metric_space.mtopology (topspace X) d = X" by (metis assms(1) Metric_space.topspace_mtopology metrizable_space_def) thus ?thesis by (metis Metric_space.compact_space_imp_separable assms(1) assms(2) compact_imp_locally_compact_space locally_compact_imp_completely_metrizable_space polish_space_def) qed +subsection \ Extended Reals and Non-Negative Extended Reals \ +lemma polish_space_ereal:"polish_space (euclidean :: ereal topology)" +proof(rule homeomorphic_polish_space_aux) + show "polish_space (subtopology euclideanreal {-1..1})" + by (auto intro!: polish_space_closedin) +next + define f :: "real \ ereal" + where "f \ (\r. if r = - 1 then - \ else if r = 1 then \ else if r \ 0 then ereal (1 - (1 / (1 + r))) else ereal ((1 / (1 - r)) - 1))" + define g :: "ereal \ real" + where "g \ (\r. if r \ 0 then real_of_ereal (inverse (1 - r)) - 1 else 1 - real_of_ereal (inverse (1 + r)))" + show "top_of_set {-1..1::real} homeomorphic_space (euclidean :: ereal topology)" + unfolding homeomorphic_space_def homeomorphic_maps_def continuous_map_iff_continuous + proof(safe intro!: exI[where x=f] exI[where x=g]) + show "continuous_on {- 1..1} f" + unfolding continuous_on_eq_continuous_within + proof safe + fix x :: real + assume "x \ {- 1..1}" + then consider "x = -1" | "-1 < x" "x < 0" | "x = 0" | "0 < x" "x < 1" | "x = 1" + by fastforce + then show "continuous (at x within {- 1..1}) f" + proof cases + show "- 1 < x \ x < 0 \ ?thesis" + by(simp add: at_within_Icc_at, intro isCont_cong[where f="\r. ereal (1 - (1 / (1 + r)))" and g=f,THEN iffD1,OF _ continuous_on_interior[of "{-1<..<0}"]]) (auto simp: at_within_Icc_at eventually_nhds f_def intro!: exI[where x="{-1<..<0}"] continuous_on_divide continuous_on_ereal continuous_on_diff continuous_on_add) + next + have *:"isCont (\r. if r \ 0 then ereal (1 - (1 / (1 + r))) else ereal ((1 / (1 - r)) - 1)) 0" + by(rule isCont_If_ge) (auto simp add: continuous_within intro!: continuous_on_Icc_at_leftD[where a="- (1 / 2)" and b=0 and f="\r::real. 1 - (1 / (1 + r))",simplified] continuous_on_Icc_at_rightD[where a=0 and b="1 / 2" and f="\r::real. (1 / (1 - r)) - 1",simplified] continuous_on_diff continuous_on_divide continuous_on_add) + show ?thesis if x:"x = 0" + unfolding x at_within_Icc_at[of "- 1 :: real" 0 1,simplified] + by(rule isCont_cong[THEN iffD1,OF _ *]) (auto simp: eventually_nhds f_def intro!: exI[where x="{-1 / 2<..<1/2}"]) + next + show "0 < x \ x < 1 \ ?thesis" + by(simp add: at_within_Icc_at, intro isCont_cong[where f="\r. ereal ((1 / (1 - r)) - 1)" and g=f,THEN iffD1,OF _ continuous_on_interior[of "{0<..<1}"]]) (auto simp: at_within_Icc_at eventually_nhds f_def intro!: exI[where x="{0<..<1}"] continuous_on_divide continuous_on_ereal continuous_on_diff continuous_on_add) + next + show ?thesis if x:"x = -1" + unfolding x at_within_Icc_at_right[where a="- 1 :: real" and b=1,simplified] continuous_within ereal_tendsto_simps(2)[symmetric] + proof(subst tendsto_cong) + show "\\<^sub>F r in at_right (ereal (- 1)). (f \ real_of_ereal) r = 1 - (1 / (1 + r))" + unfolding eventually_at_right[of "ereal (- 1)" 0,simplified] + proof(safe intro!: exI[where x="ereal (- 1 / 2)"]) + fix y + assume "ereal (- 1) < y" "y < ereal (- 1 / 2)" + then obtain y' where y':"y = ereal y'" "- 1 < y'" "y' < - 1 / 2" + by (metis ereal_real' less_ereal.simps(1) not_inftyI) + show "(f \ real_of_ereal) y = 1 - 1 / (1 + y)" + using y'(2,3) by(auto simp add: y'(1) f_def one_ereal_def) + qed simp + next + have "((\r. 1 - 1 / (1 + r)) \ - \) (at_right (ereal (- 1)))" + unfolding tendsto_MInfty + proof safe + fix r :: real + consider "r \ 1" | "r < 1" + by argo + then show "\\<^sub>F x in at_right (ereal (- 1)). 1 - 1 / (1 + x) < ereal r" + proof cases + case [arith]:1 + show ?thesis + unfolding eventually_at_right[of "ereal (- 1)" 0,simplified] + proof(safe intro!: exI[where x=0]) + fix y + assume "ereal (- 1) < y" "y < 0" + then obtain y' where y':"y = ereal y'" "- 1 < y'" "y' < 0" + using not_inftyI by force + then have *:"1 - 1 / (1 + y) < 1" + by (simp add: one_ereal_def) + show "1 - 1 / (1 + y) < ereal r" + by(rule order.strict_trans2[OF *]) (use 1 in auto) + qed simp + next + case 2 + show ?thesis + unfolding eventually_at_right[of "ereal (- 1)" 0,simplified] + proof(safe intro!: exI[where x="ereal (1 / (1 - r) - 1)"]) + fix y + assume " ereal (- 1) < y" "y < ereal (1 / (1 - r) - 1)" + then obtain y' where y':"y = ereal y'" "- 1 < y'" "y' < 1 / (1 - r) - 1" + by (metis ereal_less_eq(3) ereal_real' linorder_not_le not_inftyI) + have "1 - 1 / (1 + y) = ereal (1 - 1 / (1 + y'))" + by (metis ereal_divide ereal_minus(1) one_ereal_def order_less_irrefl plus_ereal.simps(1) real_0_less_add_iff y'(1) y'(2)) + also have "... < ereal r" + proof - + have "1 + y' < 1 / (1 - r)" + using y' by simp + hence "1 - r < 1 / (1 + y')" + using y' 2 by (simp add: less_divide_eq mult.commute) + thus ?thesis + by simp + qed + finally show "1 - 1 / (1 + y) < ereal r" . + qed(use 2 in auto) + qed + qed + thus "((\r. 1 - 1 / (1 + r)) \ f (- 1)) (at_right (ereal (- 1)))" + by(simp add: f_def) + qed + next + show ?thesis if x:"x = 1" + unfolding x at_within_Icc_at_left[where a="- 1 :: real" and b=1,simplified] continuous_within ereal_tendsto_simps(1)[symmetric] + proof(subst tendsto_cong) + show "\\<^sub>F r in at_left (ereal 1). (f \ real_of_ereal) r = (1 / (1 - r)) - 1" + unfolding eventually_at_left[of 0 "ereal 1",simplified] + proof(safe intro!: exI[where x="ereal (1 / 2)"]) + fix y + assume "ereal (1 / 2) < y" "y < ereal 1" + then obtain y' where y':"y = ereal y'" "1 / 2 < y'" "y' < 1" + using ereal_less_ereal_Ex by force + show "(f \ real_of_ereal) y = 1 / (1 - y) - 1" + using y'(2,3) by(auto simp add: y'(1) f_def one_ereal_def) + qed simp + next + have "((\r. (1 / (1 - r)) - 1) \ \) (at_left (ereal 1))" + unfolding tendsto_PInfty + proof safe + fix r :: real + consider "r \ - 1" | "- 1 < r" + by argo + then show "\\<^sub>F x in at_left (ereal 1). (1 / (1 - x)) - 1 > ereal r" + proof cases + case [arith]:1 + show ?thesis + unfolding eventually_at_left[of 0 "ereal 1",simplified] + proof(safe intro!: exI[where x=0]) + fix y + assume "0 < y" "y < ereal 1" + then obtain y' where y':"y = ereal y'" "0 < y'" "y' < 1" + using not_inftyI by force + then have *:"(1 / (1 - y)) - 1 > ereal (- 1)" + by (simp add: one_ereal_def) + show "ereal r < 1 / (1 - y) - 1" + by(rule order.strict_trans1[OF _ *]) (use 1 in auto) + qed simp + next + case 2 + show ?thesis + unfolding eventually_at_left[of 0 "ereal 1",simplified] + proof(safe intro!: exI[where x="ereal (1 - 1 / (1 + r))"]) + fix y + assume "ereal (1 - 1 / (1 + r)) < y" "y < ereal 1" + then obtain y' where y':"y = ereal y'" "1 - 1 / (1 + r) < y'" "y' < 1" + by (metis ereal_less_eq(3) ereal_real' linorder_not_le not_inftyI) + have "ereal r < ereal (1 / (1 - y') - 1)" + proof - + have "1 - y' < 1 / (r + 1)" + using y'(2) by argo + hence "r + 1 < 1 / (1 - y')" + using y' 2 by (simp add: less_divide_eq mult.commute) + thus ?thesis + by simp + qed + also have "... = 1 / (1 - y) - 1" + by (metis diff_gt_0_iff_gt ereal_divide ereal_minus(1) less_numeral_extra(3) one_ereal_def y'(1) y'(3)) + finally show "ereal r < 1 / (1 - y) - 1" . + qed(use 2 in auto) + qed + qed + thus " ((\r. 1 / (1 - r) - 1) \ f 1) (at_left (ereal 1))" + by(simp add: f_def) + qed + qed + qed + next + show "continuous_map euclidean (top_of_set {- 1..1}) g" + proof(safe intro!: continuous_map_into_subtopology) + show "continuous_map euclidean euclideanreal g" + unfolding Abstract_Topology.continuous_map_iff_continuous2 continuous_on_eq_continuous_within + proof safe + fix x :: ereal + consider "x = - \" | "- \ < x" "x < 0" | "x = 0" | "0 < x" "x < \" | "x = \" + by fastforce + then show "isCont g x" + proof cases + assume x:"- \ < x" "x < 0" + then obtain x' where x':"x = ereal x'" "x' < 0" + by (metis ereal_infty_less(2) ereal_less_ereal_Ex zero_ereal_def) + show ?thesis + proof(subst isCont_cong) + have [simp]:"isCont ((-) 1) x" + proof - + have *:"isCont (\x. ereal (real_of_ereal 1 - real_of_ereal x)) x" + using x' by(auto simp add: continuous_at_iff_ereal[symmetric,simplified comp_def] intro!: continuous_diff continuous_at_of_ereal) + have **: "ereal (x' - 1) < x \ x < 0 \ ereal (1 - real_of_ereal x) = ereal 1 - x" for x + by (metis ereal_minus(1) less_ereal.simps(2) less_ereal.simps(3) real_of_ereal.elims) + show ?thesis + apply(rule isCont_cong[THEN iffD1,OF _ *]) + using x'(2) ** by(auto simp: eventually_nhds x'(1) one_ereal_def intro!: exI[where x="{x-1<..<0}"]) + qed + have *:"abs (1 - x) \ \" " 1 - x \ 0" + using x'(2) by(auto simp add: x'(1) one_ereal_def) + show "isCont (\r. real_of_ereal (inverse (1 - r)) - 1) x" + using x * by(auto intro!: continuous_diff continuous_divide isCont_o2[OF _ continuous_at_of_ereal]) + next + show "\\<^sub>F x in nhds x. g x = real_of_ereal (inverse (1 - x)) - 1" + using x(2) by(auto simp: eventually_nhds x'(1) g_def one_ereal_def intro!: exI[where x="{x-1<..<0}"]) + qed + next + assume x:"\ > x" "x > 0" + then obtain x' where x':"x = ereal x'" "x' > 0" + by (metis ereal_less(2) less_ereal.elims(2) less_ereal.simps(2)) + show ?thesis + proof(subst isCont_cong) + have [simp]: "isCont ((+) 1) x" + proof - + have *:"isCont (\x. ereal (real_of_ereal 1 + real_of_ereal x)) x" + using x' by(auto simp add: continuous_at_iff_ereal[symmetric,simplified comp_def] intro!: continuous_add continuous_at_of_ereal) + have **: " 0 < x \ x < ereal (x' + 1) \ ereal (1 + real_of_ereal x) = ereal 1 + x" for x + using ereal_less_ereal_Ex by auto + show ?thesis + apply(rule isCont_cong[THEN iffD1,OF _ *]) + using x'(2) ** by(auto simp: eventually_nhds x'(1) one_ereal_def intro!: exI[where x="{0<.. 0" + using x' by auto + thus "isCont (\r. 1 - real_of_ereal (inverse (1 + r))) x" + using x by(auto intro!: continuous_diff continuous_divide isCont_o2[OF _ continuous_at_of_ereal]) + next + show "\\<^sub>F x in nhds x. g x = 1 - real_of_ereal (inverse (1 + x))" + using x(2) by(auto simp: eventually_nhds x'(1) g_def one_ereal_def intro!: exI[where x="{0<.." + unfolding x + proof(safe intro!: continuous_at_sequentiallyI) + fix u :: "nat \ ereal" + assume u:"u \ - \" + show "(\n. g (u n)) \ g (- \)" + unfolding LIMSEQ_def + proof safe + fix r :: real + assume r[arith]: "r > 0" + obtain no where no: "\n. n \ no \ u n < ereal (min (1 - 1 / r) 0)" + using u unfolding tendsto_MInfty eventually_sequentially by blast + show "\no. \n\no. dist (g (u n)) (g (- \)) < r" + proof(safe intro!: exI[where x=no]) + fix n + assume n:"n \ no" + have r0:"1 - min (ereal (1 - 1 / r)) (ereal 0) > 0" + by (simp add: ereal_diff_gr0 min.strict_coboundedI2) + have u1:"1 - u n > 0" + by (metis ereal_0_less_1 ereal_diff_gr0 ereal_min linorder_not_le min.strict_coboundedI2 n no order_le_less_trans order_less_not_sym zero_ereal_def) + have "real_of_ereal (inverse (1 - u n)) < r" + proof - + have "real_of_ereal (inverse (1 - u n)) < real_of_ereal (inverse (1 - ereal (min (1 - 1 / r) 0)))" + proof(safe intro!: ereal_less_real_iff[THEN iffD2]) + have "ereal (real_of_ereal (inverse (1 - u n))) = inverse (1 - u n)" + by(rule ereal_real') (use no[OF n] u1 in auto) + also have "... < inverse (1 - ereal (min (1 - 1 / r) 0))" + apply(rule ereal_inverse_antimono_strict) + using no[OF n] apply(simp add: ereal_diff_positive min.coboundedI2) + by (metis (no_types, lifting) no[OF n] ereal_add_uminus_conv_diff ereal_eq_minus_iff ereal_less_minus_iff ereal_minus_less_minus ereal_times(1) ereal_times(3)) + finally show "ereal (real_of_ereal (inverse (1 - u n))) < inverse (1 - ereal (min (1 - 1 / r) 0))" . + qed(use r0 in auto) + also have "... \ r" + by(cases "r \ 1") (auto simp add: real_of_ereal_minus) + finally show "real_of_ereal (inverse (1 - u n)) < r" . + qed + thus "dist (g (u n)) (g (- \)) < r" + using u1 no[OF n] by(auto simp: g_def zero_ereal_def dist_real_def) + qed + qed + qed + next + show "isCont g x" if x:"x = \" + unfolding x + proof(safe intro!: continuous_at_sequentiallyI) + fix u :: "nat \ ereal" + assume u:"u \ \" + show "(\n. g (u n)) \ g \" + unfolding LIMSEQ_def + proof safe + fix r :: real + assume r[arith]: "r > 0" + obtain no where no: "\n. n \ no \ u n > ereal (max (1 / r - 1) 0)" + using u unfolding tendsto_PInfty eventually_sequentially by blast + show "\no. \n\no. dist (g (u n)) (g \) < r" + proof(safe intro!: exI[where x=no]) + fix n + assume n:"n \ no" + have u0: "1 + u n > 0" + using no[OF n] by simp (metis add_nonneg_pos zero_ereal_def zero_less_one_ereal) + have "\- real_of_ereal (inverse (1 + u n))\ < r" + proof - + have "\- real_of_ereal (inverse (1 + u n))\ < \- (inverse (1 + max (1 / r - 1) 0))\" + unfolding abs_real_of_ereal abs_minus + proof(safe intro!: real_less_ereal_iff[THEN iffD2]) + have "\inverse (1 + u n)\ < inverse (1 + ereal (max (1 / r - 1) 0))" + using no[OF n] u0 by (simp add: ereal_add_strict_mono ereal_inverse_antimono_strict inverse_ereal_ge0I le_max_iff_disj order_less_imp_le u0) + also have "... = ereal \inverse (1 + max (1 / r - 1) 0)\" + by(auto simp: abs_ereal.simps(1)[symmetric] ereal_max[symmetric] simp del: abs_ereal.simps(1) ereal_max) + finally show "\inverse (1 + u n)\ < ereal \inverse (1 + max (1 / r - 1) 0)\" . + qed auto + also have "... = inverse (1 + max (1 / r - 1) 0)" + by auto + also have "... \ r" + by(cases "r \ 1") auto + finally show ?thesis . + qed + thus "dist (g (u n)) (g \) < r" + using no[OF n] by(auto simp: g_def dist_real_def zero_ereal_def) + qed + qed + qed + next + show "isCont g x" if x:"x = 0" + unfolding x g_def + proof(safe intro!: isCont_If_ge) + have "((\x. real_of_ereal (1 - x)) \ 1) (at_left 0)" + proof(subst tendsto_cong) + show "((\x. 1 - real_of_ereal x) \ 1) (at_left 0)" + by(auto intro!: tendsto_diff[where a=1 and b=0,simplified] simp: zero_ereal_def) + next + show "\\<^sub>F x in at_left 0. real_of_ereal (1 - x) = 1 - real_of_ereal x" + by(auto simp: eventually_at_left[where y="- 1" and x="0::ereal",simplified] real_of_ereal_minus ereal_uminus_eq_reorder intro!: exI[where x="-1"]) + qed + thus "continuous (at_left 0) (\x. real_of_ereal (inverse (1 - x)) - 1)" + unfolding continuous_within + by (auto intro!: tendsto_diff[where a = 1 and b=1,simplified] tendsto_divide[where a=1 and b=1,simplified]) + next + have "((\x. real_of_ereal (1 + x)) \ 1) (at_right 0)" + proof(subst tendsto_cong) + show "((\x. 1 + real_of_ereal x) \ 1) (at_right 0)" + by(auto intro!: tendsto_add[where a=1 and b=0,simplified] simp: zero_ereal_def) + next + show "\\<^sub>F x in at_right 0. real_of_ereal (1 + x) = 1 + real_of_ereal x" + by(auto simp: eventually_at_right[where y=1 and x="0::ereal",simplified] real_of_ereal_add ereal_uminus_eq_reorder intro!: exI[where x=1]) + qed + thus "((\x. 1 - real_of_ereal (inverse (1 + x))) \ real_of_ereal (inverse (1 - 0)) - 1) (at_right 0)" + by (auto intro!: tendsto_diff[where a = 1 and b=1,simplified] tendsto_divide[where a=1 and b=1,simplified]) + qed + qed + qed + next + fix x :: ereal + consider "x = - \" | "- \ < x" "x \ 0" | "0 < x" "x < \" | "x = \" + by fastforce + then show "g x \ {- 1..1}" + proof cases + assume "- \ < x" "x \ 0" + then obtain x' where "x = ereal x'" "x' \ 0" + by (metis dual_order.refl ereal_less_ereal_Ex order_less_le zero_ereal_def) + then show ?thesis + by(auto simp: g_def real_of_ereal_minus intro!: pos_divide_le_eq[THEN iffD2]) + next + assume "0 < x" "x < \" + then obtain x' where "x = ereal x'" "x' > 0" + by (metis ereal_less(2) less_ereal.elims(2) order_less_le) + then show ?thesis + by(auto simp: g_def real_of_ereal_add inverse_eq_divide intro!: pos_divide_le_eq[THEN iffD2]) + qed(auto simp: g_def) + qed + next + fix x :: ereal + consider "x = - \" | "- \ < x" "x \ 0" | "0 < x" "x < \" | "x = \" + by fastforce + then show "f (g x) = x" + proof cases + assume "- \ < x" "x \ 0" + then obtain x' where x':"x = ereal x'" "x' \ 0" + by (metis dual_order.refl ereal_less_ereal_Ex order_less_le zero_ereal_def) + then have [arith]:"1 / (1 - x') - 1 \ 0" + by simp + show ?thesis + using x' by(auto simp: g_def real_of_ereal_minus f_def) + next + assume "0 < x" "x < \" + then obtain x' where x':"x = ereal x'" "x' > 0" + by (metis ereal_less(2) less_ereal.elims(2) order_less_le) + hence [arith]: "1 - 1 / (x' + 1) \ 0" + by simp + show ?thesis + using x' by(simp add: g_def inverse_eq_divide f_def) + qed(auto simp: f_def g_def) + next + fix x :: real + assume "x \ topspace (top_of_set {- 1..1})" + then consider "x = - 1" | "- 1 < x" "x \ 0" | "0 < x" "x < 1" | "x = 1" + by fastforce + then show "g (f x) = x" + by cases (auto simp: f_def g_def real_of_ereal_minus real_of_ereal_add) + qed +qed + +corollary polish_space_ennreal:"polish_space (euclidean :: ennreal topology)" +proof(rule homeomorphic_polish_space_aux) + show "polish_space (top_of_set {0::ereal..})" + using polish_space_closedin polish_space_ereal by fastforce +next + show "top_of_set {0::ereal..} homeomorphic_space (euclidean :: ennreal topology)" + by(auto intro!: exI[where x=e2ennreal] exI[where x=enn2ereal] simp: homeomorphic_space_def homeomorphic_maps_def enn2ereal_e2ennreal continuous_on_e2ennreal continuous_map_in_subtopology continuous_on_enn2ereal image_subset_iff) +qed + subsection \Continuous Embddings\ abbreviation Hilbert_cube_topology :: "(nat \ real) topology" where "Hilbert_cube_topology \ (product_topology (\n. top_of_set {0..1}) UNIV)" lemma topspace_Hilbert_cube: "topspace Hilbert_cube_topology = (\\<^sub>E x\UNIV. {0..1})" by simp lemma polish_space_Hilbert_cube: "polish_space Hilbert_cube_topology" by(auto intro!: polish_space_closedin polish_space_product) abbreviation Cantor_space_topology :: "(nat \ real) topology" where "Cantor_space_topology \ (product_topology (\n. top_of_set {0,1}) UNIV)" lemma topspace_Cantor_space: "topspace Cantor_space_topology = (\\<^sub>E x\UNIV. {0,1})" by simp lemma polish_space_Cantor_space: "polish_space Cantor_space_topology" by(auto intro!: polish_space_closedin polish_space_product) corollary completely_metrizable_space_homeo_image_gdelta_in: assumes "completely_metrizable_space X" "completely_metrizable_space Y" "B \ topspace Y" "X homeomorphic_space subtopology Y B" shows "gdelta_in Y B" using assms completely_metrizable_space_eq_gdelta_in homeomorphic_completely_metrizable_space by blast subsubsection \ Embedding into Hilbert Cube\ lemma embedding_into_Hilbert_cube: assumes "metrizable_space X" "separable_space X" shows "\A \ topspace Hilbert_cube_topology. X homeomorphic_space (subtopology Hilbert_cube_topology A)" proof - consider "X = trivial_topology" | "topspace X \ {}" by auto then show ?thesis proof cases case 1 then show ?thesis by(auto intro!: exI[where x="{}"] simp: homeomorphic_empty_space_eq) next case S_ne:2 then obtain U where U:"countable U" "dense_in X U" "U \ {}" using assms(2) by(auto simp: separable_space_def2 dense_in_nonempty) obtain xn where xn:"\n::nat. xn n \ U" "U = range xn" by (metis U(1) U(3) from_nat_into range_from_nat_into) then have xns:"xn n \ topspace X" for n using dense_in_subset[OF U(2)] by auto obtain d' where d':"Metric_space (topspace X) d'" "Metric_space.mtopology (topspace X) d' = X" by (metis Metric_space.topspace_mtopology assms(1) metrizable_space_def) interpret ms': Metric_space "topspace X" d' by fact define d where "d = ms'.capped_dist (1/2)" have d: "Metric_space.mtopology (topspace X) d = X" "\x y. d x y < 1" by(simp add: d_def ms'.mtopology_capped_metric d') (simp add: d_def ms'.capped_dist_def) interpret ms: Metric_space "topspace X" d by (simp add: d_def ms'.capped_dist) define f where "f \ (\x n. d x (xn n))" have f_inj:"inj_on f (topspace X)" proof fix x y assume xy:"x \ topspace X" "y \ topspace X" "f x = f y" then have "\n. d x (xn n) = d y (xn n)" by(auto simp: f_def dest: fun_cong) hence d2:"d x y \ 2 * d x (xn n)" for n using ms.triangle[OF xy(1) _ xy(2),of "xn n",simplified ms.commute[of "xn n" y]] dense_in_subset[OF U(2)] xn(1)[of n] by auto have "d x y < \" if "\ > 0" for \ proof - have "0 < \ / 2" using that by simp then obtain n where "d x (xn n) < \ / 2" using ms.mdense_def2[of U,simplified d(1)] U(2) xy(1) xn(2) by blast with d2[of n] show ?thesis by simp qed hence "d x y = 0" by (metis ms.nonneg[of x y] dual_order.irrefl order_neq_le_trans) thus "x = y" using xy by simp qed have f_img: "f ` topspace X \ topspace Hilbert_cube_topology" using d(2) ms.nonneg by(auto simp: topspace_Hilbert_cube f_def less_le_not_le) have f_cont: "continuous_map X Hilbert_cube_topology f" unfolding continuous_map_componentwise_UNIV f_def continuous_map_in_subtopology proof safe show "continuous_map X euclideanreal (\x. d x (xn k))" for k proof(rule continuous_map_eq[of _ _ "mdist_set ms.Self {xn k}"]) show "continuous_map X euclideanreal (mdist_set ms.Self {xn k})" by (metis d(1) mdist_set_uniformly_continuous ms.mdist_Self ms.mspace_Self mtopology_of_def mtopology_of_euclidean uniformly_continuous_imp_continuous_map) next fix x assume "x \ topspace X" then show "mdist_set ms.Self {xn k} x = d x (xn k)" by(auto simp: ms.mdist_set_Self xns) qed next show "d x (xn k) \ {0..1}" for x k using d(2) ms.nonneg by(auto simp: less_le_not_le) qed hence f_cont': "continuous_map X (subtopology Hilbert_cube_topology (f ` topspace X)) f" using continuous_map_into_subtopology by blast obtain g where g: "g ` (f ` topspace X) = topspace X" "\x. x \ topspace X \ g (f x) = x" "\x. x \ f ` topspace X \ f (g x) = x" by (meson f_inj f_the_inv_into_f the_inv_into_f_eq the_inv_into_onto) have g_cont: "continuous_map (subtopology Hilbert_cube_topology (f ` topspace X)) X g" proof - interpret m01: Submetric UNIV dist "{0..1::real}" by(simp add: Submetric_def Submetric_axioms_def Met_TC.Metric_space_axioms) have m01_eq: "m01.sub.mtopology = top_of_set {0..1}" using m01.mtopology_submetric by auto have m01_polish: "polish_space m01.sub.mtopology" by(auto simp: m01_eq intro!: polish_space_closedin) interpret m01': Metric_space "{0..1::real}" "\x y. if 0 \ x \ x \ 1 \ 0 \ y \ y \ 1 then dist x y else 0" by(auto intro!: Metric_space_eq[OF m01.sub.Metric_space_axioms]) metric have m01'_eq: "m01'.mtopology = top_of_set {0..1}" by(auto intro!: Metric_space_eq_mtopology[OF m01.sub.Metric_space_axioms,simplified m01_eq,symmetric]) metric have "dist x y \ 1" "dist x y \ 0" if "x \ 0" "x \ 1" "y \ 0" "y \ 1" for x y :: real using dist_real_def that by auto then interpret ppm: Product_metric "1/2" "UNIV :: nat set" id id "\_. {0..1::real}" "\_ x y. if 0 \ x \ x \ 1 \ 0 \ y \ y \ 1 then dist x y else 0" 1 by(auto intro!: product_metric_natI Metric_space_eq[OF m01.sub.Metric_space_axioms] simp: m01.sub.commute) have Hilbert_cube_eq: "ppm.Product_metric.mtopology = Hilbert_cube_topology" by(simp add: ppm.Product_metric_mtopology_eq[symmetric] m01'_eq) interpret f_S: Submetric "\\<^sub>E x\UNIV. {0..1}" ppm.product_dist "f ` topspace X" by(auto simp: Submetric_def ppm.Product_metric.Metric_space_axioms Submetric_axioms_def f_def order.strict_implies_order[OF d(2)]) have 1:"subtopology Hilbert_cube_topology (f ` topspace X) = f_S.sub.mtopology" using Hilbert_cube_eq f_S.mtopology_submetric by auto have "continuous_map f_S.sub.mtopology ms.mtopology g" unfolding continuous_map_iff_limit_seq[OF f_S.sub.first_countable_mtopology] proof safe fix yn y assume h:" limitin f_S.sub.mtopology yn y sequentially" have h':"limitin ppm.Product_metric.mtopology yn y sequentially" using f_S.limitin_submetric_iff h by blast hence m01_conv:"\n. limitin m01'.mtopology (\i. yn i n) (y n) sequentially" "y \ UNIV \\<^sub>E {0..1}" by(auto simp: ppm.limitin_M_iff_limitin_Mi) have "\N. \n\N. \zn. yn n = f zn \ zn \ topspace X" using h g by(simp only: f_S.sub.limit_metric_sequentially) (meson imageE ppm.K_pos) then obtain N' zn where zn:"\n. n \ N' \ f (zn n) = yn n" "\n. n \ N' \ zn n \ topspace X" by metis obtain z where z:"f z = y" "z \ topspace X" using h f_S.sub.limitin_mspace by blast show "limitin ms.mtopology (\n. g (yn n)) (g y) sequentially" unfolding ms.limit_metric_sequentially proof safe fix \ :: real assume he: "0 < \" then have "0 < \ / 3" by simp then obtain m where m:"d z (xn m) < \ / 3" using ms.mdense_def2[of U,simplified d(1)] U(2) z(2) xn(2) by blast have "\e. e>0 \ \N. \n\N. yn n m \ {0..1} \ dist (yn n m) (y m) < e" using m01_conv(1)[of m,simplified m01'.limit_metric_sequentially] by fastforce from this[OF \0 < \ / 3\] obtain N where "\n. n \ N \ \yn n m - y m\ < \ / 3" "\n. n \ N \ yn n m \ {0..1}" by(auto simp: dist_real_def) hence N:"\n. n \ N \ yn n m < \ / 3 + y m" by (metis abs_diff_less_iff add.commute) have "\N. \n\N. zn n \ topspace X \ d (zn n) z < \" proof(safe intro!: exI[where x="max N N'"]) fix n assume "max N N' \ n" then have "N \ n" "N' \ n" by auto then have "d (zn n) z \ f (zn n) m + d z (xn m)" using ms.triangle[OF zn(2)[of n] xns[of m] z(2),simplified ms.commute[of "xn m" z]] by(auto simp: f_def) also have "... < \ / 3 + y m + d z (xn m)" using N[OF \N\n\] zn(1)[of n] \N' \ n\ by simp also have "... = \ / 3 + d z (xn m) + d z (xn m)" by(simp add: z(1)[symmetric] f_def) also have "... < \" using m by auto finally show "d (zn n) z < \" . qed(use zn in auto) thus "\N. \n\N. g (yn n) \ topspace X \ d (g (yn n)) (g y) < \" by (metis dual_order.trans nle_le zn(1) z(1) g(2)[OF z(2)] g(2)[OF zn(2)]) qed(use g z in auto) qed hence "continuous_map f_S.sub.mtopology ms.mtopology g" by(auto simp: mtopology_of_def) thus ?thesis by(simp add: d(1) 1) qed show ?thesis using f_img g(2,3) f_cont' g_cont by(auto intro!: exI[where x="f ` topspace X"] homeomorphic_maps_imp_homeomorphic_space[where f=f and g=g] simp: homeomorphic_maps_def) qed qed corollary embedding_into_Hilbert_cube_gdelta_in: assumes "polish_space X" shows "\A. gdelta_in Hilbert_cube_topology A \ X homeomorphic_space (subtopology Hilbert_cube_topology A)" proof - obtain A where h:"A \ topspace Hilbert_cube_topology" "X homeomorphic_space subtopology Hilbert_cube_topology A" using embedding_into_Hilbert_cube polish_space_imp_metrizable_space polish_space_imp_separable_space assms by blast with completely_metrizable_space_homeo_image_gdelta_in[OF polish_space_imp_completely_metrizable_space[OF assms] polish_space_imp_completely_metrizable_space[OF polish_space_Hilbert_cube] h(1,2)] show ?thesis by blast qed subsubsection \ Embedding from Cantor Space \ lemma embedding_from_Cantor_space: assumes "polish_space X" "uncountable (topspace X)" shows "\A. gdelta_in X A \ Cantor_space_topology homeomorphic_space (subtopology X A)" proof - obtain U P where up: "countable U" "openin X U" "perfect_set X P""U \ P = topspace X" "U \ P = {}" "\a. a \ {} \ openin (subtopology X P) a \ uncountable a" using Cantor_Bendixon[OF polish_space_imp_second_countable[OF assms(1)]] by auto have P: "closedin X P" "P \ topspace X" "uncountable P" using countable_Un_iff[of U P] up(1) assms up(4) by(simp_all add: perfect_setD[OF up(3)]) then have pp: "polish_space (subtopology X P)" by (simp add: assms(1) polish_space_closedin) have Ptop: "topspace (subtopology X P) = P" using P(2) by auto obtain U where U: "countable U" "dense_in (subtopology X P) U" using polish_space_def pp separable_space_def2 by auto with uncountable_infinite[OF P(3)] P(2) have "infinite U" by (metis Metric_space.t1_space_mtopology Ptop assms(1) completely_metrizable_space_def dense_in_infinite polish_space_def t1_space_subtopology) obtain d where "Metric_space P d" and d:"Metric_space.mtopology P d = subtopology X P" and mdc: "Metric_space.mcomplete P d" by (metis Metric_space.topspace_mtopology Ptop completely_metrizable_space_def polish_space_def pp) interpret md: Metric_space P d by fact define xn where "xn \ from_nat_into U" have xn: "bij_betw xn UNIV U" "\n m. n \ m \ xn n \ xn m" "\n. xn n \ U" "\n. xn n \ P" "md.mdense (range xn)" using bij_betw_from_nat_into[OF U(1) \infinite U\] dense_in_subset[OF U(2)] d U(2) range_from_nat_into[OF infinite_imp_nonempty[OF \infinite U\] U(1)] by(auto simp add: xn_def U(1) \infinite U\ from_nat_into[OF infinite_imp_nonempty[OF \infinite U\]]) have perfect:"perfect_space md.mtopology" using d perfect_set_subtopology up(3) by simp define jn where "jn \ (\n. LEAST i. i > n \ md.mcball (xn i) ((1/2)^i) \ md.mball (xn n) ((1/2)^n) - md.mball (xn n) ((1/2)^i))" define kn where "kn \ (\n. LEAST k. k > jn n \ md.mcball (xn k) ((1/2)^k) \ md.mball (xn n) ((1/2)^jn n))" have dxmxn: "\n n'. \m. m > n \ m > n' \ (1/2)^(m-1) < d (xn n) (xn m) \ d (xn n) (xn m) < (1/2)^(Suc n')" proof safe fix n n' have hinfin':"infinite (md.mball x e \ (range xn))" if "x \ P" "e > 0" for x e proof assume h_fin:"finite (md.mball x e \ range xn)" have h_nen:"md.mball x e \ range xn \ {}" using xn(5) that by(auto simp: md.mdense_def) have infin: "infinite (md.mball x e)" using md.perfect_set_mball_infinite[OF perfect] that by simp then obtain y where y:"y \ md.mball x e" "y \ range xn" using h_fin by(metis inf.absorb_iff2 inf_commute subsetI) define e' where "e' = Min {d y xk |xk. xk \ md.mball x e \ range xn}" have fin: "finite {d y xk |xk. xk \ md.mball x e \ range xn}" using finite_imageI[OF h_fin,of "d y"] by (metis Setcompr_eq_image) have nen: "{d y xk |xk. xk \ md.mball x e \ range xn} \ {}" using h_nen by auto have "e' > 0" unfolding e'_def Min_gr_iff[OF fin nen] proof safe fix l assume "xn l \ md.mball x e" with y show "0 < d y (xn l)" by auto qed obtain e'' where e'': "e'' > 0" "md.mball y e'' \ md.mball x e" "y \ md.mball y e''" by (meson md.centre_in_mball_iff md.in_mball md.openin_mball md.openin_mtopology y(1)) define \ where "\ \ min e' e''" have "\ > 0" using e''(1) \e' > 0\ by(simp add: \_def) then obtain m where m: "d y (xn m) < \" using md.mdense_def2[of "range xn"] xn(5) y(1) by fastforce consider "xn m \ md.mball x e" | "xn m \ P - md.mball x e" using xn(4) by auto then show False proof cases case 1 then have "e' \ d y (xn m)" using Min_le_iff[OF fin nen] by(auto simp: e'_def) thus ?thesis using m by(simp add: \_def) next case 2 then have "xn m \ md.mball y e''" using e''(2) by auto hence "e'' \ d y (xn m)" using y e'' xn by auto thus ?thesis using m by(simp add: \_def) qed qed have hinfin:"infinite (md.mball x e \ (xn ` {l<..}))" if "x \ P" "e > 0" for x e l proof assume "finite (md.mball x e \ xn ` {l<..})" moreover have "finite (md.mball x e \ xn ` {..l})" by simp moreover have "(md.mball x e \ (range xn)) = (md.mball x e \ xn ` {l<..}) \ (md.mball x e \ xn ` {..l})" by fastforce ultimately have "finite (md.mball x e \ (range xn))" by auto with hinfin'[OF that] show False .. qed have "infinite (md.mball (xn n) ((1/2)^Suc n'))" using md.perfect_set_mball_infinite[OF perfect] xn(4)[of n] by simp then obtain x where x: "x \ md.mball (xn n) ((1/2)^Suc n')" "x \ xn n" by (metis finite_insert finite_subset infinite_imp_nonempty singletonI subsetI) then obtain e where e: "e > 0" "md.mball x e \ md.mball (xn n) ((1/2)^Suc n')" "x \ md.mball x e" by (meson md.centre_in_mball_iff md.in_mball md.openin_mball md.openin_mtopology) have "d (xn n) x > 0" using xn x by simp then obtain m' where m': "m' - 1 > 0" "(1/2)^(m' - 1) < d (xn n) x" by (metis One_nat_def diff_Suc_Suc diff_zero one_less_numeral_iff reals_power_lt_ex semiring_norm(76)) define m where "m \ max m' (max n' (Suc n))" then have "m \ m'" "m \ n'" "m \ Suc n" by simp_all hence m: "m - 1 > 0" "(1/2)^(m - 1) < d (xn n) x" "m > n" using m' less_trans[OF _ m'(2),of "(1 / 2) ^ (m - 1)"] by auto (metis diff_less_mono le_eq_less_or_eq) define \ where "\ \ min e (d (xn n) x - (1/2)^(m - 1))" have "\ > 0" using e m by(simp add: \_def) have ball_le:"md.mball x \ \ md.mball (xn n) ((1 / 2) ^ Suc n')" using e(2) by(auto simp add: \_def) obtain k where k: "xn k \ md.mball x \" "k > m" using \\ > 0\ infinite_imp_nonempty[OF hinfin,of _ \] x(1) by fastforce show "\m>n. n' < m \ (1 / 2) ^ (m - 1) < d (xn n) (xn m) \ d (xn n) (xn m) < (1 / 2) ^ Suc n'" proof(intro exI[where x=k] conjI) have "(1 / 2) ^ (k - 1) < (1 / (2 :: real)) ^ (m - 1)" using k(2) m(3) by simp also have "... = d (xn n) x + ((1/2)^ (m - 1) - d (xn n) x)" by simp also have "... < d (xn n) x - d (xn k) x" using k by(auto simp: \_def md.commute) also have "... \ d (xn n) (xn k)" using xn x md.mdist_reverse_triangle[of "xn n" x "xn k"] by(auto simp: md.commute) finally show "(1 / 2) ^ (k - 1) < d (xn n) (xn k)" . qed(use \m \ n'\ k ball_le m(3) in auto) qed have "jn n > n \ md.mcball (xn (jn n)) ((1/2)^(jn n)) \ md.mball (xn n) ((1/2)^n) - md.mball (xn n) ((1/2)^(jn n))" for n unfolding jn_def proof(rule LeastI_ex) obtain m where m:"m > n" "(1 / 2) ^ (m - 1) < d (xn n) (xn m)" "d (xn n) (xn m) < (1 / 2) ^ Suc n" using dxmxn by auto show "\x>n. md.mcball (xn x) ((1 / 2) ^ x) \ md.mball (xn n) ((1 / 2) ^ n) - md.mball (xn n) ((1 / 2) ^ x)" proof(safe intro!: exI[where x=m] m(1)) fix x assume h:"x \ md.mcball (xn m) ((1 / 2) ^ m)" have 1:"d (xn n) x < (1 / 2) ^ n" proof - have "d (xn n) x < (1 / 2) ^ Suc n + (1 / 2) ^ m" using m(3) md.triangle[OF xn(4)[of n] xn(4)[of m],of x] h by auto also have "... \ (1 / 2) ^ Suc n + (1 / 2) ^ Suc n" by (metis Suc_lessI add_mono divide_less_eq_1_pos divide_pos_pos less_eq_real_def m(1) one_less_numeral_iff power_strict_decreasing_iff semiring_norm(76) zero_less_numeral zero_less_one) finally show ?thesis by simp qed have 2:"(1 / 2) ^ m \ d (xn n) x" proof - have "(1 / 2) ^ (m - 1) < d (xn n) x + (1 / 2) ^ m" using order.strict_trans2[OF m(2) md.triangle[OF xn(4)[of n] _ xn(4)[of m]]] h md.commute by fastforce hence "(1 / 2) ^ (m - 1) - (1 / 2) ^ m \ d (xn n) x" by simp thus ?thesis using not0_implies_Suc[OF gr_implies_not0[OF m(1)]] by auto qed show "x \ md.mball (xn n) ((1 / 2) ^ n)" "x \ md.mball (xn n) ((1 / 2) ^ m) \ False" using xn h 1 2 by auto qed qed hence jn: "\n. jn n > n" "\n. md.mcball (xn (jn n)) ((1/2)^(jn n)) \ md.mball (xn n) ((1/2)^n) - md.mball (xn n) ((1/2)^(jn n))" by simp_all have "kn n > jn n \ md.mcball (xn (kn n)) ((1/2)^(kn n)) \ md.mball (xn n) ((1/2)^jn n)" for n unfolding kn_def proof(rule LeastI_ex) obtain m where m:"m > jn n" "d (xn n) (xn m) < (1 / 2) ^ Suc (jn n)" using dxmxn by blast show "\x>jn n. md.mcball (xn x) ((1 / 2) ^ x) \ md.mball (xn n) ((1 / 2) ^ jn n)" proof(intro exI[where x=m] conjI) show "md.mcball (xn m) ((1 / 2) ^ m) \ md.mball (xn n) ((1 / 2) ^ jn n)" proof fix x assume h:"x \ md.mcball (xn m) ((1 / 2) ^ m)" have "d (xn n) x < (1 / 2)^ Suc (jn n) + (1 / 2) ^ m" using md.triangle[OF xn(4)[of n] xn(4)[of m]] h m(2) by fastforce also have "... \ (1 / 2)^ Suc (jn n) + (1 / 2)^ Suc (jn n)" by (metis Suc_le_eq add_mono dual_order.refl less_divide_eq_1_pos linorder_not_less m(1) not_numeral_less_one power_decreasing zero_le_divide_1_iff zero_le_numeral zero_less_numeral) finally show "x \ md.mball (xn n) ((1 / 2) ^ jn n)" using xn(4) h by auto qed qed(use m(1) in auto) qed hence kn: "\n. kn n > jn n" "\n. md.mcball (xn (kn n)) ((1/2)^(kn n)) \ md.mball (xn n) ((1/2)^(jn n))" by simp_all have jnkn_pos: "jn n > 0" "kn n > 0" for n using not0_implies_Suc[OF gr_implies_not0[OF jn(1)[of n]]] kn(1)[of n] by auto define bn :: "real list \ nat" where "bn \ rec_list 1 (\a l t. if a = 0 then jn t else kn t)" have bn_simp: "bn [] = 1" "bn (a # l) = (if a = 0 then jn (bn l) else kn (bn l))" for a l by(simp_all add: bn_def) define to_listn :: "(nat \ real) \ nat \ real list" where "to_listn \ (\x . rec_nat [] (\n t. x n # t))" have to_listn_simp: "to_listn x 0 = []" "to_listn x (Suc n) = x n # to_listn x n" for x n by(simp_all add: to_listn_def) have to_listn_eq: "(\m. m < n \ x m = y m) \ to_listn x n = to_listn y n" for x y n by(induction n) (auto simp: to_listn_simp) have bn_gtn: "bn (to_listn x n) > n" for x n apply(induction n arbitrary: x) using jn(1) kn(1) by(auto simp: bn_simp to_listn_simp) (meson Suc_le_eq le_less less_trans_Suc)+ define rn where "rn \ (\n. Min (range (\x. (1 / 2 :: real) ^ bn (to_listn x n))))" have rn_fin: "finite (range (\x. (1 / 2 :: real) ^ bn (to_listn x n)))" for n proof - have "finite (range (\x. bn (to_listn x n)))" proof(induction n) case ih:(Suc n) have "(range (\x. bn (to_listn x (Suc n)))) \ (range (\x. jn (bn (to_listn x n)))) \ (range (\x. kn (bn (to_listn x n))))" by(auto simp: to_listn_simp bn_simp) moreover have "finite ..." using ih finite_range_imageI by auto ultimately show ?case by(rule finite_subset) qed(simp add: to_listn_simp) thus ?thesis using finite_range_imageI by blast qed have rn_nen: "(range (\x. (1 / 2 :: real) ^ bn (to_listn x n))) \ {}" for n by simp have rn_pos: "0 < rn n" for n by(simp add: Min_gr_iff[OF rn_fin rn_nen] rn_def) have rn_less: "rn n < (1/2)^n" for n using bn_gtn[of n] by(auto simp: rn_def Min_less_iff[OF rn_fin rn_nen]) have cball_le_ball:"md.mcball (xn (bn (a#l))) ((1/2)^(bn (a#l))) \ md.mball (xn (bn l)) ((1/2) ^ (bn l))" for a l using kn(2)[of "bn l"] less_imp_le[OF jn(1)] jn(2) md.mball_subset_concentric[of "(1 / 2) ^ jn (bn l)" "(1 / 2) ^ bn l" "xn (bn l)"] by(auto simp: bn_simp) hence cball_le:"md.mcball (xn (bn (a#l))) ((1/2)^(bn (a#l))) \ md.mcball (xn (bn l)) ((1/2) ^ (bn l))" for a l using md.mball_subset_mcball by blast have cball_disj: "md.mcball (xn (bn (0#l))) ((1/2)^(bn (0#l))) \ md.mcball (xn (bn (1#l))) ((1/2)^(bn (1#l))) = {}" for l using jn(2) kn(2) by(auto simp: bn_simp) have "\x. \l. l \ P \ (\n. md.mcball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n))) = {l}" proof fix x show "\l. l \ P \ (\n. md.mcball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n))) = {l}" proof(safe intro!: md.mcomplete_nest_sing[THEN iffD1,OF mdc,rule_format]) show "md.mcball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n)) = {} \ False" for n using md.mcball_eq_empty xn(4) by auto next show "decseq (\n. md.mcball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n)))" by(intro decseq_SucI,simp add: to_listn_simp cball_le) next fix e :: real assume "0 < e" then obtain N where N: "(1 / 2) ^ N < e" by (meson reals_power_lt_ex rel_simps(49) rel_simps(9)) show "\n a. md.mcball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n)) \ md.mcball a e" proof(safe intro!: exI[where x=N] exI[where x="xn (bn (to_listn x N))"]) fix y assume "y \ md.mcball (xn (bn (to_listn x N))) ((1 / 2) ^ bn (to_listn x N))" then have "y \ md.mcball (xn (bn (to_listn x N))) ((1 / 2) ^ N)" using md.mcball_subset_concentric[OF power_decreasing[OF less_imp_le[OF bn_gtn[of N x]],of "1/2"]] by fastforce thus "y \ md.mcball (xn (bn (to_listn x N))) e" using N \0 < e\ by auto qed qed qed then obtain f where f:"\x. f x \ P" "\x. (\n. md.mcball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n))) = {f x}" by metis hence f': "\n x. f x \ md.mcball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n))" by blast have f'': "f x \ md.mball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n))" for n x using f'[of x "Suc n"] cball_le_ball[of _ "to_listn x n"] by(fastforce simp: to_listn_simp) interpret bdmd: Submetric P d "f ` (\\<^sub>E i\UNIV. {0,1})" by standard (use f in auto) have bdmd_sub: "bdmd.sub.mtopology = subtopology X (f ` (\\<^sub>E i\UNIV. {0,1}))" using f(1) Int_absorb1[of "f ` (UNIV \\<^sub>E {0, 1})" P] by(fastforce simp: bdmd.mtopology_submetric d subtopology_subtopology) let ?d = "\x y. 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}" proof - have "d01.mtopology = Metric_space.mtopology {0,1} dist" 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 ?thesis . qed interpret pd: Product_metric "1/2" 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) define def_at where "def_at x y \ LEAST n. x n \ y n" for x y :: "nat \ real" have def_atxy: "\n. n < def_at x y \ x n = y n" "x (def_at x y) \ y (def_at x y)" if "x \ y" for x y proof - have "\n. x n \ y n" using that by auto from LeastI_ex[OF this] show "\n. n < def_at x y \ x n = y n" "x (def_at x y) \ y (def_at x y)" using not_less_Least by(auto simp: def_at_def) qed have def_at_le_if: "pd.product_dist x y \ (1/2)^n \ n \ def_at x y" if assm:"x \ y" "x \ (\\<^sub>E i\UNIV. {0,1})" "y \ (\\<^sub>E i\UNIV. {0,1})" for x y n proof - assume h:"pd.product_dist x y \ (1 / 2) ^ n" have "x m = y m" if m_less_n: "m < n" for m proof(rule ccontr) assume nen: "x m \ y m" then have "?d (x m) (y m) = 1" using assm(2,3) by(auto simp: submetric_def) hence "1 \ 2 ^ m * pd.product_dist x y" using pd.product_dist_geq[of m m,simplified,OF assm(2,3)] by simp hence "(1/2)^m \ 2^m * (1/2)^m * pd.product_dist x y" by simp hence "(1/2)^m \ pd.product_dist x y" by (simp add: power_one_over) also have "... \ (1 / 2) ^ n" by(simp add: h) finally show False using that by auto qed thus "n \ def_at x y" by (meson def_atxy(2) linorder_not_le that(1)) qed have def_at_le_then: "pd.product_dist x y \ 2 * (1/2)^n" if assm:"x \ y" "x \ (\\<^sub>E i\UNIV. {0,1})" "y \ (\\<^sub>E i\UNIV. {0,1})" "n \ def_at x y" for x y n proof - have "\m. m < n \ x m = y m" by (metis def_atxy(1) order_less_le_trans that(4)) hence 1:"\m. m < n \ ?d (x m) (y m) = 0" by (simp add: submetric_def) have "pd.product_dist x y = (\i. (1/2)^(i + n) * (?d (x (i + n)) (y (i + n)))) + (\ii. (1/2)^(i + n) * (?d (x (i + n)) (y (i + n))))" by(simp add: 1) also have "... \ (\i. (1/2)^(i + n))" using pd.product_dist_summable' unfolding id_apply by(auto intro!: suminf_le summable_ignore_initial_segment) finally show ?thesis using pd.nsum_of_rK[of n] by simp qed have d_le_def: "d (f x) (f y) \ (1/2)^(def_at x y)" if assm:"x \ y" "x \ (\\<^sub>E i\UNIV. {0,1})" "y \ (\\<^sub>E i\UNIV. {0,1})" for x y proof - have 1:"to_listn x n = to_listn y n" if "n \ def_at x y" for n proof - have "\m. m < n \ x m = y m" by (metis def_atxy(1) order_less_le_trans that) then show ?thesis by(auto intro!: to_listn_eq) qed have "f x \ md.mcball (xn (bn (to_listn x (def_at x y)))) ((1 / 2) ^ bn (to_listn x (def_at x y)))" "f y \ md.mcball (xn (bn (to_listn x (def_at x y)))) ((1 / 2) ^ bn (to_listn x (def_at x y)))" using f'[of x "def_at x y"] f'[of y "def_at x y"] by(auto simp: 1[OF order_refl]) hence "d (f x) (f y) \ 2 * (1 / 2) ^ bn (to_listn x (def_at x y))" using f(1) by(auto intro!: md.mdiameter_is_sup'[OF _ _ md.mdiameter_cball_leq]) also have "... \ (1/2)^(def_at x y)" proof - have "Suc (def_at x y) \ bn (to_listn x (def_at x y))" using bn_gtn[of "def_at x y" x] by simp hence "(1 / 2) ^ bn (to_listn x (def_at x y)) \ (1 / 2 :: real) ^ Suc (def_at x y)" using power_decreasing_iff[OF pd.r] by blast thus ?thesis by simp qed finally show "d (f x) (f y) \ (1/2)^(def_at x y)" . qed have fy_in:"f y \ md.mcball (xn (bn (to_listn x m))) ((1/2)^bn (to_listn x m)) \ \l (\\<^sub>E i\UNIV. {0,1})" "y \ (\\<^sub>E i\UNIV. {0,1})" for x y m proof(induction m) case ih:(Suc m) have "f y \ md.mcball (xn (bn (to_listn x m))) ((1 / 2) ^ bn (to_listn x m))" using ih(2) cball_le by(fastforce simp: to_listn_simp) with ih(1) have k:"k < m \ x k = y k" for k by simp show ?case proof safe fix l assume "l < Suc m" then consider "l < m" | "l = m" using \l < Suc m\ by fastforce thus "x l = y l" proof cases case 2 have 3:"f y \ md.mcball (xn (bn (y l # to_listn y l))) ((1 / 2) ^ bn (y l # to_listn y l))" using f'[of y "Suc l"] by(simp add: to_listn_simp) have 4:"f y \ md.mcball (xn (bn (x l # to_listn y l))) ((1 / 2) ^ bn (x l # to_listn y l))" using ih(2) to_listn_eq[of m x y,OF k] by(simp add: to_listn_simp 2) show ?thesis proof(rule ccontr) assume "x l \ y l" then consider "x l = 0" "y l = 1" | "x l = 1" "y l = 0" using assm(1,2) by(auto simp: PiE_def Pi_def) metis thus False by cases (use cball_disj[of "to_listn y l"] 3 4 in auto) qed qed(simp add: k) qed qed simp have d_le_rn_then: "\e>0. \y \ (\\<^sub>E i\UNIV. {0,1}). x \ y \ d (f x) (f y) < e \ n \ def_at x y" if assm: "x \ (\\<^sub>E i\UNIV. {0,1})" for x n proof(safe intro!: exI[where x="(1/2)^bn (to_listn x n) - d (xn (bn (to_listn x n))) (f x)"]) show "0 < (1 / 2) ^ bn (to_listn x n) - d (xn (bn (to_listn x n))) (f x)" using f'' by auto next fix y assume h:"y \ (\\<^sub>E i\UNIV. {0,1})" "d (f x) (f y) < (1 / 2) ^ bn (to_listn x n) - d (xn (bn (to_listn x n))) (f x)" "x \ y" then have "f y \ md.mcball (xn (bn (to_listn x n))) ((1/2)^bn (to_listn x n))" using md.triangle[OF xn(4)[of "bn (to_listn x n)"] f(1)[of x] f(1)[of y]] by(simp add: xn(4)[of "bn (to_listn x n)"] f(1)[of y] md.mcball_def) with fy_in[OF assm h(1)] have "\m < n. x m = y m" by auto thus "n \ def_at x y" by (meson def_atxy(2) linorder_not_le h(3)) qed have 0: "f ` (\\<^sub>E i\UNIV. {0,1}) \ topspace X" using f(1) P(2) by auto have 1: "continuous_map pd.Product_metric.mtopology bdmd.sub.mtopology f" unfolding pd.Product_metric.metric_continuous_map[OF bdmd.sub.Metric_space_axioms] proof safe fix x :: "nat \ real" and \ :: real assume h:"x \ (\\<^sub>E i\UNIV. {0,1})" "0 < \" then obtain n where n:"(1/2)^n < \" using real_arch_pow_inv[OF _ pd.r(2)] by auto show "\\>0. \y. y\UNIV \\<^sub>E {0, 1} \ pd.product_dist x y < \ \ d (f x) (f y) < \" proof(safe intro!: exI[where x="(1/2)^n"]) fix y assume y:"y \ (\\<^sub>E i\UNIV. {0,1})" "pd.product_dist x y < (1 / 2) ^ n" consider "x = y" | "x \ y" by auto thus "d (f x) (f y) < \" proof cases case 1 with y(1) h md.zero[OF f(1)[of y] f(1)[of y]] show ?thesis by simp next case 2 then have "n \ def_at x y" using h(1) y by(auto intro!: def_at_le_if) have "d (f x) (f y) \ (1/2)^(def_at x y)" using h(1) y(1) by(auto simp: d_le_def[OF 2 h(1) y(1)]) also have "... \ (1/2)^n" using \n \ def_at x y\ by simp finally show ?thesis using n by simp qed qed simp qed have 2: "open_map pd.Product_metric.mtopology bdmd.sub.mtopology f" proof - have "open_map (mtopology_of pd.Product_metric.Self) (subtopology (mtopology_of md.Self) (f ` mspace pd.Product_metric.Self)) f" proof(safe intro!: Metric_space_open_map_from_dist) fix x :: "nat \ real" and \ :: real assume h:"x \ mspace pd.Product_metric.Self" "0 < \" then have x:"x \ (\\<^sub>E i\UNIV. {0,1})" by simp from h obtain n where n: "(1/2)^n < \" using real_arch_pow_inv[OF _ pd.r(2)] by auto obtain e where e: "e > 0" "\y. y \ (\\<^sub>E i\UNIV. {0,1}) \ x \ y \ d (f x) (f y) < e \ Suc n \ def_at x y" using d_le_rn_then[OF x,of "Suc n"] by auto show "\\>0. \y\mspace pd.Product_metric.Self. mdist md.Self (f x) (f y) < \ \ mdist pd.Product_metric.Self x y < \" unfolding md.mdist_Self pd.Product_metric.mspace_Self pd.Product_metric.mdist_Self proof(safe intro!: exI[where x=e]) fix y assume y:"y \ (\\<^sub>E i\UNIV. {0,1})" and "d (f x) (f y) < e" then have d':"d (f x) (f y) < e" using h(1) by simp consider "x = y" | "x \ y" by auto thus "pd.product_dist x y < \" by cases (use pd.Product_metric.zero[OF y y] h(2) def_at_le_then[OF _ x y e(2)[OF y _ d']] n in auto) qed(use e(1) in auto) qed(use f in auto) thus ?thesis by (simp add: bdmd.mtopology_submetric mtopology_of_def) qed have 3: "f ` (topspace pd.Product_metric.mtopology) = topspace bdmd.sub.mtopology" by simp have 4: "inj_on f (topspace pd.Product_metric.mtopology)" unfolding pd.Product_metric.topspace_mtopology proof fix x y assume h:"x \ (\\<^sub>E i\UNIV. {0,1})" "y \ (\\<^sub>E i\UNIV. {0,1})" "f x = f y" show "x = y" proof fix n have "f y \ md.mcball (xn (bn (to_listn x (Suc n)))) ((1/2)^bn (to_listn x (Suc n)))" using f'[of x "Suc n"] by(simp add: h) thus "x n = y n" using fy_in[OF h(1,2),of "Suc n"] by simp qed qed show ?thesis using homeomorphic_map_imp_homeomorphic_space[OF bijective_open_imp_homeomorphic_map[OF 1 2 3 4]] 0 by (metis (no_types, lifting) assms(1) bdmd_sub completely_metrizable_space_homeo_image_gdelta_in mpd_top polish_space_Cantor_space polish_space_def) qed subsection \Borel Spaces generated from Polish Spaces\ lemma closedin_clopen_topology: assumes "polish_space X" "closedin X a" shows "\X'. polish_space X' \ (\u. openin X u \ openin X' u) \ topspace X = topspace X' \ sets (borel_of X) = sets (borel_of X') \ openin X' a \ closedin X' a" proof - have p1:"polish_space (subtopology X a)" by (simp add: assms polish_space_closedin) then obtain da' where da': "Metric_space a da'" "subtopology X a = Metric_space.mtopology a da'" "Metric_space.mcomplete a da'" by (metis Metric_space.topspace_mtopology assms(2) closedin_subset completely_metrizable_space_def polish_space_imp_completely_metrizable_space topspace_subtopology_subset) define da where "da = Metric_space.capped_dist da' (1/2)" have da: "subtopology X a = Metric_space.mtopology a da" "Metric_space.mcomplete a da" using da' by(auto simp: da_def Metric_space.mtopology_capped_metric Metric_space.mcomplete_capped_metric) interpret pa: Metric_space a da using da' by(simp add: Metric_space.capped_dist da_def) have da_bounded: "\x y. da x y < 1" using da' by(auto simp: da_def Metric_space.capped_dist_def) have p2:"polish_space (subtopology X (topspace X - a))" by (meson assms(1) assms(2) closedin_def polish_space_openin) then obtain db' where db': "Metric_space (topspace X - a) db'" "subtopology X (topspace X - a) = Metric_space.mtopology (topspace X - a) db'" "Metric_space.mcomplete (topspace X - a) db'" by (metis Diff_subset Metric_space.topspace_mtopology completely_metrizable_space_def polish_space_imp_completely_metrizable_space topspace_subtopology_subset) define db where "db = Metric_space.capped_dist db' (1/2)" have db: "subtopology X (topspace X - a) = Metric_space.mtopology (topspace X - a) db" "Metric_space.mcomplete (topspace X - a) db" using db' by(auto simp: db_def Metric_space.mtopology_capped_metric Metric_space.mcomplete_capped_metric) interpret pb: Metric_space "topspace X - a" db using db' by(simp add: Metric_space.capped_dist db_def) have db_bounded: "\x y. db x y < 1" using db' by(auto simp: db_def Metric_space.capped_dist_def) interpret p: Sum_metric UNIV "\b. if b then a else topspace X - a" "\b. if b then da else db" using da db da_bounded db_bounded by(auto intro!: sum_metricI simp: disjoint_family_on_def pa.Metric_space_axioms pb.Metric_space_axioms) have 0: "(\i. if i then a else topspace X - a) = topspace X" using closedin_subset assms by auto have 1: "sets (borel_of X) = sets (borel_of p.Sum_metric.mtopology)" proof - have "sigma_sets (topspace X) (Collect (openin X)) = sigma_sets (topspace X) (Collect (openin p.Sum_metric.mtopology))" proof(rule sigma_sets_eqI) fix a assume "a \ Collect (openin X)" then have "openin p.Sum_metric.mtopology a" by(simp only: p.openin_mtopology_iff) (auto simp: 0 da(1)[symmetric] db(1)[symmetric] openin_subtopology dest: openin_subset) thus "a \ sigma_sets (topspace X) (Collect (openin p.Sum_metric.mtopology))" by auto next interpret s: sigma_algebra "topspace X" "sigma_sets (topspace X) (Collect (openin X))" by(auto intro!: sigma_algebra_sigma_sets openin_subset) fix b assume "b \ Collect (openin p.Sum_metric.mtopology)" then have "openin p.Sum_metric.mtopology b" by auto then have b:"b \ topspace X" "openin (subtopology X a) (b \ a)" "openin (subtopology X (topspace X - a)) (b \ (topspace X - a))" by(simp_all only: p.openin_mtopology_iff,insert 0 da(1) db(1)) (auto simp: all_bool_eq) have [simp]: "(b \ a) \ (b \ (topspace X - a)) = b" using Diff_partition b(1) by blast have "(b \ a) \ (b \ (topspace X - a)) \ sigma_sets (topspace X) (Collect (openin X))" proof(rule sigma_sets_Un) have [simp]:"a \ sigma_sets (topspace X) (Collect (openin X))" proof - have "topspace X - (topspace X - a) \ sigma_sets (topspace X) (Collect (openin X))" by(rule sigma_sets.Compl) (use assms in auto) thus ?thesis using double_diff[OF closedin_subset[OF assms(2)]] by simp qed from b(2,3) obtain T T' where T:"openin X T" "openin X T'" and [simp]:"b \ a = T \ a" "b \ (topspace X - a) = T' \ (topspace X - a)" by(auto simp: openin_subtopology) show "b \ a \ sigma_sets (topspace X) (Collect (openin X))" "b \ (topspace X - a) \ sigma_sets (topspace X) (Collect (openin X))" using T assms by auto qed thus "b \ sigma_sets (topspace X) (Collect (openin X))" by simp qed thus ?thesis by(simp only: sets_borel_of p.Sum_metric.topspace_mtopology) (use 0 in auto) qed have 2:"\u. openin X u \ openin p.Sum_metric.mtopology u" by(simp only: p.openin_mtopology_iff) (auto simp: all_bool_eq da(1)[symmetric] db(1)[symmetric] openin_subtopology dest: openin_subset) have 3:"openin p.Sum_metric.mtopology a" by(simp only: p.openin_mtopology_iff) (auto simp: all_bool_eq) have 4:"closedin p.Sum_metric.mtopology a" by (metis 0 2 assms(2) closedin_def p.Sum_metric.topspace_mtopology) have 5: "topspace X = topspace p.Sum_metric.mtopology" by(simp only: p.Sum_metric.topspace_mtopology) (simp only: 0) have 6: "polish_space p.Sum_metric.mtopology" by(rule p.polish_spaceI,insert da(2) db(2) p1 p2) (auto simp: da(1) db(1) polish_space_def) show ?thesis by(rule exI[where x=p.Sum_metric.mtopology]) (insert 5 2 6, simp only: 1 3 4 ,auto) qed lemma polish_space_union_polish: fixes X :: "nat \ 'a topology" assumes "\n. polish_space (X n)" "\n. topspace (X n) = Xt" "\x y. x \ Xt \ y \ Xt \ x \ y \ \Ox Oy. (\n. openin (X n) Ox) \ (\n. openin (X n) Oy) \ x \ Ox \ y \ Oy \ disjnt Ox Oy" defines "Xun \ topology_generated_by (\n. {u. openin (X n) u})" shows "polish_space Xun" proof - have topsXun:"topspace Xun = Xt" using assms(2) by(auto simp: Xun_def dest:openin_subset) define f :: "'a \ nat \ 'a" where "f \ (\x n. x)" have "continuous_map Xun (product_topology X UNIV) f" by(auto simp: assms(2) topsXun f_def continuous_map_componentwise, auto simp: Xun_def openin_topology_generated_by_iff continuous_map_def assms(2) dest:openin_subset[of "X _",simplified assms(2)] ) (insert openin_subopen, fastforce intro!: generate_topology_on.Basis) hence 1: "continuous_map Xun (subtopology (product_topology X UNIV) (f ` (topspace Xun))) f" by(auto simp: continuous_map_in_subtopology) have 2: "inj_on f (topspace Xun)" by(auto simp: inj_on_def f_def dest:fun_cong) have 3: "f ` (topspace Xun) = topspace (subtopology (product_topology X UNIV) (f ` (topspace Xun)))" by(auto simp: topsXun assms(2) f_def) have 4: "open_map Xun (subtopology (product_topology X UNIV) (f ` (topspace Xun))) f" proof(safe intro!: open_map_generated_topo[OF _ 2[simplified Xun_def],simplified Xun_def[symmetric]]) fix u n assume u:"openin (X n) u" show "openin (subtopology (product_topology X UNIV) (f ` topspace Xun)) (f ` u)" unfolding openin_subtopology proof(safe intro!: exI[where x="{ \i. if i = n then a else b i |a b. a \u \ b \ UNIV \ Xt}"]) show "openin (product_topology X UNIV) {\i. if i = n then a else b i |a b. a \u \ b \ UNIV \ Xt}" by(auto simp: openin_product_topology_alt u assms(2) openin_topspace[of "X _",simplified assms(2)] intro!: exI[where x="\i. if i = n then u else Xt"]) (auto simp: PiE_def Pi_def, metis openin_subset[OF u,simplified assms(2)] in_mono) next show "\y. y \ u \ \a b. f y = (\i. if i = n then a else b i) \ a \ u \ b \ UNIV \ Xt" using assms(2) f_def openin_subset u by fastforce next show "\y. y \ u \ f y \ f ` topspace Xun" using openin_subset[OF u] by(auto simp: assms(2) topsXun) next show "\x xa a b. xa \ topspace Xun \ f xa = (\i. if i = n then a else b i) \ a \ u \ b \ UNIV \ Xt \ f xa \ f ` u" using openin_subset[OF u] by(auto simp: topsXun assms(2)) (metis f_def imageI) qed qed have 5:"(subtopology (product_topology X UNIV) (f ` topspace Xun)) homeomorphic_space Xun" using homeomorphic_map_imp_homeomorphic_space[OF bijective_open_imp_homeomorphic_map[OF 1 4 3 2]] by(simp add: homeomorphic_space_sym[of Xun]) show ?thesis proof(safe intro!: homeomorphic_polish_space_aux[OF polish_space_closedin[OF polish_space_product] 5] assms) show "closedin (product_topology X UNIV) (f ` topspace Xun)" proof - have 1: "openin (product_topology X UNIV) ((UNIV \\<^sub>E Xt) - f ` Xt)" proof(rule openin_subopen[THEN iffD2]) show "\x\(UNIV \\<^sub>E Xt) - f ` Xt. \T. openin (product_topology X UNIV) T \ x \ T \ T \ (UNIV \\<^sub>E Xt) - f ` Xt" proof safe fix x assume x:"x \ UNIV \\<^sub>E Xt" "x \ f ` Xt" have "\n. x n \ x 0" proof(rule ccontr) assume " \n. x n \ x 0" then have "\n. x n = x 0" by auto hence "x = (\_. x 0)" by auto thus False using x by(auto simp: f_def topsXun assms(2)) qed then obtain n where n: "n \ 0" "x n \ x 0" by metis from assms(3)[OF _ _ this(2)] x obtain On O0 where h:"\n. openin (X n) On" "\n. openin (X n) O0" "x n \ On" "x 0 \ O0" "disjnt On O0" by fastforce have "openin (product_topology X UNIV) ((\x. x 0) -` O0 \ topspace (product_topology X UNIV))" using continuous_map_product_coordinates[of 0 UNIV X] h(2)[of 0] by blast moreover have "openin (product_topology X UNIV) ((\x. x n) -` On \ topspace (product_topology X UNIV))" using continuous_map_product_coordinates[of n UNIV X] h(1)[of n] by blast ultimately have op: "openin (product_topology X UNIV) ((\T. T 0) -` O0 \ topspace (product_topology X UNIV) \ ((\T. T n) -` On \ topspace (product_topology X UNIV)))" by auto have xin:"x \ (\T. T 0) -` O0 \ topspace (product_topology X UNIV) \ ((\T. T n) -` On \ topspace (product_topology X UNIV))" using x h(3,4) by(auto simp: assms(2)) have subset:"(\T. T 0) -` O0 \ topspace (product_topology X UNIV) \ ((\T. T n) -` On \ topspace (product_topology X UNIV)) \ (UNIV \\<^sub>E Xt) - f ` Xt" using h(5) by(auto simp: assms(2) disjnt_def f_def) show "\T. openin (product_topology X UNIV) T \ x \ T \ T \ (UNIV \\<^sub>E Xt) - f ` Xt" by(rule exI[where x="((\x. x 0) -` O0 \ topspace (product_topology X UNIV)) \ ((\x. x n) -` On \ topspace (product_topology X UNIV))"]) (use op xin subset in auto) qed qed thus ?thesis by(auto simp: closedin_def assms(2) topsXun f_def) qed qed(simp add: f_def) qed lemma sets_clopen_topology: assumes "polish_space X" "a \ sets (borel_of X)" shows "\X'. polish_space X' \ (\u. openin X u \ openin X' u) \ topspace X = topspace X' \ sets (borel_of X) = sets (borel_of X') \ openin X' a \ closedin X' a" proof - have "a \ sigma_sets (topspace X) {U. closedin X U}" using assms by(simp add: sets_borel_of_closed) thus ?thesis proof induction case (Basic a) then show ?case by(simp add: assms closedin_clopen_topology) next case Empty with polish_space_axioms assms show ?case by auto next case (Compl a) then obtain X' where S':"polish_space X'" "(\u. openin X u \ openin X' u)" "topspace X = topspace X'" "sets (borel_of X) = sets (borel_of X')" "openin X' a" "closedin X' a" by auto from closedin_clopen_topology[OF S'(1) S'(6)] S' show ?case by auto next case ih:(Union a) then obtain Si where Si: "\i. polish_space (Si i)" "\u i. openin X u \ openin (Si i) u" "\i::nat. topspace X = topspace (Si i)" "\i. sets (borel_of X) = sets (borel_of (Si i))" "\i. openin (Si i) (a i)" "\i. closedin (Si i) (a i)" by metis define Sun where "Sun \ topology_generated_by (\n. {u. openin (Si n) u})" have Sun1: "polish_space Sun" unfolding Sun_def proof(safe intro!: polish_space_union_polish[where Xt="topspace X"]) fix x y assume xy:"x \ topspace X" "y \ topspace X" "x \ y" then obtain Ox Oy where Oxy: "x \ Ox" "y \ Oy" "openin X Ox" "openin X Oy" "disjnt Ox Oy" using metrizable_imp_Hausdorff_space[OF polish_space_imp_metrizable_space[OF assms(1)]] by(simp only: Hausdorff_space_def) metis show "\Ox Oy. (\x. openin (Si x) Ox) \ (\x. openin (Si x) Oy) \ x \ Ox \ y \ Oy \ disjnt Ox Oy" by(rule exI[where x=Ox],insert Si(2) Oxy, auto intro!: exI[where x=Oy]) qed (use Si in auto) have Suntop:"topspace X = topspace Sun" using Si(3) by(auto simp: Sun_def dest: openin_subset) have Sunsets: "sets (borel_of X) = sets (borel_of Sun)" (is "?lhs = ?rhs") proof - have "?lhs = sigma_sets (topspace X) (\n. {u. openin (Si n) u})" proof show "sets (borel_of X) \ sigma_sets (topspace X) (\n. {u. openin (Si n) u})" using Si(2) by(auto simp: sets_borel_of intro!: sigma_sets_mono') next show "sigma_sets (topspace X) (\n. {u. openin (Si n) u}) \ sets (borel_of X)" by(simp add: sigma_sets_le_sets_iff[of "borel_of X" "\n. {u. openin (Si n) u}",simplified space_borel_of]) (use Si(4) sets_borel_of in fastforce) qed also have "... = ?rhs" using borel_of_second_countable'[OF polish_space_imp_second_countable[OF Sun1],of "\n. {u. openin (Si n) u}"] by (simp add: Sun_def Suntop subbase_in_def subset_Pow_Union) finally show ?thesis . qed have Sun_open: "\u i. openin (Si i) u \ openin Sun u" by(auto simp: Sun_def openin_topology_generated_by_iff intro!: generate_topology_on.Basis) have Sun_opena: "openin Sun (\i. a i)" using Sun_open[OF Si(5),simplified Sun_def] by(auto simp: Sun_def openin_topology_generated_by_iff intro!: generate_topology_on.UN) hence "closedin Sun (topspace Sun - (\i. a i))" by auto from closedin_clopen_topology[OF Sun1 this] show ?case using Suntop Sunsets Sun_open[OF Si(2)] Sun_opena by (metis closedin_def openin_closedin_eq) qed qed end \ No newline at end of file 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,1525 +1,1450 @@ (* 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) +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 \ (\\<^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 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