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