src/HOL/Analysis/Infinite_Products.thy
changeset 68452 c027dfbfad30
parent 68426 e0b5f2d14bf9
child 68517 6b5f15387353
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Thu Jun 14 17:50:23 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Fri Jun 15 12:18:06 2018 +0100
     1.3 @@ -98,6 +98,10 @@
     1.4      using LIMSEQ_unique by blast
     1.5  qed
     1.6  
     1.7 +lemma raw_has_prod_Suc: 
     1.8 +  "raw_has_prod f (Suc M) a \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a"
     1.9 +  unfolding raw_has_prod_def by auto
    1.10 +
    1.11  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))"
    1.12    by (simp add: has_prod_def)
    1.13        
    1.14 @@ -1203,21 +1207,37 @@
    1.15  qed
    1.16  
    1.17  lemma convergent_prod_Suc_iff:
    1.18 -  assumes "\<And>k. f k \<noteq> 0" shows "convergent_prod (\<lambda>n. f (Suc n)) = convergent_prod f"
    1.19 +  shows "convergent_prod (\<lambda>n. f (Suc n)) = convergent_prod f"
    1.20  proof
    1.21    assume "convergent_prod f"
    1.22 -  then have "f has_prod prodinf f"
    1.23 -    by (rule convergent_prod_has_prod)
    1.24 -  moreover have "prodinf f \<noteq> 0"
    1.25 -    by (simp add: \<open>convergent_prod f\<close> assms prodinf_nonzero)
    1.26 -  ultimately have "(\<lambda>n. f (Suc n)) has_prod (prodinf f * inverse (f 0))"
    1.27 -    by (simp add: has_prod_Suc_iff inverse_eq_divide assms)
    1.28 -  then show "convergent_prod (\<lambda>n. f (Suc n))"
    1.29 -    using has_prod_iff by blast
    1.30 +  then obtain M L where M_nz:"\<forall>n\<ge>M. f n \<noteq> 0" and 
    1.31 +        M_L:"(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> L" and "L \<noteq> 0" 
    1.32 +    unfolding convergent_prod_altdef by auto
    1.33 +  have "(\<lambda>n. \<Prod>i\<le>n. f (Suc (i + M))) \<longlonglongrightarrow> L / f M"
    1.34 +  proof -
    1.35 +    have "(\<lambda>n. \<Prod>i\<in>{0..Suc n}. f (i + M)) \<longlonglongrightarrow> L"
    1.36 +      using M_L 
    1.37 +      apply (subst (asm) LIMSEQ_Suc_iff[symmetric]) 
    1.38 +      using atLeast0AtMost by auto
    1.39 +    then have "(\<lambda>n. f M * (\<Prod>i\<in>{0..n}. f (Suc (i + M)))) \<longlonglongrightarrow> L"
    1.40 +      apply (subst (asm) prod.atLeast0_atMost_Suc_shift)
    1.41 +      by simp
    1.42 +    then have "(\<lambda>n. (\<Prod>i\<in>{0..n}. f (Suc (i + M)))) \<longlonglongrightarrow> L/f M"
    1.43 +      apply (drule_tac tendsto_divide)
    1.44 +      using M_nz[rule_format,of M,simplified] by auto
    1.45 +    then show ?thesis unfolding atLeast0AtMost .
    1.46 +  qed
    1.47 +  then show "convergent_prod (\<lambda>n. f (Suc n))" unfolding convergent_prod_altdef
    1.48 +    apply (rule_tac exI[where x=M])
    1.49 +    apply (rule_tac exI[where x="L/f M"])
    1.50 +    using M_nz \<open>L\<noteq>0\<close> by auto
    1.51  next
    1.52    assume "convergent_prod (\<lambda>n. f (Suc n))"
    1.53 -  then show "convergent_prod f"
    1.54 -    using assms convergent_prod_def raw_has_prod_Suc_iff by blast
    1.55 +  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"
    1.56 +    unfolding convergent_prod_altdef by auto
    1.57 +  then show "convergent_prod f" unfolding convergent_prod_altdef
    1.58 +    apply (rule_tac exI[where x="Suc M"])
    1.59 +    using Suc_le_D by auto
    1.60  qed
    1.61  
    1.62  lemma raw_has_prod_inverse: 
    1.63 @@ -1256,6 +1276,26 @@
    1.64  lemma prodinf_inverse: "convergent_prod f \<Longrightarrow> (\<Prod>n. inverse (f n)) = inverse (\<Prod>n. f n)"
    1.65    by (intro has_prod_unique [symmetric] has_prod_inverse convergent_prod_has_prod)
    1.66  
    1.67 +lemma has_prod_Suc_imp: 
    1.68 +  assumes "(\<lambda>n. f (Suc n)) has_prod a"
    1.69 +  shows "f has_prod (a * f 0)"
    1.70 +proof -
    1.71 +  have "f has_prod (a * f 0)" when "raw_has_prod (\<lambda>n. f (Suc n)) 0 a" 
    1.72 +    apply (cases "f 0=0")
    1.73 +    using that unfolding has_prod_def raw_has_prod_Suc 
    1.74 +    by (auto simp add: raw_has_prod_Suc_iff)
    1.75 +  moreover have "f has_prod (a * f 0)" when 
    1.76 +    "(\<exists>i q. a = 0 \<and> f (Suc i) = 0 \<and> raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) q)" 
    1.77 +  proof -
    1.78 +    from that 
    1.79 +    obtain i q where "a = 0" "f (Suc i) = 0" "raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) q"
    1.80 +      by auto
    1.81 +    then show ?thesis unfolding has_prod_def 
    1.82 +      by (auto intro!:exI[where x="Suc i"] simp:raw_has_prod_Suc)
    1.83 +  qed
    1.84 +  ultimately show "f has_prod (a * f 0)" using assms unfolding has_prod_def by auto
    1.85 +qed
    1.86 +
    1.87  lemma has_prod_iff_shift: 
    1.88    assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
    1.89    shows "(\<lambda>i. f (i + n)) has_prod a \<longleftrightarrow> f has_prod (a * (\<Prod>i<n. f i))"
    1.90 @@ -1373,6 +1413,24 @@
    1.91  
    1.92  end
    1.93  
    1.94 +lemma exp_suminf_prodinf_real:
    1.95 +  fixes f :: "nat \<Rightarrow> real"
    1.96 +  assumes ge0:"\<And>n. f n \<ge> 0" and ac: "abs_convergent_prod (\<lambda>n. exp (f n))"
    1.97 +  shows "prodinf (\<lambda>i. exp (f i)) = exp (suminf f)"
    1.98 +proof -
    1.99 +  have "summable f" 
   1.100 +    using ac unfolding abs_convergent_prod_conv_summable
   1.101 +  proof (elim summable_comparison_test')
   1.102 +    fix n
   1.103 +    show "norm (f n) \<le> norm (exp (f n) - 1)" 
   1.104 +      using ge0[of n] 
   1.105 +      by (metis abs_of_nonneg add.commute diff_add_cancel diff_ge_0_iff_ge exp_ge_add_one_self 
   1.106 +          exp_le_cancel_iff one_le_exp_iff real_norm_def)
   1.107 +  qed
   1.108 +  then show ?thesis
   1.109 +    by (simp add: prodinf_exp)
   1.110 +qed
   1.111 +
   1.112  lemma has_prod_imp_sums_ln_real: 
   1.113    fixes f :: "nat \<Rightarrow> real"
   1.114    assumes "raw_has_prod f 0 p" and 0: "\<And>x. f x > 0"