Anforderungen  |     |   Wurzel  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


SSL absconv_series.pvs   Sprache: unbekannt

 
%----------------------------------------------------------------------------
%
% 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

90%


[ Verzeichnis aufwärts0.14unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge