top: THEORY %---------------------------------------------------------------------------- % % Infinite Series % % Author: Ricky W. Butler 11/01/00 % David Lester 12/01/03 (generalizations) % (Manchester University) % % CHANGES: % % Version 1.0 -- 11/01/00 % Version 1.1 (Lester) -- updated nth_derivatives and taylors theories % Version 1.2 -- 7/8/04 proved axioms, major upgrade % new theory: taylor_series % Version 1.3 -- 1/5/05 update to analysis name changes% % Version 1.4 -- 3/22/06 simplified powerseq definition and % moved nth_derivatives and taylors % to analysis library % Version 1.5 -- 12/14/07 added series_lems, absconv theories % Version 1.6 -- 9/15/09 series_aux %---------------------------------------------------------------------------- BEGIN
IMPORTING series, % definition + properies of infinite series
series_lems, % New basic theorems
series_aux, % more theorems from David Lester
absconv_series, % Absolute convergence
power_series, % definition + properies of power series
trig_fun, % definition of trigonometric functions
trig_props, % basic trig identities
taylor_series, % expansion into Taylor's series
power_series_deriv, % derivative of a power series
power_series_integ % integral of a power series
