# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1530625574 -3600
# Node ID 1657b9a5dd5d3dd459b0aa6409ed4a4c481d8fdc
# Parent  ec4fe1032b6e03205a7a6ad1a9c7027388486d22
more on infinite products

diff -r ec4fe1032b6e -r 1657b9a5dd5d src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jul 03 10:07:35 2018 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jul 03 14:46:14 2018 +0100
@@ -278,6 +278,84 @@
     by (auto simp: norm_mult)
 qed
 
+lemma cmod_add_squared:
+  fixes r1 r2::real
+  assumes "r1 \<ge> 0" "r2 \<ge> 0"
+  shows "(cmod (r1 * exp (\<i> * \<theta>1) + r2 * exp (\<i> * \<theta>2)))\<^sup>2 = r1\<^sup>2 + r2\<^sup>2 + 2 * r1 * r2 * cos (\<theta>1 - \<theta>2)" (is "(cmod (?z1 + ?z2))\<^sup>2 = ?rhs")
+proof -
+  have "(cmod (?z1 + ?z2))\<^sup>2 = (?z1 + ?z2) * cnj (?z1 + ?z2)"
+    by (rule complex_norm_square)
+  also have "\<dots> = (?z1 * cnj ?z1 + ?z2 * cnj ?z2) + (?z1 * cnj ?z2 + cnj ?z1 * ?z2)"
+    by (simp add: algebra_simps)
+  also have "\<dots> = (norm ?z1)\<^sup>2 + (norm ?z2)\<^sup>2 + 2 * Re (?z1 * cnj ?z2)"
+    unfolding complex_norm_square [symmetric] cnj_add_mult_eq_Re by simp
+  also have "\<dots> = ?rhs"
+    by (simp add: norm_mult) (simp add: exp_Euler complex_is_Real_iff [THEN iffD1] cos_diff algebra_simps)
+  finally show ?thesis
+    using of_real_eq_iff by blast
+qed
+
+lemma cmod_diff_squared:
+  fixes r1 r2::real
+  assumes "r1 \<ge> 0" "r2 \<ge> 0"
+  shows "(cmod (r1 * exp (\<i> * \<theta>1) - r2 * exp (\<i> * \<theta>2)))\<^sup>2 = r1\<^sup>2 + r2\<^sup>2 - 2*r1*r2*cos (\<theta>1 - \<theta>2)" (is "(cmod (?z1 - ?z2))\<^sup>2 = ?rhs")
+proof -
+  have "exp (\<i> * (\<theta>2 + pi)) = - exp (\<i> * \<theta>2)"
+    by (simp add: exp_Euler cos_plus_pi sin_plus_pi)
+  then have "(cmod (?z1 - ?z2))\<^sup>2 = cmod (?z1 + r2 * exp (\<i> * (\<theta>2 + pi))) ^2"
+    by simp
+  also have "\<dots> = r1\<^sup>2 + r2\<^sup>2 + 2*r1*r2*cos (\<theta>1 - (\<theta>2 + pi))"
+    using assms cmod_add_squared by blast
+  also have "\<dots> = ?rhs"
+    by (simp add: add.commute diff_add_eq_diff_diff_swap)
+  finally show ?thesis .
+qed
+
+lemma polar_convergence:
+  fixes R::real
+  assumes "\<And>j. r j > 0" "R > 0"
+  shows "((\<lambda>j. r j * exp (\<i> * \<theta> j)) \<longlonglongrightarrow> (R * exp (\<i> * \<Theta>))) \<longleftrightarrow>
+         (r \<longlonglongrightarrow> R) \<and> (\<exists>k. (\<lambda>j. \<theta> j - of_int (k j) * (2 * pi)) \<longlonglongrightarrow> \<Theta>)"    (is "(?z \<longlonglongrightarrow> ?Z) = ?rhs")
+proof
+  assume L: "?z \<longlonglongrightarrow> ?Z"
+  have rR: "r \<longlonglongrightarrow> R"
+    using tendsto_norm [OF L] assms by (auto simp: norm_mult abs_of_pos)
+  moreover obtain k where "(\<lambda>j. \<theta> j - of_int (k j) * (2 * pi)) \<longlonglongrightarrow> \<Theta>"
+  proof -
+    have "cos (\<theta> j - \<Theta>) = ((r j)\<^sup>2 + R\<^sup>2 - (norm(?z j - ?Z))\<^sup>2) / (2 * R * r j)" for j
+      apply (subst cmod_diff_squared)
+      using assms by (auto simp: divide_simps less_le)
+    moreover have "(\<lambda>j. ((r j)\<^sup>2 + R\<^sup>2 - (norm(?z j - ?Z))\<^sup>2) / (2 * R * r j)) \<longlonglongrightarrow> ((R\<^sup>2 + R\<^sup>2 - (norm(?Z - ?Z))\<^sup>2) / (2 * R * R))"
+      by (intro L rR tendsto_intros) (use \<open>R > 0\<close> in force)
+    moreover have "((R\<^sup>2 + R\<^sup>2 - (norm(?Z - ?Z))\<^sup>2) / (2 * R * R)) = 1"
+      using \<open>R > 0\<close> by (simp add: power2_eq_square divide_simps)
+    ultimately have "(\<lambda>j. cos (\<theta> j - \<Theta>)) \<longlonglongrightarrow> 1"
+      by auto
+    then show ?thesis
+      using that cos_diff_limit_1 by blast
+  qed
+  ultimately show ?rhs
+    by metis
+next
+  assume R: ?rhs
+  show "?z \<longlonglongrightarrow> ?Z"
+  proof (rule tendsto_mult)
+    show "(\<lambda>x. complex_of_real (r x)) \<longlonglongrightarrow> of_real R"
+      using R by (auto simp: tendsto_of_real_iff)
+    obtain k where "(\<lambda>j. \<theta> j - of_int (k j) * (2 * pi)) \<longlonglongrightarrow> \<Theta>"
+      using R by metis
+    then have "(\<lambda>j. complex_of_real (\<theta> j - of_int (k j) * (2 * pi))) \<longlonglongrightarrow> of_real \<Theta>"
+      using tendsto_of_real_iff by force
+    then have "(\<lambda>j.  exp (\<i> * of_real (\<theta> j - of_int (k j) * (2 * pi)))) \<longlonglongrightarrow> exp (\<i> * \<Theta>)"
+      using tendsto_mult [OF tendsto_const] isCont_exp isCont_tendsto_compose by blast
+    moreover have "exp (\<i> * of_real (\<theta> j - of_int (k j) * (2 * pi))) = exp (\<i> * \<theta> j)" for j
+      unfolding exp_eq
+      by (rule_tac x="- k j" in exI) (auto simp: algebra_simps)
+    ultimately show "(\<lambda>j. exp (\<i> * \<theta> j)) \<longlonglongrightarrow> exp (\<i> * \<Theta>)"
+      by auto
+  qed
+qed
+
 lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * pi * n)"
 proof -
   { assume "sin y = sin x" "cos y = cos x"
diff -r ec4fe1032b6e -r 1657b9a5dd5d src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Tue Jul 03 10:07:35 2018 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy	Tue Jul 03 14:46:14 2018 +0100
@@ -6,7 +6,7 @@
 *)
 section \<open>Infinite Products\<close>
 theory Infinite_Products
-  imports Topology_Euclidean_Space
+  imports Topology_Euclidean_Space Complex_Transcendental
 begin
 
 subsection\<open>Preliminaries\<close>
@@ -1430,6 +1430,56 @@
 
 end
 
+lemma convergent_prod_iff_summable_real:
+  fixes a :: "nat \<Rightarrow> real"
+  assumes "\<And>n. a n > 0"
+  shows "convergent_prod (\<lambda>k. 1 + a k) \<longleftrightarrow> summable a" (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then obtain p where "raw_has_prod (\<lambda>k. 1 + a k) 0 p"
+    by (metis assms add_less_same_cancel2 convergent_prod_offset_0 not_one_less_zero)
+  then have to_p: "(\<lambda>n. \<Prod>k\<le>n. 1 + a k) \<longlonglongrightarrow> p"
+    by (auto simp: raw_has_prod_def)
+  moreover have le: "(\<Sum>k\<le>n. a k) \<le> (\<Prod>k\<le>n. 1 + a k)" for n
+    by (rule sum_le_prod) (use assms less_le in force)
+  have "(\<Prod>k\<le>n. 1 + a k) \<le> p" for n
+  proof (rule incseq_le [OF _ to_p])
+    show "incseq (\<lambda>n. \<Prod>k\<le>n. 1 + a k)"
+      using assms by (auto simp: mono_def order.strict_implies_order intro!: prod_mono2)
+  qed
+  with le have "(\<Sum>k\<le>n. a k) \<le> p" for n
+    by (metis order_trans)
+  with assms bounded_imp_summable show ?rhs
+    by (metis not_less order.asym)
+next
+  assume R: ?rhs
+  have "(\<Prod>k\<le>n. 1 + a k) \<le> exp (suminf a)" for n
+  proof -
+    have "(\<Prod>k\<le>n. 1 + a k) \<le> exp (\<Sum>k\<le>n. a k)" for n
+      by (rule prod_le_exp_sum) (use assms less_le in force)
+    moreover have "exp (\<Sum>k\<le>n. a k) \<le> exp (suminf a)" for n
+      unfolding exp_le_cancel_iff
+      by (meson sum_le_suminf R assms finite_atMost less_eq_real_def)
+    ultimately show ?thesis
+      by (meson order_trans)
+  qed
+  then obtain L where L: "(\<lambda>n. \<Prod>k\<le>n. 1 + a k) \<longlonglongrightarrow> L"
+    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)
+  moreover have "L \<noteq> 0"
+  proof
+    assume "L = 0"
+    with L have "(\<lambda>n. \<Prod>k\<le>n. 1 + a k) \<longlonglongrightarrow> 0"
+      by simp
+    moreover have "(\<Prod>k\<le>n. 1 + a k) > 1" for n
+      by (simp add: assms less_1_prod)
+    ultimately show False
+      by (meson Lim_bounded2 not_one_le_zero less_imp_le)
+  qed
+  ultimately show ?lhs
+    using assms convergent_prod_iff_nz_lim
+    by (metis add_less_same_cancel1 less_le not_le zero_less_one)
+qed
+
 lemma exp_suminf_prodinf_real:
   fixes f :: "nat \<Rightarrow> real"
   assumes ge0:"\<And>n. f n \<ge> 0" and ac: "abs_convergent_prod (\<lambda>n. exp (f n))"
@@ -1506,6 +1556,159 @@
   by (simp add: "0" f less_0_prodinf suminf_ln_real)
 
 
+lemma Ln_prodinf_complex:
+  fixes z :: "nat \<Rightarrow> complex"
+  assumes z: "\<And>j. z j \<noteq> 0" and \<xi>: "\<xi> \<noteq> 0"
+  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")
+proof
+  assume L: ?lhs
+  have pnz: "(\<Prod>j\<le>n. z j) \<noteq> 0" for n
+    using z by auto
+  define \<Theta> where "\<Theta> \<equiv> Arg \<xi> + 2*pi"
+  then have "\<Theta> > pi"
+    using Arg_def mpi_less_Im_Ln by fastforce
+  have \<xi>_eq: "\<xi> = cmod \<xi> * exp (\<i> * \<Theta>)"
+    using Arg_def Arg_eq \<xi> unfolding \<Theta>_def by (simp add: algebra_simps exp_add)
+  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}"
+  have uniq: "\<exists>!s. is_Arg (\<Prod>j\<le>n. z j) s \<and> s \<in> {\<Theta>-pi<..\<Theta>+pi}" for n
+    using Argument_exists_unique [OF pnz] by metis
+  have \<theta>: "is_Arg (\<Prod>j\<le>n. z j) (\<theta> n)" and \<theta>_interval: "\<theta> n \<in> {\<Theta>-pi<..\<Theta>+pi}" for n
+    unfolding \<theta>_def
+    using theI' [OF uniq] by metis+
+  have \<theta>_pos: "\<And>j. \<theta> j > 0"
+    using \<theta>_interval \<open>\<Theta> > pi\<close> by simp (meson diff_gt_0_iff_gt less_trans)
+  have "(\<Prod>j\<le>n. z j) = cmod (\<Prod>j\<le>n. z j) * exp (\<i> * \<theta> n)" for n
+    using \<theta> by (auto simp: is_Arg_def)
+  then have eq: "(\<lambda>n. \<Prod>j\<le>n. z j) = (\<lambda>n. cmod (\<Prod>j\<le>n. z j) * exp (\<i> * \<theta> n))"
+    by simp
+  then have "(\<lambda>n. (cmod (\<Prod>j\<le>n. z j)) * exp (\<i> * (\<theta> n))) \<longlonglongrightarrow> \<xi>"
+    using L by force
+  then obtain k where k: "(\<lambda>j. \<theta> j - of_int (k j) * (2 * pi)) \<longlonglongrightarrow> \<Theta>"
+    using L by (subst (asm) \<xi>_eq) (auto simp add: eq z \<xi> polar_convergence)
+  moreover have "\<forall>\<^sub>F n in sequentially. k n = 0"
+  proof -
+    have *: "kj = 0" if "dist (vj - real_of_int kj * 2) V < 1" "vj \<in> {V - 1<..V + 1}" for kj vj V
+      using that  by (auto simp: dist_norm)
+    have "\<forall>\<^sub>F j in sequentially. dist (\<theta> j - of_int (k j) * (2 * pi)) \<Theta> < pi"
+      using tendstoD [OF k] pi_gt_zero by blast
+    then show ?thesis
+    proof (rule eventually_mono)
+      fix j
+      assume d: "dist (\<theta> j - real_of_int (k j) * (2 * pi)) \<Theta> < pi"
+      show "k j = 0"
+        by (rule * [of "\<theta> j/pi" _ "\<Theta>/pi"])
+           (use \<theta>_interval [of j] d in \<open>simp_all add: divide_simps dist_norm\<close>)
+    qed
+  qed
+  ultimately have \<theta>to\<Theta>: "\<theta> \<longlonglongrightarrow> \<Theta>"
+    apply (simp only: tendsto_def)
+    apply (erule all_forward imp_forward asm_rl)+
+    apply (drule (1) eventually_conj)
+    apply (auto elim: eventually_mono)
+    done
+  then have to0: "(\<lambda>n. \<bar>\<theta> (Suc n) - \<theta> n\<bar>) \<longlonglongrightarrow> 0"
+    by (metis (full_types) diff_self filterlim_sequentially_Suc tendsto_diff tendsto_rabs_zero)
+  have "\<exists>k. Im (\<Sum>j\<le>n. Ln (z j)) - of_int k * (2*pi) = \<theta> n" for n
+  proof (rule is_Arg_exp_diff_2pi)
+    show "is_Arg (exp (\<Sum>j\<le>n. Ln (z j))) (\<theta> n)"
+      using pnz \<theta> by (simp add: is_Arg_def exp_sum prod_norm)
+  qed
+  then have "\<exists>k. (\<Sum>j\<le>n. Im (Ln (z j))) = \<theta> n + of_int k * (2*pi)" for n
+    by (simp add: algebra_simps)
+  then obtain k where k: "\<And>n. (\<Sum>j\<le>n. Im (Ln (z j))) = \<theta> n + of_int (k n) * (2*pi)"
+    by metis
+  obtain K where "\<forall>\<^sub>F n in sequentially. k n = K"
+  proof -
+    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
+    proof -
+      have "(\<Sum>j\<le>Suc n. Im (Ln (z j))) - (\<Sum>j\<le>n. Im (Ln (z j))) = Im (Ln (z (Suc n)))"
+        by simp
+      then show ?thesis
+        using k [of "Suc n"] k [of n] by (auto simp: abs_if algebra_simps)
+    qed
+    have "z \<longlonglongrightarrow> 1"
+      using L \<xi> convergent_prod_iff_nz_lim z by (blast intro: convergent_prod_imp_LIMSEQ)
+    with z have "(\<lambda>n. Ln (z n)) \<longlonglongrightarrow> Ln 1"
+      using isCont_tendsto_compose [OF continuous_at_Ln] nonpos_Reals_one_I by blast
+    then have "(\<lambda>n. Ln (z n)) \<longlonglongrightarrow> 0"
+      by simp
+    then have "(\<lambda>n. \<bar>Im (Ln (z (Suc n)))\<bar>) \<longlonglongrightarrow> 0"
+      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))
+    then have "\<forall>\<^sub>F n in sequentially. \<bar>Im (Ln (z (Suc n)))\<bar> < 1"
+      by (simp add: order_tendsto_iff)
+    moreover have "\<forall>\<^sub>F n in sequentially. \<bar>\<theta> (Suc n) - \<theta> n\<bar> < 1"
+      using to0 by (simp add: order_tendsto_iff)
+    ultimately have "\<forall>\<^sub>F n in sequentially. (2*pi) * \<bar>k (Suc n) - k n\<bar> < 1 + 1" 
+    proof (rule eventually_elim2) 
+      fix n 
+      assume "\<bar>Im (Ln (z (Suc n)))\<bar> < 1" and "\<bar>\<theta> (Suc n) - \<theta> n\<bar> < 1"
+      with k_le [of n] show "2 * pi * real_of_int \<bar>k (Suc n) - k n\<bar> < 1 + 1"
+        by linarith
+    qed
+    then have "\<forall>\<^sub>F n in sequentially. real_of_int\<bar>k (Suc n) - k n\<bar> < 1" 
+    proof (rule eventually_mono)
+      fix n :: "nat"
+      assume "2 * pi * \<bar>k (Suc n) - k n\<bar> < 1 + 1"
+      then have "\<bar>k (Suc n) - k n\<bar> < 2 / (2*pi)"
+        by (simp add: field_simps)
+      also have "... < 1"
+        using pi_ge_two by auto
+      finally show "real_of_int \<bar>k (Suc n) - k n\<bar> < 1" .
+    qed
+  then obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> \<bar>k (Suc n) - k n\<bar> = 0"
+    using eventually_sequentially less_irrefl of_int_abs by fastforce
+  have "k (N+i) = k N" for i
+  proof (induction i)
+    case (Suc i)
+    with N [of "N+i"] show ?case
+      by auto
+  qed simp
+  then have "\<And>n. n\<ge>N \<Longrightarrow> k n = k N"
+    using le_Suc_ex by auto
+  then show ?thesis
+    by (force simp add: eventually_sequentially intro: that)
+  qed
+  with \<theta>to\<Theta> have "(\<lambda>n. (\<Sum>j\<le>n. Im (Ln (z j)))) \<longlonglongrightarrow> \<Theta> + of_int K * (2*pi)"
+    by (simp add: k tendsto_add tendsto_mult Lim_eventually)
+  moreover have "(\<lambda>n. (\<Sum>k\<le>n. Re (Ln (z k)))) \<longlonglongrightarrow> Re (Ln \<xi>)"
+    using assms continuous_imp_tendsto [OF isCont_ln tendsto_norm [OF L]]
+    by (simp add: o_def flip: prod_norm ln_prod)
+  ultimately show ?rhs
+    by (rule_tac x="K+1" in exI) (auto simp: tendsto_complex_iff \<Theta>_def Arg_def assms algebra_simps)
+next
+  assume ?rhs
+  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>)" ..
+  have "(\<lambda>n. exp (\<Sum>k\<le>n. Ln (z k))) \<longlonglongrightarrow> \<xi>"
+    using assms continuous_imp_tendsto [OF isCont_exp r] exp_integer_2pi [of r]
+    by (simp add: o_def exp_add algebra_simps)
+  moreover have "exp (\<Sum>k\<le>n. Ln (z k)) = (\<Prod>k\<le>n. z k)" for n
+    by (simp add: exp_sum add_eq_0_iff assms)
+  ultimately show ?lhs
+    by auto
+qed
+
+text\<open>Prop 17.2 of Bak and Newman, Complex Analysis, p.242\<close>
+proposition convergent_prod_iff_summable_complex:
+  fixes z :: "nat \<Rightarrow> complex"
+  assumes "\<And>k. z k \<noteq> 0"
+  shows "convergent_prod (\<lambda>k. z k) \<longleftrightarrow> summable (\<lambda>k. Ln (z k))" (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then obtain p where p: "(\<lambda>n. \<Prod>k\<le>n. z k) \<longlonglongrightarrow> p" and "p \<noteq> 0"
+    using convergent_prod_LIMSEQ prodinf_nonzero add_eq_0_iff assms by fastforce
+  then show ?rhs
+    using Ln_prodinf_complex assms
+    by (auto simp: prodinf_nonzero summable_def sums_def_le)
+next
+  assume R: ?rhs
+  have "(\<Prod>k\<le>n. z k) = exp (\<Sum>k\<le>n. Ln (z k))" for n
+    by (simp add: exp_sum add_eq_0_iff assms)
+  then have "(\<lambda>n. \<Prod>k\<le>n. z k) \<longlonglongrightarrow> exp (suminf (\<lambda>k. Ln (z k)))"
+    using continuous_imp_tendsto [OF isCont_exp summable_LIMSEQ' [OF R]] by (simp add: o_def)
+  then show ?lhs
+    by (subst convergent_prod_iff_convergent) (auto simp: convergent_def tendsto_Lim assms add_eq_0_iff)
+qed
+
 subsection\<open>Embeddings from the reals into some complete real normed field\<close>
 
 lemma tendsto_eq_of_real_lim: