Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: convergence_ops.pvs Sprache: PVS

Original von: PVS^©

convergence_ops : THEORY
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Limits and operations on sequences of reals
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
BEGIN

  IMPORTING convergence_sequences, epsilon_lemmas

  s, s1, s2 : VAR sequence[real]

  s3 : VAR sequence[nzreal]

  a : VAR real

  l, l1, l2 : VAR real

  n, m, N : VAR nat

  %---------------------------------
  %  limits of sum, product, etc.
  %---------------------------------

  cnv_seq_sum : LEMMA
  convergence(s1, l1) AND convergence(s2, l2)
IMPLIES convergence(s1 + s2, l1 + l2)

  cnv_seq_neg : LEMMA
  convergence(s1, l1)
IMPLIES convergence(-s1, -l1)

  cnv_seq_diff : LEMMA
  convergence(s1, l1) AND convergence(s2, l2)
IMPLIES convergence(s1 - s2, l1 - l2)

  cnv_seq_prod : LEMMA
  convergence(s1, l1) AND convergence(s2, l2)
IMPLIES convergence(s1 * s2, l1 * l2)

  cnv_seq_const : LEMMA  convergence(const_fun(a), a)

  cnv_seq_scal : LEMMA
convergence(s1, l1) IMPLIES convergence(a * s1, a * l1)

  cnv_seq_inv : LEMMA
  convergence(s3, l2)  AND l2 /= 0
IMPLIES convergence(1 / s3, 1 / l2)

  cnv_seq_div : LEMMA
  convergence(s1, l1) AND convergence(s3, l2)
     AND l2 /= 0
IMPLIES convergence(s1 / s3, l1 / l2)

  cnv_seq_abs : LEMMA
convergence(s1, l1) IMPLIES convergence(abs(s1), abs(l1))

  cnv_seq_order : LEMMA
  convergence(s1, l1) and convergence(s2, l2)
     AND (FORALL n : s1(n) <= s2(n))
IMPLIES l1 <= l2

  convergence_shift: LEMMA convergence(s,l) IFF
                              convergence(LAMBDA n: s(n+m),l)

  %-------------
  %  Squeezing
  %-------------

  squeezing_variant : LEMMA
      convergence(s1, l) and convergence(s2, l)
     AND (FORALL n : N <= n IMPLIES s1(n) <= s(n) and s(n) <= s2(n))
IMPLIES convergence(s, l)

  squeezing_const1 : LEMMA
  convergence(s1, l)
     AND (FORALL n : N <= n IMPLIES l <= s(n) AND s(n) <= s1(n))
IMPLIES convergence(s, l)

  squeezing_const2 : LEMMA
  convergence(s1, l)
     AND (FORALL n : N <= n IMPLIES s1(n) <= s(n) AND s(n) <= l)
IMPLIES convergence(s, l)

  squeezing : LEMMA
      convergence(s1, l) and convergence(s2, l)
     AND (FORALL n : s1(n) <= s(n) and s(n) <= s2(n))
IMPLIES convergence(s, l)

  squeezing_gen : LEMMA
      convergence(s1, l) and convergence(s2, l)
     AND (FORALL n : n >= N IMPLIES s1(n) <= s(n) and s(n) <= s2(n))
IMPLIES convergence(s, l)

  abs_convergence : COROLLARY
convergence(s, 0) IFF convergence(abs(s), 0)

  %----------------------------------
  %  Same properties with convergent
  %----------------------------------

  convergent_sum : LEMMA
convergent?(s1) AND convergent?(s2) IMPLIES convergent?(s1 + s2)

  convergent_neg : LEMMA
convergent?(s1) IMPLIES convergent?(-s1)

  convergent_diff : LEMMA
convergent?(s1) AND convergent?(s2) IMPLIES convergent?(s1 - s2)

  convergent_prod : LEMMA
convergent?(s1) AND convergent?(s2) IMPLIES convergent?(s1 * s2)

  convergent_const : LEMMA  convergent?(const_fun(a))

  convergent_scal : LEMMA
convergent?(s1) IMPLIES convergent?(a * s1)

  convergent_inv : LEMMA
convergent?(s3) AND limit(s3) /= 0 IMPLIES convergent?(1 / s3)

  convergent_div : LEMMA
convergent?(s1) AND convergent?(s3) AND limit(s3) /= 0
IMPLIES convergent?(s1 / s3)

  convergent_abs : LEMMA
convergent?(s1) IMPLIES convergent?(abs(s1))

  squeezing_abs_0 : LEMMA               % BUTLER
      convergence(s1, 0)
     AND (FORALL n : abs(s(n)) <= s1(n))
IMPLIES convergence(s, 0)

  squeezing_abs_0_gen : LEMMA            % BUTLER
      (convergence(s1, 0)
     AND (EXISTS N: (FORALL n : n >= N IMPLIES abs(s(n)) <= s1(n))))
IMPLIES convergence(s, 0)

  %---------------------------------
  %  Types of convergent sequences
  %---------------------------------

  v1, v2 : VAR (convergent?)

  u : VAR { s3 | convergent?(s3) }

  convergent_nz?(u) : bool = limit(u) /= 0

  v3 : VAR (convergent_nz?)

  %--------------
  %  Judgements
  %--------------

  constant_seq1: JUDGEMENT const_fun(a) HAS_TYPE (convergent?)

  constant_seq2: JUDGEMENT const_fun(b: nzreal) HAS_TYPE (convergent_nz?)

  conv_seq_plus:  JUDGEMENT +(v1, v2) HAS_TYPE (convergent?)

  conv_seq_minus: JUDGEMENT -(v1, v2) HAS_TYPE (convergent?)

  conv_seq_times: JUDGEMENT *(v1, v2) HAS_TYPE (convergent?)

  conv_seq_scal: JUDGEMENT *(a, v1) HAS_TYPE (convergent?)

  conv_seq_neg: JUDGEMENT -(v1) HAS_TYPE (convergent?)

  conv_seq_abs: JUDGEMENT abs(v1) HAS_TYPE (convergent?)

  conv_seq_div1: JUDGEMENT /(v1, v3) HAS_TYPE (convergent?)

  conv_seq_div2: JUDGEMENT /(a, v3) HAS_TYPE (convergent?)

  %-----------------------------
  %  Combinations of sequences
  %-----------------------------

  limit_sum      : LEMMA limit(v1 + v2) = limit(v1) + limit(v2)

  limit_neg : LEMMA limit(- v1) = - limit(v1)

  limit_diff     : LEMMA limit(v1 - v2) = limit(v1) - limit(v2)

  limit_prod     : LEMMA limit(v1 * v2) = limit(v1) * limit(v2)

  limit_inv      : LEMMA limit(1 / v3) = 1 / limit(v3)

  limit_div      : LEMMA limit(v1 / v3) = limit(v1) / limit(v3)

  limit_const    : LEMMA limit(const_fun(a)) = a

  limit_scal     : LEMMA limit(a * v1) = a * limit(v1)

  limit_abs      : LEMMA limit(abs(v1)) = abs(limit(v1))

  %---------------------------------------------------
  %  Expansion of convergence (for computing limits)
  %---------------------------------------------------

  limit_equiv : LEMMA
convergence(s, l) IFF convergent?(s) AND limit(s) = l

  limit_order : PROPOSITION
                convergence(s1, l1) AND convergence(s2, l2)
            AND (FORALL n : s1(n) <= s2(n))
        => l1 <= l2

%----------------------------------------------------------------------------
% NOTE: See "convergence_special" in lnexp library for convergence of
% sequences involving x^a where a is real
%
% NOTE: See "series" in series library for convergence of |x|^n and x^n
%----------------------------------------------------------------------------
END convergence_ops

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.