|
1 (* |
|
2 File: HOL/Analysis/Infinite_Product.thy |
|
3 Author: Manuel Eberl |
|
4 |
|
5 Basic results about convergence and absolute convergence of infinite products |
|
6 and their connection to summability. |
|
7 *) |
|
8 section \<open>Infinite Products\<close> |
|
9 theory Infinite_Products |
|
10 imports Complex_Main |
|
11 begin |
|
12 |
|
13 lemma sum_le_prod: |
|
14 fixes f :: "'a \<Rightarrow> 'b :: linordered_semidom" |
|
15 assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0" |
|
16 shows "sum f A \<le> (\<Prod>x\<in>A. 1 + f x)" |
|
17 using assms |
|
18 proof (induction A rule: infinite_finite_induct) |
|
19 case (insert x A) |
|
20 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)" |
|
21 by (intro add_mono insert mult_left_mono prod_mono) (auto intro: insert.prems) |
|
22 with insert.hyps show ?case by (simp add: algebra_simps) |
|
23 qed simp_all |
|
24 |
|
25 lemma prod_le_exp_sum: |
|
26 fixes f :: "'a \<Rightarrow> real" |
|
27 assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0" |
|
28 shows "prod (\<lambda>x. 1 + f x) A \<le> exp (sum f A)" |
|
29 using assms |
|
30 proof (induction A rule: infinite_finite_induct) |
|
31 case (insert x A) |
|
32 have "(1 + f x) * (\<Prod>x\<in>A. 1 + f x) \<le> exp (f x) * exp (sum f A)" |
|
33 using insert.prems by (intro mult_mono insert prod_nonneg exp_ge_add_one_self) auto |
|
34 with insert.hyps show ?case by (simp add: algebra_simps exp_add) |
|
35 qed simp_all |
|
36 |
|
37 lemma lim_ln_1_plus_x_over_x_at_0: "(\<lambda>x::real. ln (1 + x) / x) \<midarrow>0\<rightarrow> 1" |
|
38 proof (rule lhopital) |
|
39 show "(\<lambda>x::real. ln (1 + x)) \<midarrow>0\<rightarrow> 0" |
|
40 by (rule tendsto_eq_intros refl | simp)+ |
|
41 have "eventually (\<lambda>x::real. x \<in> {-1/2<..<1/2}) (nhds 0)" |
|
42 by (rule eventually_nhds_in_open) auto |
|
43 hence *: "eventually (\<lambda>x::real. x \<in> {-1/2<..<1/2}) (at 0)" |
|
44 by (rule filter_leD [rotated]) (simp_all add: at_within_def) |
|
45 show "eventually (\<lambda>x::real. ((\<lambda>x. ln (1 + x)) has_field_derivative inverse (1 + x)) (at x)) (at 0)" |
|
46 using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps) |
|
47 show "eventually (\<lambda>x::real. ((\<lambda>x. x) has_field_derivative 1) (at x)) (at 0)" |
|
48 using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps) |
|
49 show "\<forall>\<^sub>F x in at 0. x \<noteq> 0" by (auto simp: at_within_def eventually_inf_principal) |
|
50 show "(\<lambda>x::real. inverse (1 + x) / 1) \<midarrow>0\<rightarrow> 1" |
|
51 by (rule tendsto_eq_intros refl | simp)+ |
|
52 qed auto |
|
53 |
|
54 definition convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where |
|
55 "convergent_prod f \<longleftrightarrow> (\<exists>M L. (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L \<and> L \<noteq> 0)" |
|
56 |
|
57 lemma convergent_prod_altdef: |
|
58 fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}" |
|
59 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)" |
|
60 proof |
|
61 assume "convergent_prod f" |
|
62 then obtain M L where *: "(\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L" "L \<noteq> 0" |
|
63 by (auto simp: convergent_prod_def) |
|
64 have "f i \<noteq> 0" if "i \<ge> M" for i |
|
65 proof |
|
66 assume "f i = 0" |
|
67 have **: "eventually (\<lambda>n. (\<Prod>i\<le>n. f (i+M)) = 0) sequentially" |
|
68 using eventually_ge_at_top[of "i - M"] |
|
69 proof eventually_elim |
|
70 case (elim n) |
|
71 with \<open>f i = 0\<close> and \<open>i \<ge> M\<close> show ?case |
|
72 by (auto intro!: bexI[of _ "i - M"] prod_zero) |
|
73 qed |
|
74 have "(\<lambda>n. (\<Prod>i\<le>n. f (i+M))) \<longlonglongrightarrow> 0" |
|
75 unfolding filterlim_iff |
|
76 by (auto dest!: eventually_nhds_x_imp_x intro!: eventually_mono[OF **]) |
|
77 from tendsto_unique[OF _ this *(1)] and *(2) |
|
78 show False by simp |
|
79 qed |
|
80 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)" |
|
81 by blast |
|
82 qed (auto simp: convergent_prod_def) |
|
83 |
|
84 definition abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where |
|
85 "abs_convergent_prod f \<longleftrightarrow> convergent_prod (\<lambda>i. 1 + norm (f i - 1))" |
|
86 |
|
87 lemma abs_convergent_prodI: |
|
88 assumes "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
89 shows "abs_convergent_prod f" |
|
90 proof - |
|
91 from assms obtain L where L: "(\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1)) \<longlonglongrightarrow> L" |
|
92 by (auto simp: convergent_def) |
|
93 have "L \<ge> 1" |
|
94 proof (rule tendsto_le) |
|
95 show "eventually (\<lambda>n. (\<Prod>i\<le>n. 1 + norm (f i - 1)) \<ge> 1) sequentially" |
|
96 proof (intro always_eventually allI) |
|
97 fix n |
|
98 have "(\<Prod>i\<le>n. 1 + norm (f i - 1)) \<ge> (\<Prod>i\<le>n. 1)" |
|
99 by (intro prod_mono) auto |
|
100 thus "(\<Prod>i\<le>n. 1 + norm (f i - 1)) \<ge> 1" by simp |
|
101 qed |
|
102 qed (use L in simp_all) |
|
103 hence "L \<noteq> 0" by auto |
|
104 with L show ?thesis unfolding abs_convergent_prod_def convergent_prod_def |
|
105 by (intro exI[of _ "0::nat"] exI[of _ L]) auto |
|
106 qed |
|
107 |
|
108 lemma |
|
109 fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,idom}" |
|
110 assumes "convergent_prod f" |
|
111 shows convergent_prod_imp_convergent: "convergent (\<lambda>n. \<Prod>i\<le>n. f i)" |
|
112 and convergent_prod_to_zero_iff: "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)" |
|
113 proof - |
|
114 from assms obtain M L |
|
115 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" |
|
116 by (auto simp: convergent_prod_altdef) |
|
117 note this(2) |
|
118 also have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) = (\<lambda>n. \<Prod>i=M..M+n. f i)" |
|
119 by (intro ext prod.reindex_bij_witness[of _ "\<lambda>n. n - M" "\<lambda>n. n + M"]) auto |
|
120 finally have "(\<lambda>n. (\<Prod>i<M. f i) * (\<Prod>i=M..M+n. f i)) \<longlonglongrightarrow> (\<Prod>i<M. f i) * L" |
|
121 by (intro tendsto_mult tendsto_const) |
|
122 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))" |
|
123 by (subst prod.union_disjoint) auto |
|
124 also have "(\<lambda>n. {..<M} \<union> {M..M+n}) = (\<lambda>n. {..n+M})" by auto |
|
125 finally have lim: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * L" |
|
126 by (rule LIMSEQ_offset) |
|
127 thus "convergent (\<lambda>n. \<Prod>i\<le>n. f i)" |
|
128 by (auto simp: convergent_def) |
|
129 |
|
130 show "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)" |
|
131 proof |
|
132 assume "\<exists>i. f i = 0" |
|
133 then obtain i where "f i = 0" by auto |
|
134 moreover with M have "i < M" by (cases "i < M") auto |
|
135 ultimately have "(\<Prod>i<M. f i) = 0" by auto |
|
136 with lim show "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0" by simp |
|
137 next |
|
138 assume "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0" |
|
139 from tendsto_unique[OF _ this lim] and \<open>L \<noteq> 0\<close> |
|
140 show "\<exists>i. f i = 0" by auto |
|
141 qed |
|
142 qed |
|
143 |
|
144 lemma abs_convergent_prod_altdef: |
|
145 "abs_convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
146 proof |
|
147 assume "abs_convergent_prod f" |
|
148 thus "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
149 by (auto simp: abs_convergent_prod_def intro!: convergent_prod_imp_convergent) |
|
150 qed (auto intro: abs_convergent_prodI) |
|
151 |
|
152 lemma weierstrass_prod_ineq: |
|
153 fixes f :: "'a \<Rightarrow> real" |
|
154 assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> {0..1}" |
|
155 shows "1 - sum f A \<le> (\<Prod>x\<in>A. 1 - f x)" |
|
156 using assms |
|
157 proof (induction A rule: infinite_finite_induct) |
|
158 case (insert x A) |
|
159 from insert.hyps and insert.prems |
|
160 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)" |
|
161 by (intro insert.IH add_mono mult_left_mono prod_mono) auto |
|
162 with insert.hyps show ?case by (simp add: algebra_simps) |
|
163 qed simp_all |
|
164 |
|
165 lemma norm_prod_minus1_le_prod_minus1: |
|
166 fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,comm_ring_1}" |
|
167 shows "norm (prod (\<lambda>n. 1 + f n) A - 1) \<le> prod (\<lambda>n. 1 + norm (f n)) A - 1" |
|
168 proof (induction A rule: infinite_finite_induct) |
|
169 case (insert x A) |
|
170 from insert.hyps have |
|
171 "norm ((\<Prod>n\<in>insert x A. 1 + f n) - 1) = |
|
172 norm ((\<Prod>n\<in>A. 1 + f n) - 1 + f x * (\<Prod>n\<in>A. 1 + f n))" |
|
173 by (simp add: algebra_simps) |
|
174 also have "\<dots> \<le> norm ((\<Prod>n\<in>A. 1 + f n) - 1) + norm (f x * (\<Prod>n\<in>A. 1 + f n))" |
|
175 by (rule norm_triangle_ineq) |
|
176 also have "norm (f x * (\<Prod>n\<in>A. 1 + f n)) = norm (f x) * (\<Prod>x\<in>A. norm (1 + f x))" |
|
177 by (simp add: prod_norm norm_mult) |
|
178 also have "(\<Prod>x\<in>A. norm (1 + f x)) \<le> (\<Prod>x\<in>A. norm (1::'a) + norm (f x))" |
|
179 by (intro prod_mono norm_triangle_ineq ballI conjI) auto |
|
180 also have "norm (1::'a) = 1" by simp |
|
181 also note insert.IH |
|
182 also have "(\<Prod>n\<in>A. 1 + norm (f n)) - 1 + norm (f x) * (\<Prod>x\<in>A. 1 + norm (f x)) = |
|
183 (\<Prod>n\<in>insert x A. 1 + norm (f n)) - 1" |
|
184 using insert.hyps by (simp add: algebra_simps) |
|
185 finally show ?case by - (simp_all add: mult_left_mono) |
|
186 qed simp_all |
|
187 |
|
188 lemma convergent_prod_imp_ev_nonzero: |
|
189 fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}" |
|
190 assumes "convergent_prod f" |
|
191 shows "eventually (\<lambda>n. f n \<noteq> 0) sequentially" |
|
192 using assms by (auto simp: eventually_at_top_linorder convergent_prod_altdef) |
|
193 |
|
194 lemma convergent_prod_imp_LIMSEQ: |
|
195 fixes f :: "nat \<Rightarrow> 'a :: {real_normed_field}" |
|
196 assumes "convergent_prod f" |
|
197 shows "f \<longlonglongrightarrow> 1" |
|
198 proof - |
|
199 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" |
|
200 by (auto simp: convergent_prod_altdef) |
|
201 hence L': "(\<lambda>n. \<Prod>i\<le>Suc n. f (i+M)) \<longlonglongrightarrow> L" by (subst filterlim_sequentially_Suc) |
|
202 have "(\<lambda>n. (\<Prod>i\<le>Suc n. f (i+M)) / (\<Prod>i\<le>n. f (i+M))) \<longlonglongrightarrow> L / L" |
|
203 using L L' by (intro tendsto_divide) simp_all |
|
204 also from L have "L / L = 1" by simp |
|
205 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))" |
|
206 using assms L by (auto simp: fun_eq_iff atMost_Suc) |
|
207 finally show ?thesis by (rule LIMSEQ_offset) |
|
208 qed |
|
209 |
|
210 lemma abs_convergent_prod_imp_summable: |
|
211 fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra" |
|
212 assumes "abs_convergent_prod f" |
|
213 shows "summable (\<lambda>i. norm (f i - 1))" |
|
214 proof - |
|
215 from assms have "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
216 unfolding abs_convergent_prod_def by (rule convergent_prod_imp_convergent) |
|
217 then obtain L where L: "(\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1)) \<longlonglongrightarrow> L" |
|
218 unfolding convergent_def by blast |
|
219 have "convergent (\<lambda>n. \<Sum>i\<le>n. norm (f i - 1))" |
|
220 proof (rule Bseq_monoseq_convergent) |
|
221 have "eventually (\<lambda>n. (\<Prod>i\<le>n. 1 + norm (f i - 1)) < L + 1) sequentially" |
|
222 using L(1) by (rule order_tendstoD) simp_all |
|
223 hence "\<forall>\<^sub>F x in sequentially. norm (\<Sum>i\<le>x. norm (f i - 1)) \<le> L + 1" |
|
224 proof eventually_elim |
|
225 case (elim n) |
|
226 have "norm (\<Sum>i\<le>n. norm (f i - 1)) = (\<Sum>i\<le>n. norm (f i - 1))" |
|
227 unfolding real_norm_def by (intro abs_of_nonneg sum_nonneg) simp_all |
|
228 also have "\<dots> \<le> (\<Prod>i\<le>n. 1 + norm (f i - 1))" by (rule sum_le_prod) auto |
|
229 also have "\<dots> < L + 1" by (rule elim) |
|
230 finally show ?case by simp |
|
231 qed |
|
232 thus "Bseq (\<lambda>n. \<Sum>i\<le>n. norm (f i - 1))" by (rule BfunI) |
|
233 next |
|
234 show "monoseq (\<lambda>n. \<Sum>i\<le>n. norm (f i - 1))" |
|
235 by (rule mono_SucI1) auto |
|
236 qed |
|
237 thus "summable (\<lambda>i. norm (f i - 1))" by (simp add: summable_iff_convergent') |
|
238 qed |
|
239 |
|
240 lemma summable_imp_abs_convergent_prod: |
|
241 fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra" |
|
242 assumes "summable (\<lambda>i. norm (f i - 1))" |
|
243 shows "abs_convergent_prod f" |
|
244 proof (intro abs_convergent_prodI Bseq_monoseq_convergent) |
|
245 show "monoseq (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
246 by (intro mono_SucI1) |
|
247 (auto simp: atMost_Suc algebra_simps intro!: mult_nonneg_nonneg prod_nonneg) |
|
248 next |
|
249 show "Bseq (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
250 proof (rule Bseq_eventually_mono) |
|
251 show "eventually (\<lambda>n. norm (\<Prod>i\<le>n. 1 + norm (f i - 1)) \<le> |
|
252 norm (exp (\<Sum>i\<le>n. norm (f i - 1)))) sequentially" |
|
253 by (intro always_eventually allI) (auto simp: abs_prod exp_sum intro!: prod_mono) |
|
254 next |
|
255 from assms have "(\<lambda>n. \<Sum>i\<le>n. norm (f i - 1)) \<longlonglongrightarrow> (\<Sum>i. norm (f i - 1))" |
|
256 using sums_def_le by blast |
|
257 hence "(\<lambda>n. exp (\<Sum>i\<le>n. norm (f i - 1))) \<longlonglongrightarrow> exp (\<Sum>i. norm (f i - 1))" |
|
258 by (rule tendsto_exp) |
|
259 hence "convergent (\<lambda>n. exp (\<Sum>i\<le>n. norm (f i - 1)))" |
|
260 by (rule convergentI) |
|
261 thus "Bseq (\<lambda>n. exp (\<Sum>i\<le>n. norm (f i - 1)))" |
|
262 by (rule convergent_imp_Bseq) |
|
263 qed |
|
264 qed |
|
265 |
|
266 lemma abs_convergent_prod_conv_summable: |
|
267 fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra" |
|
268 shows "abs_convergent_prod f \<longleftrightarrow> summable (\<lambda>i. norm (f i - 1))" |
|
269 by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod) |
|
270 |
|
271 lemma abs_convergent_prod_imp_LIMSEQ: |
|
272 fixes f :: "nat \<Rightarrow> 'a :: {comm_ring_1,real_normed_div_algebra}" |
|
273 assumes "abs_convergent_prod f" |
|
274 shows "f \<longlonglongrightarrow> 1" |
|
275 proof - |
|
276 from assms have "summable (\<lambda>n. norm (f n - 1))" |
|
277 by (rule abs_convergent_prod_imp_summable) |
|
278 from summable_LIMSEQ_zero[OF this] have "(\<lambda>n. f n - 1) \<longlonglongrightarrow> 0" |
|
279 by (simp add: tendsto_norm_zero_iff) |
|
280 from tendsto_add[OF this tendsto_const[of 1]] show ?thesis by simp |
|
281 qed |
|
282 |
|
283 lemma abs_convergent_prod_imp_ev_nonzero: |
|
284 fixes f :: "nat \<Rightarrow> 'a :: {comm_ring_1,real_normed_div_algebra}" |
|
285 assumes "abs_convergent_prod f" |
|
286 shows "eventually (\<lambda>n. f n \<noteq> 0) sequentially" |
|
287 proof - |
|
288 from assms have "f \<longlonglongrightarrow> 1" |
|
289 by (rule abs_convergent_prod_imp_LIMSEQ) |
|
290 hence "eventually (\<lambda>n. dist (f n) 1 < 1) at_top" |
|
291 by (auto simp: tendsto_iff) |
|
292 thus ?thesis by eventually_elim auto |
|
293 qed |
|
294 |
|
295 lemma convergent_prod_offset: |
|
296 assumes "convergent_prod (\<lambda>n. f (n + m))" |
|
297 shows "convergent_prod f" |
|
298 proof - |
|
299 from assms obtain M L where "(\<lambda>n. \<Prod>k\<le>n. f (k + (M + m))) \<longlonglongrightarrow> L" "L \<noteq> 0" |
|
300 by (auto simp: convergent_prod_def add.assoc) |
|
301 thus "convergent_prod f" unfolding convergent_prod_def by blast |
|
302 qed |
|
303 |
|
304 lemma abs_convergent_prod_offset: |
|
305 assumes "abs_convergent_prod (\<lambda>n. f (n + m))" |
|
306 shows "abs_convergent_prod f" |
|
307 using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset) |
|
308 |
|
309 lemma convergent_prod_ignore_initial_segment: |
|
310 fixes f :: "nat \<Rightarrow> 'a :: {real_normed_field}" |
|
311 assumes "convergent_prod f" |
|
312 shows "convergent_prod (\<lambda>n. f (n + m))" |
|
313 proof - |
|
314 from assms obtain M L |
|
315 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" |
|
316 by (auto simp: convergent_prod_altdef) |
|
317 define C where "C = (\<Prod>k<m. f (k + M))" |
|
318 from nz have [simp]: "C \<noteq> 0" |
|
319 by (auto simp: C_def) |
|
320 |
|
321 from L(1) have "(\<lambda>n. \<Prod>k\<le>n+m. f (k + M)) \<longlonglongrightarrow> L" |
|
322 by (rule LIMSEQ_ignore_initial_segment) |
|
323 also have "(\<lambda>n. \<Prod>k\<le>n+m. f (k + M)) = (\<lambda>n. C * (\<Prod>k\<le>n. f (k + M + m)))" |
|
324 proof (rule ext, goal_cases) |
|
325 case (1 n) |
|
326 have "{..n+m} = {..<m} \<union> {m..n+m}" by auto |
|
327 also have "(\<Prod>k\<in>\<dots>. f (k + M)) = C * (\<Prod>k=m..n+m. f (k + M))" |
|
328 unfolding C_def by (rule prod.union_disjoint) auto |
|
329 also have "(\<Prod>k=m..n+m. f (k + M)) = (\<Prod>k\<le>n. f (k + m + M))" |
|
330 by (intro ext prod.reindex_bij_witness[of _ "\<lambda>k. k + m" "\<lambda>k. k - m"]) auto |
|
331 finally show ?case by (simp add: add_ac) |
|
332 qed |
|
333 finally have "(\<lambda>n. C * (\<Prod>k\<le>n. f (k + M + m)) / C) \<longlonglongrightarrow> L / C" |
|
334 by (intro tendsto_divide tendsto_const) auto |
|
335 hence "(\<lambda>n. \<Prod>k\<le>n. f (k + M + m)) \<longlonglongrightarrow> L / C" by simp |
|
336 moreover from \<open>L \<noteq> 0\<close> have "L / C \<noteq> 0" by simp |
|
337 ultimately show ?thesis unfolding convergent_prod_def by blast |
|
338 qed |
|
339 |
|
340 lemma abs_convergent_prod_ignore_initial_segment: |
|
341 assumes "abs_convergent_prod f" |
|
342 shows "abs_convergent_prod (\<lambda>n. f (n + m))" |
|
343 using assms unfolding abs_convergent_prod_def |
|
344 by (rule convergent_prod_ignore_initial_segment) |
|
345 |
|
346 lemma summable_LIMSEQ': |
|
347 assumes "summable (f::nat\<Rightarrow>'a::{t2_space,comm_monoid_add})" |
|
348 shows "(\<lambda>n. \<Sum>i\<le>n. f i) \<longlonglongrightarrow> suminf f" |
|
349 using assms sums_def_le by blast |
|
350 |
|
351 lemma abs_convergent_prod_imp_convergent_prod: |
|
352 fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}" |
|
353 assumes "abs_convergent_prod f" |
|
354 shows "convergent_prod f" |
|
355 proof - |
|
356 from assms have "eventually (\<lambda>n. f n \<noteq> 0) sequentially" |
|
357 by (rule abs_convergent_prod_imp_ev_nonzero) |
|
358 then obtain N where N: "f n \<noteq> 0" if "n \<ge> N" for n |
|
359 by (auto simp: eventually_at_top_linorder) |
|
360 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)" |
|
361 |
|
362 have "Cauchy ?P" |
|
363 proof (rule CauchyI', goal_cases) |
|
364 case (1 \<epsilon>) |
|
365 from assms have "abs_convergent_prod (\<lambda>n. f (n + N))" |
|
366 by (rule abs_convergent_prod_ignore_initial_segment) |
|
367 hence "Cauchy ?Q" |
|
368 unfolding abs_convergent_prod_def |
|
369 by (intro convergent_Cauchy convergent_prod_imp_convergent) |
|
370 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 |
|
371 by blast |
|
372 show ?case |
|
373 proof (rule exI[of _ M], safe, goal_cases) |
|
374 case (1 m n) |
|
375 have "dist (?P m) (?P n) = norm (?P n - ?P m)" |
|
376 by (simp add: dist_norm norm_minus_commute) |
|
377 also from 1 have "{..n} = {..m} \<union> {m<..n}" by auto |
|
378 hence "norm (?P n - ?P m) = norm (?P m * (\<Prod>k\<in>{m<..n}. f (k + N)) - ?P m)" |
|
379 by (subst prod.union_disjoint [symmetric]) (auto simp: algebra_simps) |
|
380 also have "\<dots> = norm (?P m * ((\<Prod>k\<in>{m<..n}. f (k + N)) - 1))" |
|
381 by (simp add: algebra_simps) |
|
382 also have "\<dots> = (\<Prod>k\<le>m. norm (f (k + N))) * norm ((\<Prod>k\<in>{m<..n}. f (k + N)) - 1)" |
|
383 by (simp add: norm_mult prod_norm) |
|
384 also have "\<dots> \<le> ?Q m * ((\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N) - 1)) - 1)" |
|
385 using norm_prod_minus1_le_prod_minus1[of "\<lambda>k. f (k + N) - 1" "{m<..n}"] |
|
386 norm_triangle_ineq[of 1 "f k - 1" for k] |
|
387 by (intro mult_mono prod_mono ballI conjI norm_prod_minus1_le_prod_minus1 prod_nonneg) auto |
|
388 also have "\<dots> = ?Q m * (\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N) - 1)) - ?Q m" |
|
389 by (simp add: algebra_simps) |
|
390 also have "?Q m * (\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N) - 1)) = |
|
391 (\<Prod>k\<in>{..m}\<union>{m<..n}. 1 + norm (f (k + N) - 1))" |
|
392 by (rule prod.union_disjoint [symmetric]) auto |
|
393 also from 1 have "{..m}\<union>{m<..n} = {..n}" by auto |
|
394 also have "?Q n - ?Q m \<le> norm (?Q n - ?Q m)" by simp |
|
395 also from 1 have "\<dots> < \<epsilon>" by (intro M) auto |
|
396 finally show ?case . |
|
397 qed |
|
398 qed |
|
399 hence conv: "convergent ?P" by (rule Cauchy_convergent) |
|
400 then obtain L where L: "?P \<longlonglongrightarrow> L" |
|
401 by (auto simp: convergent_def) |
|
402 |
|
403 have "L \<noteq> 0" |
|
404 proof |
|
405 assume [simp]: "L = 0" |
|
406 from tendsto_norm[OF L] have limit: "(\<lambda>n. \<Prod>k\<le>n. norm (f (k + N))) \<longlonglongrightarrow> 0" |
|
407 by (simp add: prod_norm) |
|
408 |
|
409 from assms have "(\<lambda>n. f (n + N)) \<longlonglongrightarrow> 1" |
|
410 by (intro abs_convergent_prod_imp_LIMSEQ abs_convergent_prod_ignore_initial_segment) |
|
411 hence "eventually (\<lambda>n. norm (f (n + N) - 1) < 1) sequentially" |
|
412 by (auto simp: tendsto_iff dist_norm) |
|
413 then obtain M0 where M0: "norm (f (n + N) - 1) < 1" if "n \<ge> M0" for n |
|
414 by (auto simp: eventually_at_top_linorder) |
|
415 |
|
416 { |
|
417 fix M assume M: "M \<ge> M0" |
|
418 with M0 have M: "norm (f (n + N) - 1) < 1" if "n \<ge> M" for n using that by simp |
|
419 |
|
420 have "(\<lambda>n. \<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<longlonglongrightarrow> 0" |
|
421 proof (rule tendsto_sandwich) |
|
422 show "eventually (\<lambda>n. (\<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<ge> 0) sequentially" |
|
423 using M by (intro always_eventually prod_nonneg allI ballI) (auto intro: less_imp_le) |
|
424 have "norm (1::'a) - norm (f (i + M + N) - 1) \<le> norm (f (i + M + N))" for i |
|
425 using norm_triangle_ineq3[of "f (i + M + N)" 1] by simp |
|
426 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" |
|
427 using M by (intro always_eventually allI prod_mono ballI conjI) (auto intro: less_imp_le) |
|
428 |
|
429 define C where "C = (\<Prod>k<M. norm (f (k + N)))" |
|
430 from N have [simp]: "C \<noteq> 0" by (auto simp: C_def) |
|
431 from L have "(\<lambda>n. norm (\<Prod>k\<le>n+M. f (k + N))) \<longlonglongrightarrow> 0" |
|
432 by (intro LIMSEQ_ignore_initial_segment) (simp add: tendsto_norm_zero_iff) |
|
433 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))))" |
|
434 proof (rule ext, goal_cases) |
|
435 case (1 n) |
|
436 have "{..n+M} = {..<M} \<union> {M..n+M}" by auto |
|
437 also have "norm (\<Prod>k\<in>\<dots>. f (k + N)) = C * norm (\<Prod>k=M..n+M. f (k + N))" |
|
438 unfolding C_def by (subst prod.union_disjoint) (auto simp: norm_mult prod_norm) |
|
439 also have "(\<Prod>k=M..n+M. f (k + N)) = (\<Prod>k\<le>n. f (k + N + M))" |
|
440 by (intro prod.reindex_bij_witness[of _ "\<lambda>i. i + M" "\<lambda>i. i - M"]) auto |
|
441 finally show ?case by (simp add: add_ac prod_norm) |
|
442 qed |
|
443 finally have "(\<lambda>n. C * (\<Prod>k\<le>n. norm (f (k + M + N))) / C) \<longlonglongrightarrow> 0 / C" |
|
444 by (intro tendsto_divide tendsto_const) auto |
|
445 thus "(\<lambda>n. \<Prod>k\<le>n. norm (f (k + M + N))) \<longlonglongrightarrow> 0" by simp |
|
446 qed simp_all |
|
447 |
|
448 have "1 - (\<Sum>i. norm (f (i + M + N) - 1)) \<le> 0" |
|
449 proof (rule tendsto_le) |
|
450 show "eventually (\<lambda>n. 1 - (\<Sum>k\<le>n. norm (f (k+M+N) - 1)) \<le> |
|
451 (\<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1))) at_top" |
|
452 using M by (intro always_eventually allI weierstrass_prod_ineq) (auto intro: less_imp_le) |
|
453 show "(\<lambda>n. \<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<longlonglongrightarrow> 0" by fact |
|
454 show "(\<lambda>n. 1 - (\<Sum>k\<le>n. norm (f (k + M + N) - 1))) |
|
455 \<longlonglongrightarrow> 1 - (\<Sum>i. norm (f (i + M + N) - 1))" |
|
456 by (intro tendsto_intros summable_LIMSEQ' summable_ignore_initial_segment |
|
457 abs_convergent_prod_imp_summable assms) |
|
458 qed simp_all |
|
459 hence "(\<Sum>i. norm (f (i + M + N) - 1)) \<ge> 1" by simp |
|
460 also have "\<dots> + (\<Sum>i<M. norm (f (i + N) - 1)) = (\<Sum>i. norm (f (i + N) - 1))" |
|
461 by (intro suminf_split_initial_segment [symmetric] summable_ignore_initial_segment |
|
462 abs_convergent_prod_imp_summable assms) |
|
463 finally have "1 + (\<Sum>i<M. norm (f (i + N) - 1)) \<le> (\<Sum>i. norm (f (i + N) - 1))" by simp |
|
464 } note * = this |
|
465 |
|
466 have "1 + (\<Sum>i. norm (f (i + N) - 1)) \<le> (\<Sum>i. norm (f (i + N) - 1))" |
|
467 proof (rule tendsto_le) |
|
468 show "(\<lambda>M. 1 + (\<Sum>i<M. norm (f (i + N) - 1))) \<longlonglongrightarrow> 1 + (\<Sum>i. norm (f (i + N) - 1))" |
|
469 by (intro tendsto_intros summable_LIMSEQ summable_ignore_initial_segment |
|
470 abs_convergent_prod_imp_summable assms) |
|
471 show "eventually (\<lambda>M. 1 + (\<Sum>i<M. norm (f (i + N) - 1)) \<le> (\<Sum>i. norm (f (i + N) - 1))) at_top" |
|
472 using eventually_ge_at_top[of M0] by eventually_elim (use * in auto) |
|
473 qed simp_all |
|
474 thus False by simp |
|
475 qed |
|
476 with L show ?thesis by (auto simp: convergent_prod_def) |
|
477 qed |
|
478 |
|
479 end |