|
10751
|
1 |
(* Title : HSeries.thy
|
|
|
2 |
Author : Jacques D. Fleuriot
|
|
|
3 |
Copyright : 1998 University of Cambridge
|
|
|
4 |
Description : Finite summation and infinite series
|
|
|
5 |
for hyperreals
|
|
|
6 |
*)
|
|
|
7 |
|
|
|
8 |
HSeries = Series +
|
|
|
9 |
|
|
|
10 |
consts
|
|
|
11 |
sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
|
|
|
12 |
|
|
|
13 |
defs
|
|
|
14 |
sumhr_def
|
|
|
15 |
"sumhr p
|
|
|
16 |
== Abs_hypreal(UN X:Rep_hypnat(fst p).
|
|
|
17 |
UN Y: Rep_hypnat(fst(snd p)).
|
|
10834
|
18 |
hyprel``{%n::nat. sumr (X n) (Y n) (snd(snd p))})"
|
|
10751
|
19 |
|
|
|
20 |
constdefs
|
|
|
21 |
NSsums :: [nat=>real,real] => bool (infixr 80)
|
|
|
22 |
"f NSsums s == (%n. sumr 0 n f) ----NS> s"
|
|
|
23 |
|
|
|
24 |
NSsummable :: (nat=>real) => bool
|
|
|
25 |
"NSsummable f == (EX s. f NSsums s)"
|
|
|
26 |
|
|
|
27 |
NSsuminf :: (nat=>real) => real
|
|
|
28 |
"NSsuminf f == (@s. f NSsums s)"
|
|
|
29 |
|
|
|
30 |
end
|