|
power_series_conv[T: TYPE from real]: THEORY
%----------------------------------------------------------------------------
%
% Infinite sum of power series:
% n
% ----
% inf_sum(a)(x) = limit \ a(k)*x^k
% n -> inf /
% ----
% k = 0
%
% The theory parameter T is the domain of convergence of the power series.
% In theory power_series this is shown to be either be all of the reals or
% the interval {x| -R < x < R} where R is the radius of convergence
%
% Author: Ricky W. Butler 10/2/00
%
%
%----------------------------------------------------------------------------
BEGIN
ASSUMING
x: VAR T
IMPORTING power_series, analysis@deriv_domain_def
not_one_element : ASSUMPTION not_one_element?[T]
deriv_domain : ASSUMPTION deriv_domain?[T]
open : ASSUMPTION
FORALL (x : T) : EXISTS (delta : posreal): FORALL (y: real):
abs(x-y) < delta IMPLIES T_pred(y)
ENDASSUMING
n,m,N: VAR nat
a: VAR sequence[real]
AUTO_REWRITE- abs_0
AUTO_REWRITE- abs_nat
% ----- convergent over whole domain -----
conv_powerseries?(a): bool = (FORALL x: convergent?(powerseries(a)(x)))
Inf_sum(a: (conv_powerseries?))(x): real = limit(powerseries(a)(x))
conv_powerseries?(a,m): bool = (FORALL x: convergent?(powerseries(a,m)(x)))
Inf_sum(m: nat, a: {a | conv_powerseries?(a,m)})(x): real =
limit(powerseries(a,m)(x))
end_powerseries_conv : THEOREM conv_powerseries?(a) IFF
conv_powerseries?(a,m)
% t1: LEMMA
Inf_inf: LEMMA conv_powerseries?(a) IMPLIES
Inf_sum(a) = (LAMBDA x: inf_sum(powerseq(a,x)))
Inf_inf_m: LEMMA conv_powerseries?(a,m) IMPLIES
Inf_sum(m,a) = (LAMBDA x: inf_sum(m,powerseq(a,x)))
% ------ Convergent powerseries is absolutely convergent -----
powerseries_abs_conv: LEMMA (FORALL (x: T): convergent?(powerseries(a)(x)))
IMPLIES
(FORALL (x: T): convergent?(series(abs(powerseq(a,x)))))
% ------ A few simple power series --------------------- -----
simple(x): sequence[real] = (LAMBDA n: x^n/factorial(n))
simple_0_conv: LEMMA T_pred(0) IMPLIES convergent?(series(simple(0)))
simple_conv: LEMMA convergent?(series(simple(x)))
m1_conv: LEMMA abs(x) < 1 IMPLIES
convergent?(powerseries((LAMBDA (n: nat): (-1) ^ n))(x))
END power_series_conv
¤ Dauer der Verarbeitung: 0.2 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.
|
