Theory Standard_Borel_Spaces.Set_Based_Metric_Product

(*  Title:   Set_Based_Metric_Product.thy
    Author:  Michikazu Hirata, Tokyo Institute of Technology
*)

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 iI. Mi i)  y  (ΠE iI. 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 iI. 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 iI. Mi i)" "y  (ΠE iI. 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 iI. Mi i)" "y  (ΠE iI. Mi i)" "z  (ΠE iI. 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 iI. 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 iI. Mi i)  y  (ΠE iI. Mi i)" | "¬ (x  (ΠE iI. Mi i)  y  (ΠE iI. 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 iI. Mi i)" "y  (ΠE iI. 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. nN. (iI.  xn n i  Mi i)  (i. iI  xn n i = undefined))  (iI. limitin (Metric_space.mtopology (Mi i) (di i)) (λn. xn n i) (x i) sequentially)  x  (ΠE iI. Mi i)"
proof safe
  fix i
  assume h:"limitin Product_metric.mtopology xn x sequentially"
  then show "N. nN. (iI.  xn n i  Mi i)  (i. iI  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. nN. 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': "nN'. (iI. xn n i  Mi i)  (i. i  I  xn n i = undefined)"
  assume h:"iI. limitin (Metric_space.mtopology (Mi i) (di i)) (λn. xn n i) (x i) sequentially" "x  (ΠE iI. 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. nN. xn n  (ΠE iI. 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 "iI. N. nN. 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 iI. topspace (Metric_space.mtopology (Mi i) (di i))) = (ΠE iI. 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 iI. Mi i)  0 < ε}"
      then obtain a ε where hu:
        "U = Product_metric.mball a ε" "a  (ΠE iI. Mi i)" "0 < ε" by auto
      have "X. x  (ΠE iI. X i)  (ΠE iI. 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 iI. X i)  (ΠE iI. 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 iI. X i)"
              using hu that htopspace by(auto simp: X_def)
          next
            show "(ΠE iI. X i)  U"
            proof
              fix y
              assume "y  (ΠE iI. 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 iI. Mi i)"
                using htopspace' y  (ΠE iI. 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  PiE 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 iI. 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 iI. 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 iI. 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 iI. 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 iI. 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 iI. 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 iI. Mi i)"
            unfolding hu(1) using order.strict_trans1[OF product_dist_leqr,of ε] hu(2)
            by auto
          also have "... = (ΠE iI. topspace (Metric_space.mtopology (Mi i) (di i)))"
            using htopspace by auto
          finally have "U = (ΠE iI. 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. xU. x  (ΠE iI. X x i)  (ΠE iI. 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 "xU. x  (ΠE iI. X x i)  (ΠE iI. 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 iI. X x i)" "x. x  U  (ΠE iI. 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 iI. X x i)  {ΠE iI. 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 iI. X x i) | x. x  U})"
        using hX(1,2) by blast
      have "openin (topology_generated_by {ΠE iI. 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 iI. 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 iI. 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 iI. X x i) | x. x  U}) by simp
    next
      fix U
      assume "U  {ΠE iI. 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 iI. 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 iI. 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 iI. 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 : "ε > 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  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 "xU. ε. 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 iI. 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 iI. 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  PiE 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 iI. 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. nN  mN  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 "iI. 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':"(λiI. x i)  (ΠE iI. 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="λiI. x i"] limitin_M_iff_limitin_Mi[THEN iffD2,of xn] simp: Product_metric.MCauchy_def hx) blast
  qed
qed

end (* Product_metric *)

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