Marco writes:
| However, there are other definitions of polynomial function which may
| serves you better than the one in Library/poly.ml. In particular, there is
| a notion of univariate real polynomial defined in file iterated.ml (search
| for "polynomial_function") and a notion of multivariate polynomial in
| Multivariate/realanalysis.ml (search for "real_polynomial_function").
Let me just add to this helpful advice that there are also a few
library theorems just explicitly stated as sums without using any
special definition of "polynomial"; this is another possibility.
For example here is the Fundamental Theorem of Algebra
FTA =
|- !a n. a 0 = Cx(&0) \/ ~(!k. k IN 1..n ==> a k = Cx(&0))
==> ?z. vsum(0..n) (\i. a i * z pow i) = Cx(&0)`
and here is the fact that the entire proper maps are precisely the
complex polynomials:
PROPER_MAP_COMPLEX_POLYFUN_EQ =
|- !f. f holomorphic_on (:complex)
==> ((!k. compact k ==> compact {z | f z IN k}) <=>
?c n. 0 < n /\ ~(c n = Cx(&0)) /\
f = \z. vsum(0..n) (\i. c i * z pow i))
John.
------------------------------------------------------------------------------
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the
conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
