Quelle  convergence_functions.pvs   Sprache: 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