| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sigma_set/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle absconv_series_aux.pvs Sprache: PVS |
|||||||||
|
%----------------------------------------------------------------------------
% % 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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28