SSL power_series_conv.pvs Sprache: PVS

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

quality57%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Versionsinformation zu Columbo

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders