|
sincos: THEORY
BEGIN
IMPORTING sincos_def
IMPORTING analysis_ax@deriv_domains, analysis_ax@derivatives, analysis_ax@nth_derivatives,
analysis_ax@taylors
x,x0: VAR real
px: VAR posreal
n: VAR nat
% sin_convergence: LEMMA convergence(NQ(sin,x),0,cos(x))
sin_derivable : AXIOM derivable?(sin,x)
sin_derivable_fun : LEMMA derivable?(sin)
deriv_sin_fun : AXIOM deriv(sin) = cos
% cos_convergence: LEMMA convergence(NQ(cos,x),0,-sin(x))
cos_derivable : AXIOM derivable?(cos,x)
cos_derivable_fun : LEMMA derivable?(cos)
deriv_cos_fun : AXIOM deriv(cos) = -sin
sin_continuous : AXIOM continuous?(sin,x0)
cos_continuous : AXIOM continuous?(cos,x0)
sin_continuous_fun: LEMMA continuous?(sin)
cos_continuous_fun: LEMMA continuous?(cos)
nderiv_sin_fun : AXIOM derivable_n_times?(sin,n) AND
nderiv(n,sin) = LAMBDA (x:real): sin((n*pi/2)+x)
nderiv_cos_fun : AXIOM derivable_n_times?(cos,n) AND
nderiv(n,cos) = LAMBDA (x:real): cos((n*pi/2)+x)
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))
END sincos
¤ Dauer der Verarbeitung: 0.3 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.
|
