| 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 sincos_def.pvs Sprache: PVS |
|||||||||
|
sincos_def: THEORY
BEGIN IMPORTING reals@quadratic, reals@factorial, reals@sigma_nat IMPORTING trig_basic, taylor_help[real] x,x0: VAR real px: VAR posreal n: VAR nat cos_ub: LEMMA cos(x) <= 1 sin_ub: AXIOM sin(px) < px cos_lb: AXIOM 1-px*px/2 < cos(px) sin_lb: AXIOM px-px*px*px/6 < sin(px) cos_pos_bnds: LEMMA 1-px*px/2 < cos(px) AND cos(px) <= 1 sin_pos_bnds: LEMMA px-px*px*px/6 < sin(px) AND sin(px) < px sin_series_term(x:real):[nat->real] = (LAMBDA (n:nat): (-1)^n*x^(2*n+1)/factorial(2*n+1)) sin_series_n(x:real,n:nat):real = sigma(0,n,LAMBDA (i:nat): IF i>n THEN 0 ELSE sin_series_term(x)(i) ENDIF) cos_series_term(x:real):[nat->real] = (LAMBDA (n:nat): IF n=0 THEN 1 ELSE (-1)^n*x^(2*n)/factorial(2*n) ENDIF) cos_series_n(x:real,n:nat):real = sigma(0,n,LAMBDA (i:nat): IF i>n THEN 0 ELSE cos_series_term(x)(i) ENDIF) sin_series: AXIOM abs(sin(x)-sin_series_n(x,n)) <= abs(x^(2*n+3))/factorial(2*n+3) cos_series: AXIOM abs(cos(x)-cos_series_n(x,n)) <= abs(x^(2*n+2))/factorial(2*n+2) % THE FOLLOWING ARE IMPORTED TO MATCH trig_fnd IMPORTING asin, acos, atan a: VAR real sin_asin: AXIOM FORALL (x: trig_range): sin(asin(x)) = x cos_acos: AXIOM FORALL (x: trig_range): cos(acos(x)) = x tan_atan: AXIOM FORALL (x: trig_range): tan(atan(a)) = a asin_sin: AXIOM FORALL (x:real_abs_le_pi2): asin(sin(x)) = x acos_cos: AXIOM FORALL (x:nnreal_le_pi): acos(cos(x)) = x atan_tan: AXIOM FORALL (x:real_abs_lt_pi2): atan(tan(x)) = x END sincos_def ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28