Quelle power_series.pvs Sprache: PVS

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

quality94%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.