Quelle 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.0 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.