author paulson Wed Jul 04 11:00:06 2018 +0100 (12 months ago) changeset 68586 006da53a8ac1 parent 68585 1657b9a5dd5d child 68588 1df516bffaa3 child 68592 6366129107ad
infinite products: the final piece
```     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Tue Jul 03 14:46:14 2018 +0100
1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Wed Jul 04 11:00:06 2018 +0100
1.3 @@ -1709,6 +1709,60 @@
1.4      by (subst convergent_prod_iff_convergent) (auto simp: convergent_def tendsto_Lim assms add_eq_0_iff)
1.5  qed
1.6
1.7 +text\<open>Prop 17.3 of Bak and Newman, Complex Analysis\<close>
1.8 +proposition summable_imp_convergent_prod_complex:
1.9 +  fixes z :: "nat \<Rightarrow> complex"
1.10 +  assumes z: "summable (\<lambda>k. norm (z k))" and non0: "\<And>k. z k \<noteq> -1"
1.11 +  shows "convergent_prod (\<lambda>k. 1 + z k)"
1.12 +proof -
1.13 +  note if_cong [cong] power_Suc [simp del]
1.14 +  obtain N where N: "\<And>k. k\<ge>N \<Longrightarrow> norm (z k) < 1/2"
1.15 +    using summable_LIMSEQ_zero [OF z]
1.16 +    by (metis diff_zero dist_norm half_gt_zero_iff less_numeral_extra(1) lim_sequentially tendsto_norm_zero_iff)
1.17 +  have "norm (Ln (1 + z k)) \<le> 2 * norm (z k)" if "k \<ge> N" for k
1.18 +  proof (cases "z k = 0")
1.19 +    case False
1.20 +    let ?f = "\<lambda>i. cmod ((- 1) ^ i * z k ^ i / of_nat (Suc i))"
1.21 +    have normf: "norm (?f n) \<le> (1 / 2) ^ n" for n
1.22 +    proof -
1.23 +      have "norm (?f n) = cmod (z k) ^ n / cmod (1 + of_nat n)"
1.24 +        by (auto simp: norm_divide norm_mult norm_power)
1.25 +      also have "\<dots> \<le> cmod (z k) ^ n"
1.26 +        by (auto simp: divide_simps mult_le_cancel_left1 in_Reals_norm)
1.27 +      also have "\<dots> \<le> (1 / 2) ^ n"
1.28 +        using N [OF that] by (simp add: power_mono)
1.29 +      finally show "norm (?f n) \<le> (1 / 2) ^ n" .
1.30 +    qed
1.31 +    have summablef: "summable ?f"
1.32 +      by (intro normf summable_comparison_test' [OF summable_geometric [of "1/2"]]) auto
1.33 +    have "(\<lambda>n. (- 1) ^ Suc n / of_nat n * z k ^ n) sums Ln (1 + z k)"
1.34 +      using Ln_series [of "z k"] N that by fastforce
1.35 +    then have *: "(\<lambda>i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))) sums Ln (1 + z k)"
1.36 +      using sums_split_initial_segment [where n= 1]  by (force simp: power_Suc mult_ac)
1.37 +    then have "norm (Ln (1 + z k)) = norm (suminf (\<lambda>i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))))"
1.38 +      using sums_unique by force
1.39 +    also have "\<dots> = norm (z k * suminf (\<lambda>i. ((- 1) ^ i * z k ^ i) / (Suc i)))"
1.40 +      apply (subst suminf_mult)
1.41 +      using * False
1.42 +      by (auto simp: sums_summable intro: summable_mult_D [of "z k"])
1.43 +    also have "\<dots> = norm (z k) * norm (suminf (\<lambda>i. ((- 1) ^ i * z k ^ i) / (Suc i)))"
1.44 +      by (simp add: norm_mult)
1.45 +    also have "\<dots> \<le> norm (z k) * suminf (\<lambda>i. norm (((- 1) ^ i * z k ^ i) / (Suc i)))"
1.46 +      by (intro mult_left_mono summable_norm summablef) auto
1.47 +    also have "\<dots> \<le> norm (z k) * suminf (\<lambda>i. (1/2) ^ i)"
1.48 +      by (intro mult_left_mono suminf_le) (use summable_geometric [of "1/2"] summablef normf in auto)
1.49 +    also have "\<dots> \<le> norm (z k) * 2"
1.50 +      using suminf_geometric [of "1/2::real"] by simp
1.51 +    finally show ?thesis
1.52 +      by (simp add: mult_ac)
1.53 +  qed simp
1.54 +  then have "summable (\<lambda>k. Ln (1 + z k))"
1.55 +    by (metis summable_comparison_test summable_mult z)
1.56 +  with non0 show ?thesis