|
asin: THEORY
BEGIN
IMPORTING reals@sq, reals@sqrt
IMPORTING atan
% IMPORTING analysis@sqrt_derivative, analysis@derivative_props
% real_abs_le1: NONEMPTY_TYPE = {x:real | abs(x) <= 1} CONTAINING 0
% real_abs_lt1: NONEMPTY_TYPE = {x:real | abs(x) < 1} CONTAINING 0
% real_abs_le_pi2: NONEMPTY_TYPE = {x:real | abs(x) <= pi/2} CONTAINING 0
real_abs_le1: NONEMPTY_TYPE = {x:real | -1 <= x AND x <= 1} CONTAINING 0
real_abs_lt1: NONEMPTY_TYPE = {x:real | -1 < x AND x < 1} CONTAINING 0
real_abs_le_pi2: NONEMPTY_TYPE = {x:real | -pi/2 <= x AND x <= pi/2} CONTAINING 0
x,y: VAR real_abs_le1
xne: VAR real_abs_lt1
nnx,nny: VAR {x:nnreal | x <= 1}
nx: VAR {x:real_abs_le1 | x < 0}
px: VAR {x:real_abs_le1 | 0 < x}
nx_gt1: VAR {x:negreal | -1 < x}
px_lt1: VAR {x:posreal | x < 1}
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
asin_neg_restrict: LEMMA asin(nx) = -pi/2 - atan(sqrt(1-nx*nx)/nx)
asin_pos_restrict: LEMMA asin(px) = pi/2 - atan(sqrt(1-px*px)/px)
asin_0: LEMMA asin(0) = 0
asin_sqrt_half: LEMMA asin(sqrt(1/2)) = pi/4
asin_1: LEMMA asin(1) = pi/2
asin_neg: LEMMA asin(-x) = -asin(x)
asin_minus1: LEMMA asin(-1) = -pi/2
asin_minus_sqrt_half: LEMMA asin(-sqrt(1/2)) = -pi/4
asin_strict_increasing: LEMMA strict_increasing?(asin)
asin_bij: LEMMA bijective?[real_abs_le1,real_abs_le_pi2](asin)
asin_diff: LEMMA % 4.4.32
asin(nnx)-asin(nny) = asin(nnx*(sqrt(1-sq(nny)))-nny*(sqrt(1-sq(nnx))))
% asin_derivable: LEMMA
% derivable[real_abs_lt1]((LAMBDA (x:real_abs_lt1):asin(x)),xne)
% asin_derivable2: LEMMA
% derivable[real_abs_lt1](LAMBDA (x:real_abs_lt1): asin(x))
% deriv_asin_fun: LEMMA deriv[real_abs_lt1](LAMBDA (x:real_abs_lt1): asin(x))
% = (LAMBDA (x:real_abs_lt1): 1/sqrt(1-sq(x)))
asin_pos_bnds: AXIOM px < asin(px) AND
(px*(1-px*px/6) > 0 => asin(px*(1-px*px/6)) < px)
END asin
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
