Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/vect_analysis/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 5 kB

Quellcode-Bibliothek limit_vect3_real.pvs Sprache: PVS

limit_vect3_real: THEORY
BEGIN

  IMPORTING vectors@vect3_fun_ops,
            reals@abs_lems,
            analysis@epsilon_lemmas

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

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

  convergence(f, a, l) : bool =
FORALL epsilon : EXISTS delta :
     FORALL x: %%% 0 < norm(x-a) AND
                      norm(x-a) < delta          %% AND x in dom(f)
                 IMPLIES abs(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_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), v, b)

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

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

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

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

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

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

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

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

  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)

  %----------------------------
  %  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), v) = 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)

  %-----------------------------
  %  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_vect3_real

quality78%

¤ 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.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.