|
1 (* Title : SEQ.thy |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 Description : Convergence of sequences and series |
|
5 *) |
|
6 |
|
7 SEQ = NatStar + HyperPow + |
|
8 |
|
9 constdefs |
|
10 |
|
11 (* Standard definition of convergence of sequence *) |
|
12 LIMSEQ :: [nat=>real,real] => bool ("((_)/ ----> (_))" [60, 60] 60) |
|
13 "X ----> L == (ALL r. #0 < r --> (EX no. ALL n. no <= n --> abs (X n + -L) < r))" |
|
14 |
|
15 (* Nonstandard definition of convergence of sequence *) |
|
16 NSLIMSEQ :: [nat=>real,real] => bool ("((_)/ ----NS> (_))" [60, 60] 60) |
|
17 "X ----NS> L == (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)" |
|
18 |
|
19 (* define value of limit using choice operator*) |
|
20 lim :: (nat => real) => real |
|
21 "lim X == (@L. (X ----> L))" |
|
22 |
|
23 nslim :: (nat => real) => real |
|
24 "nslim X == (@L. (X ----NS> L))" |
|
25 |
|
26 (* Standard definition of convergence *) |
|
27 convergent :: (nat => real) => bool |
|
28 "convergent X == (EX L. (X ----> L))" |
|
29 |
|
30 (* Nonstandard definition of convergence *) |
|
31 NSconvergent :: (nat => real) => bool |
|
32 "NSconvergent X == (EX L. (X ----NS> L))" |
|
33 |
|
34 (* Standard definition for bounded sequence *) |
|
35 Bseq :: (nat => real) => bool |
|
36 "Bseq X == (EX K. (#0 < K & (ALL n. abs(X n) <= K)))" |
|
37 |
|
38 (* Nonstandard definition for bounded sequence *) |
|
39 NSBseq :: (nat=>real) => bool |
|
40 "NSBseq X == (ALL N: HNatInfinite. (*fNat* X) N : HFinite)" |
|
41 |
|
42 (* Definition for monotonicity *) |
|
43 monoseq :: (nat=>real)=>bool |
|
44 "monoseq X == ((ALL (m::nat) n. m <= n --> X m <= X n) | |
|
45 (ALL m n. m <= n --> X n <= X m))" |
|
46 |
|
47 (* Definition of subsequence *) |
|
48 subseq :: (nat => nat) => bool |
|
49 "subseq f == (ALL m n. m < n --> (f m) < (f n))" |
|
50 |
|
51 (** Cauchy condition **) |
|
52 |
|
53 (* Standard definition *) |
|
54 Cauchy :: (nat => real) => bool |
|
55 "Cauchy X == (ALL e. (#0 < e --> |
|
56 (EX M. (ALL m n. M <= m & M <= n |
|
57 --> abs((X m) + -(X n)) < e))))" |
|
58 |
|
59 NSCauchy :: (nat => real) => bool |
|
60 "NSCauchy X == (ALL M: HNatInfinite. ALL N: HNatInfinite. |
|
61 (*fNat* X) M @= (*fNat* X) N)" |
|
62 end |
|
63 |