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