|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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.0 Sekunden
(vorverarbeitet)
¤
|
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.
|
