|
asin: THEORY
BEGIN
IMPORTING reals@sq, reals@sqrt
IMPORTING atan
% IMPORTING reals@prelude_aux_reals
IMPORTING analysis@sqrt_derivative, analysis@derivative_props, analysis@deriv_domains
% 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
noa_abs_lt1 : LEMMA not_one_element?[real_abs_lt1]
noa_nnreal_lt1 : LEMMA not_one_element?[{x: nnreal | x < 1}]
deriv_domain_abs_lt1 : LEMMA deriv_domain?[real_abs_lt1]
deriv_domain_nnreal_lt_1: LEMMA deriv_domain?[{x: nnreal | x < 1}]
AUTO_REWRITE+ noa_abs_lt1
AUTO_REWRITE+ deriv_domain_abs_lt1
AUTO_REWRITE+ deriv_domain_nnreal_lt_1
AUTO_REWRITE+ noa_nnreal_lt1
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_derivable_fun: 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: LEMMA px < asin(px) AND
(px*(1-px*px/6) > 0 => asin(px*(1-px*px/6)) < px)
END asin
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.0Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
