(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr with additions from LCP License: BSD *) section ‹Metrics on product spaces› theory Function_Metric imports Function_Topology Elementary_Metric_Spaces begin text ‹In general, the product topology is not metrizable, unless the index set is countable. When the index set is countable, essentially any (convergent) combination of the metrics on the factors will do. We use below the simplest one, based on ‹L⇧^{1}›, but ‹L⇧^{2}› would also work, for instance. What is not completely trivial is that the distance thus defined induces the same topology as the product topology. This is what we have to prove to show that we have an instance of \<^class>‹metric_space›. The proofs below would work verbatim for general countable products of metric spaces. However, since distances are only implemented in terms of type classes, we only develop the theory for countable products of the same space.› instantiation "fun" :: (countable, metric_space) metric_space begin definition✐‹tag important› dist_fun_def: "dist x y = (∑n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)" definition✐‹tag important› uniformity_fun_def: "(uniformity::(('a ⇒ 'b) × ('a ⇒ 'b)) filter) = (INF e∈{0<..}. principal {(x, y). dist (x::('a⇒'b)) y < e})" text ‹Except for the first one, the auxiliary lemmas below are only useful when proving the instance: once it is proved, they become trivial consequences of the general theory of metric spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how to do this.› lemma dist_fun_le_dist_first_terms: "dist x y ≤ 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n ≤ N} + (1/2)^N" proof - have "(∑n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1) = (∑n. (1 / 2) ^ (Suc N) * ((1/2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1))" by (rule suminf_cong, simp add: power_add) also have "... = (1/2)^(Suc N) * (∑n. (1 / 2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)" apply (rule suminf_mult) by (rule summable_comparison_test'[of "λn. (1/2)^n"], auto simp add: summable_geometric_iff) also have "... ≤ (1/2)^(Suc N) * (∑n. (1 / 2) ^ n)" apply (simp, rule suminf_le, simp) by (rule summable_comparison_test'[of "λn. (1/2)^n"], auto simp add: summable_geometric_iff) also have "... = (1/2)^(Suc N) * 2" using suminf_geometric[of "1/2"] by auto also have "... = (1/2)^N" by auto finally have *: "(∑n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1) ≤ (1/2)^N" by simp define M where "M = Max {dist (x (from_nat n)) (y (from_nat n))|n. n ≤ N}" have "dist (x (from_nat 0)) (y (from_nat 0)) ≤ M" unfolding M_def by (rule Max_ge, auto) then have [simp]: "M ≥ 0" by (meson dual_order.trans zero_le_dist) have "dist (x (from_nat n)) (y (from_nat n)) ≤ M" if "n≤N" for n unfolding M_def apply (rule Max_ge) using that by auto then have i: "min (dist (x (from_nat n)) (y (from_nat n))) 1 ≤ M" if "n≤N" for n using that by force have "(∑n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) ≤ (∑n< Suc N. M * (1 / 2) ^ n)" by (rule sum_mono, simp add: i) also have "... = M * (∑n<Suc N. (1 / 2) ^ n)" by (rule sum_distrib_left[symmetric]) also have "... ≤ M * (∑n. (1 / 2) ^ n)" by (rule mult_left_mono, rule sum_le_suminf, auto simp add: summable_geometric_iff) also have "... = M * 2" using suminf_geometric[of "1/2"] by auto finally have **: "(∑n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) ≤ 2 * M" by simp have "dist x y = (∑n. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)" unfolding dist_fun_def by simp also have "... = (∑n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1) + (∑n<Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)" apply (rule suminf_split_initial_segment) by (rule summable_comparison_test'[of "λn. (1/2)^n"], auto simp add: summable_geometric_iff) also have "... ≤ 2 * M + (1/2)^N" using * ** by auto finally show ?thesis unfolding M_def by simp qed lemma open_fun_contains_ball_aux: assumes "open (U::(('a ⇒ 'b) set))" "x ∈ U" shows "∃e>0. {y. dist x y < e} ⊆ U" proof - have *: "openin (product_topology (λi. euclidean) UNIV) U" using open_fun_def assms by auto obtain X where H: "Pi⇩_{E}UNIV X ⊆ U" "⋀i. openin euclidean (X i)" "finite {i. X i ≠ topspace euclidean}" "x ∈ Pi⇩_{E}UNIV X" using product_topology_open_contains_basis[OF * ‹x ∈ U›] by auto define I where "I = {i. X i ≠ topspace euclidean}" have "finite I" unfolding I_def using H(3) by auto { fix i have "x i ∈ X i" using ‹x ∈ U› H by auto then have "∃e. e>0 ∧ ball (x i) e ⊆ X i" using ‹openin euclidean (X i)› open_openin open_contains_ball by blast then obtain e where "e>0" "ball (x i) e ⊆ X i" by blast define f where "f = min e (1/2)" have "f>0" "f<1" unfolding f_def using ‹e>0› by auto moreover have "ball (x i) f ⊆ X i" unfolding f_def using ‹ball (x i) e ⊆ X i› by auto ultimately have "∃f. f > 0 ∧ f < 1 ∧ ball (x i) f ⊆ X i" by auto } note * = this have "∃e. ∀i. e i > 0 ∧ e i < 1 ∧ ball (x i) (e i) ⊆ X i" by (rule choice, auto simp add: *) then obtain e where "⋀i. e i > 0" "⋀i. e i < 1" "⋀i. ball (x i) (e i) ⊆ X i" by blast define m where "m = Min {(1/2)^(to_nat i) * e i|i. i ∈ I}" have "m > 0" if "I≠{}" unfolding m_def Min_gr_iff using ‹finite I› ‹I ≠ {}› ‹⋀i. e i > 0› by auto moreover have "{y. dist x y < m} ⊆ U" proof (auto) fix y assume "dist x y < m" have "y i ∈ X i" if "i ∈ I" for i proof - have *: "summable (λn. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)" by (rule summable_comparison_test'[of "λn. (1/2)^n"], auto simp add: summable_geometric_iff) define n where "n = to_nat i" have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 < m" using ‹dist x y < m› unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto then have "(1/2)^(to_nat i) * min (dist (x i) (y i)) 1 < m" using ‹n = to_nat i› by auto also have "... ≤ (1/2)^(to_nat i) * e i" unfolding m_def apply (rule Min_le) using ‹finite I› ‹i ∈ I› by auto ultimately have "min (dist (x i) (y i)) 1 < e i" by (auto simp add: field_split_simps) then have "dist (x i) (y i) < e i" using ‹e i < 1› by auto then show "y i ∈ X i" using ‹ball (x i) (e i) ⊆ X i› by auto qed then have "y ∈ Pi⇩_{E}UNIV X" using H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff) then show "y ∈ U" using ‹Pi⇩_{E}UNIV X ⊆ U› by auto qed ultimately have *: "∃m>0. {y. dist x y < m} ⊆ U" if "I ≠ {}" using that by auto have "U = UNIV" if "I = {}" using that H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff) then have "∃m>0. {y. dist x y < m} ⊆ U" if "I = {}" using that zero_less_one by blast then show "∃m>0. {y. dist x y < m} ⊆ U" using * by blast qed lemma ball_fun_contains_open_aux: fixes x::"('a ⇒ 'b)" and e::real assumes "e>0" shows "∃U. open U ∧ x ∈ U ∧ U ⊆ {y. dist x y < e}" proof - have "∃N::nat. 2^N > 8/e" by (simp add: real_arch_pow) then obtain N::nat where "2^N > 8/e" by auto define f where "f = e/4" have [simp]: "e>0" "f > 0" unfolding f_def using assms by auto define X::"('a ⇒ 'b set)" where "X = (λi. if (∃n≤N. i = from_nat n) then {z. dist (x i) z < f} else UNIV)" have "{i. X i ≠ UNIV} ⊆ from_nat`{0..N}" unfolding X_def by auto then have "finite {i. X i ≠ topspace euclidean}" unfolding topspace_euclidean using finite_surj by blast have "⋀i. open (X i)" unfolding X_def using metric_space_class.open_ball open_UNIV by auto then have "⋀i. openin euclidean (X i)" using open_openin by auto define U where "U = Pi⇩_{E}UNIV X" have "open U" unfolding open_fun_def product_topology_def apply (rule topology_generated_by_Basis) unfolding U_def using ‹⋀i. openin euclidean (X i)› ‹finite {i. X i ≠ topspace euclidean}› by auto moreover have "x ∈ U" unfolding U_def X_def by (auto simp add: PiE_iff) moreover have "dist x y < e" if "y ∈ U" for y proof - have *: "dist (x (from_nat n)) (y (from_nat n)) ≤ f" if "n ≤ N" for n using ‹y ∈ U› unfolding U_def apply (auto simp add: PiE_iff) unfolding X_def using that by (metis less_imp_le mem_Collect_eq) have **: "Max {dist (x (from_nat n)) (y (from_nat n))|n. n ≤ N} ≤ f" apply (rule Max.boundedI) using * by auto have "dist x y ≤ 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n ≤ N} + (1/2)^N" by (rule dist_fun_le_dist_first_terms) also have "... ≤ 2 * f + e / 8" apply (rule add_mono) using ** ‹2^N > 8/e› by(auto simp add: field_split_simps) also have "... ≤ e/2 + e/8" unfolding f_def by auto also have "... < e" by auto finally show "dist x y < e" by simp qed ultimately show ?thesis by auto qed lemma fun_open_ball_aux: fixes U::"('a ⇒ 'b) set" shows "open U ⟷ (∀x∈U. ∃e>0. ∀y. dist x y < e ⟶ y ∈ U)" proof (auto) assume "open U" fix x assume "x ∈ U" then show "∃e>0. ∀y. dist x y < e ⟶ y ∈ U" using open_fun_contains_ball_aux[OF ‹open U› ‹x ∈ U›] by auto next assume H: "∀x∈U. ∃e>0. ∀y. dist x y < e ⟶ y ∈ U" define K where "K = {V. open V ∧ V ⊆ U}" { fix x assume "x ∈ U" then obtain e where e: "e>0" "{y. dist x y < e} ⊆ U" using H by blast then obtain V where V: "open V" "x ∈ V" "V ⊆ {y. dist x y < e}" using ball_fun_contains_open_aux[OF ‹e>0›, of x] by auto have "V ∈ K" unfolding K_def using e(2) V(1) V(3) by auto then have "x ∈ (⋃K)" using ‹x ∈ V› by auto } then have "(⋃K) = U" unfolding K_def by auto moreover have "open (⋃K)" unfolding K_def by auto ultimately show "open U" by simp qed instance proof fix x y::"'a ⇒ 'b" show "(dist x y = 0) = (x = y)" proof assume "x = y" then show "dist x y = 0" unfolding dist_fun_def using ‹x = y› by auto next assume "dist x y = 0" have *: "summable (λn. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)" by (rule summable_comparison_test'[of "λn. (1/2)^n"], auto simp add: summable_geometric_iff) have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 = 0" for n using ‹dist x y = 0› unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff) then have "dist (x (from_nat n)) (y (from_nat n)) = 0" for n by (metis div_0 min_def nonzero_mult_div_cancel_left power_eq_0_iff zero_eq_1_divide_iff zero_neq_numeral) then have "x (from_nat n) = y (from_nat n)" for n by auto then have "x i = y i" for i by (metis from_nat_to_nat) then show "x = y" by auto qed next text‹The proof of the triangular inequality is trivial, modulo the fact that we are dealing with infinite series, hence we should justify the convergence at each step. In this respect, the following simplification rule is extremely handy.› have [simp]: "summable (λn. (1/2)^n * min (dist (u (from_nat n)) (v (from_nat n))) 1)" for u v::"'a ⇒ 'b" by (rule summable_comparison_test'[of "λn. (1/2)^n"], auto simp add: summable_geometric_iff) fix x y z::"'a ⇒ 'b" { fix n have *: "dist (x (from_nat n)) (y (from_nat n)) ≤ dist (x (from_nat n)) (z (from_nat n)) + dist (y (from_nat n)) (z (from_nat n))" by (simp add: dist_triangle2) have "0 ≤ dist (y (from_nat n)) (z (from_nat n))" using zero_le_dist by blast moreover { assume "min (dist (y (from_nat n)) (z (from_nat n))) 1 ≠ dist (y (from_nat n)) (z (from_nat n))" then have "1 ≤ min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1" by (metis (no_types) diff_le_eq diff_self min_def zero_le_dist zero_le_one) } ultimately have "min (dist (x (from_nat n)) (y (from_nat n))) 1 ≤ min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1" using * by linarith } note ineq = this have "dist x y = (∑n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)" unfolding dist_fun_def by simp also have "... ≤ (∑n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1 + (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)" apply (rule suminf_le) using ineq apply (metis (no_types, opaque_lifting) add.right_neutral distrib_left le_divide_eq_numeral1(1) mult_2_right mult_left_mono zero_le_one zero_le_power) by (auto simp add: summable_add) also have "... = (∑n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1) + (∑n. (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)" by (rule suminf_add[symmetric], auto) also have "... = dist x z + dist y z" unfolding dist_fun_def by simp finally show "dist x y ≤ dist x z + dist y z" by simp next text‹Finally, we show that the topology generated by the distance and the product topology coincide. This is essentially contained in Lemma ‹fun_open_ball_aux›, except that the condition to prove is expressed with filters. To deal with this, we copy some mumbo jumbo from Lemma ‹eventually_uniformity_metric› in 🗏‹~~/src/HOL/Real_Vector_Spaces.thy›› fix U::"('a ⇒ 'b) set" have "eventually P uniformity ⟷ (∃e>0. ∀x (y::('a ⇒ 'b)). dist x y < e ⟶ P (x, y))" for P unfolding uniformity_fun_def apply (subst eventually_INF_base) by (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"]) then show "open U = (∀x∈U. ∀⇩_{F}(x', y) in uniformity. x' = x ⟶ y ∈ U)" unfolding fun_open_ball_aux by simp qed (simp add: uniformity_fun_def) end text ‹Nice properties of spaces are preserved under countable products. In addition to first countability, second countability and metrizability, as we have seen above, completeness is also preserved, and therefore being Polish.› instance "fun" :: (countable, complete_space) complete_space proof fix u::"nat ⇒ ('a ⇒ 'b)" assume "Cauchy u" have "Cauchy (λn. u n i)" for i unfolding Cauchy_def proof (intro strip) fix e::real assume "e>0" obtain k where "i = from_nat k" using from_nat_to_nat[of i] by metis have "(1/2)^k * min e 1 > 0" using ‹e>0› by auto then have "∃N. ∀m n. N ≤ m ∧ N ≤ n ⟶ dist (u m) (u n) < (1/2)^k * min e 1" using ‹Cauchy u› by (meson Cauchy_def) then obtain N::nat where C: "∀m n. N ≤ m ∧ N ≤ n ⟶ dist (u m) (u n) < (1/2)^k * min e 1" by blast have "∀m n. N ≤ m ∧ N ≤ n ⟶ dist (u m i) (u n i) < e" proof (auto) fix m n::nat assume "m ≥ N" "n ≥ N" have "(1/2)^k * min (dist (u m i) (u n i)) 1 = sum (λp. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1) {k}" using ‹i = from_nat k› by auto also have "... ≤ (∑p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1)" apply (rule sum_le_suminf) by (rule summable_comparison_test'[of "λn. (1/2)^n"], auto simp add: summable_geometric_iff) also have "... = dist (u m) (u n)" unfolding dist_fun_def by auto also have "... < (1/2)^k * min e 1" using C ‹m ≥ N› ‹n ≥ N› by auto finally have "min (dist (u m i) (u n i)) 1 < min e 1" by (auto simp add: field_split_simps) then show "dist (u m i) (u n i) < e" by auto qed then show "∃M. ∀m≥M. ∀n≥M. dist (u m i) (u n i) < e" by blast qed then have "∃x. (λn. u n i) ⇢ x" for i using Cauchy_convergent convergent_def by auto then have "∃x. ∀i. (λn. u n i) ⇢ x i" using choice by force then obtain x where *: "⋀i. (λn. u n i) ⇢ x i" by blast have "u ⇢ x" proof (rule metric_LIMSEQ_I) fix e assume [simp]: "e>(0::real)" have i: "∃K. ∀n≥K. dist (u n i) (x i) < e/4" for i by (rule metric_LIMSEQ_D, auto simp add: *) have "∃K. ∀i. ∀n≥K i. dist (u n i) (x i) < e/4" apply (rule choice) using i by auto then obtain K where K: "⋀i n. n ≥ K i ⟹ dist (u n i) (x i) < e/4" by blast have "∃N::nat. 2^N > 4/e" by (simp add: real_arch_pow) then obtain N::nat where "2^N > 4/e" by auto define L where "L = Max {K (from_nat n)|n. n ≤ N}" have "dist (u k) x < e" if "k ≥ L" for k proof - have *: "dist (u k (from_nat n)) (x (from_nat n)) ≤ e / 4" if "n ≤ N" for n proof - have "K (from_nat n) ≤ L" unfolding L_def apply (rule Max_ge) using ‹n ≤ N› by auto then have "k ≥ K (from_nat n)" using ‹k ≥ L› by auto then show ?thesis using K less_imp_le by auto qed have **: "Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n ≤ N} ≤ e/4" apply (rule Max.boundedI) using * by auto have "dist (u k) x ≤ 2 * Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n ≤ N} + (1/2)^N" using dist_fun_le_dist_first_terms by auto also have "... ≤ 2 * e/4 + e/4" apply (rule add_mono) using ** ‹2^N > 4/e› less_imp_le by (auto simp add: field_split_simps) also have "... < e" by auto finally show ?thesis by simp qed then show "∃L. ∀k≥L. dist (u k) x < e" by blast qed then show "convergent u" using convergent_def by blast qed instance "fun" :: (countable, polish_space) polish_space by standard end