|
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.1 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.
|
