|
%----------------------------------------------------------------------------
%
% Absolutely Convergent Series
%
% Author: David Lester (Manchester University) 22/04/05
%
%----------------------------------------------------------------------------
absconv_series: THEORY
BEGIN
IMPORTING series_lems
n,m: VAR nat
x: VAR real
nnx,nny: VAR nnreal
f: VAR extraction
a,b: VAR sequence[real]
nna,nnb: VAR sequence[nnreal]
phi: VAR (bijective?[nat,nat])
inj: VAR (injective?[nat,nat])
Convergent_Series: TYPE+ = {s: sequence[real] | convergent?(series(s))}
CONTAINING (LAMBDA n: 0)
absconvergent?(a):bool = convergent?(series(abs(a)))
absconvergent_series: TYPE+ = (absconvergent?)
absconvergent_series_is_convergent:
JUDGEMENT absconvergent_series SUBTYPE_OF Convergent_Series
aa,bb: VAR absconvergent_series
abs_series_bij_abs: LEMMA
convergence(series(aa o phi),x) IFF convergence(series(aa),x)
abs_series_bij_conv_abs: LEMMA
convergent?(series(aa o phi)) IFF convergent?(series(aa))
abs_series_bij_limit_abs: LEMMA
limit(series(aa o phi)) = limit(series(aa))
% extractions of sequences ...
extract_convergent: LEMMA convergent?(series(a)) => convergent?(series(a) o f)
extract_comp: LEMMA series(a o f)
= series(lambda n: IF (EXISTS m: n = f(m)) THEN a(n) ELSE 0 ENDIF) o f
subseq_absconvergent: LEMMA subseq(a,bb) => absconvergent?(a)
nonneg_subseq: LEMMA subseq(nna,nnb) AND convergence(series(nnb),nny) =>
EXISTS nnx:
convergence(series(nna),nnx) AND nnx <= nny
sum_absconvergent: LEMMA absconvergent?(aa+bb)
opp_absconvergent: LEMMA absconvergent?(-aa)
diff_absconvergent: LEMMA absconvergent?(aa-bb)
scal_absconvergent: LEMMA absconvergent?(x*aa)
END absconv_series
¤ Dauer der Verarbeitung: 0.16 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.
|
