|
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.19 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.
|
