| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle deriv_sincos.pvs Sprache: PVS |
|||||||||
|
deriv_sincos[ T : TYPE FROM real ] : THEORY
%------------------------------------------------------------------------------ % Convenient forms of sin cos derivatives. % % Rick Butler 4/1/2010 %------------------------------------------------------------------------------ BEGIN ASSUMING IMPORTING analysis_ax@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_ax@chain_rule, analysis_ax@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_ax@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.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28