|
%----------------------------------------------------------------------------
%
% Absolutely Convergent Series
%
% Author: David Lester (Manchester University) 22/04/05
%
%----------------------------------------------------------------------------
absconv_series_aux: THEORY
BEGIN
IMPORTING series@series_aux,
series@absconv_series,
sets_aux@infinite_image,
sets_aux@countable_props,
sets_aux@countable_image,
analysis@convergence_ops % proof only
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])
% Following should probably be in analysis@sequence_props.pvs:
extract_bij: LEMMA bijective?[nat,(image(f,fullset[nat]))](f)
subseq_def: LEMMA subseq(a,b) IFF EXISTS f: FORALL n: a(n) = b(f(n))
S: VAR countably_infinite_set[nat]
IMPORTING orders@integer_enumerations[nat]
inj_is_bij_extract: LEMMA EXISTS phi,f: inj = phi o f
nonneg_series_inj_conv: LEMMA convergent?(series(nna)) =>
convergent?(series(nna o inj))
nonneg_series_inj_limit: LEMMA convergent?(series(nna)) =>
limit(series(nna)) >= limit(series(nna o inj))
% Any absolutely convergent series can be arbitrarily rearranged omitting
% terms.
aa: VAR absconvergent_series
abs_series_inj_conv: LEMMA convergent?(series(aa o inj))
END absconv_series_aux
¤ Dauer der Verarbeitung: 0.23 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.
|
