Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: lstlang1.sty Sprache: PVS

Original von: PVS^©

limit_real_vect2[ T : TYPE FROM real ]: THEORY
BEGIN

  IMPORTING vectors@distance_2D, vect_fun_ops_rv[T],
            reals@abs_lems

  f, f1, f2: VAR [ T -> Vect2]
  g : VAR [T -> Vect2]
  e, epsilon, delta : VAR posreal
  a,b,x: VAR T
  l,l1,l2,b,c,y1,y2,v: VAR Vect2

%   const_fun(v) : [T -> Vect2] = LAMBDA x : v ;

%   +(f1, f2) : [T -> Vect2] = LAMBDA x : f1(x) + f2(x);

%   -(f1)     : [T -> Vect2] = LAMBDA x : -f1(x);

%   -(f1, f2) : [T -> Vect2] = LAMBDA x : f1(x) - f2(x);

%    *(a, f2) : [T -> Vect2] = LAMBDA x : a * f2(x);

%%  *(f1, f2) : [real -> Vect2] = (LAMBDA x : f1(x) * f2(x));   %%% ???

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

  convergence(f, a, l) : bool =
%%        (FORALL e: EXISTS x: abs(x - a) < e) AND   % a has a ball containing T values
FORALL epsilon : EXISTS delta :
     FORALL x: abs(x-a) < delta
                 IMPLIES norm(f(x) - l) < epsilon

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

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

  %-------------------------------------------
  %  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(const_vfun(b), a, b)

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

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

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

  lim(f, (x0 : {a | convergent?(f, a)})) : Vect2 =
        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 convergence 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)

  const_fun_convergent: LEMMA convergent?(const_vfun(b), 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)

%   %-----------------------------
%   %  Limit preserve order
%   %-----------------------------

%   convergence_order : LEMMA
% FORALL f1, f2, a, l1, l2 :
% convergence(f1, a, l1)
%     AND convergence(f2, a, l2)
%     AND (FORALL x : f1(x) <= f2(x))
% IMPLIES l1 <= l2


%   %-------------------------------------------
%   %  Bounds on function are bounds on limits
%   %-------------------------------------------

%   convergence_lower_bound : COROLLARY
% FORALL f, b, a, l :
% convergence(f, a, l)
%     AND (FORALL x : b <= f(x))
% IMPLIES b <= l

%   convergence_upper_bound : COROLLARY
% FORALL f, b, a, l :
% convergence(f, a, l)
%     AND (FORALL x : f(x) <= b)
% IMPLIES l <= b

%   %--------------------
%   %  Bounds on limits
%   %--------------------

%   lim_le1 : LEMMA
%         convergent?(f, a) AND (FORALL x : f(x) <= b) IMPLIES lim(f, a) <= b

%   lim_ge1 : LEMMA
%         convergent?(f, a) AND (FORALL x : f(x) >= b) IMPLIES lim(f, a) >= b

%   lim_order1 : LEMMA convergent?(f1, a) AND convergent?(f2, a)
%                      AND (FORALL x : f1(x) <= f2(x))
%                          IMPLIES lim(f1, a) <= lim(f2, a)

END limit_real_vect2

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.