Quellcode-Bibliothek epsilon_lemmas.pvs Sprache: 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

quality93%

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

*Bot Zugriff

Versionsinformation zu Columbo

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders