Quelle convergence_special.pvs Sprache: PVS

convergence_special: THEORY
%
%  Special sequences that come up over and over
%
%  Taken from Salas/Hille  Calculus page 411
%
%  Author: Ricky W. Butler    NASA Langley   8/24/04
%
%  NOTE:  All of the machinery necessary to prove these is available
%         in analysis and lnexp libraries
%
%  Nothing in the series library depends upon these UNPROVED lemmas
%
BEGIN

   IMPORTING expt, ints@factorial,
             analysis@continuous_functions_more

   n: VAR nat

   x,c: VAR real

   px,pa: VAR posreal

%   xlt1: VAR {x: real | abs(x) < 1}

   cn: VAR sequence[real]

   f: VAR [real -> real]

%  --- note use of "n+1" rather than "n" to avoid div by zero ---

   conv_1_div_n        : LEMMA convergence(LAMBDA n: 1 / (n + 1), 0)

   conv_x_to_1_div_n   : LEMMA convergence(LAMBDA n: px^^(1/(n+1)),1)

   conv_x_to_n         : LEMMA abs(x) < 1 IMPLIES
                                   convergence(LAMBDA n: x^n,0)

   expt_abs_gt         : LEMMA abs(x) ^ n >= x ^ n

   conv_x_to_n_div_fact: LEMMA convergence(LAMBDA n: x^n/factorial(n),0)

%   conv_1_div_N_to_a   : LEMMA %% UNPROVED
%                         convergence(LAMBDA n: 1/((n+1)^^pa),0)

%   conv_ln_div_n       : LEMMA convergence(LAMBDA n: ln(n+1)/(n+1), 0)

%   conv_n_to_1_div_n   : LEMMA convergence(LAMBDA n: (n+1)^^(1/(n+1)),1)

%   conv_n_to_a_div_exp : LEMMA convergence(LAMBDA n: n^^pa/exp(n), 0)

%   conv_exp_spec       : LEMMA convergence(LAMBDA n: (1 + x/(n+1))^(n+1),exp(x))

END convergence_special

quality58%

¤ Dauer der Verarbeitung: 0.14 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.