|
atan: THEORY
%------------------------------------------------------------------------------
%
% A foundational theory of atan(x) for the interval [0,pi/2]
%
% David Lester Manchester University
%
%------------------------------------------------------------------------------
BEGIN
% IMPORTING reals@prelude_aux_reals,
IMPORTING reals@sq, reals@sigma, reals@sqrt, reals@poly_rew
IMPORTING analysis@derivatives, analysis@restrict2_deriv, analysis@deriv_domains
IMPORTING analysis@derivative_props, analysis@fundamental_theorem
IMPORTING analysis@chain_rule, analysis@derivative_props % , analysis@derivatives_more
IMPORTING analysis@continuous_functions_props, analysis@integral
IMPORTING reals@factorial
IMPORTING analysis@nth_derivatives[real], analysis@taylors[real]
IMPORTING reals@harmonic_polynomials, analysis@polynomial_deriv
IMPORTING reals@binomial, analysis@indefinite_integral
AUTO_REWRITE- abs_0
AUTO_REWRITE- abs_nat
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
atan_deriv_fn(x:real):posreal = 1/(1+x*x)
one_over_one_plus_t_sq_cont: LEMMA continuous?[real](atan_deriv_fn)
atan_value(x:real):real = Integral[real](0,x,atan_deriv_fn)
atan_value_0 : LEMMA atan_value(0) = 0
atan_neg_value : LEMMA atan_value(-x) = -atan_value(x)
atan_inv_value : LEMMA atan_value(1/px) = 2*atan_value(1)-atan_value(px)
atan_inv_neg_value: LEMMA atan_value(1/nx) = -2*atan_value(1)-atan_value(nx)
atan_value_strict_increasing: LEMMA strict_increasing?(atan_value)
atan_value_minus_x1: LEMMA -1/py < x IMPLIES
atan_value(x)-atan_value(py) = atan_value((x-py)/(1+x*py))
atan_value_minus_x2: LEMMA x < -1/py IMPLIES
4*atan_value(1) + atan_value(x) - atan_value(py)
= atan_value((x-py)/(1+x*py))
atan_value_minus: LEMMA
(-1 < x*y => atan_value(x)-atan_value(y) = atan_value((x-y)/(1+x*y))) AND
(x*y < -1 & y > 0 => atan_value(x)-atan_value(y)+4*atan_value(1)
= atan_value((x-y)/(1+x*y))) AND
(x*y < -1 & y < 0 => atan_value(x)-atan_value(y)-4*atan_value(1)
= atan_value((x-y)/(1+x*y)))
pi:posreal = 4*atan_value(1)
% real_mpi_ppi: NONEMPTY_TYPE = {x:real | abs(x)<2*atan_value(1)} CONTAINING 0
% real_mpi_ppi: NONEMPTY_TYPE = {x:real | abs(x) < pi/2} CONTAINING 0
% real_abs_lt_pi2: NONEMPTY_TYPE = {x | abs(x) < pi/2} CONTAINING 0
real_abs_lt_pi2: NONEMPTY_TYPE = {x | -pi/2 < x AND x < pi/2} CONTAINING 0
% atan_abs_lt_pi2: JUDGEMENT atan(x) HAS_TYPE real_abs_lt_pi2
atan(x:real): real_abs_lt_pi2 = atan_value(x)
pi_value: LEMMA pi = 4*atan(1)
% non-A&S definitions
atan_strict_increasing: LEMMA strict_increasing?(atan)
atan_bij : LEMMA bijective?[real,real_abs_lt_pi2](atan)
atan_0 : LEMMA atan(0) = 0
atan_inv : LEMMA atan(1/px) = pi/2-atan(px)
atan_inv_neg : LEMMA atan(1/nx) = -pi/2-atan(nx)
% A&S defs
atan_def: LEMMA atan(x) = Integral(0,x,(LAMBDA (x:real):1/(1+x*x))) % 4.4.3
acot(nzx:nzreal):nzreal = atan(1/nzx) % 4.4.8
atan_neg: LEMMA atan(-x) = -atan(x) % 4.4.16
acot_neg: LEMMA acot(-nzx) = -acot(nzx) % 4.4.19
atan_minus: LEMMA % 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))
deriv_atan_fun: LEMMA derivable?(atan) AND
deriv(atan) = (LAMBDA (x:real): 1/(1+x*x)) % 4.4.54
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: LEMMA px/(1+px*px) < atan(px) AND atan(px) < px
pi_bnds: LEMMA 306/100 < pi AND pi < 319/100
% 5/26 < atan(1/5) < 1/5
% 239/57122 < atan(1/239) < 1/239
% 40/13-4/239 < pi < 16/5 - 4*239/57122
% atan Taylor's Theorem
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 %% bug %%
derivable_n_times?(atanN(n),m) AND derivable_n_times?(atanD(n),m)
atanN_derivable : LEMMA derivable?(atanN(n))
atanD_derivable : LEMMA derivable?(atanD(n))
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_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_n_increasing: LEMMA
FORALL (x,y:nnreal): x<=y AND y<=1 IMPLIES
atan_series_n(x,n) <= atan_series_n(y,n)
atan_series_n_a0: LEMMA
atan_series_n(0,n) = 0
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))
atan_series: LEMMA abs(atan(x)-atan_series_n(x,n)) <= abs(x^(2*n+3))/(2*n+3)
END atan
¤ Dauer der Verarbeitung: 0.20 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.
|
