|
integral_sincos[T : TYPE+ FROM real ] : THEORY
%------------------------------------------------------------------------------
% Convenient forms of sin cos integrals.
%
% 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
AUTO_REWRITE+ connected_domain
AUTO_REWRITE+ not_one_element
IMPORTING analysis@deriv_domain, deriv_sincos[T], analysis@fundamental_theorem[T]
k,alpha: VAR real
a,b: VAR T
sin_Integrable: LEMMA
Integrable?[T](a, b, LAMBDA (x: T): k * sin(alpha * x))
cos_Integrable: LEMMA
Integrable?[T](a, b, LAMBDA (x: T): k * cos(alpha * x))
Integral_sin: LEMMA alpha /= 0 IMPLIES
Integral[T](a,b, (LAMBDA (x:T): k*sin(alpha*x))) = -k/alpha*(cos(alpha*b) - cos(alpha*a))
Integral_cos: LEMMA alpha /= 0 IMPLIES
Integral[T](a,b, (LAMBDA (x:T): k*cos(alpha*x))) = k/alpha*(sin(alpha*b) - sin(alpha*a))
END integral_sincos
¤ 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.
|
