Quelle lim_of_functions.pvs Sprache: PVS

lim_of_functions [ T : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
%  Limit of a functions [T -> real] at a point a   %
%
%  Author:  Bruno Dutertre    Royal Holloway & Bedford New College
%----------------------------------------------------------------------------
BEGIN

  IMPORTING convergence_functions

  %------------------------------------------------
  %  Subtype of reals where the limit makes sense
  %------------------------------------------------

  a, b, l, l1, l2 : VAR real
  c : VAR (adh[T](fullset[real]))
  f, f1, f2 : VAR [ T -> real]
  g : VAR [T -> nzreal]
  epsilon, delta : VAR posreal
  x : VAR T

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

  convergence(f, a, l) : bool = convergence(f, fullset[real], a, l)

  convergence_def : LEMMA
        FORALL f, a, l :
            convergence(f, a, l)
        IFF
            adh[T](fullset[real])(a)
        AND FORALL epsilon : EXISTS delta :
                FORALL x : abs(x - a) < delta IMPLIES abs(f(x) - l) < epsilon

  adherence_fullset : LEMMA adh[T](fullset[real])(x)

  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_diff  : LEMMA convergence(f1, a, l1) AND convergence(f2, a, l2)
                     IMPLIES convergence(f1 - f2, a, l1 - l2)

  cv_prod  : LEMMA convergence(f1, a, l1) AND convergence(f2, a, l2)
                     IMPLIES convergence(f1 * f2, a, l1 * l2)

  cv_const : LEMMA convergence(const_fun(b), c, b)

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

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

  cv_div   : LEMMA convergence(f, a, l1) AND convergence(g, a, l2) AND l2 /= 0
                     IMPLIES convergence(f / g, a, l1 / l2)

  cv_inv   : LEMMA convergence(g, a, l) AND l /= 0
                     IMPLIES convergence(1 / g, a, 1 / l)

  cv_identity: LEMMA convergence(I[T], c, c)

  cv_abs   : LEMMA convergence(abs, c, abs(c))

  conv_0_0_abs: LEMMA convergence(f, 0, 0) IFF convergence(abs(f), 0, 0)

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

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

%  lim(f, (x0 : {a | convergent?(f, a)})) : real =
%        choose(LAMBDA l : convergence(f, x0, l))

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

  lim_e_del: LEMMA convergent?(f, a) IMPLIES
    (lim(f, a) = l IFF FORALL (e: posreal): EXISTS (del: posreal): FORALL (x: T):
                           abs(x-a) < del IMPLIES abs(f(x) - l) < e)

  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)

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

  const_fun_convergent: LEMMA convergent?(const_fun(b), c)

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

  inv_fun_convergent  : LEMMA convergent?(g, a) AND lim(g, a) /= 0
                                 IMPLIES convergent?(1/g, a)

  div_fun_convergent  : LEMMA convergent?(f, a) AND convergent?(g, a)
                                AND lim(g, a) /= 0 IMPLIES convergent?(f / g, a)

  convergent_identity : LEMMA convergent?(I[T], c)

  %----------------------------
  %  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(b), c) = b

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

  lim_inv_fun      : LEMMA convergent?(g, a) AND lim(g, a) /= 0
                             IMPLIES lim(1/g, a) = 1/lim(g, a)

  lim_div_fun  : LEMMA convergent?(f, a) AND convergent?(g, a) AND lim(g, a) /= 0
                             IMPLIES lim(f / g, a) = lim(f, a)/lim(g, a)

  lim_identity : LEMMA lim(I[T], c) = c


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

  E : VAR setof[real]

  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)

  lim_le2    : LEMMA convergent?(f, a) AND adh[T](E)(a) AND
                     (FORALL x : E(x) IMPLIES f(x) <= b)
                         IMPLIES lim(f, a) <= b

  lim_ge2    : LEMMA convergent?(f, a) AND adh[T](E)(a) AND
                     (FORALL x : E(x) IMPLIES f(x) >= b)
                         IMPLIES lim(f, a) >= b

  lim_order2 : LEMMA convergent?(f1, a) AND convergent?(f2, a)  AND adh[T](E)(a)
                     AND (FORALL x : E(x) IMPLIES f1(x) <= f2(x))
                         IMPLIES lim(f1, a) <= lim(f2, a)

  AUTO_REWRITE+ adherence_fullset

END lim_of_functions

quality96%

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