Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: cont_vect.pvs Sprache: PVS

Original von: PVS^©

cont_vect[n,m:posnat] : THEORY
%------------------------------------------------------------------------------
%  Continuous functions [ Vector[n] -> Vector[m] ]
%
%  Author: Cesar Munoz
%          Ricky Butler
%          NASA Langley Research Center  8/12/2009
%------------------------------------------------------------------------------
BEGIN

  IMPORTING vectors@vectors

  IMPORTING limit_vect[n,m]

  f, f1, f2,g    : VAR [Vector[n] -> Vector[m]]
  u              : VAR Vector[m]
  x, x0          : VAR Vector[n]
  epsilon, delta : VAR posreal

  %--------------------
  %  Continuity at x0
  %--------------------

  continuous_vv?(f, x0) : bool =
FORALL epsilon : EXISTS delta :
     FORALL x: norm(x-x0) < delta
                 IMPLIES norm(f(x) - f(x0)) < epsilon

  continuity_def : LEMMA
        continuous_vv?(f, x0) IFF convergence(f, x0, f(x0))

  continuity_def2 : LEMMA
        continuous_vv?(f, x0) IFF convergent?(f, x0)

%------------------------------------------
%  Operations preserving continuity at x0
%------------------------------------------

  sum_continuous_vv  : LEMMA continuous_vv?(f1, x0) AND continuous_vv?(f2, x0)
                           IMPLIES continuous_vv?(f1 + f2, x0)

  diff_continuous_vv : LEMMA continuous_vv?(f1, x0) AND continuous_vv?(f2, x0)
                           IMPLIES continuous_vv?(f1 - f2, x0)

  const_continuous_vv: LEMMA continuous_vv?(const_fun(u), x0)

%%  identity_continuous_vv: LEMMA continuous_vv?((LAMBDA(x):x),x0)

  neg_continuous_vv  : LEMMA continuous_vv?(f, x0) IMPLIES continuous_vv?(- f, x0)

%---------------------------------
%  Continuity of f in its domain
%---------------------------------

  continuous_vv?(f): bool = FORALL x0: continuous_vv?(f, x0)

%--- Properties ---%

  continuous_vv_fun: TYPE+ = { f | continuous_vv?(f) }

  nz_continuous_vv_fun: TYPE = { g | continuous_vv?(g) }

  h, h1, h2: VAR continuous_vv_fun
  h3: VAR nz_continuous_vv_fun

  sum_fun_continuous_vv : JUDGEMENT  +(h1, h2) HAS_TYPE continuous_vv_fun

  diff_fun_continuous_vv: JUDGEMENT  -(h1, h2) HAS_TYPE continuous_vv_fun

  const_fun_continuous_vv: JUDGEMENT const_fun(u) HAS_TYPE continuous_vv_fun

  neg_fun_continuous_vv : JUDGEMENT -(h) HAS_TYPE continuous_vv_fun

% ------------ Alternate forms and names for convenience ---------------

  sum_cont_fun  : LEMMA continuous_vv?(f1) AND continuous_vv?(f2)
                           IMPLIES continuous_vv?(f1 + f2)

  diff_cont_fun : LEMMA continuous_vv?(f1) AND continuous_vv?(f2)
                           IMPLIES continuous_vv?(f1 - f2)

  const_cont_fun: LEMMA continuous_vv?(const_fun(u))

  neg_cont_fun  : LEMMA continuous_vv?(f) IMPLIES continuous_vv?(-f)

%%  id_cont_fun   : LEMMA continuous_vv?((LAMBDA(x):x))

END cont_vect

¤ Dauer der Verarbeitung: 0.16 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.