Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: UniRtf2HtmlUnit1.pas Sprache: PVS

Original von: PVS^©

cont_vect2_real: THEORY
%------------------------------------------------------------------------------
%  Continuous functions [ Vect2 -> real]
%
%  Author: Rick Butler     NASA Langley Research Center  2/1/2009
%
%------------------------------------------------------------------------------
BEGIN

  IMPORTING limit_vect2_real

  f, f1, f2      : VAR [Vect2 -> real]
  g              : VAR [Vect2 -> nzreal]
  u              : VAR real
  x, x0          : VAR Vect2
  epsilon, delta : VAR posreal
  n              : VAR nat

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

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

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

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

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

  sum_continuous_vr  : LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)
                           IMPLIES continuous_vr?(f1 + f2, x0)

  diff_continuous_vr : LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)
                           IMPLIES continuous_vr?(f1 - f2, x0)

  prod_continuous_vr : LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)
                           IMPLIES continuous_vr?(f1 * f2, x0)

  const_continuous_vr: LEMMA continuous_vr?(const_fun(u), x0)

  scal_continuous_vr : LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(u * f, x0)

  neg_continuous_vr  : LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(- f, x0)

  div_continuous_vr  : LEMMA continuous_vr?(f, x0) AND continuous_vr?(g, x0)
                            IMPLIES continuous_vr?(f/g, x0)

  inv_continuous_vr  : LEMMA continuous_vr?(g, x0) IMPLIES continuous_vr?(1/g, x0)

  expt_continuous_vr : LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(f^n, x0)

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

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

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

  sum_cont_vr_fun  : LEMMA continuous_vr?(f1) AND continuous_vr?(f2)
                           IMPLIES continuous_vr?(f1 + f2)

  diff_cont_vr_fun : LEMMA continuous_vr?(f1) AND continuous_vr?(f2)
                           IMPLIES continuous_vr?(f1 - f2)

  prod_cont_vr_fun : LEMMA continuous_vr?(f1) AND continuous_vr?(f2)
                           IMPLIES continuous_vr?(f1 * f2)

  const_cont_vr_fun: LEMMA continuous_vr?(const_fun(u))

  scal_cont_vr_fun : LEMMA continuous_vr?(f) IMPLIES continuous_vr?(u * f)

  neg_cont_vr_fun  : LEMMA continuous_vr?(f) IMPLIES continuous_vr?(-f)

  div_cont_vr_fun  : LEMMA continuous_vr?(f) AND continuous_vr?(g)
                            IMPLIES continuous_vr?(f/g)

  inv_cont_vr_fun  : LEMMA continuous_vr?(g) IMPLIES continuous_vr?(1/g)

  expt_cont_vr_fun : LEMMA continuous_vr?(f) IMPLIES continuous_vr?(f^n)

  %--- Properties ---%

  continuous_vr_fun: TYPE+ = { f | continuous_vr?(f) }

  nz_continuous_vr_fun: TYPE = { g | continuous_vr?(g) }

  h, h1, h2: VAR continuous_vr_fun
  h3: VAR nz_continuous_vr_fun

  sum_fun_continuous_vr : JUDGEMENT  +(h1, h2) HAS_TYPE continuous_vr_fun

  diff_fun_continuous_vr: JUDGEMENT  -(h1, h2) HAS_TYPE continuous_vr_fun

  prod_fun_continuous_vr: JUDGEMENT  *(h1, h2) HAS_TYPE continuous_vr_fun

  const_fun_continuous_vr: JUDGEMENT const_fun(u) HAS_TYPE continuous_vr_fun

  scal_fun_continuous_vr: JUDGEMENT  *(u, h) HAS_TYPE continuous_vr_fun

  neg_fun_continuous_vr : JUDGEMENT -(h) HAS_TYPE continuous_vr_fun

  div_fun_continuous_vr : JUDGEMENT /(h, h3) HAS_TYPE continuous_vr_fun

  inv_fun_continuous_vr : LEMMA continuous_vr?(1/h3)

  expt_fun_continuous_vr: LEMMA continuous_vr?(f) IMPLIES continuous_vr?(f^n)

END cont_vect2_real

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.