|
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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
