|
%------------------------------------------------------------------------------
% Power function nnx^nny
%
% Author: David Lester, Manchester University & NIA
%
% Version 1.0 19/08/08 Initial version (DRL)
%------------------------------------------------------------------------------
nnreal_expt: THEORY
BEGIN
IMPORTING rational_props_aux,
nn_root,
nn_rational_expt
n: VAR nat
pn: VAR posnat
a,b,x,y,z: VAR nnreal
q: VAR nnrat
px,py,pa,pb,
delta,r,
epsilon: VAR posreal
nnreal_expt(x,y):nnreal
= IF y = 0 OR x = 1 THEN 1
ELSIF x < 1 THEN glb({z | EXISTS q: q <= y AND z = nn_rational_expt(x,q)})
ELSE lub({z | EXISTS q: q <= y AND z = nn_rational_expt(x,q)})
ENDIF
nnreal_expt_rat_rew: LEMMA nnreal_expt(x,q) = nn_rational_expt(x,q)
nnreal_expt_nat_rew: LEMMA nnreal_expt(x,n) = x^n
nnreal_expt_root_rew: LEMMA nnreal_expt(x,1/pn) = nn_root(x,pn)
nnreal_expt_0a: LEMMA nnreal_expt(0,a) = IF a = 0 THEN 1 ELSE 0 ENDIF
nnreal_expt_1a: LEMMA nnreal_expt(1,a) = 1
nnreal_expt_x1: LEMMA nnreal_expt(x,1) = x
nnreal_expt_pos: LEMMA nnreal_expt(px,a) > 0
nnreal_expt_is_0: LEMMA nnreal_expt(x,a) = 0 IFF x = 0 AND a /= 0
nnreal_expt_gt1: LEMMA nnreal_expt(x,pa) > 1 IFF x > 1
nnreal_expt_lt1: LEMMA nnreal_expt(x,pa) < 1 IFF x < 1
inv_nnreal_expt: LEMMA nnreal_expt(1/px,a) = 1/nnreal_expt(px,a)
mult_nnreal_expt: LEMMA nnreal_expt(x*y,a)
= nnreal_expt(x,a)*nnreal_expt(y,a)
div_nnreal_expt: LEMMA nnreal_expt(x/py,a)
= nnreal_expt(x,a)/nnreal_expt(py,a)
nnreal_expt_decreasing: LEMMA a < b AND 0 < x AND x < 1 =>
nnreal_expt(x,a) > nnreal_expt(x,b)
nnreal_expt_increasing: LEMMA a < b AND 1 < x =>
nnreal_expt(x,a) < nnreal_expt(x,b)
nnreal_expt_strict_increasing: LEMMA x < y =>
nnreal_expt(x,pa) < nnreal_expt(y,pa)
continuous_alt_nnreal_expt2: LEMMA
EXISTS delta: FORALL pb: abs(pa-pb) < delta
=> abs(nnreal_expt(x,pa)-nnreal_expt(x,pb)) < epsilon
ne1x: VAR {r | r /= 1}
gt1x: VAR {r | r > 1}
lt1x: VAR {r | r < 1}
nnreal_bijective1: LEMMA
bijective?[nnreal,{r | r>=1}](lambda y: nnreal_expt(gt1x,y))
nnreal_bijective2: LEMMA
bijective?[nnreal,{r | r<=1}](lambda y: nnreal_expt(lt1x,y))
nnreal_expt_def_gt1: LEMMA
nnreal_expt(gt1x,py)
= lub({z | EXISTS q: q < py AND z = nn_rational_expt(gt1x,q)})
nnreal_expt_plus: LEMMA nnreal_expt(x,a+b)= nnreal_expt(x,a)*nnreal_expt(x,b)
nnreal_expt_times: LEMMA nnreal_expt(x,a*b) = nnreal_expt(nnreal_expt(x,a),b)
END nnreal_expt
¤ Dauer der Verarbeitung: 0.25 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
