Suchen Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Haftungshinweis

Bemerkung: zur Agenda Produktseite wechseln Projekt Beratung

Eigene Datei ansehen e.g. http://myserver.net/mysource.java Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Fortran/ Datei vom 4.1.2008 mit Größe 279 B

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

quality90%