Theory More_Infinite_Products

subsection ‹Additional facts about infinite products›
theory More_Infinite_Products
  imports "HOL-Analysis.Analysis"
begin

(* These three facts about actually about products, but we do need them *)
lemma uniform_limit_singleton: "uniform_limit {x} f g F ⟷ ((λn. f n x) ⤏ g x) F"
  by (simp add: uniform_limit_iff tendsto_iff)

lemma uniformly_convergent_on_singleton:
  "uniformly_convergent_on {x} f ⟷ convergent (λn. f n x)"
  by (auto simp: uniformly_convergent_on_def uniform_limit_singleton convergent_def)

lemma uniformly_convergent_on_subset:
  assumes "uniformly_convergent_on A f" "B ⊆ A"
  shows   "uniformly_convergent_on B f"
  using assms by (meson uniform_limit_on_subset uniformly_convergent_on_def)



(* very general theorems about infinite products *)
lemma raw_has_prod_imp_nonzero:
  assumes "raw_has_prod f N P" "n ≥ N"
  shows   "f n ≠ 0"
proof
  assume "f n = 0"
  from assms(1) have lim: "(λm. (∏k≤m. f (k + N))) ⇢ P" and "P ≠ 0"
    unfolding raw_has_prod_def by blast+
  have "eventually (λm. m ≥ n - N) at_top"
    by (rule eventually_ge_at_top)
  hence "eventually (λm. (∏k≤m. f (k + N)) = 0) at_top"
  proof eventually_elim
    case (elim m)
    have "f ((n - N) + N) = 0" "n - N ∈ {..m}" "finite {..m}"
      using ‹n ≥ N› ‹f n = 0› elim by auto
    thus "(∏k≤m. f (k + N)) = 0"
      using prod_zero[of "{..m}" "λk. f (k + N)"] by blast
  qed
  with lim have "P = 0"
    by (simp add: LIMSEQ_const_iff tendsto_cong)
  thus False
    using ‹P ≠ 0› by contradiction
qed

lemma has_prod_imp_tendsto:
  fixes f :: "nat ⇒ 'a :: {semidom, t2_space}"
  assumes "f has_prod P"
  shows   "(λn. ∏k≤n. f k) ⇢ P"
proof (cases "P = 0")
  case False
  with assms show ?thesis
    by (auto simp: has_prod_def raw_has_prod_def)
next
  case True
  with assms obtain N P' where "f N = 0" "raw_has_prod f (Suc N) P'"
    by (auto simp: has_prod_def)
  thus ?thesis
    using LIMSEQ_prod_0 True ‹f N = 0› by blast
qed

lemma has_prod_imp_tendsto':
  fixes f :: "nat ⇒ 'a :: {semidom, t2_space}"
  assumes "f has_prod P"
  shows   "(λn. ∏k<n. f k) ⇢ P"
  using has_prod_imp_tendsto[OF assms] LIMSEQ_lessThan_iff_atMost by blast

lemma convergent_prod_tendsto_imp_has_prod:
  fixes f :: "nat ⇒ 'a :: real_normed_field"
  assumes "convergent_prod f" "(λn. (∏i≤n. f i)) ⇢ P"
  shows   "f has_prod P"
  using assms by (metis convergent_prod_imp_has_prod has_prod_imp_tendsto limI)

(*
  grouping factors into chunks of the same size

  Only one direction; other direction requires "real_normed_field" (see below).
  Not sure if real_normed_field is really necessary, but I don't see how else to do it.
*)
lemma has_prod_group_nonzero: 
  fixes f :: "nat ⇒ 'a :: {semidom, t2_space}"
  assumes "f has_prod P" "k > 0" "P ≠ 0"
  shows   "(λn. (∏i∈{n*k..<n*k+k}. f i)) has_prod P"
proof -
  have "(λn. ∏k<n. f k) ⇢ P"
    using assms(1) by (intro has_prod_imp_tendsto')
  hence "(λn. ∏k<n*k. f k) ⇢ P"
    by (rule filterlim_compose) (use ‹k > 0› in real_asymp)
  also have "(λn. ∏k<n*k. f k) = (λn. ∏m<n. prod f {m*k..<m*k+k})"
    by (subst prod.nat_group [symmetric]) auto
  finally have "(λn. ∏m≤n. prod f {m*k..<m*k+k}) ⇢ P"
    by (subst (asm) LIMSEQ_lessThan_iff_atMost)
  hence "raw_has_prod (λn. prod f {n*k..<n*k+k}) 0 P"
    using ‹P ≠ 0› by (auto simp: raw_has_prod_def)
  thus ?thesis
    by (auto simp: has_prod_def)
qed

lemma has_prod_group:
  fixes f :: "nat ⇒ 'a :: real_normed_field"
  assumes "f has_prod P" "k > 0"
  shows   "(λn. (∏i∈{n*k..<n*k+k}. f i)) has_prod P"
proof (rule convergent_prod_tendsto_imp_has_prod)
  have "(λn. ∏k<n. f k) ⇢ P"
    using assms(1) by (intro has_prod_imp_tendsto')
  hence "(λn. ∏k<n*k. f k) ⇢ P"
    by (rule filterlim_compose) (use ‹k > 0› in real_asymp)
  also have "(λn. ∏k<n*k. f k) = (λn. ∏m<n. prod f {m*k..<m*k+k})"
    by (subst prod.nat_group [symmetric]) auto
  finally show "(λn. ∏m≤n. prod f {m*k..<m*k+k}) ⇢ P"
    by (subst (asm) LIMSEQ_lessThan_iff_atMost)
next
  from assms obtain N P' where prod1: "raw_has_prod f N P'"
    by (auto simp: has_prod_def)
  define N' where "N' = nat ⌈real N / real k⌉"
  have "k * N' ≥ N"
  proof -
    have "(real N / real k * real k) ≤ real (N' * k)"
      unfolding N'_def of_nat_mult by (intro mult_right_mono) (use ‹k > 0› in auto)
    also have "real N / real k * real k = real N"
      using ‹k > 0› by simp
    finally show ?thesis
      by (simp only: mult.commute of_nat_le_iff)
  qed

  obtain P'' where prod2: "raw_has_prod f (k * N') P''"
    using prod1 ‹k * N' ≥ N› by (rule raw_has_prod_ignore_initial_segment)
  hence "P'' ≠ 0"
    by (auto simp: raw_has_prod_def)
  from prod2 have "raw_has_prod (λn. f (n + k * N')) 0 P''"
    by (simp add: raw_has_prod_def)
  hence "(λn. f (n + k * N')) has_prod P''"
    by (auto simp: has_prod_def)
  hence "(λn. ∏i=n*k..<n*k+k. f (i + k * N')) has_prod P''"
    by (rule has_prod_group_nonzero) fact+
  hence "convergent_prod (λn. ∏i=n*k..<n*k+k. f (i + k * N'))"
    using has_prod_iff by blast
  also have "(λn. ∏i=n*k..<n*k+k. f (i + k * N')) = (λn. ∏i=(n+N')*k..<(n+N')*k+k. f i)"
  proof
    fix n :: nat
    show "(∏i=n*k..<n*k+k. f (i + k * N')) = (∏i=(n+N')*k..<(n+N')*k+k. f i)"
      by (rule prod.reindex_bij_witness[of _ "λn. n - k*N'" "λn. n + k*N'"])
         (auto simp: algebra_simps)
  qed
  also have "convergent_prod … ⟷ convergent_prod (λn. (∏i=n*k..<n*k+k. f i))"
    by (rule convergent_prod_iff_shift)
  finally show "convergent_prod (λn. prod f {n * k..<n * k + k})" .
qed


(* non-negativity, positivity, monotonicity of infinite products (on the reals)
   coud perhaps be generalised to other types; not sure if it's worth it. *)
lemma has_prod_nonneg:
  assumes "f has_prod P" "⋀n. f n ≥ (0::real)"
  shows   "P ≥ 0"
proof (rule tendsto_le)
  show "((λn. ∏i≤n. f i)) ⇢ P"
    using assms(1) by (rule has_prod_imp_tendsto)
  show "(λn. 0::real) ⇢ 0"
    by auto
qed (use assms in ‹auto intro!: always_eventually prod_nonneg›)

lemma has_prod_pos:
  assumes "f has_prod P" "⋀n. f n > (0::real)"
  shows   "P > 0"
proof -
  have "P ≥ 0"
    by (rule has_prod_nonneg[OF assms(1)]) (auto intro!: less_imp_le assms(2))
  moreover have "f n ≠ 0" for n
    using assms(2)[of n] by auto
  hence "P ≠ 0"
    using has_prod_0_iff[of f] assms by auto
  ultimately show ?thesis
    by linarith
qed

lemma prod_ge_prodinf: 
  fixes f :: "nat ⇒ 'a::{linordered_idom,linorder_topology}"
  assumes "f has_prod a" "⋀i. 0 ≤ f i" "⋀i. i ≥ n ⟹ f i ≤ 1"
  shows "prod f {..<n} ≥ prodinf f"
proof (rule has_prod_le; (intro conjI)?)
  show "f has_prod prodinf f"
    using assms(1) has_prod_unique by blast
  show "(λr. if r ∈ {..<n} then f r else 1) has_prod prod f {..<n}"
    by (rule has_prod_If_finite_set) auto
next
  fix i 
  show "f i ≥ 0"
    by (rule assms)
  show "f i ≤ (if i ∈ {..<n} then f i else 1)"
    using assms(3)[of i] by auto
qed

lemma has_prod_less:
  fixes F G :: real
  assumes less: "f m < g m"
  assumes f: "f has_prod F" and g: "g has_prod G"
  assumes pos: "⋀n. 0 < f n" and le: "⋀n. f n ≤ g n"
  shows   "F < G"
proof -
  define F' G' where "F' = (∏n<Suc m. f n)" and "G' = (∏n<Suc m. g n)"
  have [simp]: "f n ≠ 0" "g n ≠ 0" for n
    using pos[of n] le[of n] by auto
  have [simp]: "F' ≠ 0" "G' ≠ 0"
    by (auto simp: F'_def G'_def)
  have f': "(λn. f (n + Suc m)) has_prod (F / F')"
    unfolding F'_def using f
    by (intro has_prod_split_initial_segment) auto
  have g': "(λn. g (n + Suc m)) has_prod (G / G')"
    unfolding G'_def using g
    by (intro has_prod_split_initial_segment) auto
  have "F' * (F / F') < G' * (F / F')"
  proof (rule mult_strict_right_mono)
    show "F' < G'"
      unfolding F'_def G'_def
      by (rule prod_mono_strict[of m])
         (auto intro: le less_imp_le[OF pos] less_le_trans[OF pos le] less)
    show "F / F' > 0"
      using f' by (rule has_prod_pos) (use pos in auto)
  qed
  also have "… ≤ G' * (G / G')"
  proof (rule mult_left_mono)
    show "F / F' ≤ G / G'"
      using f' g' by (rule has_prod_le) (auto intro: less_imp_le[OF pos] le)
    show "G' ≥ 0"
      unfolding G'_def by (intro prod_nonneg order.trans[OF less_imp_le[OF pos] le])
  qed
  finally show ?thesis
    by simp
qed




(* convergence criteria; especially uniform convergence of infinite products *)

text ‹
  Cauchy's criterion for the convergence of infinite products, adapted to proving
  uniform convergence: let $f_k(x)$ be a sequence of functions such that

    ▸ $f_k(x)$ has uniformly bounded partial products, i.e.\ there exists a constant ‹C›
      such that $\prod_{k=0}^m f_k(x) \leq C$ for all $m$ and $x\in A$.

    ▸ For any $\varepsilon > 0$ there exists a number $M \in \mathbb{N}$ such that, for any
      $m, n \geq M$ and all $x\in A$ we have $|(\prod_{k=m}^n f_k(x)) - 1| < \varepsilon$

  Then $\prod_{k=0}^n f_k(x)$ converges to $\prod_{k=0}^\infty f_k(x)$ uniformly for all
  $x \in A$.
›
lemma uniformly_convergent_prod_Cauchy:
  fixes f :: "nat ⇒ 'a :: topological_space ⇒ 'b :: {real_normed_div_algebra, comm_ring_1, banach}"
  assumes C: "⋀x m. x ∈ A ⟹ norm (∏k<m. f k x) ≤ C"
  assumes "⋀e. e > 0 ⟹ ∃M. ∀x∈A. ∀m≥M. ∀n≥m. dist (∏k=m..n. f k x) 1 < e"
  shows   "uniformly_convergent_on A (λN x. ∏n<N. f n x)"
proof (rule Cauchy_uniformly_convergent, rule uniformly_Cauchy_onI')
  fix ε :: real assume ε: "ε > 0"
  define C' where "C' = max C 1"
  have C': "C' > 0"
    by (auto simp: C'_def)
  define δ where "δ = Min {2 / 3 * ε / C', 1 / 2}"
  from ε have "δ > 0"
    using ‹C' > 0› by (auto simp: δ_def)
  obtain M where M: "⋀x m n. x ∈ A ⟹ m ≥ M ⟹ n ≥ m ⟹ dist (∏k=m..n. f k x) 1 < δ"
    using ‹δ > 0› assms by fast

  show "∃M. ∀x∈A. ∀m≥M. ∀n>m. dist (∏k<m. f k x) (∏k<n. f k x) < ε"
  proof (rule exI, intro ballI allI impI)
    fix x m n
    assume x: "x ∈ A" and mn: "M + 1 ≤ m" "m < n"
    show "dist (∏k<m. f k x) (∏k<n. f k x) < ε"
    proof (cases "∃k<m. f k x = 0")
      case True
      hence "(∏k<m. f k x) = 0" and "(∏k<n. f k x) = 0"
        using mn x by (auto intro!: prod_zero)
      thus ?thesis
        using ε by simp
    next
      case False
      have *: "{..<n} = {..<m} ∪ {m..n-1}"
        using mn by auto
      have "dist (∏k<m. f k x) (∏k<n. f k x) = norm ((∏k<m. f k x) * ((∏k=m..n-1. f k x) - 1))"
        unfolding * by (subst prod.union_disjoint)
                       (use mn in ‹auto simp: dist_norm algebra_simps norm_minus_commute›)
      also have "… = (∏k<m. norm (f k x)) * dist (∏k=m..n-1. f k x) 1"
        by (simp add: norm_mult dist_norm prod_norm)
      also have "… < (∏k<m. norm (f k x)) * (2 / 3 * ε / C')"
      proof (rule mult_strict_left_mono)
        show "dist (∏k = m..n - 1. f k x) 1 < 2 / 3 * ε / C'"
          using M[of x m "n-1"] x mn unfolding δ_def by fastforce
      qed (use False in ‹auto intro!: prod_pos›)
      also have "(∏k<m. norm (f k x)) = (∏k<M. norm (f k x)) * norm (∏k=M..<m. (f k x))"
      proof -
        have *: "{..<m} = {..<M} ∪ {M..<m}"
          using mn by auto
        show ?thesis
          unfolding * using mn by (subst prod.union_disjoint) (auto simp: prod_norm)
      qed
      also have "norm (∏k=M..<m. (f k x)) ≤ 3 / 2"
      proof -
        have "dist (∏k=M..m-1. f k x) 1 < δ"
          using M[of x M "m-1"] x mn ‹δ > 0› by auto
        also have "… ≤ 1 / 2"
          by (simp add: δ_def)
        also have "{M..m-1} = {M..<m}"
          using mn by auto
        finally have "norm (∏k=M..<m. f k x) ≤ norm (1 :: 'b) + 1 / 2"
          by norm
        thus ?thesis
          by simp
      qed
      hence "(∏k<M. norm (f k x)) * norm (∏k = M..<m. f k x) * (2 / 3 * ε / C') ≤
             (∏k<M. norm (f k x)) * (3 / 2) * (2 / 3 * ε / C')"
        using ε C' by (intro mult_left_mono mult_right_mono prod_nonneg) auto
      also have "… ≤ C' * (3 / 2) * (2 / 3 * ε / C')"
      proof (intro mult_right_mono)
        have "(∏k<M. norm (f k x)) ≤ C"
          using C[of x M] x by (simp add: prod_norm)
        also have "… ≤ C'"
          by (simp add: C'_def)
        finally show "(∏k<M. norm (f k x)) ≤ C'" .
      qed (use ε C' in auto)
      finally show "dist (∏k<m. f k x) (∏k<n. f k x) < ε"
        using ‹C' > 0› by (simp add: field_simps)
    qed
  qed
qed

text ‹
  By instantiating the set $A$ in this result with a singleton set, we obtain the ``normal''
  Cauchy criterion for infinite products:
›
lemma convergent_prod_Cauchy_sufficient:
  fixes f :: "nat ⇒ 'b :: {real_normed_div_algebra, comm_ring_1, banach}"
  assumes "⋀e. e > 0 ⟹ ∃M. ∀m n. M ≤ m ⟶ m ≤ n ⟶ dist (∏k=m..n. f k) 1 < e"
  shows   "convergent_prod f"
proof -
  obtain M where M: "⋀m n. m ≥ M ⟹ n ≥ m ⟹ dist (prod f {m..n}) 1 < 1 / 2"
    using assms(1)[of "1 / 2"] by auto
  have nz: "f m ≠ 0" if "m ≥ M" for m
    using M[of m m] that by auto

  have M': "dist (prod (λk. f (k + M)) {m..<n}) 1 < 1 / 2" for m n
  proof (cases "m < n")
    case True
    have "dist (prod f {m+M..n-1+M}) 1 < 1 / 2"
      by (rule M) (use True in auto)
    also have "prod f {m+M..n-1+M} = prod (λk. f (k + M)) {m..<n}"
      by (rule prod.reindex_bij_witness[of _ "λk. k + M" "λk. k - M"]) (use True in auto)
    finally show ?thesis .
  qed auto 

  have "uniformly_convergent_on {0::'b} (λN x. ∏n<N. f (n + M))"
  proof (rule uniformly_convergent_prod_Cauchy)
    fix m :: nat
    have "norm (∏k=0..<m. f (k + M)) < norm (1 :: 'b) + 1 / 2"
      using M'[of 0 m] by norm
    thus "norm (∏k<m. f (k + M)) ≤ 3 / 2"
      by (simp add: atLeast0LessThan)
  next
    fix e :: real assume e: "e > 0"
    obtain M' where M': "⋀m n. M' ≤ m ⟶ m ≤ n ⟶ dist (∏k=m..n. f k) 1 < e"
      using assms e by blast
    show "∃M'. ∀x∈{0}. ∀m≥M'. ∀n≥m. dist (∏k=m..n. f (k + M)) 1 < e"
    proof (rule exI[of _ M'], intro ballI impI allI)
      fix m n :: nat assume "M' ≤ m" "m ≤ n"
      thus "dist (∏k=m..n. f (k + M)) 1 < e"
        using M' by (metis add.commute add_left_mono prod.shift_bounds_cl_nat_ivl trans_le_add1)
    qed
  qed
  hence "convergent (λN. ∏n<N. f (n + M))"
    by (rule uniformly_convergent_imp_convergent[of _ _ 0]) auto
  then obtain L where L: "(λN. ∏n<N. f (n + M)) ⇢ L"
    unfolding convergent_def by blast

  show ?thesis
    unfolding convergent_prod_altdef
  proof (rule exI[of _ M], rule exI[of _ L], intro conjI)
    show "∀n≥M. f n ≠ 0"
      using nz by auto
  next
    show "(λn. ∏i≤n. f (i + M)) ⇢ L"
      using LIMSEQ_Suc[OF L] by (subst (asm) lessThan_Suc_atMost)
  next
    have "norm L ≥ 1 / 2"
    proof (rule tendsto_lowerbound)
      show "(λn. norm (∏i<n. f (i + M))) ⇢ norm L"
        by (intro tendsto_intros L)
      show "∀⇩F n in sequentially. 1 / 2 ≤ norm (∏i<n. f (i + M))"
      proof (intro always_eventually allI)
        fix m :: nat
        have "norm (∏k=0..<m. f (k + M)) ≥ norm (1 :: 'b) - 1 / 2"
          using M'[of 0 m] by norm
        thus "norm (∏k<m. f (k + M)) ≥ 1 / 2"
          by (simp add: atLeast0LessThan)
      qed
    qed auto
    thus "L ≠ 0"
      by auto
  qed
qed


text ‹
  We now prove that the Cauchy criterion for pointwise convergence is both necessary
  and sufficient.
›
lemma convergent_prod_Cauchy_necessary:
  fixes f :: "nat ⇒ 'b :: {real_normed_field, banach}"
  assumes "convergent_prod f" "e > 0"
  shows   "∃M. ∀m n. M ≤ m ⟶ m ≤ n ⟶ dist (∏k=m..n. f k) 1 < e"
proof -
  have *: "∃M. ∀m n. M ≤ m ⟶ m ≤ n ⟶ dist (∏k=m..n. f k) 1 < e"
    if f: "convergent_prod f" "0 ∉ range f" and e: "e > 0"
    for f :: "nat ⇒ 'b" and e :: real
  proof -
    have *: "(λn. norm (∏k<n. f k)) ⇢ norm (∏k. f k)"
      using has_prod_imp_tendsto' f(1) by (intro tendsto_norm) blast
    from f(1,2) have [simp]: "(∏k. f k) ≠ 0"
      using prodinf_nonzero by fastforce
    obtain M' where M': "norm (∏k<m. f k) > norm (∏k. f k) / 2" if "m ≥ M'" for m
      using order_tendstoD(1)[OF *, of "norm (∏k. f k) / 2"]
      by (auto simp: eventually_at_top_linorder)
    define M where "M = Min (insert (norm (∏k. f k) / 2) ((λm. norm (∏k<m. f k)) ` {..<M'}))"
    have "M > 0"
      unfolding M_def using f(2) by (subst Min_gr_iff) auto
    have norm_ge: "norm (∏k<m. f k) ≥ M" for m
    proof (cases "m ≥ M'")
      case True
      have "M ≤ norm (∏k. f k) / 2"
        unfolding M_def by (intro Min.coboundedI) auto
      also from True have "norm (∏k<m. f k) > norm (∏k. f k) / 2"
        by (intro M')
      finally show ?thesis by linarith
    next
      case False
      thus ?thesis
        unfolding M_def
        by (intro Min.coboundedI) auto
    qed

    have "convergent (λn. ∏k<n. f k)"
      using f(1) convergent_def has_prod_imp_tendsto' by blast
    hence "Cauchy (λn. ∏k<n. f k)"
      by (rule convergent_Cauchy)
    moreover have "e * M > 0"
      using e ‹M > 0› by auto
    ultimately obtain N where N: "dist (∏k<m. f k) (∏k<n. f k) < e * M" if "m ≥ N" "n ≥ N" for m n
      unfolding Cauchy_def by fast

    show "∃M. ∀m n. M ≤ m ⟶ m ≤ n ⟶ dist (prod f {m..n}) 1 < e"
    proof (rule exI[of _ N], intro allI impI, goal_cases)
      case (1 m n)
      have "dist (∏k<m. f k) (∏k<Suc n. f k) < e * M"
        by (rule N) (use 1 in auto)
      also have "dist (∏k<m. f k) (∏k<Suc n. f k) = norm ((∏k<Suc n. f k) - (∏k<m. f k))"
        by (simp add: dist_norm norm_minus_commute)
      also have "(∏k<Suc n. f k) = (∏k∈{..<m}∪{m..n}. f k)"
        using 1 by (intro prod.cong) auto
      also have "… = (∏k∈{..<m}. f k) * (∏k∈{m..n}. f k)"
        by (subst prod.union_disjoint) auto
      also have "… - (∏k<m. f k) = (∏k<m. f k) * ((∏k∈{m..n}. f k) - 1)"
        by (simp add: algebra_simps)
      finally have "norm (prod f {m..n} - 1) < e * M / norm (prod f {..<m})"
        using f(2) by (auto simp add: norm_mult divide_simps mult_ac)
      also have "… ≤ e * M / M"
        using e ‹M > 0› f(2) by (intro divide_left_mono norm_ge mult_pos_pos) auto
      also have "… = e"
        using ‹M > 0› by simp
      finally show ?case
        by (simp add: dist_norm)
    qed
  qed

  obtain M where M: "f m ≠ 0" if "m ≥ M" for m
    using convergent_prod_imp_ev_nonzero[OF assms(1)]
    by (auto simp: eventually_at_top_linorder)

  have "∃M'. ∀m n. M' ≤ m ⟶ m ≤ n ⟶ dist (∏k=m..n. f (k + M)) 1 < e"
    by (rule *) (use assms M in auto)
  then obtain M' where M': "dist (∏k=m..n. f (k + M)) 1 < e" if "M' ≤ m" "m ≤ n" for m n
    by blast

  show "∃M. ∀m n. M ≤ m ⟶ m ≤ n ⟶ dist (prod f {m..n}) 1 < e"
  proof (rule exI[of _ "M + M'"], safe, goal_cases)
    case (1 m n)
    have "dist (∏k=m-M..n-M. f (k + M)) 1 < e"
      by (rule M') (use 1 in auto)
    also have "(∏k=m-M..n-M. f (k + M)) = (∏k=m..n. f k)"
      using 1 by (intro prod.reindex_bij_witness[of _ "λk. k - M" "λk. k + M"]) auto
    finally show ?case .
  qed
qed

lemma convergent_prod_Cauchy_iff:
  fixes f :: "nat ⇒ 'b :: {real_normed_field, banach}"
  shows "convergent_prod f ⟷ (∀e>0. ∃M. ∀m n. M ≤ m ⟶ m ≤ n ⟶ dist (∏k=m..n. f k) 1 < e)"
  using convergent_prod_Cauchy_necessary[of f] convergent_prod_Cauchy_sufficient[of f]
  by blast

(* Note by Manuel: this is already in the library but with an unnecessarily constrained type.
   I generalised the argument from 'b to 'a :: topological_space *)
lemma uniform_limit_suminf:
  fixes f:: "nat ⇒ 'a :: topological_space ⇒ 'b::{metric_space, comm_monoid_add}"
  assumes "uniformly_convergent_on X (λn x. ∑k<n. f k x)" 
  shows "uniform_limit X (λn x. ∑k<n. f k x) (λx. ∑k. f k x) sequentially"
proof -
  obtain S where S: "uniform_limit X (λn x. ∑k<n. f k x) S sequentially"
    using assms uniformly_convergent_on_def by blast
  then have "(∑k. f k x) = S x" if "x ∈ X" for x
    using that sums_iff sums_def by (blast intro: tendsto_uniform_limitI [OF S])
  with S show ?thesis
    by (simp cong: uniform_limit_cong')
qed

lemma uniformly_convergent_on_prod:
  fixes f :: "nat ⇒ 'a :: topological_space ⇒ 'b :: {real_normed_div_algebra, comm_ring_1, banach}"
  assumes cont: "⋀n. continuous_on A (f n)"
  assumes A: "compact A"
  assumes conv_sum: "uniformly_convergent_on A (λN x. ∑n<N. norm (f n x))"
  shows   "uniformly_convergent_on A (λN x. ∏n<N. 1 + f n x)"
proof -
  have lim: "uniform_limit A (λn x. ∑k<n. norm (f k x)) (λx. ∑k. norm (f k x)) sequentially"
    by (rule uniform_limit_suminf) fact
  have cont': "∀⇩F n in sequentially. continuous_on A (λx. ∑k<n. norm (f k x))"
    using cont by (auto intro!: continuous_intros always_eventually cont)
  have "continuous_on A (λx. ∑k. norm (f k x))"
    by (rule uniform_limit_theorem[OF cont' lim]) auto
  hence "compact ((λx. ∑k. norm (f k x)) ` A)"
    by (intro compact_continuous_image A)
  hence "bounded ((λx. ∑k. norm (f k x)) ` A)"
    by (rule compact_imp_bounded)
  then obtain C where C: "norm (∑k. norm (f k x)) ≤ C" if "x ∈ A" for x
    unfolding bounded_iff by blast
  show ?thesis
  proof (rule uniformly_convergent_prod_Cauchy)
    fix x :: 'a and m :: nat
    assume x: "x ∈ A"
    have "norm (∏k<m. 1 + f k x) = (∏k<m. norm (1 + f k x))"
      by (simp add: prod_norm)
    also have "… ≤ (∏k<m. norm (1 :: 'b) + norm (f k x))"
      by (intro prod_mono) norm
    also have "… = (∏k<m. 1 + norm (f k x))"
      by simp
    also have "… ≤ exp (∑k<m. norm (f k x))"
      by (rule prod_le_exp_sum) auto
    also have "(∑k<m. norm (f k x)) ≤ (∑k. norm (f k x))"
    proof (rule sum_le_suminf)
      have "(λn. ∑k<n. norm (f k x)) ⇢ (∑k. norm (f k x))"
        by (rule tendsto_uniform_limitI[OF lim]) fact
      thus "summable (λk. norm (f k x))"
        using sums_def sums_iff by blast
    qed auto
    also have "exp (∑k. norm (f k x)) ≤ exp (norm (∑k. norm (f k x)))"
      by simp
    also have "norm (∑k. norm (f k x)) ≤ C"
      by (rule C) fact
    finally show "norm (∏k<m. 1 + f k x) ≤ exp C"
      by - simp_all
  next
    fix ε :: real assume ε: "ε > 0"
    have "uniformly_Cauchy_on A (λN x. ∑n<N. norm (f n x))"
      by (rule uniformly_convergent_Cauchy) fact
    moreover have "ln (1 + ε) > 0"
      using ε by simp
    ultimately obtain M where M: "⋀m n x. x ∈ A ⟹ M ≤ m ⟹ M ≤ n ⟹
        dist (∑k<m. norm (f k x)) (∑k<n. norm (f k x)) < ln (1 + ε)"
      using ε unfolding uniformly_Cauchy_on_def by metis
  
    show "∃M. ∀x∈A. ∀m≥M. ∀n≥m. dist (∏k = m..n. 1 + f k x) 1 < ε"
    proof (rule exI, intro ballI allI impI)
      fix x m n
      assume x: "x ∈ A" and mn: "M ≤ m" "m ≤ n"
      have "dist (∑k<m. norm (f k x)) (∑k<Suc n. norm (f k x)) < ln (1 + ε)"
        by (rule M) (use x mn in auto)
      also have "dist (∑k<m. norm (f k x)) (∑k<Suc n. norm (f k x)) =
                 ¦∑k∈{..<Suc n}-{..<m}. norm (f k x)¦"
        using mn by (subst sum_diff) (auto simp: dist_norm)
      also have "{..<Suc n}-{..<m} = {m..n}"
        using mn by auto
      also have "¦∑k=m..n. norm (f k x)¦ = (∑k=m..n. norm (f k x))"
        by (intro abs_of_nonneg sum_nonneg) auto
      finally have *: "(∑k=m..n. norm (f k x)) < ln (1 + ε)" .
  
      have "dist (∏k=m..n. 1 + f k x) 1 = norm ((∏k=m..n. 1 + f k x) - 1)"
        by (simp add: dist_norm)
      also have "norm ((∏k=m..n. 1 + f k x) - 1) ≤ (∏n=m..n. 1 + norm (f n x)) - 1"
        by (rule norm_prod_minus1_le_prod_minus1)
      also have "(∏n=m..n. 1 + norm (f n x)) ≤ exp (∑k=m..n. norm (f k x))"
        by (rule prod_le_exp_sum) auto
      also note *
      finally show "dist (∏k = m..n. 1 + f k x) 1 < ε"
        using ε by - simp_all
    qed
  qed
qed

lemma uniformly_convergent_on_prod':
  fixes f :: "nat ⇒ 'a :: topological_space ⇒ 'b :: {real_normed_div_algebra, comm_ring_1, banach}"
  assumes cont: "⋀n. continuous_on A (f n)"
  assumes A: "compact A"
  assumes conv_sum: "uniformly_convergent_on A (λN x. ∑n<N. norm (f n x - 1))"
  shows "uniformly_convergent_on A (λN x. ∏n<N. f n x)"
proof -
  have "uniformly_convergent_on A (λN x. ∏n<N. 1 + (f n x - 1))"
    by (rule uniformly_convergent_on_prod) (use assms in ‹auto intro!: continuous_intros›)
  thus ?thesis
    by simp
qed

end