Theory Standard_Borel_Spaces.Set_Based_Metric_Product
subsubsection ‹ Product Metric Spaces ›
theory Set_Based_Metric_Product
imports Set_Based_Metric_Space
begin
lemma nsum_of_r':
fixes r :: real
assumes r:"0 < r" "r < 1"
shows "(∑n. r^(n + k) * K) = r^k / (1 - r) * K"
(is "?lhs = _")
proof -
have "?lhs = (∑n. r^n * K) - (∑n∈{..<k}. r^n * K)"
using r by(auto intro!: suminf_minus_initial_segment summable_mult2)
also have "... = 1 / (1 - r) * K - (1 - r^k) / (1 - r) * K"
proof -
have "(∑n∈{..<k}. r^n * K) = (1 - r^k) / (1 - r) * K"
using one_diff_power_eq[of r k] r scale_sum_left[of "λn. r^n" "{..<k}" K,symmetric]
by auto
thus ?thesis
using r by(auto simp add: suminf_geometric[of "r"] suminf_mult2[where c=K,symmetric])
qed
finally show ?thesis
using r by (simp add: diff_divide_distrib left_diff_distrib)
qed
lemma nsum_of_r_leq:
fixes r :: real and a :: "nat ⇒ real"
assumes r:"0 < r" "r < 1"
and a:"⋀n. 0 ≤ a n" "⋀n. a n ≤ K"
shows "0 ≤ (∑n. r^(n + k) * a (n + l))" "(∑n. r^(n + k) * a (n + l)) ≤ r^k / (1 - r) * K"
proof -
have [simp]: "summable (λn. r ^ (n + k) * a (n + l))"
apply(rule summable_comparison_test'[of "λn. r^(n+k) * K"])
using r a by(auto intro!: summable_mult2)
show "0 ≤ (∑n. r^(n + k) * a (n + l))"
using r a by(auto intro!: suminf_nonneg)
have "(∑n. r^(n + k) * a (n + l)) ≤ (∑n. r^(n + k) * K)"
using a r by(auto intro!: suminf_le summable_mult2)
also have "... = r^k / (1 - r) * K"
by(rule nsum_of_r'[OF r])
finally show "(∑n. r^(n + k) * a (n + l)) ≤ r^k / (1 - r) * K" .
qed
lemma nsum_of_r_le:
fixes r :: real and a :: "nat ⇒ real"
assumes r:"0 < r" "r < 1"
and a:"⋀n. 0 ≤ a n" "⋀n. a n ≤ K" "∃n'≥ l. a n' < K"
shows "(∑n. r^(n + k) * a (n + l)) < r^k / (1 - r) * K"
proof -
obtain n' where hn': "a (n' + l) < K"
using a(3) by (metis add.commute le_iff_add)
define a' where "a' = (λn. if n = n' + l then K else a n)"
have a': "⋀n. 0 ≤ a' n" "⋀n. a' n ≤ K"
using a(1,2) le_trans order.trans[OF a(1,2)[of 0]] by(auto simp: a'_def)
have [simp]: "summable (λn. r ^ (n + k) * a (n + l))"
apply(rule summable_comparison_test'[of "λn. r^(n+k) * K"])
using r a by(auto intro!: summable_mult2)
have [simp]: "summable (λn. r^(n + k) * a' (n + l))"
apply(rule summable_comparison_test'[of "λn. r^(n+k) * K"])
using r a' by(auto intro!: summable_mult2)
have "(∑n. r^(n + k) * a (n + l)) = (∑n. r^(n + Suc n' + k) * a (n + Suc n'+ l)) + (∑i<Suc n'. r^(i + k) * a (i + l))"
by(rule suminf_split_initial_segment) simp
also have "... = (∑n. r^(n + Suc n' + k) * a (n + Suc n'+ l)) + (∑i<n'. r^(i + k) * a (i + l)) + r^(n' + k) * a (n' + l)"
by simp
also have "... < (∑n. r^(n + Suc n' + k) * a (n + Suc n'+ l)) + (∑i<n'. r^(i + k) * a (i + l)) + r^(n' + k) * K"
using r hn' by auto
also have "... = (∑n. r^(n + Suc n' + k) * a' (n + Suc n'+ l)) + (∑i<Suc n'. r^(i + k) * a' (i + l))"
by(auto simp: a'_def)
also have "... = (∑n. r^(n + k) * a' (n + l))"
by(rule suminf_split_initial_segment[symmetric]) simp
also have "... ≤ r^k / (1 - r) * K"
by(rule nsum_of_r_leq[OF r a'])
finally show ?thesis .
qed
definition product_dist' :: "[real, 'i set, nat ⇒ 'i, 'i ⇒ 'a set, 'i ⇒ 'a ⇒ 'a ⇒ real] ⇒ ('i ⇒ 'a) ⇒ ('i ⇒ 'a) ⇒ real" where
product_dist_def: "product_dist' r I g Mi di ≡ (λx y. if x ∈ (Π⇩E i∈I. Mi i) ∧ y ∈ (Π⇩E i∈I. Mi i) then (∑n. if g n ∈ I then r^n * di (g n) (x (g n)) (y (g n)) else 0) else 0)"
text ‹ $d(x,y) = \sum_{n\in \mathbb{N}} r^n * d_{g_I(i)}(x_{g_I(i)},y_{g_I(i)})$.›
locale Product_metric =
fixes r :: real
and I :: "'i set"
and f :: "'i ⇒ nat"
and g :: "nat ⇒ 'i"
and Mi :: "'i ⇒ 'a set"
and di :: "'i ⇒ 'a ⇒ 'a ⇒ real"
and K :: real
assumes r: "0 < r" "r < 1"
and I: "countable I"
and gf_comp_id : "⋀i. i ∈ I ⟹ g (f i) = i"
and gf_if_finite: "finite I ⟹ bij_betw f I {..< card I}"
"finite I ⟹ bij_betw g {..< card I} I"
and gf_if_infinite: "infinite I ⟹ bij_betw f I UNIV"
"infinite I ⟹ bij_betw g UNIV I"
"⋀n. infinite I ⟹ f (g n) = n"
and Md_metric: "⋀i. i ∈ I ⟹ Metric_space (Mi i) (di i)"
and di_nonneg: "⋀i x y. 0 ≤ di i x y"
and di_bounded: "⋀i x y. di i x y ≤ K"
and K_pos : "0 < K"
lemma from_nat_into_to_nat_on_product_metric_pair:
assumes "countable I"
shows "⋀i. i ∈ I ⟹ from_nat_into I (to_nat_on I i) = i"
and "finite I ⟹ bij_betw (to_nat_on I) I {..< card I}"
and "finite I ⟹ bij_betw (from_nat_into I) {..< card I} I"
and "infinite I ⟹ bij_betw (to_nat_on I) I UNIV"
and "infinite I ⟹ bij_betw (from_nat_into I) UNIV I"
and "⋀n. infinite I ⟹ to_nat_on I (from_nat_into I n) = n"
by(simp_all add: assms to_nat_on_finite bij_betw_from_nat_into_finite to_nat_on_infinite bij_betw_from_nat_into)
lemma product_metric_pair_finite_nat:
"bij_betw id {..n} {..< card {..n}}" "bij_betw id {..< card {..n}} {..n}"
by(auto simp: bij_betw_def)
lemma product_metric_pair_finite_nat':
"bij_betw id {..<n} {..< card {..<n}}" "bij_betw id {..< card {..<n}} {..<n}"
by(auto simp: bij_betw_def)
context Product_metric
begin
abbreviation "product_dist ≡ product_dist' r I g Mi di"
lemma nsum_of_rK: "(∑n. r^(n + k)*K) = r^k / (1 - r) * K"
by(rule nsum_of_r'[OF r])
lemma i_min:
assumes "i ∈ I" "g n = i"
shows "f i ≤ n"
proof(cases "finite I")
case h:True
show ?thesis
proof(rule ccontr)
assume "¬ f i ≤ n"
then have h0:"n < f i" by simp
have "f i ∈ {..<card I}"
using bij_betwE[OF gf_if_finite(1)[OF h]] assms(1) by simp
moreover have "n ∈ {..<card I}" "n ≠ f i"
using h0 ‹f i ∈ {..<card I}› by auto
ultimately have "g n ≠ g (f i)"
using bij_betw_imp_inj_on[OF gf_if_finite(2)[OF h]]
by (simp add: inj_on_contraD)
thus False
by(simp add: gf_comp_id[OF assms(1)] assms(2))
qed
next
show "infinite I ⟹ f i ≤ n"
using assms(2) gf_if_infinite(3)[of n] by simp
qed
lemma g_surj:
assumes "i ∈ I"
shows "∃n. g n = i"
using gf_comp_id[of i] assms by auto
lemma product_dist_summable'[simp]:
"summable (λn. r^n * di (g n) (x (g n)) (y (g n)))"
apply(rule summable_comparison_test'[of "λn. r^n * K"])
using r di_nonneg di_bounded K_pos by(auto intro!: summable_mult2)
lemma product_dist_summable[simp]:
"summable (λn. if g n ∈ I then r^n * di (g n) (x (g n)) (y (g n)) else 0)"
by(rule summable_comparison_test'[of "λn. r^n * di (g n) (x (g n)) (y (g n))"]) (use r di_nonneg di_bounded K_pos in auto)
lemma summable_rK[simp]: "summable (λn. r^n * K)"
using r by(auto intro!: summable_mult2)
lemma Product_metric: "Metric_space (Π⇩E i∈I. Mi i) product_dist"
proof -
have h': "⋀i xi yi. i ∈ I ⟹ xi ∈ Mi i ⟹ yi ∈ Mi i ⟹ xi = yi ⟷ di i xi yi = 0"
"⋀i xi yi. i ∈ I ⟹ di i xi yi = di i yi xi"
"⋀i xi yi zi. i ∈ I ⟹ xi ∈ Mi i ⟹ yi ∈ Mi i ⟹ zi ∈ Mi i ⟹ di i xi zi ≤ di i xi yi + di i yi zi"
using Md_metric by(auto simp: Metric_space_def)
show ?thesis
proof
show "⋀x y. 0 ≤ product_dist x y"
using di_nonneg r by(auto simp: product_dist_def intro!: suminf_nonneg product_dist_summable)
next
fix x y
assume hxy:"x ∈ (Π⇩E i∈I. Mi i)" "y ∈ (Π⇩E i∈I. Mi i)"
show "(product_dist x y = 0) ⟷ (x = y)"
proof
assume heq:"x = y"
then have "(if g n ∈ I then r ^ n * di (g n) (x (g n)) (y (g n)) else 0) = 0" for n
using hxy h'(1)[of "g n" "x (g n)" "y (g n)"] by(auto simp: product_dist_def)
thus "product_dist x y = 0"
by(auto simp: product_dist_def)
next
assume h0:"product_dist x y = 0"
have "(∑n. if g n ∈ I then r ^ n * di (g n) (x (g n)) (y (g n)) else 0) = 0
⟷ (∀n. (if g n ∈ I then r^n * di (g n) (x (g n)) (y (g n)) else 0) = 0)"
apply(rule suminf_eq_zero_iff)
using di_nonneg r by(auto simp: product_dist_def intro!: product_dist_summable)
hence hn0:"⋀n. (if g n ∈ I then r^n * di (g n) (x (g n)) (y (g n)) else 0) = 0"
using h0 hxy by(auto simp: product_dist_def)
show "x = y"
proof
fix i
consider "i ∈ I" | "i ∉ I" by auto
thus "x i = y i"
proof cases
case 1
from g_surj[OF this] obtain n where
hn: "g n = i" by auto
have "di (g n) (x (g n)) (y (g n)) = 0"
using hn h'(1)[OF 1,of "x i" "y i"] hxy hn0[of n] 1 r by simp
thus ?thesis
using hn h'(1)[OF 1,of "x i" "y i"] hxy 1 by auto
next
case 2
then show ?thesis
by(simp add: PiE_arb[OF hxy(1) 2] hxy PiE_arb[OF hxy(2) 2])
qed
qed
qed
next
show "product_dist x y = product_dist y x" for x y
using h'(2) by(auto simp: product_dist_def) (metis (no_types, opaque_lifting))
next
fix x y z
assume hxyz:"x ∈ (Π⇩E i∈I. Mi i)" "y ∈ (Π⇩E i∈I. Mi i)" "z ∈ (Π⇩E i∈I. Mi i)"
have "(if g n ∈ I then r ^ n * di (g n) (x (g n)) (z (g n)) else 0)
≤ (if g n ∈ I then r ^ n * di (g n) (x (g n)) (y (g n)) else 0) + (if g n ∈ I then r ^ n * di (g n) (y (g n)) (z (g n)) else 0)" for n
using h'(3)[of "g n" "x (g n)" "y (g n)" "z (g n)"] hxyz r
by(auto simp: distrib_left[of "r ^ n",symmetric])
thus "product_dist x z ≤ product_dist x y + product_dist y z"
by(auto simp add: product_dist_def suminf_add[OF product_dist_summable[of x y] product_dist_summable[of y z]] hxyz intro!: suminf_le summable_add)
qed
qed
sublocale Product_metric: Metric_space "Π⇩E i∈I. Mi i" "product_dist"
by(rule Product_metric)
lemma product_dist_leqr: "product_dist x y ≤ 1 / (1 - r) * K"
proof -
have "product_dist x y ≤ (∑n. if g n ∈ I then r^n * di (g n) (x (g n)) (y (g n)) else 0)"
proof -
consider "x ∈ (Π⇩E i∈I. Mi i) ∧ y ∈ (Π⇩E i∈I. Mi i)" | "¬ (x ∈ (Π⇩E i∈I. Mi i) ∧ y ∈ (Π⇩E i∈I. Mi i))" by auto
then show ?thesis
proof cases
case 1
then show ?thesis by(auto simp: product_dist_def)
next
case 2
then have "product_dist x y = 0"
by(auto simp: product_dist_def)
also have "... ≤ (∑n. if g n ∈ I then r^n * di (g n) (x (g n)) (y (g n)) else 0)"
using di_nonneg r by(auto intro!: suminf_nonneg product_dist_summable)
finally show ?thesis .
qed
qed
also have "... ≤ (∑n. r^n * di (g n) (x (g n)) (y (g n)))"
using r di_nonneg di_bounded by(auto intro!: suminf_le)
also have "... ≤ (∑n. r^n * K)"
using r di_bounded di_nonneg by(auto intro!: suminf_le)
also have "... = 1 / (1 - r) * K"
using r nsum_of_rK[of 0] by simp
finally show ?thesis .
qed
lemma product_dist_geq:
assumes "i ∈ I" and "g n = i" "x ∈ (Π⇩E i∈I. Mi i)" "y ∈ (Π⇩E i∈I. Mi i)"
shows "di i (x i) (y i) ≤ (1/r)^n * product_dist x y"
(is "?lhs ≤ ?rhs")
proof -
interpret mi: Metric_space "Mi i" "di i"
by(rule Md_metric[OF assms(1)])
have "(λm. if m = f i then di (g m) (x (g m)) (y (g m)) else 0) sums di (g (f i)) (x (g (f i))) (y (g (f i)))"
by(rule sums_single)
also have "... = ?lhs"
by(simp add: gf_comp_id[OF assms(1)])
finally have 1:"summable (λm. if m = f i then di (g m) (x (g m)) (y (g m)) else 0)"
"?lhs = (∑m. (if m = f i then di (g m) (x (g m)) (y (g m)) else 0))"
by(auto simp: sums_iff)
note 1(2)
also have "... ≤ (∑m. (1/r)^n * (if g m ∈ I then r^m * di (g m) (x (g m)) (y (g m)) else 0))"
proof(rule suminf_le)
show "summable (λm. (1/r)^n * (if g m ∈ I then r^m * di (g m) (x (g m)) (y (g m)) else 0))"
by(auto intro!: product_dist_summable)
next
fix k
have **:"1 ≤ (1/r) ^ n * r ^ f i"
proof -
have "(1/r) ^ n * (r ^ f i) = (1/r)^(n-f i) * (1/r)^(f i) * r ^ f i"
using r by(simp add: power_diff[OF _ i_min[OF assms(1,2)],of "1/r",simplified])
also have "... = (1/r) ^ (n-f i)"
using r by (simp add: power_one_over)
finally show ?thesis
using r by auto
qed
have *:"g k ∈ I" if "k = f i"
using gf_comp_id[OF assms(1)] assms(1) that by auto
show "(if k = f i then di (g k) (x (g k)) (y (g k)) else 0) ≤ (1/r) ^ n * (if g k ∈ I then r ^ k * di (g k) (x (g k)) (y (g k)) else 0)"
using * di_nonneg r ** mult_right_mono[OF **] by(auto simp: vector_space_over_itself.scale_scale[of "(1 / r) ^ n"])
qed(simp add: 1)
also have "... = ?rhs"
unfolding product_dist_def
using assms by(auto intro!: suminf_mult product_dist_summable)
finally show ?thesis .
qed
lemma limitin_M_iff_limitin_Mi:
shows "limitin Product_metric.mtopology xn x sequentially ⟷ (∃N. ∀n≥N. (∀i∈I. xn n i ∈ Mi i) ∧ (∀i. i∉I ⟶ xn n i = undefined)) ∧ (∀i∈I. limitin (Metric_space.mtopology (Mi i) (di i)) (λn. xn n i) (x i) sequentially) ∧ x ∈ (Π⇩E i∈I. Mi i)"
proof safe
fix i
assume h:"limitin Product_metric.mtopology xn x sequentially"
then show "∃N. ∀n≥N. (∀i∈I. xn n i ∈ Mi i) ∧ (∀i. i∉I ⟶ xn n i = undefined)"
by(simp only: Product_metric.limit_metric_sequentially) (metis PiE_E r(1))
then obtain N' where N': "⋀i n. i ∈ I ⟹ n ≥ N' ⟹ xn n i ∈ Mi i" "⋀i n. i ∉ I ⟹ n ≥ N' ⟹ xn n i = undefined"
by blast
assume i:"i ∈ I"
then interpret m: Metric_space "Mi i" "di i"
using Md_metric by blast
show "limitin m.mtopology (λn. xn n i) (x i) sequentially"
unfolding m.limitin_metric eventually_sequentially
proof safe
show "x i ∈ Mi i"
using h i by(auto simp: Product_metric.limitin_metric)
next
fix ε :: real
assume "0 < ε"
then obtain "r^ f i * ε > 0" using r by auto
then obtain N where N:"⋀n. n ≥ N ⟹ product_dist (xn n) x < r^ f i * ε"
using h(1) by(fastforce simp: Product_metric.limitin_metric eventually_sequentially)
show "∃N. ∀n≥N. xn n i ∈ Mi i ∧ di i (xn n i) (x i) < ε"
proof(safe intro!: exI[where x="max N N'"])
fix n
assume "max N N' ≤ n"
then have "N ≤ n" "N' ≤ n"
by auto
have "di i (xn n i) (x i) ≤ (1 / r) ^ f i * product_dist (xn n) x"
thm product_dist_geq[OF i gf_comp_id[OF i] ]
using h i N'[OF _ ‹N' ≤ n›] by(auto intro!: product_dist_geq[OF i gf_comp_id[OF i] ] dest: Product_metric.limitin_mspace)
also have "... < (1 / r) ^ f i * r^ f i * ε"
using N[OF ‹N ≤ n›] r by auto
also have "... ≤ ε"
by (simp add: ‹0 < ε› power_one_over)
finally show "di i (xn n i) (x i) < ε" .
qed(use N' h i in auto)
qed
next
fix N'
assume N': "∀n≥N'. (∀i∈I. xn n i ∈ Mi i) ∧ (∀i. i ∉ I ⟶ xn n i = undefined)"
assume h:"∀i∈I. limitin (Metric_space.mtopology (Mi i) (di i)) (λn. xn n i) (x i) sequentially" "x ∈ (Π⇩E i∈I. Mi i)"
show "limitin Product_metric.mtopology xn x sequentially"
unfolding Product_metric.limitin_metric eventually_sequentially
proof safe
fix ε
assume he:"(0::real) < ε"
then have "0 < ε*((1-r)/K)" using r K_pos by auto
hence "∃k. r^k < ε*((1-r)/K)"
using r(2) real_arch_pow_inv by blast
then obtain l where "r^l < ε*((1-r)/K)" by auto
hence hk:"r^l/(1-r)*K < ε"
using mult_imp_div_pos_less[OF divide_pos_pos[OF _ K_pos,of "1-r"]] r(2) by simp
hence hke: "0 < ε - r^l/(1-r)*K" by auto
consider "l = 0" | "0 < l" by auto
then show "∃N. ∀n≥N. xn n ∈ (Π⇩E i∈I. Mi i) ∧ product_dist (xn n) x < ε"
proof cases
case 1
then have he2:"1 / (1 - r)*K < ε" using hk by auto
show ?thesis
using order.strict_trans1[OF product_dist_leqr he2] N'
by(auto intro!: exI[where x=N'])
next
case 2
with hke have "0 < 1 / real l * (ε - r^l/(1-r)*K)" by auto
hence "∀i∈I. ∃N. ∀n≥N. di i (xn n i) (x i) < 1 / real l * (ε - r^l/(1-r)*K)"
using h by (meson Md_metric Metric_space.limit_metric_sequentially)
then obtain N where hn:
"⋀i n. i ∈ I ⟹ n ≥ N i ⟹ di i (xn n i) (x i) < 1 / real l * (ε - r^l/(1-r)*K)"
by metis
show ?thesis
proof(safe intro!: exI[where x="max (Sup {N (g n) | n. n < l}) N'"])
fix n
assume "max (⨆ {N (g n) |n. n < l}) N' ≤ n"
then have hsup:"⨆ {N (g n) |n. n < l} ≤ n" and N'n: "N' ≤ n"
by auto
have "product_dist (xn n) x = (∑m. if g m ∈ I then r ^ m * di (g m) (xn n (g m)) (x (g m)) else 0)"
using N' N'n h by(auto simp: product_dist_def)
also have "... = (∑m. if g (m + l) ∈ I then r ^ (m + l)* di (g (m + l)) (xn n (g (m + l))) (x (g (m + l))) else 0) + (∑m<l. if g m ∈ I then r ^ m * di (g m) (xn n (g m)) (x (g m)) else 0)"
by(auto intro!: suminf_split_initial_segment)
also have "... ≤ r^l/(1-r)*K + (∑m<l. if g m ∈ I then r ^ m * di (g m) (xn n (g m)) (x(g m)) else 0)"
proof -
have "(∑m. if g (m + l) ∈ I then r ^ (m + l)* di (g (m + l)) (xn n (g (m + l))) (x (g (m + l))) else 0) ≤ (∑m. r^(m + l)*K)"
using di_bounded N' r K_pos by(auto intro!: suminf_le summable_ignore_initial_segment)
also have "... = r^l/(1-r)*K"
by(rule nsum_of_rK)
finally show ?thesis by auto
qed
also have "... ≤ r^l / (1 - r)*K + (∑m<l. if g m ∈ I then di (g m) (xn n (g m)) (x (g m)) else 0)"
proof -
have " (∑m<l. if g m ∈ I then r ^ m * di (g m) (xn n (g m)) (x (g m)) else 0) ≤ (∑m<l. if g m ∈ I then di (g m) (xn n (g m)) (x (g m)) else 0)"
using di_bounded di_nonneg r by(auto intro!: sum_mono simp: mult_left_le_one_le power_le_one)
thus ?thesis by simp
qed
also have "... < r^l / (1 - r)*K + (∑m<l. 1 / real l * (ε - r^l/(1-r)*K))"
proof -
have "(∑m<l. if g m ∈ I then di (g m) (xn n (g m)) (x (g m)) else 0) < (∑m<l. 1 / real l * (ε - r^l/(1-r)*K))"
proof(rule sum_strict_mono_ex1)
show "∀p∈{..<l}. (if g p ∈ I then di (g p) (xn n (g p)) (x (g p)) else 0) ≤ 1 / real l * (ε - r ^ l / (1 - r)*K)"
proof -
have "0 ≤ (ε - r ^ l * K / (1 - r)) / real l"
using hke by auto
moreover {
fix p
assume "p < l" "g p ∈ I"
then have "N (g p) ∈ {N (g n) |n. n < l}"
by auto
from le_cSup_finite[OF _ this] hsup have "N (g p) ≤ n"
by auto
hence "di (g p) (xn n (g p)) (x (g p)) ≤ (ε - r ^ l *K/ (1 - r)) / real l"
using hn[OF ‹g p ∈ I›,of n] by simp
}
ultimately show ?thesis
by auto
qed
next
show "∃a∈{..<l}. (if g a ∈ I then di (g a) (xn n (g a)) (x (g a)) else 0) < 1 / real l * (ε - r ^ l / (1 - r)*K)"
proof -
have "0 < (ε - r ^ l * K / (1 - r)) / real l"
using hke 2 by auto
moreover {
assume "g 0 ∈ I"
have "N (g 0) ∈ {N (g n) |n. n < l}"
using 2 by auto
from le_cSup_finite[OF _ this] hsup have "N (g 0) ≤ n"
by auto
hence "di (g 0) (xn n (g 0)) (x (g 0)) < (ε - r ^ l * K/ (1 - r)) / real l"
using hn[OF ‹g 0 ∈ I›,of n] by simp
}
ultimately show ?thesis
by(auto intro!: bexI[where x=0] simp: 2)
qed
qed simp
thus ?thesis by simp
qed
also have "... = ε"
using 2 by auto
finally show "product_dist (xn n) x < ε" .
qed(use N' in auto)
qed
qed (use N' h in auto)
qed(auto simp: Product_metric.limitin_metric)
lemma Product_metric_mtopology_eq: "product_topology (λi. Metric_space.mtopology (Mi i) (di i)) I = Product_metric.mtopology"
proof -
have htopspace:"⋀i. i ∈ I ⟹ topspace (Metric_space.mtopology (Mi i) (di i)) = Mi i"
by (simp add: Md_metric Metric_space.topspace_mtopology)
hence htopspace':"(Π⇩E i∈I. topspace (Metric_space.mtopology (Mi i) (di i))) = (Π⇩E i∈I. Mi i)" by auto
consider "I = {}" | "I ≠ {}" by auto
then show ?thesis
proof cases
case 1
interpret d: discrete_metric "{λx. undefined}" .
have "product_dist = (λx y. 0)"
by standard+ (auto simp: product_dist_def 1)
hence 2:"Product_metric.mtopology = d.disc.mtopology"
by (metis "1" PiE_empty_domain Product_metric.open_in_mspace Product_metric.topspace_mtopology d.mtopology_discrete_metric discrete_topology_unique singleton_iff)
show ?thesis
unfolding 2 by(simp add: product_topology_empty_discrete 1 d.mtopology_discrete_metric)
next
case I':2
show ?thesis
unfolding base_is_subbase[OF Product_metric.mtopology_base_in_balls,simplified subbase_in_def] product_topology_def
proof(rule topology_generated_by_eq)
fix U
assume "U ∈ {Product_metric.mball a ε |a ε. a ∈ (Π⇩E i∈I. Mi i) ∧ 0 < ε}"
then obtain a ε where hu:
"U = Product_metric.mball a ε" "a ∈ (Π⇩E i∈I. Mi i)" "0 < ε" by auto
have "∃X. x ∈ (Π⇩E i∈I. X i) ∧ (Π⇩E i∈I. X i) ⊆ U ∧ (∀i. openin (Metric_space.mtopology (Mi i) (di i)) (X i)) ∧ finite {i. X i ≠ topspace (Metric_space.mtopology (Mi i) (di i))}" if "x ∈ U" for x
proof -
consider "ε ≤ 1 / (1 - r) * K" | "1 / (1 - r) * K < ε" by fastforce
then show "∃X. x ∈ (Π⇩E i∈I. X i) ∧ (Π⇩E i∈I. X i) ⊆ U ∧ (∀i. openin (Metric_space.mtopology (Mi i) (di i)) (X i)) ∧ finite {i. X i ≠ topspace (Metric_space.mtopology (Mi i) (di i))}"
proof cases
case he2:1
have "0 < (ε - product_dist a x)*((1-r)/ K)" using r hu K_pos that hu by auto
hence "∃k. r^k < (ε - product_dist a x)*((1-r)/ K)"
using r(2) real_arch_pow_inv by blast
then obtain k where "r^k < (ε - product_dist a x)*((1-r)/ K)" by auto
hence hk:"r^k / (1-r) * K < (ε - product_dist a x)"
using mult_imp_div_pos_less[OF divide_pos_pos[OF _ K_pos,of "1-r"]] r(2) by auto
have hk': "0 < k" apply(rule ccontr) using hk he2 Product_metric.nonneg[of a x] by auto
define ε' where "ε' ≡ (1/(real k))*(ε - product_dist a x - r^k / (1-r) * K)"
have hε' : "0 < ε'" using hk by(auto simp: ε'_def hk')
define X where "X ≡ (if finite I then (λi. if i ∈ I then Metric_space.mball (Mi i) (di i) (x i) ε' else topspace (Metric_space.mtopology (Mi i) (di i))) else (λi. if i ∈ I ∧ f i < k then Metric_space.mball (Mi i) (di i) (x i) ε' else topspace (Metric_space.mtopology (Mi i) (di i))))"
show ?thesis
proof(intro exI[where x=X] conjI)
have "x i ∈ Metric_space.mball (Mi i) (di i) (x i) ε'" if "i ∈ I" for i
using hu ‹x ∈ U› by (auto simp add: PiE_mem hε' Md_metric Metric_space.centre_in_mball_iff that)
thus "x ∈ (Π⇩E i∈I. X i)"
using hu that htopspace by(auto simp: X_def)
next
show "(Π⇩E i∈I. X i) ⊆ U"
proof
fix y
assume "y ∈ (Π⇩E i∈I. X i)"
have "⋀i. X i ⊆ topspace (Metric_space.mtopology (Mi i) (di i))"
by (simp add: Md_metric Metric_space.mball_subset_mspace X_def htopspace)
hence "y ∈ (Π⇩E i∈I. Mi i)"
using htopspace' ‹y ∈ (Π⇩E i∈I. X i)› by blast
have "product_dist a y < ε"
proof -
have "product_dist a y ≤ product_dist a x + product_dist x y"
using Product_metric.triangle ‹y ∈ Pi⇩E I Mi› hu(1) that by auto
also have "... < product_dist a x + (ε - product_dist a x)"
proof -
have "product_dist x y < (ε - product_dist a x)"
proof -
have "product_dist x y = (∑n. if g n ∈ I then r ^ n * di (g n) (x (g n)) (y (g n)) else 0)"
by (metis (no_types, lifting) hu(1) that ‹y ∈ (Π⇩E i∈I. Mi i)› Product_metric.in_mball product_dist_def suminf_cong)
also have "... = (∑n. if g (n + k) ∈ I then r ^ (n + k)* di (g (n + k)) (x (g (n + k))) (y (g (n + k))) else 0) + (∑n<k. if g n ∈ I then r ^ n * di (g n) (x (g n)) (y (g n)) else 0)"
by(rule suminf_split_initial_segment) simp
also have "... ≤ r^k / (1 - r) * K + (∑n<k. if g n ∈ I then r ^ n * di (g n) (x (g n)) (y (g n)) else 0)"
proof -
have "(∑n. if g (n + k) ∈ I then r ^ (n + k)* di (g (n + k)) (x (g (n + k))) (y (g (n + k))) else 0) ≤ (∑n. r ^ (n + k) * K)"
using di_bounded di_nonneg r K_pos by(auto intro!: suminf_le summable_ignore_initial_segment)
also have "... = r^k / (1 - r) * K"
by(rule nsum_of_rK)
finally show ?thesis by simp
qed
also have "... < r^k / (1 - r) * K + (ε - product_dist a x - r^k / (1 - r) * K)"
proof -
have "(∑n<k. if g n ∈ I then r ^ n * di (g n) (x (g n)) (y (g n)) else 0) < (∑n<k. ε')"
proof(rule sum_strict_mono_ex1)
show "∀l∈{..<k}. (if g l ∈ I then r ^ l * di (g l) (x (g l)) (y (g l)) else 0) ≤ ε'"
proof -
{
fix l
assume "g l ∈ I" "l < k"
then interpret mbd: Metric_space "Mi (g l)" "di (g l)"
by(auto intro!: Md_metric)
have "r ^ l * di (g l) (x (g l)) (y (g l)) ≤ di (g l) (x (g l)) (y (g l))"
using r by(auto intro!: mult_right_mono[of "r ^ l" 1,OF _ mbd.nonneg[of "x (g l)" "y (g l)"],simplified] simp: power_le_one)
also have "... < ε'"
proof -
have "y (g l) ∈ mbd.mball (x (g l)) ε'"
proof(cases "finite I")
case True
then show ?thesis
using PiE_mem[OF ‹y ∈ (Π⇩E i∈I. X i)› ‹g l ∈ I›]
by(simp add: X_def ‹g l ∈ I›)
next
case False
then show ?thesis
using PiE_mem[OF ‹y ∈ (Π⇩E i∈I. X i)› ‹g l ∈ I›] gf_if_infinite(3)
by(simp add: X_def ‹g l ∈ I› ‹l < k›)
qed
thus ?thesis
by auto
qed
finally have "r ^ l * di (g l) (x (g l)) (y (g l)) ≤ ε'" by simp
}
thus ?thesis
by(auto simp: order.strict_implies_order[OF hε'])
qed
next
show "∃a∈{..<k}. (if g a ∈ I then r ^ a * di (g a) (x (g a)) (y (g a)) else 0) < ε'"
proof(rule bexI[where x=0])
{
assume "g 0 ∈ I"
then interpret mbd: Metric_space "Mi (g 0)" "di (g 0)"
by(auto intro!: Md_metric)
have "y (g 0) ∈ mbd.mball (x (g 0)) ε'"
proof(cases "finite I")
case True
then show ?thesis
using PiE_mem[OF ‹y ∈ (Π⇩E i∈I. X i)› ‹g 0 ∈ I›]
by(simp add: X_def ‹g 0 ∈ I›)
next
case False
then show ?thesis
using PiE_mem[OF ‹y ∈ (Π⇩E i∈I. X i)› ‹g 0 ∈ I›] gf_if_infinite(3)
by(simp add: X_def ‹g 0 ∈ I› ‹0 < k›)
qed
hence "r ^ 0 * di (g 0) (x (g 0)) (y (g 0)) < ε'"
by auto
}
thus "(if g 0 ∈ I then r ^ 0 * di (g 0) (x (g 0)) (y (g 0)) else 0) < ε'"
using hε' by auto
qed(use hk' in auto)
qed simp
also have "... = (ε - product_dist a x - r ^ k / (1 - r) * K)"
by(simp add: ε'_def hk')
finally show ?thesis by simp
qed
finally show ?thesis by simp
qed
thus ?thesis by simp
qed
finally show ?thesis by auto
qed
thus "y ∈ U"
by(simp add: hu(1) hu(2) ‹y ∈ (Π⇩E i∈I. Mi i)›)
qed
next
have "openin (Metric_space.mtopology (Mi i) (di i)) (Metric_space.mball (Mi i) (di i) (x i) ε')" if "i ∈ I" for i
by (simp add: Md_metric Metric_space.openin_mball that)
moreover have "openin (Metric_space.mtopology (Mi i) (di i)) (topspace (Metric_space.mtopology (Mi i) (di i)))" for i
by auto
ultimately show "∀i. openin (Metric_space.mtopology (Mi i) (di i)) (X i)"
by(auto simp: X_def)
next
show "finite {i. X i ≠ topspace (Metric_space.mtopology (Mi i) (di i))}"
proof(cases "finite I")
case True
then show ?thesis
by(simp add: X_def)
next
case Iinf:False
have "finite {i ∈ I. f i < k}"
proof -
have "{i ∈ I. f i < k} = inv_into I f ` {..<k}"
proof -
have *:"⋀i. i ∈ I ⟹ inv_into I f (f i) = i"
"⋀n. f (inv_into I f n) = n"
using bij_betw_inv_into_left[OF gf_if_infinite(1)[OF Iinf]]
bij_betw_inv_into_right[OF gf_if_infinite(1)[OF Iinf]]
by auto
show ?thesis
proof
show "{i ∈ I. f i < k} ⊆ inv_into I f ` {..<k}"
proof
show "p ∈ {i ∈ I. f i < k} ⟹ p ∈ inv_into I f ` {..<k}" for p
using *(1)[of p] by (auto simp: rev_image_eqI)
qed
next
show " inv_into I f ` {..<k} ⊆ {i ∈ I. f i < k} "
using *(2) bij_betw_inv_into[OF gf_if_infinite(1)[OF Iinf]]
by (auto simp: bij_betw_def)
qed
qed
also have "finite ..." by auto
finally show ?thesis .
qed
thus ?thesis
by(simp add: X_def Iinf)
qed
qed
next
case 2
then have "U = (Π⇩E i∈I. Mi i)"
unfolding hu(1) using order.strict_trans1[OF product_dist_leqr,of ε] hu(2)
by auto
also have "... = (Π⇩E i∈I. topspace (Metric_space.mtopology (Mi i) (di i)))"
using htopspace by auto
finally have "U = (Π⇩E i∈I. topspace (Metric_space.mtopology (Mi i) (di i)))" .
thus ?thesis
using that hu htopspace by(auto intro!: exI[where x="λi. topspace (Metric_space.mtopology (Mi i) (di i))"])
qed
qed
hence "∃X. ∀x∈U. x ∈ (Π⇩E i∈I. X x i) ∧ (Π⇩E i∈I. X x i) ⊆ U ∧ (∀i. openin (Metric_space.mtopology (Mi i) (di i)) (X x i)) ∧ finite {i. X x i ≠ topspace (Metric_space.mtopology (Mi i) (di i))}"
by(auto intro!: bchoice)
then obtain X where "∀x∈U. x ∈ (Π⇩E i∈I. X x i) ∧ (Π⇩E i∈I. X x i) ⊆ U ∧ (∀i. openin (Metric_space.mtopology (Mi i) (di i)) (X x i)) ∧ finite {i. X x i ≠ topspace (Metric_space.mtopology (Mi i) (di i))}"
by auto
hence hX: "⋀x. x ∈ U ⟹ x ∈ (Π⇩E i∈I. X x i)" "⋀x. x ∈ U ⟹ (Π⇩E i∈I. X x i) ⊆ U" "⋀x. x ∈ U ⟹ (∀i. openin (Metric_space.mtopology (Mi i) (di i)) (X x i))" "⋀x. x ∈ U ⟹ finite {i. X x i ≠ topspace (Metric_space.mtopology (Mi i) (di i))}"
by auto
hence hXopen: "⋀x. x ∈ U ⟹ (Π⇩E i∈I. X x i) ∈ {Π⇩E i∈I. X i |X. (∀i. openin (Metric_space.mtopology (Mi i) (di i)) (X i)) ∧ finite {i. X i ≠ topspace (Metric_space.mtopology (Mi i) (di i))}}"
by blast
have "U = (⋃ {(Π⇩E i∈I. X x i) | x. x ∈ U})"
using hX(1,2) by blast
have "openin (topology_generated_by {Π⇩E i∈I. X i |X. (∀i. openin (Metric_space.mtopology (Mi i) (di i)) (X i)) ∧ finite {i. X i ≠ topspace (Metric_space.mtopology (Mi i) (di i))}}) (⋃ {(Π⇩E i∈I. X x i) | x. x ∈ U})"
apply(rule openin_Union)
using hXopen by(auto simp: openin_topology_generated_by_iff intro!: generate_topology_on.Basis)
thus "openin (topology_generated_by {Π⇩E i∈I. X i |X. (∀i. openin (Metric_space.mtopology (Mi i) (di i)) (X i)) ∧ finite {i. X i ≠ topspace (Metric_space.mtopology (Mi i) (di i))}}) U"
using ‹U = (⋃ {(Π⇩E i∈I. X x i) | x. x ∈ U})› by simp
next
fix U
assume "U ∈ {Π⇩E i∈I. X i |X. (∀i. openin (Metric_space.mtopology (Mi i) (di i)) (X i)) ∧ finite {i. X i ≠ topspace (Metric_space.mtopology (Mi i) (di i))}}"
then obtain X where hX:
"U = (Π⇩E i∈I. X i)" "⋀i. openin (Metric_space.mtopology (Mi i) (di i)) (X i)" "finite {i. X i ≠ topspace (Metric_space.mtopology (Mi i) (di i))}"
by auto
have "∃a ε. x ∈ Product_metric.mball a ε ∧ Product_metric.mball a ε ⊆ U" if "x ∈ U" for x
proof -
have x_intop:"x ∈ (Π⇩E i∈I. Mi i)"
unfolding htopspace'[symmetric] using that hX(1) openin_subset[OF hX(2)] by auto
define I' where "I' ≡ {i. X i ≠ topspace (Metric_space.mtopology (Mi i) (di i))} ∩ I"
then have I':"finite I'" "I' ⊆ I" using hX(3) by auto
consider "I' = {}" | "I' ≠ {}" by auto
then show ?thesis
proof cases
case 1
then have "⋀i. i ∈ I ⟹ X i = topspace (Metric_space.mtopology (Mi i) (di i))"
by(auto simp: I'_def)
then have "U = (Π⇩E i∈I. Mi i)"
by (simp add: PiE_eq hX(1) htopspace)
thus ?thesis
using 1 that by(auto intro!: exI[where x=x] exI[where x=1])
next
case I'_nonempty:2
hence "⋀i. i ∈ I' ⟹ openin (Metric_space.mtopology (Mi i) (di i)) (X i)"
using hX(2) by(simp add: I'_def)
hence "∃ε>0. Metric_space.mball (Mi i) (di i) (x i) ε ⊆ (X i)" if "i ∈ I'" for i
using I'(2) Md_metric Metric_space.openin_mtopology PiE_mem ‹x ∈ U› hX(1) subset_eq that by blast
then obtain εi' where hei:"⋀i. i ∈ I' ⟹ εi' i > 0" "⋀i. i ∈ I' ⟹ Metric_space.mball (Mi i) (di i) (x i) (εi' i) ⊆ (X i)"
by metis
define ε where "ε ≡ Min {εi' i |i. i ∈ I'}"
have εmin: "⋀i. i ∈ I' ⟹ ε ≤ εi' i"
using I' by(auto simp: ε_def intro!: Min.coboundedI)
have hε: "ε > 0"
using I' I'_nonempty Min_gr_iff[of "{εi' i |i. i ∈ I'}" 0] hei(1)
by(auto simp: ε_def)
define n where "n ≡ Max {f i | i. i ∈ I'}"
have "⋀i. i ∈ I' ⟹f i ≤ n"
using I' by(auto intro!: Max.coboundedI[of "{f i | i. i ∈ I'}"] simp: n_def)
hence hn2:"⋀i. i ∈ I' ⟹ (1 / r) ^ f i ≤ (1 / r)^n"
using r by auto
have hε' : "0 < ε*(r^n)" using hε r by auto
show ?thesis
proof(safe intro!: exI[where x=x] exI[where x="ε*(r^n)"])
fix y
assume "y ∈ Product_metric.mball x (ε * r ^ n)"
have "y i ∈ X i" if "i ∈ I'" for i
proof -
interpret mi: Metric_space "Mi i" "di i"
using Md_metric that by(simp add: I'_def)
have "di i (x i) (y i) < εi' i"
proof -
have "di i (x i) (y i) ≤ (1 / r) ^ f i * product_dist x y"
using that ‹y ∈ Product_metric.mball x (ε * r ^ n)› by(auto intro!: product_dist_geq[of i,OF _ gf_comp_id x_intop] simp: I'_def)
also have "... ≤ (1 / r)^n * product_dist x y"
by(rule mult_right_mono[OF hn2[OF that] Product_metric.nonneg])
also have "... < ε"
using ‹y ∈ Product_metric.mball x (ε * r ^ n)› r
by (simp add: pos_divide_less_eq power_one_over)
also have "... ≤ εi' i"
by(rule εmin[OF that])
finally show ?thesis .
qed
hence "(y i) ∈ mi.mball (x i) (εi' i)"
using ‹y ∈ Product_metric.mball x (ε * r ^ n)› x_intop that
by(auto simp: I'_def)
thus ?thesis
using hei[OF that] by auto
qed
moreover have "y i ∈ X i" if "i ∈ I - I'" for i
using that htopspace ‹y ∈ Product_metric.mball x (ε * r ^ n)›
by(auto simp: I'_def)
ultimately show "y ∈ U"
using ‹y ∈ Product_metric.mball x (ε * r ^ n)›
by(auto simp: hX(1))
qed(use x_intop hε' in auto)
qed
qed
then obtain a where "∀x∈U. ∃ε. x ∈ Product_metric.mball (a x) ε ∧ Product_metric.mball (a x) ε ⊆ U"
by metis
then obtain ε where hae: "⋀x. x ∈ U ⟹ x ∈ Product_metric.mball (a x) (ε x)" "⋀x. x ∈ U ⟹ Product_metric.mball (a x) (ε x) ⊆ U"
by metis
hence hae': "⋀x. x ∈ U ⟹ a x ∈ (Π⇩E i∈I. Mi i)" "⋀x. x ∈ U ⟹ 0 < ε x"
by auto[1] (metis Product_metric.mball_eq_empty empty_iff hae(1) linorder_not_less)
have "openin (topology_generated_by {Product_metric.mball a ε |a ε. a ∈ (Π⇩E i∈I. Mi i) ∧ 0 < ε}) (⋃ { Product_metric.mball (a x) (ε x) |x. x ∈ U})"
using Product_metric.openin_mball ‹Product_metric.mtopology = topology_generated_by {Product_metric.mball a ε |a ε. a ∈ Pi⇩E I Mi ∧ 0 < ε}› by auto
moreover have "U = (⋃ {Product_metric.mball (a x) (ε x) |x. x ∈ U})"
using hae by (auto simp del: Product_metric.in_mball)
ultimately show "openin (topology_generated_by {Product_metric.mball a ε |a ε. a ∈ (Π⇩E i∈I. Mi i) ∧ 0 < ε}) U"
by simp
qed
qed
qed
corollary separable_Mi_separable_M:
assumes "⋀i. i ∈ I ⟹ separable_space (Metric_space.mtopology (Mi i) (di i))"
shows "separable_space Product_metric.mtopology"
by(simp add: Product_metric_mtopology_eq[symmetric] separable_countable_product assms I)
lemma mcomplete_Mi_mcomplete_M:
assumes "⋀i. i ∈ I ⟹ Metric_space.mcomplete (Mi i) (di i)"
shows Product_metric.mcomplete
proof(cases "I = {}")
case 1:True
interpret d: discrete_metric "{λx. undefined}" .
have 2:"product_dist = (λx y. 0)"
by standard+ (auto simp: product_dist_def 1)
show ?thesis
apply(simp add: Product_metric.mcomplete_def Product_metric.limitin_metric eventually_sequentially Product_metric.MCauchy_def)
apply(simp add: 2)
by(auto simp: 1 intro!: exI[where x="(λi. undefined)"])
next
assume 2: "I ≠ {}"
show ?thesis
unfolding Product_metric.mcomplete_def
proof safe
fix xn
assume h: "Product_metric.MCauchy xn"
have *:"Metric_space.MCauchy (Mi i) (di i) (λn. xn n i)" if hi:"i ∈ I" for i
proof -
interpret mi: Metric_space "Mi i" "di i"
by(simp add: Md_metric hi)
show "mi.MCauchy (λn. xn n i)"
unfolding mi.MCauchy_def
proof safe
show "xn n i ∈ Mi i" for n
using h hi by(auto simp: Product_metric.MCauchy_def)
next
fix ε
assume he:"(0::real) < ε"
then have "0 < ε * r^(f i)" using r by auto
then obtain N where N:
"⋀n m. n≥N ⟹ m≥N ⟹ product_dist (xn n) (xn m) < ε * r^(f i)"
using h Product_metric.MCauchy_def by fastforce
show "∃N. ∀n n'. N ≤ n ⟶ N ≤ n' ⟶ di i (xn n i) (xn n' i) < ε"
proof(safe intro!: exI[where x=N])
fix n m
assume n:"n ≥ N" "m ≥ N"
have "di i (xn n i) (xn m i) ≤ (1 / r) ^ (f i) * product_dist (xn n) (xn m)"
by(rule product_dist_geq) (use h[simplified Product_metric.MCauchy_def] hi gf_comp_id[of i] in auto)
also have "... < ε"
using N[OF n] by (simp add: mult_imp_div_pos_less power_one_over r(1))
finally show "di i (xn n i) (xn m i) < ε" .
qed
qed
qed
hence "∀i∈I. ∃x. limitin (Metric_space.mtopology (Mi i) (di i)) (λn. xn n i) x sequentially"
using Md_metric Metric_space.mcomplete_alt assms by blast
then obtain x where hx:"⋀i. i ∈ I ⟹ limitin (Metric_space.mtopology (Mi i) (di i)) (λn. xn n i) (x i) sequentially"
by metis
hence hx':"(λi∈I. x i) ∈ (Π⇩E i∈I. Mi i)"
by (simp add: Md_metric Metric_space.limit_metric_sequentially)
thus "∃x. limitin Product_metric.mtopology xn x sequentially"
using h by(auto intro!: exI[where x="λi∈I. x i"] limitin_M_iff_limitin_Mi[THEN iffD2,of xn] simp: Product_metric.MCauchy_def hx) blast
qed
qed
end
lemma product_metricI:
assumes "0 < r" "r < 1" "countable I" "⋀i. i ∈ I ⟹ Metric_space (Mi i) (di i)"
and "⋀i x y. 0 ≤ di i x y" "⋀i x y. di i x y ≤ K" "0 < K"
shows "Product_metric r I (to_nat_on I) (from_nat_into I) Mi di K"
using from_nat_into_to_nat_on_product_metric_pair[OF assms(3)] assms
by(simp add: Product_metric_def Metric_space_def)
lemma product_metric_natI:
assumes "0 < r" "r < 1" "⋀n. Metric_space (Mi n) (di n)"
and "⋀i x y. 0 ≤ di i x y" "⋀i x y. di i x y ≤ K" "0 < K"
shows "Product_metric r UNIV id id Mi di K"
using assms by(auto simp: Product_metric_def)
end