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