author | paulson <lp15@cam.ac.uk> |
Mon, 11 Jun 2018 16:23:21 +0100 | |
changeset 68426 | e0b5f2d14bf9 |
parent 68424 | 02e5a44ffe7d |
child 68452 | c027dfbfad30 |
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 |
|
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
9 |
imports Topology_Euclidean_Space |
66277 | 10 |
begin |
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
11 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
12 |
subsection\<open>Preliminaries\<close> |
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 |
|
68361 | 57 |
definition raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool" |
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> |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
61 |
definition has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80) |
68361 | 62 |
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
|
63 |
|
66277 | 64 |
definition convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where |
68361 | 65 |
"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
|
66 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
67 |
definition prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a" |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
68 |
(binder "\<Prod>" 10) |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
69 |
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
|
70 |
|
68361 | 71 |
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
|
72 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
73 |
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
|
74 |
by simp |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
75 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
76 |
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
|
77 |
by presburger |
66277 | 78 |
|
68361 | 79 |
lemma raw_has_prod_nonzero [simp]: "\<not> raw_has_prod f M 0" |
80 |
by (simp add: raw_has_prod_def) |
|
68071 | 81 |
|
68361 | 82 |
lemma raw_has_prod_eq_0: |
83 |
fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}" |
|
84 |
assumes p: "raw_has_prod f m p" and i: "f i = 0" "i \<ge> m" |
|
68136 | 85 |
shows "p = 0" |
86 |
proof - |
|
87 |
have eq0: "(\<Prod>k\<le>n. f (k+m)) = 0" if "i - m \<le> n" for n |
|
68361 | 88 |
proof - |
89 |
have "\<exists>k\<le>n. f (k + m) = 0" |
|
90 |
using i that by auto |
|
91 |
then show ?thesis |
|
92 |
by auto |
|
93 |
qed |
|
68136 | 94 |
have "(\<lambda>n. \<Prod>i\<le>n. f (i + m)) \<longlonglongrightarrow> 0" |
95 |
by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0) |
|
96 |
with p show ?thesis |
|
68361 | 97 |
unfolding raw_has_prod_def |
68136 | 98 |
using LIMSEQ_unique by blast |
99 |
qed |
|
100 |
||
68361 | 101 |
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 | 102 |
by (simp add: has_prod_def) |
68136 | 103 |
|
104 |
lemma has_prod_unique2: |
|
68361 | 105 |
fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}" |
68136 | 106 |
assumes "f has_prod a" "f has_prod b" shows "a = b" |
107 |
using assms |
|
68361 | 108 |
by (auto simp: has_prod_def raw_has_prod_eq_0) (meson raw_has_prod_def sequentially_bot tendsto_unique) |
68136 | 109 |
|
110 |
lemma has_prod_unique: |
|
68361 | 111 |
fixes f :: "nat \<Rightarrow> 'a :: {semidom,t2_space}" |
68136 | 112 |
shows "f has_prod s \<Longrightarrow> s = prodinf f" |
113 |
by (simp add: has_prod_unique2 prodinf_def the_equality) |
|
68071 | 114 |
|
66277 | 115 |
lemma convergent_prod_altdef: |
116 |
fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}" |
|
117 |
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)" |
|
118 |
proof |
|
119 |
assume "convergent_prod f" |
|
120 |
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
|
121 |
by (auto simp: prod_defs) |
66277 | 122 |
have "f i \<noteq> 0" if "i \<ge> M" for i |
123 |
proof |
|
124 |
assume "f i = 0" |
|
125 |
have **: "eventually (\<lambda>n. (\<Prod>i\<le>n. f (i+M)) = 0) sequentially" |
|
126 |
using eventually_ge_at_top[of "i - M"] |
|
127 |
proof eventually_elim |
|
128 |
case (elim n) |
|
129 |
with \<open>f i = 0\<close> and \<open>i \<ge> M\<close> show ?case |
|
130 |
by (auto intro!: bexI[of _ "i - M"] prod_zero) |
|
131 |
qed |
|
132 |
have "(\<lambda>n. (\<Prod>i\<le>n. f (i+M))) \<longlonglongrightarrow> 0" |
|
133 |
unfolding filterlim_iff |
|
134 |
by (auto dest!: eventually_nhds_x_imp_x intro!: eventually_mono[OF **]) |
|
135 |
from tendsto_unique[OF _ this *(1)] and *(2) |
|
136 |
show False by simp |
|
137 |
qed |
|
138 |
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)" |
|
139 |
by blast |
|
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
140 |
qed (auto simp: prod_defs) |
66277 | 141 |
|
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
142 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
143 |
subsection\<open>Absolutely convergent products\<close> |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
144 |
|
66277 | 145 |
definition abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where |
146 |
"abs_convergent_prod f \<longleftrightarrow> convergent_prod (\<lambda>i. 1 + norm (f i - 1))" |
|
147 |
||
148 |
lemma abs_convergent_prodI: |
|
149 |
assumes "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
150 |
shows "abs_convergent_prod f" |
|
151 |
proof - |
|
152 |
from assms obtain L where L: "(\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1)) \<longlonglongrightarrow> L" |
|
153 |
by (auto simp: convergent_def) |
|
154 |
have "L \<ge> 1" |
|
155 |
proof (rule tendsto_le) |
|
156 |
show "eventually (\<lambda>n. (\<Prod>i\<le>n. 1 + norm (f i - 1)) \<ge> 1) sequentially" |
|
157 |
proof (intro always_eventually allI) |
|
158 |
fix n |
|
159 |
have "(\<Prod>i\<le>n. 1 + norm (f i - 1)) \<ge> (\<Prod>i\<le>n. 1)" |
|
160 |
by (intro prod_mono) auto |
|
161 |
thus "(\<Prod>i\<le>n. 1 + norm (f i - 1)) \<ge> 1" by simp |
|
162 |
qed |
|
163 |
qed (use L in simp_all) |
|
164 |
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
|
165 |
with L show ?thesis unfolding abs_convergent_prod_def prod_defs |
66277 | 166 |
by (intro exI[of _ "0::nat"] exI[of _ L]) auto |
167 |
qed |
|
168 |
||
169 |
lemma |
|
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
170 |
fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}" |
66277 | 171 |
assumes "convergent_prod f" |
172 |
shows convergent_prod_imp_convergent: "convergent (\<lambda>n. \<Prod>i\<le>n. f i)" |
|
173 |
and convergent_prod_to_zero_iff: "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)" |
|
174 |
proof - |
|
175 |
from assms obtain M L |
|
176 |
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" |
|
177 |
by (auto simp: convergent_prod_altdef) |
|
178 |
note this(2) |
|
179 |
also have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) = (\<lambda>n. \<Prod>i=M..M+n. f i)" |
|
180 |
by (intro ext prod.reindex_bij_witness[of _ "\<lambda>n. n - M" "\<lambda>n. n + M"]) auto |
|
181 |
finally have "(\<lambda>n. (\<Prod>i<M. f i) * (\<Prod>i=M..M+n. f i)) \<longlonglongrightarrow> (\<Prod>i<M. f i) * L" |
|
182 |
by (intro tendsto_mult tendsto_const) |
|
183 |
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))" |
|
184 |
by (subst prod.union_disjoint) auto |
|
185 |
also have "(\<lambda>n. {..<M} \<union> {M..M+n}) = (\<lambda>n. {..n+M})" by auto |
|
186 |
finally have lim: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * L" |
|
187 |
by (rule LIMSEQ_offset) |
|
188 |
thus "convergent (\<lambda>n. \<Prod>i\<le>n. f i)" |
|
189 |
by (auto simp: convergent_def) |
|
190 |
||
191 |
show "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)" |
|
192 |
proof |
|
193 |
assume "\<exists>i. f i = 0" |
|
194 |
then obtain i where "f i = 0" by auto |
|
195 |
moreover with M have "i < M" by (cases "i < M") auto |
|
196 |
ultimately have "(\<Prod>i<M. f i) = 0" by auto |
|
197 |
with lim show "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0" by simp |
|
198 |
next |
|
199 |
assume "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0" |
|
200 |
from tendsto_unique[OF _ this lim] and \<open>L \<noteq> 0\<close> |
|
201 |
show "\<exists>i. f i = 0" by auto |
|
202 |
qed |
|
203 |
qed |
|
204 |
||
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
205 |
lemma convergent_prod_iff_nz_lim: |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
206 |
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
|
207 |
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
|
208 |
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
|
209 |
(is "?lhs \<longleftrightarrow> ?rhs") |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
210 |
proof |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
211 |
assume ?lhs then show ?rhs |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
212 |
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
|
213 |
next |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
214 |
assume ?rhs then show ?lhs |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
215 |
unfolding prod_defs |
68138 | 216 |
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
|
217 |
qed |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
218 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
219 |
lemma convergent_prod_iff_convergent: |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
220 |
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
|
221 |
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
|
222 |
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 | 223 |
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
|
224 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
225 |
|
66277 | 226 |
lemma abs_convergent_prod_altdef: |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
227 |
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
|
228 |
shows "abs_convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
66277 | 229 |
proof |
230 |
assume "abs_convergent_prod f" |
|
231 |
thus "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
232 |
by (auto simp: abs_convergent_prod_def intro!: convergent_prod_imp_convergent) |
|
233 |
qed (auto intro: abs_convergent_prodI) |
|
234 |
||
235 |
lemma weierstrass_prod_ineq: |
|
236 |
fixes f :: "'a \<Rightarrow> real" |
|
237 |
assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> {0..1}" |
|
238 |
shows "1 - sum f A \<le> (\<Prod>x\<in>A. 1 - f x)" |
|
239 |
using assms |
|
240 |
proof (induction A rule: infinite_finite_induct) |
|
241 |
case (insert x A) |
|
242 |
from insert.hyps and insert.prems |
|
243 |
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)" |
|
244 |
by (intro insert.IH add_mono mult_left_mono prod_mono) auto |
|
245 |
with insert.hyps show ?case by (simp add: algebra_simps) |
|
246 |
qed simp_all |
|
247 |
||
248 |
lemma norm_prod_minus1_le_prod_minus1: |
|
249 |
fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,comm_ring_1}" |
|
250 |
shows "norm (prod (\<lambda>n. 1 + f n) A - 1) \<le> prod (\<lambda>n. 1 + norm (f n)) A - 1" |
|
251 |
proof (induction A rule: infinite_finite_induct) |
|
252 |
case (insert x A) |
|
253 |
from insert.hyps have |
|
254 |
"norm ((\<Prod>n\<in>insert x A. 1 + f n) - 1) = |
|
255 |
norm ((\<Prod>n\<in>A. 1 + f n) - 1 + f x * (\<Prod>n\<in>A. 1 + f n))" |
|
256 |
by (simp add: algebra_simps) |
|
257 |
also have "\<dots> \<le> norm ((\<Prod>n\<in>A. 1 + f n) - 1) + norm (f x * (\<Prod>n\<in>A. 1 + f n))" |
|
258 |
by (rule norm_triangle_ineq) |
|
259 |
also have "norm (f x * (\<Prod>n\<in>A. 1 + f n)) = norm (f x) * (\<Prod>x\<in>A. norm (1 + f x))" |
|
260 |
by (simp add: prod_norm norm_mult) |
|
261 |
also have "(\<Prod>x\<in>A. norm (1 + f x)) \<le> (\<Prod>x\<in>A. norm (1::'a) + norm (f x))" |
|
262 |
by (intro prod_mono norm_triangle_ineq ballI conjI) auto |
|
263 |
also have "norm (1::'a) = 1" by simp |
|
264 |
also note insert.IH |
|
265 |
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
|
266 |
(\<Prod>n\<in>insert x A. 1 + norm (f n)) - 1" |
66277 | 267 |
using insert.hyps by (simp add: algebra_simps) |
268 |
finally show ?case by - (simp_all add: mult_left_mono) |
|
269 |
qed simp_all |
|
270 |
||
271 |
lemma convergent_prod_imp_ev_nonzero: |
|
272 |
fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}" |
|
273 |
assumes "convergent_prod f" |
|
274 |
shows "eventually (\<lambda>n. f n \<noteq> 0) sequentially" |
|
275 |
using assms by (auto simp: eventually_at_top_linorder convergent_prod_altdef) |
|
276 |
||
277 |
lemma convergent_prod_imp_LIMSEQ: |
|
278 |
fixes f :: "nat \<Rightarrow> 'a :: {real_normed_field}" |
|
279 |
assumes "convergent_prod f" |
|
280 |
shows "f \<longlonglongrightarrow> 1" |
|
281 |
proof - |
|
282 |
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" |
|
283 |
by (auto simp: convergent_prod_altdef) |
|
284 |
hence L': "(\<lambda>n. \<Prod>i\<le>Suc n. f (i+M)) \<longlonglongrightarrow> L" by (subst filterlim_sequentially_Suc) |
|
285 |
have "(\<lambda>n. (\<Prod>i\<le>Suc n. f (i+M)) / (\<Prod>i\<le>n. f (i+M))) \<longlonglongrightarrow> L / L" |
|
286 |
using L L' by (intro tendsto_divide) simp_all |
|
287 |
also from L have "L / L = 1" by simp |
|
288 |
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))" |
|
289 |
using assms L by (auto simp: fun_eq_iff atMost_Suc) |
|
290 |
finally show ?thesis by (rule LIMSEQ_offset) |
|
291 |
qed |
|
292 |
||
293 |
lemma abs_convergent_prod_imp_summable: |
|
294 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra" |
|
295 |
assumes "abs_convergent_prod f" |
|
296 |
shows "summable (\<lambda>i. norm (f i - 1))" |
|
297 |
proof - |
|
298 |
from assms have "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
299 |
unfolding abs_convergent_prod_def by (rule convergent_prod_imp_convergent) |
|
300 |
then obtain L where L: "(\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1)) \<longlonglongrightarrow> L" |
|
301 |
unfolding convergent_def by blast |
|
302 |
have "convergent (\<lambda>n. \<Sum>i\<le>n. norm (f i - 1))" |
|
303 |
proof (rule Bseq_monoseq_convergent) |
|
304 |
have "eventually (\<lambda>n. (\<Prod>i\<le>n. 1 + norm (f i - 1)) < L + 1) sequentially" |
|
305 |
using L(1) by (rule order_tendstoD) simp_all |
|
306 |
hence "\<forall>\<^sub>F x in sequentially. norm (\<Sum>i\<le>x. norm (f i - 1)) \<le> L + 1" |
|
307 |
proof eventually_elim |
|
308 |
case (elim n) |
|
309 |
have "norm (\<Sum>i\<le>n. norm (f i - 1)) = (\<Sum>i\<le>n. norm (f i - 1))" |
|
310 |
unfolding real_norm_def by (intro abs_of_nonneg sum_nonneg) simp_all |
|
311 |
also have "\<dots> \<le> (\<Prod>i\<le>n. 1 + norm (f i - 1))" by (rule sum_le_prod) auto |
|
312 |
also have "\<dots> < L + 1" by (rule elim) |
|
313 |
finally show ?case by simp |
|
314 |
qed |
|
315 |
thus "Bseq (\<lambda>n. \<Sum>i\<le>n. norm (f i - 1))" by (rule BfunI) |
|
316 |
next |
|
317 |
show "monoseq (\<lambda>n. \<Sum>i\<le>n. norm (f i - 1))" |
|
318 |
by (rule mono_SucI1) auto |
|
319 |
qed |
|
320 |
thus "summable (\<lambda>i. norm (f i - 1))" by (simp add: summable_iff_convergent') |
|
321 |
qed |
|
322 |
||
323 |
lemma summable_imp_abs_convergent_prod: |
|
324 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra" |
|
325 |
assumes "summable (\<lambda>i. norm (f i - 1))" |
|
326 |
shows "abs_convergent_prod f" |
|
327 |
proof (intro abs_convergent_prodI Bseq_monoseq_convergent) |
|
328 |
show "monoseq (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
329 |
by (intro mono_SucI1) |
|
330 |
(auto simp: atMost_Suc algebra_simps intro!: mult_nonneg_nonneg prod_nonneg) |
|
331 |
next |
|
332 |
show "Bseq (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))" |
|
333 |
proof (rule Bseq_eventually_mono) |
|
334 |
show "eventually (\<lambda>n. norm (\<Prod>i\<le>n. 1 + norm (f i - 1)) \<le> |
|
335 |
norm (exp (\<Sum>i\<le>n. norm (f i - 1)))) sequentially" |
|
336 |
by (intro always_eventually allI) (auto simp: abs_prod exp_sum intro!: prod_mono) |
|
337 |
next |
|
338 |
from assms have "(\<lambda>n. \<Sum>i\<le>n. norm (f i - 1)) \<longlonglongrightarrow> (\<Sum>i. norm (f i - 1))" |
|
339 |
using sums_def_le by blast |
|
340 |
hence "(\<lambda>n. exp (\<Sum>i\<le>n. norm (f i - 1))) \<longlonglongrightarrow> exp (\<Sum>i. norm (f i - 1))" |
|
341 |
by (rule tendsto_exp) |
|
342 |
hence "convergent (\<lambda>n. exp (\<Sum>i\<le>n. norm (f i - 1)))" |
|
343 |
by (rule convergentI) |
|
344 |
thus "Bseq (\<lambda>n. exp (\<Sum>i\<le>n. norm (f i - 1)))" |
|
345 |
by (rule convergent_imp_Bseq) |
|
346 |
qed |
|
347 |
qed |
|
348 |
||
349 |
lemma abs_convergent_prod_conv_summable: |
|
350 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra" |
|
351 |
shows "abs_convergent_prod f \<longleftrightarrow> summable (\<lambda>i. norm (f i - 1))" |
|
352 |
by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod) |
|
353 |
||
354 |
lemma abs_convergent_prod_imp_LIMSEQ: |
|
355 |
fixes f :: "nat \<Rightarrow> 'a :: {comm_ring_1,real_normed_div_algebra}" |
|
356 |
assumes "abs_convergent_prod f" |
|
357 |
shows "f \<longlonglongrightarrow> 1" |
|
358 |
proof - |
|
359 |
from assms have "summable (\<lambda>n. norm (f n - 1))" |
|
360 |
by (rule abs_convergent_prod_imp_summable) |
|
361 |
from summable_LIMSEQ_zero[OF this] have "(\<lambda>n. f n - 1) \<longlonglongrightarrow> 0" |
|
362 |
by (simp add: tendsto_norm_zero_iff) |
|
363 |
from tendsto_add[OF this tendsto_const[of 1]] show ?thesis by simp |
|
364 |
qed |
|
365 |
||
366 |
lemma abs_convergent_prod_imp_ev_nonzero: |
|
367 |
fixes f :: "nat \<Rightarrow> 'a :: {comm_ring_1,real_normed_div_algebra}" |
|
368 |
assumes "abs_convergent_prod f" |
|
369 |
shows "eventually (\<lambda>n. f n \<noteq> 0) sequentially" |
|
370 |
proof - |
|
371 |
from assms have "f \<longlonglongrightarrow> 1" |
|
372 |
by (rule abs_convergent_prod_imp_LIMSEQ) |
|
373 |
hence "eventually (\<lambda>n. dist (f n) 1 < 1) at_top" |
|
374 |
by (auto simp: tendsto_iff) |
|
375 |
thus ?thesis by eventually_elim auto |
|
376 |
qed |
|
377 |
||
378 |
lemma convergent_prod_offset: |
|
379 |
assumes "convergent_prod (\<lambda>n. f (n + m))" |
|
380 |
shows "convergent_prod f" |
|
381 |
proof - |
|
382 |
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
|
383 |
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
|
384 |
thus "convergent_prod f" |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
385 |
unfolding prod_defs by blast |
66277 | 386 |
qed |
387 |
||
388 |
lemma abs_convergent_prod_offset: |
|
389 |
assumes "abs_convergent_prod (\<lambda>n. f (n + m))" |
|
390 |
shows "abs_convergent_prod f" |
|
391 |
using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset) |
|
392 |
||
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
393 |
subsection\<open>Ignoring initial segments\<close> |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
394 |
|
68361 | 395 |
lemma raw_has_prod_ignore_initial_segment: |
396 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" |
|
397 |
assumes "raw_has_prod f M p" "N \<ge> M" |
|
398 |
obtains q where "raw_has_prod f N q" |
|
66277 | 399 |
proof - |
68361 | 400 |
have p: "(\<lambda>n. \<Prod>k\<le>n. f (k + M)) \<longlonglongrightarrow> p" and "p \<noteq> 0" |
401 |
using assms by (auto simp: raw_has_prod_def) |
|
402 |
then have nz: "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0" |
|
403 |
using assms by (auto simp: raw_has_prod_eq_0) |
|
404 |
define C where "C = (\<Prod>k<N-M. f (k + M))" |
|
66277 | 405 |
from nz have [simp]: "C \<noteq> 0" |
406 |
by (auto simp: C_def) |
|
407 |
||
68361 | 408 |
from p have "(\<lambda>i. \<Prod>k\<le>i + (N-M). f (k + M)) \<longlonglongrightarrow> p" |
66277 | 409 |
by (rule LIMSEQ_ignore_initial_segment) |
68361 | 410 |
also have "(\<lambda>i. \<Prod>k\<le>i + (N-M). f (k + M)) = (\<lambda>n. C * (\<Prod>k\<le>n. f (k + N)))" |
66277 | 411 |
proof (rule ext, goal_cases) |
412 |
case (1 n) |
|
68361 | 413 |
have "{..n+(N-M)} = {..<(N-M)} \<union> {(N-M)..n+(N-M)}" by auto |
414 |
also have "(\<Prod>k\<in>\<dots>. f (k + M)) = C * (\<Prod>k=(N-M)..n+(N-M). f (k + M))" |
|
66277 | 415 |
unfolding C_def by (rule prod.union_disjoint) auto |
68361 | 416 |
also have "(\<Prod>k=(N-M)..n+(N-M). f (k + M)) = (\<Prod>k\<le>n. f (k + (N-M) + M))" |
417 |
by (intro ext prod.reindex_bij_witness[of _ "\<lambda>k. k + (N-M)" "\<lambda>k. k - (N-M)"]) auto |
|
418 |
finally show ?case |
|
419 |
using \<open>N \<ge> M\<close> by (simp add: add_ac) |
|
66277 | 420 |
qed |
68361 | 421 |
finally have "(\<lambda>n. C * (\<Prod>k\<le>n. f (k + N)) / C) \<longlonglongrightarrow> p / C" |
66277 | 422 |
by (intro tendsto_divide tendsto_const) auto |
68361 | 423 |
hence "(\<lambda>n. \<Prod>k\<le>n. f (k + N)) \<longlonglongrightarrow> p / C" by simp |
424 |
moreover from \<open>p \<noteq> 0\<close> have "p / C \<noteq> 0" by simp |
|
425 |
ultimately show ?thesis |
|
426 |
using raw_has_prod_def that by blast |
|
66277 | 427 |
qed |
428 |
||
68361 | 429 |
corollary convergent_prod_ignore_initial_segment: |
430 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" |
|
431 |
assumes "convergent_prod f" |
|
432 |
shows "convergent_prod (\<lambda>n. f (n + m))" |
|
433 |
using assms |
|
434 |
unfolding convergent_prod_def |
|
435 |
apply clarify |
|
436 |
apply (erule_tac N="M+m" in raw_has_prod_ignore_initial_segment) |
|
437 |
apply (auto simp add: raw_has_prod_def add_ac) |
|
438 |
done |
|
439 |
||
68136 | 440 |
corollary convergent_prod_ignore_nonzero_segment: |
441 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" |
|
442 |
assumes f: "convergent_prod f" and nz: "\<And>i. i \<ge> M \<Longrightarrow> f i \<noteq> 0" |
|
68361 | 443 |
shows "\<exists>p. raw_has_prod f M p" |
68136 | 444 |
using convergent_prod_ignore_initial_segment [OF f] |
445 |
by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1)) |
|
446 |
||
447 |
corollary abs_convergent_prod_ignore_initial_segment: |
|
66277 | 448 |
assumes "abs_convergent_prod f" |
449 |
shows "abs_convergent_prod (\<lambda>n. f (n + m))" |
|
450 |
using assms unfolding abs_convergent_prod_def |
|
451 |
by (rule convergent_prod_ignore_initial_segment) |
|
452 |
||
453 |
lemma abs_convergent_prod_imp_convergent_prod: |
|
454 |
fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}" |
|
455 |
assumes "abs_convergent_prod f" |
|
456 |
shows "convergent_prod f" |
|
457 |
proof - |
|
458 |
from assms have "eventually (\<lambda>n. f n \<noteq> 0) sequentially" |
|
459 |
by (rule abs_convergent_prod_imp_ev_nonzero) |
|
460 |
then obtain N where N: "f n \<noteq> 0" if "n \<ge> N" for n |
|
461 |
by (auto simp: eventually_at_top_linorder) |
|
462 |
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)" |
|
463 |
||
464 |
have "Cauchy ?P" |
|
465 |
proof (rule CauchyI', goal_cases) |
|
466 |
case (1 \<epsilon>) |
|
467 |
from assms have "abs_convergent_prod (\<lambda>n. f (n + N))" |
|
468 |
by (rule abs_convergent_prod_ignore_initial_segment) |
|
469 |
hence "Cauchy ?Q" |
|
470 |
unfolding abs_convergent_prod_def |
|
471 |
by (intro convergent_Cauchy convergent_prod_imp_convergent) |
|
472 |
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 |
|
473 |
by blast |
|
474 |
show ?case |
|
475 |
proof (rule exI[of _ M], safe, goal_cases) |
|
476 |
case (1 m n) |
|
477 |
have "dist (?P m) (?P n) = norm (?P n - ?P m)" |
|
478 |
by (simp add: dist_norm norm_minus_commute) |
|
479 |
also from 1 have "{..n} = {..m} \<union> {m<..n}" by auto |
|
480 |
hence "norm (?P n - ?P m) = norm (?P m * (\<Prod>k\<in>{m<..n}. f (k + N)) - ?P m)" |
|
481 |
by (subst prod.union_disjoint [symmetric]) (auto simp: algebra_simps) |
|
482 |
also have "\<dots> = norm (?P m * ((\<Prod>k\<in>{m<..n}. f (k + N)) - 1))" |
|
483 |
by (simp add: algebra_simps) |
|
484 |
also have "\<dots> = (\<Prod>k\<le>m. norm (f (k + N))) * norm ((\<Prod>k\<in>{m<..n}. f (k + N)) - 1)" |
|
485 |
by (simp add: norm_mult prod_norm) |
|
486 |
also have "\<dots> \<le> ?Q m * ((\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N) - 1)) - 1)" |
|
487 |
using norm_prod_minus1_le_prod_minus1[of "\<lambda>k. f (k + N) - 1" "{m<..n}"] |
|
488 |
norm_triangle_ineq[of 1 "f k - 1" for k] |
|
489 |
by (intro mult_mono prod_mono ballI conjI norm_prod_minus1_le_prod_minus1 prod_nonneg) auto |
|
490 |
also have "\<dots> = ?Q m * (\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N) - 1)) - ?Q m" |
|
491 |
by (simp add: algebra_simps) |
|
492 |
also have "?Q m * (\<Prod>k\<in>{m<..n}. 1 + norm (f (k + N) - 1)) = |
|
493 |
(\<Prod>k\<in>{..m}\<union>{m<..n}. 1 + norm (f (k + N) - 1))" |
|
494 |
by (rule prod.union_disjoint [symmetric]) auto |
|
495 |
also from 1 have "{..m}\<union>{m<..n} = {..n}" by auto |
|
496 |
also have "?Q n - ?Q m \<le> norm (?Q n - ?Q m)" by simp |
|
497 |
also from 1 have "\<dots> < \<epsilon>" by (intro M) auto |
|
498 |
finally show ?case . |
|
499 |
qed |
|
500 |
qed |
|
501 |
hence conv: "convergent ?P" by (rule Cauchy_convergent) |
|
502 |
then obtain L where L: "?P \<longlonglongrightarrow> L" |
|
503 |
by (auto simp: convergent_def) |
|
504 |
||
505 |
have "L \<noteq> 0" |
|
506 |
proof |
|
507 |
assume [simp]: "L = 0" |
|
508 |
from tendsto_norm[OF L] have limit: "(\<lambda>n. \<Prod>k\<le>n. norm (f (k + N))) \<longlonglongrightarrow> 0" |
|
509 |
by (simp add: prod_norm) |
|
510 |
||
511 |
from assms have "(\<lambda>n. f (n + N)) \<longlonglongrightarrow> 1" |
|
512 |
by (intro abs_convergent_prod_imp_LIMSEQ abs_convergent_prod_ignore_initial_segment) |
|
513 |
hence "eventually (\<lambda>n. norm (f (n + N) - 1) < 1) sequentially" |
|
514 |
by (auto simp: tendsto_iff dist_norm) |
|
515 |
then obtain M0 where M0: "norm (f (n + N) - 1) < 1" if "n \<ge> M0" for n |
|
516 |
by (auto simp: eventually_at_top_linorder) |
|
517 |
||
518 |
{ |
|
519 |
fix M assume M: "M \<ge> M0" |
|
520 |
with M0 have M: "norm (f (n + N) - 1) < 1" if "n \<ge> M" for n using that by simp |
|
521 |
||
522 |
have "(\<lambda>n. \<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<longlonglongrightarrow> 0" |
|
523 |
proof (rule tendsto_sandwich) |
|
524 |
show "eventually (\<lambda>n. (\<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<ge> 0) sequentially" |
|
525 |
using M by (intro always_eventually prod_nonneg allI ballI) (auto intro: less_imp_le) |
|
526 |
have "norm (1::'a) - norm (f (i + M + N) - 1) \<le> norm (f (i + M + N))" for i |
|
527 |
using norm_triangle_ineq3[of "f (i + M + N)" 1] by simp |
|
528 |
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" |
|
529 |
using M by (intro always_eventually allI prod_mono ballI conjI) (auto intro: less_imp_le) |
|
530 |
||
531 |
define C where "C = (\<Prod>k<M. norm (f (k + N)))" |
|
532 |
from N have [simp]: "C \<noteq> 0" by (auto simp: C_def) |
|
533 |
from L have "(\<lambda>n. norm (\<Prod>k\<le>n+M. f (k + N))) \<longlonglongrightarrow> 0" |
|
534 |
by (intro LIMSEQ_ignore_initial_segment) (simp add: tendsto_norm_zero_iff) |
|
535 |
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))))" |
|
536 |
proof (rule ext, goal_cases) |
|
537 |
case (1 n) |
|
538 |
have "{..n+M} = {..<M} \<union> {M..n+M}" by auto |
|
539 |
also have "norm (\<Prod>k\<in>\<dots>. f (k + N)) = C * norm (\<Prod>k=M..n+M. f (k + N))" |
|
540 |
unfolding C_def by (subst prod.union_disjoint) (auto simp: norm_mult prod_norm) |
|
541 |
also have "(\<Prod>k=M..n+M. f (k + N)) = (\<Prod>k\<le>n. f (k + N + M))" |
|
542 |
by (intro prod.reindex_bij_witness[of _ "\<lambda>i. i + M" "\<lambda>i. i - M"]) auto |
|
543 |
finally show ?case by (simp add: add_ac prod_norm) |
|
544 |
qed |
|
545 |
finally have "(\<lambda>n. C * (\<Prod>k\<le>n. norm (f (k + M + N))) / C) \<longlonglongrightarrow> 0 / C" |
|
546 |
by (intro tendsto_divide tendsto_const) auto |
|
547 |
thus "(\<lambda>n. \<Prod>k\<le>n. norm (f (k + M + N))) \<longlonglongrightarrow> 0" by simp |
|
548 |
qed simp_all |
|
549 |
||
550 |
have "1 - (\<Sum>i. norm (f (i + M + N) - 1)) \<le> 0" |
|
551 |
proof (rule tendsto_le) |
|
552 |
show "eventually (\<lambda>n. 1 - (\<Sum>k\<le>n. norm (f (k+M+N) - 1)) \<le> |
|
553 |
(\<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1))) at_top" |
|
554 |
using M by (intro always_eventually allI weierstrass_prod_ineq) (auto intro: less_imp_le) |
|
555 |
show "(\<lambda>n. \<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<longlonglongrightarrow> 0" by fact |
|
556 |
show "(\<lambda>n. 1 - (\<Sum>k\<le>n. norm (f (k + M + N) - 1))) |
|
557 |
\<longlonglongrightarrow> 1 - (\<Sum>i. norm (f (i + M + N) - 1))" |
|
558 |
by (intro tendsto_intros summable_LIMSEQ' summable_ignore_initial_segment |
|
559 |
abs_convergent_prod_imp_summable assms) |
|
560 |
qed simp_all |
|
561 |
hence "(\<Sum>i. norm (f (i + M + N) - 1)) \<ge> 1" by simp |
|
562 |
also have "\<dots> + (\<Sum>i<M. norm (f (i + N) - 1)) = (\<Sum>i. norm (f (i + N) - 1))" |
|
563 |
by (intro suminf_split_initial_segment [symmetric] summable_ignore_initial_segment |
|
564 |
abs_convergent_prod_imp_summable assms) |
|
565 |
finally have "1 + (\<Sum>i<M. norm (f (i + N) - 1)) \<le> (\<Sum>i. norm (f (i + N) - 1))" by simp |
|
566 |
} note * = this |
|
567 |
||
568 |
have "1 + (\<Sum>i. norm (f (i + N) - 1)) \<le> (\<Sum>i. norm (f (i + N) - 1))" |
|
569 |
proof (rule tendsto_le) |
|
570 |
show "(\<lambda>M. 1 + (\<Sum>i<M. norm (f (i + N) - 1))) \<longlonglongrightarrow> 1 + (\<Sum>i. norm (f (i + N) - 1))" |
|
571 |
by (intro tendsto_intros summable_LIMSEQ summable_ignore_initial_segment |
|
572 |
abs_convergent_prod_imp_summable assms) |
|
573 |
show "eventually (\<lambda>M. 1 + (\<Sum>i<M. norm (f (i + N) - 1)) \<le> (\<Sum>i. norm (f (i + N) - 1))) at_top" |
|
574 |
using eventually_ge_at_top[of M0] by eventually_elim (use * in auto) |
|
575 |
qed simp_all |
|
576 |
thus False by simp |
|
577 |
qed |
|
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
578 |
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
|
579 |
qed |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
580 |
|
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
581 |
subsection\<open>More elementary properties\<close> |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
582 |
|
68361 | 583 |
lemma raw_has_prod_cases: |
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
584 |
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}" |
68361 | 585 |
assumes "raw_has_prod f M p" |
586 |
obtains i where "i<M" "f i = 0" | p where "raw_has_prod f 0 p" |
|
68136 | 587 |
proof - |
588 |
have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0" |
|
68361 | 589 |
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
|
590 |
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
|
591 |
by (metis tendsto_mult_left) |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
592 |
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
|
593 |
proof - |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
594 |
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
|
595 |
by auto |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
596 |
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
|
597 |
by simp (subst prod.union_disjoint; force) |
68138 | 598 |
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
|
599 |
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
|
600 |
finally show ?thesis by metis |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
601 |
qed |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
602 |
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
|
603 |
by (auto intro: LIMSEQ_offset [where k=M]) |
68361 | 604 |
then have "raw_has_prod f 0 (prod f {..<M} * p)" if "\<forall>i<M. f i \<noteq> 0" |
605 |
using \<open>p \<noteq> 0\<close> assms that by (auto simp: raw_has_prod_def) |
|
68136 | 606 |
then show thesis |
607 |
using that by blast |
|
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
608 |
qed |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
609 |
|
68136 | 610 |
corollary convergent_prod_offset_0: |
611 |
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}" |
|
612 |
assumes "convergent_prod f" "\<And>i. f i \<noteq> 0" |
|
68361 | 613 |
shows "\<exists>p. raw_has_prod f 0 p" |
614 |
using assms convergent_prod_def raw_has_prod_cases by blast |
|
68136 | 615 |
|
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
616 |
lemma prodinf_eq_lim: |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
617 |
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
|
618 |
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
|
619 |
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
|
620 |
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
|
621 |
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
|
622 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
623 |
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
|
624 |
unfolding prod_defs by auto |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
625 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
626 |
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
|
627 |
unfolding prod_defs by auto |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
628 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
629 |
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
|
630 |
by presburger |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
631 |
|
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
632 |
lemma convergent_prod_cong: |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
633 |
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
|
634 |
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
|
635 |
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
|
636 |
proof - |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
637 |
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
|
638 |
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
|
639 |
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
|
640 |
with g have "C \<noteq> 0" |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
641 |
by (simp add: f) |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
642 |
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
|
643 |
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
|
644 |
proof eventually_elim |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
645 |
case (elim n) |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
646 |
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
|
647 |
by auto |
68138 | 648 |
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
|
649 |
by (intro prod.union_disjoint) auto |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
650 |
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
|
651 |
by (intro prod.cong) simp_all |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
652 |
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
|
653 |
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
|
654 |
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
|
655 |
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
|
656 |
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
|
657 |
by auto |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
658 |
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
|
659 |
qed |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
660 |
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
|
661 |
by (rule convergent_cong) |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
662 |
show ?thesis |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
663 |
proof |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
664 |
assume cf: "convergent_prod f" |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
665 |
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
|
666 |
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
|
667 |
then show "convergent_prod g" |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
668 |
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
|
669 |
next |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
670 |
assume cg: "convergent_prod g" |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
671 |
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
|
672 |
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
|
673 |
then show "convergent_prod f" |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
674 |
using "*" tendsto_mult_left filterlim_cong |
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
675 |
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
|
676 |
qed |
66277 | 677 |
qed |
678 |
||
68071 | 679 |
lemma has_prod_finite: |
68361 | 680 |
fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}" |
68071 | 681 |
assumes [simp]: "finite N" |
682 |
and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1" |
|
683 |
shows "f has_prod (\<Prod>n\<in>N. f n)" |
|
684 |
proof - |
|
685 |
have eq: "prod f {..n + Suc (Max N)} = prod f N" for n |
|
686 |
proof (rule prod.mono_neutral_right) |
|
687 |
show "N \<subseteq> {..n + Suc (Max N)}" |
|
68138 | 688 |
by (auto simp: le_Suc_eq trans_le_add2) |
68071 | 689 |
show "\<forall>i\<in>{..n + Suc (Max N)} - N. f i = 1" |
690 |
using f by blast |
|
691 |
qed auto |
|
692 |
show ?thesis |
|
693 |
proof (cases "\<forall>n\<in>N. f n \<noteq> 0") |
|
694 |
case True |
|
695 |
then have "prod f N \<noteq> 0" |
|
696 |
by simp |
|
697 |
moreover have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f N" |
|
698 |
by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) (simp add: eq atLeast0LessThan del: add_Suc_right) |
|
699 |
ultimately show ?thesis |
|
68361 | 700 |
by (simp add: raw_has_prod_def has_prod_def) |
68071 | 701 |
next |
702 |
case False |
|
703 |
then obtain k where "k \<in> N" "f k = 0" |
|
704 |
by auto |
|
705 |
let ?Z = "{n \<in> N. f n = 0}" |
|
706 |
have maxge: "Max ?Z \<ge> n" if "f n = 0" for n |
|
707 |
using Max_ge [of ?Z] \<open>finite N\<close> \<open>f n = 0\<close> |
|
708 |
by (metis (mono_tags) Collect_mem_eq f finite_Collect_conjI mem_Collect_eq zero_neq_one) |
|
709 |
let ?q = "prod f {Suc (Max ?Z)..Max N}" |
|
710 |
have [simp]: "?q \<noteq> 0" |
|
711 |
using maxge Suc_n_not_le_n le_trans by force |
|
68076 | 712 |
have eq: "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = ?q" for n |
713 |
proof - |
|
714 |
have "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = prod f {Suc (Max ?Z)..n + Max N + Suc (Max ?Z)}" |
|
715 |
proof (rule prod.reindex_cong [where l = "\<lambda>i. i + Suc (Max ?Z)", THEN sym]) |
|
716 |
show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\<lambda>i. i + Suc (Max ?Z)) ` {..n + Max N}" |
|
717 |
using le_Suc_ex by fastforce |
|
718 |
qed (auto simp: inj_on_def) |
|
68138 | 719 |
also have "\<dots> = ?q" |
68076 | 720 |
by (rule prod.mono_neutral_right) |
721 |
(use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>) |
|
722 |
finally show ?thesis . |
|
723 |
qed |
|
68361 | 724 |
have q: "raw_has_prod f (Suc (Max ?Z)) ?q" |
725 |
proof (simp add: raw_has_prod_def) |
|
68076 | 726 |
show "(\<lambda>n. \<Prod>i\<le>n. f (Suc (i + Max ?Z))) \<longlonglongrightarrow> ?q" |
727 |
by (rule LIMSEQ_offset[of _ "(Max N)"]) (simp add: eq) |
|
728 |
qed |
|
68071 | 729 |
show ?thesis |
730 |
unfolding has_prod_def |
|
731 |
proof (intro disjI2 exI conjI) |
|
732 |
show "prod f N = 0" |
|
733 |
using \<open>f k = 0\<close> \<open>k \<in> N\<close> \<open>finite N\<close> prod_zero by blast |
|
734 |
show "f (Max ?Z) = 0" |
|
735 |
using Max_in [of ?Z] \<open>finite N\<close> \<open>f k = 0\<close> \<open>k \<in> N\<close> by auto |
|
736 |
qed (use q in auto) |
|
737 |
qed |
|
738 |
qed |
|
739 |
||
740 |
corollary has_prod_0: |
|
68361 | 741 |
fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}" |
68071 | 742 |
assumes "\<And>n. f n = 1" |
743 |
shows "f has_prod 1" |
|
744 |
by (simp add: assms has_prod_cong) |
|
745 |
||
68361 | 746 |
lemma prodinf_zero[simp]: "prodinf (\<lambda>n. 1::'a::real_normed_field) = 1" |
747 |
using has_prod_unique by force |
|
748 |
||
68071 | 749 |
lemma convergent_prod_finite: |
750 |
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
|
751 |
assumes "finite N" "\<And>n. n \<notin> N \<Longrightarrow> f n = 1" |
|
752 |
shows "convergent_prod f" |
|
753 |
proof - |
|
68361 | 754 |
have "\<exists>n p. raw_has_prod f n p" |
68071 | 755 |
using assms has_prod_def has_prod_finite by blast |
756 |
then show ?thesis |
|
757 |
by (simp add: convergent_prod_def) |
|
758 |
qed |
|
759 |
||
68127 | 760 |
lemma has_prod_If_finite_set: |
761 |
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
|
762 |
shows "finite A \<Longrightarrow> (\<lambda>r. if r \<in> A then f r else 1) has_prod (\<Prod>r\<in>A. f r)" |
|
763 |
using has_prod_finite[of A "(\<lambda>r. if r \<in> A then f r else 1)"] |
|
764 |
by simp |
|
765 |
||
766 |
lemma has_prod_If_finite: |
|
767 |
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
|
768 |
shows "finite {r. P r} \<Longrightarrow> (\<lambda>r. if P r then f r else 1) has_prod (\<Prod>r | P r. f r)" |
|
769 |
using has_prod_If_finite_set[of "{r. P r}"] by simp |
|
770 |
||
771 |
lemma convergent_prod_If_finite_set[simp, intro]: |
|
772 |
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
|
773 |
shows "finite A \<Longrightarrow> convergent_prod (\<lambda>r. if r \<in> A then f r else 1)" |
|
774 |
by (simp add: convergent_prod_finite) |
|
775 |
||
776 |
lemma convergent_prod_If_finite[simp, intro]: |
|
777 |
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
|
778 |
shows "finite {r. P r} \<Longrightarrow> convergent_prod (\<lambda>r. if P r then f r else 1)" |
|
779 |
using convergent_prod_def has_prod_If_finite has_prod_def by fastforce |
|
780 |
||
781 |
lemma has_prod_single: |
|
782 |
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
|
783 |
shows "(\<lambda>r. if r = i then f r else 1) has_prod f i" |
|
784 |
using has_prod_If_finite[of "\<lambda>r. r = i"] by simp |
|
785 |
||
68136 | 786 |
context |
787 |
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" |
|
788 |
begin |
|
789 |
||
790 |
lemma convergent_prod_imp_has_prod: |
|
791 |
assumes "convergent_prod f" |
|
792 |
shows "\<exists>p. f has_prod p" |
|
793 |
proof - |
|
68361 | 794 |
obtain M p where p: "raw_has_prod f M p" |
68136 | 795 |
using assms convergent_prod_def by blast |
796 |
then have "p \<noteq> 0" |
|
68361 | 797 |
using raw_has_prod_nonzero by blast |
68136 | 798 |
with p have fnz: "f i \<noteq> 0" if "i \<ge> M" for i |
68361 | 799 |
using raw_has_prod_eq_0 that by blast |
68136 | 800 |
define C where "C = (\<Prod>n<M. f n)" |
801 |
show ?thesis |
|
802 |
proof (cases "\<forall>n\<le>M. f n \<noteq> 0") |
|
803 |
case True |
|
804 |
then have "C \<noteq> 0" |
|
805 |
by (simp add: C_def) |
|
806 |
then show ?thesis |
|
807 |
by (meson True assms convergent_prod_offset_0 fnz has_prod_def nat_le_linear) |
|
808 |
next |
|
809 |
case False |
|
810 |
let ?N = "GREATEST n. f n = 0" |
|
811 |
have 0: "f ?N = 0" |
|
812 |
using fnz False |
|
813 |
by (metis (mono_tags, lifting) GreatestI_ex_nat nat_le_linear) |
|
814 |
have "f i \<noteq> 0" if "i > ?N" for i |
|
815 |
by (metis (mono_tags, lifting) Greatest_le_nat fnz leD linear that) |
|
68361 | 816 |
then have "\<exists>p. raw_has_prod f (Suc ?N) p" |
68136 | 817 |
using assms by (auto simp: intro!: convergent_prod_ignore_nonzero_segment) |
818 |
then show ?thesis |
|
819 |
unfolding has_prod_def using 0 by blast |
|
820 |
qed |
|
821 |
qed |
|
822 |
||
823 |
lemma convergent_prod_has_prod [intro]: |
|
824 |
shows "convergent_prod f \<Longrightarrow> f has_prod (prodinf f)" |
|
825 |
unfolding prodinf_def |
|
826 |
by (metis convergent_prod_imp_has_prod has_prod_unique theI') |
|
827 |
||
828 |
lemma convergent_prod_LIMSEQ: |
|
829 |
shows "convergent_prod f \<Longrightarrow> (\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> prodinf f" |
|
830 |
by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent |
|
68361 | 831 |
convergent_prod_to_zero_iff raw_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le) |
68136 | 832 |
|
833 |
lemma has_prod_iff: "f has_prod x \<longleftrightarrow> convergent_prod f \<and> prodinf f = x" |
|
834 |
proof |
|
835 |
assume "f has_prod x" |
|
836 |
then show "convergent_prod f \<and> prodinf f = x" |
|
837 |
apply safe |
|
838 |
using convergent_prod_def has_prod_def apply blast |
|
839 |
using has_prod_unique by blast |
|
840 |
qed auto |
|
841 |
||
842 |
lemma convergent_prod_has_prod_iff: "convergent_prod f \<longleftrightarrow> f has_prod prodinf f" |
|
843 |
by (auto simp: has_prod_iff convergent_prod_has_prod) |
|
844 |
||
845 |
lemma prodinf_finite: |
|
846 |
assumes N: "finite N" |
|
847 |
and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1" |
|
848 |
shows "prodinf f = (\<Prod>n\<in>N. f n)" |
|
849 |
using has_prod_finite[OF assms, THEN has_prod_unique] by simp |
|
68127 | 850 |
|
66277 | 851 |
end |
68136 | 852 |
|
68361 | 853 |
subsection \<open>Infinite products on ordered, topological monoids\<close> |
854 |
||
855 |
lemma LIMSEQ_prod_0: |
|
856 |
fixes f :: "nat \<Rightarrow> 'a::{semidom,topological_space}" |
|
857 |
assumes "f i = 0" |
|
858 |
shows "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> 0" |
|
859 |
proof (subst tendsto_cong) |
|
860 |
show "\<forall>\<^sub>F n in sequentially. prod f {..n} = 0" |
|
861 |
proof |
|
862 |
show "prod f {..n} = 0" if "n \<ge> i" for n |
|
863 |
using that assms by auto |
|
864 |
qed |
|
865 |
qed auto |
|
866 |
||
867 |
lemma LIMSEQ_prod_nonneg: |
|
868 |
fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}" |
|
869 |
assumes 0: "\<And>n. 0 \<le> f n" and a: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> a" |
|
870 |
shows "a \<ge> 0" |
|
871 |
by (simp add: "0" prod_nonneg LIMSEQ_le_const [OF a]) |
|
872 |
||
873 |
||
874 |
context |
|
875 |
fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}" |
|
876 |
begin |
|
877 |
||
878 |
lemma has_prod_le: |
|
879 |
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" |
|
880 |
shows "a \<le> b" |
|
881 |
proof (cases "a=0 \<or> b=0") |
|
882 |
case True |
|
883 |
then show ?thesis |
|
884 |
proof |
|
885 |
assume [simp]: "a=0" |
|
886 |
have "b \<ge> 0" |
|
887 |
proof (rule LIMSEQ_prod_nonneg) |
|
888 |
show "(\<lambda>n. prod g {..n}) \<longlonglongrightarrow> b" |
|
889 |
using g by (auto simp: has_prod_def raw_has_prod_def LIMSEQ_prod_0) |
|
890 |
qed (use le order_trans in auto) |
|
891 |
then show ?thesis |
|
892 |
by auto |
|
893 |
next |
|
894 |
assume [simp]: "b=0" |
|
895 |
then obtain i where "g i = 0" |
|
896 |
using g by (auto simp: prod_defs) |
|
897 |
then have "f i = 0" |
|
898 |
using antisym le by force |
|
899 |
then have "a=0" |
|
900 |
using f by (auto simp: prod_defs LIMSEQ_prod_0 LIMSEQ_unique) |
|
901 |
then show ?thesis |
|
902 |
by auto |
|
903 |
qed |
|
904 |
next |
|
905 |
case False |
|
906 |
then show ?thesis |
|
907 |
using assms |
|
908 |
unfolding has_prod_def raw_has_prod_def |
|
909 |
by (force simp: LIMSEQ_prod_0 intro!: LIMSEQ_le prod_mono) |
|
910 |
qed |
|
911 |
||
912 |
lemma prodinf_le: |
|
913 |
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" |
|
914 |
shows "prodinf f \<le> prodinf g" |
|
915 |
using has_prod_le [OF assms] has_prod_unique f g by blast |
|
916 |
||
68136 | 917 |
end |
68361 | 918 |
|
919 |
||
920 |
lemma prod_le_prodinf: |
|
921 |
fixes f :: "nat \<Rightarrow> 'a::{linordered_idom,linorder_topology}" |
|
922 |
assumes "f has_prod a" "\<And>i. 0 \<le> f i" "\<And>i. i\<ge>n \<Longrightarrow> 1 \<le> f i" |
|
923 |
shows "prod f {..<n} \<le> prodinf f" |
|
924 |
by(rule has_prod_le[OF has_prod_If_finite_set]) (use assms has_prod_unique in auto) |
|
925 |
||
926 |
lemma prodinf_nonneg: |
|
927 |
fixes f :: "nat \<Rightarrow> 'a::{linordered_idom,linorder_topology}" |
|
928 |
assumes "f has_prod a" "\<And>i. 1 \<le> f i" |
|
929 |
shows "1 \<le> prodinf f" |
|
930 |
using prod_le_prodinf[of f a 0] assms |
|
931 |
by (metis order_trans prod_ge_1 zero_le_one) |
|
932 |
||
933 |
lemma prodinf_le_const: |
|
934 |
fixes f :: "nat \<Rightarrow> real" |
|
935 |
assumes "convergent_prod f" "\<And>n. prod f {..<n} \<le> x" |
|
936 |
shows "prodinf f \<le> x" |
|
937 |
by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2) |
|
938 |
||
939 |
lemma prodinf_eq_one_iff: |
|
940 |
fixes f :: "nat \<Rightarrow> real" |
|
941 |
assumes f: "convergent_prod f" and ge1: "\<And>n. 1 \<le> f n" |
|
942 |
shows "prodinf f = 1 \<longleftrightarrow> (\<forall>n. f n = 1)" |
|
943 |
proof |
|
944 |
assume "prodinf f = 1" |
|
945 |
then have "(\<lambda>n. \<Prod>i<n. f i) \<longlonglongrightarrow> 1" |
|
946 |
using convergent_prod_LIMSEQ[of f] assms by (simp add: LIMSEQ_lessThan_iff_atMost) |
|
947 |
then have "\<And>i. (\<Prod>n\<in>{i}. f n) \<le> 1" |
|
948 |
proof (rule LIMSEQ_le_const) |
|
949 |
have "1 \<le> prod f n" for n |
|
950 |
by (simp add: ge1 prod_ge_1) |
|
951 |
have "prod f {..<n} = 1" for n |
|
952 |
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) |
|
953 |
then have "(\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" if "n \<ge> Suc i" for i n |
|
954 |
by (metis mult.left_neutral order_refl prod.cong prod.neutral_const prod_lessThan_Suc) |
|
955 |
then show "\<exists>N. \<forall>n\<ge>N. (\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" for i |
|
956 |
by blast |
|
957 |
qed |
|
958 |
with ge1 show "\<forall>n. f n = 1" |
|
959 |
by (auto intro!: antisym) |
|
960 |
qed (metis prodinf_zero fun_eq_iff) |
|
961 |
||
962 |
lemma prodinf_pos_iff: |
|
963 |
fixes f :: "nat \<Rightarrow> real" |
|
964 |
assumes "convergent_prod f" "\<And>n. 1 \<le> f n" |
|
965 |
shows "1 < prodinf f \<longleftrightarrow> (\<exists>i. 1 < f i)" |
|
966 |
using prod_le_prodinf[of f 1] prodinf_eq_one_iff |
|
967 |
by (metis convergent_prod_has_prod assms less_le prodinf_nonneg) |
|
968 |
||
969 |
lemma less_1_prodinf2: |
|
970 |
fixes f :: "nat \<Rightarrow> real" |
|
971 |
assumes "convergent_prod f" "\<And>n. 1 \<le> f n" "1 < f i" |
|
972 |
shows "1 < prodinf f" |
|
973 |
proof - |
|
974 |
have "1 < (\<Prod>n<Suc i. f n)" |
|
975 |
using assms by (intro less_1_prod2[where i=i]) auto |
|
976 |
also have "\<dots> \<le> prodinf f" |
|
977 |
by (intro prod_le_prodinf) (use assms order_trans zero_le_one in \<open>blast+\<close>) |
|
978 |
finally show ?thesis . |
|
979 |
qed |
|
980 |
||
981 |
lemma less_1_prodinf: |
|
982 |
fixes f :: "nat \<Rightarrow> real" |
|
983 |
shows "\<lbrakk>convergent_prod f; \<And>n. 1 < f n\<rbrakk> \<Longrightarrow> 1 < prodinf f" |
|
984 |
by (intro less_1_prodinf2[where i=1]) (auto intro: less_imp_le) |
|
985 |
||
986 |
lemma prodinf_nonzero: |
|
987 |
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}" |
|
988 |
assumes "convergent_prod f" "\<And>i. f i \<noteq> 0" |
|
989 |
shows "prodinf f \<noteq> 0" |
|
990 |
by (metis assms convergent_prod_offset_0 has_prod_unique raw_has_prod_def has_prod_def) |
|
991 |
||
992 |
lemma less_0_prodinf: |
|
993 |
fixes f :: "nat \<Rightarrow> real" |
|
994 |
assumes f: "convergent_prod f" and 0: "\<And>i. f i > 0" |
|
995 |
shows "0 < prodinf f" |
|
996 |
proof - |
|
997 |
have "prodinf f \<noteq> 0" |
|
998 |
by (metis assms less_irrefl prodinf_nonzero) |
|
999 |
moreover have "0 < (\<Prod>n<i. f n)" for i |
|
1000 |
by (simp add: 0 prod_pos) |
|
1001 |
then have "prodinf f \<ge> 0" |
|
1002 |
using convergent_prod_LIMSEQ [OF f] LIMSEQ_prod_nonneg 0 less_le by blast |
|
1003 |
ultimately show ?thesis |
|
1004 |
by auto |
|
1005 |
qed |
|
1006 |
||
1007 |
lemma prod_less_prodinf2: |
|
1008 |
fixes f :: "nat \<Rightarrow> real" |
|
1009 |
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" |
|
1010 |
shows "prod f {..<n} < prodinf f" |
|
1011 |
proof - |
|
1012 |
have "prod f {..<n} \<le> prod f {..<i}" |
|
1013 |
by (rule prod_mono2) (use assms less_le in auto) |
|
1014 |
then have "prod f {..<n} < f i * prod f {..<i}" |
|
1015 |
using mult_less_le_imp_less[of 1 "f i" "prod f {..<n}" "prod f {..<i}"] assms |
|
1016 |
by (simp add: prod_pos) |
|
1017 |
moreover have "prod f {..<Suc i} \<le> prodinf f" |
|
1018 |
using prod_le_prodinf[of f _ "Suc i"] |
|
1019 |
by (meson "0" "1" Suc_leD convergent_prod_has_prod f \<open>n \<le> i\<close> le_trans less_eq_real_def) |
|
1020 |
ultimately show ?thesis |
|
1021 |
by (metis le_less_trans mult.commute not_le prod_lessThan_Suc) |
|
1022 |
qed |
|
1023 |
||
1024 |
lemma prod_less_prodinf: |
|
1025 |
fixes f :: "nat \<Rightarrow> real" |
|
1026 |
assumes f: "convergent_prod f" and 1: "\<And>m. m\<ge>n \<Longrightarrow> 1 < f m" and 0: "\<And>m. 0 < f m" |
|
1027 |
shows "prod f {..<n} < prodinf f" |
|
1028 |
by (meson "0" "1" f le_less prod_less_prodinf2) |
|
1029 |
||
1030 |
lemma raw_has_prodI_bounded: |
|
1031 |
fixes f :: "nat \<Rightarrow> real" |
|
1032 |
assumes pos: "\<And>n. 1 \<le> f n" |
|
1033 |
and le: "\<And>n. (\<Prod>i<n. f i) \<le> x" |
|
1034 |
shows "\<exists>p. raw_has_prod f 0 p" |
|
1035 |
unfolding raw_has_prod_def add_0_right |
|
1036 |
proof (rule exI LIMSEQ_incseq_SUP conjI)+ |
|
1037 |
show "bdd_above (range (\<lambda>n. prod f {..n}))" |
|
1038 |
by (metis bdd_aboveI2 le lessThan_Suc_atMost) |
|
1039 |
then have "(SUP i. prod f {..i}) > 0" |
|
1040 |
by (metis UNIV_I cSUP_upper less_le_trans pos prod_pos zero_less_one) |
|
1041 |
then show "(SUP i. prod f {..i}) \<noteq> 0" |
|
1042 |
by auto |
|
1043 |
show "incseq (\<lambda>n. prod f {..n})" |
|
1044 |
using pos order_trans [OF zero_le_one] by (auto simp: mono_def intro!: prod_mono2) |
|
1045 |
qed |
|
1046 |
||
1047 |
lemma convergent_prodI_nonneg_bounded: |
|
1048 |
fixes f :: "nat \<Rightarrow> real" |
|
1049 |
assumes "\<And>n. 1 \<le> f n" "\<And>n. (\<Prod>i<n. f i) \<le> x" |
|
1050 |
shows "convergent_prod f" |
|
1051 |
using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast |
|
1052 |
||
1053 |
||
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1054 |
subsection \<open>Infinite products on topological spaces\<close> |
68361 | 1055 |
|
1056 |
context |
|
1057 |
fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_semigroup_mult,idom}" |
|
1058 |
begin |
|
1059 |
||
1060 |
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)" |
|
1061 |
by (force simp add: prod.distrib tendsto_mult raw_has_prod_def) |
|
1062 |
||
1063 |
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)" |
|
1064 |
by (simp add: raw_has_prod_mult has_prod_def) |
|
1065 |
||
1066 |
end |
|
1067 |
||
1068 |
||
1069 |
context |
|
1070 |
fixes f g :: "nat \<Rightarrow> 'a::real_normed_field" |
|
1071 |
begin |
|
1072 |
||
1073 |
lemma has_prod_mult: |
|
1074 |
assumes f: "f has_prod a" and g: "g has_prod b" |
|
1075 |
shows "(\<lambda>n. f n * g n) has_prod (a * b)" |
|
1076 |
using f [unfolded has_prod_def] |
|
1077 |
proof (elim disjE exE conjE) |
|
1078 |
assume f0: "raw_has_prod f 0 a" |
|
1079 |
show ?thesis |
|
1080 |
using g [unfolded has_prod_def] |
|
1081 |
proof (elim disjE exE conjE) |
|
1082 |
assume g0: "raw_has_prod g 0 b" |
|
1083 |
with f0 show ?thesis |
|
1084 |
by (force simp add: has_prod_def prod.distrib tendsto_mult raw_has_prod_def) |
|
1085 |
next |
|
1086 |
fix j q |
|
1087 |
assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q" |
|
1088 |
obtain p where p: "raw_has_prod f (Suc j) p" |
|
1089 |
using f0 raw_has_prod_ignore_initial_segment by blast |
|
1090 |
then have "Ex (raw_has_prod (\<lambda>n. f n * g n) (Suc j))" |
|
1091 |
using q raw_has_prod_mult by blast |
|
1092 |
then show ?thesis |
|
1093 |
using \<open>b = 0\<close> \<open>g j = 0\<close> has_prod_0_iff by fastforce |
|
1094 |
qed |
|
1095 |
next |
|
1096 |
fix i p |
|
1097 |
assume "a = 0" and "f i = 0" and p: "raw_has_prod f (Suc i) p" |
|
1098 |
show ?thesis |
|
1099 |
using g [unfolded has_prod_def] |
|
1100 |
proof (elim disjE exE conjE) |
|
1101 |
assume g0: "raw_has_prod g 0 b" |
|
1102 |
obtain q where q: "raw_has_prod g (Suc i) q" |
|
1103 |
using g0 raw_has_prod_ignore_initial_segment by blast |
|
1104 |
then have "Ex (raw_has_prod (\<lambda>n. f n * g n) (Suc i))" |
|
1105 |
using raw_has_prod_mult p by blast |
|
1106 |
then show ?thesis |
|
1107 |
using \<open>a = 0\<close> \<open>f i = 0\<close> has_prod_0_iff by fastforce |
|
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 (max i j)) p'" |
|
1112 |
by (metis raw_has_prod_ignore_initial_segment max_Suc_Suc max_def p) |
|
1113 |
moreover |
|
1114 |
obtain q' where q': "raw_has_prod g (Suc (max i j)) q'" |
|
1115 |
by (metis raw_has_prod_ignore_initial_segment max.cobounded2 max_Suc_Suc q) |
|
1116 |
ultimately show ?thesis |
|
1117 |
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) |
|
1118 |
qed |
|
1119 |
qed |
|
1120 |
||
1121 |
lemma convergent_prod_mult: |
|
1122 |
assumes f: "convergent_prod f" and g: "convergent_prod g" |
|
1123 |
shows "convergent_prod (\<lambda>n. f n * g n)" |
|
1124 |
unfolding convergent_prod_def |
|
1125 |
proof - |
|
1126 |
obtain M p N q where p: "raw_has_prod f M p" and q: "raw_has_prod g N q" |
|
1127 |
using convergent_prod_def f g by blast+ |
|
1128 |
then obtain p' q' where p': "raw_has_prod f (max M N) p'" and q': "raw_has_prod g (max M N) q'" |
|
1129 |
by (meson raw_has_prod_ignore_initial_segment max.cobounded1 max.cobounded2) |
|
1130 |
then show "\<exists>M p. raw_has_prod (\<lambda>n. f n * g n) M p" |
|
1131 |
using raw_has_prod_mult by blast |
|
1132 |
qed |
|
1133 |
||
1134 |
lemma prodinf_mult: "convergent_prod f \<Longrightarrow> convergent_prod g \<Longrightarrow> prodinf f * prodinf g = (\<Prod>n. f n * g n)" |
|
1135 |
by (intro has_prod_unique has_prod_mult convergent_prod_has_prod) |
|
1136 |
||
1137 |
end |
|
1138 |
||
1139 |
context |
|
1140 |
fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_field" |
|
1141 |
and I :: "'i set" |
|
1142 |
begin |
|
1143 |
||
1144 |
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)" |
|
1145 |
by (induct I rule: infinite_finite_induct) (auto intro!: has_prod_mult) |
|
1146 |
||
1147 |
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)" |
|
1148 |
using has_prod_unique[OF has_prod_prod, OF convergent_prod_has_prod] by simp |
|
1149 |
||
1150 |
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)" |
|
1151 |
using convergent_prod_has_prod_iff has_prod_prod prodinf_prod by force |
|
1152 |
||
1153 |
end |
|
1154 |
||
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1155 |
subsection \<open>Infinite summability on real normed fields\<close> |
68361 | 1156 |
|
1157 |
context |
|
1158 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_field" |
|
1159 |
begin |
|
1160 |
||
1161 |
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" |
|
1162 |
proof - |
|
1163 |
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" |
|
1164 |
by (subst LIMSEQ_Suc_iff) (simp add: raw_has_prod_def) |
|
1165 |
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" |
|
1166 |
by (simp add: ac_simps atMost_Suc_eq_insert_0 image_Suc_atMost prod_atLeast1_atMost_eq lessThan_Suc_atMost) |
|
1167 |
also have "\<dots> \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0" |
|
1168 |
proof safe |
|
1169 |
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" |
|
1170 |
with tendsto_divide[OF tends tendsto_const, of "f M"] |
|
1171 |
show "raw_has_prod (\<lambda>n. f (Suc n)) M a" |
|
1172 |
by (simp add: raw_has_prod_def) |
|
1173 |
qed (auto intro: tendsto_mult_right simp: raw_has_prod_def) |
|
1174 |
finally show ?thesis . |
|
1175 |
qed |
|
1176 |
||
1177 |
lemma has_prod_Suc_iff: |
|
1178 |
assumes "f 0 \<noteq> 0" shows "(\<lambda>n. f (Suc n)) has_prod a \<longleftrightarrow> f has_prod (a * f 0)" |
|
1179 |
proof (cases "a = 0") |
|
1180 |
case True |
|
1181 |
then show ?thesis |
|
1182 |
proof (simp add: has_prod_def, safe) |
|
1183 |
fix i x |
|
1184 |
assume "f (Suc i) = 0" and "raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) x" |
|
1185 |
then obtain y where "raw_has_prod f (Suc (Suc i)) y" |
|
1186 |
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) |
|
1187 |
then show "\<exists>i. f i = 0 \<and> Ex (raw_has_prod f (Suc i))" |
|
1188 |
using \<open>f (Suc i) = 0\<close> by blast |
|
1189 |
next |
|
1190 |
fix i x |
|
1191 |
assume "f i = 0" and x: "raw_has_prod f (Suc i) x" |
|
1192 |
then obtain j where j: "i = Suc j" |
|
1193 |
by (metis assms not0_implies_Suc) |
|
1194 |
moreover have "\<exists> y. raw_has_prod (\<lambda>n. f (Suc n)) i y" |
|
1195 |
using x by (auto simp: raw_has_prod_def) |
|
1196 |
then show "\<exists>i. f (Suc i) = 0 \<and> Ex (raw_has_prod (\<lambda>n. f (Suc n)) (Suc i))" |
|
1197 |
using \<open>f i = 0\<close> j by blast |
|
1198 |
qed |
|
1199 |
next |
|
1200 |
case False |
|
1201 |
then show ?thesis |
|
1202 |
by (auto simp: has_prod_def raw_has_prod_Suc_iff assms) |
|
1203 |
qed |
|
1204 |
||
1205 |
lemma convergent_prod_Suc_iff: |
|
1206 |
assumes "\<And>k. f k \<noteq> 0" shows "convergent_prod (\<lambda>n. f (Suc n)) = convergent_prod f" |
|
1207 |
proof |
|
1208 |
assume "convergent_prod f" |
|
1209 |
then have "f has_prod prodinf f" |
|
1210 |
by (rule convergent_prod_has_prod) |
|
1211 |
moreover have "prodinf f \<noteq> 0" |
|
1212 |
by (simp add: \<open>convergent_prod f\<close> assms prodinf_nonzero) |
|
1213 |
ultimately have "(\<lambda>n. f (Suc n)) has_prod (prodinf f * inverse (f 0))" |
|
1214 |
by (simp add: has_prod_Suc_iff inverse_eq_divide assms) |
|
1215 |
then show "convergent_prod (\<lambda>n. f (Suc n))" |
|
1216 |
using has_prod_iff by blast |
|
1217 |
next |
|
1218 |
assume "convergent_prod (\<lambda>n. f (Suc n))" |
|
1219 |
then show "convergent_prod f" |
|
1220 |
using assms convergent_prod_def raw_has_prod_Suc_iff by blast |
|
1221 |
qed |
|
1222 |
||
1223 |
lemma raw_has_prod_inverse: |
|
1224 |
assumes "raw_has_prod f M a" shows "raw_has_prod (\<lambda>n. inverse (f n)) M (inverse a)" |
|
1225 |
using assms unfolding raw_has_prod_def by (auto dest: tendsto_inverse simp: prod_inversef [symmetric]) |
|
1226 |
||
1227 |
lemma has_prod_inverse: |
|
1228 |
assumes "f has_prod a" shows "(\<lambda>n. inverse (f n)) has_prod (inverse a)" |
|
1229 |
using assms raw_has_prod_inverse unfolding has_prod_def by auto |
|
1230 |
||
1231 |
lemma convergent_prod_inverse: |
|
1232 |
assumes "convergent_prod f" |
|
1233 |
shows "convergent_prod (\<lambda>n. inverse (f n))" |
|
1234 |
using assms unfolding convergent_prod_def by (blast intro: raw_has_prod_inverse elim: ) |
|
1235 |
||
1236 |
end |
|
1237 |
||
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1238 |
context |
68361 | 1239 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_field" |
1240 |
begin |
|
1241 |
||
1242 |
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" |
|
1243 |
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) |
|
1244 |
||
1245 |
lemma has_prod_divide: "f has_prod a \<Longrightarrow> g has_prod b \<Longrightarrow> (\<lambda>n. f n / g n) has_prod (a / b)" |
|
1246 |
unfolding divide_inverse by (intro has_prod_inverse has_prod_mult) |
|
1247 |
||
1248 |
lemma convergent_prod_divide: |
|
1249 |
assumes f: "convergent_prod f" and g: "convergent_prod g" |
|
1250 |
shows "convergent_prod (\<lambda>n. f n / g n)" |
|
1251 |
using f g has_prod_divide has_prod_iff by blast |
|
1252 |
||
1253 |
lemma prodinf_divide: "convergent_prod f \<Longrightarrow> convergent_prod g \<Longrightarrow> prodinf f / prodinf g = (\<Prod>n. f n / g n)" |
|
1254 |
by (intro has_prod_unique has_prod_divide convergent_prod_has_prod) |
|
1255 |
||
1256 |
lemma prodinf_inverse: "convergent_prod f \<Longrightarrow> (\<Prod>n. inverse (f n)) = inverse (\<Prod>n. f n)" |
|
1257 |
by (intro has_prod_unique [symmetric] has_prod_inverse convergent_prod_has_prod) |
|
1258 |
||
1259 |
lemma has_prod_iff_shift: |
|
1260 |
assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1261 |
shows "(\<lambda>i. f (i + n)) has_prod a \<longleftrightarrow> f has_prod (a * (\<Prod>i<n. f i))" |
|
1262 |
using assms |
|
1263 |
proof (induct n arbitrary: a) |
|
1264 |
case 0 |
|
1265 |
then show ?case by simp |
|
1266 |
next |
|
1267 |
case (Suc n) |
|
1268 |
then have "(\<lambda>i. f (Suc i + n)) has_prod a \<longleftrightarrow> (\<lambda>i. f (i + n)) has_prod (a * f n)" |
|
1269 |
by (subst has_prod_Suc_iff) auto |
|
1270 |
with Suc show ?case |
|
1271 |
by (simp add: ac_simps) |
|
1272 |
qed |
|
1273 |
||
1274 |
corollary has_prod_iff_shift': |
|
1275 |
assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1276 |
shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i)) \<longleftrightarrow> f has_prod a" |
|
1277 |
by (simp add: assms has_prod_iff_shift) |
|
1278 |
||
1279 |
lemma has_prod_one_iff_shift: |
|
1280 |
assumes "\<And>i. i < n \<Longrightarrow> f i = 1" |
|
1281 |
shows "(\<lambda>i. f (i+n)) has_prod a \<longleftrightarrow> (\<lambda>i. f i) has_prod a" |
|
1282 |
by (simp add: assms has_prod_iff_shift) |
|
1283 |
||
1284 |
lemma convergent_prod_iff_shift: |
|
1285 |
shows "convergent_prod (\<lambda>i. f (i + n)) \<longleftrightarrow> convergent_prod f" |
|
1286 |
apply safe |
|
1287 |
using convergent_prod_offset apply blast |
|
1288 |
using convergent_prod_ignore_initial_segment convergent_prod_def by blast |
|
1289 |
||
1290 |
lemma has_prod_split_initial_segment: |
|
1291 |
assumes "f has_prod a" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1292 |
shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i))" |
|
1293 |
using assms has_prod_iff_shift' by blast |
|
1294 |
||
1295 |
lemma prodinf_divide_initial_segment: |
|
1296 |
assumes "convergent_prod f" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1297 |
shows "(\<Prod>i. f (i + n)) = (\<Prod>i. f i) / (\<Prod>i<n. f i)" |
|
1298 |
by (rule has_prod_unique[symmetric]) (auto simp: assms has_prod_iff_shift) |
|
1299 |
||
1300 |
lemma prodinf_split_initial_segment: |
|
1301 |
assumes "convergent_prod f" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1302 |
shows "prodinf f = (\<Prod>i. f (i + n)) * (\<Prod>i<n. f i)" |
|
1303 |
by (auto simp add: assms prodinf_divide_initial_segment) |
|
1304 |
||
1305 |
lemma prodinf_split_head: |
|
1306 |
assumes "convergent_prod f" "f 0 \<noteq> 0" |
|
1307 |
shows "(\<Prod>n. f (Suc n)) = prodinf f / f 0" |
|
1308 |
using prodinf_split_initial_segment[of 1] assms by simp |
|
1309 |
||
1310 |
end |
|
1311 |
||
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1312 |
context |
68361 | 1313 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_field" |
1314 |
begin |
|
1315 |
||
1316 |
lemma convergent_prod_inverse_iff: "convergent_prod (\<lambda>n. inverse (f n)) \<longleftrightarrow> convergent_prod f" |
|
1317 |
by (auto dest: convergent_prod_inverse) |
|
1318 |
||
1319 |
lemma convergent_prod_const_iff: |
|
1320 |
fixes c :: "'a :: {real_normed_field}" |
|
1321 |
shows "convergent_prod (\<lambda>_. c) \<longleftrightarrow> c = 1" |
|
1322 |
proof |
|
1323 |
assume "convergent_prod (\<lambda>_. c)" |
|
1324 |
then show "c = 1" |
|
1325 |
using convergent_prod_imp_LIMSEQ LIMSEQ_unique by blast |
|
1326 |
next |
|
1327 |
assume "c = 1" |
|
1328 |
then show "convergent_prod (\<lambda>_. c)" |
|
1329 |
by auto |
|
1330 |
qed |
|
1331 |
||
1332 |
lemma has_prod_power: "f has_prod a \<Longrightarrow> (\<lambda>i. f i ^ n) has_prod (a ^ n)" |
|
1333 |
by (induction n) (auto simp: has_prod_mult) |
|
1334 |
||
1335 |
lemma convergent_prod_power: "convergent_prod f \<Longrightarrow> convergent_prod (\<lambda>i. f i ^ n)" |
|
1336 |
by (induction n) (auto simp: convergent_prod_mult) |
|
1337 |
||
1338 |
lemma prodinf_power: "convergent_prod f \<Longrightarrow> prodinf (\<lambda>i. f i ^ n) = prodinf f ^ n" |
|
1339 |
by (metis has_prod_unique convergent_prod_imp_has_prod has_prod_power) |
|
1340 |
||
1341 |
end |
|
1342 |
||
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1343 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1344 |
subsection\<open>Exponentials and logarithms\<close> |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1345 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1346 |
context |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1347 |
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
|
1348 |
begin |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1349 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1350 |
lemma sums_imp_has_prod_exp: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1351 |
assumes "f sums s" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1352 |
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
|
1353 |
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
|
1354 |
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
|
1355 |
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
|
1356 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1357 |
lemma convergent_prod_exp: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1358 |
assumes "summable f" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1359 |
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
|
1360 |
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
|
1361 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1362 |
lemma prodinf_exp: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1363 |
assumes "summable f" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1364 |
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
|
1365 |
proof - |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1366 |
have "f sums suminf f" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1367 |
using assms by blast |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1368 |
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
|
1369 |
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
|
1370 |
then show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1371 |
by (rule has_prod_unique [symmetric]) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1372 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1373 |
|
68361 | 1374 |
end |
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1375 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1376 |
lemma has_prod_imp_sums_ln_real: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1377 |
fixes f :: "nat \<Rightarrow> real" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1378 |
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
|
1379 |
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
|
1380 |
proof - |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1381 |
have "p > 0" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1382 |
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
|
1383 |
then show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1384 |
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
|
1385 |
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
|
1386 |
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
|
1387 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1388 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1389 |
lemma summable_ln_real: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1390 |
fixes f :: "nat \<Rightarrow> real" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1391 |
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
|
1392 |
shows "summable (\<lambda>i. ln (f i))" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1393 |
proof - |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1394 |
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
|
1395 |
using f convergent_prod_def by blast |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1396 |
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
|
1397 |
using raw_has_prod_cases by blast |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1398 |
then show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1399 |
proof cases |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1400 |
case 1 |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1401 |
with 0 show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1402 |
by (metis less_irrefl) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1403 |
next |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1404 |
case 2 |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1405 |
then show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1406 |
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
|
1407 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1408 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1409 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1410 |
lemma suminf_ln_real: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1411 |
fixes f :: "nat \<Rightarrow> real" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1412 |
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
|
1413 |
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
|
1414 |
proof - |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1415 |
have "f has_prod prodinf f" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1416 |
by (simp add: f has_prod_iff) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1417 |
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
|
1418 |
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
|
1419 |
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
|
1420 |
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
|
1421 |
then show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1422 |
by (rule sums_unique [symmetric]) |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1423 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1424 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1425 |
lemma prodinf_exp_real: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1426 |
fixes f :: "nat \<Rightarrow> real" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1427 |
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
|
1428 |
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
|
1429 |
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
|
1430 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1431 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1432 |
subsection\<open>Embeddings from the reals into some complete real normed field\<close> |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1433 |
|
68426 | 1434 |
lemma tendsto_eq_of_real_lim: |
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1435 |
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
|
1436 |
shows "q = of_real (lim f)" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1437 |
proof - |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1438 |
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
|
1439 |
using assms convergent_def by blast |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1440 |
then have "convergent f" |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1441 |
unfolding convergent_def |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1442 |
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
|
1443 |
then show ?thesis |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1444 |
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
|
1445 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1446 |
|
68426 | 1447 |
lemma tendsto_eq_of_real: |
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1448 |
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
|
1449 |
obtains r where "q = of_real r" |
68426 | 1450 |
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
|
1451 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1452 |
lemma has_prod_of_real_iff: |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1453 |
"(\<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
|
1454 |
(is "?lhs = ?rhs") |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1455 |
proof |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1456 |
assume ?lhs |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1457 |
then show ?rhs |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1458 |
apply (auto simp: prod_defs LIMSEQ_prod_0 tendsto_of_real_iff simp flip: of_real_prod) |
68426 | 1459 |
using tendsto_eq_of_real |
68424
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1460 |
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
|
1461 |
next |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1462 |
assume ?rhs |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1463 |
with tendsto_of_real_iff show ?lhs |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1464 |
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
|
1465 |
qed |
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1466 |
|
02e5a44ffe7d
the last of the infinite product proofs
paulson <lp15@cam.ac.uk>
parents:
68361
diff
changeset
|
1467 |
end |