power_series: THEORY %---------------------------------------------------------------------------- % % Definition of power series % % Author: Ricky W. Butler 10/2/00 % % %---------------------------------------------------------------------------- BEGIN reals: LIBRARY "../reals" IMPORTING series, factorial, reals@exponent_props x,r,y: VAR real c,px: VAR posreal x1,z: VAR nonzero_real n: VAR nat a: VAR sequence[real] S: VAR set[real] powerseq(a,x): sequence[real] = (LAMBDA (k: nat): a(k)*x^k) powerseries(a,x): sequence[real] = series(powerseq(a,x)) absolutely_convergent_series?(a): boolean = convergent(series(abs(a))) divergent_series?(a): boolean = NOT convergent(series(a)) powerseries_conv_point: THEOREM convergent(powerseries(a,x1)) AND abs(x) < abs(x1) IMPLIES absolutely_convergent_series?(powerseq(a,x)) powerseries_conv: COROLLARY convergent(powerseries(a,x)) AND abs(y) < abs(x) IMPLIES convergent(powerseries(a,y)) powerseries_diverg: COROLLARY divergent_series?(powerseq(a,x1)) AND abs(x) > abs(x1) IMPLIES divergent_series?(powerseq(a,x)) series_convergent_within(a,c): bool = (FORALL x: abs(x) < c IMPLIES convergent(series(powerseq(a,x)))) series_divergent_outside(a,c): bool = (FORALL x: abs(x) > c IMPLIES divergent_series?(powerseq(a,x))) series_convergent_only_at_0(a): bool = convergent(series(powerseq(a,0))) AND (FORALL x: x /= 0 IMPLIES divergent_series?(powerseq(a,x))) % ------ behavior of series at x = c or x = -c is not predictable ------ zero_powerseries_conv: LEMMA convergent(powerseries(a,0)) powerseries_three_cases: THEOREM (FORALL x: convergent(powerseries(a,x))) OR (series_convergent_only_at_0(a)) OR (EXISTS (r: posreal): series_convergent_within(a,r) AND series_divergent_outside(a,r)) interval(c): set[real] = {x: real | -c < x AND x < c} powerseries_conv_abs_intv: LEMMA (FORALL (x: (interval(c))): convergent(series(powerseq(a,x)))) IMPLIES (FORALL (x: (interval(c))): convergent(series(abs(powerseq(a,x))))) powerseries_conv_abs: LEMMA (FORALL x: convergent(series(powerseq(a,x)))) IMPLIES (FORALL x: convergent(series(abs(powerseq(a,x))))) simple(x): sequence[real] = (LAMBDA n: x^n/factorial(n)) simple_0_conv: LEMMA convergent(series(simple(0))) simple_conv: LEMMA convergent(series(simple(x))) END power_series