Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: limit_vect.pvs Sprache: PVS

Original von: PVS^©

limit_vect[n,m:posnat]: THEORY
BEGIN

  IMPORTING vectors@vectors,
            reals@abs_lems,
            analysis@epsilon_lemmas

  f, f1, f2: VAR [ Vector[n] -> Vector[m] ]
  a,b,x,v : VAR Vector[n]
  l,l1,l2 : VAR Vector[m]
  epsilon, delta : VAR posreal
  k : VAR real

  ;+(f1, f2)(v) : MACRO Vector[m] = f1(v) + f2(v)

  ;-(f)(v): MACRO Vector[m] = -f(v)

  ;-(f1, f2)(v) : MACRO Vector[m] = f1(v) - f2(v)

  ;*(k, f)(v) : MACRO Vector[m] = k*f(v)

  ;*(f1,f2)(v) : MACRO real = f1(v)*f2(v)

  const_fun(l)(x): Vector[m] = l

  %---------------------------------------------------
  %  Convergence of f at a point a towards a limit l
  %--------------------------------------------------

  convergence(f, a, l): bool =
FORALL epsilon : EXISTS delta :
     FORALL v: norm(v-a) < delta
                 IMPLIES norm(f(v) - l) < epsilon

  cv_unique : LEMMA
    convergence(f, a, l1) AND convergence(f, a, l2)
      IMPLIES l1 = l2

  cv_in_domain : LEMMA
    convergence(f, a, l)
      IMPLIES l = f(a)

  %-------------------------------------------
  %  convergence and operations on functions
  %-------------------------------------------

  cv_sum   : LEMMA
    convergence(f1, a, l1) AND convergence(f2, a, l2)
      IMPLIES convergence(f1 + f2, a, l1 + l2)

  cv_neg   : LEMMA
    convergence(f, a, l)
      IMPLIES convergence(-f, a, -l)

  cv_diff  : LEMMA
    convergence(f1, a, l1) AND convergence(f2, a, l2)
      IMPLIES convergence(f1 - f2, a, l1 - l2)

  cv_const : LEMMA convergence(LAMBDA v: l, a, l)

  cv_scal  : LEMMA
    convergence(f, a, l)
      IMPLIES convergence(k*f, a, k*l)

  %-------------------------
  %  f is convergent at a
  %-------------------------

  convergent?(f, a) : bool = EXISTS l : convergence(f, a, l)

  lim(f, (x0 : {a | convergent?(f, a)})) : Vector[m] =
        choose(LAMBDA l : convergence(f, x0, l))

  lim_fun_lemma   : LEMMA FORALL f, (x0 : {a | convergent?(f, a)}) :
                          convergence(f, x0, lim(f, x0))

  lim_fun_def     : LEMMA FORALL f, l, (x0 : {a | convergent?(f, a)}) :
                             lim(f, x0) = l IFF convergence(f, x0, l)

  convergence_equiv    : LEMMA convergence(f, a, l) IFF
                                  convergent?(f, a) AND lim(f, a) = l

  convergent_in_domain : LEMMA convergent?(f, x) IFF convergence(f, x, f(x))

  lim_in_domain        : LEMMA convergent?(f, x) IMPLIES lim(f, x) = f(x)


%------------------------------------------
%  Operations preserving convergnce at a
%------------------------------------------

  sum_fun_convergent  : LEMMA convergent?(f1, a) AND convergent?(f2, a)
                                IMPLIES convergent?(f1 + f2, a)

  neg_fun_convergent : LEMMA convergent?(f, a) IMPLIES convergent?(- f, a)

  diff_fun_convergent : LEMMA convergent?(f1, a) AND convergent?(f2, a)
                                IMPLIES convergent?(f1 - f2, a)

%    prod_fun_convergent : LEMMA convergent?(f1, a) AND convergent?(f2, a)
%                                  IMPLIES convergent?(f1 * f2, a)

  const_fun_convergent: LEMMA convergent?(const_fun(l), a)

  scal_fun_convergent : LEMMA convergent?(f, a) IMPLIES convergent?(k * f, a)

  %----------------------------
  %  Same things with lim(a)
  %----------------------------
  lim_sum_fun      : LEMMA convergent?(f1, a) AND convergent?(f2, a)
                             IMPLIES lim(f1 + f2, a) = lim(f1, a) + lim(f2, a)

  lim_neg_fun : LEMMA convergent?(f, a)
                             IMPLIES lim(- f, a) = - lim(f, a)

  lim_diff_fun     : LEMMA convergent?(f1, a) AND convergent?(f2, a)
                             IMPLIES lim(f1 - f2, a) = lim(f1, a) - lim(f2, a)

%    lim_prod_fun     : LEMMA convergent?(f1, a) AND convergent?(f2, a)
%                               IMPLIES lim(f1 * f2, a) = lim(f1, a) * lim(f2, a)

  lim_const_fun    : LEMMA lim(const_fun(l), a) = l

   lim_scal_fun     : LEMMA convergent?(f, a)
                              IMPLIES lim(k * f, a) = k * lim(f, a)

END limit_vect

¤ 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.