2 Author : Jacques D. Fleuriot
3 Copyright : 1998 University of Cambridge
4 Description : Convergence of sequences and series
7 SEQ = NatStar + HyperPow +
11 (* Standard definition of convergence of sequence *)
12 LIMSEQ :: [nat=>real,real] => bool ("((_)/ ----> (_))" [60, 60] 60)
13 "X ----> L == (ALL r. Numeral0 < r --> (EX no. ALL n. no <= n --> abs (X n + -L) < r))"
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)"
19 (* define value of limit using choice operator*)
20 lim :: (nat => real) => real
21 "lim X == (@L. (X ----> L))"
23 nslim :: (nat => real) => real
24 "nslim X == (@L. (X ----NS> L))"
26 (* Standard definition of convergence *)
27 convergent :: (nat => real) => bool
28 "convergent X == (EX L. (X ----> L))"
30 (* Nonstandard definition of convergence *)
31 NSconvergent :: (nat => real) => bool
32 "NSconvergent X == (EX L. (X ----NS> L))"
34 (* Standard definition for bounded sequence *)
35 Bseq :: (nat => real) => bool
36 "Bseq X == (EX K. (Numeral0 < K & (ALL n. abs(X n) <= K)))"
38 (* Nonstandard definition for bounded sequence *)
39 NSBseq :: (nat=>real) => bool
40 "NSBseq X == (ALL N: HNatInfinite. (*fNat* X) N : HFinite)"
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))"
47 (* Definition of subsequence *)
48 subseq :: (nat => nat) => bool
49 "subseq f == (ALL m n. m < n --> (f m) < (f n))"
51 (** Cauchy condition **)
53 (* Standard definition *)
54 Cauchy :: (nat => real) => bool
55 "Cauchy X == (ALL e. (Numeral0 < e -->
56 (EX M. (ALL m n. M <= m & M <= n
57 --> abs((X m) + -(X n)) < e))))"
59 NSCauchy :: (nat => real) => bool
60 "NSCauchy X == (ALL M: HNatInfinite. ALL N: HNatInfinite.
61 (*fNat* X) M @= (*fNat* X) N)"