Theory HOL-Analysis.Function_Metric
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 dist_fun_def:
"dist x y = (∑n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
definition 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