|
%------------------------------------------------------------------------------
% Power function for nnx^nnq
%
% Author: David Lester, Manchester University & NIA
%
% Version 1.0 19/08/08 Initial version (DRL)
%------------------------------------------------------------------------------
nn_rational_expt: THEORY
BEGIN
IMPORTING rational_props_aux,
nn_root
x,y,z,x1,x2: VAR nnreal
px,py,epsilon,delta: VAR posreal
q,r: VAR nnrat
pq: VAR posrat
n: VAR nat
pn: VAR posnat
nn_rational_expt(x,q):nnreal = nn_root(expt(x,numerator(q)),denominator(q))
nn_rational_expt_nat_rew: LEMMA nn_rational_expt(x,n) = x^n
nn_rational_expt_root_rew: LEMMA nn_rational_expt(x,1/pn) = nn_root(x,pn)
nn_rational_expt_rat_rew: LEMMA nn_rational_expt(x,n/pn) = nn_root(x^n,pn)
nn_rational_expt_strict_increasing: LEMMA x < y =>
nn_rational_expt(x,pq) < nn_rational_expt(y,pq)
nn_rational_expt_0q: LEMMA nn_rational_expt(0,q)
= IF q = 0 THEN 1 ELSE 0 ENDIF
nn_rational_expt_1q: LEMMA nn_rational_expt(1,q) = 1
nn_rational_expt_x1: LEMMA nn_rational_expt(x,1) = x
nn_rational_expt_is_0: LEMMA nn_rational_expt(x,q) = 0 IFF x = 0 AND q /= 0
nn_rational_expt_pos: LEMMA nn_rational_expt(px,q) > 0
nn_rational_expt_gt1: LEMMA nn_rational_expt(x,pq) > 1 IFF x > 1
nn_rational_expt_lt1: LEMMA nn_rational_expt(x,pq) < 1 IFF x < 1
mult_nn_rational_expt: LEMMA nn_rational_expt(x*y,q)
= nn_rational_expt(x,q)*nn_rational_expt(y,q)
inv_nn_rational_expt: LEMMA nn_rational_expt(1/px,q)
= 1/nn_rational_expt(px,q)
div_nn_rational_expt: LEMMA nn_rational_expt(x/py,q)
= nn_rational_expt(x,q)/nn_rational_expt(py,q)
nn_rational_expt_plus: LEMMA nn_rational_expt(x,q+r)
= nn_rational_expt(x,q)*nn_rational_expt(x,r)
nn_rational_expt_times:LEMMA nn_rational_expt(x,q*r)
= nn_rational_expt(nn_rational_expt(x,q),r)
nn_rational_expt_decreasing: LEMMA q < r AND 0 < x AND x < 1 =>
nn_rational_expt(x,q) > nn_rational_expt(x,r)
nn_rational_expt_increasing: LEMMA q < r AND 1 < x =>
nn_rational_expt(x,q) < nn_rational_expt(x,r)
nn_rational_expt_def: LEMMA
nn_rational_expt(x,q) = expt(nn_root(x,denominator(q)),numerator(q))
continuous_alt_nn_rational_expt: LEMMA
EXISTS delta: FORALL x2: abs(x1-x2) < delta
=> abs(nn_rational_expt(x1,q)-nn_rational_expt(x2,q)) < epsilon
nn_rational_expt_approx_gt1: LEMMA
x > 1 AND y > 1 => EXISTS q: abs(nn_rational_expt(x,q)-y) < epsilon
END nn_rational_expt
[ zur Elbe Produktseite wechseln0.2Quellennavigators
Analyse erneut starten
]
|
