src/HOL/Analysis/Infinite_Products.thy
 author paulson Tue Jul 03 14:46:14 2018 +0100 (12 months ago) changeset 68585 1657b9a5dd5d parent 68527 2f4e2aab190a child 68586 006da53a8ac1 permissions -rw-r--r--
more on infinite products
     1 (*File:      HOL/Analysis/Infinite_Product.thy

     2   Author:    Manuel Eberl & LC Paulson

     3

     4   Basic results about convergence and absolute convergence of infinite products

     5   and their connection to summability.

     6 *)

     7 section \<open>Infinite Products\<close>

     8 theory Infinite_Products

     9   imports Topology_Euclidean_Space Complex_Transcendental

    10 begin

    11

    12 subsection\<open>Preliminaries\<close>

    13

    14 lemma sum_le_prod:

    15   fixes f :: "'a \<Rightarrow> 'b :: linordered_semidom"

    16   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"

    17   shows   "sum f A \<le> (\<Prod>x\<in>A. 1 + f x)"

    18   using assms

    19 proof (induction A rule: infinite_finite_induct)

    20   case (insert x A)

    21   from insert.hyps have "sum f A + f x * (\<Prod>x\<in>A. 1) \<le> (\<Prod>x\<in>A. 1 + f x) + f x * (\<Prod>x\<in>A. 1 + f x)"

    22     by (intro add_mono insert mult_left_mono prod_mono) (auto intro: insert.prems)

    23   with insert.hyps show ?case by (simp add: algebra_simps)

    24 qed simp_all

    25

    26 lemma prod_le_exp_sum:

    27   fixes f :: "'a \<Rightarrow> real"

    28   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"

    29   shows   "prod (\<lambda>x. 1 + f x) A \<le> exp (sum f A)"

    30   using assms

    31 proof (induction A rule: infinite_finite_induct)

    32   case (insert x A)

    33   have "(1 + f x) * (\<Prod>x\<in>A. 1 + f x) \<le> exp (f x) * exp (sum f A)"

    34     using insert.prems by (intro mult_mono insert prod_nonneg exp_ge_add_one_self) auto

    35   with insert.hyps show ?case by (simp add: algebra_simps exp_add)

    36 qed simp_all

    37

    38 lemma lim_ln_1_plus_x_over_x_at_0: "(\<lambda>x::real. ln (1 + x) / x) \<midarrow>0\<rightarrow> 1"

    39 proof (rule lhopital)

    40   show "(\<lambda>x::real. ln (1 + x)) \<midarrow>0\<rightarrow> 0"

    41     by (rule tendsto_eq_intros refl | simp)+

    42   have "eventually (\<lambda>x::real. x \<in> {-1/2<..<1/2}) (nhds 0)"

    43     by (rule eventually_nhds_in_open) auto

    44   hence *: "eventually (\<lambda>x::real. x \<in> {-1/2<..<1/2}) (at 0)"

    45     by (rule filter_leD [rotated]) (simp_all add: at_within_def)

    46   show "eventually (\<lambda>x::real. ((\<lambda>x. ln (1 + x)) has_field_derivative inverse (1 + x)) (at x)) (at 0)"

    47     using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps)

    48   show "eventually (\<lambda>x::real. ((\<lambda>x. x) has_field_derivative 1) (at x)) (at 0)"

    49     using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps)

    50   show "\<forall>\<^sub>F x in at 0. x \<noteq> 0" by (auto simp: at_within_def eventually_inf_principal)

    51   show "(\<lambda>x::real. inverse (1 + x) / 1) \<midarrow>0\<rightarrow> 1"

    52     by (rule tendsto_eq_intros refl | simp)+

    53 qed auto

    54

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

    56

    57 definition raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool"

    58   where "raw_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"

    59

    60 text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close>

    61 definition has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)

    62   where "f has_prod p \<equiv> raw_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> raw_has_prod f (Suc i) q)"

    63

    64 definition convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where

    65   "convergent_prod f \<equiv> \<exists>M p. raw_has_prod f M p"

    66

    67 definition prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a"

    68     (binder "\<Prod>" 10)

    69   where "prodinf f = (THE p. f has_prod p)"

    70

    71 lemmas prod_defs = raw_has_prod_def has_prod_def convergent_prod_def prodinf_def

    72

    73 lemma has_prod_subst[trans]: "f = g \<Longrightarrow> g has_prod z \<Longrightarrow> f has_prod z"

    74   by simp

    75

    76 lemma has_prod_cong: "(\<And>n. f n = g n) \<Longrightarrow> f has_prod c \<longleftrightarrow> g has_prod c"

    77   by presburger

    78

    79 lemma raw_has_prod_nonzero [simp]: "\<not> raw_has_prod f M 0"

    80   by (simp add: raw_has_prod_def)

    81

    82 lemma raw_has_prod_eq_0:

    83   fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"

    84   assumes p: "raw_has_prod f m p" and i: "f i = 0" "i \<ge> m"

    85   shows "p = 0"

    86 proof -

    87   have eq0: "(\<Prod>k\<le>n. f (k+m)) = 0" if "i - m \<le> n" for n

    88   proof -

    89     have "\<exists>k\<le>n. f (k + m) = 0"

    90       using i that by auto

    91     then show ?thesis

    92       by auto

    93   qed

    94   have "(\<lambda>n. \<Prod>i\<le>n. f (i + m)) \<longlonglongrightarrow> 0"

    95     by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0)

    96     with p show ?thesis

    97       unfolding raw_has_prod_def

    98     using LIMSEQ_unique by blast

    99 qed

   100

   101 lemma raw_has_prod_Suc:

   102   "raw_has_prod f (Suc M) a \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a"

   103   unfolding raw_has_prod_def by auto

   104

   105 lemma has_prod_0_iff: "f has_prod 0 \<longleftrightarrow> (\<exists>i. f i = 0 \<and> (\<exists>p. raw_has_prod f (Suc i) p))"

   106   by (simp add: has_prod_def)

   107

   108 lemma has_prod_unique2:

   109   fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"

   110   assumes "f has_prod a" "f has_prod b" shows "a = b"

   111   using assms

   112   by (auto simp: has_prod_def raw_has_prod_eq_0) (meson raw_has_prod_def sequentially_bot tendsto_unique)

   113

   114 lemma has_prod_unique:

   115   fixes f :: "nat \<Rightarrow> 'a :: {semidom,t2_space}"

   116   shows "f has_prod s \<Longrightarrow> s = prodinf f"

   117   by (simp add: has_prod_unique2 prodinf_def the_equality)

   118

   119 lemma convergent_prod_altdef:

   120   fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}"

   121   shows "convergent_prod f \<longleftrightarrow> (\<exists>M L. (\<forall>n\<ge>M. f n \<noteq> 0) \<and> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L \<and> L \<noteq> 0)"

   122 proof

   123   assume "convergent_prod f"

   124   then obtain M L where *: "(\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L" "L \<noteq> 0"

   125     by (auto simp: prod_defs)

   126   have "f i \<noteq> 0" if "i \<ge> M" for i

   127   proof

   128     assume "f i = 0"

   129     have **: "eventually (\<lambda>n. (\<Prod>i\<le>n. f (i+M)) = 0) sequentially"

   130       using eventually_ge_at_top[of "i - M"]

   131     proof eventually_elim

   132       case (elim n)

   133       with \<open>f i = 0\<close> and \<open>i \<ge> M\<close> show ?case

   134         by (auto intro!: bexI[of _ "i - M"] prod_zero)

   135     qed

   136     have "(\<lambda>n. (\<Prod>i\<le>n. f (i+M))) \<longlonglongrightarrow> 0"

   137       unfolding filterlim_iff

   138       by (auto dest!: eventually_nhds_x_imp_x intro!: eventually_mono[OF **])

   139     from tendsto_unique[OF _ this *(1)] and *(2)

   140       show False by simp

   141   qed

   142   with * show "(\<exists>M L. (\<forall>n\<ge>M. f n \<noteq> 0) \<and> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L \<and> L \<noteq> 0)"

   143     by blast

   144 qed (auto simp: prod_defs)

   145

   146

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

   148

   149 definition abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where

   150   "abs_convergent_prod f \<longleftrightarrow> convergent_prod (\<lambda>i. 1 + norm (f i - 1))"

   151

   152 lemma abs_convergent_prodI:

   153   assumes "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))"

   154   shows   "abs_convergent_prod f"

   155 proof -

   156   from assms obtain L where L: "(\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1)) \<longlonglongrightarrow> L"

   157     by (auto simp: convergent_def)

   158   have "L \<ge> 1"

   159   proof (rule tendsto_le)

   160     show "eventually (\<lambda>n. (\<Prod>i\<le>n. 1 + norm (f i - 1)) \<ge> 1) sequentially"

   161     proof (intro always_eventually allI)

   162       fix n

   163       have "(\<Prod>i\<le>n. 1 + norm (f i - 1)) \<ge> (\<Prod>i\<le>n. 1)"

   164         by (intro prod_mono) auto

   165       thus "(\<Prod>i\<le>n. 1 + norm (f i - 1)) \<ge> 1" by simp

   166     qed

   167   qed (use L in simp_all)

   168   hence "L \<noteq> 0" by auto

   169   with L show ?thesis unfolding abs_convergent_prod_def prod_defs

   170     by (intro exI[of _ "0::nat"] exI[of _ L]) auto

   171 qed

   172

   173 lemma

   174   fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"

   175   assumes "convergent_prod f"

   176   shows   convergent_prod_imp_convergent: "convergent (\<lambda>n. \<Prod>i\<le>n. f i)"

   177     and   convergent_prod_to_zero_iff:    "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)"

   178 proof -

   179   from assms obtain M L

   180     where M: "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0" and "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> L" and "L \<noteq> 0"

   181     by (auto simp: convergent_prod_altdef)

   182   note this(2)

   183   also have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) = (\<lambda>n. \<Prod>i=M..M+n. f i)"

   184     by (intro ext prod.reindex_bij_witness[of _ "\<lambda>n. n - M" "\<lambda>n. n + M"]) auto

   185   finally have "(\<lambda>n. (\<Prod>i<M. f i) * (\<Prod>i=M..M+n. f i)) \<longlonglongrightarrow> (\<Prod>i<M. f i) * L"

   186     by (intro tendsto_mult tendsto_const)

   187   also have "(\<lambda>n. (\<Prod>i<M. f i) * (\<Prod>i=M..M+n. f i)) = (\<lambda>n. (\<Prod>i\<in>{..<M}\<union>{M..M+n}. f i))"

   188     by (subst prod.union_disjoint) auto

   189   also have "(\<lambda>n. {..<M} \<union> {M..M+n}) = (\<lambda>n. {..n+M})" by auto

   190   finally have lim: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * L"

   191     by (rule LIMSEQ_offset)

   192   thus "convergent (\<lambda>n. \<Prod>i\<le>n. f i)"

   193     by (auto simp: convergent_def)

   194

   195   show "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)"

   196   proof

   197     assume "\<exists>i. f i = 0"

   198     then obtain i where "f i = 0" by auto

   199     moreover with M have "i < M" by (cases "i < M") auto

   200     ultimately have "(\<Prod>i<M. f i) = 0" by auto

   201     with lim show "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0" by simp

   202   next

   203     assume "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0"

   204     from tendsto_unique[OF _ this lim] and \<open>L \<noteq> 0\<close>

   205     show "\<exists>i. f i = 0" by auto

   206   qed

   207 qed

   208

   209 lemma convergent_prod_iff_nz_lim:

   210   fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"

   211   assumes "\<And>i. f i \<noteq> 0"

   212   shows "convergent_prod f \<longleftrightarrow> (\<exists>L. (\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> L \<and> L \<noteq> 0)"

   213     (is "?lhs \<longleftrightarrow> ?rhs")

   214 proof

   215   assume ?lhs then show ?rhs

   216     using assms convergentD convergent_prod_imp_convergent convergent_prod_to_zero_iff by blast

   217 next

   218   assume ?rhs then show ?lhs

   219     unfolding prod_defs

   220     by (rule_tac x=0 in exI) auto

   221 qed

   222

   223 lemma convergent_prod_iff_convergent:

   224   fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"

   225   assumes "\<And>i. f i \<noteq> 0"

   226   shows "convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. f i) \<and> lim (\<lambda>n. \<Prod>i\<le>n. f i) \<noteq> 0"

   227   by (force simp: convergent_prod_iff_nz_lim assms convergent_def limI)

   228

   229 lemma bounded_imp_convergent_prod:

   230   fixes a :: "nat \<Rightarrow> real"

   231   assumes 1: "\<And>n. a n \<ge> 1" and bounded: "\<And>n. (\<Prod>i\<le>n. a i) \<le> B"

   232   shows "convergent_prod a"

   233 proof -

   234   have "bdd_above (range(\<lambda>n. \<Prod>i\<le>n. a i))"

   235     by (meson bdd_aboveI2 bounded)

   236   moreover have "incseq (\<lambda>n. \<Prod>i\<le>n. a i)"

   237     unfolding mono_def by (metis 1 prod_mono2 atMost_subset_iff dual_order.trans finite_atMost zero_le_one)

   238   ultimately obtain p where p: "(\<lambda>n. \<Prod>i\<le>n. a i) \<longlonglongrightarrow> p"

   239     using LIMSEQ_incseq_SUP by blast

   240   then have "p \<noteq> 0"

   241     by (metis "1" not_one_le_zero prod_ge_1 LIMSEQ_le_const)

   242   with 1 p show ?thesis

   243     by (metis convergent_prod_iff_nz_lim not_one_le_zero)

   244 qed

   245

   246

   247 lemma abs_convergent_prod_altdef:

   248   fixes f :: "nat \<Rightarrow> 'a :: {one,real_normed_vector}"

   249   shows  "abs_convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))"

   250 proof

   251   assume "abs_convergent_prod f"

   252   thus "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))"

   253     by (auto simp: abs_convergent_prod_def intro!: convergent_prod_imp_convergent)

   254 qed (auto intro: abs_convergent_prodI)

   255

   256 lemma weierstrass_prod_ineq:

   257   fixes f :: "'a \<Rightarrow> real"

   258   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> {0..1}"

   259   shows   "1 - sum f A \<le> (\<Prod>x\<in>A. 1 - f x)"

   260   using assms

   261 proof (induction A rule: infinite_finite_induct)

   262   case (insert x A)

   263   from insert.hyps and insert.prems

   264     have "1 - sum f A + f x * (\<Prod>x\<in>A. 1 - f x) \<le> (\<Prod>x\<in>A. 1 - f x) + f x * (\<Prod>x\<in>A. 1)"

   265     by (intro insert.IH add_mono mult_left_mono prod_mono) auto

   266   with insert.hyps show ?case by (simp add: algebra_simps)

   267 qed simp_all

   268

   269 lemma norm_prod_minus1_le_prod_minus1:

   270   fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,comm_ring_1}"

   271   shows "norm (prod (\<lambda>n. 1 + f n) A - 1) \<le> prod (\<lambda>n. 1 + norm (f n)) A - 1"

   272 proof (induction A rule: infinite_finite_induct)

   273   case (insert x A)

   274   from insert.hyps have

   275     "norm ((\<Prod>n\<in>insert x A. 1 + f n) - 1) =

   276        norm ((\<Prod>n\<in>A. 1 + f n) - 1 + f x * (\<Prod>n\<in>A. 1 + f n))"

   277     by (simp add: algebra_simps)

   278   also have "\<dots> \<le> norm ((\<Prod>n\<in>A. 1 + f n) - 1) + norm (f x * (\<Prod>n\<in>A. 1 + f n))"

   279     by (rule norm_triangle_ineq)

   280   also have "norm (f x * (\<Prod>n\<in>A. 1 + f n)) = norm (f x) * (\<Prod>x\<in>A. norm (1 + f x))"

   281     by (simp add: prod_norm norm_mult)

   282   also have "(\<Prod>x\<in>A. norm (1 + f x)) \<le> (\<Prod>x\<in>A. norm (1::'a) + norm (f x))"

   283     by (intro prod_mono norm_triangle_ineq ballI conjI) auto

   284   also have "norm (1::'a) = 1" by simp

   285   also note insert.IH

   286   also have "(\<Prod>n\<in>A. 1 + norm (f n)) - 1 + norm (f x) * (\<Prod>x\<in>A. 1 + norm (f x)) =

   287              (\<Prod>n\<in>insert x A. 1 + norm (f n)) - 1"

   288     using insert.hyps by (simp add: algebra_simps)

   289   finally show ?case by - (simp_all add: mult_left_mono)

   290 qed simp_all

   291

   292 lemma convergent_prod_imp_ev_nonzero:

   293   fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}"

   294   assumes "convergent_prod f"

   295   shows   "eventually (\<lambda>n. f n \<noteq> 0) sequentially"

   296   using assms by (auto simp: eventually_at_top_linorder convergent_prod_altdef)

   297

   298 lemma convergent_prod_imp_LIMSEQ:

   299   fixes f :: "nat \<Rightarrow> 'a :: {real_normed_field}"

   300   assumes "convergent_prod f"

   301   shows   "f \<longlonglongrightarrow> 1"

   302 proof -

   303   from assms obtain M L where L: "(\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L" "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0" "L \<noteq> 0"

   304     by (auto simp: convergent_prod_altdef)

   305   hence L': "(\<lambda>n. \<Prod>i\<le>Suc n. f (i+M)) \<longlonglongrightarrow> L" by (subst filterlim_sequentially_Suc)

   306   have "(\<lambda>n. (\<Prod>i\<le>Suc n. f (i+M)) / (\<Prod>i\<le>n. f (i+M))) \<longlonglongrightarrow> L / L"

   307     using L L' by (intro tendsto_divide) simp_all

   308   also from L have "L / L = 1" by simp

   309   also have "(\<lambda>n. (\<Prod>i\<le>Suc n. f (i+M)) / (\<Prod>i\<le>n. f (i+M))) = (\<lambda>n. f (n + Suc M))"

   310     using assms L by (auto simp: fun_eq_iff atMost_Suc)

   311   finally show ?thesis by (rule LIMSEQ_offset)

   312 qed

   313

   314 lemma abs_convergent_prod_imp_summable:

   315   fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra"

   316   assumes "abs_convergent_prod f"

   317   shows "summable (\<lambda>i. norm (f i - 1))"

   318 proof -

   319   from assms have "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))"

   320     unfolding abs_convergent_prod_def by (rule convergent_prod_imp_convergent)

   321   then obtain L where L: "(\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1)) \<longlonglongrightarrow> L"

   322     unfolding convergent_def by blast

   323   have "convergent (\<lambda>n. \<Sum>i\<le>n. norm (f i - 1))"

   324   proof (rule Bseq_monoseq_convergent)

   325     have "eventually (\<lambda>n. (\<Prod>i\<le>n. 1 + norm (f i - 1)) < L + 1) sequentially"

   326       using L(1) by (rule order_tendstoD) simp_all

   327     hence "\<forall>\<^sub>F x in sequentially. norm (\<Sum>i\<le>x. norm (f i - 1)) \<le> L + 1"

   328     proof eventually_elim

   329       case (elim n)

   330       have "norm (\<Sum>i\<le>n. norm (f i - 1)) = (\<Sum>i\<le>n. norm (f i - 1))"

   331         unfolding real_norm_def by (intro abs_of_nonneg sum_nonneg) simp_all

   332       also have "\<dots> \<le> (\<Prod>i\<le>n. 1 + norm (f i - 1))" by (rule sum_le_prod) auto

   333       also have "\<dots> < L + 1" by (rule elim)

   334       finally show ?case by simp

   335     qed

   336     thus "Bseq (\<lambda>n. \<Sum>i\<le>n. norm (f i - 1))" by (rule BfunI)

   337   next

   338     show "monoseq (\<lambda>n. \<Sum>i\<le>n. norm (f i - 1))"

   339       by (rule mono_SucI1) auto

   340   qed

   341   thus "summable (\<lambda>i. norm (f i - 1))" by (simp add: summable_iff_convergent')

   342 qed

   343

   344 lemma summable_imp_abs_convergent_prod:

   345   fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra"

   346   assumes "summable (\<lambda>i. norm (f i - 1))"

   347   shows   "abs_convergent_prod f"

   348 proof (intro abs_convergent_prodI Bseq_monoseq_convergent)

   349   show "monoseq (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))"

   350     by (intro mono_SucI1)

   351        (auto simp: atMost_Suc algebra_simps intro!: mult_nonneg_nonneg prod_nonneg)

   352 next

   353   show "Bseq (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))"

   354   proof (rule Bseq_eventually_mono)

   355     show "eventually (\<lambda>n. norm (\<Prod>i\<le>n. 1 + norm (f i - 1)) \<le>

   356             norm (exp (\<Sum>i\<le>n. norm (f i - 1)))) sequentially"

   357       by (intro always_eventually allI) (auto simp: abs_prod exp_sum intro!: prod_mono)

   358   next

   359     from assms have "(\<lambda>n. \<Sum>i\<le>n. norm (f i - 1)) \<longlonglongrightarrow> (\<Sum>i. norm (f i - 1))"

   360       using sums_def_le by blast

   361     hence "(\<lambda>n. exp (\<Sum>i\<le>n. norm (f i - 1))) \<longlonglongrightarrow> exp (\<Sum>i. norm (f i - 1))"

   362       by (rule tendsto_exp)

   363     hence "convergent (\<lambda>n. exp (\<Sum>i\<le>n. norm (f i - 1)))"

   364       by (rule convergentI)

   365     thus "Bseq (\<lambda>n. exp (\<Sum>i\<le>n. norm (f i - 1)))"

   366       by (rule convergent_imp_Bseq)

   367   qed

   368 qed

   369

   370 lemma abs_convergent_prod_conv_summable:

   371   fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra"

   372   shows "abs_convergent_prod f \<longleftrightarrow> summable (\<lambda>i. norm (f i - 1))"

   373   by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod)

   374

   375 lemma abs_convergent_prod_imp_LIMSEQ:

   376   fixes f :: "nat \<Rightarrow> 'a :: {comm_ring_1,real_normed_div_algebra}"

   377   assumes "abs_convergent_prod f"

   378   shows   "f \<longlonglongrightarrow> 1"

   379 proof -

   380   from assms have "summable (\<lambda>n. norm (f n - 1))"

   381     by (rule abs_convergent_prod_imp_summable)

   382   from summable_LIMSEQ_zero[OF this] have "(\<lambda>n. f n - 1) \<longlonglongrightarrow> 0"

   383     by (simp add: tendsto_norm_zero_iff)

   384   from tendsto_add[OF this tendsto_const[of 1]] show ?thesis by simp

   385 qed

   386

   387 lemma abs_convergent_prod_imp_ev_nonzero:

   388   fixes f :: "nat \<Rightarrow> 'a :: {comm_ring_1,real_normed_div_algebra}"

   389   assumes "abs_convergent_prod f"

   390   shows   "eventually (\<lambda>n. f n \<noteq> 0) sequentially"

   391 proof -

   392   from assms have "f \<longlonglongrightarrow> 1"

   393     by (rule abs_convergent_prod_imp_LIMSEQ)

   394   hence "eventually (\<lambda>n. dist (f n) 1 < 1) at_top"

   395     by (auto simp: tendsto_iff)

   396   thus ?thesis by eventually_elim auto

   397 qed

   398

   399 lemma convergent_prod_offset:

   400   assumes "convergent_prod (\<lambda>n. f (n + m))"

   401   shows   "convergent_prod f"

   402 proof -

   403   from assms obtain M L where "(\<lambda>n. \<Prod>k\<le>n. f (k + (M + m))) \<longlonglongrightarrow> L" "L \<noteq> 0"

   404     by (auto simp: prod_defs add.assoc)

   405   thus "convergent_prod f"

   406     unfolding prod_defs by blast

   407 qed

   408

   409 lemma abs_convergent_prod_offset:

   410   assumes "abs_convergent_prod (\<lambda>n. f (n + m))"

   411   shows   "abs_convergent_prod f"

   412   using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset)

   413

   414 subsection\<open>Ignoring initial segments\<close>

   415

   416 lemma raw_has_prod_ignore_initial_segment:

   417   fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"

   418   assumes "raw_has_prod f M p" "N \<ge> M"

   419   obtains q where  "raw_has_prod f N q"

   420 proof -

   421   have p: "(\<lambda>n. \<Prod>k\<le>n. f (k + M)) \<longlonglongrightarrow> p" and "p \<noteq> 0"

   422     using assms by (auto simp: raw_has_prod_def)

   423   then have nz: "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0"

   424     using assms by (auto simp: raw_has_prod_eq_0)

   425   define C where "C = (\<Prod>k<N-M. f (k + M))"

   426   from nz have [simp]: "C \<noteq> 0"

   427     by (auto simp: C_def)

   428

   429   from p have "(\<lambda>i. \<Prod>k\<le>i + (N-M). f (k + M)) \<longlonglongrightarrow> p"

   430     by (rule LIMSEQ_ignore_initial_segment)

   431   also have "(\<lambda>i. \<Prod>k\<le>i + (N-M). f (k + M)) = (\<lambda>n. C * (\<Prod>k\<le>n. f (k + N)))"

   432   proof (rule ext, goal_cases)

   433     case (1 n)

   434     have "{..n+(N-M)} = {..<(N-M)} \<union> {(N-M)..n+(N-M)}" by auto

   435     also have "(\<Prod>k\<in>\<dots>. f (k + M)) = C * (\<Prod>k=(N-M)..n+(N-M). f (k + M))"

   436       unfolding C_def by (rule prod.union_disjoint) auto

   437     also have "(\<Prod>k=(N-M)..n+(N-M). f (k + M)) = (\<Prod>k\<le>n. f (k + (N-M) + M))"

   438       by (intro ext prod.reindex_bij_witness[of _ "\<lambda>k. k + (N-M)" "\<lambda>k. k - (N-M)"]) auto

   439     finally show ?case

   440       using \<open>N \<ge> M\<close> by (simp add: add_ac)

   441   qed

   442   finally have "(\<lambda>n. C * (\<Prod>k\<le>n. f (k + N)) / C) \<longlonglongrightarrow> p / C"

   443     by (intro tendsto_divide tendsto_const) auto

   444   hence "(\<lambda>n. \<Prod>k\<le>n. f (k + N)) \<longlonglongrightarrow> p / C" by simp

   445   moreover from \<open>p \<noteq> 0\<close> have "p / C \<noteq> 0" by simp

   446   ultimately show ?thesis

   447     using raw_has_prod_def that by blast

   448 qed

   449

   450 corollary convergent_prod_ignore_initial_segment:

   451   fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"

   452   assumes "convergent_prod f"

   453   shows   "convergent_prod (\<lambda>n. f (n + m))"

   454   using assms

   455   unfolding convergent_prod_def

   456   apply clarify

   457   apply (erule_tac N="M+m" in raw_has_prod_ignore_initial_segment)

   458   apply (auto simp add: raw_has_prod_def add_ac)

   459   done

   460

   461 corollary convergent_prod_ignore_nonzero_segment:

   462   fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"

   463   assumes f: "convergent_prod f" and nz: "\<And>i. i \<ge> M \<Longrightarrow> f i \<noteq> 0"

   464   shows "\<exists>p. raw_has_prod f M p"

   465   using convergent_prod_ignore_initial_segment [OF f]

   466   by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1))

   467

   468 corollary abs_convergent_prod_ignore_initial_segment:

   469   assumes "abs_convergent_prod f"

   470   shows   "abs_convergent_prod (\<lambda>n. f (n + m))"

   471   using assms unfolding abs_convergent_prod_def

   472   by (rule convergent_prod_ignore_initial_segment)

   473

   474 lemma abs_convergent_prod_imp_convergent_prod:

   475   fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}"

   476   assumes "abs_convergent_prod f"

   477   shows   "convergent_prod f"

   478 proof -

   479   from assms have "eventually (\<lambda>n. f n \<noteq> 0) sequentially"

   480     by (rule abs_convergent_prod_imp_ev_nonzero)

   481   then obtain N where N: "f n \<noteq> 0" if "n \<ge> N" for n

   482     by (auto simp: eventually_at_top_linorder)

   483   let ?P = "\<lambda>n. \<Prod>i\<le>n. f (i + N)" and ?Q = "\<lambda>n. \<Prod>i\<le>n. 1 + norm (f (i + N) - 1)"

   484

   485   have "Cauchy ?P"

   486   proof (rule CauchyI', goal_cases)

   487     case (1 \<epsilon>)

   488     from assms have "abs_convergent_prod (\<lambda>n. f (n + N))"

   489       by (rule abs_convergent_prod_ignore_initial_segment)

   490     hence "Cauchy ?Q"

   491       unfolding abs_convergent_prod_def

   492       by (intro convergent_Cauchy convergent_prod_imp_convergent)

   493     from CauchyD[OF this 1] obtain M where M: "norm (?Q m - ?Q n) < \<epsilon>" if "m \<ge> M" "n \<ge> M" for m n

   494       by blast

   495     show ?case

   496     proof (rule exI[of _ M], safe, goal_cases)

   497       case (1 m n)

   498       have "dist (?P m) (?P n) = norm (?P n - ?P m)"

   499         by (simp add: dist_norm norm_minus_commute)

   500       also from 1 have "{..n} = {..m} \<union> {m<..n}" by auto

   501       hence "norm (?P n - ?P m) = norm (?P m * (\<Prod>k\<in>{m<..n}. f (k + N)) - ?P m)"

   502         by (subst prod.union_disjoint [symmetric]) (auto simp: algebra_simps)

   503       also have "\<dots> = norm (?P m * ((\<Prod>k\<in>{m<..n}. f (k + N)) - 1))"

   504         by (simp add: algebra_simps)

   505       also have "\<dots> = (\<Prod>k\<le>m. norm (f (k + N))) * norm ((\<Prod>k\<in>{m<..n}. f (k + N)) - 1)"

   506         by (simp add: norm_mult prod_norm)

   507       also have "\<dots> \<le> ?Q m * ((\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N) - 1)) - 1)"

   508         using norm_prod_minus1_le_prod_minus1[of "\<lambda>k. f (k + N) - 1" "{m<..n}"]

   509               norm_triangle_ineq[of 1 "f k - 1" for k]

   510         by (intro mult_mono prod_mono ballI conjI norm_prod_minus1_le_prod_minus1 prod_nonneg) auto

   511       also have "\<dots> = ?Q m * (\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N) - 1)) - ?Q m"

   512         by (simp add: algebra_simps)

   513       also have "?Q m * (\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N) - 1)) =

   514                    (\<Prod>k\<in>{..m}\<union>{m<..n}. 1 + norm (f (k + N) - 1))"

   515         by (rule prod.union_disjoint [symmetric]) auto

   516       also from 1 have "{..m}\<union>{m<..n} = {..n}" by auto

   517       also have "?Q n - ?Q m \<le> norm (?Q n - ?Q m)" by simp

   518       also from 1 have "\<dots> < \<epsilon>" by (intro M) auto

   519       finally show ?case .

   520     qed

   521   qed

   522   hence conv: "convergent ?P" by (rule Cauchy_convergent)

   523   then obtain L where L: "?P \<longlonglongrightarrow> L"

   524     by (auto simp: convergent_def)

   525

   526   have "L \<noteq> 0"

   527   proof

   528     assume [simp]: "L = 0"

   529     from tendsto_norm[OF L] have limit: "(\<lambda>n. \<Prod>k\<le>n. norm (f (k + N))) \<longlonglongrightarrow> 0"

   530       by (simp add: prod_norm)

   531

   532     from assms have "(\<lambda>n. f (n + N)) \<longlonglongrightarrow> 1"

   533       by (intro abs_convergent_prod_imp_LIMSEQ abs_convergent_prod_ignore_initial_segment)

   534     hence "eventually (\<lambda>n. norm (f (n + N) - 1) < 1) sequentially"

   535       by (auto simp: tendsto_iff dist_norm)

   536     then obtain M0 where M0: "norm (f (n + N) - 1) < 1" if "n \<ge> M0" for n

   537       by (auto simp: eventually_at_top_linorder)

   538

   539     {

   540       fix M assume M: "M \<ge> M0"

   541       with M0 have M: "norm (f (n + N) - 1) < 1" if "n \<ge> M" for n using that by simp

   542

   543       have "(\<lambda>n. \<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<longlonglongrightarrow> 0"

   544       proof (rule tendsto_sandwich)

   545         show "eventually (\<lambda>n. (\<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<ge> 0) sequentially"

   546           using M by (intro always_eventually prod_nonneg allI ballI) (auto intro: less_imp_le)

   547         have "norm (1::'a) - norm (f (i + M + N) - 1) \<le> norm (f (i + M + N))" for i

   548           using norm_triangle_ineq3[of "f (i + M + N)" 1] by simp

   549         thus "eventually (\<lambda>n. (\<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<le> (\<Prod>k\<le>n. norm (f (k+M+N)))) at_top"

   550           using M by (intro always_eventually allI prod_mono ballI conjI) (auto intro: less_imp_le)

   551

   552         define C where "C = (\<Prod>k<M. norm (f (k + N)))"

   553         from N have [simp]: "C \<noteq> 0" by (auto simp: C_def)

   554         from L have "(\<lambda>n. norm (\<Prod>k\<le>n+M. f (k + N))) \<longlonglongrightarrow> 0"

   555           by (intro LIMSEQ_ignore_initial_segment) (simp add: tendsto_norm_zero_iff)

   556         also have "(\<lambda>n. norm (\<Prod>k\<le>n+M. f (k + N))) = (\<lambda>n. C * (\<Prod>k\<le>n. norm (f (k + M + N))))"

   557         proof (rule ext, goal_cases)

   558           case (1 n)

   559           have "{..n+M} = {..<M} \<union> {M..n+M}" by auto

   560           also have "norm (\<Prod>k\<in>\<dots>. f (k + N)) = C * norm (\<Prod>k=M..n+M. f (k + N))"

   561             unfolding C_def by (subst prod.union_disjoint) (auto simp: norm_mult prod_norm)

   562           also have "(\<Prod>k=M..n+M. f (k + N)) = (\<Prod>k\<le>n. f (k + N + M))"

   563             by (intro prod.reindex_bij_witness[of _ "\<lambda>i. i + M" "\<lambda>i. i - M"]) auto

   564           finally show ?case by (simp add: add_ac prod_norm)

   565         qed

   566         finally have "(\<lambda>n. C * (\<Prod>k\<le>n. norm (f (k + M + N))) / C) \<longlonglongrightarrow> 0 / C"

   567           by (intro tendsto_divide tendsto_const) auto

   568         thus "(\<lambda>n. \<Prod>k\<le>n. norm (f (k + M + N))) \<longlonglongrightarrow> 0" by simp

   569       qed simp_all

   570

   571       have "1 - (\<Sum>i. norm (f (i + M + N) - 1)) \<le> 0"

   572       proof (rule tendsto_le)

   573         show "eventually (\<lambda>n. 1 - (\<Sum>k\<le>n. norm (f (k+M+N) - 1)) \<le>

   574                                 (\<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1))) at_top"

   575           using M by (intro always_eventually allI weierstrass_prod_ineq) (auto intro: less_imp_le)

   576         show "(\<lambda>n. \<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<longlonglongrightarrow> 0" by fact

   577         show "(\<lambda>n. 1 - (\<Sum>k\<le>n. norm (f (k + M + N) - 1)))

   578                   \<longlonglongrightarrow> 1 - (\<Sum>i. norm (f (i + M + N) - 1))"

   579           by (intro tendsto_intros summable_LIMSEQ' summable_ignore_initial_segment

   580                 abs_convergent_prod_imp_summable assms)

   581       qed simp_all

   582       hence "(\<Sum>i. norm (f (i + M + N) - 1)) \<ge> 1" by simp

   583       also have "\<dots> + (\<Sum>i<M. norm (f (i + N) - 1)) = (\<Sum>i. norm (f (i + N) - 1))"

   584         by (intro suminf_split_initial_segment [symmetric] summable_ignore_initial_segment

   585               abs_convergent_prod_imp_summable assms)

   586       finally have "1 + (\<Sum>i<M. norm (f (i + N) - 1)) \<le> (\<Sum>i. norm (f (i + N) - 1))" by simp

   587     } note * = this

   588

   589     have "1 + (\<Sum>i. norm (f (i + N) - 1)) \<le> (\<Sum>i. norm (f (i + N) - 1))"

   590     proof (rule tendsto_le)

   591       show "(\<lambda>M. 1 + (\<Sum>i<M. norm (f (i + N) - 1))) \<longlonglongrightarrow> 1 + (\<Sum>i. norm (f (i + N) - 1))"

   592         by (intro tendsto_intros summable_LIMSEQ summable_ignore_initial_segment

   593                 abs_convergent_prod_imp_summable assms)

   594       show "eventually (\<lambda>M. 1 + (\<Sum>i<M. norm (f (i + N) - 1)) \<le> (\<Sum>i. norm (f (i + N) - 1))) at_top"

   595         using eventually_ge_at_top[of M0] by eventually_elim (use * in auto)

   596     qed simp_all

   597     thus False by simp

   598   qed

   599   with L show ?thesis by (auto simp: prod_defs)

   600 qed

   601

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

   603

   604 lemma raw_has_prod_cases:

   605   fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"

   606   assumes "raw_has_prod f M p"

   607   obtains i where "i<M" "f i = 0" | p where "raw_has_prod f 0 p"

   608 proof -

   609   have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0"

   610     using assms unfolding raw_has_prod_def by blast+

   611   then have "(\<lambda>n. prod f {..<M} * (\<Prod>i\<le>n. f (i + M))) \<longlonglongrightarrow> prod f {..<M} * p"

   612     by (metis tendsto_mult_left)

   613   moreover have "prod f {..<M} * (\<Prod>i\<le>n. f (i + M)) = prod f {..n+M}" for n

   614   proof -

   615     have "{..n+M} = {..<M} \<union> {M..n+M}"

   616       by auto

   617     then have "prod f {..n+M} = prod f {..<M} * prod f {M..n+M}"

   618       by simp (subst prod.union_disjoint; force)

   619     also have "\<dots> = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"

   620       by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod_shift_bounds_cl_nat_ivl)

   621     finally show ?thesis by metis

   622   qed

   623   ultimately have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * p"

   624     by (auto intro: LIMSEQ_offset [where k=M])

   625   then have "raw_has_prod f 0 (prod f {..<M} * p)" if "\<forall>i<M. f i \<noteq> 0"

   626     using \<open>p \<noteq> 0\<close> assms that by (auto simp: raw_has_prod_def)

   627   then show thesis

   628     using that by blast

   629 qed

   630

   631 corollary convergent_prod_offset_0:

   632   fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"

   633   assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"

   634   shows "\<exists>p. raw_has_prod f 0 p"

   635   using assms convergent_prod_def raw_has_prod_cases by blast

   636

   637 lemma prodinf_eq_lim:

   638   fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"

   639   assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"

   640   shows "prodinf f = lim (\<lambda>n. \<Prod>i\<le>n. f i)"

   641   using assms convergent_prod_offset_0 [OF assms]

   642   by (simp add: prod_defs lim_def) (metis (no_types) assms(1) convergent_prod_to_zero_iff)

   643

   644 lemma has_prod_one[simp, intro]: "(\<lambda>n. 1) has_prod 1"

   645   unfolding prod_defs by auto

   646

   647 lemma convergent_prod_one[simp, intro]: "convergent_prod (\<lambda>n. 1)"

   648   unfolding prod_defs by auto

   649

   650 lemma prodinf_cong: "(\<And>n. f n = g n) \<Longrightarrow> prodinf f = prodinf g"

   651   by presburger

   652

   653 lemma convergent_prod_cong:

   654   fixes f g :: "nat \<Rightarrow> 'a::{field,topological_semigroup_mult,t2_space}"

   655   assumes ev: "eventually (\<lambda>x. f x = g x) sequentially" and f: "\<And>i. f i \<noteq> 0" and g: "\<And>i. g i \<noteq> 0"

   656   shows "convergent_prod f = convergent_prod g"

   657 proof -

   658   from assms obtain N where N: "\<forall>n\<ge>N. f n = g n"

   659     by (auto simp: eventually_at_top_linorder)

   660   define C where "C = (\<Prod>k<N. f k / g k)"

   661   with g have "C \<noteq> 0"

   662     by (simp add: f)

   663   have *: "eventually (\<lambda>n. prod f {..n} = C * prod g {..n}) sequentially"

   664     using eventually_ge_at_top[of N]

   665   proof eventually_elim

   666     case (elim n)

   667     then have "{..n} = {..<N} \<union> {N..n}"

   668       by auto

   669     also have "prod f \<dots> = prod f {..<N} * prod f {N..n}"

   670       by (intro prod.union_disjoint) auto

   671     also from N have "prod f {N..n} = prod g {N..n}"

   672       by (intro prod.cong) simp_all

   673     also have "prod f {..<N} * prod g {N..n} = C * (prod g {..<N} * prod g {N..n})"

   674       unfolding C_def by (simp add: g prod_dividef)

   675     also have "prod g {..<N} * prod g {N..n} = prod g ({..<N} \<union> {N..n})"

   676       by (intro prod.union_disjoint [symmetric]) auto

   677     also from elim have "{..<N} \<union> {N..n} = {..n}"

   678       by auto

   679     finally show "prod f {..n} = C * prod g {..n}" .

   680   qed

   681   then have cong: "convergent (\<lambda>n. prod f {..n}) = convergent (\<lambda>n. C * prod g {..n})"

   682     by (rule convergent_cong)

   683   show ?thesis

   684   proof

   685     assume cf: "convergent_prod f"

   686     then have "\<not> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> 0"

   687       using tendsto_mult_left * convergent_prod_to_zero_iff f filterlim_cong by fastforce

   688     then show "convergent_prod g"

   689       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)

   690   next

   691     assume cg: "convergent_prod g"

   692     have "\<exists>a. C * a \<noteq> 0 \<and> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> a"

   693       by (metis (no_types) \<open>C \<noteq> 0\<close> cg convergent_prod_iff_nz_lim divide_eq_0_iff g nonzero_mult_div_cancel_right)

   694     then show "convergent_prod f"

   695       using "*" tendsto_mult_left filterlim_cong

   696       by (fastforce simp add: convergent_prod_iff_nz_lim f)

   697   qed

   698 qed

   699

   700 lemma has_prod_finite:

   701   fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"

   702   assumes [simp]: "finite N"

   703     and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"

   704   shows "f has_prod (\<Prod>n\<in>N. f n)"

   705 proof -

   706   have eq: "prod f {..n + Suc (Max N)} = prod f N" for n

   707   proof (rule prod.mono_neutral_right)

   708     show "N \<subseteq> {..n + Suc (Max N)}"

   709       by (auto simp: le_Suc_eq trans_le_add2)

   710     show "\<forall>i\<in>{..n + Suc (Max N)} - N. f i = 1"

   711       using f by blast

   712   qed auto

   713   show ?thesis

   714   proof (cases "\<forall>n\<in>N. f n \<noteq> 0")

   715     case True

   716     then have "prod f N \<noteq> 0"

   717       by simp

   718     moreover have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f N"

   719       by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) (simp add: eq atLeast0LessThan del: add_Suc_right)

   720     ultimately show ?thesis

   721       by (simp add: raw_has_prod_def has_prod_def)

   722   next

   723     case False

   724     then obtain k where "k \<in> N" "f k = 0"

   725       by auto

   726     let ?Z = "{n \<in> N. f n = 0}"

   727     have maxge: "Max ?Z \<ge> n" if "f n = 0" for n

   728       using Max_ge [of ?Z] \<open>finite N\<close> \<open>f n = 0\<close>

   729       by (metis (mono_tags) Collect_mem_eq f finite_Collect_conjI mem_Collect_eq zero_neq_one)

   730     let ?q = "prod f {Suc (Max ?Z)..Max N}"

   731     have [simp]: "?q \<noteq> 0"

   732       using maxge Suc_n_not_le_n le_trans by force

   733     have eq: "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = ?q" for n

   734     proof -

   735       have "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = prod f {Suc (Max ?Z)..n + Max N + Suc (Max ?Z)}"

   736       proof (rule prod.reindex_cong [where l = "\<lambda>i. i + Suc (Max ?Z)", THEN sym])

   737         show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\<lambda>i. i + Suc (Max ?Z))  {..n + Max N}"

   738           using le_Suc_ex by fastforce

   739       qed (auto simp: inj_on_def)

   740       also have "\<dots> = ?q"

   741         by (rule prod.mono_neutral_right)

   742            (use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>)

   743       finally show ?thesis .

   744     qed

   745     have q: "raw_has_prod f (Suc (Max ?Z)) ?q"

   746     proof (simp add: raw_has_prod_def)

   747       show "(\<lambda>n. \<Prod>i\<le>n. f (Suc (i + Max ?Z))) \<longlonglongrightarrow> ?q"

   748         by (rule LIMSEQ_offset[of _ "(Max N)"]) (simp add: eq)

   749     qed

   750     show ?thesis

   751       unfolding has_prod_def

   752     proof (intro disjI2 exI conjI)

   753       show "prod f N = 0"

   754         using \<open>f k = 0\<close> \<open>k \<in> N\<close> \<open>finite N\<close> prod_zero by blast

   755       show "f (Max ?Z) = 0"

   756         using Max_in [of ?Z] \<open>finite N\<close> \<open>f k = 0\<close> \<open>k \<in> N\<close> by auto

   757     qed (use q in auto)

   758   qed

   759 qed

   760

   761 corollary has_prod_0:

   762   fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"

   763   assumes "\<And>n. f n = 1"

   764   shows "f has_prod 1"

   765   by (simp add: assms has_prod_cong)

   766

   767 lemma prodinf_zero[simp]: "prodinf (\<lambda>n. 1::'a::real_normed_field) = 1"

   768   using has_prod_unique by force

   769

   770 lemma convergent_prod_finite:

   771   fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"

   772   assumes "finite N" "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"

   773   shows "convergent_prod f"

   774 proof -

   775   have "\<exists>n p. raw_has_prod f n p"

   776     using assms has_prod_def has_prod_finite by blast

   777   then show ?thesis

   778     by (simp add: convergent_prod_def)

   779 qed

   780

   781 lemma has_prod_If_finite_set:

   782   fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"

   783   shows "finite A \<Longrightarrow> (\<lambda>r. if r \<in> A then f r else 1) has_prod (\<Prod>r\<in>A. f r)"

   784   using has_prod_finite[of A "(\<lambda>r. if r \<in> A then f r else 1)"]

   785   by simp

   786

   787 lemma has_prod_If_finite:

   788   fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"

   789   shows "finite {r. P r} \<Longrightarrow> (\<lambda>r. if P r then f r else 1) has_prod (\<Prod>r | P r. f r)"

   790   using has_prod_If_finite_set[of "{r. P r}"] by simp

   791

   792 lemma convergent_prod_If_finite_set[simp, intro]:

   793   fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"

   794   shows "finite A \<Longrightarrow> convergent_prod (\<lambda>r. if r \<in> A then f r else 1)"

   795   by (simp add: convergent_prod_finite)

   796

   797 lemma convergent_prod_If_finite[simp, intro]:

   798   fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"

   799   shows "finite {r. P r} \<Longrightarrow> convergent_prod (\<lambda>r. if P r then f r else 1)"

   800   using convergent_prod_def has_prod_If_finite has_prod_def by fastforce

   801

   802 lemma has_prod_single:

   803   fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"

   804   shows "(\<lambda>r. if r = i then f r else 1) has_prod f i"

   805   using has_prod_If_finite[of "\<lambda>r. r = i"] by simp

   806

   807 context

   808   fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"

   809 begin

   810

   811 lemma convergent_prod_imp_has_prod:

   812   assumes "convergent_prod f"

   813   shows "\<exists>p. f has_prod p"

   814 proof -

   815   obtain M p where p: "raw_has_prod f M p"

   816     using assms convergent_prod_def by blast

   817   then have "p \<noteq> 0"

   818     using raw_has_prod_nonzero by blast

   819   with p have fnz: "f i \<noteq> 0" if "i \<ge> M" for i

   820     using raw_has_prod_eq_0 that by blast

   821   define C where "C = (\<Prod>n<M. f n)"

   822   show ?thesis

   823   proof (cases "\<forall>n\<le>M. f n \<noteq> 0")

   824     case True

   825     then have "C \<noteq> 0"

   826       by (simp add: C_def)

   827     then show ?thesis

   828       by (meson True assms convergent_prod_offset_0 fnz has_prod_def nat_le_linear)

   829   next

   830     case False

   831     let ?N = "GREATEST n. f n = 0"

   832     have 0: "f ?N = 0"

   833       using fnz False

   834       by (metis (mono_tags, lifting) GreatestI_ex_nat nat_le_linear)

   835     have "f i \<noteq> 0" if "i > ?N" for i

   836       by (metis (mono_tags, lifting) Greatest_le_nat fnz leD linear that)

   837     then have "\<exists>p. raw_has_prod f (Suc ?N) p"

   838       using assms by (auto simp: intro!: convergent_prod_ignore_nonzero_segment)

   839     then show ?thesis

   840       unfolding has_prod_def using 0 by blast

   841   qed

   842 qed

   843

   844 lemma convergent_prod_has_prod [intro]:

   845   shows "convergent_prod f \<Longrightarrow> f has_prod (prodinf f)"

   846   unfolding prodinf_def

   847   by (metis convergent_prod_imp_has_prod has_prod_unique theI')

   848

   849 lemma convergent_prod_LIMSEQ:

   850   shows "convergent_prod f \<Longrightarrow> (\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> prodinf f"

   851   by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent

   852       convergent_prod_to_zero_iff raw_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le)

   853

   854 lemma has_prod_iff: "f has_prod x \<longleftrightarrow> convergent_prod f \<and> prodinf f = x"

   855 proof

   856   assume "f has_prod x"

   857   then show "convergent_prod f \<and> prodinf f = x"

   858     apply safe

   859     using convergent_prod_def has_prod_def apply blast

   860     using has_prod_unique by blast

   861 qed auto

   862

   863 lemma convergent_prod_has_prod_iff: "convergent_prod f \<longleftrightarrow> f has_prod prodinf f"

   864   by (auto simp: has_prod_iff convergent_prod_has_prod)

   865

   866 lemma prodinf_finite:

   867   assumes N: "finite N"

   868     and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"

   869   shows "prodinf f = (\<Prod>n\<in>N. f n)"

   870   using has_prod_finite[OF assms, THEN has_prod_unique] by simp

   871

   872 end

   873

   874 subsection \<open>Infinite products on ordered, topological monoids\<close>

   875

   876 lemma LIMSEQ_prod_0:

   877   fixes f :: "nat \<Rightarrow> 'a::{semidom,topological_space}"

   878   assumes "f i = 0"

   879   shows "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> 0"

   880 proof (subst tendsto_cong)

   881   show "\<forall>\<^sub>F n in sequentially. prod f {..n} = 0"

   882   proof

   883     show "prod f {..n} = 0" if "n \<ge> i" for n

   884       using that assms by auto

   885   qed

   886 qed auto

   887

   888 lemma LIMSEQ_prod_nonneg:

   889   fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}"

   890   assumes 0: "\<And>n. 0 \<le> f n" and a: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> a"

   891   shows "a \<ge> 0"

   892   by (simp add: "0" prod_nonneg LIMSEQ_le_const [OF a])

   893

   894

   895 context

   896   fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}"

   897 begin

   898

   899 lemma has_prod_le:

   900   assumes f: "f has_prod a" and g: "g has_prod b" and le: "\<And>n. 0 \<le> f n \<and> f n \<le> g n"

   901   shows "a \<le> b"

   902 proof (cases "a=0 \<or> b=0")

   903   case True

   904   then show ?thesis

   905   proof

   906     assume [simp]: "a=0"

   907     have "b \<ge> 0"

   908     proof (rule LIMSEQ_prod_nonneg)

   909       show "(\<lambda>n. prod g {..n}) \<longlonglongrightarrow> b"

   910         using g by (auto simp: has_prod_def raw_has_prod_def LIMSEQ_prod_0)

   911     qed (use le order_trans in auto)

   912     then show ?thesis

   913       by auto

   914   next

   915     assume [simp]: "b=0"

   916     then obtain i where "g i = 0"

   917       using g by (auto simp: prod_defs)

   918     then have "f i = 0"

   919       using antisym le by force

   920     then have "a=0"

   921       using f by (auto simp: prod_defs LIMSEQ_prod_0 LIMSEQ_unique)

   922     then show ?thesis

   923       by auto

   924   qed

   925 next

   926   case False

   927   then show ?thesis

   928     using assms

   929     unfolding has_prod_def raw_has_prod_def

   930     by (force simp: LIMSEQ_prod_0 intro!: LIMSEQ_le prod_mono)

   931 qed

   932

   933 lemma prodinf_le:

   934   assumes f: "f has_prod a" and g: "g has_prod b" and le: "\<And>n. 0 \<le> f n \<and> f n \<le> g n"

   935   shows "prodinf f \<le> prodinf g"

   936   using has_prod_le [OF assms] has_prod_unique f g  by blast

   937

   938 end

   939

   940

   941 lemma prod_le_prodinf:

   942   fixes f :: "nat \<Rightarrow> 'a::{linordered_idom,linorder_topology}"

   943   assumes "f has_prod a" "\<And>i. 0 \<le> f i" "\<And>i. i\<ge>n \<Longrightarrow> 1 \<le> f i"

   944   shows "prod f {..<n} \<le> prodinf f"

   945   by(rule has_prod_le[OF has_prod_If_finite_set]) (use assms has_prod_unique in auto)

   946

   947 lemma prodinf_nonneg:

   948   fixes f :: "nat \<Rightarrow> 'a::{linordered_idom,linorder_topology}"

   949   assumes "f has_prod a" "\<And>i. 1 \<le> f i"

   950   shows "1 \<le> prodinf f"

   951   using prod_le_prodinf[of f a 0] assms

   952   by (metis order_trans prod_ge_1 zero_le_one)

   953

   954 lemma prodinf_le_const:

   955   fixes f :: "nat \<Rightarrow> real"

   956   assumes "convergent_prod f" "\<And>n. prod f {..<n} \<le> x"

   957   shows "prodinf f \<le> x"

   958   by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2)

   959

   960 lemma prodinf_eq_one_iff:

   961   fixes f :: "nat \<Rightarrow> real"

   962   assumes f: "convergent_prod f" and ge1: "\<And>n. 1 \<le> f n"

   963   shows "prodinf f = 1 \<longleftrightarrow> (\<forall>n. f n = 1)"

   964 proof

   965   assume "prodinf f = 1"

   966   then have "(\<lambda>n. \<Prod>i<n. f i) \<longlonglongrightarrow> 1"

   967     using convergent_prod_LIMSEQ[of f] assms by (simp add: LIMSEQ_lessThan_iff_atMost)

   968   then have "\<And>i. (\<Prod>n\<in>{i}. f n) \<le> 1"

   969   proof (rule LIMSEQ_le_const)

   970     have "1 \<le> prod f n" for n

   971       by (simp add: ge1 prod_ge_1)

   972     have "prod f {..<n} = 1" for n

   973       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)

   974     then have "(\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" if "n \<ge> Suc i" for i n

   975       by (metis mult.left_neutral order_refl prod.cong prod.neutral_const prod_lessThan_Suc)

   976     then show "\<exists>N. \<forall>n\<ge>N. (\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" for i

   977       by blast

   978   qed

   979   with ge1 show "\<forall>n. f n = 1"

   980     by (auto intro!: antisym)

   981 qed (metis prodinf_zero fun_eq_iff)

   982

   983 lemma prodinf_pos_iff:

   984   fixes f :: "nat \<Rightarrow> real"

   985   assumes "convergent_prod f" "\<And>n. 1 \<le> f n"

   986   shows "1 < prodinf f \<longleftrightarrow> (\<exists>i. 1 < f i)"

   987   using prod_le_prodinf[of f 1] prodinf_eq_one_iff

   988   by (metis convergent_prod_has_prod assms less_le prodinf_nonneg)

   989

   990 lemma less_1_prodinf2:

   991   fixes f :: "nat \<Rightarrow> real"

   992   assumes "convergent_prod f" "\<And>n. 1 \<le> f n" "1 < f i"

   993   shows "1 < prodinf f"

   994 proof -

   995   have "1 < (\<Prod>n<Suc i. f n)"

   996     using assms  by (intro less_1_prod2[where i=i]) auto

   997   also have "\<dots> \<le> prodinf f"

   998     by (intro prod_le_prodinf) (use assms order_trans zero_le_one in \<open>blast+\<close>)

   999   finally show ?thesis .

  1000 qed

  1001

  1002 lemma less_1_prodinf:

  1003   fixes f :: "nat \<Rightarrow> real"

  1004   shows "\<lbrakk>convergent_prod f; \<And>n. 1 < f n\<rbrakk> \<Longrightarrow> 1 < prodinf f"

  1005   by (intro less_1_prodinf2[where i=1]) (auto intro: less_imp_le)

  1006

  1007 lemma prodinf_nonzero:

  1008   fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"

  1009   assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"

  1010   shows "prodinf f \<noteq> 0"

  1011   by (metis assms convergent_prod_offset_0 has_prod_unique raw_has_prod_def has_prod_def)

  1012

  1013 lemma less_0_prodinf:

  1014   fixes f :: "nat \<Rightarrow> real"

  1015   assumes f: "convergent_prod f" and 0: "\<And>i. f i > 0"

  1016   shows "0 < prodinf f"

  1017 proof -

  1018   have "prodinf f \<noteq> 0"

  1019     by (metis assms less_irrefl prodinf_nonzero)

  1020   moreover have "0 < (\<Prod>n<i. f n)" for i

  1021     by (simp add: 0 prod_pos)

  1022   then have "prodinf f \<ge> 0"

  1023     using convergent_prod_LIMSEQ [OF f] LIMSEQ_prod_nonneg 0 less_le by blast

  1024   ultimately show ?thesis

  1025     by auto

  1026 qed

  1027

  1028 lemma prod_less_prodinf2:

  1029   fixes f :: "nat \<Rightarrow> real"

  1030   assumes f: "convergent_prod f" and 1: "\<And>m. m\<ge>n \<Longrightarrow> 1 \<le> f m" and 0: "\<And>m. 0 < f m" and i: "n \<le> i" "1 < f i"

  1031   shows "prod f {..<n} < prodinf f"

  1032 proof -

  1033   have "prod f {..<n} \<le> prod f {..<i}"

  1034     by (rule prod_mono2) (use assms less_le in auto)

  1035   then have "prod f {..<n} < f i * prod f {..<i}"

  1036     using mult_less_le_imp_less[of 1 "f i" "prod f {..<n}" "prod f {..<i}"] assms

  1037     by (simp add: prod_pos)

  1038   moreover have "prod f {..<Suc i} \<le> prodinf f"

  1039     using prod_le_prodinf[of f _ "Suc i"]

  1040     by (meson "0" "1" Suc_leD convergent_prod_has_prod f \<open>n \<le> i\<close> le_trans less_eq_real_def)

  1041   ultimately show ?thesis

  1042     by (metis le_less_trans mult.commute not_le prod_lessThan_Suc)

  1043 qed

  1044

  1045 lemma prod_less_prodinf:

  1046   fixes f :: "nat \<Rightarrow> real"

  1047   assumes f: "convergent_prod f" and 1: "\<And>m. m\<ge>n \<Longrightarrow> 1 < f m" and 0: "\<And>m. 0 < f m"

  1048   shows "prod f {..<n} < prodinf f"

  1049   by (meson "0" "1" f le_less prod_less_prodinf2)

  1050

  1051 lemma raw_has_prodI_bounded:

  1052   fixes f :: "nat \<Rightarrow> real"

  1053   assumes pos: "\<And>n. 1 \<le> f n"

  1054     and le: "\<And>n. (\<Prod>i<n. f i) \<le> x"

  1055   shows "\<exists>p. raw_has_prod f 0 p"

  1056   unfolding raw_has_prod_def add_0_right

  1057 proof (rule exI LIMSEQ_incseq_SUP conjI)+

  1058   show "bdd_above (range (\<lambda>n. prod f {..n}))"

  1059     by (metis bdd_aboveI2 le lessThan_Suc_atMost)

  1060   then have "(SUP i. prod f {..i}) > 0"

  1061     by (metis UNIV_I cSUP_upper less_le_trans pos prod_pos zero_less_one)

  1062   then show "(SUP i. prod f {..i}) \<noteq> 0"

  1063     by auto

  1064   show "incseq (\<lambda>n. prod f {..n})"

  1065     using pos order_trans [OF zero_le_one] by (auto simp: mono_def intro!: prod_mono2)

  1066 qed

  1067

  1068 lemma convergent_prodI_nonneg_bounded:

  1069   fixes f :: "nat \<Rightarrow> real"

  1070   assumes "\<And>n. 1 \<le> f n" "\<And>n. (\<Prod>i<n. f i) \<le> x"

  1071   shows "convergent_prod f"

  1072   using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast

  1073

  1074

  1075 subsection \<open>Infinite products on topological spaces\<close>

  1076

  1077 context

  1078   fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_semigroup_mult,idom}"

  1079 begin

  1080

  1081 lemma raw_has_prod_mult: "\<lbrakk>raw_has_prod f M a; raw_has_prod g M b\<rbrakk> \<Longrightarrow> raw_has_prod (\<lambda>n. f n * g n) M (a * b)"

  1082   by (force simp add: prod.distrib tendsto_mult raw_has_prod_def)

  1083

  1084 lemma has_prod_mult_nz: "\<lbrakk>f has_prod a; g has_prod b; a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. f n * g n) has_prod (a * b)"

  1085   by (simp add: raw_has_prod_mult has_prod_def)

  1086

  1087 end

  1088

  1089

  1090 context

  1091   fixes f g :: "nat \<Rightarrow> 'a::real_normed_field"

  1092 begin

  1093

  1094 lemma has_prod_mult:

  1095   assumes f: "f has_prod a" and g: "g has_prod b"

  1096   shows "(\<lambda>n. f n * g n) has_prod (a * b)"

  1097   using f [unfolded has_prod_def]

  1098 proof (elim disjE exE conjE)

  1099   assume f0: "raw_has_prod f 0 a"

  1100   show ?thesis

  1101     using g [unfolded has_prod_def]

  1102   proof (elim disjE exE conjE)

  1103     assume g0: "raw_has_prod g 0 b"

  1104     with f0 show ?thesis

  1105       by (force simp add: has_prod_def prod.distrib tendsto_mult raw_has_prod_def)

  1106   next

  1107     fix j q

  1108     assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q"

  1109     obtain p where p: "raw_has_prod f (Suc j) p"

  1110       using f0 raw_has_prod_ignore_initial_segment by blast

  1111     then have "Ex (raw_has_prod (\<lambda>n. f n * g n) (Suc j))"

  1112       using q raw_has_prod_mult by blast

  1113     then show ?thesis

  1114       using \<open>b = 0\<close> \<open>g j = 0\<close> has_prod_0_iff by fastforce

  1115   qed

  1116 next

  1117   fix i p

  1118   assume "a = 0" and "f i = 0" and p: "raw_has_prod f (Suc i) p"

  1119   show ?thesis

  1120     using g [unfolded has_prod_def]

  1121   proof (elim disjE exE conjE)

  1122     assume g0: "raw_has_prod g 0 b"

  1123     obtain q where q: "raw_has_prod g (Suc i) q"

  1124       using g0 raw_has_prod_ignore_initial_segment by blast

  1125     then have "Ex (raw_has_prod (\<lambda>n. f n * g n) (Suc i))"

  1126       using raw_has_prod_mult p by blast

  1127     then show ?thesis

  1128       using \<open>a = 0\<close> \<open>f i = 0\<close> has_prod_0_iff by fastforce

  1129   next

  1130     fix j q

  1131     assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q"

  1132     obtain p' where p': "raw_has_prod f (Suc (max i j)) p'"

  1133       by (metis raw_has_prod_ignore_initial_segment max_Suc_Suc max_def p)

  1134     moreover

  1135     obtain q' where q': "raw_has_prod g (Suc (max i j)) q'"

  1136       by (metis raw_has_prod_ignore_initial_segment max.cobounded2 max_Suc_Suc q)

  1137     ultimately show ?thesis

  1138       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)

  1139   qed

  1140 qed

  1141

  1142 lemma convergent_prod_mult:

  1143   assumes f: "convergent_prod f" and g: "convergent_prod g"

  1144   shows "convergent_prod (\<lambda>n. f n * g n)"

  1145   unfolding convergent_prod_def

  1146 proof -

  1147   obtain M p N q where p: "raw_has_prod f M p" and q: "raw_has_prod g N q"

  1148     using convergent_prod_def f g by blast+

  1149   then obtain p' q' where p': "raw_has_prod f (max M N) p'" and q': "raw_has_prod g (max M N) q'"

  1150     by (meson raw_has_prod_ignore_initial_segment max.cobounded1 max.cobounded2)

  1151   then show "\<exists>M p. raw_has_prod (\<lambda>n. f n * g n) M p"

  1152     using raw_has_prod_mult by blast

  1153 qed

  1154

  1155 lemma prodinf_mult: "convergent_prod f \<Longrightarrow> convergent_prod g \<Longrightarrow> prodinf f * prodinf g = (\<Prod>n. f n * g n)"

  1156   by (intro has_prod_unique has_prod_mult convergent_prod_has_prod)

  1157

  1158 end

  1159

  1160 context

  1161   fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_field"

  1162     and I :: "'i set"

  1163 begin

  1164

  1165 lemma has_prod_prod: "(\<And>i. i \<in> I \<Longrightarrow> (f i) has_prod (x i)) \<Longrightarrow> (\<lambda>n. \<Prod>i\<in>I. f i n) has_prod (\<Prod>i\<in>I. x i)"

  1166   by (induct I rule: infinite_finite_induct) (auto intro!: has_prod_mult)

  1167

  1168 lemma prodinf_prod: "(\<And>i. i \<in> I \<Longrightarrow> convergent_prod (f i)) \<Longrightarrow> (\<Prod>n. \<Prod>i\<in>I. f i n) = (\<Prod>i\<in>I. \<Prod>n. f i n)"

  1169   using has_prod_unique[OF has_prod_prod, OF convergent_prod_has_prod] by simp

  1170

  1171 lemma convergent_prod_prod: "(\<And>i. i \<in> I \<Longrightarrow> convergent_prod (f i)) \<Longrightarrow> convergent_prod (\<lambda>n. \<Prod>i\<in>I. f i n)"

  1172   using convergent_prod_has_prod_iff has_prod_prod prodinf_prod by force

  1173

  1174 end

  1175

  1176 subsection \<open>Infinite summability on real normed fields\<close>

  1177

  1178 context

  1179   fixes f :: "nat \<Rightarrow> 'a::real_normed_field"

  1180 begin

  1181

  1182 lemma raw_has_prod_Suc_iff: "raw_has_prod f M (a * f M) \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0"

  1183 proof -

  1184   have "raw_has_prod f M (a * f M) \<longleftrightarrow> (\<lambda>i. \<Prod>j\<le>Suc i. f (j+M)) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0"

  1185     by (subst LIMSEQ_Suc_iff) (simp add: raw_has_prod_def)

  1186   also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0"

  1187     by (simp add: ac_simps atMost_Suc_eq_insert_0 image_Suc_atMost prod_atLeast1_atMost_eq lessThan_Suc_atMost)

  1188   also have "\<dots> \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0"

  1189   proof safe

  1190     assume tends: "(\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M" and 0: "a * f M \<noteq> 0"

  1191     with tendsto_divide[OF tends tendsto_const, of "f M"]

  1192     show "raw_has_prod (\<lambda>n. f (Suc n)) M a"

  1193       by (simp add: raw_has_prod_def)

  1194   qed (auto intro: tendsto_mult_right simp:  raw_has_prod_def)

  1195   finally show ?thesis .

  1196 qed

  1197

  1198 lemma has_prod_Suc_iff:

  1199   assumes "f 0 \<noteq> 0" shows "(\<lambda>n. f (Suc n)) has_prod a \<longleftrightarrow> f has_prod (a * f 0)"

  1200 proof (cases "a = 0")

  1201   case True

  1202   then show ?thesis

  1203   proof (simp add: has_prod_def, safe)

  1204     fix i x

  1205     assume "f (Suc i) = 0" and "raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) x"

  1206     then obtain y where "raw_has_prod f (Suc (Suc i)) y"

  1207       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)

  1208     then show "\<exists>i. f i = 0 \<and> Ex (raw_has_prod f (Suc i))"

  1209       using \<open>f (Suc i) = 0\<close> by blast

  1210   next

  1211     fix i x

  1212     assume "f i = 0" and x: "raw_has_prod f (Suc i) x"

  1213     then obtain j where j: "i = Suc j"

  1214       by (metis assms not0_implies_Suc)

  1215     moreover have "\<exists> y. raw_has_prod (\<lambda>n. f (Suc n)) i y"

  1216       using x by (auto simp: raw_has_prod_def)

  1217     then show "\<exists>i. f (Suc i) = 0 \<and> Ex (raw_has_prod (\<lambda>n. f (Suc n)) (Suc i))"

  1218       using \<open>f i = 0\<close> j by blast

  1219   qed

  1220 next

  1221   case False

  1222   then show ?thesis

  1223     by (auto simp: has_prod_def raw_has_prod_Suc_iff assms)

  1224 qed

  1225

  1226 lemma convergent_prod_Suc_iff:

  1227   shows "convergent_prod (\<lambda>n. f (Suc n)) = convergent_prod f"

  1228 proof

  1229   assume "convergent_prod f"

  1230   then obtain M L where M_nz:"\<forall>n\<ge>M. f n \<noteq> 0" and

  1231         M_L:"(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> L" and "L \<noteq> 0"

  1232     unfolding convergent_prod_altdef by auto

  1233   have "(\<lambda>n. \<Prod>i\<le>n. f (Suc (i + M))) \<longlonglongrightarrow> L / f M"

  1234   proof -

  1235     have "(\<lambda>n. \<Prod>i\<in>{0..Suc n}. f (i + M)) \<longlonglongrightarrow> L"

  1236       using M_L

  1237       apply (subst (asm) LIMSEQ_Suc_iff[symmetric])

  1238       using atLeast0AtMost by auto

  1239     then have "(\<lambda>n. f M * (\<Prod>i\<in>{0..n}. f (Suc (i + M)))) \<longlonglongrightarrow> L"

  1240       apply (subst (asm) prod.atLeast0_atMost_Suc_shift)

  1241       by simp

  1242     then have "(\<lambda>n. (\<Prod>i\<in>{0..n}. f (Suc (i + M)))) \<longlonglongrightarrow> L/f M"

  1243       apply (drule_tac tendsto_divide)

  1244       using M_nz[rule_format,of M,simplified] by auto

  1245     then show ?thesis unfolding atLeast0AtMost .

  1246   qed

  1247   then show "convergent_prod (\<lambda>n. f (Suc n))" unfolding convergent_prod_altdef

  1248     apply (rule_tac exI[where x=M])

  1249     apply (rule_tac exI[where x="L/f M"])

  1250     using M_nz \<open>L\<noteq>0\<close> by auto

  1251 next

  1252   assume "convergent_prod (\<lambda>n. f (Suc n))"

  1253   then obtain M where "\<exists>L. (\<forall>n\<ge>M. f (Suc n) \<noteq> 0) \<and> (\<lambda>n. \<Prod>i\<le>n. f (Suc (i + M))) \<longlonglongrightarrow> L \<and> L \<noteq> 0"

  1254     unfolding convergent_prod_altdef by auto

  1255   then show "convergent_prod f" unfolding convergent_prod_altdef

  1256     apply (rule_tac exI[where x="Suc M"])

  1257     using Suc_le_D by auto

  1258 qed

  1259

  1260 lemma raw_has_prod_inverse:

  1261   assumes "raw_has_prod f M a" shows "raw_has_prod (\<lambda>n. inverse (f n)) M (inverse a)"

  1262   using assms unfolding raw_has_prod_def by (auto dest: tendsto_inverse simp: prod_inversef [symmetric])

  1263

  1264 lemma has_prod_inverse:

  1265   assumes "f has_prod a" shows "(\<lambda>n. inverse (f n)) has_prod (inverse a)"

  1266 using assms raw_has_prod_inverse unfolding has_prod_def by auto

  1267

  1268 lemma convergent_prod_inverse:

  1269   assumes "convergent_prod f"

  1270   shows "convergent_prod (\<lambda>n. inverse (f n))"

  1271   using assms unfolding convergent_prod_def  by (blast intro: raw_has_prod_inverse elim: )

  1272

  1273 end

  1274

  1275 context

  1276   fixes f :: "nat \<Rightarrow> 'a::real_normed_field"

  1277 begin

  1278

  1279 lemma raw_has_prod_Suc_iff': "raw_has_prod f M a \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M (a / f M) \<and> f M \<noteq> 0"

  1280   by (metis raw_has_prod_eq_0 add.commute add.left_neutral raw_has_prod_Suc_iff raw_has_prod_nonzero le_add1 nonzero_mult_div_cancel_right times_divide_eq_left)

  1281

  1282 lemma has_prod_divide: "f has_prod a \<Longrightarrow> g has_prod b \<Longrightarrow> (\<lambda>n. f n / g n) has_prod (a / b)"

  1283   unfolding divide_inverse by (intro has_prod_inverse has_prod_mult)

  1284

  1285 lemma convergent_prod_divide:

  1286   assumes f: "convergent_prod f" and g: "convergent_prod g"

  1287   shows "convergent_prod (\<lambda>n. f n / g n)"

  1288   using f g has_prod_divide has_prod_iff by blast

  1289

  1290 lemma prodinf_divide: "convergent_prod f \<Longrightarrow> convergent_prod g \<Longrightarrow> prodinf f / prodinf g = (\<Prod>n. f n / g n)"

  1291   by (intro has_prod_unique has_prod_divide convergent_prod_has_prod)

  1292

  1293 lemma prodinf_inverse: "convergent_prod f \<Longrightarrow> (\<Prod>n. inverse (f n)) = inverse (\<Prod>n. f n)"

  1294   by (intro has_prod_unique [symmetric] has_prod_inverse convergent_prod_has_prod)

  1295

  1296 lemma has_prod_Suc_imp:

  1297   assumes "(\<lambda>n. f (Suc n)) has_prod a"

  1298   shows "f has_prod (a * f 0)"

  1299 proof -

  1300   have "f has_prod (a * f 0)" when "raw_has_prod (\<lambda>n. f (Suc n)) 0 a"

  1301     apply (cases "f 0=0")

  1302     using that unfolding has_prod_def raw_has_prod_Suc

  1303     by (auto simp add: raw_has_prod_Suc_iff)

  1304   moreover have "f has_prod (a * f 0)" when

  1305     "(\<exists>i q. a = 0 \<and> f (Suc i) = 0 \<and> raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) q)"

  1306   proof -

  1307     from that

  1308     obtain i q where "a = 0" "f (Suc i) = 0" "raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) q"

  1309       by auto

  1310     then show ?thesis unfolding has_prod_def

  1311       by (auto intro!:exI[where x="Suc i"] simp:raw_has_prod_Suc)

  1312   qed

  1313   ultimately show "f has_prod (a * f 0)" using assms unfolding has_prod_def by auto

  1314 qed

  1315

  1316 lemma has_prod_iff_shift:

  1317   assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"

  1318   shows "(\<lambda>i. f (i + n)) has_prod a \<longleftrightarrow> f has_prod (a * (\<Prod>i<n. f i))"

  1319   using assms

  1320 proof (induct n arbitrary: a)

  1321   case 0

  1322   then show ?case by simp

  1323 next

  1324   case (Suc n)

  1325   then have "(\<lambda>i. f (Suc i + n)) has_prod a \<longleftrightarrow> (\<lambda>i. f (i + n)) has_prod (a * f n)"

  1326     by (subst has_prod_Suc_iff) auto

  1327   with Suc show ?case

  1328     by (simp add: ac_simps)

  1329 qed

  1330

  1331 corollary has_prod_iff_shift':

  1332   assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"

  1333   shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i)) \<longleftrightarrow> f has_prod a"

  1334   by (simp add: assms has_prod_iff_shift)

  1335

  1336 lemma has_prod_one_iff_shift:

  1337   assumes "\<And>i. i < n \<Longrightarrow> f i = 1"

  1338   shows "(\<lambda>i. f (i+n)) has_prod a \<longleftrightarrow> (\<lambda>i. f i) has_prod a"

  1339   by (simp add: assms has_prod_iff_shift)

  1340

  1341 lemma convergent_prod_iff_shift:

  1342   shows "convergent_prod (\<lambda>i. f (i + n)) \<longleftrightarrow> convergent_prod f"

  1343   apply safe

  1344   using convergent_prod_offset apply blast

  1345   using convergent_prod_ignore_initial_segment convergent_prod_def by blast

  1346

  1347 lemma has_prod_split_initial_segment:

  1348   assumes "f has_prod a" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"

  1349   shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i))"

  1350   using assms has_prod_iff_shift' by blast

  1351

  1352 lemma prodinf_divide_initial_segment:

  1353   assumes "convergent_prod f" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"

  1354   shows "(\<Prod>i. f (i + n)) = (\<Prod>i. f i) / (\<Prod>i<n. f i)"

  1355   by (rule has_prod_unique[symmetric]) (auto simp: assms has_prod_iff_shift)

  1356

  1357 lemma prodinf_split_initial_segment:

  1358   assumes "convergent_prod f" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"

  1359   shows "prodinf f = (\<Prod>i. f (i + n)) * (\<Prod>i<n. f i)"

  1360   by (auto simp add: assms prodinf_divide_initial_segment)

  1361

  1362 lemma prodinf_split_head:

  1363   assumes "convergent_prod f" "f 0 \<noteq> 0"

  1364   shows "(\<Prod>n. f (Suc n)) = prodinf f / f 0"

  1365   using prodinf_split_initial_segment[of 1] assms by simp

  1366

  1367 end

  1368

  1369 context

  1370   fixes f :: "nat \<Rightarrow> 'a::real_normed_field"

  1371 begin

  1372

  1373 lemma convergent_prod_inverse_iff: "convergent_prod (\<lambda>n. inverse (f n)) \<longleftrightarrow> convergent_prod f"

  1374   by (auto dest: convergent_prod_inverse)

  1375

  1376 lemma convergent_prod_const_iff:

  1377   fixes c :: "'a :: {real_normed_field}"

  1378   shows "convergent_prod (\<lambda>_. c) \<longleftrightarrow> c = 1"

  1379 proof

  1380   assume "convergent_prod (\<lambda>_. c)"

  1381   then show "c = 1"

  1382     using convergent_prod_imp_LIMSEQ LIMSEQ_unique by blast

  1383 next

  1384   assume "c = 1"

  1385   then show "convergent_prod (\<lambda>_. c)"

  1386     by auto

  1387 qed

  1388

  1389 lemma has_prod_power: "f has_prod a \<Longrightarrow> (\<lambda>i. f i ^ n) has_prod (a ^ n)"

  1390   by (induction n) (auto simp: has_prod_mult)

  1391

  1392 lemma convergent_prod_power: "convergent_prod f \<Longrightarrow> convergent_prod (\<lambda>i. f i ^ n)"

  1393   by (induction n) (auto simp: convergent_prod_mult)

  1394

  1395 lemma prodinf_power: "convergent_prod f \<Longrightarrow> prodinf (\<lambda>i. f i ^ n) = prodinf f ^ n"

  1396   by (metis has_prod_unique convergent_prod_imp_has_prod has_prod_power)

  1397

  1398 end

  1399

  1400

  1401 subsection\<open>Exponentials and logarithms\<close>

  1402

  1403 context

  1404   fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"

  1405 begin

  1406

  1407 lemma sums_imp_has_prod_exp:

  1408   assumes "f sums s"

  1409   shows "raw_has_prod (\<lambda>i. exp (f i)) 0 (exp s)"

  1410   using assms continuous_on_exp [of UNIV "\<lambda>x::'a. x"]

  1411   using continuous_on_tendsto_compose [of UNIV exp "(\<lambda>n. sum f {..n})" s]

  1412   by (simp add: prod_defs sums_def_le exp_sum)

  1413

  1414 lemma convergent_prod_exp:

  1415   assumes "summable f"

  1416   shows "convergent_prod (\<lambda>i. exp (f i))"

  1417   using sums_imp_has_prod_exp assms unfolding summable_def convergent_prod_def  by blast

  1418

  1419 lemma prodinf_exp:

  1420   assumes "summable f"

  1421   shows "prodinf (\<lambda>i. exp (f i)) = exp (suminf f)"

  1422 proof -

  1423   have "f sums suminf f"

  1424     using assms by blast

  1425   then have "(\<lambda>i. exp (f i)) has_prod exp (suminf f)"

  1426     by (simp add: has_prod_def sums_imp_has_prod_exp)

  1427   then show ?thesis

  1428     by (rule has_prod_unique [symmetric])

  1429 qed

  1430

  1431 end

  1432

  1433 lemma convergent_prod_iff_summable_real:

  1434   fixes a :: "nat \<Rightarrow> real"

  1435   assumes "\<And>n. a n > 0"

  1436   shows "convergent_prod (\<lambda>k. 1 + a k) \<longleftrightarrow> summable a" (is "?lhs = ?rhs")

  1437 proof

  1438   assume ?lhs

  1439   then obtain p where "raw_has_prod (\<lambda>k. 1 + a k) 0 p"

  1440     by (metis assms add_less_same_cancel2 convergent_prod_offset_0 not_one_less_zero)

  1441   then have to_p: "(\<lambda>n. \<Prod>k\<le>n. 1 + a k) \<longlonglongrightarrow> p"

  1442     by (auto simp: raw_has_prod_def)

  1443   moreover have le: "(\<Sum>k\<le>n. a k) \<le> (\<Prod>k\<le>n. 1 + a k)" for n

  1444     by (rule sum_le_prod) (use assms less_le in force)

  1445   have "(\<Prod>k\<le>n. 1 + a k) \<le> p" for n

  1446   proof (rule incseq_le [OF _ to_p])

  1447     show "incseq (\<lambda>n. \<Prod>k\<le>n. 1 + a k)"

  1448       using assms by (auto simp: mono_def order.strict_implies_order intro!: prod_mono2)

  1449   qed

  1450   with le have "(\<Sum>k\<le>n. a k) \<le> p" for n

  1451     by (metis order_trans)

  1452   with assms bounded_imp_summable show ?rhs

  1453     by (metis not_less order.asym)

  1454 next

  1455   assume R: ?rhs

  1456   have "(\<Prod>k\<le>n. 1 + a k) \<le> exp (suminf a)" for n

  1457   proof -

  1458     have "(\<Prod>k\<le>n. 1 + a k) \<le> exp (\<Sum>k\<le>n. a k)" for n

  1459       by (rule prod_le_exp_sum) (use assms less_le in force)

  1460     moreover have "exp (\<Sum>k\<le>n. a k) \<le> exp (suminf a)" for n

  1461       unfolding exp_le_cancel_iff

  1462       by (meson sum_le_suminf R assms finite_atMost less_eq_real_def)

  1463     ultimately show ?thesis

  1464       by (meson order_trans)

  1465   qed

  1466   then obtain L where L: "(\<lambda>n. \<Prod>k\<le>n. 1 + a k) \<longlonglongrightarrow> L"

  1467     by (metis assms bounded_imp_convergent_prod convergent_prod_iff_nz_lim le_add_same_cancel1 le_add_same_cancel2 less_le not_le zero_le_one)

  1468   moreover have "L \<noteq> 0"

  1469   proof

  1470     assume "L = 0"

  1471     with L have "(\<lambda>n. \<Prod>k\<le>n. 1 + a k) \<longlonglongrightarrow> 0"

  1472       by simp

  1473     moreover have "(\<Prod>k\<le>n. 1 + a k) > 1" for n

  1474       by (simp add: assms less_1_prod)

  1475     ultimately show False

  1476       by (meson Lim_bounded2 not_one_le_zero less_imp_le)

  1477   qed

  1478   ultimately show ?lhs

  1479     using assms convergent_prod_iff_nz_lim

  1480     by (metis add_less_same_cancel1 less_le not_le zero_less_one)

  1481 qed

  1482

  1483 lemma exp_suminf_prodinf_real:

  1484   fixes f :: "nat \<Rightarrow> real"

  1485   assumes ge0:"\<And>n. f n \<ge> 0" and ac: "abs_convergent_prod (\<lambda>n. exp (f n))"

  1486   shows "prodinf (\<lambda>i. exp (f i)) = exp (suminf f)"

  1487 proof -

  1488   have "summable f"

  1489     using ac unfolding abs_convergent_prod_conv_summable

  1490   proof (elim summable_comparison_test')

  1491     fix n

  1492     have "\<bar>f n\<bar> = f n"

  1493       by (simp add: ge0)

  1494     also have "\<dots> \<le> exp (f n) - 1"

  1495       by (metis diff_diff_add exp_ge_add_one_self ge_iff_diff_ge_0)

  1496     finally show "norm (f n) \<le> norm (exp (f n) - 1)"

  1497       by simp

  1498   qed

  1499   then show ?thesis

  1500     by (simp add: prodinf_exp)

  1501 qed

  1502

  1503 lemma has_prod_imp_sums_ln_real:

  1504   fixes f :: "nat \<Rightarrow> real"

  1505   assumes "raw_has_prod f 0 p" and 0: "\<And>x. f x > 0"

  1506   shows "(\<lambda>i. ln (f i)) sums (ln p)"

  1507 proof -

  1508   have "p > 0"

  1509     using assms unfolding prod_defs by (metis LIMSEQ_prod_nonneg less_eq_real_def)

  1510   then show ?thesis

  1511   using assms continuous_on_ln [of "{0<..}" "\<lambda>x. x"]

  1512   using continuous_on_tendsto_compose [of "{0<..}" ln "(\<lambda>n. prod f {..n})" p]

  1513   by (auto simp: prod_defs sums_def_le ln_prod order_tendstoD)

  1514 qed

  1515

  1516 lemma summable_ln_real:

  1517   fixes f :: "nat \<Rightarrow> real"

  1518   assumes f: "convergent_prod f" and 0: "\<And>x. f x > 0"

  1519   shows "summable (\<lambda>i. ln (f i))"

  1520 proof -

  1521   obtain M p where "raw_has_prod f M p"

  1522     using f convergent_prod_def by blast

  1523   then consider i where "i<M" "f i = 0" | p where "raw_has_prod f 0 p"

  1524     using raw_has_prod_cases by blast

  1525   then show ?thesis

  1526   proof cases

  1527     case 1

  1528     with 0 show ?thesis

  1529       by (metis less_irrefl)

  1530   next

  1531     case 2

  1532     then show ?thesis

  1533       using "0" has_prod_imp_sums_ln_real summable_def by blast

  1534   qed

  1535 qed

  1536

  1537 lemma suminf_ln_real:

  1538   fixes f :: "nat \<Rightarrow> real"

  1539   assumes f: "convergent_prod f" and 0: "\<And>x. f x > 0"

  1540   shows "suminf (\<lambda>i. ln (f i)) = ln (prodinf f)"

  1541 proof -

  1542   have "f has_prod prodinf f"

  1543     by (simp add: f has_prod_iff)

  1544   then have "raw_has_prod f 0 (prodinf f)"

  1545     by (metis "0" has_prod_def less_irrefl)

  1546   then have "(\<lambda>i. ln (f i)) sums ln (prodinf f)"

  1547     using "0" has_prod_imp_sums_ln_real by blast

  1548   then show ?thesis

  1549     by (rule sums_unique [symmetric])

  1550 qed

  1551

  1552 lemma prodinf_exp_real:

  1553   fixes f :: "nat \<Rightarrow> real"

  1554   assumes f: "convergent_prod f" and 0: "\<And>x. f x > 0"

  1555   shows "prodinf f = exp (suminf (\<lambda>i. ln (f i)))"

  1556   by (simp add: "0" f less_0_prodinf suminf_ln_real)

  1557

  1558

  1559 lemma Ln_prodinf_complex:

  1560   fixes z :: "nat \<Rightarrow> complex"

  1561   assumes z: "\<And>j. z j \<noteq> 0" and \<xi>: "\<xi> \<noteq> 0"

  1562   shows "((\<lambda>n. \<Prod>j\<le>n. z j) \<longlonglongrightarrow> \<xi>) \<longleftrightarrow> (\<exists>k. (\<lambda>n. (\<Sum>j\<le>n. Ln (z j))) \<longlonglongrightarrow> Ln \<xi> + of_int k * (of_real(2*pi) * \<i>))" (is "?lhs = ?rhs")

  1563 proof

  1564   assume L: ?lhs

  1565   have pnz: "(\<Prod>j\<le>n. z j) \<noteq> 0" for n

  1566     using z by auto

  1567   define \<Theta> where "\<Theta> \<equiv> Arg \<xi> + 2*pi"

  1568   then have "\<Theta> > pi"

  1569     using Arg_def mpi_less_Im_Ln by fastforce

  1570   have \<xi>_eq: "\<xi> = cmod \<xi> * exp (\<i> * \<Theta>)"

  1571     using Arg_def Arg_eq \<xi> unfolding \<Theta>_def by (simp add: algebra_simps exp_add)

  1572   define \<theta> where "\<theta> \<equiv> \<lambda>n. THE t. is_Arg (\<Prod>j\<le>n. z j) t \<and> t \<in> {\<Theta>-pi<..\<Theta>+pi}"

  1573   have uniq: "\<exists>!s. is_Arg (\<Prod>j\<le>n. z j) s \<and> s \<in> {\<Theta>-pi<..\<Theta>+pi}" for n

  1574     using Argument_exists_unique [OF pnz] by metis

  1575   have \<theta>: "is_Arg (\<Prod>j\<le>n. z j) (\<theta> n)" and \<theta>_interval: "\<theta> n \<in> {\<Theta>-pi<..\<Theta>+pi}" for n

  1576     unfolding \<theta>_def

  1577     using theI' [OF uniq] by metis+

  1578   have \<theta>_pos: "\<And>j. \<theta> j > 0"

  1579     using \<theta>_interval \<open>\<Theta> > pi\<close> by simp (meson diff_gt_0_iff_gt less_trans)

  1580   have "(\<Prod>j\<le>n. z j) = cmod (\<Prod>j\<le>n. z j) * exp (\<i> * \<theta> n)" for n

  1581     using \<theta> by (auto simp: is_Arg_def)

  1582   then have eq: "(\<lambda>n. \<Prod>j\<le>n. z j) = (\<lambda>n. cmod (\<Prod>j\<le>n. z j) * exp (\<i> * \<theta> n))"

  1583     by simp

  1584   then have "(\<lambda>n. (cmod (\<Prod>j\<le>n. z j)) * exp (\<i> * (\<theta> n))) \<longlonglongrightarrow> \<xi>"

  1585     using L by force

  1586   then obtain k where k: "(\<lambda>j. \<theta> j - of_int (k j) * (2 * pi)) \<longlonglongrightarrow> \<Theta>"

  1587     using L by (subst (asm) \<xi>_eq) (auto simp add: eq z \<xi> polar_convergence)

  1588   moreover have "\<forall>\<^sub>F n in sequentially. k n = 0"

  1589   proof -

  1590     have *: "kj = 0" if "dist (vj - real_of_int kj * 2) V < 1" "vj \<in> {V - 1<..V + 1}" for kj vj V

  1591       using that  by (auto simp: dist_norm)

  1592     have "\<forall>\<^sub>F j in sequentially. dist (\<theta> j - of_int (k j) * (2 * pi)) \<Theta> < pi"

  1593       using tendstoD [OF k] pi_gt_zero by blast

  1594     then show ?thesis

  1595     proof (rule eventually_mono)

  1596       fix j

  1597       assume d: "dist (\<theta> j - real_of_int (k j) * (2 * pi)) \<Theta> < pi"

  1598       show "k j = 0"

  1599         by (rule * [of "\<theta> j/pi" _ "\<Theta>/pi"])

  1600            (use \<theta>_interval [of j] d in \<open>simp_all add: divide_simps dist_norm\<close>)

  1601     qed

  1602   qed

  1603   ultimately have \<theta>to\<Theta>: "\<theta> \<longlonglongrightarrow> \<Theta>"

  1604     apply (simp only: tendsto_def)

  1605     apply (erule all_forward imp_forward asm_rl)+

  1606     apply (drule (1) eventually_conj)

  1607     apply (auto elim: eventually_mono)

  1608     done

  1609   then have to0: "(\<lambda>n. \<bar>\<theta> (Suc n) - \<theta> n\<bar>) \<longlonglongrightarrow> 0"

  1610     by (metis (full_types) diff_self filterlim_sequentially_Suc tendsto_diff tendsto_rabs_zero)

  1611   have "\<exists>k. Im (\<Sum>j\<le>n. Ln (z j)) - of_int k * (2*pi) = \<theta> n" for n

  1612   proof (rule is_Arg_exp_diff_2pi)

  1613     show "is_Arg (exp (\<Sum>j\<le>n. Ln (z j))) (\<theta> n)"

  1614       using pnz \<theta> by (simp add: is_Arg_def exp_sum prod_norm)

  1615   qed

  1616   then have "\<exists>k. (\<Sum>j\<le>n. Im (Ln (z j))) = \<theta> n + of_int k * (2*pi)" for n

  1617     by (simp add: algebra_simps)

  1618   then obtain k where k: "\<And>n. (\<Sum>j\<le>n. Im (Ln (z j))) = \<theta> n + of_int (k n) * (2*pi)"

  1619     by metis

  1620   obtain K where "\<forall>\<^sub>F n in sequentially. k n = K"

  1621   proof -

  1622     have k_le: "(2*pi) * \<bar>k (Suc n) - k n\<bar> \<le> \<bar>\<theta> (Suc n) - \<theta> n\<bar> + \<bar>Im (Ln (z (Suc n)))\<bar>" for n

  1623     proof -

  1624       have "(\<Sum>j\<le>Suc n. Im (Ln (z j))) - (\<Sum>j\<le>n. Im (Ln (z j))) = Im (Ln (z (Suc n)))"

  1625         by simp

  1626       then show ?thesis

  1627         using k [of "Suc n"] k [of n] by (auto simp: abs_if algebra_simps)

  1628     qed

  1629     have "z \<longlonglongrightarrow> 1"

  1630       using L \<xi> convergent_prod_iff_nz_lim z by (blast intro: convergent_prod_imp_LIMSEQ)

  1631     with z have "(\<lambda>n. Ln (z n)) \<longlonglongrightarrow> Ln 1"

  1632       using isCont_tendsto_compose [OF continuous_at_Ln] nonpos_Reals_one_I by blast

  1633     then have "(\<lambda>n. Ln (z n)) \<longlonglongrightarrow> 0"

  1634       by simp

  1635     then have "(\<lambda>n. \<bar>Im (Ln (z (Suc n)))\<bar>) \<longlonglongrightarrow> 0"

  1636       by (metis LIMSEQ_unique \<open>z \<longlonglongrightarrow> 1\<close> continuous_at_Ln filterlim_sequentially_Suc isCont_tendsto_compose nonpos_Reals_one_I tendsto_Im tendsto_rabs_zero_iff zero_complex.simps(2))

  1637     then have "\<forall>\<^sub>F n in sequentially. \<bar>Im (Ln (z (Suc n)))\<bar> < 1"

  1638       by (simp add: order_tendsto_iff)

  1639     moreover have "\<forall>\<^sub>F n in sequentially. \<bar>\<theta> (Suc n) - \<theta> n\<bar> < 1"

  1640       using to0 by (simp add: order_tendsto_iff)

  1641     ultimately have "\<forall>\<^sub>F n in sequentially. (2*pi) * \<bar>k (Suc n) - k n\<bar> < 1 + 1"

  1642     proof (rule eventually_elim2)

  1643       fix n

  1644       assume "\<bar>Im (Ln (z (Suc n)))\<bar> < 1" and "\<bar>\<theta> (Suc n) - \<theta> n\<bar> < 1"

  1645       with k_le [of n] show "2 * pi * real_of_int \<bar>k (Suc n) - k n\<bar> < 1 + 1"

  1646         by linarith

  1647     qed

  1648     then have "\<forall>\<^sub>F n in sequentially. real_of_int\<bar>k (Suc n) - k n\<bar> < 1"

  1649     proof (rule eventually_mono)

  1650       fix n :: "nat"

  1651       assume "2 * pi * \<bar>k (Suc n) - k n\<bar> < 1 + 1"

  1652       then have "\<bar>k (Suc n) - k n\<bar> < 2 / (2*pi)"

  1653         by (simp add: field_simps)

  1654       also have "... < 1"

  1655         using pi_ge_two by auto

  1656       finally show "real_of_int \<bar>k (Suc n) - k n\<bar> < 1" .

  1657     qed

  1658   then obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> \<bar>k (Suc n) - k n\<bar> = 0"

  1659     using eventually_sequentially less_irrefl of_int_abs by fastforce

  1660   have "k (N+i) = k N" for i

  1661   proof (induction i)

  1662     case (Suc i)

  1663     with N [of "N+i"] show ?case

  1664       by auto

  1665   qed simp

  1666   then have "\<And>n. n\<ge>N \<Longrightarrow> k n = k N"

  1667     using le_Suc_ex by auto

  1668   then show ?thesis

  1669     by (force simp add: eventually_sequentially intro: that)

  1670   qed

  1671   with \<theta>to\<Theta> have "(\<lambda>n. (\<Sum>j\<le>n. Im (Ln (z j)))) \<longlonglongrightarrow> \<Theta> + of_int K * (2*pi)"

  1672     by (simp add: k tendsto_add tendsto_mult Lim_eventually)

  1673   moreover have "(\<lambda>n. (\<Sum>k\<le>n. Re (Ln (z k)))) \<longlonglongrightarrow> Re (Ln \<xi>)"

  1674     using assms continuous_imp_tendsto [OF isCont_ln tendsto_norm [OF L]]

  1675     by (simp add: o_def flip: prod_norm ln_prod)

  1676   ultimately show ?rhs

  1677     by (rule_tac x="K+1" in exI) (auto simp: tendsto_complex_iff \<Theta>_def Arg_def assms algebra_simps)

  1678 next

  1679   assume ?rhs

  1680   then obtain r where r: "(\<lambda>n. (\<Sum>k\<le>n. Ln (z k))) \<longlonglongrightarrow> Ln \<xi> + of_int r * (of_real(2*pi) * \<i>)" ..

  1681   have "(\<lambda>n. exp (\<Sum>k\<le>n. Ln (z k))) \<longlonglongrightarrow> \<xi>"

  1682     using assms continuous_imp_tendsto [OF isCont_exp r] exp_integer_2pi [of r]

  1683     by (simp add: o_def exp_add algebra_simps)

  1684   moreover have "exp (\<Sum>k\<le>n. Ln (z k)) = (\<Prod>k\<le>n. z k)" for n

  1685     by (simp add: exp_sum add_eq_0_iff assms)

  1686   ultimately show ?lhs

  1687     by auto

  1688 qed

  1689

  1690 text\<open>Prop 17.2 of Bak and Newman, Complex Analysis, p.242\<close>

  1691 proposition convergent_prod_iff_summable_complex:

  1692   fixes z :: "nat \<Rightarrow> complex"

  1693   assumes "\<And>k. z k \<noteq> 0"

  1694   shows "convergent_prod (\<lambda>k. z k) \<longleftrightarrow> summable (\<lambda>k. Ln (z k))" (is "?lhs = ?rhs")

  1695 proof

  1696   assume ?lhs

  1697   then obtain p where p: "(\<lambda>n. \<Prod>k\<le>n. z k) \<longlonglongrightarrow> p" and "p \<noteq> 0"

  1698     using convergent_prod_LIMSEQ prodinf_nonzero add_eq_0_iff assms by fastforce

  1699   then show ?rhs

  1700     using Ln_prodinf_complex assms

  1701     by (auto simp: prodinf_nonzero summable_def sums_def_le)

  1702 next

  1703   assume R: ?rhs

  1704   have "(\<Prod>k\<le>n. z k) = exp (\<Sum>k\<le>n. Ln (z k))" for n

  1705     by (simp add: exp_sum add_eq_0_iff assms)

  1706   then have "(\<lambda>n. \<Prod>k\<le>n. z k) \<longlonglongrightarrow> exp (suminf (\<lambda>k. Ln (z k)))"

  1707     using continuous_imp_tendsto [OF isCont_exp summable_LIMSEQ' [OF R]] by (simp add: o_def)

  1708   then show ?lhs

  1709     by (subst convergent_prod_iff_convergent) (auto simp: convergent_def tendsto_Lim assms add_eq_0_iff)

  1710 qed

  1711

  1712 subsection\<open>Embeddings from the reals into some complete real normed field\<close>

  1713

  1714 lemma tendsto_eq_of_real_lim:

  1715   assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q"

  1716   shows "q = of_real (lim f)"

  1717 proof -

  1718   have "convergent (\<lambda>n. of_real (f n) :: 'a)"

  1719     using assms convergent_def by blast

  1720   then have "convergent f"

  1721     unfolding convergent_def

  1722     by (simp add: convergent_eq_Cauchy Cauchy_def)

  1723   then show ?thesis

  1724     by (metis LIMSEQ_unique assms convergentD sequentially_bot tendsto_Lim tendsto_of_real)

  1725 qed

  1726

  1727 lemma tendsto_eq_of_real:

  1728   assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q"

  1729   obtains r where "q = of_real r"

  1730   using tendsto_eq_of_real_lim assms by blast

  1731

  1732 lemma has_prod_of_real_iff:

  1733   "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) has_prod of_real c \<longleftrightarrow> f has_prod c"

  1734   (is "?lhs = ?rhs")

  1735 proof

  1736   assume ?lhs

  1737   then show ?rhs

  1738     apply (auto simp: prod_defs LIMSEQ_prod_0 tendsto_of_real_iff simp flip: of_real_prod)

  1739     using tendsto_eq_of_real

  1740     by (metis of_real_0 tendsto_of_real_iff)

  1741 next

  1742   assume ?rhs

  1743   with tendsto_of_real_iff show ?lhs

  1744     by (fastforce simp: prod_defs simp flip: of_real_prod)

  1745 qed

  1746

  1747 end
`