author | huffman |
Tue, 17 Apr 2007 03:13:38 +0200 | |
changeset 22722 | 704de05715b4 |
parent 22631 | 7ae5a6ab7bd6 |
child 27435 | b3f8e9bdf9a7 |
permissions | -rw-r--r-- |
22631
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
1 |
(* Title : HSEQ.thy |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
2 |
Author : Jacques D. Fleuriot |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
3 |
Copyright : 1998 University of Cambridge |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
4 |
Description : Convergence of sequences and series |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
5 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
6 |
Additional contributions by Jeremy Avigad and Brian Huffman |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
7 |
*) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
8 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
9 |
header {* Sequences and Convergence (Nonstandard) *} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
10 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
11 |
theory HSEQ |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
12 |
imports SEQ NatStar |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
13 |
begin |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
14 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
15 |
definition |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
16 |
NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
17 |
("((_)/ ----NS> (_))" [60, 60] 60) where |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
18 |
--{*Nonstandard definition of convergence of sequence*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
19 |
"X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
20 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
21 |
definition |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
22 |
nslim :: "(nat => 'a::real_normed_vector) => 'a" where |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
23 |
--{*Nonstandard definition of limit using choice operator*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
24 |
"nslim X = (THE L. X ----NS> L)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
25 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
26 |
definition |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
27 |
NSconvergent :: "(nat => 'a::real_normed_vector) => bool" where |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
28 |
--{*Nonstandard definition of convergence*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
29 |
"NSconvergent X = (\<exists>L. X ----NS> L)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
30 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
31 |
definition |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
32 |
NSBseq :: "(nat => 'a::real_normed_vector) => bool" where |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
33 |
--{*Nonstandard definition for bounded sequence*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
34 |
"NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
35 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
36 |
definition |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
37 |
NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
38 |
--{*Nonstandard definition*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
39 |
"NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
40 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
41 |
subsection {* Limits of Sequences *} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
42 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
43 |
lemma NSLIMSEQ_iff: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
44 |
"(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
45 |
by (simp add: NSLIMSEQ_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
46 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
47 |
lemma NSLIMSEQ_I: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
48 |
"(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X ----NS> L" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
49 |
by (simp add: NSLIMSEQ_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
50 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
51 |
lemma NSLIMSEQ_D: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
52 |
"\<lbrakk>X ----NS> L; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X N \<approx> star_of L" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
53 |
by (simp add: NSLIMSEQ_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
54 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
55 |
lemma NSLIMSEQ_const: "(%n. k) ----NS> k" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
56 |
by (simp add: NSLIMSEQ_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
57 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
58 |
lemma NSLIMSEQ_add: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
59 |
"[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
60 |
by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric]) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
61 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
62 |
lemma NSLIMSEQ_add_const: "f ----NS> a ==> (%n.(f n + b)) ----NS> a + b" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
63 |
by (simp only: NSLIMSEQ_add NSLIMSEQ_const) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
64 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
65 |
lemma NSLIMSEQ_mult: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
66 |
fixes a b :: "'a::real_normed_algebra" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
67 |
shows "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
68 |
by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
69 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
70 |
lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
71 |
by (auto simp add: NSLIMSEQ_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
72 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
73 |
lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
74 |
by (drule NSLIMSEQ_minus, simp) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
75 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
76 |
(* FIXME: delete *) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
77 |
lemma NSLIMSEQ_add_minus: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
78 |
"[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
79 |
by (simp add: NSLIMSEQ_add NSLIMSEQ_minus) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
80 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
81 |
lemma NSLIMSEQ_diff: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
82 |
"[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
83 |
by (simp add: diff_minus NSLIMSEQ_add NSLIMSEQ_minus) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
84 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
85 |
lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
86 |
by (simp add: NSLIMSEQ_diff NSLIMSEQ_const) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
87 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
88 |
lemma NSLIMSEQ_inverse: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
89 |
fixes a :: "'a::real_normed_div_algebra" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
90 |
shows "[| X ----NS> a; a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
91 |
by (simp add: NSLIMSEQ_def star_of_approx_inverse) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
92 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
93 |
lemma NSLIMSEQ_mult_inverse: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
94 |
fixes a b :: "'a::real_normed_field" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
95 |
shows |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
96 |
"[| X ----NS> a; Y ----NS> b; b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
97 |
by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
98 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
99 |
lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
100 |
by transfer simp |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
101 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
102 |
lemma NSLIMSEQ_norm: "X ----NS> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----NS> norm a" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
103 |
by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
104 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
105 |
text{*Uniqueness of limit*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
106 |
lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
107 |
apply (simp add: NSLIMSEQ_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
108 |
apply (drule HNatInfinite_whn [THEN [2] bspec])+ |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
109 |
apply (auto dest: approx_trans3) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
110 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
111 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
112 |
lemma NSLIMSEQ_pow [rule_format]: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
113 |
fixes a :: "'a::{real_normed_algebra,recpower}" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
114 |
shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
115 |
apply (induct "m") |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
116 |
apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
117 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
118 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
119 |
text{*We can now try and derive a few properties of sequences, |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
120 |
starting with the limit comparison property for sequences.*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
121 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
122 |
lemma NSLIMSEQ_le: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
123 |
"[| f ----NS> l; g ----NS> m; |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
124 |
\<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
125 |
|] ==> l \<le> (m::real)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
126 |
apply (simp add: NSLIMSEQ_def, safe) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
127 |
apply (drule starfun_le_mono) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
128 |
apply (drule HNatInfinite_whn [THEN [2] bspec])+ |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
129 |
apply (drule_tac x = whn in spec) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
130 |
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+ |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
131 |
apply clarify |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
132 |
apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
133 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
134 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
135 |
lemma NSLIMSEQ_le_const: "[| X ----NS> (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
136 |
by (erule NSLIMSEQ_le [OF NSLIMSEQ_const], auto) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
137 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
138 |
lemma NSLIMSEQ_le_const2: "[| X ----NS> (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
139 |
by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const], auto) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
140 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
141 |
text{*Shift a convergent series by 1: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
142 |
By the equivalence between Cauchiness and convergence and because |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
143 |
the successor of an infinite hypernatural is also infinite.*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
144 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
145 |
lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
146 |
apply (unfold NSLIMSEQ_def, safe) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
147 |
apply (drule_tac x="N + 1" in bspec) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
148 |
apply (erule HNatInfinite_add) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
149 |
apply (simp add: starfun_shift_one) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
150 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
151 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
152 |
lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
153 |
apply (unfold NSLIMSEQ_def, safe) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
154 |
apply (drule_tac x="N - 1" in bspec) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
155 |
apply (erule Nats_1 [THEN [2] HNatInfinite_diff]) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
156 |
apply (simp add: starfun_shift_one one_le_HNatInfinite) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
157 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
158 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
159 |
lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
160 |
by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
161 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
162 |
subsubsection {* Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ} *} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
163 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
164 |
lemma LIMSEQ_NSLIMSEQ: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
165 |
assumes X: "X ----> L" shows "X ----NS> L" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
166 |
proof (rule NSLIMSEQ_I) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
167 |
fix N assume N: "N \<in> HNatInfinite" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
168 |
have "starfun X N - star_of L \<in> Infinitesimal" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
169 |
proof (rule InfinitesimalI2) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
170 |
fix r::real assume r: "0 < r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
171 |
from LIMSEQ_D [OF X r] |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
172 |
obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" .. |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
173 |
hence "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
174 |
by transfer |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
175 |
thus "hnorm (starfun X N - star_of L) < star_of r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
176 |
using N by (simp add: star_of_le_HNatInfinite) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
177 |
qed |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
178 |
thus "starfun X N \<approx> star_of L" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
179 |
by (unfold approx_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
180 |
qed |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
181 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
182 |
lemma NSLIMSEQ_LIMSEQ: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
183 |
assumes X: "X ----NS> L" shows "X ----> L" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
184 |
proof (rule LIMSEQ_I) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
185 |
fix r::real assume r: "0 < r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
186 |
have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
187 |
proof (intro exI allI impI) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
188 |
fix n assume "whn \<le> n" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
189 |
with HNatInfinite_whn have "n \<in> HNatInfinite" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
190 |
by (rule HNatInfinite_upward_closed) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
191 |
with X have "starfun X n \<approx> star_of L" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
192 |
by (rule NSLIMSEQ_D) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
193 |
hence "starfun X n - star_of L \<in> Infinitesimal" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
194 |
by (unfold approx_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
195 |
thus "hnorm (starfun X n - star_of L) < star_of r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
196 |
using r by (rule InfinitesimalD2) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
197 |
qed |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
198 |
thus "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
199 |
by transfer |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
200 |
qed |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
201 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
202 |
theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
203 |
by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
204 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
205 |
(* Used once by Integration/Rats.thy in AFP *) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
206 |
lemma NSLIMSEQ_finite_set: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
207 |
"!!(f::nat=>nat). \<forall>n. n \<le> f n ==> finite {n. f n \<le> u}" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
208 |
by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
209 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
210 |
subsubsection {* Derived theorems about @{term NSLIMSEQ} *} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
211 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
212 |
text{*We prove the NS version from the standard one, since the NS proof |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
213 |
seems more complicated than the standard one above!*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
214 |
lemma NSLIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) ----NS> 0) = (X ----NS> 0)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
215 |
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_norm_zero) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
216 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
217 |
lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> (0::real))" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
218 |
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
219 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
220 |
text{*Generalization to other limits*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
221 |
lemma NSLIMSEQ_imp_rabs: "f ----NS> (l::real) ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
222 |
apply (simp add: NSLIMSEQ_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
223 |
apply (auto intro: approx_hrabs |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
224 |
simp add: starfun_abs) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
225 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
226 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
227 |
lemma NSLIMSEQ_inverse_zero: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
228 |
"\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
229 |
==> (%n. inverse(f n)) ----NS> 0" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
230 |
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
231 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
232 |
lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
233 |
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
234 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
235 |
lemma NSLIMSEQ_inverse_real_of_nat_add: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
236 |
"(%n. r + inverse(real(Suc n))) ----NS> r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
237 |
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
238 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
239 |
lemma NSLIMSEQ_inverse_real_of_nat_add_minus: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
240 |
"(%n. r + -inverse(real(Suc n))) ----NS> r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
241 |
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
242 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
243 |
lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
244 |
"(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
245 |
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
246 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
247 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
248 |
subsection {* Convergence *} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
249 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
250 |
lemma nslimI: "X ----NS> L ==> nslim X = L" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
251 |
apply (simp add: nslim_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
252 |
apply (blast intro: NSLIMSEQ_unique) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
253 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
254 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
255 |
lemma lim_nslim_iff: "lim X = nslim X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
256 |
by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
257 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
258 |
lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X ----NS> L)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
259 |
by (simp add: NSconvergent_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
260 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
261 |
lemma NSconvergentI: "(X ----NS> L) ==> NSconvergent X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
262 |
by (auto simp add: NSconvergent_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
263 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
264 |
lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
265 |
by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
266 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
267 |
lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X ----NS> nslim X)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
268 |
by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
269 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
270 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
271 |
subsection {* Bounded Monotonic Sequences *} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
272 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
273 |
lemma NSBseqD: "[| NSBseq X; N: HNatInfinite |] ==> ( *f* X) N : HFinite" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
274 |
by (simp add: NSBseq_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
275 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
276 |
lemma Standard_subset_HFinite: "Standard \<subseteq> HFinite" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
277 |
unfolding Standard_def by auto |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
278 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
279 |
lemma NSBseqD2: "NSBseq X \<Longrightarrow> ( *f* X) N \<in> HFinite" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
280 |
apply (cases "N \<in> HNatInfinite") |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
281 |
apply (erule (1) NSBseqD) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
282 |
apply (rule subsetD [OF Standard_subset_HFinite]) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
283 |
apply (simp add: HNatInfinite_def Nats_eq_Standard) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
284 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
285 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
286 |
lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite ==> NSBseq X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
287 |
by (simp add: NSBseq_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
288 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
289 |
text{*The standard definition implies the nonstandard definition*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
290 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
291 |
lemma Bseq_NSBseq: "Bseq X ==> NSBseq X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
292 |
proof (unfold NSBseq_def, safe) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
293 |
assume X: "Bseq X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
294 |
fix N assume N: "N \<in> HNatInfinite" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
295 |
from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K" by fast |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
296 |
hence "\<forall>N. hnorm (starfun X N) \<le> star_of K" by transfer |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
297 |
hence "hnorm (starfun X N) \<le> star_of K" by simp |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
298 |
also have "star_of K < star_of (K + 1)" by simp |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
299 |
finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x" by (rule bexI, simp) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
300 |
thus "starfun X N \<in> HFinite" by (simp add: HFinite_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
301 |
qed |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
302 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
303 |
text{*The nonstandard definition implies the standard definition*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
304 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
305 |
lemma SReal_less_omega: "r \<in> \<real> \<Longrightarrow> r < \<omega>" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
306 |
apply (insert HInfinite_omega) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
307 |
apply (simp add: HInfinite_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
308 |
apply (simp add: order_less_imp_le) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
309 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
310 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
311 |
lemma NSBseq_Bseq: "NSBseq X \<Longrightarrow> Bseq X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
312 |
proof (rule ccontr) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
313 |
let ?n = "\<lambda>K. LEAST n. K < norm (X n)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
314 |
assume "NSBseq X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
315 |
hence finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
316 |
by (rule NSBseqD2) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
317 |
assume "\<not> Bseq X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
318 |
hence "\<forall>K>0. \<exists>n. K < norm (X n)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
319 |
by (simp add: Bseq_def linorder_not_le) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
320 |
hence "\<forall>K>0. K < norm (X (?n K))" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
321 |
by (auto intro: LeastI_ex) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
322 |
hence "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
323 |
by transfer |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
324 |
hence "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
325 |
by simp |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
326 |
hence "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
327 |
by (simp add: order_less_trans [OF SReal_less_omega]) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
328 |
hence "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
329 |
by (simp add: HInfinite_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
330 |
with finite show "False" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
331 |
by (simp add: HFinite_HInfinite_iff) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
332 |
qed |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
333 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
334 |
text{* Equivalence of nonstandard and standard definitions |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
335 |
for a bounded sequence*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
336 |
lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
337 |
by (blast intro!: NSBseq_Bseq Bseq_NSBseq) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
338 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
339 |
text{*A convergent sequence is bounded: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
340 |
Boundedness as a necessary condition for convergence. |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
341 |
The nonstandard version has no existential, as usual *} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
342 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
343 |
lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
344 |
apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
345 |
apply (blast intro: HFinite_star_of approx_sym approx_HFinite) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
346 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
347 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
348 |
text{*Standard Version: easily now proved using equivalence of NS and |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
349 |
standard definitions *} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
350 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
351 |
lemma convergent_Bseq: "convergent X ==> Bseq X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
352 |
by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
353 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
354 |
subsubsection{*Upper Bounds and Lubs of Bounded Sequences*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
355 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
356 |
lemma NSBseq_isUb: "NSBseq X ==> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
357 |
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
358 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
359 |
lemma NSBseq_isLub: "NSBseq X ==> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
360 |
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
361 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
362 |
subsubsection{*A Bounded and Monotonic Sequence Converges*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
363 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
364 |
text{* The best of both worlds: Easier to prove this result as a standard |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
365 |
theorem and then use equivalence to "transfer" it into the |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
366 |
equivalent nonstandard form if needed!*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
367 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
368 |
lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X ----NS> L)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
369 |
by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
370 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
371 |
lemma NSBseq_mono_NSconvergent: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
372 |
"[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent (X::nat=>real)" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
373 |
by (auto intro: Bseq_mono_convergent |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
374 |
simp add: convergent_NSconvergent_iff [symmetric] |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
375 |
Bseq_NSBseq_iff [symmetric]) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
376 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
377 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
378 |
subsection {* Cauchy Sequences *} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
379 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
380 |
lemma NSCauchyI: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
381 |
"(\<And>M N. \<lbrakk>M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X M \<approx> starfun X N) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
382 |
\<Longrightarrow> NSCauchy X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
383 |
by (simp add: NSCauchy_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
384 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
385 |
lemma NSCauchyD: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
386 |
"\<lbrakk>NSCauchy X; M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk> |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
387 |
\<Longrightarrow> starfun X M \<approx> starfun X N" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
388 |
by (simp add: NSCauchy_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
389 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
390 |
subsubsection{*Equivalence Between NS and Standard*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
391 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
392 |
lemma Cauchy_NSCauchy: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
393 |
assumes X: "Cauchy X" shows "NSCauchy X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
394 |
proof (rule NSCauchyI) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
395 |
fix M assume M: "M \<in> HNatInfinite" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
396 |
fix N assume N: "N \<in> HNatInfinite" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
397 |
have "starfun X M - starfun X N \<in> Infinitesimal" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
398 |
proof (rule InfinitesimalI2) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
399 |
fix r :: real assume r: "0 < r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
400 |
from CauchyD [OF X r] |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
401 |
obtain k where "\<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" .. |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
402 |
hence "\<forall>m\<ge>star_of k. \<forall>n\<ge>star_of k. |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
403 |
hnorm (starfun X m - starfun X n) < star_of r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
404 |
by transfer |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
405 |
thus "hnorm (starfun X M - starfun X N) < star_of r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
406 |
using M N by (simp add: star_of_le_HNatInfinite) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
407 |
qed |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
408 |
thus "starfun X M \<approx> starfun X N" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
409 |
by (unfold approx_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
410 |
qed |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
411 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
412 |
lemma NSCauchy_Cauchy: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
413 |
assumes X: "NSCauchy X" shows "Cauchy X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
414 |
proof (rule CauchyI) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
415 |
fix r::real assume r: "0 < r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
416 |
have "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. hnorm (starfun X m - starfun X n) < star_of r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
417 |
proof (intro exI allI impI) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
418 |
fix M assume "whn \<le> M" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
419 |
with HNatInfinite_whn have M: "M \<in> HNatInfinite" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
420 |
by (rule HNatInfinite_upward_closed) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
421 |
fix N assume "whn \<le> N" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
422 |
with HNatInfinite_whn have N: "N \<in> HNatInfinite" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
423 |
by (rule HNatInfinite_upward_closed) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
424 |
from X M N have "starfun X M \<approx> starfun X N" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
425 |
by (rule NSCauchyD) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
426 |
hence "starfun X M - starfun X N \<in> Infinitesimal" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
427 |
by (unfold approx_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
428 |
thus "hnorm (starfun X M - starfun X N) < star_of r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
429 |
using r by (rule InfinitesimalD2) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
430 |
qed |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
431 |
thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
432 |
by transfer |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
433 |
qed |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
434 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
435 |
theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
436 |
by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
437 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
438 |
subsubsection {* Cauchy Sequences are Bounded *} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
439 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
440 |
text{*A Cauchy sequence is bounded -- nonstandard version*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
441 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
442 |
lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
443 |
by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
444 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
445 |
subsubsection {* Cauchy Sequences are Convergent *} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
446 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
447 |
text{*Equivalence of Cauchy criterion and convergence: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
448 |
We will prove this using our NS formulation which provides a |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
449 |
much easier proof than using the standard definition. We do not |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
450 |
need to use properties of subsequences such as boundedness, |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
451 |
monotonicity etc... Compare with Harrison's corresponding proof |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
452 |
in HOL which is much longer and more complicated. Of course, we do |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
453 |
not have problems which he encountered with guessing the right |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
454 |
instantiations for his 'espsilon-delta' proof(s) in this case |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
455 |
since the NS formulations do not involve existential quantifiers.*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
456 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
457 |
lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
458 |
apply (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def, safe) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
459 |
apply (auto intro: approx_trans2) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
460 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
461 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
462 |
lemma real_NSCauchy_NSconvergent: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
463 |
fixes X :: "nat \<Rightarrow> real" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
464 |
shows "NSCauchy X \<Longrightarrow> NSconvergent X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
465 |
apply (simp add: NSconvergent_def NSLIMSEQ_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
466 |
apply (frule NSCauchy_NSBseq) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
467 |
apply (simp add: NSBseq_def NSCauchy_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
468 |
apply (drule HNatInfinite_whn [THEN [2] bspec]) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
469 |
apply (drule HNatInfinite_whn [THEN [2] bspec]) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
470 |
apply (auto dest!: st_part_Ex simp add: SReal_iff) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
471 |
apply (blast intro: approx_trans3) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
472 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
473 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
474 |
lemma NSCauchy_NSconvergent: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
475 |
fixes X :: "nat \<Rightarrow> 'a::banach" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
476 |
shows "NSCauchy X \<Longrightarrow> NSconvergent X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
477 |
apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent]) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
478 |
apply (erule convergent_NSconvergent_iff [THEN iffD1]) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
479 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
480 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
481 |
lemma NSCauchy_NSconvergent_iff: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
482 |
fixes X :: "nat \<Rightarrow> 'a::banach" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
483 |
shows "NSCauchy X = NSconvergent X" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
484 |
by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
485 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
486 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
487 |
subsection {* Power Sequences *} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
488 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
489 |
text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
490 |
"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
491 |
also fact that bounded and monotonic sequence converges.*} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
492 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
493 |
text{* We now use NS criterion to bring proof of theorem through *} |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
494 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
495 |
lemma NSLIMSEQ_realpow_zero: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
496 |
"[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) ----NS> 0" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
497 |
apply (simp add: NSLIMSEQ_def) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
498 |
apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
499 |
apply (frule NSconvergentD) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
500 |
apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
501 |
apply (frule HNatInfinite_add_one) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
502 |
apply (drule bspec, assumption) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
503 |
apply (drule bspec, assumption) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
504 |
apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
505 |
apply (simp add: hyperpow_add) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
506 |
apply (drule approx_mult_subst_star_of, assumption) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
507 |
apply (drule approx_trans3, assumption) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
508 |
apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric]) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
509 |
done |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
510 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
511 |
lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
512 |
by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric]) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
513 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
514 |
lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----NS> 0" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
515 |
by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric]) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
516 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
517 |
(***--------------------------------------------------------------- |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
518 |
Theorems proved by Harrison in HOL that we do not need |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
519 |
in order to prove equivalence between Cauchy criterion |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
520 |
and convergence: |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
521 |
-- Show that every sequence contains a monotonic subsequence |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
522 |
Goal "\<exists>f. subseq f & monoseq (%n. s (f n))" |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
523 |
-- Show that a subsequence of a bounded sequence is bounded |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
524 |
Goal "Bseq X ==> Bseq (%n. X (f n))"; |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
525 |
-- Show we can take subsequential terms arbitrarily far |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
526 |
up a sequence |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
527 |
Goal "subseq f ==> n \<le> f(n)"; |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
528 |
Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)"; |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
529 |
---------------------------------------------------------------***) |
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
530 |
|
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
diff
changeset
|
531 |
end |