136 by (simp add: Bseq_def) |
136 by (simp add: Bseq_def) |
137 |
137 |
138 lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X" |
138 lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X" |
139 by (auto simp add: Bseq_def) |
139 by (auto simp add: Bseq_def) |
140 |
140 |
|
141 lemma Bseq_bdd_above: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_above (range X)" |
|
142 proof (elim BseqE, intro bdd_aboveI2) |
|
143 fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "X n \<le> K" |
|
144 by (auto elim!: allE[of _ n]) |
|
145 qed |
|
146 |
|
147 lemma Bseq_bdd_below: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_below (range X)" |
|
148 proof (elim BseqE, intro bdd_belowI2) |
|
149 fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "- K \<le> X n" |
|
150 by (auto elim!: allE[of _ n]) |
|
151 qed |
|
152 |
141 lemma lemma_NBseq_def: |
153 lemma lemma_NBseq_def: |
142 "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" |
154 "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" |
143 proof safe |
155 proof safe |
144 fix K :: real |
156 fix K :: real |
145 from reals_Archimedean2 obtain n :: nat where "K < real n" .. |
157 from reals_Archimedean2 obtain n :: nat where "K < real n" .. |
207 apply (drule_tac x = n in spec, arith) |
219 apply (drule_tac x = n in spec, arith) |
208 done |
220 done |
209 |
221 |
210 |
222 |
211 subsubsection{*Upper Bounds and Lubs of Bounded Sequences*} |
223 subsubsection{*Upper Bounds and Lubs of Bounded Sequences*} |
212 |
|
213 lemma Bseq_isUb: |
|
214 "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U" |
|
215 by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff) |
|
216 |
|
217 text{* Use completeness of reals (supremum property) |
|
218 to show that any bounded sequence has a least upper bound*} |
|
219 |
|
220 lemma Bseq_isLub: |
|
221 "!!(X::nat=>real). Bseq X ==> |
|
222 \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U" |
|
223 by (blast intro: reals_complete Bseq_isUb) |
|
224 |
224 |
225 lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X" |
225 lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X" |
226 by (simp add: Bseq_def) |
226 by (simp add: Bseq_def) |
227 |
227 |
228 lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f" |
228 lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f" |
1356 done |
1356 done |
1357 |
1357 |
1358 |
1358 |
1359 text {* A monotone sequence converges to its least upper bound. *} |
1359 text {* A monotone sequence converges to its least upper bound. *} |
1360 |
1360 |
1361 lemma isLub_mono_imp_LIMSEQ: |
1361 lemma LIMSEQ_incseq_SUP: |
1362 fixes X :: "nat \<Rightarrow> real" |
1362 fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}" |
1363 assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *) |
1363 assumes u: "bdd_above (range X)" |
1364 assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n" |
1364 assumes X: "incseq X" |
1365 shows "X ----> u" |
1365 shows "X ----> (SUP i. X i)" |
1366 proof (rule LIMSEQ_I) |
1366 by (rule order_tendstoI) |
1367 have 1: "\<forall>n. X n \<le> u" |
1367 (auto simp: eventually_sequentially u less_cSUP_iff intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u]) |
1368 using isLubD2 [OF u] by auto |
1368 |
1369 have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y" |
1369 lemma LIMSEQ_decseq_INF: |
1370 using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def) |
1370 fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}" |
1371 hence 2: "\<forall>y<u. \<exists>n. y < X n" |
1371 assumes u: "bdd_below (range X)" |
1372 by (metis not_le) |
1372 assumes X: "decseq X" |
1373 fix r :: real assume "0 < r" |
1373 shows "X ----> (INF i. X i)" |
1374 hence "u - r < u" by simp |
1374 by (rule order_tendstoI) |
1375 hence "\<exists>m. u - r < X m" using 2 by simp |
1375 (auto simp: eventually_sequentially u cINF_less_iff intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u]) |
1376 then obtain m where "u - r < X m" .. |
|
1377 with X have "\<forall>n\<ge>m. u - r < X n" |
|
1378 by (fast intro: less_le_trans) |
|
1379 hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" .. |
|
1380 thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r" |
|
1381 using 1 by (simp add: diff_less_eq add_commute) |
|
1382 qed |
|
1383 |
|
1384 text{*A standard proof of the theorem for monotone increasing sequence*} |
|
1385 |
|
1386 lemma Bseq_mono_convergent: |
|
1387 "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)" |
|
1388 by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI) |
|
1389 |
1376 |
1390 text{*Main monotonicity theorem*} |
1377 text{*Main monotonicity theorem*} |
1391 |
1378 |
1392 lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)" |
1379 lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)" |
1393 by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff |
1380 by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP dest: Bseq_bdd_above Bseq_bdd_below) |
1394 Bseq_mono_convergent) |
1381 |
|
1382 lemma Bseq_mono_convergent: "Bseq X \<Longrightarrow> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n) \<Longrightarrow> convergent (X::nat\<Rightarrow>real)" |
|
1383 by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def) |
1395 |
1384 |
1396 lemma Cauchy_iff: |
1385 lemma Cauchy_iff: |
1397 fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" |
1386 fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" |
1398 shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)" |
1387 shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)" |
1399 unfolding Cauchy_def dist_norm .. |
1388 unfolding Cauchy_def dist_norm .. |