| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/power/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle nn_root.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% 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.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28