|
%------------------------------------------------------------------------------
% nth roots of nnreals
%
% Author: David Lester, Manchester University & NIA
%
% Version 1.0 19/08/08 Initial version (DRL)
%
% (Note that we have the essentials of continuity proved, without
% using of defining these concepts. This means that the definition can
% be used stand-alone.)
%------------------------------------------------------------------------------
nn_root: THEORY
BEGIN
IMPORTING exponentiation_aux
x,x1,x2,y: VAR nnreal
epsilon, px,py,
delta: VAR posreal
pm,pn: VAR posnat
lt1x: VAR {r:posreal | r < 1}
gt1x: VAR {r:posreal | r > 1}
continuous_alt_hat: LEMMA EXISTS delta: FORALL x2: abs(x1-x2) < delta
=> abs(x1^pn-x2^pn) < epsilon
hat_bijective: LEMMA bijective?[nnreal,nnreal](lambda x: x^pn)
nn_root(x,pn):nnreal = inverse[nnreal,nnreal](lambda x: x^pn)(x)
nn_root_0n: LEMMA nn_root(0,pn) = 0
nn_root_1n: LEMMA nn_root(1,pn) = 1
nn_root_x1: LEMMA nn_root(x,1) = x
nn_root_strict_increasing: LEMMA x < y => nn_root(x,pn) < nn_root(y,pn)
nn_root_expt: LEMMA nn_root(x^pn,pn) = x
expt_nn_root: LEMMA nn_root(x,pn)^pn = x
nn_root_is_0: LEMMA nn_root(x,pn) = 0 IFF x = 0
nn_root_pos: LEMMA nn_root(px,pn) > 0
nn_root_gt1: LEMMA nn_root(x,pn) > 1 IFF x > 1
nn_root_lt1: LEMMA nn_root(x,pn) < 1 IFF x < 1
mult_nn_root: LEMMA nn_root(x*y,pn) = nn_root(x,pn)*nn_root(y,pn)
inv_nn_root: LEMMA nn_root(1/px,pn) = 1/nn_root(px,pn)
div_nn_root: LEMMA nn_root(x/py,pn) = nn_root(x,pn)/nn_root(py,pn)
nn_root_mult: LEMMA nn_root(x,pn*pm) = nn_root(nn_root(x,pn),pm)
nn_root_increasing: LEMMA pn < pm AND 0 < x AND x < 1 =>
nn_root(x,pn) < nn_root(x,pm)
nn_root_decreasing: LEMMA pn < pm AND 1 < x =>
nn_root(x,pn) > nn_root(x,pm)
nn_root_upper_bound: LEMMA nn_root(1+px,pn) <= 1+px/pn
nn_root_bijective: LEMMA bijective?[nnreal,nnreal](lambda x: nn_root(x,pn))
continuous_alt_nn_root: LEMMA EXISTS delta: FORALL x2: abs(x1-x2) < delta
=> abs(nn_root(x1,pn)-nn_root(x2,pn)) < epsilon
both_sides_nn_root_lt: LEMMA nn_root(x,pn) < nn_root(y,pn) IFF x < y
both_sides_nn_root_le: LEMMA nn_root(x,pn) <= nn_root(y,pn) IFF x <= y
both_sides_nn_root_gt: LEMMA nn_root(x,pn) > nn_root(y,pn) IFF x > y
both_sides_nn_root_ge: LEMMA nn_root(x,pn) >= nn_root(y,pn) IFF x >= y
both_sides_nn_root: LEMMA nn_root(x,pn) = nn_root(y,pn) IFF x = y
both_sides_nn_root_lt1_lt: LEMMA
nn_root(lt1x,pn) < nn_root(lt1x,pm) IFF pn < pm
both_sides_nn_root_lt1_le: LEMMA
nn_root(lt1x,pn) <= nn_root(lt1x,pm) IFF pn <= pm
both_sides_nn_root_lt1_gt: LEMMA
nn_root(lt1x,pn) > nn_root(lt1x,pm) IFF pn > pm
both_sides_nn_root_lt1_ge: LEMMA
nn_root(lt1x,pn) >= nn_root(lt1x,pm) IFF pn >= pm
both_sides_nn_root_gt1_lt: LEMMA
nn_root(gt1x,pn) < nn_root(gt1x,pm) IFF pm < pn
both_sides_nn_root_gt1_le: LEMMA
nn_root(gt1x,pn) <= nn_root(gt1x,pm) IFF pm <= pn
both_sides_nn_root_gt1_gt: LEMMA
nn_root(gt1x,pn) > nn_root(gt1x,pm) IFF pm > pn
both_sides_nn_root_gt1_ge: LEMMA
nn_root(gt1x,pn) >= nn_root(gt1x,pm) IFF pm >= pn
both_sides_nn_root_eq: LEMMA nn_root(x,pn) = nn_root(x,pm) IFF
x = 0 OR x = 1 OR pn = pm
END nn_root
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
