author | wenzelm |
Mon, 02 May 2011 16:33:21 +0200 | |
changeset 42616 | 92715b528e78 |
parent 41972 | 8885ba629692 |
child 44194 | 0639898074ae |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
1 |
(* Title: HOL/SEQ.thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
2 |
Author: Jacques D. Fleuriot, University of Cambridge |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
3 |
Author: Lawrence C Paulson |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
4 |
Author: Jeremy Avigad |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
5 |
Author: Brian Huffman |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
6 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
7 |
Convergence of sequences and series. |
15082 | 8 |
*) |
10751 | 9 |
|
22631
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
22629
diff
changeset
|
10 |
header {* Sequences and Convergence *} |
17439 | 11 |
|
15131 | 12 |
theory SEQ |
36822 | 13 |
imports Limits RComplete |
15131 | 14 |
begin |
10751 | 15 |
|
41972 | 16 |
subsection {* Monotone sequences and subsequences *} |
10751 | 17 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
18 |
definition |
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
19 |
monoseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
20 |
--{*Definition of monotonicity. |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
21 |
The use of disjunction here complicates proofs considerably. |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
22 |
One alternative is to add a Boolean argument to indicate the direction. |
30730 | 23 |
Another is to develop the notions of increasing and decreasing first.*} |
37767 | 24 |
"monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))" |
10751 | 25 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
26 |
definition |
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
27 |
incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where |
30730 | 28 |
--{*Increasing sequence*} |
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
29 |
"incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)" |
30730 | 30 |
|
31 |
definition |
|
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
32 |
decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
33 |
--{*Decreasing sequence*} |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
34 |
"decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)" |
30730 | 35 |
|
36 |
definition |
|
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
37 |
subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where |
15082 | 38 |
--{*Definition of subsequence*} |
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
39 |
"subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)" |
10751 | 40 |
|
41972 | 41 |
lemma incseq_mono: "mono f \<longleftrightarrow> incseq f" |
42 |
unfolding mono_def incseq_def by auto |
|
43 |
||
44 |
lemma incseq_SucI: |
|
45 |
"(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X" |
|
46 |
using lift_Suc_mono_le[of X] |
|
47 |
by (auto simp: incseq_def) |
|
48 |
||
49 |
lemma incseqD: "\<And>i j. incseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f i \<le> f j" |
|
50 |
by (auto simp: incseq_def) |
|
51 |
||
52 |
lemma incseq_SucD: "incseq A \<Longrightarrow> A i \<le> A (Suc i)" |
|
53 |
using incseqD[of A i "Suc i"] by auto |
|
54 |
||
55 |
lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))" |
|
56 |
by (auto intro: incseq_SucI dest: incseq_SucD) |
|
57 |
||
58 |
lemma incseq_const[simp, intro]: "incseq (\<lambda>x. k)" |
|
59 |
unfolding incseq_def by auto |
|
60 |
||
61 |
lemma decseq_SucI: |
|
62 |
"(\<And>n. X (Suc n) \<le> X n) \<Longrightarrow> decseq X" |
|
63 |
using order.lift_Suc_mono_le[OF dual_order, of X] |
|
64 |
by (auto simp: decseq_def) |
|
65 |
||
66 |
lemma decseqD: "\<And>i j. decseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f j \<le> f i" |
|
67 |
by (auto simp: decseq_def) |
|
68 |
||
69 |
lemma decseq_SucD: "decseq A \<Longrightarrow> A (Suc i) \<le> A i" |
|
70 |
using decseqD[of A i "Suc i"] by auto |
|
71 |
||
72 |
lemma decseq_Suc_iff: "decseq f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)" |
|
73 |
by (auto intro: decseq_SucI dest: decseq_SucD) |
|
74 |
||
75 |
lemma decseq_const[simp, intro]: "decseq (\<lambda>x. k)" |
|
76 |
unfolding decseq_def by auto |
|
77 |
||
78 |
lemma monoseq_iff: "monoseq X \<longleftrightarrow> incseq X \<or> decseq X" |
|
79 |
unfolding monoseq_def incseq_def decseq_def .. |
|
80 |
||
81 |
lemma monoseq_Suc: |
|
82 |
"monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)" |
|
83 |
unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff .. |
|
84 |
||
85 |
lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X" |
|
86 |
by (simp add: monoseq_def) |
|
87 |
||
88 |
lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X" |
|
89 |
by (simp add: monoseq_def) |
|
90 |
||
91 |
lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X" |
|
92 |
by (simp add: monoseq_Suc) |
|
93 |
||
94 |
lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X" |
|
95 |
by (simp add: monoseq_Suc) |
|
96 |
||
97 |
lemma monoseq_minus: |
|
98 |
fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add" |
|
99 |
assumes "monoseq a" |
|
100 |
shows "monoseq (\<lambda> n. - a n)" |
|
101 |
proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n") |
|
102 |
case True |
|
103 |
hence "\<forall> m. \<forall> n \<ge> m. - a n \<le> - a m" by auto |
|
104 |
thus ?thesis by (rule monoI2) |
|
105 |
next |
|
106 |
case False |
|
107 |
hence "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" using `monoseq a`[unfolded monoseq_def] by auto |
|
108 |
thus ?thesis by (rule monoI1) |
|
109 |
qed |
|
110 |
||
111 |
text{*Subsequence (alternative definition, (e.g. Hoskins)*} |
|
112 |
||
113 |
lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))" |
|
114 |
apply (simp add: subseq_def) |
|
115 |
apply (auto dest!: less_imp_Suc_add) |
|
116 |
apply (induct_tac k) |
|
117 |
apply (auto intro: less_trans) |
|
118 |
done |
|
119 |
||
120 |
text{* for any sequence, there is a monotonic subsequence *} |
|
121 |
lemma seq_monosub: |
|
122 |
fixes s :: "nat => 'a::linorder" |
|
123 |
shows "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))" |
|
124 |
proof cases |
|
125 |
let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)" |
|
126 |
assume *: "\<forall>n. \<exists>p. ?P p n" |
|
127 |
def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)" |
|
128 |
have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp |
|
129 |
have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc .. |
|
130 |
have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto |
|
131 |
have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto |
|
132 |
then have "subseq f" unfolding subseq_Suc_iff by auto |
|
133 |
moreover have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc |
|
134 |
proof (intro disjI2 allI) |
|
135 |
fix n show "s (f (Suc n)) \<le> s (f n)" |
|
136 |
proof (cases n) |
|
137 |
case 0 with P_Suc[of 0] P_0 show ?thesis by auto |
|
138 |
next |
|
139 |
case (Suc m) |
|
140 |
from P_Suc[of n] Suc have "f (Suc m) \<le> f (Suc (Suc m))" by simp |
|
141 |
with P_Suc Suc show ?thesis by simp |
|
142 |
qed |
|
143 |
qed |
|
144 |
ultimately show ?thesis by auto |
|
145 |
next |
|
146 |
let "?P p m" = "m < p \<and> s m < s p" |
|
147 |
assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))" |
|
148 |
then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less) |
|
149 |
def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)" |
|
150 |
have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp |
|
151 |
have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc .. |
|
152 |
have P_0: "?P (f 0) (Suc N)" |
|
153 |
unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto |
|
154 |
{ fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)" |
|
155 |
unfolding f_Suc some_eq_ex[of "\<lambda>p. ?P p (f i)"] using N[of "f i"] . } |
|
156 |
note P' = this |
|
157 |
{ fix i have "N < f i \<and> ?P (f (Suc i)) (f i)" |
|
158 |
by (induct i) (insert P_0 P', auto) } |
|
159 |
then have "subseq f" "monoseq (\<lambda>x. s (f x))" |
|
160 |
unfolding subseq_Suc_iff monoseq_Suc by (auto simp: not_le intro: less_imp_le) |
|
161 |
then show ?thesis by auto |
|
162 |
qed |
|
163 |
||
164 |
lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n" |
|
165 |
proof(induct n) |
|
166 |
case 0 thus ?case by simp |
|
167 |
next |
|
168 |
case (Suc n) |
|
169 |
from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps |
|
170 |
have "n < f (Suc n)" by arith |
|
171 |
thus ?case by arith |
|
172 |
qed |
|
173 |
||
174 |
lemma incseq_imp_monoseq: "incseq X \<Longrightarrow> monoseq X" |
|
175 |
by (simp add: incseq_def monoseq_def) |
|
176 |
||
177 |
lemma decseq_imp_monoseq: "decseq X \<Longrightarrow> monoseq X" |
|
178 |
by (simp add: decseq_def monoseq_def) |
|
179 |
||
180 |
lemma decseq_eq_incseq: |
|
181 |
fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)" |
|
182 |
by (simp add: decseq_def incseq_def) |
|
183 |
||
184 |
subsection {* Defintions of limits *} |
|
185 |
||
186 |
abbreviation |
|
187 |
LIMSEQ :: "[nat \<Rightarrow> 'a::topological_space, 'a] \<Rightarrow> bool" |
|
188 |
("((_)/ ----> (_))" [60, 60] 60) where |
|
189 |
"X ----> L \<equiv> (X ---> L) sequentially" |
|
190 |
||
191 |
definition |
|
192 |
lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where |
|
193 |
--{*Standard definition of limit using choice operator*} |
|
194 |
"lim X = (THE L. X ----> L)" |
|
195 |
||
196 |
definition |
|
197 |
convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where |
|
198 |
--{*Standard definition of convergence*} |
|
199 |
"convergent X = (\<exists>L. X ----> L)" |
|
200 |
||
201 |
definition |
|
202 |
Bseq :: "(nat => 'a::real_normed_vector) => bool" where |
|
203 |
--{*Standard definition for bounded sequence*} |
|
204 |
"Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)" |
|
205 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset
|
206 |
definition |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
207 |
Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where |
15082 | 208 |
--{*Standard definition of the Cauchy condition*} |
37767 | 209 |
"Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)" |
10751 | 210 |
|
15082 | 211 |
|
22608 | 212 |
subsection {* Bounded Sequences *} |
213 |
||
26312 | 214 |
lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X" |
22608 | 215 |
unfolding Bseq_def |
216 |
proof (intro exI conjI allI) |
|
217 |
show "0 < max K 1" by simp |
|
218 |
next |
|
219 |
fix n::nat |
|
220 |
have "norm (X n) \<le> K" by (rule K) |
|
221 |
thus "norm (X n) \<le> max K 1" by simp |
|
222 |
qed |
|
223 |
||
224 |
lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
|
225 |
unfolding Bseq_def by auto |
|
226 |
||
26312 | 227 |
lemma BseqI2': assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X" |
228 |
proof (rule BseqI') |
|
22608 | 229 |
let ?A = "norm ` X ` {..N}" |
230 |
have 1: "finite ?A" by simp |
|
231 |
fix n::nat |
|
232 |
show "norm (X n) \<le> max K (Max ?A)" |
|
233 |
proof (cases rule: linorder_le_cases) |
|
234 |
assume "n \<ge> N" |
|
235 |
hence "norm (X n) \<le> K" using K by simp |
|
236 |
thus "norm (X n) \<le> max K (Max ?A)" by simp |
|
237 |
next |
|
238 |
assume "n \<le> N" |
|
239 |
hence "norm (X n) \<in> ?A" by simp |
|
26757
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26312
diff
changeset
|
240 |
with 1 have "norm (X n) \<le> Max ?A" by (rule Max_ge) |
22608 | 241 |
thus "norm (X n) \<le> max K (Max ?A)" by simp |
242 |
qed |
|
243 |
qed |
|
244 |
||
245 |
lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))" |
|
246 |
unfolding Bseq_def by auto |
|
247 |
||
248 |
lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X" |
|
249 |
apply (erule BseqE) |
|
26312 | 250 |
apply (rule_tac N="k" and K="K" in BseqI2') |
22608 | 251 |
apply clarify |
252 |
apply (drule_tac x="n - k" in spec, simp) |
|
253 |
done |
|
254 |
||
31355 | 255 |
lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially" |
256 |
unfolding Bfun_def eventually_sequentially |
|
257 |
apply (rule iffI) |
|
32064 | 258 |
apply (simp add: Bseq_def) |
259 |
apply (auto intro: BseqI2') |
|
31355 | 260 |
done |
261 |
||
22608 | 262 |
|
20696 | 263 |
subsection {* Limits of Sequences *} |
264 |
||
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
265 |
lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
266 |
by simp |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
267 |
|
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
268 |
lemma LIMSEQ_def: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)" |
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
269 |
unfolding tendsto_iff eventually_sequentially .. |
31392 | 270 |
|
15082 | 271 |
lemma LIMSEQ_iff: |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
272 |
fixes L :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
273 |
shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
274 |
unfolding LIMSEQ_def dist_norm .. |
22608 | 275 |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33042
diff
changeset
|
276 |
lemma LIMSEQ_iff_nz: "X ----> L = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
277 |
unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33042
diff
changeset
|
278 |
|
36657 | 279 |
lemma LIMSEQ_Zfun_iff: "((\<lambda>n. X n) ----> L) = Zfun (\<lambda>n. X n - L) sequentially" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
280 |
by (rule tendsto_Zfun_iff) |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
281 |
|
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
282 |
lemma metric_LIMSEQ_I: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
283 |
"(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> L" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
284 |
by (simp add: LIMSEQ_def) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
285 |
|
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
286 |
lemma metric_LIMSEQ_D: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
287 |
"\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
288 |
by (simp add: LIMSEQ_def) |
15082 | 289 |
|
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
290 |
lemma LIMSEQ_I: |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
291 |
fixes L :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
292 |
shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
293 |
by (simp add: LIMSEQ_iff) |
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
294 |
|
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
295 |
lemma LIMSEQ_D: |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
296 |
fixes L :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
297 |
shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
298 |
by (simp add: LIMSEQ_iff) |
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
299 |
|
22608 | 300 |
lemma LIMSEQ_const: "(\<lambda>n. k) ----> k" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
301 |
by (rule tendsto_const) |
20696 | 302 |
|
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
303 |
lemma LIMSEQ_const_iff: |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
304 |
fixes k l :: "'a::metric_space" |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
305 |
shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l" |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
306 |
by (rule tendsto_const_iff, rule sequentially_bot) |
22608 | 307 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
308 |
lemma LIMSEQ_norm: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
309 |
fixes a :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
310 |
shows "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
311 |
by (rule tendsto_norm) |
20696 | 312 |
|
22615 | 313 |
lemma LIMSEQ_ignore_initial_segment: |
314 |
"f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a" |
|
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
315 |
apply (rule topological_tendstoI) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
316 |
apply (drule (2) topological_tendstoD) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
317 |
apply (simp only: eventually_sequentially) |
22615 | 318 |
apply (erule exE, rename_tac N) |
319 |
apply (rule_tac x=N in exI) |
|
320 |
apply simp |
|
321 |
done |
|
20696 | 322 |
|
22615 | 323 |
lemma LIMSEQ_offset: |
324 |
"(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a" |
|
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
325 |
apply (rule topological_tendstoI) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
326 |
apply (drule (2) topological_tendstoD) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
327 |
apply (simp only: eventually_sequentially) |
22615 | 328 |
apply (erule exE, rename_tac N) |
329 |
apply (rule_tac x="N + k" in exI) |
|
330 |
apply clarify |
|
331 |
apply (drule_tac x="n - k" in spec) |
|
332 |
apply (simp add: le_diff_conv2) |
|
20696 | 333 |
done |
334 |
||
22615 | 335 |
lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l" |
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset
|
336 |
by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp) |
22615 | 337 |
|
338 |
lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l" |
|
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset
|
339 |
by (rule_tac k="Suc 0" in LIMSEQ_offset, simp) |
22615 | 340 |
|
341 |
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l" |
|
342 |
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) |
|
343 |
||
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
344 |
lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x" |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
345 |
unfolding tendsto_def eventually_sequentially |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
346 |
by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
347 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
348 |
lemma LIMSEQ_add: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
349 |
fixes a b :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
350 |
shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) ----> a + b" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
351 |
by (rule tendsto_add) |
22608 | 352 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
353 |
lemma LIMSEQ_minus: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
354 |
fixes a :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
355 |
shows "X ----> a \<Longrightarrow> (\<lambda>n. - X n) ----> - a" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
356 |
by (rule tendsto_minus) |
22608 | 357 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
358 |
lemma LIMSEQ_minus_cancel: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
359 |
fixes a :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
360 |
shows "(\<lambda>n. - X n) ----> - a \<Longrightarrow> X ----> a" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
361 |
by (rule tendsto_minus_cancel) |
22608 | 362 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
363 |
lemma LIMSEQ_diff: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
364 |
fixes a b :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
365 |
shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
366 |
by (rule tendsto_diff) |
22608 | 367 |
|
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
368 |
lemma LIMSEQ_unique: |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
369 |
fixes a b :: "'a::metric_space" |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
370 |
shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b" |
40811 | 371 |
by (drule (1) tendsto_dist, simp add: LIMSEQ_const_iff) |
22608 | 372 |
|
373 |
lemma (in bounded_linear) LIMSEQ: |
|
374 |
"X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a" |
|
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
375 |
by (rule tendsto) |
22608 | 376 |
|
377 |
lemma (in bounded_bilinear) LIMSEQ: |
|
378 |
"\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n ** Y n) ----> a ** b" |
|
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
379 |
by (rule tendsto) |
22608 | 380 |
|
381 |
lemma LIMSEQ_mult: |
|
382 |
fixes a b :: "'a::real_normed_algebra" |
|
383 |
shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b" |
|
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
384 |
by (rule mult.tendsto) |
22608 | 385 |
|
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
386 |
lemma increasing_LIMSEQ: |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
387 |
fixes f :: "nat \<Rightarrow> real" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
388 |
assumes inc: "!!n. f n \<le> f (Suc n)" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
389 |
and bdd: "!!n. f n \<le> l" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
390 |
and en: "!!e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
391 |
shows "f ----> l" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
392 |
proof (auto simp add: LIMSEQ_def) |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
393 |
fix e :: real |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
394 |
assume e: "0 < e" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
395 |
then obtain N where "l \<le> f N + e/2" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
396 |
by (metis half_gt_zero e en that) |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
397 |
hence N: "l < f N + e" using e |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
398 |
by simp |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
399 |
{ fix k |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
400 |
have [simp]: "!!n. \<bar>f n - l\<bar> = l - f n" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
401 |
by (simp add: bdd) |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
402 |
have "\<bar>f (N+k) - l\<bar> < e" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
403 |
proof (induct k) |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
404 |
case 0 show ?case using N |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
405 |
by simp |
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
406 |
next |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
407 |
case (Suc k) thus ?case using N inc [of "N+k"] |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
408 |
by simp |
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
409 |
qed |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
410 |
} note 1 = this |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
411 |
{ fix n |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
412 |
have "N \<le> n \<Longrightarrow> \<bar>f n - l\<bar> < e" using 1 [of "n-N"] |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
413 |
by simp |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
414 |
} note [intro] = this |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
415 |
show " \<exists>no. \<forall>n\<ge>no. dist (f n) l < e" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
416 |
by (auto simp add: dist_real_def) |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
417 |
qed |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset
|
418 |
|
22608 | 419 |
lemma Bseq_inverse_lemma: |
420 |
fixes x :: "'a::real_normed_div_algebra" |
|
421 |
shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r" |
|
422 |
apply (subst nonzero_norm_inverse, clarsimp) |
|
423 |
apply (erule (1) le_imp_inverse_le) |
|
424 |
done |
|
425 |
||
426 |
lemma Bseq_inverse: |
|
427 |
fixes a :: "'a::real_normed_div_algebra" |
|
31355 | 428 |
shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
429 |
unfolding Bseq_conv_Bfun by (rule Bfun_inverse) |
22608 | 430 |
|
431 |
lemma LIMSEQ_inverse: |
|
432 |
fixes a :: "'a::real_normed_div_algebra" |
|
31355 | 433 |
shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a" |
434 |
by (rule tendsto_inverse) |
|
22608 | 435 |
|
436 |
lemma LIMSEQ_divide: |
|
437 |
fixes a b :: "'a::real_normed_field" |
|
438 |
shows "\<lbrakk>X ----> a; Y ----> b; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. X n / Y n) ----> a / b" |
|
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
439 |
by (rule tendsto_divide) |
22608 | 440 |
|
441 |
lemma LIMSEQ_pow: |
|
31017 | 442 |
fixes a :: "'a::{power, real_normed_algebra}" |
22608 | 443 |
shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m" |
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30242
diff
changeset
|
444 |
by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult) |
22608 | 445 |
|
446 |
lemma LIMSEQ_setsum: |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
447 |
fixes L :: "'a \<Rightarrow> 'b::real_normed_vector" |
22608 | 448 |
assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n" |
449 |
shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)" |
|
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
450 |
using assms by (rule tendsto_setsum) |
22608 | 451 |
|
452 |
lemma LIMSEQ_setprod: |
|
453 |
fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}" |
|
454 |
assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n" |
|
455 |
shows "(\<lambda>m. \<Prod>n\<in>S. X n m) ----> (\<Prod>n\<in>S. L n)" |
|
456 |
proof (cases "finite S") |
|
457 |
case True |
|
458 |
thus ?thesis using n |
|
459 |
proof (induct) |
|
460 |
case empty |
|
461 |
show ?case |
|
462 |
by (simp add: LIMSEQ_const) |
|
463 |
next |
|
464 |
case insert |
|
465 |
thus ?case |
|
466 |
by (simp add: LIMSEQ_mult) |
|
467 |
qed |
|
468 |
next |
|
469 |
case False |
|
470 |
thus ?thesis |
|
471 |
by (simp add: setprod_def LIMSEQ_const) |
|
472 |
qed |
|
473 |
||
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
474 |
lemma LIMSEQ_add_const: (* FIXME: delete *) |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
475 |
fixes a :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
476 |
shows "f ----> a ==> (%n.(f n + b)) ----> a + b" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
477 |
by (intro tendsto_intros) |
22614 | 478 |
|
479 |
(* FIXME: delete *) |
|
480 |
lemma LIMSEQ_add_minus: |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
481 |
fixes a b :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
482 |
shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
483 |
by (intro tendsto_intros) |
22614 | 484 |
|
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
485 |
lemma LIMSEQ_diff_const: (* FIXME: delete *) |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
486 |
fixes a b :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
487 |
shows "f ----> a ==> (%n.(f n - b)) ----> a - b" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
488 |
by (intro tendsto_intros) |
22614 | 489 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
490 |
lemma LIMSEQ_diff_approach_zero: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
491 |
fixes L :: "'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
492 |
shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
493 |
by (drule (1) LIMSEQ_add, simp) |
22614 | 494 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
495 |
lemma LIMSEQ_diff_approach_zero2: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
496 |
fixes L :: "'a::real_normed_vector" |
35292
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
497 |
shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L" |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
498 |
by (drule (1) LIMSEQ_diff, simp) |
22614 | 499 |
|
500 |
text{*A sequence tends to zero iff its abs does*} |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
501 |
lemma LIMSEQ_norm_zero: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
502 |
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
503 |
shows "((\<lambda>n. norm (X n)) ----> 0) \<longleftrightarrow> (X ----> 0)" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
504 |
by (simp add: LIMSEQ_iff) |
22614 | 505 |
|
506 |
lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> (0::real))" |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
507 |
by (simp add: LIMSEQ_iff) |
22614 | 508 |
|
509 |
lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>" |
|
510 |
by (drule LIMSEQ_norm, simp) |
|
511 |
||
512 |
text{*An unbounded sequence's inverse tends to 0*} |
|
513 |
||
514 |
lemma LIMSEQ_inverse_zero: |
|
22974 | 515 |
"\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0" |
516 |
apply (rule LIMSEQ_I) |
|
517 |
apply (drule_tac x="inverse r" in spec, safe) |
|
518 |
apply (rule_tac x="N" in exI, safe) |
|
519 |
apply (drule_tac x="n" in spec, safe) |
|
22614 | 520 |
apply (frule positive_imp_inverse_positive) |
22974 | 521 |
apply (frule (1) less_imp_inverse_less) |
522 |
apply (subgoal_tac "0 < X n", simp) |
|
523 |
apply (erule (1) order_less_trans) |
|
22614 | 524 |
done |
525 |
||
526 |
text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*} |
|
527 |
||
528 |
lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0" |
|
529 |
apply (rule LIMSEQ_inverse_zero, safe) |
|
22974 | 530 |
apply (cut_tac x = r in reals_Archimedean2) |
22614 | 531 |
apply (safe, rule_tac x = n in exI) |
532 |
apply (auto simp add: real_of_nat_Suc) |
|
533 |
done |
|
534 |
||
535 |
text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to |
|
536 |
infinity is now easily proved*} |
|
537 |
||
538 |
lemma LIMSEQ_inverse_real_of_nat_add: |
|
539 |
"(%n. r + inverse(real(Suc n))) ----> r" |
|
540 |
by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) |
|
541 |
||
542 |
lemma LIMSEQ_inverse_real_of_nat_add_minus: |
|
543 |
"(%n. r + -inverse(real(Suc n))) ----> r" |
|
544 |
by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) |
|
545 |
||
546 |
lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: |
|
547 |
"(%n. r*( 1 + -inverse(real(Suc n)))) ----> r" |
|
548 |
by (cut_tac b=1 in |
|
549 |
LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto) |
|
550 |
||
22615 | 551 |
lemma LIMSEQ_le_const: |
552 |
"\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x" |
|
553 |
apply (rule ccontr, simp only: linorder_not_le) |
|
554 |
apply (drule_tac r="a - x" in LIMSEQ_D, simp) |
|
555 |
apply clarsimp |
|
556 |
apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI1) |
|
557 |
apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI2) |
|
558 |
apply simp |
|
559 |
done |
|
560 |
||
561 |
lemma LIMSEQ_le_const2: |
|
562 |
"\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a" |
|
563 |
apply (subgoal_tac "- a \<le> - x", simp) |
|
564 |
apply (rule LIMSEQ_le_const) |
|
565 |
apply (erule LIMSEQ_minus) |
|
566 |
apply simp |
|
567 |
done |
|
568 |
||
569 |
lemma LIMSEQ_le: |
|
570 |
"\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)" |
|
571 |
apply (subgoal_tac "0 \<le> y - x", simp) |
|
572 |
apply (rule LIMSEQ_le_const) |
|
573 |
apply (erule (1) LIMSEQ_diff) |
|
574 |
apply (simp add: le_diff_eq) |
|
575 |
done |
|
576 |
||
15082 | 577 |
|
20696 | 578 |
subsection {* Convergence *} |
15082 | 579 |
|
580 |
lemma limI: "X ----> L ==> lim X = L" |
|
581 |
apply (simp add: lim_def) |
|
582 |
apply (blast intro: LIMSEQ_unique) |
|
583 |
done |
|
584 |
||
585 |
lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)" |
|
586 |
by (simp add: convergent_def) |
|
587 |
||
588 |
lemma convergentI: "(X ----> L) ==> convergent X" |
|
589 |
by (auto simp add: convergent_def) |
|
590 |
||
591 |
lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)" |
|
20682 | 592 |
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def) |
15082 | 593 |
|
36625 | 594 |
lemma convergent_const: "convergent (\<lambda>n. c)" |
595 |
by (rule convergentI, rule LIMSEQ_const) |
|
596 |
||
597 |
lemma convergent_add: |
|
598 |
fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector" |
|
599 |
assumes "convergent (\<lambda>n. X n)" |
|
600 |
assumes "convergent (\<lambda>n. Y n)" |
|
601 |
shows "convergent (\<lambda>n. X n + Y n)" |
|
602 |
using assms unfolding convergent_def by (fast intro: LIMSEQ_add) |
|
603 |
||
604 |
lemma convergent_setsum: |
|
605 |
fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector" |
|
36647 | 606 |
assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)" |
36625 | 607 |
shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)" |
36647 | 608 |
proof (cases "finite A") |
36650 | 609 |
case True from this and assms show ?thesis |
36647 | 610 |
by (induct A set: finite) (simp_all add: convergent_const convergent_add) |
611 |
qed (simp add: convergent_const) |
|
36625 | 612 |
|
613 |
lemma (in bounded_linear) convergent: |
|
614 |
assumes "convergent (\<lambda>n. X n)" |
|
615 |
shows "convergent (\<lambda>n. f (X n))" |
|
616 |
using assms unfolding convergent_def by (fast intro: LIMSEQ) |
|
617 |
||
618 |
lemma (in bounded_bilinear) convergent: |
|
619 |
assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)" |
|
620 |
shows "convergent (\<lambda>n. X n ** Y n)" |
|
621 |
using assms unfolding convergent_def by (fast intro: LIMSEQ) |
|
622 |
||
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
623 |
lemma convergent_minus_iff: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
624 |
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
625 |
shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)" |
20696 | 626 |
apply (simp add: convergent_def) |
627 |
apply (auto dest: LIMSEQ_minus) |
|
628 |
apply (drule LIMSEQ_minus, auto) |
|
629 |
done |
|
630 |
||
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
631 |
lemma lim_le: |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
632 |
fixes x :: real |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
633 |
assumes f: "convergent f" and fn_le: "!!n. f n \<le> x" |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
634 |
shows "lim f \<le> x" |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
635 |
proof (rule classical) |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
636 |
assume "\<not> lim f \<le> x" |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
637 |
hence 0: "0 < lim f - x" by arith |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
638 |
have 1: "f----> lim f" |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
639 |
by (metis convergent_LIMSEQ_iff f) |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
640 |
thus ?thesis |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
641 |
proof (simp add: LIMSEQ_iff) |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
642 |
assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < r" |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
643 |
hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
644 |
by (metis 0) |
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
645 |
from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32877
diff
changeset
|
646 |
by blast |
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
647 |
thus "lim f \<le> x" |
37887 | 648 |
by (metis 1 LIMSEQ_le_const2 fn_le) |
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
649 |
qed |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
650 |
qed |
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
651 |
|
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
652 |
lemma monoseq_le: |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
653 |
fixes a :: "nat \<Rightarrow> real" |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
654 |
assumes "monoseq a" and "a ----> x" |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
655 |
shows "((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or> |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
656 |
((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
657 |
proof - |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
658 |
{ fix x n fix a :: "nat \<Rightarrow> real" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
659 |
assume "a ----> x" and "\<forall> m. \<forall> n \<ge> m. a m \<le> a n" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
660 |
hence monotone: "\<And> m n. m \<le> n \<Longrightarrow> a m \<le> a n" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
661 |
have "a n \<le> x" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
662 |
proof (rule ccontr) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
663 |
assume "\<not> a n \<le> x" hence "x < a n" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
664 |
hence "0 < a n - x" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
665 |
from `a ----> x`[THEN LIMSEQ_D, OF this] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
666 |
obtain no where "\<And>n'. no \<le> n' \<Longrightarrow> norm (a n' - x) < a n - x" by blast |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
667 |
hence "norm (a (max no n) - x) < a n - x" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
668 |
moreover |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
669 |
{ fix n' have "n \<le> n' \<Longrightarrow> x < a n'" using monotone[where m=n and n=n'] and `x < a n` by auto } |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
670 |
hence "x < a (max no n)" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
671 |
ultimately |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
672 |
have "a (max no n) < a n" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
673 |
with monotone[where m=n and n="max no n"] |
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32064
diff
changeset
|
674 |
show False by (auto simp:max_def split:split_if_asm) |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
675 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
676 |
} note top_down = this |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
677 |
{ fix x n m fix a :: "nat \<Rightarrow> real" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
678 |
assume "a ----> x" and "monoseq a" and "a m < x" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
679 |
have "a n \<le> x \<and> (\<forall> m. \<forall> n \<ge> m. a m \<le> a n)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
680 |
proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
681 |
case True with top_down and `a ----> x` show ?thesis by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
682 |
next |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
683 |
case False with `monoseq a`[unfolded monoseq_def] have "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
684 |
hence "- a m \<le> - x" using top_down[OF LIMSEQ_minus[OF `a ----> x`]] by blast |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
685 |
hence False using `a m < x` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
686 |
thus ?thesis .. |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
687 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
688 |
} note when_decided = this |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
689 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
690 |
show ?thesis |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
691 |
proof (cases "\<exists> m. a m \<noteq> x") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
692 |
case True then obtain m where "a m \<noteq> x" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
693 |
show ?thesis |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
694 |
proof (cases "a m < x") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
695 |
case True with when_decided[OF `a ----> x` `monoseq a`, where m2=m] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
696 |
show ?thesis by blast |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
697 |
next |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
698 |
case False hence "- a m < - x" using `a m \<noteq> x` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
699 |
with when_decided[OF LIMSEQ_minus[OF `a ----> x`] monoseq_minus[OF `monoseq a`], where m2=m] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
700 |
show ?thesis by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
701 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
702 |
qed auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
703 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
704 |
|
30730 | 705 |
lemma LIMSEQ_subseq_LIMSEQ: |
706 |
"\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L" |
|
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
707 |
apply (rule topological_tendstoI) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
708 |
apply (drule (2) topological_tendstoD) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
709 |
apply (simp only: eventually_sequentially) |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
710 |
apply (clarify, rule_tac x=N in exI, clarsimp) |
30730 | 711 |
apply (blast intro: seq_suble le_trans dest!: spec) |
712 |
done |
|
713 |
||
30196
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset
|
714 |
subsection {* Bounded Monotonic Sequences *} |
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset
|
715 |
|
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset
|
716 |
|
20696 | 717 |
text{*Bounded Sequence*} |
15082 | 718 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
719 |
lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)" |
15082 | 720 |
by (simp add: Bseq_def) |
721 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
722 |
lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X" |
15082 | 723 |
by (auto simp add: Bseq_def) |
724 |
||
725 |
lemma lemma_NBseq_def: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
726 |
"(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
727 |
(\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" |
32064 | 728 |
proof auto |
729 |
fix K :: real |
|
730 |
from reals_Archimedean2 obtain n :: nat where "K < real n" .. |
|
731 |
then have "K \<le> real (Suc n)" by auto |
|
732 |
assume "\<forall>m. norm (X m) \<le> K" |
|
733 |
have "\<forall>m. norm (X m) \<le> real (Suc n)" |
|
734 |
proof |
|
735 |
fix m :: 'a |
|
736 |
from `\<forall>m. norm (X m) \<le> K` have "norm (X m) \<le> K" .. |
|
737 |
with `K \<le> real (Suc n)` show "norm (X m) \<le> real (Suc n)" by auto |
|
738 |
qed |
|
739 |
then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" .. |
|
740 |
next |
|
741 |
fix N :: nat |
|
742 |
have "real (Suc N) > 0" by (simp add: real_of_nat_Suc) |
|
743 |
moreover assume "\<forall>n. norm (X n) \<le> real (Suc N)" |
|
744 |
ultimately show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" by blast |
|
745 |
qed |
|
746 |
||
15082 | 747 |
|
748 |
text{* alternative definition for Bseq *} |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
749 |
lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" |
15082 | 750 |
apply (simp add: Bseq_def) |
751 |
apply (simp (no_asm) add: lemma_NBseq_def) |
|
752 |
done |
|
753 |
||
754 |
lemma lemma_NBseq_def2: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
755 |
"(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))" |
15082 | 756 |
apply (subst lemma_NBseq_def, auto) |
757 |
apply (rule_tac x = "Suc N" in exI) |
|
758 |
apply (rule_tac [2] x = N in exI) |
|
759 |
apply (auto simp add: real_of_nat_Suc) |
|
760 |
prefer 2 apply (blast intro: order_less_imp_le) |
|
761 |
apply (drule_tac x = n in spec, simp) |
|
762 |
done |
|
763 |
||
764 |
(* yet another definition for Bseq *) |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
765 |
lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))" |
15082 | 766 |
by (simp add: Bseq_def lemma_NBseq_def2) |
767 |
||
20696 | 768 |
subsubsection{*Upper Bounds and Lubs of Bounded Sequences*} |
15082 | 769 |
|
770 |
lemma Bseq_isUb: |
|
771 |
"!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U" |
|
22998 | 772 |
by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff) |
15082 | 773 |
|
774 |
||
775 |
text{* Use completeness of reals (supremum property) |
|
776 |
to show that any bounded sequence has a least upper bound*} |
|
777 |
||
778 |
lemma Bseq_isLub: |
|
779 |
"!!(X::nat=>real). Bseq X ==> |
|
780 |
\<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U" |
|
781 |
by (blast intro: reals_complete Bseq_isUb) |
|
782 |
||
20696 | 783 |
subsubsection{*A Bounded and Monotonic Sequence Converges*} |
15082 | 784 |
|
785 |
lemma lemma_converg1: |
|
15360 | 786 |
"!!(X::nat=>real). [| \<forall>m. \<forall> n \<ge> m. X m \<le> X n; |
15082 | 787 |
isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma) |
15360 | 788 |
|] ==> \<forall>n \<ge> ma. X n = X ma" |
15082 | 789 |
apply safe |
790 |
apply (drule_tac y = "X n" in isLubD2) |
|
791 |
apply (blast dest: order_antisym)+ |
|
792 |
done |
|
793 |
||
794 |
lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)" |
|
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset
|
795 |
unfolding tendsto_def eventually_sequentially |
15082 | 796 |
apply (rule_tac x = "X m" in exI, safe) |
797 |
apply (rule_tac x = m in exI, safe) |
|
798 |
apply (drule spec, erule impE, auto) |
|
799 |
done |
|
800 |
||
801 |
lemma lemma_converg2: |
|
802 |
"!!(X::nat=>real). |
|
803 |
[| \<forall>m. X m ~= U; isLub UNIV {x. \<exists>n. X n = x} U |] ==> \<forall>m. X m < U" |
|
804 |
apply safe |
|
805 |
apply (drule_tac y = "X m" in isLubD2) |
|
806 |
apply (auto dest!: order_le_imp_less_or_eq) |
|
807 |
done |
|
808 |
||
809 |
lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U" |
|
810 |
by (rule setleI [THEN isUbI], auto) |
|
811 |
||
812 |
text{* FIXME: @{term "U - T < U"} is redundant *} |
|
813 |
lemma lemma_converg4: "!!(X::nat=> real). |
|
814 |
[| \<forall>m. X m ~= U; |
|
815 |
isLub UNIV {x. \<exists>n. X n = x} U; |
|
816 |
0 < T; |
|
817 |
U + - T < U |
|
818 |
|] ==> \<exists>m. U + -T < X m & X m < U" |
|
819 |
apply (drule lemma_converg2, assumption) |
|
820 |
apply (rule ccontr, simp) |
|
821 |
apply (simp add: linorder_not_less) |
|
822 |
apply (drule lemma_converg3) |
|
823 |
apply (drule isLub_le_isUb, assumption) |
|
824 |
apply (auto dest: order_less_le_trans) |
|
825 |
done |
|
826 |
||
827 |
text{*A standard proof of the theorem for monotone increasing sequence*} |
|
828 |
||
829 |
lemma Bseq_mono_convergent: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
830 |
"[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)" |
15082 | 831 |
apply (simp add: convergent_def) |
832 |
apply (frule Bseq_isLub, safe) |
|
833 |
apply (case_tac "\<exists>m. X m = U", auto) |
|
834 |
apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ) |
|
835 |
(* second case *) |
|
836 |
apply (rule_tac x = U in exI) |
|
837 |
apply (subst LIMSEQ_iff, safe) |
|
838 |
apply (frule lemma_converg2, assumption) |
|
839 |
apply (drule lemma_converg4, auto) |
|
840 |
apply (rule_tac x = m in exI, safe) |
|
841 |
apply (subgoal_tac "X m \<le> X n") |
|
842 |
prefer 2 apply blast |
|
843 |
apply (drule_tac x=n and P="%m. X m < U" in spec, arith) |
|
844 |
done |
|
845 |
||
846 |
lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X" |
|
847 |
by (simp add: Bseq_def) |
|
848 |
||
849 |
text{*Main monotonicity theorem*} |
|
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
850 |
lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent (X::nat\<Rightarrow>real)" |
15082 | 851 |
apply (simp add: monoseq_def, safe) |
852 |
apply (rule_tac [2] convergent_minus_iff [THEN ssubst]) |
|
853 |
apply (drule_tac [2] Bseq_minus_iff [THEN ssubst]) |
|
854 |
apply (auto intro!: Bseq_mono_convergent) |
|
855 |
done |
|
856 |
||
30730 | 857 |
subsubsection{*Increasing and Decreasing Series*} |
858 |
||
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
859 |
lemma incseq_le: |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
860 |
fixes X :: "nat \<Rightarrow> real" |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
861 |
assumes inc: "incseq X" and lim: "X ----> L" shows "X n \<le> L" |
30730 | 862 |
using monoseq_le [OF incseq_imp_monoseq [OF inc] lim] |
863 |
proof |
|
864 |
assume "(\<forall>n. X n \<le> L) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n)" |
|
865 |
thus ?thesis by simp |
|
866 |
next |
|
867 |
assume "(\<forall>n. L \<le> X n) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X n \<le> X m)" |
|
868 |
hence const: "(!!m n. m \<le> n \<Longrightarrow> X n = X m)" using inc |
|
869 |
by (auto simp add: incseq_def intro: order_antisym) |
|
870 |
have X: "!!n. X n = X 0" |
|
871 |
by (blast intro: const [of 0]) |
|
872 |
have "X = (\<lambda>n. X 0)" |
|
873 |
by (blast intro: ext X) |
|
874 |
hence "L = X 0" using LIMSEQ_const [of "X 0"] |
|
875 |
by (auto intro: LIMSEQ_unique lim) |
|
876 |
thus ?thesis |
|
877 |
by (blast intro: eq_refl X) |
|
878 |
qed |
|
879 |
||
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
880 |
lemma decseq_le: |
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
881 |
fixes X :: "nat \<Rightarrow> real" assumes dec: "decseq X" and lim: "X ----> L" shows "L \<le> X n" |
30730 | 882 |
proof - |
883 |
have inc: "incseq (\<lambda>n. - X n)" using dec |
|
884 |
by (simp add: decseq_eq_incseq) |
|
885 |
have "- X n \<le> - L" |
|
886 |
by (blast intro: incseq_le [OF inc] LIMSEQ_minus lim) |
|
887 |
thus ?thesis |
|
888 |
by simp |
|
889 |
qed |
|
890 |
||
20696 | 891 |
subsubsection{*A Few More Equivalence Theorems for Boundedness*} |
15082 | 892 |
|
893 |
text{*alternative formulation for boundedness*} |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
894 |
lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)" |
15082 | 895 |
apply (unfold Bseq_def, safe) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
896 |
apply (rule_tac [2] x = "k + norm x" in exI) |
15360 | 897 |
apply (rule_tac x = K in exI, simp) |
15221 | 898 |
apply (rule exI [where x = 0], auto) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
899 |
apply (erule order_less_le_trans, simp) |
37887 | 900 |
apply (drule_tac x=n in spec, fold diff_minus) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
901 |
apply (drule order_trans [OF norm_triangle_ineq2]) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
902 |
apply simp |
15082 | 903 |
done |
904 |
||
905 |
text{*alternative formulation for boundedness*} |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
906 |
lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)" |
15082 | 907 |
apply safe |
908 |
apply (simp add: Bseq_def, safe) |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
909 |
apply (rule_tac x = "K + norm (X N)" in exI) |
15082 | 910 |
apply auto |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
911 |
apply (erule order_less_le_trans, simp) |
15082 | 912 |
apply (rule_tac x = N in exI, safe) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
913 |
apply (drule_tac x = n in spec) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
914 |
apply (rule order_trans [OF norm_triangle_ineq], simp) |
15082 | 915 |
apply (auto simp add: Bseq_iff2) |
916 |
done |
|
917 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
918 |
lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f" |
15082 | 919 |
apply (simp add: Bseq_def) |
15221 | 920 |
apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset
|
921 |
apply (drule_tac x = n in spec, arith) |
15082 | 922 |
done |
923 |
||
924 |
||
20696 | 925 |
subsection {* Cauchy Sequences *} |
15082 | 926 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
927 |
lemma metric_CauchyI: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
928 |
"(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
929 |
by (simp add: Cauchy_def) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
930 |
|
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
931 |
lemma metric_CauchyD: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
932 |
"\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e" |
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
933 |
by (simp add: Cauchy_def) |
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
934 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
935 |
lemma Cauchy_iff: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
936 |
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
937 |
shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
938 |
unfolding Cauchy_def dist_norm .. |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
939 |
|
35292
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
940 |
lemma Cauchy_iff2: |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
941 |
"Cauchy X = |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
942 |
(\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))" |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
943 |
apply (simp add: Cauchy_iff, auto) |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
944 |
apply (drule reals_Archimedean, safe) |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
945 |
apply (drule_tac x = n in spec, auto) |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
946 |
apply (rule_tac x = M in exI, auto) |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
947 |
apply (drule_tac x = m in spec, simp) |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
948 |
apply (drule_tac x = na in spec, auto) |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
949 |
done |
e4a431b6d9b7
Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents:
35216
diff
changeset
|
950 |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
951 |
lemma CauchyI: |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
952 |
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
953 |
shows "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
954 |
by (simp add: Cauchy_iff) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
955 |
|
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
956 |
lemma CauchyD: |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
957 |
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
958 |
shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
959 |
by (simp add: Cauchy_iff) |
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset
|
960 |
|
30730 | 961 |
lemma Cauchy_subseq_Cauchy: |
962 |
"\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)" |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
963 |
apply (auto simp add: Cauchy_def) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
964 |
apply (drule_tac x=e in spec, clarify) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
965 |
apply (rule_tac x=M in exI, clarify) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
966 |
apply (blast intro: le_trans [OF _ seq_suble] dest!: spec) |
30730 | 967 |
done |
968 |
||
20696 | 969 |
subsubsection {* Cauchy Sequences are Bounded *} |
970 |
||
15082 | 971 |
text{*A Cauchy sequence is bounded -- this is the standard |
972 |
proof mechanization rather than the nonstandard proof*} |
|
973 |
||
20563 | 974 |
lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
975 |
==> \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
976 |
apply (clarify, drule spec, drule (1) mp) |
20563 | 977 |
apply (simp only: norm_minus_commute) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
978 |
apply (drule order_le_less_trans [OF norm_triangle_ineq2]) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
979 |
apply simp |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
980 |
done |
15082 | 981 |
|
982 |
lemma Cauchy_Bseq: "Cauchy X ==> Bseq X" |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
983 |
apply (simp add: Cauchy_iff) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
984 |
apply (drule spec, drule mp, rule zero_less_one, safe) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
985 |
apply (drule_tac x="M" in spec, simp) |
15082 | 986 |
apply (drule lemmaCauchy) |
22608 | 987 |
apply (rule_tac k="M" in Bseq_offset) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
988 |
apply (simp add: Bseq_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
989 |
apply (rule_tac x="1 + norm (X M)" in exI) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
990 |
apply (rule conjI, rule order_less_le_trans [OF zero_less_one], simp) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
991 |
apply (simp add: order_less_imp_le) |
15082 | 992 |
done |
993 |
||
20696 | 994 |
subsubsection {* Cauchy Sequences are Convergent *} |
15082 | 995 |
|
33042 | 996 |
class complete_space = |
997 |
assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X" |
|
20830
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
998 |
|
33042 | 999 |
class banach = real_normed_vector + complete_space |
31403 | 1000 |
|
22629 | 1001 |
theorem LIMSEQ_imp_Cauchy: |
1002 |
assumes X: "X ----> a" shows "Cauchy X" |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
1003 |
proof (rule metric_CauchyI) |
22629 | 1004 |
fix e::real assume "0 < e" |
1005 |
hence "0 < e/2" by simp |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
1006 |
with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
1007 |
then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" .. |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
1008 |
show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e" |
22629 | 1009 |
proof (intro exI allI impI) |
1010 |
fix m assume "N \<le> m" |
|
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
1011 |
hence m: "dist (X m) a < e/2" using N by fast |
22629 | 1012 |
fix n assume "N \<le> n" |
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
1013 |
hence n: "dist (X n) a < e/2" using N by fast |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
1014 |
have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a" |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
1015 |
by (rule dist_triangle2) |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
1016 |
also from m n have "\<dots> < e" by simp |
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset
|
1017 |
finally show "dist (X m) (X n) < e" . |
22629 | 1018 |
qed |
1019 |
qed |
|
1020 |
||
20691 | 1021 |
lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X" |
22629 | 1022 |
unfolding convergent_def |
1023 |
by (erule exE, erule LIMSEQ_imp_Cauchy) |
|
20691 | 1024 |
|
31403 | 1025 |
lemma Cauchy_convergent_iff: |
1026 |
fixes X :: "nat \<Rightarrow> 'a::complete_space" |
|
1027 |
shows "Cauchy X = convergent X" |
|
1028 |
by (fast intro: Cauchy_convergent convergent_Cauchy) |
|
1029 |
||
1030 |
lemma convergent_subseq_convergent: |
|
1031 |
fixes X :: "nat \<Rightarrow> 'a::complete_space" |
|
1032 |
shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)" |
|
1033 |
by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric]) |
|
1034 |
||
22629 | 1035 |
text {* |
1036 |
Proof that Cauchy sequences converge based on the one from |
|
1037 |
http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html |
|
1038 |
*} |
|
1039 |
||
1040 |
text {* |
|
1041 |
If sequence @{term "X"} is Cauchy, then its limit is the lub of |
|
1042 |
@{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"} |
|
1043 |
*} |
|
1044 |
||
1045 |
lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u" |
|
1046 |
by (simp add: isUbI setleI) |
|
1047 |
||
27681 | 1048 |
locale real_Cauchy = |
22629 | 1049 |
fixes X :: "nat \<Rightarrow> real" |
1050 |
assumes X: "Cauchy X" |
|
1051 |
fixes S :: "real set" |
|
1052 |
defines S_def: "S \<equiv> {x::real. \<exists>N. \<forall>n\<ge>N. x < X n}" |
|
1053 |
||
27681 | 1054 |
lemma real_CauchyI: |
1055 |
assumes "Cauchy X" |
|
1056 |
shows "real_Cauchy X" |
|
28823 | 1057 |
proof qed (fact assms) |
27681 | 1058 |
|
22629 | 1059 |
lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" |
1060 |
by (unfold S_def, auto) |
|
1061 |
||
1062 |
lemma (in real_Cauchy) bound_isUb: |
|
1063 |
assumes N: "\<forall>n\<ge>N. X n < x" |
|
1064 |
shows "isUb UNIV S x" |
|
1065 |
proof (rule isUb_UNIV_I) |
|
1066 |
fix y::real assume "y \<in> S" |
|
1067 |
hence "\<exists>M. \<forall>n\<ge>M. y < X n" |
|
1068 |
by (simp add: S_def) |
|
1069 |
then obtain M where "\<forall>n\<ge>M. y < X n" .. |
|
1070 |
hence "y < X (max M N)" by simp |
|
1071 |
also have "\<dots> < x" using N by simp |
|
1072 |
finally show "y \<le> x" |
|
1073 |
by (rule order_less_imp_le) |
|
1074 |
qed |
|
1075 |
||
1076 |
lemma (in real_Cauchy) isLub_ex: "\<exists>u. isLub UNIV S u" |
|
1077 |
proof (rule reals_complete) |
|
1078 |
obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < 1" |
|
32064 | 1079 |
using CauchyD [OF X zero_less_one] by auto |
22629 | 1080 |
hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp |
1081 |
show "\<exists>x. x \<in> S" |
|
1082 |
proof |
|
1083 |
from N have "\<forall>n\<ge>N. X N - 1 < X n" |
|
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
1084 |
by (simp add: abs_diff_less_iff) |
22629 | 1085 |
thus "X N - 1 \<in> S" by (rule mem_S) |
1086 |
qed |
|
1087 |
show "\<exists>u. isUb UNIV S u" |
|
1088 |
proof |
|
1089 |
from N have "\<forall>n\<ge>N. X n < X N + 1" |
|
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
1090 |
by (simp add: abs_diff_less_iff) |
22629 | 1091 |
thus "isUb UNIV S (X N + 1)" |
1092 |
by (rule bound_isUb) |
|
1093 |
qed |
|
1094 |
qed |
|
1095 |
||
1096 |
lemma (in real_Cauchy) isLub_imp_LIMSEQ: |
|
1097 |
assumes x: "isLub UNIV S x" |
|
1098 |
shows "X ----> x" |
|
1099 |
proof (rule LIMSEQ_I) |
|
1100 |
fix r::real assume "0 < r" |
|
1101 |
hence r: "0 < r/2" by simp |
|
1102 |
obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2" |
|
32064 | 1103 |
using CauchyD [OF X r] by auto |
22629 | 1104 |
hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp |
1105 |
hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2" |
|
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
1106 |
by (simp only: real_norm_def abs_diff_less_iff) |
22629 | 1107 |
|
1108 |
from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast |
|
1109 |
hence "X N - r/2 \<in> S" by (rule mem_S) |
|
23482 | 1110 |
hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast |
22629 | 1111 |
|
1112 |
from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast |
|
1113 |
hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb) |
|
23482 | 1114 |
hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast |
22629 | 1115 |
|
1116 |
show "\<exists>N. \<forall>n\<ge>N. norm (X n - x) < r" |
|
1117 |
proof (intro exI allI impI) |
|
1118 |
fix n assume n: "N \<le> n" |
|
23482 | 1119 |
from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+ |
1120 |
thus "norm (X n - x) < r" using 1 2 |
|
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset
|
1121 |
by (simp add: abs_diff_less_iff) |
22629 | 1122 |
qed |
1123 |
qed |
|
1124 |
||
1125 |
lemma (in real_Cauchy) LIMSEQ_ex: "\<exists>x. X ----> x" |
|
1126 |
proof - |
|
1127 |
obtain x where "isLub UNIV S x" |
|
1128 |
using isLub_ex by fast |
|
1129 |
hence "X ----> x" |
|
1130 |
by (rule isLub_imp_LIMSEQ) |
|
1131 |
thus ?thesis .. |
|
1132 |
qed |
|
1133 |
||
20830
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1134 |
lemma real_Cauchy_convergent: |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1135 |
fixes X :: "nat \<Rightarrow> real" |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1136 |
shows "Cauchy X \<Longrightarrow> convergent X" |
27681 | 1137 |
unfolding convergent_def |
1138 |
by (rule real_Cauchy.LIMSEQ_ex) |
|
1139 |
(rule real_CauchyI) |
|
20830
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1140 |
|
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1141 |
instance real :: banach |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1142 |
by intro_classes (rule real_Cauchy_convergent) |
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset
|
1143 |
|
15082 | 1144 |
|
20696 | 1145 |
subsection {* Power Sequences *} |
15082 | 1146 |
|
1147 |
text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term |
|
1148 |
"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and |
|
1149 |
also fact that bounded and monotonic sequence converges.*} |
|
1150 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1151 |
lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)" |
15082 | 1152 |
apply (simp add: Bseq_def) |
1153 |
apply (rule_tac x = 1 in exI) |
|
1154 |
apply (simp add: power_abs) |
|
22974 | 1155 |
apply (auto dest: power_mono) |
15082 | 1156 |
done |
1157 |
||
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset
|
1158 |
lemma monoseq_realpow: fixes x :: real shows "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)" |
15082 | 1159 |
apply (clarify intro!: mono_SucI2) |
1160 |
apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto) |
|
1161 |
done |
|
1162 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1163 |
lemma convergent_realpow: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1164 |
"[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)" |
15082 | 1165 |
by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) |
1166 |
||
22628 | 1167 |
lemma LIMSEQ_inverse_realpow_zero_lemma: |
1168 |
fixes x :: real |
|
1169 |
assumes x: "0 \<le> x" |
|
1170 |
shows "real n * x + 1 \<le> (x + 1) ^ n" |
|
1171 |
apply (induct n) |
|
1172 |
apply simp |
|
1173 |
apply simp |
|
1174 |
apply (rule order_trans) |
|
1175 |
prefer 2 |
|
1176 |
apply (erule mult_left_mono) |
|
1177 |
apply (rule add_increasing [OF x], simp) |
|
1178 |
apply (simp add: real_of_nat_Suc) |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23127
diff
changeset
|
1179 |
apply (simp add: ring_distribs) |
22628 | 1180 |
apply (simp add: mult_nonneg_nonneg x) |
1181 |
done |
|
1182 |
||
1183 |
lemma LIMSEQ_inverse_realpow_zero: |
|
1184 |
"1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0" |
|
1185 |
proof (rule LIMSEQ_inverse_zero [rule_format]) |
|
1186 |
fix y :: real |
|
1187 |
assume x: "1 < x" |
|
1188 |
hence "0 < x - 1" by simp |
|
1189 |
hence "\<forall>y. \<exists>N::nat. y < real N * (x - 1)" |
|
1190 |
by (rule reals_Archimedean3) |
|
1191 |
hence "\<exists>N::nat. y < real N * (x - 1)" .. |
|
1192 |
then obtain N::nat where "y < real N * (x - 1)" .. |
|
1193 |
also have "\<dots> \<le> real N * (x - 1) + 1" by simp |
|
1194 |
also have "\<dots> \<le> (x - 1 + 1) ^ N" |
|
1195 |
by (rule LIMSEQ_inverse_realpow_zero_lemma, cut_tac x, simp) |
|
1196 |
also have "\<dots> = x ^ N" by simp |
|
1197 |
finally have "y < x ^ N" . |
|
1198 |
hence "\<forall>n\<ge>N. y < x ^ n" |
|
1199 |
apply clarify |
|
1200 |
apply (erule order_less_le_trans) |
|
1201 |
apply (erule power_increasing) |
|
1202 |
apply (rule order_less_imp_le [OF x]) |
|
1203 |
done |
|
1204 |
thus "\<exists>N. \<forall>n\<ge>N. y < x ^ n" .. |
|
1205 |
qed |
|
1206 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1207 |
lemma LIMSEQ_realpow_zero: |
22628 | 1208 |
"\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0" |
1209 |
proof (cases) |
|
1210 |
assume "x = 0" |
|
1211 |
hence "(\<lambda>n. x ^ Suc n) ----> 0" by (simp add: LIMSEQ_const) |
|
1212 |
thus ?thesis by (rule LIMSEQ_imp_Suc) |
|
1213 |
next |
|
1214 |
assume "0 \<le> x" and "x \<noteq> 0" |
|
1215 |
hence x0: "0 < x" by simp |
|
1216 |
assume x1: "x < 1" |
|
1217 |
from x0 x1 have "1 < inverse x" |
|
36776
c137ae7673d3
remove a couple of redundant lemmas; simplify some proofs
huffman
parents:
36663
diff
changeset
|
1218 |
by (rule one_less_inverse) |
22628 | 1219 |
hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0" |
1220 |
by (rule LIMSEQ_inverse_realpow_zero) |
|
1221 |
thus ?thesis by (simp add: power_inverse) |
|
1222 |
qed |
|
15082 | 1223 |
|
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1224 |
lemma LIMSEQ_power_zero: |
31017 | 1225 |
fixes x :: "'a::{real_normed_algebra_1}" |
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1226 |
shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0" |
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1227 |
apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero]) |
36657 | 1228 |
apply (simp only: LIMSEQ_Zfun_iff, erule Zfun_le) |
22974 | 1229 |
apply (simp add: power_abs norm_power_ineq) |
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1230 |
done |
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1231 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1232 |
lemma LIMSEQ_divide_realpow_zero: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1233 |
"1 < (x::real) ==> (%n. a / (x ^ n)) ----> 0" |
15082 | 1234 |
apply (cut_tac a = a and x1 = "inverse x" in |
1235 |
LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero]) |
|
1236 |
apply (auto simp add: divide_inverse power_inverse) |
|
1237 |
apply (simp add: inverse_eq_divide pos_divide_less_eq) |
|
1238 |
done |
|
1239 |
||
15102 | 1240 |
text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*} |
15082 | 1241 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1242 |
lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----> 0" |
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset
|
1243 |
by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) |
15082 | 1244 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset
|
1245 |
lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----> 0" |
15082 | 1246 |
apply (rule LIMSEQ_rabs_zero [THEN iffD1]) |
1247 |
apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs) |
|
1248 |
done |
|
1249 |
||
10751 | 1250 |
end |