Quelle Infinite_Products.thy Sprache: Isabelle

(*File:      HOL/Analysis/Infinite_Product.thy
  Author:    Manuel Eberl & LC Paulson

  Basic results about convergence and absolute convergence of infinite products
  and their connection to summability.
*)
section \<open>Infinite Products\<close>
theory Infinite_Products
  imports Topology_Euclidean_Space Complex_Transcendental
begin

subsection\<^marker>\<open>tag unimportant\<close> \<open>Preliminaries\<close>

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 "\\<^sub>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

subsection\<open>Definitions and basic properties\<close>

definition\<^marker>\<open>tag important\<close> raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool"
  where "raw_has_prod f M p \ (\n. \i\n. f (i+M)) \ p \ p \ 0"

text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close>
text\<^marker>\<open>tag important\<close> \<open>%whitespace\<close>
definition\<^marker>\<open>tag important\<close>
  has_prod :: "(nat \ 'a::{t2_space, comm_semiring_1}) \ 'a \ bool" (infixr \has'_prod\ 80)
  where "f has_prod p \ raw_has_prod f 0 p \ (\i q. p = 0 \ f i = 0 \ raw_has_prod f (Suc i) q)"

definition\<^marker>\<open>tag important\<close> convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where
  "convergent_prod f \ \M p. raw_has_prod f M p"

definition\<^marker>\<open>tag important\<close> prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a"
    (binder \<open>\<Prod>\<close> 10)
  where "prodinf f = (THE p. f has_prod p)"

lemmas prod_defs = raw_has_prod_def has_prod_def convergent_prod_def prodinf_def

lemma has_prod_subst[trans]: "f = g \ g has_prod z \ f has_prod z"
  by simp

lemma has_prod_cong: "(\n. f n = g n) \ f has_prod c \ g has_prod c"
  by presburger

lemma raw_has_prod_nonzero [simp]: "\ raw_has_prod f M 0"
  by (simp add: raw_has_prod_def)

lemma raw_has_prod_eq_0:
  fixes f :: "nat \ 'a::{semidom,t2_space}"
  assumes p: "raw_has_prod f m p" and i: "f i = 0" "i \ m"
  shows "p = 0"
proof -
  have eq0: "(\k\n. f (k+m)) = 0" if "i - m \ n" for n
  proof -
    have "\k\n. f (k + m) = 0"
      using i that by auto
    then show ?thesis
      by auto
  qed
  have "(\n. \i\n. f (i + m)) \ 0"
    by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0)
    with p show ?thesis
      unfolding raw_has_prod_def
    using LIMSEQ_unique by blast
qed

lemma raw_has_prod_Suc:
  "raw_has_prod f (Suc M) a \ raw_has_prod (\n. f (Suc n)) M a"
  unfolding raw_has_prod_def by auto

lemma has_prod_0_iff: "f has_prod 0 \ (\i. f i = 0 \ (\p. raw_has_prod f (Suc i) p))"
  by (simp add: has_prod_def)

lemma has_prod_unique2:
  fixes f :: "nat \ 'a::{semidom,t2_space}"
  assumes "f has_prod a" "f has_prod b" shows "a = b"
  using assms
  by (auto simp: has_prod_def raw_has_prod_eq_0) (meson raw_has_prod_def sequentially_bot tendsto_unique)

lemma has_prod_unique:
  fixes f :: "nat \ 'a :: {semidom,t2_space}"
  shows "f has_prod s \ s = prodinf f"
  by (simp add: has_prod_unique2 prodinf_def the_equality)

lemma has_prod_eq_0_iff:
  fixes f :: "nat \ 'a :: {semidom, comm_semiring_1, t2_space}"
  assumes "f has_prod P"
  shows   "P = 0 \ 0 \ range f"
proof
  assume "0 \ range f"
  then obtain N where N: "f N = 0"
    by auto
  have "eventually (\n. n > N) at_top"
    by (rule eventually_gt_at_top)
  hence "eventually (\n. (\k
    by eventually_elim (use N in auto)
  hence "(\n. \k 0"
    by (simp add: tendsto_eventually)
  moreover have "(\n. \k P"
    using assms by (metis N calculation prod_defs(2) raw_has_prod_eq_0 zero_le)
  ultimately show "P = 0"
    using tendsto_unique by force
qed (use assms in \<open>auto simp: has_prod_def\<close>)

lemma has_prod_0D:
  fixes f :: "nat \ 'a :: {semidom, comm_semiring_1, t2_space}"
  shows "f has_prod 0 \ 0 \ range f"
  using has_prod_eq_0_iff[of f 0] by auto

lemma has_prod_zeroI:
  fixes f :: "nat \ 'a :: {semidom, comm_semiring_1, t2_space}"
  assumes "f has_prod P" "f n = 0"
  shows   "P = 0"
  using assms by (auto simp: has_prod_eq_0_iff)

lemma raw_has_prod_in_Reals:
  assumes "raw_has_prod (complex_of_real \ z) M p"
  shows "p \ \"
  using assms by (auto simp: raw_has_prod_def real_lim_sequentially)

lemma raw_has_prod_of_real_iff: "raw_has_prod (complex_of_real \ z) M (of_real p) \ raw_has_prod z M p"
  by (auto simp: raw_has_prod_def tendsto_of_real_iff simp flip: of_real_prod)

lemma convergent_prod_of_real_iff: "convergent_prod (complex_of_real \ z) \ convergent_prod z"
  by (smt (verit, best) Reals_cases convergent_prod_def raw_has_prod_in_Reals raw_has_prod_of_real_iff)

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: prod_defs)
  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 \<open>f i = 0\<close> and \<open>i \<ge> M\<close> 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: prod_defs)

lemma raw_has_prod_norm:
  fixes a :: "'a ::real_normed_field"
  assumes "raw_has_prod f M a"
  shows "raw_has_prod (\n. norm (f n)) M (norm a)"
  using assms by (auto simp: raw_has_prod_def prod_norm tendsto_norm)

lemma has_prod_norm:
  fixes a :: "'a ::real_normed_field"
  assumes f: "f has_prod a"
  shows "(\n. norm (f n)) has_prod (norm a)"
  using f [unfolded has_prod_def]
proof (elim disjE exE conjE)
  assume f0: "raw_has_prod f 0 a"
  then show "(\n. norm (f n)) has_prod norm a"
    using has_prod_def raw_has_prod_norm by blast
next
  fix i p
  assume "a = 0" and "f i = 0" and p: "raw_has_prod f (Suc i) p"
  then have "Ex (raw_has_prod (\n. norm (f n)) (Suc i))"
    using raw_has_prod_norm by blast
  then show ?thesis
    by (metis \<open>a = 0\<close> \<open>f i = 0\<close> has_prod_0_iff norm_zero)
qed

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 \<open>n \<ge> N\<close> \<open>f n = 0\<close> 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 \<open>P \<noteq> 0\<close> 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 \<open>f N = 0\<close> by blast
qed

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

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 \<open>auto intro!: always_eventually prod_nonneg\<close>)

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

subsection\<open>Absolutely convergent products\<close>

definition\<^marker>\<open>tag important\<close> abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> 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 prod_defs
    by (intro exI[of _ "0::nat"] exI[of _ L]) auto
qed

lemma
  fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}"
  assumes "convergent_prod f"
  shows   convergent_prod_imp_convergent:     "convergent (\n. \i\n. f i)"
    and   convergent_prod_to_zero_iff [simp]: "(\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. (\ii=M..M+n. f i)) \ (\i
    by (intro tendsto_mult tendsto_const)
  also have "(\n. (\ii=M..M+n. f i)) = (\n. (\i\{..{M..M+n}. f i))"
    by (subst prod.union_disjoint) auto
  also have "(\n. {.. {M..M+n}) = (\n. {..n+M})" by auto
  finally have lim: "(\n. prod f {..n}) \ prod f {..
    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
    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 \<open>L \<noteq> 0\<close>
    show "\i. f i = 0" by auto
  qed
qed

lemma convergent_prod_iff_nz_lim:
  fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}"
  assumes "\i. f i \ 0"
  shows "convergent_prod f \ (\L. (\n. \i\n. f i) \ L \ L \ 0)"
    (is "?lhs \ ?rhs")
proof
  assume ?lhs then show ?rhs
    using assms convergentD convergent_prod_imp_convergent convergent_prod_to_zero_iff by blast
next
  assume ?rhs then show ?lhs
    unfolding prod_defs
    by (rule_tac x=0 in exI) auto
qed

lemma\<^marker>\<open>tag important\<close> convergent_prod_iff_convergent:
  fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}"
  assumes "\i. f i \ 0"
  shows "convergent_prod f \ convergent (\n. \i\n. f i) \ lim (\n. \i\n. f i) \ 0"
  by (force simp: convergent_prod_iff_nz_lim assms convergent_def limI)

lemma bounded_imp_convergent_prod:
  fixes a :: "nat \ real"
  assumes 1: "\n. a n \ 1" and bounded: "\n. (\i\n. a i) \ B"
  shows "convergent_prod a"
proof -
  have "bdd_above (range(\n. \i\n. a i))"
    by (meson bdd_aboveI2 bounded)
  moreover have "incseq (\n. \i\n. a i)"
    unfolding mono_def by (metis 1 prod_mono2 atMost_subset_iff dual_order.trans finite_atMost zero_le_one)
  ultimately obtain p where p: "(\n. \i\n. a i) \ p"
    using LIMSEQ_incseq_SUP by blast
  then have "p \ 0"
    by (metis "1" not_one_le_zero prod_ge_1 LIMSEQ_le_const)
  with 1 p show ?thesis
    by (metis convergent_prod_iff_nz_lim not_one_le_zero)
qed

lemma abs_convergent_prod_altdef:
  fixes f :: "nat \ 'a :: {one,real_normed_vector}"
  shows  "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 ((\<Prod>n\<in>A. 1 + f n) - 1 + f x * (\<Prod>n\<in>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)) =
             (\<Prod>n\<in>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 "\\<^sub>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 (\<Sum>i\<le>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

theorem 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

subsection\<^marker>\<open>tag unimportant\<close> \<open>Ignoring initial segments\<close>

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: prod_defs add.assoc)
  thus "convergent_prod f"
    unfolding prod_defs 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 raw_has_prod_ignore_initial_segment:
  fixes f :: "nat \ 'a :: real_normed_field"
  assumes "raw_has_prod f M p" "N \ M"
  obtains q where  "raw_has_prod f N q"
proof -
  have p: "(\n. \k\n. f (k + M)) \ p" and "p \ 0"
    using assms by (auto simp: raw_has_prod_def)
  then have nz: "\n. n \ M \ f n \ 0"
    using assms by (auto simp: raw_has_prod_eq_0)
  define C where "C = (\k
  from nz have [simp]: "C \ 0"
    by (auto simp: C_def)

  from p have "(\i. \k\i + (N-M). f (k + M)) \ p"
    by (rule LIMSEQ_ignore_initial_segment)
  also have "(\i. \k\i + (N-M). f (k + M)) = (\n. C * (\k\n. f (k + N)))"
  proof (rule ext, goal_cases)
    case (1 n)
    have "{..n+(N-M)} = {..<(N-M)} \ {(N-M)..n+(N-M)}" by auto
    also have "(\k\\. f (k + M)) = C * (\k=(N-M)..n+(N-M). f (k + M))"
      unfolding C_def by (rule prod.union_disjoint) auto
    also have "(\k=(N-M)..n+(N-M). f (k + M)) = (\k\n. f (k + (N-M) + M))"
      by (intro ext prod.reindex_bij_witness[of _ "\k. k + (N-M)" "\k. k - (N-M)"]) auto
    finally show ?case
      using \<open>N \<ge> M\<close> by (simp add: add_ac)
  qed
  finally have "(\n. C * (\k\n. f (k + N)) / C) \ p / C"
    by (intro tendsto_divide tendsto_const) auto
  hence "(\n. \k\n. f (k + N)) \ p / C" by simp
  moreover from \<open>p \<noteq> 0\<close> have "p / C \<noteq> 0" by simp
  ultimately show ?thesis
    using raw_has_prod_def that by blast
qed

corollary\<^marker>\<open>tag unimportant\<close> convergent_prod_ignore_initial_segment:
  fixes f :: "nat \ 'a :: real_normed_field"
  assumes "convergent_prod f"
  shows   "convergent_prod (\n. f (n + m))"
  using assms
  unfolding convergent_prod_def
  apply clarify
  apply (erule_tac N="M+m" in raw_has_prod_ignore_initial_segment)
  apply (auto simp add: raw_has_prod_def add_ac)
  done

corollary\<^marker>\<open>tag unimportant\<close> convergent_prod_ignore_nonzero_segment:
  fixes f :: "nat \ 'a :: real_normed_field"
  assumes f: "convergent_prod f" and nz: "\i. i \ M \ f i \ 0"
  shows "\p. raw_has_prod f M p"
  using convergent_prod_ignore_initial_segment [OF f]
  by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1))

corollary\<^marker>\<open>tag unimportant\<close> 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)

subsection\<open>More elementary properties\<close>

theorem 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 \<epsilon>)
    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)) =
                   (\<Prod>k\<in>{..m}\<union>{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
        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..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)) \
                                (\<Prod>k\<le>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)))
                  \<longlonglongrightarrow> 1 - (\<Sum>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 "\ + (\ii. 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 (\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 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 (\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: prod_defs)
qed

lemma raw_has_prod_cases:
  fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}"
  assumes "raw_has_prod f M p"
  obtains i where "i "f i = 0" | p where "raw_has_prod f 0 p"
proof -
  have "(\n. \i\n. f (i + M)) \ p" "p \ 0"
    using assms unfolding raw_has_prod_def by blast+
  then have "(\n. prod f {..i\n. f (i + M))) \ prod f {..
    by (metis tendsto_mult_left)
  moreover have "prod f {..i\n. f (i + M)) = prod f {..n+M}" for n
  proof -
    have "{..n+M} = {.. {M..n+M}"
      by auto
    then have "prod f {..n+M} = prod f {..
      by simp (subst prod.union_disjoint; force)
    also have "\ = prod f {..i\n. f (i + M))"
      by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod.shift_bounds_cl_nat_ivl)
    finally show ?thesis by metis
  qed
  ultimately have "(\n. prod f {..n}) \ prod f {..
    by (auto intro: LIMSEQ_offset [where k=M])
  then have "raw_has_prod f 0 (prod f {.. if "\i 0"
    using \<open>p \<noteq> 0\<close> assms that by (auto simp: raw_has_prod_def)
  then show thesis
    using that by blast
qed

corollary convergent_prod_offset_0:
  fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}"
  assumes "convergent_prod f" "\i. f i \ 0"
  shows "\p. raw_has_prod f 0 p"
  using assms convergent_prod_def raw_has_prod_cases by blast

lemma prodinf_eq_lim:
  fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}"
  assumes "convergent_prod f" "\i. f i \ 0"
  shows "prodinf f = lim (\n. \i\n. f i)"
  using assms convergent_prod_offset_0 [OF assms]
  by (simp add: prod_defs lim_def) (metis (no_types) assms(1) convergent_prod_to_zero_iff)

lemma prodinf_eq_lim':
  fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}"
  assumes "convergent_prod f" "\i. f i \ 0"
  shows "prodinf f = lim (\n. \i
  by (metis assms prodinf_eq_lim LIMSEQ_lessThan_iff_atMost convergent_prod_iff_nz_lim limI)

lemma prodinf_eq_prod_lim:
  fixes a:: "'a :: {topological_semigroup_mult,t2_space,idom}"
  assumes "(\n. \k\n. f k) \ a" "a \ 0"
  shows"(\k. f k) = a"
  by (metis LIMSEQ_prod_0 LIMSEQ_unique assms convergent_prod_iff_nz_lim limI prodinf_eq_lim)

lemma prodinf_eq_prod_lim':
  fixes a:: "'a :: {topological_semigroup_mult,t2_space,idom}"
  assumes "(\n. \k a" "a \ 0"
  shows"(\k. f k) = a"
  using LIMSEQ_lessThan_iff_atMost assms prodinf_eq_prod_lim by blast

lemma has_prod_one[simp, intro]: "(\n. 1) has_prod 1"
  unfolding prod_defs by auto

lemma convergent_prod_one[simp, intro]: "convergent_prod (\n. 1)"
  unfolding prod_defs by auto

lemma prodinf_cong: "(\n. f n = g n) \ prodinf f = prodinf g"
  by presburger

lemma convergent_prod_cong:
  fixes f g :: "nat \ 'a::{field,topological_semigroup_mult,t2_space}"
  assumes ev: "eventually (\x. f x = g x) sequentially" and f: "\i. f i \ 0" and g: "\i. g i \ 0"
  shows "convergent_prod f = convergent_prod g"
proof -
  from assms obtain N where N: "\n\N. f n = g n"
    by (auto simp: eventually_at_top_linorder)
  define C where "C = (\k
  with g have "C \ 0"
    by (simp add: f)
  have *: "eventually (\n. prod f {..n} = C * prod g {..n}) sequentially"
    using eventually_ge_at_top[of N]
  proof eventually_elim
    case (elim n)
    then have "{..n} = {.. {N..n}"
      by auto
    also have "prod f \ = prod f {..
      by (intro prod.union_disjoint) auto
    also from N have "prod f {N..n} = prod g {N..n}"
      by (intro prod.cong) simp_all
    also have "prod f {..
      unfolding C_def by (simp add: g prod_dividef)
    also have "prod g {.. {N..n})"
      by (intro prod.union_disjoint [symmetric]) auto
    also from elim have "{.. {N..n} = {..n}"
      by auto
    finally show "prod f {..n} = C * prod g {..n}" .
  qed
  then have cong: "convergent (\n. prod f {..n}) = convergent (\n. C * prod g {..n})"
    by (rule convergent_cong)
  show ?thesis
  proof
    assume cf: "convergent_prod f"
    with f have "\ (\n. prod f {..n}) \ 0"
      by simp
    then have "\ (\n. prod g {..n}) \ 0"
      using * \<open>C \<noteq> 0\<close> filterlim_cong by fastforce
    then show "convergent_prod g"
      by (metis convergent_mult_const_iff \<open>C \<noteq> 0\<close> cong cf convergent_LIMSEQ_iff convergent_prod_iff_convergent convergent_prod_imp_convergent g)
  next
    assume cg: "convergent_prod g"
    have **: "eventually (\n. prod g {..n} = prod f {..n} / C) sequentially"
      using * by eventually_elim (use \<open>C \<noteq> 0\<close> in auto)
    from cg and g have "\ (\n. prod g {..n}) \ 0"
      by simp
    then have "\ (\n. prod f {..n}) \ 0"
      using ** \<open>C \<noteq> 0\<close> filterlim_cong by fastforce
    then show "convergent_prod f"
      by (metis \<open>C \<noteq> 0\<close> cg convergent_LIMSEQ_iff
          convergent_mult_const_iff convergent_prod_iff_convergent
          convergent_prod_imp_convergent f local.cong)
  qed
qed

lemma has_prod_finite:
  fixes f :: "nat \ 'a::{semidom,t2_space}"
  assumes [simp]: "finite N"
    and f: "\n. n \ N \ f n = 1"
  shows "f has_prod (\n\N. f n)"
proof -
  have eq: "prod f {..n + Suc (Max N)} = prod f N" for n
  proof (rule prod.mono_neutral_right)
    show "N \ {..n + Suc (Max N)}"
      by (auto simp: le_Suc_eq trans_le_add2)
    show "\i\{..n + Suc (Max N)} - N. f i = 1"
      using f by blast
  qed auto
  show ?thesis
  proof (cases "\n\N. f n \ 0")
    case True
    then have "prod f N \ 0"
      by simp
    moreover have "(\n. prod f {..n}) \ prod f N"
      by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) (simp add: eq atLeast0LessThan del: add_Suc_right)
    ultimately show ?thesis
      by (simp add: raw_has_prod_def has_prod_def)
  next
    case False
    then obtain k where "k \ N" "f k = 0"
      by auto
    let ?Z = "{n \ N. f n = 0}"
    have maxge: "Max ?Z \ n" if "f n = 0" for n
      using Max_ge [of ?Z] \<open>finite N\<close> \<open>f n = 0\<close>
      by (metis (mono_tags) Collect_mem_eq f finite_Collect_conjI mem_Collect_eq zero_neq_one)
    let ?q = "prod f {Suc (Max ?Z)..Max N}"
    have [simp]: "?q \ 0"
      using maxge Suc_n_not_le_n le_trans by force
    have eq: "(\i\n + Max N. f (Suc (i + Max ?Z))) = ?q" for n
    proof -
      have "(\i\n + Max N. f (Suc (i + Max ?Z))) = prod f {Suc (Max ?Z)..n + Max N + Suc (Max ?Z)}"
      proof (rule prod.reindex_cong [where l = "\i. i + Suc (Max ?Z)", THEN sym])
        show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\i. i + Suc (Max ?Z)) ` {..n + Max N}"
          using le_Suc_ex by fastforce
      qed (auto simp: inj_on_def)
      also have "\ = ?q"
        by (rule prod.mono_neutral_right)
           (use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>)
      finally show ?thesis .
    qed
    have q: "raw_has_prod f (Suc (Max ?Z)) ?q"
    proof (simp add: raw_has_prod_def)
      show "(\n. \i\n. f (Suc (i + Max ?Z))) \ ?q"
        by (rule LIMSEQ_offset[of _ "(Max N)"]) (simp add: eq)
    qed
    show ?thesis
      unfolding has_prod_def
    proof (intro disjI2 exI conjI)
      show "prod f N = 0"
        using \<open>f k = 0\<close> \<open>k \<in> N\<close> \<open>finite N\<close> prod_zero by blast
      show "f (Max ?Z) = 0"
        using Max_in [of ?Z] \<open>finite N\<close> \<open>f k = 0\<close> \<open>k \<in> N\<close> by auto
    qed (use q in auto)
  qed
qed

corollary\<^marker>\<open>tag unimportant\<close> has_prod_0:
  fixes f :: "nat \ 'a::{semidom,t2_space}"
  assumes "\n. f n = 1"
  shows "f has_prod 1"
  by (simp add: assms has_prod_cong)

lemma prodinf_zero[simp]: "prodinf (\n. 1::'a::real_normed_field) = 1"
  using has_prod_unique by force

lemma convergent_prod_finite:
  fixes f :: "nat \ 'a::{idom,t2_space}"
  assumes "finite N" "\n. n \ N \ f n = 1"
  shows "convergent_prod f"
proof -
  have "\n p. raw_has_prod f n p"
    using assms has_prod_def has_prod_finite by blast
  then show ?thesis
    by (simp add: convergent_prod_def)
qed

lemma has_prod_If_finite_set:
  fixes f :: "nat \ 'a::{idom,t2_space}"
  shows "finite A \ (\r. if r \ A then f r else 1) has_prod (\r\A. f r)"
  using has_prod_finite[of A "(\r. if r \ A then f r else 1)"]
  by simp

lemma has_prod_If_finite:
  fixes f :: "nat \ 'a::{idom,t2_space}"
  shows "finite {r. P r} \ (\r. if P r then f r else 1) has_prod (\r | P r. f r)"
  using has_prod_If_finite_set[of "{r. P r}"] by simp

lemma convergent_prod_If_finite_set[simp, intro]:
  fixes f :: "nat \ 'a::{idom,t2_space}"
  shows "finite A \ convergent_prod (\r. if r \ A then f r else 1)"
  by (simp add: convergent_prod_finite)

lemma convergent_prod_If_finite[simp, intro]:
  fixes f :: "nat \ 'a::{idom,t2_space}"
  assumes "finite {r. P r}"
  shows   "convergent_prod (\r. if P r then f r else 1)"
proof -
  have "(\r. if P r then f r else 1) has_prod (\r | P r. f r)"
    by (rule has_prod_If_finite) fact
  thus ?thesis
    by (meson convergent_prod_def has_prod_def)
qed

lemma has_prod_single:
  fixes f :: "nat \ 'a::{idom,t2_space}"
  shows "(\r. if r = i then f r else 1) has_prod f i"
  using has_prod_If_finite[of "\r. r = i"] by simp

text \<open>The ge1 assumption can probably be weakened, at the expense of extra work\<close>
lemma uniform_limit_prodinf:
  fixes f:: "nat \ real \ real"
  assumes "uniformly_convergent_on X (\n x. \k
    and ge1: "\x k . x \ X \ f k x \ 1"
  shows "uniform_limit X (\n x. \kx. \k. f k x) sequentially"
proof -
  have ul: "uniform_limit X (\n x. \kx. lim (\n. \k
    using assms uniformly_convergent_uniform_limit_iff by blast
  moreover have "(\k. f k x) = lim (\n. \k X" for x
  proof (intro prodinf_eq_lim')
    have tends: "(\n. \k lim (\n. \k
      using tendsto_uniform_limitI [OF ul] that by metis
    moreover have "(\k 1" for n
      using ge1 by (simp add: prod_ge_1 that)
    ultimately have "lim (\n. \k 1"
      by (meson LIMSEQ_le_const)
    then have "raw_has_prod (\k. f k x) 0 (lim (\n. \k
      using LIMSEQ_lessThan_iff_atMost tends by (auto simp: raw_has_prod_def)
    then show "convergent_prod (\k. f k x)"
      unfolding convergent_prod_def by blast
    show "\k. f k x \ 0"
      by (smt (verit) ge1 that)
  qed
  ultimately show ?thesis
    by (metis (mono_tags, lifting) uniform_limit_cong')
qed

context
  fixes f :: "nat \ 'a :: real_normed_field"
begin

lemma convergent_prod_imp_has_prod:
  assumes "convergent_prod f"
  shows "\p. f has_prod p"
proof -
  obtain M p where p: "raw_has_prod f M p"
    using assms convergent_prod_def by blast
  then have "p \ 0"
    using raw_has_prod_nonzero by blast
  with p have fnz: "f i \ 0" if "i \ M" for i
    using raw_has_prod_eq_0 that by blast
  define C where "C = (\n
  show ?thesis
  proof (cases "\n\M. f n \ 0")
    case True
    then have "C \ 0"
      by (simp add: C_def)
    then show ?thesis
      by (meson True assms convergent_prod_offset_0 fnz has_prod_def nat_le_linear)
  next
    case False
    let ?N = "GREATEST n. f n = 0"
    have 0: "f ?N = 0"
      using fnz False
      by (metis (mono_tags, lifting) GreatestI_ex_nat nat_le_linear)
    have "f i \ 0" if "i > ?N" for i
      by (metis (mono_tags, lifting) Greatest_le_nat fnz leD linear that)
    then have "\p. raw_has_prod f (Suc ?N) p"
      using assms by (auto simp: intro!: convergent_prod_ignore_nonzero_segment)
    then show ?thesis
      unfolding has_prod_def using 0 by blast
  qed
qed

lemma convergent_prod_has_prod [intro]:
  shows "convergent_prod f \ f has_prod (prodinf f)"
  unfolding prodinf_def
  by (metis convergent_prod_imp_has_prod has_prod_unique theI')

lemma convergent_prod_LIMSEQ:
  shows "convergent_prod f \ (\n. \i\n. f i) \ prodinf f"
  by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent
      convergent_prod_to_zero_iff raw_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le)

theorem has_prod_iff: "f has_prod x \ convergent_prod f \ prodinf f = x"
proof
  assume "f has_prod x"
  then show "convergent_prod f \ prodinf f = x"
    apply safe
    using convergent_prod_def has_prod_def apply blast
    using has_prod_unique by blast
qed auto

lemma convergent_prod_has_prod_iff: "convergent_prod f \ f has_prod prodinf f"
  by (auto simp: has_prod_iff convergent_prod_has_prod)

lemma prodinf_finite:
  assumes N: "finite N"
    and f: "\n. n \ N \ f n = 1"
  shows "prodinf f = (\n\N. f n)"
  using has_prod_finite[OF assms, THEN has_prod_unique] by simp

lemma convergent_prod_tendsto_imp_has_prod:
  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)

end

subsection\<^marker>\<open>tag unimportant\<close> \<open>Infinite products on ordered topological monoids\<close>

context
  fixes f :: "nat \ 'a::{linordered_semidom,linorder_topology}"
begin

lemma has_prod_nonzero:
  assumes "f has_prod a" "a \ 0"
  shows "f k \ 0"
  using assms by (auto simp: has_prod_def raw_has_prod_def LIMSEQ_prod_0 LIMSEQ_unique)

lemma has_prod_le:
  assumes f: "f has_prod a" and g: "g has_prod b" and le: "\n. 0 \ f n \ f n \ g n"
  shows "a \ b"
proof (cases "a=0 \ b=0")
  case True
  then show ?thesis
  proof
    assume [simp]: "a=0"
    have "b \ 0"
    proof (rule LIMSEQ_prod_nonneg)
      show "(\n. prod g {..n}) \ b"
        using g by (auto simp: has_prod_def raw_has_prod_def LIMSEQ_prod_0)
    qed (use le order_trans in auto)
    then show ?thesis
      by auto
  next
    assume [simp]: "b=0"
    then obtain i where "g i = 0"
      using g by (auto simp: prod_defs)
    then have "f i = 0"
      using antisym le by force
    then have "a=0"
      using f by (auto simp: prod_defs LIMSEQ_prod_0 LIMSEQ_unique)
    then show ?thesis
      by auto
  qed
next
  case False
  then show ?thesis
    using assms
    unfolding has_prod_def raw_has_prod_def
    by (force simp: LIMSEQ_prod_0 intro!: LIMSEQ_le prod_mono)
qed

lemma prodinf_le:
  assumes f: "f has_prod a" and g: "g has_prod b" and le: "\n. 0 \ f n \ f n \ g n"
  shows "prodinf f \ prodinf g"
  using has_prod_le [OF assms] has_prod_unique f g  by blast

end

lemma prod_le_prodinf:
  fixes f :: "nat \ 'a::{linordered_idom,linorder_topology}"
  assumes "f has_prod a" "\i. 0 \ f i" "\i. i\n \ 1 \ f i"
  shows "prod f {.. prodinf f"
  by(rule has_prod_le[OF has_prod_If_finite_set]) (use assms has_prod_unique in auto)

lemma prodinf_nonneg:
  fixes f :: "nat \ 'a::{linordered_idom,linorder_topology}"
  assumes "f has_prod a" "\i. 1 \ f i"
  shows "1 \ prodinf f"
  using prod_le_prodinf[of f a 0] assms
  by (metis order_trans prod_ge_1 zero_le_one)

lemma prodinf_le_const:
  fixes f :: "nat \ real"
  assumes "convergent_prod f" "\n. n \ N \ prod f {.. x"
  shows "prodinf f \ x"
  by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2 atMost_iff lessThan_iff less_le)

lemma prodinf_eq_one_iff [simp]:
  fixes f :: "nat \ real"
  assumes f: "convergent_prod f" and ge1: "\n. 1 \ f n"
  shows "prodinf f = 1 \ (\n. f n = 1)"
proof
  assume "prodinf f = 1"
  then have "(\n. \i 1"
    using convergent_prod_LIMSEQ[of f] assms by (simp add: LIMSEQ_lessThan_iff_atMost)
  then have "\i. (\n\{i}. f n) \ 1"
  proof (rule LIMSEQ_le_const)
    have "1 \ prod f n" for n
      by (simp add: ge1 prod_ge_1)
    have "prod f {.. for n
      by (metis \<open>\<And>n. 1 \<le> prod f n\<close> \<open>prodinf f = 1\<close> antisym f convergent_prod_has_prod ge1 order_trans prod_le_prodinf zero_le_one)
    then have "(\n\{i}. f n) \ prod f {.. Suc i" for i n
      by (metis mult.left_neutral order_refl prod.cong prod.neutral_const prod.lessThan_Suc)
    then show "\N. \n\N. (\n\{i}. f n) \ prod f {..
      by blast
  qed
  with ge1 show "\n. f n = 1"
    by (auto intro!: antisym)
qed (metis prodinf_zero fun_eq_iff)

lemma prodinf_pos_iff:
  fixes f :: "nat \ real"
  assumes "convergent_prod f" "\n. 1 \ f n"
  shows "1 < prodinf f \ (\i. 1 < f i)"
  using prod_le_prodinf[of f 1] prodinf_eq_one_iff
  by (metis convergent_prod_has_prod assms less_le prodinf_nonneg)

lemma less_1_prodinf2:
  fixes f :: "nat \ real"
  assumes "convergent_prod f" "\n. 1 \ f n" "1 < f i"
  shows "1 < prodinf f"
proof -
  have "1 < (\n
    using assms  by (intro less_1_prod2[where i=i]) auto
  also have "\ \ prodinf f"
    by (intro prod_le_prodinf) (use assms order_trans zero_le_one in \<open>blast+\<close>)
  finally show ?thesis .
qed

lemma less_1_prodinf:
  fixes f :: "nat \ real"
  shows "\convergent_prod f; \n. 1 < f n\ \ 1 < prodinf f"
  by (intro less_1_prodinf2[where i=1]) (auto intro: less_imp_le)

lemma prodinf_nonzero:
  fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}"
  assumes "convergent_prod f" "\i. f i \ 0"
  shows "prodinf f \ 0"
  by (metis assms convergent_prod_offset_0 has_prod_unique raw_has_prod_def has_prod_def)

lemma less_0_prodinf:
  fixes f :: "nat \ real"
  assumes f: "convergent_prod f" and 0: "\i. f i > 0"
  shows "0 < prodinf f"
proof -
  have "prodinf f \ 0"
    by (metis assms less_irrefl prodinf_nonzero)
  moreover have "0 < (\n
    by (simp add: 0 prod_pos)
  then have "prodinf f \ 0"
    using convergent_prod_LIMSEQ [OF f] LIMSEQ_prod_nonneg 0 less_le by blast
  ultimately show ?thesis
    by auto
qed

lemma prod_less_prodinf2:
  fixes f :: "nat \ real"
  assumes f: "convergent_prod f" and 1: "\m. m\n \ 1 \ f m" and 0: "\m. 0 < f m" and i: "n \ i" "1 < f i"
  shows "prod f {..
proof -
  have "prod f {.. prod f {..
    by (rule prod_mono2) (use assms less_le in auto)
  then have "prod f {..
    using mult_less_le_imp_less[of 1 "f i" "prod f {.. "prod f {..] assms
    by (simp add: prod_pos)
  moreover have "prod f {.. prodinf f"
    using prod_le_prodinf[of f _ "Suc i"]
    by (meson "0" "1" Suc_leD convergent_prod_has_prod f \<open>n \<le> i\<close> le_trans less_eq_real_def)
  ultimately show ?thesis
    by (metis le_less_trans mult.commute not_le prod.lessThan_Suc)
qed

lemma prod_less_prodinf:
  fixes f :: "nat \ real"
  assumes f: "convergent_prod f" and 1: "\m. m\n \ 1 < f m" and 0: "\m. 0 < f m"
  shows "prod f {..
  by (meson "0" "1" f le_less prod_less_prodinf2)

lemma raw_has_prodI_bounded:
  fixes f :: "nat \ real"
  assumes pos: "\n. 1 \ f n"
    and le: "\n. (\i x"
  shows "\p. raw_has_prod f 0 p"
  unfolding raw_has_prod_def add_0_right
proof (rule exI LIMSEQ_incseq_SUP conjI)+
  show "bdd_above (range (\n. prod f {..n}))"
    by (metis bdd_aboveI2 le lessThan_Suc_atMost)
  then have "(SUP i. prod f {..i}) > 0"
    by (metis UNIV_I cSUP_upper less_le_trans pos prod_pos zero_less_one)
  then show "(SUP i. prod f {..i}) \ 0"
    by auto
  show "incseq (\n. prod f {..n})"
    using pos order_trans [OF zero_le_one] by (auto simp: mono_def intro!: prod_mono2)
qed

lemma convergent_prodI_nonneg_bounded:
  fixes f :: "nat \ real"
  assumes "\n. 1 \ f n" "\n. (\i x"
  shows "convergent_prod f"
  using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast

subsection\<^marker>\<open>tag unimportant\<close> \<open>Infinite products on topological spaces\<close>

context
  fixes f g :: "nat \ 'a::{t2_space,topological_semigroup_mult,idom}"
begin

lemma raw_has_prod_mult: "\raw_has_prod f M a; raw_has_prod g M b\ \ raw_has_prod (\n. f n * g n) M (a * b)"
  by (force simp add: prod.distrib tendsto_mult raw_has_prod_def)

lemma has_prod_mult_nz: "\f has_prod a; g has_prod b; a \ 0; b \ 0\ \ (\n. f n * g n) has_prod (a * b)"
  by (simp add: raw_has_prod_mult has_prod_def)

end

context
  fixes f g :: "nat \ 'a::real_normed_field"
begin

lemma has_prod_mult:
  assumes f: "f has_prod a" and g: "g has_prod b"
  shows "(\n. f n * g n) has_prod (a * b)"
  using f [unfolded has_prod_def]
proof (elim disjE exE conjE)
  assume f0: "raw_has_prod f 0 a"
  show ?thesis
    using g [unfolded has_prod_def]
  proof (elim disjE exE conjE)
    assume g0: "raw_has_prod g 0 b"
    with f0 show ?thesis
      by (force simp add: has_prod_def prod.distrib tendsto_mult raw_has_prod_def)
  next
    fix j q
    assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q"
    obtain p where p: "raw_has_prod f (Suc j) p"
      using f0 raw_has_prod_ignore_initial_segment by blast
    then have "Ex (raw_has_prod (\n. f n * g n) (Suc j))"
      using q raw_has_prod_mult by blast
    then show ?thesis
      using \<open>b = 0\<close> \<open>g j = 0\<close> has_prod_0_iff by fastforce
  qed
next
  fix i p
  assume "a = 0" and "f i = 0" and p: "raw_has_prod f (Suc i) p"
  show ?thesis
    using g [unfolded has_prod_def]
  proof (elim disjE exE conjE)
    assume g0: "raw_has_prod g 0 b"
    obtain q where q: "raw_has_prod g (Suc i) q"
      using g0 raw_has_prod_ignore_initial_segment by blast
    then have "Ex (raw_has_prod (\n. f n * g n) (Suc i))"
      using raw_has_prod_mult p by blast
    then show ?thesis
      using \<open>a = 0\<close> \<open>f i = 0\<close> has_prod_0_iff by fastforce
  next
    fix j q
    assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q"
    obtain p' where p': "raw_has_prod f (Suc (max i j)) p'"
      by (metis raw_has_prod_ignore_initial_segment max_Suc_Suc max_def p)
    moreover
    obtain q' where q': "raw_has_prod g (Suc (max i j)) q'"
      by (metis raw_has_prod_ignore_initial_segment max.cobounded2 max_Suc_Suc q)
    ultimately show ?thesis
      using \<open>b = 0\<close> by (simp add: has_prod_def) (metis \<open>f i = 0\<close> \<open>g j = 0\<close> raw_has_prod_mult max_def)
  qed
qed

lemma convergent_prod_mult:
  assumes f: "convergent_prod f" and g: "convergent_prod g"
  shows "convergent_prod (\n. f n * g n)"
  unfolding convergent_prod_def
proof -
  obtain M p N q where p: "raw_has_prod f M p" and q: "raw_has_prod g N q"
    using convergent_prod_def f g by blast+
  then obtain p' q' where p': "raw_has_prod f (max M N) p'" and q': "raw_has_prod g (max M N) q'"
    by (meson raw_has_prod_ignore_initial_segment max.cobounded1 max.cobounded2)
  then show "\M p. raw_has_prod (\n. f n * g n) M p"
    using raw_has_prod_mult by blast
qed

lemma prodinf_mult: "convergent_prod f \ convergent_prod g \ prodinf f * prodinf g = (\n. f n * g n)"
  by (intro has_prod_unique has_prod_mult convergent_prod_has_prod)

end

context
  fixes f :: "'i \ nat \ 'a::real_normed_field"
    and I :: "'i set"
begin

lemma has_prod_prod: "(\i. i \ I \ (f i) has_prod (x i)) \ (\n. \i\I. f i n) has_prod (\i\I. x i)"
  by (induct I rule: infinite_finite_induct) (auto intro!: has_prod_mult)

lemma prodinf_prod: "(\i. i \ I \ convergent_prod (f i)) \ (\n. \i\I. f i n) = (\i\I. \n. f i n)"
  using has_prod_unique[OF has_prod_prod, OF convergent_prod_has_prod] by simp

lemma convergent_prod_prod: "(\i. i \ I \ convergent_prod (f i)) \ convergent_prod (\n. \i\I. f i n)"
  using convergent_prod_has_prod_iff has_prod_prod prodinf_prod by force

end

subsection\<^marker>\<open>tag unimportant\<close> \<open>Infinite summability on real normed fields\<close>

context
  fixes f :: "nat \ 'a::real_normed_field"
begin

lemma raw_has_prod_Suc_iff: "raw_has_prod f M (a * f M) \ raw_has_prod (\n. f (Suc n)) M a \ f M \ 0"
proof -
  have "raw_has_prod f M (a * f M) \ (\i. \j\Suc i. f (j+M)) \ a * f M \ a * f M \ 0"
    by (subst filterlim_sequentially_Suc) (simp add: raw_has_prod_def)
  also have "\ \ (\i. (\j\i. f (Suc j + M)) * f M) \ a * f M \ a * f M \ 0"
    by (simp add: ac_simps atMost_Suc_eq_insert_0 image_Suc_atMost prod.atLeast1_atMost_eq lessThan_Suc_atMost
                  del: prod.cl_ivl_Suc)
  also have "\ \ raw_has_prod (\n. f (Suc n)) M a \ f M \ 0"
  proof safe
    assume tends: "(\i. (\j\i. f (Suc j + M)) * f M) \ a * f M" and 0: "a * f M \ 0"
    with tendsto_divide[OF tends tendsto_const, of "f M"]
    show "raw_has_prod (\n. f (Suc n)) M a"
      by (simp add: raw_has_prod_def)
  qed (auto intro: tendsto_mult_right simp:  raw_has_prod_def)
  finally show ?thesis .
qed

lemma has_prod_Suc_iff:
  assumes "f 0 \ 0" shows "(\n. f (Suc n)) has_prod a \ f has_prod (a * f 0)"
proof (cases "a = 0")
  case True
  then show ?thesis
  proof (simp add: has_prod_def, safe)
    fix i x
    assume "f (Suc i) = 0" and "raw_has_prod (\n. f (Suc n)) (Suc i) x"
    then obtain y where "raw_has_prod f (Suc (Suc i)) y"
      by (metis (no_types) raw_has_prod_eq_0 Suc_n_not_le_n raw_has_prod_Suc_iff raw_has_prod_ignore_initial_segment raw_has_prod_nonzero linear)
    then show "\i. f i = 0 \ Ex (raw_has_prod f (Suc i))"
      using \<open>f (Suc i) = 0\<close> by blast
  next
    fix i x
    assume "f i = 0" and x: "raw_has_prod f (Suc i) x"
    then obtain j where j: "i = Suc j"
      by (metis assms not0_implies_Suc)
    moreover have "\ y. raw_has_prod (\n. f (Suc n)) i y"
      using x by (auto simp: raw_has_prod_def)
    then show "\i. f (Suc i) = 0 \ Ex (raw_has_prod (\n. f (Suc n)) (Suc i))"
      using \<open>f i = 0\<close> j by blast
  qed
next
  case False
  then show ?thesis
    by (auto simp: has_prod_def raw_has_prod_Suc_iff assms)
qed

lemma convergent_prod_Suc_iff [simp]:
  shows "convergent_prod (\n. f (Suc n)) = convergent_prod f"
proof
  assume "convergent_prod f"
  then obtain M L where M_nz:"\n\M. f n \ 0" and
        M_L:"(\n. \i\n. f (i + M)) \ L" and "L \ 0"
    unfolding convergent_prod_altdef by auto
  have "(\n. \i\n. f (Suc (i + M))) \ L / f M"
  proof -
    have "(\n. \i\{0..Suc n}. f (i + M)) \ L"
      using M_L
      apply (subst (asm) filterlim_sequentially_Suc[symmetric])
      using atLeast0AtMost by auto
    then have "(\n. f M * (\i\{0..n}. f (Suc (i + M)))) \ L"
      apply (subst (asm) prod.atLeast0_atMost_Suc_shift)
      by simp
    then have "(\n. (\i\{0..n}. f (Suc (i + M)))) \ L/f M"
      apply (drule_tac tendsto_divide)
      using M_nz[rule_format,of M,simplified] by auto
--> --------------------

--> maximum size reached

--> --------------------

quality93%

¤ Dauer der Verarbeitung: 0.25 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.