Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Brouwer_Fixpoint.thy Sprache: PVS

Original von: PVS^©

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  General convergence of functions [T -> real]  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

convergence_functions [T : TYPE FROM real] : THEORY
BEGIN

  IMPORTING reals@real_fun_ops, epsilon_lemmas

  epsilon, delta : VAR posreal
  e, e1, e2 : VAR posreal
  E, E1, E2 : VAR setof[real]
  f, f1, f2 : VAR [T -> real]
  g : VAR [T -> nzreal]
  l, l1, l2, a, b, z : VAR real
  x, y : VAR T

  %---------------------------
  %  Reals adherent to a set
  %---------------------------

  adh(E) : setof[real] =
{ z | FORALL e : EXISTS x : E(x) AND abs(x - z) < e }

  member_adherent : LEMMA   E(x) IMPLIES adh(E)(x)

  adherence_subset1 : LEMMA
subset?(E1, E2) AND adh(E1)(z) IMPLIES adh(E2)(z)

  adherence_subset2 : LEMMA
subset?(E1, E2) IMPLIES subset?(adh(E1), adh(E2))

  adherence_prop1 : LEMMA
FORALL e, E, (a : (adh(E))) :
     EXISTS x : E(x) AND abs(x - a) < e

  adherence_prop2 : LEMMA
FORALL e1, e2, E, (a : (adh(E))) :
     EXISTS x : E(x) AND abs(x - a) < e1 AND abs(x - a) < e2

  %------------------------------------------------------
  %  Definition of convergence and immediate properties
  %------------------------------------------------------

  convergence(f, E, a, l) : bool =
adh(E)(a) AND
FORALL epsilon : EXISTS delta :
     FORALL x : E(x) AND abs(x - a) < delta IMPLIES abs(f(x) - l) < epsilon

  convergence_unicity : LEMMA
FORALL E, f, a, l1, l2 :
     convergence(f, E, a, l1) AND convergence(f, E, a, l2)
        IMPLIES l1 = l2

  subset_convergence : LEMMA
subset?(E1, E2) IMPLIES
     FORALL f, (a : (adh(E1))), l :
         convergence(f, E2, a, l) IMPLIES convergence(f, E1, a, l)

  subset_convergence2 : LEMMA
FORALL E1, E2, f, (a : (adh(E1))), l :
     subset?(E1, E2) AND convergence(f, E2, a, l)
   IMPLIES convergence(f, E1, a, l)

  convergence_in_domain : LEMMA
FORALL f, x, l : E(x) AND convergence(f, E, x, l) IMPLIES l = f(x)

  %----------------------------------
  %  Limits and function operations
  %----------------------------------

  convergence_sum : LEMMA
FORALL E, f1, f2, a, l1, l2 :
  convergence(f1, E, a, l1)
     AND convergence(f2, E, a, l2)
        IMPLIES convergence(f1 + f2, E, a, l1 + l2)

  convergence_neg : LEMMA
FORALL E, f1, a, l1 :
  convergence(f1, E, a, l1)
        IMPLIES convergence(- f1, E, a, - l1)

  convergence_diff : LEMMA
FORALL E, f1, f2, a, l1, l2 :
  convergence(f1, E, a, l1)
     AND convergence(f2, E, a, l2)
        IMPLIES convergence(f1 - f2, E, a, l1 - l2)

  convergence_prod : LEMMA
FORALL E, f1, f2, a, l1, l2 :
  convergence(f1, E, a, l1)
     AND convergence(f2, E, a, l2)
        IMPLIES convergence(f1 * f2, E, a, l1 * l2)

  convergence_const : LEMMA
FORALL E, (a : (adh(E))), b : convergence(const_fun(b), E, a, b)

  convergence_scal : LEMMA
FORALL E, f1, a, l1, b :
  convergence(f1, E, a, l1)
IMPLIES convergence(b * f1, E, a, b * l1)

  convergence_inv : LEMMA
FORALL E, g, a, l1:
  convergence(g, E, a, l1)
     AND l1 /= 0
IMPLIES convergence(1/g, E, a, 1/l1)

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

  %---------------------
  %  Identity function
  %---------------------

  convergence_identity : LEMMA
FORALL E, (a : (adh(E))) : convergence(I[T], E, a, a)

  %-----------------------------
  %  Limit preserve order
  %-----------------------------

  convergence_order : LEMMA
FORALL E, f1, f2, a, l1, l2 :
  convergence(f1, E, a, l1)
     AND convergence(f2, E, a, l2)
     AND (FORALL x : E(x) IMPLIES f1(x) <= f2(x))
IMPLIES l1 <= l2


  %-------------------------------------------
  %  Bounds on function are bounds on limits
  %-------------------------------------------

  convergence_lower_bound : COROLLARY
FORALL E, f, b, a, l :
  convergence(f, E, a, l)
     AND (FORALL x : E(x) IMPLIES b <= f(x))
IMPLIES b <= l

  convergence_upper_bound : COROLLARY
FORALL E, f, b, a, l :
  convergence(f, E, a, l)
     AND (FORALL x : E(x) IMPLIES f(x) <= b)
IMPLIES l <= b

  %--------------------------
  %  Function constant on E
  %--------------------------

  convergence_locally_constant : LEMMA
FORALL E, f, b, (a : (adh(E))) :
     (FORALL x : E(x) IMPLIES f(x) = b)
IMPLIES convergence(f, E, a, b)


  %-------------
  %  Squeezing
  %-------------

  convergence_squeezing : LEMMA
FORALL f1, f2, f, a, l :
     convergence(f1, E, a, l) AND convergence(f2, E, a, l)
AND (FORALL x : E(x) IMPLIES f1(x) <= f(x) AND f(x) <= f2(x))
    IMPLIES
     convergence(f, E, a, l)

END convergence_functions

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