|
13957
|
1 |
(* Title : CSeries.thy
|
|
|
2 |
Author : Jacques D. Fleuriot
|
|
|
3 |
Copyright : 2002 University of Edinburgh
|
|
|
4 |
Description : Finite summation and infinite series for complex numbers
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
CSeries = CStar +
|
|
|
8 |
|
|
|
9 |
consts sumc :: "[nat,nat,(nat=>complex)] => complex"
|
|
|
10 |
primrec
|
|
|
11 |
sumc_0 "sumc m 0 f = 0"
|
|
|
12 |
sumc_Suc "sumc m (Suc n) f = (if n < m then 0 else sumc m n f + f(n))"
|
|
|
13 |
|
|
|
14 |
(*
|
|
|
15 |
constdefs
|
|
|
16 |
|
|
|
17 |
needs convergence of complex sequences
|
|
|
18 |
|
|
|
19 |
csums :: [nat=>complex,complex] => bool (infixr 80)
|
|
|
20 |
"f sums s == (%n. sumr 0 n f) ----C> s"
|
|
|
21 |
|
|
|
22 |
csummable :: (nat=>complex) => bool
|
|
|
23 |
"csummable f == (EX s. f csums s)"
|
|
|
24 |
|
|
|
25 |
csuminf :: (nat=>complex) => complex
|
|
|
26 |
"csuminf f == (@s. f csums s)"
|
|
|
27 |
*)
|
|
|
28 |
|
|
|
29 |
end
|
|
|
30 |
|