|
root: THEORY
% Computes nth root %
% Narkawicz 12/13 %
BEGIN
r,x,y: VAR real
n: VAR posnat
epsil,delta: VAR posreal
f,g : VAR [real->real]
nnr,nnx: VAR nnreal
m : VAR nat
mult_expt_pos: LEMMA
(x*y)^n = x^n*y^n
real_mult_cont: LEMMA
(FORALL (epsil,x): EXISTS (delta): FORALL (y):
abs(x-y)<delta IMPLIES abs(f(x)-f(y))<epsil) AND
(FORALL (epsil,x): EXISTS (delta): FORALL (y):
abs(x-y)<delta IMPLIES abs(g(x)-g(y))<epsil)
IMPLIES
(FORALL (epsil,x): EXISTS (delta): FORALL (y):
abs(x-y)<delta IMPLIES abs(f(x)*g(x)-f(y)*g(y))<epsil)
expt_increasing: LEMMA
nnr<=nnx IMPLIES nnr^m<=nnx^m
expt_cont: LEMMA
EXISTS (delta): FORALL (y):
abs(x-y)<=delta IMPLIES abs(x^n-y^n)<epsil
nn_root_exists: LEMMA
EXISTS (nnx): nnx^n=nnr
root_pos(nnr,n): {nnx|nnx^n=nnr}
root_real(r)(n|r>=0 OR odd?(n)): {x | (x=0 IFF r = 0) AND
(x>0 IFF r>0) AND
(x<0 IFF r<0) AND
(x>=0 IFF r>=0) AND
(x<=0 IFF r<=0) AND
x^n = r}
= IF r=0 THEN 0
ELSIF r>0 THEN root_pos(r,n)
ELSE -1*root_pos(-r,n) ENDIF
END root
¤ Dauer der Verarbeitung: 0.21 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.
|
