Theory Infinite_Products

theory Infinite_Products
imports Complex_Main
(*
  File:      HOL/Analysis/Infinite_Product.thy
  Author:    Manuel Eberl

  Basic results about convergence and absolute convergence of infinite products
  and their connection to summability.
*)
section ‹Infinite Products›
theory Infinite_Products
  imports Complex_Main
begin

lemma sum_le_prod:
  fixes f :: "'a ⇒ 'b :: linordered_semidom"
  assumes "⋀x. x ∈ A ⟹ f x ≥ 0"
  shows   "sum f A ≤ (∏x∈A. 1 + f x)"
  using assms
proof (induction A rule: infinite_finite_induct)
  case (insert x A)
  from insert.hyps have "sum f A + f x * (∏x∈A. 1) ≤ (∏x∈A. 1 + f x) + f x * (∏x∈A. 1 + f x)"
    by (intro add_mono insert mult_left_mono prod_mono) (auto intro: insert.prems)
  with insert.hyps show ?case by (simp add: algebra_simps)
qed simp_all

lemma prod_le_exp_sum:
  fixes f :: "'a ⇒ real"
  assumes "⋀x. x ∈ A ⟹ f x ≥ 0"
  shows   "prod (λx. 1 + f x) A ≤ exp (sum f A)"
  using assms
proof (induction A rule: infinite_finite_induct)
  case (insert x A)
  have "(1 + f x) * (∏x∈A. 1 + f x) ≤ exp (f x) * exp (sum f A)"
    using insert.prems by (intro mult_mono insert prod_nonneg exp_ge_add_one_self) auto
  with insert.hyps show ?case by (simp add: algebra_simps exp_add)
qed simp_all

lemma lim_ln_1_plus_x_over_x_at_0: "(λx::real. ln (1 + x) / x) ─0→ 1"
proof (rule lhopital)
  show "(λx::real. ln (1 + x)) ─0→ 0"
    by (rule tendsto_eq_intros refl | simp)+
  have "eventually (λx::real. x ∈ {-1/2<..<1/2}) (nhds 0)"
    by (rule eventually_nhds_in_open) auto
  hence *: "eventually (λx::real. x ∈ {-1/2<..<1/2}) (at 0)"
    by (rule filter_leD [rotated]) (simp_all add: at_within_def)   
  show "eventually (λx::real. ((λx. ln (1 + x)) has_field_derivative inverse (1 + x)) (at x)) (at 0)"
    using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps)
  show "eventually (λx::real. ((λx. x) has_field_derivative 1) (at x)) (at 0)"
    using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps)
  show "∀F x in at 0. x ≠ 0" by (auto simp: at_within_def eventually_inf_principal)
  show "(λx::real. inverse (1 + x) / 1) ─0→ 1"
    by (rule tendsto_eq_intros refl | simp)+
qed auto

definition convergent_prod :: "(nat ⇒ 'a :: {t2_space,comm_semiring_1}) ⇒ bool" where
  "convergent_prod f ⟷ (∃M L. (λn. ∏i≤n. f (i+M)) ⇢ L ∧ L ≠ 0)"

lemma convergent_prod_altdef:
  fixes f :: "nat ⇒ 'a :: {t2_space,comm_semiring_1}"
  shows "convergent_prod f ⟷ (∃M L. (∀n≥M. f n ≠ 0) ∧ (λn. ∏i≤n. f (i+M)) ⇢ L ∧ L ≠ 0)"
proof
  assume "convergent_prod f"
  then obtain M L where *: "(λn. ∏i≤n. f (i+M)) ⇢ L" "L ≠ 0"
    by (auto simp: convergent_prod_def)
  have "f i ≠ 0" if "i ≥ M" for i
  proof
    assume "f i = 0"
    have **: "eventually (λn. (∏i≤n. f (i+M)) = 0) sequentially"
      using eventually_ge_at_top[of "i - M"]
    proof eventually_elim
      case (elim n)
      with ‹f i = 0› and ‹i ≥ M› show ?case
        by (auto intro!: bexI[of _ "i - M"] prod_zero)
    qed
    have "(λn. (∏i≤n. f (i+M))) ⇢ 0"
      unfolding filterlim_iff
      by (auto dest!: eventually_nhds_x_imp_x intro!: eventually_mono[OF **])
    from tendsto_unique[OF _ this *(1)] and *(2)
      show False by simp
  qed
  with * show "(∃M L. (∀n≥M. f n ≠ 0) ∧ (λn. ∏i≤n. f (i+M)) ⇢ L ∧ L ≠ 0)" 
    by blast
qed (auto simp: convergent_prod_def)

definition abs_convergent_prod :: "(nat ⇒ _) ⇒ bool" where
  "abs_convergent_prod f ⟷ convergent_prod (λi. 1 + norm (f i - 1))"

lemma abs_convergent_prodI:
  assumes "convergent (λn. ∏i≤n. 1 + norm (f i - 1))"
  shows   "abs_convergent_prod f"
proof -
  from assms obtain L where L: "(λn. ∏i≤n. 1 + norm (f i - 1)) ⇢ L"
    by (auto simp: convergent_def)
  have "L ≥ 1"
  proof (rule tendsto_le)
    show "eventually (λn. (∏i≤n. 1 + norm (f i - 1)) ≥ 1) sequentially"
    proof (intro always_eventually allI)
      fix n
      have "(∏i≤n. 1 + norm (f i - 1)) ≥ (∏i≤n. 1)"
        by (intro prod_mono) auto
      thus "(∏i≤n. 1 + norm (f i - 1)) ≥ 1" by simp
    qed
  qed (use L in simp_all)
  hence "L ≠ 0" by auto
  with L show ?thesis unfolding abs_convergent_prod_def convergent_prod_def
    by (intro exI[of _ "0::nat"] exI[of _ L]) auto
qed

lemma
  fixes f :: "nat ⇒ 'a :: {real_normed_div_algebra,idom}"
  assumes "convergent_prod f"
  shows   convergent_prod_imp_convergent: "convergent (λn. ∏i≤n. f i)"
    and   convergent_prod_to_zero_iff:    "(λn. ∏i≤n. f i) ⇢ 0 ⟷ (∃i. f i = 0)"
proof -
  from assms obtain M L 
    where M: "⋀n. n ≥ M ⟹ f n ≠ 0" and "(λn. ∏i≤n. f (i + M)) ⇢ L" and "L ≠ 0"
    by (auto simp: convergent_prod_altdef)
  note this(2)
  also have "(λn. ∏i≤n. f (i + M)) = (λn. ∏i=M..M+n. f i)"
    by (intro ext prod.reindex_bij_witness[of _ "λn. n - M" "λn. n + M"]) auto
  finally have "(λn. (∏i<M. f i) * (∏i=M..M+n. f i)) ⇢ (∏i<M. f i) * L"
    by (intro tendsto_mult tendsto_const)
  also have "(λn. (∏i<M. f i) * (∏i=M..M+n. f i)) = (λn. (∏i∈{..<M}∪{M..M+n}. f i))"
    by (subst prod.union_disjoint) auto
  also have "(λn. {..<M} ∪ {M..M+n}) = (λn. {..n+M})" by auto
  finally have lim: "(λn. prod f {..n}) ⇢ prod f {..<M} * L" 
    by (rule LIMSEQ_offset)
  thus "convergent (λn. ∏i≤n. f i)"
    by (auto simp: convergent_def)

  show "(λn. ∏i≤n. f i) ⇢ 0 ⟷ (∃i. f i = 0)"
  proof
    assume "∃i. f i = 0"
    then obtain i where "f i = 0" by auto
    moreover with M have "i < M" by (cases "i < M") auto
    ultimately have "(∏i<M. f i) = 0" by auto
    with lim show "(λn. ∏i≤n. f i) ⇢ 0" by simp
  next
    assume "(λn. ∏i≤n. f i) ⇢ 0"
    from tendsto_unique[OF _ this lim] and ‹L ≠ 0›
    show "∃i. f i = 0" by auto
  qed
qed

lemma abs_convergent_prod_altdef:
  "abs_convergent_prod f ⟷ convergent (λn. ∏i≤n. 1 + norm (f i - 1))"
proof
  assume "abs_convergent_prod f"
  thus "convergent (λn. ∏i≤n. 1 + norm (f i - 1))"
    by (auto simp: abs_convergent_prod_def intro!: convergent_prod_imp_convergent)
qed (auto intro: abs_convergent_prodI)

lemma weierstrass_prod_ineq:
  fixes f :: "'a ⇒ real" 
  assumes "⋀x. x ∈ A ⟹ f x ∈ {0..1}"
  shows   "1 - sum f A ≤ (∏x∈A. 1 - f x)"
  using assms
proof (induction A rule: infinite_finite_induct)
  case (insert x A)
  from insert.hyps and insert.prems 
    have "1 - sum f A + f x * (∏x∈A. 1 - f x) ≤ (∏x∈A. 1 - f x) + f x * (∏x∈A. 1)"
    by (intro insert.IH add_mono mult_left_mono prod_mono) auto
  with insert.hyps show ?case by (simp add: algebra_simps)
qed simp_all

lemma norm_prod_minus1_le_prod_minus1:
  fixes f :: "nat ⇒ 'a :: {real_normed_div_algebra,comm_ring_1}"  
  shows "norm (prod (λn. 1 + f n) A - 1) ≤ prod (λn. 1 + norm (f n)) A - 1"
proof (induction A rule: infinite_finite_induct)
  case (insert x A)
  from insert.hyps have 
    "norm ((∏n∈insert x A. 1 + f n) - 1) = 
       norm ((∏n∈A. 1 + f n) - 1 + f x * (∏n∈A. 1 + f n))"
    by (simp add: algebra_simps)
  also have "… ≤ norm ((∏n∈A. 1 + f n) - 1) + norm (f x * (∏n∈A. 1 + f n))"
    by (rule norm_triangle_ineq)
  also have "norm (f x * (∏n∈A. 1 + f n)) = norm (f x) * (∏x∈A. norm (1 + f x))"
    by (simp add: prod_norm norm_mult)
  also have "(∏x∈A. norm (1 + f x)) ≤ (∏x∈A. norm (1::'a) + norm (f x))"
    by (intro prod_mono norm_triangle_ineq ballI conjI) auto
  also have "norm (1::'a) = 1" by simp
  also note insert.IH
  also have "(∏n∈A. 1 + norm (f n)) - 1 + norm (f x) * (∏x∈A. 1 + norm (f x)) =
               (∏n∈insert x A. 1 + norm (f n)) - 1"
    using insert.hyps by (simp add: algebra_simps)
  finally show ?case by - (simp_all add: mult_left_mono)
qed simp_all

lemma convergent_prod_imp_ev_nonzero:
  fixes f :: "nat ⇒ 'a :: {t2_space,comm_semiring_1}"
  assumes "convergent_prod f"
  shows   "eventually (λn. f n ≠ 0) sequentially"
  using assms by (auto simp: eventually_at_top_linorder convergent_prod_altdef)

lemma convergent_prod_imp_LIMSEQ:
  fixes f :: "nat ⇒ 'a :: {real_normed_field}"
  assumes "convergent_prod f"
  shows   "f ⇢ 1"
proof -
  from assms obtain M L where L: "(λn. ∏i≤n. f (i+M)) ⇢ L" "⋀n. n ≥ M ⟹ f n ≠ 0" "L ≠ 0"
    by (auto simp: convergent_prod_altdef)
  hence L': "(λn. ∏i≤Suc n. f (i+M)) ⇢ L" by (subst filterlim_sequentially_Suc)
  have "(λn. (∏i≤Suc n. f (i+M)) / (∏i≤n. f (i+M))) ⇢ L / L"
    using L L' by (intro tendsto_divide) simp_all
  also from L have "L / L = 1" by simp
  also have "(λn. (∏i≤Suc n. f (i+M)) / (∏i≤n. f (i+M))) = (λn. f (n + Suc M))"
    using assms L by (auto simp: fun_eq_iff atMost_Suc)
  finally show ?thesis by (rule LIMSEQ_offset)
qed

lemma abs_convergent_prod_imp_summable:
  fixes f :: "nat ⇒ 'a :: real_normed_div_algebra"
  assumes "abs_convergent_prod f"
  shows "summable (λi. norm (f i - 1))"
proof -
  from assms have "convergent (λn. ∏i≤n. 1 + norm (f i - 1))" 
    unfolding abs_convergent_prod_def by (rule convergent_prod_imp_convergent)
  then obtain L where L: "(λn. ∏i≤n. 1 + norm (f i - 1)) ⇢ L"
    unfolding convergent_def by blast
  have "convergent (λn. ∑i≤n. norm (f i - 1))"
  proof (rule Bseq_monoseq_convergent)
    have "eventually (λn. (∏i≤n. 1 + norm (f i - 1)) < L + 1) sequentially"
      using L(1) by (rule order_tendstoD) simp_all
    hence "∀F x in sequentially. norm (∑i≤x. norm (f i - 1)) ≤ L + 1"
    proof eventually_elim
      case (elim n)
      have "norm (∑i≤n. norm (f i - 1)) = (∑i≤n. norm (f i - 1))"
        unfolding real_norm_def by (intro abs_of_nonneg sum_nonneg) simp_all
      also have "… ≤ (∏i≤n. 1 + norm (f i - 1))" by (rule sum_le_prod) auto
      also have "… < L + 1" by (rule elim)
      finally show ?case by simp
    qed
    thus "Bseq (λn. ∑i≤n. norm (f i - 1))" by (rule BfunI)
  next
    show "monoseq (λn. ∑i≤n. norm (f i - 1))"
      by (rule mono_SucI1) auto
  qed
  thus "summable (λi. norm (f i - 1))" by (simp add: summable_iff_convergent')
qed

lemma summable_imp_abs_convergent_prod:
  fixes f :: "nat ⇒ 'a :: real_normed_div_algebra"
  assumes "summable (λi. norm (f i - 1))"
  shows   "abs_convergent_prod f"
proof (intro abs_convergent_prodI Bseq_monoseq_convergent)
  show "monoseq (λn. ∏i≤n. 1 + norm (f i - 1))"
    by (intro mono_SucI1) 
       (auto simp: atMost_Suc algebra_simps intro!: mult_nonneg_nonneg prod_nonneg)
next
  show "Bseq (λn. ∏i≤n. 1 + norm (f i - 1))"
  proof (rule Bseq_eventually_mono)
    show "eventually (λn. norm (∏i≤n. 1 + norm (f i - 1)) ≤ 
            norm (exp (∑i≤n. norm (f i - 1)))) sequentially"
      by (intro always_eventually allI) (auto simp: abs_prod exp_sum intro!: prod_mono)
  next
    from assms have "(λn. ∑i≤n. norm (f i - 1)) ⇢ (∑i. norm (f i - 1))"
      using sums_def_le by blast
    hence "(λn. exp (∑i≤n. norm (f i - 1))) ⇢ exp (∑i. norm (f i - 1))"
      by (rule tendsto_exp)
    hence "convergent (λn. exp (∑i≤n. norm (f i - 1)))"
      by (rule convergentI)
    thus "Bseq (λn. exp (∑i≤n. norm (f i - 1)))"
      by (rule convergent_imp_Bseq)
  qed
qed

lemma abs_convergent_prod_conv_summable:
  fixes f :: "nat ⇒ 'a :: real_normed_div_algebra"
  shows "abs_convergent_prod f ⟷ summable (λi. norm (f i - 1))"
  by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod)

lemma abs_convergent_prod_imp_LIMSEQ:
  fixes f :: "nat ⇒ 'a :: {comm_ring_1,real_normed_div_algebra}"
  assumes "abs_convergent_prod f"
  shows   "f ⇢ 1"
proof -
  from assms have "summable (λn. norm (f n - 1))"
    by (rule abs_convergent_prod_imp_summable)
  from summable_LIMSEQ_zero[OF this] have "(λn. f n - 1) ⇢ 0"
    by (simp add: tendsto_norm_zero_iff)
  from tendsto_add[OF this tendsto_const[of 1]] show ?thesis by simp
qed

lemma abs_convergent_prod_imp_ev_nonzero:
  fixes f :: "nat ⇒ 'a :: {comm_ring_1,real_normed_div_algebra}"
  assumes "abs_convergent_prod f"
  shows   "eventually (λn. f n ≠ 0) sequentially"
proof -
  from assms have "f ⇢ 1" 
    by (rule abs_convergent_prod_imp_LIMSEQ)
  hence "eventually (λn. dist (f n) 1 < 1) at_top"
    by (auto simp: tendsto_iff)
  thus ?thesis by eventually_elim auto
qed

lemma convergent_prod_offset:
  assumes "convergent_prod (λn. f (n + m))"  
  shows   "convergent_prod f"
proof -
  from assms obtain M L where "(λn. ∏k≤n. f (k + (M + m))) ⇢ L" "L ≠ 0"
    by (auto simp: convergent_prod_def add.assoc)
  thus "convergent_prod f" unfolding convergent_prod_def by blast
qed

lemma abs_convergent_prod_offset:
  assumes "abs_convergent_prod (λn. f (n + m))"  
  shows   "abs_convergent_prod f"
  using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset)

lemma convergent_prod_ignore_initial_segment:
  fixes f :: "nat ⇒ 'a :: {real_normed_field}"
  assumes "convergent_prod f"
  shows   "convergent_prod (λn. f (n + m))"
proof -
  from assms obtain M L 
    where L: "(λn. ∏k≤n. f (k + M)) ⇢ L" "L ≠ 0" and nz: "⋀n. n ≥ M ⟹ f n ≠ 0"
    by (auto simp: convergent_prod_altdef)
  define C where "C = (∏k<m. f (k + M))"
  from nz have [simp]: "C ≠ 0" 
    by (auto simp: C_def)

  from L(1) have "(λn. ∏k≤n+m. f (k + M)) ⇢ L" 
    by (rule LIMSEQ_ignore_initial_segment)
  also have "(λn. ∏k≤n+m. f (k + M)) = (λn. C * (∏k≤n. f (k + M + m)))"
  proof (rule ext, goal_cases)
    case (1 n)
    have "{..n+m} = {..<m} ∪ {m..n+m}" by auto
    also have "(∏k∈…. f (k + M)) = C * (∏k=m..n+m. f (k + M))"
      unfolding C_def by (rule prod.union_disjoint) auto
    also have "(∏k=m..n+m. f (k + M)) = (∏k≤n. f (k + m + M))"
      by (intro ext prod.reindex_bij_witness[of _ "λk. k + m" "λk. k - m"]) auto
    finally show ?case by (simp add: add_ac)
  qed
  finally have "(λn. C * (∏k≤n. f (k + M + m)) / C) ⇢ L / C"
    by (intro tendsto_divide tendsto_const) auto
  hence "(λn. ∏k≤n. f (k + M + m)) ⇢ L / C" by simp
  moreover from ‹L ≠ 0› have "L / C ≠ 0" by simp
  ultimately show ?thesis unfolding convergent_prod_def by blast
qed

lemma abs_convergent_prod_ignore_initial_segment:
  assumes "abs_convergent_prod f"
  shows   "abs_convergent_prod (λn. f (n + m))"
  using assms unfolding abs_convergent_prod_def 
  by (rule convergent_prod_ignore_initial_segment)

lemma summable_LIMSEQ': 
  assumes "summable (f::nat⇒'a::{t2_space,comm_monoid_add})"
  shows   "(λn. ∑i≤n. f i) ⇢ suminf f"
  using assms sums_def_le by blast

lemma abs_convergent_prod_imp_convergent_prod:
  fixes f :: "nat ⇒ 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}"
  assumes "abs_convergent_prod f"
  shows   "convergent_prod f"
proof -
  from assms have "eventually (λn. f n ≠ 0) sequentially"
    by (rule abs_convergent_prod_imp_ev_nonzero)
  then obtain N where N: "f n ≠ 0" if "n ≥ N" for n 
    by (auto simp: eventually_at_top_linorder)
  let ?P = "λn. ∏i≤n. f (i + N)" and ?Q = "λn. ∏i≤n. 1 + norm (f (i + N) - 1)"

  have "Cauchy ?P"
  proof (rule CauchyI', goal_cases)
    case (1 ε)
    from assms have "abs_convergent_prod (λn. f (n + N))"
      by (rule abs_convergent_prod_ignore_initial_segment)
    hence "Cauchy ?Q"
      unfolding abs_convergent_prod_def
      by (intro convergent_Cauchy convergent_prod_imp_convergent)
    from CauchyD[OF this 1] obtain M where M: "norm (?Q m - ?Q n) < ε" if "m ≥ M" "n ≥ M" for m n
      by blast
    show ?case
    proof (rule exI[of _ M], safe, goal_cases)
      case (1 m n)
      have "dist (?P m) (?P n) = norm (?P n - ?P m)"
        by (simp add: dist_norm norm_minus_commute)
      also from 1 have "{..n} = {..m} ∪ {m<..n}" by auto
      hence "norm (?P n - ?P m) = norm (?P m * (∏k∈{m<..n}. f (k + N)) - ?P m)"
        by (subst prod.union_disjoint [symmetric]) (auto simp: algebra_simps)
      also have "… = norm (?P m * ((∏k∈{m<..n}. f (k + N)) - 1))"
        by (simp add: algebra_simps)
      also have "… = (∏k≤m. norm (f (k + N))) * norm ((∏k∈{m<..n}. f (k + N)) - 1)"
        by (simp add: norm_mult prod_norm)
      also have "… ≤ ?Q m * ((∏k∈{m<..n}. 1 + norm (f (k + N) - 1)) - 1)"
        using norm_prod_minus1_le_prod_minus1[of "λk. f (k + N) - 1" "{m<..n}"]
              norm_triangle_ineq[of 1 "f k - 1" for k]
        by (intro mult_mono prod_mono ballI conjI norm_prod_minus1_le_prod_minus1 prod_nonneg) auto
      also have "… = ?Q m * (∏k∈{m<..n}. 1 + norm (f (k + N) - 1)) - ?Q m"
        by (simp add: algebra_simps)
      also have "?Q m * (∏k∈{m<..n}. 1 + norm (f (k + N) - 1)) = 
                   (∏k∈{..m}∪{m<..n}. 1 + norm (f (k + N) - 1))"
        by (rule prod.union_disjoint [symmetric]) auto
      also from 1 have "{..m}∪{m<..n} = {..n}" by auto
      also have "?Q n - ?Q m ≤ norm (?Q n - ?Q m)" by simp
      also from 1 have "… < ε" by (intro M) auto
      finally show ?case .
    qed
  qed
  hence conv: "convergent ?P" by (rule Cauchy_convergent)
  then obtain L where L: "?P ⇢ L"
    by (auto simp: convergent_def)

  have "L ≠ 0"
  proof
    assume [simp]: "L = 0"
    from tendsto_norm[OF L] have limit: "(λn. ∏k≤n. norm (f (k + N))) ⇢ 0" 
      by (simp add: prod_norm)

    from assms have "(λn. f (n + N)) ⇢ 1"
      by (intro abs_convergent_prod_imp_LIMSEQ abs_convergent_prod_ignore_initial_segment)
    hence "eventually (λn. norm (f (n + N) - 1) < 1) sequentially"
      by (auto simp: tendsto_iff dist_norm)
    then obtain M0 where M0: "norm (f (n + N) - 1) < 1" if "n ≥ M0" for n
      by (auto simp: eventually_at_top_linorder)

    {
      fix M assume M: "M ≥ M0"
      with M0 have M: "norm (f (n + N) - 1) < 1" if "n ≥ M" for n using that by simp

      have "(λn. ∏k≤n. 1 - norm (f (k+M+N) - 1)) ⇢ 0"
      proof (rule tendsto_sandwich)
        show "eventually (λn. (∏k≤n. 1 - norm (f (k+M+N) - 1)) ≥ 0) sequentially"
          using M by (intro always_eventually prod_nonneg allI ballI) (auto intro: less_imp_le)
        have "norm (1::'a) - norm (f (i + M + N) - 1) ≤ norm (f (i + M + N))" for i
          using norm_triangle_ineq3[of "f (i + M + N)" 1] by simp
        thus "eventually (λn. (∏k≤n. 1 - norm (f (k+M+N) - 1)) ≤ (∏k≤n. norm (f (k+M+N)))) at_top"
          using M by (intro always_eventually allI prod_mono ballI conjI) (auto intro: less_imp_le)
        
        define C where "C = (∏k<M. norm (f (k + N)))"
        from N have [simp]: "C ≠ 0" by (auto simp: C_def)
        from L have "(λn. norm (∏k≤n+M. f (k + N))) ⇢ 0"
          by (intro LIMSEQ_ignore_initial_segment) (simp add: tendsto_norm_zero_iff)
        also have "(λn. norm (∏k≤n+M. f (k + N))) = (λn. C * (∏k≤n. norm (f (k + M + N))))"
        proof (rule ext, goal_cases)
          case (1 n)
          have "{..n+M} = {..<M} ∪ {M..n+M}" by auto
          also have "norm (∏k∈…. f (k + N)) = C * norm (∏k=M..n+M. f (k + N))"
            unfolding C_def by (subst prod.union_disjoint) (auto simp: norm_mult prod_norm)
          also have "(∏k=M..n+M. f (k + N)) = (∏k≤n. f (k + N + M))"
            by (intro prod.reindex_bij_witness[of _ "λi. i + M" "λi. i - M"]) auto
          finally show ?case by (simp add: add_ac prod_norm)
        qed
        finally have "(λn. C * (∏k≤n. norm (f (k + M + N))) / C) ⇢ 0 / C"
          by (intro tendsto_divide tendsto_const) auto
        thus "(λn. ∏k≤n. norm (f (k + M + N))) ⇢ 0" by simp
      qed simp_all

      have "1 - (∑i. norm (f (i + M + N) - 1)) ≤ 0"
      proof (rule tendsto_le)
        show "eventually (λn. 1 - (∑k≤n. norm (f (k+M+N) - 1)) ≤ 
                                (∏k≤n. 1 - norm (f (k+M+N) - 1))) at_top"
          using M by (intro always_eventually allI weierstrass_prod_ineq) (auto intro: less_imp_le)
        show "(λn. ∏k≤n. 1 - norm (f (k+M+N) - 1)) ⇢ 0" by fact
        show "(λn. 1 - (∑k≤n. norm (f (k + M + N) - 1)))
                  ⇢ 1 - (∑i. norm (f (i + M + N) - 1))"
          by (intro tendsto_intros summable_LIMSEQ' summable_ignore_initial_segment 
                abs_convergent_prod_imp_summable assms)
      qed simp_all
      hence "(∑i. norm (f (i + M + N) - 1)) ≥ 1" by simp
      also have "… + (∑i<M. norm (f (i + N) - 1)) = (∑i. norm (f (i + N) - 1))"
        by (intro suminf_split_initial_segment [symmetric] summable_ignore_initial_segment
              abs_convergent_prod_imp_summable assms)
      finally have "1 + (∑i<M. norm (f (i + N) - 1)) ≤ (∑i. norm (f (i + N) - 1))" by simp
    } note * = this

    have "1 + (∑i. norm (f (i + N) - 1)) ≤ (∑i. norm (f (i + N) - 1))"
    proof (rule tendsto_le)
      show "(λM. 1 + (∑i<M. norm (f (i + N) - 1))) ⇢ 1 + (∑i. norm (f (i + N) - 1))"
        by (intro tendsto_intros summable_LIMSEQ summable_ignore_initial_segment 
                abs_convergent_prod_imp_summable assms)
      show "eventually (λM. 1 + (∑i<M. norm (f (i + N) - 1)) ≤ (∑i. norm (f (i + N) - 1))) at_top"
        using eventually_ge_at_top[of M0] by eventually_elim (use * in auto)
    qed simp_all
    thus False by simp
  qed
  with L show ?thesis by (auto simp: convergent_prod_def)
qed

end