Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: epsilon_lemmas.pvs Sprache: PVS

Original von: 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

¤ 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.