Impressum 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

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.