| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig_fnd/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle integral_sincos.pvs Sprache: PVS |
|||||||||
|
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.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28