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.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]