Quelle continuous_functions.pvs Sprache: PVS

%----------------------------------------------------------------------------
%  Continuous functions [ T -> real]
%
%  Defines:
%      continuous?(f, x0)                  ---- continuity at a point
%      continuous?(f, E)                   ---- continuity on a set
%
%  I some cases PVS has trouble disambiguating these, so the following are
%  defined which helps.  See cont_if_fun for an example.
%
%      continuous_at?(f, x0)               ---- continuity at a point
%      continuous_on?(f, E)                ---- continuity on a set
%
%
%
%----------------------------------------------------------------------------

continuous_functions [ T : TYPE FROM real ] : THEORY
BEGIN

  IMPORTING lim_of_functions

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

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

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

  continuous_at?(f, x0) : MACRO bool = continuous?(f, x0)

  %--- equivalent definitions ---%

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

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

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

  E: VAR setof[T]

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

  continuous_on_def: LEMMA
      continuous_on?(f, E) IFF FORALL (y: (E)): convergence(f, E, y, f(y))

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

  sum_continuous  : LEMMA continuous?(f1, x0) AND continuous?(f2, x0)
                           IMPLIES continuous?(f1 + f2, x0)

  diff_continuous : LEMMA continuous?(f1, x0) AND continuous?(f2, x0)
                           IMPLIES continuous?(f1 - f2, x0)

  prod_continuous : LEMMA continuous?(f1, x0) AND continuous?(f2, x0)
                           IMPLIES continuous?(f1 * f2, x0)

  const_continuous: LEMMA continuous?(const_fun(u), x0)

  scal_continuous : LEMMA continuous?(f, x0) IMPLIES continuous?(u * f, x0)

  neg_continuous  : LEMMA continuous?(f, x0) IMPLIES continuous?(- f, x0)

  div_continuous  : LEMMA continuous?(f, x0) AND continuous?(g, x0)
                            IMPLIES continuous?(f/g, x0)

  inv_continuous  : LEMMA continuous?(g, x0) IMPLIES continuous?(1/g, x0)

  identity_continuous: LEMMA continuous?(I[T], x0)

  expt_continuous : LEMMA continuous?(f, x0) IMPLIES continuous?(f^n, x0)

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

  F: VAR setof[real]

  %--- Operation preserving continuity in E ---%

  sum_set_continuous :  LEMMA continuous_on?(f1, E) AND continuous_on?(f2, E)
                               IMPLIES continuous_on?(f1 + f2, E)

  diff_set_continuous : LEMMA continuous_on?(f1, E) AND continuous_on?(f2, E)
                               IMPLIES continuous_on?(f1 - f2, E)

  prod_set_continuous : LEMMA continuous_on?(f1, E) AND continuous_on?(f2, E)
                               IMPLIES continuous_on?(f1 * f2, E)

  const_set_continuous: LEMMA continuous_on?(const_fun(u), E)

  scal_set_continuous : LEMMA continuous_on?(f, E) IMPLIES continuous_on?(u * f, E)

  neg_set_continuous  : LEMMA continuous_on?(f, E) IMPLIES continuous_on?(- f, E)

  div_set_continuous  : LEMMA continuous_on?(f, E) AND continuous_on?(g, E)
                              IMPLIES continuous_on?(f/g, E)

  inv_set_continuous  : LEMMA continuous_on?(g, E) IMPLIES continuous_on?(1/g, E)

  identity_set_continuous: LEMMA continuous_on?(I[T], E)


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

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

  continuous_def2: LEMMA continuous?(f) IFF continuous_on?(f, T_pred)

  continuity_subset2: LEMMA continuous?(f) IMPLIES continuous_on?(f, E)

  %--- Properties ---%

  continuous_fun: TYPE+ = { f | continuous?(f) }

  nz_continuous_fun: TYPE = { g | continuous?(g) }

  h, h1, h2: VAR continuous_fun
  h3: VAR nz_continuous_fun

  sum_fun_continuous : JUDGEMENT  +(h1, h2) HAS_TYPE continuous_fun

  diff_fun_continuous: JUDGEMENT  -(h1, h2) HAS_TYPE continuous_fun

  prod_fun_continuous: JUDGEMENT  *(h1, h2) HAS_TYPE continuous_fun

  const_fun_continuous: JUDGEMENT const_fun(u) HAS_TYPE continuous_fun

  scal_fun_continuous: JUDGEMENT  *(u, h) HAS_TYPE continuous_fun

  neg_fun_continuous  : JUDGEMENT -(h) HAS_TYPE continuous_fun

  div_fun_continuous : JUDGEMENT /(h, h3) HAS_TYPE continuous_fun

  id_fun_continuous  : JUDGEMENT I[T] HAS_TYPE continuous_fun

  inv_fun_continuous : LEMMA continuous?(1/h3)

  m,b: VAR real
  linear_fun_cont    : LEMMA continuous?(LAMBDA x: m*x + b) %% BUTLER

  one_over_x_cont    : LEMMA (FORALL x: x /= 0) IMPLIES
                                       continuous?((LAMBDA x: 1 / x))

  x_to_n_continuous  : LEMMA continuous?(LAMBDA x: x^n)   %% BUTLER

  expt_fun_continuous: LEMMA continuous?(f) IMPLIES continuous?(f^n)

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

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

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

  prod_cont_fun : LEMMA continuous?(f1) AND continuous?(f2)
                           IMPLIES continuous?(f1 * f2)

  const_cont_fun: LEMMA continuous?(const_fun(u))

  scal_cont_fun : LEMMA continuous?(f) IMPLIES continuous?(u * f)

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

  div_cont_fun  : LEMMA continuous?(f) AND continuous?(g)
                            IMPLIES continuous?(f/g)

  inv_cont_fun  : LEMMA continuous?(g) IMPLIES continuous?(1/g)

  identity_cont_fun: LEMMA continuous?(I[T])

%  id_cont_fun      : LEMMA continuous?(LAMBDA (t: posreal): t)

  expt_cont_fun    : LEMMA continuous?(f) IMPLIES continuous?(f^n)

END continuous_functions

quality94%

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