|
deriv_sincos[ T : TYPE FROM real ] : THEORY
%------------------------------------------------------------------------------
% Convenient forms of sin cos derivatives.
%
% Rick Butler 4/1/2010
%------------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING analysis@deriv_domain
connected_domain: ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
deriv_domain: LEMMA deriv_domain?[T]
IMPORTING sincos, analysis@chain_rule, analysis@composition_continuous
a,b,t: VAR T
k,alpha: VAR real
sin_continuous: LEMMA
continuous?[T](LAMBDA (x: T): k * sin(alpha * x))
cos_continuous: LEMMA
continuous?[T](LAMBDA (x: T): k * cos(alpha * x))
sin_derivable: LEMMA
derivable?[T](LAMBDA (x: T): k * sin(alpha * x))
cos_derivable: LEMMA
derivable?[T](LAMBDA (x: T): k * cos(alpha * x))
IMPORTING analysis@derivatives_lam[T]
deriv_sin: LEMMA alpha /= 0 IMPLIES
deriv[T](LAMBDA (x:T): k*sin(alpha*x)) =
(LAMBDA (t: T): k*alpha*cos(alpha*t))
deriv_cos: LEMMA alpha /= 0 IMPLIES
deriv[T](LAMBDA (x:T): k*cos(alpha*x)) =
(LAMBDA (t: T): -k*alpha*sin(alpha*t))
END deriv_sincos
¤ Dauer der Verarbeitung: 0.16 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.
|
