infinite products: the final piece
authorpaulson <lp15@cam.ac.uk>
Wed Jul 04 11:00:06 2018 +0100 (12 months ago)
changeset 68586006da53a8ac1
parent 68585 1657b9a5dd5d
child 68588 1df516bffaa3
child 68592 6366129107ad
infinite products: the final piece
src/HOL/Analysis/Infinite_Products.thy
     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
    1.57 +    by (simp add: add_eq_0_iff convergent_prod_iff_summable_complex)
    1.58 +qed
    1.59 +
    1.60 +
    1.61  subsection\<open>Embeddings from the reals into some complete real normed field\<close>
    1.62  
    1.63  lemma tendsto_eq_of_real_lim: