|
sincos: THEORY
BEGIN
IMPORTING reals@quadratic
IMPORTING trig_basic, analysis@deriv_domain
AUTO_REWRITE- abs_0
AUTO_REWRITE- abs_nat
IMPORTING analysis@deriv_domains
x,x0: VAR real
e,px: VAR posreal
n: VAR nat
noa_nnreal_lt_pi2 : LEMMA not_one_element?[{x: nnreal | x < pi / 2}]
noa_real_lt_pi2 : LEMMA not_one_element?[real_abs_lt_pi2]
noa_posreal_lt_pi : LEMMA not_one_element?[posreal_lt_pi]
noa_nnreal_pi4_to_pi : LEMMA not_one_element?[{x: nnreal | pi / 4 <= x & x < pi}]
noa_posreal_pi2_to_pi : LEMMA not_one_element?[{x: posreal | pi / 2 <= x & x < pi}]
noa_nnreal_lt_pi4 : LEMMA not_one_element?[{x: nnreal | x < pi / 4}]
noa_mpi4_to_pi4 : LEMMA not_one_element?[{x: real | -pi / 4 < x & x < pi / 4}]
conn_nnreal_lt_p2 : LEMMA connected?[{x: nnreal | x < pi / 2}]
conn_nnreal_pi4_to_pi : LEMMA connected?[{x: nnreal | pi / 4 <= x & x < pi}]
conn_posreal_pi2_to_pi: LEMMA connected?[{x: posreal | pi / 2 <= x & x < pi}]
conn_nnreal_lt_pi4 : LEMMA connected?[{x: nnreal | x < pi / 4}]
deriv_domain_nnreal_lt_pi2 : LEMMA deriv_domain?[{x: nnreal | x < pi / 2}]
deriv_domain_real_abs_lt_pi2 : LEMMA deriv_domain?[real_abs_lt_pi2]
deriv_domain_posreal_pi2_to_pi: LEMMA deriv_domain?[{x: posreal | pi / 2 <= x & x < pi}]
deriv_domain_posreal_lt_pi : LEMMA deriv_domain?[posreal_lt_pi]
deriv_domain_nnreal_pi4_to_pi : LEMMA deriv_domain?[{x: nnreal | pi / 4 <= x & x < pi}]
deriv_domain_nnreal_lt_pi4 : LEMMA deriv_domain?[{x: nnreal | x < pi / 4}]
deriv_domain_mpi4_to_pi4 : LEMMA deriv_domain?[{x: real | -pi / 4 < x & x < pi / 4}]
AUTO_REWRITE+ noa_nnreal_lt_pi2
AUTO_REWRITE+ noa_real_lt_pi2
AUTO_REWRITE+ noa_posreal_lt_pi
AUTO_REWRITE+ noa_nnreal_pi4_to_pi
AUTO_REWRITE+ noa_posreal_pi2_to_pi
AUTO_REWRITE+ noa_nnreal_lt_pi4
AUTO_REWRITE+ noa_mpi4_to_pi4
AUTO_REWRITE+ conn_nnreal_lt_p2
AUTO_REWRITE+ conn_nnreal_pi4_to_pi
AUTO_REWRITE+ conn_posreal_pi2_to_pi
AUTO_REWRITE+ conn_nnreal_lt_pi4
AUTO_REWRITE+ deriv_domain_nnreal_lt_pi2
AUTO_REWRITE+ deriv_domain_real_abs_lt_pi2
AUTO_REWRITE+ deriv_domain_posreal_pi2_to_pi
AUTO_REWRITE+ deriv_domain_posreal_lt_pi
AUTO_REWRITE+ deriv_domain_nnreal_pi4_to_pi
AUTO_REWRITE+ deriv_domain_nnreal_lt_pi4
AUTO_REWRITE+ deriv_domain_mpi4_to_pi4
cos_ub: LEMMA cos(x) <= 1
sin_ub: LEMMA sin(px) < px
cos_lb: LEMMA 1-px*px/2 < cos(px)
sin_lb: LEMMA px-px*px*px/6 < sin(px)
cos_pos_bnds: LEMMA 1-px*px/2 < cos(px) AND cos(px) <= 1
sin_pos_bnds: LEMMA px-px*px*px/6 < sin(px) AND sin(px) < px
sin_convergence : LEMMA convergence(NQ(sin,x),0,cos(x))
sin_derivable : LEMMA derivable?(sin,x)
sin_derivable_fun: LEMMA derivable?(sin)
deriv_sin_fun : LEMMA deriv(sin) = cos
cos_convergence : LEMMA convergence(NQ(cos,x),0,-sin(x))
cos_derivable : LEMMA derivable?(cos,x)
cos_derivable_fun: LEMMA derivable?(cos)
deriv_cos_fun : LEMMA deriv(cos) = -sin
sin_continuous : LEMMA continuous?(sin,x0)
cos_continuous : LEMMA continuous?(cos,x0)
sin_cont_fun : LEMMA continuous?(sin)
cos_cont_fun : LEMMA continuous?(cos)
nderiv_sin_fun: LEMMA derivable_n_times?(sin,n) AND
nderiv(n,sin) = LAMBDA (x:real): sin((n*pi/2)+x)
nderiv_cos_fun: LEMMA derivable_n_times?(cos,n) AND
nderiv(n,cos) = LAMBDA (x:real): cos((n*pi/2)+x)
sin_series_term(x:real):[nat->real]
= (LAMBDA (n:nat): (-1)^n*x^(2*n+1)/factorial(2*n+1))
sin_series_n(x:real,n:nat):real
= sigma(0,n,LAMBDA (i:nat): IF i>n THEN 0 ELSE sin_series_term(x)(i) ENDIF)
cos_series_term(x:real):[nat->real]
= (LAMBDA (n:nat): IF n=0 THEN 1 ELSE (-1)^n*x^(2*n)/factorial(2*n) ENDIF)
cos_series_n(x:real,n:nat):real
= sigma(0,n,LAMBDA (i:nat): IF i>n THEN 0 ELSE cos_series_term(x)(i) ENDIF)
sin_taylors: LEMMA (EXISTS (c: between(0,x)):
sin(x) = sin_series_n(x,n)+nderiv(2*n+3,sin)(c)*x^(2*n+3)/factorial(2*n+3))
cos_taylors: LEMMA (EXISTS (c: between(0,x)):
cos(x) = cos_series_n(x,n)+nderiv(2*n+2,cos)(c)*x^(2*n+2)/factorial(2*n+2))
sin_series: LEMMA abs(sin(x)-sin_series_n(x,n))
<= abs(x^(2*n+3))/factorial(2*n+3)
cos_series: LEMMA abs(cos(x)-cos_series_n(x,n))
<= abs(x^(2*n+2))/factorial(2*n+2)
END sincos
¤ Dauer der Verarbeitung: 0.13 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.
|
