| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle trig_doc.pvs Sprache: PVS |
|||||||||
|
trig_doc: THEORY
%------------------------------------------------------------------------------ % % Much of the foundational development was based on % % Abramovitz and Stegun, "Handbook of Mathematical Functions" Dover. % 9th Edition (1972). % % Approach: % % (1) Define atan as an integral: % % atan(x) = Integral(0, x, (LAMBDA (x:real):1/(1+x*x))) % 4.4.3 % % % (2) Define atan, as having the same values as atan_value, but with % source (-pi/2,pi/2). % % (3) Prove it's a bijection. % % (4) Define asin and acos, proving that they are bijections also: % % asin(x:real_abs_le1): real_abs_le_pi2 = % IF x = -1 THEN -pi/2 ELSIF x < 1 % THEN atan(x/sqrt(1-x*x)) ELSE pi/2 ENDIF % % acos(x:real_abs_le1):nnreal_le_pi = pi/2 - asin(x) % % % (5) Take advantage of a new theorem about the derivative % of an inverse function (derivative_inverse in analysis). % % (6) Gradually expand the domain (source) of sin/cos definition from % (0,pi/4), firstly upto (0,2*pi) and then onto the whole real line. % % (7) After establishing the derivatives, prove the series properties using % Taylor's Theorem. % % % % Some of David Lester's thoughts about why this is a better way to go than % from infinite series definitions. % % (1) At the time I wasn't too happy about arguing about infinite series, % and felt that basing the result on something more concrete would be % more useful. % % (2) I think you run into some rather nasty and subtle circular reasoning % errors if you go down this route. The first problem will be to show % that $|sin(x)| <= 1$. Not circular, but not nice! % % (3) I've remembered: at some stage you're going to have to show that % (sin(x)/cos(x)) is bijective for x in the range (-pi/2,pi/2). % Now, you could define pi = 4*atan(1), but I think you'll run into % quite a few problems establishing the connections between these three % infinite series. % % Not quite circular reasoning (though I've been down quite a few of % those blind alleys recently!), but many of the results you think you % can rely on turn out to be unavailable for this reason. %------------------------------------------------------------------------------ BEGIN END trig_doc ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28