author  paulson <lp15@cam.ac.uk> 
Wed, 02 May 2018 12:47:56 +0100  
changeset 68064  b249fab48c76 
parent 66277  512b0dc09061 
child 68071  c18af2b0f83e 
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 

75 
lemma convergent_prod_altdef: 

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

77 
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)" 

78 
proof 

79 
assume "convergent_prod f" 

80 
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

81 
by (auto simp: prod_defs) 
66277  82 
have "f i \<noteq> 0" if "i \<ge> M" for i 
83 
proof 

84 
assume "f i = 0" 

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

86 
using eventually_ge_at_top[of "i  M"] 

87 
proof eventually_elim 

88 
case (elim n) 

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

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

91 
qed 

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

93 
unfolding filterlim_iff 

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

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

96 
show False by simp 

97 
qed 

98 
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)" 

99 
by blast 

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

100 
qed (auto simp: prod_defs) 
66277  101 

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

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

104 

105 
lemma abs_convergent_prodI: 

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

107 
shows "abs_convergent_prod f" 

108 
proof  

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

110 
by (auto simp: convergent_def) 

111 
have "L \<ge> 1" 

112 
proof (rule tendsto_le) 

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

114 
proof (intro always_eventually allI) 

115 
fix n 

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

117 
by (intro prod_mono) auto 

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

119 
qed 

120 
qed (use L in simp_all) 

121 
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

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

125 

126 
lemma 

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

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

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

131 
proof  

132 
from assms obtain M L 

133 
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" 

134 
by (auto simp: convergent_prod_altdef) 

135 
note this(2) 

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

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

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

139 
by (intro tendsto_mult tendsto_const) 

140 
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))" 

141 
by (subst prod.union_disjoint) auto 

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

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

144 
by (rule LIMSEQ_offset) 

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

146 
by (auto simp: convergent_def) 

147 

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

149 
proof 

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

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

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

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

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

155 
next 

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

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

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

159 
qed 

160 
qed 

161 

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

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

163 
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

164 
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

165 
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

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

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

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

169 
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

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

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

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

173 
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

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

175 

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

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

177 
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

178 
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

179 
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

180 
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

181 

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

182 

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

184 
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

185 
shows "abs_convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i  1))" 
66277  186 
proof 
187 
assume "abs_convergent_prod f" 

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

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

190 
qed (auto intro: abs_convergent_prodI) 

191 

192 
lemma weierstrass_prod_ineq: 

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

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

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

196 
using assms 

197 
proof (induction A rule: infinite_finite_induct) 

198 
case (insert x A) 

199 
from insert.hyps and insert.prems 

200 
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)" 

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

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

203 
qed simp_all 

204 

205 
lemma norm_prod_minus1_le_prod_minus1: 

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

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

208 
proof (induction A rule: infinite_finite_induct) 

209 
case (insert x A) 

210 
from insert.hyps have 

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

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

213 
by (simp add: algebra_simps) 

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

215 
by (rule norm_triangle_ineq) 

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

217 
by (simp add: prod_norm norm_mult) 

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

219 
by (intro prod_mono norm_triangle_ineq ballI conjI) auto 

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

221 
also note insert.IH 

222 
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

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

226 
qed simp_all 

227 

228 
lemma convergent_prod_imp_ev_nonzero: 

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

230 
assumes "convergent_prod f" 

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

232 
using assms by (auto simp: eventually_at_top_linorder convergent_prod_altdef) 

233 

234 
lemma convergent_prod_imp_LIMSEQ: 

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

236 
assumes "convergent_prod f" 

237 
shows "f \<longlonglongrightarrow> 1" 

238 
proof  

239 
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" 

240 
by (auto simp: convergent_prod_altdef) 

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

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

243 
using L L' by (intro tendsto_divide) simp_all 

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

245 
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))" 

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

247 
finally show ?thesis by (rule LIMSEQ_offset) 

248 
qed 

249 

250 
lemma abs_convergent_prod_imp_summable: 

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

252 
assumes "abs_convergent_prod f" 

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

254 
proof  

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

256 
unfolding abs_convergent_prod_def by (rule convergent_prod_imp_convergent) 

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

258 
unfolding convergent_def by blast 

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

260 
proof (rule Bseq_monoseq_convergent) 

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

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

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

264 
proof eventually_elim 

265 
case (elim n) 

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

267 
unfolding real_norm_def by (intro abs_of_nonneg sum_nonneg) simp_all 

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

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

270 
finally show ?case by simp 

271 
qed 

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

273 
next 

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

275 
by (rule mono_SucI1) auto 

276 
qed 

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

278 
qed 

279 

280 
lemma summable_imp_abs_convergent_prod: 

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

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

283 
shows "abs_convergent_prod f" 

284 
proof (intro abs_convergent_prodI Bseq_monoseq_convergent) 

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

286 
by (intro mono_SucI1) 

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

288 
next 

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

290 
proof (rule Bseq_eventually_mono) 

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

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

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

294 
next 

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

296 
using sums_def_le by blast 

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

298 
by (rule tendsto_exp) 

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

300 
by (rule convergentI) 

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

302 
by (rule convergent_imp_Bseq) 

303 
qed 

304 
qed 

305 

306 
lemma abs_convergent_prod_conv_summable: 

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

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

309 
by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod) 

310 

311 
lemma abs_convergent_prod_imp_LIMSEQ: 

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

313 
assumes "abs_convergent_prod f" 

314 
shows "f \<longlonglongrightarrow> 1" 

315 
proof  

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

317 
by (rule abs_convergent_prod_imp_summable) 

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

319 
by (simp add: tendsto_norm_zero_iff) 

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

321 
qed 

322 

323 
lemma abs_convergent_prod_imp_ev_nonzero: 

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

325 
assumes "abs_convergent_prod f" 

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

327 
proof  

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

329 
by (rule abs_convergent_prod_imp_LIMSEQ) 

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

331 
by (auto simp: tendsto_iff) 

332 
thus ?thesis by eventually_elim auto 

333 
qed 

334 

335 
lemma convergent_prod_offset: 

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

337 
shows "convergent_prod f" 

338 
proof  

339 
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

340 
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

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

342 
unfolding prod_defs by blast 
66277  343 
qed 
344 

345 
lemma abs_convergent_prod_offset: 

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

347 
shows "abs_convergent_prod f" 

348 
using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset) 

349 

350 
lemma convergent_prod_ignore_initial_segment: 

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

352 
assumes "convergent_prod f" 

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

354 
proof  

355 
from assms obtain M L 

356 
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" 

357 
by (auto simp: convergent_prod_altdef) 

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

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

360 
by (auto simp: C_def) 

361 

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

363 
by (rule LIMSEQ_ignore_initial_segment) 

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

365 
proof (rule ext, goal_cases) 

366 
case (1 n) 

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

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

369 
unfolding C_def by (rule prod.union_disjoint) auto 

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

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

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

373 
qed 

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

375 
by (intro tendsto_divide tendsto_const) auto 

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

377 
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

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

379 
unfolding prod_defs by blast 
66277  380 
qed 
381 

382 
lemma abs_convergent_prod_ignore_initial_segment: 

383 
assumes "abs_convergent_prod f" 

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

385 
using assms unfolding abs_convergent_prod_def 

386 
by (rule convergent_prod_ignore_initial_segment) 

387 

388 
lemma abs_convergent_prod_imp_convergent_prod: 

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

390 
assumes "abs_convergent_prod f" 

391 
shows "convergent_prod f" 

392 
proof  

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

394 
by (rule abs_convergent_prod_imp_ev_nonzero) 

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

396 
by (auto simp: eventually_at_top_linorder) 

397 
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)" 

398 

399 
have "Cauchy ?P" 

400 
proof (rule CauchyI', goal_cases) 

401 
case (1 \<epsilon>) 

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

403 
by (rule abs_convergent_prod_ignore_initial_segment) 

404 
hence "Cauchy ?Q" 

405 
unfolding abs_convergent_prod_def 

406 
by (intro convergent_Cauchy convergent_prod_imp_convergent) 

407 
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 

408 
by blast 

409 
show ?case 

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

411 
case (1 m n) 

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

413 
by (simp add: dist_norm norm_minus_commute) 

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

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

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

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

418 
by (simp add: algebra_simps) 

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

420 
by (simp add: norm_mult prod_norm) 

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

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

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

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

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

426 
by (simp add: algebra_simps) 

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

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

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

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

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

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

433 
finally show ?case . 

434 
qed 

435 
qed 

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

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

438 
by (auto simp: convergent_def) 

439 

440 
have "L \<noteq> 0" 

441 
proof 

442 
assume [simp]: "L = 0" 

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

444 
by (simp add: prod_norm) 

445 

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

447 
by (intro abs_convergent_prod_imp_LIMSEQ abs_convergent_prod_ignore_initial_segment) 

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

449 
by (auto simp: tendsto_iff dist_norm) 

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

451 
by (auto simp: eventually_at_top_linorder) 

452 

453 
{ 

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

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

456 

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

458 
proof (rule tendsto_sandwich) 

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

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

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

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

463 
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" 

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

465 

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

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

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

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

470 
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))))" 

471 
proof (rule ext, goal_cases) 

472 
case (1 n) 

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

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

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

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

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

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

479 
qed 

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

481 
by (intro tendsto_divide tendsto_const) auto 

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

483 
qed simp_all 

484 

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

486 
proof (rule tendsto_le) 

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

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

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

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

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

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

493 
by (intro tendsto_intros summable_LIMSEQ' summable_ignore_initial_segment 

494 
abs_convergent_prod_imp_summable assms) 

495 
qed simp_all 

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

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

498 
by (intro suminf_split_initial_segment [symmetric] summable_ignore_initial_segment 

499 
abs_convergent_prod_imp_summable assms) 

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

501 
} note * = this 

502 

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

504 
proof (rule tendsto_le) 

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

506 
by (intro tendsto_intros summable_LIMSEQ summable_ignore_initial_segment 

507 
abs_convergent_prod_imp_summable assms) 

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

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

510 
qed simp_all 

511 
thus False by simp 

512 
qed 

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

513 
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

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

515 

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

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

517 
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

518 
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

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

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

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

522 
proof (clarsimp simp: prod_defs) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

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

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

525 
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

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

527 
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

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

529 
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

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

531 
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

532 
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

533 
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

534 
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

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

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

537 
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

538 
by (auto intro: LIMSEQ_offset [where k=M]) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

539 
then show "\<exists>p. (\<lambda>n. prod f {..n}) \<longlonglongrightarrow> p \<and> p \<noteq> 0" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

540 
using \<open>p \<noteq> 0\<close> assms 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

541 
by (rule_tac x="prod f {..<M} * p" in exI) auto 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset

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

543 

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

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

545 
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

546 
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

547 
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

548 
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

549 
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

550 

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

551 
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

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

553 

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

554 
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

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

556 

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

557 
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

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

559 

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

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

561 
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

562 
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

563 
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

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

565 
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

566 
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

567 
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

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

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

570 
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

571 
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

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

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

574 
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

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

576 
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

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

578 
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

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

580 
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

581 
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

582 
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

583 
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

584 
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

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

586 
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

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

588 
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

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

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

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

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

593 
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

594 
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

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

596 
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

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

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

599 
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

600 
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

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

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

603 
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

604 
qed 
66277  605 
qed 
606 

607 
end 