| products/Sources/formale Sprachen/PVS/trig/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: atan.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
atan: THEORY
%------------------------------------------------------------------------------ % % Axiomatic atan % % David Lester Manchester University % %------------------------------------------------------------------------------ BEGIN IMPORTING reals@sq, reals@sigma, reals@sqrt IMPORTING reals@factorial % IMPORTING reals@harmonic_polynomials %,polynomial_deriv IMPORTING reals@binomial, reals@real_fun_preds % IMPORTING reals@polynomials %%% INCLUDING THIS CAUSES BUG %%% bin out of date when in complex lib posreal_ge1: NONEMPTY_TYPE = {x:real | x >= 1} CONTAINING 1 x,y: VAR real px,py: VAR posreal nx: VAR negreal nnx: VAR nnreal nzx: VAR nzreal n,m: VAR nat pn: VAR posnat IMPORTING trig_basic %% to get value of pi here % --- from sincos_def --- a: VAR real tan_value_TCC: AXIOM -pi/2 < a AND a < pi/2 IMPLIES Tan?(a) real_abs_lt_pi2: NONEMPTY_TYPE = {x | -pi/2 < x AND x < pi/2} CONTAINING 0 atan(x:real):real_abs_lt_pi2 % = atan_value(x) % non-A&S definitions pi_value: AXIOM pi = 4*atan(1) %%%%% RWB conflicts with trig_basic atan_strict_increasing: AXIOM strict_increasing?(atan) atan_bij : AXIOM bijective?[real,real_abs_lt_pi2](atan) atan_0 : AXIOM atan(0) = 0 atan_inv : AXIOM atan(1/px) = pi/2-atan(px) atan_inv_neg : AXIOM atan(1/nx) = -pi/2-atan(nx) % A&S defs acot(nzx:nzreal):nzreal = atan(1/nzx) % 4.4.8 atan_neg: AXIOM atan(-x) = -atan(x) % 4.4.16 acot_neg: LEMMA acot(-nzx) = -acot(nzx) % 4.4.19 atan_minus: AXIOM % 4.4.34 (-1 < x*y => atan(x)-atan(y) = atan((x-y)/(1+x*y))) AND (x*y < -1 & y > 0 => atan(x)-atan(y)+pi = atan((x-y)/(1+x*y))) AND (x*y < -1 & y < 0 => atan(x)-atan(y)-pi = atan((x-y)/(1+x*y))) atan_plus: LEMMA % 4.4.34 (x*y < 1 => atan(x)+atan(y) = atan((x+y)/(1-x*y))) AND (1 < x*y & y > 0 => atan(x)+atan(y)-pi = atan((x+y)/(1-x*y))) AND (1 < x*y & y < 0 => atan(x)+atan(y)+pi = atan((x+y)/(1-x*y))) atan_sub_swap : LEMMA x /= 0 AND y /= 0 IMPLIES atan(x/y)-atan(y/x) = atan((x^2-y^2)/(2*x*y)) % continuous_atan: LEMMA continuous[real](atan) % more non-A&S definitions atan_1: LEMMA atan(1) = 4*atan(1/5) - atan(1/239) atan_bnds: AXIOM px/(1+px*px) < atan(px) AND atan(px) < px pi_bnds: LEMMA 306/100 < pi AND pi < 319/100 % atan Taylor's Theorem atan_series_coef(n:nat):rat = ((-1)^n)/(2*n+1) atan_series_term(x:real):[nat->real] = (LAMBDA (n:nat): x^(2*n+1) * atan_series_coef(n)) atan_series_n(x:real,n:nat):real = sigma(0,n,atan_series_term(x)) atan_series: AXIOM abs(atan(x)-atan_series_n(x,n)) <= abs(x^(2*n+3))/(2*n+3) END atan %============================================================================ % IMPORTING analysis@derivatives, analysis@restrict2_deriv % IMPORTING analysis@derivative_props, analysis@fundamental_theorem % IMPORTING analysis@chain_rule, analysis@derivatives_more % IMPORTING analysis@continuous_functions_props, analysis@integral % one_over_one_plus_t_sq_cont: LEMMA continuous[real](atan_deriv_fn) % atan_def: LEMMA atan(x) = Integral(0,x,(LAMBDA (x:real):1/(1+x*x))) % 4.4.3 % deriv_atan_fun: LEMMA derivable(atan) AND % deriv(atan) = (LAMBDA (x:real): 1/(1+x*x)) % 4.4.54 % atanS(n:nat)(x:real):real = harmonic_poly_real(2*n+1,1,x) % atanD(n:nat)(x:real):real = (1+x*x)^(2*n+1) % atanF(n:nat)(i:nat ):int % = IF i > 2*n OR odd?(i) THEN 0 % ELSE (-1)^(i/2+n)*factorial(2*n)*C(2*n+1,i) ENDIF % atanN(n:nat):[real->real] = polynomial(atanF(n),2*n) % atan_taylors_prep1: LEMMA % abs(atanS(n)(x)) <= (1+x*x)^n * sqrt(1+x*x) % atan_taylors_prep2: LEMMA % (-1)^n*factorial(2*n)*atanS(n) = atanN(n) % atan_taylors_prep3: LEMMA % derivable_n_times(atanN(n),m) AND derivable_n_times(atanD(n),m) % atan_taylors_prep4: LEMMA % deriv(atanN(n)) % = IF n = 0 THEN const_fun(0) % ELSE polynomial(LAMBDA (i:nat): (i+1)*atanF(n)(i+1),2*n-1) % ENDIF % atan_taylors_prep5: LEMMA % deriv(atanD(n)) = (LAMBDA (x:real): (4*n+2)*x*(1+x*x)^(2*n)) % atan_taylors_prep6: LEMMA % deriv(deriv(atanN(n))) % = IF n = 0 THEN const_fun(0) % ELSE polynomial(LAMBDA (i:nat): (i+2)*(i+1)*atanF(n)(i+2),2*n-2) % ENDIF % atan_taylors_prep7: LEMMA FORALL (f:[real->real], g:[real->nzreal]): % derivable(f) AND derivable(g) IMPLIES % derivable(f/g^pn) AND deriv(f/g^pn) = (deriv(f)*g-pn*f*deriv(g))/(g^(pn+1)) % atan_taylors_prep8: LEMMA % deriv(deriv(atanN(n)/atanD(n))) = atanN(n+1)/atanD(n+1) % atan_series_prep4: LEMMA derivable_n_times(atanN(n)/atanD(n),2*m) % atan_series_prep5: LEMMA nderiv(2*m,atanN(n)/atanD(n))=atanN(n+m)/atanD(n+m) % atan_series_prep6: LEMMA % derivable_n_times(LAMBDA (x:real): 1/(1+x*x),2*n) AND % nderiv(2*n,LAMBDA (x:real): 1/(1+x*x)) = atanN(n)/atanD(n) % atan_nderiv: LEMMA % nderiv(n,atan) % = IF n = 0 THEN atan ELSIF even?(n) % THEN (deriv(atanN(n/2-1))*(LAMBDA (x:real): (1+x*x)) - % atanN(n/2-1)*(LAMBDA (x:real): (2*n-2)*x)) / % (atanD(n/2-1)*(LAMBDA (x:real): (1+x*x))) % ELSE atanN((n-1)/2)/atanD((n-1)/2) ENDIF % atan_nderiv_0: LEMMA % nderiv(n,atan)(0) % = IF even?(n) THEN 0 ELSE (-1)^((n-1)/2) * factorial(n-1) ENDIF % atan_n_times_derivable: LEMMA derivable_n_times(atan,n) % atan_series_prep7: LEMMA % abs(atanN(n)(x)) <= factorial(2*n)*(1+x*x)^(2*n+1) % atan_series_prep8: LEMMA abs(nderiv(2*n+1,atan)(x)) <= factorial(2*n) % atan_series_eqv: LEMMA % atan_series_n(x,n) = sigma(0,2*n+2, % LAMBDA (nn:nat): IF nn > 2*n+2 OR nn = 0 THEN 0 ELSE % nderiv(nn,atan)(0)*x^nn/factorial(nn) ENDIF) % atan_taylors: LEMMA (EXISTS (c: between(0,x)): % atan(x) = atan_series_n(x,n) % + nderiv(2*n+3,atan)(c)*x^(2*n+3)/factorial(2*n+3)) ¤ Dauer der Verarbeitung: 0.18 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.Bot Zugriff |
