|
%------------------------------------------------------------------------------
% Appoximation results
%
% Author: David Lester, Manchester University
%
% Version 1.0 18/2/09 Initial Release Version
%------------------------------------------------------------------------------
appendix: THEORY
BEGIN
IMPORTING prelude_aux,
prelude_A4,
reals@sqrt
n,m: VAR nat
i,p,r: VAR int
pn,q: VAR posnat
px,py: VAR posreal
x,e1,e2: VAR real
lemma_A1: LEMMA m*m <= n AND n < (m+1)*(m+1) IFF m = floor(sqrt(n))
lemma_A2: LEMMA r = round(p/q) IFF (r-1/2)*q <= p AND p < (r+1/2)*q
lemma_A3: LEMMA i = floor(log2(px)) IFF 2^i <= px AND px < 2^(i+1)
lemma_A4: LEMMA e1 = 2^ -(n+floor(log2(pn))+2) AND e2 = 2^ -n AND
-1 < x AND x < 1 =>
x^pn-e2 < (x-e1)^pn AND x^pn-e2 < (x+e1)^pn AND
(x-e1)^pn < x^pn+e2 AND (x+e1)^pn < x^pn+e2
epsilon_log2_aux: LEMMA FORALL (n:posnat): EXISTS (p:nat): n < 2^p
epsilon_log2: LEMMA EXISTS (p:nat): 1/2^p < px
floor_sqrt_aux(n,m:nat): RECURSIVE nat =
(IF (m+1)*(m+1) <= n THEN 1+floor_sqrt_aux(n,m+1) ELSE 0 ENDIF)
MEASURE (LAMBDA n,m: (IF n >= (m+1)*(m+1) THEN n-m ELSE 0 ENDIF))
floor_sqrt(n:nat): nat = floor_sqrt_aux(n,0)
floor_sqrt_def: LEMMA floor_sqrt(n) = floor(sqrt(n))
floor_log2(n:posnat): RECURSIVE nat =
(IF n >= 2 THEN 1 + floor_log2(floor(n/2)) ELSE 0 ENDIF)
MEASURE (LAMBDA n:n)
floor_log2_def: LEMMA floor_log2(pn) = floor(log2(pn))
END appendix
¤ 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.
|
