|
power_series: THEORY
%----------------------------------------------------------------------------
%
% Definition of power series:
%
% n
% ----
% powerseries(a)(x) = \ a(k)*x^k
% /
% ----
% k = 0
%
% n
% ----
% powerseries(a,m)(x) = \ a(k)*x^k
% /
% ----
% k = m
%
%
% Author: Ricky W. Butler 10/2/00
%
% NOTES:
% * powerseq is defined using IF-THEN-ELSE to avoid 0^0
%
%----------------------------------------------------------------------------
BEGIN
% reals: LIBRARY "../reals"
IMPORTING series, ints@factorial, reals@exponent_props
x,r,y: VAR real
c,px: VAR posreal
x1,z: VAR nonzero_real
n,m: VAR nat
a: VAR sequence[real]
S: VAR set[real]
pn: VAR posnat
% powerseq(a,x): sequence[real] = (LAMBDA (k: nat): a(k)*x^k)
% rule out 0^0
hat_02n: LEMMA 0^pn = 0
AUTO_REWRITE+ expt_x0 % LEMMA x^0 = 1
AUTO_REWRITE+ expt_x1 % LEMMA x^1 = x
AUTO_REWRITE+ expt_1i % LEMMA 1^i = 1
AUTO_REWRITE+ hat_02n % LEMMA 0^pn = 0
powerseq(a,x): sequence[real] = (LAMBDA (k: nat): a(k)*x^k)
powerseries(a)(x): sequence[real] = series(powerseq(a,x))
powerseries(a,m)(x): sequence[real] = series(powerseq(a,x),m)
absolutely_convergent_series?(a): boolean = convergent?(series(abs(a)))
divergent_series?(a): boolean = NOT convergent?(series(a))
powerseries_bounded: LEMMA convergent?(powerseries(a)(x)) IMPLIES
bounded?(powerseq(a, x))
% *** if convergent at one point x1, then abs convergent within (-x1,x1) ***
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: real): 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)))))
% ----- old form retained to preserve old proofs -----
apowerseq(a,x): sequence[real] = (LAMBDA (k: nat): IF k = 0 THEN a(0)
ELSE a(k)*x^k
ENDIF)
apow_rew: LEMMA powerseq(a,x) = apowerseq(a,x)
% to fix old proofs replace (expand "powerseq")
% with (rewrite "apow_rew") (expand "apowerseq")
END power_series
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
