author | nipkow |
Sat, 29 Dec 2018 15:43:53 +0100 | |
changeset 69529 | 4ab9657b3257 |
parent 68651 | 16d98ef49a2c |
child 69565 | 1daf07b65385 |
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 |
|
68585 | 9 |
imports Topology_Euclidean_Space Complex_Transcendental |
66277 | 10 |
begin |
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
11 |
|
68651 | 12 |
subsection%unimportant \<open>Preliminaries\<close> |
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
13 |
|
66277 | 14 |
lemma sum_le_prod: |
15 |
fixes f :: "'a \<Rightarrow> 'b :: linordered_semidom" |
|
16 |
assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0" |
|
17 |
shows "sum f A \<le> (\<Prod>x\<in>A. 1 + f x)" |
|
18 |
using assms |
|
19 |
proof (induction A rule: infinite_finite_induct) |
|
20 |
case (insert x A) |
|
21 |
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)" |
|
22 |
by (intro add_mono insert mult_left_mono prod_mono) (auto intro: insert.prems) |
|
23 |
with insert.hyps show ?case by (simp add: algebra_simps) |
|
24 |
qed simp_all |
|
25 |
||
26 |
lemma prod_le_exp_sum: |
|
27 |
fixes f :: "'a \<Rightarrow> real" |
|
28 |
assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0" |
|
29 |
shows "prod (\<lambda>x. 1 + f x) A \<le> exp (sum f A)" |
|
30 |
using assms |
|
31 |
proof (induction A rule: infinite_finite_induct) |
|
32 |
case (insert x A) |
|
33 |
have "(1 + f x) * (\<Prod>x\<in>A. 1 + f x) \<le> exp (f x) * exp (sum f A)" |
|
34 |
using insert.prems by (intro mult_mono insert prod_nonneg exp_ge_add_one_self) auto |
|
35 |
with insert.hyps show ?case by (simp add: algebra_simps exp_add) |
|
36 |
qed simp_all |
|
37 |
||
38 |
lemma lim_ln_1_plus_x_over_x_at_0: "(\<lambda>x::real. ln (1 + x) / x) \<midarrow>0\<rightarrow> 1" |
|
39 |
proof (rule lhopital) |
|
40 |
show "(\<lambda>x::real. ln (1 + x)) \<midarrow>0\<rightarrow> 0" |
|
41 |
by (rule tendsto_eq_intros refl | simp)+ |
|
42 |
have "eventually (\<lambda>x::real. x \<in> {-1/2<..<1/2}) (nhds 0)" |
|
43 |
by (rule eventually_nhds_in_open) auto |
|
44 |
hence *: "eventually (\<lambda>x::real. x \<in> {-1/2<..<1/2}) (at 0)" |
|
45 |
by (rule filter_leD [rotated]) (simp_all add: at_within_def) |
|
46 |
show "eventually (\<lambda>x::real. ((\<lambda>x. ln (1 + x)) has_field_derivative inverse (1 + x)) (at x)) (at 0)" |
|
47 |
using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps) |
|
48 |
show "eventually (\<lambda>x::real. ((\<lambda>x. x) has_field_derivative 1) (at x)) (at 0)" |
|
49 |
using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps) |
|
50 |
show "\<forall>\<^sub>F x in at 0. x \<noteq> 0" by (auto simp: at_within_def eventually_inf_principal) |
|
51 |
show "(\<lambda>x::real. inverse (1 + x) / 1) \<midarrow>0\<rightarrow> 1" |
|
52 |
by (rule tendsto_eq_intros refl | simp)+ |
|
53 |
qed auto |
|
54 |
||
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
55 |
subsection\<open>Definitions and basic properties\<close> |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
56 |
|
68651 | 57 |
definition%important raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool" |
68361 | 58 |
where "raw_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0" |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
59 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
60 |
text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close> |
68651 | 61 |
definition%important |
62 |
has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80) |
|
68361 | 63 |
where "f has_prod p \<equiv> raw_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> raw_has_prod f (Suc i) q)" |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
64 |
|
68651 | 65 |
definition%important convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where |
68361 | 66 |
"convergent_prod f \<equiv> \<exists>M p. raw_has_prod f M p" |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
67 |
|
68651 | 68 |
definition%important prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a" |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
69 |
(binder "\<Prod>" 10) |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
70 |
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
|
71 |
|
68361 | 72 |
lemmas prod_defs = raw_has_prod_def has_prod_def convergent_prod_def prodinf_def |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
73 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
74 |
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
|
75 |
by simp |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
76 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
77 |
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
|
78 |
by presburger |
66277 | 79 |
|
68361 | 80 |
lemma raw_has_prod_nonzero [simp]: "\<not> raw_has_prod f M 0" |
81 |
by (simp add: raw_has_prod_def) |
|
68071 | 82 |
|
68361 | 83 |
lemma raw_has_prod_eq_0: |
84 |
fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}" |
|
85 |
assumes p: "raw_has_prod f m p" and i: "f i = 0" "i \<ge> m" |
|
68136 | 86 |
shows "p = 0" |
87 |
proof - |
|
88 |
have eq0: "(\<Prod>k\<le>n. f (k+m)) = 0" if "i - m \<le> n" for n |
|
68361 | 89 |
proof - |
90 |
have "\<exists>k\<le>n. f (k + m) = 0" |
|
91 |
using i that by auto |
|
92 |
then show ?thesis |
|
93 |
by auto |
|
94 |
qed |
|
68136 | 95 |
have "(\<lambda>n. \<Prod>i\<le>n. f (i + m)) \<longlonglongrightarrow> 0" |
96 |
by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0) |
|
97 |
with p show ?thesis |
|
68361 | 98 |
unfolding raw_has_prod_def |
68136 | 99 |
using LIMSEQ_unique by blast |
100 |
qed |
|
101 |
||
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
102 |
lemma raw_has_prod_Suc: |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
103 |
"raw_has_prod f (Suc M) a \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
104 |
unfolding raw_has_prod_def by auto |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
105 |
|
68361 | 106 |
lemma has_prod_0_iff: "f has_prod 0 \<longleftrightarrow> (\<exists>i. f i = 0 \<and> (\<exists>p. raw_has_prod f (Suc i) p))" |
68071 | 107 |
by (simp add: has_prod_def) |
68136 | 108 |
|
109 |
lemma has_prod_unique2: |
|
68361 | 110 |
fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}" |
68136 | 111 |
assumes "f has_prod a" "f has_prod b" shows "a = b" |
112 |
using assms |
|
68361 | 113 |
by (auto simp: has_prod_def raw_has_prod_eq_0) (meson raw_has_prod_def sequentially_bot tendsto_unique) |
68136 | 114 |
|
115 |
lemma has_prod_unique: |
|
68361 | 116 |
fixes f :: "nat \<Rightarrow> 'a :: {semidom,t2_space}" |
68136 | 117 |
shows "f has_prod s \<Longrightarrow> s = prodinf f" |
118 |
by (simp add: has_prod_unique2 prodinf_def the_equality) |
|
68071 | 119 |
|
66277 | 120 |
lemma convergent_prod_altdef: |
121 |
fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}" |
|
122 |
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)" |
|
123 |
proof |
|
124 |
assume "convergent_prod f" |
|
125 |
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
|
126 |
by (auto simp: prod_defs) |
66277 | 127 |
have "f i \<noteq> 0" if "i \<ge> M" for i |
128 |
proof |
|
129 |
assume "f i = 0" |
|
130 |
have **: "eventually (\<lambda>n. (\<Prod>i\<le>n. f (i+M)) = 0) sequentially" |
|
131 |
using eventually_ge_at_top[of "i - M"] |
|
132 |
proof eventually_elim |
|
133 |
case (elim n) |
|
134 |
with \<open>f i = 0\<close> and \<open>i \<ge> M\<close> show ?case |
|
135 |
by (auto intro!: bexI[of _ "i - M"] prod_zero) |
|
136 |
qed |
|
137 |
have "(\<lambda>n. (\<Prod>i\<le>n. f (i+M))) \<longlonglongrightarrow> 0" |
|
138 |
unfolding filterlim_iff |
|
139 |
by (auto dest!: eventually_nhds_x_imp_x intro!: eventually_mono[OF **]) |
|
140 |
from tendsto_unique[OF _ this *(1)] and *(2) |
|
141 |
show False by simp |
|
142 |
qed |
|
143 |
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)" |
|
144 |
by blast |
|
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
145 |
qed (auto simp: prod_defs) |
66277 | 146 |
|
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
147 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
148 |
subsection\<open>Absolutely convergent products\<close> |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
149 |
|
68651 | 150 |
definition%important abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where |
66277 | 151 |
"abs_convergent_prod f \<longleftrightarrow> convergent_prod (\<lambda>i. 1 + norm (f i - 1))" |
152 |
||
153 |
lemma abs_convergent_prodI: |
|
154 |
assumes "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
155 |
shows "abs_convergent_prod f" |
|
156 |
proof - |
|
157 |
from assms obtain L where L: "(\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1)) \<longlonglongrightarrow> L" |
|
158 |
by (auto simp: convergent_def) |
|
159 |
have "L \<ge> 1" |
|
160 |
proof (rule tendsto_le) |
|
161 |
show "eventually (\<lambda>n. (\<Prod>i\<le>n. 1 + norm (f i - 1)) \<ge> 1) sequentially" |
|
162 |
proof (intro always_eventually allI) |
|
163 |
fix n |
|
164 |
have "(\<Prod>i\<le>n. 1 + norm (f i - 1)) \<ge> (\<Prod>i\<le>n. 1)" |
|
165 |
by (intro prod_mono) auto |
|
166 |
thus "(\<Prod>i\<le>n. 1 + norm (f i - 1)) \<ge> 1" by simp |
|
167 |
qed |
|
168 |
qed (use L in simp_all) |
|
169 |
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
|
170 |
with L show ?thesis unfolding abs_convergent_prod_def prod_defs |
66277 | 171 |
by (intro exI[of _ "0::nat"] exI[of _ L]) auto |
172 |
qed |
|
173 |
||
174 |
lemma |
|
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
175 |
fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}" |
66277 | 176 |
assumes "convergent_prod f" |
177 |
shows convergent_prod_imp_convergent: "convergent (\<lambda>n. \<Prod>i\<le>n. f i)" |
|
178 |
and convergent_prod_to_zero_iff: "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)" |
|
179 |
proof - |
|
180 |
from assms obtain M L |
|
181 |
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" |
|
182 |
by (auto simp: convergent_prod_altdef) |
|
183 |
note this(2) |
|
184 |
also have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) = (\<lambda>n. \<Prod>i=M..M+n. f i)" |
|
185 |
by (intro ext prod.reindex_bij_witness[of _ "\<lambda>n. n - M" "\<lambda>n. n + M"]) auto |
|
186 |
finally have "(\<lambda>n. (\<Prod>i<M. f i) * (\<Prod>i=M..M+n. f i)) \<longlonglongrightarrow> (\<Prod>i<M. f i) * L" |
|
187 |
by (intro tendsto_mult tendsto_const) |
|
188 |
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))" |
|
189 |
by (subst prod.union_disjoint) auto |
|
190 |
also have "(\<lambda>n. {..<M} \<union> {M..M+n}) = (\<lambda>n. {..n+M})" by auto |
|
191 |
finally have lim: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * L" |
|
192 |
by (rule LIMSEQ_offset) |
|
193 |
thus "convergent (\<lambda>n. \<Prod>i\<le>n. f i)" |
|
194 |
by (auto simp: convergent_def) |
|
195 |
||
196 |
show "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)" |
|
197 |
proof |
|
198 |
assume "\<exists>i. f i = 0" |
|
199 |
then obtain i where "f i = 0" by auto |
|
200 |
moreover with M have "i < M" by (cases "i < M") auto |
|
201 |
ultimately have "(\<Prod>i<M. f i) = 0" by auto |
|
202 |
with lim show "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0" by simp |
|
203 |
next |
|
204 |
assume "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0" |
|
205 |
from tendsto_unique[OF _ this lim] and \<open>L \<noteq> 0\<close> |
|
206 |
show "\<exists>i. f i = 0" by auto |
|
207 |
qed |
|
208 |
qed |
|
209 |
||
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
210 |
lemma convergent_prod_iff_nz_lim: |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
211 |
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
|
212 |
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
|
213 |
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
|
214 |
(is "?lhs \<longleftrightarrow> ?rhs") |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
215 |
proof |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
216 |
assume ?lhs then show ?rhs |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
217 |
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
|
218 |
next |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
219 |
assume ?rhs then show ?lhs |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
220 |
unfolding prod_defs |
68138 | 221 |
by (rule_tac x=0 in exI) auto |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
222 |
qed |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
223 |
|
68651 | 224 |
lemma%important convergent_prod_iff_convergent: |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
225 |
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
|
226 |
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
|
227 |
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" |
68138 | 228 |
by (force simp: convergent_prod_iff_nz_lim assms convergent_def limI) |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
229 |
|
68527
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
230 |
lemma bounded_imp_convergent_prod: |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
231 |
fixes a :: "nat \<Rightarrow> real" |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
232 |
assumes 1: "\<And>n. a n \<ge> 1" and bounded: "\<And>n. (\<Prod>i\<le>n. a i) \<le> B" |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
233 |
shows "convergent_prod a" |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
234 |
proof - |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
235 |
have "bdd_above (range(\<lambda>n. \<Prod>i\<le>n. a i))" |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
236 |
by (meson bdd_aboveI2 bounded) |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
237 |
moreover have "incseq (\<lambda>n. \<Prod>i\<le>n. a i)" |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
238 |
unfolding mono_def by (metis 1 prod_mono2 atMost_subset_iff dual_order.trans finite_atMost zero_le_one) |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
239 |
ultimately obtain p where p: "(\<lambda>n. \<Prod>i\<le>n. a i) \<longlonglongrightarrow> p" |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
240 |
using LIMSEQ_incseq_SUP by blast |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
241 |
then have "p \<noteq> 0" |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
242 |
by (metis "1" not_one_le_zero prod_ge_1 LIMSEQ_le_const) |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
243 |
with 1 p show ?thesis |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
244 |
by (metis convergent_prod_iff_nz_lim not_one_le_zero) |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
245 |
qed |
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
68517
diff
changeset
|
246 |
|
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
247 |
|
66277 | 248 |
lemma abs_convergent_prod_altdef: |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
249 |
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
|
250 |
shows "abs_convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
66277 | 251 |
proof |
252 |
assume "abs_convergent_prod f" |
|
253 |
thus "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
254 |
by (auto simp: abs_convergent_prod_def intro!: convergent_prod_imp_convergent) |
|
255 |
qed (auto intro: abs_convergent_prodI) |
|
256 |
||
69529 | 257 |
lemma Weierstrass_prod_ineq: |
66277 | 258 |
fixes f :: "'a \<Rightarrow> real" |
259 |
assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> {0..1}" |
|
260 |
shows "1 - sum f A \<le> (\<Prod>x\<in>A. 1 - f x)" |
|
261 |
using assms |
|
262 |
proof (induction A rule: infinite_finite_induct) |
|
263 |
case (insert x A) |
|
264 |
from insert.hyps and insert.prems |
|
265 |
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)" |
|
266 |
by (intro insert.IH add_mono mult_left_mono prod_mono) auto |
|
267 |
with insert.hyps show ?case by (simp add: algebra_simps) |
|
268 |
qed simp_all |
|
269 |
||
270 |
lemma norm_prod_minus1_le_prod_minus1: |
|
271 |
fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,comm_ring_1}" |
|
272 |
shows "norm (prod (\<lambda>n. 1 + f n) A - 1) \<le> prod (\<lambda>n. 1 + norm (f n)) A - 1" |
|
273 |
proof (induction A rule: infinite_finite_induct) |
|
274 |
case (insert x A) |
|
275 |
from insert.hyps have |
|
276 |
"norm ((\<Prod>n\<in>insert x A. 1 + f n) - 1) = |
|
277 |
norm ((\<Prod>n\<in>A. 1 + f n) - 1 + f x * (\<Prod>n\<in>A. 1 + f n))" |
|
278 |
by (simp add: algebra_simps) |
|
279 |
also have "\<dots> \<le> norm ((\<Prod>n\<in>A. 1 + f n) - 1) + norm (f x * (\<Prod>n\<in>A. 1 + f n))" |
|
280 |
by (rule norm_triangle_ineq) |
|
281 |
also have "norm (f x * (\<Prod>n\<in>A. 1 + f n)) = norm (f x) * (\<Prod>x\<in>A. norm (1 + f x))" |
|
282 |
by (simp add: prod_norm norm_mult) |
|
283 |
also have "(\<Prod>x\<in>A. norm (1 + f x)) \<le> (\<Prod>x\<in>A. norm (1::'a) + norm (f x))" |
|
284 |
by (intro prod_mono norm_triangle_ineq ballI conjI) auto |
|
285 |
also have "norm (1::'a) = 1" by simp |
|
286 |
also note insert.IH |
|
287 |
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
|
288 |
(\<Prod>n\<in>insert x A. 1 + norm (f n)) - 1" |
66277 | 289 |
using insert.hyps by (simp add: algebra_simps) |
290 |
finally show ?case by - (simp_all add: mult_left_mono) |
|
291 |
qed simp_all |
|
292 |
||
293 |
lemma convergent_prod_imp_ev_nonzero: |
|
294 |
fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}" |
|
295 |
assumes "convergent_prod f" |
|
296 |
shows "eventually (\<lambda>n. f n \<noteq> 0) sequentially" |
|
297 |
using assms by (auto simp: eventually_at_top_linorder convergent_prod_altdef) |
|
298 |
||
299 |
lemma convergent_prod_imp_LIMSEQ: |
|
300 |
fixes f :: "nat \<Rightarrow> 'a :: {real_normed_field}" |
|
301 |
assumes "convergent_prod f" |
|
302 |
shows "f \<longlonglongrightarrow> 1" |
|
303 |
proof - |
|
304 |
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" |
|
305 |
by (auto simp: convergent_prod_altdef) |
|
306 |
hence L': "(\<lambda>n. \<Prod>i\<le>Suc n. f (i+M)) \<longlonglongrightarrow> L" by (subst filterlim_sequentially_Suc) |
|
307 |
have "(\<lambda>n. (\<Prod>i\<le>Suc n. f (i+M)) / (\<Prod>i\<le>n. f (i+M))) \<longlonglongrightarrow> L / L" |
|
308 |
using L L' by (intro tendsto_divide) simp_all |
|
309 |
also from L have "L / L = 1" by simp |
|
310 |
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))" |
|
311 |
using assms L by (auto simp: fun_eq_iff atMost_Suc) |
|
312 |
finally show ?thesis by (rule LIMSEQ_offset) |
|
313 |
qed |
|
314 |
||
315 |
lemma abs_convergent_prod_imp_summable: |
|
316 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra" |
|
317 |
assumes "abs_convergent_prod f" |
|
318 |
shows "summable (\<lambda>i. norm (f i - 1))" |
|
319 |
proof - |
|
320 |
from assms have "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
321 |
unfolding abs_convergent_prod_def by (rule convergent_prod_imp_convergent) |
|
322 |
then obtain L where L: "(\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1)) \<longlonglongrightarrow> L" |
|
323 |
unfolding convergent_def by blast |
|
324 |
have "convergent (\<lambda>n. \<Sum>i\<le>n. norm (f i - 1))" |
|
325 |
proof (rule Bseq_monoseq_convergent) |
|
326 |
have "eventually (\<lambda>n. (\<Prod>i\<le>n. 1 + norm (f i - 1)) < L + 1) sequentially" |
|
327 |
using L(1) by (rule order_tendstoD) simp_all |
|
328 |
hence "\<forall>\<^sub>F x in sequentially. norm (\<Sum>i\<le>x. norm (f i - 1)) \<le> L + 1" |
|
329 |
proof eventually_elim |
|
330 |
case (elim n) |
|
331 |
have "norm (\<Sum>i\<le>n. norm (f i - 1)) = (\<Sum>i\<le>n. norm (f i - 1))" |
|
332 |
unfolding real_norm_def by (intro abs_of_nonneg sum_nonneg) simp_all |
|
333 |
also have "\<dots> \<le> (\<Prod>i\<le>n. 1 + norm (f i - 1))" by (rule sum_le_prod) auto |
|
334 |
also have "\<dots> < L + 1" by (rule elim) |
|
335 |
finally show ?case by simp |
|
336 |
qed |
|
337 |
thus "Bseq (\<lambda>n. \<Sum>i\<le>n. norm (f i - 1))" by (rule BfunI) |
|
338 |
next |
|
339 |
show "monoseq (\<lambda>n. \<Sum>i\<le>n. norm (f i - 1))" |
|
340 |
by (rule mono_SucI1) auto |
|
341 |
qed |
|
342 |
thus "summable (\<lambda>i. norm (f i - 1))" by (simp add: summable_iff_convergent') |
|
343 |
qed |
|
344 |
||
345 |
lemma summable_imp_abs_convergent_prod: |
|
346 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra" |
|
347 |
assumes "summable (\<lambda>i. norm (f i - 1))" |
|
348 |
shows "abs_convergent_prod f" |
|
349 |
proof (intro abs_convergent_prodI Bseq_monoseq_convergent) |
|
350 |
show "monoseq (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
351 |
by (intro mono_SucI1) |
|
352 |
(auto simp: atMost_Suc algebra_simps intro!: mult_nonneg_nonneg prod_nonneg) |
|
353 |
next |
|
354 |
show "Bseq (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
355 |
proof (rule Bseq_eventually_mono) |
|
356 |
show "eventually (\<lambda>n. norm (\<Prod>i\<le>n. 1 + norm (f i - 1)) \<le> |
|
357 |
norm (exp (\<Sum>i\<le>n. norm (f i - 1)))) sequentially" |
|
358 |
by (intro always_eventually allI) (auto simp: abs_prod exp_sum intro!: prod_mono) |
|
359 |
next |
|
360 |
from assms have "(\<lambda>n. \<Sum>i\<le>n. norm (f i - 1)) \<longlonglongrightarrow> (\<Sum>i. norm (f i - 1))" |
|
361 |
using sums_def_le by blast |
|
362 |
hence "(\<lambda>n. exp (\<Sum>i\<le>n. norm (f i - 1))) \<longlonglongrightarrow> exp (\<Sum>i. norm (f i - 1))" |
|
363 |
by (rule tendsto_exp) |
|
364 |
hence "convergent (\<lambda>n. exp (\<Sum>i\<le>n. norm (f i - 1)))" |
|
365 |
by (rule convergentI) |
|
366 |
thus "Bseq (\<lambda>n. exp (\<Sum>i\<le>n. norm (f i - 1)))" |
|
367 |
by (rule convergent_imp_Bseq) |
|
368 |
qed |
|
369 |
qed |
|
370 |
||
68651 | 371 |
theorem abs_convergent_prod_conv_summable: |
66277 | 372 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra" |
373 |
shows "abs_convergent_prod f \<longleftrightarrow> summable (\<lambda>i. norm (f i - 1))" |
|
374 |
by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod) |
|
375 |
||
376 |
lemma abs_convergent_prod_imp_LIMSEQ: |
|
377 |
fixes f :: "nat \<Rightarrow> 'a :: {comm_ring_1,real_normed_div_algebra}" |
|
378 |
assumes "abs_convergent_prod f" |
|
379 |
shows "f \<longlonglongrightarrow> 1" |
|
380 |
proof - |
|
381 |
from assms have "summable (\<lambda>n. norm (f n - 1))" |
|
382 |
by (rule abs_convergent_prod_imp_summable) |
|
383 |
from summable_LIMSEQ_zero[OF this] have "(\<lambda>n. f n - 1) \<longlonglongrightarrow> 0" |
|
384 |
by (simp add: tendsto_norm_zero_iff) |
|
385 |
from tendsto_add[OF this tendsto_const[of 1]] show ?thesis by simp |
|
386 |
qed |
|
387 |
||
388 |
lemma abs_convergent_prod_imp_ev_nonzero: |
|
389 |
fixes f :: "nat \<Rightarrow> 'a :: {comm_ring_1,real_normed_div_algebra}" |
|
390 |
assumes "abs_convergent_prod f" |
|
391 |
shows "eventually (\<lambda>n. f n \<noteq> 0) sequentially" |
|
392 |
proof - |
|
393 |
from assms have "f \<longlonglongrightarrow> 1" |
|
394 |
by (rule abs_convergent_prod_imp_LIMSEQ) |
|
395 |
hence "eventually (\<lambda>n. dist (f n) 1 < 1) at_top" |
|
396 |
by (auto simp: tendsto_iff) |
|
397 |
thus ?thesis by eventually_elim auto |
|
398 |
qed |
|
399 |
||
68651 | 400 |
subsection%unimportant \<open>Ignoring initial segments\<close> |
401 |
||
66277 | 402 |
lemma convergent_prod_offset: |
403 |
assumes "convergent_prod (\<lambda>n. f (n + m))" |
|
404 |
shows "convergent_prod f" |
|
405 |
proof - |
|
406 |
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
|
407 |
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
|
408 |
thus "convergent_prod f" |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
409 |
unfolding prod_defs by blast |
66277 | 410 |
qed |
411 |
||
412 |
lemma abs_convergent_prod_offset: |
|
413 |
assumes "abs_convergent_prod (\<lambda>n. f (n + m))" |
|
414 |
shows "abs_convergent_prod f" |
|
415 |
using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset) |
|
416 |
||
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
417 |
|
68361 | 418 |
lemma raw_has_prod_ignore_initial_segment: |
419 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" |
|
420 |
assumes "raw_has_prod f M p" "N \<ge> M" |
|
421 |
obtains q where "raw_has_prod f N q" |
|
66277 | 422 |
proof - |
68361 | 423 |
have p: "(\<lambda>n. \<Prod>k\<le>n. f (k + M)) \<longlonglongrightarrow> p" and "p \<noteq> 0" |
424 |
using assms by (auto simp: raw_has_prod_def) |
|
425 |
then have nz: "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0" |
|
426 |
using assms by (auto simp: raw_has_prod_eq_0) |
|
427 |
define C where "C = (\<Prod>k<N-M. f (k + M))" |
|
66277 | 428 |
from nz have [simp]: "C \<noteq> 0" |
429 |
by (auto simp: C_def) |
|
430 |
||
68361 | 431 |
from p have "(\<lambda>i. \<Prod>k\<le>i + (N-M). f (k + M)) \<longlonglongrightarrow> p" |
66277 | 432 |
by (rule LIMSEQ_ignore_initial_segment) |
68361 | 433 |
also have "(\<lambda>i. \<Prod>k\<le>i + (N-M). f (k + M)) = (\<lambda>n. C * (\<Prod>k\<le>n. f (k + N)))" |
66277 | 434 |
proof (rule ext, goal_cases) |
435 |
case (1 n) |
|
68361 | 436 |
have "{..n+(N-M)} = {..<(N-M)} \<union> {(N-M)..n+(N-M)}" by auto |
437 |
also have "(\<Prod>k\<in>\<dots>. f (k + M)) = C * (\<Prod>k=(N-M)..n+(N-M). f (k + M))" |
|
66277 | 438 |
unfolding C_def by (rule prod.union_disjoint) auto |
68361 | 439 |
also have "(\<Prod>k=(N-M)..n+(N-M). f (k + M)) = (\<Prod>k\<le>n. f (k + (N-M) + M))" |
440 |
by (intro ext prod.reindex_bij_witness[of _ "\<lambda>k. k + (N-M)" "\<lambda>k. k - (N-M)"]) auto |
|
441 |
finally show ?case |
|
442 |
using \<open>N \<ge> M\<close> by (simp add: add_ac) |
|
66277 | 443 |
qed |
68361 | 444 |
finally have "(\<lambda>n. C * (\<Prod>k\<le>n. f (k + N)) / C) \<longlonglongrightarrow> p / C" |
66277 | 445 |
by (intro tendsto_divide tendsto_const) auto |
68361 | 446 |
hence "(\<lambda>n. \<Prod>k\<le>n. f (k + N)) \<longlonglongrightarrow> p / C" by simp |
447 |
moreover from \<open>p \<noteq> 0\<close> have "p / C \<noteq> 0" by simp |
|
448 |
ultimately show ?thesis |
|
449 |
using raw_has_prod_def that by blast |
|
66277 | 450 |
qed |
451 |
||
68651 | 452 |
corollary%unimportant convergent_prod_ignore_initial_segment: |
68361 | 453 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" |
454 |
assumes "convergent_prod f" |
|
455 |
shows "convergent_prod (\<lambda>n. f (n + m))" |
|
456 |
using assms |
|
457 |
unfolding convergent_prod_def |
|
458 |
apply clarify |
|
459 |
apply (erule_tac N="M+m" in raw_has_prod_ignore_initial_segment) |
|
460 |
apply (auto simp add: raw_has_prod_def add_ac) |
|
461 |
done |
|
462 |
||
68651 | 463 |
corollary%unimportant convergent_prod_ignore_nonzero_segment: |
68136 | 464 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" |
465 |
assumes f: "convergent_prod f" and nz: "\<And>i. i \<ge> M \<Longrightarrow> f i \<noteq> 0" |
|
68361 | 466 |
shows "\<exists>p. raw_has_prod f M p" |
68136 | 467 |
using convergent_prod_ignore_initial_segment [OF f] |
468 |
by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1)) |
|
469 |
||
68651 | 470 |
corollary%unimportant abs_convergent_prod_ignore_initial_segment: |
66277 | 471 |
assumes "abs_convergent_prod f" |
472 |
shows "abs_convergent_prod (\<lambda>n. f (n + m))" |
|
473 |
using assms unfolding abs_convergent_prod_def |
|
474 |
by (rule convergent_prod_ignore_initial_segment) |
|
475 |
||
68651 | 476 |
subsection\<open>More elementary properties\<close> |
477 |
||
478 |
theorem abs_convergent_prod_imp_convergent_prod: |
|
66277 | 479 |
fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}" |
480 |
assumes "abs_convergent_prod f" |
|
481 |
shows "convergent_prod f" |
|
482 |
proof - |
|
483 |
from assms have "eventually (\<lambda>n. f n \<noteq> 0) sequentially" |
|
484 |
by (rule abs_convergent_prod_imp_ev_nonzero) |
|
485 |
then obtain N where N: "f n \<noteq> 0" if "n \<ge> N" for n |
|
486 |
by (auto simp: eventually_at_top_linorder) |
|
487 |
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)" |
|
488 |
||
489 |
have "Cauchy ?P" |
|
490 |
proof (rule CauchyI', goal_cases) |
|
491 |
case (1 \<epsilon>) |
|
492 |
from assms have "abs_convergent_prod (\<lambda>n. f (n + N))" |
|
493 |
by (rule abs_convergent_prod_ignore_initial_segment) |
|
494 |
hence "Cauchy ?Q" |
|
495 |
unfolding abs_convergent_prod_def |
|
496 |
by (intro convergent_Cauchy convergent_prod_imp_convergent) |
|
497 |
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 |
|
498 |
by blast |
|
499 |
show ?case |
|
500 |
proof (rule exI[of _ M], safe, goal_cases) |
|
501 |
case (1 m n) |
|
502 |
have "dist (?P m) (?P n) = norm (?P n - ?P m)" |
|
503 |
by (simp add: dist_norm norm_minus_commute) |
|
504 |
also from 1 have "{..n} = {..m} \<union> {m<..n}" by auto |
|
505 |
hence "norm (?P n - ?P m) = norm (?P m * (\<Prod>k\<in>{m<..n}. f (k + N)) - ?P m)" |
|
506 |
by (subst prod.union_disjoint [symmetric]) (auto simp: algebra_simps) |
|
507 |
also have "\<dots> = norm (?P m * ((\<Prod>k\<in>{m<..n}. f (k + N)) - 1))" |
|
508 |
by (simp add: algebra_simps) |
|
509 |
also have "\<dots> = (\<Prod>k\<le>m. norm (f (k + N))) * norm ((\<Prod>k\<in>{m<..n}. f (k + N)) - 1)" |
|
510 |
by (simp add: norm_mult prod_norm) |
|
511 |
also have "\<dots> \<le> ?Q m * ((\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N) - 1)) - 1)" |
|
512 |
using norm_prod_minus1_le_prod_minus1[of "\<lambda>k. f (k + N) - 1" "{m<..n}"] |
|
513 |
norm_triangle_ineq[of 1 "f k - 1" for k] |
|
514 |
by (intro mult_mono prod_mono ballI conjI norm_prod_minus1_le_prod_minus1 prod_nonneg) auto |
|
515 |
also have "\<dots> = ?Q m * (\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N) - 1)) - ?Q m" |
|
516 |
by (simp add: algebra_simps) |
|
517 |
also have "?Q m * (\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N) - 1)) = |
|
518 |
(\<Prod>k\<in>{..m}\<union>{m<..n}. 1 + norm (f (k + N) - 1))" |
|
519 |
by (rule prod.union_disjoint [symmetric]) auto |
|
520 |
also from 1 have "{..m}\<union>{m<..n} = {..n}" by auto |
|
521 |
also have "?Q n - ?Q m \<le> norm (?Q n - ?Q m)" by simp |
|
522 |
also from 1 have "\<dots> < \<epsilon>" by (intro M) auto |
|
523 |
finally show ?case . |
|
524 |
qed |
|
525 |
qed |
|
526 |
hence conv: "convergent ?P" by (rule Cauchy_convergent) |
|
527 |
then obtain L where L: "?P \<longlonglongrightarrow> L" |
|
528 |
by (auto simp: convergent_def) |
|
529 |
||
530 |
have "L \<noteq> 0" |
|
531 |
proof |
|
532 |
assume [simp]: "L = 0" |
|
533 |
from tendsto_norm[OF L] have limit: "(\<lambda>n. \<Prod>k\<le>n. norm (f (k + N))) \<longlonglongrightarrow> 0" |
|
534 |
by (simp add: prod_norm) |
|
535 |
||
536 |
from assms have "(\<lambda>n. f (n + N)) \<longlonglongrightarrow> 1" |
|
537 |
by (intro abs_convergent_prod_imp_LIMSEQ abs_convergent_prod_ignore_initial_segment) |
|
538 |
hence "eventually (\<lambda>n. norm (f (n + N) - 1) < 1) sequentially" |
|
539 |
by (auto simp: tendsto_iff dist_norm) |
|
540 |
then obtain M0 where M0: "norm (f (n + N) - 1) < 1" if "n \<ge> M0" for n |
|
541 |
by (auto simp: eventually_at_top_linorder) |
|
542 |
||
543 |
{ |
|
544 |
fix M assume M: "M \<ge> M0" |
|
545 |
with M0 have M: "norm (f (n + N) - 1) < 1" if "n \<ge> M" for n using that by simp |
|
546 |
||
547 |
have "(\<lambda>n. \<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<longlonglongrightarrow> 0" |
|
548 |
proof (rule tendsto_sandwich) |
|
549 |
show "eventually (\<lambda>n. (\<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<ge> 0) sequentially" |
|
550 |
using M by (intro always_eventually prod_nonneg allI ballI) (auto intro: less_imp_le) |
|
551 |
have "norm (1::'a) - norm (f (i + M + N) - 1) \<le> norm (f (i + M + N))" for i |
|
552 |
using norm_triangle_ineq3[of "f (i + M + N)" 1] by simp |
|
553 |
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" |
|
554 |
using M by (intro always_eventually allI prod_mono ballI conjI) (auto intro: less_imp_le) |
|
555 |
||
556 |
define C where "C = (\<Prod>k<M. norm (f (k + N)))" |
|
557 |
from N have [simp]: "C \<noteq> 0" by (auto simp: C_def) |
|
558 |
from L have "(\<lambda>n. norm (\<Prod>k\<le>n+M. f (k + N))) \<longlonglongrightarrow> 0" |
|
559 |
by (intro LIMSEQ_ignore_initial_segment) (simp add: tendsto_norm_zero_iff) |
|
560 |
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))))" |
|
561 |
proof (rule ext, goal_cases) |
|
562 |
case (1 n) |
|
563 |
have "{..n+M} = {..<M} \<union> {M..n+M}" by auto |
|
564 |
also have "norm (\<Prod>k\<in>\<dots>. f (k + N)) = C * norm (\<Prod>k=M..n+M. f (k + N))" |
|
565 |
unfolding C_def by (subst prod.union_disjoint) (auto simp: norm_mult prod_norm) |
|
566 |
also have "(\<Prod>k=M..n+M. f (k + N)) = (\<Prod>k\<le>n. f (k + N + M))" |
|
567 |
by (intro prod.reindex_bij_witness[of _ "\<lambda>i. i + M" "\<lambda>i. i - M"]) auto |
|
568 |
finally show ?case by (simp add: add_ac prod_norm) |
|
569 |
qed |
|
570 |
finally have "(\<lambda>n. C * (\<Prod>k\<le>n. norm (f (k + M + N))) / C) \<longlonglongrightarrow> 0 / C" |
|
571 |
by (intro tendsto_divide tendsto_const) auto |
|
572 |
thus "(\<lambda>n. \<Prod>k\<le>n. norm (f (k + M + N))) \<longlonglongrightarrow> 0" by simp |
|
573 |
qed simp_all |
|
574 |
||
575 |
have "1 - (\<Sum>i. norm (f (i + M + N) - 1)) \<le> 0" |
|
576 |
proof (rule tendsto_le) |
|
577 |
show "eventually (\<lambda>n. 1 - (\<Sum>k\<le>n. norm (f (k+M+N) - 1)) \<le> |
|
578 |
(\<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1))) at_top" |
|
69529 | 579 |
using M by (intro always_eventually allI Weierstrass_prod_ineq) (auto intro: less_imp_le) |
66277 | 580 |
show "(\<lambda>n. \<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<longlonglongrightarrow> 0" by fact |
581 |
show "(\<lambda>n. 1 - (\<Sum>k\<le>n. norm (f (k + M + N) - 1))) |
|
582 |
\<longlonglongrightarrow> 1 - (\<Sum>i. norm (f (i + M + N) - 1))" |
|
583 |
by (intro tendsto_intros summable_LIMSEQ' summable_ignore_initial_segment |
|
584 |
abs_convergent_prod_imp_summable assms) |
|
585 |
qed simp_all |
|
586 |
hence "(\<Sum>i. norm (f (i + M + N) - 1)) \<ge> 1" by simp |
|
587 |
also have "\<dots> + (\<Sum>i<M. norm (f (i + N) - 1)) = (\<Sum>i. norm (f (i + N) - 1))" |
|
588 |
by (intro suminf_split_initial_segment [symmetric] summable_ignore_initial_segment |
|
589 |
abs_convergent_prod_imp_summable assms) |
|
590 |
finally have "1 + (\<Sum>i<M. norm (f (i + N) - 1)) \<le> (\<Sum>i. norm (f (i + N) - 1))" by simp |
|
591 |
} note * = this |
|
592 |
||
593 |
have "1 + (\<Sum>i. norm (f (i + N) - 1)) \<le> (\<Sum>i. norm (f (i + N) - 1))" |
|
594 |
proof (rule tendsto_le) |
|
595 |
show "(\<lambda>M. 1 + (\<Sum>i<M. norm (f (i + N) - 1))) \<longlonglongrightarrow> 1 + (\<Sum>i. norm (f (i + N) - 1))" |
|
596 |
by (intro tendsto_intros summable_LIMSEQ summable_ignore_initial_segment |
|
597 |
abs_convergent_prod_imp_summable assms) |
|
598 |
show "eventually (\<lambda>M. 1 + (\<Sum>i<M. norm (f (i + N) - 1)) \<le> (\<Sum>i. norm (f (i + N) - 1))) at_top" |
|
599 |
using eventually_ge_at_top[of M0] by eventually_elim (use * in auto) |
|
600 |
qed simp_all |
|
601 |
thus False by simp |
|
602 |
qed |
|
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
603 |
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
|
604 |
qed |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
605 |
|
68361 | 606 |
lemma raw_has_prod_cases: |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
607 |
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}" |
68361 | 608 |
assumes "raw_has_prod f M p" |
609 |
obtains i where "i<M" "f i = 0" | p where "raw_has_prod f 0 p" |
|
68136 | 610 |
proof - |
611 |
have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0" |
|
68361 | 612 |
using assms unfolding raw_has_prod_def by blast+ |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
613 |
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
|
614 |
by (metis tendsto_mult_left) |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
615 |
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
|
616 |
proof - |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
617 |
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
|
618 |
by auto |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
619 |
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
|
620 |
by simp (subst prod.union_disjoint; force) |
68138 | 621 |
also have "\<dots> = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))" |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
622 |
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
|
623 |
finally show ?thesis by metis |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
624 |
qed |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
625 |
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
|
626 |
by (auto intro: LIMSEQ_offset [where k=M]) |
68361 | 627 |
then have "raw_has_prod f 0 (prod f {..<M} * p)" if "\<forall>i<M. f i \<noteq> 0" |
628 |
using \<open>p \<noteq> 0\<close> assms that by (auto simp: raw_has_prod_def) |
|
68136 | 629 |
then show thesis |
630 |
using that by blast |
|
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
631 |
qed |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
632 |
|
68136 | 633 |
corollary convergent_prod_offset_0: |
634 |
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}" |
|
635 |
assumes "convergent_prod f" "\<And>i. f i \<noteq> 0" |
|
68361 | 636 |
shows "\<exists>p. raw_has_prod f 0 p" |
637 |
using assms convergent_prod_def raw_has_prod_cases by blast |
|
68136 | 638 |
|
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
639 |
lemma prodinf_eq_lim: |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
640 |
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
|
641 |
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
|
642 |
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
|
643 |
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
|
644 |
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
|
645 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
646 |
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
|
647 |
unfolding prod_defs by auto |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
648 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
649 |
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
|
650 |
unfolding prod_defs by auto |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
651 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
652 |
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
|
653 |
by presburger |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
654 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
655 |
lemma convergent_prod_cong: |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
656 |
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
|
657 |
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
|
658 |
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
|
659 |
proof - |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
660 |
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
|
661 |
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
|
662 |
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
|
663 |
with g have "C \<noteq> 0" |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
664 |
by (simp add: f) |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
665 |
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
|
666 |
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
|
667 |
proof eventually_elim |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
668 |
case (elim n) |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
669 |
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
|
670 |
by auto |
68138 | 671 |
also have "prod f \<dots> = prod f {..<N} * prod f {N..n}" |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
672 |
by (intro prod.union_disjoint) auto |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
673 |
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
|
674 |
by (intro prod.cong) simp_all |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
675 |
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
|
676 |
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
|
677 |
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
|
678 |
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
|
679 |
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
|
680 |
by auto |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
681 |
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
|
682 |
qed |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
683 |
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
|
684 |
by (rule convergent_cong) |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
685 |
show ?thesis |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
686 |
proof |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
687 |
assume cf: "convergent_prod f" |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
688 |
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
|
689 |
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
|
690 |
then show "convergent_prod g" |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
691 |
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
|
692 |
next |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
693 |
assume cg: "convergent_prod g" |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
694 |
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
|
695 |
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
|
696 |
then show "convergent_prod f" |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
697 |
using "*" tendsto_mult_left filterlim_cong |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
698 |
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
|
699 |
qed |
66277 | 700 |
qed |
701 |
||
68071 | 702 |
lemma has_prod_finite: |
68361 | 703 |
fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}" |
68071 | 704 |
assumes [simp]: "finite N" |
705 |
and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1" |
|
706 |
shows "f has_prod (\<Prod>n\<in>N. f n)" |
|
707 |
proof - |
|
708 |
have eq: "prod f {..n + Suc (Max N)} = prod f N" for n |
|
709 |
proof (rule prod.mono_neutral_right) |
|
710 |
show "N \<subseteq> {..n + Suc (Max N)}" |
|
68138 | 711 |
by (auto simp: le_Suc_eq trans_le_add2) |
68071 | 712 |
show "\<forall>i\<in>{..n + Suc (Max N)} - N. f i = 1" |
713 |
using f by blast |
|
714 |
qed auto |
|
715 |
show ?thesis |
|
716 |
proof (cases "\<forall>n\<in>N. f n \<noteq> 0") |
|
717 |
case True |
|
718 |
then have "prod f N \<noteq> 0" |
|
719 |
by simp |
|
720 |
moreover have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f N" |
|
721 |
by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) (simp add: eq atLeast0LessThan del: add_Suc_right) |
|
722 |
ultimately show ?thesis |
|
68361 | 723 |
by (simp add: raw_has_prod_def has_prod_def) |
68071 | 724 |
next |
725 |
case False |
|
726 |
then obtain k where "k \<in> N" "f k = 0" |
|
727 |
by auto |
|
728 |
let ?Z = "{n \<in> N. f n = 0}" |
|
729 |
have maxge: "Max ?Z \<ge> n" if "f n = 0" for n |
|
730 |
using Max_ge [of ?Z] \<open>finite N\<close> \<open>f n = 0\<close> |
|
731 |
by (metis (mono_tags) Collect_mem_eq f finite_Collect_conjI mem_Collect_eq zero_neq_one) |
|
732 |
let ?q = "prod f {Suc (Max ?Z)..Max N}" |
|
733 |
have [simp]: "?q \<noteq> 0" |
|
734 |
using maxge Suc_n_not_le_n le_trans by force |
|
68076 | 735 |
have eq: "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = ?q" for n |
736 |
proof - |
|
737 |
have "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = prod f {Suc (Max ?Z)..n + Max N + Suc (Max ?Z)}" |
|
738 |
proof (rule prod.reindex_cong [where l = "\<lambda>i. i + Suc (Max ?Z)", THEN sym]) |
|
739 |
show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\<lambda>i. i + Suc (Max ?Z)) ` {..n + Max N}" |
|
740 |
using le_Suc_ex by fastforce |
|
741 |
qed (auto simp: inj_on_def) |
|
68138 | 742 |
also have "\<dots> = ?q" |
68076 | 743 |
by (rule prod.mono_neutral_right) |
744 |
(use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>) |
|
745 |
finally show ?thesis . |
|
746 |
qed |
|
68361 | 747 |
have q: "raw_has_prod f (Suc (Max ?Z)) ?q" |
748 |
proof (simp add: raw_has_prod_def) |
|
68076 | 749 |
show "(\<lambda>n. \<Prod>i\<le>n. f (Suc (i + Max ?Z))) \<longlonglongrightarrow> ?q" |
750 |
by (rule LIMSEQ_offset[of _ "(Max N)"]) (simp add: eq) |
|
751 |
qed |
|
68071 | 752 |
show ?thesis |
753 |
unfolding has_prod_def |
|
754 |
proof (intro disjI2 exI conjI) |
|
755 |
show "prod f N = 0" |
|
756 |
using \<open>f k = 0\<close> \<open>k \<in> N\<close> \<open>finite N\<close> prod_zero by blast |
|
757 |
show "f (Max ?Z) = 0" |
|
758 |
using Max_in [of ?Z] \<open>finite N\<close> \<open>f k = 0\<close> \<open>k \<in> N\<close> by auto |
|
759 |
qed (use q in auto) |
|
760 |
qed |
|
761 |
qed |
|
762 |
||
68651 | 763 |
corollary%unimportant has_prod_0: |
68361 | 764 |
fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}" |
68071 | 765 |
assumes "\<And>n. f n = 1" |
766 |
shows "f has_prod 1" |
|
767 |
by (simp add: assms has_prod_cong) |
|
768 |
||
68361 | 769 |
lemma prodinf_zero[simp]: "prodinf (\<lambda>n. 1::'a::real_normed_field) = 1" |
770 |
using has_prod_unique by force |
|
771 |
||
68071 | 772 |
lemma convergent_prod_finite: |
773 |
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
|
774 |
assumes "finite N" "\<And>n. n \<notin> N \<Longrightarrow> f n = 1" |
|
775 |
shows "convergent_prod f" |
|
776 |
proof - |
|
68361 | 777 |
have "\<exists>n p. raw_has_prod f n p" |
68071 | 778 |
using assms has_prod_def has_prod_finite by blast |
779 |
then show ?thesis |
|
780 |
by (simp add: convergent_prod_def) |
|
781 |
qed |
|
782 |
||
68127 | 783 |
lemma has_prod_If_finite_set: |
784 |
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
|
785 |
shows "finite A \<Longrightarrow> (\<lambda>r. if r \<in> A then f r else 1) has_prod (\<Prod>r\<in>A. f r)" |
|
786 |
using has_prod_finite[of A "(\<lambda>r. if r \<in> A then f r else 1)"] |
|
787 |
by simp |
|
788 |
||
789 |
lemma has_prod_If_finite: |
|
790 |
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
|
791 |
shows "finite {r. P r} \<Longrightarrow> (\<lambda>r. if P r then f r else 1) has_prod (\<Prod>r | P r. f r)" |
|
792 |
using has_prod_If_finite_set[of "{r. P r}"] by simp |
|
793 |
||
794 |
lemma convergent_prod_If_finite_set[simp, intro]: |
|
795 |
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
|
796 |
shows "finite A \<Longrightarrow> convergent_prod (\<lambda>r. if r \<in> A then f r else 1)" |
|
797 |
by (simp add: convergent_prod_finite) |
|
798 |
||
799 |
lemma convergent_prod_If_finite[simp, intro]: |
|
800 |
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
|
801 |
shows "finite {r. P r} \<Longrightarrow> convergent_prod (\<lambda>r. if P r then f r else 1)" |
|
802 |
using convergent_prod_def has_prod_If_finite has_prod_def by fastforce |
|
803 |
||
804 |
lemma has_prod_single: |
|
805 |
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
|
806 |
shows "(\<lambda>r. if r = i then f r else 1) has_prod f i" |
|
807 |
using has_prod_If_finite[of "\<lambda>r. r = i"] by simp |
|
808 |
||
68136 | 809 |
context |
810 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" |
|
811 |
begin |
|
812 |
||
813 |
lemma convergent_prod_imp_has_prod: |
|
814 |
assumes "convergent_prod f" |
|
815 |
shows "\<exists>p. f has_prod p" |
|
816 |
proof - |
|
68361 | 817 |
obtain M p where p: "raw_has_prod f M p" |
68136 | 818 |
using assms convergent_prod_def by blast |
819 |
then have "p \<noteq> 0" |
|
68361 | 820 |
using raw_has_prod_nonzero by blast |
68136 | 821 |
with p have fnz: "f i \<noteq> 0" if "i \<ge> M" for i |
68361 | 822 |
using raw_has_prod_eq_0 that by blast |
68136 | 823 |
define C where "C = (\<Prod>n<M. f n)" |
824 |
show ?thesis |
|
825 |
proof (cases "\<forall>n\<le>M. f n \<noteq> 0") |
|
826 |
case True |
|
827 |
then have "C \<noteq> 0" |
|
828 |
by (simp add: C_def) |
|
829 |
then show ?thesis |
|
830 |
by (meson True assms convergent_prod_offset_0 fnz has_prod_def nat_le_linear) |
|
831 |
next |
|
832 |
case False |
|
833 |
let ?N = "GREATEST n. f n = 0" |
|
834 |
have 0: "f ?N = 0" |
|
835 |
using fnz False |
|
836 |
by (metis (mono_tags, lifting) GreatestI_ex_nat nat_le_linear) |
|
837 |
have "f i \<noteq> 0" if "i > ?N" for i |
|
838 |
by (metis (mono_tags, lifting) Greatest_le_nat fnz leD linear that) |
|
68361 | 839 |
then have "\<exists>p. raw_has_prod f (Suc ?N) p" |
68136 | 840 |
using assms by (auto simp: intro!: convergent_prod_ignore_nonzero_segment) |
841 |
then show ?thesis |
|
842 |
unfolding has_prod_def using 0 by blast |
|
843 |
qed |
|
844 |
qed |
|
845 |
||
846 |
lemma convergent_prod_has_prod [intro]: |
|
847 |
shows "convergent_prod f \<Longrightarrow> f has_prod (prodinf f)" |
|
848 |
unfolding prodinf_def |
|
849 |
by (metis convergent_prod_imp_has_prod has_prod_unique theI') |
|
850 |
||
851 |
lemma convergent_prod_LIMSEQ: |
|
852 |
shows "convergent_prod f \<Longrightarrow> (\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> prodinf f" |
|
853 |
by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent |
|
68361 | 854 |
convergent_prod_to_zero_iff raw_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le) |
68136 | 855 |
|
68651 | 856 |
theorem has_prod_iff: "f has_prod x \<longleftrightarrow> convergent_prod f \<and> prodinf f = x" |
68136 | 857 |
proof |
858 |
assume "f has_prod x" |
|
859 |
then show "convergent_prod f \<and> prodinf f = x" |
|
860 |
apply safe |
|
861 |
using convergent_prod_def has_prod_def apply blast |
|
862 |
using has_prod_unique by blast |
|
863 |
qed auto |
|
864 |
||
865 |
lemma convergent_prod_has_prod_iff: "convergent_prod f \<longleftrightarrow> f has_prod prodinf f" |
|
866 |
by (auto simp: has_prod_iff convergent_prod_has_prod) |
|
867 |
||
868 |
lemma prodinf_finite: |
|
869 |
assumes N: "finite N" |
|
870 |
and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1" |
|
871 |
shows "prodinf f = (\<Prod>n\<in>N. f n)" |
|
872 |
using has_prod_finite[OF assms, THEN has_prod_unique] by simp |
|
68127 | 873 |
|
66277 | 874 |
end |
68136 | 875 |
|
68651 | 876 |
subsection%unimportant \<open>Infinite products on ordered topological monoids\<close> |
68361 | 877 |
|
878 |
lemma LIMSEQ_prod_0: |
|
879 |
fixes f :: "nat \<Rightarrow> 'a::{semidom,topological_space}" |
|
880 |
assumes "f i = 0" |
|
881 |
shows "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> 0" |
|
882 |
proof (subst tendsto_cong) |
|
883 |
show "\<forall>\<^sub>F n in sequentially. prod f {..n} = 0" |
|
884 |
proof |
|
885 |
show "prod f {..n} = 0" if "n \<ge> i" for n |
|
886 |
using that assms by auto |
|
887 |
qed |
|
888 |
qed auto |
|
889 |
||
890 |
lemma LIMSEQ_prod_nonneg: |
|
891 |
fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}" |
|
892 |
assumes 0: "\<And>n. 0 \<le> f n" and a: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> a" |
|
893 |
shows "a \<ge> 0" |
|
894 |
by (simp add: "0" prod_nonneg LIMSEQ_le_const [OF a]) |
|
895 |
||
896 |
||
897 |
context |
|
898 |
fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}" |
|
899 |
begin |
|
900 |
||
901 |
lemma has_prod_le: |
|
902 |
assumes f: "f has_prod a" and g: "g has_prod b" and le: "\<And>n. 0 \<le> f n \<and> f n \<le> g n" |
|
903 |
shows "a \<le> b" |
|
904 |
proof (cases "a=0 \<or> b=0") |
|
905 |
case True |
|
906 |
then show ?thesis |
|
907 |
proof |
|
908 |
assume [simp]: "a=0" |
|
909 |
have "b \<ge> 0" |
|
910 |
proof (rule LIMSEQ_prod_nonneg) |
|
911 |
show "(\<lambda>n. prod g {..n}) \<longlonglongrightarrow> b" |
|
912 |
using g by (auto simp: has_prod_def raw_has_prod_def LIMSEQ_prod_0) |
|
913 |
qed (use le order_trans in auto) |
|
914 |
then show ?thesis |
|
915 |
by auto |
|
916 |
next |
|
917 |
assume [simp]: "b=0" |
|
918 |
then obtain i where "g i = 0" |
|
919 |
using g by (auto simp: prod_defs) |
|
920 |
then have "f i = 0" |
|
921 |
using antisym le by force |
|
922 |
then have "a=0" |
|
923 |
using f by (auto simp: prod_defs LIMSEQ_prod_0 LIMSEQ_unique) |
|
924 |
then show ?thesis |
|
925 |
by auto |
|
926 |
qed |
|
927 |
next |
|
928 |
case False |
|
929 |
then show ?thesis |
|
930 |
using assms |
|
931 |
unfolding has_prod_def raw_has_prod_def |
|
932 |
by (force simp: LIMSEQ_prod_0 intro!: LIMSEQ_le prod_mono) |
|
933 |
qed |
|
934 |
||
935 |
lemma prodinf_le: |
|
936 |
assumes f: "f has_prod a" and g: "g has_prod b" and le: "\<And>n. 0 \<le> f n \<and> f n \<le> g n" |
|
937 |
shows "prodinf f \<le> prodinf g" |
|
938 |
using has_prod_le [OF assms] has_prod_unique f g by blast |
|
939 |
||
68136 | 940 |
end |
68361 | 941 |
|
942 |
||
943 |
lemma prod_le_prodinf: |
|
944 |
fixes f :: "nat \<Rightarrow> 'a::{linordered_idom,linorder_topology}" |
|
945 |
assumes "f has_prod a" "\<And>i. 0 \<le> f i" "\<And>i. i\<ge>n \<Longrightarrow> 1 \<le> f i" |
|
946 |
shows "prod f {..<n} \<le> prodinf f" |
|
947 |
by(rule has_prod_le[OF has_prod_If_finite_set]) (use assms has_prod_unique in auto) |
|
948 |
||
949 |
lemma prodinf_nonneg: |
|
950 |
fixes f :: "nat \<Rightarrow> 'a::{linordered_idom,linorder_topology}" |
|
951 |
assumes "f has_prod a" "\<And>i. 1 \<le> f i" |
|
952 |
shows "1 \<le> prodinf f" |
|
953 |
using prod_le_prodinf[of f a 0] assms |
|
954 |
by (metis order_trans prod_ge_1 zero_le_one) |
|
955 |
||
956 |
lemma prodinf_le_const: |
|
957 |
fixes f :: "nat \<Rightarrow> real" |
|
958 |
assumes "convergent_prod f" "\<And>n. prod f {..<n} \<le> x" |
|
959 |
shows "prodinf f \<le> x" |
|
960 |
by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2) |
|
961 |
||
962 |
lemma prodinf_eq_one_iff: |
|
963 |
fixes f :: "nat \<Rightarrow> real" |
|
964 |
assumes f: "convergent_prod f" and ge1: "\<And>n. 1 \<le> f n" |
|
965 |
shows "prodinf f = 1 \<longleftrightarrow> (\<forall>n. f n = 1)" |
|
966 |
proof |
|
967 |
assume "prodinf f = 1" |
|
968 |
then have "(\<lambda>n. \<Prod>i<n. f i) \<longlonglongrightarrow> 1" |
|
969 |
using convergent_prod_LIMSEQ[of f] assms by (simp add: LIMSEQ_lessThan_iff_atMost) |
|
970 |
then have "\<And>i. (\<Prod>n\<in>{i}. f n) \<le> 1" |
|
971 |
proof (rule LIMSEQ_le_const) |
|
972 |
have "1 \<le> prod f n" for n |
|
973 |
by (simp add: ge1 prod_ge_1) |
|
974 |
have "prod f {..<n} = 1" for n |
|
975 |
by (metis \<open>\<And>n. 1 \<le> prod f n\<close> \<open>prodinf f = 1\<close> antisym f convergent_prod_has_prod ge1 order_trans prod_le_prodinf zero_le_one) |
|
976 |
then have "(\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" if "n \<ge> Suc i" for i n |
|
977 |
by (metis mult.left_neutral order_refl prod.cong prod.neutral_const prod_lessThan_Suc) |
|
978 |
then show "\<exists>N. \<forall>n\<ge>N. (\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" for i |
|
979 |
by blast |
|
980 |
qed |
|
981 |
with ge1 show "\<forall>n. f n = 1" |
|
982 |
by (auto intro!: antisym) |
|
983 |
qed (metis prodinf_zero fun_eq_iff) |
|
984 |
||
985 |
lemma prodinf_pos_iff: |
|
986 |
fixes f :: "nat \<Rightarrow> real" |
|
987 |
assumes "convergent_prod f" "\<And>n. 1 \<le> f n" |
|
988 |
shows "1 < prodinf f \<longleftrightarrow> (\<exists>i. 1 < f i)" |
|
989 |
using prod_le_prodinf[of f 1] prodinf_eq_one_iff |
|
990 |
by (metis convergent_prod_has_prod assms less_le prodinf_nonneg) |
|
991 |
||
992 |
lemma less_1_prodinf2: |
|
993 |
fixes f :: "nat \<Rightarrow> real" |
|
994 |
assumes "convergent_prod f" "\<And>n. 1 \<le> f n" "1 < f i" |
|
995 |
shows "1 < prodinf f" |
|
996 |
proof - |
|
997 |
have "1 < (\<Prod>n<Suc i. f n)" |
|
998 |
using assms by (intro less_1_prod2[where i=i]) auto |
|
999 |
also have "\<dots> \<le> prodinf f" |
|
1000 |
by (intro prod_le_prodinf) (use assms order_trans zero_le_one in \<open>blast+\<close>) |
|
1001 |
finally show ?thesis . |
|
1002 |
qed |
|
1003 |
||
1004 |
lemma less_1_prodinf: |
|
1005 |
fixes f :: "nat \<Rightarrow> real" |
|
1006 |
shows "\<lbrakk>convergent_prod f; \<And>n. 1 < f n\<rbrakk> \<Longrightarrow> 1 < prodinf f" |
|
1007 |
by (intro less_1_prodinf2[where i=1]) (auto intro: less_imp_le) |
|
1008 |
||
1009 |
lemma prodinf_nonzero: |
|
1010 |
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}" |
|
1011 |
assumes "convergent_prod f" "\<And>i. f i \<noteq> 0" |
|
1012 |
shows "prodinf f \<noteq> 0" |
|
1013 |
by (metis assms convergent_prod_offset_0 has_prod_unique raw_has_prod_def has_prod_def) |
|
1014 |
||
1015 |
lemma less_0_prodinf: |
|
1016 |
fixes f :: "nat \<Rightarrow> real" |
|
1017 |
assumes f: "convergent_prod f" and 0: "\<And>i. f i > 0" |
|
1018 |
shows "0 < prodinf f" |
|
1019 |
proof - |
|
1020 |
have "prodinf f \<noteq> 0" |
|
1021 |
by (metis assms less_irrefl prodinf_nonzero) |
|
1022 |
moreover have "0 < (\<Prod>n<i. f n)" for i |
|
1023 |
by (simp add: 0 prod_pos) |
|
1024 |
then have "prodinf f \<ge> 0" |
|
1025 |
using convergent_prod_LIMSEQ [OF f] LIMSEQ_prod_nonneg 0 less_le by blast |
|
1026 |
ultimately show ?thesis |
|
1027 |
by auto |
|
1028 |
qed |
|
1029 |
||
1030 |
lemma prod_less_prodinf2: |
|
1031 |
fixes f :: "nat \<Rightarrow> real" |
|
1032 |
assumes f: "convergent_prod f" and 1: "\<And>m. m\<ge>n \<Longrightarrow> 1 \<le> f m" and 0: "\<And>m. 0 < f m" and i: "n \<le> i" "1 < f i" |
|
1033 |
shows "prod f {..<n} < prodinf f" |
|
1034 |
proof - |
|
1035 |
have "prod f {..<n} \<le> prod f {..<i}" |
|
1036 |
by (rule prod_mono2) (use assms less_le in auto) |
|
1037 |
then have "prod f {..<n} < f i * prod f {..<i}" |
|
1038 |
using mult_less_le_imp_less[of 1 "f i" "prod f {..<n}" "prod f {..<i}"] assms |
|
1039 |
by (simp add: prod_pos) |
|
1040 |
moreover have "prod f {..<Suc i} \<le> prodinf f" |
|
1041 |
using prod_le_prodinf[of f _ "Suc i"] |
|
1042 |
by (meson "0" "1" Suc_leD convergent_prod_has_prod f \<open>n \<le> i\<close> le_trans less_eq_real_def) |
|
1043 |
ultimately show ?thesis |
|
1044 |
by (metis le_less_trans mult.commute not_le prod_lessThan_Suc) |
|
1045 |
qed |
|
1046 |
||
1047 |
lemma prod_less_prodinf: |
|
1048 |
fixes f :: "nat \<Rightarrow> real" |
|
1049 |
assumes f: "convergent_prod f" and 1: "\<And>m. m\<ge>n \<Longrightarrow> 1 < f m" and 0: "\<And>m. 0 < f m" |
|
1050 |
shows "prod f {..<n} < prodinf f" |
|
1051 |
by (meson "0" "1" f le_less prod_less_prodinf2) |
|
1052 |
||
1053 |
lemma raw_has_prodI_bounded: |
|
1054 |
fixes f :: "nat \<Rightarrow> real" |
|
1055 |
assumes pos: "\<And>n. 1 \<le> f n" |
|
1056 |
and le: "\<And>n. (\<Prod>i<n. f i) \<le> x" |
|
1057 |
shows "\<exists>p. raw_has_prod f 0 p" |
|
1058 |
unfolding raw_has_prod_def add_0_right |
|
1059 |
proof (rule exI LIMSEQ_incseq_SUP conjI)+ |
|
1060 |
show "bdd_above (range (\<lambda>n. prod f {..n}))" |
|
1061 |
by (metis bdd_aboveI2 le lessThan_Suc_atMost) |
|
1062 |
then have "(SUP i. prod f {..i}) > 0" |
|
1063 |
by (metis UNIV_I cSUP_upper less_le_trans pos prod_pos zero_less_one) |
|
1064 |
then show "(SUP i. prod f {..i}) \<noteq> 0" |
|
1065 |
by auto |
|
1066 |
show "incseq (\<lambda>n. prod f {..n})" |
|
1067 |
using pos order_trans [OF zero_le_one] by (auto simp: mono_def intro!: prod_mono2) |
|
1068 |
qed |
|
1069 |
||
1070 |
lemma convergent_prodI_nonneg_bounded: |
|
1071 |
fixes f :: "nat \<Rightarrow> real" |
|
1072 |
assumes "\<And>n. 1 \<le> f n" "\<And>n. (\<Prod>i<n. f i) \<le> x" |
|
1073 |
shows "convergent_prod f" |
|
1074 |
using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast |
|
1075 |
||
1076 |
||
68651 | 1077 |
subsection%unimportant \<open>Infinite products on topological spaces\<close> |
68361 | 1078 |
|
1079 |
context |
|
1080 |
fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_semigroup_mult,idom}" |
|
1081 |
begin |
|
1082 |
||
1083 |
lemma raw_has_prod_mult: "\<lbrakk>raw_has_prod f M a; raw_has_prod g M b\<rbrakk> \<Longrightarrow> raw_has_prod (\<lambda>n. f n * g n) M (a * b)" |
|
1084 |
by (force simp add: prod.distrib tendsto_mult raw_has_prod_def) |
|
1085 |
||
1086 |
lemma has_prod_mult_nz: "\<lbrakk>f has_prod a; g has_prod b; a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. f n * g n) has_prod (a * b)" |
|
1087 |
by (simp add: raw_has_prod_mult has_prod_def) |
|
1088 |
||
1089 |
end |
|
1090 |
||
1091 |
||
1092 |
context |
|
1093 |
fixes f g :: "nat \<Rightarrow> 'a::real_normed_field" |
|
1094 |
begin |
|
1095 |
||
1096 |
lemma has_prod_mult: |
|
1097 |
assumes f: "f has_prod a" and g: "g has_prod b" |
|
1098 |
shows "(\<lambda>n. f n * g n) has_prod (a * b)" |
|
1099 |
using f [unfolded has_prod_def] |
|
1100 |
proof (elim disjE exE conjE) |
|
1101 |
assume f0: "raw_has_prod f 0 a" |
|
1102 |
show ?thesis |
|
1103 |
using g [unfolded has_prod_def] |
|
1104 |
proof (elim disjE exE conjE) |
|
1105 |
assume g0: "raw_has_prod g 0 b" |
|
1106 |
with f0 show ?thesis |
|
1107 |
by (force simp add: has_prod_def prod.distrib tendsto_mult raw_has_prod_def) |
|
1108 |
next |
|
1109 |
fix j q |
|
1110 |
assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q" |
|
1111 |
obtain p where p: "raw_has_prod f (Suc j) p" |
|
1112 |
using f0 raw_has_prod_ignore_initial_segment by blast |
|
1113 |
then have "Ex (raw_has_prod (\<lambda>n. f n * g n) (Suc j))" |
|
1114 |
using q raw_has_prod_mult by blast |
|
1115 |
then show ?thesis |
|
1116 |
using \<open>b = 0\<close> \<open>g j = 0\<close> has_prod_0_iff by fastforce |
|
1117 |
qed |
|
1118 |
next |
|
1119 |
fix i p |
|
1120 |
assume "a = 0" and "f i = 0" and p: "raw_has_prod f (Suc i) p" |
|
1121 |
show ?thesis |
|
1122 |
using g [unfolded has_prod_def] |
|
1123 |
proof (elim disjE exE conjE) |
|
1124 |
assume g0: "raw_has_prod g 0 b" |
|
1125 |
obtain q where q: "raw_has_prod g (Suc i) q" |
|
1126 |
using g0 raw_has_prod_ignore_initial_segment by blast |
|
1127 |
then have "Ex (raw_has_prod (\<lambda>n. f n * g n) (Suc i))" |
|
1128 |
using raw_has_prod_mult p by blast |
|
1129 |
then show ?thesis |
|
1130 |
using \<open>a = 0\<close> \<open>f i = 0\<close> has_prod_0_iff by fastforce |
|
1131 |
next |
|
1132 |
fix j q |
|
1133 |
assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q" |
|
1134 |
obtain p' where p': "raw_has_prod f (Suc (max i j)) p'" |
|
1135 |
by (metis raw_has_prod_ignore_initial_segment max_Suc_Suc max_def p) |
|
1136 |
moreover |
|
1137 |
obtain q' where q': "raw_has_prod g (Suc (max i j)) q'" |
|
1138 |
by (metis raw_has_prod_ignore_initial_segment max.cobounded2 max_Suc_Suc q) |
|
1139 |
ultimately show ?thesis |
|
1140 |
using \<open>b = 0\<close> by (simp add: has_prod_def) (metis \<open>f i = 0\<close> \<open>g j = 0\<close> raw_has_prod_mult max_def) |
|
1141 |
qed |
|
1142 |
qed |
|
1143 |
||
1144 |
lemma convergent_prod_mult: |
|
1145 |
assumes f: "convergent_prod f" and g: "convergent_prod g" |
|
1146 |
shows "convergent_prod (\<lambda>n. f n * g n)" |
|
1147 |
unfolding convergent_prod_def |
|
1148 |
proof - |
|
1149 |
obtain M p N q where p: "raw_has_prod f M p" and q: "raw_has_prod g N q" |
|
1150 |
using convergent_prod_def f g by blast+ |
|
1151 |
then obtain p' q' where p': "raw_has_prod f (max M N) p'" and q': "raw_has_prod g (max M N) q'" |
|
1152 |
by (meson raw_has_prod_ignore_initial_segment max.cobounded1 max.cobounded2) |
|
1153 |
then show "\<exists>M p. raw_has_prod (\<lambda>n. f n * g n) M p" |
|
1154 |
using raw_has_prod_mult by blast |
|
1155 |
qed |
|
1156 |
||
1157 |
lemma prodinf_mult: "convergent_prod f \<Longrightarrow> convergent_prod g \<Longrightarrow> prodinf f * prodinf g = (\<Prod>n. f n * g n)" |
|
1158 |
by (intro has_prod_unique has_prod_mult convergent_prod_has_prod) |
|
1159 |
||
1160 |
end |
|
1161 |
||
1162 |
context |
|
1163 |
fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_field" |
|
1164 |
and I :: "'i set" |
|
1165 |
begin |
|
1166 |
||
1167 |
lemma has_prod_prod: "(\<And>i. i \<in> I \<Longrightarrow> (f i) has_prod (x i)) \<Longrightarrow> (\<lambda>n. \<Prod>i\<in>I. f i n) has_prod (\<Prod>i\<in>I. x i)" |
|
1168 |
by (induct I rule: infinite_finite_induct) (auto intro!: has_prod_mult) |
|
1169 |
||
1170 |
lemma prodinf_prod: "(\<And>i. i \<in> I \<Longrightarrow> convergent_prod (f i)) \<Longrightarrow> (\<Prod>n. \<Prod>i\<in>I. f i n) = (\<Prod>i\<in>I. \<Prod>n. f i n)" |
|
1171 |
using has_prod_unique[OF has_prod_prod, OF convergent_prod_has_prod] by simp |
|
1172 |
||
1173 |
lemma convergent_prod_prod: "(\<And>i. i \<in> I \<Longrightarrow> convergent_prod (f i)) \<Longrightarrow> convergent_prod (\<lambda>n. \<Prod>i\<in>I. f i n)" |
|
1174 |
using convergent_prod_has_prod_iff has_prod_prod prodinf_prod by force |
|
1175 |
||
1176 |
end |
|
1177 |
||
68651 | 1178 |
subsection%unimportant \<open>Infinite summability on real normed fields\<close> |
68361 | 1179 |
|
1180 |
context |
|
1181 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_field" |
|
1182 |
begin |
|
1183 |
||
1184 |
lemma raw_has_prod_Suc_iff: "raw_has_prod f M (a * f M) \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0" |
|
1185 |
proof - |
|
1186 |
have "raw_has_prod f M (a * f M) \<longleftrightarrow> (\<lambda>i. \<Prod>j\<le>Suc i. f (j+M)) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0" |
|
1187 |
by (subst LIMSEQ_Suc_iff) (simp add: raw_has_prod_def) |
|
1188 |
also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0" |
|
1189 |
by (simp add: ac_simps atMost_Suc_eq_insert_0 image_Suc_atMost prod_atLeast1_atMost_eq lessThan_Suc_atMost) |
|
1190 |
also have "\<dots> \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0" |
|
1191 |
proof safe |
|
1192 |
assume tends: "(\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M" and 0: "a * f M \<noteq> 0" |
|
1193 |
with tendsto_divide[OF tends tendsto_const, of "f M"] |
|
1194 |
show "raw_has_prod (\<lambda>n. f (Suc n)) M a" |
|
1195 |
by (simp add: raw_has_prod_def) |
|
1196 |
qed (auto intro: tendsto_mult_right simp: raw_has_prod_def) |
|
1197 |
finally show ?thesis . |
|
1198 |
qed |
|
1199 |
||
1200 |
lemma has_prod_Suc_iff: |
|
1201 |
assumes "f 0 \<noteq> 0" shows "(\<lambda>n. f (Suc n)) has_prod a \<longleftrightarrow> f has_prod (a * f 0)" |
|
1202 |
proof (cases "a = 0") |
|
1203 |
case True |
|
1204 |
then show ?thesis |
|
1205 |
proof (simp add: has_prod_def, safe) |
|
1206 |
fix i x |
|
1207 |
assume "f (Suc i) = 0" and "raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) x" |
|
1208 |
then obtain y where "raw_has_prod f (Suc (Suc i)) y" |
|
1209 |
by (metis (no_types) raw_has_prod_eq_0 Suc_n_not_le_n raw_has_prod_Suc_iff raw_has_prod_ignore_initial_segment raw_has_prod_nonzero linear) |
|
1210 |
then show "\<exists>i. f i = 0 \<and> Ex (raw_has_prod f (Suc i))" |
|
1211 |
using \<open>f (Suc i) = 0\<close> by blast |
|
1212 |
next |
|
1213 |
fix i x |
|
1214 |
assume "f i = 0" and x: "raw_has_prod f (Suc i) x" |
|
1215 |
then obtain j where j: "i = Suc j" |
|
1216 |
by (metis assms not0_implies_Suc) |
|
1217 |
moreover have "\<exists> y. raw_has_prod (\<lambda>n. f (Suc n)) i y" |
|
1218 |
using x by (auto simp: raw_has_prod_def) |
|
1219 |
then show "\<exists>i. f (Suc i) = 0 \<and> Ex (raw_has_prod (\<lambda>n. f (Suc n)) (Suc i))" |
|
1220 |
using \<open>f i = 0\<close> j by blast |
|
1221 |
qed |
|
1222 |
next |
|
1223 |
case False |
|
1224 |
then show ?thesis |
|
1225 |
by (auto simp: has_prod_def raw_has_prod_Suc_iff assms) |
|
1226 |
qed |
|
1227 |
||
1228 |
lemma convergent_prod_Suc_iff: |
|
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1229 |
shows "convergent_prod (\<lambda>n. f (Suc n)) = convergent_prod f" |
68361 | 1230 |
proof |
1231 |
assume "convergent_prod f" |
|
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1232 |
then obtain M L where M_nz:"\<forall>n\<ge>M. f n \<noteq> 0" and |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1233 |
M_L:"(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> L" and "L \<noteq> 0" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1234 |
unfolding convergent_prod_altdef by auto |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1235 |
have "(\<lambda>n. \<Prod>i\<le>n. f (Suc (i + M))) \<longlonglongrightarrow> L / f M" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1236 |
proof - |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1237 |
have "(\<lambda>n. \<Prod>i\<in>{0..Suc n}. f (i + M)) \<longlonglongrightarrow> L" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1238 |
using M_L |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1239 |
apply (subst (asm) LIMSEQ_Suc_iff[symmetric]) |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1240 |
using atLeast0AtMost by auto |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1241 |
then have "(\<lambda>n. f M * (\<Prod>i\<in>{0..n}. f (Suc (i + M)))) \<longlonglongrightarrow> L" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1242 |
apply (subst (asm) prod.atLeast0_atMost_Suc_shift) |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1243 |
by simp |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1244 |
then have "(\<lambda>n. (\<Prod>i\<in>{0..n}. f (Suc (i + M)))) \<longlonglongrightarrow> L/f M" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1245 |
apply (drule_tac tendsto_divide) |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1246 |
using M_nz[rule_format,of M,simplified] by auto |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1247 |
then show ?thesis unfolding atLeast0AtMost . |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1248 |
qed |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1249 |
then show "convergent_prod (\<lambda>n. f (Suc n))" unfolding convergent_prod_altdef |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1250 |
apply (rule_tac exI[where x=M]) |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1251 |
apply (rule_tac exI[where x="L/f M"]) |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1252 |
using M_nz \<open>L\<noteq>0\<close> by auto |
68361 | 1253 |
next |
1254 |
assume "convergent_prod (\<lambda>n. f (Suc n))" |
|
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1255 |
then obtain M where "\<exists>L. (\<forall>n\<ge>M. f (Suc n) \<noteq> 0) \<and> (\<lambda>n. \<Prod>i\<le>n. f (Suc (i + M))) \<longlonglongrightarrow> L \<and> L \<noteq> 0" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1256 |
unfolding convergent_prod_altdef by auto |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1257 |
then show "convergent_prod f" unfolding convergent_prod_altdef |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1258 |
apply (rule_tac exI[where x="Suc M"]) |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1259 |
using Suc_le_D by auto |
68361 | 1260 |
qed |
1261 |
||
1262 |
lemma raw_has_prod_inverse: |
|
1263 |
assumes "raw_has_prod f M a" shows "raw_has_prod (\<lambda>n. inverse (f n)) M (inverse a)" |
|
1264 |
using assms unfolding raw_has_prod_def by (auto dest: tendsto_inverse simp: prod_inversef [symmetric]) |
|
1265 |
||
1266 |
lemma has_prod_inverse: |
|
1267 |
assumes "f has_prod a" shows "(\<lambda>n. inverse (f n)) has_prod (inverse a)" |
|
1268 |
using assms raw_has_prod_inverse unfolding has_prod_def by auto |
|
1269 |
||
1270 |
lemma convergent_prod_inverse: |
|
1271 |
assumes "convergent_prod f" |
|
1272 |
shows "convergent_prod (\<lambda>n. inverse (f n))" |
|
1273 |
using assms unfolding convergent_prod_def by (blast intro: raw_has_prod_inverse elim: ) |
|
1274 |
||
1275 |
end |
|
1276 |
||
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1277 |
context |
68361 | 1278 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_field" |
1279 |
begin |
|
1280 |
||
1281 |
lemma raw_has_prod_Suc_iff': "raw_has_prod f M a \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M (a / f M) \<and> f M \<noteq> 0" |
|
1282 |
by (metis raw_has_prod_eq_0 add.commute add.left_neutral raw_has_prod_Suc_iff raw_has_prod_nonzero le_add1 nonzero_mult_div_cancel_right times_divide_eq_left) |
|
1283 |
||
1284 |
lemma has_prod_divide: "f has_prod a \<Longrightarrow> g has_prod b \<Longrightarrow> (\<lambda>n. f n / g n) has_prod (a / b)" |
|
1285 |
unfolding divide_inverse by (intro has_prod_inverse has_prod_mult) |
|
1286 |
||
1287 |
lemma convergent_prod_divide: |
|
1288 |
assumes f: "convergent_prod f" and g: "convergent_prod g" |
|
1289 |
shows "convergent_prod (\<lambda>n. f n / g n)" |
|
1290 |
using f g has_prod_divide has_prod_iff by blast |
|
1291 |
||
1292 |
lemma prodinf_divide: "convergent_prod f \<Longrightarrow> convergent_prod g \<Longrightarrow> prodinf f / prodinf g = (\<Prod>n. f n / g n)" |
|
1293 |
by (intro has_prod_unique has_prod_divide convergent_prod_has_prod) |
|
1294 |
||
1295 |
lemma prodinf_inverse: "convergent_prod f \<Longrightarrow> (\<Prod>n. inverse (f n)) = inverse (\<Prod>n. f n)" |
|
1296 |
by (intro has_prod_unique [symmetric] has_prod_inverse convergent_prod_has_prod) |
|
1297 |
||
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1298 |
lemma has_prod_Suc_imp: |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1299 |
assumes "(\<lambda>n. f (Suc n)) has_prod a" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1300 |
shows "f has_prod (a * f 0)" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1301 |
proof - |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1302 |
have "f has_prod (a * f 0)" when "raw_has_prod (\<lambda>n. f (Suc n)) 0 a" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1303 |
apply (cases "f 0=0") |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1304 |
using that unfolding has_prod_def raw_has_prod_Suc |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1305 |
by (auto simp add: raw_has_prod_Suc_iff) |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1306 |
moreover have "f has_prod (a * f 0)" when |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1307 |
"(\<exists>i q. a = 0 \<and> f (Suc i) = 0 \<and> raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) q)" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1308 |
proof - |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1309 |
from that |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1310 |
obtain i q where "a = 0" "f (Suc i) = 0" "raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) q" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1311 |
by auto |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1312 |
then show ?thesis unfolding has_prod_def |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1313 |
by (auto intro!:exI[where x="Suc i"] simp:raw_has_prod_Suc) |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1314 |
qed |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1315 |
ultimately show "f has_prod (a * f 0)" using assms unfolding has_prod_def by auto |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1316 |
qed |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1317 |
|
68361 | 1318 |
lemma has_prod_iff_shift: |
1319 |
assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1320 |
shows "(\<lambda>i. f (i + n)) has_prod a \<longleftrightarrow> f has_prod (a * (\<Prod>i<n. f i))" |
|
1321 |
using assms |
|
1322 |
proof (induct n arbitrary: a) |
|
1323 |
case 0 |
|
1324 |
then show ?case by simp |
|
1325 |
next |
|
1326 |
case (Suc n) |
|
1327 |
then have "(\<lambda>i. f (Suc i + n)) has_prod a \<longleftrightarrow> (\<lambda>i. f (i + n)) has_prod (a * f n)" |
|
1328 |
by (subst has_prod_Suc_iff) auto |
|
1329 |
with Suc show ?case |
|
1330 |
by (simp add: ac_simps) |
|
1331 |
qed |
|
1332 |
||
68651 | 1333 |
corollary%unimportant has_prod_iff_shift': |
68361 | 1334 |
assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
1335 |
shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i)) \<longleftrightarrow> f has_prod a" |
|
1336 |
by (simp add: assms has_prod_iff_shift) |
|
1337 |
||
1338 |
lemma has_prod_one_iff_shift: |
|
1339 |
assumes "\<And>i. i < n \<Longrightarrow> f i = 1" |
|
1340 |
shows "(\<lambda>i. f (i+n)) has_prod a \<longleftrightarrow> (\<lambda>i. f i) has_prod a" |
|
1341 |
by (simp add: assms has_prod_iff_shift) |
|
1342 |
||
1343 |
lemma convergent_prod_iff_shift: |
|
1344 |
shows "convergent_prod (\<lambda>i. f (i + n)) \<longleftrightarrow> convergent_prod f" |
|
1345 |
apply safe |
|
1346 |
using convergent_prod_offset apply blast |
|
1347 |
using convergent_prod_ignore_initial_segment convergent_prod_def by blast |
|
1348 |
||
1349 |
lemma has_prod_split_initial_segment: |
|
1350 |
assumes "f has_prod a" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1351 |
shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i))" |
|
1352 |
using assms has_prod_iff_shift' by blast |
|
1353 |
||
1354 |
lemma prodinf_divide_initial_segment: |
|
1355 |
assumes "convergent_prod f" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1356 |
shows "(\<Prod>i. f (i + n)) = (\<Prod>i. f i) / (\<Prod>i<n. f i)" |
|
1357 |
by (rule has_prod_unique[symmetric]) (auto simp: assms has_prod_iff_shift) |
|
1358 |
||
1359 |
lemma prodinf_split_initial_segment: |
|
1360 |
assumes "convergent_prod f" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1361 |
shows "prodinf f = (\<Prod>i. f (i + n)) * (\<Prod>i<n. f i)" |
|
1362 |
by (auto simp add: assms prodinf_divide_initial_segment) |
|
1363 |
||
1364 |
lemma prodinf_split_head: |
|
1365 |
assumes "convergent_prod f" "f 0 \<noteq> 0" |
|
1366 |
shows "(\<Prod>n. f (Suc n)) = prodinf f / f 0" |
|
1367 |
using prodinf_split_initial_segment[of 1] assms by simp |
|
1368 |
||
1369 |
end |
|
1370 |
||
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1371 |
context |
68361 | 1372 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_field" |
1373 |
begin |
|
1374 |
||
1375 |
lemma convergent_prod_inverse_iff: "convergent_prod (\<lambda>n. inverse (f n)) \<longleftrightarrow> convergent_prod f" |
|
1376 |
by (auto dest: convergent_prod_inverse) |
|
1377 |
||
1378 |
lemma convergent_prod_const_iff: |
|
1379 |
fixes c :: "'a :: {real_normed_field}" |
|
1380 |
shows "convergent_prod (\<lambda>_. c) \<longleftrightarrow> c = 1" |
|
1381 |
proof |
|
1382 |
assume "convergent_prod (\<lambda>_. c)" |
|
1383 |
then show "c = 1" |
|
1384 |
using convergent_prod_imp_LIMSEQ LIMSEQ_unique by blast |
|
1385 |
next |
|
1386 |
assume "c = 1" |
|
1387 |
then show "convergent_prod (\<lambda>_. c)" |
|
1388 |
by auto |
|
1389 |
qed |
|
1390 |
||
1391 |
lemma has_prod_power: "f has_prod a \<Longrightarrow> (\<lambda>i. f i ^ n) has_prod (a ^ n)" |
|
1392 |
by (induction n) (auto simp: has_prod_mult) |
|
1393 |
||
1394 |
lemma convergent_prod_power: "convergent_prod f \<Longrightarrow> convergent_prod (\<lambda>i. f i ^ n)" |
|
1395 |
by (induction n) (auto simp: convergent_prod_mult) |
|
1396 |
||
1397 |
lemma prodinf_power: "convergent_prod f \<Longrightarrow> prodinf (\<lambda>i. f i ^ n) = prodinf f ^ n" |
|
1398 |
by (metis has_prod_unique convergent_prod_imp_has_prod has_prod_power) |
|
1399 |
||
1400 |
end |
|
1401 |
||
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1402 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1403 |
subsection\<open>Exponentials and logarithms\<close> |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1404 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1405 |
context |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1406 |
fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1407 |
begin |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1408 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1409 |
lemma sums_imp_has_prod_exp: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1410 |
assumes "f sums s" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1411 |
shows "raw_has_prod (\<lambda>i. exp (f i)) 0 (exp s)" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1412 |
using assms continuous_on_exp [of UNIV "\<lambda>x::'a. x"] |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1413 |
using continuous_on_tendsto_compose [of UNIV exp "(\<lambda>n. sum f {..n})" s] |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1414 |
by (simp add: prod_defs sums_def_le exp_sum) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1415 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1416 |
lemma convergent_prod_exp: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1417 |
assumes "summable f" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1418 |
shows "convergent_prod (\<lambda>i. exp (f i))" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1419 |
using sums_imp_has_prod_exp assms unfolding summable_def convergent_prod_def by blast |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1420 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1421 |
lemma prodinf_exp: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1422 |
assumes "summable f" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1423 |
shows "prodinf (\<lambda>i. exp (f i)) = exp (suminf f)" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1424 |
proof - |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1425 |
have "f sums suminf f" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1426 |
using assms by blast |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1427 |
then have "(\<lambda>i. exp (f i)) has_prod exp (suminf f)" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1428 |
by (simp add: has_prod_def sums_imp_has_prod_exp) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1429 |
then show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1430 |
by (rule has_prod_unique [symmetric]) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1431 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1432 |
|
68361 | 1433 |
end |
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1434 |
|
68651 | 1435 |
theorem convergent_prod_iff_summable_real: |
68585 | 1436 |
fixes a :: "nat \<Rightarrow> real" |
1437 |
assumes "\<And>n. a n > 0" |
|
1438 |
shows "convergent_prod (\<lambda>k. 1 + a k) \<longleftrightarrow> summable a" (is "?lhs = ?rhs") |
|
1439 |
proof |
|
1440 |
assume ?lhs |
|
1441 |
then obtain p where "raw_has_prod (\<lambda>k. 1 + a k) 0 p" |
|
1442 |
by (metis assms add_less_same_cancel2 convergent_prod_offset_0 not_one_less_zero) |
|
1443 |
then have to_p: "(\<lambda>n. \<Prod>k\<le>n. 1 + a k) \<longlonglongrightarrow> p" |
|
1444 |
by (auto simp: raw_has_prod_def) |
|
1445 |
moreover have le: "(\<Sum>k\<le>n. a k) \<le> (\<Prod>k\<le>n. 1 + a k)" for n |
|
1446 |
by (rule sum_le_prod) (use assms less_le in force) |
|
1447 |
have "(\<Prod>k\<le>n. 1 + a k) \<le> p" for n |
|
1448 |
proof (rule incseq_le [OF _ to_p]) |
|
1449 |
show "incseq (\<lambda>n. \<Prod>k\<le>n. 1 + a k)" |
|
1450 |
using assms by (auto simp: mono_def order.strict_implies_order intro!: prod_mono2) |
|
1451 |
qed |
|
1452 |
with le have "(\<Sum>k\<le>n. a k) \<le> p" for n |
|
1453 |
by (metis order_trans) |
|
1454 |
with assms bounded_imp_summable show ?rhs |
|
1455 |
by (metis not_less order.asym) |
|
1456 |
next |
|
1457 |
assume R: ?rhs |
|
1458 |
have "(\<Prod>k\<le>n. 1 + a k) \<le> exp (suminf a)" for n |
|
1459 |
proof - |
|
1460 |
have "(\<Prod>k\<le>n. 1 + a k) \<le> exp (\<Sum>k\<le>n. a k)" for n |
|
1461 |
by (rule prod_le_exp_sum) (use assms less_le in force) |
|
1462 |
moreover have "exp (\<Sum>k\<le>n. a k) \<le> exp (suminf a)" for n |
|
1463 |
unfolding exp_le_cancel_iff |
|
1464 |
by (meson sum_le_suminf R assms finite_atMost less_eq_real_def) |
|
1465 |
ultimately show ?thesis |
|
1466 |
by (meson order_trans) |
|
1467 |
qed |
|
1468 |
then obtain L where L: "(\<lambda>n. \<Prod>k\<le>n. 1 + a k) \<longlonglongrightarrow> L" |
|
1469 |
by (metis assms bounded_imp_convergent_prod convergent_prod_iff_nz_lim le_add_same_cancel1 le_add_same_cancel2 less_le not_le zero_le_one) |
|
1470 |
moreover have "L \<noteq> 0" |
|
1471 |
proof |
|
1472 |
assume "L = 0" |
|
1473 |
with L have "(\<lambda>n. \<Prod>k\<le>n. 1 + a k) \<longlonglongrightarrow> 0" |
|
1474 |
by simp |
|
1475 |
moreover have "(\<Prod>k\<le>n. 1 + a k) > 1" for n |
|
1476 |
by (simp add: assms less_1_prod) |
|
1477 |
ultimately show False |
|
1478 |
by (meson Lim_bounded2 not_one_le_zero less_imp_le) |
|
1479 |
qed |
|
1480 |
ultimately show ?lhs |
|
1481 |
using assms convergent_prod_iff_nz_lim |
|
1482 |
by (metis add_less_same_cancel1 less_le not_le zero_less_one) |
|
1483 |
qed |
|
1484 |
||
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1485 |
lemma exp_suminf_prodinf_real: |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1486 |
fixes f :: "nat \<Rightarrow> real" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1487 |
assumes ge0:"\<And>n. f n \<ge> 0" and ac: "abs_convergent_prod (\<lambda>n. exp (f n))" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1488 |
shows "prodinf (\<lambda>i. exp (f i)) = exp (suminf f)" |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1489 |
proof - |
68517 | 1490 |
have "summable f" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1491 |
using ac unfolding abs_convergent_prod_conv_summable |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1492 |
proof (elim summable_comparison_test') |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1493 |
fix n |
68517 | 1494 |
have "\<bar>f n\<bar> = f n" |
1495 |
by (simp add: ge0) |
|
1496 |
also have "\<dots> \<le> exp (f n) - 1" |
|
1497 |
by (metis diff_diff_add exp_ge_add_one_self ge_iff_diff_ge_0) |
|
1498 |
finally show "norm (f n) \<le> norm (exp (f n) - 1)" |
|
1499 |
by simp |
|
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1500 |
qed |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1501 |
then show ?thesis |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1502 |
by (simp add: prodinf_exp) |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1503 |
qed |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68426
diff
changeset
|
1504 |
|
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1505 |
lemma has_prod_imp_sums_ln_real: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1506 |
fixes f :: "nat \<Rightarrow> real" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1507 |
assumes "raw_has_prod f 0 p" and 0: "\<And>x. f x > 0" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1508 |
shows "(\<lambda>i. ln (f i)) sums (ln p)" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1509 |
proof - |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1510 |
have "p > 0" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1511 |
using assms unfolding prod_defs by (metis LIMSEQ_prod_nonneg less_eq_real_def) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1512 |
then show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1513 |
using assms continuous_on_ln [of "{0<..}" "\<lambda>x. x"] |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1514 |
using continuous_on_tendsto_compose [of "{0<..}" ln "(\<lambda>n. prod f {..n})" p] |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1515 |
by (auto simp: prod_defs sums_def_le ln_prod order_tendstoD) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1516 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1517 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1518 |
lemma summable_ln_real: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1519 |
fixes f :: "nat \<Rightarrow> real" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1520 |
assumes f: "convergent_prod f" and 0: "\<And>x. f x > 0" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1521 |
shows "summable (\<lambda>i. ln (f i))" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1522 |
proof - |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1523 |
obtain M p where "raw_has_prod f M p" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1524 |
using f convergent_prod_def by blast |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1525 |
then consider i where "i<M" "f i = 0" | p where "raw_has_prod f 0 p" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1526 |
using raw_has_prod_cases by blast |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1527 |
then show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1528 |
proof cases |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1529 |
case 1 |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1530 |
with 0 show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1531 |
by (metis less_irrefl) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1532 |
next |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1533 |
case 2 |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1534 |
then show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1535 |
using "0" has_prod_imp_sums_ln_real summable_def by blast |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1536 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1537 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1538 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1539 |
lemma suminf_ln_real: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1540 |
fixes f :: "nat \<Rightarrow> real" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1541 |
assumes f: "convergent_prod f" and 0: "\<And>x. f x > 0" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1542 |
shows "suminf (\<lambda>i. ln (f i)) = ln (prodinf f)" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1543 |
proof - |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1544 |
have "f has_prod prodinf f" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1545 |
by (simp add: f has_prod_iff) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1546 |
then have "raw_has_prod f 0 (prodinf f)" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1547 |
by (metis "0" has_prod_def less_irrefl) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1548 |
then have "(\<lambda>i. ln (f i)) sums ln (prodinf f)" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1549 |
using "0" has_prod_imp_sums_ln_real by blast |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1550 |
then show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1551 |
by (rule sums_unique [symmetric]) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1552 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1553 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1554 |
lemma prodinf_exp_real: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1555 |
fixes f :: "nat \<Rightarrow> real" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1556 |
assumes f: "convergent_prod f" and 0: "\<And>x. f x > 0" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1557 |
shows "prodinf f = exp (suminf (\<lambda>i. ln (f i)))" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1558 |
by (simp add: "0" f less_0_prodinf suminf_ln_real) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1559 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1560 |
|
68651 | 1561 |
theorem Ln_prodinf_complex: |
68585 | 1562 |
fixes z :: "nat \<Rightarrow> complex" |
1563 |
assumes z: "\<And>j. z j \<noteq> 0" and \<xi>: "\<xi> \<noteq> 0" |
|
1564 |
shows "((\<lambda>n. \<Prod>j\<le>n. z j) \<longlonglongrightarrow> \<xi>) \<longleftrightarrow> (\<exists>k. (\<lambda>n. (\<Sum>j\<le>n. Ln (z j))) \<longlonglongrightarrow> Ln \<xi> + of_int k * (of_real(2*pi) * \<i>))" (is "?lhs = ?rhs") |
|
1565 |
proof |
|
1566 |
assume L: ?lhs |
|
1567 |
have pnz: "(\<Prod>j\<le>n. z j) \<noteq> 0" for n |
|
1568 |
using z by auto |
|
1569 |
define \<Theta> where "\<Theta> \<equiv> Arg \<xi> + 2*pi" |
|
1570 |
then have "\<Theta> > pi" |
|
1571 |
using Arg_def mpi_less_Im_Ln by fastforce |
|
1572 |
have \<xi>_eq: "\<xi> = cmod \<xi> * exp (\<i> * \<Theta>)" |
|
1573 |
using Arg_def Arg_eq \<xi> unfolding \<Theta>_def by (simp add: algebra_simps exp_add) |
|
1574 |
define \<theta> where "\<theta> \<equiv> \<lambda>n. THE t. is_Arg (\<Prod>j\<le>n. z j) t \<and> t \<in> {\<Theta>-pi<..\<Theta>+pi}" |
|
1575 |
have uniq: "\<exists>!s. is_Arg (\<Prod>j\<le>n. z j) s \<and> s \<in> {\<Theta>-pi<..\<Theta>+pi}" for n |
|
1576 |
using Argument_exists_unique [OF pnz] by metis |
|
1577 |
have \<theta>: "is_Arg (\<Prod>j\<le>n. z j) (\<theta> n)" and \<theta>_interval: "\<theta> n \<in> {\<Theta>-pi<..\<Theta>+pi}" for n |
|
1578 |
unfolding \<theta>_def |
|
1579 |
using theI' [OF uniq] by metis+ |
|
1580 |
have \<theta>_pos: "\<And>j. \<theta> j > 0" |
|
1581 |
using \<theta>_interval \<open>\<Theta> > pi\<close> by simp (meson diff_gt_0_iff_gt less_trans) |
|
1582 |
have "(\<Prod>j\<le>n. z j) = cmod (\<Prod>j\<le>n. z j) * exp (\<i> * \<theta> n)" for n |
|
1583 |
using \<theta> by (auto simp: is_Arg_def) |
|
1584 |
then have eq: "(\<lambda>n. \<Prod>j\<le>n. z j) = (\<lambda>n. cmod (\<Prod>j\<le>n. z j) * exp (\<i> * \<theta> n))" |
|
1585 |
by simp |
|
1586 |
then have "(\<lambda>n. (cmod (\<Prod>j\<le>n. z j)) * exp (\<i> * (\<theta> n))) \<longlonglongrightarrow> \<xi>" |
|
1587 |
using L by force |
|
1588 |
then obtain k where k: "(\<lambda>j. \<theta> j - of_int (k j) * (2 * pi)) \<longlonglongrightarrow> \<Theta>" |
|
1589 |
using L by (subst (asm) \<xi>_eq) (auto simp add: eq z \<xi> polar_convergence) |
|
1590 |
moreover have "\<forall>\<^sub>F n in sequentially. k n = 0" |
|
1591 |
proof - |
|
1592 |
have *: "kj = 0" if "dist (vj - real_of_int kj * 2) V < 1" "vj \<in> {V - 1<..V + 1}" for kj vj V |
|
1593 |
using that by (auto simp: dist_norm) |
|
1594 |
have "\<forall>\<^sub>F j in sequentially. dist (\<theta> j - of_int (k j) * (2 * pi)) \<Theta> < pi" |
|
1595 |
using tendstoD [OF k] pi_gt_zero by blast |
|
1596 |
then show ?thesis |
|
1597 |
proof (rule eventually_mono) |
|
1598 |
fix j |
|
1599 |
assume d: "dist (\<theta> j - real_of_int (k j) * (2 * pi)) \<Theta> < pi" |
|
1600 |
show "k j = 0" |
|
1601 |
by (rule * [of "\<theta> j/pi" _ "\<Theta>/pi"]) |
|
1602 |
(use \<theta>_interval [of j] d in \<open>simp_all add: divide_simps dist_norm\<close>) |
|
1603 |
qed |
|
1604 |
qed |
|
1605 |
ultimately have \<theta>to\<Theta>: "\<theta> \<longlonglongrightarrow> \<Theta>" |
|
1606 |
apply (simp only: tendsto_def) |
|
1607 |
apply (erule all_forward imp_forward asm_rl)+ |
|
1608 |
apply (drule (1) eventually_conj) |
|
1609 |
apply (auto elim: eventually_mono) |
|
1610 |
done |
|
1611 |
then have to0: "(\<lambda>n. \<bar>\<theta> (Suc n) - \<theta> n\<bar>) \<longlonglongrightarrow> 0" |
|
1612 |
by (metis (full_types) diff_self filterlim_sequentially_Suc tendsto_diff tendsto_rabs_zero) |
|
1613 |
have "\<exists>k. Im (\<Sum>j\<le>n. Ln (z j)) - of_int k * (2*pi) = \<theta> n" for n |
|
1614 |
proof (rule is_Arg_exp_diff_2pi) |
|
1615 |
show "is_Arg (exp (\<Sum>j\<le>n. Ln (z j))) (\<theta> n)" |
|
1616 |
using pnz \<theta> by (simp add: is_Arg_def exp_sum prod_norm) |
|
1617 |
qed |
|
1618 |
then have "\<exists>k. (\<Sum>j\<le>n. Im (Ln (z j))) = \<theta> n + of_int k * (2*pi)" for n |
|
1619 |
by (simp add: algebra_simps) |
|
1620 |
then obtain k where k: "\<And>n. (\<Sum>j\<le>n. Im (Ln (z j))) = \<theta> n + of_int (k n) * (2*pi)" |
|
1621 |
by metis |
|
1622 |
obtain K where "\<forall>\<^sub>F n in sequentially. k n = K" |
|
1623 |
proof - |
|
1624 |
have k_le: "(2*pi) * \<bar>k (Suc n) - k n\<bar> \<le> \<bar>\<theta> (Suc n) - \<theta> n\<bar> + \<bar>Im (Ln (z (Suc n)))\<bar>" for n |
|
1625 |
proof - |
|
1626 |
have "(\<Sum>j\<le>Suc n. Im (Ln (z j))) - (\<Sum>j\<le>n. Im (Ln (z j))) = Im (Ln (z (Suc n)))" |
|
1627 |
by simp |
|
1628 |
then show ?thesis |
|
1629 |
using k [of "Suc n"] k [of n] by (auto simp: abs_if algebra_simps) |
|
1630 |
qed |
|
1631 |
have "z \<longlonglongrightarrow> 1" |
|
1632 |
using L \<xi> convergent_prod_iff_nz_lim z by (blast intro: convergent_prod_imp_LIMSEQ) |
|
1633 |
with z have "(\<lambda>n. Ln (z n)) \<longlonglongrightarrow> Ln 1" |
|
1634 |
using isCont_tendsto_compose [OF continuous_at_Ln] nonpos_Reals_one_I by blast |
|
1635 |
then have "(\<lambda>n. Ln (z n)) \<longlonglongrightarrow> 0" |
|
1636 |
by simp |
|
1637 |
then have "(\<lambda>n. \<bar>Im (Ln (z (Suc n)))\<bar>) \<longlonglongrightarrow> 0" |
|
1638 |
by (metis LIMSEQ_unique \<open>z \<longlonglongrightarrow> 1\<close> continuous_at_Ln filterlim_sequentially_Suc isCont_tendsto_compose nonpos_Reals_one_I tendsto_Im tendsto_rabs_zero_iff zero_complex.simps(2)) |
|
1639 |
then have "\<forall>\<^sub>F n in sequentially. \<bar>Im (Ln (z (Suc n)))\<bar> < 1" |
|
1640 |
by (simp add: order_tendsto_iff) |
|
1641 |
moreover have "\<forall>\<^sub>F n in sequentially. \<bar>\<theta> (Suc n) - \<theta> n\<bar> < 1" |
|
1642 |
using to0 by (simp add: order_tendsto_iff) |
|
1643 |
ultimately have "\<forall>\<^sub>F n in sequentially. (2*pi) * \<bar>k (Suc n) - k n\<bar> < 1 + 1" |
|
1644 |
proof (rule eventually_elim2) |
|
1645 |
fix n |
|
1646 |
assume "\<bar>Im (Ln (z (Suc n)))\<bar> < 1" and "\<bar>\<theta> (Suc n) - \<theta> n\<bar> < 1" |
|
1647 |
with k_le [of n] show "2 * pi * real_of_int \<bar>k (Suc n) - k n\<bar> < 1 + 1" |
|
1648 |
by linarith |
|
1649 |
qed |
|
1650 |
then have "\<forall>\<^sub>F n in sequentially. real_of_int\<bar>k (Suc n) - k n\<bar> < 1" |
|
1651 |
proof (rule eventually_mono) |
|
1652 |
fix n :: "nat" |
|
1653 |
assume "2 * pi * \<bar>k (Suc n) - k n\<bar> < 1 + 1" |
|
1654 |
then have "\<bar>k (Suc n) - k n\<bar> < 2 / (2*pi)" |
|
1655 |
by (simp add: field_simps) |
|
1656 |
also have "... < 1" |
|
1657 |
using pi_ge_two by auto |
|
1658 |
finally show "real_of_int \<bar>k (Suc n) - k n\<bar> < 1" . |
|
1659 |
qed |
|
1660 |
then obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> \<bar>k (Suc n) - k n\<bar> = 0" |
|
1661 |
using eventually_sequentially less_irrefl of_int_abs by fastforce |
|
1662 |
have "k (N+i) = k N" for i |
|
1663 |
proof (induction i) |
|
1664 |
case (Suc i) |
|
1665 |
with N [of "N+i"] show ?case |
|
1666 |
by auto |
|
1667 |
qed simp |
|
1668 |
then have "\<And>n. n\<ge>N \<Longrightarrow> k n = k N" |
|
1669 |
using le_Suc_ex by auto |
|
1670 |
then show ?thesis |
|
1671 |
by (force simp add: eventually_sequentially intro: that) |
|
1672 |
qed |
|
1673 |
with \<theta>to\<Theta> have "(\<lambda>n. (\<Sum>j\<le>n. Im (Ln (z j)))) \<longlonglongrightarrow> \<Theta> + of_int K * (2*pi)" |
|
1674 |
by (simp add: k tendsto_add tendsto_mult Lim_eventually) |
|
1675 |
moreover have "(\<lambda>n. (\<Sum>k\<le>n. Re (Ln (z k)))) \<longlonglongrightarrow> Re (Ln \<xi>)" |
|
1676 |
using assms continuous_imp_tendsto [OF isCont_ln tendsto_norm [OF L]] |
|
1677 |
by (simp add: o_def flip: prod_norm ln_prod) |
|
1678 |
ultimately show ?rhs |
|
1679 |
by (rule_tac x="K+1" in exI) (auto simp: tendsto_complex_iff \<Theta>_def Arg_def assms algebra_simps) |
|
1680 |
next |
|
1681 |
assume ?rhs |
|
1682 |
then obtain r where r: "(\<lambda>n. (\<Sum>k\<le>n. Ln (z k))) \<longlonglongrightarrow> Ln \<xi> + of_int r * (of_real(2*pi) * \<i>)" .. |
|
1683 |
have "(\<lambda>n. exp (\<Sum>k\<le>n. Ln (z k))) \<longlonglongrightarrow> \<xi>" |
|
1684 |
using assms continuous_imp_tendsto [OF isCont_exp r] exp_integer_2pi [of r] |
|
1685 |
by (simp add: o_def exp_add algebra_simps) |
|
1686 |
moreover have "exp (\<Sum>k\<le>n. Ln (z k)) = (\<Prod>k\<le>n. z k)" for n |
|
1687 |
by (simp add: exp_sum add_eq_0_iff assms) |
|
1688 |
ultimately show ?lhs |
|
1689 |
by auto |
|
1690 |
qed |
|
1691 |
||
1692 |
text\<open>Prop 17.2 of Bak and Newman, Complex Analysis, p.242\<close> |
|
1693 |
proposition convergent_prod_iff_summable_complex: |
|
1694 |
fixes z :: "nat \<Rightarrow> complex" |
|
1695 |
assumes "\<And>k. z k \<noteq> 0" |
|
1696 |
shows "convergent_prod (\<lambda>k. z k) \<longleftrightarrow> summable (\<lambda>k. Ln (z k))" (is "?lhs = ?rhs") |
|
1697 |
proof |
|
1698 |
assume ?lhs |
|
1699 |
then obtain p where p: "(\<lambda>n. \<Prod>k\<le>n. z k) \<longlonglongrightarrow> p" and "p \<noteq> 0" |
|
1700 |
using convergent_prod_LIMSEQ prodinf_nonzero add_eq_0_iff assms by fastforce |
|
1701 |
then show ?rhs |
|
1702 |
using Ln_prodinf_complex assms |
|
1703 |
by (auto simp: prodinf_nonzero summable_def sums_def_le) |
|
1704 |
next |
|
1705 |
assume R: ?rhs |
|
1706 |
have "(\<Prod>k\<le>n. z k) = exp (\<Sum>k\<le>n. Ln (z k))" for n |
|
1707 |
by (simp add: exp_sum add_eq_0_iff assms) |
|
1708 |
then have "(\<lambda>n. \<Prod>k\<le>n. z k) \<longlonglongrightarrow> exp (suminf (\<lambda>k. Ln (z k)))" |
|
1709 |
using continuous_imp_tendsto [OF isCont_exp summable_LIMSEQ' [OF R]] by (simp add: o_def) |
|
1710 |
then show ?lhs |
|
1711 |
by (subst convergent_prod_iff_convergent) (auto simp: convergent_def tendsto_Lim assms add_eq_0_iff) |
|
1712 |
qed |
|
1713 |
||
68586
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1714 |
text\<open>Prop 17.3 of Bak and Newman, Complex Analysis\<close> |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1715 |
proposition summable_imp_convergent_prod_complex: |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1716 |
fixes z :: "nat \<Rightarrow> complex" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1717 |
assumes z: "summable (\<lambda>k. norm (z k))" and non0: "\<And>k. z k \<noteq> -1" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1718 |
shows "convergent_prod (\<lambda>k. 1 + z k)" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1719 |
proof - |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1720 |
note if_cong [cong] power_Suc [simp del] |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1721 |
obtain N where N: "\<And>k. k\<ge>N \<Longrightarrow> norm (z k) < 1/2" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1722 |
using summable_LIMSEQ_zero [OF z] |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1723 |
by (metis diff_zero dist_norm half_gt_zero_iff less_numeral_extra(1) lim_sequentially tendsto_norm_zero_iff) |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1724 |
have "norm (Ln (1 + z k)) \<le> 2 * norm (z k)" if "k \<ge> N" for k |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1725 |
proof (cases "z k = 0") |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1726 |
case False |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1727 |
let ?f = "\<lambda>i. cmod ((- 1) ^ i * z k ^ i / of_nat (Suc i))" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1728 |
have normf: "norm (?f n) \<le> (1 / 2) ^ n" for n |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1729 |
proof - |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1730 |
have "norm (?f n) = cmod (z k) ^ n / cmod (1 + of_nat n)" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1731 |
by (auto simp: norm_divide norm_mult norm_power) |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1732 |
also have "\<dots> \<le> cmod (z k) ^ n" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1733 |
by (auto simp: divide_simps mult_le_cancel_left1 in_Reals_norm) |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1734 |
also have "\<dots> \<le> (1 / 2) ^ n" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1735 |
using N [OF that] by (simp add: power_mono) |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1736 |
finally show "norm (?f n) \<le> (1 / 2) ^ n" . |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1737 |
qed |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1738 |
have summablef: "summable ?f" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1739 |
by (intro normf summable_comparison_test' [OF summable_geometric [of "1/2"]]) auto |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1740 |
have "(\<lambda>n. (- 1) ^ Suc n / of_nat n * z k ^ n) sums Ln (1 + z k)" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1741 |
using Ln_series [of "z k"] N that by fastforce |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1742 |
then have *: "(\<lambda>i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))) sums Ln (1 + z k)" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1743 |
using sums_split_initial_segment [where n= 1] by (force simp: power_Suc mult_ac) |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1744 |
then have "norm (Ln (1 + z k)) = norm (suminf (\<lambda>i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))))" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1745 |
using sums_unique by force |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1746 |
also have "\<dots> = norm (z k * suminf (\<lambda>i. ((- 1) ^ i * z k ^ i) / (Suc i)))" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1747 |
apply (subst suminf_mult) |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1748 |
using * False |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1749 |
by (auto simp: sums_summable intro: summable_mult_D [of "z k"]) |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1750 |
also have "\<dots> = norm (z k) * norm (suminf (\<lambda>i. ((- 1) ^ i * z k ^ i) / (Suc i)))" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1751 |
by (simp add: norm_mult) |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1752 |
also have "\<dots> \<le> norm (z k) * suminf (\<lambda>i. norm (((- 1) ^ i * z k ^ i) / (Suc i)))" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1753 |
by (intro mult_left_mono summable_norm summablef) auto |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1754 |
also have "\<dots> \<le> norm (z k) * suminf (\<lambda>i. (1/2) ^ i)" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1755 |
by (intro mult_left_mono suminf_le) (use summable_geometric [of "1/2"] summablef normf in auto) |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1756 |
also have "\<dots> \<le> norm (z k) * 2" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1757 |
using suminf_geometric [of "1/2::real"] by simp |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1758 |
finally show ?thesis |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1759 |
by (simp add: mult_ac) |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1760 |
qed simp |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1761 |
then have "summable (\<lambda>k. Ln (1 + z k))" |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1762 |
by (metis summable_comparison_test summable_mult z) |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1763 |
with non0 show ?thesis |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1764 |
by (simp add: add_eq_0_iff convergent_prod_iff_summable_complex) |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1765 |
qed |
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1766 |
|
68616 | 1767 |
lemma summable_Ln_complex: |
1768 |
fixes z :: "nat \<Rightarrow> complex" |
|
1769 |
assumes "convergent_prod z" "\<And>k. z k \<noteq> 0" |
|
1770 |
shows "summable (\<lambda>k. Ln (z k))" |
|
1771 |
using convergent_prod_def assms convergent_prod_iff_summable_complex by blast |
|
1772 |
||
68586
006da53a8ac1
infinite products: the final piece
paulson <lp15@cam.ac.uk>
parents:
68585
diff
changeset
|
1773 |
|
68651 | 1774 |
subsection%unimportant \<open>Embeddings from the reals into some complete real normed field\<close> |
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1775 |
|
68426 | 1776 |
lemma tendsto_eq_of_real_lim: |
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1777 |
assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1778 |
shows "q = of_real (lim f)" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1779 |
proof - |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1780 |
have "convergent (\<lambda>n. of_real (f n) :: 'a)" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1781 |
using assms convergent_def by blast |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1782 |
then have "convergent f" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1783 |
unfolding convergent_def |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1784 |
by (simp add: convergent_eq_Cauchy Cauchy_def) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1785 |
then show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1786 |
by (metis LIMSEQ_unique assms convergentD sequentially_bot tendsto_Lim tendsto_of_real) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1787 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1788 |
|
68426 | 1789 |
lemma tendsto_eq_of_real: |
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1790 |
assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1791 |
obtains r where "q = of_real r" |
68426 | 1792 |
using tendsto_eq_of_real_lim assms by blast |
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1793 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1794 |
lemma has_prod_of_real_iff: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1795 |
"(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) has_prod of_real c \<longleftrightarrow> f has_prod c" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1796 |
(is "?lhs = ?rhs") |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1797 |
proof |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1798 |
assume ?lhs |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1799 |
then show ?rhs |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1800 |
apply (auto simp: prod_defs LIMSEQ_prod_0 tendsto_of_real_iff simp flip: of_real_prod) |
68426 | 1801 |
using tendsto_eq_of_real |
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1802 |
by (metis of_real_0 tendsto_of_real_iff) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1803 |
next |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1804 |
assume ?rhs |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1805 |
with tendsto_of_real_iff show ?lhs |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1806 |
by (fastforce simp: prod_defs simp flip: of_real_prod) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1807 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1808 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1809 |
end |