Quelle convergence_ops.pvs Sprache: 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

quality93%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.