Quelle  epsilon_lemmas.pvs

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Lemmas used for limits of product and inverse
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

epsilon_lemmas : THEORY
BEGIN

  x1, x2, y1, y2 : VAR real
  e, e1, e2 : VAR posreal

  IMPORTING reals@real_facts, reals@abs_lems

  %--- Lemmas for product ---%

  prod_bound : LEMMA
 abs(x1 - y1) < e1 AND abs(x2 - y2) < e2 IMPLIES 
 abs(x1 * x2 - y1 * y2) < e1 * e2 + abs(y1) * e2 + abs(y2) * e1

  prod_epsilon : LEMMA
 EXISTS e1, e2 : e1 * e2 + abs(y1) * e2 + abs(y2) * e1 < e


  %--- Lemmas for inverse ---%

  inv_bound : LEMMA
 abs(x1 - y1) < e1 and e1 < abs(y1) and x1 /= 0 and y1 /= 0 
 IMPLIES abs(1/x1 - 1/y1) < e1 / (abs(y1) * (abs(y1) - e1))

  inv_epsilon1 : LEMMA
 y1 /= 0 IMPLIES 
    EXISTS e1 : e1 < abs(y1) and e1 < e * (abs(y1) - e1)

  inv_epsilon : LEMMA 
 y1 /= 0  IMPLIES
    EXISTS e1 : e1 < abs(y1) 
     and e1 / (abs(y1) * (abs(y1) - e1)) < e


% Proof "By varying epsilon"
%
% A technique to get the inequalities to run the "wrong way" for
% epsilon. Can be used to give yourself a small extra quantity to play with
% in analysis proofs.
% 

  epsilon: VAR posreal
  x,y:     VAR real

  varying_epsilon: LEMMA x <= y <=> (FORALL epsilon: x <= y + epsilon)


END epsilon_lemmas