| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle 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 ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28