author  paulson <lp15@cam.ac.uk> 
Thu, 10 May 2018 15:41:34 +0100  
changeset 68136  f022083489d0 
parent 68127  137d5d0112bb 
child 68138  c738f40e88d4 
permissions  rwrr 
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

1 
(*File: HOL/Analysis/Infinite_Product.thy 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

2 
Author: Manuel Eberl & LC Paulson 
66277  3 

4 
Basic results about convergence and absolute convergence of infinite products 

5 
and their connection to summability. 

6 
*) 

7 
section \<open>Infinite Products\<close> 

8 
theory Infinite_Products 

9 
imports Complex_Main 

10 
begin 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

11 

66277  12 
lemma sum_le_prod: 
13 
fixes f :: "'a \<Rightarrow> 'b :: linordered_semidom" 

14 
assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0" 

15 
shows "sum f A \<le> (\<Prod>x\<in>A. 1 + f x)" 

16 
using assms 

17 
proof (induction A rule: infinite_finite_induct) 

18 
case (insert x A) 

19 
from insert.hyps have "sum f A + f x * (\<Prod>x\<in>A. 1) \<le> (\<Prod>x\<in>A. 1 + f x) + f x * (\<Prod>x\<in>A. 1 + f x)" 

20 
by (intro add_mono insert mult_left_mono prod_mono) (auto intro: insert.prems) 

21 
with insert.hyps show ?case by (simp add: algebra_simps) 

22 
qed simp_all 

23 

24 
lemma prod_le_exp_sum: 

25 
fixes f :: "'a \<Rightarrow> real" 

26 
assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0" 

27 
shows "prod (\<lambda>x. 1 + f x) A \<le> exp (sum f A)" 

28 
using assms 

29 
proof (induction A rule: infinite_finite_induct) 

30 
case (insert x A) 

31 
have "(1 + f x) * (\<Prod>x\<in>A. 1 + f x) \<le> exp (f x) * exp (sum f A)" 

32 
using insert.prems by (intro mult_mono insert prod_nonneg exp_ge_add_one_self) auto 

33 
with insert.hyps show ?case by (simp add: algebra_simps exp_add) 

34 
qed simp_all 

35 

36 
lemma lim_ln_1_plus_x_over_x_at_0: "(\<lambda>x::real. ln (1 + x) / x) \<midarrow>0\<rightarrow> 1" 

37 
proof (rule lhopital) 

38 
show "(\<lambda>x::real. ln (1 + x)) \<midarrow>0\<rightarrow> 0" 

39 
by (rule tendsto_eq_intros refl  simp)+ 

40 
have "eventually (\<lambda>x::real. x \<in> {1/2<..<1/2}) (nhds 0)" 

41 
by (rule eventually_nhds_in_open) auto 

42 
hence *: "eventually (\<lambda>x::real. x \<in> {1/2<..<1/2}) (at 0)" 

43 
by (rule filter_leD [rotated]) (simp_all add: at_within_def) 

44 
show "eventually (\<lambda>x::real. ((\<lambda>x. ln (1 + x)) has_field_derivative inverse (1 + x)) (at x)) (at 0)" 

45 
using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps) 

46 
show "eventually (\<lambda>x::real. ((\<lambda>x. x) has_field_derivative 1) (at x)) (at 0)" 

47 
using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps) 

48 
show "\<forall>\<^sub>F x in at 0. x \<noteq> 0" by (auto simp: at_within_def eventually_inf_principal) 

49 
show "(\<lambda>x::real. inverse (1 + x) / 1) \<midarrow>0\<rightarrow> 1" 

50 
by (rule tendsto_eq_intros refl  simp)+ 

51 
qed auto 

52 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

53 
definition gen_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

54 
where "gen_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

55 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

56 
text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close> 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

57 
definition has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

58 
where "f has_prod p \<equiv> gen_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> gen_has_prod f (Suc i) q)" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

59 

66277  60 
definition convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where 
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

61 
"convergent_prod f \<equiv> \<exists>M p. gen_has_prod f M p" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

62 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

63 
definition prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

64 
(binder "\<Prod>" 10) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

65 
where "prodinf f = (THE p. f has_prod p)" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

66 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

67 
lemmas prod_defs = gen_has_prod_def has_prod_def convergent_prod_def prodinf_def 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

68 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

69 
lemma has_prod_subst[trans]: "f = g \<Longrightarrow> g has_prod z \<Longrightarrow> f has_prod z" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

70 
by simp 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

71 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

72 
lemma has_prod_cong: "(\<And>n. f n = g n) \<Longrightarrow> f has_prod c \<longleftrightarrow> g has_prod c" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

73 
by presburger 
66277  74 

68071  75 
lemma gen_has_prod_nonzero [simp]: "\<not> gen_has_prod f M 0" 
76 
by (simp add: gen_has_prod_def) 

77 

68136  78 
lemma gen_has_prod_eq_0: 
79 
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" 

80 
assumes p: "gen_has_prod f m p" and i: "f i = 0" "i \<ge> m" 

81 
shows "p = 0" 

82 
proof  

83 
have eq0: "(\<Prod>k\<le>n. f (k+m)) = 0" if "i  m \<le> n" for n 

84 
by (metis i that atMost_atLeast0 atMost_iff diff_add finite_atLeastAtMost prod_zero_iff) 

85 
have "(\<lambda>n. \<Prod>i\<le>n. f (i + m)) \<longlonglongrightarrow> 0" 

86 
by (rule LIMSEQ_offset [where k = "im"]) (simp add: eq0) 

87 
with p show ?thesis 

88 
unfolding gen_has_prod_def 

89 
using LIMSEQ_unique by blast 

90 
qed 

91 

68071  92 
lemma has_prod_0_iff: "f has_prod 0 \<longleftrightarrow> (\<exists>i. f i = 0 \<and> (\<exists>p. gen_has_prod f (Suc i) p))" 
93 
by (simp add: has_prod_def) 

68136  94 

95 
lemma has_prod_unique2: 

96 
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" 

97 
assumes "f has_prod a" "f has_prod b" shows "a = b" 

98 
using assms 

99 
by (auto simp: has_prod_def gen_has_prod_eq_0) (meson gen_has_prod_def sequentially_bot tendsto_unique) 

100 

101 
lemma has_prod_unique: 

102 
fixes f :: "nat \<Rightarrow> 'a :: {idom,t2_space}" 

103 
shows "f has_prod s \<Longrightarrow> s = prodinf f" 

104 
by (simp add: has_prod_unique2 prodinf_def the_equality) 

68071  105 

66277  106 
lemma convergent_prod_altdef: 
107 
fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}" 

108 
shows "convergent_prod f \<longleftrightarrow> (\<exists>M L. (\<forall>n\<ge>M. f n \<noteq> 0) \<and> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L \<and> L \<noteq> 0)" 

109 
proof 

110 
assume "convergent_prod f" 

111 
then obtain M L where *: "(\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L" "L \<noteq> 0" 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

112 
by (auto simp: prod_defs) 
66277  113 
have "f i \<noteq> 0" if "i \<ge> M" for i 
114 
proof 

115 
assume "f i = 0" 

116 
have **: "eventually (\<lambda>n. (\<Prod>i\<le>n. f (i+M)) = 0) sequentially" 

117 
using eventually_ge_at_top[of "i  M"] 

118 
proof eventually_elim 

119 
case (elim n) 

120 
with \<open>f i = 0\<close> and \<open>i \<ge> M\<close> show ?case 

121 
by (auto intro!: bexI[of _ "i  M"] prod_zero) 

122 
qed 

123 
have "(\<lambda>n. (\<Prod>i\<le>n. f (i+M))) \<longlonglongrightarrow> 0" 

124 
unfolding filterlim_iff 

125 
by (auto dest!: eventually_nhds_x_imp_x intro!: eventually_mono[OF **]) 

126 
from tendsto_unique[OF _ this *(1)] and *(2) 

127 
show False by simp 

128 
qed 

129 
with * show "(\<exists>M L. (\<forall>n\<ge>M. f n \<noteq> 0) \<and> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L \<and> L \<noteq> 0)" 

130 
by blast 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

131 
qed (auto simp: prod_defs) 
66277  132 

133 
definition abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where 

134 
"abs_convergent_prod f \<longleftrightarrow> convergent_prod (\<lambda>i. 1 + norm (f i  1))" 

135 

136 
lemma abs_convergent_prodI: 

137 
assumes "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i  1))" 

138 
shows "abs_convergent_prod f" 

139 
proof  

140 
from assms obtain L where L: "(\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i  1)) \<longlonglongrightarrow> L" 

141 
by (auto simp: convergent_def) 

142 
have "L \<ge> 1" 

143 
proof (rule tendsto_le) 

144 
show "eventually (\<lambda>n. (\<Prod>i\<le>n. 1 + norm (f i  1)) \<ge> 1) sequentially" 

145 
proof (intro always_eventually allI) 

146 
fix n 

147 
have "(\<Prod>i\<le>n. 1 + norm (f i  1)) \<ge> (\<Prod>i\<le>n. 1)" 

148 
by (intro prod_mono) auto 

149 
thus "(\<Prod>i\<le>n. 1 + norm (f i  1)) \<ge> 1" by simp 

150 
qed 

151 
qed (use L in simp_all) 

152 
hence "L \<noteq> 0" by auto 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

153 
with L show ?thesis unfolding abs_convergent_prod_def prod_defs 
66277  154 
by (intro exI[of _ "0::nat"] exI[of _ L]) auto 
155 
qed 

156 

157 
lemma 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

158 
fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}" 
66277  159 
assumes "convergent_prod f" 
160 
shows convergent_prod_imp_convergent: "convergent (\<lambda>n. \<Prod>i\<le>n. f i)" 

161 
and convergent_prod_to_zero_iff: "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)" 

162 
proof  

163 
from assms obtain M L 

164 
where M: "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0" and "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> L" and "L \<noteq> 0" 

165 
by (auto simp: convergent_prod_altdef) 

166 
note this(2) 

167 
also have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) = (\<lambda>n. \<Prod>i=M..M+n. f i)" 

168 
by (intro ext prod.reindex_bij_witness[of _ "\<lambda>n. n  M" "\<lambda>n. n + M"]) auto 

169 
finally have "(\<lambda>n. (\<Prod>i<M. f i) * (\<Prod>i=M..M+n. f i)) \<longlonglongrightarrow> (\<Prod>i<M. f i) * L" 

170 
by (intro tendsto_mult tendsto_const) 

171 
also have "(\<lambda>n. (\<Prod>i<M. f i) * (\<Prod>i=M..M+n. f i)) = (\<lambda>n. (\<Prod>i\<in>{..<M}\<union>{M..M+n}. f i))" 

172 
by (subst prod.union_disjoint) auto 

173 
also have "(\<lambda>n. {..<M} \<union> {M..M+n}) = (\<lambda>n. {..n+M})" by auto 

174 
finally have lim: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * L" 

175 
by (rule LIMSEQ_offset) 

176 
thus "convergent (\<lambda>n. \<Prod>i\<le>n. f i)" 

177 
by (auto simp: convergent_def) 

178 

179 
show "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)" 

180 
proof 

181 
assume "\<exists>i. f i = 0" 

182 
then obtain i where "f i = 0" by auto 

183 
moreover with M have "i < M" by (cases "i < M") auto 

184 
ultimately have "(\<Prod>i<M. f i) = 0" by auto 

185 
with lim show "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0" by simp 

186 
next 

187 
assume "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0" 

188 
from tendsto_unique[OF _ this lim] and \<open>L \<noteq> 0\<close> 

189 
show "\<exists>i. f i = 0" by auto 

190 
qed 

191 
qed 

192 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

193 
lemma convergent_prod_iff_nz_lim: 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

194 
fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

195 
assumes "\<And>i. f i \<noteq> 0" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

196 
shows "convergent_prod f \<longleftrightarrow> (\<exists>L. (\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> L \<and> L \<noteq> 0)" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

197 
(is "?lhs \<longleftrightarrow> ?rhs") 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

198 
proof 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

199 
assume ?lhs then show ?rhs 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

200 
using assms convergentD convergent_prod_imp_convergent convergent_prod_to_zero_iff by blast 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

201 
next 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

202 
assume ?rhs then show ?lhs 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

203 
unfolding prod_defs 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

204 
by (rule_tac x="0" in exI) (auto simp: ) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

205 
qed 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

206 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

207 
lemma convergent_prod_iff_convergent: 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

208 
fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

209 
assumes "\<And>i. f i \<noteq> 0" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

210 
shows "convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. f i) \<and> lim (\<lambda>n. \<Prod>i\<le>n. f i) \<noteq> 0" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

211 
by (force simp add: convergent_prod_iff_nz_lim assms convergent_def limI) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

212 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

213 

66277  214 
lemma abs_convergent_prod_altdef: 
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

215 
fixes f :: "nat \<Rightarrow> 'a :: {one,real_normed_vector}" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

216 
shows "abs_convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i  1))" 
66277  217 
proof 
218 
assume "abs_convergent_prod f" 

219 
thus "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i  1))" 

220 
by (auto simp: abs_convergent_prod_def intro!: convergent_prod_imp_convergent) 

221 
qed (auto intro: abs_convergent_prodI) 

222 

223 
lemma weierstrass_prod_ineq: 

224 
fixes f :: "'a \<Rightarrow> real" 

225 
assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> {0..1}" 

226 
shows "1  sum f A \<le> (\<Prod>x\<in>A. 1  f x)" 

227 
using assms 

228 
proof (induction A rule: infinite_finite_induct) 

229 
case (insert x A) 

230 
from insert.hyps and insert.prems 

231 
have "1  sum f A + f x * (\<Prod>x\<in>A. 1  f x) \<le> (\<Prod>x\<in>A. 1  f x) + f x * (\<Prod>x\<in>A. 1)" 

232 
by (intro insert.IH add_mono mult_left_mono prod_mono) auto 

233 
with insert.hyps show ?case by (simp add: algebra_simps) 

234 
qed simp_all 

235 

236 
lemma norm_prod_minus1_le_prod_minus1: 

237 
fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,comm_ring_1}" 

238 
shows "norm (prod (\<lambda>n. 1 + f n) A  1) \<le> prod (\<lambda>n. 1 + norm (f n)) A  1" 

239 
proof (induction A rule: infinite_finite_induct) 

240 
case (insert x A) 

241 
from insert.hyps have 

242 
"norm ((\<Prod>n\<in>insert x A. 1 + f n)  1) = 

243 
norm ((\<Prod>n\<in>A. 1 + f n)  1 + f x * (\<Prod>n\<in>A. 1 + f n))" 

244 
by (simp add: algebra_simps) 

245 
also have "\<dots> \<le> norm ((\<Prod>n\<in>A. 1 + f n)  1) + norm (f x * (\<Prod>n\<in>A. 1 + f n))" 

246 
by (rule norm_triangle_ineq) 

247 
also have "norm (f x * (\<Prod>n\<in>A. 1 + f n)) = norm (f x) * (\<Prod>x\<in>A. norm (1 + f x))" 

248 
by (simp add: prod_norm norm_mult) 

249 
also have "(\<Prod>x\<in>A. norm (1 + f x)) \<le> (\<Prod>x\<in>A. norm (1::'a) + norm (f x))" 

250 
by (intro prod_mono norm_triangle_ineq ballI conjI) auto 

251 
also have "norm (1::'a) = 1" by simp 

252 
also note insert.IH 

253 
also have "(\<Prod>n\<in>A. 1 + norm (f n))  1 + norm (f x) * (\<Prod>x\<in>A. 1 + norm (f x)) = 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

254 
(\<Prod>n\<in>insert x A. 1 + norm (f n))  1" 
66277  255 
using insert.hyps by (simp add: algebra_simps) 
256 
finally show ?case by  (simp_all add: mult_left_mono) 

257 
qed simp_all 

258 

259 
lemma convergent_prod_imp_ev_nonzero: 

260 
fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}" 

261 
assumes "convergent_prod f" 

262 
shows "eventually (\<lambda>n. f n \<noteq> 0) sequentially" 

263 
using assms by (auto simp: eventually_at_top_linorder convergent_prod_altdef) 

264 

265 
lemma convergent_prod_imp_LIMSEQ: 

266 
fixes f :: "nat \<Rightarrow> 'a :: {real_normed_field}" 

267 
assumes "convergent_prod f" 

268 
shows "f \<longlonglongrightarrow> 1" 

269 
proof  

270 
from assms obtain M L where L: "(\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L" "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0" "L \<noteq> 0" 

271 
by (auto simp: convergent_prod_altdef) 

272 
hence L': "(\<lambda>n. \<Prod>i\<le>Suc n. f (i+M)) \<longlonglongrightarrow> L" by (subst filterlim_sequentially_Suc) 

273 
have "(\<lambda>n. (\<Prod>i\<le>Suc n. f (i+M)) / (\<Prod>i\<le>n. f (i+M))) \<longlonglongrightarrow> L / L" 

274 
using L L' by (intro tendsto_divide) simp_all 

275 
also from L have "L / L = 1" by simp 

276 
also have "(\<lambda>n. (\<Prod>i\<le>Suc n. f (i+M)) / (\<Prod>i\<le>n. f (i+M))) = (\<lambda>n. f (n + Suc M))" 

277 
using assms L by (auto simp: fun_eq_iff atMost_Suc) 

278 
finally show ?thesis by (rule LIMSEQ_offset) 

279 
qed 

280 

281 
lemma abs_convergent_prod_imp_summable: 

282 
fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra" 

283 
assumes "abs_convergent_prod f" 

284 
shows "summable (\<lambda>i. norm (f i  1))" 

285 
proof  

286 
from assms have "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i  1))" 

287 
unfolding abs_convergent_prod_def by (rule convergent_prod_imp_convergent) 

288 
then obtain L where L: "(\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i  1)) \<longlonglongrightarrow> L" 

289 
unfolding convergent_def by blast 

290 
have "convergent (\<lambda>n. \<Sum>i\<le>n. norm (f i  1))" 

291 
proof (rule Bseq_monoseq_convergent) 

292 
have "eventually (\<lambda>n. (\<Prod>i\<le>n. 1 + norm (f i  1)) < L + 1) sequentially" 

293 
using L(1) by (rule order_tendstoD) simp_all 

294 
hence "\<forall>\<^sub>F x in sequentially. norm (\<Sum>i\<le>x. norm (f i  1)) \<le> L + 1" 

295 
proof eventually_elim 

296 
case (elim n) 

297 
have "norm (\<Sum>i\<le>n. norm (f i  1)) = (\<Sum>i\<le>n. norm (f i  1))" 

298 
unfolding real_norm_def by (intro abs_of_nonneg sum_nonneg) simp_all 

299 
also have "\<dots> \<le> (\<Prod>i\<le>n. 1 + norm (f i  1))" by (rule sum_le_prod) auto 

300 
also have "\<dots> < L + 1" by (rule elim) 

301 
finally show ?case by simp 

302 
qed 

303 
thus "Bseq (\<lambda>n. \<Sum>i\<le>n. norm (f i  1))" by (rule BfunI) 

304 
next 

305 
show "monoseq (\<lambda>n. \<Sum>i\<le>n. norm (f i  1))" 

306 
by (rule mono_SucI1) auto 

307 
qed 

308 
thus "summable (\<lambda>i. norm (f i  1))" by (simp add: summable_iff_convergent') 

309 
qed 

310 

311 
lemma summable_imp_abs_convergent_prod: 

312 
fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra" 

313 
assumes "summable (\<lambda>i. norm (f i  1))" 

314 
shows "abs_convergent_prod f" 

315 
proof (intro abs_convergent_prodI Bseq_monoseq_convergent) 

316 
show "monoseq (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i  1))" 

317 
by (intro mono_SucI1) 

318 
(auto simp: atMost_Suc algebra_simps intro!: mult_nonneg_nonneg prod_nonneg) 

319 
next 

320 
show "Bseq (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i  1))" 

321 
proof (rule Bseq_eventually_mono) 

322 
show "eventually (\<lambda>n. norm (\<Prod>i\<le>n. 1 + norm (f i  1)) \<le> 

323 
norm (exp (\<Sum>i\<le>n. norm (f i  1)))) sequentially" 

324 
by (intro always_eventually allI) (auto simp: abs_prod exp_sum intro!: prod_mono) 

325 
next 

326 
from assms have "(\<lambda>n. \<Sum>i\<le>n. norm (f i  1)) \<longlonglongrightarrow> (\<Sum>i. norm (f i  1))" 

327 
using sums_def_le by blast 

328 
hence "(\<lambda>n. exp (\<Sum>i\<le>n. norm (f i  1))) \<longlonglongrightarrow> exp (\<Sum>i. norm (f i  1))" 

329 
by (rule tendsto_exp) 

330 
hence "convergent (\<lambda>n. exp (\<Sum>i\<le>n. norm (f i  1)))" 

331 
by (rule convergentI) 

332 
thus "Bseq (\<lambda>n. exp (\<Sum>i\<le>n. norm (f i  1)))" 

333 
by (rule convergent_imp_Bseq) 

334 
qed 

335 
qed 

336 

337 
lemma abs_convergent_prod_conv_summable: 

338 
fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra" 

339 
shows "abs_convergent_prod f \<longleftrightarrow> summable (\<lambda>i. norm (f i  1))" 

340 
by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod) 

341 

342 
lemma abs_convergent_prod_imp_LIMSEQ: 

343 
fixes f :: "nat \<Rightarrow> 'a :: {comm_ring_1,real_normed_div_algebra}" 

344 
assumes "abs_convergent_prod f" 

345 
shows "f \<longlonglongrightarrow> 1" 

346 
proof  

347 
from assms have "summable (\<lambda>n. norm (f n  1))" 

348 
by (rule abs_convergent_prod_imp_summable) 

349 
from summable_LIMSEQ_zero[OF this] have "(\<lambda>n. f n  1) \<longlonglongrightarrow> 0" 

350 
by (simp add: tendsto_norm_zero_iff) 

351 
from tendsto_add[OF this tendsto_const[of 1]] show ?thesis by simp 

352 
qed 

353 

354 
lemma abs_convergent_prod_imp_ev_nonzero: 

355 
fixes f :: "nat \<Rightarrow> 'a :: {comm_ring_1,real_normed_div_algebra}" 

356 
assumes "abs_convergent_prod f" 

357 
shows "eventually (\<lambda>n. f n \<noteq> 0) sequentially" 

358 
proof  

359 
from assms have "f \<longlonglongrightarrow> 1" 

360 
by (rule abs_convergent_prod_imp_LIMSEQ) 

361 
hence "eventually (\<lambda>n. dist (f n) 1 < 1) at_top" 

362 
by (auto simp: tendsto_iff) 

363 
thus ?thesis by eventually_elim auto 

364 
qed 

365 

366 
lemma convergent_prod_offset: 

367 
assumes "convergent_prod (\<lambda>n. f (n + m))" 

368 
shows "convergent_prod f" 

369 
proof  

370 
from assms obtain M L where "(\<lambda>n. \<Prod>k\<le>n. f (k + (M + m))) \<longlonglongrightarrow> L" "L \<noteq> 0" 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

371 
by (auto simp: prod_defs add.assoc) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

372 
thus "convergent_prod f" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

373 
unfolding prod_defs by blast 
66277  374 
qed 
375 

376 
lemma abs_convergent_prod_offset: 

377 
assumes "abs_convergent_prod (\<lambda>n. f (n + m))" 

378 
shows "abs_convergent_prod f" 

379 
using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset) 

380 

381 
lemma convergent_prod_ignore_initial_segment: 

382 
fixes f :: "nat \<Rightarrow> 'a :: {real_normed_field}" 

383 
assumes "convergent_prod f" 

384 
shows "convergent_prod (\<lambda>n. f (n + m))" 

385 
proof  

386 
from assms obtain M L 

387 
where L: "(\<lambda>n. \<Prod>k\<le>n. f (k + M)) \<longlonglongrightarrow> L" "L \<noteq> 0" and nz: "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0" 

388 
by (auto simp: convergent_prod_altdef) 

389 
define C where "C = (\<Prod>k<m. f (k + M))" 

390 
from nz have [simp]: "C \<noteq> 0" 

391 
by (auto simp: C_def) 

392 

393 
from L(1) have "(\<lambda>n. \<Prod>k\<le>n+m. f (k + M)) \<longlonglongrightarrow> L" 

394 
by (rule LIMSEQ_ignore_initial_segment) 

395 
also have "(\<lambda>n. \<Prod>k\<le>n+m. f (k + M)) = (\<lambda>n. C * (\<Prod>k\<le>n. f (k + M + m)))" 

396 
proof (rule ext, goal_cases) 

397 
case (1 n) 

398 
have "{..n+m} = {..<m} \<union> {m..n+m}" by auto 

399 
also have "(\<Prod>k\<in>\<dots>. f (k + M)) = C * (\<Prod>k=m..n+m. f (k + M))" 

400 
unfolding C_def by (rule prod.union_disjoint) auto 

401 
also have "(\<Prod>k=m..n+m. f (k + M)) = (\<Prod>k\<le>n. f (k + m + M))" 

402 
by (intro ext prod.reindex_bij_witness[of _ "\<lambda>k. k + m" "\<lambda>k. k  m"]) auto 

403 
finally show ?case by (simp add: add_ac) 

404 
qed 

405 
finally have "(\<lambda>n. C * (\<Prod>k\<le>n. f (k + M + m)) / C) \<longlonglongrightarrow> L / C" 

406 
by (intro tendsto_divide tendsto_const) auto 

407 
hence "(\<lambda>n. \<Prod>k\<le>n. f (k + M + m)) \<longlonglongrightarrow> L / C" by simp 

408 
moreover from \<open>L \<noteq> 0\<close> have "L / C \<noteq> 0" by simp 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

409 
ultimately show ?thesis 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

410 
unfolding prod_defs by blast 
66277  411 
qed 
412 

68136  413 
corollary convergent_prod_ignore_nonzero_segment: 
414 
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" 

415 
assumes f: "convergent_prod f" and nz: "\<And>i. i \<ge> M \<Longrightarrow> f i \<noteq> 0" 

416 
shows "\<exists>p. gen_has_prod f M p" 

417 
using convergent_prod_ignore_initial_segment [OF f] 

418 
by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1)) 

419 

420 
corollary abs_convergent_prod_ignore_initial_segment: 

66277  421 
assumes "abs_convergent_prod f" 
422 
shows "abs_convergent_prod (\<lambda>n. f (n + m))" 

423 
using assms unfolding abs_convergent_prod_def 

424 
by (rule convergent_prod_ignore_initial_segment) 

425 

426 
lemma abs_convergent_prod_imp_convergent_prod: 

427 
fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}" 

428 
assumes "abs_convergent_prod f" 

429 
shows "convergent_prod f" 

430 
proof  

431 
from assms have "eventually (\<lambda>n. f n \<noteq> 0) sequentially" 

432 
by (rule abs_convergent_prod_imp_ev_nonzero) 

433 
then obtain N where N: "f n \<noteq> 0" if "n \<ge> N" for n 

434 
by (auto simp: eventually_at_top_linorder) 

435 
let ?P = "\<lambda>n. \<Prod>i\<le>n. f (i + N)" and ?Q = "\<lambda>n. \<Prod>i\<le>n. 1 + norm (f (i + N)  1)" 

436 

437 
have "Cauchy ?P" 

438 
proof (rule CauchyI', goal_cases) 

439 
case (1 \<epsilon>) 

440 
from assms have "abs_convergent_prod (\<lambda>n. f (n + N))" 

441 
by (rule abs_convergent_prod_ignore_initial_segment) 

442 
hence "Cauchy ?Q" 

443 
unfolding abs_convergent_prod_def 

444 
by (intro convergent_Cauchy convergent_prod_imp_convergent) 

445 
from CauchyD[OF this 1] obtain M where M: "norm (?Q m  ?Q n) < \<epsilon>" if "m \<ge> M" "n \<ge> M" for m n 

446 
by blast 

447 
show ?case 

448 
proof (rule exI[of _ M], safe, goal_cases) 

449 
case (1 m n) 

450 
have "dist (?P m) (?P n) = norm (?P n  ?P m)" 

451 
by (simp add: dist_norm norm_minus_commute) 

452 
also from 1 have "{..n} = {..m} \<union> {m<..n}" by auto 

453 
hence "norm (?P n  ?P m) = norm (?P m * (\<Prod>k\<in>{m<..n}. f (k + N))  ?P m)" 

454 
by (subst prod.union_disjoint [symmetric]) (auto simp: algebra_simps) 

455 
also have "\<dots> = norm (?P m * ((\<Prod>k\<in>{m<..n}. f (k + N))  1))" 

456 
by (simp add: algebra_simps) 

457 
also have "\<dots> = (\<Prod>k\<le>m. norm (f (k + N))) * norm ((\<Prod>k\<in>{m<..n}. f (k + N))  1)" 

458 
by (simp add: norm_mult prod_norm) 

459 
also have "\<dots> \<le> ?Q m * ((\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N)  1))  1)" 

460 
using norm_prod_minus1_le_prod_minus1[of "\<lambda>k. f (k + N)  1" "{m<..n}"] 

461 
norm_triangle_ineq[of 1 "f k  1" for k] 

462 
by (intro mult_mono prod_mono ballI conjI norm_prod_minus1_le_prod_minus1 prod_nonneg) auto 

463 
also have "\<dots> = ?Q m * (\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N)  1))  ?Q m" 

464 
by (simp add: algebra_simps) 

465 
also have "?Q m * (\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N)  1)) = 

466 
(\<Prod>k\<in>{..m}\<union>{m<..n}. 1 + norm (f (k + N)  1))" 

467 
by (rule prod.union_disjoint [symmetric]) auto 

468 
also from 1 have "{..m}\<union>{m<..n} = {..n}" by auto 

469 
also have "?Q n  ?Q m \<le> norm (?Q n  ?Q m)" by simp 

470 
also from 1 have "\<dots> < \<epsilon>" by (intro M) auto 

471 
finally show ?case . 

472 
qed 

473 
qed 

474 
hence conv: "convergent ?P" by (rule Cauchy_convergent) 

475 
then obtain L where L: "?P \<longlonglongrightarrow> L" 

476 
by (auto simp: convergent_def) 

477 

478 
have "L \<noteq> 0" 

479 
proof 

480 
assume [simp]: "L = 0" 

481 
from tendsto_norm[OF L] have limit: "(\<lambda>n. \<Prod>k\<le>n. norm (f (k + N))) \<longlonglongrightarrow> 0" 

482 
by (simp add: prod_norm) 

483 

484 
from assms have "(\<lambda>n. f (n + N)) \<longlonglongrightarrow> 1" 

485 
by (intro abs_convergent_prod_imp_LIMSEQ abs_convergent_prod_ignore_initial_segment) 

486 
hence "eventually (\<lambda>n. norm (f (n + N)  1) < 1) sequentially" 

487 
by (auto simp: tendsto_iff dist_norm) 

488 
then obtain M0 where M0: "norm (f (n + N)  1) < 1" if "n \<ge> M0" for n 

489 
by (auto simp: eventually_at_top_linorder) 

490 

491 
{ 

492 
fix M assume M: "M \<ge> M0" 

493 
with M0 have M: "norm (f (n + N)  1) < 1" if "n \<ge> M" for n using that by simp 

494 

495 
have "(\<lambda>n. \<Prod>k\<le>n. 1  norm (f (k+M+N)  1)) \<longlonglongrightarrow> 0" 

496 
proof (rule tendsto_sandwich) 

497 
show "eventually (\<lambda>n. (\<Prod>k\<le>n. 1  norm (f (k+M+N)  1)) \<ge> 0) sequentially" 

498 
using M by (intro always_eventually prod_nonneg allI ballI) (auto intro: less_imp_le) 

499 
have "norm (1::'a)  norm (f (i + M + N)  1) \<le> norm (f (i + M + N))" for i 

500 
using norm_triangle_ineq3[of "f (i + M + N)" 1] by simp 

501 
thus "eventually (\<lambda>n. (\<Prod>k\<le>n. 1  norm (f (k+M+N)  1)) \<le> (\<Prod>k\<le>n. norm (f (k+M+N)))) at_top" 

502 
using M by (intro always_eventually allI prod_mono ballI conjI) (auto intro: less_imp_le) 

503 

504 
define C where "C = (\<Prod>k<M. norm (f (k + N)))" 

505 
from N have [simp]: "C \<noteq> 0" by (auto simp: C_def) 

506 
from L have "(\<lambda>n. norm (\<Prod>k\<le>n+M. f (k + N))) \<longlonglongrightarrow> 0" 

507 
by (intro LIMSEQ_ignore_initial_segment) (simp add: tendsto_norm_zero_iff) 

508 
also have "(\<lambda>n. norm (\<Prod>k\<le>n+M. f (k + N))) = (\<lambda>n. C * (\<Prod>k\<le>n. norm (f (k + M + N))))" 

509 
proof (rule ext, goal_cases) 

510 
case (1 n) 

511 
have "{..n+M} = {..<M} \<union> {M..n+M}" by auto 

512 
also have "norm (\<Prod>k\<in>\<dots>. f (k + N)) = C * norm (\<Prod>k=M..n+M. f (k + N))" 

513 
unfolding C_def by (subst prod.union_disjoint) (auto simp: norm_mult prod_norm) 

514 
also have "(\<Prod>k=M..n+M. f (k + N)) = (\<Prod>k\<le>n. f (k + N + M))" 

515 
by (intro prod.reindex_bij_witness[of _ "\<lambda>i. i + M" "\<lambda>i. i  M"]) auto 

516 
finally show ?case by (simp add: add_ac prod_norm) 

517 
qed 

518 
finally have "(\<lambda>n. C * (\<Prod>k\<le>n. norm (f (k + M + N))) / C) \<longlonglongrightarrow> 0 / C" 

519 
by (intro tendsto_divide tendsto_const) auto 

520 
thus "(\<lambda>n. \<Prod>k\<le>n. norm (f (k + M + N))) \<longlonglongrightarrow> 0" by simp 

521 
qed simp_all 

522 

523 
have "1  (\<Sum>i. norm (f (i + M + N)  1)) \<le> 0" 

524 
proof (rule tendsto_le) 

525 
show "eventually (\<lambda>n. 1  (\<Sum>k\<le>n. norm (f (k+M+N)  1)) \<le> 

526 
(\<Prod>k\<le>n. 1  norm (f (k+M+N)  1))) at_top" 

527 
using M by (intro always_eventually allI weierstrass_prod_ineq) (auto intro: less_imp_le) 

528 
show "(\<lambda>n. \<Prod>k\<le>n. 1  norm (f (k+M+N)  1)) \<longlonglongrightarrow> 0" by fact 

529 
show "(\<lambda>n. 1  (\<Sum>k\<le>n. norm (f (k + M + N)  1))) 

530 
\<longlonglongrightarrow> 1  (\<Sum>i. norm (f (i + M + N)  1))" 

531 
by (intro tendsto_intros summable_LIMSEQ' summable_ignore_initial_segment 

532 
abs_convergent_prod_imp_summable assms) 

533 
qed simp_all 

534 
hence "(\<Sum>i. norm (f (i + M + N)  1)) \<ge> 1" by simp 

535 
also have "\<dots> + (\<Sum>i<M. norm (f (i + N)  1)) = (\<Sum>i. norm (f (i + N)  1))" 

536 
by (intro suminf_split_initial_segment [symmetric] summable_ignore_initial_segment 

537 
abs_convergent_prod_imp_summable assms) 

538 
finally have "1 + (\<Sum>i<M. norm (f (i + N)  1)) \<le> (\<Sum>i. norm (f (i + N)  1))" by simp 

539 
} note * = this 

540 

541 
have "1 + (\<Sum>i. norm (f (i + N)  1)) \<le> (\<Sum>i. norm (f (i + N)  1))" 

542 
proof (rule tendsto_le) 

543 
show "(\<lambda>M. 1 + (\<Sum>i<M. norm (f (i + N)  1))) \<longlonglongrightarrow> 1 + (\<Sum>i. norm (f (i + N)  1))" 

544 
by (intro tendsto_intros summable_LIMSEQ summable_ignore_initial_segment 

545 
abs_convergent_prod_imp_summable assms) 

546 
show "eventually (\<lambda>M. 1 + (\<Sum>i<M. norm (f (i + N)  1)) \<le> (\<Sum>i. norm (f (i + N)  1))) at_top" 

547 
using eventually_ge_at_top[of M0] by eventually_elim (use * in auto) 

548 
qed simp_all 

549 
thus False by simp 

550 
qed 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

551 
with L show ?thesis by (auto simp: prod_defs) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

552 
qed 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

553 

68136  554 
lemma gen_has_prod_cases: 
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

555 
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}" 
68136  556 
assumes "gen_has_prod f M p" 
557 
obtains i where "i<M" "f i = 0"  p where "gen_has_prod f 0 p" 

558 
proof  

559 
have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0" 

560 
using assms unfolding gen_has_prod_def by blast+ 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

561 
then have "(\<lambda>n. prod f {..<M} * (\<Prod>i\<le>n. f (i + M))) \<longlonglongrightarrow> prod f {..<M} * p" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

562 
by (metis tendsto_mult_left) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

563 
moreover have "prod f {..<M} * (\<Prod>i\<le>n. f (i + M)) = prod f {..n+M}" for n 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

564 
proof  
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

565 
have "{..n+M} = {..<M} \<union> {M..n+M}" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

566 
by auto 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

567 
then have "prod f {..n+M} = prod f {..<M} * prod f {M..n+M}" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

568 
by simp (subst prod.union_disjoint; force) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

569 
also have "... = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

570 
by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod_shift_bounds_cl_nat_ivl) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

571 
finally show ?thesis by metis 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

572 
qed 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

573 
ultimately have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * p" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

574 
by (auto intro: LIMSEQ_offset [where k=M]) 
68136  575 
then have "gen_has_prod f 0 (prod f {..<M} * p)" if "\<forall>i<M. f i \<noteq> 0" 
576 
using \<open>p \<noteq> 0\<close> assms that by (auto simp: gen_has_prod_def) 

577 
then show thesis 

578 
using that by blast 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

579 
qed 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

580 

68136  581 
corollary convergent_prod_offset_0: 
582 
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}" 

583 
assumes "convergent_prod f" "\<And>i. f i \<noteq> 0" 

584 
shows "\<exists>p. gen_has_prod f 0 p" 

585 
using assms convergent_prod_def gen_has_prod_cases by blast 

586 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

587 
lemma prodinf_eq_lim: 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

588 
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

589 
assumes "convergent_prod f" "\<And>i. f i \<noteq> 0" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

590 
shows "prodinf f = lim (\<lambda>n. \<Prod>i\<le>n. f i)" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

591 
using assms convergent_prod_offset_0 [OF assms] 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

592 
by (simp add: prod_defs lim_def) (metis (no_types) assms(1) convergent_prod_to_zero_iff) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

593 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

594 
lemma has_prod_one[simp, intro]: "(\<lambda>n. 1) has_prod 1" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

595 
unfolding prod_defs by auto 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

596 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

597 
lemma convergent_prod_one[simp, intro]: "convergent_prod (\<lambda>n. 1)" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

598 
unfolding prod_defs by auto 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

599 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

600 
lemma prodinf_cong: "(\<And>n. f n = g n) \<Longrightarrow> prodinf f = prodinf g" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

601 
by presburger 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

602 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

603 
lemma convergent_prod_cong: 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

604 
fixes f g :: "nat \<Rightarrow> 'a::{field,topological_semigroup_mult,t2_space}" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

605 
assumes ev: "eventually (\<lambda>x. f x = g x) sequentially" and f: "\<And>i. f i \<noteq> 0" and g: "\<And>i. g i \<noteq> 0" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

606 
shows "convergent_prod f = convergent_prod g" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

607 
proof  
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

608 
from assms obtain N where N: "\<forall>n\<ge>N. f n = g n" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

609 
by (auto simp: eventually_at_top_linorder) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

610 
define C where "C = (\<Prod>k<N. f k / g k)" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

611 
with g have "C \<noteq> 0" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

612 
by (simp add: f) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

613 
have *: "eventually (\<lambda>n. prod f {..n} = C * prod g {..n}) sequentially" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

614 
using eventually_ge_at_top[of N] 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

615 
proof eventually_elim 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

616 
case (elim n) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

617 
then have "{..n} = {..<N} \<union> {N..n}" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

618 
by auto 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

619 
also have "prod f ... = prod f {..<N} * prod f {N..n}" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

620 
by (intro prod.union_disjoint) auto 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

621 
also from N have "prod f {N..n} = prod g {N..n}" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

622 
by (intro prod.cong) simp_all 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

623 
also have "prod f {..<N} * prod g {N..n} = C * (prod g {..<N} * prod g {N..n})" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

624 
unfolding C_def by (simp add: g prod_dividef) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

625 
also have "prod g {..<N} * prod g {N..n} = prod g ({..<N} \<union> {N..n})" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

626 
by (intro prod.union_disjoint [symmetric]) auto 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

627 
also from elim have "{..<N} \<union> {N..n} = {..n}" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

628 
by auto 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

629 
finally show "prod f {..n} = C * prod g {..n}" . 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

630 
qed 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

631 
then have cong: "convergent (\<lambda>n. prod f {..n}) = convergent (\<lambda>n. C * prod g {..n})" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

632 
by (rule convergent_cong) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

633 
show ?thesis 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

634 
proof 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

635 
assume cf: "convergent_prod f" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

636 
then have "\<not> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> 0" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

637 
using tendsto_mult_left * convergent_prod_to_zero_iff f filterlim_cong by fastforce 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

638 
then show "convergent_prod g" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

639 
by (metis convergent_mult_const_iff \<open>C \<noteq> 0\<close> cong cf convergent_LIMSEQ_iff convergent_prod_iff_convergent convergent_prod_imp_convergent g) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

640 
next 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

641 
assume cg: "convergent_prod g" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

642 
have "\<exists>a. C * a \<noteq> 0 \<and> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> a" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

643 
by (metis (no_types) \<open>C \<noteq> 0\<close> cg convergent_prod_iff_nz_lim divide_eq_0_iff g nonzero_mult_div_cancel_right) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

644 
then show "convergent_prod f" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

645 
using "*" tendsto_mult_left filterlim_cong 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

646 
by (fastforce simp add: convergent_prod_iff_nz_lim f) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

647 
qed 
66277  648 
qed 
649 

68071  650 
lemma has_prod_finite: 
651 
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" 

652 
assumes [simp]: "finite N" 

653 
and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1" 

654 
shows "f has_prod (\<Prod>n\<in>N. f n)" 

655 
proof  

656 
have eq: "prod f {..n + Suc (Max N)} = prod f N" for n 

657 
proof (rule prod.mono_neutral_right) 

658 
show "N \<subseteq> {..n + Suc (Max N)}" 

659 
by (auto simp add: le_Suc_eq trans_le_add2) 

660 
show "\<forall>i\<in>{..n + Suc (Max N)}  N. f i = 1" 

661 
using f by blast 

662 
qed auto 

663 
show ?thesis 

664 
proof (cases "\<forall>n\<in>N. f n \<noteq> 0") 

665 
case True 

666 
then have "prod f N \<noteq> 0" 

667 
by simp 

668 
moreover have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f N" 

669 
by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) (simp add: eq atLeast0LessThan del: add_Suc_right) 

670 
ultimately show ?thesis 

671 
by (simp add: gen_has_prod_def has_prod_def) 

672 
next 

673 
case False 

674 
then obtain k where "k \<in> N" "f k = 0" 

675 
by auto 

676 
let ?Z = "{n \<in> N. f n = 0}" 

677 
have maxge: "Max ?Z \<ge> n" if "f n = 0" for n 

678 
using Max_ge [of ?Z] \<open>finite N\<close> \<open>f n = 0\<close> 

679 
by (metis (mono_tags) Collect_mem_eq f finite_Collect_conjI mem_Collect_eq zero_neq_one) 

680 
let ?q = "prod f {Suc (Max ?Z)..Max N}" 

681 
have [simp]: "?q \<noteq> 0" 

682 
using maxge Suc_n_not_le_n le_trans by force 

68076  683 
have eq: "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = ?q" for n 
684 
proof  

685 
have "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = prod f {Suc (Max ?Z)..n + Max N + Suc (Max ?Z)}" 

686 
proof (rule prod.reindex_cong [where l = "\<lambda>i. i + Suc (Max ?Z)", THEN sym]) 

687 
show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\<lambda>i. i + Suc (Max ?Z)) ` {..n + Max N}" 

688 
using le_Suc_ex by fastforce 

689 
qed (auto simp: inj_on_def) 

690 
also have "... = ?q" 

691 
by (rule prod.mono_neutral_right) 

692 
(use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>) 

693 
finally show ?thesis . 

694 
qed 

68071  695 
have q: "gen_has_prod f (Suc (Max ?Z)) ?q" 
68076  696 
proof (simp add: gen_has_prod_def) 
697 
show "(\<lambda>n. \<Prod>i\<le>n. f (Suc (i + Max ?Z))) \<longlonglongrightarrow> ?q" 

698 
by (rule LIMSEQ_offset[of _ "(Max N)"]) (simp add: eq) 

699 
qed 

68071  700 
show ?thesis 
701 
unfolding has_prod_def 

702 
proof (intro disjI2 exI conjI) 

703 
show "prod f N = 0" 

704 
using \<open>f k = 0\<close> \<open>k \<in> N\<close> \<open>finite N\<close> prod_zero by blast 

705 
show "f (Max ?Z) = 0" 

706 
using Max_in [of ?Z] \<open>finite N\<close> \<open>f k = 0\<close> \<open>k \<in> N\<close> by auto 

707 
qed (use q in auto) 

708 
qed 

709 
qed 

710 

711 
corollary has_prod_0: 

712 
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" 

713 
assumes "\<And>n. f n = 1" 

714 
shows "f has_prod 1" 

715 
by (simp add: assms has_prod_cong) 

716 

717 
lemma convergent_prod_finite: 

718 
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" 

719 
assumes "finite N" "\<And>n. n \<notin> N \<Longrightarrow> f n = 1" 

720 
shows "convergent_prod f" 

721 
proof  

722 
have "\<exists>n p. gen_has_prod f n p" 

723 
using assms has_prod_def has_prod_finite by blast 

724 
then show ?thesis 

725 
by (simp add: convergent_prod_def) 

726 
qed 

727 

68127  728 
lemma has_prod_If_finite_set: 
729 
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" 

730 
shows "finite A \<Longrightarrow> (\<lambda>r. if r \<in> A then f r else 1) has_prod (\<Prod>r\<in>A. f r)" 

731 
using has_prod_finite[of A "(\<lambda>r. if r \<in> A then f r else 1)"] 

732 
by simp 

733 

734 
lemma has_prod_If_finite: 

735 
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" 

736 
shows "finite {r. P r} \<Longrightarrow> (\<lambda>r. if P r then f r else 1) has_prod (\<Prod>r  P r. f r)" 

737 
using has_prod_If_finite_set[of "{r. P r}"] by simp 

738 

739 
lemma convergent_prod_If_finite_set[simp, intro]: 

740 
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" 

741 
shows "finite A \<Longrightarrow> convergent_prod (\<lambda>r. if r \<in> A then f r else 1)" 

742 
by (simp add: convergent_prod_finite) 

743 

744 
lemma convergent_prod_If_finite[simp, intro]: 

745 
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" 

746 
shows "finite {r. P r} \<Longrightarrow> convergent_prod (\<lambda>r. if P r then f r else 1)" 

747 
using convergent_prod_def has_prod_If_finite has_prod_def by fastforce 

748 

749 
lemma has_prod_single: 

750 
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" 

751 
shows "(\<lambda>r. if r = i then f r else 1) has_prod f i" 

752 
using has_prod_If_finite[of "\<lambda>r. r = i"] by simp 

753 

68136  754 
context 
755 
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" 

756 
begin 

757 

758 
lemma convergent_prod_imp_has_prod: 

759 
assumes "convergent_prod f" 

760 
shows "\<exists>p. f has_prod p" 

761 
proof  

762 
obtain M p where p: "gen_has_prod f M p" 

763 
using assms convergent_prod_def by blast 

764 
then have "p \<noteq> 0" 

765 
using gen_has_prod_nonzero by blast 

766 
with p have fnz: "f i \<noteq> 0" if "i \<ge> M" for i 

767 
using gen_has_prod_eq_0 that by blast 

768 
define C where "C = (\<Prod>n<M. f n)" 

769 
show ?thesis 

770 
proof (cases "\<forall>n\<le>M. f n \<noteq> 0") 

771 
case True 

772 
then have "C \<noteq> 0" 

773 
by (simp add: C_def) 

774 
then show ?thesis 

775 
by (meson True assms convergent_prod_offset_0 fnz has_prod_def nat_le_linear) 

776 
next 

777 
case False 

778 
let ?N = "GREATEST n. f n = 0" 

779 
have 0: "f ?N = 0" 

780 
using fnz False 

781 
by (metis (mono_tags, lifting) GreatestI_ex_nat nat_le_linear) 

782 
have "f i \<noteq> 0" if "i > ?N" for i 

783 
by (metis (mono_tags, lifting) Greatest_le_nat fnz leD linear that) 

784 
then have "\<exists>p. gen_has_prod f (Suc ?N) p" 

785 
using assms by (auto simp: intro!: convergent_prod_ignore_nonzero_segment) 

786 
then show ?thesis 

787 
unfolding has_prod_def using 0 by blast 

788 
qed 

789 
qed 

790 

791 
lemma convergent_prod_has_prod [intro]: 

792 
shows "convergent_prod f \<Longrightarrow> f has_prod (prodinf f)" 

793 
unfolding prodinf_def 

794 
by (metis convergent_prod_imp_has_prod has_prod_unique theI') 

795 

796 
lemma convergent_prod_LIMSEQ: 

797 
shows "convergent_prod f \<Longrightarrow> (\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> prodinf f" 

798 
by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent 

799 
convergent_prod_to_zero_iff gen_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le) 

800 

801 
lemma has_prod_iff: "f has_prod x \<longleftrightarrow> convergent_prod f \<and> prodinf f = x" 

802 
proof 

803 
assume "f has_prod x" 

804 
then show "convergent_prod f \<and> prodinf f = x" 

805 
apply safe 

806 
using convergent_prod_def has_prod_def apply blast 

807 
using has_prod_unique by blast 

808 
qed auto 

809 

810 
lemma convergent_prod_has_prod_iff: "convergent_prod f \<longleftrightarrow> f has_prod prodinf f" 

811 
by (auto simp: has_prod_iff convergent_prod_has_prod) 

812 

813 
lemma prodinf_finite: 

814 
assumes N: "finite N" 

815 
and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1" 

816 
shows "prodinf f = (\<Prod>n\<in>N. f n)" 

817 
using has_prod_finite[OF assms, THEN has_prod_unique] by simp 

68127  818 

66277  819 
end 
68136  820 

821 
end 